-- 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:
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))
            (unop (op ((Opens.map (pullback.fst (D.f i j) (D.f i k)).base).toPrefunctor.1 (unop (op U))))) ≫
          (D.V (i, k)).presheaf.map (eqToHom ⋯)

Tactic:
simp_rw [Category.assoc]

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

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 ⋯)
⊢ invApp (D.f i j) U ≫ (D.f i k).c.app (op ((opensFunctor (D.f i j)).obj U)) =
    (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))
          (unop (op ((Opens.map (pullback.fst (D.f i j) (D.f i k)).base).toPrefunctor.1 (unop (op U))))) ≫
        (D.V (i, k)).presheaf.map (eqToHom ⋯)

Tactic:
rw [← cancel_epi (inv ((D.f_open i j).invApp _ U)), IsIso.inv_hom_id_assoc,
  IsOpenImmersion.inv_invApp]

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 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))
            (unop (op ((Opens.map (pullback.fst (D.f i j) (D.f i k)).base).toPrefunctor.1 (unop (op U))))) ≫
          (D.V (i, k)).presheaf.map (eqToHom ⋯)

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

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

Result:
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(D.V (i, j))
⊢ op
      {
        carrier :=
          ⇑(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' := ⋯ },
        is_open' := ⋯ } =
    op
      {
        carrier :=
          ⇑(ConcreteCategory.hom (D.f i k).base) ⁻¹'
            ↑{ carrier := ⇑(ConcreteCategory.hom (D.f i j).base) '' ↑U, is_open' := ⋯ },
        is_open' := ⋯ }

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
      {
        carrier :=
          ⇑(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' := ⋯ },
        is_open' := ⋯ } =
    op
      {
        carrier :=
          ⇑(ConcreteCategory.hom (D.f i k).base) ⁻¹'
            ↑{ carrier := ⇑(ConcreteCategory.hom (D.f i j).base) '' ↑U, is_open' := ⋯ },
        is_open' := ⋯ }

Tactic:
congr

Result:
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' := ⋯ }

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

Tactic:
rfl

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))
⊢ invApp (D.f i j) U ≫ (D.f i k).c.app (op ((opensFunctor (D.f i j)).obj U)) =
    (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))
          (unop (op ((Opens.map (pullback.fst (D.f i j) (D.f i k)).base).toPrefunctor.1 (unop (op U))))) ≫
        (D.V (i, k)).presheaf.map (eqToHom ⋯)

Tactic:
have := PresheafedSpace.congr_app (@pullback.condition _ _ _ _ _ (D.f i j) (D.f i k) _)

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))ᵒᵖ),
    (pullback.fst (D.f i j) (D.f i k) ≫ D.f i j).c.app U =
      (pullback.snd (D.f i j) (D.f i k) ≫ D.f i k).c.app U ≫ (pullback (D.f i j) (D.f i k)).presheaf.map (eqToHom ⋯)
⊢ invApp (D.f i j) U ≫ (D.f i k).c.app (op ((opensFunctor (D.f i j)).obj U)) =
    (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))
          (unop (op ((Opens.map (pullback.fst (D.f i j) (D.f i k)).base).toPrefunctor.1 (unop (op U))))) ≫
        (D.V (i, k)).presheaf.map (eqToHom ⋯)