mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
h : m.degree f ≠ 0
⊢ m.toSyn (m.degree (f - m.leadingTerm f)) < m.toSyn (m.degree f)

Tactic:
classical
  by_cases hl : f - m.leadingTerm f = 0
  · simpa [hl, toSyn_lt_iff_ne_zero]
  · apply lt_of_le_of_ne (m.degree_sub_leadingTerm_le f)
    by_contra! h'
    simp only [EmbeddingLike.apply_eq_iff_eq] at h'
    apply m.degree_mem_support at hl
    rw [h', mem_support_iff] at hl
    simp [leadingTerm, leadingCoeff] at hl

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
hf : f.IsMultiplicative
k : ℕ
hi : (f.ppow k).IsMultiplicative
⊢ (f.ppow (k + 1)).IsMultiplicative

Tactic:
rw [ppow_succ']

Goal state after:
case succ
R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
hf : f.IsMultiplicative
k : ℕ
hi : (f.ppow k).IsMultiplicative
⊢ (f.pmul (f.ppow k)).IsMultiplicative
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: m n : ℕ
hm : Squarefree m
hn : n ≠ 0
p : ℕ
this : m / m.gcd n ≠ 0
⊢ Prime p ∧ m.gcd n * p ∣ m ↔ (Prime p ∧ p ∣ m) ∧ (Prime p → ¬p ∣ n)

Tactic:
refine ⟨fun hp ↦ ⟨⟨hp.1, dvd_of_mul_left_dvd hp.2⟩, fun _ hpn ↦ hp.1.not_isUnit <| hm _ <|
    (mul_dvd_mul_right (dvd_gcd (dvd_of_mul_left_dvd hp.2) hpn) _).trans hp.2⟩, fun hp ↦
      ⟨hp.1.1, Coprime.mul_dvd_of_dvd_of_dvd ?_ (gcd_dvd_left _ _) hp.1.2⟩⟩

Goal state after:
m n : ℕ
hm : Squarefree m
hn : n ≠ 0
p : ℕ
this : m / m.gcd n ≠ 0
hp : (Prime p ∧ p ∣ m) ∧ (Prime p → ¬p ∣ n)
⊢ (m.gcd n).Coprime p
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: n : ℕ
⊢ Ω n = 0 ↔ n = 0 ∨ n = 1

Tactic:
rw [cardFactors_apply, List.length_eq_zero_iff, primeFactorsList_eq_nil]

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: case mpr
n : ℕ
h0 : n ≠ 0
h : n.primeFactorsList.Nodup
⊢ n.primeFactorsList.dedup.length = Ω n

Tactic:
simp [h.dedup, cardFactors]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
q : ℚ
⊢ inducedMap α β ↑q = ↑q

Tactic:
refine csSup_eq_of_forall_le_of_forall_lt_exists_gt
    (cutMap_nonempty β (q : α)) (fun x h => ?_) fun w h => ?_
  · rw [cutMap_coe] at h
    obtain ⟨r, h, rfl⟩ := h
    exact le_of_lt h
  · obtain ⟨q', hwq, hq⟩ := exists_rat_btwn h
    rw [cutMap_coe]
    exact ⟨q', ⟨_, hq, rfl⟩, hwq⟩

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, f (i ^ 0) = 1
⊢ y.factorization.support ⊆ x.primeFactors ∪ y.primeFactors

pp: R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, f (i ^ 0) = 1
⊢ x.factorization.support ⊆ x.primeFactors ∪ y.primeFactors

pp: R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, f (i ^ 0) = 1
⊢ (x.gcd y).factorization.support ⊆ x.primeFactors ∪ y.primeFactors

pp: R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, f (i ^ 0) = 1
⊢ (x.lcm y).factorization.support ⊆ x.primeFactors ∪ y.primeFactors

Tactic:
· apply subset_union_right

Goal state after:
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, f (i ^ 0) = 1
⊢ x.factorization.support ⊆ x.primeFactors ∪ y.primeFactors

R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, f (i ^ 0) = 1
⊢ (x.gcd y).factorization.support ⊆ x.primeFactors ∪ y.primeFactors

R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, f (i ^ 0) = 1
⊢ (x.lcm y).factorization.support ⊆ x.primeFactors ∪ y.primeFactors
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
ι : Type u_2
inst✝ : LinearOrder ι
s✝ : Finset ι
a : ι → M
i : ι
s : Finset ι
hi✝ : i ∉ s
hs : s.Nonempty
hi : s.min' hs ∉ s
ih✝ : StrictMonoOn (mk ∘ a) ↑s → mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hmono : StrictMonoOn (mk ∘ a) ↑(Finset.cons i s hi✝)
ih : mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hminmem : s.min' hs ∈ Finset.cons i s hi✝
h : mk (a i) = mk (a (s.min' hs))
eq : i = s.min' hs
⊢ False

Tactic:
exact hi (Finset.min'_mem _ hs)

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: case coe
n : ℕ
x✝ : ℝ≥0
hn₀ : ¬n = 0
⊢ n ≤ ⌈x✝⌉₊ ↔ n - 1 + 1 ≤ ⌈x✝⌉₊

Tactic:
Nat.sub_add_cancel

Goal state after:
case coe
n : ℕ
x✝ : ℝ≥0
hn₀ : ¬n = 0
⊢ n ≤ ⌈x✝⌉₊ ↔ n ≤ ⌈x✝⌉₊

case coe
n : ℕ
x✝ : ℝ≥0
hn₀ : ¬n = 0
⊢ 1 ≤ n
Module: Mathlib.Algebra.Order.Group.Cone

Goal state before:
pp: case mk.mk
G : Type u_1
inst✝ : CommGroup G
toSubmonoid✝¹ : Submonoid G
eq_one_of_mem_of_inv_mem'✝¹ : ∀ {a : G}, a ∈ toSubmonoid✝¹.carrier → a⁻¹ ∈ toSubmonoid✝¹.carrier → a = 1
toSubmonoid✝ : Submonoid G
eq_one_of_mem_of_inv_mem'✝ : ∀ {a : G}, a ∈ toSubmonoid✝.carrier → a⁻¹ ∈ toSubmonoid✝.carrier → a = 1
h :
  (fun C ↦ C.carrier) { toSubmonoid := toSubmonoid✝¹, eq_one_of_mem_of_inv_mem' := eq_one_of_mem_of_inv_mem'✝¹ } =
    (fun C ↦ C.carrier) { toSubmonoid := toSubmonoid✝, eq_one_of_mem_of_inv_mem' := eq_one_of_mem_of_inv_mem'✝ }
⊢ toSubmonoid✝¹ = toSubmonoid✝

Tactic:
exact SetLike.ext' h

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

Goal state before:
pp: case refine_2
M : Type u_1
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
K : Type u_2
inst✝⁵ : Ring K
inst✝⁴ : LinearOrder K
inst✝³ : IsOrderedRing K
inst✝² : Archimedean K
inst✝¹ : Module K M
inst✝ : PosSMulMono K M
a : M
k : K
h : k ≠ 0
this : Nontrivial K
m : ℕ
hm : 1 ≤ m • |k|
n : ℕ
hn : |k| ≤ n • 1
⊢ |k| • |a| ≤ n • |a|

Tactic:
have : n • |a| = (n • (1 : K)) • |a| := by rw [smul_assoc, one_smul]
    rw [this]
    exact smul_le_smul_of_nonneg_right hn (by simp)

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a : Γ
r : R
⊢ ((single a) r).support ⊆ {a}

Tactic:
by
  classical exact Pi.support_single_subset

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

Goal state before:
pp: case mp.inr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
h : 0 ≤ (ofLex x).leadingCoeff
hlt : 0 < (ofLex x).leadingCoeff
⊢ 0 ≤ x

Tactic:
· exact (leadingCoeff_pos_iff.mp hlt).le

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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : PartialOrder R
Γ' : Type u_3
inst✝¹ : LinearOrder Γ'
f : Γ ↪o Γ'
inst✝ : Zero R
a b : Lex R⟦Γ⟧
⊢ { toFun := fun a ↦ toLex (embDomain f (ofLex a)), inj' := ⋯ } a ≤
      { toFun := fun a ↦ toLex (embDomain f (ofLex a)), inj' := ⋯ } b ↔
    a ≤ b

Tactic:
by
    simp_rw [le_iff_lt_or_eq, lt_iff]
    simp only [Function.Embedding.coeFn_mk, ofLex_toLex, EmbeddingLike.apply_eq_iff_eq]
    constructor
    · rintro (⟨i, hj, hi⟩ | heq)
      · have himem : i ∈ Set.range f := by
          contrapose hi
          simp [embDomain_of_notMem_range hi]
        obtain ⟨k, rfl⟩ := himem
        refine Or.inl ⟨k, fun j hjk ↦ ?_, by simpa using hi⟩
        simpa using hj (f j) (f.lt_iff_lt.mpr hjk)
      · exact Or.inr <| embDomain_injective.comp (ofLex.injective) heq
    · rintro (⟨i, hj, hi⟩ | rfl)
      · refine Or.inl ⟨f i, fun k hki ↦ ?_, by simpa using hi⟩
        by_cases hkmem : k ∈ Set.range f
        · obtain ⟨j', rfl⟩ := hkmem
          simpa using hj _ <| f.lt_iff_lt.mp hki
        · simp_rw [embDomain_of_notMem_range hkmem]
      · simp

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

Goal state before:
pp: case mk.mk
R : Type u_1
inst✝ : Ring R
toSubsemiring✝¹ : Subsemiring R
eq_zero_of_mem_of_neg_mem'✝¹ : ∀ {a : R}, a ∈ toSubsemiring✝¹.carrier → -a ∈ toSubsemiring✝¹.carrier → a = 0
toSubsemiring✝ : Subsemiring R
eq_zero_of_mem_of_neg_mem'✝ : ∀ {a : R}, a ∈ toSubsemiring✝.carrier → -a ∈ toSubsemiring✝.carrier → a = 0
h :
  (fun C ↦ C.carrier) { toSubsemiring := toSubsemiring✝¹, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem'✝¹ } =
    (fun C ↦ C.carrier) { toSubsemiring := toSubsemiring✝, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem'✝ }
⊢ toSubsemiring✝¹ = toSubsemiring✝

Tactic:
exact SetLike.ext' h

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

Goal state before:
pp: α : Type u_2
S : Type u_3
inst✝¹ : LinearOrder S
inst✝ : AddCommGroup α
f : α → S
fna : IsNonarchimedean f
Neg : ∀ (a : α), f a = f (-a)
a b : α
hne : f a ≠ f b
hab : f a > f b
h : f (a + b + -b) ≤ f (-b)
⊢ f (-b) < f (a + b + -b)

Tactic:
by simpa [Neg b] using hab

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

Goal state before:
pp: case mk.mk
R : Type u_1
inst✝ : CommRing R
toSubsemiring✝¹ : Subsemiring R
mem_of_isSquare'✝¹ : ∀ {x : R}, IsSquare x → x ∈ toSubsemiring✝¹.carrier
neg_one_notMem'✝¹ : -1 ∉ toSubsemiring✝¹.carrier
toSubsemiring✝ : Subsemiring R
mem_of_isSquare'✝ : ∀ {x : R}, IsSquare x → x ∈ toSubsemiring✝.carrier
neg_one_notMem'✝ : -1 ∉ toSubsemiring✝.carrier
h :
  (fun P ↦ (↑P).carrier)
      { toSubsemiring := toSubsemiring✝¹, mem_of_isSquare' := mem_of_isSquare'✝¹,
        neg_one_notMem' := neg_one_notMem'✝¹ } =
    (fun P ↦ (↑P).carrier)
      { toSubsemiring := toSubsemiring✝, mem_of_isSquare' := mem_of_isSquare'✝, neg_one_notMem' := neg_one_notMem'✝ }
⊢ toSubsemiring✝¹ = toSubsemiring✝

Tactic:
exact SetLike.ext' h

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

Goal state before:
pp: R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : Field R
inst✝ : IsOrderedRing R
n : ℕ
x : ArchimedeanClass R
⊢ ↑n.succ • x = ↑n • x + x

Tactic:
by
  induction x with | mk x
  rw [← mk_zpow, Nat.cast_succ]
  obtain rfl | hx := eq_or_ne x 0
  · simp [zero_zpow _ n.cast_add_one_ne_zero]
  · rw [zpow_add_one₀ hx, mk_mul, mk_zpow]

Goal state after:
Module: Mathlib.Order.Quotient

Goal state before:
pp: case h.h.inl
α : Type u_1
s : Setoid α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
x y : α
h : x ≤ y
⊢ ⟦x⟧ ≤ ⟦y⟧ ∨ ⟦y⟧ ≤ ⟦x⟧

pp: case h.h.inr
α : Type u_1
s : Setoid α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
x y : α
h : y ≤ x
⊢ ⟦x⟧ ≤ ⟦y⟧ ∨ ⟦y⟧ ≤ ⟦x⟧

Tactic:
· exact .inl <| .single <| .inl h

Goal state after:
case h.h.inr
α : Type u_1
s : Setoid α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
x y : α
h : y ≤ x
⊢ ⟦x⟧ ≤ ⟦y⟧ ∨ ⟦y⟧ ≤ ⟦x⟧
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
⊢ (x * y).coeff (x.order + y.order) ≠ 0

Tactic:
simp [coeff_mul_order_add_order x y, *]

Goal state after:
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
c : ↑a = 0
⊢ False

Tactic:
c,

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : ↥A
h : A.valuation 0 = 1
c : ↑a = 0
⊢ False
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A R S : ValuationSubring K
hR : A ≤ R
hS : A ≤ S
h : R ≤ S
x : ↥A
hx : x ∈ A.idealOfLE S hS
c : 1 ≤ S.valuation ↑((A.inclusion R hR) x)
⊢ False

Tactic:
apply not_le_of_gt ((valuation_lt_one_iff S _).1 hx) c

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

Goal state before:
pp: case mk.mk.mk.inl
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
h✝ : mk x ≤ mk y
z : FiniteElement K
h : x ≤ y
⊢ mk x + mk z ≤ mk y + mk z

pp: case mk.mk.mk.inr
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
h✝ : mk x ≤ mk y
z : FiniteElement K
h : mk x = mk y
⊢ mk x + mk z ≤ mk y + mk z

Tactic:
· exact mk.monotone' <| add_le_add_left h _

Goal state after:
case mk.mk.mk.inr
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
h✝ : mk x ≤ mk y
z : FiniteElement K
h : mk x = mk y
⊢ mk x + mk z ≤ mk y + mk z
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: case inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 < mk x
hy : mk y < 0
⊢ mk (x + y) ≠ 0

Tactic:
rw [mk_add_eq_mk_right (hy.trans hx)]

Goal state after:
case inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 < mk x
hy : mk y < 0
⊢ mk y ≠ 0
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : mk x < 0
hr : ∀ {r : ℝ}, mk x < mk (f r)
h : x < 0
⊢ {r | x < f r} = Set.univ

Tactic:
rw [Set.eq_univ_iff_forall]

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : mk x < 0
hr : ∀ {r : ℝ}, mk x < mk (f r)
h : x < 0
⊢ ∀ (x_1 : ℝ), x_1 ∈ {r | x < f r}
Module: Mathlib.Algebra.Polynomial.CoeffMem

Goal state before:

Tactic:
span R coeffs(p)
        _ = 1 ^ deg(p) * span R coeffs(p) := by simp
        _ ≤ spanCoeffs(q) ^ deg(p) * spanCoeffs(p) := by gcongr; exacts [le_sup_left, le_sup_right]

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree n
⊢ p = X ^ n + p.eraseLead

pp: case refine_2
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree n
⊢ p.eraseLead.natDegree < n

Tactic:
· nth_rewrite 1 [← p.eraseLead_add_C_mul_X_pow]
    rw [add_comm, hp.natDegree_eq, hp.leadingCoeff_eq, map_one, one_mul]

Goal state after:
case refine_2
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree n
⊢ p.eraseLead.natDegree < n
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: case inr
R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
h₂ : q.Monic
this : (p * q).natDegree = m + n
h : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ q.natDegree = n

Tactic:
natDegree_mul' h,

Goal state after:
case inr
R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
h₂ : q.Monic
this : p.natDegree + q.natDegree = m + n
h : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ q.natDegree = n
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: case inr
R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hq : q.IsMonicOfDegree n
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
h₂ : p.Monic
this : (p * q).natDegree = m + n
h : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ p.natDegree = m

Tactic:
natDegree_mul' h,

Goal state after:
case inr
R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hq : q.IsMonicOfDegree n
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
h₂ : p.Monic
this : p.natDegree + q.natDegree = m + n
h : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ p.natDegree = m
Module: Mathlib.Algebra.Polynomial.DenomsClearable

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * (algebraMap ℤ K) b = 1
hF :
  (algebraMap ℤ K) ev =
    (algebraMap ℤ K) b ^ f.natDegree * eval ((algebraMap ℤ K) a * bi) (Polynomial.map (algebraMap ℤ K) f)
Fa :
  |(algebraMap ℤ K) ev| =
    |(algebraMap ℤ K) b ^ f.natDegree * eval ((algebraMap ℤ K) a * bi) (Polynomial.map (algebraMap ℤ K) f)|
⊢ 1 ≤ ↑b ^ f.natDegree * |eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f)|

Tactic:
rw [eq_one_div_of_mul_eq_one_left bu, eq_intCast, eq_intCast, abs_mul] at Fa

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * (algebraMap ℤ K) b = 1
hF :
  (algebraMap ℤ K) ev =
    (algebraMap ℤ K) b ^ f.natDegree * eval ((algebraMap ℤ K) a * bi) (Polynomial.map (algebraMap ℤ K) f)
Fa : |↑ev| = |↑b ^ f.natDegree| * |eval ((algebraMap ℤ K) a * (1 / ↑b)) (Polynomial.map (algebraMap ℤ K) f)|
⊢ 1 ≤ ↑b ^ f.natDegree * |eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f)|
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : MulActionWithZero R S
x : S
⊢ smeval 0 x = 0

Tactic:
simp only [smeval_eq_sum, sum_zero_index]

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
p q : R[X]
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
x : S
c : R
f : R[X]
⊢ (c • f).smeval x = (RingHom.id R) c • f.smeval x

Tactic:
simp only [smeval_smul, RingHom.id_apply]

Goal state after:
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
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
k : ℕ
hk : q ≤ k
⊢ ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)

Tactic:
c,

Goal state after:
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
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
k : ℕ
hk : q ≤ k
⊢ ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (if hk : q ≤ k then ⋯.choose else 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
⊢ ((X - C η) * P).eraseLead.signVariations = ((X - C η) * P.eraseLead).signVariations

Tactic:
by
  obtain ⟨d, hd⟩ := Nat.exists_eq_add_one.mpr (natDegree_pos_of_nextCoeff_ne_zero hc.ne)
  have hndxP : natDegree ((X - C η) * P) = P.natDegree + 1 := by
    have hPn0 : P ≠ 0 :=
      leadingCoeff_ne_zero.mp hP₀.ne'
    rw [natDegree_mul (X_sub_C_ne_zero η) hPn0, natDegree_X_sub_C, add_comm]
  have hndxeP : natDegree ((X - C η) * P.eraseLead) = P.natDegree := by
    have hePn0 : P.eraseLead ≠ 0 :=
      mt nextCoeff_eq_zero_of_eraseLead_eq_zero hc.ne
    rw [natDegree_mul (X_sub_C_ne_zero η) hePn0, natDegree_X_sub_C, add_comm]
    exact natDegree_eraseLead_add_one hc.ne
  have hQ : ((X - C η) * P).nextCoeff = coeff P d - η * coeff P (d + 1) := by
    grind [nextCoeff_of_natDegree_pos, coeff_X_sub_C_mul]
  have hQ₁ : ((X - C η) * P).nextCoeff < 0 := by
    rw [hQ, sub_neg]
    trans 0
    · grind [nextCoeff_of_natDegree_pos]
    · exact hd ▸ mul_pos hη hP₀
  have hndexP0 : natDegree (eraseLead ((X - C η) * P)) = P.natDegree := by
    apply Nat.add_right_cancel (m := 1)
    rw [← hndxP, natDegree_eraseLead_add_one hQ₁.ne]
  --the theorem is true mainly because all the signs are the same;
  --in fact, the coefficients are all the same except the first.
  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]
  rw [← self_sub_monomial_natDegree_leadingCoeff, leadingCoeff_eraseLead_eq_nextCoeff hQ₁.ne]
  rw [hndexP0, ← self_sub_monomial_natDegree_leadingCoeff, leadingCoeff_monic_mul (monic_X_sub_C η)]
  rw [← self_sub_monomial_natDegree_leadingCoeff, leadingCoeff_monic_mul (monic_X_sub_C η)]
  rw [hndxeP, hndxP]
  rw [leadingCoeff_eraseLead_eq_nextCoeff hc.ne, ← self_sub_monomial_natDegree_leadingCoeff]
  rw [hQ, mul_sub, sub_mul, sub_mul, X_mul_monomial, C_mul_monomial, monomial_sub]
  rw [leadingCoeff, nextCoeff_of_natDegree_pos (hd ▸ d.succ_pos), hd, Nat.add_sub_cancel]
  abel

Goal state after:
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
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ (q - 1) * p'
this : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
⊢ range q = range (q - 1 + 1)

Tactic:
tsub_add_cancel_of_le (Nat.one_le_of_lt hq)

Goal state after:
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
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ (q - 1) * p'
this : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
⊢ range q = range q
Module: Mathlib.Algebra.PresentedMonoid.Basic

Goal state before:
pp: α : Type u_2
M : Type u_3
inst✝ : Monoid M
rels : FreeMonoid α → FreeMonoid α → Prop
φ ψ : PresentedMonoid rels →* M
hx : ∀ (x : α), φ (of rels x) = ψ (of rels x)
⊢ EqOn (⇑φ) (⇑ψ) (range (of rels))

Tactic:
grind [Set.eqOn_range]

Goal state after:
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝³ : SMul S R
inst✝² : SMul T R
s✝ : S
inst✝¹ : SMul Sᵐᵒᵖ R
inst✝ : IsCentralScalar S R
s : S
z : QuadraticAlgebra R a b
⊢ MulOpposite.op s • z = s • z

Tactic:
by ext <;> exact op_smul_eq_smul _ _

Goal state after: