mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
inst✝ : NoZeroDivisors R
hx : ¬x = 0
hy : y = 0
⊢ (x * y).leadingCoeff = x.leadingCoeff * y.leadingCoeff

pp: case neg
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
inst✝ : NoZeroDivisors R
hx : ¬x = 0
hy : ¬y = 0
⊢ (x * y).leadingCoeff = x.leadingCoeff * y.leadingCoeff

Tactic:
· simp [hy]

Goal state after:
case neg
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
inst✝ : NoZeroDivisors R
hx : ¬x = 0
hy : ¬y = 0
⊢ (x * y).leadingCoeff = x.leadingCoeff * y.leadingCoeff
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case succ
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
x : R⟦Γ⟧
n : ℕ
ih : n • x.orderTop ≤ (x ^ n).orderTop
⊢ (n + 1) • x.orderTop ≤ (x ^ (n + 1)).orderTop

Tactic:
| succ n ih =>

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Basic

Goal state before:
pp: R✝¹ : Type u_1
inst✝² : CommRing R✝¹
P✝¹ : RingPreordering R✝¹
R✝ : Type u_2
inst✝¹ : CommRing R✝
P✝ : Set R✝
add✝ : ?m.2
mul✝ : ?m.3
sq✝ : ?m.4
neg_one✝ : ?m.5
R : Type u_3
inst✝ : CommRing R
P : Set R
add : ∀ {x y : R}, x ∈ P → y ∈ P → x + y ∈ P
mul : ∀ {x y : R}, x ∈ P → y ∈ P → x * y ∈ P
sq : ∀ (x : R), x * x ∈ P
neg_one : -1 ∉ P
⊢ 0 ∈ P

Tactic:
by simpa using sq 0

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Basic

Goal state before:
pp: F : Type u_2
inst✝ : Field F
P : RingPreordering F
⊢ P.support = ⊥

Tactic:
by
  simpa [← Submodule.toAddSubgroup_inj] using supportAddSubgroup_eq_bot P

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case hfg
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : IsCancelAdd R
inst✝ : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this✝ : AddCancelCommMonoid R := { toAddCommMonoid := inst✝².toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ x, ¬y.coeff x = z.coeff x
this : {a | y.coeff a ≠ z.coeff a}.IsWF
a : Γ := this.min hyz
ha : y.coeff a ≠ z.coeff a
⊢ ∀ j ∈ antidiagonal ⋯ ⋯ (x.order + a) ∪ antidiagonal ⋯ ⋯ (x.order + a),
    j ≠ (x.order, a) → x.coeff j.1 * y.coeff j.2 = x.coeff j.1 * z.coeff j.2

Tactic:
simp +contextual only [mem_union, mem_antidiagonal, mul_eq_mul_left_iff, Prod.mk.injEq,
        ne_eq, ← and_or_left, ← or_and_right, or_false, and_imp, Prod.forall, mem_support, not_and]
      rintro b c hxb - hbc hbc'
      contrapose! hbc'
      rwa [eq_comm, eq_comm (a := c), ← add_eq_add_iff_eq_and_eq (order_le_of_coeff_ne_zero hxb)
        (Set.IsWF.min_le this hyz hbc'), eq_comm]

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
c : FiniteArchimedeanClass M
x : ↥(↑f).domain
hx : ↑x ∈ ball K c
d : FiniteArchimedeanClass M
hd : ↑d ≤ ↑c
ne : x ≠ 0
⊢ ArchimedeanClass.mk ↑x ≠ ⊤

Tactic:
by simpa using! ne

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
k : K
x : M
hk : ¬k = 0
c : FiniteArchimedeanClass M
this : f.evalCoeff (k • x) c = k • f.evalCoeff x c
⊢ { coeff := f.evalCoeff (k • x), isPWO_support' := ⋯ }.coeff c =
    (k • { coeff := f.evalCoeff x, isPWO_support' := ⋯ }).coeff c

Tactic:
by simpa using this

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
⊢ Ideal.comap (A.inclusion ⊤ ⋯) ⊥ = ⊥

Tactic:
Ideal.comap_bot_of_injective

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
⊢ ⊥ = ⊥

case hf
K : Type u
inst✝ : Field K
A : ValuationSubring K
⊢ Function.Injective ⇑(A.inclusion ⊤ ⋯)
Module: Mathlib.Algebra.Order.Sub.Unbundled.Hom

Goal state before:
pp: R : Type u_3
inst✝⁴ : NonUnitalCommSemiring R
inst✝³ : Preorder R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : MulLeftMono R
a b c : R
⊢ a * c - b * c ≤ (a - b) * c

Tactic:
simpa only [mul_comm _ c] using le_mul_tsub

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case convert_3
K : Type u
inst✝ : Field K
A : ValuationSubring K
x : ↥A.unitGroup
π : ↥A →+* ↥A ⧸ IsLocalRing.maximalIdeal ↥A := Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A)
⊢ ↑x ∈ A.principalUnitGroup ↔ π ↑(A.unitGroupMulEquiv x) - π 1 = 0

Tactic:
← π.map_sub,

Goal state after:
case convert_3
K : Type u
inst✝ : Field K
A : ValuationSubring K
x : ↥A.unitGroup
π : ↥A →+* ↥A ⧸ IsLocalRing.maximalIdeal ↥A := Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A)
⊢ ↑x ∈ A.principalUnitGroup ↔ π (↑(A.unitGroupMulEquiv x) - 1) = 0
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: case mk.mk
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
z : FiniteResidueField K
hz : 0 ≤ z
x y : FiniteElement K
h : mk x ≤ mk y
⊢ z * mk x ≤ z * mk y

Tactic:
induction z with | mk z
   =>  _ 

Goal state after:
case mk.mk.mk
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : FiniteElement K
h : mk x ≤ mk y
z : FiniteElement K
hz : 0 ≤ mk z
⊢ mk z * mk x ≤ mk z * mk y
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
a : G
inst✝ : DecidableEq α
s : Finset α
⊢ a ∈ stabilizer G s ↔ a • s ⊆ s

Tactic:
by
  rw [mem_stabilizer_iff, Finset.subset_iff_eq_of_card_le (Finset.card_smul_finset _ _).ge]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : P.eraseLead = 0
h₂ : (monomial P.natDegree) P.leadingCoeff = P
⊢ ((monomial P.natDegree) P.leadingCoeff).coeffList =
    P.leadingCoeff :: (List.replicate (P.natDegree - P.eraseLead.degree.succ) 0 ++ P.eraseLead.coeffList)

Tactic:
simp [coeffList_monomial (Polynomial.leadingCoeff_ne_zero.mpr h), hep]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
k : ℕ
hkd : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
⊢ P.coeff (P.degree.succ - 1 - (k + 1)) = P.eraseLead.coeff dk

Tactic:
eraseLead_coeff_of_ne (f := P) dk (by lia)

Goal state after:
R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
k : ℕ
hkd : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
⊢ P.coeff (P.degree.succ - 1 - (k + 1)) = P.coeff dk
Module: Mathlib.Algebra.Polynomial.CoeffList

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
k : ℕ
hkd : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
hkn : n ≤ k
⊢ some (P.eraseLead.coeff dk) =
    (List.map P.eraseLead.coeff
        (List.range
          P.eraseLead.degree.succ))[(List.map P.eraseLead.coeff (List.range P.eraseLead.degree.succ)).length - 1 -
        (k - n)]?

pp: case neg
R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
k : ℕ
hkd : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
hkn : n ≤ k
⊢ k - n < (List.map P.eraseLead.coeff (List.range P.eraseLead.degree.succ)).length

Tactic:
List.getElem?_map

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
k : ℕ
hkd : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
hkn : n ≤ k
⊢ some (P.eraseLead.coeff dk) =
    Option.map P.eraseLead.coeff
      (List.range
          P.eraseLead.degree.succ)[(List.map P.eraseLead.coeff (List.range P.eraseLead.degree.succ)).length - 1 -
          (k - n)]?

case neg
R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
k : ℕ
hkd : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
hkn : n ≤ k
⊢ k - n < (List.map P.eraseLead.coeff (List.range P.eraseLead.degree.succ)).length
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
inst✝ : IsOrderedAddMonoid R
c : Set (Partial seed)
hnonempty : c.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
x y : ↥(sSupFun hc).domain
h : x < y
hyx : ↑(y - x) ∈ sSup (LinearPMap.domain '' (fun x ↦ ↑x) '' c)
f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧
hmem : f ∈ (fun x ↦ ↑x) '' c
hf : ↑(y - x) ∈ f.domain
this : ↑(sSupFun hc) (y - x) = ↑f ⟨↑(y - x), hf⟩
f' : Partial seed
left✝ : f' ∈ c
hf' : ↑f' = f
hmono : StrictMono ↑f
⊢ 0 < ⟨↑(y - x), hf⟩

Tactic:
rw [← Subtype.coe_lt_coe]

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
inst✝ : IsOrderedAddMonoid R
c : Set (Partial seed)
hnonempty : c.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
x y : ↥(sSupFun hc).domain
h : x < y
hyx : ↑(y - x) ∈ sSup (LinearPMap.domain '' (fun x ↦ ↑x) '' c)
f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧
hmem : f ∈ (fun x ↦ ↑x) '' c
hf : ↑(y - x) ∈ f.domain
this : ↑(sSupFun hc) (y - x) = ↑f ⟨↑(y - x), hf⟩
f' : Partial seed
left✝ : f' ∈ c
hf' : ↑f' = f
hmono : StrictMono ↑f
⊢ ↑0 < ↑⟨↑(y - x), hf⟩
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Semiring R
p : R[X]
m : ℕ
hp : p.IsMonicOfDegree m
n : ℕ
ih : (p ^ n).IsMonicOfDegree (m * n)
⊢ (p ^ (n + 1)).IsMonicOfDegree (m * (n + 1))

Tactic:
| succ n ih =>

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hpq : (p * q).IsMonicOfDegree (m + n)
⊢ q.IsMonicOfDegree n

Tactic:
by
  rcases subsingleton_or_nontrivial R with H | H
  · simp only [isMonicOfDegree_iff_of_subsingleton, Nat.add_eq_zero_iff] at hpq ⊢
    exact hpq.2
  have h₂ : q.Monic := hp.monic.of_mul_monic_left hpq.monic
  refine ⟨?_, h₂⟩
  have := hpq.natDegree_eq
  have h : p.leadingCoeff * q.leadingCoeff ≠ 0 := by
    rw [hp.leadingCoeff_eq, h₂.leadingCoeff, one_mul]
    exact one_ne_zero
  rw [natDegree_mul' h, hp.natDegree_eq] at this
  exact (Nat.add_left_cancel this.symm).symm

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
⊢ (p * p.mirror).natDegree = 2 * p.natDegree

Tactic:
by_cases hp : p = 0
  · rw [hp, zero_mul, natDegree_zero, mul_zero]
  rw [natDegree_mul hp (mt mirror_eq_zero.mp hp), mirror_natDegree, two_mul]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
n : ℕ
hn : n ≠ 0
⊢ X.homogenize n = MvPolynomial.X 0 * MvPolynomial.X 1 ^ (n - 1)

Tactic:
rw [← pow_one X, homogenize_X_pow, pow_one]
  rwa [Nat.one_le_iff_ne_zero]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
n : ℕ
q : MvPolynomial (Fin 2) R
hq : q.IsHomogeneous n
⊢ ((MvPolynomial.aeval ![X, 1]) q).homogenize n = q

Tactic:
rw [q.as_sum]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
q : MvPolynomial (Fin 2) R
hq : q.IsHomogeneous n
⊢ ((MvPolynomial.aeval ![X, 1]) (∑ v ∈ q.support, (MvPolynomial.monomial v) (MvPolynomial.coeff v q))).homogenize n =
    ∑ v ∈ q.support, (MvPolynomial.monomial v) (MvPolynomial.coeff v q)
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
n : ℕ
q : MvPolynomial (Fin 2) R
hq : q.IsHomogeneous n
⊢ ((MvPolynomial.aeval ![X, 1]) (∑ v ∈ q.support, (MvPolynomial.monomial v) (MvPolynomial.coeff v q))).homogenize n =
    ∑ v ∈ q.support, (MvPolynomial.monomial v) (MvPolynomial.coeff v q)

Tactic:
simp only [MvPolynomial.aeval_sum, MvPolynomial.aeval_monomial, ← C_eq_algebraMap,
    homogenize_finsetSum, homogenize_C_mul]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
q : MvPolynomial (Fin 2) R
hq : q.IsHomogeneous n
⊢ ∑ x ∈ q.support, MvPolynomial.C (MvPolynomial.coeff x q) * (x.prod fun i k ↦ ![X, 1] i ^ k).homogenize n =
    ∑ v ∈ q.support, (MvPolynomial.monomial v) (MvPolynomial.coeff v q)
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
f g : R[X]
hg : g.Monic
n : ℕ
ih : ∃ q r, (∀ (i : Fin n), (r i).degree < g.degree) ∧ f = q * g ^ n + ∑ i, r i * g ^ ↑i
⊢ ∃ q r, (∀ (i : Fin (n + 1)), (r i).degree < g.degree) ∧ f = q * g ^ (n + 1) + ∑ i, r i * g ^ ↑i

Tactic:
| succ n ih =>

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
r : R
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : MulActionWithZero R S
x : S
n : ℕ
⊢ ((monomial n) r).smeval x = r • x ^ n

Tactic:
simp only [smeval_eq_sum, smul_pow, zero_smul, sum_monomial_index]

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

Goal state before:
pp: case succ
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
x : S
n : ℕ
ih : (↑n).smeval x = n • x ^ 0
⊢ (↑(n + 1)).smeval x = (n + 1) • x ^ 0

Tactic:
| succ n ih =>

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

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
g : R[X]
hg : g.Monic
n : ℕ
ih :
  ∀ {q₁ q₂ : R[X]} {r₁ r₂ : Fin n → R[X]},
    (∀ (i : Fin n), (r₁ i).degree < g.degree) →
      (∀ (i : Fin n), (r₂ i).degree < g.degree) →
        q₁ * g ^ n + ∑ i, r₁ i * g ^ ↑i = q₂ * g ^ n + ∑ i, r₂ i * g ^ ↑i → q₁ = q₂ ∧ r₁ = r₂
q₁ q₂ : R[X]
r₁ r₂ : Fin (n + 1) → R[X]
hr₁ : ∀ (i : Fin (n + 1)), (r₁ i).degree < g.degree
hr₂ : ∀ (i : Fin (n + 1)), (r₂ i).degree < g.degree
hf : q₁ * g ^ (n + 1) + ∑ i, r₁ i * g ^ ↑i = q₂ * g ^ (n + 1) + ∑ i, r₂ i * g ^ ↑i
⊢ q₁ = q₂ ∧ r₁ = r₂

Tactic:
| succ n ih =>

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

Goal state before:
pp: case monomial.succ
R : Type u_1
inst✝⁴ : Semiring R
p q : R[X]
S : Type u_2
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
x y : S
hc : Commute x y
a : R
n : ℕ
ih : Commute (x ^ n) (q.smeval y)
⊢ Commute (x ^ (n + 1)) (q.smeval y)

Tactic:
| succ n ih =>

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
d : ℕ
c : R
hcz : ¬c = 0
⊢ ((monomial d) c).signVariations = 0

Tactic:
· simp [hcz, signVariations, coeffList_eraseLead (mt (monomial_eq_zero_iff c d).mp hcz)]

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

Goal state before:
pp: case zero.zero
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
h✝¹ : SignType.sign P.leadingCoeff = SignType.zero
h✝ : SignType.sign P.eraseLead.leadingCoeff = SignType.zero
⊢ SignType.zero = -SignType.zero

Tactic:
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: case zero.neg
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
h✝¹ : SignType.sign P.leadingCoeff = SignType.zero
h✝ : SignType.sign P.eraseLead.leadingCoeff = SignType.neg
⊢ SignType.zero = -SignType.neg

Tactic:
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: case zero.pos
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
h✝¹ : SignType.sign P.leadingCoeff = SignType.zero
h✝ : SignType.sign P.eraseLead.leadingCoeff = SignType.pos
⊢ SignType.zero = -SignType.pos

Tactic:
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: case neg.zero
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
h✝¹ : SignType.sign P.leadingCoeff = SignType.neg
h✝ : SignType.sign P.eraseLead.leadingCoeff = SignType.zero
⊢ SignType.neg = -SignType.zero

Tactic:
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: case neg.neg
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
h✝¹ : SignType.sign P.leadingCoeff = SignType.neg
h✝ : SignType.sign P.eraseLead.leadingCoeff = SignType.neg
⊢ SignType.neg = -SignType.neg

Tactic:
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: case neg.pos
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
h✝¹ : SignType.sign P.leadingCoeff = SignType.neg
h✝ : SignType.sign P.eraseLead.leadingCoeff = SignType.pos
⊢ SignType.neg = -SignType.pos

Tactic:
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: case pos.zero
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
h✝¹ : SignType.sign P.leadingCoeff = SignType.pos
h✝ : SignType.sign P.eraseLead.leadingCoeff = SignType.zero
⊢ SignType.pos = -SignType.zero

Tactic:
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: case pos.neg
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
h✝¹ : SignType.sign P.leadingCoeff = SignType.pos
h✝ : SignType.sign P.eraseLead.leadingCoeff = SignType.neg
⊢ SignType.pos = -SignType.neg

Tactic:
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: case pos.pos
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
h✝¹ : SignType.sign P.leadingCoeff = SignType.pos
h✝ : SignType.sign P.eraseLead.leadingCoeff = SignType.pos
⊢ SignType.pos = -SignType.pos

Tactic:
grind [= SignType.neg_eq_neg_one, SignType.zero_eq_zero, SignType.pos_eq_one,
      SignType.neg_eq_neg_one, neg_neg]

Goal state after: