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

Goal state before:
pp: case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Epi f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
aux :
  ∀ (s : CokernelCofork (kernel.ι f)),
    Cofork.π (CokernelCofork.ofπ f ⋯) ≫
        inv (imageMonoFactorisation f).m ≫
          inv (coimageImageComparison f) ≫ colimit.desc (parallelPair (kernel.ι f) 0) s =
      Cofork.π s
⊢ ∀ (s : CokernelCofork (kernel.ι f)) (m_1 : (CokernelCofork.ofπ f ⋯).pt ⟶ s.pt),
    Cofork.π (CokernelCofork.ofπ f ⋯) ≫ m_1 = Cofork.π s →
      m_1 =
        inv (imageMonoFactorisation f).m ≫ inv (coimageImageComparison f) ≫ colimit.desc (parallelPair (kernel.ι f) 0) s

Tactic:
intro A g hg

Goal state after:
case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Epi f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
aux :
  ∀ (s : CokernelCofork (kernel.ι f)),
    Cofork.π (CokernelCofork.ofπ f ⋯) ≫
        inv (imageMonoFactorisation f).m ≫
          inv (coimageImageComparison f) ≫ colimit.desc (parallelPair (kernel.ι f) 0) s =
      Cofork.π s
A : CokernelCofork (kernel.ι f)
g : (CokernelCofork.ofπ f ⋯).pt ⟶ A.pt
hg : Cofork.π (CokernelCofork.ofπ f ⋯) ≫ g = Cofork.π A
⊢ g = inv (imageMonoFactorisation f).m ≫ inv (coimageImageComparison f) ≫ colimit.desc (parallelPair (kernel.ι f) 0) A
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Abelian C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : HasZeroMorphisms D
X Y : D
i : X ⟶ Y
inst✝³ : HasCokernel i
F : D ⥤ C
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : Mono (F.map i)
inst✝ : PreservesColimit (parallelPair i 0) F
⊢ (parallelPair (cokernel.π (F.map i)) 0).map WalkingParallelPairHom.left ≫ (asIso (cokernelComparison i F)).hom =
    (Iso.refl ((parallelPair (cokernel.π (F.map i)) 0).obj WalkingParallelPair.zero)).hom ≫
      (parallelPair (cokernel.π i) 0 ⋙ F).map WalkingParallelPairHom.left

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Abelian C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : HasZeroMorphisms D
X Y : D
i : X ⟶ Y
inst✝³ : HasCokernel i
F : D ⥤ C
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : Mono (F.map i)
inst✝ : PreservesColimit (parallelPair i 0) F
⊢ (parallelPair (cokernel.π (F.map i)) 0).map WalkingParallelPairHom.right ≫ (asIso (cokernelComparison i F)).hom =
    (Iso.refl ((parallelPair (cokernel.π (F.map i)) 0).obj WalkingParallelPair.zero)).hom ≫
      (parallelPair (cokernel.π i) 0 ⋙ F).map WalkingParallelPairHom.right

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Abelian C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : HasZeroMorphisms D
X Y : D
p : X ⟶ Y
inst✝³ : HasKernel p
F : D ⥤ C
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : Epi (F.map p)
inst✝ : PreservesLimit (parallelPair p 0) F
⊢ (parallelPair (kernel.ι p) 0 ⋙ F).map WalkingParallelPairHom.left ≫
      (Iso.refl ((parallelPair (kernel.ι p) 0 ⋙ F).obj WalkingParallelPair.one)).hom =
    (asIso (kernelComparison p F)).hom ≫ (parallelPair (kernel.ι (F.map p)) 0).map WalkingParallelPairHom.left

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Abelian C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : HasZeroMorphisms D
X Y : D
p : X ⟶ Y
inst✝³ : HasKernel p
F : D ⥤ C
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : Epi (F.map p)
inst✝ : PreservesLimit (parallelPair p 0) F
⊢ (parallelPair (kernel.ι p) 0 ⋙ F).map WalkingParallelPairHom.right ≫
      (Iso.refl ((parallelPair (kernel.ι p) 0 ⋙ F).obj WalkingParallelPair.one)).hom =
    (asIso (kernelComparison p F)).hom ≫ (parallelPair (kernel.ι (F.map p)) 0).map WalkingParallelPairHom.right

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi f
R : C
e : Y ⟶ R
h : pullback.snd f g ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc 0 e
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this : IsColimit (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯)
⊢ e = 0

Tactic:
obtain ⟨d, hd⟩ := CokernelCofork.IsColimit.desc' this u hu

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi f
R : C
e : Y ⟶ R
h : pullback.snd f g ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc 0 e
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this : IsColimit (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯)
d : (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯).pt ⟶ R
hd : Cofork.π (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯) ≫ d = u
⊢ e = 0
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi g
R : C
e : X ⟶ R
h : pullback.fst f g ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc e 0
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this : IsColimit (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯)
⊢ e = 0

Tactic:
obtain ⟨d, hd⟩ := CokernelCofork.IsColimit.desc' this u hu

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi g
R : C
e : X ⟶ R
h : pullback.fst f g ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc e 0
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this : IsColimit (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯)
d : (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯).pt ⟶ R
hd : Cofork.π (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯) ≫ d = u
⊢ e = 0
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
x : ↑B
hx : x ∈ (Hom.hom f).range
b : ↑B
hb : b ∉ (Hom.hom f).range
⊢ fromCoset ⟨b • ↑(Hom.hom f).range, ⋯⟩ ≠ ∞

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
x : ↑B
hx : x ∈ (Hom.hom f).range
b : ↑B
hb : b ∉ (Hom.hom f).range
⊢ fromCoset ⟨(x * b) • ↑(Hom.hom f).range, ⋯⟩ ≠ ∞

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
inst✝ : Epi f
⊢ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
dsimp [Function.Surjective]
  by_contra! ⟨b, hb⟩
  exact
    SurjectiveOfEpiAuxs.g_ne_h f b (fun ⟨c, hc⟩ => hb _ hc)
      (congr_arg GrpCat.Hom.hom ((cancel_epi f).1 (SurjectiveOfEpiAuxs.comp_eq f)))

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{?u.4, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteProducts C
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), Nonempty (AbelianStruct f)
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Mono f
hf : AbelianStruct f
⊢ f ≫ Cofork.π hf.cokernelCofork = 0

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{?u.4, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteProducts C
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), Nonempty (AbelianStruct f)
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Epi f
hf : AbelianStruct f
⊢ Fork.ι hf.kernelFork ≫ f = 0

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{?u.4, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteProducts C
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), Nonempty (AbelianStruct f)
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Epi f
hf : AbelianStruct f
⊢ Cofork.π hf.cokernelCofork = 0

Tactic:
by simp [← cancel_epi f]

Goal state after:
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₂
inst✝ : QuasiIso φ
⊢ QuasiIso (opMap φ)

Tactic:
rw [quasiIso_opMap_iff]

Goal state after:
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₂
inst✝ : QuasiIso φ
⊢ QuasiIso φ
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ S₄ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
h : S.HomologyData
⊢ (h.right.op.π ≫ h.iso.op.hom ≫ h.left.op.ι).unop = (h.right.op.i ≫ h.left.op.p).unop

Tactic:
by simp

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₁ S₂ S₃ S₄ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
S : ShortComplex Cᵒᵖ
h : S.HomologyData
⊢ (h.right.unop.π ≫ h.iso.unop.hom ≫ h.left.unop.ι).op = (h.right.unop.i ≫ h.left.unop.p).op

Tactic:
by simp

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₁ S₂ S₃ : ShortComplex C
h : S.RightHomologyData
A : C
hf : S.f = 0
c : KernelFork S.g
hc : IsLimit c
⊢ (Iso.refl c.pt).hom ≫ Fork.ι (KernelFork.ofι (Fork.ι c) ⋯) = Fork.ι c

Tactic:
by simp

Goal state after:
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 K' H' : C
eK : K' ≅ h.K
eH : H' ≅ h.H
⊢ eK.hom ≫ h.i ≫ S.g = 0

Tactic:
h.wi,

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 K' H' : C
eK : K' ≅ h.K
eH : H' ≅ h.H
⊢ eK.hom ≫ 0 = 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 S₁ S₂ S₃ : ShortComplex C
h : S.LeftHomologyData
A K' H' : C
eK : K' ≅ h.K
eH : H' ≅ h.H
⊢ eK.hom ≫ Fork.ι (KernelFork.ofι h.i ⋯) = eK.hom ≫ h.i

Tactic:
by simp

Goal state after:
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 K' H' : C
eK : K' ≅ h.K
eH : H' ≅ h.H
⊢ (parallelPair (h.hi.lift (KernelFork.ofι S.f ⋯)) 0).map WalkingParallelPairHom.right ≫ eK.symm.hom =
    (Iso.refl S.X₁).hom ≫
      (parallelPair ((IsKernel.isoKernel S.g (eK.hom ≫ h.i) h.hi eK ⋯).lift (KernelFork.ofι S.f ⋯)) 0).map
        WalkingParallelPairHom.right

Tactic:
by simp

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₁ S₂ S₃ : ShortComplex C
h : S.RightHomologyData
A : C
hg : S.g = 0
c : CokernelCofork S.f
hc : IsColimit c
⊢ Cofork.π c ≫ (Iso.refl c.pt).hom = Cofork.π (CokernelCofork.ofπ (Cofork.π c) ⋯)

Tactic:
by simp

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₁ S₂ S₃ : ShortComplex C
h : S.RightHomologyData
A Q' H' : C
eQ : Q' ≅ h.Q
eH : H' ≅ h.H
⊢ Cofork.π (CokernelCofork.ofπ h.p ⋯) ≫ eQ.symm.hom = h.p ≫ eQ.inv

Tactic:
by simp

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₁ S₂ S₃ S₄ : ShortComplex C
φ : S₁ ⟶ S₂
h₁✝ : S₁.HomologyData
h₂✝ : S₂.HomologyData
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
⊢ h₁.f' ≫ h₁.i ≫ h₂.p = 0

Tactic:
by simp

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₁ S₂ S₃ : ShortComplex C
h : S.RightHomologyData
A Q' H' : C
eQ : Q' ≅ h.Q
eH : H' ≅ h.H
⊢ (parallelPair (h.hp.desc (CokernelCofork.ofπ S.g ⋯)) 0).map WalkingParallelPairHom.right ≫ (Iso.refl S.X₃).hom =
    eQ.symm.hom ≫
      (parallelPair ((IsCokernel.cokernelIso S.f (h.p ≫ eQ.inv) h.hp eQ.symm ⋯).desc (CokernelCofork.ofπ S.g ⋯)) 0).map
        WalkingParallelPairHom.right

Tactic:
by simp

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₁ S₂ S₃ S₄ : ShortComplex C
φ : S₁ ⟶ S₂
h₁✝ : S₁.HomologyData
h₂✝ : S₂.HomologyData
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
⊢ (h₁.i ≫ h₂.p) ≫ h₂.g' = 0

Tactic:
by simp

Goal state after:
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
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₂.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₂.f ⋯)
hf' : φ.τ₁ ≫ f' = h.f'
wπ : f' ≫ h.π = 0
Z'✝ : C
x : h.K ⟶ Z'✝
hx : f' ≫ x = 0
⊢ h.π ≫ h.descH x ⋯ = x

Tactic:
by simp

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₂ S₃ : ShortComplex C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
h₃ : S₃.RightHomologyData
γ₁ : RightHomologyMapData φ₁ h₁ h₂ := rightHomologyMapData φ₁ h₁ h₂
γ₂ : RightHomologyMapData φ₂ h₂ h₃ := rightHomologyMapData φ₂ h₂ h₃
⊢ opcyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = γ₁.φQ ≫ γ₂.φQ

Tactic:
(γ₁.comp γ₂).opcyclesMap'_eq,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
h₃ : S₃.RightHomologyData
γ₁ : RightHomologyMapData φ₁ h₁ h₂ := rightHomologyMapData φ₁ h₁ h₂
γ₂ : RightHomologyMapData φ₂ h₂ h₃ := rightHomologyMapData φ₂ h₂ h₃
⊢ (γ₁.comp γ₂).φQ = γ₁.φQ ≫ γ₂.φQ
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ S₄ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
A : C
inst✝ : S.HasHomology
⊢ S.rightHomologyIso.hom ≫ Fork.ι (KernelFork.ofι S.homologyι ⋯) = Fork.ι (KernelFork.ofι S.rightHomologyι ⋯)

Tactic:
by simp

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₁✝ S₂✝ S₃ S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
ψ : LeftHomologyMapData φ h₁ h₂
⊢ (h₂.op.p ≫ ψ.φK.op).unop = ((opMap φ).τ₂ ≫ h₁.op.p).unop

Tactic:
by simp

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₁✝ S₂✝ S₃ S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
ψ : LeftHomologyMapData φ h₁ h₂
⊢ (ψ.φK.op ≫ h₁.op.g').unop = (h₂.op.g' ≫ (opMap φ).τ₃).unop

Tactic:
by simp

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₁✝ S₂✝ S₃ S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
ψ : LeftHomologyMapData φ h₁ h₂
⊢ (ψ.φH.op ≫ h₁.op.ι).unop = (h₂.op.ι ≫ ψ.φK.op).unop

Tactic:
by simp

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₁✝ S₂✝ S₃ : ShortComplex C
S₁ S₂ : ShortComplex Cᵒᵖ
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
ψ : LeftHomologyMapData φ h₁ h₂
⊢ (h₂.unop.p ≫ ψ.φK.unop).op = ((unopMap φ).τ₂ ≫ h₁.unop.p).op

Tactic:
by simp

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₁✝ S₂✝ S₃ : ShortComplex C
S₁ S₂ : ShortComplex Cᵒᵖ
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
ψ : LeftHomologyMapData φ h₁ h₂
⊢ (ψ.φK.unop ≫ h₁.unop.g').op = (h₂.unop.g' ≫ (unopMap φ).τ₃).op

Tactic:
by simp

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₁✝ S₂✝ S₃ : ShortComplex C
S₁ S₂ : ShortComplex Cᵒᵖ
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
ψ : LeftHomologyMapData φ h₁ h₂
⊢ (ψ.φH.unop ≫ h₁.unop.ι).op = (h₂.unop.ι ≫ ψ.φK.unop).op

Tactic:
by simp

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₁✝ S₂✝ S₃ S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
ψ : RightHomologyMapData φ h₁ h₂
⊢ (ψ.φQ.op ≫ h₁.op.i).unop = (h₂.op.i ≫ (opMap φ).τ₂).unop

Tactic:
by simp

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₁✝ S₂✝ S₃ S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
ψ : RightHomologyMapData φ h₁ h₂
⊢ (h₂.op.f' ≫ ψ.φQ.op).unop = ((opMap φ).τ₁ ≫ h₁.op.f').unop

Tactic:
by simp

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₁✝ S₂✝ S₃ S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
ψ : RightHomologyMapData φ h₁ h₂
⊢ (h₂.op.π ≫ ψ.φH.op).unop = (ψ.φQ.op ≫ h₁.op.π).unop

Tactic:
by simp

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₁✝ S₂✝ S₃ : ShortComplex C
S₁ S₂ : ShortComplex Cᵒᵖ
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
ψ : RightHomologyMapData φ h₁ h₂
⊢ (ψ.φQ.unop ≫ h₁.unop.i).op = (h₂.unop.i ≫ (unopMap φ).τ₂).op

Tactic:
by simp

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₁✝ S₂✝ S₃ : ShortComplex C
S₁ S₂ : ShortComplex Cᵒᵖ
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
ψ : RightHomologyMapData φ h₁ h₂
⊢ (h₂.unop.f' ≫ ψ.φQ.unop).op = ((unopMap φ).τ₁ ≫ h₁.unop.f').op

Tactic:
by simp

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₁✝ S₂✝ S₃ : ShortComplex C
S₁ S₂ : ShortComplex Cᵒᵖ
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
ψ : RightHomologyMapData φ h₁ h₂
⊢ (h₂.unop.π ≫ ψ.φH.unop).op = (ψ.φQ.unop ≫ h₁.unop.π).op

Tactic:
by simp

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 : ShortComplex C
inst✝ : S.HasRightHomology
⊢ S.fromOpcycles.op ≫ S.cyclesOpIso.inv = S.op.toCycles

Tactic:
dsimp [cyclesOpIso, fromOpcycles]
  rw [← cancel_mono S.op.iCycles, assoc, toCycles_i,
    LeftHomologyData.cyclesIso_inv_comp_iCycles, RightHomologyData.op_i,
    ← op_comp, RightHomologyData.p_g', op_f]

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₁ S₂ : ShortComplex C
h : S.LeftHomologyData
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : h.IsPreservedBy F
this✝ : PreservesLimit (parallelPair S.g 0) F
this : PreservesColimit (parallelPair h.f' 0) F
⊢ F.map (h.i ≫ S.g) = 0

Tactic:
h.wi,

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₁ S₂ : ShortComplex C
h : S.LeftHomologyData
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : h.IsPreservedBy F
this✝ : PreservesLimit (parallelPair S.g 0) F
this : PreservesColimit (parallelPair h.f' 0) F
⊢ F.map 0 = 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 S₁ S₂ S₃ : ShortComplex C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst✝¹ : S.HasLeftHomology
inst✝ : HasKernel S.g
⊢ S.iCycles ≫ S.g = 0

Tactic:
by simp

Goal state after:
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
inst✝ : HasKernel S.g
⊢ kernel.ι S.g ≫ S.g = 0

Tactic:
by simp

Goal state after:
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
inst✝ : S.HasLeftHomology
⊢ S.f = 𝟙 S.X₁ ≫ S.f

Tactic:
by rw [id_comp]

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₁ S₂ : ShortComplex C
h : S.LeftHomologyData
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : h.IsPreservedBy F
this✝ : PreservesLimit (parallelPair S.g 0) F
this : PreservesColimit (parallelPair h.f' 0) F
wi : F.map h.i ≫ F.map S.g = 0
hi : IsLimit ((KernelFork.ofι h.i ⋯).map F)
f' : F.obj S.X₁ ⟶ F.obj h.K := hi.lift (KernelFork.ofι (S.map F).f ⋯)
hf' : f' = F.map h.f'
wπ : f' ≫ F.map h.π = 0
⊢ (parallelPair f' 0).map WalkingParallelPairHom.right ≫
      (Iso.refl ((parallelPair f' 0).obj WalkingParallelPair.one)).hom =
    (Iso.refl ((parallelPair f' 0).obj WalkingParallelPair.zero)).hom ≫
      (parallelPair (F.map h.f') 0).map WalkingParallelPairHom.right

Tactic:
by simp

Goal state after:
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
inst✝¹ : S.HasLeftHomology
inst✝ : HasKernel S.g
h : S.LeftHomologyData := S.leftHomologyData
this : HasColimit (parallelPair h.f' 0)
⊢ (parallelPair (kernel.lift S.g S.f ⋯) 0).map WalkingParallelPairHom.right ≫
      ((kernelIsKernel S.g).conePointUniqueUpToIso h.hi).hom =
    (Iso.refl ((parallelPair (kernel.lift S.g S.f ⋯) 0).obj WalkingParallelPair.zero)).hom ≫
      (parallelPair h.f' 0).map WalkingParallelPairHom.right

Tactic:
by simp

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₁ S₂ S₃ S₄ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
A : C
inst✝ : S.HasHomology
⊢ S.iCycles ≫ S.g = 0

Tactic:
by simp

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₁ S₂ S₃ S₄ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
A : C
inst✝ : S.HasHomology
⊢ S.f ≫ S.pOpcycles = 0

Tactic:
by simp

Goal state after: