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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
n : ℕ
⊢ eval₂ f x (X ^ n) = x ^ n

Tactic:
X_pow_eq_monomial

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
n : ℕ
⊢ eval₂ f x ((monomial n) 1) = x ^ n
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case h'
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_5
inst✝³ : AddCommGroup F
inst✝² : Module S F
G : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : Module T G
f g : E →ₛₗ.[σ] F
h' : f + g = 0
x : E
hf : x ∈ (-f).domain
hg : x ∈ g.domain
⊢ ↑(-f) ⟨x, hf⟩ = ↑g ⟨x, hg⟩

Tactic:
simp only [neg_domain, neg_apply, neg_eq_iff_add_eq_zero]

Goal state after:
case h'
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_5
inst✝³ : AddCommGroup F
inst✝² : Module S F
G : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : Module T G
f g : E →ₛₗ.[σ] F
h' : f + g = 0
x : E
hf : x ∈ (-f).domain
hg : x ∈ g.domain
⊢ ↑f ⟨x, hf⟩ + ↑g ⟨x, hg⟩ = 0
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
x : X
r : R
h : ι R x = (algebraMap R (FreeAlgebra R X)) r
f0 : FreeAlgebra R X →ₐ[R] R := (lift R) 0
f1 : FreeAlgebra R X →ₐ[R] R := (lift R) 1
hf0 : f0 (ι R x) = 0
⊢ False

Tactic:
have hf1 : f1 (ι R x) = 1 := lift_ι_apply _ _

Goal state after:
R : Type u_1
X : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
x : X
r : R
h : ι R x = (algebraMap R (FreeAlgebra R X)) r
f0 : FreeAlgebra R X →ₐ[R] R := (lift R) 0
f1 : FreeAlgebra R X →ₐ[R] R := (lift R) 1
hf0 : f0 (ι R x) = 0
hf1 : f1 (ι R x) = 1
⊢ False
Module: Mathlib.Algebra.MonoidAlgebra.Support

Goal state before:
pp: k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : IsLeftCancelMul G
f : k[G]
r : k
hr : ∀ (y : k), r * y = 0 ↔ y = 0
x : G
⊢ (single x r * f).coeff.support = Finset.map (mulLeftEmbedding x) f.coeff.support

Tactic:
by
  classical ext; simp [support_coeff_single_mul_eq_image f hr (.all x)]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case h
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)
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
cne : c.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (domain '' c)
P : (x : ↥(sSup (domain '' c))) → { p // ↑x ∈ (↑p).domain }
f : ↥(sSup (domain '' c)) → F := fun x ↦ ↑↑↑(P x) ⟨↑x, ⋯⟩
f_eq : ∀ (p : ↑c) (x : ↥(sSup (domain '' c))) (y : ↥(↑p).domain), ↑x = ↑y → f x = ↑↑p y
⊢ { domain := sSup (domain '' c), toFun := { toFun := f, map_add' := ⋯, map_smul' := ⋯ } } ∈ upperBounds c

Tactic:
· intro p hpc
    refine ⟨le_sSup <| Set.mem_image_of_mem domain hpc, fun x y hxy => Eq.symm ?_⟩
    exact f_eq ⟨p, hpc⟩ _ _ hxy.symm

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : CharP R 1
r : R
⊢ ↑1 * r = 0 * r

Tactic:
rw [CharP.cast_eq_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case mp
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 : E →ₗ.[R] F
x : E
h : x ∈ f.domain
⊢ ∃ y, (x, y) ∈ f.graph

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
f : E →ₗ.[R] F
x : E
h : ∃ y, (x, y) ∈ f.graph
⊢ x ∈ f.domain

Tactic:
· use f ⟨x, h⟩
    exact f.mem_graph ⟨x, h⟩

Goal state after:
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
f : E →ₗ.[R] F
x : E
h : ∃ y, (x, y) ∈ f.graph
⊢ x ∈ f.domain
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case refine_2
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 : E × F}, x ∈ g → x.1 = 0 → x.2 = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
y₁ : F
⊢ ∀ (y₂ : F), (a, y₁) ∈ g → (a, y₂) ∈ g → y₁ = y₂

Tactic:
y₂

Goal state after:
case refine_2
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 : E × F}, x ∈ g → x.1 = 0 → x.2 = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
y₁ y₂ : F
⊢ (a, y₁) ∈ g → (a, y₂) ∈ g → y₁ = y₂
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: case single_add
R : Type u_1
S : Type u_2
A : Type u_4
M : Type u_7
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Monoid M
inst✝³ : CommSemiring S
inst✝² : Algebra S A
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S A
f✝ : M →* A
a : M
b : R
f : R[M]
a✝¹ : a ∉ f.coeff.support
a✝ : b ≠ 0
ih : ((lift S A M) f✝) ((mapRingHom M (algebraMap R S)) f) = ((lift R A M) f✝) f
⊢ ((lift S A M) f✝) ((mapRingHom M (algebraMap R S)) (single a b + f)) = ((lift R A M) f✝) (single a b + f)

Tactic:
simp [ih]

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

Goal state before:
pp: case single_add
R : Type u_1
S : Type u_2
A : Type u_4
M : Type u_7
inst✝⁷ : CommSemiring R
inst✝⁶ : AddMonoid M
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring S
inst✝² : Algebra S A
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S A
f✝ : Multiplicative M →* A
a : M
b : R
f : R[M]
a✝¹ : a ∉ f.coeff.support
a✝ : b ≠ 0
ih : ((lift S A M) f✝) ((mapRingHom M (algebraMap R S)) f) = ((lift R A M) f✝) f
⊢ ((lift S A M) f✝) ((mapRingHom M (algebraMap R S)) (single a b + f)) = ((lift R A M) f✝) (single a b + f)

Tactic:
simp [ih]

Goal state after:
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✝¹ : SemilatticeSup B
inst✝ : OrderBot B
D : A → B
s : R[A]
hs : s.coeff.support.Nonempty
⊢ supDegree (WithBot.some ∘ D) s = ↑(supDegree D s)

Tactic:
by
  unfold AddMonoidAlgebra.supDegree
  rw [← Finset.coe_sup' hs, Finset.sup'_eq_sup]

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

Goal state before:
pp: case h₀
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : SemilatticeSup B
inst✝⁴ : OrderBot B
D : A → B
p q : R[A]
inst✝³ : AddZeroClass A
inst✝² : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
a : A
ha : a ∈ p.coeff.support
hne : a ≠ ap
a' : A
ha' : a' ∈ q.coeff.support
he : D a + D a' = D ap + D aq
this : AddLeftMono B
⊢ False

Tactic:
exact (add_lt_add_of_lt_of_le (((Finset.le_sup ha).trans hp).lt_of_ne <| hD.ne_iff.2 hne)
      <| (Finset.le_sup ha').trans hq).ne he

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

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

Tactic:
by
  simpa only [add_assoc] using!
    degree_add_le_of_degree_le (degree_C_mul_X_pow_le 2 a)
      (le_trans degree_linear_le <| WithBot.coe_le_coe.mpr one_le_two)

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
hp2 : ¬p ^ i = 0
⊢ (p ^ i).natDegree < i * p.natDegree

Tactic:
refine lt_of_le_of_ne natDegree_pow_le fun h => hp2 ?_

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
hp2 : ¬p ^ i = 0
h : (p ^ i).natDegree = i * p.natDegree
⊢ p ^ i = 0
Module: Mathlib.RingTheory.Adjoin.Polynomial.Basic

Goal state before:
pp: R : Type u
A : Type z
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
a : ↥R[x]
⊢ ∃ p, (aeval x) p = ↑a

Tactic:
have : (a : A) ∈ R[x] := by simp

Goal state after:
R : Type u
A : Type z
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
a : ↥R[x]
this : ↑a ∈ R[x]
⊢ ∃ p, (aeval x) p = ↑a
Module: Mathlib.Algebra.Notation.Lemmas

Goal state before:
pp: case isTrue
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a : p → α
b : ¬p → α
inst✝ : LE α
ha : ∀ (h : p), 1 ≤ a h
hb : ∀ (h : ¬p), 1 ≤ b h
h✝ : p
⊢ 1 ≤ a h✝

pp: case isFalse
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a : p → α
b : ¬p → α
inst✝ : LE α
ha : ∀ (h : p), 1 ≤ a h
hb : ∀ (h : ¬p), 1 ≤ b h
h✝ : ¬p
⊢ 1 ≤ b h✝

Tactic:
exacts [ha ‹_›, hb ‹_›]

Goal state after:
Module: Mathlib.Algebra.Notation.Lemmas

Goal state before:
pp: case isTrue
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a : p → α
b : ¬p → α
inst✝ : LE α
ha : ∀ (h : p), a h ≤ 1
hb : ∀ (h : ¬p), b h ≤ 1
h✝ : p
⊢ a h✝ ≤ 1

pp: case isFalse
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a : p → α
b : ¬p → α
inst✝ : LE α
ha : ∀ (h : p), a h ≤ 1
hb : ∀ (h : ¬p), b h ≤ 1
h✝ : ¬p
⊢ b h✝ ≤ 1

Tactic:
exacts [ha ‹_›, hb ‹_›]

Goal state after:
Module: Mathlib.Algebra.Notation.Lemmas

Goal state before:
pp: case isTrue
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a : p → α
b : ¬p → α
inst✝ : LT α
ha : ∀ (h : p), 1 < a h
hb : ∀ (h : ¬p), 1 < b h
h✝ : p
⊢ 1 < a h✝

pp: case isFalse
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a : p → α
b : ¬p → α
inst✝ : LT α
ha : ∀ (h : p), 1 < a h
hb : ∀ (h : ¬p), 1 < b h
h✝ : ¬p
⊢ 1 < b h✝

Tactic:
exacts [ha ‹_›, hb ‹_›]

Goal state after:
Module: Mathlib.Algebra.Notation.Lemmas

Goal state before:
pp: case isTrue
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a : p → α
b : ¬p → α
inst✝ : LT α
ha : ∀ (h : p), a h < 1
hb : ∀ (h : ¬p), b h < 1
h✝ : p
⊢ a h✝ < 1

pp: case isFalse
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a : p → α
b : ¬p → α
inst✝ : LT α
ha : ∀ (h : p), a h < 1
hb : ∀ (h : ¬p), b h < 1
h✝ : ¬p
⊢ b h✝ < 1

Tactic:
exacts [ha ‹_›, hb ‹_›]

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : Preorder α
inst✝ : IsOrderedAddMonoid α
f : ι → κ
g : ι →₀ α
hg : 0 ≤ g
⊢ 0 ≤ mapDomain f g

Tactic:
by simpa using mapDomain_mono hg

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : Preorder α
inst✝ : IsOrderedAddMonoid α
f : ι → κ
g : ι →₀ α
hg : g ≤ 0
⊢ mapDomain f g ≤ 0

Tactic:
by simpa using mapDomain_mono hg

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

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
p : R[X]
⊢ (p.comp (-X)).comp (-X) = p

Tactic:
by
  rw [comp_assoc]
  simp only [neg_comp, X_comp, neg_neg, comp_X]

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : CommSemiring T
inst✝¹ : Algebra R S
inst✝ : Algebra T S
φ : R →+* T
h : (algebraMap T S).comp φ = algebraMap R S
p : R[X]
a : S
⊢ (algebraMap ?m.47 ?m.48).comp ?m.54 = RingHom.comp ?m.55 (algebraMap R S)

Tactic:
RingHom.id_comp

Goal state after:
R : Type u
S : Type v
T : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : CommSemiring T
inst✝¹ : Algebra R S
inst✝ : Algebra T S
φ : R →+* T
h : (algebraMap T S).comp φ = algebraMap R S
p : R[X]
a : S
⊢ (algebraMap ?m.47 S).comp ?m.54 = algebraMap R S
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: case pos
S : Type v
inst✝ : CommRing S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ eval z f
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j
hi : i ∈ f.support
⊢ p ∣ f.coeff i * z ^ i

pp: case neg
S : Type v
inst✝ : CommRing S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ eval z f
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j
hi : i ∉ f.support
⊢ p ∣ f.coeff i * z ^ i

Tactic:
· rw [eval, eval₂_eq_sum, sum_def] at dvd_eval
    rw [← Finset.insert_erase hi, Finset.sum_insert (Finset.notMem_erase _ _)] at dvd_eval
    refine (dvd_add_left ?_).mp dvd_eval
    apply Finset.dvd_sum
    intro j hj
    exact dvd_terms j (Finset.ne_of_mem_erase hj)

Goal state after:
case neg
S : Type v
inst✝ : CommRing S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ eval z f
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j
hi : i ∉ f.support
⊢ p ∣ f.coeff i * z ^ i
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₁
p : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    (∀ {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 (p * X n * (monomial s) a) = eval₂ f g (p * X n) * f a * s.prod fun n e ↦ g n ^ e

Tactic:
intro p n ih s a

Goal state after:
case mul_X
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
n : σ
ih : ∀ {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 (p * X n * (monomial s) a) = eval₂ f g (p * X n) * 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
α : 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:
by
  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: case zero
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
motive : MvPolynomial σ R → Prop
C : ∀ (a : R), motive (MvPolynomial.C a)
mul_X : ∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * X n)
s : σ →₀ ℕ
a : R
n : σ
e : ℕ
p : σ →₀ ℕ
_hpn : n ∉ p.support
_he : e ≠ 0
ih : motive ((monomial p) a)
⊢ motive ((monomial p) a * X n ^ 0)

Tactic:
simp [ih]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m : σ →₀ ℕ
h : m ≠ 0
a : R
⊢ (if 0 = m then a else 0) = 0

Tactic:
if_neg h.symm

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m : σ →₀ ℕ
h : m ≠ 0
a : R
⊢ 0 = 0
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: 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
i : σ →₀ ℕ
x : S
⊢ (monomial i) x ∈ coeffsIn σ M ↔ x ∈ M

Tactic:
simp only [mem_coeffsIn, coeff_monomial]
  exact ⟨fun h ↦ by simpa using h i, fun hs j ↦ by split <;> simp [hs]⟩

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

Goal state before:
pp: R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
d : τ →₀ ℕ
hd : coeff d ((rename f) φ) ≠ 0
hi : i ∈ d.support
⊢ ∃ a ∈ φ.degrees, f a = i

Tactic:
obtain ⟨x, rfl, hx⟩ := coeff_rename_ne_zero _ _ _ hd

Goal state after:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) ((rename f) φ) ≠ 0
hi : i ∈ (Finsupp.mapDomain f x).support
⊢ ∃ a ∈ φ.degrees, f a = i
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 ((monomial (Finsupp.single i k)) 1) = k

Tactic:
degreeOf_monomial_eq _ _ one_ne_zero,

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : σ
k : ℕ
⊢ (Finsupp.single i k) i = k
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

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

Tactic:
by
  rw [X_pow_eq_monomial, natTrailingDegree_monomial one_ne_zero]

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

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

Tactic:
eraseLead_monomial

Goal state after:
R : Type u_1
inst✝ : Semiring R
n : ℕ
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
N i : ℕ
f : AddMonoidAlgebra R ℕ
⊢ (embDomain (revAt N) f.coeff) i = (embDomain (revAt N) f.coeff) ((revAt N) ((revAt N) i))

Tactic:
revAt_invol

Goal state after:
R : Type u_1
inst✝ : Semiring R
N i : ℕ
f : AddMonoidAlgebra R ℕ
⊢ (embDomain (revAt N) f.coeff) i = (embDomain (revAt N) f.coeff) i
Module: Mathlib.Algebra.Polynomial.EraseLead

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

Tactic:
eraseLead_monomial

Goal state after:
R : Type u_1
inst✝ : Semiring R
r : R
n : ℕ
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
⊢ f.eraseLead.natDegree = f.natDegree - 1

Tactic:
have := natDegree_pos_of_nextCoeff_ne_zero h

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ f.eraseLead.natDegree = f.natDegree - 1
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ 0 < f.natDegree

pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ 0 < f.natDegree

pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ 0 < 1

Tactic:
all_goals positivity

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
⊢ f.eraseLead.leadingCoeff = f.nextCoeff

Tactic:
have := natDegree_pos_of_nextCoeff_ne_zero h

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ f.eraseLead.leadingCoeff = f.nextCoeff
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ 0 < f.natDegree

pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ 0 < 1

pp: case hnc
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ ¬f.natDegree = 0

Tactic:
all_goals positivity

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

Goal state before:
pp: 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
he : P.eraseLead = 0
⊢ ((X - C x) * P).eraseLead.eraseLead = (X - C x) * P.eraseLead

Tactic:
rw [he, mul_zero]
    by_cases he₂ : ((X - C x) * P).eraseLead = 0
    · simp [he₂]
    suffices #((X - C x) * P).support ≤ 2 by
      rw [← card_support_eq_zero]
      linarith [eraseLead_support_card_lt he₂,
        eraseLead_support_card_lt (mul_ne_zero (X_sub_C_ne_zero x) hp)]
    have h₂ : #(X - C x).support = 2 := by
      simpa [← sub_eq_add_neg] using!
        card_support_binomial one_ne_zero one_ne_zero (neg_ne_zero.mpr hx)
    have hmul := card_support_mul_le (p := X - C x) (q := P)
    rw [h₂] at hmul
    linarith [card_support_le_one_of_eraseLead_eq_zero he]

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
i : ℕ
m : σ →₀ ℕ
⊢ m ∈ (((optionEquivLeft R σ) f).coeff i).support ↔ optionElim i m ∈ f.support

Tactic:
simp [← optionEquivLeft_coeff_some_coeff_none]

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

Goal state before:
pp: case neg.a
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.coeff ((revAt f.natDegree) ((revAt f.natDegree) f.natTrailingDegree)) ≠ 0

Tactic:
revAt_invol

Goal state after:
case neg.a
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.coeff f.natTrailingDegree ≠ 0
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = fu n
f g : R[X]
fg : f.natDegree < g.natDegree
a✝ : g.natDegree ≤ p.natDegree
fk : (φ f).natDegree = fu f.natDegree
gk : (φ g).natDegree = fu g.natDegree
FG : f.natDegree < k
⊢ (φ f + φ g).natDegree = fu g.natDegree

Tactic:
cases k

Goal state after:
case neg.zero
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
fu : ℕ → ℕ
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = fu n
f g : R[X]
fg : f.natDegree < g.natDegree
a✝ : g.natDegree ≤ p.natDegree
fk : (φ f).natDegree = fu f.natDegree
gk : (φ g).natDegree = fu g.natDegree
fu0 : ∀ {n : ℕ}, n ≤ 0 → fu n = 0
fc : ∀ {n m : ℕ}, 0 ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < 0 → φ f = 0
FG : f.natDegree < 0
⊢ (φ f + φ g).natDegree = fu g.natDegree

case neg.succ
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
fu : ℕ → ℕ
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = fu n
f g : R[X]
fg : f.natDegree < g.natDegree
a✝ : g.natDegree ≤ p.natDegree
fk : (φ f).natDegree = fu f.natDegree
gk : (φ g).natDegree = fu g.natDegree
n✝ : ℕ
fu0 : ∀ {n : ℕ}, n ≤ n✝ + 1 → fu n = 0
fc : ∀ {n m : ℕ}, n✝ + 1 ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < n✝ + 1 → φ f = 0
FG : f.natDegree < n✝ + 1
⊢ (φ f + φ g).natDegree = fu g.natDegree
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = fu n
f g : R[X]
fg : f.natDegree < g.natDegree
a✝ : g.natDegree ≤ p.natDegree
fk : (φ f).natDegree = fu f.natDegree
gk : (φ g).natDegree = fu g.natDegree
FG : f.natDegree < k
⊢ (φ f + φ g).natDegree = fu g.natDegree

Tactic:
· cases k
      · nomatch FG
      · rwa [φ_k FG, zero_add]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ Multiset ?m.52

Tactic:
by assumption

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

Goal state before:
pp: case mp
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : h.unit⁻¹ • p * q = 0
this : h.unit⁻¹ • (p * q) = h.unit⁻¹ • p * q
⊢ q = 0

Tactic:
Monic.mul_right_eq_zero_iff

Goal state after:
case mp
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : q = 0
this : h.unit⁻¹ • (p * q) = h.unit⁻¹ • p * q
⊢ q = 0

case mp.h
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : h.unit⁻¹ • p * q = 0
this : h.unit⁻¹ • (p * q) = h.unit⁻¹ • p * q
⊢ (h.unit⁻¹ • p).Monic