awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
this :
  Eq (α := (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
    (⇑(TopCat.Hom.hom (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))
    (Function.comp (β := (↑(↑(D.V (k, i)) : TopCat) : Type v))
      (⇑(TopCat.Hom.hom (D.t k i).base) :
        (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
      (Function.comp (β := (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
        (⇑(TopCat.Hom.hom (Hom.base (pullback.fst (D.f k i) (D.f k j)))) :
          (a : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : TopCat) : Type v))
        (⇑(TopCat.Hom.hom (inv (D.t' k i j)).base) :
          (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
            (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))))
w :
  Function.LeftInverse (α := (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) (β :=
    (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (D.t' k i j).base) :
      (a : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) →
        (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))
    (⇑(TopCat.Hom.hom (inv (D.t' k i j)).base) :
      (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
        (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
w₁ :
  Function.RightInverse (α := (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) (β :=
    (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (D.t' k i j).base) :
      (a : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) →
        (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))
    (⇑(TopCat.Hom.hom (inv (D.t' k i j)).base) :
      (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
        (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
⊢ Eq (α :=
    (x : Set (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
      Set (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
    (Set.image
      (⇑(TopCat.Hom.hom (inv (D.t' k i j)).base) :
        (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
          (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)))
    (Set.preimage
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (D.t' k i j).base) :
        (a : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) →
          (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)))

Tactic:
refine Set.image_eq_preimage_of_inverse ?_ ?_

Premises used: Set.image_eq_preimage_of_inverse
-- 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)
h :
  Eq (α :=
    (D.V (i, k)).presheaf.obj (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) 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))))))))
    ((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 ⋯))
    (NatTrans.app (Hom.c (pullback.snd (D.f i j) (D.f i k)))
        (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)) ≫
      (D.t' k i j).c.app
          (Functor.obj (Functor.op (Opens.map (Hom.base (pullback.snd (D.f i j) (D.f i k)))))
            (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U))) ≫
        (Functor.obj (TopCat.Presheaf.pushforward C (D.t' k i j).base) (pullback (D.f k i) (D.f k j)).presheaf).map
            (eqToHom ⋯) ≫
          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 (α :=
    (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))))))

Tactic:
rw [← IsIso.eq_inv_comp, IsOpenImmersion.inv_invApp, Category.assoc,
      (D.t' k i j).c.naturality_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsIso.eq_inv_comp, CategoryTheory.GlueData.t', AlgebraicGeometry.PresheafedSpace.Hom.c, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_invApp, CategoryTheory.NatTrans.naturality_assoc, AlgebraicGeometry.PresheafedSpace.GlueData.toGlueData
-- 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)
h :
  Eq (α :=
    (D.V (i, k)).presheaf.obj (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) 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))) ((Opens.map (D.t' k i j).base).1 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 ⋯))
    (((NatTrans.app (Hom.c (pullback.snd (D.f i j) (D.f i k)))
            (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)) ≫
          (D.t' k i j).c.app
            (Functor.obj (Functor.op (Opens.map (Hom.base (pullback.snd (D.f i j) (D.f i k)))))
              (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)))) ≫
        (Functor.obj (TopCat.Presheaf.pushforward C (D.t' k i j).base) (pullback (D.f k i) (D.f k j)).presheaf).map
          (eqToHom ⋯)) ≫
      invApp (pullback.fst (D.f k i) (D.f k j)) ((Opens.map (D.t' k i j).base).1 U))
⊢ Eq (α :=
    (D.V (i, k)).presheaf.obj (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) 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))))))))
    ((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 ⋯))
    (NatTrans.app (Hom.c (pullback.snd (D.f i j) (D.f i k)))
        (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)) ≫
      (D.t' k i j).c.app
          (Functor.obj (Functor.op (Opens.map (Hom.base (pullback.snd (D.f i j) (D.f i k)))))
            (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U))) ≫
        (Functor.obj (TopCat.Presheaf.pushforward C (D.t' k i j).base) (pullback (D.f k i) (D.f k j)).presheaf).map
            (eqToHom ⋯) ≫
          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:
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 (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)
h :
  Eq (α :=
    (D.V (i, k)).presheaf.obj (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) 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))) ((Opens.map (D.t' k i j).base).1 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 ⋯))
    (((NatTrans.app (Hom.c (pullback.snd (D.f i j) (D.f i k)))
            (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)) ≫
          (D.t' k i j).c.app
            (op
              (Functor.obj (Opens.map (Hom.base (pullback.snd (D.f i j) (D.f i k))))
                (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)))) ≫
        (pullback (D.f k i) (D.f k j)).presheaf.map
          (Quiver.Hom.op ((Opens.map (D.t' k i j).base).map (Quiver.Hom.unop (eqToHom ⋯))))) ≫
      invApp (pullback.fst (D.f k i) (D.f k j)) ((Opens.map (D.t' k i j).base).1 U))
⊢ Eq (α :=
    (D.V (i, k)).presheaf.obj (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) 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))) ((Opens.map (D.t' k i j).base).1 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 ⋯))
    (((NatTrans.app (Hom.c (pullback.snd (D.f i j) (D.f i k)))
            (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)) ≫
          (D.t' k i j).c.app
            (Functor.obj (Functor.op (Opens.map (Hom.base (pullback.snd (D.f i j) (D.f i k)))))
              (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)))) ≫
        (Functor.obj (TopCat.Presheaf.pushforward C (D.t' k i j).base) (pullback (D.f k i) (D.f k j)).presheaf).map
          (eqToHom ⋯)) ≫
      invApp (pullback.fst (D.f k i) (D.f k j)) ((Opens.map (D.t' k i j).base).1 U))

Tactic:
dsimp
-- 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)
h :
  Eq (α :=
    (D.V (i, k)).presheaf.obj (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) 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))) ((Opens.map (D.t' k i j).base).1 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 ⋯))
    ((CategoryStruct.comp (Y :=
          (Functor.obj (TopCat.Presheaf.pushforward C (Hom.base (pullback.fst (D.f k i) (D.f k j) ≫ D.t k i)))
                (pullback (D.f k i) (D.f k j)).presheaf).obj
            (op (Functor.obj (opensFunctor (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)) ≫
            NatTrans.app (Hom.c (pullback.fst (D.f k i) (D.f k j)))
              (op
                ((Opens.map (D.t k i).base).obj
                  (unop (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U))))))
          ((pullback (D.f k i) (D.f k j)).presheaf.map (eqToHom ⋯)) ≫
        (pullback (D.f k i) (D.f k j)).presheaf.map
          (Quiver.Hom.op ((Opens.map (D.t' k i j).base).map (Quiver.Hom.unop (eqToHom ⋯))))) ≫
      invApp (pullback.fst (D.f k i) (D.f k j)) ((Opens.map (D.t' k i j).base).1 U))
⊢ Eq (α :=
    (D.V (i, k)).presheaf.obj (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) 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))) ((Opens.map (D.t' k i j).base).1 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 ⋯))
    (((NatTrans.app (Hom.c (pullback.snd (D.f i j) (D.f i k)))
            (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)) ≫
          (D.t' k i j).c.app
            (op
              (Functor.obj (Opens.map (Hom.base (pullback.snd (D.f i j) (D.f i k))))
                (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)))) ≫
        (pullback (D.f k i) (D.f k j)).presheaf.map
          (Quiver.Hom.op ((Opens.map (D.t' k i j).base).map (Quiver.Hom.unop (eqToHom ⋯))))) ≫
      invApp (pullback.fst (D.f k i) (D.f k j)) ((Opens.map (D.t' k i j).base).1 U))

Tactic:
rw [← comp_c_app, congr_app (D.t_fac k i j), comp_c_app]

Premises used: AlgebraicGeometry.PresheafedSpace.comp_c_app, CategoryTheory.GlueData.t_fac, AlgebraicGeometry.PresheafedSpace.congr_app, AlgebraicGeometry.PresheafedSpace.GlueData.toGlueData
-- 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)
h :
  Eq (α :=
    (D.V (i, k)).presheaf.obj (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) 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))) ((Opens.map (D.t' k i j).base).1 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 ⋯))
    ((CategoryStruct.comp (Y :=
          (pullback (D.f k i) (D.f k j)).presheaf.obj
            (op
              (Functor.obj (Opens.map (Hom.base (pullback.fst (D.f k i) (D.f k j))))
                ((Opens.map (D.t k i).base).obj (Functor.obj (opensFunctor (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)) ≫
            NatTrans.app (Hom.c (pullback.fst (D.f k i) (D.f k j)))
              (op ((Opens.map (D.t k i).base).obj (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U))))
          ((pullback (D.f k i) (D.f k j)).presheaf.map (eqToHom ⋯)) ≫
        (pullback (D.f k i) (D.f k j)).presheaf.map
          (Quiver.Hom.op ((Opens.map (D.t' k i j).base).map (Quiver.Hom.unop (eqToHom ⋯))))) ≫
      invApp (pullback.fst (D.f k i) (D.f k j)) ((Opens.map (D.t' k i j).base).1 U))
⊢ Eq (α :=
    (D.V (i, k)).presheaf.obj (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) 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))) ((Opens.map (D.t' k i j).base).1 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 ⋯))
    ((CategoryStruct.comp (Y :=
          (Functor.obj (TopCat.Presheaf.pushforward C (Hom.base (pullback.fst (D.f k i) (D.f k j) ≫ D.t k i)))
                (pullback (D.f k i) (D.f k j)).presheaf).obj
            (op (Functor.obj (opensFunctor (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)) ≫
            NatTrans.app (Hom.c (pullback.fst (D.f k i) (D.f k j)))
              (op
                ((Opens.map (D.t k i).base).obj
                  (unop (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U))))))
          ((pullback (D.f k i) (D.f k j)).presheaf.map (eqToHom ⋯)) ≫
        (pullback (D.f k i) (D.f k j)).presheaf.map
          (Quiver.Hom.op ((Opens.map (D.t' k i j).base).map (Quiver.Hom.unop (eqToHom ⋯))))) ≫
      invApp (pullback.fst (D.f k i) (D.f k j)) ((Opens.map (D.t' k i j).base).1 U))

Tactic:
dsimp
-- 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)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

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)
x : (↑(↑(D.V (k, i)) : TopCat) : Type v)
y : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)
eq :
  Eq (α := (↑(↑(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))
        y :
      (↑(↑(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)
            (D.t k i).base :
          (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
        x :
      (↑(↑(D.V (i, k)) : TopCat) : Type v))
⊢ Eq (α := (↑(↑(D.V (k, i)) : TopCat) : Type v))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (D.t i k).base :
          (a : (↑(↑(D.V (i, k)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : 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))
            y :
          (↑(↑(D.V (i, k)) : TopCat) : Type v)) :
      (↑(↑(D.V (k, i)) : TopCat) : Type v))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (D.t i k).base :
          (a : (↑(↑(D.V (i, k)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : TopCat) : Type v))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
                (D.t k i).base :
              (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
            x :
          (↑(↑(D.V (i, k)) : TopCat) : Type v)) :
      (↑(↑(D.V (k, i)) : TopCat) : Type v))

Tactic:
replace eq := ConcreteCategory.congr_arg (𝖣.t i k).base eq
-- 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)
x : (↑(↑(D.V (k, i)) : TopCat) : Type v)
y : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)
eq :
  Eq (α := (↑(↑(D.V (k, i)) : TopCat) : Type v))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (D.t i k).base :
          (a : (↑(↑(D.V (i, k)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : 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))
            y :
          (↑(↑(D.V (i, k)) : TopCat) : Type v)) :
      (↑(↑(D.V (k, i)) : TopCat) : Type v))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (D.t i k).base :
          (a : (↑(↑(D.V (i, k)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : TopCat) : Type v))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
                (D.t k i).base :
              (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
            x :
          (↑(↑(D.V (i, k)) : TopCat) : Type v)) :
      (↑(↑(D.V (k, i)) : TopCat) : Type v))
⊢ Eq (α := (↑(↑(D.V (k, i)) : 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) ≫ D.t i k)) :
          (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : TopCat) : Type v))
        y :
      (↑(↑(D.V (k, i)) : TopCat) : Type v))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (D.t k i ≫ D.t i k).base :
          (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : TopCat) : Type v))
        x :
      (↑(↑(D.V (k, i)) : TopCat) : Type v))

Tactic:
change ((π₂ i, j, k) ≫ D.t i k).base y = (D.t k i ≫ D.t i k).base x at eq

Premises used: CategoryTheory.GlueData.t, CategoryTheory.ConcreteCategory.hom, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe, AlgebraicGeometry.PresheafedSpace.GlueData.toGlueData
-- 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)
x : (↑(↑(D.V (k, i)) : TopCat) : Type v)
y : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)
eq :
  Eq (α := (↑(↑(D.V (k, i)) : 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) ≫ D.t i k)) :
          (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : TopCat) : Type v))
        y :
      (↑(↑(D.V (k, i)) : TopCat) : Type v))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (D.t k i ≫ D.t i k).base :
          (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : TopCat) : Type v))
        x :
      (↑(↑(D.V (k, i)) : 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) ≫ D.t i k)) :
        (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : TopCat) : Type v))
      y =
    x

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

Premises used: TopCat.id_app, AlgebraicGeometry.PresheafedSpace.id_base