mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (shiftFunctorAdd C a 0).inv.app X = (shiftFunctorZero C A).hom.app ((shiftFunctor C a).obj X) ≫ eqToHom ⋯

Tactic:
by

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

Goal state before:
pp: V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : ChainComplex V ℕ
X : V
⊢ Function.LeftInverse (fun f ↦ HomologicalComplex.mkHomFromSingle f ⋯) fun f ↦ f.f 0

Tactic:
by

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

Goal state before:
pp: V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : ChainComplex V ℕ
X : V
⊢ Function.RightInverse (fun f ↦ HomologicalComplex.mkHomFromSingle f ⋯) fun f ↦ f.f 0

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j : ι
r : c.Rel i j
⊢ C.dTo j = (C.xPrevIso r).hom ≫ C.d i j

Tactic:
by

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

Goal state before:
pp: V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : ChainComplex V ℕ
X : V
f : X ⟶ C.X 0
⊢ ((C.fromSingle₀Equiv X).symm f).f 0 = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃
X : C
⊢ a₁₂ + a₃ = a₁₂₃

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
j : ι
h : ¬c.Rel (c.prev j) j
⊢ C.dTo j = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
⊢ (DLinearMap R S) 1 = 0

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j : ι
r : c.Rel i j
⊢ C.dFrom i = C.d i j ≫ (C.xNextIso r).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃
X : C
⊢ a₁ + a₂₃ = a₁₂₃

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i : ι
h : ¬c.Rel i (c.next i)
⊢ C.dFrom i = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃
X : C
⊢ (shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ ⋯).hom.app X ≫
      (shiftFunctor C a₃).map ((shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂).hom.app X) =
    (shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ ⋯).hom.app X ≫
      (shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃).hom.app ((shiftFunctor C a₁).obj X)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j : ι
r : c.Rel i j
⊢ (C.xPrevIso r).inv ≫ C.dTo j = C.d i j

Tactic:
by

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

Goal state before:
pp: V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : CochainComplex V ℕ
X : V
φ : (single₀ V).obj X ⟶ C
⊢ φ.f 0 ≫ C.d 0 1 = 0

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
j : ι
h : ¬c.Rel (c.prev j) j
⊢ (C.xPrevIsoSelf h).inv ≫ C.dTo j = 0

Tactic:
by

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

Goal state before:
pp: V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : CochainComplex V ℕ
X : V
f : { f // f ≫ C.d 0 1 = 0 }
i : ℕ
hi : (ComplexShape.up ℕ).Rel 0 i
⊢ i = 1

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j : ι
r : c.Rel i j
⊢ C.dFrom i ≫ (C.xNextIso r).hom = C.d i j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃
X : C
⊢ (shiftFunctor C a₃).map ((shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂).inv.app X) ≫
      (shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ ⋯).inv.app X =
    (shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃).inv.app ((shiftFunctor C a₁).obj X) ≫
      (shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ ⋯).inv.app X

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i : ι
h : ¬c.Rel i (c.next i)
⊢ C.dFrom i ≫ (C.xNextIsoSelf h).hom = 0

Tactic:
by

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

Goal state before:
pp: V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : CochainComplex V ℕ
X : V
f : { f // f ≫ C.d 0 1 = 0 }
i : ℕ
hi : (ComplexShape.up ℕ).Rel 0 i
⊢ ↑f ≫ C.d 0 i = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
X : C
⊢ (shiftFunctorAdd C (a₁ + a₂) a₃).hom.app X ≫ (shiftFunctor C a₃).map ((shiftFunctorAdd C a₁ a₂).hom.app X) =
    (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯).hom.app X ≫
      (shiftFunctorAdd C a₂ a₃).hom.app ((shiftFunctor C a₁).obj X)

Tactic:
by

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

Goal state before:
pp: V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : CochainComplex V ℕ
X : V
φ : (single₀ V).obj X ⟶ C
⊢ (fun f ↦ HomologicalComplex.mkHomFromSingle ↑f ⋯) ((fun φ ↦ ⟨φ.f 0, ⋯⟩) φ) = φ

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
i j : ι
r : c.Rel i j
⊢ kernelSubobject (C.dFrom i) = kernelSubobject (C.d i j)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
X : C
⊢ (shiftFunctor C a₃).map ((shiftFunctorAdd C a₁ a₂).inv.app X) ≫ (shiftFunctorAdd C (a₁ + a₂) a₃).inv.app X =
    (shiftFunctorAdd C a₂ a₃).inv.app ((shiftFunctor C a₁).obj X) ≫
      (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯).inv.app X

Tactic:
by

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

Goal state before:
pp: V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : CochainComplex V ℕ
X : V
⊢ Function.RightInverse (fun f ↦ HomologicalComplex.mkHomFromSingle ↑f ⋯) fun φ ↦ ⟨φ.f 0, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
i j : A
⊢ (shiftFunctor C j).map ((shiftFunctor C i).map f) =
    (shiftAdd X i j).inv ≫ (shiftFunctor C (i + j)).map f ≫ (shiftAdd Y i j).hom

Tactic:
by

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

Goal state before:
pp: V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
hf : f ≫ C.d 0 1 = 0
⊢ ((C.fromSingle₀Equiv X).symm ⟨f, hf⟩).f 0 = f

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝¹ : HasImages V
inst✝ : HasEqualizers V
i j : ι
r : c.Rel i j
⊢ imageSubobject (C.dTo j) = imageSubobject (C.d i j)

Tactic:
by

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

Goal state before:
pp: V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : CochainComplex V ℕ
X : V
f : C.X 0 ⟶ X
i : ℕ
hi : (ComplexShape.up ℕ).Rel i 0
⊢ C.d i 0 ≫ f = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
⊢ (shiftFunctor C 0).map f = (shiftZero A X).hom ≫ f ≫ (shiftZero A Y).inv

Tactic:
by

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

Goal state before:
pp: V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : CochainComplex V ℕ
X : V
⊢ Function.LeftInverse (fun f ↦ HomologicalComplex.mkHomToSingle f ⋯) fun f ↦ f.f 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
i j : A
h : i + j = 0
⊢ j + i = 0

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : (i : ι) → C₁.X i ≅ C₂.X i
hf : ∀ (i j : ι), c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom
i j : ι
hij : c.Rel i j
⊢ (f i).inv ≫ C₁.d i j = (f i).inv ≫ (C₁.d i j ≫ (f j).hom) ≫ (f j).inv

Tactic:
by

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

Goal state before:
pp: V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : CochainComplex V ℕ
X : V
⊢ Function.RightInverse (fun f ↦ HomologicalComplex.mkHomToSingle f ⋯) fun f ↦ f.f 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
i j : A
h : i + j = 0
X : C
⊢ (MonoidalCategoryStruct.tensorObj { as := j } { as := i }).as = (MonoidalCategoryStruct.tensorUnit (Discrete A)).as

Tactic:
by

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

Goal state before:
pp: V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : CochainComplex V ℕ
X : V
f : C.X 0 ⟶ X
⊢ ((C.toSingle₀Equiv X).symm f).f 0 = f

Tactic:
by

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

Goal state before:
pp: V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : CochainComplex V ℕ
X : V
f : C.X 0 ⟶ X
n : ℕ
⊢ ((C.toSingle₀Equiv X).symm f).f (n + 1) = 0

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : (i : ι) → C₁.X i ≅ C₂.X i
hf : ∀ (i j : ι), c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom
i j : ι
hij : c.Rel i j
⊢ (f i).inv ≫ (C₁.d i j ≫ (f j).hom) ≫ (f j).inv = (f i).inv ≫ ((f i).hom ≫ C₂.d i j) ≫ (f j).inv

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝⁷ : Category.{v, u} V
inst✝⁶ : Preadditive V
W : Type u_2
inst✝⁵ : Category.{v_1, u_2} W
inst✝⁴ : Preadditive W
W₁ : Type u_3
W₂ : Type u_4
inst✝³ : Category.{v_2, u_3} W₁
inst✝² : Category.{v_3, u_4} W₂
inst✝¹ : HasZeroMorphisms W₁
inst✝ : HasZeroMorphisms W₂
c : ComplexShape ι
C D : HomologicalComplex V c
f✝ : C ⟶ D
i✝ : ι
n : ℕ
f : C ⟶ D
i j : ι
x✝ : c.Rel i j
⊢ (n • f.f i) ≫ D.d i j = C.d i j ≫ (n • f.f j)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝⁷ : Category.{v, u} V
inst✝⁶ : Preadditive V
W : Type u_2
inst✝⁵ : Category.{v_1, u_2} W
inst✝⁴ : Preadditive W
W₁ : Type u_3
W₂ : Type u_4
inst✝³ : Category.{v_2, u_3} W₁
inst✝² : Category.{v_3, u_4} W₂
inst✝¹ : HasZeroMorphisms W₁
inst✝ : HasZeroMorphisms W₂
c : ComplexShape ι
C D : HomologicalComplex V c
f✝ : C ⟶ D
i✝ : ι
n : ℤ
f : C ⟶ D
i j : ι
x✝ : c.Rel i j
⊢ (n • f.f i) ≫ D.d i j = C.d i j ≫ (n • f.f j)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝⁷ : Category.{v, u} V
inst✝⁶ : Preadditive V
W : Type u_2
inst✝⁵ : Category.{v_1, u_2} W
inst✝⁴ : Preadditive W
W₁ : Type u_3
W₂ : Type u_4
inst✝³ : Category.{v_2, u_3} W₁
inst✝² : Category.{v_3, u_4} W₂
inst✝¹ : HasZeroMorphisms W₁
inst✝ : HasZeroMorphisms W₂
c : ComplexShape ι
C D : HomologicalComplex V c
f : C ⟶ D
i : ι
⊢ Hom.f 0 = 0

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝⁷ : Category.{v, u} V
inst✝⁶ : Preadditive V
W : Type u_2
inst✝⁵ : Category.{v_1, u_2} W
inst✝⁴ : Preadditive W
W₁ : Type u_3
W₂ : Type u_4
inst✝³ : Category.{v_2, u_3} W₁
inst✝² : Category.{v_3, u_4} W₂
inst✝¹ : HasZeroMorphisms W₁
inst✝ : HasZeroMorphisms W₂
c : ComplexShape ι
C D : HomologicalComplex V c
f : C ⟶ D
i : ι
⊢ ∀ (x y : C ⟶ D), (x + y).f = x.f + y.f

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝⁷ : Category.{v, u} V
inst✝⁶ : Preadditive V
W : Type u_2
inst✝⁵ : Category.{v_1, u_2} W
inst✝⁴ : Preadditive W
W₁ : Type u_3
W₂ : Type u_4
inst✝³ : Category.{v_2, u_3} W₁
inst✝² : Category.{v_3, u_4} W₂
inst✝¹ : HasZeroMorphisms W₁
inst✝ : HasZeroMorphisms W₂
c : ComplexShape ι
C D : HomologicalComplex V c
f : C ⟶ D
i : ι
⊢ ∀ (x : C ⟶ D), (-x).f = -x.f

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝⁷ : Category.{v, u} V
inst✝⁶ : Preadditive V
W : Type u_2
inst✝⁵ : Category.{v_1, u_2} W
inst✝⁴ : Preadditive W
W₁ : Type u_3
W₂ : Type u_4
inst✝³ : Category.{v_2, u_3} W₁
inst✝² : Category.{v_3, u_4} W₂
inst✝¹ : HasZeroMorphisms W₁
inst✝ : HasZeroMorphisms W₂
c : ComplexShape ι
C D : HomologicalComplex V c
f : C ⟶ D
i : ι
⊢ ∀ (x y : C ⟶ D), (x - y).f = x.f - y.f

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝⁷ : Category.{v, u} V
inst✝⁶ : Preadditive V
W : Type u_2
inst✝⁵ : Category.{v_1, u_2} W
inst✝⁴ : Preadditive W
W₁ : Type u_3
W₂ : Type u_4
inst✝³ : Category.{v_2, u_3} W₁
inst✝² : Category.{v_3, u_4} W₂
inst✝¹ : HasZeroMorphisms W₁
inst✝ : HasZeroMorphisms W₂
c : ComplexShape ι
C D : HomologicalComplex V c
f : C ⟶ D
i : ι
⊢ ∀ (x : C ⟶ D) (n : ℕ), (n • x).f = n • x.f

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝⁷ : Category.{v, u} V
inst✝⁶ : Preadditive V
W : Type u_2
inst✝⁵ : Category.{v_1, u_2} W
inst✝⁴ : Preadditive W
W₁ : Type u_3
W₂ : Type u_4
inst✝³ : Category.{v_2, u_3} W₁
inst✝² : Category.{v_3, u_4} W₂
inst✝¹ : HasZeroMorphisms W₁
inst✝ : HasZeroMorphisms W₂
c : ComplexShape ι
C D : HomologicalComplex V c
f : C ⟶ D
i : ι
⊢ ∀ (x : C ⟶ D) (n : ℤ), (n • x).f = n • x.f

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : (i : ι) → C₁.X i ≅ C₂.X i
hf : ∀ (i j : ι), c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom
i j : ι
hij : c.Rel i j
⊢ (f i).inv ≫ ((f i).hom ≫ C₂.d i j) ≫ (f j).inv = C₂.d i j ≫ (f j).inv

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
a b : S
⊢ (DLinearMap R S) (a * b) = a • (DLinearMap R S) b + b • (DLinearMap R S) a

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : (i : ι) → C₁.X i ≅ C₂.X i
hf : ∀ (i j : ι), c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom
⊢ { f := fun i ↦ (f i).hom, comm' := hf } ≫ { f := fun i ↦ (f i).inv, comm' := ⋯ } = 𝟙 C₁

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : Preadditive V
W : Type u_2
inst✝⁶ : Category.{v_1, u_2} W
inst✝⁵ : Preadditive W
W₁ : Type u_3
W₂ : Type u_4
inst✝⁴ : Category.{v_2, u_3} W₁
inst✝³ : Category.{v_3, u_4} W₂
inst✝² : HasZeroMorphisms W₁
inst✝¹ : HasZeroMorphisms W₂
c✝ : ComplexShape ι
C✝ D : HomologicalComplex V c✝
f : C✝ ⟶ D
i✝ : ι
F : W₁ ⥤ W₂
inst✝ : F.PreservesZeroMorphisms
c : ComplexShape ι
C : HomologicalComplex W₁ c
i j : ι
w : ¬c.Rel i j
⊢ F.map (C.d i j) = 0

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : (i : ι) → C₁.X i ≅ C₂.X i
hf : ∀ (i j : ι), c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom
⊢ { f := fun i ↦ (f i).inv, comm' := ⋯ } ≫ { f := fun i ↦ (f i).hom, comm' := hf } = 𝟙 C₂

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : Preadditive V
W : Type u_2
inst✝⁶ : Category.{v_1, u_2} W
inst✝⁵ : Preadditive W
W₁ : Type u_3
W₂ : Type u_4
inst✝⁴ : Category.{v_2, u_3} W₁
inst✝³ : Category.{v_3, u_4} W₂
inst✝² : HasZeroMorphisms W₁
inst✝¹ : HasZeroMorphisms W₂
c✝ : ComplexShape ι
C✝ D : HomologicalComplex V c✝
f : C✝ ⟶ D
i✝ : ι
F : W₁ ⥤ W₂
inst✝ : F.PreservesZeroMorphisms
c : ComplexShape ι
C : HomologicalComplex W₁ c
i j k : ι
x✝¹ : c.Rel i j
x✝ : c.Rel j k
⊢ F.map (C.d i j) ≫ F.map (C.d j k) = 0

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C₁ C₂ : HomologicalComplex V c
f : (i : ι) → C₁.X i ≅ C₂.X i
hf : ∀ (i j : ι), c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom
i : ι
⊢ isoApp (isoOfComponents f hf) i = f i

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C₁ C₂ : HomologicalComplex V c
f : C₁.Hom C₂
i j : ι
w : c.Rel i j
⊢ f.prev j = (C₁.xPrevIso w).hom ≫ f.f i ≫ (C₂.xPrevIso w).inv

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C₁ C₂ : HomologicalComplex V c
f : C₁.Hom C₂
i j : ι
w : c.Rel i j
⊢ f.next i = (C₁.xNextIso w).hom ≫ f.f j ≫ (C₂.xNextIso w).inv

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C₁ C₂ : HomologicalComplex V c
f : C₁ ⟶ C₂
inst✝ : IsIso f
j : ι
⊢ (inv f).f j = inv (f.f j)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : Preadditive V
W : Type u_2
inst✝⁶ : Category.{v_1, u_2} W
inst✝⁵ : Preadditive W
W₁ : Type u_3
W₂ : Type u_4
inst✝⁴ : Category.{v_2, u_3} W₁
inst✝³ : Category.{v_3, u_4} W₂
inst✝² : HasZeroMorphisms W₁
inst✝¹ : HasZeroMorphisms W₂
c✝ : ComplexShape ι
C D : HomologicalComplex V c✝
f✝ : C ⟶ D
i✝ : ι
F : W₁ ⥤ W₂
inst✝ : F.PreservesZeroMorphisms
c : ComplexShape ι
X✝ Y✝ : HomologicalComplex W₁ c
f : X✝ ⟶ Y✝
i j : ι
x✝ : c.Rel i j
⊢ F.map (f.f i) ≫ { X := fun i ↦ F.obj (Y✝.X i), d := fun i j ↦ F.map (Y✝.d i j), shape := ⋯, d_comp_d' := ⋯ }.d i j =
    { X := fun i ↦ F.obj (X✝.X i), d := fun i j ↦ F.map (X✝.d i j), shape := ⋯, d_comp_d' := ⋯ }.d i j ≫ F.map (f.f j)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
i j : α
h : i = j + 1
⊢ X i = X (j + 1)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
i j : α
w : ¬(ComplexShape.down α).Rel i j
⊢ of.d X d i j = 0

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝⁹ : Category.{v, u} V
inst✝⁸ : Preadditive V
W : Type u_2
inst✝⁷ : Category.{v_1, u_2} W
inst✝⁶ : Preadditive W
W₁ : Type u_3
W₂ : Type u_4
inst✝⁵ : Category.{v_2, u_3} W₁
inst✝⁴ : Category.{v_3, u_4} W₂
inst✝³ : HasZeroMorphisms W₁
inst✝² : HasZeroMorphisms W₂
c✝ : ComplexShape ι
C D : HomologicalComplex V c✝
f✝ : C ⟶ D
i : ι
F : W₁ ⥤ W₂
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : F.ReflectsIsomorphisms
c : ComplexShape ι
A✝ B✝ : HomologicalComplex W₁ c
f : A✝ ⟶ B✝
⊢ ∀ [IsIso ((F.mapHomologicalComplex c).map f)], IsIso f

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
i j k : α
hij : (ComplexShape.down α).Rel i j
hjk : (ComplexShape.down α).Rel j k
⊢ of.d X d i j ≫ of.d X d j k = 0

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
i j k : α
hij : (ComplexShape.down α).Rel i j
hjk : (ComplexShape.down α).Rel j k
⊢ of.d X d i j ≫ of.d X d j k = 0

Tactic:
by
      dsimp [of.d] at hij hjk ⊢
      subst hij hjk
      simp only [eqToHom_refl, id_comp, dite_eq_ite, ite_true, sq]

Goal state after: