awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
F G K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
φ₁ φ₂ : F ⟶ G
z : { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }
a :
  ∀ (p q : ℤ) (hpq : p + -1 = q),
    v
        (↑((fun (ho : Homotopy φ₁ φ₂) ↦
                (Subtype.mk (p := fun (z : Cochain F G (-1)) ↦ ofHom φ₁ = δ (-1) 0 z + ofHom φ₂) (ofHomotopy ho) ⋯ :
                  { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }))
              ((fun (z : { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }) ↦
                  ({ hom := fun (i j : ℤ) ↦ if hij : i + -1 = j then (↑z : Cochain F G (-1)).v i j hij else 0,
                      zero := ⋯, comm := ⋯ } :
                    Homotopy φ₁ φ₂))
                z)) :
          Cochain F G (-1))
        p q hpq =
      (↑z : Cochain F G (-1)).v p q hpq
⊢ (fun (ho : Homotopy φ₁ φ₂) ↦
        (Subtype.mk (p := fun (z : Cochain F G (-1)) ↦ ofHom φ₁ = δ (-1) 0 z + ofHom φ₂) (ofHomotopy ho) ⋯ :
          { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }))
      ((fun (z : { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }) ↦
          ({ hom := fun (i j : ℤ) ↦ if hij : i + -1 = j then (↑z : Cochain F G (-1)).v i j hij else 0, zero := ⋯,
              comm := ⋯ } :
            Homotopy φ₁ φ₂))
        z) =
    z

Tactic:
ext p q hpq
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
F G K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
φ₁ φ₂ : F ⟶ G
z : { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }
p q : ℤ
hpq : p + -1 = q
a : (if hij : p + -1 = q then (↑z : Cochain F G (-1)).v p q hij else 0) = (↑z : Cochain F G (-1)).v p q hpq
⊢ v
      (↑((fun (ho : Homotopy φ₁ φ₂) ↦
              (Subtype.mk (p := fun (z : Cochain F G (-1)) ↦ ofHom φ₁ = δ (-1) 0 z + ofHom φ₂) (ofHomotopy ho) ⋯ :
                { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }))
            ((fun (z : { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }) ↦
                ({ hom := fun (i j : ℤ) ↦ if hij : i + -1 = j then (↑z : Cochain F G (-1)).v i j hij else 0, zero := ⋯,
                    comm := ⋯ } :
                  Homotopy φ₁ φ₂))
              z)) :
        Cochain F G (-1))
      p q hpq =
    (↑z : Cochain F G (-1)).v p q hpq

Tactic:
dsimp [Cochain.ofHomotopy]

Premises used: CochainComplex.HomComplex.Cochain.ofHomotopy
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
F G K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
φ₁ φ₂ : F ⟶ G
z : { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }
p q : ℤ
hpq : p + -1 = q
a a₁ : (↑z : Cochain F G (-1)).v p q hpq = (↑z : Cochain F G (-1)).v p q hpq
⊢ (if hij : p + -1 = q then (↑z : Cochain F G (-1)).v p q hij else 0) = (↑z : Cochain F G (-1)).v p q hpq

Tactic:
rw [dif_pos hpq]

Premises used: dif_pos
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
F G : CochainComplex.{v, u, 0} C ℤ
φ₁ φ₂ : F ⟶ G
h : φ₁ = φ₂
⊢ Eq.{v + 1} (α := Cochain F G (-1))
    (↑((equivHomotopy φ₁ φ₂ : (a : Homotopy φ₁ φ₂) → { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ })
          (Homotopy.ofEq h)) :
      Cochain F G (-1))
    0

Tactic:
rfl

Premises used: CochainComplex.HomComplex.Cochain.mk, rfl, CochainComplex.HomComplex.Cochain.ofHomotopy
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
F G : CochainComplex.{v, u, 0} C ℤ
f₁ f₂ : F ⟶ G
h : ofHom f₁ = ofHom f₂
h₁ :
  Eq.{v + 1} (α := Cochain F G 0) (↑((Cocycle.equivHom F G : (a : F ⟶ G) → Cocycle F G 0) f₁) : Cochain F G 0)
    (↑((Cocycle.equivHom F G : (a : F ⟶ G) → Cocycle F G 0) f₂) : Cochain F G 0)
⊢ Eq (α := Cocycle F G 0) ((Cocycle.equivHom F G : (a : F ⟶ G) → Cocycle F G 0) f₁ : Cocycle F G 0)
    ((Cocycle.equivHom F G : (a : F ⟶ G) → Cocycle F G 0) f₂ : Cocycle F G 0)

Tactic:
ext1
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
F G : CochainComplex.{v, u, 0} C ℤ
f₁ f₂ : F ⟶ G
h : ofHom f₁ = ofHom f₂
⊢ Eq.{v + 1} (α := Cochain F G 0) (↑((Cocycle.equivHom F G : (a : F ⟶ G) → Cocycle F G 0) f₁) : Cochain F G 0)
    (↑((Cocycle.equivHom F G : (a : F ⟶ G) → Cocycle F G 0) f₂) : Cochain F G 0)

Tactic:
h

Premises used: CochainComplex.HomComplex.Cochain.mk, CochainComplex.HomComplex.Cochain.ofHom, CochainComplex.HomComplex.Cochain.ofHoms
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
F G : CochainComplex.{v, u, 0} C ℤ
f₁ f₂ : F ⟶ G
h : ofHom f₁ = ofHom f₂
⊢ Eq.{v + 1} (α := Cochain F G 0) (↑((Cocycle.equivHom F G : (a : F ⟶ G) → Cocycle F G 0) f₁) : Cochain F G 0)
    (↑((Cocycle.equivHom F G : (a : F ⟶ G) → Cocycle F G 0) f₂) : Cochain F G 0)

Tactic:
exact h
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n : ℤ
hpq : p + n = q
dsimp : (if p = p ∧ q = q then 𝟙 (K.X p) ≫ f ≫ 𝟙 (L.X q) else 0) = f
⊢ (single f n).v p q hpq = f

Tactic:
dsimp [single]

Premises used: CochainComplex.HomComplex.Cochain.single
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n : ℤ
hpq : p + n = q
hc : p = p ∧ q = q
⊢ (if p = p ∧ q = q then 𝟙 (K.X p) ≫ f ≫ 𝟙 (L.X q) else 0) = f

Tactic:
rw [if_pos, id_comp, comp_id]

Premises used: CategoryTheory.Category.comp_id, if_pos, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n : ℤ
hpq : p + n = q
hc : p = p
hc₁ : q = q
hc₂ hc₃ hc₄ : p = p
hc₅ hc₆ hc₇ : q = q
hc₈ : p = p
hc₉ : q = q
⊢ p = p ∧ q = q

Tactic:
tauto
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n p' q' : ℤ
hpq' : p' + n = q'
hp' : p' ≠ p
hnc : ¬(p = p' ∧ q = q')
⊢ Eq.{v + 1} (α := K.X p' ⟶ L.X q')
    (if h : p = p' ∧ q = q' then (HomologicalComplex.XIsoOfEq K ⋯).inv ≫ f ≫ (HomologicalComplex.XIsoOfEq L ⋯).hom
    else 0)
    0

Tactic:
rw [dif_neg]

Premises used: dif_neg
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n p' q' : ℤ
hpq' : p' + n = q'
hp' : p' ≠ p
h : p = p' ∧ q = q'
⊢ p' = p

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n p' q' : ℤ
hpq' : p' + n = q'
hp' : p' ≠ p
h : p = p' ∧ q = q'
⊢ False

Tactic:
exact hp' (by lia)
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n p' q' : ℤ
hpq' : p' + n = q'
hq' : q' ≠ q
⊢ Eq.{v + 1} (α := K.X p' ⟶ L.X q')
    (if h : p = p' ∧ q = q' then (HomologicalComplex.XIsoOfEq K ⋯).inv ≫ f ≫ (HomologicalComplex.XIsoOfEq L ⋯).hom
    else 0)
    0

Tactic:
grind
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q n : ℤ
h :
  ∀ (p' q' : ℤ) (hpq' : p' + n = q'),
    Eq.{v + 1} (α := K.X p' ⟶ L.X q') (v (single (p := p) (q := q) 0 n) p' q' hpq') (v 0 p' q' hpq')
⊢ Eq.{v + 1} (α := Cochain K L n) (single (p := p) (q := q) 0 n) 0

Tactic:
ext p' q' hpq'
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q n p' q' : ℤ
hpq' : p' + n = q'
pos : ∀ (hp : p' = p), Eq.{v + 1} (α := K.X p' ⟶ L.X q') (v (single (p := p) (q := q) 0 n) p' q' hpq') (v 0 p' q' hpq')
neg : ∀ (hp : ¬p' = p), Eq.{v + 1} (α := K.X p' ⟶ L.X q') (v (single (p := p) (q := q) 0 n) p' q' hpq') (v 0 p' q' hpq')
⊢ Eq.{v + 1} (α := K.X p' ⟶ L.X q') (v (single (p := p) (q := q) 0 n) p' q' hpq') (v 0 p' q' hpq')

Tactic:
by_cases hp : p' = p
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q n p' q' : ℤ
hpq' : p' + n = q'
hp : p' = p
pos : Eq.{v + 1} (α := K.X p' ⟶ L.X q') (v (single (p := p') (q := q) 0 n) p' q' hpq') (v 0 p' q' hpq')
⊢ Eq.{v + 1} (α := K.X p' ⟶ L.X q') (v (single (p := p) (q := q) 0 n) p' q' hpq') (v 0 p' q' hpq')

Tactic:
subst hp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
q n p' q' : ℤ
hpq' : p' + n = q'
pos : ∀ (hq : q' = q), Eq.{v + 1} (α := K.X p' ⟶ L.X q') (v (single (p := p') (q := q) 0 n) p' q' hpq') (v 0 p' q' hpq')
neg :
  ∀ (hq : ¬q' = q), Eq.{v + 1} (α := K.X p' ⟶ L.X q') (v (single (p := p') (q := q) 0 n) p' q' hpq') (v 0 p' q' hpq')
⊢ Eq.{v + 1} (α := K.X p' ⟶ L.X q') (v (single (p := p') (q := q) 0 n) p' q' hpq') (v 0 p' q' hpq')

Tactic:
by_cases hq : q' = q
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
q n p' q' : ℤ
hpq' : p' + n = q'
hq : q' = q
pos : Eq.{v + 1} (α := K.X p' ⟶ L.X q') (v (single (p := p') (q := q') 0 n) p' q' hpq') (v 0 p' q' hpq')
⊢ Eq.{v + 1} (α := K.X p' ⟶ L.X q') (v (single (p := p') (q := q) 0 n) p' q' hpq') (v 0 p' q' hpq')

Tactic:
subst hq
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n p' q' : ℤ
hpq' : p' + n = q'
⊢ Eq.{v + 1} (α := K.X p' ⟶ L.X q') (v (single (p := p') (q := q') 0 n) p' q' hpq') (v 0 p' q' hpq')

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
q n p' q' : ℤ
hpq' : p' + n = q'
hq : ¬q' = q
⊢ Eq.{v + 1} (α := K.X p' ⟶ L.X q') (v (single (p := p') (q := q) 0 n) p' q' hpq') (v 0 p' q' hpq')

Tactic:
simp [single_v_eq_zero' _ _ _ _ _ hq]

Premises used: CochainComplex.HomComplex.Cochain.single_v_eq_zero'
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q n p' q' : ℤ
hpq' : p' + n = q'
hp : ¬p' = p
⊢ Eq.{v + 1} (α := K.X p' ⟶ L.X q') (v (single (p := p) (q := q) 0 n) p' q' hpq') (v 0 p' q' hpq')

Tactic:
simp [single_v_eq_zero _ _ _ _ _ hp]

Premises used: CochainComplex.HomComplex.Cochain.single_v_eq_zero
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
h :
  ∀ (p'' q'' : ℤ) (hpq'' : p'' + m = q''),
    (δ n m (single f n)).v p'' q'' hpq'' =
      (single (f ≫ L.d q q') m + m.negOnePow • single (K.d p' p ≫ f) m).v p'' q'' hpq''
⊢ δ n m (single f n) = single (f ≫ L.d q q') m + m.negOnePow • single (K.d p' p ≫ f) m

Tactic:
ext p'' q'' hpq''
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + m = q''
⊢ p'' + m = q''

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + m = q''
⊢ p'' + 1 = p'' + 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + m = q''
h :
  (single f n).v p'' (q'' - 1) ⋯ ≫ L.d (q'' - 1) q'' +
      m.negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    (single (f ≫ L.d q q') m).v p'' q'' hpq'' + m.negOnePow • (single (K.d p' p ≫ f) m).v p'' q'' hpq''
⊢ (δ n m (single f n)).v p'' q'' hpq'' =
    (single (f ≫ L.d q q') m + m.negOnePow • single (K.d p' p ≫ f) m).v p'' q'' hpq''

Tactic:
rw [δ_v n m hm (single f n) p'' q'' (by lia) (q'' - 1) (p'' + 1) rfl (by lia),
    add_v, units_smul_v]

Premises used: CochainComplex.HomComplex.δ_v, HSub.hSub, CochainComplex.HomComplex.Cochain.units_smul_v, HAdd.hAdd, CochainComplex.HomComplex.Cochain.single, OfNat.ofNat, CochainComplex.HomComplex.Cochain.add_v, rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + m = q''
h : (single f n).v p'' (q'' - 1) ⋯ ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d q q') m).v p'' q'' hpq''
h₁ :
  m.negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    m.negOnePow • (single (K.d p' p ≫ f) m).v p'' q'' hpq''
⊢ (single f n).v p'' (q'' - 1) ⋯ ≫ L.d (q'' - 1) q'' +
      m.negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    (single (f ≫ L.d q q') m).v p'' q'' hpq'' + m.negOnePow • (single (K.d p' p ≫ f) m).v p'' q'' hpq''

Tactic:
congr 1
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + m = q''
pos : ∀ (h : p'' = p), (single f n).v p'' (q'' - 1) ⋯ ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d q q') m).v p'' q'' hpq''
neg : ∀ (h : ¬p'' = p), (single f n).v p'' (q'' - 1) ⋯ ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d q q') m).v p'' q'' hpq''
⊢ (single f n).v p'' (q'' - 1) ⋯ ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d q q') m).v p'' q'' hpq''

Tactic:
by_cases h : p'' = p
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + m = q''
h : p'' = p
pos :
  ∀ (f : K.X p'' ⟶ L.X q) (hp' : p' + 1 = p''),
    (single f n).v p'' (q'' - 1) ⋯ ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d q q') m).v p'' q'' hpq''
⊢ (single f n).v p'' (q'' - 1) ⋯ ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d q q') m).v p'' q'' hpq''

Tactic:
subst h
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
q n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + m = q''
f : K.X p'' ⟶ L.X q
hp' : p' + 1 = p''
pos :
  ∀ (h : q = q'' - 1), (single f n).v p'' (q'' - 1) ⋯ ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d q q') m).v p'' q'' hpq''
neg :
  ∀ (h : ¬q = q'' - 1), (single f n).v p'' (q'' - 1) ⋯ ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d q q') m).v p'' q'' hpq''
⊢ (single f n).v p'' (q'' - 1) ⋯ ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d q q') m).v p'' q'' hpq''

Tactic:
by_cases h : q = q'' - 1
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
q n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + m = q''
f : K.X p'' ⟶ L.X q
hp' : p' + 1 = p''
h : q = q'' - 1
pos :
  ∀ (hq' : q'' - 1 + 1 = q') (f : K.X p'' ⟶ L.X (q'' - 1)),
    (single f n).v p'' (q'' - 1) ⋯ ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d (q'' - 1) q') m).v p'' q'' hpq''
⊢ (single f n).v p'' (q'' - 1) ⋯ ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d q q') m).v p'' q'' hpq''

Tactic:
subst h
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
hm : n + 1 = m
p' q' p'' q'' : ℤ
hpq'' : p'' + m = q''
hp' : p' + 1 = p''
hq' : q'' - 1 + 1 = q'
f : K.X p'' ⟶ L.X (q'' - 1)
⊢ q' = q''

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
hm : n + 1 = m
p' q' p'' q'' : ℤ
hpq'' : p'' + m = q''
hp' : p' + 1 = p''
hq' : q'' - 1 + 1 = q'
f : K.X p'' ⟶ L.X (q'' - 1)
pos :
  ∀ (hpq'' : p'' + m = q') (hq' : q' - 1 + 1 = q') (f : K.X p'' ⟶ L.X (q' - 1)),
    (single f n).v p'' (q' - 1) ⋯ ≫ L.d (q' - 1) q' = (single (f ≫ L.d (q' - 1) q') m).v p'' q' hpq''
⊢ (single f n).v p'' (q'' - 1) ⋯ ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d (q'' - 1) q') m).v p'' q'' hpq''

Tactic:
obtain rfl : q' = q'' := by lia

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
hm : n + 1 = m
p' q' p'' : ℤ
hp' : p' + 1 = p''
hpq'' : p'' + m = q'
hq' : q' - 1 + 1 = q'
f : K.X p'' ⟶ L.X (q' - 1)
⊢ (single f n).v p'' (q' - 1) ⋯ ≫ L.d (q' - 1) q' = (single (f ≫ L.d (q' - 1) q') m).v p'' q' hpq''

Tactic:
simp only [single_v]

Premises used: CochainComplex.HomComplex.Cochain.single_v
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
q n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + m = q''
f : K.X p'' ⟶ L.X q
hp' : p' + 1 = p''
h : ¬q = q'' - 1
neg : q'' ≠ q'
neg₁ : q'' - 1 ≠ q
⊢ (single f n).v p'' (q'' - 1) ⋯ ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d q q') m).v p'' q'' hpq''

Tactic:
rw [single_v_eq_zero', single_v_eq_zero', zero_comp]

Premises used: CochainComplex.HomComplex.Cochain.single_v_eq_zero', CategoryTheory.Limits.zero_comp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
q n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + m = q''
f : K.X p'' ⟶ L.X q
hp' : p' + 1 = p''
h : ¬q = q'' - 1
⊢ q'' ≠ q'

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
q n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + m = q''
f : K.X p'' ⟶ L.X q
hp' : p' + 1 = p''
h : ¬q = q'' - 1
⊢ q'' - 1 ≠ q

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + m = q''
h : ¬p'' = p
neg : CategoryStruct.comp (Y := L.X (q'' - 1)) 0 (L.d (q'' - 1) q'') = (single (f ≫ L.d q q') m).v p'' q'' hpq''
neg₁ : Eq (α := K.X p'' ⟶ L.X q'') (CategoryStruct.comp (Y := L.X (q'' - 1)) 0 (L.d (q'' - 1) q'')) 0
neg₂ neg₃ : Eq.{v + 1} (α := K.X p'' ⟶ L.X q'') 0 0
⊢ (single f n).v p'' (q'' - 1) ⋯ ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d q q') m).v p'' q'' hpq''

Tactic:
rw [single_v_eq_zero _ _ _ _ _ h, single_v_eq_zero _ _ _ _ _ h, zero_comp]

Premises used: CategoryTheory.Limits.zero_comp, CochainComplex.HomComplex.Cochain.single_v_eq_zero
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + m = q''
h :
  ∀ (hpq'' : p'' + (n + 1) = q''),
    (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
      (n + 1).negOnePow • v (single (K.d p' p ≫ f) (n + 1)) p'' q'' hpq''
⊢ m.negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    m.negOnePow • (single (K.d p' p ≫ f) m).v p'' q'' hpq''

Tactic:
subst hm
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n p' q' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + (n + 1) = q''
pos :
  ∀ (h : q'' = q),
    (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
      (n + 1).negOnePow • v (single (K.d p' p ≫ f) (n + 1)) p'' q'' hpq''
neg :
  ∀ (h : ¬q'' = q),
    (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
      (n + 1).negOnePow • v (single (K.d p' p ≫ f) (n + 1)) p'' q'' hpq''
⊢ (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    (n + 1).negOnePow • v (single (K.d p' p ≫ f) (n + 1)) p'' q'' hpq''

Tactic:
by_cases h : q'' = q
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n p' q' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + (n + 1) = q''
h : q'' = q
pos :
  ∀ (f : K.X p ⟶ L.X q'') (hq' : q'' + 1 = q'),
    (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
      (n + 1).negOnePow • v (single (K.d p' p ≫ f) (n + 1)) p'' q'' hpq''
⊢ (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    (n + 1).negOnePow • v (single (K.d p' p ≫ f) (n + 1)) p'' q'' hpq''

Tactic:
subst h
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p n p' q' : ℤ
hp' : p' + 1 = p
p'' q'' : ℤ
hpq'' : p'' + (n + 1) = q''
f : K.X p ⟶ L.X q''
hq' : q'' + 1 = q'
pos :
  ∀ (h : p'' = p'),
    (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
      (n + 1).negOnePow • v (single (K.d p' p ≫ f) (n + 1)) p'' q'' hpq''
neg :
  ∀ (h : ¬p'' = p'),
    (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
      (n + 1).negOnePow • v (single (K.d p' p ≫ f) (n + 1)) p'' q'' hpq''
⊢ (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    (n + 1).negOnePow • v (single (K.d p' p ≫ f) (n + 1)) p'' q'' hpq''

Tactic:
by_cases h : p'' = p'
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p n p' q' : ℤ
hp' : p' + 1 = p
p'' q'' : ℤ
hpq'' : p'' + (n + 1) = q''
f : K.X p ⟶ L.X q''
hq' : q'' + 1 = q'
h : p'' = p'
pos :
  ∀ (hp' : p'' + 1 = p),
    (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
      (n + 1).negOnePow • v (single (K.d p'' p ≫ f) (n + 1)) p'' q'' hpq''
⊢ (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    (n + 1).negOnePow • v (single (K.d p' p ≫ f) (n + 1)) p'' q'' hpq''

Tactic:
subst h