mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: case refine_1
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (Pi.evalRingHom R i) S
r₁ : (i : ι) → R i
s₁ : ↥T
r₂ : (i : ι) → R i
s₂ : ↥T
eq :
  (mapPiEvalRingHom S) (mk' (Localization (Submonoid.comap (Pi.evalRingHom R i) S)) r₁ s₁) =
    (mapPiEvalRingHom S) (mk' (Localization (Submonoid.comap (Pi.evalRingHom R i) S)) r₂ s₂)
⊢ mk' (Localization (Submonoid.comap (Pi.evalRingHom R i) S)) r₁ s₁ =
    mk' (Localization (Submonoid.comap (Pi.evalRingHom R i) S)) r₂ s₂

Tactic:
map_mk'

Goal state after:
case refine_1
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (Pi.evalRingHom R i) S
r₁ : (i : ι) → R i
s₁ : ↥T
r₂ : (i : ι) → R i
s₂ : ↥T
eq :
  mk' (Localization S) ((Pi.evalRingHom R i) r₁) ⟨(Pi.evalRingHom R i) ↑s₁, ⋯⟩ =
    mk' (Localization S) ((Pi.evalRingHom R i) r₂) ⟨(Pi.evalRingHom R i) ↑s₂, ⋯⟩
⊢ mk' (Localization (Submonoid.comap (Pi.evalRingHom R i) S)) r₁ s₁ =
    mk' (Localization (Submonoid.comap (Pi.evalRingHom R i) S)) r₂ s₂
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: case exists_of_eq
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
x y : R
⊢ h.symm.toEquiv ((algebraMap R P) x) = h.symm.toEquiv ((algebraMap R P) y) → ∃ c, ↑c * x = ↑c * y

Tactic:
← IsLocalization.eq_iff_exists M S,

Goal state after:
case exists_of_eq
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
x y : R
⊢ h.symm.toEquiv ((algebraMap R P) x) = h.symm.toEquiv ((algebraMap R P) y) → (algebraMap R S) x = (algebraMap R S) y
Module: Mathlib.RingTheory.Adjoin.Basic

Goal state before:
pp: R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
⊢ adjoin R (s ∪ t) = Subalgebra.restrictScalars R (adjoin (↥(adjoin R s)) t)

Tactic:
by
  simpa using adjoin_algebraMap_image_union_eq_adjoin_adjoin R s t

Goal state after:
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: A : Type u_4
inst✝¹⁹ : CommRing A
B : Type u_6
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
K₁ : Type u_8
K₂ : Type u_9
inst✝¹⁶ : Field K₁
inst✝¹⁵ : Field K₂
inst✝¹⁴ : Algebra A K₁
inst✝¹³ : Algebra A K₂
inst✝¹² : IsFractionRing A K₁
L₁ : Type u_10
L₂ : Type u_11
inst✝¹¹ : Field L₁
inst✝¹⁰ : Field L₂
inst✝⁹ : Algebra B L₁
inst✝⁸ : Algebra B L₂
inst✝⁷ : Algebra K₁ L₁
inst✝⁶ : Algebra K₂ L₂
inst✝⁵ : Algebra A L₁
inst✝⁴ : Algebra A L₂
inst✝³ : IsScalarTower A K₁ L₁
inst✝² : IsScalarTower A K₂ L₂
inst✝¹ : IsScalarTower A B L₁
inst✝ : IsScalarTower A B L₂
e : K₁ ≃ₐ[A] K₂
f : L₁ ≃ₐ[B] L₂
x : K₁
⊢ (algebraMap K₂ L₂) (e x) = f ((algebraMap K₁ L₁) x)

Tactic:
exact algHom_commutes e.toAlgHom f.toAlgHom _

Goal state after:
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: A : Type u_8
B : Type u_9
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra A B
K : Type u_10
L : Type u_11
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra A K
inst✝⁶ : Algebra B L
inst✝⁵ : IsFractionRing A K
inst✝⁴ : IsFractionRing B L
inst✝³ : Algebra A L
inst✝² : IsScalarTower A B L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower A K L
⊢ Injective ⇑(fieldEquivOfAlgEquivHom K L)

Tactic:
intro f g h
  ext b
  simpa using AlgEquiv.ext_iff.mp h (algebraMap B L b)

Goal state after:
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: case inl
R : Type u_8
S : Type u_9
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
h : IsFractionRing R S
left✝ : Nontrivial R
right✝ : Subsingleton S
⊢ False

Tactic:
obtain ⟨c, hc⟩ := h.exists_of_eq (x := 1) (y := 0) (Subsingleton.elim _ _)

Goal state after:
case inl
R : Type u_8
S : Type u_9
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
h : IsFractionRing R S
left✝ : Nontrivial R
right✝ : Subsingleton S
c : ↥R⁰
hc : ↑c * 1 = ↑c * 0
⊢ False
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommRing P
A : Type u_4
inst✝¹ : CommRing A
K : Type u_5
inst✝ : DecidableEq R
⊢ DecidableEq (FractionRing R)

Tactic:
intro x y
  apply Localization.recOnSubsingleton₂ x y (r := fun x y ↦ Decidable (x = y))
  intro a c b d
  simp only [Localization.mk_eq_mk_iff, Localization.r_iff_of_le_nonZeroDivisors (le_refl _)]
  infer_instance

Goal state after:
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: case refine_2.refine_1
R : Type u_1
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
p : R
hp : p ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
⊢ ∀ x ∈ range fun s ↦ star s * s, ∀ (x_1 y : R), y = x_1 + x → x_1 ≤ y

Tactic:
rintro _ ⟨s, rfl⟩ x y rfl
        exact (h_le_iff _ _).mpr ⟨s, rfl⟩

Goal state after:
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
p : R
hp : IsStarProjection p
⊢ p ∈ Icc 0 1

Tactic:
simp only [Set.mem_Icc, hp.nonneg, hp.le_one, and_self]

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

Goal state before:
pp: F : Type u_2
E : Type u_3
inst✝² : CommSemiring F
inst✝¹ : Semiring E
inst✝ : Algebra F E
⊢ Module.rank F ↥⊤ = Module.rank F ↥⊤

Tactic:
rw [← Algebra.top_toSubmodule]
  rfl

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

Goal state before:
pp: F : Type u_2
E : Type u_3
inst✝² : CommSemiring F
inst✝¹ : Semiring E
inst✝ : Algebra F E
⊢ finrank F ↥⊤ = finrank F ↥⊤

Tactic:
rw [← Algebra.top_toSubmodule]
  rfl

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

Goal state before:
pp: K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
ι : Type u_1
inst✝ : Unique ι
h✝ : finrank K V = 1
v : V
hv : v ≠ 0
b : Basis ι K V := basisUnique ι h✝
h : (b.repr v) default ≠ 0
w : V
⊢ b.repr ((fun f ↦ f default • v) ((fun w ↦ Finsupp.single default ((b.repr w) default / (b.repr v) default)) w)) =
    b.repr w

Tactic:
apply_fun Finsupp.uniqueEquiv default

Goal state after:
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
ι : Type u_1
inst✝ : Unique ι
h✝ : finrank K V = 1
v : V
hv : v ≠ 0
b : Basis ι K V := basisUnique ι h✝
h : (b.repr v) default ≠ 0
w : V
⊢ (Finsupp.uniqueEquiv default)
      (b.repr
        ((fun f ↦ f default • v) ((fun w ↦ Finsupp.single default ((b.repr w) default / (b.repr v) default)) w))) =
    (Finsupp.uniqueEquiv default) (b.repr w)
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
f g : End K (Fin n → K)
hfg : f * g = 1
x : Fin n → K
⊢ (f * g) x = 1 x

Tactic:
rw [hfg]

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

Goal state before:
pp: case empty
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
comm : (↑∅).Pairwise (Commute on f)
h : ∅.SupIndep fun i ↦ (f i).ker
⊢ (∅.noncommProd f comm).ker = ⨆ i ∈ ∅, (f i).ker

Tactic:
simp [Module.End.one_eq_id]

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

Goal state before:
pp: K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Free K V
inst✝ : Module.Finite K V
⊢ finrank K V ≤ 1 ↔ ↑(finrank K V) ≤ 1

Tactic:
Nat.cast_le_one

Goal state after:
K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Free K V
inst✝ : Module.Finite K V
⊢ finrank K V ≤ 1 ↔ finrank K V ≤ 1
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
W : Submodule K V
inst✝¹ : Free K ↥W
inst✝ : Module.Finite K ↥W
⊢ finrank K ↥W ≤ 1 ↔ ↑(finrank K ↥W) ≤ 1

Tactic:
Nat.cast_le_one

Goal state after:
K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
W : Submodule K V
inst✝¹ : Free K ↥W
inst✝ : Module.Finite K ↥W
⊢ finrank K ↥W ≤ 1 ↔ finrank K ↥W ≤ 1
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
m : ℕ
⊢ LinearMap.ker (f ^ k) ≤ LinearMap.ker (f ^ (m + 1 + k))

Tactic:
pow_add

Goal state after:
case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
m : ℕ
⊢ LinearMap.ker (f ^ k) ≤ LinearMap.ker (f ^ (m + 1) * f ^ k)
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: case append_singleton
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
ps : List R[X]
p : R[X]
ihp : (∀ p ∈ ps, ∀ (k : ℕ), Commute (f (p.coeff k)) x) → eval₂ f x ps.prod = (List.map (eval₂ f x) ps).prod
hf : ∀ p_1 ∈ ps ++ [p], ∀ (k : ℕ), Commute (f (p_1.coeff k)) x
⊢ eval₂ f x (ps ++ [p]).prod = (List.map (eval₂ f x) (ps ++ [p])).prod

Tactic:
| append_singleton ps p ihp =>

Goal state after:
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
⊢ 2 ≤ k

Tactic:
subst e

Goal state after:
n : ℕ
n2 : 2 ≤ n
i : ℕ
k : ℕ := 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → 2 * i + 3 ≤ m
h : ¬n < k * k
⊢ 2 ≤ k
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ¬∀ (p : ℕ), ↑p = 0 → p = 0
x : ℕ
H1 : ↑x = 0
H2 : ¬x % Nat.find ⋯ = 0
⊢ ↑(x % Nat.find ⋯) = 0

Tactic:
rwa [← Nat.mod_add_div x (Nat.find (not_forall.1 H)), Nat.cast_add,
                      Nat.cast_mul,
                      of_not_not (not_not_of_not_imp <| Nat.find_spec (not_forall.1 H)),
                      zero_mul, add_zero] at H1

Goal state after:
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: n : ℕ
pos : 0 < n
np : ¬Prime n
h1 : n = n.minFac * 1
⊢ n.minFac ≤ n / n.minFac

Tactic:
by
    rw [mul_one] at h1
    rw [prime_def_minFac, not_and_or, ← h1, eq_self_iff_true, _root_.not_true, _root_.or_false,
      not_le] at np
    rw [le_antisymm (le_of_lt_succ np) (succ_le_of_lt pos), minFac_one, Nat.div_one]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_4
M : Type u_7
N : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Monoid M
inst✝ : Monoid N
m : M
n : N
a : A
⊢ (curryAlgEquiv R).symm (single m (single n a)) = single (m, n) a

Tactic:
by
  simp [curryAlgEquiv]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
x✝¹ x✝ : MulAut M
⊢ domCongr R A (MulEquiv.trans x✝ x✝¹) = (domCongr R A x✝).trans (domCongr R A x✝¹)

Tactic:
trans_domCongr_domCongr

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
x✝¹ x✝ : MulAut M
⊢ domCongr R A (MulEquiv.trans x✝ x✝¹) = domCongr R A (MulEquiv.trans x✝ x✝¹)
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
h : q.coeff p.natDegree ≠ 0
hp : ¬p = 0
⊢ p.degree ≤ q.degree

Tactic:
· rw [degree_eq_natDegree hp]
    exact le_degree_of_ne_zero h

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
a : R
⊢ (C a * X ^ n).degree ≤ ↑n

Tactic:
by
  rw [C_mul_X_pow_eq_monomial]
  apply degree_monomial_le

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case pos
R : Type u_7
A : Type u_8
B : Type u_9
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : SemilatticeSup B
inst✝² : OrderBot B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s : Finset ι
f : ι → R[A]
h✝ : 1 = 0
⊢ ⊥ ≤ 0

pp: case neg
R : Type u_7
A : Type u_8
B : Type u_9
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : SemilatticeSup B
inst✝² : OrderBot B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s : Finset ι
f : ι → R[A]
h✝ : ¬1 = 0
⊢ D 0 ≤ 0

Tactic:
exacts [bot_le, hzero.le]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
ι : Type u_1
s✝ : Finset ι
f : ι → R[X]
a : ι
s : Finset ι
has : a ∉ s
ih : (∑ i ∈ s, f i).degree ≤ s.sup fun b ↦ (f b).degree
⊢ (f a + ∑ x ∈ s, f x).degree ≤ max (f a).degree (∑ i ∈ s, f i).degree

Tactic:
exact degree_add_le _ _

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
ι : Type u_1
s✝ : Finset ι
f : ι → R[X]
a : ι
s : Finset ι
has : a ∉ s
ih : (∑ i ∈ s, f i).degree ≤ s.sup fun b ↦ (f b).degree
⊢ max (f a).degree (∑ i ∈ s, f i).degree ≤ (cons a s has).sup fun b ↦ (f b).degree

Tactic:
rw [sup_cons]

Goal state after:
R : Type u
inst✝ : Semiring R
ι : Type u_1
s✝ : Finset ι
f : ι → R[X]
a : ι
s : Finset ι
has : a ∉ s
ih : (∑ i ∈ s, f i).degree ≤ s.sup fun b ↦ (f b).degree
⊢ max (f a).degree (∑ i ∈ s, f i).degree ≤ max (f a).degree (s.sup fun b ↦ (f b).degree)
Module: Mathlib.Algebra.Polynomial.Degree.Support

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ #p.support ≤ p.natDegree + 1

Tactic:
by
  rw [← Finset.card_range (p.natDegree + 1)]
  exact Finset.card_le_card supp_subset_range_natDegree_succ

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Support

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.support.Nonempty ↔ p ≠ 0

Tactic:
rw [Ne, nonempty_iff_ne_empty, Ne, ← support_eq_empty]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
r : R
hr : r = 0
⊢ (C r * p).leadingCoeff = r

Tactic:
simp_all [leadingCoeff_mul']

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
r : R
hr : ¬r = 0
⊢ (C r * p).leadingCoeff = r

Tactic:
simp_all [leadingCoeff_mul']

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
⊢ (p * C a).degree = p.degree

Tactic:
obtain rfl | hp := eq_or_ne p 0
  · simp
  nontriviality R
  rw [degree_mul', degree_C ha.ne_zero]
  · simp
  · simpa [ha.mul_left_eq_zero]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 1
⊢ p = C (p.coeff p.natDegree) * X + C (p.coeff 0)

Tactic:
hnd,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 1
⊢ p = C (p.coeff 1) * X + C (p.coeff 0)
Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree

Goal state before:
pp: R : Type u
a b c : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ (C b * X + C c).degree < (C a * X ^ 2).degree

Tactic:
by
  simpa only [degree_C_mul_X_pow 2 ha] using! degree_linear_lt

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
a : R
inst✝ : Ring R
p : R[X]
hp : 0 < p.degree
⊢ (p - C a).degree = p.degree

Tactic:
rw [sub_eq_add_neg, ← C_neg, degree_add_C hp]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
h : p.degree < (-q).degree
⊢ (-q).leadingCoeff = -q.leadingCoeff

Tactic:
leadingCoeff_neg

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
h : p.degree < (-q).degree
⊢ -q.leadingCoeff = -q.leadingCoeff
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ eval 0 p = p.coeff 0 * 0 ^ 0

Tactic:
rw [eval_eq_sum]

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (p.sum fun e a ↦ a * 0 ^ e) = p.coeff 0 * 0 ^ 0
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.IsRoot 0 ↔ p.coeff 0 = 0

Tactic:
by
  rw [coeff_zero_eq_eval_zero, IsRoot]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
a : R
⊢ (X - C a).degree = 1

Tactic:
rw [sub_eq_add_neg, ← map_neg C a, degree_X_add_C]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: S : Type v
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑d.succ
⊢ ↑d.succ * ∑ x ∈ range d, ↑(d.choose x) * y ^ x + ↑d.succ * y ^ d - ↑d.succ * y ^ d =
    ∑ x_1 ∈ range (d + 1), ↑((d + 1).choose x_1) * (↑x_1 * y ^ (x_1 - 1))

Tactic:
add_sub_cancel_right,

Goal state after:
S : Type v
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑d.succ
⊢ ↑d.succ * ∑ x ∈ range d, ↑(d.choose x) * y ^ x = ∑ x_1 ∈ range (d + 1), ↑((d + 1).choose x_1) * (↑x_1 * y ^ (x_1 - 1))
Module: Mathlib.Data.Finsupp.Antidiagonal

Goal state before:
pp: case mp
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
i : α
h : (x + y) i = if a = i then n else 0
⊢ (if a = i then x a else 0) = x i ∧ (if a = i then y a else 0) = y i

Tactic:
Finsupp.add_apply

Goal state after:
case mp
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
i : α
h : x i + y i = if a = i then n else 0
⊢ (if a = i then x a else 0) = x i ∧ (if a = i then y a else 0) = y i
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
p q : R[X]
a b : R
inst✝ : Invertible a
⊢ p ∣ q.comp (C a * X + C b) ↔ p.comp (C ⅟a * (X - C b)) ∣ q

Tactic:
convert! map_dvd_iff <| algEquivCMulXAddC a b using 2

Goal state after:
case e'_1.e'_3
R : Type u
inst✝¹ : CommRing R
p q : R[X]
a b : R
inst✝ : Invertible a
⊢ p = (algEquivCMulXAddC a b) (p.comp (C ⅟a * (X - C b)))
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
α : Type u_2
s : Finset α
f : α → σ →₀ ℕ
g : α → R
⊢ (monomial (∑ i ∈ s, f i)) (∏ i ∈ s, g i) = ∏ i ∈ s, (monomial (f i)) (g i)

Tactic:
simp_rw [monomial_sum_index, map_prod, ← Finset.prod_mul_distrib, C_mul_monomial, mul_one]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
x : σ → ℕ
t : Finset σ
i : σ
hi : i ∈ t
hi' : ¬(Finsupp.indicator t fun i x_1 ↦ x i) i ≠ 0
⊢ X i ^ (Finsupp.indicator t fun i x_1 ↦ x i) i = 1

Tactic:
ne_eq,

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
x : σ → ℕ
t : Finset σ
i : σ
hi : i ∈ t
hi' : ¬¬(Finsupp.indicator t fun i x_1 ↦ x i) i = 0
⊢ X i ^ (Finsupp.indicator t fun i x_1 ↦ x i) i = 1
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ p.support ≠ ∅ ↔ p ≠ 0

Tactic:
ne_eq,

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ¬p.support = ∅ ↔ p ≠ 0
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: case add.refine_1
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial (↥s) R
t : Finset σ
q : MvPolynomial (↥t) R
⊢ MvPolynomial (↥(s ∪ t)) R

Tactic:
refine rename (Subtype.map id ?_) p + rename (Subtype.map id ?_) q <;>
        simp +contextual only [id, true_or, or_true,
          Finset.mem_union, forall_true_iff]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: case mul_X.refine_1
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial (↥s) R
⊢ MvPolynomial (↥(insert n s)) R

pp: case mul_X.refine_2
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial (↥s) R
⊢ (rename Subtype.val) p * X n = (rename Subtype.val) ?mul_X.refine_1

Tactic:
· refine rename (Subtype.map id ?_) p * X ⟨n, s.mem_insert_self n⟩
      simp +contextual only [id, or_true, Finset.mem_insert, forall_true_iff]

Goal state after:
case mul_X.refine_2
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial (↥s) R
⊢ (rename Subtype.val) p * X n = (rename Subtype.val) ((rename (Subtype.map id ⋯)) p * X ⟨n, ⋯⟩)
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : σ
f : MvPolynomial σ R
⊢ Multiset.count n (f.support.sup fun s ↦ toMultiset s) = f.support.sup fun m ↦ m n

Tactic:
Multiset.count_finset_sup

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : σ
f : MvPolynomial σ R
⊢ (f.support.sup fun a ↦ Multiset.count n (toMultiset a)) = f.support.sup fun m ↦ m n
Module: Mathlib.Data.Finsupp.Fin

Goal state before:
pp: n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
h : cons y s ≠ 0
h' : y = 0
c : s = 0
⊢ cons 0 0 = 0

Tactic:
Finsupp.cons_zero_zero

Goal state after:
n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
h : cons y s ≠ 0
h' : y = 0
c : s = 0
⊢ 0 = 0
Module: Mathlib.Data.Finsupp.Fin

Goal state before:
pp: n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
x : M
⊢ cons x s = single 0 y ↔ s = 0 ∧ x = y

Tactic:
← cons_zero_eq_single_zero,

Goal state after:
n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
x : M
⊢ cons x s = cons y 0 ↔ s = 0 ∧ x = y
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i (p + q) < degreeOf i p
⊢ degreeOf i p = degreeOf i q

Tactic:
by
  contrapose! h
  apply le_trans (Nat.le_max_left _ (q.degreeOf i))
  rcases Nat.lt_or_lt_of_ne h with h | h
  · simp [add_comm p q, degreeOf_add_eq_of_degreeOf_lt h, max_eq_right_of_lt h]
  · simp [degreeOf_add_eq_of_degreeOf_lt h, max_eq_left_of_lt h]

Goal state after:
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
⊢ ((X - C x) * P).eraseLead.eraseLead = (X - C x) * P.eraseLead

Tactic:
by_cases hp : P = 0

Goal state after:
case pos
R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : P = 0
⊢ ((X - C x) * P).eraseLead.eraseLead = (X - C x) * P.eraseLead

case neg
R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
⊢ ((X - C x) * P).eraseLead.eraseLead = (X - C x) * P.eraseLead