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 φ
p q : ℤ
hpq : p + -1 = q
⊢ CategoryStruct.comp (Y := (mappingCone φ).X q) (Cochain.v (inl φ) p q hpq) (Cochain.v (snd φ) q q ⋯) = 0

Tactic:
simp [inl, snd]

Premises used: CochainComplex.mappingCone.snd, 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 φ
p q : ℤ
hpq : p + 1 = q
⊢ CategoryStruct.comp (Y := (mappingCone φ).X p) (Hom.f (inr φ) p)
      (Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) p q hpq) =
    0

Tactic:
simp [inr, fst]

Premises used: CochainComplex.mappingCone.inr, CochainComplex.mappingCone.fst
-- 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 : ℤ
⊢ CategoryStruct.comp (Y := (mappingCone φ).X p) (Hom.f (inr φ) p) (Cochain.v (snd φ) p p ⋯) = 𝟙 (G.X p)

Tactic:
simp [inr, snd]

Premises used: CochainComplex.mappingCone.inr, CochainComplex.mappingCone.snd
-- 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 φ
h :
  ∀ (p : ℤ),
    (Cochain.comp (G := mappingCone φ) (inl φ) (↑(fst φ) : Cochain (mappingCone φ) F 1) ⋯).v p p ⋯ =
      (Cochain.ofHom (𝟙 F)).v p p ⋯
⊢ Cochain.comp (G := mappingCone φ) (inl φ) (↑(fst φ) : Cochain (mappingCone φ) F 1) ⋯ = Cochain.ofHom (𝟙 F)

Tactic:
ext p
-- 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 : ℤ
⊢ 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 φ
p : ℤ
⊢ (Cochain.comp (G := mappingCone φ) (inl φ) (↑(fst φ) : Cochain (mappingCone φ) F 1) ⋯).v p p ⋯ =
    (Cochain.ofHom (𝟙 F)).v p p ⋯

Tactic:
simp [Cochain.comp_v _ _ (neg_add_cancel 1) p (p - 1) p rfl (by lia)]

Premises used: CochainComplex.HomComplex.Cochain.comp_v, HSub.hSub, neg_add_cancel, 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 φ
h :
  ∀ (p q : ℤ) (hpq : p + -1 = q), (Cochain.comp (G := mappingCone φ) (inl φ) (snd φ) ⋯).v p q hpq = Cochain.v 0 p q hpq
⊢ Cochain.comp (G := mappingCone φ) (inl φ) (snd φ) ⋯ = 0

Tactic:
ext
-- 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
⊢ (Cochain.comp (G := mappingCone φ) (inl φ) (snd φ) ⋯).v p q hpq = Cochain.v 0 p q hpq

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 φ
h :
  ∀ (p q : ℤ) (hpq : p + 1 = q),
    (Cochain.comp (G := mappingCone φ) (Cochain.ofHom (inr φ)) (↑(fst φ) : Cochain (mappingCone φ) F 1) ⋯).v p q hpq =
      Cochain.v 0 p q hpq
⊢ Cochain.comp (G := mappingCone φ) (Cochain.ofHom (inr φ)) (↑(fst φ) : Cochain (mappingCone φ) F 1) ⋯ = 0

Tactic:
ext
-- 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
⊢ (Cochain.comp (G := mappingCone φ) (Cochain.ofHom (inr φ)) (↑(fst φ) : Cochain (mappingCone φ) F 1) ⋯).v p q hpq =
    Cochain.v 0 p q hpq

Tactic:
simp
-- 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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
d e : ℤ
γ : Cochain F K d
he : 1 + d = e
rw : -1 + (1 + d) = d
rw₁ rw₂ : d = d
⊢ -1 + e = d

Tactic:
rw [← he, neg_add_cancel_left]

Premises used: neg_add_cancel_left
-- 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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
d e : ℤ
γ : Cochain F K d
he : 1 + d = e
⊢ 1 + d = e

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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
d e : ℤ
γ : Cochain F K d
he : 1 + d = e
⊢ HAdd.hAdd (α := ℤ) (-1) 1 + d = d

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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
d e : ℤ
γ : Cochain F K d
he : 1 + d = e
rw : (Cochain.comp (G := mappingCone φ) (inl φ) (↑(fst φ) : Cochain (mappingCone φ) F 1) ⋯).comp γ ⋯ = γ
rw₁ : (Cochain.ofHom (𝟙 F)).comp γ ⋯ = γ
rw₂ rw₃ : γ = γ
⊢ Cochain.comp (G := mappingCone φ) (inl φ) (Cochain.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) γ he) ⋯ = γ

Tactic:
rw [← Cochain.comp_assoc _ _ _ (neg_add_cancel 1) (by lia) (by lia), inl_fst,
    Cochain.id_comp]

Premises used: CochainComplex.HomComplex.Cochain.comp_assoc, neg_add_cancel, CochainComplex.mappingCone.inl_fst, CochainComplex.HomComplex.Cochain.id_comp, OfNat.ofNat
-- 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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
d e f : ℤ
γ : Cochain G K d
he : 0 + d = e
hf : -1 + e = f
⊢ e = d

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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
d e f : ℤ
γ : Cochain G K d
he : 0 + d = e
hf : -1 + e = f
obtain :
  ∀ (γ : Cochain G K e) (he : 0 + e = e), Cochain.comp (G := mappingCone φ) (inl φ) (Cochain.comp (snd φ) γ he) hf = 0
⊢ Cochain.comp (G := mappingCone φ) (inl φ) (Cochain.comp (snd φ) γ he) hf = 0

Tactic:
obtain rfl : e = d := by lia

Premises used: 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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
e f : ℤ
hf : -1 + e = f
γ : Cochain G K e
he : 0 + e = e
rw : (Cochain.comp (G := mappingCone φ) (inl φ) (snd φ) ⋯).comp γ hf = 0
rw₁ : Eq (α := Cochain F K f) (Cochain.comp 0 γ hf) 0
rw₂ rw₃ : Eq.{v + 1} (α := Cochain F K f) 0 0
⊢ Cochain.comp (G := mappingCone φ) (inl φ) (Cochain.comp (snd φ) γ he) hf = 0

Tactic:
rw [← Cochain.comp_assoc_of_second_is_zero_cochain, inl_snd, Cochain.zero_comp]

Premises used: CochainComplex.mappingCone.inl_snd, CochainComplex.HomComplex.Cochain.zero_comp, CochainComplex.HomComplex.Cochain.comp_assoc_of_second_is_zero_cochain
-- 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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
d e f : ℤ
γ : Cochain F K d
he : 1 + d = e
hf : 0 + e = f
⊢ e = f

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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
d e f : ℤ
γ : Cochain F K d
he : 1 + d = e
hf : 0 + e = f
obtain :
  ∀ (hf : 0 + e = e),
    Cochain.comp (G := mappingCone φ) (Cochain.ofHom (inr φ))
        (Cochain.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) γ he) hf =
      0
⊢ Cochain.comp (G := mappingCone φ) (Cochain.ofHom (inr φ)) (Cochain.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) γ he)
      hf =
    0

Tactic:
obtain rfl : e = f := by lia

Premises used: 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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
d e : ℤ
γ : Cochain F K d
he : 1 + d = e
hf : 0 + e = e
rw :
  (Cochain.comp (G := mappingCone φ) (Cochain.ofHom (inr φ)) (↑(fst φ) : Cochain (mappingCone φ) F 1) ⋯).comp γ he = 0
rw₁ : Eq (α := Cochain G K e) (Cochain.comp 0 γ he) 0
rw₂ rw₃ : Eq.{v + 1} (α := Cochain G K e) 0 0
⊢ Cochain.comp (G := mappingCone φ) (Cochain.ofHom (inr φ)) (Cochain.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) γ he)
      hf =
    0

Tactic:
rw [← Cochain.comp_assoc_of_first_is_zero_cochain, inr_fst, Cochain.zero_comp]

Premises used: CochainComplex.HomComplex.Cochain.comp_assoc_of_first_is_zero_cochain, CochainComplex.HomComplex.Cochain.zero_comp, CochainComplex.mappingCone.inr_fst
-- 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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
d e : ℤ
γ : Cochain G K d
he : 0 + d = e
⊢ 0 + e = d

Tactic:
simp only [← he, zero_add]

Premises used: zero_add
-- 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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
d e : ℤ
γ : Cochain G K d
he : 0 + d = e
⊢ d = e

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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
d e : ℤ
γ : Cochain G K d
he : 0 + d = e
obtain : ∀ (he : 0 + d = d), Cochain.comp (G := mappingCone φ) (Cochain.ofHom (inr φ)) (Cochain.comp (snd φ) γ he) ⋯ = γ
⊢ Cochain.comp (G := mappingCone φ) (Cochain.ofHom (inr φ)) (Cochain.comp (snd φ) γ he) ⋯ = γ

Tactic:
obtain rfl : d = e := by lia

Premises used: 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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
d : ℤ
γ : Cochain G K d
he : 0 + d = d
rw : (Cochain.comp (G := mappingCone φ) (Cochain.ofHom (inr φ)) (snd φ) ⋯).comp γ he = γ
rw₁ : (Cochain.ofHom (𝟙 G)).comp γ he = γ
rw₂ rw₃ : γ = γ
⊢ Cochain.comp (G := mappingCone φ) (Cochain.ofHom (inr φ)) (Cochain.comp (snd φ) γ he) ⋯ = γ

Tactic:
rw [← Cochain.comp_assoc_of_first_is_zero_cochain, inr_snd, Cochain.id_comp]

Premises used: CochainComplex.HomComplex.Cochain.comp_assoc_of_first_is_zero_cochain, CochainComplex.mappingCone.inr_snd, CochainComplex.HomComplex.Cochain.id_comp
-- 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
A : C
f g : A ⟶ (mappingCone φ).X i
h₁ :
  f ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij =
    g ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij
h₂ : f ≫ Cochain.v (snd φ) i i ⋯ = g ≫ Cochain.v (snd φ) i i ⋯
⊢ f ≫ homotopyCofiber.sndX φ i = g ≫ homotopyCofiber.sndX φ i

Tactic:
simpa [snd] using h₂

Premises used: CochainComplex.mappingCone.snd
-- 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
A : C
f g : A ⟶ (mappingCone φ).X i
mp :
  f = g →
    f ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij =
        g ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij ∧
      f ≫ Cochain.v (snd φ) i i ⋯ = g ≫ Cochain.v (snd φ) i i ⋯
mpr :
  f ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij =
        g ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij ∧
      f ≫ Cochain.v (snd φ) i i ⋯ = g ≫ Cochain.v (snd φ) i i ⋯ →
    f = g
⊢ f = g ↔
    f ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij =
        g ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij ∧
      f ≫ Cochain.v (snd φ) i i ⋯ = g ≫ Cochain.v (snd φ) i i ⋯

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
A : C
f : A ⟶ (mappingCone φ).X i
mp :
  f ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij =
    f ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij
mp₁ : f ≫ Cochain.v (snd φ) i i ⋯ = f ≫ Cochain.v (snd φ) i i ⋯
mp₂ mp₃ mp₄ :
  f ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij =
    f ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij
mp₅ mp₆ mp₇ : f ≫ Cochain.v (snd φ) i i ⋯ = f ≫ Cochain.v (snd φ) i i ⋯
mp₈ :
  f ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij =
    f ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij
mp₉ : f ≫ Cochain.v (snd φ) i i ⋯ = f ≫ Cochain.v (snd φ) i i ⋯
⊢ f ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij =
      f ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij ∧
    f ≫ Cochain.v (snd φ) i i ⋯ = f ≫ Cochain.v (snd φ) i i ⋯

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
A : C
f g : A ⟶ (mappingCone φ).X i
h₁ :
  f ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij =
    g ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij
h₂ : f ≫ Cochain.v (snd φ) i i ⋯ = g ≫ Cochain.v (snd φ) i i ⋯
⊢ f = g

Tactic:
ext_to φ i j hij h₁ h₂

Premises used: CochainComplex.mappingCone.ext_to
-- 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
A : C
f g : A ⟶ (mappingCone φ).X i
h₁ :
  f ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij =
    g ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij
h₂ : f ≫ Cochain.v (snd φ) i i ⋯ = g ≫ Cochain.v (snd φ) i i ⋯
⊢ f = g

Tactic:
exact ext_to φ i j hij h₁ h₂

Premises used: CochainComplex.mappingCone.ext_to
-- 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 : j + 1 = i
A : C
f g : (mappingCone φ).X j ⟶ A
⊢ i + -1 = j

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 : j + 1 = i
A : C
f g : (mappingCone φ).X j ⟶ A
h₁ : Cochain.v (inl φ) i j ⋯ ≫ f = Cochain.v (inl φ) i j ⋯ ≫ g
h₂ : Hom.f (inr φ) j ≫ f = Hom.f (inr φ) j ≫ g
⊢ f = g

Tactic:
homotopyCofiber.ext_from_X φ i j hij h₁ h₂

Premises used: HomologicalComplex.homotopyCofiber.X, dite, HomologicalComplex.homotopyCofiber.ext_from_X
-- 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 : j + 1 = i
A : C
f g : (mappingCone φ).X j ⟶ A
mp : f = g → Cochain.v (inl φ) i j ⋯ ≫ f = Cochain.v (inl φ) i j ⋯ ≫ g ∧ Hom.f (inr φ) j ≫ f = Hom.f (inr φ) j ≫ g
mpr : Cochain.v (inl φ) i j ⋯ ≫ f = Cochain.v (inl φ) i j ⋯ ≫ g ∧ Hom.f (inr φ) j ≫ f = Hom.f (inr φ) j ≫ g → f = g
⊢ f = g ↔ Cochain.v (inl φ) i j ⋯ ≫ f = Cochain.v (inl φ) i j ⋯ ≫ g ∧ Hom.f (inr φ) j ≫ f = Hom.f (inr φ) j ≫ g

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 : j + 1 = i
A : C
f : (mappingCone φ).X j ⟶ A
mp : Cochain.v (inl φ) i j ⋯ ≫ f = Cochain.v (inl φ) i j ⋯ ≫ f
mp₁ : Hom.f (inr φ) j ≫ f = Hom.f (inr φ) j ≫ f
mp₂ mp₃ mp₄ : Cochain.v (inl φ) i j ⋯ ≫ f = Cochain.v (inl φ) i j ⋯ ≫ f
mp₅ mp₆ mp₇ : Hom.f (inr φ) j ≫ f = Hom.f (inr φ) j ≫ f
mp₈ : Cochain.v (inl φ) i j ⋯ ≫ f = Cochain.v (inl φ) i j ⋯ ≫ f
mp₉ : Hom.f (inr φ) j ≫ f = Hom.f (inr φ) j ≫ f
⊢ Cochain.v (inl φ) i j ⋯ ≫ f = Cochain.v (inl φ) i j ⋯ ≫ f ∧ Hom.f (inr φ) j ≫ f = Hom.f (inr φ) j ≫ f

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 : j + 1 = i
A : C
f g : (mappingCone φ).X j ⟶ A
h₁ : Cochain.v (inl φ) i j ⋯ ≫ f = Cochain.v (inl φ) i j ⋯ ≫ g
h₂ : Hom.f (inr φ) j ≫ f = Hom.f (inr φ) j ≫ g
⊢ f = g

Tactic:
ext_from φ i j hij h₁ h₂

Premises used: CochainComplex.mappingCone.ext_from
-- 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 : j + 1 = i
A : C
f g : (mappingCone φ).X j ⟶ A
h₁ : Cochain.v (inl φ) i j ⋯ ≫ f = Cochain.v (inl φ) i j ⋯ ≫ g
h₂ : Hom.f (inr φ) j ≫ f = Hom.f (inr φ) j ≫ g
⊢ f = g

Tactic:
exact ext_from φ i j hij h₁ h₂

Premises used: CochainComplex.mappingCone.ext_from
-- 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 : ℤ
A : C
f : A ⟶ (mappingCone φ).X i
j : ℤ
hij : i + 1 = j
a : A ⟶ F.X j
b : A ⟶ G.X 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 : ℤ
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
h₂ :
  f ≫ Cochain.v (snd φ) i i ⋯ =
    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 (snd φ) i i ⋯
⊢ 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)

Tactic:
apply ext_to φ i j hij

Premises used: CochainComplex.mappingCone.ext_to
-- 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 : ℤ
A : C
f : A ⟶ (mappingCone φ).X i
j : ℤ
hij : i + 1 = j
⊢ 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

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 : ℤ
A : C
f : A ⟶ (mappingCone φ).X i
j : ℤ
hij : i + 1 = j
⊢ f ≫ Cochain.v (snd φ) i i ⋯ =
    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 (snd φ) i i ⋯

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 φ
j : ℤ
A : C
f : (mappingCone φ).X j ⟶ A
i : ℤ
hij : j + 1 = i
⊢ i + -1 = j

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 φ
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)
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 ⋯ ≫ 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)

Tactic:
apply ext_from φ i j hij

Premises used: CochainComplex.mappingCone.ext_from
-- 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
⊢ 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)

Tactic:
simp