awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
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
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
⊢ (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₃

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
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
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:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
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 σ)
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 _ _ ⋯ _ (instPreadditive C (ComplexShape.up ℤ)) ⋯ _) T
⊢ 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 σ)

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
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
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 σ)
⊢ ∃ (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

Premises used: CategoryTheory.Pretriangulated.inv_rot_of_distTriang
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
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
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:
⟨_, _, ⟨(triangleRotation _).counitIso.symm.app _ ≪≫ (rotate _).mapIso e ≪≫
      CochainComplex.mappingCone.trianglehRotateIsoTrianglehOfDegreewiseSplit φ⟩⟩

Premises used: CategoryTheory.Pretriangulated.triangleRotation, Nonempty.intro, CategoryTheory.Iso.trans, Exists.intro, CategoryTheory.Iso.symm, CategoryTheory.Pretriangulated.rotate, CochainComplex.mappingCone.trianglehRotateIsoTrianglehOfDegreewiseSplit, CategoryTheory.Iso.app, CategoryTheory.Functor.mapIso, CategoryTheory.Equivalence.counitIso
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
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
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:
exact ⟨_, _, ⟨(triangleRotation _).counitIso.symm.app _ ≪≫ (rotate _).mapIso e ≪≫
      CochainComplex.mappingCone.trianglehRotateIsoTrianglehOfDegreewiseSplit φ⟩⟩
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
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 σ
mpr :
  Membership.mem (γ := Set (Triangle (HomotopyCategory.{v, u_1, 0} C (ComplexShape.up ℤ))))
    (@distinguishedTriangles _ _ ⋯ _ (instPreadditive C (ComplexShape.up ℤ)) ⋯ _) T.rotate.rotate
⊢ Membership.mem (γ := Set (Triangle (HomotopyCategory.{v, u_1, 0} C (ComplexShape.up ℤ))))
    (@distinguishedTriangles _ _ ⋯ _ (instPreadditive C (ComplexShape.up ℤ)) ⋯ _) T

Tactic:
rw [rotate_distinguished_triangle, rotate_distinguished_triangle]

Premises used: CategoryTheory.Pretriangulated.rotate_distinguished_triangle
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
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

Tactic:
isomorphic_distinguished _ ?_ _
      ((rotate _ ⋙ rotate _).mapIso e ≪≫
        CochainComplex.trianglehOfDegreewiseSplitRotateRotateIso S σ)

Premises used: CochainComplex.trianglehOfDegreewiseSplitRotateRotateIso, CategoryTheory.Functor.comp, CategoryTheory.Pretriangulated.isomorphic_distinguished, CategoryTheory.Iso.trans, CategoryTheory.Pretriangulated.rotate, CategoryTheory.Functor.mapIso
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
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 σ
mpr :
  Membership.mem (γ := Set (Triangle (HomotopyCategory.{v, u_1, 0} C (ComplexShape.up ℤ))))
    (@distinguishedTriangles _ _ ⋯ _ (instPreadditive C (ComplexShape.up ℤ)) ⋯ _)
    (CochainComplex.mappingCone.triangleh (CochainComplex.homOfDegreewiseSplit S σ))
⊢ Membership.mem (γ := Set (Triangle (HomotopyCategory.{v, u_1, 0} C (ComplexShape.up ℤ))))
    (@distinguishedTriangles _ _ ⋯ _ (instPreadditive C (ComplexShape.up ℤ)) ⋯ _) T.rotate.rotate

Tactic:
refine isomorphic_distinguished _ ?_ _
      ((rotate _ ⋙ rotate _).mapIso e ≪≫
        CochainComplex.trianglehOfDegreewiseSplitRotateRotateIso S σ)

Premises used: CochainComplex.trianglehOfDegreewiseSplitRotateRotateIso, CategoryTheory.Functor.comp, CategoryTheory.Pretriangulated.isomorphic_distinguished, CategoryTheory.Iso.trans, CategoryTheory.Pretriangulated.rotate, CategoryTheory.Functor.mapIso
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
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 ℤ)) ⋯ _)
    (CochainComplex.mappingCone.triangleh (CochainComplex.homOfDegreewiseSplit S σ))

Tactic:
⟨_, _, _, ⟨Iso.refl _⟩⟩

Premises used: Set.Mem, setOf, CategoryTheory.Iso.refl, Nonempty.intro, Exists.intro, HomotopyCategory.Pretriangulated.distinguishedTriangles
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
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 ℤ)) ⋯ _)
    (CochainComplex.mappingCone.triangleh (CochainComplex.homOfDegreewiseSplit S σ))

Tactic:
exact ⟨_, _, _, ⟨Iso.refl _⟩⟩
-- 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 : ℤ
v : (p q : ℤ) → p + n = q → (F.X p ⟶ G.X q)
p q : ℤ
hpq : p + n = q
⊢ (mk v).v p q hpq = v p q hpq

Tactic:
rfl

Premises used: CochainComplex.HomComplex.Cochain.mk, CochainComplex.HomComplex.Cochain.v, 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₂ : Cochain F G n
h : z₁ = z₂
p q : ℤ
hpq : p + n = q
subst : z₁.v p q hpq = z₁.v p q hpq
⊢ z₁.v p q hpq = z₂.v p q hpq

Tactic:
subst h
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
F G : CochainComplex.{v, u, 0} C ℤ
n : ℤ
z₁ : Cochain F G n
p q : ℤ
hpq : p + n = q
⊢ z₁.v p q hpq = z₁.v p q hpq

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₂ : Cochain F G n
h : ∀ (p q : ℤ) (hpq : p + n = q), z₁.v p q hpq = z₂.v p q hpq
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 })
⊢ z₁ = z₂

Tactic:
funext ⟨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 : 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
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:
apply h
-- 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₁ z₂ : Cochain F G 0
h : ∀ (p : ℤ), z₁.v p p ⋯ = z₂.v p p ⋯
h₁ : ∀ (p q : ℤ) (hpq : p + 0 = q), z₁.v p q hpq = z₂.v p q hpq
⊢ z₁ = z₂

Tactic:
ext
-- 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₁ z₂ : Cochain F G 0
h : ∀ (p : ℤ), z₁.v p p ⋯ = z₂.v p p ⋯
p q : ℤ
hpq : p + 0 = q
⊢ z₁.v p q hpq = z₂.v p q hpq

Tactic:
grind
-- 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 p q : ℤ
hpq : p + n = q
⊢ Eq.{v + 1} (α := F.X p ⟶ G.X q) (v 0 p q hpq) 0

Tactic:
rfl

Premises used: CochainComplex.HomComplex.Cochain.v, 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₂ : Cochain F G n
p q : ℤ
hpq : p + n = q
⊢ (z₁ + z₂).v p q hpq = z₁.v p q hpq + z₂.v p q hpq

Tactic:
rfl

Premises used: CochainComplex.HomComplex.Cochain.v, 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₂ : Cochain F G n
p q : ℤ
hpq : p + n = q
⊢ (z₁ - z₂).v p q hpq = z₁.v p q hpq - z₂.v p q hpq

Tactic:
rfl

Premises used: CochainComplex.HomComplex.Cochain.v, 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 : Cochain F G n
p q : ℤ
hpq : p + n = q
⊢ (-z).v p q hpq = -z.v p q hpq

Tactic:
rfl

Premises used: CochainComplex.HomComplex.Cochain.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 : CochainComplex.{v, u, 0} C ℤ
n : ℤ
k : R
z : Cochain F G n
p q : ℤ
hpq : p + n = q
⊢ (k • z).v p q hpq = k • z.v p q hpq

Tactic:
rfl

Premises used: CochainComplex.HomComplex.Cochain.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 : CochainComplex.{v, u, 0} C ℤ
n : ℤ
k : Rˣ
z : Cochain F G n
p q : ℤ
hpq : p + n = q
⊢ (k • z).v p q hpq = k • z.v p q hpq

Tactic:
rfl

Premises used: CochainComplex.HomComplex.Cochain.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 : ℤ
ψ : (p : ℤ) → F.X p ⟶ G.X p
p q : ℤ
hpq : p + 0 = q
rw : G.X p = G.X (p + 0)
rw₁ rw₂ : G.X p = G.X p
⊢ G.X p = G.X q

Tactic:
rw [← hpq, add_zero]

Premises used: add_zero
-- 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 ℤ
ψ : (p : ℤ) → F.X p ⟶ G.X p
p : ℤ
⊢ (ofHoms ψ).v p p ⋯ = ψ p

Tactic:
simp only [ofHoms, mk_v, eqToHom_refl, comp_id]

Premises used: CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id, CochainComplex.HomComplex.Cochain.mk_v, CochainComplex.HomComplex.Cochain.ofHoms
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
F G : CochainComplex.{v, u, 0} C ℤ
ψ : (p : ℤ) → F.X p ⟶ G.X p
p q q' : ℤ
hpq : p + 0 = q
⊢ p = q

Tactic:
rw [add_zero] at hpq

Premises used: add_zero
-- 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 ℤ
ψ : (p : ℤ) → F.X p ⟶ G.X p
p q q' : ℤ
hpq_1 : p + 0 = q
hpq : p = q
subst : ∀ (hpq : p + 0 = p), (ofHoms ψ).v p p hpq ≫ G.d p q' = ψ p ≫ G.d p q'
⊢ (ofHoms ψ).v p q hpq_1 ≫ G.d q q' = ψ p ≫ G.d p q'

Tactic:
subst hpq
-- 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 ℤ
ψ : (p : ℤ) → F.X p ⟶ G.X p
p q' : ℤ
hpq : p + 0 = p
rw rw₁ : ψ p ≫ G.d p q' = ψ p ≫ G.d p q'
⊢ (ofHoms ψ).v p p hpq ≫ G.d p q' = ψ p ≫ G.d p q'

Tactic:
rw [ofHoms_v]

Premises used: CochainComplex.HomComplex.Cochain.ofHoms_v
-- 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 ℤ
ψ : (p : ℤ) → F.X p ⟶ G.X p
p' p q : ℤ
hpq : p + 0 = q
⊢ p = q

Tactic:
rw [add_zero] at hpq

Premises used: add_zero
-- 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 ℤ
ψ : (p : ℤ) → F.X p ⟶ G.X p
p' p q : ℤ
hpq_1 : p + 0 = q
hpq : p = q
subst : ∀ (hpq : p + 0 = p), F.d p' p ≫ (ofHoms ψ).v p p hpq = F.d p' p ≫ ψ p
⊢ F.d p' p ≫ (ofHoms ψ).v p q hpq_1 = F.d p' q ≫ ψ q

Tactic:
subst hpq
-- 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 ℤ
ψ : (p : ℤ) → F.X p ⟶ G.X p
p' p : ℤ
hpq : p + 0 = p
rw rw₁ : F.d p' p ≫ ψ p = F.d p' p ≫ ψ p
⊢ F.d p' p ≫ (ofHoms ψ).v p p hpq = F.d p' p ≫ ψ p

Tactic:
rw [ofHoms_v]

Premises used: CochainComplex.HomComplex.Cochain.ofHoms_v
-- 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 ℤ
⊢ Eq.{v + 1} (α := Cochain F G 0) (ofHom 0) 0

Tactic:
simp only [ofHom, HomologicalComplex.zero_f_apply, ofHoms_zero]

Premises used: CochainComplex.HomComplex.Cochain.ofHom, HomologicalComplex.zero_f_apply, CochainComplex.HomComplex.Cochain.ofHoms_zero
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
F G : CochainComplex.{v, u, 0} C ℤ
φ : F ⟶ G
p : ℤ
⊢ (ofHom φ).v p p ⋯ = φ.f p

Tactic:
simp only [ofHom, ofHoms_v]

Premises used: CochainComplex.HomComplex.Cochain.ofHoms_v, CochainComplex.HomComplex.Cochain.ofHom
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
F G : CochainComplex.{v, u, 0} C ℤ
φ : F ⟶ G
p q q' : ℤ
hpq : p + 0 = q
⊢ (ofHom φ).v p q hpq ≫ G.d q q' = φ.f p ≫ G.d p q'

Tactic:
simp only [ofHom, ofHoms_v_comp_d]

Premises used: CochainComplex.HomComplex.Cochain.ofHoms_v_comp_d, CochainComplex.HomComplex.Cochain.ofHom
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
F G : CochainComplex.{v, u, 0} C ℤ
φ : F ⟶ G
p' p q : ℤ
hpq : p + 0 = q
⊢ F.d p' p ≫ (ofHom φ).v p q hpq = F.d p' q ≫ φ.f q

Tactic:
simp only [ofHom, d_comp_ofHoms_v]

Premises used: CochainComplex.HomComplex.Cochain.ofHom, CochainComplex.HomComplex.Cochain.d_comp_ofHoms_v
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
F G : CochainComplex.{v, u, 0} C ℤ
φ₁ φ₂ : F ⟶ G
h : φ₁ = φ₂
⊢ ofHomotopy (Homotopy.ofEq h) = 0

Tactic:
rfl

Premises used: CochainComplex.HomComplex.Cochain.mk, rfl, CochainComplex.HomComplex.Cochain.ofHomotopy
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
F G : CochainComplex.{v, u, 0} C ℤ
φ : F ⟶ G
⊢ ofHomotopy (Homotopy.refl φ) = 0

Tactic:
rfl

Premises used: CochainComplex.HomComplex.Cochain.mk, rfl, CochainComplex.HomComplex.Cochain.ofHomotopy
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
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
rw₁ rw₂ : q = q
⊢ p + n = q'

Tactic:
rw [← hq', hpq]
-- 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 : ℤ
γ : Cochain F G n
p q q' : ℤ
hpq : p + n = q
hq' : q = q'
subst : γ.v p q hpq ≫ (HomologicalComplex.XIsoOfEq G ⋯).hom = γ.v p q ⋯
⊢ γ.v p q hpq ≫ (HomologicalComplex.XIsoOfEq G hq').hom = γ.v p q' ⋯

Tactic:
subst hq'
-- 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 : ℤ
γ : Cochain F G n
p q : ℤ
hpq : p + n = q
⊢ γ.v p q hpq ≫ (HomologicalComplex.XIsoOfEq G ⋯).hom = γ.v p q ⋯

Tactic:
simp only [HomologicalComplex.XIsoOfEq, eqToIso_refl, Iso.refl_hom, comp_id]

Premises used: HomologicalComplex.XIsoOfEq, CategoryTheory.Category.comp_id, CategoryTheory.eqToIso_refl, CategoryTheory.Iso.refl_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 : ℤ
γ : Cochain F G n
p q q' : ℤ
hpq : p + n = q
hq' : q' = q
rw : p + n = q
rw₁ rw₂ : q = q
⊢ p + n = q'

Tactic:
rw [hq', hpq]
-- 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 : ℤ
γ : Cochain F G n
p q q' : ℤ
hpq : p + n = q
hq' : q' = q
subst : ∀ (hpq : p + n = q'), γ.v p q' hpq ≫ (HomologicalComplex.XIsoOfEq G ⋯).inv = γ.v p q' ⋯
⊢ γ.v p q hpq ≫ (HomologicalComplex.XIsoOfEq G hq').inv = γ.v p q' ⋯

Tactic:
subst hq'