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 x x_1 x_2 : ℤ
h : (ComplexShape.up ℤ).Rel x x_1
h_1 : (ComplexShape.up ℤ).Rel x_1 x_2
x_3 : (↑(AddCommGrpCat.of (Cochain F G x)) : Type v)
p q : ℤ
hpq : p + x_2 = q
⊢ Eq.{v + 1} (α := F.X p ⟶ G.X q)
    (Cochain.v
      ((AddCommGrpCat.Hom.hom
            (CategoryStruct.comp (Y := AddCommGrpCat.of (Cochain F G x_1))
              (AddCommGrpCat.ofHom (↑(δ_hom ℤ F G x x_1) : Cochain F G x →+ Cochain F G x_1))
              (AddCommGrpCat.ofHom (↑(δ_hom ℤ F G x_1 x_2) : Cochain F G x_1 →+ Cochain F G x_2))) :
          (a : (↑(AddCommGrpCat.of (Cochain F G x)) : Type v)) → (↑(AddCommGrpCat.of (Cochain F G x_2)) : Type v))
        x_3)
      p q hpq)
    (Cochain.v
      ((AddCommGrpCat.Hom.hom 0 :
          (a : (↑(AddCommGrpCat.of (Cochain F G x)) : Type v)) → (↑(AddCommGrpCat.of (Cochain F G x_2)) : Type v))
        x_3)
      p q hpq)

Tactic:
simp [δ_δ]

Premises used: CochainComplex.HomComplex.δ_δ
-- 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 : ℤ
⊢ AddCommGroup ↥(cocycle F G n)

Tactic:
infer_instance
-- 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 ℤ
n m : ℤ
hnm : n + 1 = m
z : Cochain F G n
subst : z ∈ cocycle F G n ↔ Eq (α := Cochain F G (n + 1)) (δ n (n + 1) z) 0
⊢ z ∈ cocycle F G n ↔ δ n m z = 0

Tactic:
subst hnm
-- 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 ℤ
n : ℤ
z : Cochain F G n
⊢ z ∈ cocycle F G n ↔ Eq (α := Cochain F G (n + 1)) (δ n (n + 1) z) 0

Tactic:
rfl
-- 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 ℤ
n : ℤ
z₁ z₂ : Cocycle F G n
h : (↑z₁ : Cochain F G n) = (↑z₂ : Cochain F G n)
⊢ z₁ = z₂

Tactic:
Subtype.ext h

Premises used: CochainComplex.HomComplex.Cocycle, Subtype.ext
-- 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 : ℤ
r : R
z : Cocycle F G n
⊢ (↑z : Cochain F G n) ∈ cocycle F G n

Tactic:
have hz := z.2
-- 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 : ℤ
r : R
z : Cocycle F G n
hz : (↑z : Cochain F G n) ∈ cocycle F G n
rw :
  ∀ (hz : Eq (α := Cochain F G (n + 1)) (δ n (n + 1) (↑z : Cochain F G n)) 0),
    Eq (α := Cochain F G (n + 1)) (δ n (n + 1) (r • (↑z : Cochain F G n))) 0
⊢ r • (↑z : Cochain F G n) ∈ cocycle F G n

Tactic:
rw [mem_iff n (n + 1) rfl] at hz ⊢

Premises used: HAdd.hAdd, OfNat.ofNat, rfl, CochainComplex.HomComplex.Cocycle.mem_iff
-- 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 : ℤ
r : R
z : Cocycle F G n
hz : Eq (α := Cochain F G (n + 1)) (δ n (n + 1) (↑z : Cochain F G n)) 0
⊢ Eq (α := Cochain F G (n + 1)) (δ n (n + 1) (r • (↑z : Cochain F G n))) 0

Tactic:
simp only [δ_smul, hz, smul_zero]

Premises used: smul_zero, CochainComplex.HomComplex.δ_smul
-- 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 ℤ
n : ℤ
⊢ Eq.{v + 1} (α := Cochain F G n) (↑0 : Cochain F G n) 0

Tactic:
rfl
-- 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 ℤ
n : ℤ
z₁ z₂ : Cocycle F G n
⊢ (↑(z₁ + z₂) : Cochain F G n) = (↑z₁ : Cochain F G n) + (↑z₂ : Cochain F G n)

Tactic:
rfl

Premises used: rfl
-- 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 ℤ
n : ℤ
z : Cocycle F G n
⊢ (↑(-z) : Cochain F G n) = -(↑z : Cochain F G n)

Tactic:
rfl

Premises used: rfl
-- 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 : CochainComplex.{v, u, 0} C ℤ
n : ℤ
z : Cocycle F G n
x : R
⊢ (↑(x • z) : Cochain F G n) = x • (↑z : Cochain F G n)

Tactic:
rfl

Premises used: rfl
-- 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 : CochainComplex.{v, u, 0} C ℤ
n : ℤ
z : Cocycle F G n
x : Rˣ
⊢ (↑(x • z) : Cochain F G n) = x • (↑z : Cochain F G n)

Tactic:
rfl

Premises used: rfl
-- 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 ℤ
n : ℤ
z₁ z₂ : Cocycle F G n
⊢ (↑(z₁ - z₂) : Cochain F G n) = (↑z₁ : Cochain F G n) - (↑z₂ : Cochain F G n)

Tactic:
rfl

Premises used: rfl
-- 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 : ℤ
x x_1 : R
x_2 : Cocycle F G n
h :
  ∀ (p q : ℤ) (hpq : p + n = q),
    (↑((x * x_1) • x_2) : Cochain F G n).v p q hpq = (↑(x • x_1 • x_2) : Cochain F G n).v p q hpq
⊢ (x * x_1) • x_2 = x • x_1 • x_2

Tactic:
ext
-- 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 : ℤ
x x_1 : R
x_2 : Cocycle F G n
p q : ℤ
hpq : p + n = q
h : (x * x_1) • (↑x_2 : Cochain F G n).v p q hpq = x • x_1 • (↑x_2 : Cochain F G n).v p q hpq
⊢ (↑((x * x_1) • x_2) : Cochain F G n).v p q hpq = (↑(x • x_1 • x_2) : Cochain F G n).v p q hpq

Tactic:
dsimp
-- 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 : ℤ
x x_1 : R
x_2 : Cocycle F G n
p q : ℤ
hpq : p + n = q
h h₁ : (x * x_1) • (↑x_2 : Cochain F G n).v p q hpq = (x * x_1) • (↑x_2 : Cochain F G n).v p q hpq
⊢ (x * x_1) • (↑x_2 : Cochain F G n).v p q hpq = x • x_1 • (↑x_2 : Cochain F G n).v p q hpq

Tactic:
rw [smul_smul]

Premises used: smul_smul
-- 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 : ℤ
x : Cocycle F G n
⊢ HSMul.hSMul.{u_1, v, v} (α := R) 1 x = x

Tactic:
aesop
-- 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 : ℤ
x : R
⊢ HSMul.hSMul (β := Cocycle F G n) x 0 = 0

Tactic:
aesop
-- 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 : ℤ
x : R
x_1 x_2 : Cocycle F G n
⊢ x • (x_1 + x_2) = x • x_1 + x • x_2

Tactic:
aesop
-- 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 : ℤ
x x_1 : R
x_2 : Cocycle F G n
h :
  ∀ (p q : ℤ) (hpq : p + n = q),
    (↑((x + x_1) • x_2) : Cochain F G n).v p q hpq = (↑(x • x_2 + x_1 • x_2) : Cochain F G n).v p q hpq
⊢ (x + x_1) • x_2 = x • x_2 + x_1 • x_2

Tactic:
ext
-- 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 : ℤ
x x_1 : R
x_2 : Cocycle F G n
p q : ℤ
hpq : p + n = q
h :
  (x + x_1) • (↑x_2 : Cochain F G n).v p q hpq =
    x • (↑x_2 : Cochain F G n).v p q hpq + x_1 • (↑x_2 : Cochain F G n).v p q hpq
⊢ (↑((x + x_1) • x_2) : Cochain F G n).v p q hpq = (↑(x • x_2 + x_1 • x_2) : Cochain F G n).v p q hpq

Tactic:
dsimp
-- 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 : ℤ
x x_1 : R
x_2 : Cocycle F G n
p q : ℤ
hpq : p + n = q
h h₁ :
  x • (↑x_2 : Cochain F G n).v p q hpq + x_1 • (↑x_2 : Cochain F G n).v p q hpq =
    x • (↑x_2 : Cochain F G n).v p q hpq + x_1 • (↑x_2 : Cochain F G n).v p q hpq
⊢ (x + x_1) • (↑x_2 : Cochain F G n).v p q hpq =
    x • (↑x_2 : Cochain F G n).v p q hpq + x_1 • (↑x_2 : Cochain F G n).v p q hpq

Tactic:
rw [add_smul]

Premises used: add_smul
-- 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 : ℤ
⊢ ∀ (x : Cocycle F G n), HSMul.hSMul.{u_1, v, v} (α := R) 0 x = 0

Tactic:
aesop
-- 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_1 : ℤ
z : Cochain F G n
m : ℤ
hnm : n + 1 = m
h : δ n m z = 0
⊢ z ∈ cocycle F G n

Tactic:
simpa only [mem_iff n m hnm z] using h

Premises used: CochainComplex.HomComplex.Cocycle.mem_iff
-- 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 ℤ
n : ℤ
z : Cocycle F G n
m : ℤ
pos : ∀ (h : n + 1 = m), δ n m (↑z : Cochain F G n) = 0
neg : ∀ (h : ¬n + 1 = m), δ n m (↑z : Cochain F G n) = 0
⊢ δ n m (↑z : Cochain F G n) = 0

Tactic:
by_cases h : n + 1 = m
-- 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 ℤ
n : ℤ
z : Cocycle F G n
m : ℤ
h : n + 1 = m
pos : (↑z : Cochain F G n) ∈ cocycle F G n
⊢ δ n m (↑z : Cochain F G n) = 0

Tactic:
rw [← mem_iff n m h]

Premises used: CochainComplex.HomComplex.Cocycle.mem_iff
-- 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 ℤ
n : ℤ
z : Cocycle F G n
m : ℤ
h : n + 1 = m
⊢ (↑z : Cochain F G n) ∈ cocycle F G n

Tactic:
z.2

Premises used: Subtype.property
-- 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 ℤ
n : ℤ
z : Cocycle F G n
m : ℤ
h : n + 1 = m
⊢ (↑z : Cochain F G n) ∈ cocycle F G n

Tactic:
exact z.2

Premises used: Subtype.property
-- 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 ℤ
n : ℤ
z : Cocycle F G n
m : ℤ
h : ¬n + 1 = m
⊢ δ n m (↑z : Cochain F G n) = 0

Tactic:
δ_shape n m h _

Premises used: CochainComplex.HomComplex.δ_shape
-- 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 ℤ
n : ℤ
z : Cocycle F G n
m : ℤ
h : ¬n + 1 = m
⊢ δ n m (↑z : Cochain F G n) = 0

Tactic:
exact δ_shape n m h _

Premises used: CochainComplex.HomComplex.δ_shape
-- 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
⊢ Eq (α := Cochain F G 1) (δ 0 1 (Cochain.ofHom φ)) 0

Tactic:
simp
-- 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 : ℤ
z : Cocycle F G 0
i : ℤ
rcases :
  ∀ (z : Cochain F G 0) (hz : Membership.mem (γ := AddSubgroup (Cochain F G 0)) (cocycle F G 0) z),
    (↑(Subtype.mk (p := fun (x : Cochain F G 0) ↦ Membership.mem (γ := AddSubgroup (Cochain F G 0)) (cocycle F G 0) x) z
                  hz) :
              Cochain F G 0).v
          i i ⋯ ≫
        G.d i (i + 1) =
      F.d i (i + 1) ≫
        (↑(Subtype.mk (p := fun (x : Cochain F G 0) ↦
                  Membership.mem (γ := AddSubgroup (Cochain F G 0)) (cocycle F G 0) x) z hz) :
              Cochain F G 0).v
          (i + 1) (i + 1) ⋯
⊢ (↑z : Cochain F G 0).v i i ⋯ ≫ G.d i (i + 1) = F.d i (i + 1) ≫ (↑z : Cochain F G 0).v (i + 1) (i + 1) ⋯

Tactic:
rcases z with ⟨z, hz⟩
-- 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 i : ℤ
z : Cochain F G 0
hz : Membership.mem (γ := AddSubgroup (Cochain F G 0)) (cocycle F G 0) z
dsimp : z.v i i ⋯ ≫ G.d i (i + 1) = F.d i (i + 1) ≫ z.v (i + 1) (i + 1) ⋯
⊢ (↑(Subtype.mk (p := fun (x : Cochain F G 0) ↦ Membership.mem (γ := AddSubgroup (Cochain F G 0)) (cocycle F G 0) x) z
                hz) :
            Cochain F G 0).v
        i i ⋯ ≫
      G.d i (i + 1) =
    F.d i (i + 1) ≫
      (↑(Subtype.mk (p := fun (x : Cochain F G 0) ↦ Membership.mem (γ := AddSubgroup (Cochain F G 0)) (cocycle F G 0) x)
                z hz) :
            Cochain F G 0).v
        (i + 1) (i + 1) ⋯

Tactic:
dsimp
-- 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 i : ℤ
z : Cochain F G 0
hz : Membership.mem (γ := AddSubgroup (Cochain F G 0)) (cocycle F G 0) z
⊢ Eq (α := Cochain F G 1) (δ 0 1 z) 0

Tactic:
rw [mem_iff 0 1 (zero_add 1)] at hz

Premises used: zero_add, OfNat.ofNat, CochainComplex.HomComplex.Cocycle.mem_iff
-- 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 i : ℤ
z : Cochain F G 0
hz : Eq (α := Cochain F G 1) (δ 0 1 z) 0
⊢ z.v i i ⋯ ≫ G.d i (i + 1) = F.d i (i + 1) ≫ z.v (i + 1) (i + 1) ⋯

Tactic:
simpa only [δ_zero_cochain_v, Cochain.zero_v, sub_eq_zero]
      using Cochain.congr_v hz i (i + 1) rfl

Premises used: sub_eq_zero, CochainComplex.HomComplex.Cochain.zero_v, CochainComplex.HomComplex.Cochain.congr_v, CochainComplex.HomComplex.δ_zero_cochain_v, HAdd.hAdd, OfNat.ofNat, rfl
-- 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 ℤ
z : Cocycle F G 0
⊢ Cochain.ofHom z.homOf = (↑z : Cochain F G 0)

Tactic:
simpa only [Cocycle.ext_iff] using ofHom_homOf_eq_self z

Premises used: CochainComplex.HomComplex.Cocycle.ofHom_homOf_eq_self, CochainComplex.HomComplex.Cocycle.ext_iff
-- 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 : ℤ
h : ∀ (p q : ℤ) (hpq : p + 2 = q), Cochain.v (δ 1 2 (Cochain.diff K)) p q hpq = Cochain.v 0 p q hpq
⊢ Eq (α := Cochain K K 2) (δ 1 2 (Cochain.diff K)) 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
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 p q : ℤ
hpq : p + 2 = q
⊢ Cochain.v (δ 1 2 (Cochain.diff K)) p q hpq = Cochain.v 0 p q hpq

Tactic:
simp only [Cochain.zero_v, δ_v 1 2 rfl _ p q hpq _ _ rfl rfl, Cochain.diff_v,
      HomologicalComplex.d_comp_d, smul_zero, add_zero]

Premises used: CochainComplex.HomComplex.δ_v, CochainComplex.HomComplex.Cochain.zero_v, smul_zero, HomologicalComplex.d_comp_d, add_zero, OfNat.ofNat, CochainComplex.HomComplex.Cochain.diff_v, rfl
-- 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 : ℤ
⊢ Eq.{v + 1} (α := Cochain K L n) (↑0 : Cochain K L n) 0

Tactic:
simp
-- 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 : ℤ
⊢ ∀ (x y : Cocycle K L n), (↑(x + y) : Cochain K L n) = (↑x : Cochain K L n) + (↑y : Cochain K L n)

Tactic:
simp
-- 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 : ℤ
hm : n + 1 = m
s : Fork ((K.HomComplex L).d n m) 0
x : (↑s.1 : Type v)
rw :
  Eq.{v + 1} (α := Cochain K L m)
    (δ n m
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) s.ι :
          (a : (↑s.pt : Type v)) → (↑((K.HomComplex L).X n) : Type v))
        x))
    0
⊢ Membership.mem (α := Cochain K L n) (cocycle K L n)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) s.ι :
          (a : (↑s.pt : Type v)) → (↑((K.HomComplex L).X n) : Type v))
        x :
      (↑((K.HomComplex L).X n) : Type v))

Tactic:
rw [mem_iff _ _ hm]

Premises used: CochainComplex.HomComplex.Cocycle.mem_iff
-- 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 : ℤ
hm : n + 1 = m
s : Fork ((K.HomComplex L).d n m) 0
x : (↑s.1 : Type v)
⊢ Eq.{v + 1} (α := Cochain K L m)
    (δ n m
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) s.ι :
          (a : (↑s.pt : Type v)) → (↑((K.HomComplex L).X n) : Type v))
        x))
    0

Tactic:
ConcreteCategory.congr_hom s.condition x

Premises used: CochainComplex.HomComplex.Cochain.mk, CategoryTheory.Limits.Fork.condition, CochainComplex.HomComplex.δ, CategoryTheory.ConcreteCategory.congr_hom, CochainComplex.HomComplex.Cochain
-- 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 : ℤ
hm : n + 1 = m
s : Fork ((K.HomComplex L).d n m) 0
x : (↑s.1 : Type v)
⊢ Eq.{v + 1} (α := Cochain K L m)
    (δ n m
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) s.ι :
          (a : (↑s.pt : Type v)) → (↑((K.HomComplex L).X n) : Type v))
        x))
    0

Tactic:
exact ConcreteCategory.congr_hom s.condition x

Premises used: CategoryTheory.Limits.Fork.condition, CategoryTheory.ConcreteCategory.congr_hom
-- 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 : ℤ
hm : n + 1 = m
s : Fork ((K.HomComplex L).d n m) 0
simp : Subtype.mk (p := fun (x : Cochain K L n) ↦ x ∈ cocycle K L n) 0 ⋯ = 0
⊢ Eq (α := Cocycle K L n)
    (Subtype.mk (p := fun (x : Cochain K L n) ↦ x ∈ cocycle K L n)
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
              AddCommGrpCat.carrier) s.ι :
            (a : (↑s.pt : Type v)) → (↑((K.HomComplex L).X n) : Type v))
          0)
        ⋯ :
      ↥(cocycle K L n))
    (0 : Cocycle K L n)

Tactic:
simp +instances only [HomComplex_X, map_zero]

Premises used: map_zero, CochainComplex.HomComplex_X
-- 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 : ℤ
hm : n + 1 = m
s : Fork ((K.HomComplex L).d n m) 0
⊢ Subtype.mk (p := fun (x : Cochain K L n) ↦ x ∈ cocycle K L n) 0 ⋯ = 0

Tactic:
rfl