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

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

Tactic:
simpa only [C_1, one_mul] using degree_C_mul_X_pow_le n (1 : R)

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ ∑ x ∈ antidiagonal (p.natDegree + q.natDegree), p.coeff x.1 * q.coeff x.2 = p.coeff p.natDegree * q.coeff q.natDegree

Tactic:
by
      refine Finset.sum_eq_single (natDegree p, natDegree q) ?_ ?_
      · rintro ⟨i, j⟩ h₁ h₂
        rw [mem_antidiagonal] at h₁
        by_cases H : natDegree p < i
        · rw [coeff_eq_zero_of_degree_lt
              (lt_of_le_of_lt degree_le_natDegree (WithBot.coe_lt_coe.2 H)),
            zero_mul]
        · rw [not_lt_iff_eq_or_lt] at H
          rcases H with H | H
          · simp_all
          · suffices natDegree q < j by
              rw [coeff_eq_zero_of_degree_lt
                  (lt_of_le_of_lt degree_le_natDegree (WithBot.coe_lt_coe.2 this)),
                mul_zero]
            by_contra! H'
            exact
              ne_of_lt (Nat.lt_of_lt_of_le (Nat.add_lt_add_right H j) (Nat.add_le_add_left H' _))
                h₁
      · intro H
        exfalso
        apply H
        rw [mem_antidiagonal]

Goal state after:
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: n : ℕ
⊢ ↑0 ≤ ↑n

Tactic:
cast_withBot,

Goal state after:
n : ℕ
⊢ ↑0 ≤ ↑n
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p q : R[A]
D : A → B
inst✝ : AddZeroClass A
h : supDegree D q < supDegree D p
⊢ leadingCoeff D (p + q) = leadingCoeff D p

Tactic:
obtain ⟨a, he⟩ := supDegree_mem_range D (ne_zero_of_not_supDegree_le h.not_ge)
  rw [leadingCoeff, supDegree_add_eq_left h, coeff_add, Finsupp.add_apply, ← leadingCoeff,
    coeff_eq_zero_of_not_le_supDegree (D := D), add_zero]
  rw [← he, Function.apply_invFun_apply (f := D), he]; exact h.not_ge

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

Goal state before:
pp: R✝ : Type u
S : Type v
T : Type w
ι✝ : Type y
a b : R✝
m n : ℕ
inst✝³ : Semiring R✝
p✝ q r : R✝[X]
inst✝² : Semiring S
f : R✝ →+* S
ι : Type ?u.38
inst✝¹ : Finite ι
R : ι → Type u_1
inst✝ : (i : ι) → Semiring (R i)
p : (i : ι) → (R i)[X]
⊢ (RingHom.pi fun i ↦ mapRingHom (Pi.evalRingHom R i))
      { toFinsupp := ofCoeff (Finsupp.ofSupportFinite (fun n i ↦ (p i).coeff n) ⋯) } =
    p

Tactic:
ext i n

Goal state after:
R✝ : Type u
S : Type v
T : Type w
ι✝ : Type y
a b : R✝
m n✝ : ℕ
inst✝³ : Semiring R✝
p✝ q r : R✝[X]
inst✝² : Semiring S
f : R✝ →+* S
ι : Type ?u.38
inst✝¹ : Finite ι
R : ι → Type u_1
inst✝ : (i : ι) → Semiring (R i)
p : (i : ι) → (R i)[X]
i : ι
n : ℕ
⊢ ((RingHom.pi fun i ↦ mapRingHom (Pi.evalRingHom R i))
          { toFinsupp := ofCoeff (Finsupp.ofSupportFinite (fun n i ↦ (p i).coeff n) ⋯) } i).coeff
      n =
    (p i).coeff n
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

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

Tactic:
induction p using Polynomial.induction_on' with
  | add p q hp hq => simp only [hp, hq, Polynomial.map_add, map_add, eval_add]
  | monomial n r => simp only [one_pow, mul_one, eval_monomial, map_monomial]

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

Goal state before:
pp: case mp
R : Type u
inst✝ : Semiring R
f : R[X]
H : f.support.card ≤ 1
⊢ ∃ n a, f = (monomial n) a

Tactic:
rw [Finset.card_le_one_iff_subset_singleton] at H

Goal state after:
case mp
R : Type u
inst✝ : Semiring R
f : R[X]
H : ∃ x, f.support ⊆ {x}
⊢ ∃ n a, f = (monomial n) a
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u_3
inst✝¹ : CommRing R
a b : R
inst✝ : Invertible a
p : R[X]
⊢ (algEquivCMulXAddC a b).symm p = (algEquivCMulXAddC (⅟a) (-⅟a * b)) p

Tactic:
simp only [algEquivCMulXAddC_symm_apply, neg_mul, algEquivCMulXAddC_apply, map_neg, map_mul]

Goal state after:
R : Type u_3
inst✝¹ : CommRing R
a b : R
inst✝ : Invertible a
p : R[X]
⊢ (aeval (C ⅟a * (X - C b))) p = (aeval (C ⅟a * X + -(C ⅟a * C b))) p
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
inst✝ : (i : ι) → PartialOrder (β i)
r : ι → ι → Prop
hwf : WellFounded r
x y : (i : ι) → β i
hlt : x < y
⊢ Pi.Lex r (fun {i} x1 x2 ↦ x1 < x2) x y

Tactic:
simp_rw [Pi.Lex, le_antisymm_iff]
  exact lex_lt_of_lt_of_preorder hwf hlt

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₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
n : ℕ
⊢ eval₂ f g (p ^ (n + 1)) = eval₂ f g p ^ (n + 1)

Tactic:
pow_add,

Goal state after:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
n : ℕ
⊢ eval₂ f g (p ^ n * p ^ 1) = eval₂ f g p ^ (n + 1)
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
n : ℕ
⊢ eval₂ f g (p ^ n * p) = eval₂ f g p ^ (n + 1)

Tactic:
pow_add,

Goal state after:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
n : ℕ
⊢ eval₂ f g (p ^ n * p) = eval₂ f g p ^ n * eval₂ f g p ^ 1
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case pos
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
h : s ≤ m
⊢ coeff m (p * (monomial s) r) = coeff (m - s + s) (p * (monomial s) r)

Tactic:
tsub_add_cancel_of_le h

Goal state after:
case pos
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
h : s ≤ m
⊢ coeff m (p * (monomial s) r) = coeff m (p * (monomial s) r)
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
m : σ →₀ ℕ
s : σ
p : MvPolynomial σ R
⊢ (if Finsupp.single s 1 ≤ m then coeff (m - Finsupp.single s 1) p * 1 else 0) =
    if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0

Tactic:
Finsupp.single_le_iff,

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
m : σ →₀ ℕ
s : σ
p : MvPolynomial σ R
⊢ (if 1 ≤ m s then coeff (m - Finsupp.single s 1) p * 1 else 0) =
    if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
m : σ →₀ ℕ
s : σ
p : MvPolynomial σ R
⊢ (if Finsupp.single s 1 ≤ m then 1 * coeff (m - Finsupp.single s 1) p else 0) =
    if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0

Tactic:
Finsupp.single_le_iff,

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
m : σ →₀ ℕ
s : σ
p : MvPolynomial σ R
⊢ (if 1 ≤ m s then 1 * coeff (m - Finsupp.single s 1) p else 0) =
    if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
hf : Injective f
φ : R →+* S
p : MvPolynomial τ R
⊢ (↑(killCompl hf)).comp (map φ) = (map φ).comp ↑(killCompl hf)

Tactic:
ext i n

Goal state after:
case hC
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
hf : Injective f
φ : R →+* S
p : MvPolynomial τ R
i : R
n : σ →₀ ℕ
⊢ coeff n ((((↑(killCompl hf)).comp (map φ)).comp C) i) = coeff n ((((map φ).comp ↑(killCompl hf)).comp C) i)

case hX
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
hf : Injective f
φ : R →+* S
p : MvPolynomial τ R
i : τ
n : σ →₀ ℕ
⊢ coeff n (((↑(killCompl hf)).comp (map φ)) (X i)) = coeff n (((map φ).comp ↑(killCompl hf)) (X i))
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case refine_1
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
⊢ coeffsIn σ M ≤ Submodule.span R {x | ∃ m ∈ M, ∃ i, (monomial i) m = x}

Tactic:
rintro p hp
    rw [p.as_sum]
    exact sum_mem fun i hi ↦ Submodule.subset_span ⟨_, hp i, _, rfl⟩

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
⊢ (φ * ψ).degrees.toFinset ⊆ φ.degrees.toFinset ∪ ψ.degrees.toFinset

Tactic:
← Multiset.toFinset_add,

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
⊢ (φ * ψ).degrees.toFinset ⊆ (φ.degrees + ψ.degrees).toFinset
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: case succ
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
ih : (φ ^ n).vars ⊆ φ.vars
⊢ (φ * φ ^ n).vars ⊆ φ.vars

Tactic:
apply Finset.Subset.trans (vars_mul _ _)

Goal state after:
case succ
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
ih : (φ ^ n).vars ⊆ φ.vars
⊢ φ.vars ∪ (φ ^ n).vars ⊆ φ.vars
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : σ
k : ℕ
⊢ degreeOf i (X i ^ k) = k

Tactic:
rw [X_pow_eq_monomial, degreeOf_monomial_eq _ _ one_ne_zero, Finsupp.single_eq_same]

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

Goal state before:
pp: case insert
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
inst✝ : DecidableEq σ
f : ι → MvPolynomial σ R
a✝ : ι
s✝ : Finset ι
hs : a✝ ∉ s✝
hsub : (∏ i ∈ s✝, f i).vars ⊆ s✝.biUnion fun i ↦ (f i).vars
⊢ (f a✝ * ∏ i ∈ s✝, f i).vars ⊆ (f a✝).vars ∪ s✝.biUnion fun i ↦ (f i).vars

Tactic:
apply Finset.Subset.trans (vars_mul _ _)

Goal state after:
case insert
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
inst✝ : DecidableEq σ
f : ι → MvPolynomial σ R
a✝ : ι
s✝ : Finset ι
hs : a✝ ∉ s✝
hsub : (∏ i ∈ s✝, f i).vars ⊆ s✝.biUnion fun i ↦ (f i).vars
⊢ (f a✝).vars ∪ (∏ i ∈ s✝, f i).vars ⊆ (f a✝).vars ∪ s✝.biUnion fun i ↦ (f i).vars
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case succ
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i j : σ
h : i ≠ j
k : ℕ
hk : degreeOf i (X j ^ k) = 0
⊢ degreeOf i (X j ^ (k + 1)) = 0

Tactic:
pow_add,

Goal state after:
case succ
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i j : σ
h : i ≠ j
k : ℕ
hk : degreeOf i (X j ^ k) = 0
⊢ degreeOf i (X j ^ k * X j ^ 1) = 0
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case succ
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
h : p ≠ 0
k : ℕ
hk : degreeOf i (p * X i ^ k) = degreeOf i p + k
this : p * X i ^ k ≠ 0
⊢ degreeOf i (p * X i ^ (k + 1)) = degreeOf i p + (k + 1)

Tactic:
pow_add,

Goal state after:
case succ
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
h : p ≠ 0
k : ℕ
hk : degreeOf i (p * X i ^ k) = degreeOf i p + k
this : p * X i ^ k ≠ 0
⊢ degreeOf i (p * (X i ^ k * X i ^ 1)) = degreeOf i p + (k + 1)
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case succ
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i j : σ
h : i ≠ j
k : ℕ
hk : degreeOf i (p * X j ^ k) = degreeOf i p
⊢ degreeOf i (p * X j ^ (k + 1)) = degreeOf i p

Tactic:
pow_add,

Goal state after:
case succ
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i j : σ
h : i ≠ j
k : ℕ
hk : degreeOf i (p * X j ^ k) = degreeOf i p
⊢ degreeOf i (p * (X j ^ k * X j ^ 1)) = degreeOf i p
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : Algebra R S₁
s : Set S₁
⊢ Algebra.adjoin R s = (aeval Subtype.val).range

Tactic:
by
  rw [← Algebra.adjoin_range_eq_range_aeval, Subtype.range_coe]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Fin

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Zero M
inst✝ : AddCommMonoid N
n : ℕ
σ : Fin n →₀ M
i : M
f : Fin (n + 1) → M → N
h : ∀ (x : Fin (n + 1)), f x 0 = 0
⊢ f 0 ((cons i σ) 0) + ∑ i_1, f i_1.succ ((cons i σ) i_1.succ) = f 0 i + ∑ i, Fin.tail f i (σ i)

Tactic:
cons_zero,

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : Zero M
inst✝ : AddCommMonoid N
n : ℕ
σ : Fin n →₀ M
i : M
f : Fin (n + 1) → M → N
h : ∀ (x : Fin (n + 1)), f x 0 = 0
⊢ f 0 i + ∑ i_1, f i_1.succ ((cons i σ) i_1.succ) = f 0 i + ∑ i, Fin.tail f i (σ i)
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
p : MvPolynomial σ R
inst✝ : LinearOrder σ
⊢ leadingCoeff (⇑toLex) p = coeff (ofLex (supDegree (⇑toLex) p)) p

Tactic:
rw [leadingCoeff]
  apply congr_arg p.coeff
  apply toLex.injective
  rw [Function.rightInverse_invFun toLex.surjective, toLex_ofLex]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
i : ℕ
r : R
hr : ¬r = 0
⊢ ((monomial i) r).eraseLead = 0

Tactic:
· rw [eraseLead, natDegree_monomial, if_neg hr, erase_monomial]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
⊢ (X ^ n).eraseLead = 0

Tactic:
by
  rw [X_pow_eq_monomial, eraseLead_monomial]

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 + n) = i r * x ^ n

Tactic:
pow_add,

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 ^ (N - n) * (x ^ (N - n) * x ^ n) = i r * x ^ n
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
f g : R[X]
⊢ (f * g).reverse = f.reverse * g.reverse

Tactic:
by
  by_cases f0 : f = 0
  · simp only [f0, zero_mul, reverse_zero]
  by_cases g0 : g = 0
  · rw [g0, mul_zero, reverse_zero, mul_zero]
  simp [reverse_mul, *]

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun m i ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
⊢ (x + y) ^ n * y ^ (n + 1 - 1 - n) = (x + y) ^ n

Tactic:
rw [← tsub_add_eq_tsub_tsub, Nat.add_comm, tsub_self, pow_zero, mul_one]

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

Goal state before:
pp: case left
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
⊢ IsLeftRegular p

Tactic:
intro q

Goal state after:
case left
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
q : R[X]
⊢ ∀ ⦃a₂ : R[X]⦄, (fun x ↦ p * x) q = (fun x ↦ p * x) a₂ → q = a₂
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case right
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
⊢ IsRightRegular p

Tactic:
intro q

Goal state after:
case right
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
q : R[X]
⊢ ∀ ⦃a₂ : R[X]⦄, (fun x ↦ x * p) q = (fun x ↦ x * p) a₂ → q = a₂
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
t : Multiset R[X]
⊢ t.prod.leadingCoeff = (Multiset.map (fun f ↦ f.leadingCoeff) t).prod

Tactic:
rw [← leadingCoeffHom_apply, MonoidHom.map_multiset_prod]
  simp only [leadingCoeffHom_apply]

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x y : R
h : Commute x y
m n : ℕ
hmn : m ≤ n
this : ∑ k ∈ range m, x ^ k * y ^ (n - 1 - k) = ∑ k ∈ range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))
⊢ (x - y) * (∑ k ∈ range n, x ^ k * y ^ (n - 1 - k) - ∑ k ∈ range m, x ^ k * y ^ (n - 1 - k)) =
    x ^ n - x ^ m * y ^ (n - m)

Tactic:
rw [this]

Goal state after:
R : Type u_1
inst✝ : Ring R
x y : R
h : Commute x y
m n : ℕ
hmn : m ≤ n
this : ∑ k ∈ range m, x ^ k * y ^ (n - 1 - k) = ∑ k ∈ range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))
⊢ (x - y) * (∑ k ∈ range n, x ^ k * y ^ (n - 1 - k) - ∑ k ∈ range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))) =
    x ^ n - x ^ m * y ^ (n - m)
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x y : R
h : Commute x y
n i : ℕ
hi : i ∈ range n
this : n - 1 - i + 1 = n - i
⊢ x ^ i * y ^ (n - i) = x ^ i * y ^ (n - 1 - i + 1)

Tactic:
rw [this]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : p ∈ Submodule.span R s
h : ∀ p' ∈ s, p'.degree < p.degree
hp_zero : ¬p = 0
⊢ p ∈ degreeLT R p.natDegree

Tactic:
refine (Submodule.span_le.mpr fun p' p'_mem => ?_) hp

Goal state after:
R : Type u
inst✝ : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : p ∈ Submodule.span R s
h : ∀ p' ∈ s, p'.degree < p.degree
hp_zero : ¬p = 0
p' : R[X]
p'_mem : p' ∈ s
⊢ p' ∈ ↑(degreeLT R p.natDegree)
Module: Mathlib.RingTheory.Adjoin.Tower

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁶ : CommSemiring C
inst✝⁵ : CommSemiring D
inst✝⁴ : CommSemiring E
inst✝³ : Algebra C D
inst✝² : Algebra C E
inst✝¹ : Algebra D E
inst✝ : IsScalarTower C D E
S : Set E
this : Set.range ⇑(algebraMap D E) = Set.range ⇑(algebraMap (↥(Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤)) E)
x : E
⊢ x ∈ Subsemiring.closure (Set.range ⇑(algebraMap D E) ∪ S) ↔
    x ∈ Subsemiring.closure (Set.range ⇑(algebraMap (↥(Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤)) E) ∪ S)

Tactic:
rw [this]

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
n : ι → ℕ
hn : ∀ (i : ι), s i ^ n i • x ∈ S'
s' : ι → ↥S' := fun x ↦ ⟨s x, ⋯⟩
l' : ι → ↥S' := fun x ↦ ⟨l x, ⋯⟩
e' : ∑ i ∈ ι', l' i * s' i = 1
this : Ideal.span (s' '' ↑ι') = ⊤
N : ℕ := ι'.sup n
hN : Ideal.span ((fun x ↦ x ^ N) '' s' '' ↑ι') = ⊤
i : ι
hi : i ∈ ↑ι'
⊢ s' i ^ (N - n i + n i) • x ∈ toSubmodule (ofId (↥S') S).range

Tactic:
pow_add,

Goal state after:
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
n : ι → ℕ
hn : ∀ (i : ι), s i ^ n i • x ∈ S'
s' : ι → ↥S' := fun x ↦ ⟨s x, ⋯⟩
l' : ι → ↥S' := fun x ↦ ⟨l x, ⋯⟩
e' : ∑ i ∈ ι', l' i * s' i = 1
this : Ideal.span (s' '' ↑ι') = ⊤
N : ℕ := ι'.sup n
hN : Ideal.span ((fun x ↦ x ^ N) '' s' '' ↑ι') = ⊤
i : ι
hi : i ∈ ↑ι'
⊢ (s' i ^ (N - n i) * s' i ^ n i) • x ∈ toSubmodule (ofId (↥S') S).range
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
ι : Type u_2
s : Finset ι
f : ι → Ideal R[X]
⊢ ∏ i ∈ s, (f i).leadingCoeff ≤ (s.prod f).leadingCoeff

Tactic:
classical
  refine Finset.induction_on s (by simp) ?_
  intro i s hi hs
  simpa [hi] using (mul_mono_right hs).trans (leadingCoeff_mul_le (f i) (s.prod f))

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

Goal state before:
pp: case mpr.ne_top'
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
⊢ ¬map C P = ⊤

Tactic:
eq_top_iff_one,

Goal state after:
case mpr.ne_top'
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
⊢ 1 ∉ map C P
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
r : R
hr : (Ideal.span {r}).IsPrime
this : r ≠ 0
⊢ (Ideal.span (⇑C '' {r})).IsPrime

Tactic:
← Ideal.map_span

Goal state after:
R : Type u
inst✝ : CommRing R
r : R
hr : (Ideal.span {r}).IsPrime
this : r ≠ 0
⊢ (Ideal.map C (Ideal.span {r})).IsPrime
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
σ : Type v
r : R
inst✝¹ : CommRing R
inst✝ : Finite σ
⊢ Prime (C r) ↔ Prime r

Tactic:
by
  have := Fintype.ofFinite σ
  rw [← MulEquiv.prime_iff (renameEquiv R (Fintype.equivFin σ))]
  convert_to Prime (C r) ↔ _
  · congr!
    simp only [renameEquiv_apply, algHom_C, algebraMap_eq]
  · induction Fintype.card σ with
    | zero => simpa using MulEquiv.prime_iff (isEmptyAlgEquiv R (Fin 0)).symm (p := r)
    | succ d hd =>
      convert! MulEquiv.prime_iff (finSuccEquiv R d).symm (p := Polynomial.C (C r))
      · simp [← finSuccEquiv_comp_C_eq_C]
      · simp [← hd, Polynomial.prime_C_iff]

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
⊢ I ≤ Submodule.span R[X] ↑s

Tactic:
rw [this]

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
⊢ I ≤ Ideal.span ↑s
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case mp
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
ι : Type uS
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] S
hsur : Surjective ⇑f
⊢ ∃ n f, Surjective ⇑f

Tactic:
have equiv := MvPolynomial.renameEquiv R (Fintype.equivFin ι)

Goal state after:
case mp
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
ι : Type uS
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] S
hsur : Surjective ⇑f
equiv : MvPolynomial ι R ≃ₐ[R] MvPolynomial (Fin (Fintype.card ι)) R
⊢ ∃ n f, Surjective ⇑f
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set R[M]
hS : adjoin R S = ⊤
this : of' R M '' ⋃ f ∈ S, ↑f.coeff.support = ⋃ f ∈ S, of' R M '' ↑f.coeff.support
⊢ adjoin R (of' R M '' ⋃ f ∈ S, ↑f.coeff.support) = ⊤

Tactic:
rw [this]

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set R[M]
hS : adjoin R S = ⊤
this : of' R M '' ⋃ f ∈ S, ↑f.coeff.support = ⋃ f ∈ S, of' R M '' ↑f.coeff.support
⊢ adjoin R (⋃ f ∈ S, of' R M '' ↑f.coeff.support) = ⊤
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case h
R : Type u_1
M : Type u_2
inst✝¹ : CommRing R
inst✝ : AddMonoid M
S : Finset R[M]
hS : adjoin R ↑S = ⊤
this✝ : DecidableEq M := Classical.decEq M
this : ↑(S.biUnion fun f ↦ f.coeff.support) = ⋃ f ∈ S, ↑f.coeff.support
⊢ adjoin R (of' R M '' ↑(S.biUnion fun f ↦ f.coeff.support)) = ⊤

Tactic:
rw [this]

Goal state after:
case h
R : Type u_1
M : Type u_2
inst✝¹ : CommRing R
inst✝ : AddMonoid M
S : Finset R[M]
hS : adjoin R ↑S = ⊤
this✝ : DecidableEq M := Classical.decEq M
this : ↑(S.biUnion fun f ↦ f.coeff.support) = ⋃ f ∈ S, ↑f.coeff.support
⊢ adjoin R (of' R M '' ⋃ f ∈ S, ↑f.coeff.support) = ⊤