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

Goal state before:
pp: case neg
R : Type u_3
V : Type u_5
inst✝⁵ : AddCommMonoid V
Γ : Type u_6
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : Zero R
inst✝ : SMulWithZero R V
x : R⟦Γ⟧
y : HahnModule Γ R V
hx : ¬x = 0
hy : ¬(of R).symm y = 0
⊢ ∑ ij ∈ VAddAntidiagonal (⋯.min ⋯ + ⋯.min ⋯) ⋯, x.coeff ij.1 • ((of R).symm y).coeff ij.2 =
    x.leadingCoeff • ((of R).symm y).leadingCoeff

Tactic:
HahnSeries.leadingCoeff_of_ne_zero hx,

Goal state after:
case neg
R : Type u_3
V : Type u_5
inst✝⁵ : AddCommMonoid V
Γ : Type u_6
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : Zero R
inst✝ : SMulWithZero R V
x : R⟦Γ⟧
y : HahnModule Γ R V
hx : ¬x = 0
hy : ¬(of R).symm y = 0
⊢ ∑ ij ∈ VAddAntidiagonal (⋯.min ⋯ + ⋯.min ⋯) ⋯, x.coeff ij.1 • ((of R).symm y).coeff ij.2 =
    x.coeff (x.orderTop.untop ⋯) • ((of R).symm y).leadingCoeff
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x : R
hx : 0 ≤ mk x
n : ℕ
hn : x ≤ ↑n
⊢ ∃ n, x ≤ ↑n

Tactic:
exact ⟨n, mod_cast hn⟩

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x : R
hx : 0 ≤ mk x
n : ℕ
hn : x < ↑n
⊢ ∃ n, x < ↑n

Tactic:
exact ⟨n, mod_cast hn⟩

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : LinearOrder R
inst✝⁶ : LinearOrder S
inst✝⁵ : CommRing R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : Ring S
inst✝² : IsStrictOrderedRing S
inst✝¹ : DenselyOrdered R
inst✝ : Archimedean R
x y : S
f : R →+* S
hf : StrictMono ⇑f
H : ∀ {q : R}, 0 < f q ↔ 0 < q
q : R
hq₀ : 0 < f q
hq : f q * |y| ≤ |x|
hq₀' : 0 < q
n : ℕ
hn : 1 < n • q
⊢ 0 ≤ f (n • q)

Tactic:
rw [← f.map_zero]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : LinearOrder R
inst✝⁶ : LinearOrder S
inst✝⁵ : CommRing R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : Ring S
inst✝² : IsStrictOrderedRing S
inst✝¹ : DenselyOrdered R
inst✝ : Archimedean R
x y : S
f : R →+* S
hf : StrictMono ⇑f
H : ∀ {q : R}, 0 < f q ↔ 0 < q
q : R
hq₀ : 0 < f q
hq : f q * |y| ≤ |x|
hq₀' : 0 < q
n : ℕ
hn : 1 < n • q
⊢ f 0 ≤ f (n • q)
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case neg
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
hx : ¬x = 0
hy : ¬y = 0
this : (x * y).coeff (x.order + y.order) ≠ 0
hxy : x * y ≠ 0
⊢ ⋯.min ⋯ ≤ ⋯.min ⋯

Tactic:
exact Set.IsWF.min_le_min_of_subset support_mul_subset

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : LinearOrder R
inst✝⁶ : LinearOrder S
inst✝⁵ : CommRing R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : Ring S
inst✝² : IsStrictOrderedRing S
inst✝¹ : DenselyOrdered R
inst✝ : Archimedean R
x y : S
f : R →+* S
hf : StrictMono ⇑f
⊢ mk x ≤ mk y ↔ ∃ q, 0 < f q ∧ f q * |y| ≤ |x|

Tactic:
have H {q} : 0 < f q ↔ 0 < q := by simpa using hf.lt_iff_lt (a := 0)
  constructor
  · rintro ⟨(_ | n), hn⟩
    · simp_all [exists_zero_lt]
    · obtain ⟨q, hq₀, hq⟩ := exists_nsmul_lt_of_pos (one_pos (α := R)) (n + 1)
      refine ⟨q, H.2 hq₀, le_of_mul_le_mul_left ?_ n.cast_add_one_pos⟩
      simpa [← mul_assoc] using mul_le_mul (hf hq).le hn (abs_nonneg y) (by simp)
  · rintro ⟨q, hq₀, hq⟩
    have hq₀' := H.1 hq₀
    obtain ⟨n, hn⟩ := exists_lt_nsmul hq₀' 1
    refine ⟨n, le_of_mul_le_mul_left ?_ hq₀⟩
    have h : 0 ≤ f (n • q) := by
      rw [← f.map_zero]
      exact hf.monotone (nsmul_nonneg hq₀'.le n)
    simpa [mul_comm, mul_assoc] using mul_le_mul (hf hn).le hq (mul_nonneg hq₀.le (abs_nonneg y)) h

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : Field R
inst✝ : IsOrderedRing R
x y : R
h : mk x = mk y
hx : x ≠ 0
hy : y ≠ 0
⊢ mk x ≠ ⊤

Tactic:
simpa using hx

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
hx : x.leadingCoeff ≠ 0
hy : y.leadingCoeff ≠ 0
hxy : (x * y).coeff (x.order + y.order) ≠ 0
⊢ ⋯.min ⋯ ≤ ⋯.min ⋯

Tactic:
exact Set.IsWF.min_le_min_of_subset support_mul_subset

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
⊢ P.IsOrdering ↔ ∀ (a b : R), -(a * b) ∈ P → a ∈ P ∨ b ∈ P

Tactic:
refine ⟨fun _ a b _ => ?_, fun h => ?_⟩
  · by_contra
    have : a * b ∈ P := by simpa using mul_mem (by aesop : -a ∈ P) (by aesop : -b ∈ P)
    have : a ∈ P.support ∨ b ∈ P.support :=
      Ideal.IsPrime.mem_or_mem inferInstance (by simp_all [mem_support])
    simp_all [mem_support]
  · have : HasMemOrNegMem P := ⟨by simp [h]⟩
    refine IsOrdering.mk' P (fun {x y} _ => ?_)
    by_contra
    have := h (-x) y
    have := h (-x) (-y)
    have := h x y
    have := h x (-y)
    cases (by aesop : x ∈ P ∨ -x ∈ P) <;> simp_all [mem_support]

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

Goal state before:
pp: case a
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
x y : R⟦Γ⟧
hx : x ≠ 0
hy : y ≠ 0
⊢ ⋯.min ⋯ ≤ ⋯.min ⋯

Tactic:
exact Set.IsWF.min_le_min_of_subset support_mul_subset

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Units

Goal state before:
pp: case inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : Rˣ
h : ↑a < 0
⊢ Xor (a * -1 ∈ posSubgroup R) (a ∈ posSubgroup R)

pp: case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : Rˣ
h : 0 < ↑a
⊢ Xor (a * -1 ∈ posSubgroup R) (a ∈ posSubgroup R)

Tactic:
· simp [h, h.le]

Goal state after:
case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : Rˣ
h : 0 < ↑a
⊢ Xor (a * -1 ∈ posSubgroup R) (a ∈ posSubgroup R)
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case neg.refine_1
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
this : x ≠ 0
hr : x⁻¹ ∈ R
⊢ ⟨x⁻¹, hr⟩ ∈ (R.idealOfLE S h).primeCompl

Tactic:
simp only [Ideal.primeCompl, Submonoid.mem_mk, Subsemigroup.mem_mk, Set.mem_compl_iff,
        SetLike.mem_coe, idealOfLE, Ideal.mem_comap, IsLocalRing.mem_maximalIdeal, mem_nonunits_iff,
        not_not]

Goal state after:
case neg.refine_1
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
this : x ≠ 0
hr : x⁻¹ ∈ R
⊢ IsUnit ((R.inclusion S h) ⟨x⁻¹, hr⟩)
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case mpr
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A ≤ B
x : Kˣ
hx : (A.mapOfLE B h) (A.valuation ↑x) = (A.mapOfLE B h) 1
⊢ x ∈ B.unitGroup

Tactic:
simpa using hx

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

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
x : K
⊢ x ∈ A.nonunits ↔ x = 0 ∨ x⁻¹ ∉ A

Tactic:
rw [← valuation_le_one_iff, ← or_congr_right' fun h ↦ (A.valuation.one_le_val_iff h).not,
    ← lt_iff_not_ge, ← mem_nonunits_iff, or_iff_right_of_imp]
  rintro rfl
  exact A.nonunits.zero_mem

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

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
x✝ : ↥A.unitGroup
⊢ x✝ ∈ ((Units.map ↑(Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A))).comp A.unitGroupMulEquiv.toMonoidHom).ker ↔
    A.unitGroupMulEquiv x✝ ∈ (Units.map ↑(Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A))).ker

Tactic:
RingHom.toMonoidHom_eq_coe,

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
x✝ : ↥A.unitGroup
⊢ x✝ ∈ ((Units.map ↑(Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A))).comp A.unitGroupMulEquiv.toMonoidHom).ker ↔
    A.unitGroupMulEquiv x✝ ∈ (Units.map ↑(Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A))).ker
Module: Mathlib.Algebra.Order.UpperLower

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s t : Set α
⊢ ↑(lowerClosure (s * t)) = ↑(lowerClosure (↑(lowerClosure s) * t))

Tactic:
lowerClosure_mul,

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s t : Set α
⊢ ↑(lowerClosure (s * t)) = ↑(lowerClosure ↑(lowerClosure (s * t)))
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: case h
K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
x✝ y✝ : K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x y : FiniteElement K
hy : 0 < mk y
hx : mk x ≤ 0
⊢ mk x ≤ 0 • mk y

Tactic:
rwa [zero_nsmul]

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
hx' : ∀ {c : K}, c ≠ 0 → -c • x ∉ (↑f).domain
y z : ↥(f.extendFun hx).domain
hyzmem : ↑(z - y) ∈ (↑f).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f).domain
b : M
hb : b ∈ K ∙ x
hab : a + b = ↑(z - y)
hyz : 0 < ⟨a + b, ⋯⟩
this : z - y = ⟨a + b, ⋯⟩
c : K
habpos : 0 < a + c • x
hc : c • x = b
⊢ -(c • x) < a

Tactic:
exact neg_lt_iff_pos_add.mpr habpos

Goal state after:
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 y : K
hx : 0 < mk x
hy : 0 ≤ mk y
⊢ stdPart x + stdPart y = stdPart y

Tactic:
stdPart_of_mk_ne_zero hx.ne',

Goal state after:
case inl
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 < mk x
hy : 0 ≤ mk y
⊢ 0 + stdPart y = stdPart y
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:
sub_eq_add_neg,

Goal state after:
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
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:
sub_eq_add_neg,

Goal state after:
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
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
⊢ stdPart (x - y) = -stdPart y

Tactic:
sub_eq_add_neg,

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 < mk x
⊢ stdPart (x + -y) = -stdPart y
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
hy : 0 < mk y
⊢ stdPart (x - y) = stdPart x

Tactic:
sub_eq_add_neg,

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hy : 0 < mk y
⊢ stdPart (x + -y) = stdPart x
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
f : ℝ →+*o K
r : ℝ
hl : ∀ s < r, f s ≤ x
hr : ∀ s > r, x ≤ f s
hx : 0 ≤ mk x
h : stdPart x < r
⊢ stdPart x = r

Tactic:
obtain ⟨s, hs, hs'⟩ := exists_between h

Goal state after:
case inl
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 : stdPart x < r
s : ℝ
hs : stdPart x < s
hs' : s < r
⊢ stdPart x = r
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
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:
obtain ⟨s, hs, hs'⟩ := exists_between h

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
s : ℝ
hs : r < s
hs' : s < stdPart x
⊢ stdPart x = r
Module: Mathlib.Algebra.Polynomial.CoeffList

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
P : R[X]
⊢ P.coeffList.length = if P = 0 then 0 else P.natDegree + 1

Tactic:
by
  by_cases h : P = 0 <;> simp [h, coeffList, withBotSucc_degree_eq_natDegree_add_one]

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

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i✝ i : ℕ
⊢ 1 ^ deg(p) * span R coeffs(p) ≤ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)

Tactic:
by gcongr; exacts [le_sup_left, le_sup_right]

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
c : Set (Partial seed)
hnonempty : c.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
⊢ seed.baseEmbedding ≤ sSupFun hc

Tactic:
obtain ⟨f, hf⟩ := hnonempty
  exact le_trans f.prop.baseEmbedding_le (le_sSupFun hc hf)

Goal state after:
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:
rw [pow_succ, mul_add, mul_one]
    exact ih.mul hp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b r : R[X]
m n : ℕ
hmn : n ≤ m
ha : a.IsMonicOfDegree m
hb : b.IsMonicOfDegree n
hr : r.natDegree < m
h : b ∣ a - r
q : R[X]
⊢ q * b + r = q * b - -r

pp: R : Type u_1
inst✝ : CommRing R
a b r : R[X]
m n : ℕ
hmn : n ≤ m
ha : a.IsMonicOfDegree m
hb : b.IsMonicOfDegree n
hr : r.natDegree < m
h : b ∣ a - r
⊢ (-r).natDegree < m

Tactic:
· rw [sub_neg_eq_add]

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b r : R[X]
m n : ℕ
hmn : n ≤ m
ha : a.IsMonicOfDegree m
hb : b.IsMonicOfDegree n
hr : r.natDegree < m
h : b ∣ a - r
⊢ (-r).natDegree < m
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
r : R
⊢ ((aeval (X - C r)) p).IsMonicOfDegree n

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u_1
inst✝ : CommRing R
p : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
r : R
⊢ ((aeval (X + -C r)) p).IsMonicOfDegree n
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
ha : ¬a = 0
⊢ reflect n ((monomial n) a) * X ^ n = (monomial n) a

Tactic:
←
        C_mul_X_pow_eq_monomial,

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
ha : ¬a = 0
⊢ reflect n (C a * X ^ n) * X ^ n = C a * X ^ n
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∀ a ∈ Finset.range (p.natDegree + 1),
    p.mirror.coeff a ≠ 0 → (revAt (p.natDegree + p.natTrailingDegree)) a ∈ Finset.range (p.natDegree + 1)

Tactic:
intro n hn hp
    rw [Finset.mem_range_succ_iff] at *
    rw [revAt_le (hn.trans (Nat.le_add_right _ _))]
    rw [tsub_le_iff_tsub_le, add_comm, add_tsub_cancel_right, ← mirror_natTrailingDegree]
    exact natTrailingDegree_le_of_ne_zero hp

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
⊢ ((ofFn n) v).degree < ↑n

Tactic:
by
  by_cases h : ofFn n v = 0
  · simp only [h, degree_zero]
    exact Batteries.compareOfLessAndEq_eq_lt.mp rfl
  · exact (natDegree_lt_iff_degree_lt h).mp
      <| ofFn_natDegree_lt (Nat.one_le_iff_ne_zero.mpr <| ne_zero_of_ofFn_ne_zero h) _

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: case cons_cons
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b c : α
l : List α
IH : ∀ (a : α), IsChain R (destutter' R a l)
a : α
IH2 : ∀ (y a : α), R a y → IsChain R (a :: destutter' R y l)
⊢ if R a b then if R b c then R a b ∧ IsChain R (b :: destutter' R c l) else IsChain R (a :: destutter' R b l)
  else R a c → IsChain R (a :: destutter' R c l)

Tactic:
ite_prop_iff_and,

Goal state after:
case cons_cons
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b c : α
l : List α
IH : ∀ (a : α), IsChain R (destutter' R a l)
a : α
IH2 : ∀ (y a : α), R a y → IsChain R (a :: destutter' R y l)
⊢ (R a b → (R b c → R a b ∧ IsChain R (b :: destutter' R c l)) ∧ (¬R b c → IsChain R (a :: destutter' R b l))) ∧
    (¬R a b → R a c → IsChain R (a :: destutter' R c l))
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : ¬R b c
hac : R a c
⊢ (destutter' R b l).length ≤ (destutter' R c l).length + 1

Tactic:
exact Nat.le_succ_of_le (length_destutter'_cotrans_ge hbc)

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

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
S : Type u_2
inst✝² : AddCommGroup S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
p q : R[X]
x : S
⊢ (p - q).smeval x = p.smeval x - q.smeval x

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u_1
inst✝³ : Ring R
S : Type u_2
inst✝² : AddCommGroup S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
p q : R[X]
x : S
⊢ (p + -q).smeval x = p.smeval x - q.smeval x
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: case add
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
m n : ℕ
p q : R[X]
ph : p.smeval x * x ^ m * x ^ n = p.smeval x * (x ^ m * x ^ n)
qh : q.smeval x * x ^ m * x ^ n = q.smeval x * (x ^ m * x ^ n)
⊢ (p + q).smeval x * x ^ m * x ^ n = (p + q).smeval x * (x ^ m * x ^ n)

Tactic:
simp only [smeval_add, ph, qh, add_mul]

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
hp2 : 2 ≤ natDegree 0
hp3 : natDegree 0 ≤ 3
⊢ False

Tactic:
natDegree_zero

Goal state after:
K : Type u_1
inst✝ : Field K
hp2 : 2 ≤ 0
hp3 : natDegree 0 ≤ 3
⊢ False
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
⊢ ((0 + if n = m then v else 0) + if n = n then w else 0) = w

Tactic:
if_neg hmn.ne',

Goal state after:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
⊢ (0 + 0 + if n = n then w else 0) = w
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case refine_1
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ (trinomial k m n ↑u ↑v ↑w).coeff k ^ 2 + ∑ x ∈ {m, n}, (trinomial k m n ↑u ↑v ↑w).coeff x ^ 2 = 3

Tactic:
sum_insert (mt mem_singleton.mp hmn.ne),

Goal state after:
case refine_1
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ (trinomial k m n ↑u ↑v ↑w).coeff k ^ 2 +
      ((trinomial k m n ↑u ↑v ↑w).coeff m ^ 2 + ∑ x ∈ {n}, (trinomial k m n ↑u ↑v ↑w).coeff x ^ 2) =
    3
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case h
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q k : ℕ
hk : k < q
⊢ natDegree 0 ≤ p.natDegree - q ∧
    ∀ (r : A), (X - C r) ^ q ∣ map (algebraMap R A) p → (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) 0

Tactic:
natDegree_zero

Goal state after:
case h
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q k : ℕ
hk : k < q
⊢ 0 ≤ p.natDegree - q ∧
    ∀ (r : A), (X - C r) ^ q ∣ map (algebraMap R A) p → (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) 0
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]
q k : ℕ
x✝ : k < q ∨ q ≤ k
⊢ ∃ gp,
    gp.natDegree ≤ p.natDegree - q ∧
      ∀ (r : A), (X - C r) ^ q ∣ map (algebraMap R A) p → (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) gp

Tactic:
cases lt_or_ge k q with

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

Goal state before:
pp: case h
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)
⊢ natDegree 0 ≤ 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) 0

Tactic:
natDegree_zero

Goal state after:
case h
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)
⊢ 0 ≤ 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) 0
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.signVariations = ((X - C η) * P.eraseLead).signVariations

Tactic:
suffices eraseLead (eraseLead ((X - C η) * P)) = eraseLead ((X - C η) * P.eraseLead) by
    suffices (coeffList (eraseLead ((X - C η) * P))).map SignType.sign =
      (coeffList ((X - C η) * P.eraseLead)).map SignType.sign by
        rw [signVariations, signVariations, this]
    have : 0 < natDegree ((X - C η) * P.eraseLead) := by lia
    grind [leadingCoeff_mul, leadingCoeff_X_sub_C, one_mul, leadingCoeff_eraseLead_eq_nextCoeff,
      LT.lt.ne, sign_neg, coeffList_eraseLead, ne_zero_of_natDegree_gt,
      nextCoeff_eq_zero_of_eraseLead_eq_zero]

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.eraseLead = ((X - C η) * P.eraseLead).eraseLead