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

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : CartesianMonoidalCategory C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : CartesianMonoidalCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : CartesianMonoidalCategory E
F✝ : C ⥤ D
G : D ⥤ E
X✝ Y✝ Z : C
inst✝² : BraidedCategory C
inst✝¹ : BraidedCategory D
F : C ⥤ D
inst✝ : PreservesFiniteProducts F
X Y : C
⊢ μ F X Y ≫ F.map (β_ X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X

Tactic:
← cancel_mono (Monoidal.μIso _ _ _).inv

Goal state after:
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : CartesianMonoidalCategory C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : CartesianMonoidalCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : CartesianMonoidalCategory E
F✝ : C ⥤ D
G : D ⥤ E
X✝ Y✝ Z : C
inst✝² : BraidedCategory C
inst✝¹ : BraidedCategory D
F : C ⥤ D
inst✝ : PreservesFiniteProducts F
X Y : C
⊢ (μ F X Y ≫ F.map (β_ X Y).hom) ≫ (Monoidal.μIso F Y X).inv =
    ((β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X) ≫ (Monoidal.μIso F Y X).inv
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
G✝ H✝ H₁ H₂ G H : Grp C
⊢ (homMk' (fst G.toMon H.toMon)).hom.hom =
    (G ◁ (IsTerminal.ofUniqueHom (fun G ↦ homMk' (toUnit G.toMon)) ⋯).from H ≫ (ρ_ G).hom).hom.hom

Tactic:
apply fst_def

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y : C
inst✝ : ExactPairing X Y
⊢ Y ◁ η_ X Y ⊗≫ ε_ X Y ▷ Y = ⊗𝟙.hom

Tactic:
convert! coevaluation_evaluation X Y <;> simp [monoidalComp]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X₁ X₂ Y₁ Y₂ : C
inst✝¹ : ExactPairing X₁ Y₁
inst✝ : ExactPairing X₂ Y₂
⊢ 𝟙 ((Y₂ ⊗ Y₁) ⊗ 𝟙_ C) ⊗≫
      Y₂ ◁ (Y₁ ◁ η_ X₁ Y₁ ⊗≫ ε_ X₁ Y₁ ▷ Y₁) ⊗≫ (Y₂ ◁ η_ X₂ Y₂ ⊗≫ ε_ X₂ Y₂ ▷ Y₂) ▷ Y₁ ⊗≫ 𝟙 (𝟙_ C ⊗ Y₂ ⊗ Y₁) =
    (ρ_ (Y₂ ⊗ Y₁)).hom ≫ (λ_ (Y₂ ⊗ Y₁)).inv

Tactic:
coevaluation_evaluation'',

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X₁ X₂ Y₁ Y₂ : C
inst✝¹ : ExactPairing X₁ Y₁
inst✝ : ExactPairing X₂ Y₂
⊢ 𝟙 ((Y₂ ⊗ Y₁) ⊗ 𝟙_ C) ⊗≫ Y₂ ◁ ⊗𝟙.hom ⊗≫ (Y₂ ◁ η_ X₂ Y₂ ⊗≫ ε_ X₂ Y₂ ▷ Y₂) ▷ Y₁ ⊗≫ 𝟙 (𝟙_ C ⊗ Y₂ ⊗ Y₁) =
    (ρ_ (Y₂ ⊗ Y₁)).hom ≫ (λ_ (Y₂ ⊗ Y₁)).inv
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
sec : M ⧸ span R s → M
hsec : ∀ (b : M ⧸ span R s), (span R s).mkQ (sec b) = b
hsec' : ⇑(span R s).mkQ ∘ sec = _root_.id
hst : Disjoint s (sec '' t)
⊢ Injective sec

Tactic:
exact HasLeftInverse.injective ⟨Submodule.Quotient.mk, hsec⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
h : ↑n < Module.rank R M
⊢ ∃ x, LinearIndependent R (Fin.snoc v x)

Tactic:
simp only [Fin.snoc_eq_cons_rotate]

Goal state after:
R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
h : ↑n < Module.rank R M
⊢ ∃ x, LinearIndependent R fun i ↦ Fin.cons x v ((finRotate (n + 1)) i)
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
s t : Submodule K V
inst✝¹ : FiniteDimensional K ↥s
inst✝ : FiniteDimensional K ↥t
⊢ finrank K ↥(s ⊔ t) ≤ finrank K ↥s + finrank K ↥t

Tactic:
by
  rw [← finrank_sup_add_finrank_inf_eq]
  exact self_le_add_right _ _

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ (∀ (n m : ℕ) (f : Matrix (Fin n) (Fin m) Rᵐᵒᵖ) (g : Matrix (Fin m) (Fin n) Rᵐᵒᵖ), g * f = 1 → m ≤ n) ↔
    ∀ (n m : ℕ) (f : Matrix (Fin n) (Fin m) R) (g : Matrix (Fin m) (Fin n) R), g * f = 1 → m ≤ n

Tactic:
← opEquiv.mapMatrix.forall_congr_right,

Goal state after:
R : Type u_1
inst✝ : Semiring R
⊢ (∀ (n m : ℕ) (a : Matrix (Fin n) (Fin m) R) (a_1 : Matrix (Fin m) (Fin n) R),
      opEquiv.mapMatrix a_1 * opEquiv.mapMatrix a = 1 → m ≤ n) ↔
    ∀ (n m : ℕ) (f : Matrix (Fin n) (Fin m) R) (g : Matrix (Fin m) (Fin n) R), g * f = 1 → m ≤ n
Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ (∀ (n m : ℕ) (f : Matrix (Fin n) (Fin m) Rᵐᵒᵖ) (g : Matrix (Fin m) (Fin n) Rᵐᵒᵖ), f * g = 1 → g * f = 1 → n = m) ↔
    ∀ (n m : ℕ) (f : Matrix (Fin n) (Fin m) R) (g : Matrix (Fin m) (Fin n) R), f * g = 1 → g * f = 1 → n = m

Tactic:
← opEquiv.mapMatrix.forall_congr_right,

Goal state after:
R : Type u_1
inst✝ : Semiring R
⊢ (∀ (n m : ℕ) (a : Matrix (Fin n) (Fin m) R) (a_1 : Matrix (Fin m) (Fin n) R),
      opEquiv.mapMatrix a * opEquiv.mapMatrix a_1 = 1 → opEquiv.mapMatrix a_1 * opEquiv.mapMatrix a = 1 → n = m) ↔
    ∀ (n m : ℕ) (f : Matrix (Fin n) (Fin m) R) (g : Matrix (Fin m) (Fin n) R), f * g = 1 → g * f = 1 → n = m
Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n m : ℕ
f : Matrix (Fin m) (Fin n) R
g : Matrix (Fin n) (Fin m) R
⊢ opEquiv.mapMatrix.symm (opEquiv.mapMatrix g * opEquiv.mapMatrix f) = opEquiv.mapMatrix.symm 1 →
      opEquiv.mapMatrix.symm (opEquiv.mapMatrix f * opEquiv.mapMatrix g) = opEquiv.mapMatrix.symm 1 → n = m ↔
    (transposeAddEquiv (Fin m) (Fin n) R).toEquiv f * (transposeAddEquiv (Fin n) (Fin m) R).toEquiv g = 1 →
      (transposeAddEquiv (Fin n) (Fin m) R).toEquiv g * (transposeAddEquiv (Fin m) (Fin n) R).toEquiv f = 1 → n = m

Tactic:
← (transposeAddEquiv ..).injective.eq_iff,

Goal state after:
R : Type u_1
inst✝ : Semiring R
n m : ℕ
f : Matrix (Fin m) (Fin n) R
g : Matrix (Fin n) (Fin m) R
⊢ (transposeAddEquiv (Fin n) (Fin n) R) (opEquiv.mapMatrix.symm (opEquiv.mapMatrix g * opEquiv.mapMatrix f)) =
        (transposeAddEquiv (Fin n) (Fin n) R) (opEquiv.mapMatrix.symm 1) →
      opEquiv.mapMatrix.symm (opEquiv.mapMatrix f * opEquiv.mapMatrix g) = opEquiv.mapMatrix.symm 1 → n = m ↔
    (transposeAddEquiv (Fin m) (Fin n) R).toEquiv f * (transposeAddEquiv (Fin n) (Fin m) R).toEquiv g = 1 →
      (transposeAddEquiv (Fin n) (Fin m) R).toEquiv g * (transposeAddEquiv (Fin m) (Fin n) R).toEquiv f = 1 → n = m
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: case left
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module.Finite R M
inst✝ : Projective R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
g : M →ₗ[R] Fin n → R
eq : f ∘ₗ g = LinearMap.id
⊢ Function.Injective (⇑(dualTensorHomEquivOfBasis (Pi.basisFun R (Fin n))) ∘ ⇑(rTensor N f.dualMap))

Tactic:
refine (EquivLike.injective _).comp (injective_of_comp_eq_id _ (rTensor _ g.dualMap) ?_)

Goal state after:
case left
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module.Finite R M
inst✝ : Projective R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
g : M →ₗ[R] Fin n → R
eq : f ∘ₗ g = LinearMap.id
⊢ rTensor N g.dualMap ∘ₗ rTensor N f.dualMap = LinearMap.id
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: case right
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module.Finite R M
inst✝ : Projective R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
g : M →ₗ[R] Fin n → R
eq : f ∘ₗ g = LinearMap.id
⊢ Function.Surjective ⇑(dualTensorHom R M N)

Tactic:
refine .of_comp (g := g.dualMap.rTensor N) ?_

Goal state after:
case right
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module.Finite R M
inst✝ : Projective R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
g : M →ₗ[R] Fin n → R
eq : f ∘ₗ g = LinearMap.id
⊢ Function.Surjective (⇑(dualTensorHom R M N) ∘ ⇑(rTensor N g.dualMap))
Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryCoproducts C
inst✝² : HasPushouts C
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
K : WalkingParallelPair ⥤ C
c : Cocone (K ⋙ G)
j : WalkingParallelPair
⊢ (G.mapCocone (coequalizerCocone K)).ι.app j ≫
      (PreservesPushout.iso G (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left))
            (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))).inv ≫
        pushout.desc (c.ι.app WalkingParallelPair.one) (c.ι.app WalkingParallelPair.one) ⋯ =
    c.ι.app j

Tactic:
rcases j with (_ | _) <;>
            simp only [Functor.mapCocone_ι_app, Cocone.ofCofork_ι, Category.id_comp,
              eqToHom_refl, Category.assoc, Functor.map_comp, Cofork.ofπ_ι_app, pushout.inl_desc,
              PreservesPushout.inl_iso_inv_assoc]

Goal state after:
case zero
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryCoproducts C
inst✝² : HasPushouts C
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
K : WalkingParallelPair ⥤ C
c : Cocone (K ⋙ G)
⊢ G.map (K.map WalkingParallelPairHom.left) ≫ c.ι.app WalkingParallelPair.one = c.ι.app WalkingParallelPair.zero
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
x : M
hx : x ∉ p
hp' : Projective R (M ⧸ p)
⊢ ∃ f, f x ≠ 0 ∧ map f p = ⊥

Tactic:
suffices ∃ f : Dual R (M ⧸ p), f (p.mkQ x) ≠ 0 by
    obtain ⟨f, hf⟩ := this; exact ⟨f.comp p.mkQ, hf, by simp [Submodule.map_comp]⟩
  rw [← Submodule.Quotient.mk_eq_zero, ← Submodule.mkQ_apply] at hx
  exact Projective.exists_dual_ne_zero R hx

Goal state after:
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
inst✝¹ : IsReflexive R M
s : Set (M →ₗ[R] R)
inst✝ : Projective R ((M →ₗ[R] R) ⧸ span R s)
h : ∀ (z : M), z ≠ 0 → ∃ f ∈ s, f z ≠ 0
hn : span R s ≠ ⊤
φ : Dual R (M →ₗ[R] R)
φne : φ ≠ 0
hφ : map φ (span R s) = ⊥
φs : M := (evalEquiv R M).symm φ
f : M →ₗ[R] R
hf : f ∈ s
⊢ f φs ∈ map φ (span R s)

Tactic:
mem_map

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsReflexive R M
s : Set (M →ₗ[R] R)
inst✝ : Projective R ((M →ₗ[R] R) ⧸ span R s)
h : ∀ (z : M), z ≠ 0 → ∃ f ∈ s, f z ≠ 0
hn : span R s ≠ ⊤
φ : Dual R (M →ₗ[R] R)
φne : φ ≠ 0
hφ : map φ (span R s) = ⊥
φs : M := (evalEquiv R M).symm φ
f : M →ₗ[R] R
hf : f ∈ s
⊢ ∃ y ∈ span R s, φ y = f φs
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
inst✝ : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y : M
hle : ∀ (z : M), 0 ≤ (B z) z
r s : R
hl : r • x + s • y = 0
h0 : r = 0 → s ≠ 0
hr : ¬r = 0
hs : ¬s = 0
this : r * r * s * s * ((B x) x * (B y) y) = s * (r * (B x) y) * (r * (s * (B y) x))
⊢ (B x) x * (B y) y ≤ (B x) y * (B y) x

Tactic:
show s * (r * (B x) y) * (r * (s * (B y) x)) = (r * r * s * s) * ((B x) y * (B y) x)
        by ring

Goal state after:
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
inst✝ : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y : M
hle : ∀ (z : M), 0 ≤ (B z) z
r s : R
hl : r • x + s • y = 0
h0 : r = 0 → s ≠ 0
hr : ¬r = 0
hs : ¬s = 0
this : r * r * s * s * ((B x) x * (B y) y) = r * r * s * s * ((B x) y * (B y) x)
⊢ (B x) x * (B y) y ≤ (B x) y * (B y) x
Module: Mathlib.Algebra.Category.FGModuleCat.Colimits

Goal state before:
pp: J✝ : Type
inst✝⁴ : SmallCategory J✝
inst✝³ : FinCategory J✝
k : Type u
inst✝² : Ring k
J : Type
inst✝¹ : Finite J
Z : J → ModuleCat k
inst✝ : ∀ (j : J), Module.Finite k ↑(Z j)
⊢ Module.Finite k ↑(∐ fun j ↦ Z j)

Tactic:
classical
exact (Module.Finite.equiv_iff (ModuleCat.coprodIsoDirectSum Z).toLinearEquiv).mpr inferInstance

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

Goal state before:
pp: K : Type u_1
V₁ : Type u_2
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
f : Dual K V₁
hf : f ≠ 0
inst✝ : FiniteDimensional K V₁
p : Submodule K V₁
hpf : Disjoint (LinearMap.ker f) p
hp : p ≠ ⊥
⊢ finrank K ↥(LinearMap.ker f ⊔ p) = finrank K ↥(LinearMap.ker f) + finrank K ↥p

Tactic:
simp [← Submodule.finrank_sup_add_finrank_inf_eq (LinearMap.ker f) p, hpf.eq_bot]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
c : Cone (parallelPair 0 0)
hc : IsLimit c
this : IsIso (Fork.ι c)
⊢ IsLimit (KernelFork.map c G)

Tactic:
refine IsLimit.ofIsoLimit (KernelFork.IsLimit.ofId _ (G.map_zero _ _)) ?_

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
c : Cone (parallelPair 0 0)
hc : IsLimit c
this : IsIso (Fork.ι c)
⊢ KernelFork.ofι (𝟙 (G.obj X)) ⋯ ≅ KernelFork.map c G
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
⊢ Mono (r A)

Tactic:
by
  let hl : IsLimit (KernelFork.ofι (diag A) (cokernel.condition (diag A))) :=
    monoIsKernelOfCokernel _ (colimit.isColimit _)
  apply NormalEpiCategory.mono_of_cancel_zero
  intro Z x hx
  have hxx : (x ≫ prod.lift (𝟙 A) (0 : A ⟶ A)) ≫ cokernel.π (diag A) = 0 := by
    rw [Category.assoc, hx]
  obtain ⟨y, hy⟩ := KernelFork.IsLimit.lift' hl _ hxx
  rw [KernelFork.ι_ofι] at hy
  have hyy : y = 0 := by
    erw [← Category.comp_id y, ← Limits.prod.lift_snd (𝟙 A) (𝟙 A), ← Category.assoc, hy,
      Category.assoc, prod.lift_snd, HasZeroMorphisms.comp_zero]
  have : Mono (prod.lift (𝟙 A) (0 : A ⟶ A)) := mono_of_mono_fac (prod.lift_fst _ _)
  apply (cancel_mono (prod.lift (𝟙 A) (0 : A ⟶ A))).1
  rw [← hy, hyy, zero_comp, zero_comp]

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

Goal state before:
pp: case refine_1.fromCoset
A B : GrpCat
f : A ⟶ B
a : ↑A
y : ↑B
⊢ (h ((ConcreteCategory.hom f) a)) (fromCoset ⟨(fun x ↦ x • ↑(Hom.hom f).range) y, ⋯⟩) =
    fromCoset ⟨(ConcreteCategory.hom f) a • ↑⟨(fun x ↦ x • ↑(Hom.hom f).range) y, ⋯⟩, ⋯⟩

Tactic:
by_cases m : y ∈ f.hom.range

Goal state after:
case pos
A B : GrpCat
f : A ⟶ B
a : ↑A
y : ↑B
m : y ∈ (Hom.hom f).range
⊢ (h ((ConcreteCategory.hom f) a)) (fromCoset ⟨(fun x ↦ x • ↑(Hom.hom f).range) y, ⋯⟩) =
    fromCoset ⟨(ConcreteCategory.hom f) a • ↑⟨(fun x ↦ x • ↑(Hom.hom f).range) y, ⋯⟩, ⋯⟩

case neg
A B : GrpCat
f : A ⟶ B
a : ↑A
y : ↑B
m : y ∉ (Hom.hom f).range
⊢ (h ((ConcreteCategory.hom f) a)) (fromCoset ⟨(fun x ↦ x • ↑(Hom.hom f).range) y, ⋯⟩) =
    fromCoset ⟨(ConcreteCategory.hom f) a • ↑⟨(fun x ↦ x • ↑(Hom.hom f).range) y, ⋯⟩, ⋯⟩
Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso

Goal state before:
pp: case mp
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
⊢ QuasiIso φ → IsIso (homologyMap φ)

Tactic:
intro h
    infer_instance

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

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

Tactic:
intro h
    infer_instance

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

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

Tactic:
intro h
    infer_instance

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

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

Tactic:
intro h
    infer_instance

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
e : S₁ ≅ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
⊢ homologyMap e.inv ≫ homologyMap e.hom = 𝟙 S₂.homology

Tactic:
by rw [← homologyMap_comp, e.inv_hom_id, homologyMap_id]

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
inst✝ : S.HasHomology
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
⊢ IsIso (leftRightHomologyComparison' h₁ h₂)

Tactic:
rw [leftRightHomologyComparison'_compatibility h₁ S.homologyData.left h₂
    S.homologyData.right]

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
inst✝ : S.HasHomology
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
⊢ IsIso
    (leftHomologyMap' (𝟙 S) h₁ S.homologyData.left ≫
      leftRightHomologyComparison' S.homologyData.left S.homologyData.right ≫
        rightHomologyMap' (𝟙 S) S.homologyData.right h₂)
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 φ.τ₂
⊢ S₁.LeftHomologyData

Tactic:
have wi : i ≫ S₁.g = 0 := by
    rw [assoc, ← cancel_mono φ.τ₃, zero_comp, assoc, assoc, ← φ.comm₂₃,
      IsIso.inv_hom_id_assoc, 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
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
⊢ S₁.LeftHomologyData
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
⊢ (S₁.iCycles ≫ φ.τ₂).op = (cyclesMap φ ≫ S₂.iCycles).op

Tactic:
cyclesMap_i

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
⊢ (S₁.iCycles ≫ φ.τ₂).op = (S₁.iCycles ≫ φ.τ₂).op
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.RightHomologyData
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : h.IsPreservedBy F
this✝ : PreservesColimit (parallelPair S.f 0) F
this : PreservesLimit (parallelPair h.g' 0) F
wp : F.map S.f ≫ F.map h.p = 0
hp : IsColimit ((CokernelCofork.ofπ h.p ⋯).map F)
g' : F.obj h.Q ⟶ F.obj S.X₃ := hp.desc (CokernelCofork.ofπ (S.map F).g ⋯)
hg' : g' = F.map h.g'
wι : F.map h.ι ≫ g' = 0
⊢ (parallelPair g' 0).map WalkingParallelPairHom.left ≫
      (Iso.refl ((parallelPair g' 0).obj WalkingParallelPair.one)).hom =
    (Iso.refl ((parallelPair g' 0).obj WalkingParallelPair.zero)).hom ≫
      (parallelPair (F.map h.g') 0).map WalkingParallelPairHom.left

Tactic:
by simpa using hg'

Goal state after:
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
⊢ Abelian.image.ι S.f ≫ S.g = 0

Tactic:
simp only [← cancel_epi (Abelian.factorThruImage S.f),
      kernel.lift_ι_assoc, zero, comp_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
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ leftHomologyMap' (-φ) h₁ h₂ = -leftHomologyMap' φ h₁ h₂

Tactic:
by
  have γ : LeftHomologyMapData φ h₁ h₂ := default
  simp only [γ.leftHomologyMap'_eq, γ.neg.leftHomologyMap'_eq, LeftHomologyMapData.neg_φ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₁.g ≫ (-h.h₂) + (-h.h₁) ≫ S₂.f + φ₁.τ₂

Tactic:
rw [h.comm₂, comp_neg, neg_comp]; abel

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (cokernel.π f).op ≫ f.op = 0

Tactic:
by simp [← op_comp]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ f.op ≫ (kernel.ι f).op = 0

Tactic:
by simp [← op_comp]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : IsColimit (CokernelCofork.ofπ S.g ⋯)
inst✝ : S.HasHomology
⊢ S.fromOpcycles ≫ hS.desc (CokernelCofork.ofπ S.pOpcycles ⋯) = 𝟙 S.opcycles

Tactic:
by
          rw [← cancel_epi S.pOpcycles, p_fromOpcycles_assoc, comp_id]
          exact Cofork.IsColimit.π_desc hS

Goal state after:
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
inst✝ : HasImages C
f : Over X
g : MonoOver X
k : image.obj f ⟶ g
⊢ f ⟶ (forget X).obj g

Tactic:
apply Over.homMk (factorThruImage f.hom ≫ k.hom.left) _
            rw [assoc, Over.w k.hom]
            apply image.fac

Goal state after: