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

Goal state before:
pp: case h_snd
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
inst✝ : CartesianMonoidalCategory D
F : C ⥤ D
A B A' B' : C
f : A ⟶ A'
g : B ⟶ B'
⊢ (F.map (f ⊗ₘ g) ≫ prodComparison F A' B') ≫ snd (F.obj A') (F.obj B') =
    (prodComparison F A B ≫ (F.map f ⊗ₘ F.map g)) ≫ snd (F.obj A') (F.obj B')

Tactic:
simp only [Category.assoc, prodComparison_fst, tensorHom_fst, prodComparison_fst_assoc,
    prodComparison_snd, tensorHom_snd, prodComparison_snd_assoc, ← F.map_comp]

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a : A
⊢ counit ((antipode R) a) = ∑ x ∈ (ℛ R a).index, counit ((ℛ R a).left x) * counit ((antipode R) ((ℛ R a).right x))

Tactic:
← smul_eq_mul,

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a : A
⊢ counit ((antipode R) a) = ∑ x ∈ (ℛ R a).index, counit ((ℛ R a).left x) • counit ((antipode R) ((ℛ R a).right x))
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
A B : C
inst✝² : GrpObj A
inst✝¹ : GrpObj B
f : A ⟶ B
inst✝ : IsMonHom f
⊢ lift f (ι ≫ f) ≫ μ = toUnit A ≫ η

Tactic:
have := right_inv A =≫ f

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
A B : C
inst✝² : GrpObj A
inst✝¹ : GrpObj B
f : A ⟶ B
inst✝ : IsMonHom f
this : (lift (𝟙 A) ι ≫ μ) ≫ f = (toUnit A ≫ η) ≫ f
⊢ lift f (ι ≫ f) ≫ μ = toUnit A ≫ η
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
A B : C
inst✝² : GrpObj A
inst✝¹ : GrpObj B
f : A ⟶ B
inst✝ : IsMonHom f
⊢ lift (lift f (ι ≫ f)) f = lift (lift f (f ≫ ι)) f

Tactic:
apply (isPullback B).hom_ext

Goal state after:
case h₀
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
A B : C
inst✝² : GrpObj A
inst✝¹ : GrpObj B
f : A ⟶ B
inst✝ : IsMonHom f
⊢ lift (lift f (ι ≫ f)) f ≫ μ ▷ B = lift (lift f (f ≫ ι)) f ≫ μ ▷ B

case h₁
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
A B : C
inst✝² : GrpObj A
inst✝¹ : GrpObj B
f : A ⟶ B
inst✝ : IsMonHom f
⊢ lift (lift f (ι ≫ f)) f ≫ (α_ B B B).hom ≫ B ◁ μ = lift (lift f (f ≫ ι)) f ≫ (α_ B B B).hom ≫ B ◁ μ
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : CartesianMonoidalCategory C
G✝ X : C
inst✝¹ : GrpObj G✝
A B G : C
inst✝ : MonObj G
h : (X : C) → (f : X ⟶ G) → Invertible f
⊢ lift (Yoneda.fullyFaithful.preimage { app := fun X ↦ ↾fun f ↦ ⅟f, naturality := ⋯ }) (𝟙 G) ≫ μ = toUnit G ≫ η

Tactic:
by simp [Yoneda.fullyFaithful_preimage, ← Hom.mul_def, Hom.one_def]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : CartesianMonoidalCategory C
G✝ X : C
inst✝¹ : GrpObj G✝
A B G : C
inst✝ : MonObj G
h : (X : C) → (f : X ⟶ G) → Invertible f
⊢ lift (𝟙 G) (Yoneda.fullyFaithful.preimage { app := fun X ↦ ↾fun f ↦ ⅟f, naturality := ⋯ }) ≫ μ = toUnit G ≫ η

Tactic:
by simp [Yoneda.fullyFaithful_preimage, ← Hom.mul_def, Hom.one_def]

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
inst✝ : Fintype ι
f : Dual R M
m : M
⊢ ∑ x, (b.coord x) m * f (b x) = f m

Tactic:
← smul_eq_mul,

Goal state after:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
inst✝ : Fintype ι
f : Dual R M
m : M
⊢ ∑ x, (b.coord x) m • f (b x) = f m
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
l : Dual R M
i : ι
⊢ ((Finsupp.linearCombination R ⇑b.dualBasis) (b.dualBasis.repr l)) (b i) = l (b i)

Tactic:
Basis.linearCombination_repr b.dualBasis l

Goal state after:
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
l : Dual R M
i : ι
⊢ l (b i) = l (b i)
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
i j : ι
⊢ (h.basis.repr (e i)) j = (Finsupp.single i 1) j

Tactic:
rcases eq_or_ne i j with rfl | hne

Goal state after:
case inl
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
i : ι
⊢ (h.basis.repr (e i)) i = (Finsupp.single i 1) i

case inr
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
i j : ι
hne : i ≠ j
⊢ (h.basis.repr (e i)) j = (Finsupp.single i 1) j
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₃ : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
I : R →+* R
B : M →ₗ[R] M →ₛₗ[I] M₃
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃
f : M →ₗ[R] M₁
g : M₁ →ₗ[R] M
h : B' ∘ₗ f = B.compl₂ g
⊢ B.IsAdjointPair B' ⇑f ⇑g

Tactic:
· intro _ _
    rw [← compl₂_apply, ← comp_apply, h]

Goal state after:
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup M₁
inst✝² : Module R M₁
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
B F : M →ₗ[R] M →ₗ[R] M₂
e : M₁ ≃ₗ[R] M
f : End R M
hₗ : F.compl₁₂ ↑e ↑e ∘ₗ e.symm.conj f = (F ∘ₗ f).compl₁₂ ↑e ↑e
hᵣ : (B.compl₁₂ ↑e ↑e).compl₂ (e.symm.conj f) = (B.compl₂ f).compl₁₂ ↑e ↑e
he : Function.Surjective ⇑↑e
⊢ F ∘ₗ f = B.compl₂ f ↔ F.compl₁₂ ↑e ↑e ∘ₗ e.symm.conj f = (B.compl₁₂ ↑e ↑e).compl₂ (e.symm.conj f)

Tactic:
hₗ,

Goal state after:
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup M₁
inst✝² : Module R M₁
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
B F : M →ₗ[R] M →ₗ[R] M₂
e : M₁ ≃ₗ[R] M
f : End R M
hₗ : F.compl₁₂ ↑e ↑e ∘ₗ e.symm.conj f = (F ∘ₗ f).compl₁₂ ↑e ↑e
hᵣ : (B.compl₁₂ ↑e ↑e).compl₂ (e.symm.conj f) = (B.compl₂ f).compl₁₂ ↑e ↑e
he : Function.Surjective ⇑↑e
⊢ F ∘ₗ f = B.compl₂ f ↔ (F ∘ₗ f).compl₁₂ ↑e ↑e = (B.compl₁₂ ↑e ↑e).compl₂ (e.symm.conj f)
Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers

Goal state before:
pp: case h₁
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
c : Cone F
m✝ : c.pt ⟶ (equalizerCone F).pt
J : ∀ (j : WalkingParallelPair), m✝ ≫ (equalizerCone F).π.app j = c.π.app j
J0 : m✝ ≫ (equalizerCone F).π.app WalkingParallelPair.zero = c.π.app WalkingParallelPair.zero
⊢ m✝ ≫
      pullback.snd (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
        (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) =
    pullback.lift (c.π.app WalkingParallelPair.zero) (c.π.app WalkingParallelPair.zero) ⋯ ≫
      pullback.snd (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
        (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right))

Tactic:
simp [← J0, pullbackFst_eq_pullback_snd]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f g : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = h ≫ g
inst✝¹ : HasEqualizer f g
inst✝ : PreservesLimit (parallelPair f g) G
⊢ G.map (equalizer.ι f g ≫ f) = G.map (equalizer.ι f g ≫ g)

Tactic:
rw [equalizer.condition]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasCoequalizer (G.map f) (G.map g)
i : IsIso (coequalizerComparison f g G)
⊢ PreservesColimit (parallelPair f g) G

Tactic:
apply preservesColimit_of_preserves_colimit_cocone (coequalizerIsCoequalizer f g)

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasCoequalizer (G.map f) (G.map g)
i : IsIso (coequalizerComparison f g G)
⊢ IsColimit (G.mapCocone (Cofork.ofπ (coequalizer.π f g) ⋯))
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
inst✝² : HasCoequalizer f g
inst✝¹ : HasCoequalizer (G.map f) (G.map g)
inst✝ : PreservesColimit (parallelPair f g) G
⊢ coequalizer.π (G.map f) (G.map g) ≫ (PreservesCoequalizer.iso G f g).hom ≫ (PreservesCoequalizer.iso G f g).inv =
    coequalizer.π (G.map f) (G.map g)

Tactic:
Iso.hom_inv_id,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
inst✝² : HasCoequalizer f g
inst✝¹ : HasCoequalizer (G.map f) (G.map g)
inst✝ : PreservesColimit (parallelPair f g) G
⊢ coequalizer.π (G.map f) (G.map g) ≫ 𝟙 (coequalizer (G.map f) (G.map g)) = coequalizer.π (G.map f) (G.map g)
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
⊢ Nondegenerate B ↔ ∀ (x : M), x ≠ 0 → 0 < (B x) x

Tactic:
rw [B.nondegenerate_iff hs hB]
  contrapose!
  exact exists_congr fun x ↦ ⟨by aesop, fun ⟨h₀, h⟩ ↦ Or.inl ⟨le_antisymm h (hs x), h₀⟩⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
x✝ : V
⊢ x✝ ∈ comap (Dual.eval K V) (dualAnnihilator W).dualAnnihilator ↔ x✝ ∈ W

Tactic:
Iff.comm,

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
x✝ : V
⊢ x✝ ∈ W ↔ x✝ ∈ comap (Dual.eval K V) (dualAnnihilator W).dualAnnihilator
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
W : Submodule R M
⊢ W.mkQ.dualMap.range = W.dualAnnihilator

Tactic:
by
  ext φ
  rw [LinearMap.mem_range]
  constructor
  · rintro ⟨ψ, rfl⟩
    have := LinearMap.mem_range_self W.mkQ.dualMap ψ
    simpa only [ker_mkQ] using W.mkQ.range_dualMap_le_dualAnnihilator_ker this
  · intro hφ
    exists W.dualCopairing ⟨φ, hφ⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ∐ K.obj
⊢ PreservesColimit K G

Tactic:
let Q := ∐ fun f : Σ p : J × J, p.fst ⟶ p.snd => K.obj f.1.1

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f ↦ K.obj f.fst.1
⊢ PreservesColimit K G
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.IsEquivalence
X Y : C
f : X ⟶ Y
hf : NormalMono (F.map f)
⊢ F.map (f ≫ F.preimage (NormalMono.g ≫ (F.objObjPreimageIso (NormalMono.Z (F.map f))).inv)) = F.map 0

Tactic:
have reassoc' {W : D} (h : hf.Z ⟶ W) : F.map f ≫ hf.g ≫ h = 0 ≫ h := by
      rw [← Category.assoc, eq_whisker hf.w]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.IsEquivalence
X Y : C
f : X ⟶ Y
hf : NormalMono (F.map f)
reassoc' : ∀ {W : D} (h : NormalMono.Z (F.map f) ⟶ W), F.map f ≫ NormalMono.g ≫ h = 0 ≫ h
⊢ F.map (f ≫ F.preimage (NormalMono.g ≫ (F.objObjPreimageIso (NormalMono.Z (F.map f))).inv)) = F.map 0
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: 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 : Mono f
⊢ IsLimit (KernelFork.ofι f ⋯)

Tactic:
by
        haveI : Limits.HasImages C := hasImages
        haveI : HasEqualizers C := Preadditive.hasEqualizers_of_hasKernels
        haveI : HasZeroObject C := Limits.hasZeroObject_of_hasFiniteBiproducts _
        have aux (s : KernelFork (cokernel.π f)) :
            (limit.lift (parallelPair (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e) ≫
            Fork.ι (KernelFork.ofι _ (cokernel.condition f)) = Fork.ι s := ?_
        · refine isLimitAux _ (fun A => limit.lift _ _ ≫ inv (imageMonoFactorisation f).e) aux ?_
          intro A g hg
          rw [KernelFork.ι_ofι] at hg
          rw [← cancel_mono f, hg, ← aux, KernelFork.ι_ofι]
        · simp only [KernelFork.ι_ofι, Category.assoc]
          convert! limit.lift_π s WalkingParallelPair.zero using 2
          rw [IsIso.inv_comp_eq, eq_comm]
          exact (imageMonoFactorisation f).fac

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

Goal state before:
pp: case refine_1
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
s : CokernelCofork (kernel.ι f)
⊢ Cofork.π (CokernelCofork.ofπ f ⋯) ≫
      inv (imageMonoFactorisation f).m ≫ inv (coimageImageComparison f) ≫ colimit.desc (parallelPair (kernel.ι f) 0) s =
    Cofork.π s

Tactic:
simp only [CokernelCofork.π_ofπ, ← Category.assoc]
          convert! colimit.ι_desc s WalkingParallelPair.one using 2
          rw [IsIso.comp_inv_eq, IsIso.comp_inv_eq, eq_comm, ← imageMonoFactorisation_e']
          exact (imageMonoFactorisation f).fac

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
k : S.X₂ ⟶ A
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
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ S.f ≫ S.g ≫ x = 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₂
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₂
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 S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
ψ₁ ψ₂ : LeftHomologyMapData φ h₁ h₂
hK : ψ₁.φK = ψ₂.φK
⊢ ψ₁.φH = ψ₂.φH

Tactic:
← cancel_epi h₁.π,

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₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
ψ₁ ψ₂ : LeftHomologyMapData φ h₁ h₂
hK : ψ₁.φK = ψ₂.φK
⊢ h₁.π ≫ ψ₁.φH = h₁.π ≫ ψ₂.φH
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₁.descH (h₁.i ≫ h₂.p) ⋯ ≫ h₂.g' = 0

Tactic:
← cancel_epi h₁.π,

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

Tactic:
hx,

Goal state after:
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
k : A ⟶ S.X₂
x : A ⟶ S.X₁
hx : k = x ≫ S.f
⊢ (x ≫ S.f) ≫ S.g = 0
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
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ S.f ≫ k = 0

Tactic:
hx,

Goal state after:
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
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ S.f ≫ S.g ≫ x = 0
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
h₁ : IsIso (cyclesMap φ)
h₂ : Epi φ.τ₁
⊢ IsIso (homologyMap φ)

Tactic:
have h : S₂.toCycles ≫ inv (cyclesMap φ) ≫ S₁.homologyπ = 0 := by
    simp only [← cancel_epi φ.τ₁, ← toCycles_naturality_assoc,
      IsIso.hom_inv_id_assoc, toCycles_comp_homologyπ, comp_zero]

Goal state after:
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 (cyclesMap φ)
h₂ : Epi φ.τ₁
h : S₂.toCycles ≫ inv (cyclesMap φ) ≫ S₁.homologyπ = 0
⊢ IsIso (homologyMap φ)
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₂
inst✝¹ : S₁.HasLeftHomology
inst✝ : S₂.HasLeftHomology
⊢ opcyclesMap (opMap φ) ≫ S₁.opcyclesOpIso.hom ≫ S₁.opcyclesOpIso.inv = opcyclesMap (opMap φ)

Tactic:
Iso.hom_inv_id,

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasLeftHomology
inst✝ : S₂.HasLeftHomology
⊢ opcyclesMap (opMap φ) ≫ 𝟙 S₁.op.opcycles = opcyclesMap (opMap φ)
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₂
inst✝¹ : S₁.HasRightHomology
inst✝ : S₂.HasRightHomology
⊢ cyclesMap (opMap φ) ≫ S₁.cyclesOpIso.hom ≫ S₁.cyclesOpIso.inv =
    S₂.cyclesOpIso.hom ≫ (opcyclesMap φ).op ≫ S₁.cyclesOpIso.inv

Tactic:
Iso.hom_inv_id,

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasRightHomology
inst✝ : S₂.HasRightHomology
⊢ cyclesMap (opMap φ) ≫ 𝟙 S₁.op.cycles = S₂.cyclesOpIso.hom ≫ (opcyclesMap φ).op ≫ S₁.cyclesOpIso.inv