awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
i : ℤ
A : C
f : A ⟶ (mappingCone φ).X i
j : ℤ
hij : i + 1 = j
h₁ :
  f ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij =
    HAdd.hAdd (α := A ⟶ (mappingCone φ).X i)
        ((f ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij) ≫ Cochain.v (inl φ) j i ⋯)
        ((f ≫ Cochain.v (snd φ) i i ⋯) ≫ Hom.f (inr φ) i) ≫
      Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij
⊢ f =
    HAdd.hAdd (α := A ⟶ (mappingCone φ).X i)
      ((f ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij) ≫ Cochain.v (inl φ) j i ⋯)
      ((f ≫ Cochain.v (snd φ) i i ⋯) ≫ Hom.f (inr φ) i)
have h₂ : f ≫ Cochain.v (snd φ) i i sorry =
  HAdd.hAdd (α := A ⟶ (mappingCone φ).X i)
      ((f ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij) ≫ Cochain.v (inl φ) j i sorry)
      ((f ≫ Cochain.v (snd φ) i i sorry) ≫ Hom.f (inr φ) i) ≫
    Cochain.v (snd φ) i i sorry
Tactic: apply ext_to φ i j hij
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
j : ℤ
A : C
f : (mappingCone φ).X j ⟶ A
i : ℤ
hij : j + 1 = i
⊢ f =
    HAdd.hAdd (α := (mappingCone φ).X j ⟶ A)
      (Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) j i hij ≫ Cochain.v (inl φ) i j ⋯ ≫ f)
      (Cochain.v (snd φ) j j ⋯ ≫ Hom.f (inr φ) j ≫ f)
have h₁ : Cochain.v (inl φ) i j sorry ≫ f =
  Cochain.v (inl φ) i j sorry ≫
    HAdd.hAdd (α := (mappingCone φ).X j ⟶ A)
      (Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) j i hij ≫ Cochain.v (inl φ) i j sorry ≫ f)
      (Cochain.v (snd φ) j j sorry ≫ Hom.f (inr φ) j ≫ f)
Tactic: apply ext_from φ i j hij
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
j : ℤ
A : C
f : (mappingCone φ).X j ⟶ A
i : ℤ
hij : j + 1 = i
h₁ :
  Cochain.v (inl φ) i j ⋯ ≫ f =
    Cochain.v (inl φ) i j ⋯ ≫
      HAdd.hAdd (α := (mappingCone φ).X j ⟶ A)
        (Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) j i hij ≫ Cochain.v (inl φ) i j ⋯ ≫ f)
        (Cochain.v (snd φ) j j ⋯ ≫ Hom.f (inr φ) j ≫ f)
⊢ f =
    HAdd.hAdd (α := (mappingCone φ).X j ⟶ A)
      (Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) j i hij ≫ Cochain.v (inl φ) i j ⋯ ≫ f)
      (Cochain.v (snd φ) j j ⋯ ≫ Hom.f (inr φ) j ≫ f)
have h₂ : Hom.f (inr φ) j ≫ f =
  Hom.f (inr φ) j ≫
    HAdd.hAdd (α := (mappingCone φ).X j ⟶ A)
      (Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) j i hij ≫ Cochain.v (inl φ) i j sorry ≫ f)
      (Cochain.v (snd φ) j j sorry ≫ Hom.f (inr φ) j ≫ f)
Tactic: apply ext_from φ i j hij
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
K : CochainComplex.{v, u_1, 0} C ℤ
γ₁ γ₂ : Cochain K (mappingCone φ) i
⊢ γ₁ = γ₂ ↔
    γ₁.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) hij = γ₂.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) hij ∧
      γ₁.comp (snd φ) ⋯ = γ₂.comp (snd φ) ⋯
have mp : γ₁ = γ₂ →
  γ₁.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) hij = γ₂.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) hij ∧
    γ₁.comp (snd φ) sorry = γ₂.comp (snd φ) sorry
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
K : CochainComplex.{v, u_1, 0} C ℤ
γ₁ γ₂ : Cochain K (mappingCone φ) i
mp :
  γ₁ = γ₂ →
    γ₁.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) hij = γ₂.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) hij ∧
      γ₁.comp (snd φ) ⋯ = γ₂.comp (snd φ) ⋯
⊢ γ₁ = γ₂ ↔
    γ₁.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) hij = γ₂.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) hij ∧
      γ₁.comp (snd φ) ⋯ = γ₂.comp (snd φ) ⋯
have mpr : γ₁.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) hij = γ₂.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) hij ∧
    γ₁.comp (snd φ) sorry = γ₂.comp (snd φ) sorry →
  γ₁ = γ₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
K : CochainComplex.{v, u_1, 0} C ℤ
γ₁ : Cochain K (mappingCone φ) i
⊢ γ₁.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) hij = γ₁.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) hij ∧
    γ₁.comp (snd φ) ⋯ = γ₁.comp (snd φ) ⋯
have mp : γ₁.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) hij = γ₁.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) hij
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
K : CochainComplex.{v, u_1, 0} C ℤ
γ₁ : Cochain K (mappingCone φ) i
mp : γ₁.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) hij = γ₁.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) hij
⊢ γ₁.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) hij = γ₁.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) hij ∧
    γ₁.comp (snd φ) ⋯ = γ₁.comp (snd φ) ⋯
have mp₁ : γ₁.comp (snd φ) sorry = γ₁.comp (snd φ) sorry
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
K : CochainComplex.{v, u_1, 0} C ℤ
γ₁ γ₂ : Cochain K (mappingCone φ) i
h₁ : γ₁.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) hij = γ₂.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) hij
h₂ : γ₁.comp (snd φ) ⋯ = γ₂.comp (snd φ) ⋯
⊢ γ₁ = γ₂
have mpr : ∀ (p q : ℤ) (hpq : p + i = q), γ₁.v p q hpq = γ₂.v p q hpq
Tactic: ext p q hpq
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
K : CochainComplex.{v, u_1, 0} C ℤ
γ₁ γ₂ : Cochain K (mappingCone φ) i
h₁ : γ₁.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) hij = γ₂.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) hij
h₂ : γ₁.comp (snd φ) ⋯ = γ₂.comp (snd φ) ⋯
p q : ℤ
hpq : p + i = q
⊢ γ₁.v p q hpq = γ₂.v p q hpq
have mpr : γ₁.v p q hpq ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) q (q + 1) sorry =
    γ₂.v p q hpq ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) q (q + 1) sorry ∧
  γ₁.v p q hpq ≫ Cochain.v (snd φ) q q sorry = γ₂.v p q hpq ≫ Cochain.v (snd φ) q q sorry
Tactic: rw [ext_to_iff φ q (q + 1) rfl]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (hypothesis)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
K : CochainComplex.{v, u_1, 0} C ℤ
γ₁ γ₂ : Cochain K (mappingCone φ) i
h₁ : γ₁.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) hij = γ₂.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) hij
h₂ : γ₁.comp (snd φ) ⋯ = γ₂.comp (snd φ) ⋯
p q : ℤ
hpq : p + i = q
⊢ γ₁.v p q hpq ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) q (q + 1) ⋯ =
      γ₂.v p q hpq ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) q (q + 1) ⋯ ∧
    γ₁.v p q hpq ≫ Cochain.v (snd φ) q q ⋯ = γ₂.v p q hpq ≫ Cochain.v (snd φ) q q ⋯
have h₃ : (γ₁.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) hij).v p (q + 1) sorry =
  (γ₂.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) hij).v p (q + 1) sorry
Tactic: replace h₁ := Cochain.congr_v h₁ p (q + 1) (by lia)
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (hypothesis)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
K : CochainComplex.{v, u_1, 0} C ℤ
γ₁ γ₂ : Cochain K (mappingCone φ) i
h₂ : γ₁.comp (snd φ) ⋯ = γ₂.comp (snd φ) ⋯
p q : ℤ
hpq : p + i = q
h₁ :
  (γ₁.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) hij).v p (q + 1) ⋯ =
    (γ₂.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) hij).v p (q + 1) ⋯
⊢ γ₁.v p q hpq ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) q (q + 1) ⋯ =
      γ₂.v p q hpq ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) q (q + 1) ⋯ ∧
    γ₁.v p q hpq ≫ Cochain.v (snd φ) q q ⋯ = γ₂.v p q hpq ≫ Cochain.v (snd φ) q q ⋯
have h₃ : (γ₁.comp (snd φ) sorry).v p q hpq = (γ₂.comp (snd φ) sorry).v p q hpq
Tactic: replace h₂ := Cochain.congr_v h₂ p q hpq
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (hypothesis)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
K : CochainComplex.{v, u_1, 0} C ℤ
γ₁ γ₂ : Cochain K (mappingCone φ) i
p q : ℤ
hpq : p + i = q
h₁ :
  (γ₁.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) hij).v p (q + 1) ⋯ =
    (γ₂.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) hij).v p (q + 1) ⋯
h₂ : (γ₁.comp (snd φ) ⋯).v p q hpq = (γ₂.comp (snd φ) ⋯).v p q hpq
⊢ γ₁.v p q hpq ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) q (q + 1) ⋯ =
      γ₂.v p q hpq ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) q (q + 1) ⋯ ∧
    γ₁.v p q hpq ≫ Cochain.v (snd φ) q q ⋯ = γ₂.v p q hpq ≫ Cochain.v (snd φ) q q ⋯
have h₃ : γ₁.v p q hpq ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) q (q + 1) sorry =
  γ₂.v p q hpq ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) q (q + 1) sorry
Tactic: simp only [Cochain.comp_v _ _ _ p q (q + 1) hpq rfl] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (hypothesis)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
K : CochainComplex.{v, u_1, 0} C ℤ
γ₁ γ₂ : Cochain K (mappingCone φ) i
p q : ℤ
hpq : p + i = q
h₂ : (γ₁.comp (snd φ) ⋯).v p q hpq = (γ₂.comp (snd φ) ⋯).v p q hpq
h₁ :
  γ₁.v p q hpq ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) q (q + 1) ⋯ =
    γ₂.v p q hpq ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) q (q + 1) ⋯
⊢ γ₁.v p q hpq ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) q (q + 1) ⋯ =
      γ₂.v p q hpq ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) q (q + 1) ⋯ ∧
    γ₁.v p q hpq ≫ Cochain.v (snd φ) q q ⋯ = γ₂.v p q hpq ≫ Cochain.v (snd φ) q q ⋯
have h₃ : γ₁.v p q hpq ≫ Cochain.v (snd φ) q q sorry = γ₂.v p q hpq ≫ Cochain.v (snd φ) q q sorry
Tactic: simp only [Cochain.comp_zero_cochain_v] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
K : CochainComplex.{v, u_1, 0} C ℤ
γ₁ γ₂ : Cochain (mappingCone φ) K j
⊢ γ₁ = γ₂ ↔
    Cochain.comp (inl φ) γ₁ ⋯ = Cochain.comp (inl φ) γ₂ ⋯ ∧
      Cochain.comp (Cochain.ofHom (inr φ)) γ₁ ⋯ = Cochain.comp (Cochain.ofHom (inr φ)) γ₂ ⋯
have mp : γ₁ = γ₂ →
  Cochain.comp (inl φ) γ₁ sorry = Cochain.comp (inl φ) γ₂ sorry ∧
    Cochain.comp (Cochain.ofHom (inr φ)) γ₁ sorry = Cochain.comp (Cochain.ofHom (inr φ)) γ₂ sorry
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
K : CochainComplex.{v, u_1, 0} C ℤ
γ₁ γ₂ : Cochain (mappingCone φ) K j
mp :
  γ₁ = γ₂ →
    Cochain.comp (inl φ) γ₁ ⋯ = Cochain.comp (inl φ) γ₂ ⋯ ∧
      Cochain.comp (Cochain.ofHom (inr φ)) γ₁ ⋯ = Cochain.comp (Cochain.ofHom (inr φ)) γ₂ ⋯
⊢ γ₁ = γ₂ ↔
    Cochain.comp (inl φ) γ₁ ⋯ = Cochain.comp (inl φ) γ₂ ⋯ ∧
      Cochain.comp (Cochain.ofHom (inr φ)) γ₁ ⋯ = Cochain.comp (Cochain.ofHom (inr φ)) γ₂ ⋯
have mpr : Cochain.comp (inl φ) γ₁ sorry = Cochain.comp (inl φ) γ₂ sorry ∧
    Cochain.comp (Cochain.ofHom (inr φ)) γ₁ sorry = Cochain.comp (Cochain.ofHom (inr φ)) γ₂ sorry →
  γ₁ = γ₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
K : CochainComplex.{v, u_1, 0} C ℤ
γ₁ : Cochain (mappingCone φ) K j
⊢ Cochain.comp (inl φ) γ₁ ⋯ = Cochain.comp (inl φ) γ₁ ⋯ ∧
    Cochain.comp (Cochain.ofHom (inr φ)) γ₁ ⋯ = Cochain.comp (Cochain.ofHom (inr φ)) γ₁ ⋯
have mp : Cochain.comp (inl φ) γ₁ sorry = Cochain.comp (inl φ) γ₁ sorry
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
K : CochainComplex.{v, u_1, 0} C ℤ
γ₁ : Cochain (mappingCone φ) K j
mp : Cochain.comp (inl φ) γ₁ ⋯ = Cochain.comp (inl φ) γ₁ ⋯
⊢ Cochain.comp (inl φ) γ₁ ⋯ = Cochain.comp (inl φ) γ₁ ⋯ ∧
    Cochain.comp (Cochain.ofHom (inr φ)) γ₁ ⋯ = Cochain.comp (Cochain.ofHom (inr φ)) γ₁ ⋯
have mp₁ : Cochain.comp (Cochain.ofHom (inr φ)) γ₁ sorry = Cochain.comp (Cochain.ofHom (inr φ)) γ₁ sorry
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
K : CochainComplex.{v, u_1, 0} C ℤ
γ₁ γ₂ : Cochain (mappingCone φ) K j
h₁ : Cochain.comp (inl φ) γ₁ ⋯ = Cochain.comp (inl φ) γ₂ ⋯
h₂ : Cochain.comp (Cochain.ofHom (inr φ)) γ₁ ⋯ = Cochain.comp (Cochain.ofHom (inr φ)) γ₂ ⋯
⊢ γ₁ = γ₂
have mpr : ∀ (p q : ℤ) (hpq : p + j = q), γ₁.v p q hpq = γ₂.v p q hpq
Tactic: ext p q hpq
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
K : CochainComplex.{v, u_1, 0} C ℤ
γ₁ γ₂ : Cochain (mappingCone φ) K j
h₁ : Cochain.comp (inl φ) γ₁ ⋯ = Cochain.comp (inl φ) γ₂ ⋯
h₂ : Cochain.comp (Cochain.ofHom (inr φ)) γ₁ ⋯ = Cochain.comp (Cochain.ofHom (inr φ)) γ₂ ⋯
p q : ℤ
hpq : p + j = q
⊢ γ₁.v p q hpq = γ₂.v p q hpq
have mpr : Cochain.v (inl φ) (p + 1) p sorry ≫ γ₁.v p q hpq = Cochain.v (inl φ) (p + 1) p sorry ≫ γ₂.v p q hpq ∧
  Hom.f (inr φ) p ≫ γ₁.v p q hpq = Hom.f (inr φ) p ≫ γ₂.v p q hpq
Tactic: rw [ext_from_iff φ (p + 1) p rfl]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (hypothesis)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
K : CochainComplex.{v, u_1, 0} C ℤ
γ₁ γ₂ : Cochain (mappingCone φ) K j
h₁ : Cochain.comp (inl φ) γ₁ ⋯ = Cochain.comp (inl φ) γ₂ ⋯
h₂ : Cochain.comp (Cochain.ofHom (inr φ)) γ₁ ⋯ = Cochain.comp (Cochain.ofHom (inr φ)) γ₂ ⋯
p q : ℤ
hpq : p + j = q
⊢ Cochain.v (inl φ) (p + 1) p ⋯ ≫ γ₁.v p q hpq = Cochain.v (inl φ) (p + 1) p ⋯ ≫ γ₂.v p q hpq ∧
    Hom.f (inr φ) p ≫ γ₁.v p q hpq = Hom.f (inr φ) p ≫ γ₂.v p q hpq
have h₃ : Cochain.v (Cochain.comp (inl φ) γ₁ sorry) (p + 1) q sorry = (Cochain.comp (inl φ) γ₂ sorry).v (p + 1) q sorry
Tactic: replace h₁ := Cochain.congr_v h₁ (p + 1) q (by lia)
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (hypothesis)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
K : CochainComplex.{v, u_1, 0} C ℤ
γ₁ γ₂ : Cochain (mappingCone φ) K j
h₂ : Cochain.comp (Cochain.ofHom (inr φ)) γ₁ ⋯ = Cochain.comp (Cochain.ofHom (inr φ)) γ₂ ⋯
p q : ℤ
hpq : p + j = q
h₁ : Cochain.v (Cochain.comp (inl φ) γ₁ ⋯) (p + 1) q ⋯ = (Cochain.comp (inl φ) γ₂ ⋯).v (p + 1) q ⋯
⊢ Cochain.v (inl φ) (p + 1) p ⋯ ≫ γ₁.v p q hpq = Cochain.v (inl φ) (p + 1) p ⋯ ≫ γ₂.v p q hpq ∧
    Hom.f (inr φ) p ≫ γ₁.v p q hpq = Hom.f (inr φ) p ≫ γ₂.v p q hpq
have h₃ : (Cochain.comp (Cochain.ofHom (inr φ)) γ₁ sorry).v p q sorry = (Cochain.comp (Cochain.ofHom (inr φ)) γ₂ sorry).v p q sorry
Tactic: replace h₂ := Cochain.congr_v h₂ p q (by lia)
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (hypothesis)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
K : CochainComplex.{v, u_1, 0} C ℤ
γ₁ γ₂ : Cochain (mappingCone φ) K j
p q : ℤ
hpq : p + j = q
h₁ : Cochain.v (Cochain.comp (inl φ) γ₁ ⋯) (p + 1) q ⋯ = (Cochain.comp (inl φ) γ₂ ⋯).v (p + 1) q ⋯
h₂ : (Cochain.comp (Cochain.ofHom (inr φ)) γ₁ ⋯).v p q ⋯ = (Cochain.comp (Cochain.ofHom (inr φ)) γ₂ ⋯).v p q ⋯
⊢ Cochain.v (inl φ) (p + 1) p ⋯ ≫ γ₁.v p q hpq = Cochain.v (inl φ) (p + 1) p ⋯ ≫ γ₂.v p q hpq ∧
    Hom.f (inr φ) p ≫ γ₁.v p q hpq = Hom.f (inr φ) p ≫ γ₂.v p q hpq
have h₃ : Cochain.v (inl φ) (p + 1) p sorry ≫ γ₁.v p q hpq = Cochain.v (inl φ) (p + 1) p sorry ≫ γ₂.v p q hpq
Tactic: simp only [Cochain.comp_v (inl φ) _ _ (p + 1) p q (by lia) hpq] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (hypothesis)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
K : CochainComplex.{v, u_1, 0} C ℤ
γ₁ γ₂ : Cochain (mappingCone φ) K j
p q : ℤ
hpq : p + j = q
h₂ : (Cochain.comp (Cochain.ofHom (inr φ)) γ₁ ⋯).v p q ⋯ = (Cochain.comp (Cochain.ofHom (inr φ)) γ₂ ⋯).v p q ⋯
h₁ : Cochain.v (inl φ) (p + 1) p ⋯ ≫ γ₁.v p q hpq = Cochain.v (inl φ) (p + 1) p ⋯ ≫ γ₂.v p q hpq
⊢ Cochain.v (inl φ) (p + 1) p ⋯ ≫ γ₁.v p q hpq = Cochain.v (inl φ) (p + 1) p ⋯ ≫ γ₂.v p q hpq ∧
    Hom.f (inr φ) p ≫ γ₁.v p q hpq = Hom.f (inr φ) p ≫ γ₂.v p q hpq
have h₃ : Hom.f (inr φ) p ≫ γ₁.v p q sorry = Hom.f (inr φ) p ≫ γ₂.v p q sorry
Tactic: simp only [Cochain.zero_cochain_comp_v, Cochain.ofHom_v] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
i j k : ℤ
hij : i + -1 = j
hik : k + -1 = i
⊢ Cochain.v (inl φ) i j hij ≫ (mappingCone φ).d j i =
    HSub.hSub (α := F.X i ⟶ (mappingCone φ).X i) (φ.f i ≫ Hom.f (inr φ) i) (F.d i k ≫ Cochain.v (inl φ) k i hik)
have dsimp : homotopyCofiber.inlX φ i j sorry ≫ homotopyCofiber.d φ j i =
  HSub.hSub (α := F.X i ⟶ homotopyCofiber.X φ i) (φ.f i ≫ homotopyCofiber.inrX φ i)
    (F.d i k ≫ homotopyCofiber.inlX φ k i sorry)
Tactic: dsimp [mappingCone, inl, inr]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
i j k : ℤ
hij : i + -1 = j
hik : k + -1 = i
⊢ homotopyCofiber.inlX φ i j ⋯ ≫ homotopyCofiber.d φ j i =
    HSub.hSub (α := F.X i ⟶ homotopyCofiber.X φ i) (φ.f i ≫ homotopyCofiber.inrX φ i)
      (F.d i k ≫ homotopyCofiber.inlX φ k i ⋯)
have rw : HAdd.hAdd (α := F.X i ⟶ homotopyCofiber.X φ i) (-F.d i k ≫ homotopyCofiber.inlX φ k i sorry)
    (φ.f i ≫ homotopyCofiber.inrX φ i) =
  HSub.hSub (α := F.X i ⟶ homotopyCofiber.X φ i) (φ.f i ≫ homotopyCofiber.inrX φ i)
    (F.d i k ≫ homotopyCofiber.inlX φ k i sorry)
Tactic: rw [homotopyCofiber.inlX_d φ j i k (by dsimp; lia) (by dsimp; lia)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
⊢ (mappingCone φ).d i j ≫ Cochain.v (snd φ) j j ⋯ =
    HAdd.hAdd (α := (mappingCone φ).X i ⟶ G.X j) (Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij ≫ φ.f j)
      (Cochain.v (snd φ) i i ⋯ ≫ G.d i j)
have dsimp : homotopyCofiber.d φ i j ≫ Cochain.v (Cochain.ofHoms (homotopyCofiber.sndX φ)) j j sorry =
  HAdd.hAdd (α := homotopyCofiber.X φ i ⟶ G.X j) (β := homotopyCofiber.X φ i ⟶ G.X j)
    (homotopyCofiber.fstX φ i j hij ≫ φ.f j) (Cochain.v (Cochain.ofHoms (homotopyCofiber.sndX φ)) i i sorry ≫ G.d i j)
Tactic: dsimp [mappingCone, snd, fst]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
⊢ homotopyCofiber.d φ i j ≫ Cochain.v (Cochain.ofHoms (homotopyCofiber.sndX φ)) j j ⋯ =
    HAdd.hAdd (α := homotopyCofiber.X φ i ⟶ G.X j) (β := homotopyCofiber.X φ i ⟶ G.X j)
      (homotopyCofiber.fstX φ i j hij ≫ φ.f j) (Cochain.v (Cochain.ofHoms (homotopyCofiber.sndX φ)) i i ⋯ ≫ G.d i j)
have simp : homotopyCofiber.d φ i j ≫ homotopyCofiber.sndX φ j =
  HAdd.hAdd (α := homotopyCofiber.X φ i ⟶ G.X j) (homotopyCofiber.fstX φ i j hij ≫ φ.f j)
    (homotopyCofiber.sndX φ i ≫ G.d i j)
Tactic: simp only [Cochain.ofHoms_v]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
⊢ Eq (α := Cochain F (mappingCone φ) 0) (δ (-1) 0 (inl φ)) (Cochain.ofHom (φ ≫ inr φ))
have h : ∀ (p : ℤ),
  Eq (α := F.X p ⟶ (mappingCone φ).X p) (Cochain.v (δ (-1) 0 (inl φ)) p p sorry)
    (Cochain.v (Cochain.ofHom (φ ≫ inr φ)) p p sorry)
Tactic: ext p
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
⊢ Eq (α := Cochain (mappingCone φ) G 1) (δ 0 1 (snd φ))
    (-Cochain.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) (Cochain.ofHom φ) ⋯)
have h : ∀ (p q : ℤ) (hpq : p + 1 = q),
  Eq (α := (mappingCone φ).X p ⟶ G.X q) (Cochain.v (δ 0 1 (snd φ)) p q hpq)
    (Cochain.v (-Cochain.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) (Cochain.ofHom φ) sorry) p q hpq)
Tactic: ext p q hpq
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : Category.{v', u_2} D
inst_2 : Preadditive.{v, u_1} C
inst_3 : Preadditive.{v', u_2} D
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_4 : HasHomotopyCofiber φ
K : CochainComplex.{v, u_1, 0} C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
⊢ 1 + m = n
have rw : 1 + m = m + 1
Tactic: rw [← h, add_comm]