awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
inst : Epi f.base
⊢ Epi (forgetToSheafedSpace.map f).hom.base

Tactic:
assumption
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
inst : Epi f.base
⊢ Epi (forgetToSheafedSpace.map f).hom.base

Tactic:
have : Epi (forgetToSheafedSpace.map f).hom.base := by assumption
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
inst : Epi f.base
this : Epi (forgetToSheafedSpace.map f).hom.base
⊢ IsIso (forgetToSheafedSpace.map f)

Tactic:
apply SheafedSpace.IsOpenImmersion.to_iso

Premises used: AlgebraicGeometry.SheafedSpace.IsOpenImmersion.to_iso
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i : D.J
rw :
  IsOpenEmbedding (X := (↑(↑(D.U i) : TopCat) : Type v)) (Y := (↑(↑D.glued : TopCat) : Type v))
    (Function.comp (β := (↑(D.mapGlueData (forget C)).glued : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (X := (D.mapGlueData (forget C)).glued) (Y := (↑D.glued : TopCat))
              (Iso.inv (D.gluedIso (forget C)) : (D.mapGlueData (forget C)).glued ⟶ Functor.obj (forget C) D.glued) :
            C((↑(D.mapGlueData (forget C)).glued : Type v), (↑(↑D.glued : TopCat) : Type v))) :
        (a : (↑(D.mapGlueData (forget C)).glued : Type v)) → (↑(↑D.glued : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (Y := (D.mapGlueData (forget C)).glued) ((D.mapGlueData (forget C)).ι i)) :
        (a : (↑(↑(D.U i) : TopCat) : Type v)) → (↑(D.mapGlueData (forget C)).glued : Type v)))
⊢ IsOpenEmbedding (X := (↑(↑(D.U i) : TopCat) : Type v)) (Y := (↑(↑D.glued : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (Y := (↑D.glued : TopCat)) (Hom.base (D.ι i))) :
      (a : (↑(↑(D.U i) : TopCat) : Type v)) → (↑(↑D.glued : TopCat) : Type v))

Tactic:
rw [← show _ = (𝖣.ι i).base from 𝖣.ι_gluedIso_inv (PresheafedSpace.forget _) _, TopCat.coe_comp]

Premises used: TopCat.coe_comp
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i : D.J
⊢ IsOpenEmbedding (X := (↑(↑(D.U i) : TopCat) : Type v)) (Y := (↑(↑D.glued : TopCat) : Type v))
    (Function.comp (β := (↑(D.mapGlueData (forget C)).glued : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (X := (D.mapGlueData (forget C)).glued) (Y := (↑D.glued : TopCat))
              (Iso.inv (D.gluedIso (forget C)) : (D.mapGlueData (forget C)).glued ⟶ Functor.obj (forget C) D.glued) :
            C((↑(D.mapGlueData (forget C)).glued : Type v), (↑(↑D.glued : TopCat) : Type v))) :
        (a : (↑(D.mapGlueData (forget C)).glued : Type v)) → (↑(↑D.glued : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (Y := (D.mapGlueData (forget C)).glued) ((D.mapGlueData (forget C)).ι i)) :
        (a : (↑(↑(D.U i) : TopCat) : Type v)) → (↑(D.mapGlueData (forget C)).glued : Type v)))

Tactic:
(TopCat.homeoOfIso (𝖣.gluedIso (PresheafedSpace.forget _)).symm).isOpenEmbedding.comp
      (D.toTopGlueData.ι_isOpenEmbedding i)

Premises used: AlgebraicGeometry.PresheafedSpace.GlueData.toTopGlueData, TopCat.homeoOfIso, TopCat.GlueData.ι_isOpenEmbedding, AlgebraicGeometry.PresheafedSpace.forget, CategoryTheory.Iso.symm, CategoryTheory.GlueData.gluedIso, Homeomorph.isOpenEmbedding, Topology.IsOpenEmbedding.comp, AlgebraicGeometry.PresheafedSpace.GlueData.toGlueData
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i : D.J
⊢ IsOpenEmbedding (X := (↑(↑(D.U i) : TopCat) : Type v)) (Y := (↑(↑D.glued : TopCat) : Type v))
    (Function.comp (β := (↑(D.mapGlueData (forget C)).glued : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (X := (D.mapGlueData (forget C)).glued) (Y := (↑D.glued : TopCat))
              (Iso.inv (D.gluedIso (forget C)) : (D.mapGlueData (forget C)).glued ⟶ Functor.obj (forget C) D.glued) :
            C((↑(D.mapGlueData (forget C)).glued : Type v), (↑(↑D.glued : TopCat) : Type v))) :
        (a : (↑(D.mapGlueData (forget C)).glued : Type v)) → (↑(↑D.glued : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (Y := (D.mapGlueData (forget C)).glued) ((D.mapGlueData (forget C)).ι i)) :
        (a : (↑(↑(D.U i) : TopCat) : Type v)) → (↑(D.mapGlueData (forget C)).glued : Type v)))

Tactic:
exact (TopCat.homeoOfIso (𝖣.gluedIso (PresheafedSpace.forget _)).symm).isOpenEmbedding.comp
      (D.toTopGlueData.ι_isOpenEmbedding i)
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
i j k : D.J
S : Set (↑(↑(D.V (i, j)) : TopCat) : Type v)
⊢ Eq (α := (↑(pullback (D.f i j) (D.f i k)) : TopCat) ⟶ (↑(D.V (i, j)) : TopCat))
    (CategoryStruct.comp (Y :=
        pullback (X := Functor.obj (forget C) (D.V (i, j))) (CategoryTheory.Functor.map (forget C) (D.f i j))
          (CategoryTheory.Functor.map (forget C) (D.f i k)))
        (Iso.hom (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)))
        (pullback.fst (CategoryTheory.Functor.map (forget C) (D.f i j))
          (CategoryTheory.Functor.map (forget C) (D.f i k))) :
      Functor.obj (forget C) (pullback (D.f i j) (D.f i k)) ⟶ Functor.obj (forget C) (D.V (i, j)))
    (Hom.base (pullback.fst (D.f i j) (D.f i k)))

Tactic:
have eq₁ : _ = (π₁ i, j, k).base := PreservesPullback.iso_hom_fst (forget C) _ _
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
i j k : D.J
S : Set (↑(↑(D.V (i, j)) : TopCat) : Type v)
eq₁ :
  Eq (α := (↑(pullback (D.f i j) (D.f i k)) : TopCat) ⟶ (↑(D.V (i, j)) : TopCat))
    (CategoryStruct.comp (Y :=
        pullback (X := Functor.obj (forget C) (D.V (i, j))) (CategoryTheory.Functor.map (forget C) (D.f i j))
          (CategoryTheory.Functor.map (forget C) (D.f i k)))
        (Iso.hom (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)))
        (pullback.fst (CategoryTheory.Functor.map (forget C) (D.f i j))
          (CategoryTheory.Functor.map (forget C) (D.f i k))) :
      Functor.obj (forget C) (pullback (D.f i j) (D.f i k)) ⟶ Functor.obj (forget C) (D.V (i, j)))
    (Hom.base (pullback.fst (D.f i j) (D.f i k)))
⊢ Eq (α := (↑(pullback (D.f i j) (D.f i k)) : TopCat) ⟶ (↑(D.V (i, k)) : TopCat))
    (CategoryStruct.comp (Y :=
        pullback (X := Functor.obj (forget C) (D.V (i, j))) (CategoryTheory.Functor.map (forget C) (D.f i j))
          (CategoryTheory.Functor.map (forget C) (D.f i k)))
        (Iso.hom (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)))
        (pullback.snd (CategoryTheory.Functor.map (forget C) (D.f i j))
          (CategoryTheory.Functor.map (forget C) (D.f i k))) :
      Functor.obj (forget C) (pullback (D.f i j) (D.f i k)) ⟶ Functor.obj (forget C) (D.V (i, k)))
    (Hom.base (pullback.snd (D.f i j) (D.f i k)))

Tactic:
have eq₂ : _ = (π₂ i, j, k).base := PreservesPullback.iso_hom_snd (forget C) _ _
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
i j k : D.J
S : Set (↑(↑(D.V (i, j)) : TopCat) : Type v)
eq₁ :
  Eq (α := (↑(pullback (D.f i j) (D.f i k)) : TopCat) ⟶ (↑(D.V (i, j)) : TopCat))
    (CategoryStruct.comp (Y :=
        pullback (X := Functor.obj (forget C) (D.V (i, j))) (CategoryTheory.Functor.map (forget C) (D.f i j))
          (CategoryTheory.Functor.map (forget C) (D.f i k)))
        (Iso.hom (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)))
        (pullback.fst (CategoryTheory.Functor.map (forget C) (D.f i j))
          (CategoryTheory.Functor.map (forget C) (D.f i k))) :
      Functor.obj (forget C) (pullback (D.f i j) (D.f i k)) ⟶ Functor.obj (forget C) (D.V (i, j)))
    (Hom.base (pullback.fst (D.f i j) (D.f i k)))
eq₂ :
  Eq (α := (↑(pullback (D.f i j) (D.f i k)) : TopCat) ⟶ (↑(D.V (i, k)) : TopCat))
    (CategoryStruct.comp (Y :=
        pullback (X := Functor.obj (forget C) (D.V (i, j))) (CategoryTheory.Functor.map (forget C) (D.f i j))
          (CategoryTheory.Functor.map (forget C) (D.f i k)))
        (Iso.hom (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)))
        (pullback.snd (CategoryTheory.Functor.map (forget C) (D.f i j))
          (CategoryTheory.Functor.map (forget C) (D.f i k))) :
      Functor.obj (forget C) (pullback (D.f i j) (D.f i k)) ⟶ Functor.obj (forget C) (D.V (i, k)))
    (Hom.base (pullback.snd (D.f i j) (D.f i k)))
⊢ Epi (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat)) (Y :=
    pullback (X := Functor.obj (forget C) (D.V (i, j))) (CategoryTheory.Functor.map (forget C) (D.f i j))
      (CategoryTheory.Functor.map (forget C) (D.f i k)))
    (Iso.hom (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)) :
      Functor.obj (forget C) (pullback (D.f i j) (D.f i k)) ⟶
        pullback (X := Functor.obj (forget C) (D.V (i, j))) (CategoryTheory.Functor.map (forget C) (D.f i j))
          (CategoryTheory.Functor.map (forget C) (D.f i k)))

Tactic:
infer_instance
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
i j k : D.J
U : Opens (↑(↑(D.V (i, j)) : TopCat) : Type v)
dsimp :
  op
      {
        carrier :=
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                  TopCat.carrier) (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat))
                  (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
              (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v)) ''
            (↑{
                  carrier :=
                    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                            TopCat.carrier) (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat))
                            (Hom.base (pullback.fst (D.f i j) (D.f i k)))) :
                        (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
                          (↑(↑(D.V (i, j)) : TopCat) : Type v)) ⁻¹'
                      (↑U : Set (↑(↑(D.V (i, j)) : TopCat) : Type v)),
                  is_open' := ⋯ : Opens (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v) } :
              Set (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)),
        is_open' := ⋯ } =
    op
      {
        carrier :=
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                  TopCat.carrier) (D.f i k).base) :
              (a : (↑(↑(D.V (i, k)) : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v)) ⁻¹'
            (↑{
                  carrier :=
                    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                            TopCat.carrier) (D.f i j).base) :
                        (a : (↑(↑(D.V (i, j)) : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v)) ''
                      (↑U : Set (↑(↑(D.V (i, j)) : TopCat) : Type v)),
                  is_open' := ⋯ : Opens (↑(↑(D.U i) : TopCat) : Type v) } :
              Set (↑(↑(D.U i) : TopCat) : Type v)),
        is_open' := ⋯ : Opens (↑(↑(D.V (i, k)) : TopCat) : Type v) }
⊢ op
      (Functor.obj (C := Opens (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))
        (IsOpenMap.functor (f := Hom.base (pullback.snd (D.f i j) (D.f i k))) ⋯)
        (unop
          (op
            ((Opens.map (Hom.base (pullback.fst (D.f i j) (D.f i k))) :
                  Opens (↑(↑(D.V (i, j)) : TopCat) : Type v) ⥤
                    Opens (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)).1
              (unop (op U)))))) =
    (Opens.map (D.f i k).base).op.obj (op (Functor.obj (IsOpenMap.functor (f := (D.f i j).base) ⋯) U))

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

Premises used: CategoryTheory.Functor.op, IsOpenMap.functor, Opposite.unop_op, TopologicalSpace.Opens.map
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
i j k : D.J
U : Opens (↑(↑(D.V (i, j)) : TopCat) : Type v)
⊢ Eq (α := Set (↑(↑(D.V (i, k)) : TopCat) : Type v))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat)) (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
        (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v)) ''
      (↑{
            carrier :=
              (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                      TopCat.carrier) (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat))
                      (Hom.base (pullback.fst (D.f i j) (D.f i k)))) :
                  (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
                    (↑(↑(D.V (i, j)) : TopCat) : Type v)) ⁻¹'
                (↑U : Set (↑(↑(D.V (i, j)) : TopCat) : Type v)),
            is_open' := ⋯ : Opens (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v) } :
        Set (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (D.f i k).base) :
        (a : (↑(↑(D.V (i, k)) : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v)) ⁻¹'
      (↑{
            carrier :=
              (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                      TopCat.carrier) (D.f i j).base) :
                  (a : (↑(↑(D.V (i, j)) : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v)) ''
                (↑U : Set (↑(↑(D.V (i, j)) : TopCat) : Type v)),
            is_open' := ⋯ : Opens (↑(↑(D.U i) : TopCat) : Type v) } :
        Set (↑(↑(D.U i) : TopCat) : Type v)))

Tactic:
apply pullback_base

Premises used: AlgebraicGeometry.PresheafedSpace.GlueData.pullback_base
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
i j k : D.J
U : Opens (↑(↑(D.V (i, j)) : TopCat) : Type v)
⊢ ∀ (U : (Opens (↑(↑(D.U i) : TopCat) : Type v))ᵒᵖ),
    NatTrans.app (Hom.c (pullback.fst (D.f i j) (D.f i k) ≫ D.f i j)) U =
      NatTrans.app (Hom.c (pullback.snd (D.f i j) (D.f i k) ≫ D.f i k)) U ≫
        (pullback (D.f i j) (D.f i k)).presheaf.map (eqToHom ⋯)

Tactic:
have := PresheafedSpace.congr_app (@pullback.condition _ _ _ _ _ (D.f i j) (D.f i k) _)
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
i j k : D.J
U : Opens (↑(↑(D.V (i, j)) : TopCat) : Type v)
this :
  ∀ (U : (Opens (↑(↑(D.U i) : TopCat) : Type v))ᵒᵖ),
    (D.f i j).c.app U ≫
        NatTrans.app (Hom.c (pullback.fst (D.f i j) (D.f i k))) (op ((Opens.map (D.f i j).base).obj (unop U))) =
      ((D.f i k).c.app U ≫
          NatTrans.app (Hom.c (pullback.snd (D.f i j) (D.f i k))) (op ((Opens.map (D.f i k).base).obj (unop U)))) ≫
        (pullback (D.f i j) (D.f i k)).presheaf.map (eqToHom ⋯)
rw :
  (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 ⋯)) ≫
      NatTrans.app (Hom.c (pullback.fst (D.f i j) (D.f i k))) (op U) ≫
        invApp (pullback.snd (D.f i j) (D.f i k))
            (unop
              (op
                ((Opens.map (Hom.base (pullback.fst (D.f i j) (D.f i k))) :
                      Opens (↑(↑(D.V (i, j)) : TopCat) : Type v) ⥤
                        Opens (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)).1
                  (unop (op U))))) ≫
          (D.V (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)) =
    NatTrans.app (Hom.c (pullback.fst (D.f i j) (D.f i k))) (op U) ≫
      invApp (pullback.snd (D.f i j) (D.f i k))
          (unop
            (op
              ((Opens.map (Hom.base (pullback.fst (D.f i j) (D.f i k))) :
                    Opens (↑(↑(D.V (i, j)) : TopCat) : Type v) ⥤
                      Opens (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)).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]

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp, CategoryTheory.inv, CategoryTheory.IsIso.inv_hom_id_assoc, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_invApp, CategoryTheory.cancel_epi
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
i j k : D.J
U : Opens (↑(↑(D.V (i, j)) : TopCat) : Type v)
this :
  ∀ (U : (Opens (↑(↑(D.U i) : TopCat) : Type v))ᵒᵖ),
    (D.f i j).c.app U ≫
        NatTrans.app (Hom.c (pullback.fst (D.f i j) (D.f i k))) (op ((Opens.map (D.f i j).base).obj (unop U))) =
      ((D.f i k).c.app U ≫
          NatTrans.app (Hom.c (pullback.snd (D.f i j) (D.f i k))) (op ((Opens.map (D.f i k).base).obj (unop U)))) ≫
        (pullback (D.f i j) (D.f i k)).presheaf.map (eqToHom ⋯)
simp_rw :
  (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 ⋯) ≫
        NatTrans.app (Hom.c (pullback.fst (D.f i j) (D.f i k))) (op U) ≫
          invApp (pullback.snd (D.f i j) (D.f i k))
              ((Opens.map (Hom.base (pullback.fst (D.f i j) (D.f i k))) :
                    Opens (↑(↑(D.V (i, j)) : TopCat) : Type v) ⥤
                      Opens (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)).1
                U) ≫
            (D.V (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 ⋯)) ≫
      NatTrans.app (Hom.c (pullback.fst (D.f i j) (D.f i k))) (op U) ≫
        invApp (pullback.snd (D.f i j) (D.f i k))
            (unop
              (op
                ((Opens.map (Hom.base (pullback.fst (D.f i j) (D.f i k))) :
                      Opens (↑(↑(D.V (i, j)) : TopCat) : Type v) ⥤
                        Opens (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)).1
                  (unop (op U))))) ≫
          (D.V (i, k)).presheaf.map (eqToHom ⋯)

Tactic:
simp_rw [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
i j k : D.J
U : Opens (↑(↑(D.V (i, j)) : TopCat) : Type v)
this :
  ∀ (U : (Opens (↑(↑(D.U i) : TopCat) : Type v))ᵒᵖ),
    (D.f i j).c.app U ≫
        NatTrans.app (Hom.c (pullback.fst (D.f i j) (D.f i k))) (op ((Opens.map (D.f i j).base).obj (unop U))) =
      ((D.f i k).c.app U ≫
          NatTrans.app (Hom.c (pullback.snd (D.f i j) (D.f i k))) (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)) ≫
      𝟙
        ((Functor.obj (TopCat.Presheaf.pushforward C (D.f i k).base) (D.V (i, k)).presheaf).obj
          (op ((opensFunctor (D.f i j)).obj U)))

Tactic:
(Category.comp_id _).symm

Premises used: CategoryTheory.Category.comp_id, Eq.symm
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
i j k : D.J
U : Opens (↑(↑(D.V (i, j)) : TopCat) : Type v)
this :
  ∀ (U : (Opens (↑(↑(D.U i) : TopCat) : Type v))ᵒᵖ),
    (D.f i j).c.app U ≫
        NatTrans.app (Hom.c (pullback.fst (D.f i j) (D.f i k))) (op ((Opens.map (D.f i j).base).obj (unop U))) =
      ((D.f i k).c.app U ≫
          NatTrans.app (Hom.c (pullback.snd (D.f i j) (D.f i k))) (op ((Opens.map (D.f i k).base).obj (unop U)))) ≫
        (pullback (D.f i j) (D.f i k)).presheaf.map (eqToHom ⋯)
⊢ Eq.{v + 1} (α :=
    (Functor.obj (TopCat.Presheaf.pushforward C (D.f i k).base) (D.V (i, k)).presheaf).obj
        (op ((opensFunctor (D.f i j)).obj U)) ⟶
      (Functor.obj (TopCat.Presheaf.pushforward C (D.f i k).base) (D.V (i, k)).presheaf).obj
        (op ((opensFunctor (D.f i j)).obj U)))
    (𝟙 ((D.V (i, k)).presheaf.obj (op ((Opens.map (D.f i k).base).obj (unop (op ((opensFunctor (D.f i j)).obj U)))))))
    (𝟙
      ((Functor.obj (TopCat.Presheaf.pushforward C (D.f i k).base) (D.V (i, k)).presheaf).obj
        (op ((opensFunctor (D.f i j)).obj U))))

Tactic:
rfl
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
i j k : D.J
U : Opens (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)
w :
  (Opens.map (D.t k i).base).op.obj (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)) =
    op
      (Functor.obj (C := Opens (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
        (opensFunctor (pullback.fst (D.f k i) (D.f k j))) (unop (op ((Opens.map (D.t' k i j).base).1 (unop (op U))))))
h :
  Eq (α :=
    (pullback (D.f i j) (D.f i k)).presheaf.obj (op U) ⟶
      (D.V (k, i)).presheaf.obj
        (op
          (Functor.obj (C := Opens (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
            (opensFunctor (pullback.fst (D.f k i) (D.f k j)))
            (unop (op ((Opens.map (D.t' k i j).base).1 (unop (op U))))))))
    (CategoryStruct.comp (Y :=
      (D.V (i, k)).presheaf.obj (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)))
      (invApp (pullback.snd (D.f i j) (D.f i k)) U)
      ((D.t k i).c.app (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) 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).1 (unop (op U))))))
⊢ ∃ (eq :
    (Opens.map (D.t k i).base).op.obj (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)) =
      op
        (Functor.obj (C := Opens (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
          (opensFunctor (pullback.fst (D.f k i) (D.f k j)))
          (unop (op ((Opens.map (D.t' k i j).base).1 (unop (op U))))))),
    invApp (pullback.snd (D.f i j) (D.f i k)) U ≫
        (D.t k i).c.app (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)) ≫
          (D.V (k, i)).presheaf.map (eqToHom eq) =
      (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).1 (unop (op U)))))

Tactic:
fconstructor