mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: case add
R : Type u
inst✝ : CommSemiring R
p q : R[X]
x : R
r s : R[X]
hr : eval x (r.comp q) = eval (eval x q) r
hs : eval x (s.comp q) = eval (eval x q) s
⊢ eval x ((r + s).comp q) = eval (eval x q) (r + s)

Tactic:
| add r s hr hs =>

Goal state after:
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
p : ℕ
hp : CharP R p
hq : ExpChar R 1
⊢ p = 0

Tactic:
cases hq
  · exact CharP.eq R hp (.ofCharZero R)
  · exact False.elim (CharP.char_ne_one R 1 rfl)

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case h'
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph = g.graph
⊢ ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥g.domain⦄, ↑x = ↑y → ↑f x = ↑g y

Tactic:
· apply (le_of_le_graph h.le).2

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case mpr
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
x_fst : E
x_snd : F
hx : (x_fst, x_snd) ∈ g
hx_fst : x_fst ∈ map (LinearMap.fst R E F) g
⊢ valFromGraph hg ⋯ = (x_fst, x_snd).2

Tactic:
exact (existsUnique_from_graph @hg hx_fst).unique (valFromGraph_mem hg hx_fst) hx

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

Goal state before:
pp: R : Type u_1
A : Type u_4
M : Type u_7
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Monoid M
F : M →* A
a : M
b : R
⊢ (liftNC ↑(algebraMap R A) ⇑F) (single a b) = b • F a

Tactic:
liftNC_single,

Goal state after:
R : Type u_1
A : Type u_4
M : Type u_7
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Monoid M
F : M →* A
a : M
b : R
⊢ ↑(algebraMap R A) b * F a = b • F a
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Preorder β
f g : α → β
a : α
l : Filter α
hle : g ≤ᶠ[l] f
hfga : f a = g a
h : IsMaxFilter f l a
x : α
hf : f x ≤ f a
hgf : g x ≤ f x
⊢ g x ≤ g a

Tactic:
rw [← hfga]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Preorder β
f g : α → β
a : α
l : Filter α
hle : g ≤ᶠ[l] f
hfga : f a = g a
h : IsMaxFilter f l a
x : α
hf : f x ≤ f a
hgf : g x ≤ f x
⊢ g x ≤ f a
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✝¹ : Algebra R A
inst✝ : Monoid M
r : R
⊢ (toAdditive A M).toFun ((algebraMap R A[M]) r) = (algebraMap R (AddMonoidAlgebra A (Additive M))) r

Tactic:
simp [toAdditive]

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

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ (C a).degree = 0

Tactic:
by
  rw [degree, ← monomial_zero_left, support_monomial 0 ha, max_eq_sup_coe, sup_singleton,
    WithBot.coe_zero]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.nextCoeff ≠ 0 ↔ p.natDegree ≠ 0 ∧ p.coeff (p.natDegree - 1) ≠ 0

Tactic:
simp [nextCoeff]

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

Goal state before:
pp: case mpr
R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
⊢ (∀ (i : ℕ), r ∣ φ.coeff i) → C r ∣ φ

Tactic:
intro h
    choose c hc using h
    classical
      let c' : ℕ → R := fun i => if i ∈ φ.support then c i else 0
      let ψ : R[X] := ∑ i ∈ φ.support, monomial i (c' i)
      use ψ
      ext i
      simp only [c', ψ, coeff_C_mul, mem_support_iff, coeff_monomial, finsetSum_coeff,
        Finset.sum_ite_eq']
      split_ifs with hi
      · rw [hc]
      · rw [Classical.not_not] at hi
        rwa [mul_zero]

Goal state after:
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:
← Finset.card_range (p.natDegree + 1)

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ #p.support ≤ #(range (p.natDegree + 1))
Module: Mathlib.Algebra.Polynomial.Degree.Domain

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h2 : p * q ≠ 0
⊢ p.natDegree ≤ (p * q).natDegree

Tactic:
rw [mul_ne_zero_iff] at h2

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h2 : p ≠ 0 ∧ q ≠ 0
⊢ p.natDegree ≤ (p * q).natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Domain

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h2 : p * q ≠ 0
⊢ p.degree ≤ (p * q).degree

Tactic:
rw [mul_ne_zero_iff] at h2

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h2 : p ≠ 0 ∧ q ≠ 0
⊢ p.degree ≤ (p * q).degree
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: n m : WithBot ℕ
h : n < m
⊢ n + 1 ≤ m

Tactic:
by
  cases n
  · simp only [WithBot.bot_add, bot_le]
  cases m
  · exact (not_lt_bot h).elim
  · rwa [WithBot.coe_lt_coe, ← Nat.add_one_le_iff, ← WithBot.coe_le_coe, WithBot.coe_add,
      WithBot.coe_one] at h

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : p.degree ≤ 1
n✝ n m : ℕ
⊢ p.coeff m.succ.succ = (C (p.coeff 1) * X + C (p.coeff 0)).coeff m.succ.succ

Tactic:
have : degree p < m.succ.succ := lt_of_le_of_lt h Nat.one_lt_ofNat

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.degree ≤ 1
n✝ n m : ℕ
this : p.degree < ↑m.succ.succ
⊢ p.coeff m.succ.succ = (C (p.coeff 1) * X + C (p.coeff 0)).coeff m.succ.succ
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type u_2
inst✝ : SMulZeroClass S R
a : S
p : R[X]
⊢ (a • p).degree ≤ p.degree

Tactic:
by
  refine (degree_le_iff_coeff_zero _ _).2 fun m hm => ?_
  rw [degree_lt_iff_coeff_zero] at hm
  simp [hm m le_rfl]

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : R[X]
_hp : p ∈ ⊤
⊢ p ∈ R[ X]

Tactic:
set S := adjoin R ({X} : Set R[X])

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : R[X]
_hp : p ∈ ⊤
S : Subalgebra R R[X] := R[ X]
⊢ p ∈ S
Module: Mathlib.RingTheory.Adjoin.Polynomial.Basic

Goal state before:
pp: R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R
n : ℕ
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : CommSemiring A'
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p✝ q✝ : R[X]
x : A
x✝¹ x✝ : ↥R[x]
p : A
hp : p ∈ R[x]
q : A
hq : q ∈ R[x]
⊢ ⟨p, hp⟩ * ⟨q, hq⟩ = ⟨q, hq⟩ * ⟨p, hp⟩

Tactic:
by
      obtain ⟨p', rfl⟩ := Algebra.adjoin_singleton_eq_range_aeval R x ▸ hp
      obtain ⟨q', rfl⟩ := Algebra.adjoin_singleton_eq_range_aeval R x ▸ hq
      simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, MulMemClass.mk_mul_mk, ← map_mul,
        mul_comm p' q']

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
⊢ (map f p).degree ≤ p.degree

Tactic:
by
  refine (degree_le_iff_coeff_zero _ _).2 fun m hm => ?_
  rw [degree_lt_iff_coeff_zero] at hm
  simp [hm m le_rfl]

Goal state after:
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsBotZeroClass α
f g : ι →₀ α
⊢ Disjoint f g ↔ Disjoint f.support g.support

Tactic:
by
  classical
  simp [disjoint_iff, bot_eq_zero, ← Finsupp.support_eq_empty]

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
v : M
p : R[X]
⊢ (p.sum fun e a ↦ (algebraMap R (M →ₗ[R] M)) a * f ^ e) v = p.sum fun n b ↦ b • (f ^ n) v

Tactic:
exact map_sum (LinearMap.applyₗ v) _ _

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

Goal state before:
pp: case e'_2.e'_3
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
n : ℕ
⊢ X ^ n = (algEquivAevalXAddC t) ((X - C t) ^ n)

Tactic:
simp [C_eq_algebraMap]

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

Goal state before:
pp: case h
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
s : σ
⊢ coeff (Finsupp.single s 1) (X s) ≠ 0

Tactic:
simp only [coeff_X_same, ne_eq, one_ne_zero, not_false_eq_true]

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

Goal state before:
pp: case refine_2
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M N : Submodule R S
x : MvPolynomial σ S
hx : x ∈ coeffsIn σ M
y : MvPolynomial σ S
hy : y ∈ coeffsIn σ N
k : σ →₀ ℕ
⊢ coeff k (x * y) ∈ M * N

Tactic:
rw [MvPolynomial.coeff_mul]

Goal state after:
case refine_2
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M N : Submodule R S
x : MvPolynomial σ S
hx : x ∈ coeffsIn σ M
y : MvPolynomial σ S
hy : y ∈ coeffsIn σ N
k : σ →₀ ℕ
⊢ ∑ x_1 ∈ Finset.antidiagonal k, coeff x_1.1 x * coeff x_1.2 y ∈ M * N
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case monomial_add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
f : R →+* S₁
inst✝ : DecidableEq S₁
a : σ →₀ ℕ
s : R
p : MvPolynomial σ R
ha : a ∉ p.coeff.support
hs : s ≠ 0
hp : ((map f) p).coeffs ⊆ Finset.image (⇑f) p.coeffs
ih : ((map f) ((monomial a) s)).coeffs ⊆ Finset.image (⇑f) ((monomial a) s).coeffs
⊢ ((map f) ((monomial a) s + p)).coeffs ⊆ Finset.image (⇑f) ((monomial a) s + p).coeffs

Tactic:
coeffs_add (disjoint_support_monomial ha hs),

Goal state after:
case monomial_add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
f : R →+* S₁
inst✝ : DecidableEq S₁
a : σ →₀ ℕ
s : R
p : MvPolynomial σ R
ha : a ∉ p.coeff.support
hs : s ≠ 0
hp : ((map f) p).coeffs ⊆ Finset.image (⇑f) p.coeffs
ih : ((map f) ((monomial a) s)).coeffs ⊆ Finset.image (⇑f) ((monomial a) s).coeffs
⊢ ((map f) ((monomial a) s + p)).coeffs ⊆ Finset.image (⇑f) (((monomial a) s).coeffs ∪ p.coeffs)
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: σ : Type u_1
A : Type u_3
inst✝¹ : CommRing A
inst✝ : NoZeroDivisors A
a : A
ha : a ≠ 0
φ : MvPolynomial σ A
⊢ (C a * φ).vars = φ.vars

Tactic:
ext1 i
  simp only [mem_vars_iff_mem_support, mem_support_iff]
  apply exists_congr
  intro d
  rw [coeff_C_mul, mul_ne_zero_iff, eq_true ha, true_and]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
i : σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ degreeOf i (∏ j ∈ s, f j) ≤ ∑ j ∈ s, degreeOf i (f j)

Tactic:
by
  simp_rw [degreeOf_eq_sup]
  exact supDegree_prod_le (by simp only [coe_zero, Pi.zero_apply]) (by simp)

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

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : Algebra R S₁
f : σ → S₁
⊢ (aeval f).range = Algebra.adjoin R (range f)

Tactic:
by
  apply le_antisymm
  · rintro x ⟨p, rfl⟩
    simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe]
    induction p using induction_on with
    | C a => exact aeval_C f a ▸ Subsemiring.subset_closure (Or.inl (Set.mem_range_self a))
    | add p q hp hq => rw [map_add]; exact Subalgebra.add_mem _ hp hq
    | mul_X p n h =>
      simp only [map_mul, aeval_X]
      exact Subalgebra.mul_mem _ h (Algebra.subset_adjoin (Set.mem_range_self n))
  · rw [Algebra.adjoin_le_iff]
    rintro x ⟨i, rfl⟩
    use X i, by aesop

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i : σ
e : ℕ
r : R
he : e ≠ 0
hr : r ≠ 0
⊢ ((monomial (Finsupp.single i e)) r).vars = {i}

Tactic:
vars_monomial hr,

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i : σ
e : ℕ
r : R
he : e ≠ 0
hr : r ≠ 0
⊢ (Finsupp.single i e).support = {i}
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
this : p.support.Nonempty
s : σ →₀ ℕ
hs1 : s ∈ p.support
hs2 : degreeOf i p = s i
⊢ s ∈ (p + q).support

Tactic:
have : s ∉ q.support := by
    contrapose! h
    rw [hs2]
    exact le_degreeOf_of_mem_support i h

Goal state after:
case a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
this✝ : p.support.Nonempty
s : σ →₀ ℕ
hs1 : s ∈ p.support
hs2 : degreeOf i p = s i
this : s ∉ q.support
⊢ s ∈ (p + q).support
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case monomial_add.refine_2
R : Type u
σ : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
subS : Type u_3
inst✝² : CommSemiring S
inst✝¹ : SetLike subS S
inst✝ : SubsemiringClass subS S
f✝ : R →+* S
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
a : σ →₀ ℕ
b : R
f : MvPolynomial σ R
ha : a ∉ f.coeff.support
a✝ : b ≠ 0
ih : (∀ (i : σ →₀ ℕ), f✝ (coeff i f) ∈ s) → eval₂ f✝ v f ∈ s
hs : ∀ (i : σ →₀ ℕ), f✝ (coeff i ((monomial a) b + f)) ∈ s
i : σ →₀ ℕ
this : f✝ (coeff i ((monomial a) b + f)) ∈ s
⊢ f✝ (coeff i f) ∈ s

Tactic:
rw [coeff_add, coeff_monomial] at this

Goal state after:
case monomial_add.refine_2
R : Type u
σ : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
subS : Type u_3
inst✝² : CommSemiring S
inst✝¹ : SetLike subS S
inst✝ : SubsemiringClass subS S
f✝ : R →+* S
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
a : σ →₀ ℕ
b : R
f : MvPolynomial σ R
ha : a ∉ f.coeff.support
a✝ : b ≠ 0
ih : (∀ (i : σ →₀ ℕ), f✝ (coeff i f) ∈ s) → eval₂ f✝ v f ∈ s
hs : ∀ (i : σ →₀ ℕ), f✝ (coeff i ((monomial a) b + f)) ∈ s
i : σ →₀ ℕ
this : f✝ ((if a = i then b else 0) + coeff i f) ∈ s
⊢ f✝ (coeff i f) ∈ s
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
h : p.coeff 0 = 0
hlt : p.degree ≤ 0
this : p = C (p.coeff 0)
⊢ False

Tactic:
simp only [h, map_zero] at this

Goal state after:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
h : p.coeff 0 = 0
hlt : p.degree ≤ 0
this : p = 0
⊢ False
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
f0 : 2 ≤ #f.support
⊢ f.eraseLead ≠ 0

Tactic:
by
  rw [Ne, ← card_support_eq_zero, eraseLead_support]
  exact
    (zero_lt_one.trans_le <| (tsub_le_tsub_right f0 1).trans Finset.pred_card_le_card_erase).ne.symm

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : #f.support ≤ 1
⊢ f.eraseLead.natDegree < f.natDegree ∨ f.eraseLead = 0

Tactic:
right

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : #f.support ≤ 1
⊢ f.eraseLead = 0
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Function.Injective ⇑f
p : R[X]
⊢ (if p.natDegree = 0 then 0 else (map f p).coeff (p.natDegree - 1)) =
    f (if p.natDegree = 0 then 0 else p.coeff (p.natDegree - 1))

Tactic:
split_ifs <;> simp

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

Goal state before:
pp: R : Type u_2
S₁ : Type u_3
S₂ : Type u_4
inst✝ : CommSemiring R
i : S₁
⊢ (commAlgEquiv R S₁ S₂) (X i) = C (X i)

Tactic:
by
  ext x y; simp [X, C, monomial, commAlgEquiv]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
p : R[X]
a : R
inst✝ : NoZeroDivisors R
a0 : a ≠ 0
⊢ (C a * p).natDegree = p.natDegree

Tactic:
by
  simp only [natDegree, degree_C_mul a0]

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
n : ℕ
r : R
a✝ : r ≠ 0
hnN : n ≤ N
⊢ i r * (⅟x ^ (N - n) * x ^ (N - n)) * x ^ n = i r * x ^ n

Tactic:
← mul_pow,

Goal state after:
case refine_2
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
n : ℕ
r : R
a✝ : r ≠ 0
hnN : n ≤ N
⊢ i r * (⅟x * x) ^ (N - n) * x ^ n = i r * x ^ n
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
⊢ p = X ^ p.natDegree + ∑ i ∈ range p.natDegree, C (p.coeff i) * X ^ i

Tactic:
by
  conv_lhs => rw [p.as_sum_range_C_mul_X_pow, sum_range_succ_comm]
  suffices C (p.coeff p.natDegree) = 1 by rw [this, one_mul]
  exact congr_arg C hp

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

Goal state before:
pp: case monomial.e_a
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ coeff m (if i = j 0 then ∏ x, X x ^ j x.succ else 0) = if j = cons i m then 1 else 0

Tactic:
obtain rfl | hjmi := eq_or_ne j (m.cons i)

Goal state after:
case monomial.e_a.inl
R : Type u
inst✝ : CommSemiring R
n : ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ coeff m (if i = (cons i m) 0 then ∏ x, X x ^ (cons i m) x.succ else 0) = if cons i m = cons i m then 1 else 0

case monomial.e_a.inr
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
hjmi : j ≠ cons i m
⊢ coeff m (if i = j 0 then ∏ x, X x ^ j x.succ else 0) = if j = cons i m then 1 else 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
σ : Type u_2
τ : Type u_3
f : σ → τ
i : σ
p : R[X]
⊢ (rename f) ((Polynomial.aeval (X i)) p) = (Polynomial.aeval (X (f i))) p

Tactic:
by
  rw [← aeval_algHom_apply, rename_X]

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

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
n : ℕ
x : R[X]
x_zero : ¬x = 0
⊢ x ∈ degreeLT R (n + 1) ↔ x ∈ degreeLE R ↑n

Tactic:
rw [mem_degreeLT, mem_degreeLE, ← natDegree_lt_iff_degree_lt (by rwa [ne_eq]),
      ← natDegree_le_iff_degree_le, Nat.lt_succ_iff]

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Tower

Goal state before:
pp: A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
hBC : ⊤.FG
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
⊢ ∃ B₀, B₀.FG ∧ ⊤.FG

Tactic:
obtain ⟨y, hy⟩ := hBC

Goal state after:
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
⊢ ∃ B₀, B₀.FG ∧ ⊤.FG
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
h : ⊤.FG
s : Finset A
hs : span R ↑s = ⊤
⊢ toSubmodule (Algebra.adjoin R ↑s) = toSubmodule ⊤

Tactic:
rw [Algebra.top_toSubmodule, eq_top_iff, ← hs, span_le]
    exact Algebra.subset_adjoin

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Operations

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
S' : Subalgebra R S
ι : Type u_3
ι' : Finset ι
s l : ι → S
e : ∑ i ∈ ι', l i * s i = 1
hs : ∀ (i : ι), s i ∈ S'
hl : ∀ (i : ι), l i ∈ S'
x : ↥S'
H : ∀ (i : ι), ∃ n, s i ^ n • (ofId (↥S') S).toRingHom x ∈ S'
⊢ (ofId (↥S') S).toRingHom x ∈ S'

Tactic:
exact x.2

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
⊢ p.leadingCoeff ∈ I.leadingCoeffNth N

Tactic:
rw [HN]

Goal state after:
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
⊢ p.leadingCoeff ∈ M
Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise

Goal state before:
pp: R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ toSubmodule S * toSubmodule T = toSubmodule (S ⊔ T)

Tactic:
refine le_antisymm (mul_toSubmodule_le _ _) ?_
  rintro x (hx : x ∈ Algebra.adjoin R (S ∪ T : Set A))
  refine
    Algebra.adjoin_induction (fun x hx => ?_) (fun r => ?_) (fun _ _ _ _ => Submodule.add_mem _)
      (fun x y _ _ hx hy => ?_) hx
  · rcases hx with hxS | hxT
    · rw [← mul_one x]
      exact Submodule.mul_mem_mul hxS (show (1 : A) ∈ T from one_mem T)
    · rw [← one_mul x]
      exact Submodule.mul_mem_mul (show (1 : A) ∈ S from one_mem S) hxT
  · rw [← one_mul (algebraMap _ _ _)]
    exact Submodule.mul_mem_mul (show (1 : A) ∈ S from one_mem S) (algebraMap_mem T _)
  have := Submodule.mul_mem_mul hx hy
  rwa [mul_assoc, mul_comm _ (Subalgebra.toSubmodule T), ← mul_assoc _ _ (Subalgebra.toSubmodule S),
    isIdempotentElem_toSubmodule, mul_comm T.toSubmodule, ← mul_assoc,
    isIdempotentElem_toSubmodule] at this

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_2
C : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : Module R A
inst✝³ : SMulCommClass R A A
inst✝² : IsScalarTower R A A
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A →ₙₐ[R] C
S : Subalgebra R C
h : NonUnitalAlgHom.range f ≤ S.toNonUnitalSubalgebra
x : Unitization R A
⊢ (lift f).toRingHom x ∈ S

Tactic:
induction x with
    | _ r a => simpa using! add_mem (algebraMap_mem S r) (h ⟨a, rfl⟩)

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_2
C : Type u_3
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing R
inst✝⁸ : StarRing A
inst✝⁷ : Module R A
inst✝⁶ : SMulCommClass R A A
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : StarModule R A
inst✝³ : Semiring C
inst✝² : StarRing C
inst✝¹ : Algebra R C
inst✝ : StarModule R C
f : A →⋆ₙₐ[R] C
S : StarSubalgebra R C
h : NonUnitalStarAlgHom.range f ≤ S.toNonUnitalStarSubalgebra
x : Unitization R A
⊢ (↑(starLift f)).toRingHom x ∈ S

Tactic:
induction x with
    | _ r a => simpa using! add_mem (algebraMap_mem S r) (h ⟨a, rfl⟩)

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

Goal state before:
pp: n : ℕ
⊢ ¬2 ∣ n ↔ Odd n

Tactic:
← not_even_iff_odd,

Goal state after:
n : ℕ
⊢ ¬2 ∣ n ↔ ¬Even n
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: case inr
x✝ y✝ p : ℕ
hp : Prime p
hx✝ : x✝ ≠ 1
hy✝ : y✝ ≠ 1
h✝ : x✝ * y✝ = p ^ 2
pdvdxy : p ∣ x✝ * y✝
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
a : ℕ
ha : x = p * a
this : a ∣ p
hap : a = p
⊢ y = 1

Tactic:
subst hap

Goal state after:
case inr
x✝ y✝ : ℕ
hx✝ : x✝ ≠ 1
hy✝ : y✝ ≠ 1
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
a : ℕ
hp : Prime a
h✝ : x✝ * y✝ = a ^ 2
pdvdxy : a ∣ x✝ * y✝
h : x * y = a ^ 2
ha : x = a * a
this : a ∣ a
⊢ y = 1