-- Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean
theorem ι_image_preimage_eq (i j : D.J) (U : Opens (D.U i).carrier) :
    (Opens.map (𝖣.ι j).base).obj ((D.ι_isOpenEmbedding i).isOpenMap.functor.obj U) =
      (opensFunctor (D.f j i)).obj
        ((Opens.map (𝖣.t j i).base).obj ((Opens.map (𝖣.f i j).base).obj U))

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ (Opens.map (D.ι j).base).obj (⋯.functor.obj U) =
    (opensFunctor (D.f j i)).obj ((Opens.map (D.t j i).base).obj ((Opens.map (D.f i j).base).obj U))

Tactic:
ext1

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ ↑((Opens.map (D.ι j).base).obj (⋯.functor.obj U)) =
    ↑((opensFunctor (D.f j i)).obj ((Opens.map (D.t j i).base).obj ((Opens.map (D.f i j).base).obj U)))

Proof state:
case h.h
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ Mono
    ((HasColimit.isoOfNatIso (D.diagramIso (forget C))).inv ≫ (preservesColimitIso (forget C) D.diagram.multispan).inv)

Tactic:
infer_instance

Result:
no goals

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ ⇑(ConcreteCategory.hom (D.t j i).base) ∘ ⇑(TopCat.Hom.hom (D.t i j).base) ''
      (⇑(ConcreteCategory.hom (D.f i j).base) ⁻¹' ↑U) =
    ⇑(ConcreteCategory.hom (D.f i j).base) ⁻¹' ↑U

case h.hf
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ Function.Bijective ⇑(ConcreteCategory.hom (D.t j i).base)

Tactic:
swap

Result:
case h.hf
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ Function.Bijective ⇑(ConcreteCategory.hom (D.t j i).base)

case h
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ ⇑(ConcreteCategory.hom (D.t j i).base) ∘ ⇑(TopCat.Hom.hom (D.t i j).base) ''
      (⇑(ConcreteCategory.hom (D.f i j).base) ⁻¹' ↑U) =
    ⇑(ConcreteCategory.hom (D.f i j).base) ⁻¹' ↑U

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ ⇑(ConcreteCategory.hom (D.t j i).base) ∘ ⇑(TopCat.Hom.hom (D.t i j).base) ''
      (⇑(ConcreteCategory.hom (D.f i j).base) ⁻¹' ↑U) =
    ⇑(ConcreteCategory.hom (D.f i j).base) ⁻¹' ↑U

Tactic:
change (D.t i j ≫ D.t j i).base '' _ = _

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ ⇑(ConcreteCategory.hom (D.t i j ≫ D.t j i).base) '' (⇑(ConcreteCategory.hom (D.f i j).base) ⁻¹' ↑U) =
    ⇑(ConcreteCategory.hom (D.f i j).base) ⁻¹' ↑U

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ ⇑(ConcreteCategory.hom (𝟙 (D.V (i, j))).base) '' (⇑(ConcreteCategory.hom (D.f i j).base) ⁻¹' ↑U) =
    ⇑(ConcreteCategory.hom (D.f i j).base) ⁻¹' ↑U

Tactic:
simp

Result:
no goals

Proof state:
case h.hf
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ Function.Bijective ⇑(ConcreteCategory.hom (D.t j i).base)

Tactic:
exact CategoryTheory.ConcreteCategory.bijective_of_isIso (C := TopCat) _

Result:
no goals

Proof state:
case h.h
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ Function.Injective
    (⇑(ConcreteCategory.hom (preservesColimitIso (forget C) D.diagram.multispan).inv) ∘
      ⇑(ConcreteCategory.hom (HasColimit.isoOfNatIso (D.diagramIso (forget C))).inv))

Tactic:
rw [← TopCat.coe_comp, ← TopCat.mono_iff_injective]

Result:
case h.h
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ Mono
    ((HasColimit.isoOfNatIso (D.diagramIso (forget C))).inv ≫ (preservesColimitIso (forget C) D.diagram.multispan).inv)

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ ⇑(ConcreteCategory.hom (D.t i j ≫ D.t j i).base) '' (⇑(ConcreteCategory.hom (D.f i j).base) ⁻¹' ↑U) =
    ⇑(ConcreteCategory.hom (D.f i j).base) ⁻¹' ↑U

Tactic:
rw [𝖣.t_inv]

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ ⇑(ConcreteCategory.hom (𝟙 (D.V (i, j))).base) '' (⇑(ConcreteCategory.hom (D.f i j).base) ⁻¹' ↑U) =
    ⇑(ConcreteCategory.hom (D.f i j).base) ⁻¹' ↑U

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ ⇑(ConcreteCategory.hom (D.toTopGlueData.t i j ≫ D.toTopGlueData.f j i)) ''
      (⇑(ConcreteCategory.hom (D.toTopGlueData.f i j)) ⁻¹' ↑U) =
    ⇑(ConcreteCategory.hom (D.f j i).base) ''
      (⇑(ConcreteCategory.hom (D.t j i).base) ⁻¹' (⇑(ConcreteCategory.hom (D.f i j).base) ⁻¹' ↑U))

Tactic:
dsimp

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ ⇑(TopCat.Hom.hom (D.f j i).base) ∘ ⇑(TopCat.Hom.hom (D.t i j).base) ''
      (⇑(ConcreteCategory.hom (D.f i j).base) ⁻¹' ↑U) =
    ⇑(ConcreteCategory.hom (D.f j i).base) ''
      (⇑(ConcreteCategory.hom (D.t j i).base) ⁻¹' (⇑(ConcreteCategory.hom (D.f i j).base) ⁻¹' ↑U))

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ ↑((Opens.map (D.ι j).base).obj (⋯.functor.obj U)) =
    ↑((opensFunctor (D.f j i)).obj ((Opens.map (D.t j i).base).obj ((Opens.map (D.f i j).base).obj U)))

Tactic:
dsimp only [Opens.map_coe, IsOpenMap.coe_functor_obj]

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ ⇑(ConcreteCategory.hom (D.ι j).base) ⁻¹' (⇑(ConcreteCategory.hom (D.ι i).base) '' ↑U) =
    ⇑(ConcreteCategory.hom (D.f j i).base) ''
      (⇑(ConcreteCategory.hom (D.t j i).base) ⁻¹' (⇑(ConcreteCategory.hom (D.f i j).base) ⁻¹' ↑U))