awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
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
⊢ Eq (α := AddCommGrpCat.of (Cochain F G x) ⟶ AddCommGrpCat.of (Cochain F G x_2))
    (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)))
    0
have hf : ∀ (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: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
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
⊢ z ∈ cocycle F G n ↔ δ n m z = 0
have subst : z ∈ cocycle F G n ↔ Eq (α := Cochain F G (n + 1)) (δ n (n + 1) z) 0
Tactic: subst hnm
Cleared hypotheses: m, hnm
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (hypothesis)
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
⊢ r • (↑z : Cochain F G n) ∈ cocycle F G n
have hz : (↑z : Cochain F G n) ∈ cocycle F G n
Tactic: have hz := z.2
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
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
⊢ r • (↑z : Cochain F G n) ∈ cocycle F G n
have 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
Tactic: rw [mem_iff n (n + 1) rfl] at hz ⊢
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
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
⊢ (x * x_1) • x_2 = x • x_1 • x_2
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
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
⊢ (↑((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
have 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
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
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
⊢ (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
have 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
Tactic: rw [smul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
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
⊢ (x + x_1) • x_2 = x • x_2 + x_1 • x_2
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
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
⊢ (↑((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
have 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
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
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
⊢ (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
have 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
Tactic: rw [add_smul]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
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 : ℤ
⊢ δ n m (↑z : Cochain F G n) = 0
have pos : ∀ (h : n + 1 = m), δ n m (↑z : Cochain F G n) = 0
Tactic: by_cases h : n + 1 = m
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
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
⊢ δ n m (↑z : Cochain F G n) = 0
have neg : ∀ (h : ¬n + 1 = m), δ n m (↑z : Cochain F G n) = 0
Tactic: by_cases h : n + 1 = m
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
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
have pos : (↑z : Cochain F G n) ∈ cocycle F G n
Tactic: rw [← mem_iff n m h]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
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 : ℤ
⊢ (↑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) ⋯
have 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 sorry ≫
      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) sorry
Tactic: rcases z with ⟨z, hz⟩
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
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
⊢ (↑(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) ⋯
have dsimp : z.v i i sorry ≫ G.d i (i + 1) = F.d i (i + 1) ≫ z.v (i + 1) (i + 1) sorry
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (hypothesis)
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
⊢ z.v i i ⋯ ≫ G.d i (i + 1) = F.d i (i + 1) ≫ z.v (i + 1) (i + 1) ⋯
have hz₁ : Eq (α := Cochain F G 1) (δ 0 1 z) 0
Tactic: rw [mem_iff 0 1 (zero_add 1)] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
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 (α := Cochain K K 2) (δ 1 2 (Cochain.diff K)) 0
have h : ∀ (p q : ℤ) (hpq : p + 2 = q), Cochain.v (δ 1 2 (Cochain.diff K)) p q hpq = Cochain.v 0 p q hpq
Tactic: ext p q hpq
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
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)
⊢ 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))
have 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
Tactic: rw [mem_iff _ _ hm]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
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
⊢ 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)
have simp : Subtype.mk (p := fun (x : Cochain K L n) ↦ x ∈ cocycle K L n) 0 sorry = 0
Tactic: simp +instances only [HomComplex_X, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
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 x_1 : (↑s.1 : Type v)
⊢ 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))
        (x + x_1))
      ⋯ =
    HAdd.hAdd (α := Cocycle K L n) (β := 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))
            x)
          ⋯ :
        ↥(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))
            x_1)
          ⋯ :
        ↥(cocycle K L n))
have simp : Subtype.mk (p := fun (x : Cochain K L n) ↦ x ∈ cocycle K L n)
    (HAdd.hAdd (α := Cochain K L n) (β := Cochain 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)) → Cochain K L n)
          x :
        Cochain 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)) → Cochain K L n)
          x_1 :
        Cochain K L n))
    sorry =
  HAdd.hAdd (α := Cocycle K L n) (β := 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)) → Cochain K L n)
          x)
        sorry :
      ↥(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)) → Cochain K L n)
          x_1)
        sorry :
      ↥(cocycle K L n))
Tactic: simp +instances only [HomComplex_X, map_add]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
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
l : s.pt ⟶ (KernelFork.ofι (AddCommGrpCat.ofHom (toCochainAddMonoidHom K L n)) ⋯).pt
hl : l ≫ Fork.ι (KernelFork.ofι (AddCommGrpCat.ofHom (toCochainAddMonoidHom K L n)) ⋯) = s.ι
⊢ l =
    (fun (s : Fork ((K.HomComplex L).d n m) 0) ↦
        (AddCommGrpCat.ofHom
            {
              toFun := fun (x : (↑s.1 : Type v)) ↦
                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))
                    x)
                  ⋯,
              map_zero' := ⋯, map_add' := ⋯ } :
          AddCommGrpCat.of (↑s.1 : Type v) ⟶ AddCommGrpCat.of (Cocycle K L n)))
      s
have hf : ∀ (x : (↑s.pt : Type v)),
  Eq (α := (↑(KernelFork.ofι (AddCommGrpCat.ofHom (toCochainAddMonoidHom K L n)) sorry).pt : Type v))
    ((AddCommGrpCat.Hom.hom l :
          (a : (↑s.pt : Type v)) →
            (↑(KernelFork.ofι (AddCommGrpCat.ofHom (toCochainAddMonoidHom K L n)) sorry).pt : Type v))
        x :
      (↑(KernelFork.ofι (AddCommGrpCat.ofHom (toCochainAddMonoidHom K L n)) sorry).pt : Type v))
    ((AddCommGrpCat.Hom.hom
            ((fun (s : Fork ((K.HomComplex L).d n m) 0) ↦
                (AddCommGrpCat.ofHom
                    {
                      toFun := fun (x : (↑s.1 : Type v)) ↦
                        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))
                            x)
                          sorry,
                      map_zero' := sorry, map_add' := sorry } :
                  AddCommGrpCat.of (↑s.1 : Type v) ⟶ AddCommGrpCat.of (Cocycle K L n)))
              s) :
          (a : (↑s.pt : Type v)) →
            (↑(KernelFork.ofι (AddCommGrpCat.ofHom (toCochainAddMonoidHom K L n)) sorry).pt : Type v))
        x :
      (↑(KernelFork.ofι (AddCommGrpCat.ofHom (toCochainAddMonoidHom K L n)) sorry).pt : Type v))
Tactic: ext : 3
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
F G K : CochainComplex.{v, u, 0} C ℤ
n : ℤ
z₁ : Cochain F G n
z₂ : Cocycle G K 0
m : ℤ
⊢ δ n m (z₁.comp (↑z₂ : Cochain G K 0) ⋯) = (δ n m z₁).comp (↑z₂ : Cochain G K 0) ⋯
have pos : ∀ (hnm : n + 1 = m), δ n m (z₁.comp (↑z₂ : Cochain G K 0) sorry) = (δ n m z₁).comp (↑z₂ : Cochain G K 0) sorry
Tactic: by_cases hnm : n + 1 = m
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
F G K : CochainComplex.{v, u, 0} C ℤ
n : ℤ
z₁ : Cochain F G n
z₂ : Cocycle G K 0
m : ℤ
pos : ∀ (hnm : n + 1 = m), δ n m (z₁.comp (↑z₂ : Cochain G K 0) ⋯) = (δ n m z₁).comp (↑z₂ : Cochain G K 0) ⋯
⊢ δ n m (z₁.comp (↑z₂ : Cochain G K 0) ⋯) = (δ n m z₁).comp (↑z₂ : Cochain G K 0) ⋯
have neg : ∀ (hnm : ¬n + 1 = m), δ n m (z₁.comp (↑z₂ : Cochain G K 0) sorry) = (δ n m z₁).comp (↑z₂ : Cochain G K 0) sorry
Tactic: by_cases hnm : n + 1 = m
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
F G K : CochainComplex.{v, u, 0} C ℤ
n : ℤ
z₁ : Cochain F G n
f : G ⟶ K
m : ℤ
⊢ δ n m (z₁.comp (Cochain.ofHom f) ⋯) = (δ n m z₁).comp (Cochain.ofHom f) ⋯
have rw : δ n m (z₁.comp (↑(Cocycle.ofHom f) : Cochain G K 0) sorry) = (δ n m z₁).comp (↑(Cocycle.ofHom f) : Cochain G K 0) sorry
Tactic: rw [← Cocycle.ofHom_coe, δ_comp_zero_cocycle]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
F G K : CochainComplex.{v, u, 0} C ℤ
n : ℤ
z₁ : Cochain F G n
f : G ⟶ K
m : ℤ
rw : δ n m (z₁.comp (↑(Cocycle.ofHom f) : Cochain G K 0) ⋯) = (δ n m z₁).comp (↑(Cocycle.ofHom f) : Cochain G K 0) ⋯
⊢ δ n m (z₁.comp (Cochain.ofHom f) ⋯) = (δ n m z₁).comp (Cochain.ofHom f) ⋯
have rw₁ : (δ n m z₁).comp (↑(Cocycle.ofHom f) : Cochain G K 0) sorry = (δ n m z₁).comp (↑(Cocycle.ofHom f) : Cochain G K 0) sorry
Tactic: rw [← Cocycle.ofHom_coe, δ_comp_zero_cocycle]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
F G K : CochainComplex.{v, u, 0} C ℤ
n : ℤ
z₁ : Cocycle F G 0
z₂ : Cochain G K n
m : ℤ
⊢ δ n m ((↑z₁ : Cochain F G 0).comp z₂ ⋯) = (↑z₁ : Cochain F G 0).comp (δ n m z₂) ⋯
have pos : ∀ (hnm : n + 1 = m), δ n m ((↑z₁ : Cochain F G 0).comp z₂ sorry) = (↑z₁ : Cochain F G 0).comp (δ n m z₂) sorry
Tactic: by_cases hnm : n + 1 = m
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
F G K : CochainComplex.{v, u, 0} C ℤ
n : ℤ
z₁ : Cocycle F G 0
z₂ : Cochain G K n
m : ℤ
pos : ∀ (hnm : n + 1 = m), δ n m ((↑z₁ : Cochain F G 0).comp z₂ ⋯) = (↑z₁ : Cochain F G 0).comp (δ n m z₂) ⋯
⊢ δ n m ((↑z₁ : Cochain F G 0).comp z₂ ⋯) = (↑z₁ : Cochain F G 0).comp (δ n m z₂) ⋯
have neg : ∀ (hnm : ¬n + 1 = m), δ n m ((↑z₁ : Cochain F G 0).comp z₂ sorry) = (↑z₁ : Cochain F G 0).comp (δ n m z₂) sorry
Tactic: by_cases hnm : n + 1 = m
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
F G K : CochainComplex.{v, u, 0} C ℤ
n : ℤ
f : F ⟶ G
z : Cochain G K n
m : ℤ
⊢ δ n m ((Cochain.ofHom f).comp z ⋯) = (Cochain.ofHom f).comp (δ n m z) ⋯
have rw : δ n m ((↑(Cocycle.ofHom f) : Cochain F G 0).comp z sorry) = (↑(Cocycle.ofHom f) : Cochain F G 0).comp (δ n m z) sorry
Tactic: rw [← Cocycle.ofHom_coe, δ_zero_cocycle_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
F G K : CochainComplex.{v, u, 0} C ℤ
n : ℤ
f : F ⟶ G
z : Cochain G K n
m : ℤ
rw : δ n m ((↑(Cocycle.ofHom f) : Cochain F G 0).comp z ⋯) = (↑(Cocycle.ofHom f) : Cochain F G 0).comp (δ n m z) ⋯
⊢ δ n m ((Cochain.ofHom f).comp z ⋯) = (Cochain.ofHom f).comp (δ n m z) ⋯
have rw₁ : (↑(Cocycle.ofHom f) : Cochain F G 0).comp (δ n m z) sorry = (↑(Cocycle.ofHom f) : Cochain F G 0).comp (δ n m z) sorry
Tactic: rw [← Cocycle.ofHom_coe, δ_zero_cocycle_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (hypothesis)
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 : ℤ
⊢ φ₁.f p =
    HAdd.hAdd (α := F.X p ⟶ G.X p) (β := F.X p ⟶ G.X p)
        ((dNext p : (a : (i j : ℤ) → F.X i ⟶ G.X j) → F.X p ⟶ G.X p) fun (i j : ℤ) ↦
            if hij : i + -1 = j then (↑z : Cochain F G (-1)).v i j hij else 0 :
          F.X p ⟶ G.X p)
        ((prevD p : (a : (i j : ℤ) → F.X i ⟶ G.X j) → F.X p ⟶ G.X p) fun (i j : ℤ) ↦
            if hij : i + -1 = j then (↑z : Cochain F G (-1)).v i j hij else 0 :
          F.X p ⟶ G.X p) +
      φ₂.f p
have eq : (ofHom φ₁).v p p sorry = (δ (-1) 0 (↑z : Cochain F G (-1)) + ofHom φ₂).v p p sorry
Tactic: have eq := Cochain.congr_v z.2 p p (add_zero p)
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (hypothesis)
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 : ℤ
eq : (ofHom φ₁).v p p ⋯ = (δ (-1) 0 (↑z : Cochain F G (-1)) + ofHom φ₂).v p p ⋯
⊢ φ₁.f p =
    HAdd.hAdd (α := F.X p ⟶ G.X p) (β := F.X p ⟶ G.X p)
        ((dNext p : (a : (i j : ℤ) → F.X i ⟶ G.X j) → F.X p ⟶ G.X p) fun (i j : ℤ) ↦
            if hij : i + -1 = j then (↑z : Cochain F G (-1)).v i j hij else 0 :
          F.X p ⟶ G.X p)
        ((prevD p : (a : (i j : ℤ) → F.X i ⟶ G.X j) → F.X p ⟶ G.X p) fun (i j : ℤ) ↦
            if hij : i + -1 = j then (↑z : Cochain F G (-1)).v i j hij else 0 :
          F.X p ⟶ G.X p) +
      φ₂.f p
have h₁ : (ComplexShape.up ℤ).Rel (p - 1) p
Tactic: have h₁ : (ComplexShape.up ℤ).Rel (p - 1) p := by simp