awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
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
⊢ r.natDegree ≤ 0
have a : ℕ
Tactic: apply Nat.le_of_add_le_add_left
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (hypothesis)
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
⊢ p = p * r
have this : 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)
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
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
⊢ p = p * r
have inl : p = HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) (r.coeff 0) : A[X])
Tactic: rw [eq_C_of_natDegree_le_zero this, ← Nat.eq_zero_of_le_zero this, ← leadingCoeff, ← hlead, C_1,
    mul_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
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])
⊢ p = p * r
have inl₁ : p = HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) (r.coeff r.natDegree) : A[X])
Tactic: rw [eq_C_of_natDegree_le_zero this, ← Nat.eq_zero_of_le_zero this, ← leadingCoeff, ← hlead, C_1,
    mul_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
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])
⊢ p = p * r
have inl₂ : p = HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) r.leadingCoeff : A[X])
Tactic: rw [eq_C_of_natDegree_le_zero this, ← Nat.eq_zero_of_le_zero this, ← leadingCoeff, ← hlead, C_1,
    mul_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
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])
⊢ p = p * r
have inl₃ : p = p * (C : (a : A) → A[X]) 1
Tactic: rw [eq_C_of_natDegree_le_zero this, ← Nat.eq_zero_of_le_zero this, ← leadingCoeff, ← hlead, C_1,
    mul_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
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
⊢ p = p * r
have inl₄ : p = p * 1
Tactic: rw [eq_C_of_natDegree_le_zero this, ← Nat.eq_zero_of_le_zero this, ← leadingCoeff, ← hlead, C_1,
    mul_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
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
⊢ p = p * r
have inl₅ : p = p
Tactic: rw [eq_C_of_natDegree_le_zero this, ← Nat.eq_zero_of_le_zero this, ← leadingCoeff, ← hlead, C_1,
    mul_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
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 : ℕ
⊢ q.coeff i = coeff 0 i
have 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
Tactic: rw [q.as_sum_range' _ ((natDegree_lt_iff_degree_lt ne).mpr (hpn ▸ lt))] at hq
Cleared hypotheses: hq, i
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
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 : ℕ
⊢ q.coeff i = coeff 0 i
have inl : ∀ (lt : i < n), q.coeff i = coeff 0 i
Tactic: obtain lt | le := lt_or_ge i n
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
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
⊢ q.coeff i = coeff 0 i
have inr : ∀ (le : n ≤ i), q.coeff i = coeff 0 i
Tactic: obtain lt | le := lt_or_ge i n
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (hypothesis)
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
⊢ Eq (α := A[X]) (minpoly A x) 1
have a : Nontrivial A
Tactic: nontriviality A
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (hypothesis)
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
⊢ Eq (α := A[X]) (minpoly A x) 1
have this : degree (minpoly A x) ≤ degree.{u_1} (R := A) 1
Tactic: have := minpoly.min A x monic_one (Subsingleton.elim _ _)
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (hypothesis)
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
⊢ Eq (α := A[X]) (minpoly A x) 1
have this₁ : degree (minpoly A x) ≤ 0
Tactic: rw [degree_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
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
⊢ Eq (α := A[X]) (minpoly A x) 1
have inl : ∀ (h : degree (minpoly A x) ≤ 0), Eq (α := A[X]) (minpoly A x) 1
Tactic: rcases le_or_gt (minpoly A x).degree 0 with h | h
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
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
⊢ Eq (α := A[X]) (minpoly A x) 1
have inr : ∀ (h : 0 < degree (minpoly A x)), Eq (α := A[X]) (minpoly A x) 1
Tactic: rcases le_or_gt (minpoly A x).degree 0 with h | h
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
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
⊢ Eq (α := A[X]) (minpoly A x) 1
have inl : ∀ (h : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
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 < natDegree (minpoly A x)
have rw : natDegree (minpoly A x) ≠ 0
Tactic: rw [pos_iff_ne_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
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
have rw : Eq (α := A[X]) ((C : (a : A) → A[X]) (coeff (minpoly A x) 0) : A[X]) (1 : A[X])
Tactic: rw [eq_C_of_natDegree_eq_zero ndeg_eq_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
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]) ((C : (a : A) → A[X]) (coeff (minpoly A x) 0) : A[X]) (1 : A[X])
have h : coeff (minpoly A x) 0 = 1
Tactic: convert! C_1 (R := A)
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (hypothesis)
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
⊢ False
have eq_one : 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
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
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
have refine : Membership.mem (γ := Subring B) (RingHom.range.{u_1, u_2} (R := A) (algebraMap A B)) x → degree (minpoly A x) = 1
Tactic: refine ⟨minpoly.mem_range_of_degree_eq_one _ _, ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (hypothesis)
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
⊢ degree (minpoly.{u_1, u_2} A (B := B) (((algebraMap A B : A →+* B) : (a : A) → B) x : B)) = 1
have this : Nontrivial A
Tactic: haveI := Module.nontrivial A B
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
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
⊢ natDegree (minpoly A x) = 1 ↔ Membership.mem (γ := Subring B) (RingHom.range.{u_1, u_2} (R := A) (algebraMap A B)) x
have rw : degree (minpoly A x) = (↑1 : WithBot ℕ) ↔
  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]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
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
⊢ 2 ≤ natDegree (minpoly A x) ↔ x ∉ RingHom.range.{u_1, u_2} (R := A) (algebraMap A B)
have rw : natDegree (minpoly A x) = 1 ↔ natDegree (minpoly A x) < 2
Tactic: rw [iff_not_comm, ← natDegree_eq_one_iff, not_le]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
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
⊢ natDegree (minpoly A x) = 1
have linarith : natDegree (minpoly A x) < 1 →
  -1 + (HAdd.hAdd (α := ℤ) (↑(natDegree (minpoly A x)) : ℤ) 1 - 1) +
      (HAdd.hAdd (α := ℤ) 0 1 - (↑(natDegree (minpoly A x)) : ℤ)) =
    0
Tactic: linarith only [minpoly.natDegree_pos int, h]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
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
⊢ natDegree (minpoly A x) = 1
have linarith₁ : 1 < natDegree (minpoly A x) →
  -1 + (HAdd.hAdd (α := ℤ) 1 1 - (↑(natDegree (minpoly A x)) : ℤ)) +
      (HAdd.hAdd (α := ℤ) (↑(natDegree (minpoly A x)) : ℤ) 1 - 2) =
    0
Tactic: linarith only [minpoly.natDegree_pos int, h]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
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
⊢ 2 ≤ natDegree (R := ↥S) (minpoly (↥S) x) ↔ x ∉ S
have rw : Membership.mem (γ := Subring B) (RingHom.range (R := ↥S) (algebraMap (↥S) B)) x ↔ x ∈ S
Tactic: rw [two_le_natDegree_iff int, Iff.not]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (hypothesis)
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)
⊢ 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])
have a₁ : Nontrivial A
Tactic: nontriviality A
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
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])
have 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)
Tactic: refine (unique' A _ (monic_X_sub_C a) ?_ ?_).symm
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
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)
⊢ 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])
have 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)
Tactic: refine (unique' A _ (monic_X_sub_C a) ?_ ?_).symm
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
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
⊢ 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)
have 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
Tactic: rw [map_sub, aeval_C, aeval_X, sub_self]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
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
⊢ 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)
have 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
Tactic: rw [map_sub, aeval_C, aeval_X, sub_self]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
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
⊢ 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)
have refine_1₂ : HSub.hSub (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((algebraMap A B : (a : A) → B) a : B) = 0
Tactic: rw [map_sub, aeval_C, aeval_X, sub_self]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
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
⊢ 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)
have refine_1₃ : Eq.{u_2 + 1} (α := B) 0 0
Tactic: rw [map_sub, aeval_C, aeval_X, sub_self]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
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]),
    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)
have 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)
Tactic: simp_rw [or_iff_not_imp_left]