-- Mathlib/Topology/FiberPartition.lean
lemma sigmaIsoHom_inj : Function.Injective (sigmaIsoHom f)

Proof state:
case mk.mk.intro.mk.mk.mk.intro.mk
S : Type u_1
Y : Type u_2
f : S → Y
inst✝ : TopologicalSpace S
w✝¹ : ↑(Set.range f)
val✝¹ : S
hx : val✝¹ ∈ ↑⟨(fun x => f ⁻¹' {↑x}) w✝¹, ⋯⟩
w✝ : ↑(Set.range f)
val✝ : S
hy : val✝ ∈ ↑⟨(fun x => f ⁻¹' {↑x}) w✝, ⋯⟩
h : val✝¹ = val✝
⊢ ⟨⟨(fun x => f ⁻¹' {↑x}) w✝¹, ⋯⟩, ⟨val✝¹, hx⟩⟩.fst = ⟨⟨(fun x => f ⁻¹' {↑x}) w✝, ⋯⟩, ⟨val✝, hy⟩⟩.fst

Tactic:
rw [Set.mem_preimage, Set.mem_singleton_iff] at hx hy

Result:
case mk.mk.intro.mk.mk.mk.intro.mk
S : Type u_1
Y : Type u_2
f : S → Y
inst✝ : TopologicalSpace S
w✝¹ : ↑(Set.range f)
val✝¹ : S
hx✝ : val✝¹ ∈ ↑⟨(fun x => f ⁻¹' {↑x}) w✝¹, ⋯⟩
hx : f val✝¹ = ↑w✝¹
w✝ : ↑(Set.range f)
val✝ : S
hy✝ : val✝ ∈ ↑⟨(fun x => f ⁻¹' {↑x}) w✝, ⋯⟩
hy : f val✝ = ↑w✝
h : val✝¹ = val✝
⊢ ⟨⟨(fun x => f ⁻¹' {↑x}) w✝¹, ⋯⟩, ⟨val✝¹, hx✝⟩⟩.fst = ⟨⟨(fun x => f ⁻¹' {↑x}) w✝, ⋯⟩, ⟨val✝, hy✝⟩⟩.fst

Proof state:
S : Type u_1
Y : Type u_2
f : S → Y
inst✝ : TopologicalSpace S
⊢ Injective ⇑(sigmaIsoHom f)

Tactic:
rintro ⟨⟨_, _, rfl⟩, ⟨_, hx⟩⟩ ⟨⟨_, _, rfl⟩, ⟨_, hy⟩⟩ h

Result:
case mk.mk.intro.mk.mk.mk.intro.mk
S : Type u_1
Y : Type u_2
f : S → Y
inst✝ : TopologicalSpace S
w✝¹ : ↑(Set.range f)
val✝¹ : S
hx : val✝¹ ∈ ↑⟨(fun x => f ⁻¹' {↑x}) w✝¹, ⋯⟩
w✝ : ↑(Set.range f)
val✝ : S
hy : val✝ ∈ ↑⟨(fun x => f ⁻¹' {↑x}) w✝, ⋯⟩
h :
  (sigmaIsoHom f) ⟨⟨(fun x => f ⁻¹' {↑x}) w✝¹, ⋯⟩, ⟨val✝¹, hx⟩⟩ =
    (sigmaIsoHom f) ⟨⟨(fun x => f ⁻¹' {↑x}) w✝, ⋯⟩, ⟨val✝, hy⟩⟩
⊢ ⟨⟨(fun x => f ⁻¹' {↑x}) w✝¹, ⋯⟩, ⟨val✝¹, hx⟩⟩ = ⟨⟨(fun x => f ⁻¹' {↑x}) w✝, ⋯⟩, ⟨val✝, hy⟩⟩

Proof state:
case mk.mk.intro.mk.mk.mk.intro.mk
S : Type u_1
Y : Type u_2
f : S → Y
inst✝ : TopologicalSpace S
w✝¹ : ↑(Set.range f)
val✝¹ : S
hx : val✝¹ ∈ ↑⟨(fun x => f ⁻¹' {↑x}) w✝¹, ⋯⟩
w✝ : ↑(Set.range f)
val✝ : S
hy : val✝ ∈ ↑⟨(fun x => f ⁻¹' {↑x}) w✝, ⋯⟩
h :
  (sigmaIsoHom f) ⟨⟨(fun x => f ⁻¹' {↑x}) w✝¹, ⋯⟩, ⟨val✝¹, hx⟩⟩ =
    (sigmaIsoHom f) ⟨⟨(fun x => f ⁻¹' {↑x}) w✝, ⋯⟩, ⟨val✝, hy⟩⟩
⊢ ⟨⟨(fun x => f ⁻¹' {↑x}) w✝¹, ⋯⟩, ⟨val✝¹, hx⟩⟩.fst = ⟨⟨(fun x => f ⁻¹' {↑x}) w✝, ⋯⟩, ⟨val✝, hy⟩⟩.fst

Tactic:
simp only [sigmaIsoHom_apply] at h

Result:
case mk.mk.intro.mk.mk.mk.intro.mk
S : Type u_1
Y : Type u_2
f : S → Y
inst✝ : TopologicalSpace S
w✝¹ : ↑(Set.range f)
val✝¹ : S
hx : val✝¹ ∈ ↑⟨(fun x => f ⁻¹' {↑x}) w✝¹, ⋯⟩
w✝ : ↑(Set.range f)
val✝ : S
hy : val✝ ∈ ↑⟨(fun x => f ⁻¹' {↑x}) w✝, ⋯⟩
h : val✝¹ = val✝
⊢ ⟨⟨(fun x => f ⁻¹' {↑x}) w✝¹, ⋯⟩, ⟨val✝¹, hx⟩⟩.fst = ⟨⟨(fun x => f ⁻¹' {↑x}) w✝, ⋯⟩, ⟨val✝, hy⟩⟩.fst

Proof state:
case mk.mk.intro.mk.mk.mk.intro.mk
S : Type u_1
Y : Type u_2
f : S → Y
inst✝ : TopologicalSpace S
w✝¹ : ↑(Set.range f)
val✝¹ : S
hx : val✝¹ ∈ ↑⟨(fun x => f ⁻¹' {↑x}) w✝¹, ⋯⟩
w✝ : ↑(Set.range f)
val✝ : S
hy : val✝ ∈ ↑⟨(fun x => f ⁻¹' {↑x}) w✝, ⋯⟩
h :
  (sigmaIsoHom f) ⟨⟨(fun x => f ⁻¹' {↑x}) w✝¹, ⋯⟩, ⟨val✝¹, hx⟩⟩ =
    (sigmaIsoHom f) ⟨⟨(fun x => f ⁻¹' {↑x}) w✝, ⋯⟩, ⟨val✝, hy⟩⟩
⊢ ⟨⟨(fun x => f ⁻¹' {↑x}) w✝¹, ⋯⟩, ⟨val✝¹, hx⟩⟩ = ⟨⟨(fun x => f ⁻¹' {↑x}) w✝, ⋯⟩, ⟨val✝, hy⟩⟩

Tactic:
refine Sigma.subtype_ext ?_ h

Result:
case mk.mk.intro.mk.mk.mk.intro.mk
S : Type u_1
Y : Type u_2
f : S → Y
inst✝ : TopologicalSpace S
w✝¹ : ↑(Set.range f)
val✝¹ : S
hx : val✝¹ ∈ ↑⟨(fun x => f ⁻¹' {↑x}) w✝¹, ⋯⟩
w✝ : ↑(Set.range f)
val✝ : S
hy : val✝ ∈ ↑⟨(fun x => f ⁻¹' {↑x}) w✝, ⋯⟩
h :
  (sigmaIsoHom f) ⟨⟨(fun x => f ⁻¹' {↑x}) w✝¹, ⋯⟩, ⟨val✝¹, hx⟩⟩ =
    (sigmaIsoHom f) ⟨⟨(fun x => f ⁻¹' {↑x}) w✝, ⋯⟩, ⟨val✝, hy⟩⟩
⊢ ⟨⟨(fun x => f ⁻¹' {↑x}) w✝¹, ⋯⟩, ⟨val✝¹, hx⟩⟩.fst = ⟨⟨(fun x => f ⁻¹' {↑x}) w✝, ⋯⟩, ⟨val✝, hy⟩⟩.fst

Proof state:
case mk.mk.intro.mk.mk.mk.intro.mk
S : Type u_1
Y : Type u_2
f : S → Y
inst✝ : TopologicalSpace S
w✝¹ : ↑(Set.range f)
val✝¹ : S
hx✝ : val✝¹ ∈ ↑⟨(fun x => f ⁻¹' {↑x}) w✝¹, ⋯⟩
hx : f val✝¹ = ↑w✝¹
w✝ : ↑(Set.range f)
val✝ : S
hy✝ : val✝ ∈ ↑⟨(fun x => f ⁻¹' {↑x}) w✝, ⋯⟩
hy : f val✝ = ↑w✝
h : val✝¹ = val✝
⊢ ⟨⟨(fun x => f ⁻¹' {↑x}) w✝¹, ⋯⟩, ⟨val✝¹, hx✝⟩⟩.fst = ⟨⟨(fun x => f ⁻¹' {↑x}) w✝, ⋯⟩, ⟨val✝, hy✝⟩⟩.fst

Tactic:
simp [← hx, ← hy, h]

Result:
no goals