[GOAL]
X : Type u_1
ι : Type u_2
Y : ι → Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : (i : ι) → TopologicalSpace (Y i)
inst✝ : Nonempty X
⊢ Function.Injective fun g => comp (sigmaMk g.fst) g.snd
[PROOFSTEP]
rintro ⟨i, g⟩ ⟨i', g'⟩ h
[GOAL]
case mk.mk
X : Type u_1
ι : Type u_2
Y : ι → Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : (i : ι) → TopologicalSpace (Y i)
inst✝ : Nonempty X
i : ι
g : C(X, Y i)
i' : ι
g' : C(X, Y i')
h :
  (fun g => comp (sigmaMk g.fst) g.snd) { fst := i, snd := g } =
    (fun g => comp (sigmaMk g.fst) g.snd) { fst := i', snd := g' }
⊢ { fst := i, snd := g } = { fst := i', snd := g' }
[PROOFSTEP]
obtain ⟨rfl, hg⟩ : i = i' ∧ HEq (⇑g) (⇑g') := Function.eq_of_sigmaMk_comp <| congr_arg FunLike.coe h
[GOAL]
case mk.mk.intro
X : Type u_1
ι : Type u_2
Y : ι → Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : (i : ι) → TopologicalSpace (Y i)
inst✝ : Nonempty X
i : ι
g g' : C(X, Y i)
h :
  (fun g => comp (sigmaMk g.fst) g.snd) { fst := i, snd := g } =
    (fun g => comp (sigmaMk g.fst) g.snd) { fst := i, snd := g' }
hg : HEq ↑g ↑g'
⊢ { fst := i, snd := g } = { fst := i, snd := g' }
[PROOFSTEP]
simpa using hg
