mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: case h₁.h₀
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ ((lift (fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (fst f' g') i₁)
            (snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (snd f' g') i₂) ⋯ ≫
          lift (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (fst f g) ⋯) (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (snd f g) ⋯) ⋯) ≫
        snd (fst (fst f' g') i₁) (fst (snd f' g') i₂)) ≫
      fst (snd f' g') i₂ =
    (𝟙 (pullback (fst (fst f' g') i₁) (fst (snd f' g') i₂)) ≫ snd (fst (fst f' g') i₁) (fst (snd f' g') i₂)) ≫
      fst (snd f' g') i₂

pp: case h₁
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ ((lift (fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (fst f' g') i₁)
            (snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (snd f' g') i₂) ⋯ ≫
          lift (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (fst f g) ⋯) (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (snd f g) ⋯) ⋯) ≫
        snd (fst (fst f' g') i₁) (fst (snd f' g') i₂)) ≫
      snd (snd f' g') i₂ =
    (𝟙 (pullback (fst (fst f' g') i₁) (fst (snd f' g') i₂)) ≫ snd (fst (fst f' g') i₁) (fst (snd f' g') i₂)) ≫
      snd (snd f' g') i₂

Tactic:
· apply pullback.hom_ext
        · simp only [Category.assoc, lift_snd_assoc, lift_fst_assoc, lift_fst, Category.id_comp]
          rw [← condition_assoc, condition]
        · simp only [Category.assoc, lift_snd, lift_fst_assoc, lift_snd_assoc, Category.id_comp]
          rw [condition]

Goal state after:
case h₁
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ ((lift (fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (fst f' g') i₁)
            (snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (snd f' g') i₂) ⋯ ≫
          lift (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (fst f g) ⋯) (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (snd f g) ⋯) ⋯) ≫
        snd (fst (fst f' g') i₁) (fst (snd f' g') i₂)) ≫
      snd (snd f' g') i₂ =
    (𝟙 (pullback (fst (fst f' g') i₁) (fst (snd f' g') i₂)) ≫ snd (fst (fst f' g') i₁) (fst (snd f' g') i₂)) ≫
      snd (snd f' g') i₂
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X Y : C
f : X ⟶ Y
Z : C
⊢ f ▷ Z ≫ snd Y Z = snd X Z

Tactic:
simp [snd_def, ← comp_whiskerRight_assoc]

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

Goal state before:
pp: C✝ : Type u
inst✝⁹ : Category.{v, u} C✝
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
E✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} E✝
inst✝³ : CartesianMonoidalCategory E✝
G✝ : D ⥤ E✝
A✝ B A' B' : C
E : Type u₂
inst✝² : Category.{v₂, u₂} E
inst✝¹ : CartesianMonoidalCategory E
G : D ⥤ E
A : C
inst✝ : ∀ (B : C), IsIso (prodComparison F A B)
⊢ IsIso (prodComparisonNatTrans F A)

Tactic:
let : ∀ X, IsIso ((prodComparisonNatTrans F A).app X) := by assumption
  apply NatIso.isIso_of_isIso_app

Goal state after:
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 B
f g h : A ⟶ B
⊢ lift f (g ≫ ι) ≫ μ = h ↔ f = lift h g ≫ μ

Tactic:
by
  rw [eq_comm, eq_lift_inv_right, eq_comm]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Parametrized

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
adj₂ : F ⊣₂ G
X₁ : C₁
X₂ Y₂ : C₂
X₃ : C₃
f₂ : X₂ ⟶ Y₂
g : Y₂ ⟶ (G.obj (op X₁)).obj X₃
⊢ adj₂.homEquiv (adj₂.homEquiv.symm (f₂ ≫ g)) = adj₂.homEquiv ((F.obj X₁).map f₂ ≫ adj₂.homEquiv.symm g)

Tactic:
simp [homEquiv_naturality_two]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring C
inst✝¹ : Bialgebra R C
inst✝ : HopfAlgebra R A
f : WithConv (A →ₐ[R] C)
H : (lmul' R).comp (Algebra.TensorProduct.map f.ofConv f.ofConv) = f.ofConv.comp (lmul' R)
⊢ f.ofConv.toLinearMap ∘ₗ (toConv (antipode R) * toConv LinearMap.id).ofConv = ofConv 1

Tactic:
rw [LinearMap.antipode_mul_id]

Goal state after:
R : Type u_1
A : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring C
inst✝¹ : Bialgebra R C
inst✝ : HopfAlgebra R A
f : WithConv (A →ₐ[R] C)
H : (lmul' R).comp (Algebra.TensorProduct.map f.ofConv f.ofConv) = f.ofConv.comp (lmul' R)
⊢ f.ofConv.toLinearMap ∘ₗ ofConv 1 = ofConv 1
Module: Mathlib.RingTheory.HopfAlgebra.Convolution

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : HopfAlgebra R A
⊢ toConv (toConv (antipodeAlgHom R A)).ofConv.toLinearMap * toConv (toConv (AlgHom.id R A)).ofConv.toLinearMap = 1

Tactic:
simp [LinearMap.antipode_mul_id]

Goal state after:
Module: Mathlib.Data.W.Cardinal

Goal state before:
pp: α : Type u
β : α → Type v
κ : Cardinal.{max u v}
hκ : (sum fun a ↦ κ ^ lift.{u, v} #(β a)) ≤ κ
⊢ #(WType β) ≤ κ

Tactic:
induction κ using Cardinal.inductionOn with | _ γ
  simp_rw [← lift_umax.{v, u}] at hκ
  nth_rewrite 1 [← lift_id'.{v, u} #γ] at hκ
  simp_rw [← mk_arrow, ← mk_sigma, le_def] at hκ
  obtain ⟨hκ⟩ := hκ
  exact Cardinal.mk_le_of_injective (elim_injective _ hκ.1 hκ.2)

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
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ (b.toDual ((Finsupp.linearCombination R ⇑b) f)) (b i) = f i

Tactic:
Finsupp.linearCombination_apply,

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
f : ι →₀ R
i : ι
⊢ (b.toDual (f.sum fun i a ↦ a • b i)) (b i) = f i
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
f : ι →₀ R
i : ι
⊢ (b.toDual (b i)) ((Finsupp.linearCombination R ⇑b) f) = f i

Tactic:
Finsupp.linearCombination_apply,

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
f : ι →₀ R
i : ι
⊢ (b.toDual (b i)) (f.sum fun i a ↦ a • b i) = f i
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: case intro
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 ι
f : ι →₀ R
i : ι
val✝ : Fintype ι
⊢ ((Finsupp.linearCombination R ⇑b.dualBasis) f) (b i) = f i

Tactic:
Finsupp.linearCombination_apply,

Goal state after:
case intro
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 ι
f : ι →₀ R
i : ι
val✝ : Fintype ι
⊢ (f.sum fun i a ↦ a • b.dualBasis i) (b i) = f i
Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky

Goal state before:
pp: case inr
K : Type u
inst✝ : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this✝ : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Module.Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun i ↦ bK i.1 i.2)
hLK : #↥L < #K
this : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)
ιL : Type u
bL : Module.Basis ιL (↥L)ᵐᵒᵖ K
card_ιL : ℵ₀ ≤ #ιL
e : ℕ ↪ ιL
rep_e : (Finsupp.linearCombination K ⇑bK) (bK.repr (⇑bL ∘ ⇑e)) = ⇑bL ∘ ⇑e
⊢ False

Tactic:
Finsupp.linearCombination_apply,

Goal state after:
case inr
K : Type u
inst✝ : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this✝ : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Module.Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun i ↦ bK i.1 i.2)
hLK : #↥L < #K
this : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)
ιL : Type u
bL : Module.Basis ιL (↥L)ᵐᵒᵖ K
card_ιL : ℵ₀ ≤ #ιL
e : ℕ ↪ ιL
rep_e : ((bK.repr (⇑bL ∘ ⇑e)).sum fun i a ↦ a • bK i) = ⇑bL ∘ ⇑e
⊢ False
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
inst✝ : Module.Finite R M
N : Submodule R M
h : finrank R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank R (M ⧸ N)
hs' : LinearIndependent R Subtype.val
v : M
hv : N.mkQ v ∈ s
⊢ ∃ m, ∀ (r : R), r ≠ 0 → r • m ∉ N

Tactic:
refine ⟨v, fun r hr ↦ mt ?_ hr⟩

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
inst✝ : Module.Finite R M
N : Submodule R M
h : finrank R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank R (M ⧸ N)
hs' : LinearIndependent R Subtype.val
v : M
hv : N.mkQ v ∈ s
r : R
hr : r ≠ 0
⊢ r • v ∈ N → r = 0
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✝¹ : HasLeftDual X
inst✝ : HasLeftDual Y
f : X ⟶ Y
⊢ (X ◁ ᘁf) ≫ ε_ (ᘁX) X = f ▷ ᘁY ≫ ε_ (ᘁY) Y

Tactic:
apply_fun tensorLeftHomEquiv _ (ᘁX) X _

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y : C
inst✝¹ : HasLeftDual X
inst✝ : HasLeftDual Y
f : X ⟶ Y
⊢ (tensorLeftHomEquiv (ᘁY) (ᘁX) X (𝟙_ C)) ((X ◁ ᘁf) ≫ ε_ (ᘁX) X) =
    (tensorLeftHomEquiv (ᘁY) (ᘁX) X (𝟙_ C)) (f ▷ ᘁY ≫ ε_ (ᘁY) Y)
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : C
p : ExactPairing X Y
⊢ leftDualIso p p = Iso.refl X

Tactic:
ext
  simp only [leftDualIso, Iso.refl_hom, @leftAdjointMate_id]

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

Goal state before:
pp: n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M
inst✝¹ : Module R M₁
I I' : R →+* R
B : M →ₛₗ[I] M →ₛₗ[I'] M₁
inst✝ : Nontrivial R
v : Basis n R M
h : B.IsOrthoᵢ ⇑v
hB : B.SeparatingLeft
i : n
ho : (B (v i)) (v i) = 0
vi : n →₀ R
⊢ (B (v i)) ((Finsupp.linearCombination R ⇑v) vi) = 0

Tactic:
Finsupp.linearCombination_apply,

Goal state after:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M
inst✝¹ : Module R M₁
I I' : R →+* R
B : M →ₛₗ[I] M →ₛₗ[I'] M₁
inst✝ : Nontrivial R
v : Basis n R M
h : B.IsOrthoᵢ ⇑v
hB : B.SeparatingLeft
i : n
ho : (B (v i)) (v i) = 0
vi : n →₀ R
⊢ (B (v i)) (vi.sum fun i a ↦ a • v i) = 0
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : B.IsOrthoᵢ ⇑v
h : ∀ (i : n), (B (v i)) (v i) ≠ 0
vi : n →₀ R
i : n
hB : (B ((Finsupp.linearCombination R ⇑v) vi)) (v i) = 0
⊢ vi i = 0

Tactic:
Finsupp.linearCombination_apply,

Goal state after:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : B.IsOrthoᵢ ⇑v
h : ∀ (i : n), (B (v i)) (v i) ≠ 0
vi : n →₀ R
i : n
hB : (B (vi.sum fun i a ↦ a • v i)) (v i) = 0
⊢ vi i = 0
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) ≫ G.map f = G.map (equalizer.ι f g) ≫ G.map g

Tactic:
by simp only [← G.map_comp]; rw [equalizer.condition]

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

Goal state before:
pp: ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, (L i).ker ≤ K.ker
⊢ K ∈ span 𝕜 (Set.range L)

Tactic:
have _ := Fintype.ofFinite ι

Goal state after:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, (L i).ker ≤ K.ker
x✝ : Fintype ι
⊢ K ∈ span 𝕜 (Set.range L)
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
W : Submodule R M
φ : Dual R M
hφ : φ ∈ W.dualAnnihilator
⊢ ∃ y, W.mkQ.dualMap y = φ

Tactic:
exists W.dualCopairing ⟨φ, hφ⟩

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Kernels

Goal state before:
pp: R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
x y : ↑N
m : ↑M
w : x = y + (ConcreteCategory.hom f) m
⊢ (ConcreteCategory.hom (cokernel.π f)) x = (ConcreteCategory.hom (cokernel.π f)) y

Tactic:
subst w

Goal state after:
R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
y : ↑N
m : ↑M
⊢ (ConcreteCategory.hom (cokernel.π f)) (y + (ConcreteCategory.hom f) m) = (ConcreteCategory.hom (cokernel.π f)) y
Module: Mathlib.CategoryTheory.Limits.Constructions.Pullbacks

Goal state before:
pp: case h₂
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasLimit (pair X Y)
inst✝ : HasLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : X ⨯ Y ⟶ X := ⋯
π₂ : X ⨯ Y ⟶ Y := ⋯
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ X ⨯ Y := ⋯
s : PullbackCone f g
m : s.pt ⟶ equalizer (π₁ ≫ f) (π₂ ≫ g)
h₁ : m ≫ e ≫ π₁ = s.fst
h₂ : m ≫ e ≫ π₂ = s.snd
⊢ (m ≫ equalizer.ι (π₁ ≫ f) (π₂ ≫ g)) ≫ prod.snd =
    (equalizer.lift (prod.lift (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right)) ⋯ ≫
        equalizer.ι (π₁ ≫ f) (π₂ ≫ g)) ≫
      prod.snd

Tactic:
· simpa using h₂

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

Goal state before:
pp: case h₂
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasColimit (pair Y Z)
inst✝ : HasColimit (parallelPair (f ≫ coprod.inl) (g ≫ coprod.inr))
ι₁ : Y ⟶ Y ⨿ Z := ⋯
ι₂ : Z ⟶ Y ⨿ Z := ⋯
c : Y ⨿ Z ⟶ coequalizer (f ≫ ι₁) (g ≫ ι₂) := ⋯
s : PushoutCocone f g
m : coequalizer (f ≫ ι₁) (g ≫ ι₂) ⟶ s.pt
h₁ : (ι₁ ≫ c) ≫ m = s.inl
h₂ : (ι₂ ≫ c) ≫ m = s.inr
⊢ coprod.inr ≫ coequalizer.π (f ≫ ι₁) (g ≫ ι₂) ≫ m =
    coprod.inr ≫
      coequalizer.π (f ≫ ι₁) (g ≫ ι₂) ≫
        coequalizer.desc (coprod.desc (s.ι.app WalkingSpan.left) (s.ι.app WalkingSpan.right)) ⋯

Tactic:
· simpa using h₂

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
P Q : C
f : P ⟶ Q
inst✝³ : HasCokernel f
inst✝² : HasKernel f
inst✝¹ : HasKernel (cokernel.π f)
inst✝ : HasCokernel (kernel.ι f)
⊢ (coequalizer.π (kernel.ι f) 0 ≫ coimageImageComparison f) ≫ equalizer.ι (cokernel.π f) 0 =
    (coequalizer.π (kernel.ι f) 0 ≫ coimageImageComparison' f) ≫ equalizer.ι (cokernel.π f) 0

Tactic:
simp [coimageImageComparison, coimageImageComparison']

Goal state after:
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
hwf : f ≫ w = 0
n : (CokernelCofork.ofπ 0 ⋯).pt ⟶ W
hn : 0 = w
this : IsIso (equalizer.ι u v)
⊢ u = v

Tactic:
apply (cancel_epi (equalizer.ι u v)).1

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
hwf : f ≫ w = 0
n : (CokernelCofork.ofπ 0 ⋯).pt ⟶ W
hn : 0 = w
this : IsIso (equalizer.ι u v)
⊢ equalizer.ι u v ≫ u = equalizer.ι u v ≫ v
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 : X ⟶ Y
⊢ -(a + b) = -a - b

Tactic:
by rw [add_def, neg_sub', add_neg]

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

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
b : ↑B
hb : b ∈ (Hom.hom f).range
⊢ b • ↑(Hom.hom f).range = 1 • ↑(Hom.hom f).range

Tactic:
leftCoset_eq_iff,

Goal state after:
A B : GrpCat
f : A ⟶ B
b : ↑B
hb : b ∈ (Hom.hom f).range
⊢ b⁻¹ * 1 ∈ (Hom.hom f).range
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
b : ↑B
hb : b ∉ (Hom.hom f).range
r : b • ↑(Hom.hom f).range = 1 • ↑(Hom.hom f).range
⊢ False

Tactic:
leftCoset_eq_iff,

Goal state after:
A B : GrpCat
f : A ⟶ B
b : ↑B
hb : b ∉ (Hom.hom f).range
r : b⁻¹ * 1 ∈ (Hom.hom f).range
⊢ False
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
⊢ ↑(Hom.hom f).range = {x | h x = g x}

Tactic:
refine Set.ext fun b => ⟨?_, fun hb : h b = g b => by_contradiction fun r => ?_⟩
  · rintro ⟨a, rfl⟩
    change h (f a) = g (f a)
    ext ⟨⟨_, ⟨y, rfl⟩⟩⟩
    · rw [g_apply_fromCoset]
      by_cases m : y ∈ f.hom.range
      · rw [h_apply_fromCoset' _ _ _ m, fromCoset_eq_of_mem_range _ m]
        change fromCoset _ = fromCoset ⟨f a • (y • _), _⟩
        simp only [← fromCoset_eq_of_mem_range _ (Subgroup.mul_mem _ ⟨a, rfl⟩ m), smul_smul]
      · rw [h_apply_fromCoset_nin_range f (f a) ⟨_, rfl⟩ _ m]
        simp only [leftCoset_assoc]
    · rw [g_apply_infinity, h_apply_infinity f (f a) ⟨_, rfl⟩]
  · have eq1 : (h b) (fromCoset ⟨f.hom.range, 1, one_leftCoset _⟩) =
        fromCoset ⟨f.hom.range, 1, one_leftCoset _⟩ := by
      change ((τ).symm.trans (g b)).trans τ _ = _
      dsimp [tau]
      simp [g_apply_infinity f]
    have eq2 :
        g b (fromCoset ⟨f.hom.range, 1, one_leftCoset _⟩) = fromCoset ⟨b • ↑f.hom.range, b, rfl⟩ :=
      rfl
    exact (fromCoset_ne_of_nin_range _ r).symm (by rw [← eq1, ← eq2, DFunLike.congr_fun hb])

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
hg : S.g = 0
c : CokernelCofork S.f
hc : IsColimit c
⊢ 𝟙 S.X₂ ≫ S.g = 0

Tactic:
rw [id_comp, hg]

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

Tactic:
rw [id_comp, hg]

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
inst✝ : S.HasLeftHomology
hg : S.g = 0
this : IsIso S.iCycles
⊢ S.cycles ≅ S.X₂

Tactic:
exact asIso S.iCycles

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₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasRightHomology
inst✝ : S₂.HasRightHomology
⊢ (rightHomologyMap' φ S₁.rightHomologyData S₂.rightHomologyData).op =
    leftHomologyMap' (𝟙 S₂.op) S₂.rightHomologyData.op S₂.op.leftHomologyData ≫
      leftHomologyMap' (opMap φ) S₂.op.leftHomologyData S₁.op.leftHomologyData ≫
        leftHomologyMap' (𝟙 S₁.op) S₁.op.leftHomologyData S₁.rightHomologyData.op

Tactic:
simp only [← leftHomologyMap'_comp, comp_id, id_comp, rightHomologyMap'_op]

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
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : HasKernels Cᵒᵖ
inst✝ : HasCokernels Cᵒᵖ
⊢ ∀ {X Y : (ShortComplex C)ᵒᵖ} (f : X ⟶ Y),
    (rightHomologyFunctor C).op.map f ≫ (Opposite.unop Y).leftHomologyOpIso.symm.hom =
      (Opposite.unop X).leftHomologyOpIso.symm.hom ≫ (opFunctor C ⋙ leftHomologyFunctor Cᵒᵖ).map f

Tactic:
by simp [rightHomologyMap_op]

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

Goal state before:
pp: case refine_3
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₂✝ : IsIso φ.τ₂
h₁✝ : Epi φ.τ₁
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ h₂.descQ (inv φ.τ₂ ≫ h₁.p) ⋯ ≫ opcyclesMap' φ h₁ h₂ = 𝟙 h₂.Q

Tactic:
· simp only [← cancel_epi h₂.p, h₂.p_descQ_assoc, assoc, p_opcyclesMap',
      IsIso.inv_hom_id_assoc, comp_id]

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

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✝¹ : Preadditive C
inst✝ : Preadditive D
S✝ : ShortComplex C
S : ShortComplex Cᵒᵖ
h : S.Splitting
⊢ (h.s.unop ≫ S.unop.f + S.unop.g ≫ h.r.unop).op = (𝟙 S.unop.X₂).op

Tactic:
by
    simp only [unop_X₂, Opposite.op_unop, unop_X₁, unop_f, unop_X₃, unop_g, op_add,
      op_comp, Quiver.Hom.op_unop, op_id, ← h.id]
    abel

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 g : Over X
k : f ⟶ g
⊢ (forget X).obj (imageMonoOver f.hom) ⟶ (forget X).obj (imageMonoOver g.hom)

Tactic:
apply Over.homMk _ _

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasImages C
f g : Over X
k : f ⟶ g
⊢ ((forget X).obj (imageMonoOver f.hom)).left ⟶ ((forget X).obj (imageMonoOver g.hom)).left

C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasImages C
f g : Over X
k : f ⟶ g
⊢ ?m.43 ≫ ((forget X).obj (imageMonoOver g.hom)).hom = ((forget X).obj (imageMonoOver f.hom)).hom
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f : X✝ ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasKernels C
X : C
⊢ ∀ ⦃A B : Cᵒᵖ⦄ (f : A ⟶ op X) (g : B ⟶ op X) [inst : Mono f] [inst_1 : Mono g],
    Subobject.mk f ≤ Subobject.mk g →
      Subobject.lift (fun x f x_1 ↦ Subobject.mk (kernel.ι f.unop)) ⋯ (Subobject.mk f) ≤
        Subobject.lift (fun x f x_1 ↦ Subobject.mk (kernel.ι f.unop)) ⋯ (Subobject.mk g)

Tactic:
intro A B f g hf hg h
      dsimp only [Subobject.lift_mk]
      refine Subobject.mk_le_mk_of_comm (kernel.lift g.unop (kernel.ι f.unop) ?_) ?_
      · rw [← Subobject.ofMkLEMk_comp h, unop_comp, kernel.condition_assoc, zero_comp]
      · exact Quiver.Hom.op_inj (by simp)

Goal state after: