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

Tactic:
congr

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))
⊢ ⇑(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)

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 :
  (fun x => x.toFun) ((fun x => x.hom) (pullback.snd (D.f i j) (D.f i k)).base) =
    (fun x => x.toFun) ((fun x => x.hom) (inv (D.t' k i j) ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i).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:
dsimp at this

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)
⊢ ⇑(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)

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

Tactic:
refine congr_fun ?_ _

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)
⊢ Set.image ⇑(TopCat.Hom.hom (inv (D.t' k i j)).base) = Set.preimage ⇑(ConcreteCategory.hom (D.t' k i j).base)

Proof state:
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)
x : ↑↑(D.V (k, i))
⊢ (ConcreteCategory.hom (D.t i k).base) ((ConcreteCategory.hom (D.t k i).base) x) = x

Tactic:
rw [← ConcreteCategory.comp_apply, ← comp_base, D.t_inv, id_base, ConcreteCategory.id_apply]

Result:
no goals

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

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

Result:
no goals

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 ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) =
    op
      ((opensFunctor (pullback.fst (D.f k i) (D.f k j))).obj
        (unop (op ((Opens.map (D.t' k i j).base).toPrefunctor.1 (unop (op U))))))

Tactic:
delta IsOpenImmersion.opensFunctor

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

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

Tactic:
change ((π₂ i, j, k) ≫ D.t i k).base y = (D.t k i ≫ D.t i k).base x 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 =
    (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)

Proof state:
case h.e_a.e_a.e_self
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))
⊢ inv (D.t' k i j) ≫ pullback.fst (D.f k i) (D.f k j) = pullback.snd (D.f i j) (D.f i k) ≫ D.t i k

Tactic:
rw [IsIso.inv_comp_eq, 𝖣.t_fac_assoc, 𝖣.t_inv, Category.comp_id]

Result:
no goals

Proof state:
case h.hU
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).obj ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ⊆
    Set.range ⇑(ConcreteCategory.hom (pullback.fst (D.f k i) (D.f k j)).base)

Tactic:
rintro x ⟨y, -, 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)).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)