awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
this : p.leadingCoeff ≠ 0
hp3 : (HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X])).leadingCoeff = 1
hp3₁ : p.leadingCoeff * leadingCoeff ((C : (a : A) → A[X]) p.leadingCoeff⁻¹) = 1
⊢ (HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X])).Monic
have hp3₂ : p.leadingCoeff * p.leadingCoeff⁻¹ = 1
Tactic: rwa [Polynomial.Monic, leadingCoeff_mul, leadingCoeff_C, mul_inv_cancel₀]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
this : p.leadingCoeff ≠ 0
hp3 : (HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X])).leadingCoeff = 1
hp3₁ : p.leadingCoeff * leadingCoeff ((C : (a : A) → A[X]) p.leadingCoeff⁻¹) = 1
hp3₂ : p.leadingCoeff * p.leadingCoeff⁻¹ = 1
⊢ (HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X])).Monic
have hp3₃ : Eq.{u_1 + 1} (α := A) 1 1
Tactic: rwa [Polynomial.Monic, leadingCoeff_mul, leadingCoeff_C, mul_inv_cancel₀]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : Nontrivial B
p : A[X]
hi : Irreducible p
hx : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
⊢ p = HMul.hMul (α := A[X]) (β := A[X]) ((C : (a : A) → A[X]) p.leadingCoeff : A[X]) (minpoly A x)
have rw : p =
  HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) p.leadingCoeff : A[X])
    (HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X]))
Tactic: rw [← minpoly.eq_of_irreducible hi hx, mul_comm, mul_assoc, ← C_mul,
    inv_mul_cancel₀ (leadingCoeff_ne_zero.mpr hi.ne_zero), C_1, mul_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : Nontrivial B
p : A[X]
hi : Irreducible p
hx : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
rw :
  p =
    HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) p.leadingCoeff : A[X])
      (HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X]))
⊢ p = HMul.hMul (α := A[X]) (β := A[X]) ((C : (a : A) → A[X]) p.leadingCoeff : A[X]) (minpoly A x)
have rw₁ : p =
  HMul.hMul (β := A[X]) (HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X]))
    ((C : (a : A) → A[X]) p.leadingCoeff : A[X])
Tactic: rw [← minpoly.eq_of_irreducible hi hx, mul_comm, mul_assoc, ← C_mul,
    inv_mul_cancel₀ (leadingCoeff_ne_zero.mpr hi.ne_zero), C_1, mul_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : Nontrivial B
p : A[X]
hi : Irreducible p
hx : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
rw :
  p =
    HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) p.leadingCoeff : A[X])
      (HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X]))
rw₁ :
  p =
    HMul.hMul (β := A[X]) (HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X]))
      ((C : (a : A) → A[X]) p.leadingCoeff : A[X])
⊢ p = HMul.hMul (α := A[X]) (β := A[X]) ((C : (a : A) → A[X]) p.leadingCoeff : A[X]) (minpoly A x)
have rw₂ : p =
  p *
    HMul.hMul (α := A[X]) (β := A[X]) ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X])
      ((C : (a : A) → A[X]) p.leadingCoeff : A[X])
Tactic: rw [← minpoly.eq_of_irreducible hi hx, mul_comm, mul_assoc, ← C_mul,
    inv_mul_cancel₀ (leadingCoeff_ne_zero.mpr hi.ne_zero), C_1, mul_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : Nontrivial B
p : A[X]
hi : Irreducible p
hx : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
rw :
  p =
    HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) p.leadingCoeff : A[X])
      (HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X]))
rw₁ :
  p =
    HMul.hMul (β := A[X]) (HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X]))
      ((C : (a : A) → A[X]) p.leadingCoeff : A[X])
rw₂ :
  p =
    p *
      HMul.hMul (α := A[X]) (β := A[X]) ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X])
        ((C : (a : A) → A[X]) p.leadingCoeff : A[X])
⊢ p = HMul.hMul (α := A[X]) (β := A[X]) ((C : (a : A) → A[X]) p.leadingCoeff : A[X]) (minpoly A x)
have rw₃ : p = HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) (p.leadingCoeff⁻¹ * p.leadingCoeff) : A[X])
Tactic: rw [← minpoly.eq_of_irreducible hi hx, mul_comm, mul_assoc, ← C_mul,
    inv_mul_cancel₀ (leadingCoeff_ne_zero.mpr hi.ne_zero), C_1, mul_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : Nontrivial B
p : A[X]
hi : Irreducible p
hx : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
rw :
  p =
    HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) p.leadingCoeff : A[X])
      (HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X]))
rw₁ :
  p =
    HMul.hMul (β := A[X]) (HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X]))
      ((C : (a : A) → A[X]) p.leadingCoeff : A[X])
rw₂ :
  p =
    p *
      HMul.hMul (α := A[X]) (β := A[X]) ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X])
        ((C : (a : A) → A[X]) p.leadingCoeff : A[X])
rw₃ : p = HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) (p.leadingCoeff⁻¹ * p.leadingCoeff) : A[X])
⊢ p = HMul.hMul (α := A[X]) (β := A[X]) ((C : (a : A) → A[X]) p.leadingCoeff : A[X]) (minpoly A x)
have rw₄ : p = p * (C : (a : A) → A[X]) 1
Tactic: rw [← minpoly.eq_of_irreducible hi hx, mul_comm, mul_assoc, ← C_mul,
    inv_mul_cancel₀ (leadingCoeff_ne_zero.mpr hi.ne_zero), C_1, mul_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : Nontrivial B
p : A[X]
hi : Irreducible p
hx : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
rw :
  p =
    HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) p.leadingCoeff : A[X])
      (HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X]))
rw₁ :
  p =
    HMul.hMul (β := A[X]) (HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X]))
      ((C : (a : A) → A[X]) p.leadingCoeff : A[X])
rw₂ :
  p =
    p *
      HMul.hMul (α := A[X]) (β := A[X]) ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X])
        ((C : (a : A) → A[X]) p.leadingCoeff : A[X])
rw₃ : p = HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) (p.leadingCoeff⁻¹ * p.leadingCoeff) : A[X])
rw₄ : p = p * (C : (a : A) → A[X]) 1
⊢ p = HMul.hMul (α := A[X]) (β := A[X]) ((C : (a : A) → A[X]) p.leadingCoeff : A[X]) (minpoly A x)
have rw₅ : p = p * 1
Tactic: rw [← minpoly.eq_of_irreducible hi hx, mul_comm, mul_assoc, ← C_mul,
    inv_mul_cancel₀ (leadingCoeff_ne_zero.mpr hi.ne_zero), C_1, mul_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : Nontrivial B
p : A[X]
hi : Irreducible p
hx : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
rw :
  p =
    HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) p.leadingCoeff : A[X])
      (HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X]))
rw₁ :
  p =
    HMul.hMul (β := A[X]) (HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X]))
      ((C : (a : A) → A[X]) p.leadingCoeff : A[X])
rw₂ :
  p =
    p *
      HMul.hMul (α := A[X]) (β := A[X]) ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X])
        ((C : (a : A) → A[X]) p.leadingCoeff : A[X])
rw₃ : p = HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) (p.leadingCoeff⁻¹ * p.leadingCoeff) : A[X])
rw₄ : p = p * (C : (a : A) → A[X]) 1
rw₅ : p = p * 1
⊢ p = HMul.hMul (α := A[X]) (β := A[X]) ((C : (a : A) → A[X]) p.leadingCoeff : A[X]) (minpoly A x)
have rw₆ : p = p
Tactic: rw [← minpoly.eq_of_irreducible hi hx, mul_comm, mul_assoc, ← C_mul,
    inv_mul_cancel₀ (leadingCoeff_ne_zero.mpr hi.ne_zero), C_1, mul_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
A : Type u_1
inst : Field A
B : Type u_3
inst_1 : CommRing B
inst_2 : Algebra A B
x : B
a : A
⊢ minpoly A (HAdd.hAdd (β := B) x ((algebraMap A B : (a : A) → B) a : B)) =
    Polynomial.comp (minpoly A x) (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))
have pos : ∀ (hx : IsIntegral A x),
  minpoly A (HAdd.hAdd (β := B) x ((algebraMap A B : (a : A) → B) a : B)) =
    Polynomial.comp (minpoly A x) (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))
Tactic: by_cases hx : IsIntegral A x
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
A : Type u_1
inst : Field A
B : Type u_3
inst_1 : CommRing B
inst_2 : Algebra A B
x : B
a : A
pos :
  ∀ (hx : IsIntegral A x),
    minpoly A (HAdd.hAdd (β := B) x ((algebraMap A B : (a : A) → B) a : B)) =
      Polynomial.comp (minpoly A x) (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))
⊢ minpoly A (HAdd.hAdd (β := B) x ((algebraMap A B : (a : A) → B) a : B)) =
    Polynomial.comp (minpoly A x) (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))
have neg : ∀ (hx : ¬IsIntegral A x),
  minpoly A (HAdd.hAdd (β := B) x ((algebraMap A B : (a : A) → B) a : B)) =
    Polynomial.comp (minpoly A x) (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))
Tactic: by_cases hx : IsIntegral A x
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
A : Type u_1
inst : Field A
B : Type u_3
inst_1 : CommRing B
inst_2 : Algebra A B
x : B
a : A
hx : IsIntegral A x
⊢ minpoly A (HAdd.hAdd (β := B) x ((algebraMap A B : (a : A) → B) a : B)) =
    Polynomial.comp (minpoly A x) (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))
have pos : Eq.{u_3 + 1} (α := B)
  ((Polynomial.aeval (HAdd.hAdd (β := B) x ((algebraMap A B : (a : A) → B) a : B)) : (a : A[X]) → B)
      (Polynomial.comp (minpoly A x) (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))) :
    B)
  (0 : B)
Tactic: refine (minpoly.unique _ _ ((minpoly.monic hx).comp_X_sub_C _) ?_ fun q qmo hq => ?_).symm
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
A : Type u_1
inst : Field A
B : Type u_3
inst_1 : CommRing B
inst_2 : Algebra A B
x : B
a : A
hx : IsIntegral A x
pos :
  Eq.{u_3 + 1} (α := B)
    ((Polynomial.aeval (HAdd.hAdd (β := B) x ((algebraMap A B : (a : A) → B) a : B)) : (a : A[X]) → B)
        (Polynomial.comp (minpoly A x) (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))) :
      B)
    (0 : B)
⊢ minpoly A (HAdd.hAdd (β := B) x ((algebraMap A B : (a : A) → B) a : B)) =
    Polynomial.comp (minpoly A x) (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))
have pos₁ : ∀ (q : A[X]) (qmo : q.Monic)
  (hq :
    Eq.{u_3 + 1} (α := B)
      ((Polynomial.aeval (HAdd.hAdd (β := B) x ((algebraMap A B : (a : A) → B) a : B)) : (a : A[X]) → B) q : B)
      (0 : B)),
  (Polynomial.comp (minpoly A x) (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))).degree ≤
    q.degree
Tactic: refine (minpoly.unique _ _ ((minpoly.monic hx).comp_X_sub_C _) ?_ fun q qmo hq => ?_).symm
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (hypothesis)
Goal:
A : Type u_1
inst : Field A
B : Type u_3
inst_1 : CommRing B
inst_2 : Algebra A B
x : B
a : A
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq :
  Eq.{u_3 + 1} (α := B)
    ((Polynomial.aeval (HAdd.hAdd (β := B) x ((algebraMap A B : (a : A) → B) a : B)) : (a : A[X]) → B) q : B) (0 : B)
⊢ (Polynomial.comp (minpoly A x) (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))).degree ≤
    q.degree
have this : Eq.{u_3 + 1} (α := B)
  ((Polynomial.aeval x : (a : A[X]) → B)
      (q.comp (HAdd.hAdd (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))) :
    B)
  (0 : B)
Tactic: have : (Polynomial.aeval x) (q.comp (X + C a)) = 0 := by simpa [aeval_comp] using hq
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (hypothesis)
Goal:
A : Type u_1
inst : Field A
B : Type u_3
inst_1 : CommRing B
inst_2 : Algebra A B
x : B
a : A
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq :
  Eq.{u_3 + 1} (α := B)
    ((Polynomial.aeval (HAdd.hAdd (β := B) x ((algebraMap A B : (a : A) → B) a : B)) : (a : A[X]) → B) q : B) (0 : B)
this :
  Eq.{u_3 + 1} (α := B)
    ((Polynomial.aeval x : (a : A[X]) → B)
        (q.comp (HAdd.hAdd (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))) :
      B)
    (0 : B)
⊢ (Polynomial.comp (minpoly A x) (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))).degree ≤
    q.degree
have H : degree (minpoly A x) ≤ (q.comp (HAdd.hAdd (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))).degree
Tactic: have H := minpoly.min A x (qmo.comp_X_add_C _) this
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
A : Type u_1
inst : Field A
B : Type u_3
inst_1 : CommRing B
inst_2 : Algebra A B
x : B
a : A
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq :
  Eq.{u_3 + 1} (α := B)
    ((Polynomial.aeval (HAdd.hAdd (β := B) x ((algebraMap A B : (a : A) → B) a : B)) : (a : A[X]) → B) q : B) (0 : B)
this :
  Eq.{u_3 + 1} (α := B)
    ((Polynomial.aeval x : (a : A[X]) → B)
        (q.comp (HAdd.hAdd (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))) :
      B)
    (0 : B)
H : degree (minpoly A x) ≤ (q.comp (HAdd.hAdd (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))).degree
⊢ (Polynomial.comp (minpoly A x) (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))).degree ≤
    q.degree
have pos : LE.le (α := WithBot ℕ) (↑(natDegree (minpoly A x)) : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
Tactic: rw [degree_eq_natDegree qmo.ne_zero,
        degree_eq_natDegree ((minpoly.monic hx).comp_X_sub_C _).ne_zero, natDegree_comp,
        natDegree_X_sub_C, mul_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
A : Type u_1
inst : Field A
B : Type u_3
inst_1 : CommRing B
inst_2 : Algebra A B
x : B
a : A
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq :
  Eq.{u_3 + 1} (α := B)
    ((Polynomial.aeval (HAdd.hAdd (β := B) x ((algebraMap A B : (a : A) → B) a : B)) : (a : A[X]) → B) q : B) (0 : B)
this :
  Eq.{u_3 + 1} (α := B)
    ((Polynomial.aeval x : (a : A[X]) → B)
        (q.comp (HAdd.hAdd (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))) :
      B)
    (0 : B)
H : degree (minpoly A x) ≤ (q.comp (HAdd.hAdd (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))).degree
⊢ LE.le (α := WithBot ℕ) (↑(natDegree (minpoly A x)) : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
have pos : ∀
  (H :
    (↑(natDegree (minpoly A x)) : WithBot ℕ) ≤
      (q.comp (HAdd.hAdd (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))).degree),
  LE.le (α := WithBot ℕ) (↑(natDegree (minpoly A x)) : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
Tactic: rwa [degree_eq_natDegree (minpoly.ne_zero hx),
        degree_eq_natDegree (qmo.comp_X_add_C _).ne_zero, natDegree_comp,
        natDegree_X_add_C, mul_one] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
A : Type u_1
inst : Field A
B : Type u_3
inst_1 : CommRing B
inst_2 : Algebra A B
x : B
a : A
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq :
  Eq.{u_3 + 1} (α := B)
    ((Polynomial.aeval (HAdd.hAdd (β := B) x ((algebraMap A B : (a : A) → B) a : B)) : (a : A[X]) → B) q : B) (0 : B)
this :
  Eq.{u_3 + 1} (α := B)
    ((Polynomial.aeval x : (a : A[X]) → B)
        (q.comp (HAdd.hAdd (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))) :
      B)
    (0 : B)
H : degree (minpoly A x) ≤ (q.comp (HAdd.hAdd (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))).degree
pos :
  ∀
    (H :
      (↑(natDegree (minpoly A x)) : WithBot ℕ) ≤
        (q.comp (HAdd.hAdd (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))).degree),
    LE.le (α := WithBot ℕ) (↑(natDegree (minpoly A x)) : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
⊢ LE.le (α := WithBot ℕ) (↑(natDegree (minpoly A x)) : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
have pos₁ : ∀
  (H :
    LE.le (α := WithBot ℕ) (↑(natDegree (minpoly A x)) : WithBot ℕ)
      (↑(q.comp (HAdd.hAdd (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))).natDegree : WithBot ℕ)),
  LE.le (α := WithBot ℕ) (↑(natDegree (minpoly A x)) : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
Tactic: rwa [degree_eq_natDegree (minpoly.ne_zero hx),
        degree_eq_natDegree (qmo.comp_X_add_C _).ne_zero, natDegree_comp,
        natDegree_X_add_C, mul_one] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
A : Type u_1
inst : Field A
B : Type u_3
inst_1 : CommRing B
inst_2 : Algebra A B
x : B
a : A
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq :
  Eq.{u_3 + 1} (α := B)
    ((Polynomial.aeval (HAdd.hAdd (β := B) x ((algebraMap A B : (a : A) → B) a : B)) : (a : A[X]) → B) q : B) (0 : B)
this :
  Eq.{u_3 + 1} (α := B)
    ((Polynomial.aeval x : (a : A[X]) → B)
        (q.comp (HAdd.hAdd (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))) :
      B)
    (0 : B)
H : degree (minpoly A x) ≤ (q.comp (HAdd.hAdd (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))).degree
pos :
  ∀
    (H :
      (↑(natDegree (minpoly A x)) : WithBot ℕ) ≤
        (q.comp (HAdd.hAdd (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))).degree),
    LE.le (α := WithBot ℕ) (↑(natDegree (minpoly A x)) : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
pos₁ :
  ∀
    (H :
      LE.le (α := WithBot ℕ) (↑(natDegree (minpoly A x)) : WithBot ℕ)
        (↑(q.comp (HAdd.hAdd (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))).natDegree : WithBot ℕ)),
    LE.le (α := WithBot ℕ) (↑(natDegree (minpoly A x)) : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
⊢ LE.le (α := WithBot ℕ) (↑(natDegree (minpoly A x)) : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
have pos₂ : ∀
  (H :
    LE.le (α := WithBot ℕ) (↑(natDegree (minpoly A x)) : WithBot ℕ)
      (↑(q.natDegree * (HAdd.hAdd (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X])).natDegree) : WithBot ℕ)),
  LE.le (α := WithBot ℕ) (↑(natDegree (minpoly A x)) : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
Tactic: rwa [degree_eq_natDegree (minpoly.ne_zero hx),
        degree_eq_natDegree (qmo.comp_X_add_C _).ne_zero, natDegree_comp,
        natDegree_X_add_C, mul_one] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
A : Type u_1
inst : Field A
B : Type u_3
inst_1 : CommRing B
inst_2 : Algebra A B
x : B
a : A
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq :
  Eq.{u_3 + 1} (α := B)
    ((Polynomial.aeval (HAdd.hAdd (β := B) x ((algebraMap A B : (a : A) → B) a : B)) : (a : A[X]) → B) q : B) (0 : B)
this :
  Eq.{u_3 + 1} (α := B)
    ((Polynomial.aeval x : (a : A[X]) → B)
        (q.comp (HAdd.hAdd (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))) :
      B)
    (0 : B)
H : degree (minpoly A x) ≤ (q.comp (HAdd.hAdd (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))).degree
pos :
  ∀
    (H :
      (↑(natDegree (minpoly A x)) : WithBot ℕ) ≤
        (q.comp (HAdd.hAdd (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))).degree),
    LE.le (α := WithBot ℕ) (↑(natDegree (minpoly A x)) : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
pos₁ :
  ∀
    (H :
      LE.le (α := WithBot ℕ) (↑(natDegree (minpoly A x)) : WithBot ℕ)
        (↑(q.comp (HAdd.hAdd (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))).natDegree : WithBot ℕ)),
    LE.le (α := WithBot ℕ) (↑(natDegree (minpoly A x)) : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
pos₂ :
  ∀
    (H :
      LE.le (α := WithBot ℕ) (↑(natDegree (minpoly A x)) : WithBot ℕ)
        (↑(q.natDegree * (HAdd.hAdd (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X])).natDegree) : WithBot ℕ)),
    LE.le (α := WithBot ℕ) (↑(natDegree (minpoly A x)) : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
⊢ LE.le (α := WithBot ℕ) (↑(natDegree (minpoly A x)) : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
have pos₃ : ∀ (H : LE.le (α := WithBot ℕ) (↑(natDegree (minpoly A x)) : WithBot ℕ) (↑(q.natDegree * 1) : WithBot ℕ)),
  LE.le (α := WithBot ℕ) (↑(natDegree (minpoly A x)) : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
Tactic: rwa [degree_eq_natDegree (minpoly.ne_zero hx),
        degree_eq_natDegree (qmo.comp_X_add_C _).ne_zero, natDegree_comp,
        natDegree_X_add_C, mul_one] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
A : Type u_1
inst : Field A
B : Type u_3
inst_1 : CommRing B
inst_2 : Algebra A B
x : B
a : A
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq :
  Eq.{u_3 + 1} (α := B)
    ((Polynomial.aeval (HAdd.hAdd (β := B) x ((algebraMap A B : (a : A) → B) a : B)) : (a : A[X]) → B) q : B) (0 : B)
this :
  Eq.{u_3 + 1} (α := B)
    ((Polynomial.aeval x : (a : A[X]) → B)
        (q.comp (HAdd.hAdd (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))) :
      B)
    (0 : B)
H : degree (minpoly A x) ≤ (q.comp (HAdd.hAdd (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))).degree
pos :
  ∀
    (H :
      (↑(natDegree (minpoly A x)) : WithBot ℕ) ≤
        (q.comp (HAdd.hAdd (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))).degree),
    LE.le (α := WithBot ℕ) (↑(natDegree (minpoly A x)) : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
pos₁ :
  ∀
    (H :
      LE.le (α := WithBot ℕ) (↑(natDegree (minpoly A x)) : WithBot ℕ)
        (↑(q.comp (HAdd.hAdd (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))).natDegree : WithBot ℕ)),
    LE.le (α := WithBot ℕ) (↑(natDegree (minpoly A x)) : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
pos₂ :
  ∀
    (H :
      LE.le (α := WithBot ℕ) (↑(natDegree (minpoly A x)) : WithBot ℕ)
        (↑(q.natDegree * (HAdd.hAdd (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X])).natDegree) : WithBot ℕ)),
    LE.le (α := WithBot ℕ) (↑(natDegree (minpoly A x)) : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
pos₃ :
  ∀ (H : LE.le (α := WithBot ℕ) (↑(natDegree (minpoly A x)) : WithBot ℕ) (↑(q.natDegree * 1) : WithBot ℕ)),
    LE.le (α := WithBot ℕ) (↑(natDegree (minpoly A x)) : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
⊢ LE.le (α := WithBot ℕ) (↑(natDegree (minpoly A x)) : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
have pos₄ : ∀ (H : LE.le (α := WithBot ℕ) (↑(natDegree (minpoly A x)) : WithBot ℕ) (↑q.natDegree : WithBot ℕ)),
  LE.le (α := WithBot ℕ) (↑(natDegree (minpoly A x)) : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
Tactic: rwa [degree_eq_natDegree (minpoly.ne_zero hx),
        degree_eq_natDegree (qmo.comp_X_add_C _).ne_zero, natDegree_comp,
        natDegree_X_add_C, mul_one] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
A : Type u_1
inst : Field A
B : Type u_3
inst_1 : CommRing B
inst_2 : Algebra A B
x : B
a : A
hx : ¬IsIntegral A x
⊢ minpoly A (HAdd.hAdd (β := B) x ((algebraMap A B : (a : A) → B) a : B)) =
    Polynomial.comp (minpoly A x) (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))
have neg : ¬IsIntegral A (HAdd.hAdd (β := B) x ((algebraMap A B : (a : A) → B) a : B))
Tactic: rw [minpoly.eq_zero hx, minpoly.eq_zero, zero_comp]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
A : Type u_1
inst : Field A
B : Type u_3
inst_1 : CommRing B
inst_2 : Algebra A B
x : B
a : A
hx : ¬IsIntegral A x
⊢ ¬IsIntegral A (HAdd.hAdd (β := B) x ((algebraMap A B : (a : A) → B) a : B))
have neg : ∀ (h : IsIntegral A (HAdd.hAdd (β := B) x ((algebraMap A B : (a : A) → B) a : B))), IsIntegral A x
Tactic: refine fun h ↦ hx ?_