awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.CochainComplexPlus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
J : Type u_2
inst_2 : SmallCategory J
inst_3 : FinCategory J
inst_4 : HasLimitsOfShape.{u_2, u_2, v_1, u_1} J C
K : CochainComplex.{v_1, u_1, 0} C ℤ
p : ObjectProperty.LimitOfShape (CochainComplex.plus C) J K
n : ℤ
hn : ∀ (j : J), (p.toLimitPresentation (P := CochainComplex.plus C).diag.obj j).IsStrictlyGE n
i : ℤ
hi : autoParam (i < n) isStrictlyGE_iff._auto_1
⊢ IsZero.{v_1, u_1} (K.X i)
have rw : Eq.{v_1 + 1} (α := K.X i ⟶ K.X i) (𝟙 (K.X i)) 0
Tactic: rw [IsZero.iff_id_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.CochainComplexPlus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
J : Type u_2
inst_2 : SmallCategory J
inst_3 : FinCategory J
inst_4 : HasColimitsOfShape.{u_2, u_2, v_1, u_1} J C
K : CochainComplex.{v_1, u_1, 0} C ℤ
p : ObjectProperty.ColimitOfShape (CochainComplex.plus C) J K
⊢ ∃ (n : ℤ), ∀ (j : J), (p.toColimitPresentation (P := CochainComplex.plus C).diag.obj j).IsStrictlyGE n
have choose : ∀ (n : (j : J) → ℤ)
  (hn : ∀ (j : J), (p.toColimitPresentation (P := CochainComplex.plus C).diag.obj j).IsStrictlyGE (n j)),
  ∃ (n : ℤ), ∀ (j : J), (p.toColimitPresentation (P := CochainComplex.plus C).diag.obj j).IsStrictlyGE n
Tactic: choose n hn using p.prop_diag_obj
-- Lean 4 proof step from Mathlib.Algebra.Homology.CochainComplexPlus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
J : Type u_2
inst_2 : SmallCategory J
inst_3 : FinCategory J
inst_4 : HasColimitsOfShape.{u_2, u_2, v_1, u_1} J C
K : CochainComplex.{v_1, u_1, 0} C ℤ
p : ObjectProperty.ColimitOfShape (CochainComplex.plus C) J K
⊢ CochainComplex.plus C K
have obtain : ∀ (n : ℤ) (hn : ∀ (j : J), (p.toColimitPresentation (P := CochainComplex.plus C).diag.obj j).IsStrictlyGE n),
  CochainComplex.plus C K
Tactic: obtain ⟨n, hn⟩ : ∃ (n : ℤ), ∀ (j : J), (p.diag.obj j).IsStrictlyGE n := by
      choose n hn using p.prop_diag_obj
      exact ⟨Finset.min' (Finset.image n ⊤ ∪ {0}) ⟨0, by grind⟩, fun j ↦
        (p.diag.obj j).isStrictlyGE_of_ge _ _ (Finset.min'_le _ (n j) (by simp))⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.CochainComplexPlus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
J : Type u_2
inst_2 : SmallCategory J
inst_3 : FinCategory J
inst_4 : HasColimitsOfShape.{u_2, u_2, v_1, u_1} J C
K : CochainComplex.{v_1, u_1, 0} C ℤ
p : ObjectProperty.ColimitOfShape (CochainComplex.plus C) J K
n : ℤ
hn : ∀ (j : J), (p.toColimitPresentation (P := CochainComplex.plus C).diag.obj j).IsStrictlyGE n
⊢ CochainComplex.plus C K
have refine : K.IsStrictlyGE n
Tactic: refine ⟨n, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.CochainComplexPlus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
J : Type u_2
inst_2 : SmallCategory J
inst_3 : FinCategory J
inst_4 : HasColimitsOfShape.{u_2, u_2, v_1, u_1} J C
K : CochainComplex.{v_1, u_1, 0} C ℤ
p : ObjectProperty.ColimitOfShape (CochainComplex.plus C) J K
n : ℤ
hn : ∀ (j : J), (p.toColimitPresentation (P := CochainComplex.plus C).diag.obj j).IsStrictlyGE n
⊢ K.IsStrictlyGE n
have rw : ∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero.{v_1, u_1} (K.X i)
Tactic: rw [isStrictlyGE_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.CochainComplexPlus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
J : Type u_2
inst_2 : SmallCategory J
inst_3 : FinCategory J
inst_4 : HasColimitsOfShape.{u_2, u_2, v_1, u_1} J C
K : CochainComplex.{v_1, u_1, 0} C ℤ
p : ObjectProperty.ColimitOfShape (CochainComplex.plus C) J K
n : ℤ
hn : ∀ (j : J), (p.toColimitPresentation (P := CochainComplex.plus C).diag.obj j).IsStrictlyGE n
i : ℤ
hi : autoParam (i < n) isStrictlyGE_iff._auto_1
⊢ IsZero.{v_1, u_1} (K.X i)
have rw : Eq.{v_1 + 1} (α := K.X i ⟶ K.X i) (𝟙 (K.X i)) 0
Tactic: rw [IsZero.iff_id_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.CochainComplexPlus (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
inst_4 : F.PreservesZeroMorphisms
K : CochainComplex.Plus.{v_1, u_1} C
⊢ CochainComplex.plus D (obj (CochainComplex.Plus.ι C ⋙ F.mapHomologicalComplex (ComplexShape.up ℤ)) K)
have obtain : ∀ (i : ℤ) (hi : K.obj (P := CochainComplex.plus C).IsStrictlyGE i),
  CochainComplex.plus D (obj (CochainComplex.Plus.ι C ⋙ F.mapHomologicalComplex (ComplexShape.up ℤ)) K)
Tactic: obtain ⟨i, hi⟩ := K.2
-- Lean 4 proof step from Mathlib.Algebra.Homology.CochainComplexPlus (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
inst_4 : F.PreservesZeroMorphisms
K : CochainComplex.Plus.{v_1, u_1} C
i : ℤ
hi : K.obj (P := CochainComplex.plus C).IsStrictlyGE i
⊢ CochainComplex.plus D (obj (CochainComplex.Plus.ι C ⋙ F.mapHomologicalComplex (ComplexShape.up ℤ)) K)
have refine : CochainComplex.IsStrictlyGE (obj (CochainComplex.Plus.ι C ⋙ F.mapHomologicalComplex (ComplexShape.up ℤ)) K) i
Tactic: refine ⟨i, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.CochainComplexPlus (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
inst_4 : F.PreservesZeroMorphisms
K : CochainComplex.Plus.{v_1, u_1} C
i : ℤ
hi : K.obj (P := CochainComplex.plus C).IsStrictlyGE i
⊢ CochainComplex.IsStrictlyGE (obj (CochainComplex.Plus.ι C ⋙ F.mapHomologicalComplex (ComplexShape.up ℤ)) K) i
have dsimp : CochainComplex.IsStrictlyGE (obj (F.mapHomologicalComplex (ComplexShape.up ℤ)) (K.obj (P := CochainComplex.plus C))) i
Tactic: dsimp [CochainComplex.Plus.ι]
-- Lean 4 proof step from Mathlib.Algebra.Homology.CommSq (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0
⊢ f ≫ biprod.inl ≫ s.π = g ≫ biprod.inr ≫ s.π
have rw : HSub.hSub (α := X₁ ⟶ biprod.{v_1, u_1} X₂ X₃) (f ≫ biprod.inl) (g ≫ biprod.inr) ≫ s.π = 0
Tactic: rw [← sub_eq_zero, ← assoc, ← assoc, ← Preadditive.sub_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.CommSq (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0
⊢ HSub.hSub (α := X₁ ⟶ biprod.{v_1, u_1} X₂ X₃) (f ≫ biprod.inl) (g ≫ biprod.inr) ≫ s.π = 0
have h₁ : HSub.hSub (α := X₁ ⟶ biprod.{v_1, u_1} X₂ X₃) (f ≫ biprod.inl) (g ≫ biprod.inr) = biprod.lift f (-g)
Tactic: convert! s.condition
-- Lean 4 proof step from Mathlib.Algebra.Homology.CommSq (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0
h₁ : HSub.hSub (α := X₁ ⟶ biprod.{v_1, u_1} X₂ X₃) (f ≫ biprod.inl) (g ≫ biprod.inr) = biprod.lift f (-g)
⊢ HSub.hSub (α := X₁ ⟶ biprod.{v_1, u_1} X₂ X₃) (f ≫ biprod.inl) (g ≫ biprod.inr) ≫ s.π = 0
have h₂ : Eq (α := X₁ ⟶ s.pt) 0 (0 ≫ s.π)
Tactic: convert! s.condition
-- Lean 4 proof step from Mathlib.Algebra.Homology.CommSq (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0
⊢ CategoryStruct.comp (Y :=
      Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) sq.cokernelCofork)
      (Cofork.π sq.cokernelCofork)
      ((fun (s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) ↦
          PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯)
        s) =
    s.π
have dsimp : biprod.desc inl inr ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) sorry = s.π
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.CommSq (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0
⊢ biprod.desc inl inr ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯ = s.π
have h₀ : CategoryStruct.comp (Y := biprod.{v_1, u_1} X₂ X₃) biprod.inl
    (biprod.desc inl inr ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) sorry) =
  biprod.inl ≫ s.π
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.CommSq (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0
h₀ :
  CategoryStruct.comp (Y := biprod.{v_1, u_1} X₂ X₃) biprod.inl
      (biprod.desc inl inr ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯) =
    biprod.inl ≫ s.π
⊢ biprod.desc inl inr ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯ = s.π
have h₁ : CategoryStruct.comp (Y := biprod.{v_1, u_1} X₂ X₃) biprod.inr
    (biprod.desc inl inr ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) sorry) =
  biprod.inr ≫ s.π
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.CommSq (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0
⊢ CategoryStruct.comp (Y := biprod.{v_1, u_1} X₂ X₃) biprod.inl
      (biprod.desc inl inr ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯) =
    biprod.inl ≫ s.π
have h₀ : inl ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) sorry = biprod.inl ≫ s.π
Tactic: simp only [biprod.inl_desc_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.CommSq (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0
⊢ CategoryStruct.comp (Y := biprod.{v_1, u_1} X₂ X₃) biprod.inr
      (biprod.desc inl inr ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯) =
    biprod.inr ≫ s.π
have h₁ : inr ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) sorry = biprod.inr ≫ s.π
Tactic: simp only [biprod.inr_desc_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.CommSq (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0
m : Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) sq.cokernelCofork ⟶ s.pt
hm : Cofork.π sq.cokernelCofork ≫ m = s.π
⊢ m =
    (fun (s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) ↦
        PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯)
      s
have h₀ : (PushoutCocone.mk inl inr sorry).inl ≫ m =
  (PushoutCocone.mk inl inr sorry).inl ≫
    (fun (s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) ↦
        PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) sorry)
      s
Tactic: apply PushoutCocone.IsColimit.hom_ext h
-- Lean 4 proof step from Mathlib.Algebra.Homology.CommSq (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0
m : Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) sq.cokernelCofork ⟶ s.pt
hm : Cofork.π sq.cokernelCofork ≫ m = s.π
h₀ :
  (PushoutCocone.mk inl inr ⋯).inl ≫ m =
    (PushoutCocone.mk inl inr ⋯).inl ≫
      (fun (s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) ↦
          PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯)
        s
⊢ m =
    (fun (s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) ↦
        PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯)
      s
have h₁ : (PushoutCocone.mk inl inr sorry).inr ≫ m =
  (PushoutCocone.mk inl inr sorry).inr ≫
    (fun (s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) ↦
        PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) sorry)
      s
Tactic: apply PushoutCocone.IsColimit.hom_ext h
-- Lean 4 proof step from Mathlib.Algebra.Homology.CommSq (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0
m : Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) sq.cokernelCofork ⟶ s.pt
hm : Cofork.π sq.cokernelCofork ≫ m = s.π
⊢ (PushoutCocone.mk inl inr ⋯).inl ≫ m =
    (PushoutCocone.mk inl inr ⋯).inl ≫
      (fun (s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) ↦
          PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯)
        s
have hm₁ : biprod.inl ≫ Cofork.π sq.cokernelCofork ≫ m = biprod.inl ≫ s.π
Tactic: replace hm := biprod.inl ≫= hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Algebra.Homology.CommSq (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0
m : Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) sq.cokernelCofork ⟶ s.pt
hm : biprod.inl ≫ Cofork.π sq.cokernelCofork ≫ m = biprod.inl ≫ s.π
⊢ (PushoutCocone.mk inl inr ⋯).inl ≫ m =
    (PushoutCocone.mk inl inr ⋯).inl ≫
      (fun (s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) ↦
          PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯)
        s
have h₀ : inl ≫ m = inl ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) sorry
Tactic: dsimp at hm ⊢
-- Lean 4 proof step from Mathlib.Algebra.Homology.CommSq (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0
m : Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) sq.cokernelCofork ⟶ s.pt
hm : CategoryStruct.comp (Y := biprod.{v_1, u_1} X₂ X₃) biprod.inl (biprod.desc inl inr ≫ m) = biprod.inl ≫ s.π
⊢ inl ≫ m = inl ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯
have hm₁ : inl ≫ m = biprod.inl ≫ s.π
Tactic: simp only [biprod.inl_desc_assoc] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Algebra.Homology.CommSq (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0
m : Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) sq.cokernelCofork ⟶ s.pt
hm : inl ≫ m = biprod.inl ≫ s.π
⊢ inl ≫ m = inl ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯
have h₀ : biprod.inl ≫ s.π = inl ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) sorry
Tactic: rw [hm]
-- Lean 4 proof step from Mathlib.Algebra.Homology.CommSq (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0
m : Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) sq.cokernelCofork ⟶ s.pt
hm : inl ≫ m = biprod.inl ≫ s.π
⊢ biprod.inl ≫ s.π = inl ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯
have h₀ : inl ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) sorry = biprod.inl ≫ s.π
Tactic: symm
-- Lean 4 proof step from Mathlib.Algebra.Homology.CommSq (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0
m : Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) sq.cokernelCofork ⟶ s.pt
hm : Cofork.π sq.cokernelCofork ≫ m = s.π
⊢ (PushoutCocone.mk inl inr ⋯).inr ≫ m =
    (PushoutCocone.mk inl inr ⋯).inr ≫
      (fun (s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) ↦
          PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯)
        s
have hm₁ : biprod.inr ≫ Cofork.π sq.cokernelCofork ≫ m = biprod.inr ≫ s.π
Tactic: replace hm := biprod.inr ≫= hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Algebra.Homology.CommSq (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0
m : Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) sq.cokernelCofork ⟶ s.pt
hm : biprod.inr ≫ Cofork.π sq.cokernelCofork ≫ m = biprod.inr ≫ s.π
⊢ (PushoutCocone.mk inl inr ⋯).inr ≫ m =
    (PushoutCocone.mk inl inr ⋯).inr ≫
      (fun (s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) ↦
          PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯)
        s
have h₁ : inr ≫ m = inr ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) sorry
Tactic: dsimp at hm ⊢
-- Lean 4 proof step from Mathlib.Algebra.Homology.CommSq (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0
m : Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) sq.cokernelCofork ⟶ s.pt
hm : CategoryStruct.comp (Y := biprod.{v_1, u_1} X₂ X₃) biprod.inr (biprod.desc inl inr ≫ m) = biprod.inr ≫ s.π
⊢ inr ≫ m = inr ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯
have hm₁ : inr ≫ m = biprod.inr ≫ s.π
Tactic: simp only [biprod.inr_desc_assoc] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Algebra.Homology.CommSq (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0
m : Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) sq.cokernelCofork ⟶ s.pt
hm : inr ≫ m = biprod.inr ≫ s.π
⊢ inr ≫ m = inr ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯
have h₁ : biprod.inr ≫ s.π = inr ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) sorry
Tactic: rw [hm]
-- Lean 4 proof step from Mathlib.Algebra.Homology.CommSq (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0
m : Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) sq.cokernelCofork ⟶ s.pt
hm : inr ≫ m = biprod.inr ≫ s.π
⊢ biprod.inr ≫ s.π = inr ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯
have h₁ : inr ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) sorry = biprod.inr ≫ s.π
Tactic: symm
-- Lean 4 proof step from Mathlib.Algebra.Homology.CommSq (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) sq.cokernelCofork
s : PushoutCocone f g
m : X₄ ⟶ s.pt
hm₁ : inl ≫ m = s.inl
hm₂ : inr ≫ m = s.inr
⊢ m =
    (fun (s : PushoutCocone f g) ↦
        (h.desc (CokernelCofork.ofπ (biprod.desc s.inl s.inr) ⋯) :
          Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) sq.cokernelCofork ⟶
            Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0)
              (CokernelCofork.ofπ (biprod.desc s.inl s.inr) ⋯)))
      s
have apply : Eq (α := biprod.{v_1, u_1} X₂ X₃ ⟶ s.pt) (Cofork.π sq.cokernelCofork ≫ m)
  (CategoryStruct.comp (Y :=
    Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) sq.cokernelCofork)
    (Cofork.π sq.cokernelCofork)
    ((fun (s : PushoutCocone f g) ↦
        (h.desc (CokernelCofork.ofπ (biprod.desc s.inl s.inr) sorry) :
          Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) sq.cokernelCofork ⟶
            Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0)
              (CokernelCofork.ofπ (biprod.desc s.inl s.inr) sorry)))
      s))
Tactic: apply Cofork.IsColimit.hom_ext h