Weird HEq goal

Stream: new members

[Gareth Ma]

Hi, I am not sure why the following yield a HEq goal that I can't seem to solve.

import Mathlib.Data.Finset.Basic
import Mathlib.Data.Fintype.Basic
import Mathlib.Data.Int.Interval

open Int Finset

def T (q a b : ℤ) : Finset (Ico 0 q) := univ.filter (fun x ↦ x.val ∈ Ico a b)

example {q a b : ℤ} :
    { x // x ∈ T q a b } ≃ Σ i : Ico a b, T q i.val i.val.succ where
  toFun := by
    intro ⟨x, h⟩
    use ⟨x.val, sorry⟩, ⟨x.val, sorry⟩, sorry
  invFun := by
    intro ⟨x, y⟩
    use ⟨y.val, sorry⟩, sorry
  left_inv := by intro; simp
  right_inv := by
    intro ⟨i, ⟨⟨x, y⟩, h⟩⟩
    simp
    use sorry, ?_
    congr 1
    · sorry
    · sorry

(Just the final sorry, where it has a HEq goal)

[Damiano Testa]

Does apply proof_irrel_heq work?

[Gareth Ma]

Ahh yes thanks

[Gareth Ma]

Why doesn't rw [heq_iff_eq] work then?

[Damiano Testa]

I have no idea: I found the proof using exact?...

[Gareth Ma]

what

[Damiano Testa]

exact? produces the correct lemma, plus some non-roundtripping filling. Luckily, apply comes to the rescue.

[Gareth Ma]

Ahh okay it works on this example because I minimised it, but in my actual use case it times out
apply? doesn't find anything useful either.

[Gareth Ma]

(My example involves Ico 0 q \x Ico 0 q and a few more conditions)

[Gareth Ma]

thanks, weird

[Kyle Miller]

If you use congr! 1 instead of congr 1, then it solves that last sorry for you. It knows about proof_irrel_heq.

[Gareth Ma]

Great thanks

[Gareth Ma]

In my use case it didn’t find it with exact? Because I forgot to congr first haha