awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
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
⊢ 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 ⋯ ≫ f)
        (Cochain.v (snd φ) j j ⋯ ≫ Hom.f (inr φ) j ≫ f)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
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 φ) ⋯
mpr :
  γ₁.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 φ) ⋯

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
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
mp₁ : γ₁.comp (snd φ) ⋯ = γ₁.comp (snd φ) ⋯
mp₂ mp₃ mp₄ :
  γ₁.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) hij = γ₁.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) hij
mp₅ mp₆ mp₇ : γ₁.comp (snd φ) ⋯ = γ₁.comp (snd φ) ⋯
mp₈ : γ₁.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) hij = γ₁.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) hij
mp₉ : γ₁.comp (snd φ) ⋯ = γ₁.comp (snd φ) ⋯
⊢ γ₁.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) hij = γ₁.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) hij ∧
    γ₁.comp (snd φ) ⋯ = γ₁.comp (snd φ) ⋯

Tactic:
tauto
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
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 φ) ⋯
mpr : ∀ (p q : ℤ) (hpq : p + i = q), γ₁.v p q hpq = γ₂.v p q hpq
⊢ γ₁ = γ₂

Tactic:
ext p q hpq
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
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
mpr :
  γ₁.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 ⋯
⊢ γ₁.v p q hpq = γ₂.v p q hpq

Tactic:
rw [ext_to_iff φ q (q + 1) rfl]

Premises used: CochainComplex.mappingCone.ext_to_iff, HAdd.hAdd, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
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
⊢ p + j = q + 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
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
⊢ (γ₁.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) hij).v p (q + 1) ⋯ =
    (γ₂.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) hij).v p (q + 1) ⋯

Tactic:
replace h₁ := Cochain.congr_v h₁ p (q + 1) (by lia)
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
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) ⋯
⊢ (γ₁.comp (snd φ) ⋯).v p q hpq = (γ₂.comp (snd φ) ⋯).v p q hpq

Tactic:
replace h₂ := Cochain.congr_v h₂ p q hpq
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
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) ⋯

Tactic:
simp only [Cochain.comp_v _ _ _ p q (q + 1) hpq rfl] at h₁

Premises used: CochainComplex.HomComplex.Cochain.comp_v, HAdd.hAdd, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
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 (snd φ) q q ⋯ = γ₂.v p q hpq ≫ Cochain.v (snd φ) q q ⋯

Tactic:
simp only [Cochain.comp_zero_cochain_v] at h₂

Premises used: CochainComplex.HomComplex.Cochain.comp_zero_cochain_v
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
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₁ :
  γ₁.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) ⋯
h₂ : γ₁.v p q hpq ≫ Cochain.v (snd φ) q q ⋯ = γ₂.v p q hpq ≫ Cochain.v (snd φ) q 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 ⋯

Tactic:
⟨h₁, h₂⟩

Premises used: And.intro
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
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₁ :
  γ₁.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) ⋯
h₂ : γ₁.v p q hpq ≫ Cochain.v (snd φ) q q ⋯ = γ₂.v p q hpq ≫ Cochain.v (snd φ) q 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 ⋯

Tactic:
exact ⟨h₁, h₂⟩
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
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 φ
i j : ℤ
hij : i + 1 = j
K : CochainComplex.{v, u_1, 0} C ℤ
γ₁ γ₂ : Cochain (mappingCone φ) K j
⊢ -1 + j = i

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
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 φ)) γ₂ ⋯
mpr :
  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 φ)) γ₂ ⋯

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
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 φ) γ₁ ⋯
mp₁ : Cochain.comp (Cochain.ofHom (inr φ)) γ₁ ⋯ = Cochain.comp (Cochain.ofHom (inr φ)) γ₁ ⋯
mp₂ mp₃ mp₄ : Cochain.comp (inl φ) γ₁ ⋯ = Cochain.comp (inl φ) γ₁ ⋯
mp₅ mp₆ mp₇ : Cochain.comp (Cochain.ofHom (inr φ)) γ₁ ⋯ = Cochain.comp (Cochain.ofHom (inr φ)) γ₁ ⋯
mp₈ : Cochain.comp (inl φ) γ₁ ⋯ = Cochain.comp (inl φ) γ₁ ⋯
mp₉ : 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 φ)) γ₁ ⋯

Tactic:
tauto
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
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 φ)) γ₂ ⋯
mpr : ∀ (p q : ℤ) (hpq : p + j = q), γ₁.v p q hpq = γ₂.v p q hpq
⊢ γ₁ = γ₂

Tactic:
ext p q hpq
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
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
mpr :
  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
⊢ γ₁.v p q hpq = γ₂.v p q hpq

Tactic:
rw [ext_from_iff φ (p + 1) p rfl]

Premises used: CochainComplex.mappingCone.ext_from_iff, HAdd.hAdd, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
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
⊢ p + 1 + i = q

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
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 (Cochain.comp (inl φ) γ₁ ⋯) (p + 1) q ⋯ = (Cochain.comp (inl φ) γ₂ ⋯).v (p + 1) q ⋯

Tactic:
replace h₁ := Cochain.congr_v h₁ (p + 1) q (by lia)
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
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 ⋯
⊢ p + j = q

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
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.comp (Cochain.ofHom (inr φ)) γ₁ ⋯).v p q ⋯ = (Cochain.comp (Cochain.ofHom (inr φ)) γ₂ ⋯).v p q ⋯

Tactic:
replace h₂ := Cochain.congr_v h₂ p q (by lia)
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
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 ⋯
⊢ p + 1 + -1 = p

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
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

Tactic:
simp only [Cochain.comp_v (inl φ) _ _ (p + 1) p q (by lia) hpq] at h₁

Premises used: CochainComplex.HomComplex.Cochain.comp_v, HAdd.hAdd, OfNat.ofNat, CochainComplex.mappingCone.inl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
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
⊢ Hom.f (inr φ) p ≫ γ₁.v p q ⋯ = Hom.f (inr φ) p ≫ γ₂.v p q ⋯

Tactic:
simp only [Cochain.zero_cochain_comp_v, Cochain.ofHom_v] at h₂

Premises used: CochainComplex.HomComplex.Cochain.zero_cochain_comp_v, CochainComplex.HomComplex.Cochain.ofHom_v
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
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 (inl φ) (p + 1) p ⋯ ≫ γ₁.v p q hpq = Cochain.v (inl φ) (p + 1) p ⋯ ≫ γ₂.v p q hpq
h₂ : Hom.f (inr φ) p ≫ γ₁.v p q ⋯ = Hom.f (inr φ) p ≫ γ₂.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

Tactic:
⟨h₁, h₂⟩

Premises used: And.intro
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
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 (inl φ) (p + 1) p ⋯ ≫ γ₁.v p q hpq = Cochain.v (inl φ) (p + 1) p ⋯ ≫ γ₂.v p q hpq
h₂ : Hom.f (inr φ) p ≫ γ₁.v p q ⋯ = Hom.f (inr φ) p ≫ γ₂.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

Tactic:
exact ⟨h₁, h₂⟩
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
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 φ
⊢ HAdd.hAdd (α := Cochain (mappingCone φ) (mappingCone φ) 0)
      (Cochain.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) (inl φ) ⋯)
      (Cochain.comp (snd φ) (Cochain.ofHom (inr φ)) ⋯) =
    Cochain.ofHom (𝟙 (mappingCone φ))

Tactic:
simp [ext_cochain_from_iff φ (-1) 0 (neg_add_cancel 1)]

Premises used: CochainComplex.mappingCone.ext_cochain_from_iff, neg_add_cancel, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
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 φ
p q : ℤ
hpq : p + 1 = q
⊢ q + -1 = p

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
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 φ
p q : ℤ
hpq : p + 1 = q
⊢ q + -1 = p

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
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 φ
p q : ℤ
hpq : p + 1 = q
⊢ HAdd.hAdd (α := (mappingCone φ).X p ⟶ (mappingCone φ).X p)
      (Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) p q hpq ≫ Cochain.v (inl φ) q p ⋯)
      (Cochain.v (snd φ) p p ⋯ ≫ Hom.f (inr φ) p) =
    𝟙 ((mappingCone φ).X p)

Tactic:
simpa only [Cochain.add_v, Cochain.comp_zero_cochain_v, Cochain.ofHom_v, id_f,
    Cochain.comp_v _ _ (add_neg_cancel 1) p q p hpq (by lia)]
    using Cochain.congr_v (id φ) p p (add_zero p)

Premises used: add_neg_cancel, CochainComplex.mappingCone.id, CochainComplex.HomComplex.Cochain.comp_v, CochainComplex.HomComplex.Cochain.comp_zero_cochain_v, HomologicalComplex.id_f, CochainComplex.HomComplex.Cochain.congr_v, CochainComplex.HomComplex.Cochain.ofHom_v, add_zero, OfNat.ofNat, CochainComplex.HomComplex.Cochain.add_v
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
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
dsimp :
  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 ⋯)
⊢ 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)

Tactic:
dsimp [mappingCone, inl, inr]

Premises used: CochainComplex.mappingCone.inr, CochainComplex.mappingCone, CochainComplex.mappingCone.inl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
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
⊢ j + 1 = i

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
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
⊢ i + 1 = k

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
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
rw :
  HAdd.hAdd (α := F.X i ⟶ homotopyCofiber.X φ i) (-F.d i k ≫ homotopyCofiber.inlX φ k i ⋯)
      (φ.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 ⋯)
⊢ 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 ⋯)

Tactic:
rw [homotopyCofiber.inlX_d φ j i k (by dsimp; lia) (by dsimp; lia)]

Premises used: HomologicalComplex.homotopyCofiber.inlX_d
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
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
⊢ HAdd.hAdd (α := F.X i ⟶ homotopyCofiber.X φ i) (-F.d i k ≫ homotopyCofiber.inlX φ k i ⋯)
      (φ.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 ⋯)

Tactic:
abel
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
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 φ
n₁ n₂ : ℤ
⊢ Hom.f (inr φ) n₁ ≫ (mappingCone φ).d n₁ n₂ = G.d n₁ n₂ ≫ Hom.f (inr φ) n₂

Tactic:
simp