-- Mathlib/Topology/Gluing.lean
theorem fromOpenSubsetsGlue_injective : Function.Injective (fromOpenSubsetsGlue U)

Proof state:
case intro.intro.mk.intro.intro.mk
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
i : (ofOpenSubsets U).J
x : ↑(of α)
hx : x ∈ U i
j : (ofOpenSubsets U).J
hy : x ∈ U j
⊢ (ofOpenSubsets U).Rel ⟨i, ⟨x, hx⟩⟩ ⟨j, ⟨x, hy⟩⟩

Tactic:
exact ⟨⟨⟨x, hx⟩, hy⟩, rfl, rfl⟩

Result:
no goals

Proof state:
case intro.intro.mk.intro.intro.mk
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
i : (ofOpenSubsets U).J
x : ↑(of α)
hx : x ∈ U i
j : (ofOpenSubsets U).J
y : ↑(of α)
hy : y ∈ U j
e : (U i).inclusion' ⟨x, hx⟩ = (U j).inclusion' ⟨y, hy⟩
⊢ (ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx⟩ = (ConcreteCategory.hom ((ofOpenSubsets U).ι j)) ⟨y, hy⟩

Tactic:
change x = y at e

Result:
case intro.intro.mk.intro.intro.mk
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
i : (ofOpenSubsets U).J
x : ↑(of α)
hx : x ∈ U i
j : (ofOpenSubsets U).J
y : ↑(of α)
hy : y ∈ U j
e : x = y
⊢ (ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx⟩ = (ConcreteCategory.hom ((ofOpenSubsets U).ι j)) ⟨y, hy⟩

Proof state:
case intro.intro.mk.intro.intro.mk
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
i : (ofOpenSubsets U).J
x : ↑(of α)
hx : x ∈ U i
j : (ofOpenSubsets U).J
y : ↑(of α)
hy : y ∈ U j
e : x = y
⊢ (ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx⟩ = (ConcreteCategory.hom ((ofOpenSubsets U).ι j)) ⟨y, hy⟩

Tactic:
subst e

Result:
case intro.intro.mk.intro.intro.mk
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
i : (ofOpenSubsets U).J
x : ↑(of α)
hx : x ∈ U i
j : (ofOpenSubsets U).J
hy : x ∈ U j
⊢ (ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx⟩ = (ConcreteCategory.hom ((ofOpenSubsets U).ι j)) ⟨x, hy⟩

Proof state:
case intro.intro.mk.intro.intro.mk
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
i : (ofOpenSubsets U).J
x : ↑(of α)
hx : x ∈ U i
j : (ofOpenSubsets U).J
y : ↑(of α)
hy : y ∈ U j
e :
  (ConcreteCategory.hom (fromOpenSubsetsGlue U)) ((ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx⟩) =
    (ConcreteCategory.hom (fromOpenSubsetsGlue U)) ((ConcreteCategory.hom ((ofOpenSubsets U).ι j)) ⟨y, hy⟩)
⊢ (ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx⟩ = (ConcreteCategory.hom ((ofOpenSubsets U).ι j)) ⟨y, hy⟩

Tactic:
rw [ι_fromOpenSubsetsGlue_apply, ι_fromOpenSubsetsGlue_apply] at e

Result:
case intro.intro.mk.intro.intro.mk
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
i : (ofOpenSubsets U).J
x : ↑(of α)
hx : x ∈ U i
j : (ofOpenSubsets U).J
y : ↑(of α)
hy : y ∈ U j
e : (U i).inclusion' ⟨x, hx⟩ = (U j).inclusion' ⟨y, hy⟩
⊢ (ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx⟩ = (ConcreteCategory.hom ((ofOpenSubsets U).ι j)) ⟨y, hy⟩

Proof state:
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
x y : ↑(ofOpenSubsets U).glued
e : (ConcreteCategory.hom (fromOpenSubsetsGlue U)) x = (ConcreteCategory.hom (fromOpenSubsetsGlue U)) y
⊢ x = y

Tactic:
obtain ⟨i, ⟨x, hx⟩, rfl⟩ := (ofOpenSubsets U).ι_jointly_surjective x

Result:
case intro.intro.mk
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
y : ↑(ofOpenSubsets U).glued
i : (ofOpenSubsets U).J
x : ↑(of α)
hx : x ∈ U i
e :
  (ConcreteCategory.hom (fromOpenSubsetsGlue U)) ((ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx⟩) =
    (ConcreteCategory.hom (fromOpenSubsetsGlue U)) y
⊢ (ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx⟩ = y

Proof state:
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
⊢ Function.Injective ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U))

Tactic:
intro x y e

Result:
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
x y : ↑(ofOpenSubsets U).glued
e : (ConcreteCategory.hom (fromOpenSubsetsGlue U)) x = (ConcreteCategory.hom (fromOpenSubsetsGlue U)) y
⊢ x = y

Proof state:
case intro.intro.mk
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
y : ↑(ofOpenSubsets U).glued
i : (ofOpenSubsets U).J
x : ↑(of α)
hx : x ∈ U i
e :
  (ConcreteCategory.hom (fromOpenSubsetsGlue U)) ((ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx⟩) =
    (ConcreteCategory.hom (fromOpenSubsetsGlue U)) y
⊢ (ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx⟩ = y

Tactic:
obtain ⟨j, ⟨y, hy⟩, rfl⟩ := (ofOpenSubsets U).ι_jointly_surjective y

Result:
case intro.intro.mk.intro.intro.mk
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
i : (ofOpenSubsets U).J
x : ↑(of α)
hx : x ∈ U i
j : (ofOpenSubsets U).J
y : ↑(of α)
hy : y ∈ U j
e :
  (ConcreteCategory.hom (fromOpenSubsetsGlue U)) ((ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx⟩) =
    (ConcreteCategory.hom (fromOpenSubsetsGlue U)) ((ConcreteCategory.hom ((ofOpenSubsets U).ι j)) ⟨y, hy⟩)
⊢ (ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx⟩ = (ConcreteCategory.hom ((ofOpenSubsets U).ι j)) ⟨y, hy⟩

Proof state:
case intro.intro.mk.intro.intro.mk
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
i : (ofOpenSubsets U).J
x : ↑(of α)
hx : x ∈ U i
j : (ofOpenSubsets U).J
hy : x ∈ U j
⊢ (ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx⟩ = (ConcreteCategory.hom ((ofOpenSubsets U).ι j)) ⟨x, hy⟩

Tactic:
rw [(ofOpenSubsets U).ι_eq_iff_rel]

Result:
case intro.intro.mk.intro.intro.mk
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
i : (ofOpenSubsets U).J
x : ↑(of α)
hx : x ∈ U i
j : (ofOpenSubsets U).J
hy : x ∈ U j
⊢ (ofOpenSubsets U).Rel ⟨i, ⟨x, hx⟩⟩ ⟨j, ⟨x, hy⟩⟩