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

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
c : S₂
m✝ : S₁ ⊕ S₂ →₀ ℕ
⊢ coeff m✝ ((sumAlgEquiv R S₁ S₂).symm (C (X c))) = coeff m✝ (X (Sum.inr c))

Tactic:
;

Goal state after:
R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
c : S₂
m✝ : S₁ ⊕ S₂ →₀ ℕ
⊢ coeff m✝ ((sumAlgEquiv R S₁ S₂).symm (C (X c))) = coeff m✝ (X (Sum.inr c))
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
i✝ : S₂
m✝¹ : S₁ →₀ ℕ
m✝ : S₂ →₀ ℕ
⊢ coeff m✝ (coeff m✝¹ (((↑(sumAlgEquiv R S₁ S₂)).comp (rename Sum.inr)) (X i✝))) =
    coeff m✝ (coeff m✝¹ ((IsScalarTower.toAlgHom R (MvPolynomial S₂ R) (MvPolynomial S₁ (MvPolynomial S₂ R))) (X i✝)))

Tactic:
;

Goal state after:
R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
i✝ : S₂
m✝¹ : S₁ →₀ ℕ
m✝ : S₂ →₀ ℕ
⊢ coeff m✝ (coeff m✝¹ (((↑(sumAlgEquiv R S₁ S₂)).comp (rename Sum.inr)) (X i✝))) =
    coeff m✝ (coeff m✝¹ ((IsScalarTower.toAlgHom R (MvPolynomial S₂ R) (MvPolynomial S₁ (MvPolynomial S₂ R))) (X i✝)))
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
i✝ : S₁
m✝¹ : S₁ →₀ ℕ
m✝ : S₂ →₀ ℕ
⊢ coeff m✝ (coeff m✝¹ (((↑(sumAlgEquiv R S₁ S₂)).comp (rename Sum.inl)) (X i✝))) =
    coeff m✝ (coeff m✝¹ ((mapAlgHom (Algebra.ofId R (MvPolynomial S₂ R))) (X i✝)))

Tactic:
;

Goal state after:
R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
i✝ : S₁
m✝¹ : S₁ →₀ ℕ
m✝ : S₂ →₀ ℕ
⊢ coeff m✝ (coeff m✝¹ (((↑(sumAlgEquiv R S₁ S₂)).comp (rename Sum.inl)) (X i✝))) =
    coeff m✝ (coeff m✝¹ ((mapAlgHom (Algebra.ofId R (MvPolynomial S₂ R))) (X i✝)))
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u_2
S₁ : Type u_3
S₂ : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial S₂ R
i✝ : S₂
m✝¹ : S₂ →₀ ℕ
m✝ : S₁ →₀ ℕ
⊢ coeff m✝
      (coeff m✝¹
        (((↑(commAlgEquiv R S₁ S₂)).comp
            (IsScalarTower.toAlgHom R (MvPolynomial S₂ R) (MvPolynomial S₁ (MvPolynomial S₂ R))))
          (X i✝))) =
    coeff m✝ (coeff m✝¹ ((mapAlgHom (Algebra.ofId R (MvPolynomial S₁ R))) (X i✝)))

Tactic:
;

Goal state after:
R : Type u_2
S₁ : Type u_3
S₂ : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial S₂ R
i✝ : S₂
m✝¹ : S₂ →₀ ℕ
m✝ : S₁ →₀ ℕ
⊢ coeff m✝
      (coeff m✝¹
        (((↑(commAlgEquiv R S₁ S₂)).comp
            (IsScalarTower.toAlgHom R (MvPolynomial S₂ R) (MvPolynomial S₁ (MvPolynomial S₂ R))))
          (X i✝))) =
    coeff m✝ (coeff m✝¹ ((mapAlgHom (Algebra.ofId R (MvPolynomial S₁ R))) (X i✝)))
Module: Mathlib.Algebra.MvPolynomial.Equiv

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

Tactic:
;

Goal state after:
R : Type u_2
S₁ : Type u_3
S₂ : Type u_4
inst✝ : CommSemiring R
i : S₁
x : S₂ →₀ ℕ
y : S₁ →₀ ℕ
⊢ coeff y (coeff x ((commAlgEquiv R S₁ S₂) (X i))) = coeff y (coeff x (C (X i)))
Module: Mathlib.Algebra.MvPolynomial.Equiv

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

Tactic:
simp [X, C, monomial, commAlgEquiv]

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

Goal state before:
pp: 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
i : Option S₁
m✝ : Option S₁ →₀ ℕ
⊢ coeff m✝
      (((Polynomial.aevalTower (rename Option.some) (X none)).comp
          (aeval fun o ↦ o.elim Polynomial.X fun s ↦ Polynomial.C (X s)))
        (X i)) =
    coeff m✝ ((AlgHom.id R (MvPolynomial (Option S₁) R)) (X i))

Tactic:
;

Goal state after:
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
i : Option S₁
m✝ : Option S₁ →₀ ℕ
⊢ coeff m✝
      (((Polynomial.aevalTower (rename Option.some) (X none)).comp
          (aeval fun o ↦ o.elim Polynomial.X fun s ↦ Polynomial.C (X s)))
        (X i)) =
    coeff m✝ ((AlgHom.id R (MvPolynomial (Option S₁) R)) (X i))
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case h_add
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
m : Option S₁ →₀ ℕ
r : R
o✝ : Option S₁
m₁✝ m₂✝ : ℕ
⊢ (o✝.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ (m₁✝ + m₂✝) =
    (o✝.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ m₁✝ * (o✝.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ m₂✝

Tactic:
;

Goal state after:
case h_add
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
m : Option S₁ →₀ ℕ
r : R
o✝ : Option S₁
m₁✝ m₂✝ : ℕ
⊢ (o✝.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ (m₁✝ + m₂✝) =
    (o✝.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ m₁✝ * (o✝.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ m₂✝
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
⊢ ⊥ = if q.degree = 0 then 0 else ⊥

Tactic:
simp [hq.ne']

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

Goal state before:
pp: case pos
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
hpi : ((optionEquivLeft R S₁) p).coeff i = 0
⊢ totalDegree 0 + i ≤ p.totalDegree

Tactic:
;

Goal state after:
case pos
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
hpi : ((optionEquivLeft R S₁) p).coeff i = 0
⊢ totalDegree 0 + i ≤ p.totalDegree
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case pos
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hpi : ((optionEquivLeft R S₁) p).coeff i = 0
⊢ totalDegree 0 ≤ p.totalDegree

Tactic:
;

Goal state after:
case pos
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hpi : ((optionEquivLeft R S₁) p).coeff i = 0
⊢ totalDegree 0 ≤ p.totalDegree
Module: Mathlib.Algebra.MvPolynomial.Equiv

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

Tactic:
;

Goal state after:
case monomial
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ r * coeff m (if i = j 0 then ∏ x, X x ^ j x.succ else 0) = r * if j = cons i m then 1 else 0
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
ih : (p * X ^ n).reverse = p.reverse
⊢ (p * X ^ n * X).reverse = p.reverse

Tactic:
reverse_mul_X,

Goal state after:
case succ
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
ih : (p * X ^ n).reverse = p.reverse
⊢ (p * X ^ n).reverse = p.reverse
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case refine_1
R : Type u
ι : Type y
inst✝ : CommSemiring R
t : Multiset ι
f : ι → R[X]
⊢ (∀ i ∈ 0, (f i).Monic) → (Multiset.map f 0).prod.Monic

pp: case refine_2
R : Type u
ι : Type y
inst✝ : CommSemiring R
t : Multiset ι
f : ι → R[X]
⊢ ∀ (a : ι) (s : Multiset ι),
    ((∀ i ∈ s, (f i).Monic) → (Multiset.map f s).prod.Monic) →
      (∀ i ∈ a ::ₘ s, (f i).Monic) → (Multiset.map f (a ::ₘ s)).prod.Monic

Tactic:
;

Goal state after:
case refine_1
R : Type u
ι : Type y
inst✝ : CommSemiring R
t : Multiset ι
f : ι → R[X]
⊢ (∀ i ∈ 0, (f i).Monic) → (Multiset.map f 0).prod.Monic

case refine_2
R : Type u
ι : Type y
inst✝ : CommSemiring R
t : Multiset ι
f : ι → R[X]
⊢ ∀ (a : ι) (s : Multiset ι),
    ((∀ i ∈ s, (f i).Monic) → (Multiset.map f s).prod.Monic) →
      (∀ i ∈ a ::ₘ s, (f i).Monic) → (Multiset.map f (a ::ₘ s)).prod.Monic
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
⊢ (Multiset.map (fun f ↦ f.leadingCoeff) 0).prod ≠ 0 → (prod 0).natDegree = (Multiset.map (fun f ↦ f.natDegree) 0).sum

pp: case refine_2
R : Type u
inst✝ : CommSemiring R
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih : (Multiset.map (fun f ↦ f.leadingCoeff) t).prod ≠ 0 → t.prod.natDegree = (Multiset.map (fun f ↦ f.natDegree) t).sum
ht : (Multiset.map (fun f ↦ f.leadingCoeff) (a ::ₘ t)).prod ≠ 0
⊢ (a ::ₘ t).prod.natDegree = (Multiset.map (fun f ↦ f.natDegree) (a ::ₘ t)).sum

Tactic:
;

Goal state after:
case refine_1
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
⊢ (Multiset.map (fun f ↦ f.leadingCoeff) 0).prod ≠ 0 → (prod 0).natDegree = (Multiset.map (fun f ↦ f.natDegree) 0).sum

case refine_2
R : Type u
inst✝ : CommSemiring R
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih : (Multiset.map (fun f ↦ f.leadingCoeff) t).prod ≠ 0 → t.prod.natDegree = (Multiset.map (fun f ↦ f.natDegree) t).sum
ht : (Multiset.map (fun f ↦ f.leadingCoeff) (a ::ₘ t)).prod ≠ 0
⊢ (a ::ₘ t).prod.natDegree = (Multiset.map (fun f ↦ f.natDegree) (a ::ₘ t)).sum
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
⊢ ∀ (a : ℕ), (∑ x_1, if a = k x_1 then x x_1 else 0) ≠ 0 ↔ ∃ a_1, k a_1 = a

Tactic:
refine fun i => ⟨fun h => ?_, ?_⟩

Goal state after:
case refine_1
R : Type u_1
inst✝ : Semiring R
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
i : ℕ
h : (∑ x_1, if i = k x_1 then x x_1 else 0) ≠ 0
⊢ ∃ a, k a = i

case refine_2
R : Type u_1
inst✝ : Semiring R
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
i : ℕ
⊢ (∃ a, k a = i) → (∑ x_1, if i = k x_1 then x x_1 else 0) ≠ 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case pos
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p = 1
⊢ Irreducible p ↔ p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0

pp: case neg
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : ¬p = 1
⊢ Irreducible p ↔ p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0

Tactic:
;

Goal state after:
case pos
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p = 1
⊢ Irreducible p ↔ p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0

case neg
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : ¬p = 1
⊢ Irreducible p ↔ p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

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

Tactic:
rw [← aeval_algHom_apply, rename_X]

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

Goal state before:
pp: R : Type u_1
σ : Type u_3
inst✝ : CommSemiring R
i : σ
r : R
⊢ (toMvPolynomial i) (C r) = MvPolynomial.C r

Tactic:
by
  simp [toMvPolynomial]

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

Goal state before:
pp: R : Type u_1
σ : Type u_3
inst✝ : CommSemiring R
i : σ
⊢ (toMvPolynomial i) X = MvPolynomial.X i

Tactic:
by
  simp [toMvPolynomial]

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

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
⊢ (prod 0).coeff 0 = (Multiset.map (fun f ↦ f.coeff 0) 0).prod

pp: case refine_2
R : Type u
inst✝ : CommSemiring R
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ht : t.prod.coeff 0 = (Multiset.map (fun f ↦ f.coeff 0) t).prod
⊢ (a ::ₘ t).prod.coeff 0 = (Multiset.map (fun f ↦ f.coeff 0) (a ::ₘ t)).prod

Tactic:
;

Goal state after:
case refine_1
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
⊢ (prod 0).coeff 0 = (Multiset.map (fun f ↦ f.coeff 0) 0).prod

case refine_2
R : Type u
inst✝ : CommSemiring R
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ht : t.prod.coeff 0 = (Multiset.map (fun f ↦ f.coeff 0) t).prod
⊢ (a ::ₘ t).prod.coeff 0 = (Multiset.map (fun f ↦ f.coeff 0) (a ::ₘ t)).prod
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
⊢ ∑ i ∈ range 0, x ^ i * y ^ (0 - 1 - i) = ∑ i ∈ range 0, y ^ i * x ^ (0 - 1 - i)

pp: case succ
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
⊢ ∑ i ∈ range (n✝ + 1), x ^ i * y ^ (n✝ + 1 - 1 - i) = ∑ i ∈ range (n✝ + 1), y ^ i * x ^ (n✝ + 1 - 1 - i)

Tactic:
;

Goal state after:
case zero
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
⊢ ∑ i ∈ range 0, x ^ i * y ^ (0 - 1 - i) = ∑ i ∈ range 0, y ^ i * x ^ (0 - 1 - i)

case succ
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
⊢ ∑ i ∈ range (n✝ + 1), x ^ i * y ^ (n✝ + 1 - 1 - i) = ∑ i ∈ range (n✝ + 1), y ^ i * x ^ (n✝ + 1 - 1 - i)
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: case e_a.e_a
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ t.card = (Multiset.map (fun x ↦ X - C x) t).prod.natDegree

Tactic:
;

Goal state after:
case e_a.e_a
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ t.card = (Multiset.map (fun x ↦ X - C x) t).prod.natDegree
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
h : IsUnit (X ^ n - 1)
hn : n ≠ 0
⊢ False

Tactic:
apply hn

Goal state after:
case inr
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
h : IsUnit (X ^ n - 1)
hn : n ≠ 0
⊢ n = 0
Module: Mathlib.Algebra.Ring.GeomSum

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

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : Ring R
x : R
m n : ℕ
⊢ x ^ m - 1 ∣ (x ^ m) ^ n - 1
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
r : R
p b : ℕ
hp₀ : p = 0
hb₀ : ¬b = 0
h : 0 ∣ b
⊢ False

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : Ring R
r : R
p b : ℕ
hp₀ : p = 0
hb₀ : ¬b = 0
h : 0 ∣ b
⊢ False
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
r : R
p b : ℕ
hp₀ : p = 0
hb₀ : ¬b = 0
h : b = 0
⊢ False

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : Ring R
r : R
p b : ℕ
hp₀ : p = 0
hb₀ : ¬b = 0
h : b = 0
⊢ False
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
h : ∀ i ∈ s, f i ≠ 0
a✝ : Nontrivial R
x : ι
hx : x ∈ s
⊢ (f x).leadingCoeff ≠ 0

Tactic:
;

Goal state after:
R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
h : ∀ i ∈ s, f i ≠ 0
a✝ : Nontrivial R
x : ι
hx : x ∈ s
⊢ (f x).leadingCoeff ≠ 0
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case zero
R : Type u
S : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
⊢ ExpChar R[X] 1

pp: case prime
R : Type u
S : Type u_1
inst✝ : Semiring R
p : ℕ
hprime✝ : Nat.Prime p
hchar✝ : CharP R p
⊢ ExpChar R[X] p

Tactic:
;

Goal state after:
case zero
R : Type u
S : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
⊢ ExpChar R[X] 1

case prime
R : Type u
S : Type u_1
inst✝ : Semiring R
p : ℕ
hprime✝ : Nat.Prime p
hchar✝ : CharP R p
⊢ ExpChar R[X] p
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : WithBot ℕ
f : R[X]
⊢ (∀ (i : ℕ), ↑i > n → (lcoeff R i) f = 0) ↔ ∀ (m : ℕ), n < ↑m → f.coeff m = 0

Tactic:
;

Goal state after:
R : Type u
inst✝ : Semiring R
n : WithBot ℕ
f : R[X]
⊢ (∀ (i : ℕ), ↑i > n → (lcoeff R i) f = 0) ↔ ∀ (m : ℕ), n < ↑m → f.coeff m = 0
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree ≤ ↑n
k : ℕ
hk : k ∈ p.support
this : k ≤ ↑n
⊢ p.coeff k • X ^ k ∈ Submodule.span R ↑(image (fun n ↦ X ^ n) (range (n + 1)))

Tactic:
refine
      Submodule.smul_mem _ _
        (Submodule.subset_span <|
          Finset.mem_coe.2 <|
            Finset.mem_image.2 ⟨_, Finset.mem_range.2 (Nat.lt_succ_of_le this), rfl⟩)

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

Goal state before:
pp: R : Type u
S : Type u_1
inst✝ : Semiring R
n : ℕ
p q : ↥(degreeLT R n)
x✝ : Fin n
⊢ (↑(p + q)).coeff ↑x✝ = ((fun n_1 ↦ (↑p).coeff ↑n_1) + fun n_1 ↦ (↑q).coeff ↑n_1) x✝

Tactic:
;

Goal state after:
R : Type u
S : Type u_1
inst✝ : Semiring R
n : ℕ
p q : ↥(degreeLT R n)
x✝ : Fin n
⊢ (↑(p + q)).coeff ↑x✝ = ((fun n_1 ↦ (↑p).coeff ↑n_1) + fun n_1 ↦ (↑q).coeff ↑n_1) x✝
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
S : Type u_1
inst✝ : Semiring R
n : ℕ
x : R
p : ↥(degreeLT R n)
x✝ : Fin n
⊢ (↑(x • p)).coeff ↑x✝ = ((RingHom.id R) x • fun n_1 ↦ (↑p).coeff ↑n_1) x✝

Tactic:
;

Goal state after:
R : Type u
S : Type u_1
inst✝ : Semiring R
n : ℕ
x : R
p : ↥(degreeLT R n)
x✝ : Fin n
⊢ (↑(x • p)).coeff ↑x✝ = ((RingHom.id R) x • fun n_1 ↦ (↑p).coeff ↑n_1) x✝
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
S : Type u_1
inst✝ : Semiring R
n : ℕ
f : Fin n → R
i : Fin n
⊢ (fun p n_1 ↦ (↑p).coeff ↑n_1) ((fun f ↦ ⟨∑ i, (monomial ↑i) (f i), ⋯⟩) f) i = f i

Tactic:
;

Goal state after:
R : Type u
S : Type u_1
inst✝ : Semiring R
n : ℕ
f : Fin n → R
i : Fin n
⊢ (fun p n_1 ↦ (↑p).coeff ↑n_1) ((fun f ↦ ⟨∑ i, (monomial ↑i) (f i), ⋯⟩) f) i = f i
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: case refine_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
⊢ Subalgebra.toSubmodule (adjoin R (s ∪ t)) ≤ span R (p * q)

Tactic:
intro r

Goal state after:
case refine_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
r : A
⊢ r ∈ Subalgebra.toSubmodule (adjoin R (s ∪ t)) → r ∈ span R (p * q)
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: m x y n : ℕ
⊢ x ^ m - y ^ m ∣ x ^ (m * n) - y ^ (m * n)

Tactic:
;

Goal state after:
m x y n : ℕ
⊢ x ^ m - y ^ m ∣ x ^ (m * n) - y ^ (m * n)
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n i : ℕ
⊢ ((∑ i ∈ range n, X ^ i).comp (X + 1)).coeff i = ↑(n.choose (i + 1))

pp: R : Type u
inst✝ : Semiring R
n i : ℕ
⊢ ↑(n.choose (i + 1)) = (∑ i ∈ range n, ↑(n.choose (i + 1)) * X ^ i).coeff i

Tactic:
;

Goal state after:
R : Type u
inst✝ : Semiring R
n i : ℕ
⊢ ((∑ i ∈ range n, X ^ i).comp (X + 1)).coeff i = ↑(n.choose (i + 1))

R : Type u
inst✝ : Semiring R
n i : ℕ
⊢ ↑(n.choose (i + 1)) = (∑ i ∈ range n, ↑(n.choose (i + 1)) * X ^ i).coeff i
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
i : ℕ
⊢ (comp 0 (X + 1)).coeff i = ↑0

Tactic:
;

Goal state after:
case zero
R : Type u
inst✝ : Semiring R
i : ℕ
⊢ (comp 0 (X + 1)).coeff i = ↑0
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
i : ℕ
⊢ (if i = 0 then 1 else 0) = ↑(if i = 0 then 1 else 0)

Tactic:
;

Goal state after:
R : Type u
inst✝ : Ring R
i : ℕ
⊢ (if i = 0 then 1 else 0) = ↑(if i = 0 then 1 else 0)
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
m n : ℕ
H : m ≤ n
⊢ I.leadingCoeffNth m ≤ I.leadingCoeffNth n

Tactic:
intro r

Goal state after:
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
m n : ℕ
H : m ≤ n
r : R
⊢ r ∈ I.leadingCoeffNth m → r ∈ I.leadingCoeffNth n
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
a✝ : Nontrivial R
hR : IsField R[X]
p : R[X]
hp : X * p = 1
hp0 : p ≠ 0
this : p.degree < degree 1
⊢ False

Tactic:
degree_one,

Goal state after:
R : Type u
inst✝ : Ring R
a✝ : Nontrivial R
hR : IsField R[X]
p : R[X]
hp : X * p = 1
hp0 : p ≠ 0
this : p.degree < 0
⊢ False
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
hR : IsField R
I : Ideal R[X]
hI : I.IsMaximal
x : R
hx : C x ∈ I
hx0 : ¬x = 0
y : R
hy : x * y = 1
⊢ 1 ∈ I

Tactic:
convert! I.mul_mem_left (C y) hx

Goal state after:
R : Type u
inst✝ : Ring R
hR : IsField R
I : Ideal R[X]
hI : I.IsMaximal
x : R
hx : C x ∈ I
hx0 : ¬x = 0
y : R
hy : x * y = 1
⊢ 1 = C y * C x
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
h : C r = 0
⊢ False

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommRing R
r : R
hr : (Ideal.span {r}).IsPrime
this : r ≠ 0
h : C r = 0
⊢ False
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
k : ℕ
h : N < k
x✝ : R
hx : x✝ ∈ I.leadingCoeffNth k
hxm : x✝ ∉ M
⊢ I.leadingCoeffNth k ∈ Set.range I.leadingCoeffNth

Tactic:
;

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
k : ℕ
h : N < k
x✝ : R
hx : x✝ ∈ I.leadingCoeffNth k
hxm : x✝ ∉ M
⊢ I.leadingCoeffNth k ∈ Set.range I.leadingCoeffNth
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
⊢ { toSubsemiring := Subsemiring.closure (Set.range ⇑(algebraMap R A) ∪ s), algebraMap_mem' := ⋯ }.op.toSubsemiring =
    Subsemiring.closure (Set.range ⇑(algebraMap R Aᵐᵒᵖ) ∪ MulOpposite.unop ⁻¹' s)

Tactic:
op_toSubsemiring,

Goal state after:
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
⊢ (Subsemiring.closure (Set.range ⇑(algebraMap R A) ∪ s)).op =
    Subsemiring.closure (Set.range ⇑(algebraMap R Aᵐᵒᵖ) ∪ MulOpposite.unop ⁻¹' s)
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
p : R[X]
hp : p ∈ I
k : ℕ
hn : p.natDegree = k
⊢ p ∈ Ideal.span ↑s

Tactic:
induction k using Nat.strong_induction_on generalizing p with | _ k ih
         =>  _ 

Goal state after:
case h
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
⊢ p ∈ Ideal.span ↑s