-- 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:
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.mapGlueData (forget C)).ι j)) ⁻¹'
      (⇑(ConcreteCategory.hom ((D.mapGlueData (forget C)).ι i)) '' ↑U) =
    ⇑(ConcreteCategory.hom (D.f j i).base) ''
      (⇑(ConcreteCategory.hom (D.t j i).base) ⁻¹' (⇑(ConcreteCategory.hom (D.f i j).base) ⁻¹' ↑U))

Tactic:
refine Eq.trans (D.toTopGlueData.preimage_image_eq_image' _ _ _) ?_

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.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))

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.mapGlueData (forget C)).ι j)) ⁻¹'
      (⇑(ConcreteCategory.hom (preservesColimitIso (forget C) D.diagram.multispan).inv) ∘
          ⇑(ConcreteCategory.hom (HasColimit.isoOfNatIso (D.diagramIso (forget C))).inv) ⁻¹'
        (⇑(ConcreteCategory.hom (D.gluedIso (forget C)).inv) ''
          (⇑(ConcreteCategory.hom ((D.mapGlueData (forget C)).ι i)) '' ↑U))) =
    ⇑(ConcreteCategory.hom (D.f j i).base) ''
      (⇑(ConcreteCategory.hom (D.t j i).base) ⁻¹' (⇑(ConcreteCategory.hom (D.f i j).base) ⁻¹' ↑U))

Tactic:
erw [Set.preimage_image_eq]

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.mapGlueData (forget C)).ι j)) ⁻¹'
      (⇑(ConcreteCategory.hom ((D.mapGlueData (forget C)).ι i)) '' ↑U) =
    ⇑(ConcreteCategory.hom (D.f j i).base) ''
      (⇑(ConcreteCategory.hom (D.t j i).base) ⁻¹' (⇑(ConcreteCategory.hom (D.f i j).base) ⁻¹' ↑U))

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))

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 (preservesColimitIso (forget C) D.diagram.multispan).inv) ∘
          ⇑(ConcreteCategory.hom (HasColimit.isoOfNatIso (D.diagramIso (forget C))).inv)) ∘
        ⇑(ConcreteCategory.hom ((D.mapGlueData (forget C)).ι j)) ⁻¹'
      (⇑(ConcreteCategory.hom (D.gluedIso (forget C)).inv) ∘ ⇑(ConcreteCategory.hom ((D.mapGlueData (forget C)).ι i)) ''
        ↑U) =
    ⇑(ConcreteCategory.hom (D.f j i).base) ''
      (⇑(ConcreteCategory.hom (D.t j i).base) ⁻¹' (⇑(ConcreteCategory.hom (D.f i j).base) ⁻¹' ↑U))

Tactic:
rw [Set.image_comp, Set.preimage_comp]

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.mapGlueData (forget C)).ι j)) ⁻¹'
      (⇑(ConcreteCategory.hom (preservesColimitIso (forget C) D.diagram.multispan).inv) ∘
          ⇑(ConcreteCategory.hom (HasColimit.isoOfNatIso (D.diagramIso (forget C))).inv) ⁻¹'
        (⇑(ConcreteCategory.hom (D.gluedIso (forget C)).inv) ''
          (⇑(ConcreteCategory.hom ((D.mapGlueData (forget C)).ι i)) '' ↑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)
⊢ ⇑(ConcreteCategory.hom ((D.mapGlueData (forget C)).ι j ≫ (D.gluedIso (forget C)).inv)) ⁻¹'
      (⇑(ConcreteCategory.hom ((D.mapGlueData (forget C)).ι i ≫ (D.gluedIso (forget C)).inv)) '' ↑U) =
    ⇑(ConcreteCategory.hom (D.f j i).base) ''
      (⇑(ConcreteCategory.hom (D.t j i).base) ⁻¹' (⇑(ConcreteCategory.hom (D.f i j).base) ⁻¹' ↑U))

Tactic:
erw [TopCat.coe_comp, TopCat.coe_comp, TopCat.coe_comp]

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 (preservesColimitIso (forget C) D.diagram.multispan).inv) ∘
          ⇑(ConcreteCategory.hom (HasColimit.isoOfNatIso (D.diagramIso (forget C))).inv)) ∘
        ⇑(ConcreteCategory.hom ((D.mapGlueData (forget C)).ι j)) ⁻¹'
      (⇑(ConcreteCategory.hom (D.gluedIso (forget C)).inv) ∘ ⇑(ConcreteCategory.hom ((D.mapGlueData (forget C)).ι i)) ''
        ↑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)
⊢ ⇑(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))

Tactic:
rw [← show _ = (𝖣.ι i).base from 𝖣.ι_gluedIso_inv (PresheafedSpace.forget _) i, ←
  show _ = (𝖣.ι j).base from 𝖣.ι_gluedIso_inv (PresheafedSpace.forget _) j]

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.mapGlueData (forget C)).ι j ≫ (D.gluedIso (forget C)).inv)) ⁻¹'
      (⇑(ConcreteCategory.hom ((D.mapGlueData (forget C)).ι i ≫ (D.gluedIso (forget C)).inv)) '' ↑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)
⊢ ⇑(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))

Tactic:
rw [Set.image_comp]

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)
⊢ ⇑(TopCat.Hom.hom (D.t i j).base) '' (⇑(ConcreteCategory.hom (D.f i j).base) ⁻¹' ↑U) =
    ⇑(ConcreteCategory.hom (D.t j i).base) ⁻¹' (⇑(ConcreteCategory.hom (D.f i j).base) ⁻¹' ↑U)

Tactic:
rw [Set.eq_preimage_iff_image_eq, ← Set.image_comp]

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 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)