mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.BifunctorShift

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁸ : Category.{v_1, u_1} C₁
inst✝⁷ : Category.{v_2, u_2} C₂
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : Preadditive C₁
inst✝⁴ : Preadditive C₂
inst✝³ : Preadditive D
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.Additive
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst✝ : ∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₂✝ : CochainComplex C₂ ℤ
K₂ : CochainComplex C₁ ℤ
n p q : ℤ
h : (ComplexShape.up ℤ).π (ComplexShape.up ℤ) (ComplexShape.up ℤ) (p, q) = n
⊢ p = p + 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.BifunctorShift

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁸ : Category.{v_1, u_1} C₁
inst✝⁷ : Category.{v_2, u_2} C₂
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : Preadditive C₁
inst✝⁴ : Preadditive C₂
inst✝³ : Preadditive D
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.Additive
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst✝ : ∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₂✝ : CochainComplex C₂ ℤ
K₂ : CochainComplex C₁ ℤ
n p q : ℤ
h : (ComplexShape.up ℤ).π (ComplexShape.up ℤ) (ComplexShape.up ℤ) (p, q) = n
⊢ n = n + 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.BifunctorShift

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁸ : Category.{v_1, u_1} C₁
inst✝⁷ : Category.{v_2, u_2} C₂
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : Preadditive C₁
inst✝⁴ : Preadditive C₂
inst✝³ : Preadditive D
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.Additive
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst✝ : ∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₂ : CochainComplex C₂ ℤ
⊢ NatIso.ofComponents (fun K₁ ↦ K₁.mapBifunctorShift₁Iso K₂ F 0) ⋯ =
    CommShift.isoZero (F.map₂CochainComplex.flip.obj K₂) ℤ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.BifunctorShift

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁸ : Category.{v_1, u_1} C₁
inst✝⁷ : Category.{v_2, u_2} C₂
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : Preadditive C₁
inst✝⁴ : Preadditive C₂
inst✝³ : Preadditive D
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.Additive
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst✝ : ∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₂✝ : CochainComplex C₂ ℤ
a b : ℤ
K₂ : CochainComplex C₁ ℤ
n p q : ℤ
h : p + q = n
⊢ p + a + b = p + (a + b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.BifunctorShift

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁸ : Category.{v_1, u_1} C₁
inst✝⁷ : Category.{v_2, u_2} C₂
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : Preadditive C₁
inst✝⁴ : Preadditive C₂
inst✝³ : Preadditive D
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.Additive
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst✝ : ∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₂✝ : CochainComplex C₂ ℤ
a b : ℤ
K₂ : CochainComplex C₁ ℤ
n p q : ℤ
h : p + q = n
⊢ n + a + b = n + (a + b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.BifunctorShift

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁸ : Category.{v_1, u_1} C₁
inst✝⁷ : Category.{v_2, u_2} C₂
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : Preadditive C₁
inst✝⁴ : Preadditive C₂
inst✝³ : Preadditive D
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.Additive
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst✝ : ∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₂✝ : CochainComplex C₂ ℤ
a b : ℤ
K₂ : CochainComplex C₁ ℤ
n p q : ℤ
h : p + q = n
⊢ p + b + q = n + b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.BifunctorShift

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁸ : Category.{v_1, u_1} C₁
inst✝⁷ : Category.{v_2, u_2} C₂
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : Preadditive C₁
inst✝⁴ : Preadditive C₂
inst✝³ : Preadditive D
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.Additive
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst✝ : ∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₂✝ : CochainComplex C₂ ℤ
a b : ℤ
K₂ : CochainComplex C₁ ℤ
n p q : ℤ
h : p + q = n
⊢ p + a + b = p + b + a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.BifunctorShift

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁸ : Category.{v_1, u_1} C₁
inst✝⁷ : Category.{v_2, u_2} C₂
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : Preadditive C₁
inst✝⁴ : Preadditive C₂
inst✝³ : Preadditive D
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.Additive
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst✝ : ∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₂✝ : CochainComplex C₂ ℤ
a b : ℤ
K₂ : CochainComplex C₁ ℤ
n p q : ℤ
h : p + q = n
⊢ n + a + b = n + b + a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.BifunctorShift

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁸ : Category.{v_1, u_1} C₁
inst✝⁷ : Category.{v_2, u_2} C₂
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : Preadditive C₁
inst✝⁴ : Preadditive C₂
inst✝³ : Preadditive D
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.Additive
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst✝ : ∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₂ : CochainComplex C₂ ℤ
a b : ℤ
⊢ NatIso.ofComponents (fun K₁ ↦ K₁.mapBifunctorShift₁Iso K₂ F (a + b)) ⋯ =
    CommShift.isoAdd (NatIso.ofComponents (fun K₁ ↦ K₁.mapBifunctorShift₁Iso K₂ F a) ⋯)
      (NatIso.ofComponents (fun K₁ ↦ K₁.mapBifunctorShift₁Iso K₂ F b) ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.CommSq

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit (PullbackCone.mk fst snd ⋯)
s : Fork (biprod.desc f (-g)) 0
m : s.pt ⟶ sq.kernelFork.pt
hm : m ≫ Fork.ι sq.kernelFork = s.ι
⊢ m = PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.CommSq

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit sq.kernelFork
s : PullbackCone f g
⊢ biprod.lift s.fst s.snd ≫ biprod.desc f (-g) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.CommSq

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit sq.kernelFork
s : PullbackCone f g
⊢ h.lift (KernelFork.ofι (biprod.lift s.fst s.snd) ⋯) ≫ fst = s.fst

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.BifunctorShift

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁸ : Category.{v_1, u_1} C₁
inst✝⁷ : Category.{v_2, u_2} C₂
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : Preadditive C₁
inst✝⁴ : Preadditive C₂
inst✝³ : Preadditive D
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.Additive
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst✝ : ∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₂ L₂ : CochainComplex C₂ ℤ
g : K₂ ⟶ L₂
n : ℤ
⊢ (commShiftIso (F.map₂CochainComplex.flip.obj K₂) n).hom ≫
      whiskerRight (F.map₂CochainComplex.flip.map g) (shiftFunctor (CochainComplex D ℤ) n) =
    (shiftFunctor (CochainComplex C₁ ℤ) n).whiskerLeft (F.map₂CochainComplex.flip.map g) ≫
      (commShiftIso (F.map₂CochainComplex.flip.obj L₂) n).hom

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.CommSq

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit sq.kernelFork
s : PullbackCone f g
⊢ h.lift (KernelFork.ofι (biprod.lift s.fst s.snd) ⋯) ≫ snd = s.snd

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.CommSq

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit sq.kernelFork
s : PullbackCone f g
m : s.pt ⟶ X₁
hm₁ : m ≫ fst = s.fst
hm₂ : m ≫ snd = s.snd
⊢ biprod.lift s.fst s.snd ≫ biprod.desc f (-g) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.CommSq

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit sq.kernelFork
s : PullbackCone f g
m : s.pt ⟶ X₁
hm₁ : m ≫ fst = s.fst
hm₂ : m ≫ snd = s.snd
⊢ m = h.lift (KernelFork.ofι (biprod.lift s.fst s.snd) ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.CommSq

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
h : IsPullback fst snd f g
P✝ : C
b : P✝ ⟶ ⋯.shortComplex'.X₁
hb : b ≫ ⋯.shortComplex'.f = 0
⊢ b ≫ Fork.ι ⋯.kernelFork = 0 ≫ Fork.ι ⋯.kernelFork

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.CommSq

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
h : IsPullback fst snd f g
⊢ Mono ⋯.shortComplex'.f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.BifunctorShift

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁸ : Category.{v_1, u_1} C₁
inst✝⁷ : Category.{v_2, u_2} C₂
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : Preadditive C₁
inst✝⁴ : Preadditive C₂
inst✝³ : Preadditive D
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.Additive
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst✝ : ∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₁ : CochainComplex C₁ ℤ
K₂ : CochainComplex C₂ ℤ
p q : ℤ
⊢ (commShiftIso (F.map₂CochainComplex.obj ((shiftFunctor (CochainComplex C₁ ℤ) p).obj K₁)) q).hom.app K₂ ≫
      (shiftFunctor (CochainComplex D ℤ) q).map ((commShiftIso (F.map₂CochainComplex.flip.obj K₂) p).hom.app K₁) =
    (commShiftIso (F.map₂CochainComplex.flip.obj ((shiftFunctor (CochainComplex C₂ ℤ) q).obj K₂)) p).hom.app K₁ ≫
      (shiftFunctor (CochainComplex D ℤ) p).map ((commShiftIso (F.map₂CochainComplex.obj K₁) q).hom.app K₂) ≫
        (shiftComm ((F.map₂CochainComplex.obj K₁).obj K₂) p q).inv ≫
          (↑(CommShift₂Setup.int.ε p q)).app
            ((shiftFunctor (CochainComplex D ℤ) q).obj
              ((shiftFunctor (CochainComplex D ℤ) p).obj ((F.map₂CochainComplex.obj K₁).obj K₂)))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.SmallShiftedHom

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
n : ℤ
inst✝ : HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
x : CohomologyClass K L n
⊢ ∀ (a b : Cocycle K L n),
    a ≈ b →
      SmallShiftedHom.mk (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) (Cocycle.equivHomShift.symm a) =
        SmallShiftedHom.mk (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) (Cocycle.equivHomShift.symm b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.SmallShiftedHom

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
n : ℤ
inst✝¹ : HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
inst✝ : HasDerivedCategory C
x : Cocycle K L n
⊢ (SmallShiftedHom.equiv (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) DerivedCategory.Q)
      (mk x).toSmallShiftedHom =
    ShiftedHom.map (Cocycle.equivHomShift.symm x) DerivedCategory.Q

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n m✝ p : ℤ
α₁ α₂ : Cocycle K L n
m : ℤ
hm : m + 1 = n
β₁ : Cochain K L m
hβ₁ : δ m n β₁ = ↑α₁
m' : ℤ
hm' : m' + 1 = n
β₂ : Cochain K L m'
hβ₂ : δ m' n β₂ = ↑α₂
⊢ m = m'

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n m✝ p : ℤ
α₁ α₂ : Cocycle K L n
m : ℤ
hm : m + 1 = n
β₁ : Cochain K L m
hβ₁ : δ m n β₁ = ↑α₁
hm' : m + 1 = n
β₂ : Cochain K L m
hβ₂ : δ m n β₂ = ↑α₂
⊢ δ m n (β₁ + β₂) = ↑(α₁ + α₂)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexInduction

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
d : ℤ
X : ℕ → Set (Cochain K L d)
φ : (n : ℕ) → ↑(X n) → ↑(X (n + 1))
p₀ : ℤ
hφ : ∀ (n : ℕ) (x : ↑(X n)), (↑(φ n x)).EqUpTo (↑x) (p₀ + ↑n)
x₀ : ↑(X 0)
k : ℕ
hk : ∀ (n₁ : ℕ), (↑(sequence φ x₀ n₁)).EqUpTo (↑(sequence φ x₀ (n₁ + k))) (p₀ + ↑n₁)
n₁ : ℕ
p q : ℤ
hpq : p + d = q
hp : p ≤ p₀ + ↑n₁
⊢ p ≤ p₀ + ↑(n₁ + k)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n m p : ℤ
⊢ ∀ {a b : Cocycle K L n},
    a ∈ {α | ∃ m, ∃ (_ : m + 1 = n), ∃ β, δ m n β = ↑α} →
      b ∈ {α | ∃ m, ∃ (_ : m + 1 = n), ∃ β, δ m n β = ↑α} → a + b ∈ {α | ∃ m, ∃ (_ : m + 1 = n), ∃ β, δ m n β = ↑α}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n m p : ℤ
⊢ n - 1 + 1 = n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n m p : ℤ
⊢ δ (n - 1) n 0 = ↑0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n m✝ p : ℤ
α : Cocycle K L n
m : ℤ
hm : m + 1 = n
β : Cochain K L m
hβ : δ m n β = ↑α
⊢ δ m n (-β) = ↑(-α)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexInduction

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
d : ℤ
X : ℕ → Set (Cochain K L d)
φ : (n : ℕ) → ↑(X n) → ↑(X (n + 1))
p₀ : ℤ
hφ : ∀ (n : ℕ) (x : ↑(X n)), (↑(φ n x)).EqUpTo (↑x) (p₀ + ↑n)
x₀ : ↑(X 0)
n₁ n₂ : ℕ
h : n₁ ≤ n₂
⊢ (↑(sequence φ x₀ n₁)).EqUpTo (↑(sequence φ x₀ n₂)) (p₀ + ↑n₁)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n m p : ℤ
⊢ ∀ {x : Cocycle K L n},
    x ∈ {α | ∃ m, ∃ (_ : m + 1 = n), ∃ β, δ m n β = ↑α} → -x ∈ {α | ∃ m, ∃ (_ : m + 1 = n), ∃ β, δ m n β = ↑α}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
α : Cocycle K L n
m : ℤ
hm : m + 1 = n
⊢ α ∈ coboundaries K L n ↔ ∃ β, δ m n β = ↑α

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n m p : ℤ
⊢ mk 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n m p : ℤ
⊢ ∀ (x y : Cocycle K L n), mk (x + y) = mk x + mk y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n m✝ p m : ℤ
hm : m + 1 = n
β : Cochain K L m
property✝ : δ m n β ∈ cocycle K L n
⊢ -1 + n = m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n m✝ p m : ℤ
hm : m + 1 = n
β : Cochain K L m
property✝ : δ m n β ∈ cocycle K L n
⊢ Cochain.ofHom (Cocycle.rightShift ⟨δ m n β, property✝⟩ n 0 ⋯).homOf =
    δ (-1) 0 (n.negOnePow • β.rightShift n (-1) (CochainComplex.HomComplex.CohomologyClass.toHom._proof_4 n m hm)) +
      Cochain.ofHom 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n m p : ℤ
⊢ coboundaries K L n ≤
    ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).mapAddHom.comp Cocycle.equivHomShift.symm.toAddMonoidHom).ker

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexInduction

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
d : ℤ
X : ℕ → Set (Cochain K L d)
φ : (n : ℕ) → ↑(X n) → ↑(X (n + 1))
p₀ : ℤ
hφ : ∀ (n : ℕ) (x : ↑(X n)), (↑(φ n x)).EqUpTo (↑x) (p₀ + ↑n)
x₀ : ↑(X 0)
n : ℕ
p q : ℤ
hpq : p + d = q
hp : p ≤ p₀ + ↑n
⊢ (p - p₀).toNat ≤ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexInduction

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
d : ℤ
X : ℕ → Set (Cochain K L d)
φ : (n : ℕ) → ↑(X n) → ↑(X (n + 1))
p₀ : ℤ
hφ : ∀ (n : ℕ) (x : ↑(X n)), (↑(φ n x)).EqUpTo (↑x) (p₀ + ↑n)
x₀ : ↑(X 0)
n : ℕ
p q : ℤ
hpq : p + d = q
hp : p ≤ p₀ + ↑n
⊢ p ≤ p₀ + ↑(p - p₀).toNat

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexInduction

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
d : ℤ
X : ℕ → Set (Cochain K L d)
φ : (n : ℕ) → ↑(X n) → ↑(X (n + 1))
p₀ : ℤ
hφ : ∀ (n : ℕ) (x : ↑(X n)), (↑(φ n x)).EqUpTo (↑x) (p₀ + ↑n)
x₀ : ↑(X 0)
n : ℕ
⊢ (limitSequence φ hφ x₀).EqUpTo (↑(sequence φ x₀ n)) (p₀ + ↑n)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.ConcreteCategory

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
ι : Type u_2
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i j : ι
hij : c.Rel i j
x₃ : ↑((forget₂ C Ab).obj (S.X₃.X i))
hx₃ : (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₃.d i j))) x₃ = 0
x₂ : ↑((forget₂ C Ab).obj (S.X₂.X i))
hx₂ : (ConcreteCategory.hom ((forget₂ C Ab).map (S.g.f i))) x₂ = x₃
x₁ : ↑((forget₂ C Ab).obj (S.X₁.X j))
hx₁ :
  (ConcreteCategory.hom ((forget₂ C Ab).map (S.f.f j))) x₁ = (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₂.d i j))) x₂
k : ι
hk : c.next j = k
⊢ (ConcreteCategory.hom ((forget₂ C Ab).map (hS.δ i j hij)))
      ((ConcreteCategory.hom ((forget₂ C Ab).map (S.X₃.homologyπ i))) (S.X₃.cyclesMk x₃ j ⋯ hx₃)) =
    (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₁.homologyπ j))) (S.X₁.cyclesMk x₁ k hk ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
x : Cocycle K L n
h✝ : Nonempty (Homotopy (Cocycle.equivHomShift.symm x) 0)
γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) (-1)
h : (↑x).rightShift n 0 ⋯ = δ (-1) 0 γ
⊢ n - 1 + 1 = n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
x : Cocycle K L n
h✝ : Nonempty (Homotopy (Cocycle.equivHomShift.symm x) 0)
γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) (-1)
h : (↑x).rightShift n 0 ⋯ = δ (-1) 0 γ
⊢ -1 + n = n - 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
x : Cocycle K L n
h✝ : Nonempty (Homotopy (Cocycle.equivHomShift.symm x) 0)
γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) (-1)
h : (↑x).rightShift n 0 ⋯ = δ (-1) 0 γ
⊢ δ (n - 1) n (n.negOnePow • γ.rightUnshift (n - 1) ⋯) = ↑x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Orthogonal

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P : ObjectProperty C
X✝ Y✝ : C
e : X✝ ≅ Y✝
h : P.rightOrthogonal X✝
X : C
f : X ⟶ Y✝
hX : P X
⊢ f = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Orthogonal

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P : ObjectProperty C
X✝ Y✝ : C
e : X✝ ≅ Y✝
h : P.leftOrthogonal X✝
Y : C
f : Y✝ ⟶ Y
hY : P Y
⊢ f = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Orthogonal

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
P : ObjectProperty C
inst✝ : HasZeroObject C
x✝² : C
x✝¹ : x✝² ⟶ 0
x✝ : P x✝²
⊢ x✝¹ = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Orthogonal

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
P : ObjectProperty C
inst✝ : HasZeroObject C
x✝² : C
x✝¹ : 0 ⟶ x✝²
x✝ : P x✝²
⊢ x✝¹ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
x : Cocycle K L n
⊢ toHom (mk x) = 0 ↔ x ∈ coboundaries K L n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
f : K ⟶ (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L
⊢ toHom (mk (Cocycle.equivHomShift f)) = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
⊢ Function.Bijective ⇑toHom

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n m p : ℤ
hm : n + 1 = m
hp : m + 1 = p
⊢ AddCommGrpCat.ofHom (Cocycle.toCochainAddMonoidHom K L m) ≫ (HomologicalComplex.sc' (K.HomComplex L) n m p).g = 0

Tactic:
by

Goal state after: