awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Presheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Limits.HasColimits.{v, u} C
X Y : TopCat
f : X ⟶ Y
hf :
  IsOpenMap (X := (↑X : Type v)) (Y := (↑Y : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type v)) → (↑Y : Type v))
ℱ 𝒢 : TopCat.Presheaf C Y
u : ℱ ⟶ 𝒢
U : Opens (↑X : Type v)
j : CostructuredArrow (Opens.map f).op (op U)
⊢ Eq (α := obj (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ ℱ) j ⟶ (obj (pullback C f) 𝒢).obj (op U))
    (CategoryStruct.comp (Y :=
        obj
          (obj (const (CostructuredArrow (Opens.map f).op (op U)))
            (Limits.Cocone.pt (J := CostructuredArrow (Opens.map f).op (op U))
              ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ)
                    ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
                (op U))))
          j)
        (NatTrans.app
          (Limits.Cocone.ι
            ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
              (op U)))
          j)
        (NatTrans.app (CategoryTheory.Functor.map (pullback C f) u) (op U)) :
      obj (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ ℱ) j ⟶ (obj (pullback C f) 𝒢).obj (op U))
    (NatTrans.app (whiskerLeft (CostructuredArrow.proj (Opens.map f).op (op U)) u) j ≫
        NatTrans.app
          (Limits.Cocone.ι
            ((LeftExtension.mk ((Opens.map f).op.leftKanExtension 𝒢) ((Opens.map f).op.leftKanExtensionUnit 𝒢)).coconeAt
              (op U)))
          j :
      obj (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ ℱ) j ⟶
        obj
          (obj (const (CostructuredArrow (Opens.map f).op (op U)))
            (Limits.Cocone.pt (J := CostructuredArrow (Opens.map f).op (op U))
              ((LeftExtension.mk ((Opens.map f).op.leftKanExtension 𝒢)
                    ((Opens.map f).op.leftKanExtensionUnit 𝒢)).coconeAt
                (op U))))
          j)
have dsimp : (NatTrans.app ((Opens.map f).op.leftKanExtensionUnit ℱ) j.left ≫ ((Opens.map f).op.leftKanExtension ℱ).map j.hom) ≫
    NatTrans.app (CategoryTheory.Functor.map (Opens.map f).op.lan u) (op U) =
  u.app j.left ≫
    NatTrans.app ((Opens.map f).op.leftKanExtensionUnit 𝒢) j.left ≫ ((Opens.map f).op.leftKanExtension 𝒢).map j.hom
Tactic: dsimp [pullback]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Presheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Limits.HasColimits.{v, u} C
X Y : TopCat
f : X ⟶ Y
hf :
  IsOpenMap (X := (↑X : Type v)) (Y := (↑Y : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type v)) → (↑Y : Type v))
ℱ 𝒢 : TopCat.Presheaf C Y
u : ℱ ⟶ 𝒢
U : Opens (↑X : Type v)
j : CostructuredArrow (Opens.map f).op (op U)
⊢ (NatTrans.app ((Opens.map f).op.leftKanExtensionUnit ℱ) j.left ≫ ((Opens.map f).op.leftKanExtension ℱ).map j.hom) ≫
      NatTrans.app (CategoryTheory.Functor.map (Opens.map f).op.lan u) (op U) =
    u.app j.left ≫
      NatTrans.app ((Opens.map f).op.leftKanExtensionUnit 𝒢) j.left ≫ ((Opens.map f).op.leftKanExtension 𝒢).map j.hom
have simp : NatTrans.app ((Opens.map f).op.leftKanExtensionUnit ℱ) j.left ≫
    NatTrans.app (CategoryTheory.Functor.map (Opens.map f).op.lan u) (op ((Opens.map f).obj (unop j.left))) ≫
      (obj (Opens.map f).op.lan 𝒢).map j.hom =
  u.app j.left ≫
    NatTrans.app ((Opens.map f).op.leftKanExtensionUnit 𝒢) j.left ≫ ((Opens.map f).op.leftKanExtension 𝒢).map j.hom
Tactic: simp only [Category.assoc, NatTrans.naturality]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Presheaf (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Limits.HasColimits.{v, u} C
X Y : TopCat
f : X ⟶ Y
hf :
  IsOpenMap (X := (↑X : Type v)) (Y := (↑Y : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type v)) → (↑Y : Type v))
ℱ 𝒢 : TopCat.Presheaf C Y
u : ℱ ⟶ 𝒢
U : Opens (↑X : Type v)
j : CostructuredArrow (Opens.map f).op (op U)
⊢ NatTrans.app ((Opens.map f).op.leftKanExtensionUnit ℱ) j.left ≫
      NatTrans.app (CategoryTheory.Functor.map (Opens.map f).op.lan u) (op ((Opens.map f).obj (unop j.left))) ≫
        (obj (Opens.map f).op.lan 𝒢).map j.hom =
    u.app j.left ≫
      NatTrans.app ((Opens.map f).op.leftKanExtensionUnit 𝒢) j.left ≫ ((Opens.map f).op.leftKanExtension 𝒢).map j.hom
have this : Eq (α :=
  (obj (𝟭 (CategoryTheory.Functor.{v, v, v, u} (Opens (↑Y : Type v))ᵒᵖ C)) ℱ).obj j.left ⟶
    (obj
          ((Opens.map f).op.lan ⋙
            obj (whiskeringLeft (Opens (↑Y : Type v))ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (Opens.map f).op)
          𝒢).obj
      j.left)
  (NatTrans.app
    (CategoryTheory.Functor.map (𝟭 (CategoryTheory.Functor.{v, v, v, u} (Opens (↑Y : Type v))ᵒᵖ C)) u ≫
      NatTrans.app (Opens.map f).op.lanUnit 𝒢)
    j.left)
  (NatTrans.app
    (NatTrans.app (Opens.map f).op.lanUnit ℱ ≫
      CategoryTheory.Functor.map
        ((Opens.map f).op.lan ⋙ obj (whiskeringLeft (Opens (↑Y : Type v))ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (Opens.map f).op)
        u)
    j.left)
Tactic: have := NatTrans.congr_app ((Opens.map f).op.lanUnit.naturality u) j.left
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Presheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Limits.HasColimits.{v, u} C
X Y : TopCat
f : X ⟶ Y
hf :
  IsOpenMap (X := (↑X : Type v)) (Y := (↑Y : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type v)) → (↑Y : Type v))
ℱ 𝒢 : TopCat.Presheaf C Y
u : ℱ ⟶ 𝒢
U : Opens (↑X : Type v)
j : CostructuredArrow (Opens.map f).op (op U)
this :
  Eq (α := ℱ.obj j.left ⟶ (obj (Opens.map f).op.lan 𝒢).obj (op ((Opens.map f).obj (unop j.left))))
    (u.app j.left ≫ NatTrans.app ((Opens.map f).op.leftKanExtensionUnit 𝒢) j.left)
    (CategoryStruct.comp (Y := (obj (Opens.map f).op.lan ℱ).obj (op ((Opens.map f).obj (unop j.left))))
      (NatTrans.app ((Opens.map f).op.leftKanExtensionUnit ℱ) j.left)
      (NatTrans.app (CategoryTheory.Functor.map (Opens.map f).op.lan u) (op ((Opens.map f).obj (unop j.left)))))
⊢ NatTrans.app ((Opens.map f).op.leftKanExtensionUnit ℱ) j.left ≫
      NatTrans.app (CategoryTheory.Functor.map (Opens.map f).op.lan u) (op ((Opens.map f).obj (unop j.left))) ≫
        (obj (Opens.map f).op.lan 𝒢).map j.hom =
    u.app j.left ≫
      NatTrans.app ((Opens.map f).op.leftKanExtensionUnit 𝒢) j.left ≫ ((Opens.map f).op.leftKanExtension 𝒢).map j.hom
have rw : NatTrans.app ((Opens.map f).op.leftKanExtensionUnit ℱ) j.left ≫
    NatTrans.app (CategoryTheory.Functor.map (Opens.map f).op.lan u) (op ((Opens.map f).obj (unop j.left))) ≫
      (obj (Opens.map f).op.lan 𝒢).map j.hom =
  CategoryStruct.comp (Y := (obj (Opens.map f).op.lan ℱ).obj (op ((Opens.map f).obj (unop j.left))))
    (NatTrans.app ((Opens.map f).op.leftKanExtensionUnit ℱ) j.left)
    (NatTrans.app (CategoryTheory.Functor.map (Opens.map f).op.lan u) (op ((Opens.map f).obj (unop j.left))) ≫
      ((Opens.map f).op.leftKanExtension 𝒢).map j.hom)
Tactic: rw [reassoc_of% this]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Sheaf (hypothesis)
Goal:
X : TopCat
A : Type u_1
inst : Category.{u, u_1} A
FC : A → A → Type u_2
CC : A → Type u
inst_1 : (X Y : A) → FunLike.{u_2 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory A FC (CC := CC)
inst_3 : HasLimits.{u, u_1} A
inst_4 : PreservesLimits (forget A (FC := FC) (CC := CC))
inst_5 : Functor.ReflectsIsomorphisms (forget A (FC := FC) (CC := CC))
F : Presheaf A X
hF : F.IsSheaf
U : (Opens (↑X : Type u))ᵒᵖ
s t : ToType (FC := FC) (CC := CC) (F.obj U)
hst :
  ∀ x ∈ unop U,
    ∃ (V : Opens (↑X : Type u)) (hV : V ≤ unop U),
      x ∈ V ∧
        Eq (α := CC (F.obj (op V)))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE hV).op) :
                (a : CC (F.obj (op (unop U)))) → CC (F.obj (op V)))
              s :
            CC (F.obj (op V)))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE hV).op) :
                (a : CC (F.obj (op (unop U)))) → CC (F.obj (op V)))
              t :
            CC (F.obj (op V)))
⊢ s = t
have this : Presieve.IsSheaf (Opens.grothendieckTopology (↑X : Type u)) (F ⋙ forget A (FC := FC) (CC := CC))
Tactic: have := (isSheaf_iff_isSheaf_of_type _ _).mp
    ((Presheaf.isSheaf_iff_isSheaf_forget (C := Opens X) (A' := A) _ F (forget _)).mp hF)
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Sheaf (goal)
Goal:
X : TopCat
A : Type u_1
inst : Category.{u, u_1} A
FC : A → A → Type u_2
CC : A → Type u
inst_1 : (X Y : A) → FunLike.{u_2 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory A FC (CC := CC)
inst_3 : HasLimits.{u, u_1} A
inst_4 : PreservesLimits (forget A (FC := FC) (CC := CC))
inst_5 : Functor.ReflectsIsomorphisms (forget A (FC := FC) (CC := CC))
F : Presheaf A X
hF : F.IsSheaf
U : (Opens (↑X : Type u))ᵒᵖ
s t : ToType (FC := FC) (CC := CC) (F.obj U)
hst :
  ∀ x ∈ unop U,
    ∃ (V : Opens (↑X : Type u)) (hV : V ≤ unop U),
      x ∈ V ∧
        Eq (α := CC (F.obj (op V)))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE hV).op) :
                (a : CC (F.obj (op (unop U)))) → CC (F.obj (op V)))
              s :
            CC (F.obj (op V)))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE hV).op) :
                (a : CC (F.obj (op (unop U)))) → CC (F.obj (op V)))
              t :
            CC (F.obj (op V)))
this : Presieve.IsSheaf (Opens.grothendieckTopology (↑X : Type u)) (F ⋙ forget A (FC := FC) (CC := CC))
⊢ s = t
have choose : ∀ (V : (x : ↥(unop U)) → Opens (↑X : Type u)) (hV : ∀ (x : ↥(unop U)), V x ≤ unop U)
  (hxV : ∀ (x : ↥(unop U)), (↑x : (↑X : Type u)) ∈ V x)
  (H :
    ∀ (x : ↥(unop U)),
      Eq (α := CC (F.obj (op (V x))))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE sorry).op) :
              (a : CC (F.obj (op (unop U)))) → CC (F.obj (op (V x))))
            s :
          CC (F.obj (op (V x))))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE sorry).op) :
              (a : CC (F.obj (op (unop U)))) → CC (F.obj (op (V x))))
            t :
          CC (F.obj (op (V x))))),
  s = t
Tactic: choose V hV hxV H using fun x : U.unop ↦ hst x.1 x.2
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Sheaf (goal)
Goal:
X : TopCat
A : Type u_1
inst : Category.{u, u_1} A
FC : A → A → Type u_2
CC : A → Type u
inst_1 : (X Y : A) → FunLike.{u_2 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory A FC (CC := CC)
inst_3 : HasLimits.{u, u_1} A
inst_4 : PreservesLimits (forget A (FC := FC) (CC := CC))
inst_5 : Functor.ReflectsIsomorphisms (forget A (FC := FC) (CC := CC))
F : Presheaf A X
hF : F.IsSheaf
U : (Opens (↑X : Type u))ᵒᵖ
s t : ToType (FC := FC) (CC := CC) (F.obj U)
hst :
  ∀ x ∈ unop U,
    ∃ (V : Opens (↑X : Type u)) (hV : V ≤ unop U),
      x ∈ V ∧
        Eq (α := CC (F.obj (op V)))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE hV).op) :
                (a : CC (F.obj (op (unop U)))) → CC (F.obj (op V)))
              s :
            CC (F.obj (op V)))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE hV).op) :
                (a : CC (F.obj (op (unop U)))) → CC (F.obj (op V)))
              t :
            CC (F.obj (op V)))
this : Presieve.IsSheaf (Opens.grothendieckTopology (↑X : Type u)) (F ⋙ forget A (FC := FC) (CC := CC))
V : (x : ↥(unop U)) → Opens (↑X : Type u)
hV : ∀ (x : ↥(unop U)), V x ≤ unop U
hxV : ∀ (x : ↥(unop U)), (↑x : (↑X : Type u)) ∈ V x
H :
  ∀ (x : ↥(unop U)),
    Eq (α := CC (F.obj (op (V x))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE ⋯).op) :
            (a : CC (F.obj (op (unop U)))) → CC (F.obj (op (V x))))
          s :
        CC (F.obj (op (V x))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE ⋯).op) :
            (a : CC (F.obj (op (unop U)))) → CC (F.obj (op (V x))))
          t :
        CC (F.obj (op (V x))))
⊢ s = t
have refine_1 : Membership.mem (γ := Set (Sieve (unop U)))
  ((Opens.grothendieckTopology (↑X : Type u) : (a : Opens (↑X : Type u)) → Set (Sieve a)) (unop U))
  (Sieve.generate (Presieve.ofArrows V fun (x : ↥(unop U)) ↦ homOfLE sorry))
Tactic: refine (this.isSheafFor (.ofArrows V fun x ↦ homOfLE (hV x)) ?_).isSeparatedFor.ext ?_
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Sheaf (goal)
Goal:
X : TopCat
A : Type u_1
inst : Category.{u, u_1} A
FC : A → A → Type u_2
CC : A → Type u
inst_1 : (X Y : A) → FunLike.{u_2 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory A FC (CC := CC)
inst_3 : HasLimits.{u, u_1} A
inst_4 : PreservesLimits (forget A (FC := FC) (CC := CC))
inst_5 : Functor.ReflectsIsomorphisms (forget A (FC := FC) (CC := CC))
F : Presheaf A X
hF : F.IsSheaf
U : (Opens (↑X : Type u))ᵒᵖ
s t : ToType (FC := FC) (CC := CC) (F.obj U)
hst :
  ∀ x ∈ unop U,
    ∃ (V : Opens (↑X : Type u)) (hV : V ≤ unop U),
      x ∈ V ∧
        Eq (α := CC (F.obj (op V)))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE hV).op) :
                (a : CC (F.obj (op (unop U)))) → CC (F.obj (op V)))
              s :
            CC (F.obj (op V)))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE hV).op) :
                (a : CC (F.obj (op (unop U)))) → CC (F.obj (op V)))
              t :
            CC (F.obj (op V)))
this : Presieve.IsSheaf (Opens.grothendieckTopology (↑X : Type u)) (F ⋙ forget A (FC := FC) (CC := CC))
V : (x : ↥(unop U)) → Opens (↑X : Type u)
hV : ∀ (x : ↥(unop U)), V x ≤ unop U
hxV : ∀ (x : ↥(unop U)), (↑x : (↑X : Type u)) ∈ V x
H :
  ∀ (x : ↥(unop U)),
    Eq (α := CC (F.obj (op (V x))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE ⋯).op) :
            (a : CC (F.obj (op (unop U)))) → CC (F.obj (op (V x))))
          s :
        CC (F.obj (op (V x))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE ⋯).op) :
            (a : CC (F.obj (op (unop U)))) → CC (F.obj (op (V x))))
          t :
        CC (F.obj (op (V x))))
refine_1 :
  Membership.mem (γ := Set (Sieve (unop U)))
    ((Opens.grothendieckTopology (↑X : Type u) : (a : Opens (↑X : Type u)) → Set (Sieve a)) (unop U))
    (Sieve.generate (Presieve.ofArrows V fun (x : ↥(unop U)) ↦ homOfLE ⋯))
⊢ s = t
have refine_2 : ∀ ⦃Y : Opens (↑X : Type u)⦄ ⦃f : Y ⟶ unop U⦄,
  Presieve.ofArrows V (fun (x : ↥(unop U)) ↦ homOfLE sorry) f →
    Eq (α := (fun (X : Type u) ↦ X) ((F ⋙ forget A (FC := FC) (CC := CC)).obj (op Y)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget A (FC := FC) (CC := CC)).map f.op) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ forget A).obj (op (unop U)))) →
              (fun (X : Type u) ↦ X) ((F ⋙ forget A).obj (op Y)))
          s :
        (fun (X : Type u) ↦ X) ((F ⋙ forget A (FC := FC) (CC := CC)).obj (op Y)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget A (FC := FC) (CC := CC)).map f.op) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ forget A).obj (op (unop U)))) →
              (fun (X : Type u) ↦ X) ((F ⋙ forget A).obj (op Y)))
          t :
        (fun (X : Type u) ↦ X) ((F ⋙ forget A (FC := FC) (CC := CC)).obj (op Y)))
Tactic: refine (this.isSheafFor (.ofArrows V fun x ↦ homOfLE (hV x)) ?_).isSeparatedFor.ext ?_
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
ι : Type v'
U : ι → Opens (↑X : Type v')
i : ι
⊢ CategoryStruct.comp (Y := piOpens F U) (res F U)
      (limit.π (Discrete.functor fun (i : ι) ↦ F.obj (op (U i))) { as := i : Discrete ι }) =
    F.map (leSupr U i).op
have rw : CategoryStruct.comp (Y := piOpens F U) (Pi.lift fun (i : ι) ↦ F.map (leSupr U i).op)
    (limit.π (Discrete.functor fun (i : ι) ↦ F.obj (op (U i))) { as := i }) =
  F.map (leSupr U i).op
Tactic: rw [res, limit.lift_π, Fan.mk_π_app]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
ι : Type v'
U : ι → Opens (↑X : Type v')
i : ι
rw :
  CategoryStruct.comp (Y := piOpens F U) (Pi.lift fun (i : ι) ↦ F.map (leSupr U i).op)
      (limit.π (Discrete.functor fun (i : ι) ↦ F.obj (op (U i))) { as := i }) =
    F.map (leSupr U i).op
⊢ CategoryStruct.comp (Y := piOpens F U) (res F U)
      (limit.π (Discrete.functor fun (i : ι) ↦ F.obj (op (U i))) { as := i : Discrete ι }) =
    F.map (leSupr U i).op
have rw₁ : NatTrans.app (Cone.π (Fan.mk (F.obj (op (iSup U))) fun (i : ι) ↦ F.map (leSupr U i).op)) { as := i } =
  F.map (leSupr U i).op
Tactic: rw [res, limit.lift_π, Fan.mk_π_app]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
ι : Type v'
U : ι → Opens (↑X : Type v')
i : ι
rw :
  CategoryStruct.comp (Y := piOpens F U) (Pi.lift fun (i : ι) ↦ F.map (leSupr U i).op)
      (limit.π (Discrete.functor fun (i : ι) ↦ F.obj (op (U i))) { as := i }) =
    F.map (leSupr U i).op
rw₁ :
  NatTrans.app (Cone.π (Fan.mk (F.obj (op (iSup U))) fun (i : ι) ↦ F.map (leSupr U i).op)) { as := i } =
    F.map (leSupr U i).op
⊢ CategoryStruct.comp (Y := piOpens F U) (res F U)
      (limit.π (Discrete.functor fun (i : ι) ↦ F.obj (op (U i))) { as := i : Discrete ι }) =
    F.map (leSupr U i).op
have rw₂ : F.map (Quiver.Hom.op (leSupr U { as := i }.as)) = F.map (leSupr U i).op
Tactic: rw [res, limit.lift_π, Fan.mk_π_app]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
ι : Type v'
U : ι → Opens (↑X : Type v')
⊢ Eq (α := F.obj (op (iSup U)) ⟶ piInters F U) (res F U ≫ leftRes F U) (res F U ≫ rightRes F U)
have dsimp : Eq.{v + 1} (α := F.obj (op (iSup U)) ⟶ piInters F U)
  (CategoryStruct.comp (Y := piOpens F U) (Pi.lift fun (i : ι) ↦ F.map (leSupr U i).op)
    (Pi.lift fun (p : ι × ι) ↦
      Pi.π (fun (i : ι) ↦ F.obj (op (U i))) p.1 ≫ F.map (Quiver.Hom.op ((U p.1).infLELeft (U p.2)))))
  (CategoryStruct.comp (Y := piOpens F U) (Pi.lift fun (i : ι) ↦ F.map (leSupr U i).op)
    (Pi.lift fun (p : ι × ι) ↦
      Pi.π (fun (i : ι) ↦ F.obj (op (U i))) p.2 ≫ F.map (Quiver.Hom.op ((U p.1).infLERight (U p.2)))))
Tactic: dsimp [res, leftRes, rightRes]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
ι : Type v'
U : ι → Opens (↑X : Type v')
⊢ Eq.{v + 1} (α := F.obj (op (iSup U)) ⟶ piInters F U)
    (CategoryStruct.comp (Y := piOpens F U) (Pi.lift fun (i : ι) ↦ F.map (leSupr U i).op)
      (Pi.lift fun (p : ι × ι) ↦
        Pi.π (fun (i : ι) ↦ F.obj (op (U i))) p.1 ≫ F.map (Quiver.Hom.op ((U p.1).infLELeft (U p.2)))))
    (CategoryStruct.comp (Y := piOpens F U) (Pi.lift fun (i : ι) ↦ F.map (leSupr U i).op)
      (Pi.lift fun (p : ι × ι) ↦
        Pi.π (fun (i : ι) ↦ F.obj (op (U i))) p.2 ≫ F.map (Quiver.Hom.op ((U p.1).infLERight (U p.2)))))
have w₁ : ∀ (j : Discrete (ι × ι)),
  Eq.{v + 1} (α :=
    F.obj (op (iSup U)) ⟶ Functor.obj.{v', v, v', u} (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j)
    (CategoryStruct.comp (Y := piInters F U)
      (CategoryStruct.comp (Y := piOpens F U) (Pi.lift fun (i : ι) ↦ F.map (leSupr U i).op)
        (Pi.lift fun (p : ι × ι) ↦
          Pi.π (fun (i : ι) ↦ F.obj (op (U i))) p.1 ≫ F.map (Quiver.Hom.op ((U p.1).infLELeft (U p.2)))))
      (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j))
    (CategoryStruct.comp (Y := piInters F U)
      (CategoryStruct.comp (Y := piOpens F U) (Pi.lift fun (i : ι) ↦ F.map (leSupr U i).op)
        (Pi.lift fun (p : ι × ι) ↦
          Pi.π (fun (i : ι) ↦ F.obj (op (U i))) p.2 ≫ F.map (Quiver.Hom.op ((U p.1).infLERight (U p.2)))))
      (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j))
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
ι : Type v'
U : ι → Opens (↑X : Type v')
j : Discrete (ι × ι)
⊢ Eq.{v + 1} (α :=
    F.obj (op (iSup U)) ⟶ Functor.obj.{v', v, v', u} (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j)
    (CategoryStruct.comp (Y := piInters F U)
      (CategoryStruct.comp (Y := piOpens F U) (Pi.lift fun (i : ι) ↦ F.map (leSupr U i).op)
        (Pi.lift fun (p : ι × ι) ↦
          Pi.π (fun (i : ι) ↦ F.obj (op (U i))) p.1 ≫ F.map (Quiver.Hom.op ((U p.1).infLELeft (U p.2)))))
      (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j))
    (CategoryStruct.comp (Y := piInters F U)
      (CategoryStruct.comp (Y := piOpens F U) (Pi.lift fun (i : ι) ↦ F.map (leSupr U i).op)
        (Pi.lift fun (p : ι × ι) ↦
          Pi.π (fun (i : ι) ↦ F.obj (op (U i))) p.2 ≫ F.map (Quiver.Hom.op ((U p.1).infLERight (U p.2)))))
      (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j))
have w₁ : Eq (α :=
  F.obj (op (iSup U)) ⟶ Functor.obj.{v', v, v', u} (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j)
  (F.map (Quiver.Hom.op (leSupr U j.as.1)) ≫ F.map (Quiver.Hom.op ((U j.as.1).infLELeft (U j.as.2))))
  (F.map (Quiver.Hom.op (leSupr U j.as.2)) ≫ F.map (Quiver.Hom.op ((U j.as.1).infLERight (U j.as.2))))
Tactic: simp only [limit.lift_π, limit.lift_π_assoc, Fan.mk_π_app, Category.assoc]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
ι : Type v'
U : ι → Opens (↑X : Type v')
j : Discrete (ι × ι)
⊢ Eq (α :=
    F.obj (op (iSup U)) ⟶ Functor.obj.{v', v, v', u} (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j)
    (F.map (Quiver.Hom.op (leSupr U j.as.1)) ≫ F.map (Quiver.Hom.op ((U j.as.1).infLELeft (U j.as.2))))
    (F.map (Quiver.Hom.op (leSupr U j.as.2)) ≫ F.map (Quiver.Hom.op ((U j.as.1).infLERight (U j.as.2))))
have w₁ : Eq (α :=
  F.obj (op (iSup U)) ⟶ Functor.obj.{v', v, v', u} (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j)
  (F.map (Quiver.Hom.op (leSupr U j.as.1) ≫ Quiver.Hom.op ((U j.as.1).infLELeft (U j.as.2))))
  (F.map (Quiver.Hom.op (leSupr U j.as.2)) ≫ F.map (Quiver.Hom.op ((U j.as.1).infLERight (U j.as.2))))
Tactic: rw [← F.map_comp]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
ι : Type v'
U : ι → Opens (↑X : Type v')
j : Discrete (ι × ι)
⊢ Eq (α :=
    F.obj (op (iSup U)) ⟶ Functor.obj.{v', v, v', u} (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j)
    (F.map (Quiver.Hom.op (leSupr U j.as.1) ≫ Quiver.Hom.op ((U j.as.1).infLELeft (U j.as.2))))
    (F.map (Quiver.Hom.op (leSupr U j.as.2)) ≫ F.map (Quiver.Hom.op ((U j.as.1).infLERight (U j.as.2))))
have w₁ : Eq (α :=
  F.obj (op (iSup U)) ⟶ Functor.obj.{v', v, v', u} (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j)
  (F.map (Quiver.Hom.op (leSupr U j.as.1) ≫ Quiver.Hom.op ((U j.as.1).infLELeft (U j.as.2))))
  (F.map (Quiver.Hom.op (leSupr U j.as.2) ≫ Quiver.Hom.op ((U j.as.1).infLERight (U j.as.2))))
Tactic: rw [← F.map_comp]