I don't understand heq

Stream: general

[Kevin Buzzard]

Here's a self-contained extract from analysis/topology/topological.space_lean:

[Kevin Buzzard]

import analysis.topology.topological_space
open topological_space
universes u v w
variables {α : Type u} {β : Type v} {ι : Sort w} {a a₁ a₂ : α} {s s₁ s₂ : set α} {p p₁ p₂ : α → Prop}
variables [topological_space α]

lemma is_open_Union_orig {f : ι → set α} (h : ∀i, is_open (f i)) : is_open (⋃i, f i) :=
is_open_sUnion $ assume t ⟨i, (heq : t = f i)⟩, heq.symm ▸ h i

lemma is_open_Union' {f : ι → set α} (h : ∀i, is_open (f i)) : is_open (⋃i, f i) :=
begin
  refine is_open_sUnion _,
  intro t,
  intro Ht,
  cases Ht with i Hi,
  exact eq.symm Hi ▸ h i,
end

lemma is_open_Union'' {f : ι → set α} (h : ∀i, is_open (f i)) : is_open (⋃i, f i) :=
is_open_sUnion $ assume t ⟨i, (rfl : t = f i)⟩, eq.symm ▸ h i -- doesn't compile

[Kevin Buzzard]

well, the first lemma is the extract -- it's called is_open_Union in the actual file.

[Kevin Buzzard]

I should perhaps say lemma is_open_sUnion {s : set (set α)} (h : ∀t ∈ s, is_open t) : is_open (⋃₀ s)

[Kevin Buzzard]

So I realised I didn't really understand the mathlib proof of is_open_Union_orig (which is the proof given in the extract above, with its heq)

[Kevin Buzzard]

so I proved the lemma "in the same way", in tactic mode

[Kevin Buzzard]

and that's is_open_Union'

[Kevin Buzzard]

and everything works fine with eq

[Kevin Buzzard]

Oh -- got it:

[Kevin Buzzard]

lemma is_open_Union'' {f : ι → set α} (h : ∀i, is_open (f i)) : is_open (⋃i, f i) :=
is_open_sUnion $ assume t ⟨i, (eq : t = f i)⟩, eq.symm ▸ h i

[Kevin Buzzard]

What's with this heq in the mathlib version?

[Kevin Buzzard]

Oh!

[Kevin Buzzard]

Got it :-)

[Kevin Buzzard]

heq has nothing to do with heq, it's just a variable name :-)

[Kevin Buzzard]

Oh OK, so I do understand this particular use of heq, we're calling a variable by the same name as a Lean function :-)