-- Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean
theorem f_invApp_f_app (i j k : D.J) (U : Opens (D.V (i, j)).carrier) :
    (D.f_open i j).invApp _ U ≫ (D.f i k).c.app _ =
      (π₁ i, j, k).c.app (op U) ≫
        (π₂⁻¹ i, j, k) (unop _) ≫
          (D.V _).presheaf.map
            (eqToHom
              (by
                delta IsOpenImmersion.opensFunctor
                dsimp only [Functor.op, IsOpenMap.functor, Opens.map, unop_op]
                congr
                apply pullback_base))

Proof state:
case h.e'_3.h.h.e'_7
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(D.V (i, j))
this :
  ∀ (U : (Opens ↑↑(D.U i))ᵒᵖ),
    (D.f i j).c.app U ≫ (pullback.fst (D.f i j) (D.f i k)).c.app (op ((Opens.map (D.f i j).base).obj (unop U))) =
      ((D.f i k).c.app U ≫ (pullback.snd (D.f i j) (D.f i k)).c.app (op ((Opens.map (D.f i k).base).obj (unop U)))) ≫
        (pullback (D.f i j) (D.f i k)).presheaf.map (eqToHom ⋯)
⊢ (D.V (i, k)).presheaf.map
      ((homOfLE ⋯).op ≫
        (opensFunctor (pullback.snd (D.f i j) (D.f i k))).op.map
            (eqToHom ⋯ ≫ (Opens.map (pullback.fst (D.f i j) (D.f i k)).base).op.map (eqToHom ⋯)) ≫
          eqToHom ⋯) =
    𝟙
      (((TopCat.Presheaf.pushforward C (D.f i k).base).obj (D.V (i, k)).presheaf).obj
        (op ((opensFunctor (D.f i j)).obj U)))

Tactic:
erw [(D.V (i, k)).presheaf.map_id]

Result:
case h.e'_3.h.h.e'_7
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(D.V (i, j))
this :
  ∀ (U : (Opens ↑↑(D.U i))ᵒᵖ),
    (D.f i j).c.app U ≫ (pullback.fst (D.f i j) (D.f i k)).c.app (op ((Opens.map (D.f i j).base).obj (unop U))) =
      ((D.f i k).c.app U ≫ (pullback.snd (D.f i j) (D.f i k)).c.app (op ((Opens.map (D.f i k).base).obj (unop U)))) ≫
        (pullback (D.f i j) (D.f i k)).presheaf.map (eqToHom ⋯)
⊢ 𝟙 ((D.V (i, k)).presheaf.obj (op ((Opens.map (D.f i k).base).obj (unop (op ((opensFunctor (D.f i j)).obj U)))))) =
    𝟙
      (((TopCat.Presheaf.pushforward C (D.f i k).base).obj (D.V (i, k)).presheaf).obj
        (op ((opensFunctor (D.f i j)).obj U)))

Proof state:
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(D.V (i, j))
⊢ op
      ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj
        (unop (op ((Opens.map (pullback.fst (D.f i j) (D.f i k)).base).toPrefunctor.1 (unop (op U)))))) =
    (Opens.map (D.f i k).base).op.obj (op ((opensFunctor (D.f i j)).obj U))

Tactic:
delta IsOpenImmersion.opensFunctor

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

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

Tactic:
apply pullback_base

Result:
no goals

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

Tactic:
convert (Category.comp_id ((f D.toGlueData i k).c.app _)).symm

Result:
case h.e'_3.h.h.e'_7
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(D.V (i, j))
this :
  ∀ (U : (Opens ↑↑(D.U i))ᵒᵖ),
    (D.f i j).c.app U ≫ (pullback.fst (D.f i j) (D.f i k)).c.app (op ((Opens.map (D.f i j).base).obj (unop U))) =
      ((D.f i k).c.app U ≫ (pullback.snd (D.f i j) (D.f i k)).c.app (op ((Opens.map (D.f i k).base).obj (unop U)))) ≫
        (pullback (D.f i j) (D.f i k)).presheaf.map (eqToHom ⋯)
⊢ (D.V (i, k)).presheaf.map
      ((homOfLE ⋯).op ≫
        (opensFunctor (pullback.snd (D.f i j) (D.f i k))).op.map
            (eqToHom ⋯ ≫ (Opens.map (pullback.fst (D.f i j) (D.f i k)).base).op.map (eqToHom ⋯)) ≫
          eqToHom ⋯) =
    𝟙
      (((TopCat.Presheaf.pushforward C (D.f i k).base).obj (D.V (i, k)).presheaf).obj
        (op ((opensFunctor (D.f i j)).obj U)))

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

Tactic:
erw [(π₁ i, j, k).c.naturality_assoc, reassoc_of% this, ← Functor.map_comp_assoc,
  IsOpenImmersion.inv_naturality_assoc, IsOpenImmersion.app_invApp_assoc, ←
  (D.V (i, k)).presheaf.map_comp, ← (D.V (i, k)).presheaf.map_comp]

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