-- Mathlib/Topology/Gluing.lean
theorem image_inter (i j : D.J) :
    Set.range (𝖣.ι i) ∩ Set.range (𝖣.ι j) = Set.range (D.f i j ≫ 𝖣.ι _)

Proof state:
case h.mpr
D : GlueData
i j : D.J
x : ↑D.glued
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (D.f i j ≫ D.ι i)) →
    x ∈ Set.range ⇑(ConcreteCategory.hom (D.ι i)) ∩ Set.range ⇑(ConcreteCategory.hom (D.ι j))

Tactic:
rintro ⟨x, hx⟩

Result:
case h.mpr.intro
D : GlueData
i j : D.J
x✝ : ↑D.glued
x : ↑(D.V (i, j))
hx : (ConcreteCategory.hom (D.f i j ≫ D.ι i)) x = x✝
⊢ x✝ ∈ Set.range ⇑(ConcreteCategory.hom (D.ι i)) ∩ Set.range ⇑(ConcreteCategory.hom (D.ι j))

Proof state:
case h.mpr.intro
D : GlueData
i j : D.J
x✝ : ↑D.glued
x : ↑(D.V (i, j))
hx : (ConcreteCategory.hom (D.f i j ≫ D.ι i)) x = x✝
⊢ (ConcreteCategory.hom (D.ι i)) ((ConcreteCategory.hom (D.f i j)) x) = x✝

Tactic:
exact hx

Result:
no goals

Proof state:
case h.mpr.intro
D : GlueData
i j : D.J
x✝ : ↑D.glued
x : ↑(D.V (i, j))
hx : (ConcreteCategory.hom (D.f i j ≫ D.ι i)) x = x✝
⊢ (ConcreteCategory.hom (D.ι j)) ((ConcreteCategory.hom (D.f j i)) ((ConcreteCategory.hom (D.t i j)) x)) = x✝

Tactic:
rw [D.glue_condition_apply]

Result:
case h.mpr.intro
D : GlueData
i j : D.J
x✝ : ↑D.glued
x : ↑(D.V (i, j))
hx : (ConcreteCategory.hom (D.f i j ≫ D.ι i)) x = x✝
⊢ (ConcreteCategory.hom (D.ι i)) ((ConcreteCategory.hom (D.f i j)) x) = x✝

Proof state:
D : GlueData
i j : D.J
x₁ : ↑(D.U i)
x₂ : ↑(D.U j)
y : ↑(D.V (⟨i, x₁⟩.fst, ⟨j, x₂⟩.fst))
e₁ : (ConcreteCategory.hom (D.f ⟨i, x₁⟩.fst ⟨j, x₂⟩.fst)) y = ⟨i, x₁⟩.snd
eq₂ : (ConcreteCategory.hom (D.ι j)) x₂ = (ConcreteCategory.hom (D.ι i)) x₁
⊢ (ConcreteCategory.hom (D.f i j ≫ D.ι i)) y = (ConcreteCategory.hom (D.ι i)) x₁

Tactic:
simp [e₁]

Result:
no goals

Proof state:
case h.mp.intro.intro.intro.intro.intro
D : GlueData
i j : D.J
x₁ : ↑(D.U i)
x₂ : ↑(D.U j)
y : ↑(D.V (⟨i, x₁⟩.fst, ⟨j, x₂⟩.fst))
e₁ : (ConcreteCategory.hom (D.f ⟨i, x₁⟩.fst ⟨j, x₂⟩.fst)) y = ⟨i, x₁⟩.snd
eq₂ : (ConcreteCategory.hom (D.ι j)) x₂ = (ConcreteCategory.hom (D.ι i)) x₁
⊢ (ConcreteCategory.hom (D.ι i)) x₁ ∈ Set.range ⇑(ConcreteCategory.hom (D.f i j ≫ D.ι i))

Tactic:
exact ⟨y, by simp [e₁]⟩

Result:
no goals

Proof state:
case h.mpr.intro
D : GlueData
i j : D.J
x✝ : ↑D.glued
x : ↑(D.V (i, j))
hx : (ConcreteCategory.hom (D.f i j ≫ D.ι i)) x = x✝
⊢ x✝ ∈ Set.range ⇑(ConcreteCategory.hom (D.ι i)) ∩ Set.range ⇑(ConcreteCategory.hom (D.ι j))

Tactic:
refine ⟨⟨D.f i j x, hx⟩, ⟨D.f j i (D.t _ _ x), ?_⟩⟩

Result:
case h.mpr.intro
D : GlueData
i j : D.J
x✝ : ↑D.glued
x : ↑(D.V (i, j))
hx : (ConcreteCategory.hom (D.f i j ≫ D.ι i)) x = x✝
⊢ (ConcreteCategory.hom (D.ι j)) ((ConcreteCategory.hom (D.f j i)) ((ConcreteCategory.hom (D.t i j)) x)) = x✝

Proof state:
D : GlueData
i j : D.J
⊢ Set.range ⇑(ConcreteCategory.hom (D.ι i)) ∩ Set.range ⇑(ConcreteCategory.hom (D.ι j)) =
    Set.range ⇑(ConcreteCategory.hom (D.f i j ≫ D.ι i))

Tactic:
ext x

Result:
case h
D : GlueData
i j : D.J
x : ↑D.glued
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (D.ι i)) ∩ Set.range ⇑(ConcreteCategory.hom (D.ι j)) ↔
    x ∈ Set.range ⇑(ConcreteCategory.hom (D.f i j ≫ D.ι i))

Proof state:
case h.mp.intro.intro.intro.intro.intro
D : GlueData
i j : D.J
x : ↑D.glued
x₁ : ↑(D.U i)
eq₁ : (ConcreteCategory.hom (D.ι i)) x₁ = x
x₂ : ↑(D.U j)
eq₂ : (ConcreteCategory.hom (D.ι j)) x₂ = x
y : ↑(D.V (⟨i, x₁⟩.fst, ⟨j, x₂⟩.fst))
e₁ : (ConcreteCategory.hom (D.f ⟨i, x₁⟩.fst ⟨j, x₂⟩.fst)) y = ⟨i, x₁⟩.snd
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (D.f i j ≫ D.ι i))

Tactic:
substs eq₁

Result:
case h.mp.intro.intro.intro.intro.intro
D : GlueData
i j : D.J
x₁ : ↑(D.U i)
x₂ : ↑(D.U j)
y : ↑(D.V (⟨i, x₁⟩.fst, ⟨j, x₂⟩.fst))
e₁ : (ConcreteCategory.hom (D.f ⟨i, x₁⟩.fst ⟨j, x₂⟩.fst)) y = ⟨i, x₁⟩.snd
eq₂ : (ConcreteCategory.hom (D.ι j)) x₂ = (ConcreteCategory.hom (D.ι i)) x₁
⊢ (ConcreteCategory.hom (D.ι i)) x₁ ∈ Set.range ⇑(ConcreteCategory.hom (D.f i j ≫ D.ι i))

Proof state:
case h.mp.intro.intro.intro
D : GlueData
i j : D.J
x : ↑D.glued
x₁ : ↑(D.U i)
eq₁ : (ConcreteCategory.hom (D.ι i)) x₁ = x
x₂ : ↑(D.U j)
eq₂ : (ConcreteCategory.hom (D.ι j)) x₂ = x
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (D.f i j ≫ D.ι i))

Tactic:
obtain ⟨y, e₁, -⟩ := (D.ι_eq_iff_rel _ _ _ _).mp (eq₁.trans eq₂.symm)

Result:
case h.mp.intro.intro.intro.intro.intro
D : GlueData
i j : D.J
x : ↑D.glued
x₁ : ↑(D.U i)
eq₁ : (ConcreteCategory.hom (D.ι i)) x₁ = x
x₂ : ↑(D.U j)
eq₂ : (ConcreteCategory.hom (D.ι j)) x₂ = x
y : ↑(D.V (⟨i, x₁⟩.fst, ⟨j, x₂⟩.fst))
e₁ : (ConcreteCategory.hom (D.f ⟨i, x₁⟩.fst ⟨j, x₂⟩.fst)) y = ⟨i, x₁⟩.snd
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (D.f i j ≫ D.ι i))

Proof state:
case h
D : GlueData
i j : D.J
x : ↑D.glued
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (D.ι i)) ∩ Set.range ⇑(ConcreteCategory.hom (D.ι j)) ↔
    x ∈ Set.range ⇑(ConcreteCategory.hom (D.f i j ≫ D.ι i))

Tactic:
constructor

Result:
case h.mp
D : GlueData
i j : D.J
x : ↑D.glued
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (D.ι i)) ∩ Set.range ⇑(ConcreteCategory.hom (D.ι j)) →
    x ∈ Set.range ⇑(ConcreteCategory.hom (D.f i j ≫ D.ι i))

case h.mpr
D : GlueData
i j : D.J
x : ↑D.glued
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (D.f i j ≫ D.ι i)) →
    x ∈ Set.range ⇑(ConcreteCategory.hom (D.ι i)) ∩ Set.range ⇑(ConcreteCategory.hom (D.ι j))

Proof state:
case h.mp
D : GlueData
i j : D.J
x : ↑D.glued
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (D.ι i)) ∩ Set.range ⇑(ConcreteCategory.hom (D.ι j)) →
    x ∈ Set.range ⇑(ConcreteCategory.hom (D.f i j ≫ D.ι i))

Tactic:
rintro ⟨⟨x₁, eq₁⟩, ⟨x₂, eq₂⟩⟩

Result:
case h.mp.intro.intro.intro
D : GlueData
i j : D.J
x : ↑D.glued
x₁ : ↑(D.U i)
eq₁ : (ConcreteCategory.hom (D.ι i)) x₁ = x
x₂ : ↑(D.U j)
eq₂ : (ConcreteCategory.hom (D.ι j)) x₂ = x
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (D.f i j ≫ D.ι i))