awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ 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) ⋯) :
            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 h₁ : (biprod.{v_1, u_1} X₂ X₃ ⟶ s.pt) =
    ((parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0).obj WalkingParallelPair.one ⟶
      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)) →
  Eq (α := biprod.{v_1, u_1} X₂ X₃ ⟶ s.pt) (Cofork.π sq.cokernelCofork ≫ m : biprod.{v_1, u_1} X₂ X₃ ⟶ s.pt)
    (NatTrans.app (Cocone.ι (CokernelCofork.ofπ (biprod.desc s.inl s.inr) sorry)) WalkingParallelPair.one :
      (parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0).obj WalkingParallelPair.one ⟶
        Functor.obj.{0, v_1, 0, u_1}
          (Functor.obj (Functor.const WalkingParallelPair)
            (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)))
          WalkingParallelPair.one)
Tactic: convert!
          (h.fac (CokernelCofork.ofπ (biprod.desc s.inl s.inr) (by simp [s.condition])) .one).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₄
h : IsPushout f g inl inr
⊢ Epi (X := ShortComplex.X₂ ⋯.shortComplex) (ShortComplex.g ⋯.shortComplex)
have rw : ∀ (R : C) (g_1 : ShortComplex.X₃ sorry.shortComplex ⟶ R), ShortComplex.g sorry.shortComplex ≫ g_1 = 0 → g_1 = 0
Tactic: rw [Preadditive.epi_iff_cancel_zero]
-- 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₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit (PullbackCone.mk fst snd ⋯)
s : Fork (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0
⊢ (s.ι ≫ biprod.fst) ≫ f = (s.ι ≫ biprod.snd) ≫ g
have rw : s.ι ≫ HSub.hSub (α := biprod.{v_1, u_1} X₂ X₃ ⟶ X₄) (biprod.fst ≫ f) (biprod.snd ≫ g) = 0
Tactic: rw [← sub_eq_zero, assoc, assoc, ← Preadditive.comp_sub]
-- 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₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit (PullbackCone.mk fst snd ⋯)
s : Fork (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0
⊢ s.ι ≫ HSub.hSub (α := biprod.{v_1, u_1} X₂ X₃ ⟶ X₄) (biprod.fst ≫ f) (biprod.snd ≫ g) = 0
have h₁ : HSub.hSub (α := biprod.{v_1, u_1} X₂ X₃ ⟶ X₄) (biprod.fst ≫ f) (biprod.snd ≫ g) = biprod.desc 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₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit (PullbackCone.mk fst snd ⋯)
s : Fork (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0
h₁ : HSub.hSub (α := biprod.{v_1, u_1} X₂ X₃ ⟶ X₄) (biprod.fst ≫ f) (biprod.snd ≫ g) = biprod.desc f (-g)
⊢ s.ι ≫ HSub.hSub (α := biprod.{v_1, u_1} X₂ X₃ ⟶ X₄) (biprod.fst ≫ f) (biprod.snd ≫ g) = 0
have h₂ : Eq (α := s.pt ⟶ X₄) 0 (s.ι ≫ 0)
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₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit (PullbackCone.mk fst snd ⋯)
s : Fork (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0
⊢ CategoryStruct.comp (Y :=
      Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork)
      ((fun (s : Fork (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) ↦
          PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯)
        s)
      (Fork.ι sq.kernelFork) =
    s.ι
have dsimp : PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) sorry ≫ biprod.lift fst snd = 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₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit (PullbackCone.mk fst snd ⋯)
s : Fork (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0
⊢ PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ biprod.lift fst snd = s.ι
have h₀ : CategoryStruct.comp (Y := biprod.{v_1, u_1} X₂ X₃)
    (PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) sorry ≫ biprod.lift fst snd) biprod.fst =
  s.ι ≫ biprod.fst
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₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit (PullbackCone.mk fst snd ⋯)
s : Fork (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0
h₀ :
  CategoryStruct.comp (Y := biprod.{v_1, u_1} X₂ X₃)
      (PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ biprod.lift fst snd) biprod.fst =
    s.ι ≫ biprod.fst
⊢ PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ biprod.lift fst snd = s.ι
have h₁ : CategoryStruct.comp (Y := biprod.{v_1, u_1} X₂ X₃)
    (PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) sorry ≫ biprod.lift fst snd) biprod.snd =
  s.ι ≫ biprod.snd
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₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit (PullbackCone.mk fst snd ⋯)
s : Fork (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0
⊢ CategoryStruct.comp (Y := biprod.{v_1, u_1} X₂ X₃)
      (PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ biprod.lift fst snd) biprod.fst =
    s.ι ≫ biprod.fst
have h₀ : PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) sorry ≫ fst = s.ι ≫ biprod.fst
Tactic: simp only [assoc, biprod.lift_fst]
-- 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₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit (PullbackCone.mk fst snd ⋯)
s : Fork (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0
⊢ CategoryStruct.comp (Y := biprod.{v_1, u_1} X₂ X₃)
      (PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ biprod.lift fst snd) biprod.snd =
    s.ι ≫ biprod.snd
have h₁ : PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) sorry ≫ snd = s.ι ≫ biprod.snd
Tactic: simp only [assoc, biprod.lift_snd]
-- 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₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit (PullbackCone.mk fst snd ⋯)
s : Fork (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0
m : s.pt ⟶ Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork
hm : m ≫ Fork.ι sq.kernelFork = s.ι
⊢ m =
    (fun (s : Fork (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) ↦
        PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯)
      s
have h₀ : m ≫ (PullbackCone.mk fst snd sorry).fst =
  (fun (s : Fork (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) ↦
        PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) sorry)
      s ≫
    (PullbackCone.mk fst snd sorry).fst
Tactic: apply PullbackCone.IsLimit.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₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit (PullbackCone.mk fst snd ⋯)
s : Fork (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0
m : s.pt ⟶ Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork
hm : m ≫ Fork.ι sq.kernelFork = s.ι
h₀ :
  m ≫ (PullbackCone.mk fst snd ⋯).fst =
    (fun (s : Fork (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) ↦
          PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯)
        s ≫
      (PullbackCone.mk fst snd ⋯).fst
⊢ m =
    (fun (s : Fork (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) ↦
        PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯)
      s
have h₁ : m ≫ (PullbackCone.mk fst snd sorry).snd =
  (fun (s : Fork (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) ↦
        PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) sorry)
      s ≫
    (PullbackCone.mk fst snd sorry).snd
Tactic: apply PullbackCone.IsLimit.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₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit (PullbackCone.mk fst snd ⋯)
s : Fork (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0
m : s.pt ⟶ Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork
hm : m ≫ Fork.ι sq.kernelFork = s.ι
⊢ m ≫ (PullbackCone.mk fst snd ⋯).fst =
    (fun (s : Fork (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) ↦
          PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯)
        s ≫
      (PullbackCone.mk fst snd ⋯).fst
have hm₁ : (m ≫ Fork.ι sq.kernelFork) ≫ biprod.fst = s.ι ≫ biprod.fst
Tactic: replace hm := hm =≫ biprod.fst
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₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit (PullbackCone.mk fst snd ⋯)
s : Fork (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0
m : s.pt ⟶ Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork
hm : (m ≫ Fork.ι sq.kernelFork) ≫ biprod.fst = s.ι ≫ biprod.fst
⊢ m ≫ (PullbackCone.mk fst snd ⋯).fst =
    (fun (s : Fork (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) ↦
          PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯)
        s ≫
      (PullbackCone.mk fst snd ⋯).fst
have h₀ : m ≫ fst = PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) sorry ≫ fst
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₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit (PullbackCone.mk fst snd ⋯)
s : Fork (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0
m : s.pt ⟶ Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork
hm : CategoryStruct.comp (Y := biprod.{v_1, u_1} X₂ X₃) (m ≫ biprod.lift fst snd) biprod.fst = s.ι ≫ biprod.fst
⊢ m ≫ fst = PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ fst
have hm₁ : m ≫ fst = s.ι ≫ biprod.fst
Tactic: simp only [assoc, biprod.lift_fst] 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₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit (PullbackCone.mk fst snd ⋯)
s : Fork (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0
m : s.pt ⟶ Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork
hm : m ≫ fst = s.ι ≫ biprod.fst
⊢ m ≫ fst = PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ fst
have h₀ : s.ι ≫ biprod.fst = PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) sorry ≫ fst
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₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit (PullbackCone.mk fst snd ⋯)
s : Fork (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0
m : s.pt ⟶ Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork
hm : m ≫ fst = s.ι ≫ biprod.fst
⊢ s.ι ≫ biprod.fst = PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ fst
have h₀ : PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) sorry ≫ fst = s.ι ≫ biprod.fst
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₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit (PullbackCone.mk fst snd ⋯)
s : Fork (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0
m : s.pt ⟶ Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork
hm : m ≫ Fork.ι sq.kernelFork = s.ι
⊢ m ≫ (PullbackCone.mk fst snd ⋯).snd =
    (fun (s : Fork (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) ↦
          PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯)
        s ≫
      (PullbackCone.mk fst snd ⋯).snd
have hm₁ : (m ≫ Fork.ι sq.kernelFork) ≫ biprod.snd = s.ι ≫ biprod.snd
Tactic: replace hm := hm =≫ biprod.snd
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₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit (PullbackCone.mk fst snd ⋯)
s : Fork (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0
m : s.pt ⟶ Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork
hm : (m ≫ Fork.ι sq.kernelFork) ≫ biprod.snd = s.ι ≫ biprod.snd
⊢ m ≫ (PullbackCone.mk fst snd ⋯).snd =
    (fun (s : Fork (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) ↦
          PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯)
        s ≫
      (PullbackCone.mk fst snd ⋯).snd
have h₁ : m ≫ snd = PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) sorry ≫ snd
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₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit (PullbackCone.mk fst snd ⋯)
s : Fork (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0
m : s.pt ⟶ Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork
hm : CategoryStruct.comp (Y := biprod.{v_1, u_1} X₂ X₃) (m ≫ biprod.lift fst snd) biprod.snd = s.ι ≫ biprod.snd
⊢ m ≫ snd = PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ snd
have hm₁ : m ≫ snd = s.ι ≫ biprod.snd
Tactic: simp only [assoc, biprod.lift_snd] 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₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit (PullbackCone.mk fst snd ⋯)
s : Fork (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0
m : s.pt ⟶ Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork
hm : m ≫ snd = s.ι ≫ biprod.snd
⊢ m ≫ snd = PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ snd
have h₁ : s.ι ≫ biprod.snd = PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) sorry ≫ snd
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₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit (PullbackCone.mk fst snd ⋯)
s : Fork (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0
m : s.pt ⟶ Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork
hm : m ≫ snd = s.ι ≫ biprod.snd
⊢ s.ι ≫ biprod.snd = PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ snd
have h₁ : PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) sorry ≫ snd = s.ι ≫ biprod.snd
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₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork
s : PullbackCone f g
m : s.pt ⟶ X₁
hm₁ : m ≫ fst = s.fst
hm₂ : m ≫ snd = s.snd
⊢ m =
    (fun (s : PullbackCone f g) ↦
        (h.lift (KernelFork.ofι (biprod.lift s.fst s.snd) ⋯) :
          Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0)
              (KernelFork.ofι (biprod.lift s.fst s.snd) ⋯) ⟶
            Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork))
      s
have apply : Eq (α := s.pt ⟶ biprod.{v_1, u_1} X₂ X₃) (m ≫ Fork.ι sq.kernelFork)
  (CategoryStruct.comp (Y :=
    Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork)
    ((fun (s : PullbackCone f g) ↦
        (h.lift (KernelFork.ofι (biprod.lift s.fst s.snd) sorry) :
          Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0)
              (KernelFork.ofι (biprod.lift s.fst s.snd) sorry) ⟶
            Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork))
      s)
    (Fork.ι sq.kernelFork))
Tactic: apply Fork.IsLimit.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₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork
s : PullbackCone f g
m : s.pt ⟶ X₁
hm₁ : m ≫ fst = s.fst
hm₂ : m ≫ snd = s.snd
⊢ Eq (α := s.pt ⟶ biprod.{v_1, u_1} X₂ X₃) (m ≫ Fork.ι sq.kernelFork)
    (CategoryStruct.comp (Y :=
      Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork)
      ((fun (s : PullbackCone f g) ↦
          (h.lift (KernelFork.ofι (biprod.lift s.fst s.snd) ⋯) :
            Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0)
                (KernelFork.ofι (biprod.lift s.fst s.snd) ⋯) ⟶
              Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork))
        s)
      (Fork.ι sq.kernelFork))
have h₁ : (s.pt ⟶ biprod.{v_1, u_1} X₂ X₃) =
    (Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0)
        (KernelFork.ofι (biprod.lift s.fst s.snd) sorry) ⟶
      (parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0).obj WalkingParallelPair.zero) →
  Eq (α := s.pt ⟶ biprod.{v_1, u_1} X₂ X₃) (m ≫ Fork.ι sq.kernelFork)
    (NatTrans.app (Cone.π (KernelFork.ofι (biprod.lift s.fst s.snd) sorry)) WalkingParallelPair.zero)
Tactic: convert!
          (h.fac (KernelFork.ofι (biprod.lift s.fst s.snd) (by simp [s.condition])) .zero).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₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
h : IsPullback fst snd f g
⊢ Mono (X := ShortComplex.X₁ ⋯.shortComplex') (ShortComplex.f ⋯.shortComplex')
have rw : ∀ (P : C) (g_1 : P ⟶ ShortComplex.X₁ sorry.shortComplex'), g_1 ≫ ShortComplex.f sorry.shortComplex' = 0 → g_1 = 0
Tactic: rw [Preadditive.mono_iff_cancel_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShape (goal)
Goal:
ι : Type u_1
c₁ c₂ : ComplexShape ι
i j j' : ι
w : Relation.Comp c₁.Rel c₂.Rel i j
w' : Relation.Comp c₁.Rel c₂.Rel i j'
⊢ j = j'
have obtain : ∀ (k : ι) (w₁ : c₁.Rel i k) (w₂ : c₂.Rel k j), j = j'
Tactic: obtain ⟨k, w₁, w₂⟩ := w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShape (goal)
Goal:
ι : Type u_1
c₁ c₂ : ComplexShape ι
i j j' : ι
w' : Relation.Comp c₁.Rel c₂.Rel i j'
k : ι
w₁ : c₁.Rel i k
w₂ : c₂.Rel k j
⊢ j = j'
have obtain : ∀ (k' : ι) (w₁' : c₁.Rel i k') (w₂' : c₂.Rel k' j'), j = j'
Tactic: obtain ⟨k', w₁', w₂'⟩ := w'
Cleared hypotheses: w'
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShape (hypothesis)
Goal:
ι : Type u_1
c₁ c₂ : ComplexShape ι
i j j' k : ι
w₁ : c₁.Rel i k
w₂ : c₂.Rel k j
k' : ι
w₁' : c₁.Rel i k'
w₂' : c₂.Rel k' j'
⊢ j = j'
have w₃ : c₂.Rel k' j
Tactic: rw [c₁.next_eq w₁ w₁'] at w₂
Cleared hypotheses: w₂, w₁', w₂'
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShape (goal)
Goal:
ι : Type u_1
c₁ c₂ : ComplexShape ι
i i' j : ι
w : Relation.Comp c₁.Rel c₂.Rel i j
w' : Relation.Comp c₁.Rel c₂.Rel i' j
⊢ i = i'
have obtain : ∀ (k : ι) (w₁ : c₁.Rel i k) (w₂ : c₂.Rel k j), i = i'
Tactic: obtain ⟨k, w₁, w₂⟩ := w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShape (goal)
Goal:
ι : Type u_1
c₁ c₂ : ComplexShape ι
i i' j : ι
w' : Relation.Comp c₁.Rel c₂.Rel i' j
k : ι
w₁ : c₁.Rel i k
w₂ : c₂.Rel k j
⊢ i = i'
have obtain : ∀ (k' : ι) (w₁' : c₁.Rel i' k') (w₂' : c₂.Rel k' j), i = i'
Tactic: obtain ⟨k', w₁', w₂'⟩ := w'
Cleared hypotheses: w'