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
K L : CochainComplex.{v, u, 0} C ℤ
p n q' p'' q'' : ℤ
hpq'' : p'' + (n + 1) = q''
f : K.X p ⟶ L.X q''
hq' : q'' + 1 = q'
hp' : p'' + 1 = p
⊢ p = 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 n q' p'' q'' : ℤ
hpq'' : p'' + (n + 1) = q''
f : K.X p ⟶ L.X q''
hq' : q'' + 1 = q'
hp' : p'' + 1 = p
pos :
  ∀ (f : K.X (p'' + 1) ⟶ L.X q'') (hp' : p'' + 1 = p'' + 1),
    (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
      (n + 1).negOnePow • v (single (K.d p'' (p'' + 1) ≫ 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:
obtain rfl : p = p'' + 1 := 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 q' p'' q'' : ℤ
hpq'' : p'' + (n + 1) = q''
hq' : q'' + 1 = q'
f : K.X (p'' + 1) ⟶ L.X q''
hp' : p'' + 1 = p'' + 1
⊢ (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    (n + 1).negOnePow • v (single (K.d p'' (p'' + 1) ≫ f) (n + 1)) 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 ℤ
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'
neg : 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''

Tactic:
rw [single_v_eq_zero _ _ _ _ _ h, single_v_eq_zero, comp_zero, smul_zero]

Premises used: CategoryTheory.Limits.comp_zero, smul_zero, 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 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'
⊢ p'' + 1 ≠ 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' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + (n + 1) = q''
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''

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

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 ℤ
n : ℤ
D : Type u_2
inst_2 : Category.{v_1, u_2} D
inst_3 : Preadditive.{v_1, u_2} D
z : Cochain K L n
Φ : CategoryTheory.Functor.{v, v_1, u, u_2} C D
inst_4 : Φ.Additive
p q : ℤ
hpq : p + n = q
⊢ v (z.map Φ) p q hpq = Φ.map (z.v p q hpq)

Tactic:
rfl

Premises used: CochainComplex.HomComplex.Cochain.mk, CochainComplex.HomComplex.Cochain.v, CochainComplex.HomComplex.Cochain.map, rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
F G K : CochainComplex.{v, u, 0} C ℤ
D : Type u_2
inst_2 : Category.{v_1, u_2} D
inst_3 : Preadditive.{v_1, u_2} D
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
Φ : CategoryTheory.Functor.{v, v_1, u, u_2} C D
inst_4 : Φ.Additive
h₁ :
  ∀ (p q : ℤ) (hpq : p + n₁₂ = q),
    Eq (α :=
      HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) F) p ⟶
        HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K) q)
      (v ((z₁.comp z₂ h).map Φ) p q hpq :
        HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) F) p ⟶
          HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K) q)
      (v
          (comp (G := Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) G)
            (z₁.map Φ :
              Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) F)
                (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) G) n₁)
            (z₂.map Φ :
              Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) G)
                (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K) n₂)
            h)
          p q hpq :
        HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) F) p ⟶
          HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K) q)
⊢ Eq (α :=
    Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) F)
      (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K) n₁₂)
    ((z₁.comp z₂ h).map Φ :
      Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) F)
        (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K) n₁₂)
    (comp (G := Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) G)
        (z₁.map Φ :
          Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) F)
            (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) G) n₁)
        (z₂.map Φ :
          Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) G)
            (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K) n₂)
        h :
      Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) F)
        (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K) n₁₂)

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
F G K : CochainComplex.{v, u, 0} C ℤ
D : Type u_2
inst_2 : Category.{v_1, u_2} D
inst_3 : Preadditive.{v_1, u_2} D
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
Φ : CategoryTheory.Functor.{v, v_1, u, u_2} C D
inst_4 : Φ.Additive
p q : ℤ
hpq : p + n₁₂ = q
h₁ :
  Φ.map ((z₁.comp z₂ h).v p q hpq) =
    v
      (comp (G := Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) G)
        (z₁.map Φ :
          Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) F)
            (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) G) n₁)
        (z₂.map Φ :
          Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) G)
            (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K) n₂)
        h)
      p q hpq
⊢ Eq (α :=
    HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) F) p ⟶
      HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K) q)
    (v ((z₁.comp z₂ h).map Φ) p q hpq :
      HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) F) p ⟶
        HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K) q)
    (v
        (comp (G := Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) G)
          (z₁.map Φ :
            Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) F)
              (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) G) n₁)
          (z₂.map Φ :
            Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) G)
              (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K) n₂)
          h)
        p q hpq :
      HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) F) p ⟶
        HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K) q)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
F G K : CochainComplex.{v, u, 0} C ℤ
D : Type u_2
inst_2 : Category.{v_1, u_2} D
inst_3 : Preadditive.{v_1, u_2} D
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
Φ : CategoryTheory.Functor.{v, v_1, u, u_2} C D
inst_4 : Φ.Additive
p q : ℤ
hpq : p + n₁₂ = q
⊢ p + n₁ + n₂ = q

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
F G K : CochainComplex.{v, u, 0} C ℤ
D : Type u_2
inst_2 : Category.{v_1, u_2} D
inst_3 : Preadditive.{v_1, u_2} D
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
Φ : CategoryTheory.Functor.{v, v_1, u, u_2} C D
inst_4 : Φ.Additive
p q : ℤ
hpq : p + n₁₂ = q
⊢ Φ.map ((z₁.comp z₂ h).v p q hpq) =
    v
      (comp (G := Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) G)
        (z₁.map Φ :
          Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) F)
            (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) G) n₁)
        (z₂.map Φ :
          Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) G)
            (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K) n₂)
        h)
      p q hpq

Tactic:
simp only [map_v, comp_v _ _ h p _ q rfl (by lia), Φ.map_comp]

Premises used: CochainComplex.HomComplex.Cochain.map_v, CochainComplex.HomComplex.Cochain.comp_v, CategoryTheory.Functor.map_comp, 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 : ℤ
D : Type u_2
inst_2 : Category.{v_1, u_2} D
inst_3 : Preadditive.{v_1, u_2} D
z : Cochain K L n
Φ : CategoryTheory.Functor.{v, v_1, u, u_2} C D
inst_4 : Φ.Additive
pos :
  ∀ (hnm : n + 1 = m),
    Eq (α :=
      Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K)
        (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) m)
      (δ n m (z.map Φ) :
        Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K)
          (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) m)
      ((δ n m z).map Φ :
        Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K)
          (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) m)
neg :
  ∀ (hnm : ¬n + 1 = m),
    Eq (α :=
      Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K)
        (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) m)
      (δ n m (z.map Φ) :
        Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K)
          (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) m)
      ((δ n m z).map Φ :
        Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K)
          (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) m)
⊢ Eq (α :=
    Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K)
      (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) m)
    (δ n m (z.map Φ) :
      Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K)
        (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) m)
    ((δ n m z).map Φ :
      Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K)
        (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) m)

Tactic:
by_cases hnm : n + 1 = m
-- 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 : ℤ
D : Type u_2
inst_2 : Category.{v_1, u_2} D
inst_3 : Preadditive.{v_1, u_2} D
z : Cochain K L n
Φ : CategoryTheory.Functor.{v, v_1, u, u_2} C D
inst_4 : Φ.Additive
hnm : n + 1 = m
pos :
  ∀ (p q : ℤ) (hpq : p + m = q),
    Eq (α :=
      HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K) p ⟶
        HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) q)
      (Cochain.v (δ n m (z.map Φ)) p q hpq :
        HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K) p ⟶
          HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) q)
      (Cochain.v ((δ n m z).map Φ) p q hpq :
        HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K) p ⟶
          HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) q)
⊢ Eq (α :=
    Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K)
      (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) m)
    (δ n m (z.map Φ) :
      Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K)
        (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) m)
    ((δ n m z).map Φ :
      Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K)
        (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) 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 ℤ
n m : ℤ
D : Type u_2
inst_2 : Category.{v_1, u_2} D
inst_3 : Preadditive.{v_1, u_2} D
z : Cochain K L n
Φ : CategoryTheory.Functor.{v, v_1, u, u_2} C D
inst_4 : Φ.Additive
hnm : n + 1 = m
p q : ℤ
hpq : p + m = q
pos : Cochain.v (δ n m (z.map Φ)) p q hpq = Φ.map ((δ n m z).v p q hpq)
⊢ Eq (α :=
    HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K) p ⟶
      HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) q)
    (Cochain.v (δ n m (z.map Φ)) p q hpq :
      HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K) p ⟶
        HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) q)
    (Cochain.v ((δ n m z).map Φ) p q hpq :
      HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K) p ⟶
        HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) q)

Tactic:
dsimp
-- 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 : ℤ
D : Type u_2
inst_2 : Category.{v_1, u_2} D
inst_3 : Preadditive.{v_1, u_2} D
z : Cochain K L n
Φ : CategoryTheory.Functor.{v, v_1, u, u_2} C D
inst_4 : Φ.Additive
hnm : n + 1 = m
p q : ℤ
hpq : p + m = q
⊢ Cochain.v (δ n m (z.map Φ)) p q hpq = Φ.map ((δ n m z).v p q hpq)

Tactic:
simp only [δ_v n m hnm _ p q hpq (q - 1) (p + 1) rfl rfl,
      Functor.map_add, Functor.map_comp, Functor.map_units_smul,
      Cochain.map_v, Functor.mapHomologicalComplex_obj_d]

Premises used: CategoryTheory.Functor.mapHomologicalComplex_obj_d, CochainComplex.HomComplex.Cochain.map_v, CochainComplex.HomComplex.δ_v, HSub.hSub, CategoryTheory.Functor.map_add, CategoryTheory.Functor.map_units_smul, HAdd.hAdd, CategoryTheory.Functor.map_comp, OfNat.ofNat, 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 : ℤ
D : Type u_2
inst_2 : Category.{v_1, u_2} D
inst_3 : Preadditive.{v_1, u_2} D
z : Cochain K L n
Φ : CategoryTheory.Functor.{v, v_1, u, u_2} C D
inst_4 : Φ.Additive
hnm : ¬n + 1 = m
⊢ Eq (α :=
    Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K)
      (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) m)
    (δ n m (z.map Φ) :
      Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K)
        (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) m)
    ((δ n m z).map Φ :
      Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K)
        (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) m)

Tactic:
simp only [δ_shape _ _ hnm, Cochain.map_zero]

Premises used: CochainComplex.HomComplex.Cochain.map_zero, CochainComplex.HomComplex.δ_shape
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
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
K L : CochainComplex.{v, u, 0} C ℤ
n m_1 p : ℤ
α₁ α₂ : Cocycle K L n
m : ℤ
hm : m + 1 = n
β₁ : Cochain K L m
hβ₁ : δ m n β₁ = (↑α₁ : Cochain K L n)
m' : ℤ
hm' : m' + 1 = n
β₂ : Cochain K L m'
hβ₂ : δ m' n β₂ = (↑α₂ : Cochain K L n)
⊢ m = m'

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
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
K L : CochainComplex.{v, u, 0} C ℤ
n m_1 p : ℤ
α₁ α₂ : Cocycle K L n
m : ℤ
hm : m + 1 = n
β₁ : Cochain K L m
hβ₁ : δ m n β₁ = (↑α₁ : Cochain K L n)
m' : ℤ
hm' : m' + 1 = n
β₂ : Cochain K L m'
hβ₂ : δ m' n β₂ = (↑α₂ : Cochain K L n)
obtain :
  ∀ (hm' : m + 1 = n) (β₂ : Cochain K L m) (hβ₂ : δ m n β₂ = (↑α₂ : Cochain K L n)),
    Membership.mem (γ := Set (Cocycle K L n))
      {α : Cocycle K L n | ∃ (m : ℤ) (_ : m + 1 = n) (β : Cochain K L m), δ m n β = (↑α : Cochain K L n)} (α₁ + α₂)
⊢ Membership.mem (γ := Set (Cocycle K L n))
    {α : Cocycle K L n | ∃ (m : ℤ) (_ : m + 1 = n) (β : Cochain K L m), δ m n β = (↑α : Cochain K L n)} (α₁ + α₂)

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

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
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
K L : CochainComplex.{v, u, 0} C ℤ
n m_1 p : ℤ
α₁ α₂ : Cocycle K L n
m : ℤ
hm : m + 1 = n
β₁ : Cochain K L m
hβ₁ : δ m n β₁ = (↑α₁ : Cochain K L n)
hm' : m + 1 = n
β₂ : Cochain K L m
hβ₂ : δ m n β₂ = (↑α₂ : Cochain K L n)
⊢ δ m n (β₁ + β₂) = (↑(α₁ + α₂) : Cochain K L n)

Tactic:
aesop
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
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
K L : CochainComplex.{v, u, 0} C ℤ
n m_1 p : ℤ
α₁ α₂ : Cocycle K L n
m : ℤ
hm : m + 1 = n
β₁ : Cochain K L m
hβ₁ : δ m n β₁ = (↑α₁ : Cochain K L n)
hm' : m + 1 = n
β₂ : Cochain K L m
hβ₂ : δ m n β₂ = (↑α₂ : Cochain K L n)
⊢ Membership.mem (γ := Set (Cocycle K L n))
    {α : Cocycle K L n | ∃ (m : ℤ) (_ : m + 1 = n) (β : Cochain K L m), δ m n β = (↑α : Cochain K L n)} (α₁ + α₂)

Tactic:
exact ⟨m, hm, β₁ + β₂, by aesop⟩
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
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
K L : CochainComplex.{v, u, 0} C ℤ
n m p : ℤ
⊢ n - 1 + 1 = n

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
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
K L : CochainComplex.{v, u, 0} C ℤ
n m p : ℤ
⊢ Eq.{v + 1} (α := Cochain K L n) (δ (n - 1) n 0) (↑0 : Cochain K L n)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
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
K L : CochainComplex.{v, u, 0} C ℤ
n m_1 p : ℤ
α : Cocycle K L n
m : ℤ
hm : m + 1 = n
β : Cochain K L m
hβ : δ m n β = (↑α : Cochain K L n)
⊢ δ m n (-β) = (↑(-α) : Cochain K L n)

Tactic:
aesop
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
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
K L : CochainComplex.{v, u, 0} C ℤ
n m_1 p : ℤ
α : Cocycle K L n
m : ℤ
hm : m + 1 = n
β : Cochain K L m
hβ : δ m n β = (↑α : Cochain K L n)
⊢ Membership.mem (γ := Set (Cocycle K L n))
    {α : Cocycle K L n | ∃ (m : ℤ) (_ : m + 1 = n) (β : Cochain K L m), δ m n β = (↑α : Cochain K L n)} (-α)

Tactic:
exact ⟨m, hm, -β, by aesop⟩
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
α : Cocycle K L n
m : ℤ
hm : m + 1 = n
⊢ Membership.mem (γ := Set (Cocycle K L n))
      {α : Cocycle K L n | ∃ (m : ℤ) (_ : m + 1 = n) (β : Cochain K L m), δ m n β = (↑α : Cochain K L n)} α ↔
    ∃ (β : Cochain K L m), δ m n β = (↑α : Cochain K L n)

Tactic:
grind
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
⊢ Function.Surjective.{v + 1, v + 1} (α := Cocycle K L n) mk

Tactic:
Quotient.mk_surjective

Premises used: CochainComplex.HomComplex.CohomologyClass.mk, CochainComplex.HomComplex.CohomologyClass, Quotient.mk_surjective
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
⊢ Eq.{v + 1} (α := CohomologyClass K L n) (mk 0) 0

Tactic:
rfl

Premises used: CochainComplex.HomComplex.CohomologyClass.mk, rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
x y : Cocycle K L n
⊢ mk (x + y) = mk x + mk y

Tactic:
rfl

Premises used: CochainComplex.HomComplex.CohomologyClass.mk, Quotient.map₂, rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
x y : Cocycle K L n
⊢ mk (x - y) = mk x - mk y

Tactic:
rfl

Premises used: CochainComplex.HomComplex.CohomologyClass.mk, Quotient.map₂, rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
x : Cocycle K L n
⊢ mk (-x) = -mk x

Tactic:
rfl

Premises used: CochainComplex.HomComplex.CohomologyClass.mk, Quot.map, Quotient.map', rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
x : Cocycle K L n
⊢ mk x = 0 ↔ x ∈ coboundaries K L n

Tactic:
QuotientAddGroup.eq_zero_iff x

Premises used: CochainComplex.HomComplex.CohomologyClass.mk, CochainComplex.HomComplex.CohomologyClass, QuotientAddGroup.eq_zero_iff
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
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
K L : CochainComplex.{v, u, 0} C ℤ
n m p : ℤ
⊢ Eq.{v + 1} (α := CohomologyClass K L n) (mk 0) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
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
K L : CochainComplex.{v, u, 0} C ℤ
n m p : ℤ
⊢ ∀ (x y : Cocycle K L n), mk (x + y) = mk x + mk y

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
G : Type u_2
inst_2 : AddCommGroup G
f : AddMonoidHom.{v, u_2} (Cocycle K L n) G
hf : coboundaries K L n ≤ f.ker
x : Cocycle K L n
⊢ Eq.{u_2 + 1} (α := G) ((descAddMonoidHom f hf : (a : CohomologyClass K L n) → G) (mk x) : G)
    ((f : (a : Cocycle K L n) → G) x : G)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl