awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (goal)
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)
⊢ 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))))))
have 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 sorry))
  (((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 sorry)) ≫
    invApp (pullback.fst (D.f k i) (D.f k j)) ((Opens.map (D.t' k i j).base).1 U))
Tactic: simp_rw [← Category.assoc]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (goal)
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)
⊢ 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))
have 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 sorry))
  (((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 sorry))))) ≫
    invApp (pullback.fst (D.f k i) (D.f k j)) ((Opens.map (D.t' k i j).base).1 U))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (goal)
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)
⊢ 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))
have 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 sorry))
  ((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 sorry)) ≫
      (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 sorry))))) ≫
    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]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (goal)
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)
⊢ 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))
have 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 sorry))
  ((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 sorry)) ≫
      (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 sorry))))) ≫
    invApp (pullback.fst (D.f k i) (D.f k j)) ((Opens.map (D.t' k i j).base).1 U))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (hypothesis)
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))
⊢ Membership.mem (γ := Set (↑(↑(D.V (k, i)) : TopCat) : Type v))
    (Set.range (ι := (↑(↑(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)
            (X := (↑(pullback (D.f k i) (D.f k j)) : TopCat)) (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)))
    x
have 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))
Tactic: replace eq := ConcreteCategory.congr_arg (𝖣.t i k).base eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (hypothesis)
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))
⊢ Membership.mem (γ := Set (↑(↑(D.V (k, i)) : TopCat) : Type v))
    (Set.range (ι := (↑(↑(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)
            (X := (↑(pullback (D.f k i) (D.f k j)) : TopCat)) (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)))
    x
have 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))
Tactic: change ((π₂ i, j, k) ≫ D.t i k).base y = (D.t k i ≫ D.t i k).base x at eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (hypothesis)
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))
⊢ Membership.mem (γ := Set (↑(↑(D.V (k, i)) : TopCat) : Type v))
    (Set.range (ι := (↑(↑(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)
            (X := (↑(pullback (D.f k i) (D.f k j)) : TopCat)) (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)))
    x
have eq₁ : (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
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (goal)
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 :
  (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
⊢ Membership.mem (γ := Set (↑(↑(D.V (k, i)) : TopCat) : Type v))
    (Set.range (ι := (↑(↑(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)
            (X := (↑(pullback (D.f k i) (D.f k j)) : TopCat)) (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)))
    x
have h : Membership.mem (α := (↑(↑(D.V (k, i)) : TopCat) : Type v)) (γ := Set (↑(↑(D.V (k, i)) : TopCat) : Type v))
  (Set.range (ι := (↑(↑(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)
          (X := (↑(pullback (D.f k i) (D.f k j)) : TopCat)) (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)))
  ((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))
Tactic: subst eq
Cleared hypotheses: x, eq
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (goal)
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)
y : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)
⊢ Membership.mem (α := (↑(↑(D.V (k, i)) : TopCat) : Type v)) (γ := Set (↑(↑(D.V (k, i)) : TopCat) : Type v))
    (Set.range (ι := (↑(↑(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)
            (X := (↑(pullback (D.f k i) (D.f k j)) : TopCat)) (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)))
    ((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))
have h : 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 k i) (D.f k j)) : TopCat)) (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))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (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))
          y :
        (↑(↑(pullback (D.f k i) (D.f k j)) : 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) ≫ 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))
Tactic: use (inv (D.t' k i j)).base y
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (goal)
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)
y : (↑(↑(pullback (D.f i j) (D.f 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)
            (inv (D.t' k i j) ≫ pullback.fst (D.f k i) (D.f k j)).base :
          (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) (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))
have h : 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: congr 3