awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₃ ⟶ S₁
rw : ψ.τ₂ ≫ S₁.g ≫ h.h₃ = 0
⊢ S₃.g ≫ ψ.τ₃ ≫ h.h₃ = 0
have rw₁ : Eq (α := S₃.X₂ ⟶ S₂.X₃) (ψ.τ₂ ≫ 0) 0
Tactic: rw [← ψ.comm₂₃_assoc, h.g_h₃, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₃ ⟶ S₁
rw : ψ.τ₂ ≫ S₁.g ≫ h.h₃ = 0
rw₁ : Eq (α := S₃.X₂ ⟶ S₂.X₃) (ψ.τ₂ ≫ 0) 0
⊢ S₃.g ≫ ψ.τ₃ ≫ h.h₃ = 0
have rw₂ : Eq.{v_1 + 1} (α := S₃.X₂ ⟶ S₂.X₃) 0 0
Tactic: rw [← ψ.comm₂₃_assoc, h.g_h₃, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₃ ⟶ S₁
⊢ (ψ ≫ φ₁).τ₁ = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + (ψ ≫ φ₂).τ₁
have rw : ψ.τ₁ ≫ φ₁.τ₁ = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + (ψ ≫ φ₂).τ₁
Tactic: rw [comp_τ₁, comp_τ₁, h.comm₁, comp_add, comp_add, add_left_inj, ψ.comm₁₂_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₃ ⟶ S₁
rw : ψ.τ₁ ≫ φ₁.τ₁ = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + (ψ ≫ φ₂).τ₁
⊢ (ψ ≫ φ₁).τ₁ = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + (ψ ≫ φ₂).τ₁
have rw₁ : ψ.τ₁ ≫ φ₁.τ₁ = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + ψ.τ₁ ≫ φ₂.τ₁
Tactic: rw [comp_τ₁, comp_τ₁, h.comm₁, comp_add, comp_add, add_left_inj, ψ.comm₁₂_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₃ ⟶ S₁
rw : ψ.τ₁ ≫ φ₁.τ₁ = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + (ψ ≫ φ₂).τ₁
rw₁ : ψ.τ₁ ≫ φ₁.τ₁ = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + ψ.τ₁ ≫ φ₂.τ₁
⊢ (ψ ≫ φ₁).τ₁ = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + (ψ ≫ φ₂).τ₁
have rw₂ : ψ.τ₁ ≫ (S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁) = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + ψ.τ₁ ≫ φ₂.τ₁
Tactic: rw [comp_τ₁, comp_τ₁, h.comm₁, comp_add, comp_add, add_left_inj, ψ.comm₁₂_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₃ ⟶ S₁
rw : ψ.τ₁ ≫ φ₁.τ₁ = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + (ψ ≫ φ₂).τ₁
rw₁ : ψ.τ₁ ≫ φ₁.τ₁ = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + ψ.τ₁ ≫ φ₂.τ₁
rw₂ : ψ.τ₁ ≫ (S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁) = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + ψ.τ₁ ≫ φ₂.τ₁
⊢ (ψ ≫ φ₁).τ₁ = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + (ψ ≫ φ₂).τ₁
have rw₃ : ψ.τ₁ ≫ (S₁.f ≫ h.h₁ + h.h₀) + ψ.τ₁ ≫ φ₂.τ₁ = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + ψ.τ₁ ≫ φ₂.τ₁
Tactic: rw [comp_τ₁, comp_τ₁, h.comm₁, comp_add, comp_add, add_left_inj, ψ.comm₁₂_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₃ ⟶ S₁
rw : ψ.τ₁ ≫ φ₁.τ₁ = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + (ψ ≫ φ₂).τ₁
rw₁ : ψ.τ₁ ≫ φ₁.τ₁ = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + ψ.τ₁ ≫ φ₂.τ₁
rw₂ : ψ.τ₁ ≫ (S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁) = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + ψ.τ₁ ≫ φ₂.τ₁
rw₃ : ψ.τ₁ ≫ (S₁.f ≫ h.h₁ + h.h₀) + ψ.τ₁ ≫ φ₂.τ₁ = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + ψ.τ₁ ≫ φ₂.τ₁
⊢ (ψ ≫ φ₁).τ₁ = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + (ψ ≫ φ₂).τ₁
have rw₄ : ψ.τ₁ ≫ S₁.f ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + ψ.τ₁ ≫ φ₂.τ₁ = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + ψ.τ₁ ≫ φ₂.τ₁
Tactic: rw [comp_τ₁, comp_τ₁, h.comm₁, comp_add, comp_add, add_left_inj, ψ.comm₁₂_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₃ ⟶ S₁
rw : ψ.τ₁ ≫ φ₁.τ₁ = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + (ψ ≫ φ₂).τ₁
rw₁ : ψ.τ₁ ≫ φ₁.τ₁ = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + ψ.τ₁ ≫ φ₂.τ₁
rw₂ : ψ.τ₁ ≫ (S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁) = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + ψ.τ₁ ≫ φ₂.τ₁
rw₃ : ψ.τ₁ ≫ (S₁.f ≫ h.h₁ + h.h₀) + ψ.τ₁ ≫ φ₂.τ₁ = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + ψ.τ₁ ≫ φ₂.τ₁
rw₄ : ψ.τ₁ ≫ S₁.f ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + ψ.τ₁ ≫ φ₂.τ₁ = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + ψ.τ₁ ≫ φ₂.τ₁
⊢ (ψ ≫ φ₁).τ₁ = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + (ψ ≫ φ₂).τ₁
have rw₅ : ψ.τ₁ ≫ S₁.f ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀
Tactic: rw [comp_τ₁, comp_τ₁, h.comm₁, comp_add, comp_add, add_left_inj, ψ.comm₁₂_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₃ ⟶ S₁
rw : ψ.τ₁ ≫ φ₁.τ₁ = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + (ψ ≫ φ₂).τ₁
rw₁ : ψ.τ₁ ≫ φ₁.τ₁ = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + ψ.τ₁ ≫ φ₂.τ₁
rw₂ : ψ.τ₁ ≫ (S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁) = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + ψ.τ₁ ≫ φ₂.τ₁
rw₃ : ψ.τ₁ ≫ (S₁.f ≫ h.h₁ + h.h₀) + ψ.τ₁ ≫ φ₂.τ₁ = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + ψ.τ₁ ≫ φ₂.τ₁
rw₄ : ψ.τ₁ ≫ S₁.f ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + ψ.τ₁ ≫ φ₂.τ₁ = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + ψ.τ₁ ≫ φ₂.τ₁
rw₅ : ψ.τ₁ ≫ S₁.f ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀
⊢ (ψ ≫ φ₁).τ₁ = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + (ψ ≫ φ₂).τ₁
have rw₆ : S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀
Tactic: rw [comp_τ₁, comp_τ₁, h.comm₁, comp_add, comp_add, add_left_inj, ψ.comm₁₂_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₃ ⟶ S₁
⊢ (ψ ≫ φ₁).τ₂ = S₃.g ≫ ψ.τ₃ ≫ h.h₂ + (ψ.τ₂ ≫ h.h₁) ≫ S₂.f + (ψ ≫ φ₂).τ₂
have rw : ψ.τ₂ ≫ φ₁.τ₂ = S₃.g ≫ ψ.τ₃ ≫ h.h₂ + (ψ.τ₂ ≫ h.h₁) ≫ S₂.f + (ψ ≫ φ₂).τ₂
Tactic: rw [comp_τ₂, comp_τ₂, h.comm₂, comp_add, comp_add, assoc, ψ.comm₂₃_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₃ ⟶ S₁
rw : ψ.τ₂ ≫ φ₁.τ₂ = S₃.g ≫ ψ.τ₃ ≫ h.h₂ + (ψ.τ₂ ≫ h.h₁) ≫ S₂.f + (ψ ≫ φ₂).τ₂
⊢ (ψ ≫ φ₁).τ₂ = S₃.g ≫ ψ.τ₃ ≫ h.h₂ + (ψ.τ₂ ≫ h.h₁) ≫ S₂.f + (ψ ≫ φ₂).τ₂
have rw₁ : ψ.τ₂ ≫ φ₁.τ₂ = S₃.g ≫ ψ.τ₃ ≫ h.h₂ + (ψ.τ₂ ≫ h.h₁) ≫ S₂.f + ψ.τ₂ ≫ φ₂.τ₂
Tactic: rw [comp_τ₂, comp_τ₂, h.comm₂, comp_add, comp_add, assoc, ψ.comm₂₃_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₃ ⟶ S₁
rw : ψ.τ₂ ≫ φ₁.τ₂ = S₃.g ≫ ψ.τ₃ ≫ h.h₂ + (ψ.τ₂ ≫ h.h₁) ≫ S₂.f + (ψ ≫ φ₂).τ₂
rw₁ : ψ.τ₂ ≫ φ₁.τ₂ = S₃.g ≫ ψ.τ₃ ≫ h.h₂ + (ψ.τ₂ ≫ h.h₁) ≫ S₂.f + ψ.τ₂ ≫ φ₂.τ₂
⊢ (ψ ≫ φ₁).τ₂ = S₃.g ≫ ψ.τ₃ ≫ h.h₂ + (ψ.τ₂ ≫ h.h₁) ≫ S₂.f + (ψ ≫ φ₂).τ₂
have rw₂ : ψ.τ₂ ≫ (S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂) = S₃.g ≫ ψ.τ₃ ≫ h.h₂ + (ψ.τ₂ ≫ h.h₁) ≫ S₂.f + ψ.τ₂ ≫ φ₂.τ₂
Tactic: rw [comp_τ₂, comp_τ₂, h.comm₂, comp_add, comp_add, assoc, ψ.comm₂₃_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₃ ⟶ S₁
rw : ψ.τ₂ ≫ φ₁.τ₂ = S₃.g ≫ ψ.τ₃ ≫ h.h₂ + (ψ.τ₂ ≫ h.h₁) ≫ S₂.f + (ψ ≫ φ₂).τ₂
rw₁ : ψ.τ₂ ≫ φ₁.τ₂ = S₃.g ≫ ψ.τ₃ ≫ h.h₂ + (ψ.τ₂ ≫ h.h₁) ≫ S₂.f + ψ.τ₂ ≫ φ₂.τ₂
rw₂ : ψ.τ₂ ≫ (S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂) = S₃.g ≫ ψ.τ₃ ≫ h.h₂ + (ψ.τ₂ ≫ h.h₁) ≫ S₂.f + ψ.τ₂ ≫ φ₂.τ₂
⊢ (ψ ≫ φ₁).τ₂ = S₃.g ≫ ψ.τ₃ ≫ h.h₂ + (ψ.τ₂ ≫ h.h₁) ≫ S₂.f + (ψ ≫ φ₂).τ₂
have rw₃ : ψ.τ₂ ≫ (S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f) + ψ.τ₂ ≫ φ₂.τ₂ = S₃.g ≫ ψ.τ₃ ≫ h.h₂ + (ψ.τ₂ ≫ h.h₁) ≫ S₂.f + ψ.τ₂ ≫ φ₂.τ₂
Tactic: rw [comp_τ₂, comp_τ₂, h.comm₂, comp_add, comp_add, assoc, ψ.comm₂₃_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₃ ⟶ S₁
rw : ψ.τ₂ ≫ φ₁.τ₂ = S₃.g ≫ ψ.τ₃ ≫ h.h₂ + (ψ.τ₂ ≫ h.h₁) ≫ S₂.f + (ψ ≫ φ₂).τ₂
rw₁ : ψ.τ₂ ≫ φ₁.τ₂ = S₃.g ≫ ψ.τ₃ ≫ h.h₂ + (ψ.τ₂ ≫ h.h₁) ≫ S₂.f + ψ.τ₂ ≫ φ₂.τ₂
rw₂ : ψ.τ₂ ≫ (S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂) = S₃.g ≫ ψ.τ₃ ≫ h.h₂ + (ψ.τ₂ ≫ h.h₁) ≫ S₂.f + ψ.τ₂ ≫ φ₂.τ₂
rw₃ : ψ.τ₂ ≫ (S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f) + ψ.τ₂ ≫ φ₂.τ₂ = S₃.g ≫ ψ.τ₃ ≫ h.h₂ + (ψ.τ₂ ≫ h.h₁) ≫ S₂.f + ψ.τ₂ ≫ φ₂.τ₂
⊢ (ψ ≫ φ₁).τ₂ = S₃.g ≫ ψ.τ₃ ≫ h.h₂ + (ψ.τ₂ ≫ h.h₁) ≫ S₂.f + (ψ ≫ φ₂).τ₂
have rw₄ : ψ.τ₂ ≫ S₁.g ≫ h.h₂ + ψ.τ₂ ≫ h.h₁ ≫ S₂.f + ψ.τ₂ ≫ φ₂.τ₂ = S₃.g ≫ ψ.τ₃ ≫ h.h₂ + (ψ.τ₂ ≫ h.h₁) ≫ S₂.f + ψ.τ₂ ≫ φ₂.τ₂
Tactic: rw [comp_τ₂, comp_τ₂, h.comm₂, comp_add, comp_add, assoc, ψ.comm₂₃_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₃ ⟶ S₁
rw : ψ.τ₂ ≫ φ₁.τ₂ = S₃.g ≫ ψ.τ₃ ≫ h.h₂ + (ψ.τ₂ ≫ h.h₁) ≫ S₂.f + (ψ ≫ φ₂).τ₂
rw₁ : ψ.τ₂ ≫ φ₁.τ₂ = S₃.g ≫ ψ.τ₃ ≫ h.h₂ + (ψ.τ₂ ≫ h.h₁) ≫ S₂.f + ψ.τ₂ ≫ φ₂.τ₂
rw₂ : ψ.τ₂ ≫ (S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂) = S₃.g ≫ ψ.τ₃ ≫ h.h₂ + (ψ.τ₂ ≫ h.h₁) ≫ S₂.f + ψ.τ₂ ≫ φ₂.τ₂
rw₃ : ψ.τ₂ ≫ (S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f) + ψ.τ₂ ≫ φ₂.τ₂ = S₃.g ≫ ψ.τ₃ ≫ h.h₂ + (ψ.τ₂ ≫ h.h₁) ≫ S₂.f + ψ.τ₂ ≫ φ₂.τ₂
rw₄ : ψ.τ₂ ≫ S₁.g ≫ h.h₂ + ψ.τ₂ ≫ h.h₁ ≫ S₂.f + ψ.τ₂ ≫ φ₂.τ₂ = S₃.g ≫ ψ.τ₃ ≫ h.h₂ + (ψ.τ₂ ≫ h.h₁) ≫ S₂.f + ψ.τ₂ ≫ φ₂.τ₂
⊢ (ψ ≫ φ₁).τ₂ = S₃.g ≫ ψ.τ₃ ≫ h.h₂ + (ψ.τ₂ ≫ h.h₁) ≫ S₂.f + (ψ ≫ φ₂).τ₂
have rw₅ : ψ.τ₂ ≫ S₁.g ≫ h.h₂ + ψ.τ₂ ≫ h.h₁ ≫ S₂.f + ψ.τ₂ ≫ φ₂.τ₂ = S₃.g ≫ ψ.τ₃ ≫ h.h₂ + ψ.τ₂ ≫ h.h₁ ≫ S₂.f + ψ.τ₂ ≫ φ₂.τ₂
Tactic: rw [comp_τ₂, comp_τ₂, h.comm₂, comp_add, comp_add, assoc, ψ.comm₂₃_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₃ ⟶ S₁
rw : ψ.τ₂ ≫ φ₁.τ₂ = S₃.g ≫ ψ.τ₃ ≫ h.h₂ + (ψ.τ₂ ≫ h.h₁) ≫ S₂.f + (ψ ≫ φ₂).τ₂
rw₁ : ψ.τ₂ ≫ φ₁.τ₂ = S₃.g ≫ ψ.τ₃ ≫ h.h₂ + (ψ.τ₂ ≫ h.h₁) ≫ S₂.f + ψ.τ₂ ≫ φ₂.τ₂
rw₂ : ψ.τ₂ ≫ (S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂) = S₃.g ≫ ψ.τ₃ ≫ h.h₂ + (ψ.τ₂ ≫ h.h₁) ≫ S₂.f + ψ.τ₂ ≫ φ₂.τ₂
rw₃ : ψ.τ₂ ≫ (S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f) + ψ.τ₂ ≫ φ₂.τ₂ = S₃.g ≫ ψ.τ₃ ≫ h.h₂ + (ψ.τ₂ ≫ h.h₁) ≫ S₂.f + ψ.τ₂ ≫ φ₂.τ₂
rw₄ : ψ.τ₂ ≫ S₁.g ≫ h.h₂ + ψ.τ₂ ≫ h.h₁ ≫ S₂.f + ψ.τ₂ ≫ φ₂.τ₂ = S₃.g ≫ ψ.τ₃ ≫ h.h₂ + (ψ.τ₂ ≫ h.h₁) ≫ S₂.f + ψ.τ₂ ≫ φ₂.τ₂
rw₅ : ψ.τ₂ ≫ S₁.g ≫ h.h₂ + ψ.τ₂ ≫ h.h₁ ≫ S₂.f + ψ.τ₂ ≫ φ₂.τ₂ = S₃.g ≫ ψ.τ₃ ≫ h.h₂ + ψ.τ₂ ≫ h.h₁ ≫ S₂.f + ψ.τ₂ ≫ φ₂.τ₂
⊢ (ψ ≫ φ₁).τ₂ = S₃.g ≫ ψ.τ₃ ≫ h.h₂ + (ψ.τ₂ ≫ h.h₁) ≫ S₂.f + (ψ ≫ φ₂).τ₂
have rw₆ : S₃.g ≫ ψ.τ₃ ≫ h.h₂ + ψ.τ₂ ≫ h.h₁ ≫ S₂.f + ψ.τ₂ ≫ φ₂.τ₂ = S₃.g ≫ ψ.τ₃ ≫ h.h₂ + ψ.τ₂ ≫ h.h₁ ≫ S₂.f + ψ.τ₂ ≫ φ₂.τ₂
Tactic: rw [comp_τ₂, comp_τ₂, h.comm₂, comp_add, comp_add, assoc, ψ.comm₂₃_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₃ ⟶ S₁
⊢ (ψ ≫ φ₁).τ₃ = ψ.τ₃ ≫ h.h₃ + (ψ.τ₃ ≫ h.h₂) ≫ S₂.g + (ψ ≫ φ₂).τ₃
have rw : ψ.τ₃ ≫ φ₁.τ₃ = ψ.τ₃ ≫ h.h₃ + (ψ.τ₃ ≫ h.h₂) ≫ S₂.g + (ψ ≫ φ₂).τ₃
Tactic: rw [comp_τ₃, comp_τ₃, h.comm₃, comp_add, comp_add, assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₃ ⟶ S₁
rw : ψ.τ₃ ≫ φ₁.τ₃ = ψ.τ₃ ≫ h.h₃ + (ψ.τ₃ ≫ h.h₂) ≫ S₂.g + (ψ ≫ φ₂).τ₃
⊢ (ψ ≫ φ₁).τ₃ = ψ.τ₃ ≫ h.h₃ + (ψ.τ₃ ≫ h.h₂) ≫ S₂.g + (ψ ≫ φ₂).τ₃
have rw₁ : ψ.τ₃ ≫ φ₁.τ₃ = ψ.τ₃ ≫ h.h₃ + (ψ.τ₃ ≫ h.h₂) ≫ S₂.g + ψ.τ₃ ≫ φ₂.τ₃
Tactic: rw [comp_τ₃, comp_τ₃, h.comm₃, comp_add, comp_add, assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₃ ⟶ S₁
rw : ψ.τ₃ ≫ φ₁.τ₃ = ψ.τ₃ ≫ h.h₃ + (ψ.τ₃ ≫ h.h₂) ≫ S₂.g + (ψ ≫ φ₂).τ₃
rw₁ : ψ.τ₃ ≫ φ₁.τ₃ = ψ.τ₃ ≫ h.h₃ + (ψ.τ₃ ≫ h.h₂) ≫ S₂.g + ψ.τ₃ ≫ φ₂.τ₃
⊢ (ψ ≫ φ₁).τ₃ = ψ.τ₃ ≫ h.h₃ + (ψ.τ₃ ≫ h.h₂) ≫ S₂.g + (ψ ≫ φ₂).τ₃
have rw₂ : ψ.τ₃ ≫ (h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃) = ψ.τ₃ ≫ h.h₃ + (ψ.τ₃ ≫ h.h₂) ≫ S₂.g + ψ.τ₃ ≫ φ₂.τ₃
Tactic: rw [comp_τ₃, comp_τ₃, h.comm₃, comp_add, comp_add, assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₃ ⟶ S₁
rw : ψ.τ₃ ≫ φ₁.τ₃ = ψ.τ₃ ≫ h.h₃ + (ψ.τ₃ ≫ h.h₂) ≫ S₂.g + (ψ ≫ φ₂).τ₃
rw₁ : ψ.τ₃ ≫ φ₁.τ₃ = ψ.τ₃ ≫ h.h₃ + (ψ.τ₃ ≫ h.h₂) ≫ S₂.g + ψ.τ₃ ≫ φ₂.τ₃
rw₂ : ψ.τ₃ ≫ (h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃) = ψ.τ₃ ≫ h.h₃ + (ψ.τ₃ ≫ h.h₂) ≫ S₂.g + ψ.τ₃ ≫ φ₂.τ₃
⊢ (ψ ≫ φ₁).τ₃ = ψ.τ₃ ≫ h.h₃ + (ψ.τ₃ ≫ h.h₂) ≫ S₂.g + (ψ ≫ φ₂).τ₃
have rw₃ : ψ.τ₃ ≫ (h.h₃ + h.h₂ ≫ S₂.g) + ψ.τ₃ ≫ φ₂.τ₃ = ψ.τ₃ ≫ h.h₃ + (ψ.τ₃ ≫ h.h₂) ≫ S₂.g + ψ.τ₃ ≫ φ₂.τ₃
Tactic: rw [comp_τ₃, comp_τ₃, h.comm₃, comp_add, comp_add, assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₃ ⟶ S₁
rw : ψ.τ₃ ≫ φ₁.τ₃ = ψ.τ₃ ≫ h.h₃ + (ψ.τ₃ ≫ h.h₂) ≫ S₂.g + (ψ ≫ φ₂).τ₃
rw₁ : ψ.τ₃ ≫ φ₁.τ₃ = ψ.τ₃ ≫ h.h₃ + (ψ.τ₃ ≫ h.h₂) ≫ S₂.g + ψ.τ₃ ≫ φ₂.τ₃
rw₂ : ψ.τ₃ ≫ (h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃) = ψ.τ₃ ≫ h.h₃ + (ψ.τ₃ ≫ h.h₂) ≫ S₂.g + ψ.τ₃ ≫ φ₂.τ₃
rw₃ : ψ.τ₃ ≫ (h.h₃ + h.h₂ ≫ S₂.g) + ψ.τ₃ ≫ φ₂.τ₃ = ψ.τ₃ ≫ h.h₃ + (ψ.τ₃ ≫ h.h₂) ≫ S₂.g + ψ.τ₃ ≫ φ₂.τ₃
⊢ (ψ ≫ φ₁).τ₃ = ψ.τ₃ ≫ h.h₃ + (ψ.τ₃ ≫ h.h₂) ≫ S₂.g + (ψ ≫ φ₂).τ₃
have rw₄ : ψ.τ₃ ≫ h.h₃ + ψ.τ₃ ≫ h.h₂ ≫ S₂.g + ψ.τ₃ ≫ φ₂.τ₃ = ψ.τ₃ ≫ h.h₃ + (ψ.τ₃ ≫ h.h₂) ≫ S₂.g + ψ.τ₃ ≫ φ₂.τ₃
Tactic: rw [comp_τ₃, comp_τ₃, h.comm₃, comp_add, comp_add, assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₃ ⟶ S₁
rw : ψ.τ₃ ≫ φ₁.τ₃ = ψ.τ₃ ≫ h.h₃ + (ψ.τ₃ ≫ h.h₂) ≫ S₂.g + (ψ ≫ φ₂).τ₃
rw₁ : ψ.τ₃ ≫ φ₁.τ₃ = ψ.τ₃ ≫ h.h₃ + (ψ.τ₃ ≫ h.h₂) ≫ S₂.g + ψ.τ₃ ≫ φ₂.τ₃
rw₂ : ψ.τ₃ ≫ (h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃) = ψ.τ₃ ≫ h.h₃ + (ψ.τ₃ ≫ h.h₂) ≫ S₂.g + ψ.τ₃ ≫ φ₂.τ₃
rw₃ : ψ.τ₃ ≫ (h.h₃ + h.h₂ ≫ S₂.g) + ψ.τ₃ ≫ φ₂.τ₃ = ψ.τ₃ ≫ h.h₃ + (ψ.τ₃ ≫ h.h₂) ≫ S₂.g + ψ.τ₃ ≫ φ₂.τ₃
rw₄ : ψ.τ₃ ≫ h.h₃ + ψ.τ₃ ≫ h.h₂ ≫ S₂.g + ψ.τ₃ ≫ φ₂.τ₃ = ψ.τ₃ ≫ h.h₃ + (ψ.τ₃ ≫ h.h₂) ≫ S₂.g + ψ.τ₃ ≫ φ₂.τ₃
⊢ (ψ ≫ φ₁).τ₃ = ψ.τ₃ ≫ h.h₃ + (ψ.τ₃ ≫ h.h₂) ≫ S₂.g + (ψ ≫ φ₂).τ₃
have rw₅ : ψ.τ₃ ≫ h.h₃ + ψ.τ₃ ≫ h.h₂ ≫ S₂.g + ψ.τ₃ ≫ φ₂.τ₃ = ψ.τ₃ ≫ h.h₃ + ψ.τ₃ ≫ h.h₂ ≫ S₂.g + ψ.τ₃ ≫ φ₂.τ₃
Tactic: rw [comp_τ₃, comp_τ₃, h.comm₃, comp_add, comp_add, assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₂ ⟶ S₃
⊢ (φ₁ ≫ ψ).τ₁ = S₁.f ≫ h.h₁ ≫ ψ.τ₁ + h.h₀ ≫ ψ.τ₁ + (φ₂ ≫ ψ).τ₁
have rw : φ₁.τ₁ ≫ ψ.τ₁ = S₁.f ≫ h.h₁ ≫ ψ.τ₁ + h.h₀ ≫ ψ.τ₁ + (φ₂ ≫ ψ).τ₁
Tactic: rw [comp_τ₁, comp_τ₁, h.comm₁, add_comp, add_comp, assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₂ ⟶ S₃
rw : φ₁.τ₁ ≫ ψ.τ₁ = S₁.f ≫ h.h₁ ≫ ψ.τ₁ + h.h₀ ≫ ψ.τ₁ + (φ₂ ≫ ψ).τ₁
⊢ (φ₁ ≫ ψ).τ₁ = S₁.f ≫ h.h₁ ≫ ψ.τ₁ + h.h₀ ≫ ψ.τ₁ + (φ₂ ≫ ψ).τ₁
have rw₁ : φ₁.τ₁ ≫ ψ.τ₁ = S₁.f ≫ h.h₁ ≫ ψ.τ₁ + h.h₀ ≫ ψ.τ₁ + φ₂.τ₁ ≫ ψ.τ₁
Tactic: rw [comp_τ₁, comp_τ₁, h.comm₁, add_comp, add_comp, assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₂ ⟶ S₃
rw : φ₁.τ₁ ≫ ψ.τ₁ = S₁.f ≫ h.h₁ ≫ ψ.τ₁ + h.h₀ ≫ ψ.τ₁ + (φ₂ ≫ ψ).τ₁
rw₁ : φ₁.τ₁ ≫ ψ.τ₁ = S₁.f ≫ h.h₁ ≫ ψ.τ₁ + h.h₀ ≫ ψ.τ₁ + φ₂.τ₁ ≫ ψ.τ₁
⊢ (φ₁ ≫ ψ).τ₁ = S₁.f ≫ h.h₁ ≫ ψ.τ₁ + h.h₀ ≫ ψ.τ₁ + (φ₂ ≫ ψ).τ₁
have rw₂ : (S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁) ≫ ψ.τ₁ = S₁.f ≫ h.h₁ ≫ ψ.τ₁ + h.h₀ ≫ ψ.τ₁ + φ₂.τ₁ ≫ ψ.τ₁
Tactic: rw [comp_τ₁, comp_τ₁, h.comm₁, add_comp, add_comp, assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₂ ⟶ S₃
rw : φ₁.τ₁ ≫ ψ.τ₁ = S₁.f ≫ h.h₁ ≫ ψ.τ₁ + h.h₀ ≫ ψ.τ₁ + (φ₂ ≫ ψ).τ₁
rw₁ : φ₁.τ₁ ≫ ψ.τ₁ = S₁.f ≫ h.h₁ ≫ ψ.τ₁ + h.h₀ ≫ ψ.τ₁ + φ₂.τ₁ ≫ ψ.τ₁
rw₂ : (S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁) ≫ ψ.τ₁ = S₁.f ≫ h.h₁ ≫ ψ.τ₁ + h.h₀ ≫ ψ.τ₁ + φ₂.τ₁ ≫ ψ.τ₁
⊢ (φ₁ ≫ ψ).τ₁ = S₁.f ≫ h.h₁ ≫ ψ.τ₁ + h.h₀ ≫ ψ.τ₁ + (φ₂ ≫ ψ).τ₁
have rw₃ : (S₁.f ≫ h.h₁ + h.h₀) ≫ ψ.τ₁ + φ₂.τ₁ ≫ ψ.τ₁ = S₁.f ≫ h.h₁ ≫ ψ.τ₁ + h.h₀ ≫ ψ.τ₁ + φ₂.τ₁ ≫ ψ.τ₁
Tactic: rw [comp_τ₁, comp_τ₁, h.comm₁, add_comp, add_comp, assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₂ ⟶ S₃
rw : φ₁.τ₁ ≫ ψ.τ₁ = S₁.f ≫ h.h₁ ≫ ψ.τ₁ + h.h₀ ≫ ψ.τ₁ + (φ₂ ≫ ψ).τ₁
rw₁ : φ₁.τ₁ ≫ ψ.τ₁ = S₁.f ≫ h.h₁ ≫ ψ.τ₁ + h.h₀ ≫ ψ.τ₁ + φ₂.τ₁ ≫ ψ.τ₁
rw₂ : (S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁) ≫ ψ.τ₁ = S₁.f ≫ h.h₁ ≫ ψ.τ₁ + h.h₀ ≫ ψ.τ₁ + φ₂.τ₁ ≫ ψ.τ₁
rw₃ : (S₁.f ≫ h.h₁ + h.h₀) ≫ ψ.τ₁ + φ₂.τ₁ ≫ ψ.τ₁ = S₁.f ≫ h.h₁ ≫ ψ.τ₁ + h.h₀ ≫ ψ.τ₁ + φ₂.τ₁ ≫ ψ.τ₁
⊢ (φ₁ ≫ ψ).τ₁ = S₁.f ≫ h.h₁ ≫ ψ.τ₁ + h.h₀ ≫ ψ.τ₁ + (φ₂ ≫ ψ).τ₁
have rw₄ : (S₁.f ≫ h.h₁) ≫ ψ.τ₁ + h.h₀ ≫ ψ.τ₁ + φ₂.τ₁ ≫ ψ.τ₁ = S₁.f ≫ h.h₁ ≫ ψ.τ₁ + h.h₀ ≫ ψ.τ₁ + φ₂.τ₁ ≫ ψ.τ₁
Tactic: rw [comp_τ₁, comp_τ₁, h.comm₁, add_comp, add_comp, assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₂ ⟶ S₃
rw : φ₁.τ₁ ≫ ψ.τ₁ = S₁.f ≫ h.h₁ ≫ ψ.τ₁ + h.h₀ ≫ ψ.τ₁ + (φ₂ ≫ ψ).τ₁
rw₁ : φ₁.τ₁ ≫ ψ.τ₁ = S₁.f ≫ h.h₁ ≫ ψ.τ₁ + h.h₀ ≫ ψ.τ₁ + φ₂.τ₁ ≫ ψ.τ₁
rw₂ : (S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁) ≫ ψ.τ₁ = S₁.f ≫ h.h₁ ≫ ψ.τ₁ + h.h₀ ≫ ψ.τ₁ + φ₂.τ₁ ≫ ψ.τ₁
rw₃ : (S₁.f ≫ h.h₁ + h.h₀) ≫ ψ.τ₁ + φ₂.τ₁ ≫ ψ.τ₁ = S₁.f ≫ h.h₁ ≫ ψ.τ₁ + h.h₀ ≫ ψ.τ₁ + φ₂.τ₁ ≫ ψ.τ₁
rw₄ : (S₁.f ≫ h.h₁) ≫ ψ.τ₁ + h.h₀ ≫ ψ.τ₁ + φ₂.τ₁ ≫ ψ.τ₁ = S₁.f ≫ h.h₁ ≫ ψ.τ₁ + h.h₀ ≫ ψ.τ₁ + φ₂.τ₁ ≫ ψ.τ₁
⊢ (φ₁ ≫ ψ).τ₁ = S₁.f ≫ h.h₁ ≫ ψ.τ₁ + h.h₀ ≫ ψ.τ₁ + (φ₂ ≫ ψ).τ₁
have rw₅ : S₁.f ≫ h.h₁ ≫ ψ.τ₁ + h.h₀ ≫ ψ.τ₁ + φ₂.τ₁ ≫ ψ.τ₁ = S₁.f ≫ h.h₁ ≫ ψ.τ₁ + h.h₀ ≫ ψ.τ₁ + φ₂.τ₁ ≫ ψ.τ₁
Tactic: rw [comp_τ₁, comp_τ₁, h.comm₁, add_comp, add_comp, assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₂ ⟶ S₃
⊢ (φ₁ ≫ ψ).τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + (φ₂ ≫ ψ).τ₂
have rw : φ₁.τ₂ ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + (φ₂ ≫ ψ).τ₂
Tactic: rw [comp_τ₂, comp_τ₂, h.comm₂, add_comp, add_comp, assoc, assoc, assoc, ψ.comm₁₂]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₂ ⟶ S₃
rw : φ₁.τ₂ ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + (φ₂ ≫ ψ).τ₂
⊢ (φ₁ ≫ ψ).τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + (φ₂ ≫ ψ).τ₂
have rw₁ : φ₁.τ₂ ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + φ₂.τ₂ ≫ ψ.τ₂
Tactic: rw [comp_τ₂, comp_τ₂, h.comm₂, add_comp, add_comp, assoc, assoc, assoc, ψ.comm₁₂]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₂ ⟶ S₃
rw : φ₁.τ₂ ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + (φ₂ ≫ ψ).τ₂
rw₁ : φ₁.τ₂ ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + φ₂.τ₂ ≫ ψ.τ₂
⊢ (φ₁ ≫ ψ).τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + (φ₂ ≫ ψ).τ₂
have rw₂ : (S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂) ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + φ₂.τ₂ ≫ ψ.τ₂
Tactic: rw [comp_τ₂, comp_τ₂, h.comm₂, add_comp, add_comp, assoc, assoc, assoc, ψ.comm₁₂]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₂ ⟶ S₃
rw : φ₁.τ₂ ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + (φ₂ ≫ ψ).τ₂
rw₁ : φ₁.τ₂ ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + φ₂.τ₂ ≫ ψ.τ₂
rw₂ : (S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂) ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + φ₂.τ₂ ≫ ψ.τ₂
⊢ (φ₁ ≫ ψ).τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + (φ₂ ≫ ψ).τ₂
have rw₃ : (S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f) ≫ ψ.τ₂ + φ₂.τ₂ ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + φ₂.τ₂ ≫ ψ.τ₂
Tactic: rw [comp_τ₂, comp_τ₂, h.comm₂, add_comp, add_comp, assoc, assoc, assoc, ψ.comm₁₂]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₂ ⟶ S₃
rw : φ₁.τ₂ ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + (φ₂ ≫ ψ).τ₂
rw₁ : φ₁.τ₂ ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + φ₂.τ₂ ≫ ψ.τ₂
rw₂ : (S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂) ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + φ₂.τ₂ ≫ ψ.τ₂
rw₃ : (S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f) ≫ ψ.τ₂ + φ₂.τ₂ ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + φ₂.τ₂ ≫ ψ.τ₂
⊢ (φ₁ ≫ ψ).τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + (φ₂ ≫ ψ).τ₂
have rw₄ : (S₁.g ≫ h.h₂) ≫ ψ.τ₂ + (h.h₁ ≫ S₂.f) ≫ ψ.τ₂ + φ₂.τ₂ ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + φ₂.τ₂ ≫ ψ.τ₂
Tactic: rw [comp_τ₂, comp_τ₂, h.comm₂, add_comp, add_comp, assoc, assoc, assoc, ψ.comm₁₂]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₂ ⟶ S₃
rw : φ₁.τ₂ ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + (φ₂ ≫ ψ).τ₂
rw₁ : φ₁.τ₂ ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + φ₂.τ₂ ≫ ψ.τ₂
rw₂ : (S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂) ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + φ₂.τ₂ ≫ ψ.τ₂
rw₃ : (S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f) ≫ ψ.τ₂ + φ₂.τ₂ ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + φ₂.τ₂ ≫ ψ.τ₂
rw₄ :
  (S₁.g ≫ h.h₂) ≫ ψ.τ₂ + (h.h₁ ≫ S₂.f) ≫ ψ.τ₂ + φ₂.τ₂ ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + φ₂.τ₂ ≫ ψ.τ₂
⊢ (φ₁ ≫ ψ).τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + (φ₂ ≫ ψ).τ₂
have rw₅ : S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ S₂.f) ≫ ψ.τ₂ + φ₂.τ₂ ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + φ₂.τ₂ ≫ ψ.τ₂
Tactic: rw [comp_τ₂, comp_τ₂, h.comm₂, add_comp, add_comp, assoc, assoc, assoc, ψ.comm₁₂]