awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.AdditiveFunctor (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : HasBinaryBiproducts.{v₁, u₁} C
inst_5 : F.PreservesZeroMorphisms
inst_6 : PreservesBinaryBiproducts F
X Y : C
f g : X ⟶ Y
rw :
  F.map (CategoryStruct.comp (Y := biprod.{v₁, u₁} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g)) = F.map f + F.map g
rw₁ :
  CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X X)) (F.map (biprod.lift (𝟙 X) (𝟙 X))) (F.map (biprod.desc f g)) =
    F.map f + F.map g
rw₂ :
  CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X X))
      (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj X))
        (biprod.lift (F.map (𝟙 X)) (F.map (𝟙 X)) : F.obj X ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj X))
        (Iso.inv (F.mapBiprod X X) : biprod.{v₂, u₂} (F.obj X) (F.obj X) ⟶ F.obj (biprod.{v₁, u₁} X X)))
      (F.map (biprod.desc f g)) =
    F.map f + F.map g
rw₃ :
  CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X X))
      (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj X))
        (biprod.lift (F.map (𝟙 X)) (F.map (𝟙 X)) : F.obj X ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj X))
        (Iso.inv (F.mapBiprod X X) : biprod.{v₂, u₂} (F.obj X) (F.obj X) ⟶ F.obj (biprod.{v₁, u₁} X X)))
      (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj X))
        (Iso.hom (F.mapBiprod X X) : F.obj (biprod.{v₁, u₁} X X) ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj X))
        (biprod.desc (F.map f) (F.map g) : biprod.{v₂, u₂} (F.obj X) (F.obj X) ⟶ F.obj Y)) =
    F.map f + F.map g
rw₄ :
  CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj X))
      (biprod.lift (F.map (𝟙 X)) (F.map (𝟙 X)) : F.obj X ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj X))
      (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X X)) (Iso.inv (F.mapBiprod X X))
          (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj X))
            (Iso.hom (F.mapBiprod X X) : F.obj (biprod.{v₁, u₁} X X) ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj X))
            (biprod.desc (F.map f) (F.map g) : biprod.{v₂, u₂} (F.obj X) (F.obj X) ⟶ F.obj Y)) :
        biprod.{v₂, u₂} (F.obj X) (F.obj X) ⟶ F.obj Y) =
    F.map f + F.map g
rw₅ :
  CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj X)) (biprod.lift (F.map (𝟙 X)) (F.map (𝟙 X)))
      (biprod.desc (F.map f) (F.map g)) =
    F.map f + F.map g
⊢ F.map (f + g) = F.map f + F.map g
have rw₆ : CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj X)) (biprod.lift (𝟙 (F.obj X)) (𝟙 (F.obj X)))
    (biprod.desc (F.map f) (F.map g)) =
  F.map f + F.map g
Tactic: rw [biprod.add_eq_lift_id_desc, F.map_comp, ← biprod.lift_mapBiprod,
      ← biprod.mapBiprod_hom_desc, Category.assoc, Iso.inv_hom_id_assoc, F.map_id,
      biprod.add_eq_lift_id_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.AdditiveFunctor (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : HasBinaryBiproducts.{v₁, u₁} C
inst_5 : F.PreservesZeroMorphisms
inst_6 : PreservesBinaryBiproducts F
X Y : C
f g : X ⟶ Y
rw :
  F.map (CategoryStruct.comp (Y := biprod.{v₁, u₁} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g)) = F.map f + F.map g
rw₁ :
  CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X X)) (F.map (biprod.lift (𝟙 X) (𝟙 X))) (F.map (biprod.desc f g)) =
    F.map f + F.map g
rw₂ :
  CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X X))
      (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj X))
        (biprod.lift (F.map (𝟙 X)) (F.map (𝟙 X)) : F.obj X ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj X))
        (Iso.inv (F.mapBiprod X X) : biprod.{v₂, u₂} (F.obj X) (F.obj X) ⟶ F.obj (biprod.{v₁, u₁} X X)))
      (F.map (biprod.desc f g)) =
    F.map f + F.map g
rw₃ :
  CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X X))
      (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj X))
        (biprod.lift (F.map (𝟙 X)) (F.map (𝟙 X)) : F.obj X ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj X))
        (Iso.inv (F.mapBiprod X X) : biprod.{v₂, u₂} (F.obj X) (F.obj X) ⟶ F.obj (biprod.{v₁, u₁} X X)))
      (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj X))
        (Iso.hom (F.mapBiprod X X) : F.obj (biprod.{v₁, u₁} X X) ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj X))
        (biprod.desc (F.map f) (F.map g) : biprod.{v₂, u₂} (F.obj X) (F.obj X) ⟶ F.obj Y)) =
    F.map f + F.map g
rw₄ :
  CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj X))
      (biprod.lift (F.map (𝟙 X)) (F.map (𝟙 X)) : F.obj X ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj X))
      (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X X)) (Iso.inv (F.mapBiprod X X))
          (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj X))
            (Iso.hom (F.mapBiprod X X) : F.obj (biprod.{v₁, u₁} X X) ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj X))
            (biprod.desc (F.map f) (F.map g) : biprod.{v₂, u₂} (F.obj X) (F.obj X) ⟶ F.obj Y)) :
        biprod.{v₂, u₂} (F.obj X) (F.obj X) ⟶ F.obj Y) =
    F.map f + F.map g
rw₅ :
  CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj X)) (biprod.lift (F.map (𝟙 X)) (F.map (𝟙 X)))
      (biprod.desc (F.map f) (F.map g)) =
    F.map f + F.map g
rw₆ :
  CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj X)) (biprod.lift (𝟙 (F.obj X)) (𝟙 (F.obj X)))
      (biprod.desc (F.map f) (F.map g)) =
    F.map f + F.map g
⊢ F.map (f + g) = F.map f + F.map g
have rw₇ : CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj X)) (biprod.lift (𝟙 (F.obj X)) (𝟙 (F.obj X)))
    (biprod.desc (F.map f) (F.map g)) =
  CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj X)) (biprod.lift (𝟙 (F.obj X)) (𝟙 (F.obj X)))
    (biprod.desc (F.map f) (F.map g))
Tactic: rw [biprod.add_eq_lift_id_desc, F.map_comp, ← biprod.lift_mapBiprod,
      ← biprod.mapBiprod_hom_desc, Category.assoc, Iso.inv_hom_id_assoc, F.map_id,
      biprod.add_eq_lift_id_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.AdditiveFunctor (hypothesis)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : HasBinaryProducts.{v₁, u₁} C
inst_5 : PreservesLimitsOfShape (Discrete WalkingPair) F
inst_6 : F.PreservesZeroMorphisms
⊢ F.Additive
have this : HasBinaryBiproducts.{v₁, u₁} C
Tactic: have : HasBinaryBiproducts C := HasBinaryBiproducts.of_hasBinaryProducts
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.AdditiveFunctor (hypothesis)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : HasBinaryProducts.{v₁, u₁} C
inst_5 : PreservesLimitsOfShape (Discrete WalkingPair) F
inst_6 : F.PreservesZeroMorphisms
this : HasBinaryBiproducts.{v₁, u₁} C
⊢ F.Additive
have this₁ : PreservesBinaryBiproducts F
Tactic: have := preservesBinaryBiproducts_of_preservesBinaryProducts F
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.AdditiveFunctor (hypothesis)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
inst_4 : HasZeroObject.{v₁, u₁} C
inst_5 : HasZeroObject.{v₂, u₂} D
inst_6 : HasBinaryBiproducts.{v₁, u₁} C
F : Functor.{v₁, v₂, u₁, u₂} C D
h : leftExactFunctor C D F
⊢ additiveFunctor C D F
have h₁ : PreservesFiniteLimits F
Tactic: simp only [leftExactFunctor_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.AdditiveFunctor (hypothesis)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
inst_4 : HasZeroObject.{v₁, u₁} C
inst_5 : HasZeroObject.{v₂, u₂} D
inst_6 : HasBinaryBiproducts.{v₁, u₁} C
F : Functor.{v₁, v₂, u₁, u₂} C D
h : rightExactFunctor C D F
⊢ additiveFunctor C D F
have h₁ : PreservesFiniteColimits F
Tactic: simp only [rightExactFunctor_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
F : D → C
x x_1 x_2 : InducedCategory C F
x_3 x_4 : x ⟶ x_1
x_5 : x_1 ⟶ x_2
⊢ (x_3 + x_4) ≫ x_5 = x_3 ≫ x_5 + x_4 ≫ x_5
have h : ((x_3 + x_4) ≫ x_5).hom = (x_3 ≫ x_5 + x_4 ≫ x_5).hom
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
F : D → C
x x_1 x_2 : InducedCategory C F
x_3 : x ⟶ x_1
x_4 x_5 : x_1 ⟶ x_2
⊢ x_3 ≫ (x_4 + x_5) = x_3 ≫ x_4 + x_3 ≫ x_5
have h : (x_3 ≫ (x_4 + x_5)).hom = (x_3 ≫ x_4 + x_3 ≫ x_5).hom
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
Z : ObjectProperty.{v, u} C
x x_1 x_2 : Z.FullSubcategory
x_3 x_4 : x ⟶ x_1
x_5 : x_1 ⟶ x_2
⊢ (x_3 + x_4) ≫ x_5 = x_3 ≫ x_5 + x_4 ≫ x_5
have h : ((x_3 + x_4) ≫ x_5).hom = (x_3 ≫ x_5 + x_4 ≫ x_5).hom
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
Z : ObjectProperty.{v, u} C
x x_1 x_2 : Z.FullSubcategory
x_3 : x ⟶ x_1
x_4 x_5 : x_1 ⟶ x_2
⊢ x_3 ≫ (x_4 + x_5) = x_3 ≫ x_4 + x_3 ≫ x_5
have h : (x_3 ≫ (x_4 + x_5)).hom = (x_3 ≫ x_4 + x_3 ≫ x_5).hom
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P Q R S : C
J : Type u_1
s : Finset J
f : J → (P ⟶ Q)
g : J → (Q ⟶ R)
h : R ⟶ S
⊢ Eq (α := P ⟶ S) ((∑ j ∈ s, f j ≫ g j) ≫ h) (∑ j ∈ s, f j ≫ g j ≫ h)
have simp : Eq (α := P ⟶ S) ((∑ j ∈ s, f j ≫ g j) ≫ h) (∑ j ∈ s, (f j ≫ g j) ≫ h)
Tactic: simp only [← Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P_1 Q_1 R : C
f_1 f' : P_1 ⟶ Q_1
g_1 g'_1 : Q_1 ⟶ R
P Q : C
f : P ⟶ Q
inst_2 : Epi f
Z : C
g g' : Q ⟶ Z
H : (-f) ≫ g = (-f) ≫ g'
⊢ g = g'
have rwa : ∀ (H : -f ≫ g = (-f) ≫ g'), g = g'
Tactic: rwa [neg_comp, neg_comp, ← comp_neg, ← comp_neg, cancel_epi, neg_inj] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P_1 Q_1 R : C
f_1 f' : P_1 ⟶ Q_1
g_1 g'_1 : Q_1 ⟶ R
P Q : C
f : P ⟶ Q
inst_2 : Epi f
Z : C
g g' : Q ⟶ Z
H : (-f) ≫ g = (-f) ≫ g'
rwa : ∀ (H : -f ≫ g = (-f) ≫ g'), g = g'
⊢ g = g'
have rwa₁ : ∀ (H : -f ≫ g = -f ≫ g'), g = g'
Tactic: rwa [neg_comp, neg_comp, ← comp_neg, ← comp_neg, cancel_epi, neg_inj] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P_1 Q_1 R : C
f_1 f' : P_1 ⟶ Q_1
g_1 g'_1 : Q_1 ⟶ R
P Q : C
f : P ⟶ Q
inst_2 : Epi f
Z : C
g g' : Q ⟶ Z
H : (-f) ≫ g = (-f) ≫ g'
rwa : ∀ (H : -f ≫ g = (-f) ≫ g'), g = g'
rwa₁ : ∀ (H : -f ≫ g = -f ≫ g'), g = g'
⊢ g = g'
have rwa₂ : ∀ (H : f ≫ (-g) = -f ≫ g'), g = g'
Tactic: rwa [neg_comp, neg_comp, ← comp_neg, ← comp_neg, cancel_epi, neg_inj] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P_1 Q_1 R : C
f_1 f' : P_1 ⟶ Q_1
g_1 g'_1 : Q_1 ⟶ R
P Q : C
f : P ⟶ Q
inst_2 : Epi f
Z : C
g g' : Q ⟶ Z
H : (-f) ≫ g = (-f) ≫ g'
rwa : ∀ (H : -f ≫ g = (-f) ≫ g'), g = g'
rwa₁ : ∀ (H : -f ≫ g = -f ≫ g'), g = g'
rwa₂ : ∀ (H : f ≫ (-g) = -f ≫ g'), g = g'
⊢ g = g'
have rwa₃ : ∀ (H : f ≫ (-g) = f ≫ (-g')), g = g'
Tactic: rwa [neg_comp, neg_comp, ← comp_neg, ← comp_neg, cancel_epi, neg_inj] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P_1 Q_1 R : C
f_1 f' : P_1 ⟶ Q_1
g_1 g'_1 : Q_1 ⟶ R
P Q : C
f : P ⟶ Q
inst_2 : Epi f
Z : C
g g' : Q ⟶ Z
H : (-f) ≫ g = (-f) ≫ g'
rwa : ∀ (H : -f ≫ g = (-f) ≫ g'), g = g'
rwa₁ : ∀ (H : -f ≫ g = -f ≫ g'), g = g'
rwa₂ : ∀ (H : f ≫ (-g) = -f ≫ g'), g = g'
rwa₃ : ∀ (H : f ≫ (-g) = f ≫ (-g')), g = g'
⊢ g = g'
have rwa₄ : ∀ (H : -g = -g'), g = g'
Tactic: rwa [neg_comp, neg_comp, ← comp_neg, ← comp_neg, cancel_epi, neg_inj] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P_1 Q_1 R : C
f_1 f' : P_1 ⟶ Q_1
g_1 g'_1 : Q_1 ⟶ R
P Q : C
f : P ⟶ Q
inst_2 : Epi f
Z : C
g g' : Q ⟶ Z
H : (-f) ≫ g = (-f) ≫ g'
rwa : ∀ (H : -f ≫ g = (-f) ≫ g'), g = g'
rwa₁ : ∀ (H : -f ≫ g = -f ≫ g'), g = g'
rwa₂ : ∀ (H : f ≫ (-g) = -f ≫ g'), g = g'
rwa₃ : ∀ (H : f ≫ (-g) = f ≫ (-g')), g = g'
rwa₄ : ∀ (H : -g = -g'), g = g'
⊢ g = g'
have rwa₅ : ∀ (H : g = g'), g = g'
Tactic: rwa [neg_comp, neg_comp, ← comp_neg, ← comp_neg, cancel_epi, neg_inj] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P_1 Q_1 R : C
f_1 f' : P_1 ⟶ Q_1
g_1 g'_1 : Q_1 ⟶ R
P Q : C
f : P ⟶ Q
inst_2 : Mono f
Z : C
g g' : Z ⟶ P
H : g ≫ (-f) = g' ≫ (-f)
⊢ g = g'
have rwa : ∀ (H : -g ≫ f = g' ≫ (-f)), g = g'
Tactic: rwa [comp_neg, comp_neg, ← neg_comp, ← neg_comp, cancel_mono, neg_inj] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P_1 Q_1 R : C
f_1 f' : P_1 ⟶ Q_1
g_1 g'_1 : Q_1 ⟶ R
P Q : C
f : P ⟶ Q
inst_2 : Mono f
Z : C
g g' : Z ⟶ P
H : g ≫ (-f) = g' ≫ (-f)
rwa : ∀ (H : -g ≫ f = g' ≫ (-f)), g = g'
⊢ g = g'
have rwa₁ : ∀ (H : -g ≫ f = -g' ≫ f), g = g'
Tactic: rwa [comp_neg, comp_neg, ← neg_comp, ← neg_comp, cancel_mono, neg_inj] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P_1 Q_1 R : C
f_1 f' : P_1 ⟶ Q_1
g_1 g'_1 : Q_1 ⟶ R
P Q : C
f : P ⟶ Q
inst_2 : Mono f
Z : C
g g' : Z ⟶ P
H : g ≫ (-f) = g' ≫ (-f)
rwa : ∀ (H : -g ≫ f = g' ≫ (-f)), g = g'
rwa₁ : ∀ (H : -g ≫ f = -g' ≫ f), g = g'
⊢ g = g'
have rwa₂ : ∀ (H : (-g) ≫ f = -g' ≫ f), g = g'
Tactic: rwa [comp_neg, comp_neg, ← neg_comp, ← neg_comp, cancel_mono, neg_inj] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P_1 Q_1 R : C
f_1 f' : P_1 ⟶ Q_1
g_1 g'_1 : Q_1 ⟶ R
P Q : C
f : P ⟶ Q
inst_2 : Mono f
Z : C
g g' : Z ⟶ P
H : g ≫ (-f) = g' ≫ (-f)
rwa : ∀ (H : -g ≫ f = g' ≫ (-f)), g = g'
rwa₁ : ∀ (H : -g ≫ f = -g' ≫ f), g = g'
rwa₂ : ∀ (H : (-g) ≫ f = -g' ≫ f), g = g'
⊢ g = g'
have rwa₃ : ∀ (H : (-g) ≫ f = (-g') ≫ f), g = g'
Tactic: rwa [comp_neg, comp_neg, ← neg_comp, ← neg_comp, cancel_mono, neg_inj] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P_1 Q_1 R : C
f_1 f' : P_1 ⟶ Q_1
g_1 g'_1 : Q_1 ⟶ R
P Q : C
f : P ⟶ Q
inst_2 : Mono f
Z : C
g g' : Z ⟶ P
H : g ≫ (-f) = g' ≫ (-f)
rwa : ∀ (H : -g ≫ f = g' ≫ (-f)), g = g'
rwa₁ : ∀ (H : -g ≫ f = -g' ≫ f), g = g'
rwa₂ : ∀ (H : (-g) ≫ f = -g' ≫ f), g = g'
rwa₃ : ∀ (H : (-g) ≫ f = (-g') ≫ f), g = g'
⊢ g = g'
have rwa₄ : ∀ (H : -g = -g'), g = g'
Tactic: rwa [comp_neg, comp_neg, ← neg_comp, ← neg_comp, cancel_mono, neg_inj] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P_1 Q_1 R : C
f_1 f' : P_1 ⟶ Q_1
g_1 g'_1 : Q_1 ⟶ R
P Q : C
f : P ⟶ Q
inst_2 : Mono f
Z : C
g g' : Z ⟶ P
H : g ≫ (-f) = g' ≫ (-f)
rwa : ∀ (H : -g ≫ f = g' ≫ (-f)), g = g'
rwa₁ : ∀ (H : -g ≫ f = -g' ≫ f), g = g'
rwa₂ : ∀ (H : (-g) ≫ f = -g' ≫ f), g = g'
rwa₃ : ∀ (H : (-g) ≫ f = (-g') ≫ f), g = g'
rwa₄ : ∀ (H : -g = -g'), g = g'
⊢ g = g'
have rwa₅ : ∀ (H : g = g'), g = g'
Tactic: rwa [comp_neg, comp_neg, ← neg_comp, ← neg_comp, cancel_mono, neg_inj] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P Q R : C
f_1 f' : P ⟶ Q
g g' : Q ⟶ R
X : C
f : End X
⊢ 0 * f = 0
have dsimp : Eq (α := End X) (f ≫ 0) 0
Tactic: dsimp [mul]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P Q R : C
f_1 f' : P ⟶ Q
g g' : Q ⟶ R
X : C
f : End X
⊢ f * 0 = 0
have dsimp : Eq (α := End X) (0 ≫ f) 0
Tactic: dsimp [mul]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : HasLimit (parallelPair f 0)
w : Eq (α := kernel f ⟶ X) (kernel.ι f) 0
P : C
g : P ⟶ X
h : g ≫ f = 0
⊢ g = 0
have rw : CategoryStruct.comp (Y := kernel f) (kernel.lift f g h) (kernel.ι f) = 0
Tactic: rw [← kernel.lift_ι f g h, w, Limits.comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : HasLimit (parallelPair f 0)
w : Eq (α := kernel f ⟶ X) (kernel.ι f) 0
P : C
g : P ⟶ X
h : g ≫ f = 0
rw : CategoryStruct.comp (Y := kernel f) (kernel.lift f g h) (kernel.ι f) = 0
⊢ g = 0
have rw₁ : Eq (α := P ⟶ X) (CategoryStruct.comp (Y := kernel f) (kernel.lift f g h) 0) 0
Tactic: rw [← kernel.lift_ι f g h, w, Limits.comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : HasLimit (parallelPair f 0)
w : Eq (α := kernel f ⟶ X) (kernel.ι f) 0
P : C
g : P ⟶ X
h : g ≫ f = 0
rw : CategoryStruct.comp (Y := kernel f) (kernel.lift f g h) (kernel.ι f) = 0
rw₁ : Eq (α := P ⟶ X) (CategoryStruct.comp (Y := kernel f) (kernel.lift f g h) 0) 0
⊢ g = 0
have rw₂ : Eq.{v + 1} (α := P ⟶ X) 0 0
Tactic: rw [← kernel.lift_ι f g h, w, Limits.comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f : X ⟶ Y
c : KernelFork f
hc : IsLimit c
h : IsZero.{v, u} c.pt
P : C
g : P ⟶ X
hg : g ≫ f = 0
⊢ g = 0
have obtain : ∀ (a : P ⟶ c.pt) (ha : a ≫ Fork.ι c = g), g = 0
Tactic: obtain ⟨a, ha⟩ := KernelFork.IsLimit.lift' hc _ hg
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f : X ⟶ Y
c : KernelFork f
hc : IsLimit c
h : IsZero.{v, u} c.pt
P : C
g : P ⟶ X
hg : g ≫ f = 0
a : P ⟶ c.pt
ha : a ≫ Fork.ι c = g
⊢ g = 0
have rw : a ≫ Fork.ι c = 0
Tactic: rw [← ha, h.eq_of_tgt a 0, Limits.zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f : X ⟶ Y
c : KernelFork f
hc : IsLimit c
h : IsZero.{v, u} c.pt
P : C
g : P ⟶ X
hg : g ≫ f = 0
a : P ⟶ c.pt
ha : a ≫ Fork.ι c = g
rw : a ≫ Fork.ι c = 0
⊢ g = 0
have rw₁ : Eq (α := P ⟶ X) (0 ≫ Fork.ι c) 0
Tactic: rw [← ha, h.eq_of_tgt a 0, Limits.zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f : X ⟶ Y
c : KernelFork f
hc : IsLimit c
h : IsZero.{v, u} c.pt
P : C
g : P ⟶ X
hg : g ≫ f = 0
a : P ⟶ c.pt
ha : a ≫ Fork.ι c = g
rw : a ≫ Fork.ι c = 0
rw₁ : Eq (α := P ⟶ X) (0 ≫ Fork.ι c) 0
⊢ g = 0
have rw₂ : Eq.{v + 1} (α := P ⟶ X) 0 0
Tactic: rw [← ha, h.eq_of_tgt a 0, Limits.zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : HasColimit (parallelPair f 0)
w : Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0
R : C
g : Y ⟶ R
h : f ≫ g = 0
⊢ g = 0
have rw : CategoryStruct.comp (Y := cokernel f) (cokernel.π f) (cokernel.desc f g h) = 0
Tactic: rw [← cokernel.π_desc f g h, w, Limits.zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : HasColimit (parallelPair f 0)
w : Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0
R : C
g : Y ⟶ R
h : f ≫ g = 0
rw : CategoryStruct.comp (Y := cokernel f) (cokernel.π f) (cokernel.desc f g h) = 0
⊢ g = 0
have rw₁ : Eq (α := Y ⟶ R) (CategoryStruct.comp (Y := cokernel f) 0 (cokernel.desc f g h)) 0
Tactic: rw [← cokernel.π_desc f g h, w, Limits.zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : HasColimit (parallelPair f 0)
w : Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0
R : C
g : Y ⟶ R
h : f ≫ g = 0
rw : CategoryStruct.comp (Y := cokernel f) (cokernel.π f) (cokernel.desc f g h) = 0
rw₁ : Eq (α := Y ⟶ R) (CategoryStruct.comp (Y := cokernel f) 0 (cokernel.desc f g h)) 0
⊢ g = 0
have rw₂ : Eq.{v + 1} (α := Y ⟶ R) 0 0
Tactic: rw [← cokernel.π_desc f g h, w, Limits.zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
h : IsZero.{v, u} c.pt
R : C
g : Y ⟶ R
hg : f ≫ g = 0
⊢ g = 0
have obtain : ∀ (a : c.pt ⟶ R) (ha : Cofork.π c ≫ a = g), g = 0
Tactic: obtain ⟨a, ha⟩ := CokernelCofork.IsColimit.desc' hc _ hg
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
h : IsZero.{v, u} c.pt
R : C
g : Y ⟶ R
hg : f ≫ g = 0
a : c.pt ⟶ R
ha : Cofork.π c ≫ a = g
⊢ g = 0
have rw : Cofork.π c ≫ a = 0
Tactic: rw [← ha, h.eq_of_src a 0, Limits.comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
h : IsZero.{v, u} c.pt
R : C
g : Y ⟶ R
hg : f ≫ g = 0
a : c.pt ⟶ R
ha : Cofork.π c ≫ a = g
rw : Cofork.π c ≫ a = 0
⊢ g = 0
have rw₁ : Eq (α := Y ⟶ R) (Cofork.π c ≫ 0) 0
Tactic: rw [← ha, h.eq_of_src a 0, Limits.comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
h : IsZero.{v, u} c.pt
R : C
g : Y ⟶ R
hg : f ≫ g = 0
a : c.pt ⟶ R
ha : Cofork.π c ≫ a = g
rw : Cofork.π c ≫ a = 0
rw₁ : Eq (α := Y ⟶ R) (Cofork.π c ≫ 0) 0
⊢ g = 0
have rw₂ : Eq.{v + 1} (α := Y ⟶ R) 0 0
Tactic: rw [← ha, h.eq_of_src a 0, Limits.comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst_2 : IsIso f
⊢ f ≫ g = 0 ↔ g = 0
have rw : g = inv f ≫ 0 ↔ g = 0
Tactic: rw [← IsIso.eq_inv_comp, Limits.comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst_2 : IsIso f
rw : g = inv f ≫ 0 ↔ g = 0
⊢ f ≫ g = 0 ↔ g = 0
have rw₁ : g = 0 ↔ g = 0
Tactic: rw [← IsIso.eq_inv_comp, Limits.comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst_2 : IsIso g
⊢ f ≫ g = 0 ↔ f = 0
have rw : f = 0 ≫ inv g ↔ f = 0
Tactic: rw [← IsIso.eq_comp_inv, Limits.zero_comp]