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 : IsDomain B
inst_3 : Algebra A B
x : B
hx : IsIntegral A x
y : A
h : IsRoot (minpoly A x) y
key : minpoly A x = HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) y : A[X])
this : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) (minpoly A x) : B) (0 : B)
rwa :
  ∀
    (this :
      Eq.{u_2 + 1} (α := B)
        ((Polynomial.aeval x : (a : A[X]) → B) (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) y : A[X])) :
          B)
        (0 : B)),
    (algebraMap A B : (a : A) → B) y = x
rwa₁ :
  ∀
    (this :
      HSub.hSub (α := B) (β := B) ((Polynomial.aeval x : (a : A[X]) → B) X : B)
          ((Polynomial.aeval x : (a : A[X]) → B) ((C : (a : A) → A[X]) y : A[X]) : B) =
        0),
    (algebraMap A B : (a : A) → B) y = x
rwa₂ :
  ∀ (this : HSub.hSub (β := B) x ((Polynomial.aeval x : (a : A[X]) → B) ((C : (a : A) → A[X]) y : A[X]) : B) = 0),
    (algebraMap A B : (a : A) → B) y = x
rwa₃ : ∀ (this : HSub.hSub (β := B) x ((algebraMap A B : (a : A) → B) y : B) = 0), (algebraMap A B : (a : A) → B) y = x
⊢ (algebraMap A B : (a : A) → B) y = x
have rwa₄ : ∀ (this : x = (algebraMap A B : (a : A) → B) y), (algebraMap A B : (a : A) → B) y = x
Tactic: rwa [key, map_sub, aeval_X, aeval_C, sub_eq_zero, eq_comm] at this
Cleared hypotheses: this
-- 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 : IsDomain B
inst_3 : Algebra A B
x : B
hx : IsIntegral A x
y : A
h : IsRoot (minpoly A x) y
key : minpoly A x = HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) y : A[X])
this : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) (minpoly A x) : B) (0 : B)
rwa :
  ∀
    (this :
      Eq.{u_2 + 1} (α := B)
        ((Polynomial.aeval x : (a : A[X]) → B) (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) y : A[X])) :
          B)
        (0 : B)),
    (algebraMap A B : (a : A) → B) y = x
rwa₁ :
  ∀
    (this :
      HSub.hSub (α := B) (β := B) ((Polynomial.aeval x : (a : A[X]) → B) X : B)
          ((Polynomial.aeval x : (a : A[X]) → B) ((C : (a : A) → A[X]) y : A[X]) : B) =
        0),
    (algebraMap A B : (a : A) → B) y = x
rwa₂ :
  ∀ (this : HSub.hSub (β := B) x ((Polynomial.aeval x : (a : A[X]) → B) ((C : (a : A) → A[X]) y : A[X]) : B) = 0),
    (algebraMap A B : (a : A) → B) y = x
rwa₃ : ∀ (this : HSub.hSub (β := B) x ((algebraMap A B : (a : A) → B) y : B) = 0), (algebraMap A B : (a : A) → B) y = x
rwa₄ : ∀ (this : x = (algebraMap A B : (a : A) → B) y), (algebraMap A B : (a : A) → B) y = x
⊢ (algebraMap A B : (a : A) → B) y = x
have rwa₅ : ∀ (this : (algebraMap A B : (a : A) → B) y = x), (algebraMap A B : (a : A) → B) y = x
Tactic: rwa [key, map_sub, aeval_X, aeval_C, sub_eq_zero, eq_comm] at this
Cleared hypotheses: this
-- 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 : IsDomain B
inst_3 : Algebra A B
x : B
hx : IsIntegral A x
⊢ coeff (minpoly A x) 0 = 0 ↔ x = 0
have mp : coeff (minpoly A x) 0 = 0 → x = 0
Tactic: constructor
-- 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 : IsDomain B
inst_3 : Algebra A B
x : B
hx : IsIntegral A x
mp : coeff (minpoly A x) 0 = 0 → x = 0
⊢ coeff (minpoly A x) 0 = 0 ↔ x = 0
have mpr : x = 0 → coeff (minpoly A x) 0 = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : IsDomain B
inst_3 : Algebra A B
x : B
hx : IsIntegral A x
h : coeff (minpoly A x) 0 = 0
⊢ x = 0
have zero_root : IsRoot (minpoly A x) 0
Tactic: have zero_root := zero_isRoot_of_coeff_zero_eq_zero h
-- 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 : IsDomain B
inst_3 : Algebra A B
x : B
hx : IsIntegral A x
h : coeff (minpoly A x) 0 = 0
zero_root : IsRoot (minpoly A x) 0
⊢ x = 0
have mp : Eq.{u_2 + 1} (α := B) ((algebraMap A B : (a : A) → B) 0 : B) (0 : B)
Tactic: rw [← root hx zero_root]
-- 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 : IsDomain B
inst_3 : Algebra A B
x : B
hx : IsIntegral A x
h : x ≠ 0
⊢ coeff (minpoly A x) 0 ≠ 0
have contrapose : ∀ (h : coeff (minpoly A x) 0 = 0), x = 0
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CommRing L
inst_2 : IsDomain L
inst_3 : Algebra K L
σ : L ≃ₐ[K] L
hσ : IsOfFinOrder σ
⊢ minpoly K σ.toLinearMap = HPow.hPow (α := K[X]) X (orderOf σ) - (C : (a : K) → K[X]) 1
have refine_1 : Eq.{u_2 + 1} (α := L →ₗ[K] L)
  ((Polynomial.aeval σ.toLinearMap : (a : K[X]) → L →ₗ[K] L)
      (HPow.hPow (α := K[X]) X (orderOf σ) - (C : (a : K) → K[X]) 1) :
    L →ₗ[K] L)
  (0 : L →ₗ[K] L)
Tactic: refine (minpoly.unique _ _ (monic_X_pow_sub_C _ hσ.orderOf_pos.ne.symm) ?_ ?_).symm
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CommRing L
inst_2 : IsDomain L
inst_3 : Algebra K L
σ : L ≃ₐ[K] L
hσ : IsOfFinOrder σ
refine_1 :
  Eq.{u_2 + 1} (α := L →ₗ[K] L)
    ((Polynomial.aeval σ.toLinearMap : (a : K[X]) → L →ₗ[K] L)
        (HPow.hPow (α := K[X]) X (orderOf σ) - (C : (a : K) → K[X]) 1) :
      L →ₗ[K] L)
    (0 : L →ₗ[K] L)
⊢ minpoly K σ.toLinearMap = HPow.hPow (α := K[X]) X (orderOf σ) - (C : (a : K) → K[X]) 1
have refine_2 : ∀ (q : K[X]),
  q.Monic →
    Eq.{u_2 + 1} (α := L →ₗ[K] L) ((Polynomial.aeval σ.toLinearMap : (a : K[X]) → L →ₗ[K] L) q : L →ₗ[K] L)
        (0 : L →ₗ[K] L) →
      (HPow.hPow (α := K[X]) X (orderOf σ) - (C : (a : K) → K[X]) 1).degree ≤ q.degree
Tactic: refine (minpoly.unique _ _ (monic_X_pow_sub_C _ hσ.orderOf_pos.ne.symm) ?_ ?_).symm
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CommRing L
inst_2 : IsDomain L
inst_3 : Algebra K L
σ : L ≃ₐ[K] L
hσ : IsOfFinOrder σ
q : K[X]
hq : q.Monic
hs :
  Eq.{u_2 + 1} (α := L →ₗ[K] L) ((Polynomial.aeval σ.toLinearMap : (a : K[X]) → L →ₗ[K] L) q : L →ₗ[K] L)
    (0 : L →ₗ[K] L)
⊢ (HPow.hPow (α := K[X]) X (orderOf σ) - (C : (a : K) → K[X]) 1).degree ≤ q.degree
have refine_2 : ¬q.natDegree < orderOf σ
Tactic: rw [degree_eq_natDegree hq.ne_zero, degree_X_pow_sub_C hσ.orderOf_pos, Nat.cast_le, ← not_lt]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CommRing L
inst_2 : IsDomain L
inst_3 : Algebra K L
σ : L ≃ₐ[K] L
hσ : IsOfFinOrder σ
q : K[X]
hq : q.Monic
hs :
  Eq.{u_2 + 1} (α := L →ₗ[K] L) ((Polynomial.aeval σ.toLinearMap : (a : K[X]) → L →ₗ[K] L) q : L →ₗ[K] L)
    (0 : L →ₗ[K] L)
H : q.natDegree < orderOf σ
⊢ False
have hs₁ : Eq.{u_2 + 1} (α := L →ₗ[K] L) (∑ i : Fin (orderOf σ), q.coeff (↑i : ℕ) • σ.toLinearMap ^ (↑i : ℕ)) 0
Tactic: rw [aeval_eq_sum_range' H, ← Fin.sum_univ_eq_sum_range] at hs
Cleared hypotheses: hs, H
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CommRing L
inst_2 : IsDomain L
inst_3 : Algebra K L
σ : L ≃ₐ[K] L
hσ : IsOfFinOrder σ
q : K[X]
hq : q.Monic
hs : Eq.{u_2 + 1} (α := L →ₗ[K] L) (∑ i : Fin (orderOf σ), q.coeff (↑i : ℕ) • σ.toLinearMap ^ (↑i : ℕ)) 0
H : q.natDegree < orderOf σ
⊢ False
have hs₁ : Eq.{u_2 + 1} (α := L →ₗ[K] L) (∑ x : Fin (orderOf σ), q.coeff (↑x : ℕ) • (σ ^ (↑x : ℕ)).toLinearMap) 0
Tactic: simp_rw [← AlgEquiv.pow_toLinearMap] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CommRing L
inst_2 : IsDomain L
inst_3 : Algebra K L
σ : L ≃ₐ[K] L
hσ : IsOfFinOrder σ
q : K[X]
hq : q.Monic
H : q.natDegree < orderOf σ
hs : Eq.{u_2 + 1} (α := L →ₗ[K] L) (∑ x : Fin (orderOf σ), q.coeff (↑x : ℕ) • (σ ^ (↑x : ℕ)).toLinearMap) 0
⊢ False
have refine_2 : q = 0
Tactic: apply hq.ne_zero
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CommRing L
inst_2 : IsDomain L
inst_3 : Algebra K L
σ : L →ₐ[K] L
hσ : IsOfFinOrder σ
⊢ orderOf σ =
    orderOf (G := L ≃ₐ[K] L) ((AlgEquiv.algHomUnitsEquiv K L : (a : (L →ₐ[K] L)ˣ) → L ≃ₐ[K] L) hσ.unit : L ≃ₐ[K] L)
have hf : Injective (α := (L →ₐ[K] L)ˣ) (β := L ≃ₐ[K] L)
  (⇑(↑(AlgEquiv.algHomUnitsEquiv K L) : (L →ₐ[K] L)ˣ →* L ≃ₐ[K] L) : (a : (L →ₐ[K] L)ˣ) → L ≃ₐ[K] L)
Tactic: rw [← MonoidHom.coe_coe, orderOf_injective, ← orderOf_units, IsOfFinOrder.val_unit]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CommRing L
inst_2 : IsDomain L
inst_3 : Algebra K L
σ : L →ₐ[K] L
hσ : IsOfFinOrder σ
⊢ minpoly K σ.toLinearMap = HPow.hPow (α := K[X]) X (orderOf σ) - (C : (a : K) → K[X]) 1
have this : orderOf σ =
  orderOf (G := L ≃ₐ[K] L) ((AlgEquiv.algHomUnitsEquiv K L : (a : (L →ₐ[K] L)ˣ) → L ≃ₐ[K] L) hσ.unit : L ≃ₐ[K] L)
Tactic: have : orderOf σ = orderOf (AlgEquiv.algHomUnitsEquiv _ _ hσ.unit) := by
    rw [← MonoidHom.coe_coe, orderOf_injective, ← orderOf_units, IsOfFinOrder.val_unit]
    exact (AlgEquiv.algHomUnitsEquiv K L).injective
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CommRing L
inst_2 : IsDomain L
inst_3 : Algebra K L
σ : L →ₐ[K] L
hσ : IsOfFinOrder σ
this :
  orderOf σ =
    orderOf (G := L ≃ₐ[K] L) ((AlgEquiv.algHomUnitsEquiv K L : (a : (L →ₐ[K] L)ˣ) → L ≃ₐ[K] L) hσ.unit : L ≃ₐ[K] L)
⊢ minpoly K σ.toLinearMap = HPow.hPow (α := K[X]) X (orderOf σ) - (C : (a : K) → K[X]) 1
have rw : Eq (α := K[X]) (minpoly K σ.toLinearMap)
  (minpoly.{u_1, u_2} K (B := L →ₗ[K] L)
    (AlgEquiv.toLinearMap ((AlgEquiv.algHomUnitsEquiv K L : (a : (L →ₐ[K] L)ˣ) → L ≃ₐ[K] L) hσ.unit)))
Tactic: rw [this, ← minpoly_algEquiv_toLinearMap]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CommRing L
inst_2 : IsDomain L
inst_3 : Algebra K L
σ : L →ₐ[K] L
hσ : IsOfFinOrder σ
this :
  orderOf σ =
    orderOf (G := L ≃ₐ[K] L) ((AlgEquiv.algHomUnitsEquiv K L : (a : (L →ₐ[K] L)ˣ) → L ≃ₐ[K] L) hσ.unit : L ≃ₐ[K] L)
rw :
  Eq (α := K[X]) (minpoly K σ.toLinearMap)
    (minpoly.{u_1, u_2} K (B := L →ₗ[K] L)
      (AlgEquiv.toLinearMap ((AlgEquiv.algHomUnitsEquiv K L : (a : (L →ₐ[K] L)ˣ) → L ≃ₐ[K] L) hσ.unit)))
⊢ minpoly K σ.toLinearMap = HPow.hPow (α := K[X]) X (orderOf σ) - (C : (a : K) → K[X]) 1
have hσ₁ : IsOfFinOrder (G := L ≃ₐ[K] L) ((AlgEquiv.algHomUnitsEquiv K L : (a : (L →ₐ[K] L)ˣ) → L ≃ₐ[K] L) hσ.unit : L ≃ₐ[K] L)
Tactic: rw [this, ← minpoly_algEquiv_toLinearMap]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CommRing L
inst_2 : IsDomain L
inst_3 : Algebra K L
σ : L →ₐ[K] L
hσ : IsOfFinOrder σ
this :
  orderOf σ =
    orderOf (G := L ≃ₐ[K] L) ((AlgEquiv.algHomUnitsEquiv K L : (a : (L →ₐ[K] L)ˣ) → L ≃ₐ[K] L) hσ.unit : L ≃ₐ[K] L)
⊢ Eq (α := K[X]) (minpoly K σ.toLinearMap)
    (minpoly.{u_1, u_2} K (B := L →ₗ[K] L)
      (AlgEquiv.toLinearMap ((AlgEquiv.algHomUnitsEquiv K L : (a : (L →ₐ[K] L)ˣ) → L ≃ₐ[K] L) hσ.unit)))
have h : σ.toLinearMap = AlgEquiv.toLinearMap ((AlgEquiv.algHomUnitsEquiv K L : (a : (L →ₐ[K] L)ˣ) → L ≃ₐ[K] L) hσ.unit)
Tactic: apply congr_arg
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CommRing L
inst_2 : IsDomain L
inst_3 : Algebra K L
σ : L →ₐ[K] L
hσ : IsOfFinOrder σ
this :
  orderOf σ =
    orderOf (G := L ≃ₐ[K] L) ((AlgEquiv.algHomUnitsEquiv K L : (a : (L →ₐ[K] L)ˣ) → L ≃ₐ[K] L) hσ.unit : L ≃ₐ[K] L)
⊢ σ.toLinearMap = AlgEquiv.toLinearMap ((AlgEquiv.algHomUnitsEquiv K L : (a : (L →ₐ[K] L)ˣ) → L ≃ₐ[K] L) hσ.unit)
have h : ∀ (x : L),
  Eq (α := L) ((σ.toLinearMap : (a : L) → L) x : L)
    ((AlgEquiv.toLinearMap ((AlgEquiv.algHomUnitsEquiv K L : (a : (L →ₐ[K] L)ˣ) → L ≃ₐ[K] L) hσ.unit) : (a : L) → L) x :
      L)
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CommRing L
inst_2 : IsDomain L
inst_3 : Algebra K L
σ : L →ₐ[K] L
hσ : IsOfFinOrder σ
this :
  orderOf σ =
    orderOf (G := L ≃ₐ[K] L) ((AlgEquiv.algHomUnitsEquiv K L : (a : (L →ₐ[K] L)ˣ) → L ≃ₐ[K] L) hσ.unit : L ≃ₐ[K] L)
⊢ IsOfFinOrder (G := L ≃ₐ[K] L) ((AlgEquiv.algHomUnitsEquiv K L : (a : (L →ₐ[K] L)ˣ) → L ≃ₐ[K] L) hσ.unit : L ≃ₐ[K] L)
have hσ₁ : 0 < orderOf (G := L ≃ₐ[K] L) ((AlgEquiv.algHomUnitsEquiv K L : (a : (L →ₐ[K] L)ˣ) → L ≃ₐ[K] L) hσ.unit : L ≃ₐ[K] L)
Tactic: rwa [← orderOf_pos_iff, ← this, orderOf_pos_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CommRing L
inst_2 : IsDomain L
inst_3 : Algebra K L
σ : L →ₐ[K] L
hσ : IsOfFinOrder σ
this :
  orderOf σ =
    orderOf (G := L ≃ₐ[K] L) ((AlgEquiv.algHomUnitsEquiv K L : (a : (L →ₐ[K] L)ˣ) → L ≃ₐ[K] L) hσ.unit : L ≃ₐ[K] L)
hσ₁ :
  0 < orderOf (G := L ≃ₐ[K] L) ((AlgEquiv.algHomUnitsEquiv K L : (a : (L →ₐ[K] L)ˣ) → L ≃ₐ[K] L) hσ.unit : L ≃ₐ[K] L)
⊢ IsOfFinOrder (G := L ≃ₐ[K] L) ((AlgEquiv.algHomUnitsEquiv K L : (a : (L →ₐ[K] L)ˣ) → L ≃ₐ[K] L) hσ.unit : L ≃ₐ[K] L)
have hσ₂ : 0 < orderOf σ
Tactic: rwa [← orderOf_pos_iff, ← this, orderOf_pos_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Finite (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
inst_3 : Module.Finite A B
x : B
⊢ natDegree (minpoly A x) ≤ Submodule.spanFinrank.{u_2, u_1} (R := A) (M := B) ⊤
have rcases : ∀ (f : A[X]) (f_monic : f.Monic) (f_deg : f.natDegree = Submodule.spanFinrank.{u_2, u_1} (R := A) (M := B) ⊤)
  (f_aeval :
    Eq.{u_2 + 1} (α := Module.End A B)
      (((Polynomial.aeval ((Algebra.lmul A B : (a : B) → Module.End A B) x) :
              AlgHom.{u_1, u_1, u_2} A A[X] (Module.End A B)) :
            (a : A[X]) → Module.End A B)
          f :
        Module.End A B)
      (0 : Module.End A B)),
  natDegree (minpoly A x) ≤ Submodule.spanFinrank.{u_2, u_1} (R := A) (M := B) ⊤
Tactic: rcases LinearMap.exists_monic_and_natDegree_eq_and_aeval_eq_zero _ (Algebra.lmul A _ x) with
    ⟨f, f_monic, f_deg, f_aeval⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Finite (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
inst_3 : Module.Finite A B
x : B
f : A[X]
f_monic : f.Monic
f_deg : f.natDegree = Submodule.spanFinrank.{u_2, u_1} (R := A) (M := B) ⊤
f_aeval :
  Eq.{u_2 + 1} (α := Module.End A B)
    (((Polynomial.aeval ((Algebra.lmul A B : (a : B) → Module.End A B) x) :
            AlgHom.{u_1, u_1, u_2} A A[X] (Module.End A B)) :
          (a : A[X]) → Module.End A B)
        f :
      Module.End A B)
    (0 : Module.End A B)
⊢ natDegree (minpoly A x) ≤ Submodule.spanFinrank.{u_2, u_1} (R := A) (M := B) ⊤
have refine : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) f : B) (0 : B)
Tactic: refine f_deg ▸ (natDegree_le_natDegree <| minpoly.min _ _ f_monic ?_)
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Finite (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
inst_3 : Module.Finite A B
x : B
f : A[X]
f_monic : f.Monic
f_deg : f.natDegree = Submodule.spanFinrank.{u_2, u_1} (R := A) (M := B) ⊤
f_aeval :
  Eq.{u_2 + 1} (α := Module.End A B)
    (((Polynomial.aeval ((Algebra.lmul A B : (a : B) → Module.End A B) x) :
            AlgHom.{u_1, u_1, u_2} A A[X] (Module.End A B)) :
          (a : A[X]) → Module.End A B)
        f :
      Module.End A B)
    (0 : Module.End A B)
⊢ Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) f : B) (0 : B)
have f_aeval₁ : Eq (α := Module.End A B)
  ((Algebra.lmul A B : (a : B) → Module.End A B) ((Polynomial.aeval x : (a : A[X]) → B) f : B) : Module.End A B)
  (0 : Module.End A B)
Tactic: rw [aeval_algHom_apply] at f_aeval
Cleared hypotheses: f_aeval
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Finite (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
inst_3 : Module.Finite A B
x : B
inst_4 : Module.Free A B
⊢ natDegree (minpoly A x) ≤ Module.finrank A B
have a : Nontrivial A
Tactic: nontriviality A
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
K : Type u_3
L : Type u_4
inst_4 : Field K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : CommRing L
inst_8 : Nontrivial L
inst_9 : Algebra R L
inst_10 : Algebra S L
inst_11 : Algebra K L
inst_12 : IsScalarTower R K L
inst_13 : IsScalarTower R S L
inst_14 : IsIntegrallyClosed R
inst_15 : IsDomain S
s : S
hs : IsIntegral R s
⊢ Eq (α := K[X]) (minpoly.{u_3, u_4} K (B := L) ((algebraMap S L : (a : S) → L) s : L))
    (map (algebraMap R K) (minpoly R s))
have refine_1 : Irreducible (M := K[X]) (map (algebraMap R K) (minpoly R s))
Tactic: refine (eq_of_irreducible_of_monic ?_ ?_ ?_).symm
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
K : Type u_3
L : Type u_4
inst_4 : Field K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : CommRing L
inst_8 : Nontrivial L
inst_9 : Algebra R L
inst_10 : Algebra S L
inst_11 : Algebra K L
inst_12 : IsScalarTower R K L
inst_13 : IsScalarTower R S L
inst_14 : IsIntegrallyClosed R
inst_15 : IsDomain S
s : S
hs : IsIntegral R s
refine_1 : Irreducible (M := K[X]) (map (algebraMap R K) (minpoly R s))
⊢ Eq (α := K[X]) (minpoly.{u_3, u_4} K (B := L) ((algebraMap S L : (a : S) → L) s : L))
    (map (algebraMap R K) (minpoly R s))
have refine_2 : Eq.{u_4 + 1} (α := L)
  (((Polynomial.aeval ((algebraMap S L : (a : S) → L) s) : K[X] →ₐ[K] L) : (a : K[X]) → L)
      (map (algebraMap R K) (minpoly R s)) :
    L)
  (0 : L)
Tactic: refine (eq_of_irreducible_of_monic ?_ ?_ ?_).symm
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
K : Type u_3
L : Type u_4
inst_4 : Field K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : CommRing L
inst_8 : Nontrivial L
inst_9 : Algebra R L
inst_10 : Algebra S L
inst_11 : Algebra K L
inst_12 : IsScalarTower R K L
inst_13 : IsScalarTower R S L
inst_14 : IsIntegrallyClosed R
inst_15 : IsDomain S
s : S
hs : IsIntegral R s
refine_1 : Irreducible (M := K[X]) (map (algebraMap R K) (minpoly R s))
refine_2 :
  Eq.{u_4 + 1} (α := L)
    (((Polynomial.aeval ((algebraMap S L : (a : S) → L) s) : K[X] →ₐ[K] L) : (a : K[X]) → L)
        (map (algebraMap R K) (minpoly R s)) :
      L)
    (0 : L)
⊢ Eq (α := K[X]) (minpoly.{u_3, u_4} K (B := L) ((algebraMap S L : (a : S) → L) s : L))
    (map (algebraMap R K) (minpoly R s))
have refine_3 : Monic (map (algebraMap R K) (minpoly R s))
Tactic: refine (eq_of_irreducible_of_monic ?_ ?_ ?_).symm
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
K : Type u_3
L : Type u_4
inst_4 : Field K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : CommRing L
inst_8 : Nontrivial L
inst_9 : Algebra R L
inst_10 : Algebra S L
inst_11 : Algebra K L
inst_12 : IsScalarTower R K L
inst_13 : IsScalarTower R S L
inst_14 : IsIntegrallyClosed R
inst_15 : IsDomain S
s : S
hs : IsIntegral R s
⊢ Eq.{u_4 + 1} (α := L)
    (((Polynomial.aeval ((algebraMap S L : (a : S) → L) s) : K[X] →ₐ[K] L) : (a : K[X]) → L)
        (map (algebraMap R K) (minpoly R s)) :
      L)
    (0 : L)
have refine_2 : Eq.{u_4 + 1} (α := L)
  (((Polynomial.aeval ((algebraMap S L : (a : S) → L) s) : R[X] →ₐ[R] L) : (a : R[X]) → L) (minpoly R s) : L) (0 : L)
Tactic: rw [aeval_map_algebraMap, aeval_algebraMap_apply, aeval, map_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
K : Type u_3
L : Type u_4
inst_4 : Field K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : CommRing L
inst_8 : Nontrivial L
inst_9 : Algebra R L
inst_10 : Algebra S L
inst_11 : Algebra K L
inst_12 : IsScalarTower R K L
inst_13 : IsScalarTower R S L
inst_14 : IsIntegrallyClosed R
inst_15 : IsDomain S
s : S
hs : IsIntegral R s
refine_2 :
  Eq.{u_4 + 1} (α := L)
    (((Polynomial.aeval ((algebraMap S L : (a : S) → L) s) : R[X] →ₐ[R] L) : (a : R[X]) → L) (minpoly R s) : L) (0 : L)
⊢ Eq.{u_4 + 1} (α := L)
    (((Polynomial.aeval ((algebraMap S L : (a : S) → L) s) : K[X] →ₐ[K] L) : (a : K[X]) → L)
        (map (algebraMap R K) (minpoly R s)) :
      L)
    (0 : L)
have refine_2₁ : Eq.{u_4 + 1} (α := L) ((algebraMap S L : (a : S) → L) ((Polynomial.aeval s : (a : R[X]) → S) (minpoly R s) : S) : L)
  (0 : L)
Tactic: rw [aeval_map_algebraMap, aeval_algebraMap_apply, aeval, map_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
K : Type u_3
L : Type u_4
inst_4 : Field K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : CommRing L
inst_8 : Nontrivial L
inst_9 : Algebra R L
inst_10 : Algebra S L
inst_11 : Algebra K L
inst_12 : IsScalarTower R K L
inst_13 : IsScalarTower R S L
inst_14 : IsIntegrallyClosed R
inst_15 : IsDomain S
s : S
hs : IsIntegral R s
refine_2 :
  Eq.{u_4 + 1} (α := L)
    (((Polynomial.aeval ((algebraMap S L : (a : S) → L) s) : R[X] →ₐ[R] L) : (a : R[X]) → L) (minpoly R s) : L) (0 : L)
refine_2₁ :
  Eq.{u_4 + 1} (α := L) ((algebraMap S L : (a : S) → L) ((Polynomial.aeval s : (a : R[X]) → S) (minpoly R s) : S) : L)
    (0 : L)
⊢ Eq.{u_4 + 1} (α := L)
    (((Polynomial.aeval ((algebraMap S L : (a : S) → L) s) : K[X] →ₐ[K] L) : (a : K[X]) → L)
        (map (algebraMap R K) (minpoly R s)) :
      L)
    (0 : L)
have refine_2₂ : Eq.{u_4 + 1} (α := L) ((algebraMap S L : (a : S) → L) 0 : L) (0 : L)
Tactic: rw [aeval_map_algebraMap, aeval_algebraMap_apply, aeval, map_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
K : Type u_3
L : Type u_4
inst_4 : Field K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : CommRing L
inst_8 : Nontrivial L
inst_9 : Algebra R L
inst_10 : Algebra S L
inst_11 : Algebra K L
inst_12 : IsScalarTower R K L
inst_13 : IsScalarTower R S L
inst_14 : IsIntegrallyClosed R
inst_15 : IsDomain S
s : S
hs : IsIntegral R s
refine_2 :
  Eq.{u_4 + 1} (α := L)
    (((Polynomial.aeval ((algebraMap S L : (a : S) → L) s) : R[X] →ₐ[R] L) : (a : R[X]) → L) (minpoly R s) : L) (0 : L)
refine_2₁ :
  Eq.{u_4 + 1} (α := L) ((algebraMap S L : (a : S) → L) ((Polynomial.aeval s : (a : R[X]) → S) (minpoly R s) : S) : L)
    (0 : L)
refine_2₂ : Eq.{u_4 + 1} (α := L) ((algebraMap S L : (a : S) → L) 0 : L) (0 : L)
⊢ Eq.{u_4 + 1} (α := L)
    (((Polynomial.aeval ((algebraMap S L : (a : S) → L) s) : K[X] →ₐ[K] L) : (a : K[X]) → L)
        (map (algebraMap R K) (minpoly R s)) :
      L)
    (0 : L)
have refine_2₃ : Eq.{u_4 + 1} (α := L) 0 0
Tactic: rw [aeval_map_algebraMap, aeval_algebraMap_apply, aeval, map_zero]