awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : Nontrivial B
this : Nontrivial A
hx : IsIntegral A x
⊢ ¬IsUnit (M := A[X]) (minpoly A x)

Tactic:
exact mt (monic hx).eq_one_of_isUnit (ne_one A x)

Premises used: minpoly.monic, minpoly.ne_one, mt, Polynomial.Monic.eq_one_of_isUnit
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : Nontrivial B
this : Nontrivial A
hx : ¬IsIntegral A x
neg : ¬IsUnit.{u_1} (M := A[X]) 0
⊢ ¬IsUnit (M := A[X]) (minpoly A x)

Tactic:
rw [eq_zero hx]

Premises used: minpoly.eq_zero
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : Nontrivial B
this : Nontrivial A
hx : ¬IsIntegral A x
⊢ ¬IsUnit.{u_1} (M := A[X]) 0

Tactic:
not_isUnit_zero

Premises used: not_isUnit_zero
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : Nontrivial B
this : Nontrivial A
hx : ¬IsIntegral A x
⊢ ¬IsUnit.{u_1} (M := A[X]) 0

Tactic:
exact not_isUnit_zero

Premises used: not_isUnit_zero
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
hx : degree (minpoly A x) = 1
by_contra : ∀ (h : ¬IsIntegral A x), False
⊢ IsIntegral A x

Tactic:
by_contra h
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
hx : degree (minpoly A x) = 1
h : ¬IsIntegral A x
⊢ Eq (α := WithBot ℕ) ⊥ (↑1 : WithBot ℕ)

Tactic:
rw [eq_zero h, degree_zero, ← WithBot.coe_one] at hx

Premises used: Polynomial.degree_zero, minpoly.eq_zero, WithBot.coe_one
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
hx : degree (minpoly A x) = 1
h : ¬IsIntegral A x
hx₁ : Eq (α := WithBot ℕ) ⊥ (↑1 : WithBot ℕ)
⊢ ¬IsIntegral A x

Tactic:
rw [eq_zero h, degree_zero, ← WithBot.coe_one] at hx

Premises used: Polynomial.degree_zero, minpoly.eq_zero, WithBot.coe_one
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
hx : Eq (α := WithBot ℕ) ⊥ (↑1 : WithBot ℕ)
h : ¬IsIntegral A x
⊢ False

Tactic:
ne_of_lt (show ⊥ < ↑1 from WithBot.bot_lt_coe 1) hx

Premises used: ne_of_lt
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
hx : Eq (α := WithBot ℕ) ⊥ (↑1 : WithBot ℕ)
h : ¬IsIntegral A x
⊢ False

Tactic:
exact ne_of_lt (show ⊥ < ↑1 from WithBot.bot_lt_coe 1) hx

Premises used: ne_of_lt
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
hx : degree (minpoly A x) = 1
⊢ IsIntegral A x

Tactic:
have h : IsIntegral A x := by
    by_contra h
    rw [eq_zero h, degree_zero, ← WithBot.coe_one] at hx
    exact ne_of_lt (show ⊥ < ↑1 from WithBot.bot_lt_coe 1) hx
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
hx : degree (minpoly A x) = 1
h : IsIntegral A x
⊢ Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) (minpoly A x) : B) (0 : B)

Tactic:
have key := minpoly.aeval A x
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
hx : degree (minpoly A x) = 1
h : IsIntegral A x
key : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) (minpoly A x) : B) (0 : B)
⊢ x = (algebraMap A B : (a : A) → B) (-coeff (minpoly A x) 0)

Tactic:
rw [eq_X_add_C_of_degree_eq_one hx, (minpoly.monic h).leadingCoeff, C_1, one_mul, aeval_add,
    aeval_C, aeval_X, ← eq_neg_iff_add_eq_zero, ← map_neg] at key

Premises used: Polynomial.C_1, minpoly.monic, Polynomial.eq_X_add_C_of_degree_eq_one, map_neg, Polynomial.aeval_C, Polynomial.Monic.leadingCoeff, eq_neg_iff_add_eq_zero, Polynomial.aeval_add, one_mul, Polynomial.aeval_X
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
hx : degree (minpoly A x) = 1
h : IsIntegral A x
key : x = (algebraMap A B : (a : A) → B) (-coeff (minpoly A x) 0)
⊢ Membership.mem (γ := Subring B) (RingHom.range.{u_1, u_2} (R := A) (algebraMap A B)) x

Tactic:
⟨-(minpoly A x).coeff 0, key.symm⟩

Premises used: Set.Mem, setOf, minpoly, Polynomial.coeff, Exists.intro, Set.range, OfNat.ofNat, Eq.symm, Neg.neg
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
hx : degree (minpoly A x) = 1
h : IsIntegral A x
key : x = (algebraMap A B : (a : A) → B) (-coeff (minpoly A x) 0)
⊢ Membership.mem (γ := Subring B) (RingHom.range.{u_1, u_2} (R := A) (algebraMap A B)) x

Tactic:
exact ⟨-(minpoly A x).coeff 0, key.symm⟩
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
pmonic : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
pos :
  ∀ (hx : IsIntegral A x),
    (WellFounded.min (r := fun (p q : A[X]) ↦ p.degree < q.degree) ⋯
          (fun (x_1 : A[X]) ↦ x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx).degree ≤
      p.degree
neg : ∀ (hx : ¬IsIntegral A x), degree.{u_1} (R := A) 0 ≤ p.degree
⊢ degree.{u_1} (R := A)
      (if hx : IsIntegral A x then
        WellFounded.min (r := fun (p q : A[X]) ↦ p.degree < q.degree) ⋯
          (fun (x_1 : A[X]) ↦ x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx
      else 0) ≤
    p.degree

Tactic:
split_ifs with hx
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
pmonic : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
hx : IsIntegral A x
⊢ (WellFounded.min (r := fun (p q : A[X]) ↦ p.degree < q.degree) ⋯
        (fun (x_1 : A[X]) ↦ x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx).degree ≤
    p.degree

Tactic:
le_of_not_gt <| degree_lt_wf.not_lt_min _ ?_

Premises used: Polynomial.degree_lt_wf, le_of_not_gt, WellFounded.not_lt_min
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
pmonic : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
hx : IsIntegral A x
pos : Membership.mem (γ := Set A[X]) (fun (x_1 : A[X]) ↦ x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) p
⊢ (WellFounded.min (r := fun (p q : A[X]) ↦ p.degree < q.degree) ⋯
        (fun (x_1 : A[X]) ↦ x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx).degree ≤
    p.degree

Tactic:
refine le_of_not_gt <| degree_lt_wf.not_lt_min _ ?_

Premises used: Polynomial.degree_lt_wf, le_of_not_gt, WellFounded.not_lt_min
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
pmonic : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
hx : IsIntegral A x
⊢ Membership.mem (γ := Set A[X]) (fun (x_1 : A[X]) ↦ x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) p

Tactic:
⟨pmonic, hp⟩

Premises used: Set.Mem, And.intro
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
pmonic : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
hx : IsIntegral A x
⊢ Membership.mem (γ := Set A[X]) (fun (x_1 : A[X]) ↦ x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) p

Tactic:
exact ⟨pmonic, hp⟩
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
pmonic : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
hx : ¬IsIntegral A x
⊢ degree.{u_1} (R := A) 0 ≤ p.degree

Tactic:
simp only [degree_zero, bot_le]

Premises used: Polynomial.degree_zero, bot_le
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
hm : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
hl :
  ∀ (q : A[X]),
    q.degree < p.degree → q = 0 ∨ Ne.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) (0 : B)
⊢ Nontrivial A

Tactic:
nontriviality A
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
hm : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
hl :
  ∀ (q : A[X]),
    q.degree < p.degree → q = 0 ∨ Ne.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) (0 : B)
h : Nontrivial A
⊢ IsIntegral A x

Tactic:
have hx : IsIntegral A x := ⟨p, hm, hp⟩
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
hm : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
hl :
  ∀ (q : A[X]),
    q.degree < p.degree → q = 0 ∨ Ne.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) (0 : B)
h : Nontrivial A
hx : IsIntegral A x
inl : ∀ (h : minpoly A x %ₘ p = 0), p = minpoly A x
inr :
  ∀ (h : Ne.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) (minpoly A x %ₘ p) : B) (0 : B)), p = minpoly A x
⊢ p = minpoly A x

Tactic:
obtain h | h := hl _ ((minpoly A x).degree_modByMonic_lt hm)

Premises used: minpoly, Polynomial.degree_modByMonic_lt
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
hm : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
hl :
  ∀ (q : A[X]),
    q.degree < p.degree → q = 0 ∨ Ne.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) (0 : B)
h_1 : Nontrivial A
hx : IsIntegral A x
h : Ne.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) (minpoly A x %ₘ p) : B) (0 : B)
⊢ p = minpoly A x

Tactic:
(h <| (aeval_modByMonic_eq_self_of_root hp).trans <| aeval A x).elim

Premises used: False.elim, Polynomial.aeval_modByMonic_eq_self_of_root, minpoly.aeval, Eq.trans
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
hm : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
hl :
  ∀ (q : A[X]),
    q.degree < p.degree → q = 0 ∨ Ne.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) (0 : B)
h_1 : Nontrivial A
hx : IsIntegral A x
h : Ne.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) (minpoly A x %ₘ p) : B) (0 : B)
⊢ p = minpoly A x

Tactic:
exact (h <| (aeval_modByMonic_eq_self_of_root hp).trans <| aeval A x).elim

Premises used: False.elim, Polynomial.aeval_modByMonic_eq_self_of_root, minpoly.aeval, Eq.trans
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
hm : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
hl :
  ∀ (q : A[X]),
    q.degree < p.degree → q = 0 ∨ Ne.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) (0 : B)
h_1 : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
inl : ∀ (r : A[X]) (hr : minpoly A x = p * r), p = minpoly A x
⊢ p = minpoly A x

Tactic:
obtain ⟨r, hr⟩ := (modByMonic_eq_zero_iff_dvd hm).1 h

Premises used: Polynomial.modByMonic_eq_zero_iff_dvd, Iff.mp
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
hm : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
hl :
  ∀ (q : A[X]),
    q.degree < p.degree → q = 0 ∨ Ne.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) (0 : B)
h_1 : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
inl : p = p * r
⊢ p = minpoly A x

Tactic:
rw [hr]
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
hm : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
hl :
  ∀ (q : A[X]),
    q.degree < p.degree → q = 0 ∨ Ne.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) (0 : B)
h_1 : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
⊢ leadingCoeff (minpoly A x) = (p * r).leadingCoeff

Tactic:
have hlead := congr_arg leadingCoeff hr
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
hm : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
hl :
  ∀ (q : A[X]),
    q.degree < p.degree → q = 0 ∨ Ne.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) (0 : B)
h_1 : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
hlead : leadingCoeff (minpoly A x) = (p * r).leadingCoeff
⊢ 1 = r.leadingCoeff

Tactic:
rw [mul_comm, leadingCoeff_mul_monic hm, (monic hx).leadingCoeff] at hlead

Premises used: minpoly.monic, mul_comm, Polynomial.leadingCoeff_mul_monic, Polynomial.Monic.leadingCoeff
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
hm : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
hl :
  ∀ (q : A[X]),
    q.degree < p.degree → q = 0 ∨ Ne.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) (0 : B)
h_1 : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
hr : minpoly A x = p * 0
hlead : Eq.{u_1 + 1} (α := A) 1 (leadingCoeff 0)
⊢ False

Tactic:
ne_zero hx (mul_zero p ▸ hr)

Premises used: Eq.rec, MulZeroClass.mul_zero, minpoly.ne_zero
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
hm : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
hl :
  ∀ (q : A[X]),
    q.degree < p.degree → q = 0 ∨ Ne.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) (0 : B)
h_1 : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
hr : minpoly A x = p * 0
hlead : Eq.{u_1 + 1} (α := A) 1 (leadingCoeff 0)
⊢ False

Tactic:
exact ne_zero hx (mul_zero p ▸ hr)

Premises used: Eq.rec, MulZeroClass.mul_zero, minpoly.ne_zero
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
hm : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
hl :
  ∀ (q : A[X]),
    q.degree < p.degree → q = 0 ∨ Ne.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) (0 : B)
h_1 : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
hlead : 1 = r.leadingCoeff
⊢ r ≠ 0

Tactic:
have hr0 : r ≠ 0 := by
      rintro rfl
      exact ne_zero hx (mul_zero p ▸ hr)
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
hm : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
hl :
  ∀ (q : A[X]),
    q.degree < p.degree → q = 0 ∨ Ne.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) (0 : B)
h_1 : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
hlead : 1 = r.leadingCoeff
hr0 : r ≠ 0
⊢ natDegree (minpoly A x) = (p * r).natDegree

Tactic:
apply_fun natDegree at hr

Premises used: Polynomial.natDegree
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
hm : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
hl :
  ∀ (q : A[X]),
    q.degree < p.degree → q = 0 ∨ Ne.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) (0 : B)
h_1 : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hlead : 1 = r.leadingCoeff
hr0 : r ≠ 0
hr : natDegree (minpoly A x) = (p * r).natDegree
⊢ natDegree (minpoly A x) = p.natDegree + r.natDegree

Tactic:
rw [hm.natDegree_mul' hr0] at hr

Premises used: Polynomial.Monic.natDegree_mul'
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
hm : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
hl :
  ∀ (q : A[X]),
    q.degree < p.degree → q = 0 ∨ Ne.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) (0 : B)
h_1 : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hlead : 1 = r.leadingCoeff
hr0 : r ≠ 0
hr : natDegree (minpoly A x) = p.natDegree + r.natDegree
h₁ : p.natDegree + r.natDegree ≤ p.natDegree + 0
a : ℕ
⊢ r.natDegree ≤ 0

Tactic:
apply Nat.le_of_add_le_add_left

Premises used: Nat.le_of_add_le_add_left
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
hm : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
hl :
  ∀ (q : A[X]),
    q.degree < p.degree → q = 0 ∨ Ne.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) (0 : B)
h_1 : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hlead : 1 = r.leadingCoeff
hr0 : r ≠ 0
hr : natDegree (minpoly A x) = p.natDegree + r.natDegree
⊢ p.natDegree + r.natDegree ≤ p.natDegree

Tactic:
hr.symm.trans_le (natDegree_le_natDegree <| min A x hm hp)

Premises used: Polynomial.natDegree_le_natDegree, Eq.trans_le, minpoly.min, Eq.symm
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
hm : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
hl :
  ∀ (q : A[X]),
    q.degree < p.degree → q = 0 ∨ Ne.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) (0 : B)
h_1 : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
hlead : 1 = r.leadingCoeff
⊢ r.natDegree ≤ 0

Tactic:
have : natDegree r ≤ 0 := by
    have hr0 : r ≠ 0 := by
      rintro rfl
      exact ne_zero hx (mul_zero p ▸ hr)
    apply_fun natDegree at hr
    rw [hm.natDegree_mul' hr0] at hr
    apply Nat.le_of_add_le_add_left
    rw [add_zero]
    exact hr.symm.trans_le (natDegree_le_natDegree <| min A x hm hp)
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
hm : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
hl :
  ∀ (q : A[X]),
    q.degree < p.degree → q = 0 ∨ Ne.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) (0 : B)
h_1 : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
hlead : 1 = r.leadingCoeff
this : r.natDegree ≤ 0
inl : p = HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) (r.coeff 0) : A[X])
inl₁ : p = HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) (r.coeff r.natDegree) : A[X])
inl₂ : p = HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) r.leadingCoeff : A[X])
inl₃ : p = p * (C : (a : A) → A[X]) 1
inl₄ : p = p * 1
inl₅ inl₆ : p = p
⊢ p = p * r

Tactic:
rw [eq_C_of_natDegree_le_zero this, ← Nat.eq_zero_of_le_zero this, ← leadingCoeff, ← hlead, C_1,
    mul_one]

Premises used: Polynomial.C_1, Polynomial.eq_C_of_natDegree_le_zero, Polynomial.leadingCoeff, mul_one, Nat.eq_zero_of_le_zero
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
monic : p.Monic
hp0 : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
n : ℕ
hpn : p.degree = (↑n : WithBot ℕ)
ind : LinearIndependent.{0, u_1, u_2} A (M := B) fun (i : Fin n) ↦ x ^ (↑i : ℕ)
q : A[X]
lt : q.degree < p.degree
ne : ¬q = 0
hq : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) (0 : B)
i : ℕ
rw :
  ∀
    (hq :
      Eq.{u_2 + 1} (α := B)
        ((Polynomial.aeval x : (a : A[X]) → B) (∑ i ∈ Finset.range n, (monomial i : (a : A) → A[X]) (q.coeff i)) : B)
        (0 : B))
    (i : ℕ), q.coeff i = coeff 0 i
⊢ q.coeff i = coeff 0 i

Tactic:
rw [q.as_sum_range' _ ((natDegree_lt_iff_degree_lt ne).mpr (hpn ▸ lt))] at hq

Premises used: Iff.mpr, Polynomial.natDegree_lt_iff_degree_lt, Polynomial.as_sum_range'
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
monic : p.Monic
hp0 : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
n : ℕ
hpn : p.degree = (↑n : WithBot ℕ)
ind : LinearIndependent.{0, u_1, u_2} A (M := B) fun (i : Fin n) ↦ x ^ (↑i : ℕ)
q : A[X]
lt : q.degree < p.degree
ne : ¬q = 0
hq :
  Eq.{u_2 + 1} (α := B)
    ((Polynomial.aeval x : (a : A[X]) → B) (∑ i ∈ Finset.range n, (monomial i : (a : A) → A[X]) (q.coeff i)) : B)
    (0 : B)
i : ℕ
inl : ∀ (lt : i < n), q.coeff i = coeff 0 i
inr : ∀ (le : n ≤ i), q.coeff i = coeff 0 i
⊢ q.coeff i = coeff 0 i

Tactic:
obtain lt | le := lt_or_ge i n

Premises used: lt_or_ge
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
monic : p.Monic
hp0 : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
n : ℕ
hpn : p.degree = (↑n : WithBot ℕ)
ind : LinearIndependent.{0, u_1, u_2} A (M := B) fun (i : Fin n) ↦ x ^ (↑i : ℕ)
q : A[X]
lt_1 : q.degree < p.degree
ne : ¬q = 0
hq :
  Eq.{u_2 + 1} (α := B)
    ((Polynomial.aeval x : (a : A[X]) → B) (∑ i ∈ Finset.range n, (monomial i : (a : A) → A[X]) (q.coeff i)) : B)
    (0 : B)
i : ℕ
lt : i < n
⊢ Eq.{u_2 + 1} (α := B)
    (∑ i : Fin n, HSMul.hSMul.{u_1, u_2, u_2} (α := A) ((fun (x : Fin n) ↦ q.coeff (↑x : ℕ)) i) (x ^ (↑i : ℕ))) 0

Tactic:
simpa [Finset.sum_range, Algebra.smul_def] using hq

Premises used: Finset.sum_range, Algebra.smul_def
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
monic : p.Monic
hp0 : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
n : ℕ
hpn : p.degree = (↑n : WithBot ℕ)
ind : LinearIndependent.{0, u_1, u_2} A (M := B) fun (i : Fin n) ↦ x ^ (↑i : ℕ)
q : A[X]
lt_1 : q.degree < p.degree
ne : ¬q = 0
hq :
  Eq.{u_2 + 1} (α := B)
    ((Polynomial.aeval x : (a : A[X]) → B) (∑ i ∈ Finset.range n, (monomial i : (a : A) → A[X]) (q.coeff i)) : B)
    (0 : B)
i : ℕ
lt : i < n
⊢ q.coeff i = coeff 0 i

Tactic:
simpa using Fintype.linearIndependent_iff.mp ind (q.coeff ·)
        (by simpa [Finset.sum_range, Algebra.smul_def] using hq) ⟨i, lt⟩

Premises used: Fin.mk, Fin.val, Polynomial.coeff, Fintype.linearIndependent_iff, Iff.mp