mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
n : ℕ
⊢ ∀ (x : FreeAlgebra R X), (n + 1) • x = n • x + x

Tactic:
rintro ⟨a⟩

Goal state after:
case mk
R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
n : ℕ
x✝ : FreeAlgebra R X
a : Pre R X
⊢ (n + 1) • Quot.mk (Rel R X) a = n • Quot.mk (Rel R X) a + Quot.mk (Rel R X) a
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
x : R
n : ℕ
⊢ eval x (C ↑n * p) = ↑n * eval x p

Tactic:
eval_C_mul

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
x : R
n : ℕ
⊢ ↑n * eval x p = ↑n * eval x p
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
c : Set (E →ₛₗ.[σ] F)
hnonempty : c.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
x : E
⊢ x ∈ (LinearPMap.sSup c hc).domain ↔ ∃ f ∈ c, x ∈ f.domain

Tactic:
by
  rw [domain_sSup, Submodule.mem_sSup_of_directed (hnonempty.image _)
    (DirectedOn.mono_comp LinearPMap.domain_mono.monotone hc)]
  simp

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

Goal state before:
pp: case prime
R : Type u_1
inst✝ : AddMonoidWithOne R
p q : ℕ
hq : ExpChar R q
hp' : Nat.Prime p
hchar✝ : CharP R p
⊢ p = q

Tactic:
· rcases hq with hq | hq'
    exacts [False.elim (Nat.not_prime_zero (CharP.eq R ‹_› (CharP.ofCharZero R) ▸ hp')),
      CharP.eq R ‹_› ‹_›]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
k m : ℕ
hkm : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ x + 0 ≠ 0 ∧ 0 + y ≠ 0

Tactic:
zero_add,

Goal state after:
R : Type u
inst✝ : Semiring R
k m : ℕ
hkm : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ x + 0 ≠ 0 ∧ y ≠ 0
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ x ≠ 0 ∧ 0 + y ≠ 0 ∧ 0 + z ≠ 0

Tactic:
zero_add,

Goal state after:
R : Type u
inst✝ : Semiring R
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ x ≠ 0 ∧ y ≠ 0 ∧ z ≠ 0
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (p * X).coeff (n + 1) = p.coeff n

Tactic:
coeff_mul_X

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ p.coeff n = p.coeff n
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case h
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : SemilatticeSup B
inst✝⁵ : OrderBot B
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : AddCommMonoid B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
a✝ : List R[A]
⊢ a✝.prod.coeff.support.sup degb ≤ (List.map (fun f ↦ f.coeff.support.sup degb) a✝).sum

Tactic:
exact sup_support_list_prod_le degb0 degbm _

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : p ≠ 0
⊢ p.degree.succ = p.natDegree + 1

Tactic:
degree_eq_natDegree h

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
h : p ≠ 0
⊢ (↑p.natDegree).succ = p.natDegree + 1
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (erase n p).support ⊆ p.support

Tactic:
simpa using Finset.erase_subset ..

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

Goal state before:
pp: case neg
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
inst✝ : Nonempty A
hD : Function.Injective D
a : A
r : R
hr : ¬r = 0
⊢ (single a r).coeff (Function.invFun D (D a)) = r

Tactic:
rw [Function.leftInverse_invFun hD]

Goal state after:
case neg
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
inst✝ : Nonempty A
hD : Function.Injective D
a : A
r : R
hr : ¬r = 0
⊢ (single a r).coeff a = r
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: case coe
a✝ : ℕ
h : 0 + 1 ≤ a✝
⊢ 1 ≤ ↑a✝

Tactic:
zero_add,

Goal state after:
case coe
a✝ : ℕ
h : 1 ≤ a✝
⊢ 1 ≤ ↑a✝
Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree

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

Tactic:
degree_C_mul_X ha

Goal state after:
R : Type u
a b : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ 1 = 1
Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree

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

Tactic:
leadingCoeff_C_mul_X

Goal state after:
R : Type u
a b : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ a = a
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:
degree_X_add_C

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
a : R
⊢ 1 = 1
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]
hp : p.Monic
hfp : map f p = 0
x : R
⊢ f x * (map f p).coeff p.natDegree = 0

Tactic:
by simp only [hfp, mul_zero, coeff_zero]

Goal state after:
Module: Mathlib.Algebra.Order.Pi

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : One γ
inst✝ : LE γ
f : α → β
g : α → γ
e : β → γ
hg : 1 ≤ g
he : 1 ≤ e
_b : β
⊢ 1 _b ≤ extend f g e _b

Tactic:
by classical exact one_le_dite (fun _ ↦ hg _) (fun _ ↦ he _)

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
f g : ι →₀ α
h : f ≤ g
a : ι
ha : f a ≠ 0
⊢ g a ≠ 0

Tactic:
← pos_iff_ne_zero

Goal state after:
ι : Type u_1
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
f g : ι →₀ α
h : f ≤ g
a : ι
ha : 0 < f a
⊢ 0 < g a
Module: Mathlib.Data.DFinsupp.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : (i : ι) → AddCommMonoid (α i)
inst✝³ : (i : ι) → PartialOrder (α i)
inst✝² : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
f g : Π₀ (i : ι), α i
h : f ≤ g
a : ι
ha : f a ≠ 0
⊢ g a ≠ 0

Tactic:
← pos_iff_ne_zero

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : (i : ι) → AddCommMonoid (α i)
inst✝³ : (i : ι) → PartialOrder (α i)
inst✝² : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
f g : Π₀ (i : ι), α i
h : f ≤ g
a : ι
ha : 0 < f a
⊢ 0 < g a
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ ∀ (q : MvPolynomial σ R),
    (∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (p * (monomial s) a) = eval₂ f g p * f a * s.prod fun n e ↦ g n ^ e) →
      (∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (q * (monomial s) a) = eval₂ f g q * f a * s.prod fun n e ↦ g n ^ e) →
        ∀ {s : σ →₀ ℕ} {a : R},
          eval₂ f g ((p + q) * (monomial s) a) = eval₂ f g (p + q) * f a * s.prod fun n e ↦ g n ^ e

Tactic:
q

Goal state after:
case add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
p q : MvPolynomial σ R
⊢ (∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (p * (monomial s) a) = eval₂ f g p * f a * s.prod fun n e ↦ g n ^ e) →
    (∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (q * (monomial s) a) = eval₂ f g q * f a * s.prod fun n e ↦ g n ^ e) →
      ∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g ((p + q) * (monomial s) a) = eval₂ f g (p + q) * f a * s.prod fun n e ↦ g n ^ e
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : ℕ
⊢ C ↑n = ↑n

Tactic:
induction n <;> simp [*]

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

Goal state before:
pp: case add
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
τ : Type u_3
x : τ → S
inst✝ : CommSemiring S
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
p✝ p : MvPolynomial σ R
⊢ ∀ (q : MvPolynomial σ R),
    (eval x) (eval₂ f g p) = eval₂ ((eval x).comp f) (fun s ↦ (eval x) (g s)) p →
      (eval x) (eval₂ f g q) = eval₂ ((eval x).comp f) (fun s ↦ (eval x) (g s)) q →
        (eval x) (eval₂ f g (p + q)) = eval₂ ((eval x).comp f) (fun s ↦ (eval x) (g s)) (p + q)

Tactic:
q

Goal state after:
case add
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
τ : Type u_3
x : τ → S
inst✝ : CommSemiring S
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
p✝ p q : MvPolynomial σ R
⊢ (eval x) (eval₂ f g p) = eval₂ ((eval x).comp f) (fun s ↦ (eval x) (g s)) p →
    (eval x) (eval₂ f g q) = eval₂ ((eval x).comp f) (fun s ↦ (eval x) (g s)) q →
      (eval x) (eval₂ f g (p + q)) = eval₂ ((eval x).comp f) (fun s ↦ (eval x) (g s)) (p + q)
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m : σ →₀ ℕ
a : R
ha : IsRegular a
p : MvPolynomial σ R
⊢ ∀ ⦃a₂ : MvPolynomial σ R⦄,
    (fun x ↦ (MvPolynomial.monomial m) a * x) p = (fun x ↦ (MvPolynomial.monomial m) a * x) a₂ → p = a₂

Tactic:
q

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m : σ →₀ ℕ
a : R
ha : IsRegular a
p q : MvPolynomial σ R
⊢ (fun x ↦ (MvPolynomial.monomial m) a * x) p = (fun x ↦ (MvPolynomial.monomial m) a * x) q → p = q
Module: Mathlib.Data.DFinsupp.Lex

Goal state before:
pp: case h₂
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
P : Lex (Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i) → Sort u_3
h_lt : {f g : Π₀ (i : ι), α i} → toLex f < toLex g → P (toLex f) (toLex g)
h_eq : {f g : Π₀ (i : ι), α i} → toLex f = toLex g → P (toLex f) (toLex g)
h_gt : {f g : Π₀ (i : ι), α i} → toLex g < toLex f → P (toLex f) (toLex g)
f g : Π₀ (i : ι), α i
wit : ι
h : (f.neLocus g).min = ↑wit
hwit : g wit < f wit
⊢ P (toLex f) (toLex g)

Tactic:
exact h_gt ⟨wit, fun j hj ↦
        notMem_neLocus.mp (Finset.notMem_of_lt_min hj <| by rwa [neLocus_comm]), hwit⟩

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

Goal state before:
pp: case add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
S₂ : Type u_2
inst✝ : CommSemiring S₂
k : S₁ →+* S₂
f : R →+* S₁
g : σ → S₁
p✝ p : MvPolynomial σ R
⊢ ∀ (q : MvPolynomial σ R),
    k (eval₂ f g p) = eval₂ k (⇑k ∘ g) ((map f) p) →
      k (eval₂ f g q) = eval₂ k (⇑k ∘ g) ((map f) q) → k (eval₂ f g (p + q)) = eval₂ k (⇑k ∘ g) ((map f) (p + q))

Tactic:
q

Goal state after:
case add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
S₂ : Type u_2
inst✝ : CommSemiring S₂
k : S₁ →+* S₂
f : R →+* S₁
g : σ → S₁
p✝ p q : MvPolynomial σ R
⊢ k (eval₂ f g p) = eval₂ k (⇑k ∘ g) ((map f) p) →
    k (eval₂ f g q) = eval₂ k (⇑k ∘ g) ((map f) q) → k (eval₂ f g (p + q)) = eval₂ k (⇑k ∘ g) ((map f) (p + q))
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
g : τ → α
p : MvPolynomial σ R
⊢ (rename g) ((rename f) p) = (rename (g ∘ f)) p

Tactic:
simp [MvPolynomial, rename, mapDomain.addMonoidHom_comp]

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

Goal state before:
pp: case mul_X
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
S₂ : Type u_2
inst✝ : CommSemiring S₂
k : S₁ →+* S₂
f : R →+* S₁
g : σ → S₁
p✝ p : MvPolynomial σ R
s : σ
hp : k (eval₂ f g p) = eval₂ k (⇑k ∘ g) ((map f) p)
⊢ eval₂ k (⇑k ∘ g) ((map f) p) * k (eval₂ f g (X s)) = eval₂ k (⇑k ∘ g) ((map f) p) * eval₂ k (⇑k ∘ g) (X s)

Tactic:
eval₂_X,

Goal state after:
case mul_X
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
S₂ : Type u_2
inst✝ : CommSemiring S₂
k : S₁ →+* S₂
f : R →+* S₁
g : σ → S₁
p✝ p : MvPolynomial σ R
s : σ
hp : k (eval₂ f g p) = eval₂ k (⇑k ∘ g) ((map f) p)
⊢ eval₂ k (⇑k ∘ g) ((map f) p) * k (g s) = eval₂ k (⇑k ∘ g) ((map f) p) * eval₂ k (⇑k ∘ g) (X s)
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case mul_X
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
S₂ : Type u_2
inst✝ : CommSemiring S₂
k : S₁ →+* S₂
f : R →+* S₁
g : σ → S₁
p✝ p : MvPolynomial σ R
s : σ
hp : k (eval₂ f g p) = eval₂ k (⇑k ∘ g) ((map f) p)
⊢ eval₂ k (⇑k ∘ g) ((map f) p) * k (g s) = eval₂ k (⇑k ∘ g) ((map f) p) * eval₂ k (⇑k ∘ g) (X s)

Tactic:
eval₂_X,

Goal state after:
case mul_X
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
S₂ : Type u_2
inst✝ : CommSemiring S₂
k : S₁ →+* S₂
f : R →+* S₁
g : σ → S₁
p✝ p : MvPolynomial σ R
s : σ
hp : k (eval₂ f g p) = eval₂ k (⇑k ∘ g) ((map f) p)
⊢ eval₂ k (⇑k ∘ g) ((map f) p) * k (g s) = eval₂ k (⇑k ∘ g) ((map f) p) * (⇑k ∘ g) s
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case add
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : S₂ → MvPolynomial S₃ R
p✝ p : MvPolynomial S₂ R
⊢ ∀ (q : MvPolynomial S₂ R),
    (map f) (eval₂ C g p) = eval₂ C (⇑(map f) ∘ g) ((map f) p) →
      (map f) (eval₂ C g q) = eval₂ C (⇑(map f) ∘ g) ((map f) q) →
        (map f) (eval₂ C g (p + q)) = eval₂ C (⇑(map f) ∘ g) ((map f) (p + q))

Tactic:
q

Goal state after:
case add
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : S₂ → MvPolynomial S₃ R
p✝ p q : MvPolynomial S₂ R
⊢ (map f) (eval₂ C g p) = eval₂ C (⇑(map f) ∘ g) ((map f) p) →
    (map f) (eval₂ C g q) = eval₂ C (⇑(map f) ∘ g) ((map f) q) →
      (map f) (eval₂ C g (p + q)) = eval₂ C (⇑(map f) ∘ g) ((map f) (p + q))
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case mul_X
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : S₂ → MvPolynomial S₃ R
p✝ p : MvPolynomial S₂ R
s : S₂
hp : (map f) (eval₂ C g p) = eval₂ C (⇑(map f) ∘ g) ((map f) p)
⊢ eval₂ C (⇑(map f) ∘ g) ((map f) p) * (map f) (eval₂ C g (X s)) =
    eval₂ C (⇑(map f) ∘ g) ((map f) p) * eval₂ C (⇑(map f) ∘ g) (X s)

Tactic:
eval₂_X,

Goal state after:
case mul_X
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : S₂ → MvPolynomial S₃ R
p✝ p : MvPolynomial S₂ R
s : S₂
hp : (map f) (eval₂ C g p) = eval₂ C (⇑(map f) ∘ g) ((map f) p)
⊢ eval₂ C (⇑(map f) ∘ g) ((map f) p) * (map f) (g s) = eval₂ C (⇑(map f) ∘ g) ((map f) p) * eval₂ C (⇑(map f) ∘ g) (X s)
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case mul_X
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : S₂ → MvPolynomial S₃ R
p✝ p : MvPolynomial S₂ R
s : S₂
hp : (map f) (eval₂ C g p) = eval₂ C (⇑(map f) ∘ g) ((map f) p)
⊢ eval₂ C (⇑(map f) ∘ g) ((map f) p) * (map f) (g s) = eval₂ C (⇑(map f) ∘ g) ((map f) p) * eval₂ C (⇑(map f) ∘ g) (X s)

Tactic:
eval₂_X,

Goal state after:
case mul_X
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : S₂ → MvPolynomial S₃ R
p✝ p : MvPolynomial S₂ R
s : S₂
hp : (map f) (eval₂ C g p) = eval₂ C (⇑(map f) ∘ g) ((map f) p)
⊢ eval₂ C (⇑(map f) ∘ g) ((map f) p) * (map f) (g s) = eval₂ C (⇑(map f) ∘ g) ((map f) p) * (⇑(map f) ∘ g) s
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
p : MvPolynomial σ R
⊢ ∀ (q : MvPolynomial σ R),
    (∀ (m : σ →₀ ℕ), coeff m ((map f) p) = f (coeff m p)) →
      (∀ (m : σ →₀ ℕ), coeff m ((map f) q) = f (coeff m q)) →
        ∀ (m : σ →₀ ℕ), coeff m ((map f) (p + q)) = f (coeff m (p + q))

Tactic:
q

Goal state after:
case add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
p q : MvPolynomial σ R
⊢ (∀ (m : σ →₀ ℕ), coeff m ((map f) p) = f (coeff m p)) →
    (∀ (m : σ →₀ ℕ), coeff m ((map f) q) = f (coeff m q)) →
      ∀ (m : σ →₀ ℕ), coeff m ((map f) (p + q)) = f (coeff m (p + q))
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₁
hf : Injective ⇑f
p : MvPolynomial σ R
⊢ ∀ ⦃a₂ : MvPolynomial σ R⦄, (map f) p = (map f) a₂ → p = a₂

Tactic:
q

Goal state after:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
hf : Injective ⇑f
p q : MvPolynomial σ R
⊢ (map f) p = (map f) q → p = q
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case inl
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
hd : 0 ∈ p.support
⊢ toMultiset 0 ≤ (p + q).degrees

Tactic:
rw [toMultiset_zero]; apply Multiset.zero_le

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

Goal state before:
pp: case add
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
τ : Type u_6
f : σ → τ
φ p : MvPolynomial σ R
⊢ ∀ (q : MvPolynomial σ R),
    constantCoeff ((rename f) p) = constantCoeff p →
      constantCoeff ((rename f) q) = constantCoeff q → constantCoeff ((rename f) (p + q)) = constantCoeff (p + q)

Tactic:
q

Goal state after:
case add
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
τ : Type u_6
f : σ → τ
φ p q : MvPolynomial σ R
⊢ constantCoeff ((rename f) p) = constantCoeff p →
    constantCoeff ((rename f) q) = constantCoeff q → constantCoeff ((rename f) (p + q)) = constantCoeff (p + q)
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: case insert
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
hsum : (∑ i ∈ s✝, φ i).vars ⊆ s✝.biUnion fun i ↦ (φ i).vars
⊢ (∑ i ∈ insert a✝ s✝, φ i).vars ⊆ (insert a✝ s✝).biUnion fun i ↦ (φ i).vars

Tactic:
rw [Finset.biUnion_insert, Finset.sum_insert has]
    refine Finset.Subset.trans
      (vars_add_subset _ _) (Finset.union_subset_union (Finset.Subset.refl _) ?_)
    assumption

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

Goal state before:
pp: S : Type v
inst✝ : CommRing S
R : Type u
c : ℤ →+* S
f : MvPolynomial R ℤ →+* S
x p : MvPolynomial R ℤ
n : R
hp : eval₂ c (⇑f ∘ X) p = f p
⊢ eval₂ c (⇑f ∘ X) p * eval₂ c (⇑f ∘ X) (X n) = f (p * X n)

Tactic:
eval₂_X,

Goal state after:
S : Type v
inst✝ : CommRing S
R : Type u
c : ℤ →+* S
f : MvPolynomial R ℤ →+* S
x p : MvPolynomial R ℤ
n : R
hp : eval₂ c (⇑f ∘ X) p = f p
⊢ eval₂ c (⇑f ∘ X) p * (⇑f ∘ X) n = f (p * X n)
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
s : σ
n : ℕ
⊢ (X s ^ n).totalDegree = n

Tactic:
by simp [X_pow_eq_monomial, one_ne_zero]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
h0 : ¬p.comp q = 0
n : ℕ
hn : n ∈ p.support
⊢ 0 + n • ↑q.natDegree = ↑(n * q.natDegree)

Tactic:
zero_add,

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
h0 : ¬p.comp q = 0
n : ℕ
hn : n ∈ p.support
⊢ n • ↑q.natDegree = ↑(n * q.natDegree)
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case succ
R : Type u
m✝ n : ℕ
inst✝ : Semiring R
p : R[X]
pn : p.natDegree ≤ n
m : ℕ
hm : (p ^ m).coeff (m * n) = p.coeff n ^ m
⊢ (p ^ (m + 1)).coeff ((m + 1) * n) = p.coeff n ^ (m + 1)

Tactic:
rw [pow_succ, pow_succ, ← hm, Nat.succ_mul, coeff_mul_add_eq_of_natDegree_le _ pn]
    refine natDegree_pow_le.trans (le_trans ?_ (le_refl _))
    gcongr

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
⊢ (X ^ n).trailingDegree = ↑n

Tactic:
by
  rw [X_pow_eq_monomial, trailingDegree_monomial one_ne_zero]

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

Goal state before:
pp: case hX
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ✝ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ✝ →₀ ℕ
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : Unique σ
f : R[X] →+* MvPolynomial σ R := eval₂RingHom C (X default)
g : MvPolynomial σ R →+* R[X] := eval₂Hom Polynomial.C fun x ↦ Polynomial.X
i : σ
⊢ Polynomial.eval₂ C (X default) (eval₂ Polynomial.C (fun x ↦ Polynomial.X) (X i)) = X i

Tactic:
eval₂_X,

Goal state after:
case hX
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ✝ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ✝ →₀ ℕ
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : Unique σ
f : R[X] →+* MvPolynomial σ R := eval₂RingHom C (X default)
g : MvPolynomial σ R →+* R[X] := eval₂Hom Polynomial.C fun x ↦ Polynomial.X
i : σ
⊢ Polynomial.eval₂ C (X default) Polynomial.X = X i
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case neg
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
H : ∀ x ∈ s, f x = 0
⊢ (s.sup fun i ↦ (f i).natDegree) = 0

Tactic:
show 0 = ⊥ from rfl,

Goal state after:
case neg
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
H : ∀ x ∈ s, f x = 0
⊢ (s.sup fun i ↦ (f i).natDegree) = ⊥
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
hp : p ≠ 0
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), f x = 0 → x = 0
hlt : p.natDegree ≤ 0
A : p = C (p.coeff 0)
⊢ False

Tactic:
A,

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
hp : p ≠ 0
f : R →+* S
z : S
hz : eval₂ f z (C (p.coeff 0)) = 0
inj : ∀ (x : R), f x = 0 → x = 0
hlt : p.natDegree ≤ 0
A : p = C (p.coeff 0)
⊢ False
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case inl
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : C (p.coeff 0) = 0
key✝ : p.natDegree = 0 ∨ q.natDegree = 0
key : p = C (p.coeff 0)
⊢ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = C (q.coeff 0)

Tactic:
exact Or.inl (key.trans h)

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

Goal state before:
pp: case inl
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
q : R[X]
hq : 0 < q.degree
⊢ (comp 0 q).degree = degree 0 * q.degree

pp: case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hq : 0 < q.degree
hp : p ≠ 0
⊢ (p.comp q).degree = p.degree * q.degree

Tactic:
· rw [zero_comp, degree_zero, WithBot.bot_mul']
    simp [hq.ne']

Goal state after:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hq : 0 < q.degree
hp : p ≠ 0
⊢ (p.comp q).degree = p.degree * q.degree
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial (Option σ) R
h : f ≠ 0
⊢ (((optionEquivLeft R σ) f).support.sup fun x ↦ x) = degreeOf none f

Tactic:
rw [degreeOf_eq_sup, support_optionEquivLeft, Finset.sup_image, Function.comp_def]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial (Option σ) R
h : f ≠ 0
h' : (((optionEquivLeft R σ) f).support.sup fun x ↦ x) = degreeOf none f
⊢ ((optionEquivLeft R σ) f).degree = ↑(degreeOf none f)

Tactic:
Polynomial.degree,

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial (Option σ) R
h : f ≠ 0
h' : (((optionEquivLeft R σ) f).support.sup fun x ↦ x) = degreeOf none f
⊢ ((optionEquivLeft R σ) f).support.max = ↑(degreeOf none f)
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
⊢ (finSuccEquiv R n) (X 0) = Polynomial.X

Tactic:
by simp [finSuccEquiv_apply]

Goal state after: