mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
a : ↥A
h : A.valuation ↑a = 1
ha : ↑a ≠ 0
⊢ IsUnit a

Tactic:
have ha' : (a : K)⁻¹ ∈ A := by rw [← valuation_le_one_iff, map_inv₀, h, inv_one]

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : ↥A
h : A.valuation ↑a = 1
ha : ↑a ≠ 0
ha' : (↑a)⁻¹ ∈ A
⊢ IsUnit a
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: case inl
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
hx : mk x = 0
⊢ (if h : 0 ≤ mk x⁻¹ then (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x⁻¹ h) else 0) =
    (if h : 0 ≤ mk x then (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x h) else 0)⁻¹

Tactic:
have hx' : 0 ≤ mk x⁻¹ := by simp_all

Goal state after:
case inl
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
hx : mk x = 0
hx' : 0 ≤ mk x⁻¹
⊢ (if h : 0 ≤ mk x⁻¹ then (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x⁻¹ h) else 0) =
    (if h : 0 ≤ mk x then (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x h) else 0)⁻¹
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: case inl
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
hx : mk x = 0
⊢ stdPart x⁻¹ = (stdPart x)⁻¹

pp: case inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
hx : mk x ≠ 0
⊢ stdPart x⁻¹ = (stdPart x)⁻¹

Tactic:
· unfold stdPart
    have hx' : 0 ≤ mk x⁻¹ := by simp_all
    rw [dif_pos hx.ge, dif_pos hx']
    · apply eq_inv_of_mul_eq_one_left
      suffices FiniteElement.mk x⁻¹ hx' * .mk x hx.ge = 1 by
        rw [← map_mul, this, map_one]
      ext
      apply inv_mul_cancel₀
      aesop

Goal state after:
case inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
hx : mk x ≠ 0
⊢ stdPart x⁻¹ = (stdPart x)⁻¹
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 ≤ mk x
hy : 0 ≤ mk y
⊢ stdPart (x + y) = stdPart x + stdPart y

Tactic:
by
  unfold stdPart
  rw [dif_pos hx, dif_pos hy, dif_pos]
  exact map_add _ (FiniteElement.mk x hx) (.mk y hy)

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

Goal state before:
pp: K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
c : FiniteArchimedeanClass M
⊢ toLex ((truncLTLinearMap K c) (ofLex (f.eval x))) ∈ ((↑f).supSpanSingleton x (f.eval x) hx).toFun.range

Tactic:
LinearMap.mem_range

Goal state after:
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
c : FiniteArchimedeanClass M
⊢ ∃ y, ((↑f).supSpanSingleton x (f.eval x) hx).toFun y = toLex ((truncLTLinearMap K c) (ofLex (f.eval x)))
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: case inr.inl
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
f : ℝ →+*o K
hx : 0 ≤ mk x
hl : ∀ s < stdPart x, f s ≤ x
hr : ∀ s > stdPart x, x ≤ f s
⊢ stdPart x = stdPart x

pp: case inr.inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hl : ∀ s < r, f s ≤ x
hr : ∀ s > r, x ≤ f s
hx : 0 ≤ mk x
h : r < stdPart x
⊢ stdPart x = r

Tactic:
· rfl

Goal state after:
case inr.inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hl : ∀ s < r, f s ≤ x
hr : ∀ s > r, x ≤ f s
hx : 0 ≤ mk x
h : r < stdPart x
⊢ stdPart x = r
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case neg.inr
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
c : FiniteArchimedeanClass M
h : ¬∃ y, ↑y - x ∈ ball K c
d : FiniteArchimedeanClass M
hdc : c ≤ d
⊢ (ofLex (f.eval x)).coeff d = 0

Tactic:
eval,

Goal state after:
case neg.inr
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
c : FiniteArchimedeanClass M
h : ¬∃ y, ↑y - x ∈ ball K c
d : FiniteArchimedeanClass M
hdc : c ≤ d
⊢ (ofLex (toLex { coeff := f.evalCoeff x, isPWO_support' := ⋯ })).coeff d = 0
Module: Mathlib.Algebra.Polynomial.CoeffList

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Ring R
P : R[X]
hp : P = 0
⊢ (-P).coeffList = List.map (fun x ↦ -x) P.coeffList

Tactic:
rw [hp, coeffList_zero, neg_zero, coeffList_zero, List.map_nil]

Goal state after:
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: case monomial
R : Type u_1
A : Type u_2
M : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module A M
inst✝⁷ : Module R M
d : Derivation R A M
B : Type u_4
M' : Type u_5
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : AddCommGroup M'
inst✝² : Module B M'
inst✝¹ : Module R M'
inst✝ : Module A M'
d' : Derivation R B M'
f : M →ₗ[A] M'
h : ∀ (a : A), f (d a) = d' ((algebraMap A B) a)
x : B
n✝ : ℕ
a✝ : A
⊢ d' ((aeval x) ((monomial n✝) a✝)) =
    (PolynomialModule.eval x) ((PolynomialModule.map B f) (d.mapCoeffs ((monomial n✝) a✝))) +
      (aeval x) (derivative ((monomial n✝) a✝)) • d' x

Tactic:
simp only [aeval_monomial, leibniz, leibniz_pow, mapCoeffs_monomial,
      PolynomialModule.map_single, PolynomialModule.eval_single, derivative_monomial, map_mul,
      _root_.map_natCast, h]
    rw [add_comm, ← smul_smul, ← smul_smul, Nat.cast_smul_eq_nsmul]

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

Goal state before:
pp: case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
this : DecidableEq Fq := Classical.decEq Fq
p : Fq[X]
h✝ : p = 0
⊢ 0 ≤ 0

pp: case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
this : DecidableEq Fq := Classical.decEq Fq
p : Fq[X]
h✝ : ¬p = 0
⊢ 0 ≤ ↑(Fintype.card Fq) ^ p.natDegree

Tactic:
· rfl

Goal state after:
case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
this : DecidableEq Fq := Classical.decEq Fq
p : Fq[X]
h✝ : ¬p = 0
⊢ 0 ≤ ↑(Fintype.card Fq) ^ p.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree

Goal state before:
pp: Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
⊢ cardPowDegree p < cardPowDegree q ↔ p.degree < q.degree

Tactic:
simp only [cardPowDegree_apply]

Goal state after:
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
⊢ ((if p = 0 then 0 else ↑(Fintype.card Fq) ^ p.natDegree) < if q = 0 then 0 else ↑(Fintype.card Fq) ^ q.natDegree) ↔
    p.degree < q.degree
Module: Mathlib.Algebra.Polynomial.OfFn

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
x y : Fin n → R
i : ℕ
⊢ { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn (x + y)).toFinsupp }.coeff i =
    ({ toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn x).toFinsupp } +
          { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn y).toFinsupp }).coeff
      i

Tactic:
by_cases h : i < n

Goal state after:
case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
x y : Fin n → R
i : ℕ
h : i < n
⊢ { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn (x + y)).toFinsupp }.coeff i =
    ({ toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn x).toFinsupp } +
          { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn y).toFinsupp }).coeff
      i

case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
x y : Fin n → R
i : ℕ
h : ¬i < n
⊢ { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn (x + y)).toFinsupp }.coeff i =
    ({ toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn x).toFinsupp } +
          { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn y).toFinsupp }).coeff
      i
Module: Mathlib.Algebra.Polynomial.OfFn

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
x : R
p : Fin n → R
i : ℕ
⊢ { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn (x • p)).toFinsupp }.coeff i =
    ((RingHom.id R) x • { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn p).toFinsupp }).coeff i

Tactic:
by_cases h : i < n

Goal state after:
case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
x : R
p : Fin n → R
i : ℕ
h : i < n
⊢ { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn (x • p)).toFinsupp }.coeff i =
    ((RingHom.id R) x • { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn p).toFinsupp }).coeff i

case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
x : R
p : Fin n → R
i : ℕ
h : ¬i < n
⊢ { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn (x • p)).toFinsupp }.coeff i =
    ((RingHom.id R) x • { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn p).toFinsupp }).coeff i
Module: Mathlib.Algebra.Polynomial.Module.TensorProduct

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : R[X] ⊗[R] M →ₗ[R[X]] PolynomialModule R M := liftBaseChange R[X] (lsingle R 0)
inv : PolynomialModule R M →ₗ[R] R[X] ⊗[R] M := ↑R (eval X) ∘ₗ map R[X] ((TensorProduct.mk R R[X] M) 1)
⊢ inv ∘ₗ ↑R e = LinearMap.id

Tactic:
ext n x
    simp [inv, e, ← monomial_one_right_eq_X_pow, smul_tmul']

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
v : Fin n → R
h : n = 0
⊢ (ofFn n) v = 0

Tactic:
subst h

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
v : Fin 0 → R
⊢ (ofFn 0) v = 0
Module: Mathlib.Algebra.Polynomial.OfFn

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n i : ℕ
v : Fin n → R
hi : i < n
⊢ ((ofFn n) v).coeff i = v ⟨i, hi⟩

Tactic:
by
  simp [ofFn, hi]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
v : Fin n → R
h : n = 0
⊢ (ofFn n) v = ∑ i, (monomial ↑i) (v i)

Tactic:
subst h

Goal state after:
case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
v : Fin 0 → R
⊢ (ofFn 0) v = ∑ i, (monomial ↑i) (v i)
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: case monomial.succ
R : Type u_1
inst✝⁴ : Semiring R
p : R[X]
S : Type u_2
inst✝³ : NonAssocSemiring S
inst✝² : Module R S
inst✝¹ : Pow S ℕ
inst✝ : NatPowAssoc S
a : R
n : ℕ
⊢ a • 0 ^ (n + 1) = 0 • 1

Tactic:
npow_add,

Goal state after:
case monomial.succ
R : Type u_1
inst✝⁴ : Semiring R
p : R[X]
S : Type u_2
inst✝³ : NonAssocSemiring S
inst✝² : Module R S
inst✝¹ : Pow S ℕ
inst✝ : NatPowAssoc S
a : R
n : ℕ
⊢ a • (0 ^ n * 0 ^ 1) = 0 • 1
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: case monomial
R : Type u_1
inst✝⁵ : Semiring R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : SMulCommClass R S S
n : ℕ
a : R
⊢ a • x ^ (1 + n) = x * ((monomial n) a).smeval x

Tactic:
npow_add,

Goal state after:
case monomial
R : Type u_1
inst✝⁵ : Semiring R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : SMulCommClass R S S
n : ℕ
a : R
⊢ a • (x ^ 1 * x ^ n) = x * ((monomial n) a).smeval x
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : SMulCommClass R S S
n : ℕ
⊢ (X ^ (1 + n) * p).smeval x = x ^ (1 + n) * p.smeval x

Tactic:
npow_add,

Goal state after:
R : Type u_1
inst✝⁵ : Semiring R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : SMulCommClass R S S
n : ℕ
⊢ (X ^ 1 * X ^ n * p).smeval x = x ^ (1 + n) * p.smeval x
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : SMulCommClass R S S
n : ℕ
⊢ x * (x ^ n * p.smeval x) = x ^ (1 + n) * p.smeval x

Tactic:
npow_add,

Goal state after:
R : Type u_1
inst✝⁵ : Semiring R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : SMulCommClass R S S
n : ℕ
⊢ x * (x ^ n * p.smeval x) = x ^ 1 * x ^ n * p.smeval x
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: case monomial
R : Type u_1
inst✝⁵ : Semiring R
r : R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : SMulCommClass R S S
n✝ n : ℕ
a : R
⊢ (r * a) • x ^ (n✝ + n) = r • (x ^ n✝ * a • x ^ n)

Tactic:
npow_add,

Goal state after:
case monomial
R : Type u_1
inst✝⁵ : Semiring R
r : R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : SMulCommClass R S S
n✝ n : ℕ
a : R
⊢ (r * a) • (x ^ n✝ * x ^ n) = r • (x ^ n✝ * a • x ^ n)
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : IsScalarTower R S S
n : ℕ
⊢ (p * X ^ (n + 1)).smeval x = p.smeval x * x ^ (n + 1)

Tactic:
npow_add,

Goal state after:
R : Type u_1
inst✝⁵ : Semiring R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : IsScalarTower R S S
n : ℕ
⊢ (p * (X ^ n * X ^ 1)).smeval x = p.smeval x * x ^ (n + 1)
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : IsScalarTower R S S
n : ℕ
⊢ p.smeval x * x ^ n * x = p.smeval x * x ^ (n + 1)

Tactic:
npow_add,

Goal state after:
R : Type u_1
inst✝⁵ : Semiring R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : IsScalarTower R S S
n : ℕ
⊢ p.smeval x * x ^ n * x = p.smeval x * (x ^ n * x ^ 1)
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
p : R[X]
S : Type u_2
inst✝⁵ : NonAssocSemiring S
inst✝⁴ : Module R S
inst✝³ : Pow S ℕ
x : S
inst✝² : NatPowAssoc S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
n : ℕ
⊢ (p ^ (n + 1)).smeval x = p.smeval x ^ (n + 1)

Tactic:
npow_add,

Goal state after:
R : Type u_1
inst✝⁶ : Semiring R
p : R[X]
S : Type u_2
inst✝⁵ : NonAssocSemiring S
inst✝⁴ : Module R S
inst✝³ : Pow S ℕ
x : S
inst✝² : NatPowAssoc S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
n : ℕ
⊢ (p ^ n * p ^ 1).smeval x = p.smeval x ^ (n + 1)
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
p : R[X]
S : Type u_2
inst✝⁵ : NonAssocSemiring S
inst✝⁴ : Module R S
inst✝³ : Pow S ℕ
x : S
inst✝² : NatPowAssoc S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
n : ℕ
⊢ p.smeval x ^ n * p.smeval x = p.smeval x ^ (n + 1)

Tactic:
npow_add,

Goal state after:
R : Type u_1
inst✝⁶ : Semiring R
p : R[X]
S : Type u_2
inst✝⁵ : NonAssocSemiring S
inst✝⁴ : Module R S
inst✝³ : Pow S ℕ
x : S
inst✝² : NatPowAssoc S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
n : ℕ
⊢ p.smeval x ^ n * p.smeval x = p.smeval x ^ n * p.smeval x ^ 1
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
r : A
⊢ eval₂ (algebraMap R A) r (sumIDeriv p) = eval r (sumIDeriv (map (algebraMap R A) p))

Tactic:
eval,

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
r : A
⊢ eval₂ (algebraMap R A) r (sumIDeriv p) = eval₂ (RingHom.id A) r (sumIDeriv (map (algebraMap R A) p))
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
hsl : SignType.sign P.leadingCoeff ≠ 0
cs : List R
h_eL : P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: cs
h₁ : SignType.sign P.eraseLead.leadingCoeff ≠ 0
h₄ : ¬SignType.sign P.leadingCoeff = SignType.sign P.eraseLead.leadingCoeff
⊢ SignType.sign P.leadingCoeff = -SignType.sign P.eraseLead.leadingCoeff

Tactic:
cases _ : SignType.sign P.leadingCoeff
  <;> cases _ : SignType.sign P.eraseLead.leadingCoeff
  <;> grind [= SignType.neg_eq_neg_one, SignType.zero_eq_zero, SignType.pos_eq_one,
      SignType.neg_eq_neg_one, neg_neg]

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

Goal state before:
pp: R✝ : Type u_1
inst✝⁴ : Ring R✝
inst✝³ : LinearOrder R✝
η✝ : R✝
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
P : R[X]
hx : η ≠ 0
hx2 : 0 < η
⊢ (C η * P).signVariations = P.signVariations

Tactic:
rw [signVariations, signVariations]

Goal state after:
R✝ : Type u_1
inst✝⁴ : Ring R✝
inst✝³ : LinearOrder R✝
η✝ : R✝
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
P : R[X]
hx : η ≠ 0
hx2 : 0 < η
⊢ (List.destutter (fun x1 x2 ↦ x1 ≠ x2)
          (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) (C η * P).coeffList))).length -
      1 =
    (List.destutter (fun x1 x2 ↦ x1 ≠ x2)
          (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) P.coeffList))).length -
      1
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case inl
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
⊢ ∃ gp,
    gp.natDegree ≤ natDegree 0 - q ∧
      ∀ (r : A) {p' : A[X]},
        map (algebraMap R A) 0 = (X - C r) ^ (q - 1) * p' →
          (aeval r) (sumIDeriv 0) = (q - 1)! • eval r p' + q ! • (aeval r) gp

pp: case inr
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
⊢ ∃ gp,
    gp.natDegree ≤ p.natDegree - q ∧
      ∀ (r : A) {p' : A[X]},
        map (algebraMap R A) p = (X - C r) ^ (q - 1) * p' →
          (aeval r) (sumIDeriv p) = (q - 1)! • eval r p' + q ! • (aeval r) gp

Tactic:
· use 0
    rw [natDegree_zero]
    use Nat.zero_le _
    intro r p' hp
    rw [map_zero, map_zero, smul_zero, add_zero]
    rw [Polynomial.map_zero] at hp
    replace hp := (mul_eq_zero.mp hp.symm).resolve_left ?_
    · rw [hp, eval_zero, smul_zero]
    exact fun h => X_sub_C_ne_zero r (eq_zero_of_pow_eq_zero h)

Goal state after:
case inr
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
⊢ ∃ gp,
    gp.natDegree ≤ p.natDegree - q ∧
      ∀ (r : A) {p' : A[X]},
        map (algebraMap R A) p = (X - C r) ^ (q - 1) * p' →
          (aeval r) (sumIDeriv p) = (q - 1)! • eval r p' + q ! • (aeval r) gp
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : ((X - C η) * P).natDegree = P.natDegree + 1
hndxeP : ((X - C η) * P.eraseLead).natDegree = P.natDegree
hQ : ((X - C η) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
hQ₁ : ((X - C η) * P).nextCoeff < 0
hndexP0 : ((X - C η) * P).eraseLead.natDegree = P.natDegree
⊢ ((X - C η) * P).eraseLead.eraseLead = ((X - C η) * P.eraseLead).eraseLead

Tactic:
← self_sub_monomial_natDegree_leadingCoeff,

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : ((X - C η) * P).natDegree = P.natDegree + 1
hndxeP : ((X - C η) * P.eraseLead).natDegree = P.natDegree
hQ : ((X - C η) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
hQ₁ : ((X - C η) * P).nextCoeff < 0
hndexP0 : ((X - C η) * P).eraseLead.natDegree = P.natDegree
⊢ ((X - C η) * P).eraseLead - (monomial ((X - C η) * P).eraseLead.natDegree) ((X - C η) * P).eraseLead.leadingCoeff =
    ((X - C η) * P.eraseLead).eraseLead
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : ((X - C η) * P).natDegree = P.natDegree + 1
hndxeP : ((X - C η) * P.eraseLead).natDegree = P.natDegree
hQ : ((X - C η) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
hQ₁ : ((X - C η) * P).nextCoeff < 0
hndexP0 : ((X - C η) * P).eraseLead.natDegree = P.natDegree
⊢ ((X - C η) * P).eraseLead - (monomial P.natDegree) ((X - C η) * P).nextCoeff = ((X - C η) * P.eraseLead).eraseLead

Tactic:
← self_sub_monomial_natDegree_leadingCoeff,

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : ((X - C η) * P).natDegree = P.natDegree + 1
hndxeP : ((X - C η) * P.eraseLead).natDegree = P.natDegree
hQ : ((X - C η) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
hQ₁ : ((X - C η) * P).nextCoeff < 0
hndexP0 : ((X - C η) * P).eraseLead.natDegree = P.natDegree
⊢ (X - C η) * P - (monomial ((X - C η) * P).natDegree) ((X - C η) * P).leadingCoeff -
      (monomial P.natDegree) ((X - C η) * P).nextCoeff =
    ((X - C η) * P.eraseLead).eraseLead