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

Goal state before:
pp: case hb
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
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ supDegree D p + supDegree D q ∈ Set.range D

pp: case hmem
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
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ Function.invFun D (supDegree D p + supDegree D q) ∈ (p * q).coeff.support

pp: case hmax
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
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ ∀ a ∈ (p * q).coeff.support, D a ≤ supDegree D p + supDegree D q

Tactic:
· rw [← AddSubsemigroup.coe_set_mk (Set.range D), ← AddHom.srange_mk _ hadd, SetLike.mem_coe]
    · exact add_mem (supDegree_mem_range D hp) (supDegree_mem_range D hq)
    · exact (AddHom.srange ⟨D, hadd⟩).add_mem

Goal state after:
case hmem
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
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ Function.invFun D (supDegree D p + supDegree D q) ∈ (p * q).coeff.support

case hmax
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
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ ∀ a ∈ (p * q).coeff.support, D a ≤ supDegree D p + supDegree D q
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: S : Type v
inst✝¹ : CommSemiring S
R : Type u_1
inst✝ : Ring R
f : R →+* S
x : R
p : R[X]
h : (Polynomial.map f p).IsRoot (f x)
hf : Function.Injective ⇑f
⊢ eval x p = 0

Tactic:
← (injective_iff_map_eq_zero' f).mp hf,

Goal state after:
S : Type v
inst✝¹ : CommSemiring S
R : Type u_1
inst✝ : Ring R
f : R →+* S
x : R
p : R[X]
h : (Polynomial.map f p).IsRoot (f x)
hf : Function.Injective ⇑f
⊢ f (eval x p) = 0
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case succ
R : Type u_1
inst✝⁶ : Semiring R
A : Type u_8
B : Type u_9
inst✝⁵ : AddMonoid A
inst✝⁴ : AddMonoid B
inst✝³ : LinearOrder B
inst✝² : OrderBot B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
D : A → B
p : R[A]
n✝ : ℕ
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
hp : Monic D p
n : ℕ
ih : Monic D (p ^ n)
⊢ Monic D (p ^ (n + 1))

Tactic:
pow_succ'

Goal state after:
case succ
R : Type u_1
inst✝⁶ : Semiring R
A : Type u_8
B : Type u_9
inst✝⁵ : AddMonoid A
inst✝⁴ : AddMonoid B
inst✝³ : LinearOrder B
inst✝² : OrderBot B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
D : A → B
p : R[A]
n✝ : ℕ
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
hp : Monic D p
n : ℕ
ih : Monic D (p ^ n)
⊢ Monic D (p * p ^ n)
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: case C
R : Type u
A : Type z
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
q : Submodule R M
m : M
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
hm : m ∈ q
a✝ : A
hq : q ≤ Submodule.comap ((Algebra.lsmul R R M) a✝) q
a : R
⊢ (aeval a✝) (C a) • m ∈ q

Tactic:
| C a =>

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

Goal state before:
pp: case add
R : Type u
A : Type z
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
q : Submodule R M
m : M
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
hm : m ∈ q
a : A
hq : q ≤ Submodule.comap ((Algebra.lsmul R R M) a) q
f₁ f₂ : R[X]
h₁ : (aeval a) f₁ • m ∈ q
h₂ : (aeval a) f₂ • m ∈ q
⊢ (aeval a) (f₁ + f₂) • m ∈ q

Tactic:
| add f₁ f₂ h₁ h₂ =>

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

Goal state before:
pp: R : Type u
A : Type z
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
q : Submodule R M
m : M
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
hm : m ∈ q
p : R[X]
a : A
hq : q ≤ Submodule.comap ((Algebra.lsmul R R M) a) q
⊢ (aeval a) p • m ∈ q

Tactic:
induction p using Polynomial.induction_on with
  | C a => simpa using SMulMemClass.smul_mem a hm
  | add f₁ f₂ h₁ h₂ =>
    simp_rw [map_add, add_smul]
    exact Submodule.add_mem q h₁ h₂
  | monomial n t hmq =>
    rw [pow_succ', mul_left_comm, map_mul, aeval_X, mul_smul]
    solve_by_elim

Goal state after:
Module: Mathlib.Data.DFinsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → AddGroup (N a)
f₁ f₂ g : Π₀ (a : α), N a
⊢ (f₁ - g).neLocus (f₂ - g) = f₁.neLocus f₂

Tactic:
by
  simpa only [sub_eq_add_neg] using @neLocus_add_right α N _ _ _ _ _ _

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

Goal state before:
pp: 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 : MvPolynomial σ R
⊢ (eval x) (eval₂ f g p) = eval₂ ((eval x).comp f) (fun s ↦ (eval x) (g s)) p

Tactic:
apply induction_on p

Goal state after:
case C
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 : MvPolynomial σ R
⊢ ∀ (a : R), (eval x) (eval₂ f g (C a)) = eval₂ ((eval x).comp f) (fun s ↦ (eval x) (g s)) (C a)

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 : MvPolynomial σ R
⊢ ∀ (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)

case mul_X
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 : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    (eval x) (eval₂ f g p) = eval₂ ((eval x).comp f) (fun s ↦ (eval x) (g s)) p →
      (eval x) (eval₂ f g (p * X n)) = eval₂ ((eval x).comp f) (fun s ↦ (eval x) (g s)) (p * X n)
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ∃ s q, p = (rename Subtype.val) q

Tactic:
apply induction_on p

Goal state after:
case C
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ∀ (a : R), ∃ s q, C a = (rename Subtype.val) q

case add
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    (∃ s q, p = (rename Subtype.val) q) →
      (∃ s q_1, q = (rename Subtype.val) q_1) → ∃ s q_1, p + q = (rename Subtype.val) q_1

case mul_X
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ), (∃ s q, p = (rename Subtype.val) q) → ∃ s q, p * X n = (rename Subtype.val) 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₁
⊢ map f = eval₂Hom (C.comp f) X

Tactic:
ext a x

Goal state after:
case hC
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
a : R
x : σ →₀ ℕ
⊢ coeff x (((map f).comp C) a) = coeff x (((eval₂Hom (C.comp f) X).comp C) a)

case hX
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
a : σ
x : σ →₀ ℕ
⊢ coeff x ((map f) (X a)) = coeff x ((eval₂Hom (C.comp f) X) (X a))
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case C
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
f : R →+* S₁
inst✝ : DecidableEq S₁
a : R
⊢ ((map f) (C a)).coeffs ⊆ Finset.image (⇑f) (C a).coeffs

Tactic:
| C a =>

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.vars = ∅
⊢ p.degrees.card = 0

Tactic:
classical rw [vars_def, Multiset.toFinset_eq_empty] at h

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.degrees = 0
⊢ p.degrees.card = 0
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case refine_2.C
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
a : S₁
hx : ↑(C a).coeffs ⊆ range ⇑f
⊢ C a ∈ range ⇑(map f)

Tactic:
| C a =>

Goal state after:
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 + 1)).vars ⊆ φ.vars

Tactic:
pow_succ'

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

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

Tactic:
by
  classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert _ _ hs hsub =>
    simp only [hs, Finset.biUnion_insert, Finset.prod_insert, not_false_iff]
    apply Finset.Subset.trans (vars_mul _ _)
    exact Finset.union_subset_union (Finset.Subset.refl _) hsub

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

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

Tactic:
| C a =>

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
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
h : Pairwise (Disjoint on fun i ↦ (φ i).vars)
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, vars_add_of_disjoint, hsum]
    unfold Pairwise onFun at h
    simp only [Finset.disjoint_iff_ne] at h ⊢
    grind

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

Goal state before:
pp: 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
p : MvPolynomial σ R
s : subS
hs : ∀ i ∈ p.support, f (coeff i p) ∈ s
v : σ → S
hv : ∀ (i : σ), v i ∈ s
i : σ →₀ ℕ
⊢ f (coeff i p) ∈ s

Tactic:
by_cases hi : i ∈ p.support

Goal state after:
case pos
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
p : MvPolynomial σ R
s : subS
hs : ∀ i ∈ p.support, f (coeff i p) ∈ s
v : σ → S
hv : ∀ (i : σ), v i ∈ s
i : σ →₀ ℕ
hi : i ∈ p.support
⊢ f (coeff i p) ∈ s

case neg
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
p : MvPolynomial σ R
s : subS
hs : ∀ i ∈ p.support, f (coeff i p) ∈ s
v : σ → S
hv : ∀ (i : σ), v i ∈ s
i : σ →₀ ℕ
hi : i ∉ p.support
⊢ f (coeff i p) ∈ s
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case C
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 : R
hs : ∀ (i : σ →₀ ℕ), f (coeff i (C a)) ∈ s
⊢ eval₂ f v (C a) ∈ s

Tactic:
| C a =>

Goal state after:
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
⊢ 0 = s.sup fun i ↦ (f i).natDegree

Tactic:
eq_comm,

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) = 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
n : ℕ
hn : (p ^ n).natDegree = n * p.natDegree
⊢ (p ^ (n + 1)).natDegree = (n + 1) * p.natDegree

Tactic:
rw [pow_succ, (hp.pow n).natDegree_mul hp, hn, Nat.succ_mul, add_comm]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hm : p.Monic
hpu : IsUnit p
a✝ : Nontrivial R
q : R[X]
h : p * q = 1
this : 0 = p.natDegree + q.natDegree
⊢ p = 1

Tactic:
eq_comm,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
hm : p.Monic
hpu : IsUnit p
a✝ : Nontrivial R
q : R[X]
h : p * q = 1
this : p.natDegree + q.natDegree = 0
⊢ p = 1
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
x : ℕ
⊢ x ∈ ((finSuccEquiv R n) f).support ↔ x ∈ (fun m ↦ m 0) '' ↑f.support

Tactic:
simpa using congr(x ∈ $(support_finSuccEquiv f))

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
n : ℕ
⊢ MulOpposite.op ((y - x) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) = MulOpposite.op (y ^ n - x ^ n)

Tactic:
simp only [op_mul, op_sub, op_pow]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
⊢ 1 - x ∣ 1 - x ^ n

Tactic:
by
  conv_rhs => rw [← one_pow n]
  exact (Commute.one_left x).sub_dvd_pow_sub_pow n

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.Polynomial.Basic

Goal state before:
pp: R : Type u
S : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p : R[X]
hp : p.Monic
⊢ p.eraseLead.degree < p.degree

Tactic:
exact degree_eraseLead_lt (Polynomial.Monic.ne_zero_of_polynomial_ne hp one_ne_zero)

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
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
⊢ ∃ B₀, B₀.FG ∧ ⊤.FG

Tactic:
have := hy

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 this : span B ↑y = ⊤
⊢ ∃ B₀, B₀.FG ∧ ⊤.FG
Module: Mathlib.Algebra.Algebra.Subalgebra.MulOpposite

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
⊢ (Algebra.adjoin R s).op.toSubsemiring = (Algebra.adjoin R (MulOpposite.unop ⁻¹' s)).toSubsemiring

Tactic:
Algebra.adjoin,

Goal state after:
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
⊢ { toSubsemiring := Subsemiring.closure (Set.range ⇑(algebraMap R A) ∪ s), algebraMap_mem' := ⋯ }.op.toSubsemiring =
    Subsemiring.closure (Set.range ⇑(algebraMap R Aᵐᵒᵖ) ∪ MulOpposite.unop ⁻¹' s)
Module: Mathlib.Algebra.Algebra.Subalgebra.MulOpposite

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set Aᵐᵒᵖ
⊢ (Algebra.adjoin R s).unop.toSubsemiring = (Algebra.adjoin R (MulOpposite.op ⁻¹' s)).toSubsemiring

Tactic:
Algebra.adjoin,

Goal state after:
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set Aᵐᵒᵖ
⊢ { toSubsemiring := Subsemiring.closure (Set.range ⇑(algebraMap R Aᵐᵒᵖ) ∪ s),
          algebraMap_mem' := ⋯ }.unop.toSubsemiring =
    Subsemiring.closure (Set.range ⇑(algebraMap R A) ∪ MulOpposite.op ⁻¹' s)
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case add
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
g : R[M]
ihg : ∃ a, (MvPolynomial.aeval fun s ↦ of' R M ↑s) a = g
P : MvPolynomial (↑S) R
⊢ ∃ a, (MvPolynomial.aeval fun s ↦ of' R M ↑s) a = (MvPolynomial.aeval fun s ↦ of' R M ↑s) P + g

Tactic:
rcases ihg with ⟨Q, rfl⟩

Goal state after:
case add
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
P Q : MvPolynomial (↑S) R
⊢ ∃ a,
    (MvPolynomial.aeval fun s ↦ of' R M ↑s) a =
      (MvPolynomial.aeval fun s ↦ of' R M ↑s) P + (MvPolynomial.aeval fun s ↦ of' R M ↑s) Q
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case add
R : Type u_1
M : Type u_2
inst✝¹ : AddMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
g : R[M]
ihg : ∃ a, ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) a = g
P : FreeAlgebra R ↑S
⊢ ∃ a, ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) a = ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) P + g

Tactic:
rcases ihg with ⟨Q, rfl⟩

Goal state after:
case add
R : Type u_1
M : Type u_2
inst✝¹ : AddMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
P Q : FreeAlgebra R ↑S
⊢ ∃ a,
    ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) a =
      ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) P + ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) Q
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
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ ↑N
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
⊢ ↑p.natDegree = q.degree + ↑(k - q.natDegree)

Tactic:
Polynomial.degree_eq_natDegree hq0

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
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ ↑N
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
⊢ ↑p.natDegree = ↑q.natDegree + ↑(k - q.natDegree)
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case add
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
g : R[M]
ihg : ∃ a, (MvPolynomial.aeval fun s ↦ (of R M) ↑s) a = g
P : MvPolynomial (↑S) R
⊢ ∃ a, (MvPolynomial.aeval fun s ↦ (of R M) ↑s) a = (MvPolynomial.aeval fun s ↦ (of R M) ↑s) P + g

Tactic:
rcases ihg with ⟨Q, rfl⟩

Goal state after:
case add
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
P Q : MvPolynomial (↑S) R
⊢ ∃ a,
    (MvPolynomial.aeval fun s ↦ (of R M) ↑s) a =
      (MvPolynomial.aeval fun s ↦ (of R M) ↑s) P + (MvPolynomial.aeval fun s ↦ (of R M) ↑s) Q
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case add
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
g : R[M]
ihg : ∃ a, ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) a = g
P : FreeAlgebra R ↑S
⊢ ∃ a, ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) a = ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) P + g

Tactic:
rcases ihg with ⟨Q, rfl⟩

Goal state after:
case add
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
P Q : FreeAlgebra R ↑S
⊢ ∃ a,
    ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) a =
      ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) P + ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) Q
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
hpq : IsCoprime p q
⊢ ((aeval f) p).ker ⊓ ((aeval f) q).ker ≤ ⊥

Tactic:
intro v hv

Goal state after:
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
hpq : IsCoprime p q
v : M
hv : v ∈ ((aeval f) p).ker ⊓ ((aeval f) q).ker
⊢ v ∈ ⊥
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
⊢ ((aeval f) p).ker ⊔ ((aeval f) q).ker ≤ ((aeval f) (p * q)).ker

Tactic:
intro v hv

Goal state after:
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ ((aeval f) p).ker ⊔ ((aeval f) q).ker
⊢ v ∈ ((aeval f) (p * q)).ker
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
hpq : IsCoprime p q
⊢ ((aeval f) (p * q)).ker ≤ ((aeval f) p).ker ⊔ ((aeval f) q).ker

Tactic:
intro v hv

Goal state after:
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
hpq : IsCoprime p q
v : M
hv : v ∈ ((aeval f) (p * q)).ker
⊢ v ∈ ((aeval f) p).ker ⊔ ((aeval f) q).ker