mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.UniqueFactorization

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : NoZeroDivisors R
inst✝ : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : a * c = 0
⊢ Prod.Lex (fun x1 x2 ↦ x1 < x2) DvdNotUnit (↑a.degree, a.leadingCoeff) (⊤, (a * c).leadingCoeff)

Tactic:
rw [hac, Polynomial.leadingCoeff_zero]

Goal state after:
case pos
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : NoZeroDivisors R
inst✝ : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : a * c = 0
⊢ Prod.Lex (fun x1 x2 ↦ x1 < x2) DvdNotUnit (↑a.degree, a.leadingCoeff) (⊤, 0)
Module: Mathlib.RingTheory.Polynomial.UniqueFactorization

Goal state before:
pp: σ : Type v
D : Type u
inst✝¹ : CommRing D
inst✝ : UniqueFactorizationMonoid D
f : D[X]
hf : f ≠ 0
G : Type u := { g // g.Monic ∧ g ∣ f }
y : Associates D[X] := Associates.mk f
⊢ Fintype G

Tactic:
have hy : y ≠ 0 := Associates.mk_ne_zero.mpr hf

Goal state after:
σ : Type v
D : Type u
inst✝¹ : CommRing D
inst✝ : UniqueFactorizationMonoid D
f : D[X]
hf : f ≠ 0
G : Type u := { g // g.Monic ∧ g ∣ f }
y : Associates D[X] := Associates.mk f
hy : y ≠ 0
⊢ Fintype G
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a p : α
ha0 : a ≠ 0
hp : Irreducible p
h : Associates.mk p ^ 1 ≤ Associates.mk a
⊢ (Associates.mk p).count (Associates.mk a).factors ≠ 0

Tactic:
Associates.prime_pow_dvd_iff_le (Associates.mk_ne_zero.mpr ha0)
      (Associates.irreducible_mk.mpr hp)

Goal state after:
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a p : α
ha0 : a ≠ 0
hp : Irreducible p
h : 1 ≤ (Associates.mk p).count (Associates.mk a).factors
⊢ (Associates.mk p).count (Associates.mk a).factors ≠ 0
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : Field R
p : R[X]
hp0 : p ≠ 0
hpu : ¬IsUnit p
⊢ Irreducible p ↔ ∀ (q : R[X]), q.Monic → q.natDegree ∈ Finset.Ioc 0 (p.natDegree / 2) → ¬q ∣ p

Tactic:
have : p * C (leadingCoeff p)⁻¹ ≠ 1 := by
    contrapose hpu
    exact .of_mul_eq_one _ hpu
  rw [← irreducible_mul_leadingCoeff_inv,
      (monic_mul_leadingCoeff_inv hp0).irreducible_iff_lt_natDegree_lt this,
      natDegree_mul_leadingCoeff_inv _ hp0]
  simp only [IsUnit.dvd_mul_right
    (isUnit_C.mpr (IsUnit.mk0 (leadingCoeff p)⁻¹ (inv_ne_zero (leadingCoeff_ne_zero.mpr hp0))))]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hs : s ∈ S⁰
p : R[X]
hp0 : p ≠ 0
hp : (aeval s) p = 0
q : R[X]
hpq : p = q * X ^ rootMultiplicity 0 p
hq : ¬q.coeff 0 = 0
⊢ ∃ q, q.coeff 0 ≠ 0 ∧ (aeval s) q = 0

Tactic:
hpq,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hs : s ∈ S⁰
p : R[X]
hp0 : p ≠ 0
q : R[X]
hp : (aeval s) (q * X ^ rootMultiplicity 0 p) = 0
hpq : p = q * X ^ rootMultiplicity 0 p
hq : ¬q.coeff 0 = 0
⊢ ∃ q, q.coeff 0 ≠ 0 ∧ (aeval s) q = 0
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι : Type u_1
inst✝³ : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)
inst✝¹ : DirectedSystem F fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝ : IsDirectedOrder ι
C : DirectLimit F f → DirectLimit F f → DirectLimit F f → Prop
ih : ∀ (i : ι) (x y z : F i), C ⟦⟨i, x⟩⟧ ⟦⟨i, y⟩⟧ ⟦⟨i, z⟩⟧
x y z : DirectLimit F f
⊢ C x y z

Tactic:
by
  obtain ⟨_, _, _, _, rfl, rfl, rfl⟩ := exists_eq_mk₃ f x y z; apply ih

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

Goal state before:
pp: case refine_3.inr
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p✝ p : K[X]
hp : p ≠ 0
ih : p ≠ 0 → (aeval x) p = 0 → (↑x)⁻¹ ∈ A
_ne_zero : p * X ≠ 0
x_eq : x = 0
⊢ (↑0)⁻¹ ∈ A

Tactic:
Subalgebra.coe_zero,

Goal state after:
case refine_3.inr
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p✝ p : K[X]
hp : p ≠ 0
ih : p ≠ 0 → (aeval x) p = 0 → (↑x)⁻¹ ∈ A
_ne_zero : p * X ≠ 0
x_eq : x = 0
⊢ 0⁻¹ ∈ A
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: case inl.inr
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
inst✝¹ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝ : InverseSystem f
j k : ι
h : k ≤ j
t : F j
equiv : (j_1 : ↑(Iio j)) → F ↑j_1 ≃ piLT X ↑j_1
nat : IsNatEquiv f equiv
equivLim : F j ≃ ↑(limit f j)
hi : IsSuccPrelimit j
H : ∀ (x : F j) (l : ↑(Iio j)), ↑(equivLim x) l = f ⋯ x
hj : j ∈ Iic j
hk✝ : k ∈ Iic j
hk : k < j
l : ↑(Iio ↑⟨k, hk✝⟩)
⊢ (equiv ⟨k, hk⟩) (f h t) l = (equiv ⟨k, hk⟩) (↑(equivLim t) ⟨k, hk⟩) ⟨↑⟨↑l, ⋯⟩, ⋯⟩

Tactic:
H

Goal state after:
case inl.inr
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
inst✝¹ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝ : InverseSystem f
j k : ι
h : k ≤ j
t : F j
equiv : (j_1 : ↑(Iio j)) → F ↑j_1 ≃ piLT X ↑j_1
nat : IsNatEquiv f equiv
equivLim : F j ≃ ↑(limit f j)
hi : IsSuccPrelimit j
H : ∀ (x : F j) (l : ↑(Iio j)), ↑(equivLim x) l = f ⋯ x
hj : j ∈ Iic j
hk✝ : k ∈ Iic j
hk : k < j
l : ↑(Iio ↑⟨k, hk✝⟩)
⊢ (equiv ⟨k, hk⟩) (f h t) l = (equiv ⟨k, hk⟩) (f ⋯ t) ⟨↑⟨↑l, ⋯⟩, ⋯⟩
Module: Mathlib.RingTheory.Finiteness.Small

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Small.{u, u_1} R
inst✝ : Module.Finite R M
this : Small.{u, u_2} ↥⊤
⊢ Small.{u, u_2} M

Tactic:
rwa [← small_univ_iff]

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Small

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : Small.{u, u_1} R
inst✝ : FiniteType R S
this : Small.{u, u_2} ↥⊤
⊢ Small.{u, u_2} S

Tactic:
rwa [← small_univ_iff]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness

Goal state before:
pp: case insert.refine_2.refine_2
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
s✝ : Set (M ⊗[R] N)
a : M ⊗[R] N
s : Set (M ⊗[R] N)
a✝ : a ∉ s
hs✝ : s.Finite
M' : Submodule R M
N' : Submodule R N
hM' : M'.FG
hN' : N'.FG
h : s ⊆ ↑(mapIncl M' N').range
x : M
y : N
z : M ⊗[R] N
hz : z ∈ s
⊢ z ∈ ↑(mapIncl (M' ⊔ R ∙ x) (N' ⊔ R ∙ y)).range

Tactic:
exact range_mapIncl_mono le_sup_left le_sup_left (h hz)

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R M
inst✝⁷ : Module R N
M₁ : Type u_5
M₂ : Type u_6
N₂ : Type u_8
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R N₂
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
g : M₁ →ₗ[R] N₂ →ₗ[R] N
hg : IsTensorProduct g
i : M₂ →ₗ[R] N₂
hi : Function.Injective ⇑i
inst✝ : Module.Flat R M₁
x x✝¹ x✝ : M
hx : (hf.map hg LinearMap.id i) x✝¹ = (⇑hg.equiv ∘ ⇑(LinearMap.lTensor M₁ i) ∘ ⇑hf.equiv.symm) x✝¹
hy : (hf.map hg LinearMap.id i) x✝ = (⇑hg.equiv ∘ ⇑(LinearMap.lTensor M₁ i) ∘ ⇑hf.equiv.symm) x✝
⊢ (hf.map hg LinearMap.id i) (x✝¹ + x✝) = (⇑hg.equiv ∘ ⇑(LinearMap.lTensor M₁ i) ∘ ⇑hf.equiv.symm) (x✝¹ + x✝)

Tactic:
by simp [hx, hy]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R M
inst✝⁷ : Module R N
M₁ : Type u_5
M₂ : Type u_6
N₁ : Type u_7
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : AddCommMonoid N₁
inst✝¹ : Module R N₁
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
g : N₁ →ₗ[R] M₂ →ₗ[R] N
hg : IsTensorProduct g
i : M₁ →ₗ[R] N₁
hi : Function.Injective ⇑i
inst✝ : Module.Flat R M₂
x x✝¹ x✝ : M
hx : (hf.map hg i LinearMap.id) x✝¹ = (⇑hg.equiv ∘ ⇑(LinearMap.rTensor M₂ i) ∘ ⇑hf.equiv.symm) x✝¹
hy : (hf.map hg i LinearMap.id) x✝ = (⇑hg.equiv ∘ ⇑(LinearMap.rTensor M₂ i) ∘ ⇑hf.equiv.symm) x✝
⊢ (hf.map hg i LinearMap.id) (x✝¹ + x✝) = (⇑hg.equiv ∘ ⇑(LinearMap.rTensor M₂ i) ∘ ⇑hf.equiv.symm) (x✝¹ + x✝)

Tactic:
by simp [hx, hy]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁴ : CommSemiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
M₁ : Type u_5
M₂ : Type u_6
N₁ : Type u_7
N₂ : Type u_8
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : Module R M₁
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N₁
inst✝² : Module R N₂
f : M₁ →ₗ[R] M₂ →ₗ[R] M
g : N₁ →ₗ[R] N₂ →ₗ[R] N
hf : IsTensorProduct f
hg : IsTensorProduct g
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
h₁ : Function.Injective ⇑i₁
h₂ : Function.Injective ⇑i₂
inst✝¹ : Module.Flat R M₂
inst✝ : Module.Flat R N₁
x x✝¹ x✝ : M
hx : (hf.map hg i₁ i₂) x✝¹ = (⇑hg.equiv ∘ ⇑(TensorProduct.map i₁ i₂) ∘ ⇑hf.equiv.symm) x✝¹
hy : (hf.map hg i₁ i₂) x✝ = (⇑hg.equiv ∘ ⇑(TensorProduct.map i₁ i₂) ∘ ⇑hf.equiv.symm) x✝
⊢ (hf.map hg i₁ i₂) (x✝¹ + x✝) = (⇑hg.equiv ∘ ⇑(TensorProduct.map i₁ i₂) ∘ ⇑hf.equiv.symm) (x✝¹ + x✝)

Tactic:
by simp [hx, hy]

Goal state after:
Module: Mathlib.Data.Finset.Density

Goal state before:
pp: α : Type u_2
inst✝ : Fintype α
⊢ ∅.dens = 0

Tactic:
by simp [dens]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁴ : CommSemiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
M₁ : Type u_5
M₂ : Type u_6
N₁ : Type u_7
N₂ : Type u_8
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : Module R M₁
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N₁
inst✝² : Module R N₂
f : M₁ →ₗ[R] M₂ →ₗ[R] M
g : N₁ →ₗ[R] N₂ →ₗ[R] N
hf : IsTensorProduct f
hg : IsTensorProduct g
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
h₁ : Function.Injective ⇑i₁
h₂ : Function.Injective ⇑i₂
inst✝¹ : Module.Flat R M₁
inst✝ : Module.Flat R N₂
x x✝¹ x✝ : M
hx : (hf.map hg i₁ i₂) x✝¹ = (⇑hg.equiv ∘ ⇑(TensorProduct.map i₁ i₂) ∘ ⇑hf.equiv.symm) x✝¹
hy : (hf.map hg i₁ i₂) x✝ = (⇑hg.equiv ∘ ⇑(TensorProduct.map i₁ i₂) ∘ ⇑hf.equiv.symm) x✝
⊢ (hf.map hg i₁ i₂) (x✝¹ + x✝) = (⇑hg.equiv ∘ ⇑(TensorProduct.map i₁ i₂) ∘ ⇑hf.equiv.symm) (x✝¹ + x✝)

Tactic:
by simp [hx, hy]

Goal state after:
Module: Mathlib.Data.Finset.Density

Goal state before:
pp: case hd
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
s : Finset α
inst✝ : Fintype β
f : α ↪ β
h✝ : Nonempty α
⊢ 0 < ↑(Fintype.card α)

pp: case a
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
s : Finset α
inst✝ : Fintype β
f : α ↪ β
h✝ : Nonempty α
⊢ Fintype.card α ≤ Fintype.card β

Tactic:
· exact mod_cast Fintype.card_pos

Goal state after:
case a
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
s : Finset α
inst✝ : Fintype β
f : α ↪ β
h✝ : Nonempty α
⊢ Fintype.card α ≤ Fintype.card β
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: ι : Type u_2
inst✝⁹ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁸ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁷ : (i : ι) → FunLike (H i) (G i) C
inst✝⁶ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁵ : IsDirectedOrder ι
inst✝⁴ : Nonempty ι
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MonoidHomClass (H i) (G i) C
g : (i : ι) → H i
h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)
x✝ : DirectLimit G f
i : ι
x : G i
⊢ DirectLimit.lift f (fun x ↦ ⇑(g x)) h (⟦⟨i, x⟩⟧)⁻¹ = (DirectLimit.lift f (fun x ↦ ⇑(g x)) h ⟦⟨i, x⟩⟧)⁻¹

Tactic:
by simp_rw [inv_def, lift_def, map_inv (g i)]

Goal state after:
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
n✝ : ℕ
xs ys : List α
h✝ : xs <+ ys
n : ℕ
l₁✝ l₂✝ : List α
a : α
h : l₁✝ <+ l₂✝
⊢ map (fun p ↦ a ::ₛ p) (List.sym n (a :: l₁✝)) ++ List.sym (n + 1) l₁✝ <+ List.sym (n + 1) (a :: l₂✝)

Tactic:
List.sym

Goal state after:
α : Type u_1
n✝ : ℕ
xs ys : List α
h✝ : xs <+ ys
n : ℕ
l₁✝ l₂✝ : List α
a : α
h : l₁✝ <+ l₂✝
⊢ map (fun p ↦ a ::ₛ p) (List.sym n (a :: l₁✝)) ++ List.sym (n + 1) l₁✝ <+
    map (fun p ↦ a ::ₛ p) (List.sym n (a :: l₂✝)) ++ List.sym (n + 1) l₂✝
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
⊢ (List.sym (n + 1) (x :: xs)).Nodup

Tactic:
List.sym

Goal state after:
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
⊢ (map (fun p ↦ x ::ₛ p) (List.sym n (x :: xs)) ++ List.sym (n + 1) xs).Nodup
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
f : (a : α) → P a → β
s : Sym2 α
g : (p : α × α) → (∀ a ∈ s(p.1, p.2), P a) → Sym2 β := fun p H ↦ s(f p.1 ⋯, f p.2 ⋯)
p q : α × α
hpq✝ : Rel α p q
hpq : p = q ∨ p = q.swap
Hq : ∀ a ∈ Quot.mk (Rel α) q, P a
Hp : ∀ a ∈ s(p.1, p.2), P a
h :
  ∀ {s₂ : Sym2 α} {e : s(p.1, p.2) = s₂} {H : ∀ a ∈ s₂, P a},
    Eq.ndrec (motive := fun s ↦ (∀ a ∈ s, P a) → Sym2 β) (g p) e H = g p Hp
⊢ f p.1 ⋯ = f q.1 ⋯ ∧ f p.2 ⋯ = f q.2 ⋯ ∨ (f p.1 ⋯, f p.2 ⋯) = (f q.2 ⋯, f q.1 ⋯)

Tactic:
apply hpq.imp <;> rintro rfl

Goal state after:
case f
α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
f : (a : α) → P a → β
s : Sym2 α
g : (p : α × α) → (∀ a ∈ s(p.1, p.2), P a) → Sym2 β := fun p H ↦ s(f p.1 ⋯, f p.2 ⋯)
p : α × α
Hp : ∀ a ∈ s(p.1, p.2), P a
h :
  ∀ {s₂ : Sym2 α} {e : s(p.1, p.2) = s₂} {H : ∀ a ∈ s₂, P a},
    Eq.ndrec (motive := fun s ↦ (∀ a ∈ s, P a) → Sym2 β) (g p) e H = g p Hp
hpq✝ : Rel α p p
hpq : p = p ∨ p = p.swap
Hq : ∀ a ∈ Quot.mk (Rel α) p, P a
⊢ f p.1 ⋯ = f p.1 ⋯ ∧ f p.2 ⋯ = f p.2 ⋯

case g
α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
f : (a : α) → P a → β
s : Sym2 α
g : (p : α × α) → (∀ a ∈ s(p.1, p.2), P a) → Sym2 β := fun p H ↦ s(f p.1 ⋯, f p.2 ⋯)
q : α × α
Hq : ∀ a ∈ Quot.mk (Rel α) q, P a
hpq✝ : Rel α q.swap q
hpq : q.swap = q ∨ q.swap = q.swap
Hp : ∀ a ∈ s(q.swap.1, q.swap.2), P a
h :
  ∀ {s₂ : Sym2 α} {e : s(q.swap.1, q.swap.2) = s₂} {H : ∀ a ∈ s₂, P a},
    Eq.ndrec (motive := fun s ↦ (∀ a ∈ s, P a) → Sym2 β) (g q.swap) e H = g q.swap Hp
⊢ (f q.swap.1 ⋯, f q.swap.2 ⋯) = (f q.2 ⋯, f q.1 ⋯)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
a : α
z : Sym2 α
h : a ∈ z
hd : Mem.other h = a
h' : s(a, Mem.other h) = z
⊢ z.IsDiag

Tactic:
rw [hd] at h'

Goal state after:
α : Type u_1
a : α
z : Sym2 α
h : a ∈ z
hd : Mem.other h = a
h' : s(a, a) = z
⊢ z.IsDiag
Module: Mathlib.CategoryTheory.ObjectProperty.Basic

Goal state before:
pp: C : Type u
D : Type u'
inst✝¹ : Category.{v, u} C
inst✝ : Category.{v', u'} D
P Q : ObjectProperty C
h : P ≤ Q
F : C ⥤ D
⊢ P.strictMap F ≤ Q.strictMap F

Tactic:
rintro _ ⟨X, hX⟩
  exact ⟨X, h _ hX⟩

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

Goal state before:
pp: case mpr
I : Type w₀
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ⟶ Y
⊢ (∀ (i : I), IsIso (f i)) → IsIso f

Tactic:
· intro
    exact ⟨fun i => inv (f i), by cat_disch, by cat_disch⟩

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

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : F.cones.RepresentableBy X
s : Cone F
⊢ (limitCone h).extend (homOfCone h s) = s

Tactic:
rw [← coneOfHom_homOfCone h s]

Goal state after:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : F.cones.RepresentableBy X
s : Cone F
⊢ (limitCone h).extend (homOfCone h (coneOfHom h (homOfCone h s))) = coneOfHom h (homOfCone h s)
Module: Mathlib.CategoryTheory.Functor.EpiMono

Goal state before:
pp: 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
X Y : C
f : X ⟶ Y
hf : Epi f
Z : D
g h : F.obj Y ⟶ Z
⊢ F.map f ≫ g = F.map f ≫ h → g = h

Tactic:
H

Goal state after:
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
X Y : C
f : X ⟶ Y
hf : Epi f
Z : D
g h : F.obj Y ⟶ Z
H : F.map f ≫ g = F.map f ≫ h
⊢ g = h
Module: Mathlib.CategoryTheory.Functor.EpiMono

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F : C ⥤ D
inst✝ : F.Faithful
X Y : C
f : X ⟶ Y
x✝ : Mono (F.map f)
Z : C
g h : Z ⟶ X
hgh : g ≫ f = h ≫ f
⊢ F.map (g ≫ f) = F.map h ≫ F.map f

Tactic:
hgh,

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F : C ⥤ D
inst✝ : F.Faithful
X Y : C
f : X ⟶ Y
x✝ : Mono (F.map f)
Z : C
g h : Z ⟶ X
hgh : g ≫ f = h ≫ f
⊢ F.map (h ≫ f) = F.map h ≫ F.map f
Module: Mathlib.CategoryTheory.Functor.EpiMono

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : F.IsEquivalence
inst✝¹ : SplitEpiCategory C
X Y : D
f : X ⟶ Y
inst✝ : Epi f
⊢ IsSplitEpi f

Tactic:
← F.inv.isSplitEpi_iff f

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : F.IsEquivalence
inst✝¹ : SplitEpiCategory C
X Y : D
f : X ⟶ Y
inst✝ : Epi f
⊢ IsSplitEpi (F.inv.map f)
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasLimitsOfSize.{v₁, u₁, v, u} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : Small.{u₁, u₂} J
inst✝ : LocallySmall.{v₁, v₂, u₂} J
this : HasLimitsOfShape (ShrinkHoms.{u₁} (Shrink.{u₁, u₂} J)) C
⊢ HasLimitsOfShape J C

Tactic:
exact hasLimitsOfShape_of_equivalence
    ((ShrinkHoms.equivalence _).symm.trans (Shrink.equivalence _).symm)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝² : Category.{v, u} C
ι : Type u_1
f : ι → Type u_2
g : (i : ι) → f i → C
inst✝¹ : ∀ (i : ι), HasProduct (g i)
inst✝ : HasProduct fun i ↦ ∏ᶜ g i
⊢ ∀ (s : Fan fun p ↦ g p.fst p.snd)
    (m : s.pt ⟶ (Fan.mk (∏ᶜ fun i ↦ ∏ᶜ g i) fun X ↦ Pi.π (fun i ↦ ∏ᶜ g i) X.fst ≫ Pi.π (g X.fst) X.snd).pt),
    (∀ (j : (i : ι) × f i),
        m ≫ (Fan.mk (∏ᶜ fun i ↦ ∏ᶜ g i) fun X ↦ Pi.π (fun i ↦ ∏ᶜ g i) X.fst ≫ Pi.π (g X.fst) X.snd).proj j = s.proj j) →
      m = Pi.lift fun b ↦ Pi.lift fun c ↦ s.proj ⟨b, c⟩

Tactic:
intro s (m : _ ⟶ (∏ᶜ fun i ↦ ∏ᶜ g i)) w; aesop (add norm simp Sigma.forall)

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝³ : Category.{v₁, u₁} T
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : T
f g : Over X
φ : f ⟶ g
F : T ⥤ D
inst✝¹ : F.Full
inst✝ : F.EssSurj
B : Over (F.obj X)
⊢ (post F).essImage B

Tactic:
obtain ⟨A', ⟨e⟩⟩ := Functor.EssSurj.mem_essImage (F := F) B.left

Goal state after:
T : Type u₁
inst✝³ : Category.{v₁, u₁} T
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : T
f g : Over X
φ : f ⟶ g
F : T ⥤ D
inst✝¹ : F.Full
inst✝ : F.EssSurj
B : Over (F.obj X)
A' : T
e : F.obj A' ≅ B.left
⊢ (post F).essImage B
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X : T
f✝ g✝ : Under X
φ : f✝ ⟶ g✝
f g : Under X
k : f ⟶ g
inst✝ : Epi k
Y : T
l m : g.right ⟶ Y
a : Hom.right k ≫ l = Hom.right k ≫ m
l' : g ⟶ mk (g.hom ≫ m) := homMk l ⋯
⊢ l' = homMk m ⋯

Tactic:
rw [← cancel_epi k]

Goal state after:
T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X : T
f✝ g✝ : Under X
φ : f✝ ⟶ g✝
f g : Under X
k : f ⟶ g
inst✝ : Epi k
Y : T
l m : g.right ⟶ Y
a : Hom.right k ≫ l = Hom.right k ≫ m
l' : g ⟶ mk (g.hom ≫ m) := homMk l ⋯
⊢ k ≫ l' = k ≫ homMk m ⋯
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ⟶ G.obj zero
q : F.obj one ⟶ G.obj one
hl : F.map left ≫ q = p ≫ G.map left
hr : F.map right ≫ q = p ≫ G.map right
⊢ ∀ ⦃X Y : WalkingParallelPair⦄ (f : X ⟶ Y),
    F.map f ≫ WalkingParallelPair.casesOn Y p q = WalkingParallelPair.casesOn X p q ≫ G.map f

Tactic:
rintro _ _ (_ | _)

Goal state after:
case left
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ⟶ G.obj zero
q : F.obj one ⟶ G.obj one
hl : F.map left ≫ q = p ≫ G.map left
hr : F.map right ≫ q = p ≫ G.map right
⊢ F.map left ≫ WalkingParallelPair.casesOn one p q = WalkingParallelPair.casesOn zero p q ≫ G.map left

case right
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ⟶ G.obj zero
q : F.obj one ⟶ G.obj one
hl : F.map left ≫ q = p ≫ G.map left
hr : F.map right ≫ q = p ≫ G.map right
⊢ F.map right ≫ WalkingParallelPair.casesOn one p q = WalkingParallelPair.casesOn zero p q ≫ G.map right

case id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ⟶ G.obj zero
q : F.obj one ⟶ G.obj one
hl : F.map left ≫ q = p ≫ G.map left
hr : F.map right ≫ q = p ≫ G.map right
X✝ : WalkingParallelPair
⊢ F.map (WalkingParallelPairHom.id X✝) ≫ WalkingParallelPair.casesOn X✝ p q =
    WalkingParallelPair.casesOn X✝ p q ≫ G.map (WalkingParallelPairHom.id X✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ≅ G.obj zero
q : F.obj one ≅ G.obj one
hl : F.map left ≫ q.hom = p.hom ≫ G.map left
hr : F.map right ≫ q.hom = p.hom ≫ G.map right
⊢ ∀ {X Y : WalkingParallelPair} (f : X ⟶ Y),
    F.map f ≫ (WalkingParallelPair.casesOn Y p q).hom = (WalkingParallelPair.casesOn X p q).hom ≫ G.map f

Tactic:
rintro _ _ (_ | _)

Goal state after:
case left
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ≅ G.obj zero
q : F.obj one ≅ G.obj one
hl : F.map left ≫ q.hom = p.hom ≫ G.map left
hr : F.map right ≫ q.hom = p.hom ≫ G.map right
⊢ F.map left ≫ (WalkingParallelPair.casesOn one p q).hom = (WalkingParallelPair.casesOn zero p q).hom ≫ G.map left

case right
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ≅ G.obj zero
q : F.obj one ≅ G.obj one
hl : F.map left ≫ q.hom = p.hom ≫ G.map left
hr : F.map right ≫ q.hom = p.hom ≫ G.map right
⊢ F.map right ≫ (WalkingParallelPair.casesOn one p q).hom = (WalkingParallelPair.casesOn zero p q).hom ≫ G.map right

case id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ≅ G.obj zero
q : F.obj one ≅ G.obj one
hl : F.map left ≫ q.hom = p.hom ≫ G.map left
hr : F.map right ≫ q.hom = p.hom ≫ G.map right
X✝ : WalkingParallelPair
⊢ F.map (WalkingParallelPairHom.id X✝) ≫ (WalkingParallelPair.casesOn X✝ p q).hom =
    (WalkingParallelPair.casesOn X✝ p q).hom ≫ G.map (WalkingParallelPairHom.id X✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X Y : C
inst✝³ : Category.{v, u} C
f g : X ⟶ Y
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasCoequalizer f g
inst✝ : HasCoequalizer (G.map f) (G.map g)
Z : C
h : Y ⟶ Z
w : f ≫ h = g ≫ h
⊢ coequalizerComparison f g G ≫ G.map (coequalizer.desc h w) = coequalizer.desc (G.map h) ⋯

Tactic:
by
  apply coequalizer.hom_ext
  simp [← G.map_comp]

Goal state after: