awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
W' : C
x : W' ⟶ S₁.X₂
hx : x ≫ S₁.g = 0
b : W' ⟶ h.K
hb : b ≫ i = x
rw : b ≫ h.i = (fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx ≫ h.i
⊢ b = (fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx
have rw₁ : (b ≫ h.i) ≫ inv φ.τ₂ =
  ((fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) sorry) x hx ≫ h.i) ≫ inv φ.τ₂
Tactic: rw [← cancel_mono h.i, ← cancel_mono (inv φ.τ₂), assoc, assoc,
      hb, liftK_i_assoc, assoc, IsIso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
W' : C
x : W' ⟶ S₁.X₂
hx : x ≫ S₁.g = 0
b : W' ⟶ h.K
hb : b ≫ i = x
rw : b ≫ h.i = (fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx ≫ h.i
rw₁ :
  (b ≫ h.i) ≫ inv φ.τ₂ =
    ((fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx ≫ h.i) ≫ inv φ.τ₂
⊢ b = (fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx
have rw₂ : b ≫ h.i ≫ inv φ.τ₂ = ((fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) sorry) x hx ≫ h.i) ≫ inv φ.τ₂
Tactic: rw [← cancel_mono h.i, ← cancel_mono (inv φ.τ₂), assoc, assoc,
      hb, liftK_i_assoc, assoc, IsIso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
W' : C
x : W' ⟶ S₁.X₂
hx : x ≫ S₁.g = 0
b : W' ⟶ h.K
hb : b ≫ i = x
rw : b ≫ h.i = (fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx ≫ h.i
rw₁ :
  (b ≫ h.i) ≫ inv φ.τ₂ =
    ((fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx ≫ h.i) ≫ inv φ.τ₂
rw₂ :
  b ≫ h.i ≫ inv φ.τ₂ =
    ((fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx ≫ h.i) ≫ inv φ.τ₂
⊢ b = (fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx
have rw₃ : b ≫ h.i ≫ inv φ.τ₂ = (fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) sorry) x hx ≫ h.i ≫ inv φ.τ₂
Tactic: rw [← cancel_mono h.i, ← cancel_mono (inv φ.τ₂), assoc, assoc,
      hb, liftK_i_assoc, assoc, IsIso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
W' : C
x : W' ⟶ S₁.X₂
hx : x ≫ S₁.g = 0
b : W' ⟶ h.K
hb : b ≫ i = x
rw : b ≫ h.i = (fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx ≫ h.i
rw₁ :
  (b ≫ h.i) ≫ inv φ.τ₂ =
    ((fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx ≫ h.i) ≫ inv φ.τ₂
rw₂ :
  b ≫ h.i ≫ inv φ.τ₂ =
    ((fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx ≫ h.i) ≫ inv φ.τ₂
rw₃ :
  b ≫ h.i ≫ inv φ.τ₂ = (fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx ≫ h.i ≫ inv φ.τ₂
⊢ b = (fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx
have rw₄ : x = (fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) sorry) x hx ≫ h.i ≫ inv φ.τ₂
Tactic: rw [← cancel_mono h.i, ← cancel_mono (inv φ.τ₂), assoc, assoc,
      hb, liftK_i_assoc, assoc, IsIso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
W' : C
x : W' ⟶ S₁.X₂
hx : x ≫ S₁.g = 0
b : W' ⟶ h.K
hb : b ≫ i = x
rw : b ≫ h.i = (fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx ≫ h.i
rw₁ :
  (b ≫ h.i) ≫ inv φ.τ₂ =
    ((fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx ≫ h.i) ≫ inv φ.τ₂
rw₂ :
  b ≫ h.i ≫ inv φ.τ₂ =
    ((fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx ≫ h.i) ≫ inv φ.τ₂
rw₃ :
  b ≫ h.i ≫ inv φ.τ₂ = (fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx ≫ h.i ≫ inv φ.τ₂
rw₄ : x = (fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx ≫ h.i ≫ inv φ.τ₂
⊢ b = (fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx
have rw₅ : x = (x ≫ φ.τ₂) ≫ inv φ.τ₂
Tactic: rw [← cancel_mono h.i, ← cancel_mono (inv φ.τ₂), assoc, assoc,
      hb, liftK_i_assoc, assoc, IsIso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
W' : C
x : W' ⟶ S₁.X₂
hx : x ≫ S₁.g = 0
b : W' ⟶ h.K
hb : b ≫ i = x
rw : b ≫ h.i = (fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx ≫ h.i
rw₁ :
  (b ≫ h.i) ≫ inv φ.τ₂ =
    ((fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx ≫ h.i) ≫ inv φ.τ₂
rw₂ :
  b ≫ h.i ≫ inv φ.τ₂ =
    ((fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx ≫ h.i) ≫ inv φ.τ₂
rw₃ :
  b ≫ h.i ≫ inv φ.τ₂ = (fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx ≫ h.i ≫ inv φ.τ₂
rw₄ : x = (fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx ≫ h.i ≫ inv φ.τ₂
rw₅ : x = (x ≫ φ.τ₂) ≫ inv φ.τ₂
⊢ b = (fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx
have rw₆ : x = x ≫ φ.τ₂ ≫ inv φ.τ₂
Tactic: rw [← cancel_mono h.i, ← cancel_mono (inv φ.τ₂), assoc, assoc,
      hb, liftK_i_assoc, assoc, IsIso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
W' : C
x : W' ⟶ S₁.X₂
hx : x ≫ S₁.g = 0
b : W' ⟶ h.K
hb : b ≫ i = x
rw : b ≫ h.i = (fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx ≫ h.i
rw₁ :
  (b ≫ h.i) ≫ inv φ.τ₂ =
    ((fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx ≫ h.i) ≫ inv φ.τ₂
rw₂ :
  b ≫ h.i ≫ inv φ.τ₂ =
    ((fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx ≫ h.i) ≫ inv φ.τ₂
rw₃ :
  b ≫ h.i ≫ inv φ.τ₂ = (fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx ≫ h.i ≫ inv φ.τ₂
rw₄ : x = (fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx ≫ h.i ≫ inv φ.τ₂
rw₅ : x = (x ≫ φ.τ₂) ≫ inv φ.τ₂
rw₆ : x = x ≫ φ.τ₂ ≫ inv φ.τ₂
⊢ b = (fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx
have rw₇ : x = x ≫ 𝟙 S₁.X₂
Tactic: rw [← cancel_mono h.i, ← cancel_mono (inv φ.τ₂), assoc, assoc,
      hb, liftK_i_assoc, assoc, IsIso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
W' : C
x : W' ⟶ S₁.X₂
hx : x ≫ S₁.g = 0
b : W' ⟶ h.K
hb : b ≫ i = x
rw : b ≫ h.i = (fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx ≫ h.i
rw₁ :
  (b ≫ h.i) ≫ inv φ.τ₂ =
    ((fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx ≫ h.i) ≫ inv φ.τ₂
rw₂ :
  b ≫ h.i ≫ inv φ.τ₂ =
    ((fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx ≫ h.i) ≫ inv φ.τ₂
rw₃ :
  b ≫ h.i ≫ inv φ.τ₂ = (fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx ≫ h.i ≫ inv φ.τ₂
rw₄ : x = (fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx ≫ h.i ≫ inv φ.τ₂
rw₅ : x = (x ≫ φ.τ₂) ≫ inv φ.τ₂
rw₆ : x = x ≫ φ.τ₂ ≫ inv φ.τ₂
rw₇ : x = x ≫ 𝟙 S₁.X₂
⊢ b = (fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx
have rw₈ : x = x
Tactic: rw [← cancel_mono h.i, ← cancel_mono (inv φ.τ₂), assoc, assoc,
      hb, liftK_i_assoc, assoc, IsIso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
⊢ S₁.LeftHomologyData
have have : (hi : IsLimit (KernelFork.ofι i wi)) → S₁.LeftHomologyData
Tactic: have hi : IsLimit (KernelFork.ofι i wi) := KernelFork.IsLimit.ofι _ _
    (fun x hx => h.liftK (x ≫ φ.τ₂)
      (by rw [assoc, φ.comm₂₃, reassoc_of% hx, zero_comp]))
    (fun x hx => by simp [i])
    (fun x hx b hb => by rw [← cancel_mono h.i, ← cancel_mono (inv φ.τ₂), assoc, assoc,
      hb, liftK_i_assoc, assoc, IsIso.hom_inv_id, comp_id])
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₁.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₁.f ⋯)
⊢ S₁.LeftHomologyData
have hf' : f' ≫ i = S₁.f
Tactic: have hf' : f' ≫ i = S₁.f := Fork.IsLimit.lift_ι _
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₁.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₁.f ⋯)
hf' : f' ≫ i = S₁.f
⊢ f' = φ.τ₁ ≫ h.f'
have rw : f' ≫ h.i = (φ.τ₁ ≫ h.f') ≫ h.i
Tactic: rw [← cancel_mono h.i, ← cancel_mono (inv φ.τ₂), assoc, assoc, assoc, hf', f'_i_assoc,
      φ.comm₁₂_assoc, IsIso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₁.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₁.f ⋯)
hf' : f' ≫ i = S₁.f
rw : f' ≫ h.i = (φ.τ₁ ≫ h.f') ≫ h.i
⊢ f' = φ.τ₁ ≫ h.f'
have rw₁ : (f' ≫ h.i) ≫ inv φ.τ₂ = ((φ.τ₁ ≫ h.f') ≫ h.i) ≫ inv φ.τ₂
Tactic: rw [← cancel_mono h.i, ← cancel_mono (inv φ.τ₂), assoc, assoc, assoc, hf', f'_i_assoc,
      φ.comm₁₂_assoc, IsIso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₁.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₁.f ⋯)
hf' : f' ≫ i = S₁.f
rw : f' ≫ h.i = (φ.τ₁ ≫ h.f') ≫ h.i
rw₁ : (f' ≫ h.i) ≫ inv φ.τ₂ = ((φ.τ₁ ≫ h.f') ≫ h.i) ≫ inv φ.τ₂
⊢ f' = φ.τ₁ ≫ h.f'
have rw₂ : f' ≫ h.i ≫ inv φ.τ₂ = ((φ.τ₁ ≫ h.f') ≫ h.i) ≫ inv φ.τ₂
Tactic: rw [← cancel_mono h.i, ← cancel_mono (inv φ.τ₂), assoc, assoc, assoc, hf', f'_i_assoc,
      φ.comm₁₂_assoc, IsIso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₁.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₁.f ⋯)
hf' : f' ≫ i = S₁.f
rw : f' ≫ h.i = (φ.τ₁ ≫ h.f') ≫ h.i
rw₁ : (f' ≫ h.i) ≫ inv φ.τ₂ = ((φ.τ₁ ≫ h.f') ≫ h.i) ≫ inv φ.τ₂
rw₂ : f' ≫ h.i ≫ inv φ.τ₂ = ((φ.τ₁ ≫ h.f') ≫ h.i) ≫ inv φ.τ₂
⊢ f' = φ.τ₁ ≫ h.f'
have rw₃ : f' ≫ h.i ≫ inv φ.τ₂ = (φ.τ₁ ≫ h.f') ≫ h.i ≫ inv φ.τ₂
Tactic: rw [← cancel_mono h.i, ← cancel_mono (inv φ.τ₂), assoc, assoc, assoc, hf', f'_i_assoc,
      φ.comm₁₂_assoc, IsIso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₁.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₁.f ⋯)
hf' : f' ≫ i = S₁.f
rw : f' ≫ h.i = (φ.τ₁ ≫ h.f') ≫ h.i
rw₁ : (f' ≫ h.i) ≫ inv φ.τ₂ = ((φ.τ₁ ≫ h.f') ≫ h.i) ≫ inv φ.τ₂
rw₂ : f' ≫ h.i ≫ inv φ.τ₂ = ((φ.τ₁ ≫ h.f') ≫ h.i) ≫ inv φ.τ₂
rw₃ : f' ≫ h.i ≫ inv φ.τ₂ = (φ.τ₁ ≫ h.f') ≫ h.i ≫ inv φ.τ₂
⊢ f' = φ.τ₁ ≫ h.f'
have rw₄ : f' ≫ h.i ≫ inv φ.τ₂ = φ.τ₁ ≫ h.f' ≫ h.i ≫ inv φ.τ₂
Tactic: rw [← cancel_mono h.i, ← cancel_mono (inv φ.τ₂), assoc, assoc, assoc, hf', f'_i_assoc,
      φ.comm₁₂_assoc, IsIso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₁.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₁.f ⋯)
hf' : f' ≫ i = S₁.f
rw : f' ≫ h.i = (φ.τ₁ ≫ h.f') ≫ h.i
rw₁ : (f' ≫ h.i) ≫ inv φ.τ₂ = ((φ.τ₁ ≫ h.f') ≫ h.i) ≫ inv φ.τ₂
rw₂ : f' ≫ h.i ≫ inv φ.τ₂ = ((φ.τ₁ ≫ h.f') ≫ h.i) ≫ inv φ.τ₂
rw₃ : f' ≫ h.i ≫ inv φ.τ₂ = (φ.τ₁ ≫ h.f') ≫ h.i ≫ inv φ.τ₂
rw₄ : f' ≫ h.i ≫ inv φ.τ₂ = φ.τ₁ ≫ h.f' ≫ h.i ≫ inv φ.τ₂
⊢ f' = φ.τ₁ ≫ h.f'
have rw₅ : S₁.f = φ.τ₁ ≫ h.f' ≫ h.i ≫ inv φ.τ₂
Tactic: rw [← cancel_mono h.i, ← cancel_mono (inv φ.τ₂), assoc, assoc, assoc, hf', f'_i_assoc,
      φ.comm₁₂_assoc, IsIso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₁.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₁.f ⋯)
hf' : f' ≫ i = S₁.f
rw : f' ≫ h.i = (φ.τ₁ ≫ h.f') ≫ h.i
rw₁ : (f' ≫ h.i) ≫ inv φ.τ₂ = ((φ.τ₁ ≫ h.f') ≫ h.i) ≫ inv φ.τ₂
rw₂ : f' ≫ h.i ≫ inv φ.τ₂ = ((φ.τ₁ ≫ h.f') ≫ h.i) ≫ inv φ.τ₂
rw₃ : f' ≫ h.i ≫ inv φ.τ₂ = (φ.τ₁ ≫ h.f') ≫ h.i ≫ inv φ.τ₂
rw₄ : f' ≫ h.i ≫ inv φ.τ₂ = φ.τ₁ ≫ h.f' ≫ h.i ≫ inv φ.τ₂
rw₅ : S₁.f = φ.τ₁ ≫ h.f' ≫ h.i ≫ inv φ.τ₂
⊢ f' = φ.τ₁ ≫ h.f'
have rw₆ : S₁.f = φ.τ₁ ≫ S₂.f ≫ inv φ.τ₂
Tactic: rw [← cancel_mono h.i, ← cancel_mono (inv φ.τ₂), assoc, assoc, assoc, hf', f'_i_assoc,
      φ.comm₁₂_assoc, IsIso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₁.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₁.f ⋯)
hf' : f' ≫ i = S₁.f
rw : f' ≫ h.i = (φ.τ₁ ≫ h.f') ≫ h.i
rw₁ : (f' ≫ h.i) ≫ inv φ.τ₂ = ((φ.τ₁ ≫ h.f') ≫ h.i) ≫ inv φ.τ₂
rw₂ : f' ≫ h.i ≫ inv φ.τ₂ = ((φ.τ₁ ≫ h.f') ≫ h.i) ≫ inv φ.τ₂
rw₃ : f' ≫ h.i ≫ inv φ.τ₂ = (φ.τ₁ ≫ h.f') ≫ h.i ≫ inv φ.τ₂
rw₄ : f' ≫ h.i ≫ inv φ.τ₂ = φ.τ₁ ≫ h.f' ≫ h.i ≫ inv φ.τ₂
rw₅ : S₁.f = φ.τ₁ ≫ h.f' ≫ h.i ≫ inv φ.τ₂
rw₆ : S₁.f = φ.τ₁ ≫ S₂.f ≫ inv φ.τ₂
⊢ f' = φ.τ₁ ≫ h.f'
have rw₇ : S₁.f = S₁.f ≫ φ.τ₂ ≫ inv φ.τ₂
Tactic: rw [← cancel_mono h.i, ← cancel_mono (inv φ.τ₂), assoc, assoc, assoc, hf', f'_i_assoc,
      φ.comm₁₂_assoc, IsIso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₁.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₁.f ⋯)
hf' : f' ≫ i = S₁.f
rw : f' ≫ h.i = (φ.τ₁ ≫ h.f') ≫ h.i
rw₁ : (f' ≫ h.i) ≫ inv φ.τ₂ = ((φ.τ₁ ≫ h.f') ≫ h.i) ≫ inv φ.τ₂
rw₂ : f' ≫ h.i ≫ inv φ.τ₂ = ((φ.τ₁ ≫ h.f') ≫ h.i) ≫ inv φ.τ₂
rw₃ : f' ≫ h.i ≫ inv φ.τ₂ = (φ.τ₁ ≫ h.f') ≫ h.i ≫ inv φ.τ₂
rw₄ : f' ≫ h.i ≫ inv φ.τ₂ = φ.τ₁ ≫ h.f' ≫ h.i ≫ inv φ.τ₂
rw₅ : S₁.f = φ.τ₁ ≫ h.f' ≫ h.i ≫ inv φ.τ₂
rw₆ : S₁.f = φ.τ₁ ≫ S₂.f ≫ inv φ.τ₂
rw₇ : S₁.f = S₁.f ≫ φ.τ₂ ≫ inv φ.τ₂
⊢ f' = φ.τ₁ ≫ h.f'
have rw₈ : S₁.f = S₁.f ≫ 𝟙 S₁.X₂
Tactic: rw [← cancel_mono h.i, ← cancel_mono (inv φ.τ₂), assoc, assoc, assoc, hf', f'_i_assoc,
      φ.comm₁₂_assoc, IsIso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₁.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₁.f ⋯)
hf' : f' ≫ i = S₁.f
rw : f' ≫ h.i = (φ.τ₁ ≫ h.f') ≫ h.i
rw₁ : (f' ≫ h.i) ≫ inv φ.τ₂ = ((φ.τ₁ ≫ h.f') ≫ h.i) ≫ inv φ.τ₂
rw₂ : f' ≫ h.i ≫ inv φ.τ₂ = ((φ.τ₁ ≫ h.f') ≫ h.i) ≫ inv φ.τ₂
rw₃ : f' ≫ h.i ≫ inv φ.τ₂ = (φ.τ₁ ≫ h.f') ≫ h.i ≫ inv φ.τ₂
rw₄ : f' ≫ h.i ≫ inv φ.τ₂ = φ.τ₁ ≫ h.f' ≫ h.i ≫ inv φ.τ₂
rw₅ : S₁.f = φ.τ₁ ≫ h.f' ≫ h.i ≫ inv φ.τ₂
rw₆ : S₁.f = φ.τ₁ ≫ S₂.f ≫ inv φ.τ₂
rw₇ : S₁.f = S₁.f ≫ φ.τ₂ ≫ inv φ.τ₂
rw₈ : S₁.f = S₁.f ≫ 𝟙 S₁.X₂
⊢ f' = φ.τ₁ ≫ h.f'
have rw₉ : S₁.f = S₁.f
Tactic: rw [← cancel_mono h.i, ← cancel_mono (inv φ.τ₂), assoc, assoc, assoc, hf', f'_i_assoc,
      φ.comm₁₂_assoc, IsIso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₁.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₁.f ⋯)
hf' : f' ≫ i = S₁.f
⊢ S₁.LeftHomologyData
have hf'' : f' = φ.τ₁ ≫ h.f'
Tactic: have hf'' : f' = φ.τ₁ ≫ h.f' := by
    rw [← cancel_mono h.i, ← cancel_mono (inv φ.τ₂), assoc, assoc, assoc, hf', f'_i_assoc,
      φ.comm₁₂_assoc, IsIso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₁.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₁.f ⋯)
hf' : f' ≫ i = S₁.f
hf'' : f' = φ.τ₁ ≫ h.f'
⊢ S₁.LeftHomologyData
have wπ : f' ≫ h.π = 0
Tactic: have wπ : f' ≫ h.π = 0 := by simp only [hf'', assoc, f'_π, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₁.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₁.f ⋯)
hf' : f' ≫ i = S₁.f
hf'' : f' = φ.τ₁ ≫ h.f'
wπ : f' ≫ h.π = 0
Z' : C
x : h.K ⟶ Z'
hx : f' ≫ x = 0
⊢ h.f' ≫ x = 0
have rw : φ.τ₁ ≫ h.f' ≫ x = φ.τ₁ ≫ 0
Tactic: rw [← cancel_epi φ.τ₁, ← reassoc_of% hf'', hx, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₁.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₁.f ⋯)
hf' : f' ≫ i = S₁.f
hf'' : f' = φ.τ₁ ≫ h.f'
wπ : f' ≫ h.π = 0
Z' : C
x : h.K ⟶ Z'
hx : f' ≫ x = 0
rw : φ.τ₁ ≫ h.f' ≫ x = φ.τ₁ ≫ 0
⊢ h.f' ≫ x = 0
have rw₁ : f' ≫ x = φ.τ₁ ≫ 0
Tactic: rw [← cancel_epi φ.τ₁, ← reassoc_of% hf'', hx, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₁.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₁.f ⋯)
hf' : f' ≫ i = S₁.f
hf'' : f' = φ.τ₁ ≫ h.f'
wπ : f' ≫ h.π = 0
Z' : C
x : h.K ⟶ Z'
hx : f' ≫ x = 0
rw : φ.τ₁ ≫ h.f' ≫ x = φ.τ₁ ≫ 0
rw₁ : f' ≫ x = φ.τ₁ ≫ 0
⊢ h.f' ≫ x = 0
have rw₂ : Eq (α := S₁.X₁ ⟶ Z') 0 (φ.τ₁ ≫ 0)
Tactic: rw [← cancel_epi φ.τ₁, ← reassoc_of% hf'', hx, comp_zero]