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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
P Q : C
f : P ⟶ Q
I : C := Abelian.coimage f
i : Abelian.coimage f ⟶ Q := Abelian.factorThruCoimage f
p : P ⟶ cokernel (kernel.ι f) := cokernel.π (kernel.ι f)
R : C
g : R ⟶ I
hgi : g ≫ i = 0
u : P ⟶ cokernel g := p ≫ cokernel.π g
hu : NormalEpi u
h : NormalEpi.W u ⟶ P := NormalEpi.g
t : cokernel g ⟶ Q
ht : cokernel.π g ≫ t = i
hf : h ≫ f = 0
l : NormalEpi.W u ⟶ kernel f
hl : l ≫ kernel.ι f = h
⊢ (l ≫ kernel.ι f) ≫ p = l ≫ 0

Tactic:
Category.assoc,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
P Q : C
f : P ⟶ Q
I : C := Abelian.coimage f
i : Abelian.coimage f ⟶ Q := Abelian.factorThruCoimage f
p : P ⟶ cokernel (kernel.ι f) := cokernel.π (kernel.ι f)
R : C
g : R ⟶ I
hgi : g ≫ i = 0
u : P ⟶ cokernel g := p ≫ cokernel.π g
hu : NormalEpi u
h : NormalEpi.W u ⟶ P := NormalEpi.g
t : cokernel g ⟶ Q
ht : cokernel.π g ≫ t = i
hf : h ≫ f = 0
l : NormalEpi.W u ⟶ kernel f
hl : l ≫ kernel.ι f = h
⊢ l ≫ kernel.ι f ≫ p = l ≫ 0
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteProducts C
inst✝¹ : HasKernels C
inst✝ : IsNormalMonoCategory C
X Y : C
f : X ⟶ Y
Z : C
l : IsColimit (CokernelCofork.ofπ 0 ⋯)
Z✝ : C
u v : Y ⟶ Z✝
huv : f ≫ u = f ≫ v
W : C
w : Y ⟶ W
hw : equalizer.ι u v ≫ w = 0
hl : IsLimit (KernelFork.ofι (equalizer.ι u v) hw)
m : X ⟶ equalizer u v
hm : m ≫ equalizer.ι u v = f
⊢ (m ≫ equalizer.ι u v) ≫ w = 0

Tactic:
Category.assoc,

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteProducts C
inst✝¹ : HasKernels C
inst✝ : IsNormalMonoCategory C
X Y : C
f : X ⟶ Y
Z : C
l : IsColimit (CokernelCofork.ofπ 0 ⋯)
Z✝ : C
u v : Y ⟶ Z✝
huv : f ≫ u = f ≫ v
W : C
w : Y ⟶ W
hw : equalizer.ι u v ≫ w = 0
hl : IsLimit (KernelFork.ofι (equalizer.ι u v) hw)
m : X ⟶ equalizer u v
hm : m ≫ equalizer.ι u v = f
⊢ m ≫ equalizer.ι u v ≫ w = 0
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hl : IsLimit (KernelFork.ofι (diag A) ⋯) :=
  monoIsKernelOfCokernel (colimit.cocone (parallelPair (diag A) 0)) (colimit.isColimit (parallelPair (diag A) 0))
Z : C
x : Z ⟶ A
hx : x ≫ r A = 0
⊢ (x ≫ prod.lift (𝟙 A) 0) ≫ cokernel.π (diag A) = 0

Tactic:
Category.assoc,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hl : IsLimit (KernelFork.ofι (diag A) ⋯) :=
  monoIsKernelOfCokernel (colimit.cocone (parallelPair (diag A) 0)) (colimit.isColimit (parallelPair (diag A) 0))
Z : C
x : Z ⟶ A
hx : x ≫ r A = 0
⊢ x ≫ prod.lift (𝟙 A) 0 ≫ cokernel.π (diag A) = 0
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hl : IsLimit (KernelFork.ofι (diag A) ⋯) :=
  monoIsKernelOfCokernel (colimit.cocone (parallelPair (diag A) 0)) (colimit.isColimit (parallelPair (diag A) 0))
Z : C
x : Z ⟶ A
hx : x ≫ r A = 0
hxx : (x ≫ prod.lift (𝟙 A) 0) ≫ cokernel.π (diag A) = 0
y : Z ⟶ (KernelFork.ofι (diag A) ⋯).pt
hy : y ≫ diag A = x ≫ prod.lift (𝟙 A) 0
⊢ (x ≫ prod.lift (𝟙 A) 0) ≫ prod.snd = 0

Tactic:
Category.assoc,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hl : IsLimit (KernelFork.ofι (diag A) ⋯) :=
  monoIsKernelOfCokernel (colimit.cocone (parallelPair (diag A) 0)) (colimit.isColimit (parallelPair (diag A) 0))
Z : C
x : Z ⟶ A
hx : x ≫ r A = 0
hxx : (x ≫ prod.lift (𝟙 A) 0) ≫ cokernel.π (diag A) = 0
y : Z ⟶ (KernelFork.ofι (diag A) ⋯).pt
hy : y ≫ diag A = x ≫ prod.lift (𝟙 A) 0
⊢ x ≫ prod.lift (𝟙 A) 0 ≫ prod.snd = 0
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hlp : prod.lift (𝟙 A) 0 ≫ prod.snd = 0
hp1 : IsLimit (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp) :=
  Fork.IsLimit.mk (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp) (fun s ↦ s.ι ≫ prod.fst) ⋯ ⋯
hp2 : IsColimit (CokernelCofork.ofπ prod.snd hlp) := epiIsCokernelOfKernel (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp) hp1
Z : C
z : cokernel (diag A) ⟶ Z
hz : r A ≫ z = 0
h : prod.lift (𝟙 A) 0 ≫ cokernel.π (diag A) ≫ z = 0
t : (CokernelCofork.ofπ prod.snd hlp).pt ⟶ Z
ht : prod.snd ≫ t = cokernel.π (diag A) ≫ z
⊢ (prod.lift (𝟙 A) (𝟙 A) ≫ prod.snd) ≫ t = 0

Tactic:
Category.assoc,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hlp : prod.lift (𝟙 A) 0 ≫ prod.snd = 0
hp1 : IsLimit (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp) :=
  Fork.IsLimit.mk (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp) (fun s ↦ s.ι ≫ prod.fst) ⋯ ⋯
hp2 : IsColimit (CokernelCofork.ofπ prod.snd hlp) := epiIsCokernelOfKernel (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp) hp1
Z : C
z : cokernel (diag A) ⟶ Z
hz : r A ≫ z = 0
h : prod.lift (𝟙 A) 0 ≫ cokernel.π (diag A) ≫ z = 0
t : (CokernelCofork.ofπ prod.snd hlp).pt ⟶ Z
ht : prod.snd ≫ t = cokernel.π (diag A) ≫ z
⊢ prod.lift (𝟙 A) (𝟙 A) ≫ prod.snd ≫ t = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : HasFiniteCoproducts C
inst✝³ : HasCokernels C
inst✝² : IsNormalEpiCategory C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst✝¹ : Epi a
inst✝ : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (coprod.desc f g)
ha' : Cofork.π (CokernelCofork.ofπ a hfa) ≫ a' = cokernel.π (coprod.desc f g)
b' : (CokernelCofork.ofπ b hgb).pt ⟶ cokernel (coprod.desc f g)
hb' : Cofork.π (CokernelCofork.ofπ b hgb) ≫ b' = cokernel.π (coprod.desc f g)
s : PushoutCocone a b
m : cokernel (coprod.desc f g) ⟶ s.pt
h₁ : a' ≫ m = s.inl
x✝ : b' ≫ m = s.inr
⊢ (a ≫ a') ≫ m = a ≫ s.inl

Tactic:
Category.assoc,

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : HasFiniteCoproducts C
inst✝³ : HasCokernels C
inst✝² : IsNormalEpiCategory C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst✝¹ : Epi a
inst✝ : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (coprod.desc f g)
ha' : Cofork.π (CokernelCofork.ofπ a hfa) ≫ a' = cokernel.π (coprod.desc f g)
b' : (CokernelCofork.ofπ b hgb).pt ⟶ cokernel (coprod.desc f g)
hb' : Cofork.π (CokernelCofork.ofπ b hgb) ≫ b' = cokernel.π (coprod.desc f g)
s : PushoutCocone a b
m : cokernel (coprod.desc f g) ⟶ s.pt
h₁ : a' ≫ m = s.inl
x✝ : b' ≫ m = s.inr
⊢ a ≫ a' ≫ m = a ≫ s.inl
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ (a ≫ prod.lift (𝟙 Y) 0) ≫ σ = a

Tactic:
Category.assoc,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ a ≫ prod.lift (𝟙 Y) 0 ≫ σ = a
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ (a ≫ prod.lift (𝟙 Y) (𝟙 Y)) ≫ σ = 0

Tactic:
Category.assoc,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ a ≫ prod.lift (𝟙 Y) (𝟙 Y) ≫ σ = 0
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c d : X ⟶ Y
⊢ (prod.lift (prod.lift a b) (prod.lift c d) ≫ σ) ≫ prod.fst =
    prod.lift (prod.lift a c ≫ σ) (prod.lift b d ≫ σ) ≫ prod.fst

Tactic:
Category.assoc,

Goal state after:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c d : X ⟶ Y
⊢ prod.lift (prod.lift a b) (prod.lift c d) ≫ σ ≫ prod.fst =
    prod.lift (prod.lift a c ≫ σ) (prod.lift b d ≫ σ) ≫ prod.fst
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c d : X ⟶ Y
⊢ (prod.lift (prod.lift a b) (prod.lift c d) ≫ σ) ≫ prod.snd =
    prod.lift (prod.lift a c ≫ σ) (prod.lift b d ≫ σ) ≫ prod.snd

Tactic:
Category.assoc,

Goal state after:
case h₂
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c d : X ⟶ Y
⊢ prod.lift (prod.lift a b) (prod.lift c d) ≫ σ ≫ prod.snd =
    prod.lift (prod.lift a c ≫ σ) (prod.lift b d ≫ σ) ≫ prod.snd
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c d : X ⟶ Y
⊢ (prod.lift (prod.lift a b) (prod.lift c d) ≫ σ) ≫ σ = a - b - (c - d)

Tactic:
Category.assoc,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c d : X ⟶ Y
⊢ prod.lift (prod.lift a b) (prod.lift c d) ≫ σ ≫ σ = a - b - (c - d)
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c : X ⟶ Y
⊢ a - -b + c = a + (b + c)

Tactic:
rw [sub_add, ← add_neg, neg_sub', neg_neg]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
⊢ (prod.lift f g ≫ σ) ≫ h = f ≫ h - g ≫ h

Tactic:
Category.assoc,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
⊢ prod.lift f g ≫ σ ≫ h = f ≫ h - g ≫ h
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
⊢ Abelian.factorThruImage f ≫ equalizer.ι (cokernel.π f) 0 =
    (factorThruImage f ≫ kernel.lift (cokernel.π f) (Limits.image.ι f) ⋯) ≫ equalizer.ι (cokernel.π f) 0

Tactic:
Category.assoc,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ Abelian.factorThruImage f ≫ equalizer.ι (cokernel.π f) 0 =
    factorThruImage f ≫ kernel.lift (cokernel.π f) (Limits.image.ι f) ⋯ ≫ equalizer.ι (cokernel.π f) 0
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (biprod.desc f (-g)) 0
⊢ (s.ι ≫ biprod.fst) ≫ f - (s.ι ≫ biprod.snd) ≫ g = 0

Tactic:
Category.assoc,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (biprod.desc f (-g)) 0
⊢ s.ι ≫ biprod.fst ≫ f - (s.ι ≫ biprod.snd) ≫ g = 0
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (biprod.desc f (-g)) 0
⊢ s.ι ≫ biprod.fst ≫ f - (s.ι ≫ biprod.snd) ≫ g = 0

Tactic:
Category.assoc,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (biprod.desc f (-g)) 0
⊢ s.ι ≫ biprod.fst ≫ f - s.ι ≫ biprod.snd ≫ g = 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 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 : Z ⟶ R
hd : biprod.desc f (-g) ≫ d = biprod.desc 0 e
⊢ (biprod.inl ≫ biprod.desc f (-g)) ≫ d = biprod.inl ≫ u

Tactic:
Category.assoc,

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 : Z ⟶ R
hd : biprod.desc f (-g) ≫ d = biprod.desc 0 e
⊢ biprod.inl ≫ biprod.desc f (-g) ≫ d = biprod.inl ≫ u
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)) ⋯)
d : Z ⟶ R
hd : biprod.desc f (-g) ≫ d = biprod.desc e 0
⊢ (biprod.inr ≫ biprod.desc f (-g)) ≫ d = biprod.inr ≫ u

Tactic:
Category.assoc,

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 : Z ⟶ R
hd : biprod.desc f (-g) ≫ d = biprod.desc e 0
⊢ biprod.inr ≫ biprod.desc f (-g) ≫ d = biprod.inr ≫ u
Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso

Goal state before:
pp: C : Type ?u.2
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : HasZeroMorphisms C
S₁ S₂ S₃ S₄ : ShortComplex C
inst✝³ : S₁.HasHomology
inst✝² : S₂.HasHomology
inst✝¹ : S₃.HasHomology
inst✝ : S₄.HasHomology
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
⊢ S₁.f ≫ φ.τ₂ = 0

Tactic:
by rw [← φ.comm₁₂, hf₂, comp_zero]

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₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
⊢ S₁.f ≫ φ.τ₂ = 0

Tactic:
by rw [← φ.comm₁₂, hf₂, comp_zero]

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.cyclesOpIso.inv ≫ S.op.iCycles = S.pOpcycles.op

Tactic:
dsimp [cyclesOpIso]
  rw [← S.rightHomologyData.op.cyclesIso_hom_comp_i, Iso.inv_hom_id_assoc]
  rfl

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

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
h₁ : IsIso (opcyclesMap φ)
h₂ : Mono φ.τ₃
h : (S₂.homologyι ≫ inv (opcyclesMap φ)) ≫ S₁.fromOpcycles = 0
z : S₂.homology ⟶ (KernelFork.ofι S₁.homologyι ⋯).pt
hz : z ≫ S₁.homologyι = S₂.homologyι ≫ inv (opcyclesMap φ)
⊢ homologyMap φ ≫ z = 𝟙 S₁.homology

Tactic:
rw [← cancel_mono S₁.homologyι, id_comp, assoc, hz, homologyι_naturality_assoc,
      IsIso.hom_inv_id, comp_id]

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
eq₁ : ∀ (j : J), h₁.lift (π₁.mapCone s) ≫ (c.π.app j).τ₁ = (s.π.app j).τ₁
eq₂ : ∀ (j : J), h₂.lift (π₂.mapCone s) ≫ (c.π.app j).τ₂ = (s.π.app j).τ₂
eq₁₂ : ∀ (j : J), (c.π.app j).τ₁ ≫ (F.obj j).f = c.pt.f ≫ (c.π.app j).τ₂
eq₁₂' : ∀ (j : J), (s.π.app j).τ₁ ≫ (F.obj j).f = s.pt.f ≫ (s.π.app j).τ₂
⊢ (h₁.lift (π₁.mapCone s) ≫ c.pt.f) ≫ (c.π.app j).τ₂ = (s.pt.f ≫ h₂.lift (π₂.mapCone s)) ≫ (c.π.app j).τ₂

Tactic:
rw [assoc, assoc, ← eq₁₂, reassoc_of% eq₁, eq₂, eq₁₂']

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₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
h₂' : S₂.RightHomologyData := RightHomologyData.ofEpiOfIsIsoOfMono φ h₁
⊢ IsIso (rightHomologyMap' φ h₁ h₂')

Tactic:
rw [(RightHomologyMapData.ofEpiOfIsIsoOfMono φ h₁).rightHomologyMap'_eq]

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
h₂' : S₂.RightHomologyData := RightHomologyData.ofEpiOfIsIsoOfMono φ h₁
⊢ IsIso (RightHomologyMapData.ofEpiOfIsIsoOfMono φ 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
φ φ' : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ cyclesMap' (φ - φ') h₁ h₂ = cyclesMap' φ h₁ h₂ - cyclesMap' φ' h₁ h₂

Tactic:
by
  simp only [sub_eq_add_neg, cyclesMap'_add, cyclesMap'_neg]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic

Goal state before:
pp: case h
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.PreservesEpimorphisms
P : C
hP : Projective P
E✝ X✝ : D
f : F.obj P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
f' : P ⟶ G.obj E✝
hf' : f' ≫ G.map g = adj.unit.app P ≫ G.map f
⊢ (F.map f' ≫ adj.counit.app E✝) ≫ g = f

Tactic:
Category.assoc,

Goal state after:
case h
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.PreservesEpimorphisms
P : C
hP : Projective P
E✝ X✝ : D
f : F.obj P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
f' : P ⟶ G.obj E✝
hf' : f' ≫ G.map g = adj.unit.app P ≫ G.map f
⊢ F.map f' ≫ adj.counit.app E✝ ≫ g = f
Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : C
i : P ≅ Q
hP : Injective P
X✝ Y✝ : C
g : X✝ ⟶ Q
f : X✝ ⟶ Y✝
mono : Mono f
h : Y✝ ⟶ P
h_eq : f ≫ h = g ≫ i.inv
⊢ (g ≫ i.inv) ≫ i.hom = g

Tactic:
Category.assoc,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : C
i : P ≅ Q
hP : Injective P
X✝ Y✝ : C
g : X✝ ⟶ Q
f : X✝ ⟶ Y✝
mono : Mono f
h : Y✝ ⟶ P
h_eq : f ≫ h = g ≫ i.inv
⊢ g ≫ i.inv ≫ i.hom = g
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₁ : S₁.RightHomologyData
H₂ : S₂.RightHomologyData
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
⊢ H₁.descQ (S₁.g ≫ h₂ ≫ H₂.p) ⋯ ≫ H₂.g' = H₁.g' ≫ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃

Tactic:
rw [← cancel_epi H₁.p, RightHomologyData.p_descQ_assoc, RightHomologyData.p_g'_assoc,
      nullHomotopic_τ₃, comp_add, assoc, assoc, RightHomologyData.p_g', g_h₃, add_zero]

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
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:
by
  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:
by
  apply leftHomologyMap'_nullHomotopic

Goal state after:
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
P Q : MonoOver Y
h : P ≅ Q
i : X ⟶ P.obj.left
w : i ≫ P.arrow = f
⊢ (i ≫ Over.Hom.left h.hom.hom) ≫ Q.arrow = f

Tactic:
Category.assoc,

Goal state after:
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
P Q : MonoOver Y
h : P ≅ Q
i : X ⟶ P.obj.left
w : i ≫ P.arrow = f
⊢ i ≫ Over.Hom.left h.hom.hom ≫ Q.arrow = 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
P Q : MonoOver Y
h : P ≅ Q
i : X ⟶ Q.obj.left
w : i ≫ Q.arrow = f
⊢ (i ≫ Over.Hom.left h.inv.hom) ≫ P.arrow = f

Tactic:
Category.assoc,

Goal state after:
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
P Q : MonoOver Y
h : P ≅ Q
i : X ⟶ Q.obj.left
w : i ≫ Q.arrow = f
⊢ i ≫ Over.Hom.left h.inv.hom ≫ P.arrow = f
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₂ : S₂.Exact
inst✝³ : Epi S₁.g
inst✝² : Epi S₂.g
inst✝¹ : Epi φ.τ₁
inst✝ : Epi φ.τ₃
this✝¹ : Mono S₁.op.f
this✝ : Mono S₂.op.f
this : Mono (opMap φ).τ₁
⊢ Epi φ.τ₂

Tactic:
have : Mono (opMap φ).τ₃ := by dsimp; infer_instance

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₂ : S₂.Exact
inst✝³ : Epi S₁.g
inst✝² : Epi S₂.g
inst✝¹ : Epi φ.τ₁
inst✝ : Epi φ.τ₃
this✝² : Mono S₁.op.f
this✝¹ : Mono S₂.op.f
this✝ : Mono (opMap φ).τ₁
this : Mono (opMap φ).τ₃
⊢ Epi φ.τ₂
Module: Mathlib.CategoryTheory.Subobject.MonoOver

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
f : MonoOver X
⊢ Mono ((Over.post e.functor).obj ((forget X).obj f)).hom

Tactic:
by
      dsimp
      infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝ : HasEqualizer f g
⊢ ((equalizerSubobjectIso f g).hom ≫ equalizer.ι f g) ≫ f = ((equalizerSubobjectIso f g).hom ≫ equalizer.ι f g) ≫ g

Tactic:
Category.assoc,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝ : HasEqualizer f g
⊢ (equalizerSubobjectIso f g).hom ≫ equalizer.ι f g ≫ f = ((equalizerSubobjectIso f g).hom ≫ equalizer.ι f g) ≫ g
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝ : HasEqualizer f g
⊢ (equalizerSubobjectIso f g).hom ≫ equalizer.ι f g ≫ f = ((equalizerSubobjectIso f g).hom ≫ equalizer.ι f g) ≫ g

Tactic:
Category.assoc,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝ : HasEqualizer f g
⊢ (equalizerSubobjectIso f g).hom ≫ equalizer.ι f g ≫ f = (equalizerSubobjectIso f g).hom ≫ equalizer.ι f g ≫ g
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝ : HasEqualizer f g
W : C
h : W ⟶ X
w : (equalizerSubobject f g).Factors h
⊢ ((equalizerSubobject f g).factorThru h w ≫ (equalizerSubobject f g).arrow) ≫ f =
    ((equalizerSubobject f g).factorThru h w ≫ (equalizerSubobject f g).arrow) ≫ g

Tactic:
Category.assoc,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝ : HasEqualizer f g
W : C
h : W ⟶ X
w : (equalizerSubobject f g).Factors h
⊢ (equalizerSubobject f g).factorThru h w ≫ (equalizerSubobject f g).arrow ≫ f =
    ((equalizerSubobject f g).factorThru h w ≫ (equalizerSubobject f g).arrow) ≫ g