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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
x : Fin (n + 1) →₀ ℕ
⊢ x ∈ cons i '' ↑(((finSuccEquiv R n) f).coeff i).support ↔ x ∈ f.support ∧ x 0 = i

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
x : Fin (n + 1) →₀ ℕ
⊢ (∃ x_1, ¬coeff x_1 (((finSuccEquiv R n) f).coeff i) = 0 ∧ cons i x_1 = x) ↔ ¬coeff x f = 0 ∧ x 0 = i
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: S : Type u_1
inst✝ : Semiring S
n : ℕ
hd : S[X]
tl : List S[X]
IH : (∀ p ∈ tl, p.natDegree ≤ n) → tl.prod.coeff (tl.length * n) = (List.map (fun p ↦ p.coeff n) tl).prod
hl : ∀ p ∈ hd :: tl, p.natDegree ≤ n
hl' : ∀ p ∈ tl, p.natDegree ≤ n
⊢ ∀ x ∈ List.map natDegree tl, x ≤ n

Tactic:
simpa using

Goal state after:
S : Type u_1
inst✝ : Semiring S
n : ℕ
hd : S[X]
tl : List S[X]
IH : (∀ p ∈ tl, p.natDegree ≤ n) → tl.prod.coeff (tl.length * n) = (List.map (fun p ↦ p.coeff n) tl).prod
hl : ∀ p ∈ hd :: tl, p.natDegree ≤ n
hl' : ∀ p ∈ tl, p.natDegree ≤ n
⊢ ∀ a ∈ tl, a.natDegree ≤ n
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
⊢ ∀ (a : List R[X]), (prod ⟦a⟧).natDegree ≤ (Multiset.map natDegree ⟦a⟧).sum

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
⊢ ∀ (a : List R[X]), a.prod.natDegree ≤ (List.map natDegree a).sum
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
⊢ (∏ i ∈ s, f i).natDegree ≤ ∑ i ∈ s, (f i).natDegree

Tactic:
simpa using

Goal state after:
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
⊢ (∏ i ∈ s, f i).natDegree ≤ ∑ i ∈ s, (f i).natDegree
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
⊢ ∀ (a : List R[X]), (prod ⟦a⟧).degree ≤ (Multiset.map degree ⟦a⟧).sum

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
⊢ ∀ (a : List R[X]), a.prod.degree ≤ (List.map degree a).sum
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
h : ∏ i ∈ s, (f i).leadingCoeff ≠ 0
⊢ (∏ i ∈ s, f i).leadingCoeff = ∏ i ∈ s, (f i).leadingCoeff

Tactic:
simpa using

Goal state after:
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
h : ∏ i ∈ s, (f i).leadingCoeff ≠ 0
⊢ (∏ i ∈ s, f i).leadingCoeff = ∏ i ∈ s, (f i).leadingCoeff
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
h : ∏ i ∈ s, (f i).leadingCoeff ≠ 0
⊢ (Multiset.map leadingCoeff (Multiset.map f s.val)).prod ≠ 0

Tactic:
simpa using

Goal state after:
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
h : ∏ i ∈ s, (f i).leadingCoeff ≠ 0
⊢ ¬∏ x ∈ s, (f x).leadingCoeff = 0
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
h : ∏ i ∈ s, (f i).leadingCoeff ≠ 0
⊢ (∏ i ∈ s, f i).natDegree = ∑ i ∈ s, (f i).natDegree

Tactic:
simpa using

Goal state after:
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
h : ∏ i ∈ s, (f i).leadingCoeff ≠ 0
⊢ (∏ i ∈ s, f i).natDegree = ∑ i ∈ s, (f i).natDegree
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
h : ∏ i ∈ s, (f i).leadingCoeff ≠ 0
⊢ (Multiset.map (fun f ↦ f.leadingCoeff) (Multiset.map f s.val)).prod ≠ 0

Tactic:
simpa using

Goal state after:
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
h : ∏ i ∈ s, (f i).leadingCoeff ≠ 0
⊢ ¬∏ x ∈ s, (f x).leadingCoeff = 0
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
t : Multiset R[X]
inst✝ : Nontrivial R
h : ∀ f ∈ t, f.Monic
⊢ t.prod.Monic

Tactic:
simpa using

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
t : Multiset R[X]
inst✝ : Nontrivial R
h : ∀ f ∈ t, f.Monic
⊢ t.prod.Monic
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
h : ∀ i ∈ s, (f i).Monic
⊢ (∏ i ∈ s, f i).natDegree = ∑ i ∈ s, (f i).natDegree

Tactic:
simpa using

Goal state after:
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
h : ∀ i ∈ s, (f i).Monic
⊢ (∏ i ∈ s, f i).natDegree = ∑ i ∈ s, (f i).natDegree
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
h : ∀ i ∈ s, (f i).Monic
⊢ ∀ f_1 ∈ Multiset.map f s.val, f_1.Monic

Tactic:
simpa using

Goal state after:
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
h : ∀ i ∈ s, (f i).Monic
⊢ ∀ a ∈ s, (f a).Monic
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
f : ι → R[X]
inst✝ : Nontrivial R
h : ∀ i ∈ s, (f i).Monic
⊢ (∏ i ∈ s, f i).degree = ∑ i ∈ s, (f i).degree

Tactic:
simpa using

Goal state after:
R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
f : ι → R[X]
inst✝ : Nontrivial R
h : ∀ i ∈ s, (f i).Monic
⊢ (∏ i ∈ s, f i).degree = ∑ i ∈ s, (f i).degree
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
f : ι → R[X]
inst✝ : Nontrivial R
h : ∀ i ∈ s, (f i).Monic
⊢ ∀ f_1 ∈ Multiset.map f s.val, f_1.Monic

Tactic:
simpa using

Goal state after:
R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
f : ι → R[X]
inst✝ : Nontrivial R
h : ∀ i ∈ s, (f i).Monic
⊢ ∀ a ∈ s, (f a).Monic
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: case h
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
n : ℕ
a✝ : List R[X]
hl : ∀ p ∈ ⟦a✝⟧, p.natDegree ≤ n
⊢ (prod ⟦a✝⟧).coeff (Multiset.card ⟦a✝⟧ * n) = (Multiset.map (fun p ↦ p.coeff n) ⟦a✝⟧).prod

Tactic:
simpa using

Goal state after:
case h
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
n : ℕ
a✝ : List R[X]
hl : ∀ p ∈ ⟦a✝⟧, p.natDegree ≤ n
⊢ a✝.prod.coeff (a✝.length * n) = (List.map (fun p ↦ p.coeff n) a✝).prod
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
ι : Type w
inst✝ : CommSemiring R
f : ι → R[X]
n : ℕ
l : Multiset ι
hl : l.Nodup
h : ∀ p ∈ { val := l, nodup := hl }, (f p).natDegree ≤ n
⊢ ∀ p ∈ Multiset.map f l, p.natDegree ≤ n

Tactic:
simpa using

Goal state after:
R : Type u
ι : Type w
inst✝ : CommSemiring R
f : ι → R[X]
n : ℕ
l : Multiset ι
hl : l.Nodup
h : ∀ p ∈ { val := l, nodup := hl }, (f p).natDegree ≤ n
⊢ ∀ a ∈ l, (f a).natDegree ≤ n
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
⊢ (∏ i ∈ s, f i).coeff 0 = ∏ i ∈ s, (f i).coeff 0

Tactic:
simpa using

Goal state after:
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
⊢ (∏ i ∈ s, f i).coeff 0 = ∏ i ∈ s, (f i).coeff 0
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
ι : Type w
inst✝ : CommRing R
s : Finset ι
f : ι → R
⊢ (∏ i ∈ s, (X - C (f i))).nextCoeff = -∑ i ∈ s, f i

Tactic:
simpa using

Goal state after:
R : Type u
ι : Type w
inst✝ : CommRing R
s : Finset ι
f : ι → R
⊢ (∏ i ∈ s, (X - C (f i))).nextCoeff = -∑ i ∈ s, f i
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : AddLeftReflectLE R
inst✝³ : AddLeftMono R
inst✝² : ExistsAddOfLE R
inst✝¹ : Sub R
inst✝ : OrderedSub R
x y : R
hxy : y ≤ x
n : ℕ
⊢ (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) + y ^ n = x ^ n

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : AddLeftReflectLE R
inst✝³ : AddLeftMono R
inst✝² : ExistsAddOfLE R
inst✝¹ : Sub R
inst✝ : OrderedSub R
x y : R
hxy : y ≤ x
n : ℕ
⊢ (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) + y ^ n = x ^ n
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : AddLeftReflectLE R
inst✝³ : AddLeftMono R
inst✝² : ExistsAddOfLE R
inst✝¹ : Sub R
inst✝ : OrderedSub R
x : R
hx : 1 ≤ x
n : ℕ
⊢ (∑ i ∈ range n, x ^ i) * (x - 1) = x ^ n - 1

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : AddLeftReflectLE R
inst✝³ : AddLeftMono R
inst✝² : ExistsAddOfLE R
inst✝¹ : Sub R
inst✝ : OrderedSub R
x : R
hx : 1 ≤ x
n : ℕ
⊢ (∑ i ∈ range n, x ^ i) * (x - 1) = x ^ n - 1
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
ι : Type w
inst✝ : CommRing R
s : Finset ι
f : ι → R
hs : 0 < #s
⊢ (∏ i ∈ s, (X - C (f i))).coeff (#s - 1) = -∑ i ∈ s, f i

Tactic:
simpa using

Goal state after:
R : Type u
ι : Type w
inst✝ : CommRing R
s : Finset ι
f : ι → R
hs : 0 < #s
⊢ (∏ i ∈ s, (X - C (f i))).coeff (#s - 1) = -∑ i ∈ s, f i
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : AddLeftReflectLE R
inst✝³ : AddLeftMono R
inst✝² : ExistsAddOfLE R
inst✝¹ : Sub R
inst✝ : OrderedSub R
x : R
hx : x ≤ 1
n : ℕ
⊢ (∑ i ∈ range n, x ^ i) * (1 - x) = 1 - x ^ n

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : AddLeftReflectLE R
inst✝³ : AddLeftMono R
inst✝² : ExistsAddOfLE R
inst✝¹ : Sub R
inst✝ : OrderedSub R
x : R
hx : x ≤ 1
n : ℕ
⊢ (∑ i ∈ range n, x ^ i) * (1 - x) = 1 - x ^ n
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
ι : Type w
inst✝ : CommRing R
s : Finset ι
f : ι → R
hs : 0 < #s
⊢ 0 < (Multiset.map f s.val).card

Tactic:
simpa using

Goal state after:
R : Type u
ι : Type w
inst✝ : CommRing R
s : Finset ι
f : ι → R
hs : 0 < #s
⊢ s.Nonempty
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Ring R
x : R
⊢ (X - C x).Monic

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : Ring R
x : R
⊢ (X + -C x).Monic
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
n : ℕ
H : p.degree < ↑n
⊢ (X ^ n - p).Monic

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
n : ℕ
H : p.degree < ↑n
⊢ (X ^ n + -p).Monic
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Ring R
a : R
n : ℕ
h : n ≠ 0
⊢ (X ^ n - C a).Monic

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : Ring R
a : R
n : ℕ
h : n ≠ 0
⊢ (X ^ n - C a).Monic
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
hp : p.Monic
r : R
⊢ (p.comp (X - C r)).Monic

Tactic:
by
  simpa using! hp.comp_X_add_C (-r)

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

Goal state before:
pp: case neg
R : Type u
ι : Type w
s : Finset ι
inst✝² : CommRing R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v ↑s
i : ι
hi : i ∈ s
hf : ¬f i = 0
H : ∑ x ∈ s, (f x).coeff (f i).natDegree • v x = 0
⊢ False

Tactic:
exact hf (leadingCoeff_eq_zero.mp (linearIndepOn_finset_iff.mp h _ H i hi))

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
⊢ op ((x - 1) * ∑ i ∈ range n, x ^ i) = op (x ^ n - 1)

Tactic:
simpa using

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
⊢ (∑ i ∈ range n, x ^ i) * (1 - x) = 1 - x ^ n

Tactic:
have := congr_arg Neg.neg (geom_sum_mul x n)

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
⊢ op ((1 - x) * ∑ i ∈ range n, x ^ i) = op (1 - x ^ n)

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
⊢ (∑ x_1 ∈ range n, op x ^ x_1) * (1 - op x) = 1 - op x ^ n
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case refine_2
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
m : ℕ
hm : ∀ (m_1 : ℕ), m ≤ m_1 → (k • p).coeff m_1 = 0
⊢ (fun x ↦ k • x) (p.coeff m) = (fun x ↦ k • x) 0

Tactic:
simpa using

Goal state after:
case refine_2
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
m : ℕ
hm : ∀ (m_1 : ℕ), m ≤ m_1 → (k • p).coeff m_1 = 0
⊢ k • p.coeff m = 0
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]
⊢ (∏ i ∈ s, f i).leadingCoeff = ∏ i ∈ s, (f i).leadingCoeff

Tactic:
simpa using

Goal state after:
R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
⊢ (∏ i ∈ s, f i).leadingCoeff = ∏ i ∈ s, (f i).leadingCoeff
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
f : R[X]
⊢ f ∈ degreeLT R n ↔ f.degree < ↑n

Tactic:
simpa using

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

Goal state before:
pp: R : Type u
S : Type u_1
inst✝ : Semiring R
n : ℕ
x✝ : ↥(degreeLT R n)
p : R[X]
hp : p ∈ degreeLT R n
⊢ (fun f ↦ ⟨∑ i, (monomial ↑i) (f i), ⋯⟩) ((fun p n_1 ↦ (↑p).coeff ↑n_1) ⟨p, hp⟩) = ⟨p, hp⟩

Tactic:
simpa using

Goal state after:
R : Type u
S : Type u_1
inst✝ : Semiring R
n : ℕ
x✝ : ↥(degreeLT R n)
p : R[X]
hp : p ∈ degreeLT R n
⊢ ∑ x, (monomial ↑x) (p.coeff ↑x) = p
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x y : R
h : Commute x y
m n : ℕ
hmn : m ≤ n
k : ℕ
x✝ : k ∈ Ico m n
hp : Commute (MulOpposite.op y ^ (n - 1 - k)) (MulOpposite.op x ^ k)
⊢ MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k = MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k)

Tactic:
simpa using

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

Goal state before:
pp: x n : ℕ
⊢ x - 1 ∣ x ^ n - 1

Tactic:
simpa using

Goal state after:
x n : ℕ
⊢ x - 1 ∣ x ^ n - 1
Module: Mathlib.Algebra.Ring.GeomSum

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

Tactic:
simpa using

Goal state after:
m x y n : ℕ
⊢ x ^ m - y ^ m ∣ (x ^ m) ^ n - (y ^ m) ^ n
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: m k x : ℕ
hmk : m ∣ k
⊢ x ^ m - 1 ∣ x ^ k - 1

Tactic:
simpa using

Goal state after:
m k x : ℕ
hmk : m ∣ k
⊢ x ^ m - 1 ∣ x ^ k - 1
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: m : ℕ
hm : 2 ≤ m
n : ℕ
⊢ m ^ n = (∑ k ∈ range n, m ^ k) * (m - 1) + 1

Tactic:
simpa using

Goal state after:
m : ℕ
hm : 2 ≤ m
n : ℕ
⊢ m ^ n = (∑ k ∈ range n, m ^ k) * (m - 1) + 1
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: case refine_1
R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : IsNoetherian R A
P : Subalgebra R A → Prop
base : P ⊥
ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x ↑S))
t : Finset A
⊢ P (Algebra.adjoin R ↑∅)

Tactic:
simpa using

Goal state after:
case refine_1
R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : IsNoetherian R A
P : Subalgebra R A → Prop
base : P ⊥
ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x ↑S))
t : Finset A
⊢ P ⊥
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case pos
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f✝ : R[X]
hf✝ : f✝ ∈ map C I
f : R[X]
hf : f ∈ ⇑C '' ↑I
n : ℕ
x : R
hx : x ∈ ↑I ∧ C x = f
h : n = 0
⊢ (if n = 0 then x else 0) ∈ I

Tactic:
simpa using

Goal state after:
case pos
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f✝ : R[X]
hf✝ : f✝ ∈ map C I
f : R[X]
hf : f ∈ ⇑C '' ↑I
n : ℕ
x : R
hx : x ∈ ↑I ∧ C x = f
h : n = 0
⊢ x ∈ I
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: case refine_2
R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : IsNoetherian R A
P : Subalgebra R A → Prop
base : P ⊥
ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x ↑S))
t✝ : Finset A
x : A
t : Finset A
a✝ : x ∉ t
h : P (Algebra.adjoin R ↑t)
⊢ P (Algebra.adjoin R (insert x ↑t))

Tactic:
simpa using

Goal state after:
case refine_2
R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : IsNoetherian R A
P : Subalgebra R A → Prop
base : P ⊥
ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x ↑S))
t✝ : Finset A
x : A
t : Finset A
a✝ : x ∉ t
h : P (Algebra.adjoin R ↑t)
⊢ P (Algebra.adjoin R (insert x ↑t))
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
I J : Ideal R[X]
a : R
ha : a ∈ I.leadingCoeff
b : R
hb : b ∈ J.leadingCoeff
p : R[X]
hpI : p ∈ I
hp : p.leadingCoeff = a
q : R[X]
hqJ : q ∈ J
hq : q.leadingCoeff = b
⊢ (p * q).leadingCoeff = a * b

Tactic:
by simp [hp, hq]

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

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

Tactic:
simpa using

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
ι : Type u_2
s✝ : Finset ι
f : ι → Ideal R[X]
i : ι
s : Finset ι
hi : i ∉ s
hs : ∏ i ∈ s, (f i).leadingCoeff ≤ (s.prod f).leadingCoeff
⊢ (f i).leadingCoeff * ∏ i ∈ s, (f i).leadingCoeff ≤ (f i * ∏ x ∈ s, f x).leadingCoeff
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
I : Ideal R[X]
inst✝ : NoZeroDivisors R
n : ℕ
⊢ I.leadingCoeff ^ n ≤ (I ^ n).leadingCoeff

Tactic:
simpa using

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
I : Ideal R[X]
inst✝ : NoZeroDivisors R
n : ℕ
⊢ I.leadingCoeff ^ n ≤ (I ^ n).leadingCoeff
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommRing R
P : Ideal R
H : (map C P).IsPrime
this : (comap C (map C P)).IsPrime
x : R
h : ∀ (n : ℕ), (C x).coeff n ∈ P
⊢ x ∈ P

Tactic:
simpa using

Goal state after:
case mpr
R : Type u
inst✝ : CommRing R
P : Ideal R
H : (map C P).IsPrime
this : (comap C (map C P)).IsPrime
x : R
h : ∀ (n : ℕ), (C x).coeff n ∈ P
⊢ x ∈ P
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R[X]
hI : comap C I = I.leadingCoeff
n✝ : ℕ
ih : ∀ m < n✝, ∀ f ∈ I, f.natDegree = m → f ∈ map C (comap C I)
f : R[X]
hfI : f ∈ I
hn : f.natDegree = n✝
⊢ f.leadingCoeff ∈ comap C I

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : CommRing R
I : Ideal R[X]
hI : comap C I = I.leadingCoeff
n✝ : ℕ
ih : ∀ m < n✝, ∀ f ∈ I, f.natDegree = m → f ∈ map C (comap C I)
f : R[X]
hfI : f ∈ I
hn : f.natDegree = n✝
⊢ f.leadingCoeff ∈ I.leadingCoeff
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R[X]
hI : comap C I = I.leadingCoeff
n✝ : ℕ
ih : ∀ m < n✝, ∀ f ∈ I, f.natDegree = m → f ∈ map C (comap C I)
f : R[X]
hfI : f ∈ I
hn : f.natDegree = n✝
h : C f.leadingCoeff * X ^ f.natDegree ∈ map C (comap C I)
hlt : f.eraseLead.natDegree < f.natDegree
⊢ f.eraseLead ∈ I

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : CommRing R
I : Ideal R[X]
hI : comap C I = I.leadingCoeff
n✝ : ℕ
ih : ∀ m < n✝, ∀ f ∈ I, f.natDegree = m → f ∈ map C (comap C I)
f : R[X]
hfI : f ∈ I
hn : f.natDegree = n✝
h : C f.leadingCoeff * X ^ f.natDegree ∈ map C (comap C I)
hlt : f.eraseLead.natDegree < f.natDegree
⊢ f.eraseLead ∈ I
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case h.inl
R : Type u
inst✝ : CommRing R
I : Ideal R[X]
hI : comap C I = I.leadingCoeff
n✝ : ℕ
ih : ∀ m < n✝, ∀ f ∈ I, f.natDegree = m → f ∈ map C (comap C I)
f : R[X]
hfI : f ∈ I
hn : f.natDegree = n✝
h : C f.leadingCoeff * X ^ f.natDegree ∈ map C (comap C I)
hlt : f.eraseLead.natDegree < f.natDegree
he : f.eraseLead ∈ I
⊢ f ∈ map C (comap C I)

Tactic:
simpa using

Goal state after:
case h.inl
R : Type u
inst✝ : CommRing R
I : Ideal R[X]
hI : comap C I = I.leadingCoeff
n✝ : ℕ
ih : ∀ m < n✝, ∀ f ∈ I, f.natDegree = m → f ∈ map C (comap C I)
f : R[X]
hfI : f ∈ I
hn : f.natDegree = n✝
h : C f.leadingCoeff * X ^ f.natDegree ∈ map C (comap C I)
hlt : f.eraseLead.natDegree < f.natDegree
he : f.eraseLead ∈ I
⊢ f ∈ map C (comap C I)
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R[X]
hI : comap C I = I.leadingCoeff
n✝ : ℕ
ih : ∀ m < n✝, ∀ f ∈ I, f.natDegree = m → f ∈ map C (comap C I)
f : R[X]
hfI : f ∈ I
hn : f.natDegree = n✝
h : C f.leadingCoeff * X ^ f.natDegree ∈ map C (comap C I)
hlt : f.eraseLead.natDegree < f.natDegree
he : f.eraseLead ∈ I
⊢ f.eraseLead.natDegree < n✝

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : CommRing R
I : Ideal R[X]
hI : comap C I = I.leadingCoeff
n✝ : ℕ
ih : ∀ m < n✝, ∀ f ∈ I, f.natDegree = m → f ∈ map C (comap C I)
f : R[X]
hfI : f ∈ I
hn : f.natDegree = n✝
h : C f.leadingCoeff * X ^ f.natDegree ∈ map C (comap C I)
hlt : f.eraseLead.natDegree < f.natDegree
he : f.eraseLead ∈ I
⊢ f.eraseLead.natDegree < n✝
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case convert_3.zero
R : Type u
σ : Type v
r : R
inst✝¹ : CommRing R
inst✝ : Finite σ
this : Fintype σ
⊢ Prime (C r) ↔ Prime r

Tactic:
simpa using

Goal state after:
case convert_3.zero
R : Type u
σ : Type v
r : R
inst✝¹ : CommRing R
inst✝ : Finite σ
this : Fintype σ
⊢ Prime (C r) ↔ Prime r
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
σ : Type v
inst✝ : CommRing R
s : Set σ
p : MvPolynomial (↑s) R
⊢ Prime p ↔ Prime ((rename Subtype.val) p)

Tactic:
let eqv :=
      (sumAlgEquiv R (↥sᶜ) s).symm.trans
        (renameEquiv R <| (Equiv.sumComm (↥sᶜ) s).trans <| Equiv.Set.sumCompl s)

Goal state after:
R : Type u
σ : Type v
inst✝ : CommRing R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑sᶜ) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  (sumAlgEquiv R ↑sᶜ ↑s).symm.trans (renameEquiv R ((Equiv.sumComm ↑sᶜ ↑s).trans (Equiv.Set.sumCompl s)))
⊢ Prime p ↔ Prime ((rename Subtype.val) p)
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
σ : Type v
inst✝ : CommRing R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑sᶜ) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  (sumAlgEquiv R ↑sᶜ ↑s).symm.trans (renameEquiv R ((Equiv.sumComm ↑sᶜ ↑s).trans (Equiv.Set.sumCompl s)))
this :
  (rename Subtype.val) p =
    ((↑eqv).comp (Algebra.algHom R (MvPolynomial (↑s) R) (MvPolynomial (↑sᶜ) (MvPolynomial (↑s) R)))) p
⊢ Prime p ↔ Prime ((rename Subtype.val) p)

Tactic:
simpa using

Goal state after:
R : Type u
σ : Type v
inst✝ : CommRing R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑sᶜ) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  (sumAlgEquiv R ↑sᶜ ↑s).symm.trans (renameEquiv R ((Equiv.sumComm ↑sᶜ ↑s).trans (Equiv.Set.sumCompl s)))
this :
  (rename Subtype.val) p =
    ((↑eqv).comp (Algebra.algHom R (MvPolynomial (↑s) R) (MvPolynomial (↑sᶜ) (MvPolynomial (↑s) R)))) p
⊢ Prime p ↔ Prime (C p)