-- 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.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))
x : ↑↑(D.V (k, i))
y : ↑↑(pullback (D.f i j) (D.f i k))
eq : (ConcreteCategory.hom (pullback.snd (D.f i j) (D.f i k)).base) y = (ConcreteCategory.hom (D.t k i).base) x
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (pullback.fst (D.f k i) (D.f k j)).base)

Tactic:
replace eq := ConcreteCategory.congr_arg (𝖣.t i k).base eq

Result:
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))
x : ↑↑(D.V (k, i))
y : ↑↑(pullback (D.f i j) (D.f i k))
eq :
  (D.t i k).base ((ConcreteCategory.hom (pullback.snd (D.f i j) (D.f i k)).base) y) =
    (D.t i k).base ((ConcreteCategory.hom (D.t k i).base) x)
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (pullback.fst (D.f k i) (D.f k j)).base)

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

Tactic:
change (inv (D.t' k i j) ≫ π₁ 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 (inv (D.t' k i j) ≫ pullback.fst (D.f k i) (D.f k j)).base) y =
    (ConcreteCategory.hom (pullback.snd (D.f i j) (D.f i k) ≫ D.t i k).base) y

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

case w.e_unop.e_carrier.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))
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.Injective ⇑(ConcreteCategory.hom (D.t k i).base)

Tactic:
swap

Result:
case w.e_unop.e_carrier.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))
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.Injective ⇑(ConcreteCategory.hom (D.t k i).base)

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

Tactic:
rw [this, Set.image_comp, Set.image_comp, Set.preimage_image_eq]

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

case w.e_unop.e_carrier.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))
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.Injective ⇑(ConcreteCategory.hom (D.t k i).base)

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

Tactic:
rfl

Result:
no goals

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))
x : ↑↑(D.V (k, i))
y : ↑↑(pullback (D.f i j) (D.f i k))
eq :
  (ConcreteCategory.hom (pullback.snd (D.f i j) (D.f i k) ≫ D.t i k).base) y =
    (ConcreteCategory.hom (D.t k i ≫ D.t i k).base) x
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (pullback.fst (D.f k i) (D.f k j)).base)

Tactic:
rw [𝖣.t_inv, id_base, TopCat.id_app] at eq

Result:
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))
x : ↑↑(D.V (k, i))
y : ↑↑(pullback (D.f i j) (D.f i k))
eq : (ConcreteCategory.hom (pullback.snd (D.f i j) (D.f i k) ≫ D.t i k).base) y = x
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (pullback.fst (D.f k i) (D.f k j)).base)