mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: case hi
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ¬a1 * a2 = 0
cop : (a1 * a2).Coprime (b1 * b2)
hb : ¬b1 * b2 = 0
⊢ (match ((a1, a2), b1, b2) with
    | ((i, j), k, l) => (i * k, j * l)) ∈
    (a1 * a2 * (b1 * b2)).divisorsAntidiagonal

Tactic:
simp only [mem_divisorsAntidiagonal, mul_eq_zero, Ne]

Goal state after:
case hi
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ¬a1 * a2 = 0
cop : (a1 * a2).Coprime (b1 * b2)
hb : ¬b1 * b2 = 0
⊢ a1 * b1 * (a2 * b2) = a1 * a2 * (b1 * b2) ∧ ¬((a1 = 0 ∨ a2 = 0) ∨ b1 = 0 ∨ b2 = 0)
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: R : Type u_2
inst✝ : Semiring R
f g : ArithmeticFunction R
N n : ℕ
hn : 0 < n ∧ n ≤ N
⊢ ∑ x ∈ n.divisorsAntidiagonal, f x.1 * g x.2 = ∑ x ∈ Ioc 0 N ×ˢ Ioc 0 N with x.1 * x.2 = n, f x.1 * g x.2

Tactic:
divisorsAntidiagonal_eq_prod_filter_of_le hn.1.ne' hn.2

Goal state after:
R : Type u_2
inst✝ : Semiring R
f g : ArithmeticFunction R
N n : ℕ
hn : 0 < n ∧ n ≤ N
⊢ ∑ x ∈ Ioc 0 N ×ˢ Ioc 0 N with x.1 * x.2 = n, f x.1 * g x.2 =
    ∑ x ∈ Ioc 0 N ×ˢ Ioc 0 N with x.1 * x.2 = n, f x.1 * g x.2
Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard

Goal state before:
pp: case mp
R : Type u_1
inst✝⁴ : AddCommMonoid R
inst✝³ : PartialOrder R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
h_mono : Monotone fun n ↦ ∑ k ∈ Finset.range n, s.indicator (fun x ↦ r) k
⊢ s.Infinite → ∀ (b : R), ∃ a, b ≤ ∑ k ∈ Finset.range a, s.indicator (fun x ↦ r) k

Tactic:
intro hs

Goal state after:
case mp
R : Type u_1
inst✝⁴ : AddCommMonoid R
inst✝³ : PartialOrder R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
h_mono : Monotone fun n ↦ ∑ k ∈ Finset.range n, s.indicator (fun x ↦ r) k
hs : s.Infinite
⊢ ∀ (b : R), ∃ a, b ≤ ∑ k ∈ Finset.range a, s.indicator (fun x ↦ r) k
Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard

Goal state before:
pp: case mpr
R : Type u_1
inst✝⁴ : AddCommMonoid R
inst✝³ : PartialOrder R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
⊢ s.Finite → ¬Tendsto (fun n ↦ ∑ k ∈ Finset.range n, s.indicator (fun x ↦ r) k) atTop atTop

Tactic:
intro hs

Goal state after:
case mpr
R : Type u_1
inst✝⁴ : AddCommMonoid R
inst✝³ : PartialOrder R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
hs : s.Finite
⊢ ¬Tendsto (fun n ↦ ∑ k ∈ Finset.range n, s.indicator (fun x ↦ r) k) atTop atTop
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
ι : Type u_3
m : MonomialOrder ι
i : ι
r : R
⊢ m.degree (X i - C r) = single i 1

Tactic:
by
  rw [sub_eq_add_neg, ← map_neg, degree_X_add_C]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : Semiring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
s : Finset ι
f g : ι → α
hfg : AntivaryOn f g ↑s
⊢ ↑(#s) * ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i) * ∑ i ∈ s, g i

Tactic:
by
  rw [← nsmul_eq_mul]
  exact hfg.card_smul_sum_le_sum_smul_sum

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

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a b : M
⊢ min (mk a) (mk b) ≤ mk (a * b)

Tactic:
by_contra! h
  rw [lt_min_iff] at h
  have h1 := (mk_lt_mk.mp h.1 2).trans_le (mabs_mul_le _ _)
  have h2 := (mk_lt_mk.mp h.2 2).trans_le (mabs_mul_le _ _)
  simp only [mul_lt_mul_iff_left, mul_lt_mul_iff_right, pow_two] at h1 h2
  exact h1.not_gt h2

Goal state after:
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - ↑(#s)) c
⊢ #s = #r

Tactic:
Int.card_Ioc,

Goal state after:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - ↑(#s)) c
⊢ #s = (c - (c - ↑(#s))).toNat
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
r : Finset ℤ := Ico c (c + ↑(#s))
⊢ #r = #s

Tactic:
Int.card_Ico,

Goal state after:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
r : Finset ℤ := Ico c (c + ↑(#s))
⊢ (c + ↑(#s) - c).toNat = #s
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Sub α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
a b : α
⊢ Ioo (a - 1) b = Ico a b

Tactic:
by
  simpa [pred_eq_sub_one] using Ioo_pred_left_eq_Ioc a b

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Basic

Goal state before:
pp: case coe.coe
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a✝¹ a✝ : NonemptyInterval α
⊢ ↑a✝¹ * ↑a✝ = 1 ↔ ∃ a b, ↑a✝¹ = pure a ∧ ↑a✝ = pure b ∧ a * b = 1

Tactic:
simp_rw [← NonemptyInterval.coe_mul_interval, ← NonemptyInterval.coe_one_interval,
      Interval.coe_inj, NonemptyInterval.coe_eq_pure]
    exact NonemptyInterval.mul_eq_one_iff

Goal state after:
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
s₁ : Set (Interval α)
s : NonemptyInterval α
ha : ↑s ∈ lowerBounds s₁
h : ¬(⊥ ∉ s₁ ∧ ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ s₁ → s.toProd.1 ≤ t.toProd.2)
⊢ ↑s ≤ ⊥

Tactic:
· rw [not_and_or, not_not] at h
          rcases h with h | h
          · exact ha h
          · cases h fun b hb c hc ↦ (WithBot.coe_le_coe.1 <| ha hb).1.trans
              (s.fst_le_snd.trans (WithBot.coe_le_coe.1 <| ha hc).2)

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : R⟦Γ⟧
hx : 0 < x.order
⊢ 0 < x.orderTop

Tactic:
by_cases h : x = 0

Goal state after:
case pos
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : R⟦Γ⟧
hx : 0 < x.order
h : x = 0
⊢ 0 < x.orderTop

case neg
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : R⟦Γ⟧
hx : 0 < x.order
h : ¬x = 0
⊢ 0 < x.orderTop
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : R⟦Γ⟧
⊢ 0 ≤ x.orderTop ↔ 0 ≤ x.order

Tactic:
by_cases h : x = 0

Goal state after:
case pos
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : R⟦Γ⟧
h : x = 0
⊢ 0 ≤ x.orderTop ↔ 0 ≤ x.order

case neg
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : R⟦Γ⟧
h : ¬x = 0
⊢ 0 ≤ x.orderTop ↔ 0 ≤ x.order
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : R⟦Γ⟧
⊢ x.leadingCoeff = x.coeff x.order

Tactic:
by_cases h : x = 0

Goal state after:
case pos
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : R⟦Γ⟧
h : x = 0
⊢ x.leadingCoeff = x.coeff x.order

case neg
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : R⟦Γ⟧
h : ¬x = 0
⊢ x.leadingCoeff = x.coeff x.order
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddGroup R
x y : R⟦Γ⟧
g : Γ
hxg : x.orderTop = ↑g
hyg : y.orderTop = ↑g
hxyc : x.leadingCoeff = y.leadingCoeff
⊢ (x - y).orderTop ≠ ↑g

Tactic:
refine orderTop_ne_of_coeff_eq_zero ?_

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddGroup R
x y : R⟦Γ⟧
g : Γ
hxg : x.orderTop = ↑g
hyg : y.orderTop = ↑g
hxyc : x.leadingCoeff = y.leadingCoeff
⊢ (x - y).coeff g = 0
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddGroup R
x y : R⟦Γ⟧
g : Γ
hxg : x.orderTop = ↑g
hyg : y.orderTop = ↑g
hxyc : x.leadingCoeff = y.leadingCoeff
hx : x ≠ 0
⊢ (x - y).coeff g = 0

Tactic:
rw [orderTop_of_ne_zero hx, WithTop.coe_eq_coe] at hxg

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddGroup R
x y : R⟦Γ⟧
g : Γ
hyg : y.orderTop = ↑g
hxyc : x.leadingCoeff = y.leadingCoeff
hx : x ≠ 0
hxg : ⋯.min ⋯ = g
⊢ (x - y).coeff g = 0
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝⁵ : LinearOrder Γ
inst✝⁴ : LinearOrder R
inst✝³ : AddCommGroup R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : Archimedean R
inst✝ : Nontrivial R
x : Lex R⟦Γ⟧
h : x ≠ 0
⊢ ↑((finiteArchimedeanClassOrderIso Γ R) (FiniteArchimedeanClass.mk x h)) = (ofLex x).orderTop

Tactic:
simp [finiteArchimedeanClassOrderIso]

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

Goal state before:
pp: case pos
R : Type u_3
V : Type u_5
inst✝⁷ : AddCommMonoid V
Γ : Type u_6
Γ' : Type u_7
inst✝⁶ : LinearOrder Γ
inst✝⁵ : LinearOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : MulZeroClass R
inst✝¹ : SMulWithZero R V
x : R⟦Γ⟧
inst✝ : VAdd (WithTop Γ) (WithTop Γ')
y : HahnModule Γ' R V
h : ∀ (γ : Γ) (γ' : Γ'), ↑(γ +ᵥ γ') = ↑γ +ᵥ ↑γ'
hx : ¬x = 0
hy : ¬y = 0
hhy : (of R).symm y ≠ 0
hxy : (of R).symm (x • y) = 0
⊢ ↑(⋯.min ⋯) ≤ ⊤

Tactic:
exact OrderTop.le_top (α := WithTop Γ') _

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

Goal state before:
pp: S : Type u_3
inst✝³ : LinearOrder S
inst✝² : CommRing S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Archimedean S
x : ArchimedeanClass S
⊢ x = 0 ∨ x = ⊤

Tactic:
induction x with | mk x
  obtain rfl | h := eq_or_ne x 0 <;> simp_all

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

Goal state before:
pp: case mpr
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
h : 0 ≤ f (n • q)
⊢ f q * |ArchimedeanOrder.val (ArchimedeanOrder.of y)| ≤ f q * n • |ArchimedeanOrder.val (ArchimedeanOrder.of x)|

Tactic:
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.Order.Quotient

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
s : Setoid α
inst✝ : Preorder β
f : α → β
hf : Monotone f
H : ∀ (x₁ x₂ : α), x₁ ≈ x₂ → f x₁ = f x₂
⊢ Monotone (Quotient.lift f H)

Tactic:
by
  intro x y h
  induction x using Quotient.inductionOn with | h x
  induction y using Quotient.inductionOn with | h y
  induction h
  on_goal 2 => rename_i IH; apply IH.trans
  all_goals
    rename_i h
    cases h with
    | inl h => exact hf h
    | inr h => exact (H _ _ h).le

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

Goal state before:
pp: case mpr
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
⊢ x ∈ S → x ∈ R.ofPrime (R.idealOfLE S h)

Tactic:
intro hx; by_cases hr : x ∈ R; · exact R.le_ofPrime _ hr
    have : x ≠ 0 := fun h => hr (by rw [h]; exact R.zero_mem)
    replace hr := (R.mem_or_inv_mem x).resolve_left hr
    refine ⟨1, ⟨x⁻¹, hr⟩, ?_, ?_⟩
    · 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]
      change IsUnit (⟨x⁻¹, h hr⟩ : S)
      refine .of_mul_eq_one (⟨x, hx⟩ : S) ?_
      ext
      simp [field]
    · simp

Goal state after:
Module: Mathlib.Algebra.Order.Star.Real

Goal state before:
pp: case refine_1
x y : ℝ≥0
h : x ≤ y
⊢ ∃ s, y = x + star s * s

Tactic:
obtain ⟨d, rfl⟩ := exists_add_of_le h

Goal state after:
case refine_1
x d : ℝ≥0
h : x ≤ x + d
⊢ ∃ s, x + d = x + star s * s
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
⊢ ∀ {a b : Kˣ},
    a ∈ {x | A.valuation (↑x - 1) < 1} → b ∈ {x | A.valuation (↑x - 1) < 1} → a * b ∈ {x | A.valuation (↑x - 1) < 1}

Tactic:
intro a b ha hb

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : Kˣ
ha : a ∈ {x | A.valuation (↑x - 1) < 1}
hb : b ∈ {x | A.valuation (↑x - 1) < 1}
⊢ a * b ∈ {x | A.valuation (↑x - 1) < 1}
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case a
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
y : ↥(↑f).domain
h : x < ↑y
hxy0 : ↑y - x ≠ 0
z : ↥(↑f).domain
hz : ↑z - x ∈ ball K (FiniteArchimedeanClass.mk (↑y - x) ⋯)
this : ↑z ≠ x
hzyne : ↑z - ↑y ≠ 0
hzyclass : FiniteArchimedeanClass.mk (↑y - x) hxy0 = FiniteArchimedeanClass.mk (↑z - ↑y) hzyne
i : FiniteArchimedeanClass M
hj : ∀ j < i, (ofLex (↑↑f z)).coeff j = (ofLex (↑↑f y)).coeff j
hi : (ofLex (↑↑f z)).coeff i < (ofLex (↑↑f y)).coeff i
⊢ FiniteArchimedeanClass.mk (↑y - x) hxy0 ≤ i

Tactic:
contrapose! hi
      rw [hzyclass] at hi
      have hzy : z.val - y.val ∈ ball K i := fun _ ↦ hi
      exact (f.coeff_eq_of_mem y.val (by simp) hzy (by simp)).le

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✝ : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : ¬r = 0
i : ℕ
⊢ (p.coeff i - if deg(p) - deg(q) ≤ i then q.coeff (i - (deg(p) - deg(q))) * p.leadingCoeff else 0) ∈
    ↑(span R coeffs(p) ⊔ span R coeffs(q) * span R coeffs(p))

Tactic:
apply sub_mem

Goal state after:
case hx
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✝ : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : ¬r = 0
i : ℕ
⊢ p.coeff i ∈ span R coeffs(p) ⊔ span R coeffs(q) * span R coeffs(p)

case hy
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✝ : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : ¬r = 0
i : ℕ
⊢ (if deg(p) - deg(q) ≤ i then q.coeff (i - (deg(p) - deg(q))) * p.leadingCoeff else 0) ∈
    span R coeffs(p) ⊔ span R coeffs(q) * span R coeffs(p)
Module: Mathlib.Algebra.Polynomial.CoeffMem

Goal state before:
pp: case h₂
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 : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : ¬r = 0
H : span R coeffs(r) ≤ span R coeffs(p) ⊔ span R coeffs(q) * span R coeffs(p)
deg_r_lt_deg_p : deg(r) < deg(p)
⊢ 1 ⊔ (span R coeffs(p) ⊔ span R coeffs(q) * span R coeffs(p)) ≤ spanCoeffs(q) * spanCoeffs(p)

Tactic:
simp only [sup_le_iff]

Goal state after:
case h₂
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 : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : ¬r = 0
H : span R coeffs(r) ≤ span R coeffs(p) ⊔ span R coeffs(q) * span R coeffs(p)
deg_r_lt_deg_p : deg(r) < deg(p)
⊢ 1 ≤ spanCoeffs(q) * spanCoeffs(p) ∧
    span R coeffs(p) ≤ spanCoeffs(q) * spanCoeffs(p) ∧
      span R coeffs(q) * span R coeffs(p) ≤ spanCoeffs(q) * spanCoeffs(p)
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

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

Tactic:
exact hq.add_right hp

Goal state after:
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 : |↑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)|

Tactic:
rw [abs_of_pos (pow_pos (Int.cast_pos.mpr b0) _ : 0 < (b : K) ^ _), one_div, eq_intCast] 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 (↑a * (↑b)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
⊢ 1 ≤ ↑b ^ f.natDegree * |eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f)|
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
ha : a = 0
⊢ ((monomial n) a).mirror = (monomial n) a

Tactic:
ha,

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
ha : a = 0
⊢ ((monomial n) 0).mirror = (monomial n) 0
Module: Mathlib.Algebra.Polynomial.PartialFractions

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

Tactic:
cases i using Fin.lastCases with
      | cast i => simpa using hr i
      | last => simpa using degree_modByMonic_lt q hg

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

Goal state before:
pp: K : Type u_1
inst✝ : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ (p.coeff k * ((fun₀ | 0 => k) + fun₀ | 1 => n - k).prod fun n e ↦ x n ^ e) = p.coeff k * (x 0 / x 1) ^ k * x 1 ^ n

pp: case h
K : Type u_1
inst✝ : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ (fun₀ | 0 => k) 1 = 0

Tactic:
Finsupp.prod_add_index',

Goal state after:
K : Type u_1
inst✝ : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ p.coeff k * (((fun₀ | 0 => k).prod fun n e ↦ x n ^ e) * (fun₀ | 1 => n - k).prod fun n e ↦ x n ^ e) =
    p.coeff k * (x 0 / x 1) ^ k * x 1 ^ n

case h_zero
K : Type u_1
inst✝ : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ ∀ (a : Fin 2), x a ^ 0 = 1

case h_add
K : Type u_1
inst✝ : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ ∀ (a : Fin 2) (b₁ b₂ : ℕ), x a ^ (b₁ + b₂) = x a ^ b₁ * x a ^ b₂

case h
K : Type u_1
inst✝ : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ (fun₀ | 0 => k) 1 = 0
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : Std.Antisymm r
x y : α
xs : List α
h : Pairwise r (x :: y :: xs)
⊢ destutter (fun x1 x2 ↦ x1 ≠ x2) (x :: y :: xs) = (x :: y :: xs).dedup

Tactic:
rw [pairwise_cons] at h
    rw [destutter_cons_cons, ← destutter_cons', ← destutter_cons', h.2.destutter_eq_dedup]
    obtain rfl | hxy := eq_or_ne x y
    · simpa using h.2.destutter_eq_dedup
    · simp only [mem_cons, forall_eq_or_imp, pairwise_cons] at h
      have : x ∉ xs := fun hx ↦ hxy (antisymm h.1.1 (h.2.1 x hx))
      rw [if_pos hxy, dedup_cons_of_notMem (a := x) (by simp [*])]

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

Goal state before:
pp: 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]
rs₁ : Fin n → R[X]
r₁ : R[X]
hr₁ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₁ r₁ i).degree < g.degree
rs₂ : Fin n → R[X]
r₂ : R[X]
hr₂ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₂ r₂ i).degree < g.degree
hf : (r₁ + g * q₁) * g ^ n + ∑ x, rs₁ x * g ^ ↑x = (r₂ + g * q₂) * g ^ n + ∑ x, rs₂ x * g ^ ↑x
hqr : r₁ + g * q₁ = r₂ + g * q₂
hrs : rs₁ = rs₂
hq₁ : (r₁ + g * q₁) /ₘ g = q₁
hrr₁ : (r₁ + g * q₁) %ₘ g = r₁
⊢ r₂.degree < g.degree

Tactic:
simpa using hr₂ (Fin.last n)

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
⊢ Irreducible p ↔ p.roots = 0

Tactic:
have hp0 : p ≠ 0 := hp.ne_zero

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
⊢ Irreducible p ↔ p.roots = 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)
⊢ P.coeff d < 0

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)
⊢ 0 < η * P.coeff (d + 1)

Tactic:
· grind [nextCoeff_of_natDegree_pos]

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)
⊢ 0 < η * P.coeff (d + 1)
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
d : ℕ
c : R
hc : c ≠ 0
hη : 0 < η
h₁ : ((X - C η) * (monomial d) c).nextCoeff = -(η * c)
⊢ ((X - C η) * (monomial d) c).eraseLead ≠ 0

Tactic:
apply mt nextCoeff_eq_zero_of_eraseLead_eq_zero

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
d : ℕ
c : R
hc : c ≠ 0
hη : 0 < η
h₁ : ((X - C η) * (monomial d) c).nextCoeff = -(η * c)
⊢ ¬((X - C η) * (monomial d) c).nextCoeff = 0