awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
J' : Type w'
h : J ≃ J'
j : WidePushoutShape J'
⊢ Functor.obj
      (Functor.comp.{w', w, w', w', w, w'} (D := WidePushoutShape J)
        (wideSpan none (fun (j : J') ↦ some (h.invFun j)) fun (j : J') ↦ Hom.init (h.invFun j))
        (wideSpan none (fun (j : J) ↦ some ((h : (a : J) → J') j)) fun (j : J) ↦ Hom.init ((h : (a : J) → J') j)))
      j ≅
    Functor.obj (𝟭 (WidePushoutShape J')) j
have none : Iso (C := WidePushoutShape J')
  (Functor.obj (C := WidePushoutShape J')
    (Functor.comp.{w', w, w', w', w, w'} (D := WidePushoutShape J)
      (wideSpan none (fun (j : J') ↦ some (h.invFun j)) fun (j : J') ↦ Hom.init (h.invFun j))
      (wideSpan none (fun (j : J) ↦ some ((h : (a : J) → J') j)) fun (j : J) ↦ Hom.init ((h : (a : J) → J') j)))
    none)
  (Functor.obj (𝟭 (WidePushoutShape J')) none)
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
J' : Type w'
h : J ≃ J'
j : WidePushoutShape J'
none :
  Iso (C := WidePushoutShape J')
    (Functor.obj (C := WidePushoutShape J')
      (Functor.comp.{w', w, w', w', w, w'} (D := WidePushoutShape J)
        (wideSpan Option.none (fun (j : J') ↦ some (h.invFun j)) fun (j : J') ↦ Hom.init (h.invFun j))
        (wideSpan Option.none (fun (j : J) ↦ some ((h : (a : J) → J') j)) fun (j : J) ↦
          Hom.init ((h : (a : J) → J') j)))
      Option.none)
    (Functor.obj (𝟭 (WidePushoutShape J')) Option.none)
⊢ Functor.obj
      (Functor.comp.{w', w, w', w', w, w'} (D := WidePushoutShape J)
        (wideSpan Option.none (fun (j : J') ↦ some (h.invFun j)) fun (j : J') ↦ Hom.init (h.invFun j))
        (wideSpan Option.none (fun (j : J) ↦ some ((h : (a : J) → J') j)) fun (j : J) ↦
          Hom.init ((h : (a : J) → J') j)))
      j ≅
    Functor.obj (𝟭 (WidePushoutShape J')) j
have some : (val : J') →
  Functor.obj
      (Functor.comp.{w', w, w', w', w, w'} (D := WidePushoutShape J)
        (wideSpan Option.none (fun (j : J') ↦ some (h.invFun j)) fun (j : J') ↦ Hom.init (h.invFun j))
        (wideSpan Option.none (fun (j : J) ↦ some ((h : (a : J) → J') j)) fun (j : J) ↦
          Hom.init ((h : (a : J) → J') j)))
      (some val) ≅
    Functor.obj (𝟭 (WidePushoutShape J')) (some val)
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
inst_1 : HasWidePullback B objs arrows
X : C
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
g : X ⟶ widePullback B objs arrows
h1 : ∀ (j : J), g ≫ π arrows j = fs j
h2 : g ≫ base arrows = f
⊢ g = lift f fs w
have x : ∀ (j : WidePullbackShape J),
  g ≫ (limit.cone (WidePullbackShape.wideCospan B objs arrows)).π.app j =
    NatTrans.app (Cone.π (WidePullbackShape.mkCone f fs w)) j
Tactic: apply
    (limit.isLimit (WidePullbackShape.wideCospan B objs arrows)).uniq
      (WidePullbackShape.mkCone f fs <| w)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
inst_1 : HasWidePullback B objs arrows
X : C
g1 g2 : X ⟶ widePullback B objs arrows
h1 : ∀ (j : J), g1 ≫ π arrows j = g2 ≫ π arrows j
h2 : g1 ≫ base arrows = g2 ≫ base arrows
⊢ g1 = g2
have w : ∀ (j : WidePullbackShape J),
  g1 ≫ limit.π (WidePullbackShape.wideCospan B objs arrows) j =
    g2 ≫ limit.π (WidePullbackShape.wideCospan B objs arrows) j
Tactic: apply limit.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
lift : (t : WidePullbackCone f) → t.pt ⟶ s.pt
facbase : ∀ (t : WidePullbackCone f), lift t ≫ s.base = t.base
facπ : ∀ (t : WidePullbackCone f) (i : ι), lift t ≫ s.π i = t.π i
uniq : ∀ (t : WidePullbackCone f) (m : t.pt ⟶ s.pt), m ≫ s.base = t.base → (∀ (i : ι), m ≫ s.π i = t.π i) → m = lift t
t : Cone (WidePullbackShape.wideCospan X Y f)
j : WidePullbackShape ι
⊢ lift t ≫ s.π.app j = t.π.app j
have none : Eq (α := t.pt ⟶ (WidePullbackShape.wideCospan X Y f).obj none) (lift t ≫ s.π.app none) (t.π.app none)
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
lift : (t : WidePullbackCone f) → t.pt ⟶ s.pt
facbase : ∀ (t : WidePullbackCone f), lift t ≫ s.base = t.base
facπ : ∀ (t : WidePullbackCone f) (i : ι), lift t ≫ s.π i = t.π i
uniq : ∀ (t : WidePullbackCone f) (m : t.pt ⟶ s.pt), m ≫ s.base = t.base → (∀ (i : ι), m ≫ s.π i = t.π i) → m = lift t
t : Cone (WidePullbackShape.wideCospan X Y f)
j : WidePullbackShape ι
none :
  Eq (α := t.pt ⟶ (WidePullbackShape.wideCospan X Y f).obj Option.none) (lift t ≫ s.π.app Option.none)
    (t.π.app Option.none)
⊢ lift t ≫ s.π.app j = t.π.app j
have some : ∀ (val : ι),
  Eq (α := t.pt ⟶ (WidePullbackShape.wideCospan X Y f).obj (some val)) (lift t ≫ s.π.app (some val))
    (t.π.app (some val))
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks (goal)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
hs : IsLimit s
W : C
k l : W ⟶ s.pt
hbase : k ≫ s.base = l ≫ s.base
hπ : ∀ (i : ι), k ≫ s.π i = l ≫ s.π i
⊢ k = l
have apply : ∀ (j : WidePullbackShape ι), k ≫ s.π.app j = l ≫ s.π.app j
Tactic: apply hs.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst_1 : HasWidePushout B objs arrows
X : C
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g : widePushout B objs arrows ⟶ X
h1 : ∀ (j : J), ι arrows j ≫ g = fs j
h2 : head arrows ≫ g = f
⊢ g = desc f fs w
have x : ∀ (j : WidePushoutShape J),
  (colimit.cocone (WidePushoutShape.wideSpan B objs arrows)).ι.app j ≫ g =
    NatTrans.app (Cocone.ι (WidePushoutShape.mkCocone f fs w)) j
Tactic: apply
    (colimit.isColimit (WidePushoutShape.wideSpan B objs arrows)).uniq
      (WidePushoutShape.mkCocone f fs <| w)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks (goal)
Goal:
J : Type w
C_1 : Type u
inst : Category.{v, u} C_1
C : Type u
inst_1 : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst_2 : HasWidePushout B objs arrows
X : C
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g : widePushout B objs arrows ⟶ X
j : J
⊢ arrows j ≫ (fun (j : J) ↦ ι arrows j ≫ g) j = head arrows ≫ g
have rw : (arrows j ≫ ι arrows j) ≫ g = head arrows ≫ g
Tactic: rw [← Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst_1 : HasWidePushout B objs arrows
X : C
g1 g2 : widePushout B objs arrows ⟶ X
h1 : ∀ (j : J), ι arrows j ≫ g1 = ι arrows j ≫ g2
h2 : head arrows ≫ g1 = head arrows ≫ g2
⊢ g1 = g2
have w : ∀ (j : WidePushoutShape J),
  colimit.ι (WidePushoutShape.wideSpan B objs arrows) j ≫ g1 =
    colimit.ι (WidePushoutShape.wideSpan B objs arrows) j ≫ g2
Tactic: apply colimit.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y : Discrete PUnit.{u_1 + 1}
⊢ Zero (X ⟶ Y)
have zero : X ⟶ Y
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y : Discrete PUnit.{u_1 + 1}
⊢ X ⟶ Y
have zero : PLift (X.as = Y.as)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y : Discrete PUnit.{u_1 + 1}
⊢ PLift (X.as = Y.as)
have zero : X.as = Y.as
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y : Discrete PUnit.{u_1 + 1}
⊢ Zero (X ⟶ Y)
have zero : X ⟶ Y
Tactic: repeat (constructor)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y : Discrete PUnit.{u_1 + 1}
zero : X ⟶ Y
⊢ Zero (X ⟶ Y)
have zero₁ : PLift (X.as = Y.as)
Tactic: repeat (constructor)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y : Discrete PUnit.{u_1 + 1}
zero : X ⟶ Y
zero₁ : PLift (X.as = Y.as)
⊢ Zero (X ⟶ Y)
have zero₂ : X.as = Y.as
Tactic: repeat (constructor)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
I J : HasZeroMorphisms.{v, u} C
w : ∀ (X Y : C), Eq.{v + 1} (α := X ⟶ Y) Zero.zero Zero.zero
⊢ Eq (α := (X Y : C) → Zero (X ⟶ Y)) zero zero
have h : ∀ (X Y : C), Eq.{v + 1} (α := Zero (X ⟶ Y)) (zero X Y) (zero X Y)
Tactic: funext X Y
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
I J : HasZeroMorphisms.{v, u} C
w : ∀ (X Y : C), Eq.{v + 1} (α := X ⟶ Y) Zero.zero Zero.zero
X Y : C
⊢ Eq.{v + 1} (α := Zero (X ⟶ Y)) (zero X Y) (zero X Y)
have w₁ : Eq.{v + 1} (α := X ⟶ Y) Zero.zero Zero.zero
Tactic: specialize w X Y
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
I J : HasZeroMorphisms.{v, u} C
w : ∀ (X Y : C), Eq.{v + 1} (α := X ⟶ Y) Zero.zero Zero.zero
⊢ I = J
have this : Eq (α := (X Y : C) → Zero (X ⟶ Y)) zero zero
Tactic: have : I.zero = J.zero := by
    funext X Y
    specialize w X Y
    apply congrArg Zero.mk w
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
I J : HasZeroMorphisms.{v, u} C
w : ∀ (X Y : C), Eq.{v + 1} (α := X ⟶ Y) Zero.zero Zero.zero
this : Eq (α := (X Y : C) → Zero (X ⟶ Y)) zero zero
⊢ I = J
have mk : ∀ [zero : (X Y : C) → Zero (X ⟶ Y)] (comp_zero : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), Eq (α := X ⟶ Z) (f ≫ 0) 0)
  (zero_comp : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), Eq (α := X ⟶ Z) (0 ≫ f) 0)
  (w : ∀ (X Y : C), Eq.{v + 1} (α := X ⟶ Y) Zero.zero Zero.zero)
  (this : Eq (α := (X Y : C) → Zero (X ⟶ Y)) HasZeroMorphisms.zero HasZeroMorphisms.zero),
  { zero := zero, comp_zero := @comp_zero, zero_comp := zero_comp : HasZeroMorphisms.{v, u} C } = J
Tactic: cases I
Cleared hypotheses: I, w, this
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : HasZeroMorphisms.{v, u} C
zero : (X Y : C) → Zero (X ⟶ Y)
comp_zero : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), Eq (α := X ⟶ Z) (f ≫ 0) 0
zero_comp : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), Eq (α := X ⟶ Z) (0 ≫ f) 0
w : ∀ (X Y : C), Eq.{v + 1} (α := X ⟶ Y) Zero.zero Zero.zero
this : Eq (α := (X Y : C) → Zero (X ⟶ Y)) HasZeroMorphisms.zero HasZeroMorphisms.zero
⊢ { zero := zero, comp_zero := @comp_zero, zero_comp := zero_comp : HasZeroMorphisms.{v, u} C } = J
have mk : ∀ [zero_1 : (X Y : C) → Zero (X ⟶ Y)] (comp_zero_1 : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), Eq (α := X ⟶ Z) (f ≫ 0) 0)
  (zero_comp_1 : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), Eq (α := X ⟶ Z) (0 ≫ f) 0)
  (w : ∀ (X Y : C), Eq.{v + 1} (α := X ⟶ Y) Zero.zero Zero.zero)
  (this : Eq (α := (X Y : C) → Zero (X ⟶ Y)) HasZeroMorphisms.zero HasZeroMorphisms.zero),
  { zero := zero, comp_zero := @comp_zero, zero_comp := zero_comp : HasZeroMorphisms.{v, u} C } =
    { zero := zero_1, comp_zero := @comp_zero_1, zero_comp := zero_comp_1 }
Tactic: cases J
Cleared hypotheses: J, w, this
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
zero : (X Y : C) → Zero (X ⟶ Y)
comp_zero : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), Eq (α := X ⟶ Z) (f ≫ 0) 0
zero_comp : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), Eq (α := X ⟶ Z) (0 ≫ f) 0
zero_1 : (X Y : C) → Zero (X ⟶ Y)
comp_zero_1 : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), Eq (α := X ⟶ Z) (f ≫ 0) 0
zero_comp_1 : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), Eq (α := X ⟶ Z) (0 ≫ f) 0
w : ∀ (X Y : C), Eq.{v + 1} (α := X ⟶ Y) Zero.zero Zero.zero
this : Eq (α := (X Y : C) → Zero (X ⟶ Y)) HasZeroMorphisms.zero HasZeroMorphisms.zero
⊢ { zero := zero, comp_zero := @comp_zero, zero_comp := zero_comp : HasZeroMorphisms.{v, u} C } =
    { zero := zero_1, comp_zero := @comp_zero_1, zero_comp := zero_comp_1 }
have mk : @comp_zero ≍ @comp_zero_1
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
zero : (X Y : C) → Zero (X ⟶ Y)
comp_zero : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), Eq (α := X ⟶ Z) (f ≫ 0) 0
zero_comp : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), Eq (α := X ⟶ Z) (0 ≫ f) 0
zero_1 : (X Y : C) → Zero (X ⟶ Y)
comp_zero_1 : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), Eq (α := X ⟶ Z) (f ≫ 0) 0
zero_comp_1 : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), Eq (α := X ⟶ Z) (0 ≫ f) 0
w : ∀ (X Y : C), Eq.{v + 1} (α := X ⟶ Y) Zero.zero Zero.zero
this : Eq (α := (X Y : C) → Zero (X ⟶ Y)) HasZeroMorphisms.zero HasZeroMorphisms.zero
mk : @comp_zero ≍ @comp_zero_1
⊢ { zero := zero, comp_zero := @comp_zero, zero_comp := zero_comp : HasZeroMorphisms.{v, u} C } =
    { zero := zero_1, comp_zero := @comp_zero_1, zero_comp := zero_comp_1 }
have mk₁ : zero_comp ≍ zero_comp_1
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
I J : HasZeroMorphisms.{v, u} C
⊢ I = J
have w : ∀ (X Y : C), Eq.{v + 1} (α := X ⟶ Y) Zero.zero Zero.zero
Tactic: apply ext_aux
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
I J : HasZeroMorphisms.{v, u} C
X Y : C
⊢ Eq.{v + 1} (α := X ⟶ Y) Zero.zero Zero.zero
have this : Eq.{v + 1} (α := X ⟶ Y) (CategoryStruct.comp (Y := Y) Zero.zero Zero.zero) Zero.zero
Tactic: have : (I.zero X Y).zero ≫ (J.zero Y Y).zero = (I.zero X Y).zero := by
    apply I.zero_comp X (J.zero Y Y).zero
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
I J : HasZeroMorphisms.{v, u} C
X Y : C
this : Eq.{v + 1} (α := X ⟶ Y) (CategoryStruct.comp (Y := Y) Zero.zero Zero.zero) Zero.zero
⊢ Eq.{v + 1} (α := X ⟶ Y) Zero.zero Zero.zero
have that : Eq.{v + 1} (α := X ⟶ Y) (CategoryStruct.comp (Y := Y) Zero.zero Zero.zero) Zero.zero
Tactic: have that : (I.zero X Y).zero ≫ (J.zero Y Y).zero = (J.zero X Y).zero := by
    apply J.comp_zero (I.zero X Y).zero Y
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
I J : HasZeroMorphisms.{v, u} C
X Y : C
this : Eq.{v + 1} (α := X ⟶ Y) (CategoryStruct.comp (Y := Y) Zero.zero Zero.zero) Zero.zero
that : Eq.{v + 1} (α := X ⟶ Y) (CategoryStruct.comp (Y := Y) Zero.zero Zero.zero) Zero.zero
w : Eq.{v + 1} (α := X ⟶ Y) (CategoryStruct.comp (Y := Y) Zero.zero Zero.zero) Zero.zero
⊢ Eq.{v + 1} (α := X ⟶ Y) Zero.zero Zero.zero
have w₁ : Eq.{v + 1} (α := X ⟶ Y) (CategoryStruct.comp (Y := Y) Zero.zero Zero.zero)
  (CategoryStruct.comp (Y := Y) Zero.zero Zero.zero)
Tactic: rw [← this, ← that]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : HasImage f
w : Eq (α := image f ⟶ Y) (image.ι f) 0
⊢ f = 0
have rw : CategoryStruct.comp (Y := image f) (factorThruImage f) (image.ι f) = 0
Tactic: rw [← image.fac f, w, HasZeroMorphisms.comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : HasImage f
w : Eq (α := image f ⟶ Y) (image.ι f) 0
rw : CategoryStruct.comp (Y := image f) (factorThruImage f) (image.ι f) = 0
⊢ f = 0
have rw₁ : Eq (α := X ⟶ Y) (CategoryStruct.comp (Y := image f) (factorThruImage f) 0) 0
Tactic: rw [← image.fac f, w, HasZeroMorphisms.comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : HasImage f
w : Eq (α := image f ⟶ Y) (image.ι f) 0
rw : CategoryStruct.comp (Y := image f) (factorThruImage f) (image.ι f) = 0
rw₁ : Eq (α := X ⟶ Y) (CategoryStruct.comp (Y := image f) (factorThruImage f) 0) 0
⊢ f = 0
have rw₂ : Eq.{v + 1} (α := X ⟶ Y) 0 0
Tactic: rw [← image.fac f, w, HasZeroMorphisms.comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroMorphisms.{v', u'} D
X Y : Functor.{v, v', u, u'} C D
η : X ⟶ Y
H : Functor.{v, v', u, u'} C D
⊢ Eq (α := X ⟶ H) (η ≫ 0) 0
have w : ∀ (X_1 : C), Eq (α := X.obj X_1 ⟶ H.obj X_1) (NatTrans.app (η ≫ 0) X_1) (NatTrans.app 0 X_1)
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroMorphisms.{v', u'} D
X_1 Y : Functor.{v, v', u, u'} C D
η : X_1 ⟶ Y
H : Functor.{v, v', u, u'} C D
X : C
⊢ Eq (α := X_1.obj X ⟶ H.obj X) (NatTrans.app (η ≫ 0) X) (NatTrans.app 0 X)
have w : Eq (α := X_1.obj X ⟶ H.obj X) (η.app X ≫ NatTrans.app 0 X) (NatTrans.app 0 X)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroMorphisms.{v', u'} D
F G H : Functor.{v, v', u, u'} C D
η : G ⟶ H
⊢ Eq (α := F ⟶ H) (0 ≫ η) 0
have w : ∀ (X : C), Eq (α := F.obj X ⟶ H.obj X) (NatTrans.app (0 ≫ η) X) (NatTrans.app 0 X)
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroMorphisms.{v', u'} D
F G H : Functor.{v, v', u, u'} C D
η : G ⟶ H
X : C
⊢ Eq (α := F.obj X ⟶ H.obj X) (NatTrans.app (0 ≫ η) X) (NatTrans.app 0 X)
have w : Eq (α := F.obj X ⟶ H.obj X) (NatTrans.app 0 X ≫ η.app X) (NatTrans.app 0 X)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X : C
h : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0
Y : C
f : X ⟶ Y
⊢ f = default
have rw : Eq.{v + 1} (α := X ⟶ Y) 0 default
Tactic: rw [← id_comp f, ← id_comp (0 : X ⟶ Y), h, zero_comp, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X : C
h : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0
Y : C
f : Y ⟶ X
⊢ f = default
have rw : Eq.{v + 1} (α := Y ⟶ X) 0 default
Tactic: rw [← comp_id f, ← comp_id (0 : Y ⟶ X), h, comp_zero, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : Mono f
h : f = 0
⊢ IsZero.{v, u} X
have inst : Mono.{v, u} (C := C) (X := X) (Y := Y) 0
Tactic: subst h
Cleared hypotheses: f, inst_2, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : Epi f
h : f = 0
⊢ IsZero.{v, u} Y
have inst : Epi.{v, u} (C := C) (X := X) (Y := Y) 0
Tactic: subst h
Cleared hypotheses: f, inst_2, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : IsSplitMono f
⊢ IsZero.{v, u} X ↔ f = 0
have rw : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0 ↔ f = 0
Tactic: rw [iff_id_eq_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : IsSplitMono f
⊢ Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0 ↔ f = 0
have mp : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0 → f = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : IsSplitMono f
mp : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0 → f = 0
⊢ Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0 ↔ f = 0
have mpr : f = 0 → Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : IsSplitMono f
h : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0
⊢ f = 0
have mp : 𝟙 X ≫ f = 0
Tactic: rw [← Category.id_comp f, h, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : IsSplitMono f
h : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0
mp : 𝟙 X ≫ f = 0
⊢ f = 0
have mp₁ : Eq (α := X ⟶ Y) (0 ≫ f) 0
Tactic: rw [← Category.id_comp f, h, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : IsSplitMono f
h : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0
mp : 𝟙 X ≫ f = 0
mp₁ : Eq (α := X ⟶ Y) (0 ≫ f) 0
⊢ f = 0
have mp₂ : Eq.{v + 1} (α := X ⟶ Y) 0 0
Tactic: rw [← Category.id_comp f, h, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : IsSplitMono f
h : f = 0
⊢ Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0
have mpr : f ≫ retraction f = 0
Tactic: rw [← IsSplitMono.id f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : IsSplitEpi f
⊢ IsZero.{v, u} Y ↔ f = 0
have rw : Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0 ↔ f = 0
Tactic: rw [iff_id_eq_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : IsSplitEpi f
⊢ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0 ↔ f = 0
have mp : Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0 → f = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : IsSplitEpi f
mp : Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0 → f = 0
⊢ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0 ↔ f = 0
have mpr : f = 0 → Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : IsSplitEpi f
h : Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0
⊢ f = 0
have mp : f ≫ 𝟙 Y = 0
Tactic: rw [← Category.comp_id f, h, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : IsSplitEpi f
h : Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0
mp : f ≫ 𝟙 Y = 0
⊢ f = 0
have mp₁ : Eq (α := X ⟶ Y) (f ≫ 0) 0
Tactic: rw [← Category.comp_id f, h, comp_zero]