awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} C (Type w)
u : F.Elementsᵒᵖ
X Y : C
f : X ⟶ Y
⊢ Eq (α :=
    (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj u).obj X ⟶
      (obj (obj (const F.Elementsᵒᵖ) F) u).obj Y)
    ((((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj u).map f ≫
        NatTrans.app (Cocone.ι (coconeπOpCompShrinkYonedaObj F Y)) u :
      (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj u).obj X ⟶
        (obj (obj (const F.Elementsᵒᵖ) F) u).obj Y)
    (NatTrans.app (Cocone.ι (coconeπOpCompShrinkYonedaObj F X)) u ≫ (obj (obj (const F.Elementsᵒᵖ) F) u).map f :
      (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj u).obj X ⟶
        (obj (obj (const F.Elementsᵒᵖ) F) u).obj Y)
have h : ∀ (x : (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj u).obj X),
  Eq (α := (obj (obj (const F.Elementsᵒᵖ) F) u).obj Y)
    (TypeCat.Fun.toFun
        (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
          ((((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj u).map f ≫
            NatTrans.app (Cocone.ι (coconeπOpCompShrinkYonedaObj F Y)) u))
        x :
      (obj (obj (const F.Elementsᵒᵖ) F) u).obj Y)
    (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app (Cocone.ι (coconeπOpCompShrinkYonedaObj F X)) u ≫ (obj (obj (const F.Elementsᵒᵖ) F) u).map f))
        x :
      (obj (obj (const F.Elementsᵒᵖ) F) u).obj Y)
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} C (Type w)
u : F.Elementsᵒᵖ
X Y : C
f : X ⟶ Y
x : (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj u).obj X
⊢ Eq (α := (obj (obj (const F.Elementsᵒᵖ) F) u).obj Y)
    (TypeCat.Fun.toFun
        (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
          ((((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj u).map f ≫
            NatTrans.app (Cocone.ι (coconeπOpCompShrinkYonedaObj F Y)) u))
        x :
      (obj (obj (const F.Elementsᵒᵖ) F) u).obj Y)
    (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app (Cocone.ι (coconeπOpCompShrinkYonedaObj F X)) u ≫ (obj (obj (const F.Elementsᵒᵖ) F) u).map f))
        x :
      (obj (obj (const F.Elementsᵒᵖ) F) u).obj Y)
have h : ∀ (x : unop ((CategoryOfElements.π F).op.obj u) ⟶ X),
  Eq (α := (obj (obj (const F.Elementsᵒᵖ) F) u).obj Y)
    (TypeCat.Fun.toFun (X := (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj u).obj X)
        (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            ((((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj u).map f ≫
              NatTrans.app (Cocone.ι (coconeπOpCompShrinkYonedaObj F Y)) u) :
          TypeCat.Fun ((((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj u).obj X)
            ((obj (obj (const F.Elementsᵒᵖ) F) u).obj Y))
        ((Equiv.symm shrinkYonedaObjObjEquiv :
              (a : unop ((CategoryOfElements.π F).op.obj u) ⟶ X) →
                (shrinkYoneda.{w, v₁, u₁}.obj X).obj ((CategoryOfElements.π F).op.obj u))
            x :
          obj.{v₁, w, u₁, w + 1} (obj shrinkYoneda.{w, v₁, u₁} X) ((CategoryOfElements.π F).op.obj u)) :
      (obj (obj (const F.Elementsᵒᵖ) F) u).obj Y)
    (TypeCat.Fun.toFun (X := (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj u).obj X)
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app (Cocone.ι (coconeπOpCompShrinkYonedaObj F X)) u ≫ (obj (obj (const F.Elementsᵒᵖ) F) u).map f))
        ((Equiv.symm shrinkYonedaObjObjEquiv :
            (a : unop ((CategoryOfElements.π F).op.obj u) ⟶ X) →
              (shrinkYoneda.{w, v₁, u₁}.obj X).obj ((CategoryOfElements.π F).op.obj u))
          x) :
      (obj (obj (const F.Elementsᵒᵖ) F) u).obj Y)
Tactic: obtain ⟨x, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} C (Type w)
u v : F.Elementsᵒᵖ
g : u ⟶ v
⊢ Eq (α :=
    ((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj u ⟶ obj (obj (const F.Elementsᵒᵖ) F) v)
    (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).map g ≫
      { app := fun (X : C) ↦ NatTrans.app (Cocone.ι (coconeπOpCompShrinkYonedaObj F X)) v, naturality := ⋯ })
    ({ app := fun (X : C) ↦ NatTrans.app (Cocone.ι (coconeπOpCompShrinkYonedaObj F X)) u, naturality := ⋯ } ≫
      map (obj (const F.Elementsᵒᵖ) F) g)
have w : ∀ (X : C) (x : (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj u).obj X),
  Eq (α := (obj (obj (const F.Elementsᵒᵖ) F) v).obj X)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).map g ≫
            { app := fun (X : C) ↦ NatTrans.app (Cocone.ι (coconeπOpCompShrinkYonedaObj F X)) v, naturality := sorry :
              NatTrans (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj v)
                (obj (obj (const F.Elementsᵒᵖ) F) v) })
          X))
      x)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ({ app := fun (X : C) ↦ NatTrans.app (Cocone.ι (coconeπOpCompShrinkYonedaObj F X)) u, naturality := sorry :
              NatTrans (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj u)
                (obj (obj (const F.Elementsᵒᵖ) F) u) } ≫
            map (obj (const F.Elementsᵒᵖ) F) g)
          X))
      x)
Tactic: ext X x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} C (Type w)
u v : F.Elementsᵒᵖ
g : u ⟶ v
X : C
x : (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj u).obj X
⊢ Eq (α := (obj (obj (const F.Elementsᵒᵖ) F) v).obj X)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).map g ≫
            { app := fun (X : C) ↦ NatTrans.app (Cocone.ι (coconeπOpCompShrinkYonedaObj F X)) v, naturality := ⋯ :
              NatTrans (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj v)
                (obj (obj (const F.Elementsᵒᵖ) F) v) })
          X))
      x)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ({ app := fun (X : C) ↦ NatTrans.app (Cocone.ι (coconeπOpCompShrinkYonedaObj F X)) u, naturality := ⋯ :
              NatTrans (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj u)
                (obj (obj (const F.Elementsᵒᵖ) F) u) } ≫
            map (obj (const F.Elementsᵒᵖ) F) g)
          X))
      x)
have w : ∀ (x : unop ((CategoryOfElements.π F).op.obj u) ⟶ X),
  Eq (α := (obj (obj (const F.Elementsᵒᵖ) F) v).obj X)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).map g ≫
            { app := fun (X : C) ↦ NatTrans.app (Cocone.ι (coconeπOpCompShrinkYonedaObj F X)) v, naturality := sorry :
              NatTrans (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj v)
                (obj (obj (const F.Elementsᵒᵖ) F) v) })
          X))
      ((Equiv.symm shrinkYonedaObjObjEquiv :
          (a : unop ((CategoryOfElements.π F).op.obj u) ⟶ X) →
            (shrinkYoneda.{w, v₁, u₁}.obj X).obj ((CategoryOfElements.π F).op.obj u))
        x))
    (TypeCat.Fun.toFun (X := (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj u).obj X)
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ({ app := fun (X : C) ↦ NatTrans.app (Cocone.ι (coconeπOpCompShrinkYonedaObj F X)) u, naturality := sorry :
              NatTrans (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj u)
                (obj (obj (const F.Elementsᵒᵖ) F) u) } ≫
            map (obj (const F.Elementsᵒᵖ) F) g)
          X))
      ((Equiv.symm shrinkYonedaObjObjEquiv :
          (a : unop ((CategoryOfElements.π F).op.obj u) ⟶ X) →
            (shrinkYoneda.{w, v₁, u₁}.obj X).obj ((CategoryOfElements.π F).op.obj u))
        x))
Tactic: obtain ⟨x, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Set (goal)
Goal:
J : Type w
inst : Category.{w', w} J
X : Type u
inst_1 : IsFilteredOrEmpty.{w', w} J
F : CategoryTheory.Functor.{w', u, w, u} J (Set X)
⊢ PreservesColimit F functorToTypes
have apply : IsColimit (F := F ⋙ functorToTypes) (Functor.mapCocone functorToTypes (colimitCocone F).cocone)
Tactic: apply preservesColimit_of_preserves_colimit_cocone (colimitCocone F).isColimit
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Set (goal)
Goal:
J : Type w
inst : Category.{w', w} J
X : Type u
inst_1 : IsFilteredOrEmpty.{w', w} J
F : CategoryTheory.Functor.{w', u, w, u} J (Set X)
⊢ IsColimit (F := F ⋙ functorToTypes) (Functor.mapCocone functorToTypes (colimitCocone F).cocone)
have hsurj : ∀ (x : Cocone.pt (F := F ⋙ functorToTypes) (Functor.mapCocone functorToTypes (colimitCocone F).cocone)),
  ∃ (i : J) (xi : (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj i)),
    x =
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (Functor.mapCocone functorToTypes (colimitCocone F).cocone)) i) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj i)) →
            (fun (X : Type u) ↦ X)
              (((Functor.const J).obj (functorToTypes.mapCocone (colimitCocone F).cocone).pt).obj i))
        xi
Tactic: apply Types.FilteredColimit.isColimitOf
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Set (hypothesis)
Goal:
J : Type w
inst : Category.{w', w} J
X : Type u
inst_1 : IsFilteredOrEmpty.{w', w} J
F : CategoryTheory.Functor.{w', u, w, u} J (Set X)
x : X
hx : x ∈ (colimitCocone F).cocone.pt
⊢ ∃ (i : J) (xi : (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj i)),
    Subtype.mk (p := fun (x : X) ↦ x ∈ (colimitCocone F).cocone.pt) x hx =
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (Functor.mapCocone functorToTypes (colimitCocone F).cocone)) i) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj i)) →
            (fun (X : Type u) ↦ X)
              (((Functor.const J).obj (functorToTypes.mapCocone (colimitCocone F).cocone).pt).obj i))
        xi
have hx₁ : ∃ (i : J), x ∈ F.obj i
Tactic: simp only [colimitCocone_cocone_pt, iSup_eq_iUnion, mem_iUnion] at hx
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Set (goal)
Goal:
J : Type w
inst : Category.{w', w} J
X : Type u
inst_1 : IsFilteredOrEmpty.{w', w} J
F : CategoryTheory.Functor.{w', u, w, u} J (Set X)
x : X
hx_1 : x ∈ (colimitCocone F).cocone.pt
hx : ∃ (i : J), x ∈ F.obj i
⊢ ∃ (i : J) (xi : (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj i)),
    Subtype.mk (p := fun (x : X) ↦ x ∈ (colimitCocone F).cocone.pt) x hx_1 =
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (Functor.mapCocone functorToTypes (colimitCocone F).cocone)) i) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj i)) →
            (fun (X : Type u) ↦ X)
              (((Functor.const J).obj (functorToTypes.mapCocone (colimitCocone F).cocone).pt).obj i))
        xi
have hsurj : ∀ (i : J) (hi : x ∈ F.obj i),
  ∃ (i : J) (xi : (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj i)),
    Subtype.mk (p := fun (x : X) ↦ x ∈ (colimitCocone F).cocone.pt) x hx_1 =
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (Functor.mapCocone functorToTypes (colimitCocone F).cocone)) i) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj i)) →
            (fun (X : Type u) ↦ X)
              (((Functor.const J).obj (functorToTypes.mapCocone (colimitCocone F).cocone).pt).obj i))
        xi
Tactic: obtain ⟨i, hi⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
P Q : C
c c' : BinaryBicone.{uC', uC} P Q
f g : c ⟶ c'
w : f.hom = g.hom
⊢ f = g
have mk : ∀ (hom : c.pt ⟶ c'.pt) (wfst : hom ≫ c'.fst = c.fst) (wsnd : hom ≫ c'.snd = c.snd) (winl : c.inl ≫ hom = c'.inl)
  (winr : c.inr ≫ hom = c'.inr)
  (w : { hom := hom, wfst := wfst, wsnd := wsnd, winl := winl, winr := winr : BinaryBiconeMorphism c c' }.hom = g.hom),
  { hom := hom, wfst := wfst, wsnd := wsnd, winl := winl, winr := winr : BinaryBiconeMorphism c c' } = g
Tactic: cases f
Cleared hypotheses: f, w
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
P Q : C
c c' : BinaryBicone.{uC', uC} P Q
g : c ⟶ c'
hom : c.pt ⟶ c'.pt
wfst : hom ≫ c'.fst = c.fst
wsnd : hom ≫ c'.snd = c.snd
winl : c.inl ≫ hom = c'.inl
winr : c.inr ≫ hom = c'.inr
w : { hom := hom, wfst := wfst, wsnd := wsnd, winl := winl, winr := winr : BinaryBiconeMorphism c c' }.hom = g.hom
⊢ { hom := hom, wfst := wfst, wsnd := wsnd, winl := winl, winr := winr : BinaryBiconeMorphism c c' } = g
have mk : ∀ (hom_1 : c.pt ⟶ c'.pt) (wfst_1 : hom_1 ≫ c'.fst = c.fst) (wsnd_1 : hom_1 ≫ c'.snd = c.snd)
  (winl_1 : c.inl ≫ hom_1 = c'.inl) (winr_1 : c.inr ≫ hom_1 = c'.inr)
  (w :
    { hom := hom, wfst := wfst, wsnd := wsnd, winl := winl, winr := winr : BinaryBiconeMorphism c c' }.hom =
      { hom := hom_1, wfst := wfst_1, wsnd := wsnd_1, winl := winl_1, winr := winr_1 }.hom),
  { hom := hom, wfst := wfst, wsnd := wsnd, winl := winl, winr := winr : BinaryBiconeMorphism c c' } =
    { hom := hom_1, wfst := wfst_1, wsnd := wsnd_1, winl := winl_1, winr := winr_1 }
Tactic: cases g
Cleared hypotheses: g, w
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P Q : C
F : Functor.{uC', uD', uC, uD} C D
inst_4 : F.PreservesZeroMorphisms
A : BinaryBicone.{uC', uC} P Q
⊢ F.map A.inl ≫ F.map A.fst = 𝟙 (F.obj P)
have rw : F.map (A.inl ≫ A.fst) = 𝟙 (F.obj P)
Tactic: rw [← F.map_comp, A.inl_fst, F.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P Q : C
F : Functor.{uC', uD', uC, uD} C D
inst_4 : F.PreservesZeroMorphisms
A : BinaryBicone.{uC', uC} P Q
rw : F.map (A.inl ≫ A.fst) = 𝟙 (F.obj P)
⊢ F.map A.inl ≫ F.map A.fst = 𝟙 (F.obj P)
have rw₁ : F.map (𝟙 P) = 𝟙 (F.obj P)
Tactic: rw [← F.map_comp, A.inl_fst, F.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P Q : C
F : Functor.{uC', uD', uC, uD} C D
inst_4 : F.PreservesZeroMorphisms
A : BinaryBicone.{uC', uC} P Q
rw : F.map (A.inl ≫ A.fst) = 𝟙 (F.obj P)
rw₁ : F.map (𝟙 P) = 𝟙 (F.obj P)
⊢ F.map A.inl ≫ F.map A.fst = 𝟙 (F.obj P)
have rw₂ : Eq.{uD' + 1} (α := F.obj P ⟶ F.obj P) (𝟙 (F.obj P)) (𝟙 (F.obj P))
Tactic: rw [← F.map_comp, A.inl_fst, F.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P Q : C
F : Functor.{uC', uD', uC, uD} C D
inst_4 : F.PreservesZeroMorphisms
A : BinaryBicone.{uC', uC} P Q
⊢ F.map A.inl ≫ F.map A.snd = 0
have rw : F.map (A.inl ≫ A.snd) = 0
Tactic: rw [← F.map_comp, A.inl_snd, F.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P Q : C
F : Functor.{uC', uD', uC, uD} C D
inst_4 : F.PreservesZeroMorphisms
A : BinaryBicone.{uC', uC} P Q
rw : F.map (A.inl ≫ A.snd) = 0
⊢ F.map A.inl ≫ F.map A.snd = 0
have rw₁ : Eq (α := F.obj P ⟶ F.obj Q) (F.map 0) 0
Tactic: rw [← F.map_comp, A.inl_snd, F.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P Q : C
F : Functor.{uC', uD', uC, uD} C D
inst_4 : F.PreservesZeroMorphisms
A : BinaryBicone.{uC', uC} P Q
rw : F.map (A.inl ≫ A.snd) = 0
rw₁ : Eq (α := F.obj P ⟶ F.obj Q) (F.map 0) 0
⊢ F.map A.inl ≫ F.map A.snd = 0
have rw₂ : Eq.{uD' + 1} (α := F.obj P ⟶ F.obj Q) 0 0
Tactic: rw [← F.map_comp, A.inl_snd, F.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P Q : C
F : Functor.{uC', uD', uC, uD} C D
inst_4 : F.PreservesZeroMorphisms
A : BinaryBicone.{uC', uC} P Q
⊢ F.map A.inr ≫ F.map A.fst = 0
have rw : F.map (A.inr ≫ A.fst) = 0
Tactic: rw [← F.map_comp, A.inr_fst, F.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P Q : C
F : Functor.{uC', uD', uC, uD} C D
inst_4 : F.PreservesZeroMorphisms
A : BinaryBicone.{uC', uC} P Q
rw : F.map (A.inr ≫ A.fst) = 0
⊢ F.map A.inr ≫ F.map A.fst = 0
have rw₁ : Eq (α := F.obj Q ⟶ F.obj P) (F.map 0) 0
Tactic: rw [← F.map_comp, A.inr_fst, F.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P Q : C
F : Functor.{uC', uD', uC, uD} C D
inst_4 : F.PreservesZeroMorphisms
A : BinaryBicone.{uC', uC} P Q
rw : F.map (A.inr ≫ A.fst) = 0
rw₁ : Eq (α := F.obj Q ⟶ F.obj P) (F.map 0) 0
⊢ F.map A.inr ≫ F.map A.fst = 0
have rw₂ : Eq.{uD' + 1} (α := F.obj Q ⟶ F.obj P) 0 0
Tactic: rw [← F.map_comp, A.inr_fst, F.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P Q : C
F : Functor.{uC', uD', uC, uD} C D
inst_4 : F.PreservesZeroMorphisms
A : BinaryBicone.{uC', uC} P Q
⊢ F.map A.inr ≫ F.map A.snd = 𝟙 (F.obj Q)
have rw : F.map (A.inr ≫ A.snd) = 𝟙 (F.obj Q)
Tactic: rw [← F.map_comp, A.inr_snd, F.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P Q : C
F : Functor.{uC', uD', uC, uD} C D
inst_4 : F.PreservesZeroMorphisms
A : BinaryBicone.{uC', uC} P Q
rw : F.map (A.inr ≫ A.snd) = 𝟙 (F.obj Q)
⊢ F.map A.inr ≫ F.map A.snd = 𝟙 (F.obj Q)
have rw₁ : F.map (𝟙 Q) = 𝟙 (F.obj Q)
Tactic: rw [← F.map_comp, A.inr_snd, F.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P Q : C
F : Functor.{uC', uD', uC, uD} C D
inst_4 : F.PreservesZeroMorphisms
A : BinaryBicone.{uC', uC} P Q
rw : F.map (A.inr ≫ A.snd) = 𝟙 (F.obj Q)
rw₁ : F.map (𝟙 Q) = 𝟙 (F.obj Q)
⊢ F.map A.inr ≫ F.map A.snd = 𝟙 (F.obj Q)
have rw₂ : Eq.{uD' + 1} (α := F.obj Q ⟶ F.obj Q) (𝟙 (F.obj Q)) (𝟙 (F.obj Q))
Tactic: rw [← F.map_comp, A.inr_snd, F.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P P' Q Q' X Y : C
b : BinaryBicone.{uC', uC} X Y
j j' : WalkingPair
⊢ Eq.{uC' + 1} (α := pairFunction X Y j ⟶ pairFunction X Y j')
    (CategoryStruct.comp (Y := b.pt)
        (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction X Y x ⟶ b.pt) j b.inl b.inr)
        (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ b.pt ⟶ pairFunction X Y x) j' b.fst b.snd) :
      pairFunction X Y j ⟶ pairFunction X Y j')
    (if h : j = j' then eqToHom ⋯ else 0 : pairFunction X Y j ⟶ pairFunction X Y j')
have left : Eq.{uC' + 1} (α := pairFunction X Y WalkingPair.left ⟶ pairFunction X Y j')
  (CategoryStruct.comp (Y := b.pt)
      (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction X Y x ⟶ b.pt) WalkingPair.left b.inl b.inr)
      (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ b.pt ⟶ pairFunction X Y x) j' b.fst b.snd) :
    pairFunction X Y WalkingPair.left ⟶ pairFunction X Y j')
  (if h : WalkingPair.left = j' then eqToHom sorry else 0 : pairFunction X Y WalkingPair.left ⟶ pairFunction X Y j')
Tactic: rcases j with ⟨⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P P' Q Q' X Y : C
b : BinaryBicone.{uC', uC} X Y
j j' : WalkingPair
left :
  Eq.{uC' + 1} (α := pairFunction X Y WalkingPair.left ⟶ pairFunction X Y j')
    (CategoryStruct.comp (Y := b.pt)
        (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction X Y x ⟶ b.pt) WalkingPair.left b.inl b.inr)
        (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ b.pt ⟶ pairFunction X Y x) j' b.fst b.snd) :
      pairFunction X Y WalkingPair.left ⟶ pairFunction X Y j')
    (if h : WalkingPair.left = j' then eqToHom ⋯ else 0 : pairFunction X Y WalkingPair.left ⟶ pairFunction X Y j')
⊢ Eq.{uC' + 1} (α := pairFunction X Y j ⟶ pairFunction X Y j')
    (CategoryStruct.comp (Y := b.pt)
        (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction X Y x ⟶ b.pt) j b.inl b.inr)
        (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ b.pt ⟶ pairFunction X Y x) j' b.fst b.snd) :
      pairFunction X Y j ⟶ pairFunction X Y j')
    (if h : j = j' then eqToHom ⋯ else 0 : pairFunction X Y j ⟶ pairFunction X Y j')
have right : Eq.{uC' + 1} (α := pairFunction X Y WalkingPair.right ⟶ pairFunction X Y j')
  (CategoryStruct.comp (Y := b.pt)
      (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction X Y x ⟶ b.pt) WalkingPair.right b.inl b.inr)
      (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ b.pt ⟶ pairFunction X Y x) j' b.fst b.snd) :
    pairFunction X Y WalkingPair.right ⟶ pairFunction X Y j')
  (if h : WalkingPair.right = j' then eqToHom sorry else 0 : pairFunction X Y WalkingPair.right ⟶ pairFunction X Y j')
Tactic: rcases j with ⟨⟩
Cleared hypotheses: j