-- Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean
theorem snd_invApp_t_app' (i j k : D.J) (U : Opens (pullback (D.f i j) (D.f i k)).carrier) :
    ∃ eq,
      (π₂⁻¹ i, j, k) U ≫ (D.t k i).c.app _ ≫ (D.V (k, i)).presheaf.map (eqToHom eq) =
        (D.t' k i j).c.app _ ≫ (π₁⁻¹ k, j, i) (unop _)

Proof state:
case h
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
⊢ (D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ≫
      (D.V (k, i)).presheaf.map (eqToHom ⋯) =
    (D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ≫
      (D.V (k, i)).presheaf.map (eqToHom ⋯).op ≫
        (D.V (k, i)).presheaf.map ((opensFunctor (pullback.fst (D.f k i) (D.f k j))).op.map (eqToHom ⋯)) ≫
          (D.V (k, i)).presheaf.map
            ((opensFunctor (pullback.fst (D.f k i) (D.f k j))).op.map
              ((Opens.map (D.t' k i j).base).map (eqToHom ⋯).unop).op)

Tactic:
simp_rw [← (𝖣.V (k, i)).presheaf.map_comp]

Result:
case h
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
⊢ (D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ≫
      (D.V (k, i)).presheaf.map (eqToHom ⋯) =
    (D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ≫
      (D.V (k, i)).presheaf.map
        ((eqToHom ⋯).op ≫
          (opensFunctor (pullback.fst (D.f k i) (D.f k j))).op.map (eqToHom ⋯) ≫
            (opensFunctor (pullback.fst (D.f k i) (D.f k j))).op.map
              ((Opens.map (D.t' k i j).base).map (eqToHom ⋯).unop).op)

Proof state:
case w
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
⊢ (Opens.map (D.t k i).base).op.obj (op (⋯.functor.obj U)) =
    op (⋯.functor.obj (unop (op ((Opens.map (D.t' k i j).base).toPrefunctor.1 (unop (op U))))))

Tactic:
dsimp only [Functor.op, Opens.map, IsOpenMap.functor, unop_op, Opens.coe_mk]

Result:
case w
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
⊢ op
      {
        carrier :=
          ⇑(ConcreteCategory.hom (D.t k i).base) ⁻¹'
            (⇑(ConcreteCategory.hom (pullback.snd (D.f i j) (D.f i k)).base) '' ↑U),
        is_open' := ⋯ } =
    op
      {
        carrier :=
          ⇑(ConcreteCategory.hom (pullback.fst (D.f k i) (D.f k j)).base) ''
            (⇑(ConcreteCategory.hom (D.t' k i j).base) ⁻¹' ↑U),
        is_open' := ⋯ }

Proof state:
case w.e_unop.e_carrier.refine_1
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
this :
  ⇑(TopCat.Hom.hom (pullback.snd (D.f i j) (D.f i k)).base) =
    ⇑(TopCat.Hom.hom (D.t k i).base) ∘
      ⇑(TopCat.Hom.hom (pullback.fst (D.f k i) (D.f k j)).base) ∘ ⇑(TopCat.Hom.hom (inv (D.t' k i j)).base)
x : ↑↑(pullback (D.f i j) (D.f i k))
⊢ (ConcreteCategory.hom (D.t' k i j).base) ((TopCat.Hom.hom (inv (D.t' k i j)).base) x) = x

Tactic:
rw [← ConcreteCategory.comp_apply, ← comp_base, IsIso.inv_hom_id, id_base,
  ConcreteCategory.id_apply]

Result:
no goals

Proof state:
case h
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
⊢ (D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ≫
      (D.V (k, i)).presheaf.map (eqToHom ⋯) =
    ((((D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ≫
            (pullback.fst (D.f k i) (D.f k j)).c.app
              (op ((Opens.map (D.t k i).base).obj ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)))) ≫
          (pullback (D.f k i) (D.f k j)).presheaf.map (eqToHom ⋯)) ≫
        (pullback (D.f k i) (D.f k j)).presheaf.map ((Opens.map (D.t' k i j).base).map (eqToHom ⋯).unop).op) ≫
      invApp (pullback.fst (D.f k i) (D.f k j)) ((Opens.map (D.t' k i j).base).toPrefunctor.1 U)

Tactic:
simp_rw [Category.assoc]

Result:
case h
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
⊢ (D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ≫
      (D.V (k, i)).presheaf.map (eqToHom ⋯) =
    (D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ≫
      (pullback.fst (D.f k i) (D.f k j)).c.app
          (op ((Opens.map (D.t k i).base).obj ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U))) ≫
        (pullback (D.f k i) (D.f k j)).presheaf.map (eqToHom ⋯) ≫
          (pullback (D.f k i) (D.f k j)).presheaf.map ((Opens.map (D.t' k i j).base).map (eqToHom ⋯).unop).op ≫
            invApp (pullback.fst (D.f k i) (D.f k j)) ((Opens.map (D.t' k i j).base).toPrefunctor.1 U)

Proof state:
case w.e_unop.e_carrier
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
this :
  ⇑(TopCat.Hom.hom (pullback.snd (D.f i j) (D.f i k)).base) =
    ⇑(TopCat.Hom.hom (D.t k i).base) ∘
      ⇑(TopCat.Hom.hom (pullback.fst (D.f k i) (D.f k j)).base) ∘ ⇑(TopCat.Hom.hom (inv (D.t' k i j)).base)
⊢ Set.image ⇑(TopCat.Hom.hom (inv (D.t' k i j)).base) = Set.preimage ⇑(ConcreteCategory.hom (D.t' k i j).base)

Tactic:
refine Set.image_eq_preimage_of_inverse ?_ ?_

Result:
case w.e_unop.e_carrier.refine_1
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
this :
  ⇑(TopCat.Hom.hom (pullback.snd (D.f i j) (D.f i k)).base) =
    ⇑(TopCat.Hom.hom (D.t k i).base) ∘
      ⇑(TopCat.Hom.hom (pullback.fst (D.f k i) (D.f k j)).base) ∘ ⇑(TopCat.Hom.hom (inv (D.t' k i j)).base)
⊢ Function.LeftInverse ⇑(ConcreteCategory.hom (D.t' k i j).base) ⇑(TopCat.Hom.hom (inv (D.t' k i j)).base)

case w.e_unop.e_carrier.refine_2
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
this :
  ⇑(TopCat.Hom.hom (pullback.snd (D.f i j) (D.f i k)).base) =
    ⇑(TopCat.Hom.hom (D.t k i).base) ∘
      ⇑(TopCat.Hom.hom (pullback.fst (D.f k i) (D.f k j)).base) ∘ ⇑(TopCat.Hom.hom (inv (D.t' k i j)).base)
⊢ Function.RightInverse ⇑(ConcreteCategory.hom (D.t' k i j).base) ⇑(TopCat.Hom.hom (inv (D.t' k i j)).base)

Proof state:
case w.e_unop.e_carrier.refine_2
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
this :
  ⇑(TopCat.Hom.hom (pullback.snd (D.f i j) (D.f i k)).base) =
    ⇑(TopCat.Hom.hom (D.t k i).base) ∘
      ⇑(TopCat.Hom.hom (pullback.fst (D.f k i) (D.f k j)).base) ∘ ⇑(TopCat.Hom.hom (inv (D.t' k i j)).base)
⊢ Function.RightInverse ⇑(ConcreteCategory.hom (D.t' k i j).base) ⇑(TopCat.Hom.hom (inv (D.t' k i j)).base)

Tactic:
intro x

Result:
case w.e_unop.e_carrier.refine_2
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
this :
  ⇑(TopCat.Hom.hom (pullback.snd (D.f i j) (D.f i k)).base) =
    ⇑(TopCat.Hom.hom (D.t k i).base) ∘
      ⇑(TopCat.Hom.hom (pullback.fst (D.f k i) (D.f k j)).base) ∘ ⇑(TopCat.Hom.hom (inv (D.t' k i j)).base)
x : ↑↑(pullback (D.f k i) (D.f k j))
⊢ (TopCat.Hom.hom (inv (D.t' k i j)).base) ((ConcreteCategory.hom (D.t' k i j).base) x) = x

Proof state:
case h.hU.intro.intro
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
y : ↑↑(pullback (D.f i j) (D.f i k))
⊢ (ConcreteCategory.hom (pullback.snd (D.f i j) (D.f i k) ≫ D.t i k).base) y ∈
    Set.range ⇑(ConcreteCategory.hom (pullback.fst (D.f k i) (D.f k j)).base)

Tactic:
use (inv (D.t' k i j)).base y

Result:
case h
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
y : ↑↑(pullback (D.f i j) (D.f i k))
⊢ (ConcreteCategory.hom (pullback.fst (D.f k i) (D.f k j)).base) ((ConcreteCategory.hom (inv (D.t' k i j)).base) y) =
    (ConcreteCategory.hom (pullback.snd (D.f i j) (D.f i k) ≫ D.t i k).base) y