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
B' : Type u_3
inst : CommRing A
inst_1 : Ring B
inst_2 : Ring B'
inst_3 : Algebra A B
inst_4 : Algebra A B'
f : B →ₐ[A] B'
hf : Injective.{u_2 + 1, u_3 + 1} (α := B) (β := B') (⇑f : (a : B) → B')
x : B
simp_rw :
  Eq.{u_1 + 1} (α := A[X])
    (if hx : IsIntegral.{u_1, u_3} A (A := B') ((f : (a : B) → B') x : B') 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') ((f : (a : B) → B') x) x_1 = 0) hx
    else 0)
    (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)
simp_rw₁ :
  Eq.{u_1 + 1} (α := A[X])
    (if h : 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') ((f : (a : B) → B') x) x_1 = 0) ⋯
    else 0)
    (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)
simp_rw₂ :
  Eq.{u_1 + 1} (α := A[X])
    (if h : IsIntegral A x then
      WellFounded.min (r := fun (p q : A[X]) ↦ p.degree < q.degree) ⋯
        (fun (x_1 : A[X]) ↦
          x_1.Monic ∧
            Eq.{u_3 + 1} (α := B') (((aeval ((f : (a : B) → B') x) : A[X] →ₐ[A] B') : (a : A[X]) → B') x_1 : B')
              (0 : B'))
        ⋯
    else 0)
    (if h : IsIntegral A x then
      WellFounded.min (r := fun (p q : A[X]) ↦ p.degree < q.degree) ⋯
        (fun (x_1 : A[X]) ↦ x_1.Monic ∧ Eq.{u_2 + 1} (α := B) ((aeval x : (a : A[X]) → B) x_1 : B) (0 : B)) ⋯
    else 0)
simp_rw₃ :
  Eq.{u_1 + 1} (α := A[X])
    (if h : IsIntegral A x then
      WellFounded.min (r := fun (p q : A[X]) ↦ p.degree < q.degree) ⋯
        (fun (x_1 : A[X]) ↦ x_1.Monic ∧ Eq.{u_3 + 1} (α := B') ((f.comp (aeval x) : (a : A[X]) → B') x_1 : B') (0 : B'))
        ⋯
    else 0)
    (if h : IsIntegral A x then
      WellFounded.min (r := fun (p q : A[X]) ↦ p.degree < q.degree) ⋯
        (fun (x_1 : A[X]) ↦ x_1.Monic ∧ Eq.{u_2 + 1} (α := B) ((aeval x : (a : A[X]) → B) x_1 : B) (0 : B)) ⋯
    else 0)
⊢ Eq (α := A[X]) (minpoly.{u_1, u_3} A (B := B') ((f : (a : B) → B') x : B')) (minpoly A x)
have simp_rw₄ : Eq.{u_1 + 1} (α := A[X])
  (if h : IsIntegral A x then
    WellFounded.min (r := fun (p q : A[X]) ↦ p.degree < q.degree) sorry
      (fun (x_1 : A[X]) ↦
        x_1.Monic ∧ Eq.{u_3 + 1} (α := B') ((f : (a : B) → B') ((aeval x : (a : A[X]) → B) x_1 : B) : B') (0 : B'))
      sorry
  else 0)
  (if h : IsIntegral A x then
    WellFounded.min (r := fun (p q : A[X]) ↦ p.degree < q.degree) sorry
      (fun (x_1 : A[X]) ↦ x_1.Monic ∧ Eq.{u_2 + 1} (α := B) ((aeval x : (a : A[X]) → B) x_1 : B) (0 : B)) sorry
  else 0)
Tactic: classical
  simp_rw [minpoly, isIntegral_algHom_iff _ hf, ← Polynomial.aeval_def, aeval_algHom,
    AlgHom.comp_apply, _root_.map_eq_zero_iff f hf]
-- 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
⊢ Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) (minpoly A x) : B) (0 : B)
have delta : Eq.{u_2 + 1} (α := B)
  ((Polynomial.aeval x : (a : A[X]) → B)
      (if hx : IsIntegral A x then
        WellFounded.min (r := fun (p q : A[X]) ↦ p.degree < q.degree) sorry
          (fun (x_1 : A[X]) ↦ x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx
      else 0) :
    B)
  (0 : B)
Tactic: delta minpoly
-- 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
⊢ Eq.{u_2 + 1} (α := B)
    ((Polynomial.aeval x : (a : A[X]) → B)
        (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) :
      B)
    (0 : B)
have pos : ∀ (hx : IsIntegral A x),
  Eq.{u_2 + 1} (α := B)
    ((Polynomial.aeval x : (a : A[X]) → B)
        (WellFounded.min (r := fun (p q : A[X]) ↦ p.degree < q.degree) sorry
          (fun (x_1 : A[X]) ↦ x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx) :
      B)
    (0 : B)
Tactic: split_ifs with hx
-- 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
pos :
  ∀ (hx : IsIntegral A x),
    Eq.{u_2 + 1} (α := B)
      ((Polynomial.aeval x : (a : A[X]) → B)
          (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) :
        B)
      (0 : B)
⊢ Eq.{u_2 + 1} (α := B)
    ((Polynomial.aeval x : (a : A[X]) → B)
        (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) :
      B)
    (0 : B)
have neg : ∀ (hx : ¬IsIntegral A x), Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) 0 : B) (0 : B)
Tactic: split_ifs with hx
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
B' : Type u_3
inst : CommRing A
inst_1 : Ring B
inst_2 : Ring B'
inst_3 : Algebra A B
inst_4 : Algebra A B'
f : B →ₐ[A] B'
x : B
⊢ Eq.{u_3 + 1} (α := B')
    (((Polynomial.aeval ((f : (a : B) → B') x) : A[X] →ₐ[A] B') : (a : A[X]) → B') (minpoly A x) : B') (0 : B')
have rw : Eq.{u_3 + 1} (α := B') ((f.comp (Polynomial.aeval x) : (a : A[X]) → B') (minpoly A x) : B') (0 : B')
Tactic: rw [Polynomial.aeval_algHom, AlgHom.coe_comp, comp_apply, aeval, map_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
B' : Type u_3
inst : CommRing A
inst_1 : Ring B
inst_2 : Ring B'
inst_3 : Algebra A B
inst_4 : Algebra A B'
f : B →ₐ[A] B'
x : B
rw : Eq.{u_3 + 1} (α := B') ((f.comp (Polynomial.aeval x) : (a : A[X]) → B') (minpoly A x) : B') (0 : B')
⊢ Eq.{u_3 + 1} (α := B')
    (((Polynomial.aeval ((f : (a : B) → B') x) : A[X] →ₐ[A] B') : (a : A[X]) → B') (minpoly A x) : B') (0 : B')
have rw₁ : Eq.{u_3 + 1} (α := B')
  (Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} (α := A[X]) (β := B) (⇑f : (a : B) → B')
    (⇑(Polynomial.aeval x) : (a : A[X]) → B) (minpoly A x))
  0
Tactic: rw [Polynomial.aeval_algHom, AlgHom.coe_comp, comp_apply, aeval, map_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
B' : Type u_3
inst : CommRing A
inst_1 : Ring B
inst_2 : Ring B'
inst_3 : Algebra A B
inst_4 : Algebra A B'
f : B →ₐ[A] B'
x : B
rw : Eq.{u_3 + 1} (α := B') ((f.comp (Polynomial.aeval x) : (a : A[X]) → B') (minpoly A x) : B') (0 : B')
rw₁ :
  Eq.{u_3 + 1} (α := B')
    (Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} (α := A[X]) (β := B) (⇑f : (a : B) → B')
      (⇑(Polynomial.aeval x) : (a : A[X]) → B) (minpoly A x))
    0
⊢ Eq.{u_3 + 1} (α := B')
    (((Polynomial.aeval ((f : (a : B) → B') x) : A[X] →ₐ[A] B') : (a : A[X]) → B') (minpoly A x) : B') (0 : B')
have rw₂ : Eq.{u_3 + 1} (α := B') ((f : (a : B) → B') ((Polynomial.aeval x : (a : A[X]) → B) (minpoly A x) : B) : B') (0 : B')
Tactic: rw [Polynomial.aeval_algHom, AlgHom.coe_comp, comp_apply, aeval, map_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
B' : Type u_3
inst : CommRing A
inst_1 : Ring B
inst_2 : Ring B'
inst_3 : Algebra A B
inst_4 : Algebra A B'
f : B →ₐ[A] B'
x : B
rw : Eq.{u_3 + 1} (α := B') ((f.comp (Polynomial.aeval x) : (a : A[X]) → B') (minpoly A x) : B') (0 : B')
rw₁ :
  Eq.{u_3 + 1} (α := B')
    (Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} (α := A[X]) (β := B) (⇑f : (a : B) → B')
      (⇑(Polynomial.aeval x) : (a : A[X]) → B) (minpoly A x))
    0
rw₂ :
  Eq.{u_3 + 1} (α := B') ((f : (a : B) → B') ((Polynomial.aeval x : (a : A[X]) → B) (minpoly A x) : B) : B') (0 : B')
⊢ Eq.{u_3 + 1} (α := B')
    (((Polynomial.aeval ((f : (a : B) → B') x) : A[X] →ₐ[A] B') : (a : A[X]) → B') (minpoly A x) : B') (0 : B')
have rw₃ : Eq.{u_3 + 1} (α := B') ((f : (a : B) → B') 0 : B') (0 : B')
Tactic: rw [Polynomial.aeval_algHom, AlgHom.coe_comp, comp_apply, aeval, map_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
B' : Type u_3
inst : CommRing A
inst_1 : Ring B
inst_2 : Ring B'
inst_3 : Algebra A B
inst_4 : Algebra A B'
f : B →ₐ[A] B'
x : B
rw : Eq.{u_3 + 1} (α := B') ((f.comp (Polynomial.aeval x) : (a : A[X]) → B') (minpoly A x) : B') (0 : B')
rw₁ :
  Eq.{u_3 + 1} (α := B')
    (Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} (α := A[X]) (β := B) (⇑f : (a : B) → B')
      (⇑(Polynomial.aeval x) : (a : A[X]) → B) (minpoly A x))
    0
rw₂ :
  Eq.{u_3 + 1} (α := B') ((f : (a : B) → B') ((Polynomial.aeval x : (a : A[X]) → B) (minpoly A x) : B) : B') (0 : B')
rw₃ : Eq.{u_3 + 1} (α := B') ((f : (a : B) → B') 0 : B') (0 : B')
⊢ Eq.{u_3 + 1} (α := B')
    (((Polynomial.aeval ((f : (a : B) → B') x) : A[X] →ₐ[A] B') : (a : A[X]) → B') (minpoly A x) : B') (0 : B')
have rw₄ : Eq.{u_3 + 1} (α := B') 0 0
Tactic: rw [Polynomial.aeval_algHom, AlgHom.coe_comp, comp_apply, aeval, map_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
h : Eq (α := A[X]) (minpoly A x) 1
⊢ False
have refine : Eq.{u_2 + 1} (α := B) 1 0
Tactic: refine (one_ne_zero : (1 : B) ≠ 0) ?_
-- 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
R : Type u_4
inst_4 : Semiring R
inst_5 : Nontrivial R
f : A →+* R
⊢ map f (minpoly A x) ≠ 1
have pos : ∀ (hx : IsIntegral A x), map f (minpoly A x) ≠ 1
Tactic: by_cases hx : IsIntegral A x
-- 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
R : Type u_4
inst_4 : Semiring R
inst_5 : Nontrivial R
f : A →+* R
pos : ∀ (hx : IsIntegral A x), map f (minpoly A x) ≠ 1
⊢ map f (minpoly A x) ≠ 1
have neg : ∀ (hx : ¬IsIntegral A x), map f (minpoly A x) ≠ 1
Tactic: by_cases hx : IsIntegral A x
-- 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
R : Type u_4
inst_4 : Semiring R
inst_5 : Nontrivial R
f : A →+* R
hx : ¬IsIntegral A x
⊢ map f (minpoly A x) ≠ 1
have neg : Ne.{u_4 + 1} (α := R[X]) 0 1
Tactic: rw [eq_zero hx, Polynomial.map_zero]
-- 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
⊢ ¬IsUnit (M := A[X]) (minpoly A x)
have this : Nontrivial A
Tactic: haveI : Nontrivial A := (algebraMap A B).domain_nontrivial
-- 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
this : Nontrivial A
⊢ ¬IsUnit (M := A[X]) (minpoly A x)
have pos : ∀ (hx : IsIntegral A x), ¬IsUnit (M := A[X]) (minpoly A x)
Tactic: by_cases hx : IsIntegral A x
-- 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
this : Nontrivial A
pos : ∀ (hx : IsIntegral A x), ¬IsUnit (M := A[X]) (minpoly A x)
⊢ ¬IsUnit (M := A[X]) (minpoly A x)
have neg : ∀ (hx : ¬IsIntegral A x), ¬IsUnit (M := A[X]) (minpoly A x)
Tactic: by_cases hx : IsIntegral A x
-- 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
this : Nontrivial A
hx : ¬IsIntegral A x
⊢ ¬IsUnit (M := A[X]) (minpoly A x)
have neg : ¬IsUnit.{u_1} (M := A[X]) 0
Tactic: rw [eq_zero hx]
-- 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
hx : degree (minpoly A x) = 1
⊢ IsIntegral A x
have by_contra : ∀ (h : ¬IsIntegral A x), False
Tactic: by_contra h
-- 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
hx : degree (minpoly A x) = 1
h : ¬IsIntegral A x
⊢ False
have hx₁ : Eq (α := WithBot ℕ) ⊥ (↑1 : WithBot ℕ)
Tactic: rw [eq_zero h, degree_zero, ← WithBot.coe_one] at hx
Cleared hypotheses: hx, h
-- 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
hx : degree (minpoly A x) = 1
⊢ Membership.mem (γ := Subring B) (RingHom.range.{u_1, u_2} (R := A) (algebraMap A B)) x
have h : 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
-- 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
hx : degree (minpoly A x) = 1
h : IsIntegral A x
⊢ Membership.mem (γ := Subring B) (RingHom.range.{u_1, u_2} (R := A) (algebraMap A B)) x
have key : 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
-- 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
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)
⊢ Membership.mem (γ := Subring B) (RingHom.range.{u_1, u_2} (R := A) (algebraMap A B)) x
have key₁ : 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
Cleared hypotheses: key
-- 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]
pmonic : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
⊢ 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
have pos : ∀ (hx : IsIntegral A x),
  (WellFounded.min (r := fun (p q : A[X]) ↦ p.degree < q.degree) sorry
        (fun (x_1 : A[X]) ↦ x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx).degree ≤
    p.degree
Tactic: split_ifs with hx
-- 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]
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
⊢ 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
have neg : ∀ (hx : ¬IsIntegral A x), degree.{u_1} (R := A) 0 ≤ p.degree
Tactic: split_ifs with hx
-- 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]
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
have pos : Membership.mem (γ := Set A[X]) (fun (x_1 : A[X]) ↦ x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) p
Tactic: refine le_of_not_gt <| degree_lt_wf.not_lt_min _ ?_
-- 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)
⊢ p = minpoly A x
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
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
⊢ p = minpoly A x
have hx : IsIntegral A x
Tactic: have hx : IsIntegral A x := ⟨p, 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 : Nontrivial A
hx : IsIntegral A x
⊢ p = minpoly A x
have inl : ∀ (h : minpoly A x %ₘ p = 0), p = minpoly A x
Tactic: obtain h | h := hl _ ((minpoly A x).degree_modByMonic_lt hm)
-- 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 : Nontrivial A
hx : IsIntegral A x
inl : ∀ (h : minpoly A x %ₘ p = 0), p = minpoly A x
⊢ p = minpoly A x
have 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
Tactic: obtain h | h := hl _ ((minpoly A x).degree_modByMonic_lt hm)
-- 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
⊢ p = minpoly A x
have inl : ∀ (r : A[X]) (hr : minpoly A x = p * r), p = minpoly A x
Tactic: obtain ⟨r, hr⟩ := (modByMonic_eq_zero_iff_dvd hm).1 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
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
⊢ p = minpoly A x
have inl : p = p * r
Tactic: rw [hr]
-- 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
⊢ p = p * r
have hlead : leadingCoeff (minpoly A x) = (p * r).leadingCoeff
Tactic: have hlead := congr_arg leadingCoeff hr
-- 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 : leadingCoeff (minpoly A x) = (p * r).leadingCoeff
⊢ p = p * r
have hlead₁ : 1 = r.leadingCoeff
Tactic: rw [mul_comm, leadingCoeff_mul_monic hm, (monic hx).leadingCoeff] at hlead
Cleared hypotheses: hlead
-- 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
⊢ r.natDegree ≤ 0
have hr0 : r ≠ 0
Tactic: have hr0 : r ≠ 0 := by
      rintro rfl
      exact ne_zero hx (mul_zero p ▸ hr)
-- 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
hr0 : r ≠ 0
⊢ r.natDegree ≤ 0
have hr₁ : natDegree (minpoly A x) = (p * r).natDegree
Tactic: apply_fun natDegree at hr
Cleared hypotheses: hr
-- 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]
hlead : 1 = r.leadingCoeff
hr0 : r ≠ 0
hr : natDegree (minpoly A x) = (p * r).natDegree
⊢ r.natDegree ≤ 0
have hr₁ : natDegree (minpoly A x) = p.natDegree + r.natDegree
Tactic: rw [hm.natDegree_mul' hr0] at hr
Cleared hypotheses: hr
-- 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
⊢ r.natDegree ≤ 0
have h₁ : p.natDegree + r.natDegree ≤ p.natDegree + 0
Tactic: apply Nat.le_of_add_le_add_left