awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
x y : R
this :
  ∀ (t : R),
    eval t ((taylor x : (a : R[X]) → R[X]) p) =
      ∑ i ∈ Finset.range (natDegree.{u_1} (R := R) ((taylor x : (a : R[X]) → R[X]) p) + 2),
        coeff ((taylor x : (a : R[X]) → R[X]) p) i * t ^ i
⊢ (∑ i ∈ Finset.range p.natDegree, coeff ((taylor x : (a : R[X]) → R[X]) p) (i + 2) * y ^ i) * HPow.hPow (β := ℕ) y 2 +
        eval x ((derivative : (a : R[X]) → R[X]) p) * y +
      eval x p =
    ∑ k ∈ Finset.range (natDegree.{u_1} (R := R) ((taylor x : (a : R[X]) → R[X]) p)),
          coeff ((taylor x : (a : R[X]) → R[X]) p) (k + 1 + 1) * y ^ (k + 1 + 1) +
        coeff ((taylor x : (a : R[X]) → R[X]) p) (HAdd.hAdd (α := ℕ) 0 1) * y ^ HAdd.hAdd (α := ℕ) 0 1 +
      coeff ((taylor x : (a : R[X]) → R[X]) p) 0 * HPow.hPow (β := ℕ) y 0

Tactic:
simp [pow_succ, mul_assoc, Finset.sum_mul]

Premises used: pow_succ, mul_assoc, Finset.sum_mul
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
x y : R
hy : HPow.hPow (β := ℕ) y 2 = 0
rcases :
  ∀ (c : R)
    (h : c * HPow.hPow (β := ℕ) y 2 + eval x ((derivative : (a : R[X]) → R[X]) p) * y + eval x p = eval (x + y) p),
    eval (x + y) p = eval x p + eval x ((derivative : (a : R[X]) → R[X]) p) * y
⊢ eval (x + y) p = eval x p + eval x ((derivative : (a : R[X]) → R[X]) p) * y

Tactic:
rcases exists_mul_sq_add_linear_part_eq_eval_add p x y with ⟨c, h⟩

Premises used: Polynomial.exists_mul_sq_add_linear_part_eq_eval_add
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
x y : R
hy : HPow.hPow (β := ℕ) y 2 = 0
c : R
h : c * HPow.hPow (β := ℕ) y 2 + eval x ((derivative : (a : R[X]) → R[X]) p) * y + eval x p = eval (x + y) p
rw :
  c * 0 + eval x ((derivative : (a : R[X]) → R[X]) p) * y + eval x p =
    eval x p + eval x ((derivative : (a : R[X]) → R[X]) p) * y
⊢ eval (x + y) p = eval x p + eval x ((derivative : (a : R[X]) → R[X]) p) * y

Tactic:
rw [← h, hy]
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
x y : R
hy : HPow.hPow (β := ℕ) y 2 = 0
c : R
h : c * HPow.hPow (β := ℕ) y 2 + eval x ((derivative : (a : R[X]) → R[X]) p) * y + eval x p = eval (x + y) p
⊢ c * 0 + eval x ((derivative : (a : R[X]) → R[X]) p) * y + eval x p =
    eval x p + eval x ((derivative : (a : R[X]) → R[X]) p) * y

Tactic:
ring
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
p : R[X]
x y : S
hy : HPow.hPow (β := ℕ) y 2 = 0
⊢ (aeval (x + y) : (a : R[X]) → S) p =
    HAdd.hAdd (α := S) ((aeval x : (a : R[X]) → S) p : S)
      (HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) p : R[X]) : S) y)

Tactic:
simp only [← eval_map_algebraMap, Polynomial.eval_add_of_sq_eq_zero _ _ _ hy, derivative_map]

Premises used: Polynomial.eval_map_algebraMap, Polynomial.eval_add_of_sq_eq_zero, Polynomial.derivative_map
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : CommRing R
r_1 : R
f : R[X]
r : R
P : R[X]
⊢ (taylorAlgHom (-r) : (a : R[X]) → R[X])
      (OneHom.toFun (↑(↑(AlgHom.toRingHom (taylorAlgHom r)) : R[X] →* R[X]) : OneHom R[X] R[X]) P) =
    P

Tactic:
simp [taylor, comp_assoc]

Premises used: Polynomial.comp_assoc, Polynomial.taylor
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : CommRing R
r_1 : R
f : R[X]
r : R
P : R[X]
⊢ OneHom.toFun (↑(↑(AlgHom.toRingHom (taylorAlgHom r)) : R[X] →* R[X]) : OneHom R[X] R[X])
      ((taylorAlgHom (-r) : (a : R[X]) → R[X]) P) =
    P

Tactic:
simp [taylor, comp_assoc]

Premises used: Polynomial.comp_assoc, Polynomial.taylor
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : CommRing R
r : R
⊢ Eq (α := R[X] →ₐ[R] R[X]) (↑(taylorEquiv r) : R[X] →ₐ[R] R[X]) (taylorAlgHom r)

Tactic:
rfl

Premises used: AlgEquiv.toAlgHom, AlgHom.ofLinearMap, Polynomial.taylorAlgHom, rfl
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : CommRing R
r : R
⊢ (↑(↑(taylorEquiv r) : R[X] ≃ₗ[R] R[X]) : R[X] →ₗ[R] R[X]) = taylor r

Tactic:
rfl

Premises used: Polynomial.taylor, Polynomial.comp, rfl
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : CommRing R
r : R
⊢ Eq (α := R[X] ≃ₐ[R] R[X]) (AlgEquiv.symm (taylorEquiv r)) (taylorEquiv (-r))

Tactic:
AlgEquiv.ext fun _ ↦ rfl

Premises used: AlgEquiv.ext, rfl
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : CommRing R
r : R
f : R[X]
s : R
rw : eval (s - r + r) f = eval s f
rw₁ rw₂ : eval s f = eval s f
⊢ eval (s - r) ((taylor r : (a : R[X]) → R[X]) f) = eval s f

Tactic:
rw [taylor_eval, sub_add_cancel]

Premises used: Polynomial.taylor_eval, sub_add_cancel
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
r : R
rw : comp ((taylor r : (a : R[X]) → R[X]) f) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) = f
rw₁ : comp ((taylor r : (a : R[X]) → R[X]) f) (HAdd.hAdd (α := R[X]) (β := R[X]) X (-(C : (a : R) → R[X]) r : R[X])) = f
rw₂ :
  comp ((taylor r : (a : R[X]) → R[X]) f) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-r) : R[X])) = f
rw₃ : (taylor (-r) : (a : R[X]) → R[X]) ((taylor r : (a : R[X]) → R[X]) f) = f
rw₄ : (taylor (-r + r) : (a : R[X]) → R[X]) f = f
rw₅ : (taylor 0 : (a : R[X]) → R[X]) f = f
rw₆ rw₇ : f = f
⊢ (sum ((taylor r : (a : R[X]) → R[X]) f) fun (i : ℕ) (a : R) ↦
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) ^ i)) =
    f

Tactic:
rw [← comp_eq_sum_left, sub_eq_add_neg, ← C_neg, ← taylor_apply, taylor_taylor, neg_add_cancel,
    taylor_zero]

Premises used: sub_eq_add_neg, Polynomial.taylor_apply, Polynomial.taylor_taylor, neg_add_cancel, Polynomial.taylor_zero, Polynomial.comp_eq_sum_left, Polynomial.C_neg
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
R : Type u_1
inst : Semiring R
k m n : ℕ
u v w : R
⊢ trinomial k m n u v w =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m) +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)

Tactic:
rfl

Premises used: Polynomial.trinomial, rfl
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
R : Type u_1
inst : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
rw :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff
      n =
    w
rw₁ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff
        n +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff n =
    w
rw₂ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k)).coeff n +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff n +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff n =
    w
rw₃ :
  (if n = k then u else 0) +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff n +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff n =
    w
rw₄ :
  ((if n = k then u else 0) + if n = m then v else 0) +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff n =
    w
rw₅ : (((if n = k then u else 0) + if n = m then v else 0) + if n = n then w else 0) = w
rw₆ : ((0 + if n = m then v else 0) + if n = n then w else 0) = w
rw₇ : (HAdd.hAdd (α := R) 0 0 + if n = n then w else 0) = w
rw₈ : HAdd.hAdd (α := R) 0 0 + w = w
rw₉ : 0 + w = w
rw₁₀ rw₁₁ : w = w
⊢ coeff (trinomial k m n u v w) n = w

Tactic:
rw [trinomial_def, coeff_add, coeff_add, coeff_C_mul_X_pow, coeff_C_mul_X_pow, coeff_C_mul_X_pow,
    if_neg (hkm.trans hmn).ne', if_neg hmn.ne', if_pos rfl, zero_add, zero_add]

Premises used: Polynomial.coeff_add, if_pos, zero_add, LT.lt.ne', Polynomial.trinomial_def, LT.lt.trans, Polynomial.coeff_C_mul_X_pow, if_neg, rfl
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
R : Type u_1
inst : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
rw :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff
      m =
    v
rw₁ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff
        m +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff m =
    v
rw₂ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k)).coeff m +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff m +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff m =
    v
rw₃ :
  (if m = k then u else 0) +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff m +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff m =
    v
rw₄ :
  ((if m = k then u else 0) + if m = m then v else 0) +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff m =
    v
rw₅ : (((if m = k then u else 0) + if m = m then v else 0) + if m = n then w else 0) = v
rw₆ : ((0 + if m = m then v else 0) + if m = n then w else 0) = v
rw₇ : (0 + v + if m = n then w else 0) = v
rw₈ : 0 + v + 0 = v
rw₉ : v + 0 = v
rw₁₀ rw₁₁ : v = v
⊢ coeff (trinomial k m n u v w) m = v

Tactic:
rw [trinomial_def, coeff_add, coeff_add, coeff_C_mul_X_pow, coeff_C_mul_X_pow, coeff_C_mul_X_pow,
    if_neg hkm.ne', if_pos rfl, if_neg hmn.ne, zero_add, add_zero]

Premises used: Polynomial.coeff_add, if_pos, zero_add, LT.lt.ne', Polynomial.trinomial_def, Polynomial.coeff_C_mul_X_pow, add_zero, if_neg, rfl, LT.lt.ne
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
R : Type u_1
inst : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
rw :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff
      k =
    u
rw₁ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff
        k +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff k =
    u
rw₂ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k)).coeff k +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff k +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff k =
    u
rw₃ :
  (if k = k then u else 0) +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff k +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff k =
    u
rw₄ :
  ((if k = k then u else 0) + if k = m then v else 0) +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff k =
    u
rw₅ : (((if k = k then u else 0) + if k = m then v else 0) + if k = n then w else 0) = u
rw₆ : ((u + if k = m then v else 0) + if k = n then w else 0) = u
rw₇ : (u + 0 + if k = n then w else 0) = u
rw₈ : u + 0 + 0 = u
rw₉ : u + 0 = u
rw₁₀ rw₁₁ : u = u
⊢ coeff (trinomial k m n u v w) k = u

Tactic:
rw [trinomial_def, coeff_add, coeff_add, coeff_C_mul_X_pow, coeff_C_mul_X_pow, coeff_C_mul_X_pow,
    if_pos rfl, if_neg hkm.ne, if_neg (hkm.trans hmn).ne, add_zero, add_zero]

Premises used: Polynomial.coeff_add, if_pos, Polynomial.trinomial_def, LT.lt.trans, Polynomial.coeff_C_mul_X_pow, add_zero, if_neg, rfl, LT.lt.ne
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
R : Type u_1
inst : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hw rwa rwa₁ rwa₂ rwa₃ : w ≠ 0
⊢ coeff (trinomial k m n u v w) n ≠ 0

Tactic:
rwa [trinomial_leading_coeff' hkm hmn]

Premises used: Polynomial.trinomial_leading_coeff'
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
R : Type u_1
inst : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hw : w ≠ 0
fun : ∀ (i : ℕ) (h : i ∈ support (trinomial k m n u v w)), (↑i : WithBot ℕ) ≤ (↑n : WithBot ℕ)
⊢ natDegree (trinomial k m n u v w) = n

Tactic:
refine
    natDegree_eq_of_degree_eq_some
      ((Finset.sup_le fun i h => ?_).antisymm <|
        le_degree_of_ne_zero <| by rwa [trinomial_leading_coeff' hkm hmn])

Premises used: LE.le.antisymm, Finset.sup_le, Polynomial.natDegree_eq_of_degree_eq_some, Polynomial.le_degree_of_ne_zero
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
R : Type u_1
inst : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hw : w ≠ 0
i : ℕ
h : i ∈ support (trinomial k m n u v w)
⊢ Membership.mem (γ := Finset ℕ) {k, m, n} i

Tactic:
replace h := support_trinomial' k m n u v w h
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
R : Type u_1
inst : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hw : w ≠ 0
i : ℕ
h : Membership.mem (γ := Finset ℕ) {k, m, n} i
⊢ i = k ∨ i = m ∨ i = n

Tactic:
rw [mem_insert, mem_insert, mem_singleton] at h

Premises used: Finset.mem_singleton, Finset.mem_insert
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
R : Type u_1
inst : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hw : w ≠ 0
i : ℕ
h : i = k ∨ i = m ∨ i = n
inl : ∀ (hkm : i < m), (↑i : WithBot ℕ) ≤ (↑n : WithBot ℕ)
inr : ∀ (hkm : k < i) (hmn : i < n), (↑i : WithBot ℕ) ≤ (↑n : WithBot ℕ)
inr₁ : ∀ (hmn : m < i), (↑i : WithBot ℕ) ≤ (↑i : WithBot ℕ)
⊢ (↑i : WithBot ℕ) ≤ (↑n : WithBot ℕ)

Tactic:
rcases h with (rfl | rfl | rfl)

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
u v w : R
hmn : m < n
hw : w ≠ 0
i : ℕ
hkm : i < m
⊢ (↑i : WithBot ℕ) ≤ (↑n : WithBot ℕ)

Tactic:
WithBot.coe_le_coe.mpr (hkm.trans hmn).le

Premises used: Iff.mpr, LT.lt.le, WithBot.coe_le_coe, LT.lt.trans
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
u v w : R
hmn : m < n
hw : w ≠ 0
i : ℕ
hkm : i < m
⊢ (↑i : WithBot ℕ) ≤ (↑n : WithBot ℕ)

Tactic:
exact WithBot.coe_le_coe.mpr (hkm.trans hmn).le

Premises used: Iff.mpr, LT.lt.le, WithBot.coe_le_coe, LT.lt.trans
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
R : Type u_1
inst : Semiring R
k n : ℕ
u v w : R
hw : w ≠ 0
i : ℕ
hkm : k < i
hmn : i < n
⊢ (↑i : WithBot ℕ) ≤ (↑n : WithBot ℕ)

Tactic:
WithBot.coe_le_coe.mpr hmn.le

Premises used: Iff.mpr, LT.lt.le, WithBot.coe_le_coe
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
R : Type u_1
inst : Semiring R
k n : ℕ
u v w : R
hw : w ≠ 0
i : ℕ
hkm : k < i
hmn : i < n
⊢ (↑i : WithBot ℕ) ≤ (↑n : WithBot ℕ)

Tactic:
exact WithBot.coe_le_coe.mpr hmn.le

Premises used: Iff.mpr, LT.lt.le, WithBot.coe_le_coe
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
R : Type u_1
inst : Semiring R
k m : ℕ
u v w : R
hkm : k < m
hw : w ≠ 0
i : ℕ
hmn : m < i
⊢ (↑i : WithBot ℕ) ≤ (↑i : WithBot ℕ)

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
R : Type u_1
inst : Semiring R
k m : ℕ
u v w : R
hkm : k < m
hw : w ≠ 0
i : ℕ
hmn : m < i
⊢ (↑i : WithBot ℕ) ≤ (↑i : WithBot ℕ)

Tactic:
exact le_rfl

Premises used: le_rfl
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
R : Type u_1
inst : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu rwa rwa₁ rwa₂ rwa₃ : u ≠ 0
⊢ coeff (trinomial k m n u v w) k ≠ 0

Tactic:
rwa [trinomial_trailing_coeff' hkm hmn]

Premises used: Polynomial.trinomial_trailing_coeff'
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
R : Type u_1
inst : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
fun : ∀ (i : ℕ) (h : i ∈ support (trinomial k m n u v w)), (↑k : ℕ∞) ≤ (↑i : WithTop ℕ)
⊢ natTrailingDegree (trinomial k m n u v w) = k

Tactic:
refine
    natTrailingDegree_eq_of_trailingDegree_eq_some
      ((Finset.le_inf fun i h => ?_).antisymm <|
          trailingDegree_le_of_ne_zero <| by rwa [trinomial_trailing_coeff' hkm hmn]).symm

Premises used: LE.le.antisymm, Polynomial.trailingDegree_le_of_ne_zero, Finset.le_inf, Eq.symm, Polynomial.natTrailingDegree_eq_of_trailingDegree_eq_some
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
R : Type u_1
inst : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
i : ℕ
h : i ∈ support (trinomial k m n u v w)
⊢ Membership.mem (γ := Finset ℕ) {k, m, n} i

Tactic:
replace h := support_trinomial' k m n u v w h
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
R : Type u_1
inst : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
i : ℕ
h : Membership.mem (γ := Finset ℕ) {k, m, n} i
⊢ i = k ∨ i = m ∨ i = n

Tactic:
rw [mem_insert, mem_insert, mem_singleton] at h

Premises used: Finset.mem_singleton, Finset.mem_insert
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
R : Type u_1
inst : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
i : ℕ
h : i = k ∨ i = m ∨ i = n
inl : ∀ (hkm : i < m), (↑i : ℕ∞) ≤ (↑i : WithTop ℕ)
inr : ∀ (hkm : k < i) (hmn : i < n), (↑k : ℕ∞) ≤ (↑i : WithTop ℕ)
inr₁ : ∀ (hmn : m < i), (↑k : ℕ∞) ≤ (↑i : WithTop ℕ)
⊢ (↑k : ℕ∞) ≤ (↑i : WithTop ℕ)

Tactic:
rcases h with (rfl | rfl | rfl)

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
u v w : R
hmn : m < n
hu : u ≠ 0
i : ℕ
hkm : i < m
⊢ (↑i : ℕ∞) ≤ (↑i : WithTop ℕ)

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
u v w : R
hmn : m < n
hu : u ≠ 0
i : ℕ
hkm : i < m
⊢ (↑i : ℕ∞) ≤ (↑i : WithTop ℕ)

Tactic:
exact le_rfl

Premises used: le_rfl
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
R : Type u_1
inst : Semiring R
k n : ℕ
u v w : R
hu : u ≠ 0
i : ℕ
hkm : k < i
hmn : i < n
⊢ (↑k : ℕ∞) ≤ (↑i : WithTop ℕ)

Tactic:
WithTop.coe_le_coe.mpr hkm.le

Premises used: Iff.mpr, LT.lt.le, WithTop.coe_le_coe
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
R : Type u_1
inst : Semiring R
k n : ℕ
u v w : R
hu : u ≠ 0
i : ℕ
hkm : k < i
hmn : i < n
⊢ (↑k : ℕ∞) ≤ (↑i : WithTop ℕ)

Tactic:
exact WithTop.coe_le_coe.mpr hkm.le

Premises used: Iff.mpr, LT.lt.le, WithTop.coe_le_coe
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
R : Type u_1
inst : Semiring R
k m : ℕ
u v w : R
hkm : k < m
hu : u ≠ 0
i : ℕ
hmn : m < i
⊢ (↑k : ℕ∞) ≤ (↑i : WithTop ℕ)

Tactic:
WithTop.coe_le_coe.mpr (hkm.trans hmn).le

Premises used: Iff.mpr, LT.lt.le, LT.lt.trans, WithTop.coe_le_coe
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
R : Type u_1
inst : Semiring R
k m : ℕ
u v w : R
hkm : k < m
hu : u ≠ 0
i : ℕ
hmn : m < i
⊢ (↑k : ℕ∞) ≤ (↑i : WithTop ℕ)

Tactic:
exact WithTop.coe_le_coe.mpr (hkm.trans hmn).le

Premises used: Iff.mpr, LT.lt.le, LT.lt.trans, WithTop.coe_le_coe
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
R : Type u_1
inst : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hw : w ≠ 0
rw : coeff (trinomial k m n u v w) (natDegree (trinomial k m n u v w)) = w
rw₁ : coeff (trinomial k m n u v w) n = w
rw₂ rw₃ : w = w
⊢ leadingCoeff (trinomial k m n u v w) = w

Tactic:
rw [leadingCoeff, trinomial_natDegree hkm hmn hw, trinomial_leading_coeff' hkm hmn]

Premises used: Polynomial.trinomial_leading_coeff', Polynomial.trinomial_natDegree, Polynomial.leadingCoeff
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
R : Type u_1
inst : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
rw : coeff (trinomial k m n u v w) (natTrailingDegree (trinomial k m n u v w)) = u
rw₁ : coeff (trinomial k m n u v w) k = u
rw₂ rw₃ : u = u
⊢ trailingCoeff (trinomial k m n u v w) = u

Tactic:
rw [trailingCoeff, trinomial_natTrailingDegree hkm hmn hu, trinomial_trailing_coeff' hkm hmn]

Premises used: Polynomial.trinomial_trailing_coeff', Polynomial.trinomial_natTrailingDegree, Polynomial.trailingCoeff
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
R : Type u_1
inst : Semiring R
k m n : ℕ
u v : R
hkm : k < m
hmn : m < n
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
R : Type u_1
inst : Semiring R
k m n : ℕ
u v : R
hkm : k < m
hmn : m < n
h : Nontrivial R
⊢ Monic (trinomial k m n u v 1)

Tactic:
trinomial_leadingCoeff hkm hmn one_ne_zero

Premises used: Polynomial.Monic, Polynomial.trinomial_leadingCoeff, one_ne_zero
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
R : Type u_1
inst : Semiring R
k m n : ℕ
u v : R
hkm : k < m
hmn : m < n
h : Nontrivial R
⊢ Monic (trinomial k m n u v 1)

Tactic:
exact trinomial_leadingCoeff hkm hmn one_ne_zero

Premises used: Polynomial.trinomial_leadingCoeff, one_ne_zero
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
R : Type u_1
inst : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
⊢ support (trinomial k m n u v w) = {k, m, n}

Tactic:
support_trinomial hkm hmn hu hv hw

Premises used: Polynomial.support_trinomial, Polynomial.trinomial
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
hp : p.IsUnitTrinomial
obtain :
  ∀ (k m n : ℕ) (hkm : k < m) (hmn : m < n) (u v w : ℤˣ),
    ¬IsUnit (M := ℤ[X]) (trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ))
⊢ ¬IsUnit p

Tactic:
obtain ⟨k, m, n, hkm, hmn, u, v, w, rfl⟩ := hp

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ ¬IsUnit (M := ℤ[X]) (trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ))

Tactic:
fun h =>
    ne_zero_of_lt hmn
      ((trinomial_natDegree hkm hmn w.ne_zero).symm.trans
        (natDegree_eq_of_degree_eq_some (degree_eq_zero_of_isUnit h)))

Premises used: ne_zero_of_lt, Polynomial.trinomial_natDegree, Units.ne_zero, Polynomial.natDegree_eq_of_degree_eq_some, Polynomial.degree_eq_zero_of_isUnit, Eq.symm, Not, Eq.trans
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ ¬IsUnit (M := ℤ[X]) (trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ))

Tactic:
exact fun h =>
    ne_zero_of_lt hmn
      ((trinomial_natDegree hkm hmn w.ne_zero).symm.trans
        (natDegree_eq_of_degree_eq_some (degree_eq_zero_of_isUnit h)))

Premises used: ne_zero_of_lt, Polynomial.trinomial_natDegree, Units.ne_zero, Polynomial.natDegree_eq_of_degree_eq_some, Polynomial.degree_eq_zero_of_isUnit, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
hp : p.IsUnitTrinomial
obtain :
  ∀ (k m n : ℕ) (hkm : k < m) (hmn : m < n) (u v w : ℤˣ), #(support (trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ))) = 3
⊢ #p.support = 3

Tactic:
obtain ⟨k, m, n, hkm, hmn, u, v, w, rfl⟩ := hp

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ #(support (trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ))) = 3

Tactic:
card_support_trinomial hkm hmn u.ne_zero v.ne_zero w.ne_zero

Premises used: Polynomial.trinomial, Units.ne_zero, Polynomial.card_support_trinomial
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ #(support (trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ))) = 3

Tactic:
exact card_support_trinomial hkm hmn u.ne_zero v.ne_zero w.ne_zero

Premises used: Units.ne_zero, Polynomial.card_support_trinomial