-- 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) :
    (π₂⁻¹ i, j, k) U ≫ (D.t k i).c.app _ =
      (D.t' k i j).c.app _ ≫
        (π₁⁻¹ k, j, i) (unop _) ≫
          (D.V (k, i)).presheaf.map (eqToHom (D.snd_invApp_t_app' i j k U).choose.symm)

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

Tactic:
replace e := reassoc_of% e

Result:
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))
e :
  ∀ {Z : C}
    (h :
      (D.V (k, i)).presheaf.obj
          (op
            ((opensFunctor (pullback.fst (D.f k i) (D.f k j))).obj ((Opens.map (D.t' k i j).base).toPrefunctor.1 U))) ⟶
        Z),
    invApp (pullback.snd (D.f i j) (D.f i k)) U ≫
        (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 ⋯) ≫ h =
      (D.t' k i j).c.app (op U) ≫
        invApp (pullback.fst (D.f k i) (D.f k j)) ((Opens.map (D.t' k i j).base).toPrefunctor.1 U) ≫ h
⊢ invApp (pullback.snd (D.f i j) (D.f i k)) U ≫
      (D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) =
    (D.t' k i j).c.app (op U) ≫
      invApp (pullback.fst (D.f k i) (D.f k j))
          (unop (op ((Opens.map (D.t' k i j).base).toPrefunctor.1 (unop (op U))))) ≫
        (D.V (k, i)).presheaf.map (eqToHom ⋯)

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

Tactic:
have e := (D.snd_invApp_t_app' i j k U).choose_spec

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

Proof state:
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))
e :
  ∀ {Z : C}
    (h :
      (D.V (k, i)).presheaf.obj
          (op
            ((opensFunctor (pullback.fst (D.f k i) (D.f k j))).obj ((Opens.map (D.t' k i j).base).toPrefunctor.1 U))) ⟶
        Z),
    invApp (pullback.snd (D.f i j) (D.f i k)) U ≫
        (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 ⋯) ≫ h =
      (D.t' k i j).c.app (op U) ≫
        invApp (pullback.fst (D.f k i) (D.f k j)) ((Opens.map (D.t' k i j).base).toPrefunctor.1 U) ≫ h
⊢ invApp (pullback.snd (D.f i j) (D.f i k)) U ≫
      (D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) =
    invApp (pullback.snd (D.f i j) (D.f i k)) U ≫
      (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.V (k, i)).presheaf.map (eqToHom ⋯)

Tactic:
simp [eqToHom_map]

Result:
no goals

Proof state:
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))
e :
  ∀ {Z : C}
    (h :
      (D.V (k, i)).presheaf.obj
          (op
            ((opensFunctor (pullback.fst (D.f k i) (D.f k j))).obj ((Opens.map (D.t' k i j).base).toPrefunctor.1 U))) ⟶
        Z),
    invApp (pullback.snd (D.f i j) (D.f i k)) U ≫
        (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 ⋯) ≫ h =
      (D.t' k i j).c.app (op U) ≫
        invApp (pullback.fst (D.f k i) (D.f k j)) ((Opens.map (D.t' k i j).base).toPrefunctor.1 U) ≫ h
⊢ invApp (pullback.snd (D.f i j) (D.f i k)) U ≫
      (D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) =
    (D.t' k i j).c.app (op U) ≫
      invApp (pullback.fst (D.f k i) (D.f k j))
          (unop (op ((Opens.map (D.t' k i j).base).toPrefunctor.1 (unop (op U))))) ≫
        (D.V (k, i)).presheaf.map (eqToHom ⋯)

Tactic:
rw [← e]

Result:
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))
e :
  ∀ {Z : C}
    (h :
      (D.V (k, i)).presheaf.obj
          (op
            ((opensFunctor (pullback.fst (D.f k i) (D.f k j))).obj ((Opens.map (D.t' k i j).base).toPrefunctor.1 U))) ⟶
        Z),
    invApp (pullback.snd (D.f i j) (D.f i k)) U ≫
        (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 ⋯) ≫ h =
      (D.t' k i j).c.app (op U) ≫
        invApp (pullback.fst (D.f k i) (D.f k j)) ((Opens.map (D.t' k i j).base).toPrefunctor.1 U) ≫ h
⊢ invApp (pullback.snd (D.f i j) (D.f i k)) U ≫
      (D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) =
    invApp (pullback.snd (D.f i j) (D.f i k)) U ≫
      (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.V (k, i)).presheaf.map (eqToHom ⋯)