awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
t1 t2 : Monomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length t1.unit = List.length t2.unit
grw :
  (t1.coef * t2.coef) • (t1.unit.toFun basis * t2.unit.toFun basis) =ᶠ[atTop]
    t2.coef • t1.coef • (t1.unit.toFun basis * t2.unit.toFun basis)
⊢ (t1.coef * t2.coef) • (t1.unit.mul t2.unit).toFun basis =ᶠ[atTop]
    t2.coef • t1.coef • (t1.unit.toFun basis * t2.unit.toFun basis)

Tactic:
grw [UnitMonomial.mul_toFun h_basis h_length]

Premises used: Tactic.ComputeAsymptotics.UnitMonomial.mul_toFun
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
t1 t2 : Monomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length t1.unit = List.length t2.unit
h :
  ∀ (t : ℝ),
    ((t1.coef * t2.coef) • (t1.unit.toFun basis * t2.unit.toFun basis)) t =
      (t2.coef • t1.coef • (t1.unit.toFun basis * t2.unit.toFun basis)) t
⊢ (t1.coef * t2.coef) • (t1.unit.toFun basis * t2.unit.toFun basis) =ᶠ[atTop]
    t2.coef • t1.coef • (t1.unit.toFun basis * t2.unit.toFun basis)

Tactic:
filter_upwards [] with t
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
t1 t2 : Monomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length t1.unit = List.length t2.unit
t : ℝ
⊢ t1.coef * t2.coef * (t1.unit.toFun basis t * t2.unit.toFun basis t) =
    t2.coef * (t1.coef * (t1.unit.toFun basis t * t2.unit.toFun basis t))

Tactic:
ring
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
t : Monomial
basis : Basis
c : ℝ
h : ∀ (x : ℝ), (t.smul c).toFun basis x = (c • t.toFun basis) x
⊢ (t.smul c).toFun basis = c • t.toFun basis

Tactic:
ext x
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
t : Monomial
basis : Basis
c x : ℝ
h : c * t.coef * t.unit.toFun basis x = c * (t.coef * t.unit.toFun basis x)
⊢ (t.smul c).toFun basis x = (c • t.toFun basis) x

Tactic:
simp [smul, toFun]

Premises used: Tactic.ComputeAsymptotics.Monomial.toFun, Tactic.ComputeAsymptotics.Monomial.smul
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
t : Monomial
basis : Basis
c x : ℝ
⊢ c * t.coef * t.unit.toFun basis x = c * (t.coef * t.unit.toFun basis x)

Tactic:
ring
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
t : Monomial
basis : Basis
h_basis : WellFormedBasis basis
simp : t.coef⁻¹ • t.unit.inv.toFun basis =ᶠ[atTop] (t.coef • t.unit.toFun basis)⁻¹
⊢ t.inv.toFun basis =ᶠ[atTop] (t.toFun basis)⁻¹

Tactic:
simp only [toFun, inv]

Premises used: Tactic.ComputeAsymptotics.Monomial.toFun, Tactic.ComputeAsymptotics.Monomial.inv
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
t : Monomial
basis : Basis
h_basis : WellFormedBasis basis
grw : t.coef⁻¹ • (t.unit.toFun basis)⁻¹ =ᶠ[atTop] (t.coef • t.unit.toFun basis)⁻¹
⊢ t.coef⁻¹ • t.unit.inv.toFun basis =ᶠ[atTop] (t.coef • t.unit.toFun basis)⁻¹

Tactic:
grw [UnitMonomial.inv_toFun h_basis]

Premises used: Tactic.ComputeAsymptotics.UnitMonomial.inv_toFun
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
t : Monomial
basis : Basis
h_basis : WellFormedBasis basis
h : ∀ (x : ℝ), (t.coef⁻¹ • (t.unit.toFun basis)⁻¹) x = (t.coef • t.unit.toFun basis)⁻¹ x
⊢ t.coef⁻¹ • (t.unit.toFun basis)⁻¹ =ᶠ[atTop] (t.coef • t.unit.toFun basis)⁻¹

Tactic:
filter_upwards [] with x
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
t : Monomial
basis : Basis
h_basis : WellFormedBasis basis
x : ℝ
h : t.coef⁻¹ * (t.unit.toFun basis x)⁻¹ = (t.unit.toFun basis x)⁻¹ * t.coef⁻¹
⊢ (t.coef⁻¹ • (t.unit.toFun basis)⁻¹) x = (t.coef • t.unit.toFun basis)⁻¹ x

Tactic:
simp [Pi.smul_apply, Pi.inv_apply]

Premises used: Pi.inv_apply, Pi.smul_apply
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
t : Monomial
basis : Basis
h_basis : WellFormedBasis basis
x : ℝ
⊢ t.coef⁻¹ * (t.unit.toFun basis x)⁻¹ = (t.unit.toFun basis x)⁻¹ * t.coef⁻¹

Tactic:
ring
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
t : Monomial
⊢ List.length t.inv.unit = List.length t.unit

Tactic:
simp [inv]

Premises used: Tactic.ComputeAsymptotics.Monomial.inv
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Goal:
⊢ AllZero []

Tactic:
rfl

Premises used: Tactic.ComputeAsymptotics.UnitMonomial.AllZero, Tactic.ComputeAsymptotics.UnitMonomial.sign, rfl
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Goal:
hd : ℝ
tl : UnitMonomial
⊢ AllZero (hd :: tl) ↔ hd = 0 ∧ tl.AllZero

Tactic:
grind [AllZero, sign]

Premises used: Tactic.ComputeAsymptotics.UnitMonomial.AllZero, Tactic.ComputeAsymptotics.UnitMonomial.sign
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Goal:
hd : ℝ
tl : UnitMonomial
h_hd : hd = 0
h_tl : tl.AllZero
⊢ AllZero (hd :: tl)

Tactic:
cons_iff.mpr ⟨h_hd, h_tl⟩

Premises used: Iff.mpr, Tactic.ComputeAsymptotics.UnitMonomial.AllZero.cons_iff, And.intro
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Goal:
n : ℕ
zero : AllZero (List.replicate 0 0)
succ : ∀ (n : ℕ), AllZero (List.replicate n 0) → AllZero (List.replicate (n + 1) 0)
⊢ AllZero (List.replicate n 0)

Tactic:
induction n
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Goal:
⊢ AllZero (List.replicate 0 0)

Tactic:
grind [AllZero, sign]

Premises used: Tactic.ComputeAsymptotics.UnitMonomial.AllZero, Tactic.ComputeAsymptotics.UnitMonomial.sign
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Goal:
n : ℕ
h : AllZero (List.replicate n 0)
⊢ AllZero (List.replicate (n + 1) 0)

Tactic:
grind [AllZero, sign]

Premises used: Tactic.ComputeAsymptotics.UnitMonomial.AllZero, Tactic.ComputeAsymptotics.UnitMonomial.sign
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Goal:
li : UnitMonomial
h : li.AllZero
⊢ ¬li.FirstNonzeroIsPos

Tactic:
grind [AllZero, FirstNonzeroIsPos]

Premises used: Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsPos, Tactic.ComputeAsymptotics.UnitMonomial.AllZero
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Goal:
li : UnitMonomial
h : li.AllZero
⊢ ¬li.FirstNonzeroIsNeg

Tactic:
grind [AllZero, FirstNonzeroIsNeg]

Premises used: Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsNeg, Tactic.ComputeAsymptotics.UnitMonomial.AllZero
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Goal:
⊢ ¬FirstNonzeroIsPos []

Tactic:
simp [FirstNonzeroIsPos, sign]

Premises used: Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsPos, Tactic.ComputeAsymptotics.UnitMonomial.sign
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Goal:
hd : ℝ
tl : UnitMonomial
⊢ FirstNonzeroIsPos (hd :: tl) ↔ 0 < hd ∨ hd = 0 ∧ tl.FirstNonzeroIsPos

Tactic:
grind [FirstNonzeroIsPos, sign]

Premises used: Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsPos, Tactic.ComputeAsymptotics.UnitMonomial.sign
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Goal:
hd : ℝ
tl : UnitMonomial
h_hd : 0 < hd
⊢ FirstNonzeroIsPos (hd :: tl)

Tactic:
simp [h_hd]
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Goal:
hd : ℝ
tl : UnitMonomial
h_hd : hd = 0
h_tl : tl.FirstNonzeroIsPos
⊢ FirstNonzeroIsPos (hd :: tl)

Tactic:
simp [h_hd, h_tl]
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Goal:
li : UnitMonomial
h : li.FirstNonzeroIsPos
⊢ ¬li.AllZero

Tactic:
fun h' ↦ h'.not_FirstNonzeroIsPos h

Premises used: Tactic.ComputeAsymptotics.UnitMonomial.AllZero.not_FirstNonzeroIsPos, Not
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Goal:
li : UnitMonomial
h : li.FirstNonzeroIsPos
⊢ ¬li.FirstNonzeroIsNeg

Tactic:
grind [FirstNonzeroIsPos, FirstNonzeroIsNeg]

Premises used: Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsNeg, Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsPos
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Goal:
⊢ ¬FirstNonzeroIsNeg []

Tactic:
simp [FirstNonzeroIsNeg, sign]

Premises used: Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsNeg, Tactic.ComputeAsymptotics.UnitMonomial.sign
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Goal:
hd : ℝ
tl : UnitMonomial
⊢ FirstNonzeroIsNeg (hd :: tl) ↔ hd < 0 ∨ hd = 0 ∧ tl.FirstNonzeroIsNeg

Tactic:
grind [FirstNonzeroIsNeg, sign]

Premises used: Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsNeg, Tactic.ComputeAsymptotics.UnitMonomial.sign
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Goal:
hd : ℝ
tl : UnitMonomial
h_hd : hd < 0
⊢ FirstNonzeroIsNeg (hd :: tl)

Tactic:
simp [h_hd]
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Goal:
hd : ℝ
tl : UnitMonomial
h_hd : hd = 0
h_tl : tl.FirstNonzeroIsNeg
⊢ FirstNonzeroIsNeg (hd :: tl)

Tactic:
simp [h_hd, h_tl]
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Goal:
li : UnitMonomial
h : li.FirstNonzeroIsNeg
⊢ ¬li.AllZero

Tactic:
fun h' ↦ h'.not_FirstNonzeroIsNeg h

Premises used: Tactic.ComputeAsymptotics.UnitMonomial.AllZero.not_FirstNonzeroIsNeg, Not
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Goal:
li : UnitMonomial
h : li.FirstNonzeroIsNeg
⊢ ¬li.FirstNonzeroIsPos

Tactic:
fun h' ↦ h'.not_FirstNonzeroIsNeg h

Premises used: Not, Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsPos.not_FirstNonzeroIsNeg
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Semiring R
a : R
⊢ natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) a) ≤ 0

Tactic:
(natDegree_C a).le

Premises used: Polynomial.natDegree_C, Eq.le
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
⊢ natDegree.{u_1} (R := R) (↑n : R[X]) ≤ 0

Tactic:
(natDegree_natCast _).le

Premises used: Eq.le, Polynomial.natDegree_natCast
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Semiring R
⊢ natDegree.{u_1} (R := R) 0 ≤ 0

Tactic:
natDegree_zero.le

Premises used: Eq.le, Polynomial.natDegree_zero
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Semiring R
⊢ natDegree.{u_1} (R := R) 1 ≤ 0

Tactic:
natDegree_one.le

Premises used: Eq.le, Polynomial.natDegree_one
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a b : R
f g : R[X]
h_add_left : f.coeff n = a
h_add_right : g.coeff n = b
subst : (f + g).coeff n = f.coeff n + g.coeff n
⊢ (f + g).coeff n = a + b

Tactic:
subst ‹_› ‹_›
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
f g : R[X]
⊢ (f + g).coeff n = f.coeff n + g.coeff n

Tactic:
apply coeff_add

Premises used: Polynomial.coeff_add
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Semiring R
d df dg : ℕ
a b : R
f g : R[X]
h_mul_left_1 : f.natDegree ≤ df
h_mul_right_1 : g.natDegree ≤ dg
h_mul_left : f.coeff df = a
h_mul_right : g.coeff dg = b
ddf : df + dg ≤ d
pos : ∀ (h : d = df + dg), (f * g).coeff d = a * b
neg : ∀ (h : ¬d = df + dg), (f * g).coeff d = 0
⊢ (f * g).coeff d = if d = df + dg then a * b else 0

Tactic:
split_ifs with h
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Semiring R
d df dg : ℕ
a b : R
f g : R[X]
h_mul_left_1 : f.natDegree ≤ df
h_mul_right_1 : g.natDegree ≤ dg
h_mul_left : f.coeff df = a
h_mul_right : g.coeff dg = b
ddf : df + dg ≤ d
h : d = df + dg
pos : ∀ (ddf : df + dg ≤ df + dg), (f * g).coeff (df + dg) = f.coeff df * g.coeff dg
⊢ (f * g).coeff d = a * b

Tactic:
subst h_mul_left h_mul_right h
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Semiring R
df dg : ℕ
f g : R[X]
h_mul_left : f.natDegree ≤ df
h_mul_right : g.natDegree ≤ dg
ddf : df + dg ≤ df + dg
⊢ (f * g).coeff (df + dg) = f.coeff df * g.coeff dg

Tactic:
coeff_mul_add_eq_of_natDegree_le ‹_› ‹_›

Premises used: Polynomial.coeff_mul_add_eq_of_natDegree_le
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Semiring R
df dg : ℕ
f g : R[X]
h_mul_left : f.natDegree ≤ df
h_mul_right : g.natDegree ≤ dg
ddf : df + dg ≤ df + dg
⊢ (f * g).coeff (df + dg) = f.coeff df * g.coeff dg

Tactic:
exact coeff_mul_add_eq_of_natDegree_le ‹_› ‹_›

Premises used: Polynomial.coeff_mul_add_eq_of_natDegree_le
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Semiring R
d df dg : ℕ
a b : R
f g : R[X]
h_mul_left_1 : f.natDegree ≤ df
h_mul_right_1 : g.natDegree ≤ dg
h_mul_left : f.coeff df = a
h_mul_right : g.coeff dg = b
ddf : df + dg ≤ d
h : ¬d = df + dg
neg : (f * g).natDegree < d
⊢ (f * g).coeff d = 0

Tactic:
apply coeff_eq_zero_of_natDegree_lt

Premises used: Polynomial.coeff_eq_zero_of_natDegree_lt
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Semiring R
d df dg : ℕ
a b : R
f g : R[X]
h_mul_left_1 : f.natDegree ≤ df
h_mul_right_1 : g.natDegree ≤ dg
h_mul_left : f.coeff df = a
h_mul_right : g.coeff dg = b
ddf : df + dg ≤ d
h : ¬d = df + dg
apply : (f * g).natDegree ≤ df + dg
apply₁ : df + dg ≠ d
⊢ (f * g).natDegree < d

Tactic:
apply lt_of_le_of_lt ?_ (lt_of_le_of_ne ddf ?_)

Premises used: lt_of_le_of_lt, lt_of_le_of_ne
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Semiring R
d df dg : ℕ
a b : R
f g : R[X]
h_mul_left_1 : f.natDegree ≤ df
h_mul_right_1 : g.natDegree ≤ dg
h_mul_left : f.coeff df = a
h_mul_right : g.coeff dg = b
ddf : df + dg ≤ d
h : ¬d = df + dg
⊢ (f * g).natDegree ≤ df + dg

Tactic:
natDegree_mul_le_of_le ‹_› ‹_›

Premises used: Polynomial.natDegree_mul_le_of_le
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Semiring R
d df dg : ℕ
a b : R
f g : R[X]
h_mul_left_1 : f.natDegree ≤ df
h_mul_right_1 : g.natDegree ≤ dg
h_mul_left : f.coeff df = a
h_mul_right : g.coeff dg = b
ddf : df + dg ≤ d
h : ¬d = df + dg
⊢ (f * g).natDegree ≤ df + dg

Tactic:
exact natDegree_mul_le_of_le ‹_› ‹_›

Premises used: Polynomial.natDegree_mul_le_of_le
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Semiring R
d df dg : ℕ
a b : R
f g : R[X]
h_mul_left_1 : f.natDegree ≤ df
h_mul_right_1 : g.natDegree ≤ dg
h_mul_left : f.coeff df = a
h_mul_right : g.coeff dg = b
ddf : df + dg ≤ d
h : ¬d = df + dg
⊢ df + dg ≠ d

Tactic:
ne_comm.mp h

Premises used: Iff.mp, ne_comm
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Semiring R
d df dg : ℕ
a b : R
f g : R[X]
h_mul_left_1 : f.natDegree ≤ df
h_mul_right_1 : g.natDegree ≤ dg
h_mul_left : f.coeff df = a
h_mul_right : g.coeff dg = b
ddf : df + dg ≤ d
h : ¬d = df + dg
⊢ df + dg ≠ d

Tactic:
exact ne_comm.mp h

Premises used: Iff.mp, ne_comm
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Semiring R
m n o : ℕ
a : R
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ o
h_pow_bas : p.coeff n = a
pos : ∀ (h : o = m * n), (p ^ m).coeff o = a ^ m
neg : ∀ (h : ¬o = m * n), (p ^ m).coeff o = 0
⊢ (p ^ m).coeff o = if o = m * n then a ^ m else 0

Tactic:
split_ifs with h
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Semiring R
m n o : ℕ
a : R
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ o
h_pow_bas : p.coeff n = a
h : o = m * n
pos : ∀ (h_exp : m * n ≤ m * n), (p ^ m).coeff (m * n) = p.coeff n ^ m
⊢ (p ^ m).coeff o = a ^ m

Tactic:
subst h h_pow_bas
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ m * n
⊢ (p ^ m).coeff (m * n) = p.coeff n ^ m

Tactic:
coeff_pow_of_natDegree_le ‹_›

Premises used: Polynomial.coeff_pow_of_natDegree_le
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ m * n
⊢ (p ^ m).coeff (m * n) = p.coeff n ^ m

Tactic:
exact coeff_pow_of_natDegree_le ‹_›

Premises used: Polynomial.coeff_pow_of_natDegree_le
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Semiring R
m n o : ℕ
a : R
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ o
h_pow_bas : p.coeff n = a
h : ¬o = m * n
neg : (p ^ m).natDegree < o
⊢ (p ^ m).coeff o = 0

Tactic:
apply coeff_eq_zero_of_natDegree_lt

Premises used: Polynomial.coeff_eq_zero_of_natDegree_lt
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Semiring R
m n o : ℕ
a : R
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ o
h_pow_bas : p.coeff n = a
h : ¬o = m * n
apply : (p ^ m).natDegree ≤ m * n
apply₁ : m * n ≠ o
⊢ (p ^ m).natDegree < o

Tactic:
apply lt_of_le_of_lt ?_ (lt_of_le_of_ne ‹_› ?_)

Premises used: lt_of_le_of_lt, lt_of_le_of_ne
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Semiring R
m n o : ℕ
a : R
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ o
h_pow_bas : p.coeff n = a
h : ¬o = m * n
⊢ (p ^ m).natDegree ≤ m * n

Tactic:
natDegree_pow_le_of_le m ‹_›

Premises used: Polynomial.natDegree_pow_le_of_le
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Semiring R
m n o : ℕ
a : R
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ o
h_pow_bas : p.coeff n = a
h : ¬o = m * n
⊢ (p ^ m).natDegree ≤ m * n

Tactic:
exact natDegree_pow_le_of_le m ‹_›

Premises used: Polynomial.natDegree_pow_le_of_le
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Semiring R
m n o : ℕ
a : R
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ o
h_pow_bas : p.coeff n = a
h : ¬o = m * n
⊢ m * n ≠ o

Tactic:
Iff.mp ne_comm h

Premises used: Iff.mp, ne_comm
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Semiring R
m n o : ℕ
a : R
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ o
h_pow_bas : p.coeff n = a
h : ¬o = m * n
⊢ m * n ≠ o

Tactic:
exact Iff.mp ne_comm h

Premises used: Iff.mp, ne_comm
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : SMulZeroClass S R
n : ℕ
a : S
f : R[X]
hf : f.natDegree ≤ n
⊢ (a • f).natDegree ≤ n

Tactic:
(natDegree_smul_le a f).trans hf

Premises used: Polynomial.natDegree_smul_le, LE.le.trans
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : SMulZeroClass S R
n : ℕ
a : S
f : R[X]
hf : f.degree ≤ (↑n : WithBot ℕ)
⊢ (a • f).degree ≤ (↑n : WithBot ℕ)

Tactic:
(degree_smul_le a f).trans hf

Premises used: Polynomial.degree_smul_le, LE.le.trans
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : SMulZeroClass S R
n : ℕ
a : S
f : R[X]
⊢ (a • f).coeff n = a • f.coeff n

Tactic:
rfl

Premises used: Polynomial.coeff, rfl
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Semiring R
deg m o : ℕ
c : R
p : R[X]
h_natDeg_le : p.natDegree ≤ m
coeff_eq : p.coeff o = c
coeff_ne_zero : c ≠ 0
deg_eq_deg : m = deg
coeff_eq_deg : o = deg
subst : ∀ (coeff_ne_zero : p.coeff o ≠ 0) (h_natDeg_le : p.natDegree ≤ o), p.natDegree = o
⊢ p.natDegree = deg

Tactic:
subst coeff_eq deg_eq_deg coeff_eq_deg
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Semiring R
o : ℕ
p : R[X]
coeff_ne_zero : p.coeff o ≠ 0
h_natDeg_le : p.natDegree ≤ o
⊢ p.natDegree = o

Tactic:
natDegree_eq_of_le_of_coeff_ne_zero ‹_› ‹_›

Premises used: Polynomial.natDegree_eq_of_le_of_coeff_ne_zero
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Semiring R
o : ℕ
p : R[X]
coeff_ne_zero : p.coeff o ≠ 0
h_natDeg_le : p.natDegree ≤ o
⊢ p.natDegree = o

Tactic:
exact natDegree_eq_of_le_of_coeff_ne_zero ‹_› ‹_›

Premises used: Polynomial.natDegree_eq_of_le_of_coeff_ne_zero
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Semiring R
deg m o : WithBot ℕ
c : R
p : R[X]
h_deg_le : p.degree ≤ m
coeff_eq : p.coeff (WithBot.unbotD 0 deg) = c
coeff_ne_zero : c ≠ 0
deg_eq_deg : m = deg
coeff_eq_deg : o = deg
subst : ∀ (coeff_ne_zero : p.coeff (WithBot.unbotD 0 m) ≠ 0), p.degree = m
⊢ p.degree = deg

Tactic:
subst coeff_eq coeff_eq_deg deg_eq_deg
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Semiring R
m : WithBot ℕ
p : R[X]
h_deg_le : p.degree ≤ m
coeff_ne_zero : p.coeff (WithBot.unbotD 0 m) ≠ 0
inl : ∀ (h_deg_le : p.degree ≤ ⊥) (coeff_ne_zero : p.coeff (WithBot.unbotD 0 ⊥) ≠ 0), p.degree = ⊥
inr : ∀ (hh : m ≠ ⊥), p.degree = m
⊢ p.degree = m

Tactic:
rcases eq_or_ne m ⊥ with rfl | hh

Premises used: Bot.bot, eq_or_ne, rfl
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
h_deg_le : p.degree ≤ ⊥
coeff_ne_zero : p.coeff (WithBot.unbotD 0 ⊥) ≠ 0
⊢ p.degree = ⊥

Tactic:
bot_unique h_deg_le

Premises used: bot_unique
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
h_deg_le : p.degree ≤ ⊥
coeff_ne_zero : p.coeff (WithBot.unbotD 0 ⊥) ≠ 0
⊢ p.degree = ⊥

Tactic:
exact bot_unique h_deg_le

Premises used: bot_unique
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Semiring R
m : WithBot ℕ
p : R[X]
h_deg_le : p.degree ≤ m
coeff_ne_zero : p.coeff (WithBot.unbotD 0 m) ≠ 0
hh : m ≠ ⊥
inr :
  ∀ (m : ℕ) (h_deg_le : p.degree ≤ (↑m : WithBot ℕ)) (coeff_ne_zero : p.coeff (WithBot.unbotD 0 (↑m : WithBot ℕ)) ≠ 0)
    (hh : (↑m : WithBot ℕ) ≠ ⊥), p.degree = (↑m : WithBot ℕ)
⊢ p.degree = m

Tactic:
obtain ⟨m, rfl⟩ := WithBot.ne_bot_iff_exists.mp hh

Premises used: WithBot.ne_bot_iff_exists, Iff.mp, rfl
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
m : ℕ
h_deg_le : p.degree ≤ (↑m : WithBot ℕ)
coeff_ne_zero : p.coeff (WithBot.unbotD 0 (↑m : WithBot ℕ)) ≠ 0
hh : (↑m : WithBot ℕ) ≠ ⊥
⊢ p.degree = (↑m : WithBot ℕ)

Tactic:
degree_eq_of_le_of_coeff_ne_zero ‹_› ‹_›

Premises used: Polynomial.degree_eq_of_le_of_coeff_ne_zero
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
m : ℕ
h_deg_le : p.degree ≤ (↑m : WithBot ℕ)
coeff_ne_zero : p.coeff (WithBot.unbotD 0 (↑m : WithBot ℕ)) ≠ 0
hh : (↑m : WithBot ℕ) ≠ ⊥
⊢ p.degree = (↑m : WithBot ℕ)

Tactic:
exact degree_eq_of_le_of_coeff_ne_zero ‹_› ‹_›

Premises used: Polynomial.degree_eq_of_le_of_coeff_ne_zero
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
f : R[X]
r : R
h : f.coeff m = r
natDeg_eq_coeff : m = n
⊢ f.coeff n = r

Tactic:
natDeg_eq_coeff ▸ h

Premises used: Eq.rec
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
f : R[X]
r : R
h : f.coeff m = r
natDeg_eq_coeff : m = n
s : R
rs : r = s
⊢ f.coeff n = s

Tactic:
natDeg_eq_coeff ▸ rs ▸ h

Premises used: Eq.rec
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Ring R
n : ℤ
⊢ natDegree.{u_1} (R := R) (↑n : R[X]) ≤ 0

Tactic:
(natDegree_intCast _).le

Premises used: Eq.le, Polynomial.natDegree_intCast
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Ring R
n : ℕ
a b : R
f g : R[X]
hf : f.coeff n = a
hg : g.coeff n = b
subst : (f - g).coeff n = f.coeff n - g.coeff n
⊢ (f - g).coeff n = a - b

Tactic:
subst hf hg
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Ring R
n : ℕ
f g : R[X]
⊢ (f - g).coeff n = f.coeff n - g.coeff n

Tactic:
apply coeff_sub

Premises used: Polynomial.coeff_sub
-- Module: Mathlib.Tactic.ComputeDegree
Goal:
R : Type u_1
inst : Ring R
n : ℕ
a : ℤ
⊢ Eq.{u_1 + 1} (α := R) (coeff (↑a : R[X]) n) (↑(if n = 0 then a else 0) : R)

Tactic:
simp only [← C_eq_intCast, coeff_C, Int.cast_ite, Int.cast_zero]

Premises used: Int.cast_zero, Polynomial.C_eq_intCast, Polynomial.coeff_C, Int.cast_ite
-- Module: Mathlib.Tactic.CongrExclamation
Goal:
α α' : Sort u
β β' : Sort v
h : α = α'
h' : ∀ (a : α'), β = β'
refl : ∀ (h' : ∀ (a : α), β = β'), Eq (α := Sort (imax u v)) (α → β) (α → β')
⊢ Eq (α := Sort (imax u v)) (α → β) (α' → β')

Tactic:
cases h
-- Module: Mathlib.Tactic.CongrExclamation
Goal:
α : Sort u
β β' : Sort v
h' : ∀ (a : α), β = β'
refl : Eq (α := Sort (imax u v)) ((x : α) → (fun (x : α) ↦ β) x) (α → β')
⊢ Eq (α := Sort (imax u v)) (α → β) (α → β')

Tactic:
change (∀ (x : α), (fun _ => β) x) = _
-- Module: Mathlib.Tactic.CongrExclamation
Goal:
α : Sort u
β β' : Sort v
h' : ∀ (a : α), β = β'
refl refl₁ : Eq (α := Sort (imax u v)) ((x : α) → (fun (x : α) ↦ β') x) (α → β')
⊢ Eq (α := Sort (imax u v)) ((x : α) → (fun (x : α) ↦ β) x) (α → β')

Tactic:
rw [funext h']

Premises used: funext
-- Module: Mathlib.Tactic.CongrExclamation
Goal:
α : Sort u_1
x y : α
p : x ≍ y → Prop
h : ∀ (he : x = y), p ⋯
he : x ≍ y
refl : ∀ {p : x ≍ x → Prop} (h : ∀ (he : x = x), p ⋯), p ⋯
⊢ p he

Tactic:
cases he