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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst✝ : S.HasLeftHomology
x : A ⟶ S.X₁
hx : k = x ≫ S.f
⊢ k ≫ S.g = 0

Tactic:
hx,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst✝ : S.HasLeftHomology
x : A ⟶ S.X₁
hx : k = x ≫ S.f
⊢ (x ≫ S.f) ≫ S.g = 0
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst✝ : S.HasLeftHomology
⊢ S.liftCycles k hk ≫ h.cyclesIso.hom ≫ h.cyclesIso.inv = S.liftCycles k hk

Tactic:
Iso.hom_inv_id,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst✝ : S.HasLeftHomology
⊢ S.liftCycles k hk ≫ 𝟙 S.cycles = S.liftCycles k hk
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₁ S₂ S₃ : ShortComplex C
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst✝ : S.HasRightHomology
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ S.f ≫ k = 0

Tactic:
hx,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst✝ : S.HasRightHomology
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ S.f ≫ S.g ≫ x = 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
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ φ₂.τ₁ = S₁.f ≫ (-h.h₁) + -h.h₀ + φ₁.τ₁

Tactic:
h.comm₁,

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 φ₁ φ₂
⊢ φ₂.τ₁ = S₁.f ≫ (-h.h₁) + -h.h₀ + (S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁)
Module: Mathlib.Algebra.Homology.ShortComplex.Abelian

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
S : ShortComplex C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms D
⊢ S.LeftHomologyData

Tactic:
by
  let γ := kernel.ι S.g ≫ cokernel.π S.f
  let f' := kernel.lift S.g S.f S.zero
  have hf' : f' = kernel.lift γ f' (by simp [γ, f']) ≫ kernel.ι γ := by rw [kernel.lift_ι]
  have wπ : f' ≫ cokernel.π (kernel.ι γ) = 0 := by
    rw [hf']
    simp only [assoc, cokernel.condition, comp_zero]
  let e : Abelian.image S.f ≅ kernel γ :=
    IsLimit.conePointUniqueUpToIso S.abelianImageToKernelIsKernel (limit.isLimit _)
  have he : e.hom ≫ kernel.ι γ = S.abelianImageToKernel :=
    IsLimit.conePointUniqueUpToIso_hom_comp _ _ WalkingParallelPair.zero
  have fac : f' = Abelian.factorThruImage S.f ≫ e.hom ≫ kernel.ι γ := by
    rw [hf', he]
    simp only [γ, f', kernel.lift_ι, abelianImageToKernel, ← cancel_mono (kernel.ι S.g),
      assoc]
  have hπ : IsColimit (CokernelCofork.ofπ _ wπ) :=
    CokernelCofork.IsColimit.ofπ _ _
    (fun x hx => cokernel.desc _ x (by
      simpa only [← cancel_epi e.hom, ← cancel_epi (Abelian.factorThruImage S.f),
        comp_zero, fac, assoc] using hx))
    (fun x hx => cokernel.π_desc _ _ _)
    (fun x hx b hb => coequalizer.hom_ext (by simp only [hb, cokernel.π_desc]))
  exact
    { K := kernel S.g,
      H := Abelian.coimage (kernel.ι S.g ≫ cokernel.π S.f)
      i := kernel.ι _,
      π := cokernel.π _
      wi := kernel.condition _
      hi := kernelIsKernel _
      wπ := wπ
      hπ := hπ }

Goal state after:
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 φ₁ φ₂
⊢ -φ₁.τ₁ = S₁.f ≫ (-h.h₁) + -h.h₀ + -φ₂.τ₁

Tactic:
h.comm₁,

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 φ₁ φ₂
⊢ -(S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁) = S₁.f ≫ (-h.h₁) + -h.h₀ + -φ₂.τ₁
Module: Mathlib.Algebra.Homology.ShortComplex.Abelian

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
S : ShortComplex C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
g' : cokernel S.f ⟶ S.X₃ := cokernel.desc S.f S.g ⋯
hg' : g' = cokernel.π γ ≫ cokernel.desc γ g' ⋯
wι : kernel.ι (cokernel.π γ) ≫ g' = 0
e : cokernel γ ≅ Abelian.coimage S.g :=
  (colimit.isColimit (parallelPair (kernel.ι S.g ≫ cokernel.π S.f) 0)).coconePointUniqueUpToIso
    S.cokernelToAbelianCoimageIsCokernel
⊢ S.RightHomologyData

Tactic:
have he : cokernel.π γ ≫ e.hom = S.cokernelToAbelianCoimage :=
    IsColimit.comp_coconePointUniqueUpToIso_hom _ _ WalkingParallelPair.one

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
S : ShortComplex C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
g' : cokernel S.f ⟶ S.X₃ := cokernel.desc S.f S.g ⋯
hg' : g' = cokernel.π γ ≫ cokernel.desc γ g' ⋯
wι : kernel.ι (cokernel.π γ) ≫ g' = 0
e : cokernel γ ≅ Abelian.coimage S.g :=
  (colimit.isColimit (parallelPair (kernel.ι S.g ≫ cokernel.π S.f) 0)).coconePointUniqueUpToIso
    S.cokernelToAbelianCoimageIsCokernel
he : cokernel.π γ ≫ e.hom = S.cokernelToAbelianCoimage
⊢ S.RightHomologyData
Module: Mathlib.Algebra.Homology.ShortComplex.Abelian

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
S : ShortComplex C
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst✝¹ : Epi π
inst✝ : Mono ι
⊢ π ≫ (isoHomology S hkf hcc fac).hom = (S.isoCyclesOfIsLimit hkf).hom ≫ S.homologyπ

Tactic:
dsimp [isoHomology]
  simp [← cancel_mono (S.homologyIsoImageICyclesCompPOpcycles.hom),
    ← cancel_mono (image.ι (S.iCycles ≫ S.pOpcycles)),
    ← reassoc_of% fac]

Goal state after:
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₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasLeftHomology
inst✝² : S₂.HasLeftHomology
inst✝¹ : F.PreservesLeftHomologyOf S₁
inst✝ : F.PreservesLeftHomologyOf S₂
⊢ cyclesMap (F.mapShortComplex.map φ) ≫ (S₂.mapCyclesIso F).hom ≫ (S₂.mapCyclesIso F).inv =
    (S₁.mapCyclesIso F).hom ≫ (S₁.mapCyclesIso F).inv ≫ cyclesMap (F.mapShortComplex.map φ)

Tactic:
Iso.hom_inv_id,

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₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasLeftHomology
inst✝² : S₂.HasLeftHomology
inst✝¹ : F.PreservesLeftHomologyOf S₁
inst✝ : F.PreservesLeftHomologyOf S₂
⊢ cyclesMap (F.mapShortComplex.map φ) ≫ 𝟙 (F.mapShortComplex.obj S₂).cycles =
    (S₁.mapCyclesIso F).hom ≫ (S₁.mapCyclesIso F).inv ≫ cyclesMap (F.mapShortComplex.map φ)
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₁.f ≫ (h.h₁ + h'.h₁) + (h.h₀ + h'.h₀) + (φ₂.τ₁ + φ₄.τ₁)

Tactic:
h.comm₁,

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₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁ + φ₃.τ₁ = S₁.f ≫ (h.h₁ + h'.h₁) + (h.h₀ + h'.h₀) + (φ₂.τ₁ + φ₄.τ₁)
Module: Mathlib.Algebra.Homology.ShortComplex.Abelian

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
S : ShortComplex C
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst✝¹ : Epi π
inst✝ : Mono ι
⊢ (isoHomology S hkf hcc fac).hom ≫ S.homologyι = ι ≫ (S.isoOpcyclesOfIsColimit hcc).hom

Tactic:
← cancel_mono (S.isoOpcyclesOfIsColimit hcc).inv,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
S : ShortComplex C
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst✝¹ : Epi π
inst✝ : Mono ι
⊢ ((isoHomology S hkf hcc fac).hom ≫ S.homologyι) ≫ (S.isoOpcyclesOfIsColimit hcc).inv =
    (ι ≫ (S.isoOpcyclesOfIsColimit hcc).hom) ≫ (S.isoOpcyclesOfIsColimit hcc).inv
Module: Mathlib.Algebra.Homology.ShortComplex.Abelian

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
S : ShortComplex C
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst✝¹ : Epi π
inst✝ : Mono ι
⊢ (isoHomology S hkf hcc fac).hom ≫ S.homologyι ≫ (S.isoOpcyclesOfIsColimit hcc).inv =
    ι ≫ (S.isoOpcyclesOfIsColimit hcc).hom ≫ (S.isoOpcyclesOfIsColimit hcc).inv

Tactic:
Iso.hom_inv_id,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
S : ShortComplex C
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst✝¹ : Epi π
inst✝ : Mono ι
⊢ (isoHomology S hkf hcc fac).hom ≫ S.homologyι ≫ (S.isoOpcyclesOfIsColimit hcc).inv = ι ≫ 𝟙 cc.pt
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₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasLeftHomology
inst✝² : S₂.HasLeftHomology
inst✝¹ : F.PreservesLeftHomologyOf S₁
inst✝ : F.PreservesLeftHomologyOf S₂
⊢ leftHomologyMap (F.mapShortComplex.map φ) ≫ (S₂.mapLeftHomologyIso F).hom ≫ (S₂.mapLeftHomologyIso F).inv =
    (S₁.mapLeftHomologyIso F).hom ≫ (S₁.mapLeftHomologyIso F).inv ≫ leftHomologyMap (F.mapShortComplex.map φ)

Tactic:
Iso.hom_inv_id,

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₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasLeftHomology
inst✝² : S₂.HasLeftHomology
inst✝¹ : F.PreservesLeftHomologyOf S₁
inst✝ : F.PreservesLeftHomologyOf S₂
⊢ leftHomologyMap (F.mapShortComplex.map φ) ≫ 𝟙 (F.mapShortComplex.obj S₂).leftHomology =
    (S₁.mapLeftHomologyIso F).hom ≫ (S₁.mapLeftHomologyIso F).inv ≫ leftHomologyMap (F.mapShortComplex.map φ)
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₁.f ≫ (h.h₁ - h'.h₁) + (h.h₀ - h'.h₀) + (φ₂.τ₁ - φ₄.τ₁)

Tactic:
h.comm₁,

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₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁ - φ₃.τ₁ = S₁.f ≫ (h.h₁ - h'.h₁) + (h.h₀ - h'.h₀) + (φ₂.τ₁ - φ₄.τ₁)
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₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasRightHomology
inst✝² : S₂.HasRightHomology
inst✝¹ : F.PreservesRightHomologyOf S₁
inst✝ : F.PreservesRightHomologyOf S₂
⊢ opcyclesMap (F.mapShortComplex.map φ) ≫ (S₂.mapOpcyclesIso F).hom ≫ (S₂.mapOpcyclesIso F).inv =
    (S₁.mapOpcyclesIso F).hom ≫ (S₁.mapOpcyclesIso F).inv ≫ opcyclesMap (F.mapShortComplex.map φ)

Tactic:
Iso.hom_inv_id,

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₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasRightHomology
inst✝² : S₂.HasRightHomology
inst✝¹ : F.PreservesRightHomologyOf S₁
inst✝ : F.PreservesRightHomologyOf S₂
⊢ opcyclesMap (F.mapShortComplex.map φ) ≫ 𝟙 (F.mapShortComplex.obj S₂).opcycles =
    (S₁.mapOpcyclesIso F).hom ≫ (S₁.mapOpcyclesIso F).inv ≫ opcyclesMap (F.mapShortComplex.map φ)
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₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasRightHomology
inst✝² : S₂.HasRightHomology
inst✝¹ : F.PreservesRightHomologyOf S₁
inst✝ : F.PreservesRightHomologyOf S₂
⊢ rightHomologyMap (F.mapShortComplex.map φ) ≫ (S₂.mapRightHomologyIso F).hom ≫ (S₂.mapRightHomologyIso F).inv =
    (S₁.mapRightHomologyIso F).hom ≫ (S₁.mapRightHomologyIso F).inv ≫ rightHomologyMap (F.mapShortComplex.map φ)

Tactic:
Iso.hom_inv_id,

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₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasRightHomology
inst✝² : S₂.HasRightHomology
inst✝¹ : F.PreservesRightHomologyOf S₁
inst✝ : F.PreservesRightHomologyOf S₂
⊢ rightHomologyMap (F.mapShortComplex.map φ) ≫ 𝟙 (F.mapShortComplex.obj S₂).rightHomology =
    (S₁.mapRightHomologyIso F).hom ≫ (S₁.mapRightHomologyIso F).inv ≫ rightHomologyMap (F.mapShortComplex.map φ)
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₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁶ : F.PreservesZeroMorphisms
inst✝⁵ : S₁.HasHomology
inst✝⁴ : S₂.HasHomology
inst✝³ : (S₁.map F).HasHomology
inst✝² : (S₂.map F).HasHomology
inst✝¹ : F.PreservesLeftHomologyOf S₁
inst✝ : F.PreservesLeftHomologyOf S₂
⊢ homologyMap (F.mapShortComplex.map φ) ≫ (S₂.mapHomologyIso F).hom ≫ (S₂.mapHomologyIso F).inv =
    (S₁.mapHomologyIso F).hom ≫ (S₁.mapHomologyIso F).inv ≫ homologyMap (F.mapShortComplex.map φ)

Tactic:
Iso.hom_inv_id,

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₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁶ : F.PreservesZeroMorphisms
inst✝⁵ : S₁.HasHomology
inst✝⁴ : S₂.HasHomology
inst✝³ : (S₁.map F).HasHomology
inst✝² : (S₂.map F).HasHomology
inst✝¹ : F.PreservesLeftHomologyOf S₁
inst✝ : F.PreservesLeftHomologyOf S₂
⊢ homologyMap (F.mapShortComplex.map φ) ≫ 𝟙 (S₂.map F).homology =
    (S₁.mapHomologyIso F).hom ≫ (S₁.mapHomologyIso F).inv ≫ homologyMap (F.mapShortComplex.map φ)
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 φ₁ φ₂
ψ : S₃ ⟶ S₁
⊢ ψ.τ₁ ≫ φ₁.τ₁ = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + ψ.τ₁ ≫ φ₂.τ₁

Tactic:
h.comm₁,

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 φ₁ φ₂
ψ : S₃ ⟶ S₁
⊢ ψ.τ₁ ≫ (S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁) = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + ψ.τ₁ ≫ φ₂.τ₁
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₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁶ : F.PreservesZeroMorphisms
inst✝⁵ : S₁.HasHomology
inst✝⁴ : S₂.HasHomology
inst✝³ : (S₁.map F).HasHomology
inst✝² : (S₂.map F).HasHomology
inst✝¹ : F.PreservesRightHomologyOf S₁
inst✝ : F.PreservesRightHomologyOf S₂
⊢ homologyMap (F.mapShortComplex.map φ) ≫ (S₂.mapHomologyIso' F).hom ≫ (S₂.mapHomologyIso' F).inv =
    (S₁.mapHomologyIso' F).hom ≫ (S₁.mapHomologyIso' F).inv ≫ homologyMap (F.mapShortComplex.map φ)

Tactic:
Iso.hom_inv_id,

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₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁶ : F.PreservesZeroMorphisms
inst✝⁵ : S₁.HasHomology
inst✝⁴ : S₂.HasHomology
inst✝³ : (S₁.map F).HasHomology
inst✝² : (S₂.map F).HasHomology
inst✝¹ : F.PreservesRightHomologyOf S₁
inst✝ : F.PreservesRightHomologyOf S₂
⊢ homologyMap (F.mapShortComplex.map φ) ≫ 𝟙 (S₂.map F).homology =
    (S₁.mapHomologyIso' F).hom ≫ (S₁.mapHomologyIso' F).inv ≫ homologyMap (F.mapShortComplex.map φ)
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 φ₁ φ₂
ψ : S₂ ⟶ S₃
⊢ φ₁.τ₁ ≫ ψ.τ₁ = S₁.f ≫ h.h₁ ≫ ψ.τ₁ + h.h₀ ≫ ψ.τ₁ + φ₂.τ₁ ≫ ψ.τ₁

Tactic:
h.comm₁,

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 φ₁ φ₂
ψ : S₂ ⟶ S₃
⊢ (S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁) ≫ ψ.τ₁ = S₁.f ≫ h.h₁ ≫ ψ.τ₁ + h.h₀ ≫ ψ.τ₁ + φ₂.τ₁ ≫ ψ.τ₁
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₂ : ShortComplex C
H₁ : S₁.HomologyData
H₂ : S₂.HomologyData
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
⊢ homologyMap' (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) H₁ H₂ = 0

Tactic:
apply leftHomologyMap'_nullHomotopic

Goal state after:
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₂ : ShortComplex C
inst✝¹ : S₁.HasLeftHomology
inst✝ : S₂.HasLeftHomology
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
⊢ leftHomologyMap (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) = 0

Tactic:
apply leftHomologyMap'_nullHomotopic

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.LeftExact

Goal state before:
pp: C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : Preadditive C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : Preadditive D
F : C ⥤ D
inst✝⁶ : F.PreservesZeroMorphisms
inst✝⁵ : HasBinaryBiproducts C
inst✝⁴ : HasFiniteCoproducts C
inst✝³ : HasCoequalizers C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroObject D
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
this✝¹ : PreservesColimitsOfShape WalkingParallelPair F := preservesCoequalizers_of_preservesCokernels F
this✝ : PreservesColimit (empty C) F := preservesInitialObject_of_preservesZeroMorphisms F
this : PreservesColimitsOfShape (Discrete PEmpty.{1}) F := preservesColimitsOfShape_pempty_of_preservesInitial F
⊢ PreservesFiniteColimits F

Tactic:
let : PreservesFiniteCoproducts F :=
    ⟨fun _ ↦ PreservesFiniteCoproducts.of_preserves_binary_and_initial F _⟩

Goal state after:
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : Preadditive C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : Preadditive D
F : C ⥤ D
inst✝⁶ : F.PreservesZeroMorphisms
inst✝⁵ : HasBinaryBiproducts C
inst✝⁴ : HasFiniteCoproducts C
inst✝³ : HasCoequalizers C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroObject D
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
this✝² : PreservesColimitsOfShape WalkingParallelPair F := preservesCoequalizers_of_preservesCokernels F
this✝¹ : PreservesColimit (empty C) F := preservesInitialObject_of_preservesZeroMorphisms F
this✝ : PreservesColimitsOfShape (Discrete PEmpty.{1}) F := preservesColimitsOfShape_pempty_of_preservesInitial F
this : PreservesFiniteCoproducts F :=
  { preserves := fun x ↦ PreservesFiniteCoproducts.of_preserves_binary_and_initial F (Fin x) }
⊢ PreservesFiniteColimits F
Module: Mathlib.CategoryTheory.Subobject.FactorThru

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
P : Subobject Y
f : X ⟶ Y
⊢ ∀ (a b : MonoOver Y), (isIsomorphicSetoid (MonoOver Y)) a b → a.Factors f = b.Factors f

Tactic:
by
      rintro P Q ⟨h⟩
      apply propext
      constructor
      · rintro ⟨i, w⟩
        exact ⟨i ≫ h.hom.hom.left, by rw [Category.assoc, Over.w h.hom.hom, w]⟩
      · rintro ⟨i, w⟩
        exact ⟨i ≫ h.inv.hom.left, by rw [Category.assoc, Over.w h.inv.hom, w]⟩

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
x✝¹ : Cᵒᵖ
x✝ : Subobject (Opposite.unop x✝¹)
⊢ (ConcreteCategory.hom (↾(pullback (𝟙 x✝¹).unop).obj)).toFun x✝ =
    (ConcreteCategory.hom (𝟙 (Subobject (Opposite.unop x✝¹)))).toFun x✝

Tactic:
simp [pullback_id]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
h : kernel.ι S.g ≫ cokernel.π S.f = 0
W'✝ : C
x✝² : W'✝ ⟶ S.X₂
x✝¹ : x✝² ≫ S.g = 0
x✝ : W'✝ ⟶ Abelian.image S.f
hm : x✝ ≫ Abelian.image.ι S.f = x✝²
⊢ x✝ = kernel.lift (cokernel.π S.f) x✝² ⋯

Tactic:
rw [← cancel_mono (Abelian.image.ι S.f), hm, kernel.lift_ι]

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

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✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
tfae_1_to_2 :
  (∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Epi (F.map S.g)) →
    ∀ (S : ShortComplex C), S.Exact ∧ Epi S.g → (S.map F).Exact ∧ Epi (F.map S.g)
tfae_2_to_3 :
  (∀ (S : ShortComplex C), S.Exact ∧ Epi S.g → (S.map F).Exact ∧ Epi (F.map S.g)) →
    ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
x✝ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
hF : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F := x✝
⊢ PreservesFiniteColimits F

Tactic:
by
    exact preservesFiniteColimits_of_preservesCokernels F

Goal state after: