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
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 : ℕ
le : n ≤ i
⊢ q.coeff i = coeff 0 i

Tactic:
coeff_eq_zero_of_degree_lt ((hpn ▸ lt).trans_le <| WithBot.coe_le_coe.mpr le)

Premises used: Polynomial.coeff, Polynomial.coeff_eq_zero_of_degree_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]
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 : ℕ
le : n ≤ i
⊢ q.coeff i = coeff 0 i

Tactic:
exact coeff_eq_zero_of_degree_lt ((hpn ▸ lt).trans_le <| WithBot.coe_le_coe.mpr le)

Premises used: Polynomial.coeff_eq_zero_of_degree_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
inst_3 : Subsingleton 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
inst_3 : Subsingleton B
h : Nontrivial A
⊢ degree (minpoly A x) ≤ degree.{u_1} (R := A) 1

Tactic:
have := minpoly.min A x monic_one (Subsingleton.elim _ _)
-- 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 : Subsingleton B
h : Nontrivial A
this : degree (minpoly A x) ≤ degree.{u_1} (R := A) 1
⊢ degree (minpoly A x) ≤ 0

Tactic:
rw [degree_one] at this

Premises used: Polynomial.degree_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
inst_3 : Subsingleton B
h : Nontrivial A
this : degree (minpoly A x) ≤ 0
inl : ∀ (h : degree (minpoly A x) ≤ 0), Eq (α := A[X]) (minpoly A x) 1
inr : ∀ (h : 0 < degree (minpoly A x)), Eq (α := A[X]) (minpoly A x) 1
⊢ Eq (α := A[X]) (minpoly A x) 1

Tactic:
rcases le_or_gt (minpoly A x).degree 0 with h | h

Premises used: Polynomial.degree, minpoly, le_or_gt, OfNat.ofNat
-- 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 : Subsingleton B
h_1 : Nontrivial A
this : degree (minpoly A x) ≤ 0
h : degree (minpoly A x) ≤ 0
⊢ eval₂ (algebraMap A B) x 1 = 0

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- 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 : Subsingleton B
h_1 : Nontrivial A
this : degree (minpoly A x) ≤ 0
h : degree (minpoly A x) ≤ 0
inl inl₁ inl₂ inl₃ : ∀ (h : Eq (α := A[X]) (minpoly A x) 1), Eq (α := A[X]) (minpoly A x) 1
⊢ Eq (α := A[X]) (minpoly A x) 1

Tactic:
rwa [(monic ⟨1, monic_one, by simp [eq_iff_true_of_subsingleton]⟩ :
           (minpoly A x).Monic).degree_le_zero_iff_eq_one] at h

Premises used: minpoly.monic, And.intro, Exists.intro, Polynomial.monic_one, OfNat.ofNat, Polynomial.Monic.degree_le_zero_iff_eq_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
inst_3 : Subsingleton B
h_1 : Nontrivial A
this : degree (minpoly A x) ≤ 0
h : 0 < degree (minpoly A x)
⊢ Eq (α := A[X]) (minpoly A x) 1

Tactic:
(this.not_gt h).elim

Premises used: False.elim, LE.le.not_gt
-- 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 : Subsingleton B
h_1 : Nontrivial A
this : degree (minpoly A x) ≤ 0
h : 0 < degree (minpoly A x)
⊢ Eq (α := A[X]) (minpoly A x) 1

Tactic:
exact (this.not_gt h).elim

Premises used: False.elim, LE.le.not_gt
-- 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
hx : IsIntegral A x
rw : natDegree (minpoly A x) ≠ 0
⊢ 0 < natDegree (minpoly A x)

Tactic:
rw [pos_iff_ne_zero]

Premises used: pos_iff_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
inst_3 : Nontrivial B
hx : IsIntegral A x
ndeg_eq_zero : natDegree (minpoly A x) = 0
rw : Eq (α := A[X]) ((C : (a : A) → A[X]) (coeff (minpoly A x) 0) : A[X]) (1 : A[X])
⊢ Eq (α := A[X]) (minpoly A x) 1

Tactic:
rw [eq_C_of_natDegree_eq_zero ndeg_eq_zero]

Premises used: Polynomial.eq_C_of_natDegree_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
hx : IsIntegral A x
ndeg_eq_zero : natDegree (minpoly A x) = 0
⊢ Eq.{u_1 + 1} (α := A[X]) ((C : (a : A) → A[X]) 1) 1

Tactic:
C_1 (R := A)

Premises used: Polynomial.C_1
-- 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
hx : IsIntegral A x
ndeg_eq_zero : natDegree (minpoly A x) = 0
h : coeff (minpoly A x) 0 = 1
⊢ Eq (α := A[X]) ((C : (a : A) → A[X]) (coeff (minpoly A x) 0) : A[X]) (1 : A[X])

Tactic:
convert! C_1 (R := A)

Premises used: Polynomial.C_1
-- 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
hx : IsIntegral A x
ndeg_eq_zero : natDegree (minpoly A x) = 0
⊢ coeff (minpoly A x) 0 = 1

Tactic:
simpa only [ndeg_eq_zero.symm] using (monic hx).leadingCoeff

Premises used: minpoly.monic, Polynomial.Monic.leadingCoeff, 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
inst_3 : Nontrivial B
hx : IsIntegral A x
ndeg_eq_zero : natDegree (minpoly A x) = 0
⊢ Eq (α := A[X]) (minpoly A x) 1

Tactic:
have eq_one : minpoly A x = 1 := by
    rw [eq_C_of_natDegree_eq_zero ndeg_eq_zero]
    convert! C_1 (R := A)
    simpa only [ndeg_eq_zero.symm] using (monic hx).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
inst_3 : Nontrivial B
hx : IsIntegral A x
ndeg_eq_zero : natDegree (minpoly A x) = 0
eq_one : Eq (α := A[X]) (minpoly A x) 1
⊢ False

Tactic:
simpa only [eq_one, map_one, one_ne_zero] using aeval A x

Premises used: minpoly.aeval, map_one, one_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
inst_3 : Nontrivial B
hx : IsIntegral A x
⊢ 0 < degree (minpoly A x)

Tactic:
natDegree_pos_iff_degree_pos.mp (natDegree_pos hx)

Premises used: Iff.mp, Polynomial.natDegree_pos_iff_degree_pos, minpoly.natDegree_pos
-- 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
⊢ degree (minpoly A x) = 1 ↔ Membership.mem (γ := Subring B) (RingHom.range.{u_1, u_2} (R := A) (algebraMap A B)) x

Tactic:
⟨minpoly.mem_range_of_degree_eq_one _ _, ?_⟩

Premises used: minpoly.mem_range_of_degree_eq_one, Iff.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
inst_3 : Nontrivial B
refine :
  Membership.mem (γ := Subring B) (RingHom.range.{u_1, u_2} (R := A) (algebraMap A B)) x → degree (minpoly A x) = 1
⊢ degree (minpoly A x) = 1 ↔ Membership.mem (γ := Subring B) (RingHom.range.{u_1, u_2} (R := A) (algebraMap A B)) x

Tactic:
refine ⟨minpoly.mem_range_of_degree_eq_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
inst_3 : Nontrivial B
x : A
⊢ Nontrivial A

Tactic:
haveI := Module.nontrivial A B
-- 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
inst_3 : Nontrivial B
x : A
this : Nontrivial A
⊢ Eq.{u_2 + 1} (α := B)
    (((Polynomial.aeval ((algebraMap A B : (a : A) → B) x) : A[X] →ₐ[A] B) : (a : A[X]) → B)
        (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) x : A[X])) :
      B)
    (0 : B)

Tactic:
simp
-- 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
inst_3 : Nontrivial B
x : A
this : Nontrivial A
⊢ degree (minpoly.{u_1, u_2} A (B := B) (((algebraMap A B : A →+* B) : (a : A) → B) x : B)) = 1

Tactic:
exact (degree_X_sub_C x ▸ minpoly.min A (algebraMap A B x) (monic_X_sub_C x) (by simp)).antisymm
    (Nat.WithBot.add_one_le_of_lt <| minpoly.degree_pos isIntegral_algebraMap)
-- 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
rw :
  degree (minpoly A x) = (↑1 : WithBot ℕ) ↔
    Membership.mem (γ := Subring B) (RingHom.range.{u_1, u_2} (R := A) (algebraMap A B)) x
⊢ natDegree (minpoly A x) = 1 ↔ Membership.mem (γ := Subring B) (RingHom.range.{u_1, u_2} (R := A) (algebraMap A B)) x

Tactic:
rw [← Polynomial.degree_eq_iff_natDegree_eq_of_pos zero_lt_one]

Premises used: Polynomial.degree_eq_iff_natDegree_eq_of_pos, zero_lt_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
inst_3 : Nontrivial B
⊢ degree (minpoly A x) = (↑1 : WithBot ℕ) ↔
    Membership.mem (γ := Subring B) (RingHom.range.{u_1, u_2} (R := A) (algebraMap A B)) x

Tactic:
degree_eq_one_iff

Premises used: minpoly.degree_eq_one_iff
-- 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
⊢ degree (minpoly A x) = (↑1 : WithBot ℕ) ↔
    Membership.mem (γ := Subring B) (RingHom.range.{u_1, u_2} (R := A) (algebraMap A B)) x

Tactic:
exact degree_eq_one_iff

Premises used: minpoly.degree_eq_one_iff
-- 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
int : IsIntegral A x
rw : natDegree (minpoly A x) = 1 ↔ natDegree (minpoly A x) < 2
⊢ 2 ≤ natDegree (minpoly A x) ↔ x ∉ RingHom.range.{u_1, u_2} (R := A) (algebraMap A B)

Tactic:
rw [iff_not_comm, ← natDegree_eq_one_iff, not_le]

Premises used: not_le, iff_not_comm, minpoly.natDegree_eq_one_iff
-- 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
int : IsIntegral A x
h : natDegree (minpoly A x) < 2
linarith :
  natDegree (minpoly A x) < 1 →
    -1 + (HAdd.hAdd (α := ℤ) (↑(natDegree (minpoly A x)) : ℤ) 1 - 1) +
        (HAdd.hAdd (α := ℤ) 0 1 - (↑(natDegree (minpoly A x)) : ℤ)) =
      0
linarith₁ :
  1 < natDegree (minpoly A x) →
    -1 + (HAdd.hAdd (α := ℤ) 1 1 - (↑(natDegree (minpoly A x)) : ℤ)) +
        (HAdd.hAdd (α := ℤ) (↑(natDegree (minpoly A x)) : ℤ) 1 - 2) =
      0
⊢ natDegree (minpoly A x) = 1

Tactic:
linarith only [minpoly.natDegree_pos int, h]

Premises used: minpoly.natDegree_pos
-- 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
int : IsIntegral A x
⊢ natDegree (minpoly A x) = 1 ↔ natDegree (minpoly A x) < 2

Tactic:
exact ⟨fun h ↦ h.trans_lt one_lt_two, fun h ↦ by linarith only [minpoly.natDegree_pos int, h]⟩
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
inst : CommRing A
B : Type u_4
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Nontrivial B
S : Subalgebra A B
x : B
int : IsIntegral (↥S) x
rw : Membership.mem (γ := Subring B) (RingHom.range (R := ↥S) (algebraMap (↥S) B)) x ↔ x ∈ S
⊢ 2 ≤ natDegree (R := ↥S) (minpoly (↥S) x) ↔ x ∉ S

Tactic:
rw [two_le_natDegree_iff int, Iff.not]

Premises used: minpoly.two_le_natDegree_iff, Iff.not
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
inst : CommRing A
B : Type u_4
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Nontrivial B
S : Subalgebra A B
x : B
int : IsIntegral (↥S) x
⊢ Membership.mem (γ := Subring B) (RingHom.range (R := ↥S) (algebraMap (↥S) B)) x ↔ x ∈ S

Tactic:
apply Set.ext_iff.mp Subtype.range_val_subtype

Premises used: Subtype.range_val_subtype, Iff.mp, Set.ext_iff
-- 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
a : A
hf : Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → 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
a : A
hf : Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
h : Nontrivial A
⊢ minpoly.{u_1, u_2} A (B := B) ((algebraMap A B : (a : A) → B) a : B) =
    HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X])

Tactic:
(unique' A _ (monic_X_sub_C a) ?_ ?_).symm

Premises used: Polynomial.monic_X_sub_C, Eq.symm, minpoly.unique'
-- 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
a : A
hf : Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
h : Nontrivial A
refine_1 :
  Eq.{u_2 + 1} (α := B)
    (((Polynomial.aeval ((algebraMap A B : (a : A) → B) a) : A[X] →ₐ[A] B) : (a : A[X]) → B)
        (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X])) :
      B)
    (0 : B)
refine_2 :
  ∀ (q : A[X]),
    q.degree < (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X])).degree →
      q = 0 ∨
        Ne.{u_2 + 1} (α := B)
          (((Polynomial.aeval ((algebraMap A B : (a : A) → B) a) : A[X] →ₐ[A] B) : (a : A[X]) → B) q : B) (0 : B)
⊢ minpoly.{u_1, u_2} A (B := B) ((algebraMap A B : (a : A) → B) a : B) =
    HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X])

Tactic:
refine (unique' A _ (monic_X_sub_C a) ?_ ?_).symm

Premises used: Polynomial.monic_X_sub_C, Eq.symm, minpoly.unique'
-- 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
a : A
hf : Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
h : Nontrivial A
refine_1 :
  HSub.hSub (α := B) (β := B)
      (((Polynomial.aeval ((algebraMap A B : (a : A) → B) a) : A[X] →ₐ[A] B) : (a : A[X]) → B) X : B)
      (((Polynomial.aeval ((algebraMap A B : (a : A) → B) a) : A[X] →ₐ[A] B) : (a : A[X]) → B)
          ((C : (a : A) → A[X]) a : A[X]) :
        B) =
    0
refine_1₁ :
  HSub.hSub (α := B) (β := B)
      (((Polynomial.aeval ((algebraMap A B : (a : A) → B) a) : A[X] →ₐ[A] B) : (a : A[X]) → B) X : B)
      ((algebraMap A B : (a : A) → B) a : B) =
    0
refine_1₂ :
  HSub.hSub (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((algebraMap A B : (a : A) → B) a : B) = 0
refine_1₃ refine_1₄ : Eq.{u_2 + 1} (α := B) 0 0
⊢ Eq.{u_2 + 1} (α := B)
    (((Polynomial.aeval ((algebraMap A B : (a : A) → B) a) : A[X] →ₐ[A] B) : (a : A[X]) → B)
        (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X])) :
      B)
    (0 : B)

Tactic:
rw [map_sub, aeval_C, aeval_X, sub_self]

Premises used: map_sub, sub_self, Polynomial.aeval_C, 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
a : A
hf : Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
h : Nontrivial A
refine_2 :
  ∀ (q : A[X]),
    q.degree < (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X])).degree →
      ¬q = 0 →
        Ne.{u_2 + 1} (α := B)
          (((Polynomial.aeval ((algebraMap A B : (a : A) → B) a) : A[X] →ₐ[A] B) : (a : A[X]) → B) q : B) (0 : B)
⊢ ∀ (q : A[X]),
    q.degree < (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X])).degree →
      q = 0 ∨
        Ne.{u_2 + 1} (α := B)
          (((Polynomial.aeval ((algebraMap A B : (a : A) → B) a) : A[X] →ₐ[A] B) : (a : A[X]) → B) q : B) (0 : B)

Tactic:
simp_rw [or_iff_not_imp_left]

Premises used: Classical.or_iff_not_imp_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
a : A
hf : Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
h : Nontrivial A
q : A[X]
hl : q.degree < (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X])).degree
h0 : ¬q = 0
⊢ q.natDegree = 0

Tactic:
rw [← natDegree_lt_natDegree_iff h0, natDegree_X_sub_C, Nat.lt_one_iff] at hl

Premises used: Polynomial.natDegree_lt_natDegree_iff, Polynomial.natDegree_X_sub_C, Nat.lt_one_iff
-- 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
a : A
hf : Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
h : Nontrivial A
q : A[X]
hl : q.degree < (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X])).degree
h0 : ¬q = 0
hl₁ : q.natDegree = 0
⊢ ¬q = 0

Tactic:
rw [← natDegree_lt_natDegree_iff h0, natDegree_X_sub_C, Nat.lt_one_iff] at hl

Premises used: Polynomial.natDegree_lt_natDegree_iff, Polynomial.natDegree_X_sub_C, Nat.lt_one_iff
-- 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
a : A
hf : Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
h : Nontrivial A
q : A[X]
hl : q.natDegree = 0
h0 : ¬q = 0
refine_2 :
  ∀ (h0 : ¬Eq (α := A[X]) ((C : (a : A) → A[X]) (q.coeff 0) : A[X]) (0 : A[X])),
    Ne.{u_2 + 1} (α := B)
      (((Polynomial.aeval ((algebraMap A B : (a : A) → B) a) : A[X] →ₐ[A] B) : (a : A[X]) → B)
          ((C : (a : A) → A[X]) (q.coeff 0) : A[X]) :
        B)
      (0 : B)
⊢ Ne.{u_2 + 1} (α := B) (((Polynomial.aeval ((algebraMap A B : (a : A) → B) a) : A[X] →ₐ[A] B) : (a : A[X]) → B) q : B)
    (0 : B)

Tactic:
rw [eq_C_of_natDegree_eq_zero hl] at h0 ⊢

Premises used: Polynomial.eq_C_of_natDegree_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
a : A
hf : Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
h : Nontrivial A
q : A[X]
hl : q.natDegree = 0
h0 : ¬Eq (α := A[X]) ((C : (a : A) → A[X]) (q.coeff 0) : A[X]) (0 : A[X])
refine_2 : Ne.{u_2 + 1} (α := B) ((algebraMap A B : (a : A) → B) (q.coeff 0) : B) (0 : B)
refine_2₁ : q.coeff 0 ≠ 0
refine_2₂ refine_2₃ refine_2₄ refine_2₅ : Ne (α := A[X]) ((C : (a : A) → A[X]) (q.coeff 0) : A[X]) (0 : A[X])
⊢ Ne.{u_2 + 1} (α := B)
    (((Polynomial.aeval ((algebraMap A B : (a : A) → B) a) : A[X] →ₐ[A] B) : (a : A[X]) → B)
        ((C : (a : A) → A[X]) (q.coeff 0) : A[X]) :
      B)
    (0 : B)

Tactic:
rwa [aeval_C, map_ne_zero_iff _ hf, ← C_ne_zero]

Premises used: Polynomial.aeval_C, map_ne_zero_iff, Polynomial.C_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
a : A[X]
hx : IsIntegral A x
hamonic : a.Monic
hdvd : DvdNotUnit a (minpoly A x)
⊢ Ne.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) a : B) (0 : B)

Tactic:
fun ha => (min A x hamonic ha).not_gt (degree_lt_degree ?_)

Premises used: minpoly.min, LE.le.not_gt, Polynomial.degree_lt_degree, Not
-- 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
a : A[X]
hx : IsIntegral A x
hamonic : a.Monic
hdvd : DvdNotUnit a (minpoly A x)
refine :
  ∀ (ha : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) a : B) (0 : B)),
    a.natDegree < natDegree (minpoly A x)
⊢ Ne.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) a : B) (0 : B)

Tactic:
refine fun ha => (min A x hamonic ha).not_gt (degree_lt_degree ?_)

Premises used: minpoly.min, LE.le.not_gt, Polynomial.degree_lt_degree
-- 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
a : A[X]
hx : IsIntegral A x
hamonic : a.Monic
hdvd : DvdNotUnit a (minpoly A x)
ha : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) a : B) (0 : B)
obtain : a ≠ 0 → ∀ (c : A[X]) (hu : ¬IsUnit c) (he : minpoly A x = a * c), a.natDegree < natDegree (minpoly A x)
⊢ a.natDegree < natDegree (minpoly A x)

Tactic:
obtain ⟨_, c, hu, he⟩ := hdvd
-- 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
a : A[X]
hx : IsIntegral A x
hamonic : a.Monic
ha : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) a : B) (0 : B)
left : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
⊢ c.Monic

Tactic:
have hcm := hamonic.of_mul_monic_left (he.subst <| monic 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
a : A[X]
hx : IsIntegral A x
hamonic : a.Monic
ha : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) a : B) (0 : B)
left : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : c.Monic
rw : a.natDegree < a.natDegree + c.natDegree
⊢ a.natDegree < natDegree (minpoly A x)

Tactic:
rw [he, hamonic.natDegree_mul hcm]

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
a : A[X]
hx : IsIntegral A x
hamonic : a.Monic
ha : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) a : B) (0 : B)
left : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : c.Monic
h : 0 < c.natDegree
⊢ a.natDegree < a.natDegree + c.natDegree

Tactic:
apply lt_add_of_pos_right

Premises used: lt_add_of_pos_right
-- 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
a : A[X]
hx : IsIntegral A x
hamonic : a.Monic
ha : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) a : B) (0 : B)
left : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : c.Monic
⊢ 0 < c.natDegree

Tactic:
(lt_of_not_ge fun h => hu ?_)

Premises used: lt_of_not_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
a : A[X]
hx : IsIntegral A x
hamonic : a.Monic
ha : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) a : B) (0 : B)
left : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : c.Monic
h : ∀ (h : c.natDegree ≤ 0), IsUnit c
⊢ 0 < c.natDegree

Tactic:
refine (lt_of_not_ge fun h => hu ?_)

Premises used: lt_of_not_ge