awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (eval C (ComplexShape.up ℤ) n))
inst_2 : HasBinaryBiproducts.{v, u_1} C
⊢ (triangleOfDegreewiseSplit S σ).rotate.rotate.mor₂ ≫ Iso.hom (Iso.symm (mappingConeHomOfDegreewiseSplitIso S σ)) =
    Iso.hom (Iso.refl (triangleOfDegreewiseSplit S σ).rotate.rotate.obj₂) ≫
      (mappingCone.triangle (homOfDegreewiseSplit S σ)).mor₂
have dsimp : Eq (α :=
  Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) S.X₁ ⟶
    mappingCone (homOfDegreewiseSplit S σ))
  ((-CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) S.f) ≫
      Iso.inv (mappingConeHomOfDegreewiseSplitIso S σ) :
    Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) S.X₁ ⟶
      mappingCone (homOfDegreewiseSplit S σ))
  (𝟙 (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) S.X₁) ≫
      mappingCone.inr (homOfDegreewiseSplit S σ) :
    Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) S.X₁ ⟶
      mappingCone (homOfDegreewiseSplit S σ))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (eval C (ComplexShape.up ℤ) n))
inst_2 : HasBinaryBiproducts.{v, u_1} C
⊢ (triangleOfDegreewiseSplit S σ).rotate.rotate.mor₃ ≫
      CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1)
        (Iso.hom (Iso.refl (triangleOfDegreewiseSplit S σ).rotate.rotate.obj₁)) =
    Iso.hom (Iso.symm (mappingConeHomOfDegreewiseSplitIso S σ)) ≫ (mappingCone.triangle (homOfDegreewiseSplit S σ)).mor₃
have dsimp : (-CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) S.g) ≫
    CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) (𝟙 S.X₃) =
  Iso.inv (mappingConeHomOfDegreewiseSplitIso S σ) ≫ (mappingCone.triangle (homOfDegreewiseSplit S σ)).mor₃
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (eval C (ComplexShape.up ℤ) n))
inst_2 : HasBinaryBiproducts.{v, u_1} C
K L : CochainComplex.{v, u_1, 0} C ℤ
φ : K ⟶ L
⊢ (triangle φ).rotate.mor₃ ≫
      CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1)
        (Iso.hom (Iso.refl (triangle φ).rotate.obj₁)) =
    Iso.hom (Iso.refl (triangle φ).rotate.obj₃) ≫
      (triangleOfDegreewiseSplit (triangleRotateShortComplex φ) (triangleRotateShortComplexSplitting φ)).mor₃
have h : ∀ (i : ℤ),
  ((triangle φ).rotate.mor₃ ≫
          CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1)
            (Iso.hom (Iso.refl (triangle φ).rotate.obj₁))).f
      i =
    (Iso.hom (Iso.refl (triangle φ).rotate.obj₃) ≫
          (triangleOfDegreewiseSplit (triangleRotateShortComplex φ) (triangleRotateShortComplexSplitting φ)).mor₃).f
      i
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
inst_2 : HasZeroObject.{v, u_1} C
inst_3 : HasBinaryBiproducts.{v, u_1} C
T : Triangle (HomotopyCategory.{v, u_1, 0} C (ComplexShape.up ℤ))
⊢ Membership.mem (γ := Set (Triangle (HomotopyCategory.{v, u_1, 0} C (ComplexShape.up ℤ))))
      (@distinguishedTriangles _ _ ⋯ _ (instPreadditive C (ComplexShape.up ℤ)) ⋯ _) T ↔
    ∃ (S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)) (σ :
      (n : ℤ) → ShortComplex.Splitting (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n))),
      Nonempty.{v + 1} (T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ)
have mp : Membership.mem (γ := Set (Triangle (HomotopyCategory.{v, u_1, 0} C (ComplexShape.up ℤ))))
    (@distinguishedTriangles _ _ sorry _ (instPreadditive C (ComplexShape.up ℤ)) sorry _) T →
  ∃ (S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)) (σ :
    (n : ℤ) → ShortComplex.Splitting (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n))),
    Nonempty.{v + 1} (T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
inst_2 : HasZeroObject.{v, u_1} C
inst_3 : HasBinaryBiproducts.{v, u_1} C
T : Triangle (HomotopyCategory.{v, u_1, 0} C (ComplexShape.up ℤ))
mp :
  Membership.mem (γ := Set (Triangle (HomotopyCategory.{v, u_1, 0} C (ComplexShape.up ℤ))))
      (@distinguishedTriangles _ _ ⋯ _ (instPreadditive C (ComplexShape.up ℤ)) ⋯ _) T →
    ∃ (S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)) (σ :
      (n : ℤ) → ShortComplex.Splitting (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n))),
      Nonempty.{v + 1} (T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ)
⊢ Membership.mem (γ := Set (Triangle (HomotopyCategory.{v, u_1, 0} C (ComplexShape.up ℤ))))
      (@distinguishedTriangles _ _ ⋯ _ (instPreadditive C (ComplexShape.up ℤ)) ⋯ _) T ↔
    ∃ (S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)) (σ :
      (n : ℤ) → ShortComplex.Splitting (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n))),
      Nonempty.{v + 1} (T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ)
have mpr : (∃ (S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)) (σ :
    (n : ℤ) → ShortComplex.Splitting (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n))),
    Nonempty.{v + 1} (T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ)) →
  Membership.mem (γ := Set (Triangle (HomotopyCategory.{v, u_1, 0} C (ComplexShape.up ℤ))))
    (@distinguishedTriangles _ _ sorry _ (instPreadditive C (ComplexShape.up ℤ)) sorry _) T
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
inst_2 : HasZeroObject.{v, u_1} C
inst_3 : HasBinaryBiproducts.{v, u_1} C
T : Triangle (HomotopyCategory.{v, u_1, 0} C (ComplexShape.up ℤ))
hT :
  Membership.mem (γ := Set (Triangle (HomotopyCategory.{v, u_1, 0} C (ComplexShape.up ℤ))))
    (@distinguishedTriangles _ _ ⋯ _ (instPreadditive C (ComplexShape.up ℤ)) ⋯ _) T
⊢ ∃ (S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)) (σ :
    (n : ℤ) → ShortComplex.Splitting (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n))),
    Nonempty.{v + 1} (T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ)
have mp : ∀ (K L : CochainComplex.{v, u_1, 0} C ℤ) (φ : K ⟶ L) (e : T.invRotate ≅ CochainComplex.mappingCone.triangleh φ),
  ∃ (S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)) (σ :
    (n : ℤ) → ShortComplex.Splitting (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n))),
    Nonempty.{v + 1} (T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ)
Tactic: obtain ⟨K, L, φ, ⟨e⟩⟩ := inv_rot_of_distTriang _ hT
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
inst_2 : HasZeroObject.{v, u_1} C
inst_3 : HasBinaryBiproducts.{v, u_1} C
T : Triangle (HomotopyCategory.{v, u_1, 0} C (ComplexShape.up ℤ))
S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n))
e : T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ
⊢ Membership.mem (γ := Set (Triangle (HomotopyCategory.{v, u_1, 0} C (ComplexShape.up ℤ))))
    (@distinguishedTriangles _ _ ⋯ _ (instPreadditive C (ComplexShape.up ℤ)) ⋯ _) T
have mpr : Membership.mem (γ := Set (Triangle (HomotopyCategory.{v, u_1, 0} C (ComplexShape.up ℤ))))
  (@distinguishedTriangles _ _ sorry _ (instPreadditive C (ComplexShape.up ℤ)) sorry _) T.rotate.rotate
Tactic: rw [rotate_distinguished_triangle, rotate_distinguished_triangle]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
inst_2 : HasZeroObject.{v, u_1} C
inst_3 : HasBinaryBiproducts.{v, u_1} C
T : Triangle (HomotopyCategory.{v, u_1, 0} C (ComplexShape.up ℤ))
S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n))
e : T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ
⊢ Membership.mem (γ := Set (Triangle (HomotopyCategory.{v, u_1, 0} C (ComplexShape.up ℤ))))
    (@distinguishedTriangles _ _ ⋯ _ (instPreadditive C (ComplexShape.up ℤ)) ⋯ _) T.rotate.rotate
have mpr : Membership.mem (γ := Set (Triangle (HomotopyCategory.{v, u_1, 0} C (ComplexShape.up ℤ))))
  (@distinguishedTriangles _ _ sorry _ (instPreadditive C (ComplexShape.up ℤ)) sorry _)
  (CochainComplex.mappingCone.triangleh (CochainComplex.homOfDegreewiseSplit S σ))
Tactic: refine isomorphic_distinguished _ ?_ _
      ((rotate _ ⋙ rotate _).mapIso e ≪≫
        CochainComplex.trianglehOfDegreewiseSplitRotateRotateIso S σ)
-- 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₁ z₂ : Cochain F G n
h : z₁ = z₂
p q : ℤ
hpq : p + n = q
⊢ z₁.v p q hpq = z₂.v p q hpq
have subst : z₁.v p q hpq = z₁.v p q hpq
Tactic: subst h
Cleared hypotheses: z₂, 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
F G : CochainComplex.{v, u, 0} C ℤ
n : ℤ
z₁ z₂ : Cochain F G n
h : ∀ (p q : ℤ) (hpq : p + n = q), z₁.v p q hpq = z₂.v p q hpq
⊢ z₁ = z₂
have h₁ : ∀ (p q : ℤ) (hpq : p + n = q),
  Eq.{v + 1} (α := F.X { p := p, q := q, hpq := hpq : Triplet n }.p ⟶ G.X { p := p, q := q, hpq := hpq : Triplet n }.q)
    (z₁ { p := p, q := q, hpq := hpq }) (z₂ { p := p, q := q, hpq := hpq })
Tactic: funext ⟨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
F G : CochainComplex.{v, u, 0} C ℤ
z₁ z₂ : Cochain F G 0
h : ∀ (p : ℤ), z₁.v p p ⋯ = z₂.v p p ⋯
⊢ z₁ = z₂
have h₁ : ∀ (p q : ℤ) (hpq : p + 0 = q), z₁.v p q hpq = z₂.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 : ℤ
ψ : (p : ℤ) → F.X p ⟶ G.X p
p q : ℤ
hpq : p + 0 = q
⊢ G.X p = G.X q
have rw : G.X p = G.X (p + 0)
Tactic: rw [← hpq, add_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 : ℤ
ψ : (p : ℤ) → F.X p ⟶ G.X p
p q : ℤ
hpq : p + 0 = q
rw : G.X p = G.X (p + 0)
⊢ G.X p = G.X q
have rw₁ : G.X p = G.X p
Tactic: rw [← hpq, add_zero]
-- 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
F G : CochainComplex.{v, u, 0} C ℤ
ψ : (p : ℤ) → F.X p ⟶ G.X p
p q q' : ℤ
hpq : p + 0 = q
⊢ (ofHoms ψ).v p q hpq ≫ G.d q q' = ψ p ≫ G.d p q'
have hpq₁ : p = q
Tactic: rw [add_zero] at 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
F G : CochainComplex.{v, u, 0} C ℤ
ψ : (p : ℤ) → F.X p ⟶ G.X p
p q q' : ℤ
hpq_1 : p + 0 = q
hpq : p = q
⊢ (ofHoms ψ).v p q hpq_1 ≫ G.d q q' = ψ p ≫ G.d p q'
have subst : ∀ (hpq : p + 0 = p), (ofHoms ψ).v p p hpq ≫ G.d p q' = ψ p ≫ G.d p q'
Tactic: subst hpq
Cleared hypotheses: q, hpq_1, 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
F G : CochainComplex.{v, u, 0} C ℤ
ψ : (p : ℤ) → F.X p ⟶ G.X p
p q' : ℤ
hpq : p + 0 = p
⊢ (ofHoms ψ).v p p hpq ≫ G.d p q' = ψ p ≫ G.d p q'
have rw : ψ p ≫ G.d p q' = ψ p ≫ G.d p q'
Tactic: rw [ofHoms_v]
-- 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
F G : CochainComplex.{v, u, 0} C ℤ
ψ : (p : ℤ) → F.X p ⟶ G.X p
p' p q : ℤ
hpq : p + 0 = q
⊢ F.d p' p ≫ (ofHoms ψ).v p q hpq = F.d p' q ≫ ψ q
have hpq₁ : p = q
Tactic: rw [add_zero] at 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
F G : CochainComplex.{v, u, 0} C ℤ
ψ : (p : ℤ) → F.X p ⟶ G.X p
p' p q : ℤ
hpq_1 : p + 0 = q
hpq : p = q
⊢ F.d p' p ≫ (ofHoms ψ).v p q hpq_1 = F.d p' q ≫ ψ q
have subst : ∀ (hpq : p + 0 = p), F.d p' p ≫ (ofHoms ψ).v p p hpq = F.d p' p ≫ ψ p
Tactic: subst hpq
Cleared hypotheses: q, hpq_1, 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
F G : CochainComplex.{v, u, 0} C ℤ
ψ : (p : ℤ) → F.X p ⟶ G.X p
p' p : ℤ
hpq : p + 0 = p
⊢ F.d p' p ≫ (ofHoms ψ).v p p hpq = F.d p' p ≫ ψ p
have rw : F.d p' p ≫ ψ p = F.d p' p ≫ ψ p
Tactic: rw [ofHoms_v]
-- 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 : ℤ
γ : Cochain F G n
p q q' : ℤ
hpq : p + n = q
hq' : q = q'
rw : p + n = q
⊢ p + n = q'
have rw₁ : q = q
Tactic: rw [← hq', 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
F G : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain F G n
p q q' : ℤ
hpq : p + n = q
hq' : q = q'
⊢ γ.v p q hpq ≫ (HomologicalComplex.XIsoOfEq G hq').hom = γ.v p q' ⋯
have subst : γ.v p q hpq ≫ (HomologicalComplex.XIsoOfEq G sorry).hom = γ.v p q sorry
Tactic: subst hq'
Cleared hypotheses: q', hq'
-- 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 : ℤ
γ : Cochain F G n
p q q' : ℤ
hpq : p + n = q
hq' : q' = q
rw : p + n = q
⊢ p + n = q'
have rw₁ : q = q
Tactic: rw [hq', 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
F G : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain F G n
p q q' : ℤ
hpq : p + n = q
hq' : q' = q
⊢ γ.v p q hpq ≫ (HomologicalComplex.XIsoOfEq G hq').inv = γ.v p q' ⋯
have subst : ∀ (hpq : p + n = q'), γ.v p q' hpq ≫ (HomologicalComplex.XIsoOfEq G sorry).inv = γ.v p q' sorry
Tactic: subst hq'
Cleared hypotheses: q, hpq, hq'
-- 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 n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
p₁ p₂ p₃ : ℤ
h₁ : p₁ + n₁ = p₂
h₂ : p₂ + n₂ = p₃
⊢ p₁ + n₁₂ = p₃
have rw : p₁ + n₁₂ = p₂ + n₂
Tactic: rw [← h₂, ← h₁, ← h, add_assoc]
-- 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 n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
p₁ p₂ p₃ : ℤ
h₁ : p₁ + n₁ = p₂
h₂ : p₂ + n₂ = p₃
rw : p₁ + n₁₂ = p₂ + n₂
⊢ p₁ + n₁₂ = p₃
have rw₁ : p₁ + n₁₂ = p₁ + n₁ + n₂
Tactic: rw [← h₂, ← h₁, ← h, add_assoc]
-- 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 n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
p₁ p₂ p₃ : ℤ
h₁ : p₁ + n₁ = p₂
h₂ : p₂ + n₂ = p₃
rw : p₁ + n₁₂ = p₂ + n₂
rw₁ : p₁ + n₁₂ = p₁ + n₁ + n₂
⊢ p₁ + n₁₂ = p₃
have rw₂ : p₁ + (n₁ + n₂) = p₁ + n₁ + n₂
Tactic: rw [← h₂, ← h₁, ← h, add_assoc]
-- 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 n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
p₁ p₂ p₃ : ℤ
h₁ : p₁ + n₁ = p₂
h₂ : p₂ + n₂ = p₃
rw : p₁ + n₁₂ = p₂ + n₂
rw₁ : p₁ + n₁₂ = p₁ + n₁ + n₂
rw₂ : p₁ + (n₁ + n₂) = p₁ + n₁ + n₂
⊢ p₁ + n₁₂ = p₃
have rw₃ : p₁ + (n₁ + n₂) = p₁ + (n₁ + n₂)
Tactic: rw [← h₂, ← h₁, ← h, add_assoc]
-- 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₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
p₁ p₂ p₃ : ℤ
h₁ : p₁ + n₁ = p₂
h₂ : p₂ + n₂ = p₃
⊢ (z₁.comp z₂ h).v p₁ p₃ ⋯ = z₁.v p₁ p₂ h₁ ≫ z₂.v p₂ p₃ h₂
have subst : ∀ (h₂ : p₁ + n₁ + n₂ = p₃), (z₁.comp z₂ h).v p₁ p₃ sorry = z₁.v p₁ (p₁ + n₁) sorry ≫ z₂.v (p₁ + n₁) p₃ h₂
Tactic: subst h₁
Cleared hypotheses: p₂, h₁, 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 n₁ n₂ n₃ n₁₂ n₂₃ n₁₂₃ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
z₃ : Cochain K L n₃
h₁₂ : n₁ + n₂ = n₁₂
h₂₃ : n₂ + n₃ = n₂₃
h₁₂₃ rw : n₁ + n₂ + n₃ = n₁₂₃
⊢ n₁₂ + n₃ = n₁₂₃
have rw₁ : n₁₂₃ = n₁₂₃
Tactic: rw [← h₁₂, 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 n₁ n₂ n₃ n₁₂ n₂₃ n₁₂₃ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
z₃ : Cochain K L n₃
h₁₂ : n₁ + n₂ = n₁₂
h₂₃ : n₂ + n₃ = n₂₃
h₁₂₃ : n₁ + n₂ + n₃ = n₁₂₃
⊢ n₁ + n₂₃ = n₁₂₃
have rw : n₁ + (n₂ + n₃) = n₁₂₃
Tactic: rw [← h₂₃, ← h₁₂₃, add_assoc]
-- 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 n₁ n₂ n₃ n₁₂ n₂₃ n₁₂₃ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
z₃ : Cochain K L n₃
h₁₂ : n₁ + n₂ = n₁₂
h₂₃ : n₂ + n₃ = n₂₃
h₁₂₃ : n₁ + n₂ + n₃ = n₁₂₃
rw : n₁ + (n₂ + n₃) = n₁₂₃
⊢ n₁ + n₂₃ = n₁₂₃
have rw₁ : n₁ + (n₂ + n₃) = n₁ + n₂ + n₃
Tactic: rw [← h₂₃, ← h₁₂₃, add_assoc]
-- 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 n₁ n₂ n₃ n₁₂ n₂₃ n₁₂₃ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
z₃ : Cochain K L n₃
h₁₂ : n₁ + n₂ = n₁₂
h₂₃ : n₂ + n₃ = n₂₃
h₁₂₃ : n₁ + n₂ + n₃ = n₁₂₃
rw : n₁ + (n₂ + n₃) = n₁₂₃
rw₁ : n₁ + (n₂ + n₃) = n₁ + n₂ + n₃
⊢ n₁ + n₂₃ = n₁₂₃
have rw₂ : n₁ + (n₂ + n₃) = n₁ + (n₂ + n₃)
Tactic: rw [← h₂₃, ← h₁₂₃, add_assoc]
-- 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 L : CochainComplex.{v, u, 0} C ℤ
n₁ n₂ n₃ n₁₂ n₂₃ n₁₂₃ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
z₃ : Cochain K L n₃
h₁₂ : n₁ + n₂ = n₁₂
h₂₃ : n₂ + n₃ = n₂₃
h₁₂₃ : n₁ + n₂ + n₃ = n₁₂₃
⊢ (z₁.comp z₂ h₁₂).comp z₃ ⋯ = z₁.comp (z₂.comp z₃ h₂₃) ⋯
have substs : (z₁.comp z₂ sorry).comp z₃ sorry = z₁.comp (z₂.comp z₃ sorry) sorry
Tactic: substs h₁₂ h₂₃ h₁₂₃
Cleared hypotheses: n₁₂, n₂₃, n₁₂₃, h₁₂, h₂₃, 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
F G K L : CochainComplex.{v, u, 0} C ℤ
n₁ n₂ n₃ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
z₃ : Cochain K L n₃
⊢ (z₁.comp z₂ ⋯).comp z₃ ⋯ = z₁.comp (z₂.comp z₃ ⋯) ⋯
have h : ∀ (p q : ℤ) (hpq : p + (n₁ + n₂ + n₃) = q), v ((z₁.comp z₂ sorry).comp z₃ sorry) p q hpq = (z₁.comp (z₂.comp z₃ sorry) sorry).v 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
F G K L : CochainComplex.{v, u, 0} C ℤ
n₁ n₂ n₃ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
z₃ : Cochain K L n₃
p q : ℤ
hpq : p + (n₁ + n₂ + n₃) = q
⊢ v ((z₁.comp z₂ ⋯).comp z₃ ⋯) p q hpq = (z₁.comp (z₂.comp z₃ ⋯) ⋯).v p q hpq
have h : (z₁.comp z₂ sorry).v p (p + n₁ + n₂) sorry ≫ z₃.v (p + n₁ + n₂) q sorry = (z₁.comp (z₂.comp z₃ sorry) sorry).v p q hpq
Tactic: rw [comp_v _ _ rfl p (p + n₁ + n₂) q (add_assoc _ _ _).symm (by lia),
    comp_v z₁ z₂ rfl p (p + n₁) (p + n₁ + n₂) (by lia) (by lia),
    comp_v z₁ (z₂.comp z₃ rfl) (add_assoc n₁ n₂ n₃).symm p (p + n₁) q (by lia) (by lia),
    comp_v z₂ z₃ rfl (p + n₁) (p + n₁ + n₂) q (by lia) (by lia), assoc]
-- 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 L : CochainComplex.{v, u, 0} C ℤ
n₁ n₂ n₃ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
z₃ : Cochain K L n₃
p q : ℤ
hpq : p + (n₁ + n₂ + n₃) = q
h : (z₁.comp z₂ ⋯).v p (p + n₁ + n₂) ⋯ ≫ z₃.v (p + n₁ + n₂) q ⋯ = (z₁.comp (z₂.comp z₃ ⋯) ⋯).v p q hpq
⊢ v ((z₁.comp z₂ ⋯).comp z₃ ⋯) p q hpq = (z₁.comp (z₂.comp z₃ ⋯) ⋯).v p q hpq
have h₁ : (z₁.v p (p + n₁) sorry ≫ z₂.v (p + n₁) (p + n₁ + n₂) sorry) ≫ z₃.v (p + n₁ + n₂) q sorry = (z₁.comp (z₂.comp z₃ sorry) sorry).v p q hpq
Tactic: rw [comp_v _ _ rfl p (p + n₁ + n₂) q (add_assoc _ _ _).symm (by lia),
    comp_v z₁ z₂ rfl p (p + n₁) (p + n₁ + n₂) (by lia) (by lia),
    comp_v z₁ (z₂.comp z₃ rfl) (add_assoc n₁ n₂ n₃).symm p (p + n₁) q (by lia) (by lia),
    comp_v z₂ z₃ rfl (p + n₁) (p + n₁ + n₂) q (by lia) (by lia), assoc]
-- 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 L : CochainComplex.{v, u, 0} C ℤ
n₁ n₂ n₃ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
z₃ : Cochain K L n₃
p q : ℤ
hpq : p + (n₁ + n₂ + n₃) = q
h : (z₁.comp z₂ ⋯).v p (p + n₁ + n₂) ⋯ ≫ z₃.v (p + n₁ + n₂) q ⋯ = (z₁.comp (z₂.comp z₃ ⋯) ⋯).v p q hpq
h₁ : (z₁.v p (p + n₁) ⋯ ≫ z₂.v (p + n₁) (p + n₁ + n₂) ⋯) ≫ z₃.v (p + n₁ + n₂) q ⋯ = (z₁.comp (z₂.comp z₃ ⋯) ⋯).v p q hpq
⊢ v ((z₁.comp z₂ ⋯).comp z₃ ⋯) p q hpq = (z₁.comp (z₂.comp z₃ ⋯) ⋯).v p q hpq
have h₂ : (z₁.v p (p + n₁) sorry ≫ z₂.v (p + n₁) (p + n₁ + n₂) sorry) ≫ z₃.v (p + n₁ + n₂) q sorry =
  z₁.v p (p + n₁) sorry ≫ (z₂.comp z₃ sorry).v (p + n₁) q sorry
Tactic: rw [comp_v _ _ rfl p (p + n₁ + n₂) q (add_assoc _ _ _).symm (by lia),
    comp_v z₁ z₂ rfl p (p + n₁) (p + n₁ + n₂) (by lia) (by lia),
    comp_v z₁ (z₂.comp z₃ rfl) (add_assoc n₁ n₂ n₃).symm p (p + n₁) q (by lia) (by lia),
    comp_v z₂ z₃ rfl (p + n₁) (p + n₁ + n₂) q (by lia) (by lia), assoc]