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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
⊢ IsIso (h₁.homologyIso.hom ≫ γ.φH ≫ h₂.homologyIso.inv) ↔ IsIso γ.φH

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
⊢ IsIso (h₁.homologyIso.hom ≫ γ.φH ≫ h₂.homologyIso.inv) → IsIso γ.φH

case mpr
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
⊢ IsIso γ.φH → IsIso (h₁.homologyIso.hom ≫ γ.φH ≫ h₂.homologyIso.inv)
Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
γ : HomologyMapData φ S₁.homologyData S₂.homologyData
⊢ IsIso γ.left.φH.op ↔ IsIso γ.left.φH

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
γ : HomologyMapData φ S₁.homologyData S₂.homologyData
⊢ IsIso γ.left.φH.op → IsIso γ.left.φH

case mpr
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
γ : HomologyMapData φ S₁.homologyData S₂.homologyData
⊢ IsIso γ.left.φH → IsIso γ.left.φH.op
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
⊢ S.leftHomologyData.homologyIso = S.leftHomologyIso.symm

Tactic:
ext

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
⊢ S.leftHomologyData.homologyIso.hom = S.leftHomologyIso.symm.hom
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
⊢ S.rightHomologyData.homologyIso = S.rightHomologyIso.symm

Tactic:
ext

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
⊢ S.rightHomologyData.homologyIso.hom = S.rightHomologyIso.symm.hom
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
inst✝ : S.HasHomology
⊢ h.iso = h.left.homologyIso.symm ≪≫ h.right.homologyIso

Tactic:
ext

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
inst✝ : S.HasHomology
⊢ h.iso.hom = (h.left.homologyIso.symm ≪≫ h.right.homologyIso).hom
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
⊢ S₁.rightHomologyIso.hom ≫ homologyMap φ = rightHomologyMap φ ≫ S₂.rightHomologyIso.hom

Tactic:
by
  simpa only [RightHomologyData.homologyIso_rightHomologyData, Iso.symm_inv] using!
    RightHomologyData.rightHomologyIso_inv_naturality φ S₁.rightHomologyData S₂.rightHomologyData

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasRightHomology
inst✝ : S₂.HasRightHomology
⊢ opcyclesMap φ = h₁.opcyclesIso.hom ≫ γ.φQ ≫ h₂.opcyclesIso.inv

Tactic:
by
  dsimp [RightHomologyData.opcyclesIso, cyclesMapIso']
  rw [← γ.opcyclesMap'_eq, ← opcyclesMap'_comp, ← opcyclesMap'_comp, id_comp, comp_id]
  rfl

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.LeftHomologyData
⊢ S.homologyπ ≫ h.homologyIso.hom = h.cyclesIso.hom ≫ h.π

Tactic:
dsimp only [homologyπ, homologyIso]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.LeftHomologyData
⊢ (S.leftHomologyπ ≫ S.leftHomologyIso.hom) ≫ (S.leftHomologyIso.symm ≪≫ h.leftHomologyIso).hom = h.cyclesIso.hom ≫ h.π
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.LeftHomologyData
⊢ h.π ≫ h.homologyIso.inv = h.cyclesIso.inv ≫ S.homologyπ

Tactic:
dsimp only [homologyπ, homologyIso]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.LeftHomologyData
⊢ h.π ≫ (S.leftHomologyIso.symm ≪≫ h.leftHomologyIso).inv = h.cyclesIso.inv ≫ S.leftHomologyπ ≫ S.leftHomologyIso.hom
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
⊢ homologyMap (opMap φ) ≫ S₁.homologyOpIso.hom = S₂.homologyOpIso.hom ≫ (homologyMap φ).op

Tactic:
by
  simp [homologyMap_op]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
⊢ (homologyMap φ).op ≫ S₁.homologyOpIso.inv = S₂.homologyOpIso.inv ≫ homologyMap (opMap φ)

Tactic:
by
  simp [homologyMap_op]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Limits

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cone F
h₁ : IsLimit (π₁.mapCone c)
h₂ : IsLimit (π₂.mapCone c)
h₃ : IsLimit (π₃.mapCone c)
s : Cone F
j : J
⊢ { τ₁ := h₁.lift (π₁.mapCone s), τ₂ := h₂.lift (π₂.mapCone s), τ₃ := h₃.lift (π₃.mapCone s), comm₁₂ := ⋯,
        comm₂₃ := ⋯ } ≫
      c.π.app j =
    s.π.app j

Tactic:
ext

Goal state after:
case h₁
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cone F
h₁ : IsLimit (π₁.mapCone c)
h₂ : IsLimit (π₂.mapCone c)
h₃ : IsLimit (π₃.mapCone c)
s : Cone F
j : J
⊢ ({ τ₁ := h₁.lift (π₁.mapCone s), τ₂ := h₂.lift (π₂.mapCone s), τ₃ := h₃.lift (π₃.mapCone s), comm₁₂ := ⋯,
          comm₂₃ := ⋯ } ≫
        c.π.app j).τ₁ =
    (s.π.app j).τ₁

case h₂
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cone F
h₁ : IsLimit (π₁.mapCone c)
h₂ : IsLimit (π₂.mapCone c)
h₃ : IsLimit (π₃.mapCone c)
s : Cone F
j : J
⊢ ({ τ₁ := h₁.lift (π₁.mapCone s), τ₂ := h₂.lift (π₂.mapCone s), τ₃ := h₃.lift (π₃.mapCone s), comm₁₂ := ⋯,
          comm₂₃ := ⋯ } ≫
        c.π.app j).τ₂ =
    (s.π.app j).τ₂

case h₃
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cone F
h₁ : IsLimit (π₁.mapCone c)
h₂ : IsLimit (π₂.mapCone c)
h₃ : IsLimit (π₃.mapCone c)
s : Cone F
j : J
⊢ ({ τ₁ := h₁.lift (π₁.mapCone s), τ₂ := h₂.lift (π₂.mapCone s), τ₃ := h₃.lift (π₃.mapCone s), comm₁₂ := ⋯,
          comm₂₃ := ⋯ } ≫
        c.π.app j).τ₃ =
    (s.π.app j).τ₃
Module: Mathlib.Algebra.Homology.ShortComplex.Limits

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cone F
h₁ : IsLimit (π₁.mapCone c)
h₂ : IsLimit (π₂.mapCone c)
h₃ : IsLimit (π₃.mapCone c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
⊢ m =
    { τ₁ := h₁.lift (π₁.mapCone s), τ₂ := h₂.lift (π₂.mapCone s), τ₃ := h₃.lift (π₃.mapCone s), comm₁₂ := ⋯,
      comm₂₃ := ⋯ }

Tactic:
ext

Goal state after:
case h₁
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cone F
h₁ : IsLimit (π₁.mapCone c)
h₂ : IsLimit (π₂.mapCone c)
h₃ : IsLimit (π₃.mapCone c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
⊢ m.τ₁ =
    { τ₁ := h₁.lift (π₁.mapCone s), τ₂ := h₂.lift (π₂.mapCone s), τ₃ := h₃.lift (π₃.mapCone s), comm₁₂ := ⋯,
        comm₂₃ := ⋯ }.τ₁

case h₂
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cone F
h₁ : IsLimit (π₁.mapCone c)
h₂ : IsLimit (π₂.mapCone c)
h₃ : IsLimit (π₃.mapCone c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
⊢ m.τ₂ =
    { τ₁ := h₁.lift (π₁.mapCone s), τ₂ := h₂.lift (π₂.mapCone s), τ₃ := h₃.lift (π₃.mapCone s), comm₁₂ := ⋯,
        comm₂₃ := ⋯ }.τ₂

case h₃
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cone F
h₁ : IsLimit (π₁.mapCone c)
h₂ : IsLimit (π₂.mapCone c)
h₃ : IsLimit (π₃.mapCone c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
⊢ m.τ₃ =
    { τ₁ := h₁.lift (π₁.mapCone s), τ₂ := h₂.lift (π₂.mapCone s), τ₃ := h₃.lift (π₃.mapCone s), comm₁₂ := ⋯,
        comm₂₃ := ⋯ }.τ₃
Module: Mathlib.Algebra.Homology.ShortComplex.Limits

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasLimit (F ⋙ π₁)
inst✝¹ : HasLimit (F ⋙ π₂)
inst✝ : HasLimit (F ⋙ π₃)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ ((const J).obj
            { X₁ := limit (F ⋙ π₁), X₂ := limit (F ⋙ π₂), X₃ := limit (F ⋙ π₃), f := limMap (F.whiskerLeft π₁Toπ₂),
              g := limMap (F.whiskerLeft π₂Toπ₃), zero := ⋯ }).map
        f ≫
      { τ₁ := limit.π (F ⋙ π₁) x✝, τ₂ := limit.π (F ⋙ π₂) x✝, τ₃ := limit.π (F ⋙ π₃) x✝, comm₁₂ := ⋯, comm₂₃ := ⋯ } =
    { τ₁ := limit.π (F ⋙ π₁) x✝¹, τ₂ := limit.π (F ⋙ π₂) x✝¹, τ₃ := limit.π (F ⋙ π₃) x✝¹, comm₁₂ := ⋯, comm₂₃ := ⋯ } ≫
      F.map f

Tactic:
ext

Goal state after:
case h₁
J : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasLimit (F ⋙ π₁)
inst✝¹ : HasLimit (F ⋙ π₂)
inst✝ : HasLimit (F ⋙ π₃)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ (((const J).obj
              { X₁ := limit (F ⋙ π₁), X₂ := limit (F ⋙ π₂), X₃ := limit (F ⋙ π₃), f := limMap (F.whiskerLeft π₁Toπ₂),
                g := limMap (F.whiskerLeft π₂Toπ₃), zero := ⋯ }).map
          f ≫
        { τ₁ := limit.π (F ⋙ π₁) x✝, τ₂ := limit.π (F ⋙ π₂) x✝, τ₃ := limit.π (F ⋙ π₃) x✝, comm₁₂ := ⋯,
          comm₂₃ := ⋯ }).τ₁ =
    ({ τ₁ := limit.π (F ⋙ π₁) x✝¹, τ₂ := limit.π (F ⋙ π₂) x✝¹, τ₃ := limit.π (F ⋙ π₃) x✝¹, comm₁₂ := ⋯, comm₂₃ := ⋯ } ≫
        F.map f).τ₁

case h₂
J : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasLimit (F ⋙ π₁)
inst✝¹ : HasLimit (F ⋙ π₂)
inst✝ : HasLimit (F ⋙ π₃)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ (((const J).obj
              { X₁ := limit (F ⋙ π₁), X₂ := limit (F ⋙ π₂), X₃ := limit (F ⋙ π₃), f := limMap (F.whiskerLeft π₁Toπ₂),
                g := limMap (F.whiskerLeft π₂Toπ₃), zero := ⋯ }).map
          f ≫
        { τ₁ := limit.π (F ⋙ π₁) x✝, τ₂ := limit.π (F ⋙ π₂) x✝, τ₃ := limit.π (F ⋙ π₃) x✝, comm₁₂ := ⋯,
          comm₂₃ := ⋯ }).τ₂ =
    ({ τ₁ := limit.π (F ⋙ π₁) x✝¹, τ₂ := limit.π (F ⋙ π₂) x✝¹, τ₃ := limit.π (F ⋙ π₃) x✝¹, comm₁₂ := ⋯, comm₂₃ := ⋯ } ≫
        F.map f).τ₂

case h₃
J : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasLimit (F ⋙ π₁)
inst✝¹ : HasLimit (F ⋙ π₂)
inst✝ : HasLimit (F ⋙ π₃)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ (((const J).obj
              { X₁ := limit (F ⋙ π₁), X₂ := limit (F ⋙ π₂), X₃ := limit (F ⋙ π₃), f := limMap (F.whiskerLeft π₁Toπ₂),
                g := limMap (F.whiskerLeft π₂Toπ₃), zero := ⋯ }).map
          f ≫
        { τ₁ := limit.π (F ⋙ π₁) x✝, τ₂ := limit.π (F ⋙ π₂) x✝, τ₃ := limit.π (F ⋙ π₃) x✝, comm₁₂ := ⋯,
          comm₂₃ := ⋯ }).τ₃ =
    ({ τ₁ := limit.π (F ⋙ π₁) x✝¹, τ₂ := limit.π (F ⋙ π₂) x✝¹, τ₃ := limit.π (F ⋙ π₃) x✝¹, comm₁₂ := ⋯, comm₂₃ := ⋯ } ≫
        F.map f).τ₃
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
a b c : S₁ ⟶ S₂
⊢ a + b + c = a + (b + c)

Tactic:
ext

Goal state after:
case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
a b c : S₁ ⟶ S₂
⊢ (a + b + c).τ₁ = (a + (b + c)).τ₁

case h₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
a b c : S₁ ⟶ S₂
⊢ (a + b + c).τ₂ = (a + (b + c)).τ₂

case h₃
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
a b c : S₁ ⟶ S₂
⊢ (a + b + c).τ₃ = (a + (b + c)).τ₃
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
a : S₁ ⟶ S₂
⊢ 0 + a = a

Tactic:
ext

Goal state after:
case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
a : S₁ ⟶ S₂
⊢ (0 + a).τ₁ = a.τ₁

case h₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
a : S₁ ⟶ S₂
⊢ (0 + a).τ₂ = a.τ₂

case h₃
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
a : S₁ ⟶ S₂
⊢ (0 + a).τ₃ = a.τ₃
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
a : S₁ ⟶ S₂
⊢ a + 0 = a

Tactic:
ext

Goal state after:
case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
a : S₁ ⟶ S₂
⊢ (a + 0).τ₁ = a.τ₁

case h₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
a : S₁ ⟶ S₂
⊢ (a + 0).τ₂ = a.τ₂

case h₃
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
a : S₁ ⟶ S₂
⊢ (a + 0).τ₃ = a.τ₃
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
a b : S₁ ⟶ S₂
⊢ a - b = a + -b

Tactic:
ext

Goal state after:
case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
a b : S₁ ⟶ S₂
⊢ (a - b).τ₁ = (a + -b).τ₁

case h₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
a b : S₁ ⟶ S₂
⊢ (a - b).τ₂ = (a + -b).τ₂

case h₃
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
a b : S₁ ⟶ S₂
⊢ (a - b).τ₃ = (a + -b).τ₃
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
a : S₁ ⟶ S₂
⊢ -a + a = 0

Tactic:
ext

Goal state after:
case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
a : S₁ ⟶ S₂
⊢ (-a + a).τ₁ = Hom.τ₁ 0

case h₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
a : S₁ ⟶ S₂
⊢ (-a + a).τ₂ = Hom.τ₂ 0

case h₃
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
a : S₁ ⟶ S₂
⊢ (-a + a).τ₃ = Hom.τ₃ 0
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
a b : S₁ ⟶ S₂
⊢ a + b = b + a

Tactic:
ext

Goal state after:
case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
a b : S₁ ⟶ S₂
⊢ (a + b).τ₁ = (b + a).τ₁

case h₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
a b : S₁ ⟶ S₂
⊢ (a + b).τ₂ = (b + a).τ₂

case h₃
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
a b : S₁ ⟶ S₂
⊢ (a + b).τ₃ = (b + a).τ₃
Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
hl : S.LeftHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : S.HasLeftHomology
inst✝ : F.PreservesLeftHomologyOf S
⊢ S.mapCyclesIso F = (hl.map F).cyclesIso ≪≫ F.mapIso hl.cyclesIso.symm

Tactic:
ext

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
hl : S.LeftHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : S.HasLeftHomology
inst✝ : F.PreservesLeftHomologyOf S
⊢ (S.mapCyclesIso F).hom = ((hl.map F).cyclesIso ≪≫ F.mapIso hl.cyclesIso.symm).hom
Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
hl : S.LeftHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : S.HasLeftHomology
inst✝ : F.PreservesLeftHomologyOf S
⊢ S.mapLeftHomologyIso F = (hl.map F).leftHomologyIso ≪≫ F.mapIso hl.leftHomologyIso.symm

Tactic:
ext

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
hl : S.LeftHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : S.HasLeftHomology
inst✝ : F.PreservesLeftHomologyOf S
⊢ (S.map F).leftHomologyπ ≫ (S.mapLeftHomologyIso F).hom =
    (S.map F).leftHomologyπ ≫ ((hl.map F).leftHomologyIso ≪≫ F.mapIso hl.leftHomologyIso.symm).hom
Module: Mathlib.Algebra.Homology.ShortComplex.Limits

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
j : J
⊢ c.ι.app j ≫
      { τ₁ := h₁.desc (π₁.mapCocone s), τ₂ := h₂.desc (π₂.mapCocone s), τ₃ := h₃.desc (π₃.mapCocone s), comm₁₂ := ⋯,
        comm₂₃ := ⋯ } =
    s.ι.app j

Tactic:
ext

Goal state after:
case h₁
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
j : J
⊢ (c.ι.app j ≫
        { τ₁ := h₁.desc (π₁.mapCocone s), τ₂ := h₂.desc (π₂.mapCocone s), τ₃ := h₃.desc (π₃.mapCocone s), comm₁₂ := ⋯,
          comm₂₃ := ⋯ }).τ₁ =
    (s.ι.app j).τ₁

case h₂
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
j : J
⊢ (c.ι.app j ≫
        { τ₁ := h₁.desc (π₁.mapCocone s), τ₂ := h₂.desc (π₂.mapCocone s), τ₃ := h₃.desc (π₃.mapCocone s), comm₁₂ := ⋯,
          comm₂₃ := ⋯ }).τ₂ =
    (s.ι.app j).τ₂

case h₃
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
j : J
⊢ (c.ι.app j ≫
        { τ₁ := h₁.desc (π₁.mapCocone s), τ₂ := h₂.desc (π₂.mapCocone s), τ₃ := h₃.desc (π₃.mapCocone s), comm₁₂ := ⋯,
          comm₂₃ := ⋯ }).τ₃ =
    (s.ι.app j).τ₃
Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
hr : S.RightHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : S.HasRightHomology
inst✝ : F.PreservesRightHomologyOf S
⊢ S.mapOpcyclesIso F = (hr.map F).opcyclesIso ≪≫ F.mapIso hr.opcyclesIso.symm

Tactic:
ext

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
hr : S.RightHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : S.HasRightHomology
inst✝ : F.PreservesRightHomologyOf S
⊢ (S.map F).pOpcycles ≫ (S.mapOpcyclesIso F).hom =
    (S.map F).pOpcycles ≫ ((hr.map F).opcyclesIso ≪≫ F.mapIso hr.opcyclesIso.symm).hom
Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
hr : S.RightHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : S.HasRightHomology
inst✝ : F.PreservesRightHomologyOf S
⊢ S.mapRightHomologyIso F = (hr.map F).rightHomologyIso ≪≫ F.mapIso hr.rightHomologyIso.symm

Tactic:
ext

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
hr : S.RightHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : S.HasRightHomology
inst✝ : F.PreservesRightHomologyOf S
⊢ (S.mapRightHomologyIso F).hom = ((hr.map F).rightHomologyIso ≪≫ F.mapIso hr.rightHomologyIso.symm).hom
Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : HasZeroMorphisms D
S : ShortComplex C
hl : S.LeftHomologyData
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
inst✝² : S.HasHomology
inst✝¹ : (S.map F).HasHomology
inst✝ : F.PreservesLeftHomologyOf S
⊢ S.mapHomologyIso F = (hl.map F).homologyIso ≪≫ F.mapIso hl.homologyIso.symm

Tactic:
ext

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : HasZeroMorphisms D
S : ShortComplex C
hl : S.LeftHomologyData
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
inst✝² : S.HasHomology
inst✝¹ : (S.map F).HasHomology
inst✝ : F.PreservesLeftHomologyOf S
⊢ (S.mapHomologyIso F).hom = ((hl.map F).homologyIso ≪≫ F.mapIso hl.homologyIso.symm).hom
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h₁₂ : Homotopy φ₁ φ₂
h₂₃ : Homotopy φ₂ φ₃
⊢ φ₁.τ₂ = S₁.g ≫ (h₁₂.h₂ + h₂₃.h₂) + (h₁₂.h₁ + h₂₃.h₁) ≫ S₂.f + φ₃.τ₂

Tactic:
rw [h₁₂.comm₂, h₂₃.comm₂, comp_add, add_comp]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h₁₂ : Homotopy φ₁ φ₂
h₂₃ : Homotopy φ₂ φ₃
⊢ S₁.g ≫ h₁₂.h₂ + h₁₂.h₁ ≫ S₂.f + (S₁.g ≫ h₂₃.h₂ + h₂₃.h₁ ≫ S₂.f + φ₃.τ₂) =
    S₁.g ≫ h₁₂.h₂ + S₁.g ≫ h₂₃.h₂ + (h₁₂.h₁ ≫ S₂.f + h₂₃.h₁ ≫ S₂.f) + φ₃.τ₂