awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
F : Type u_3
E : Type u_4
K : Type u_5
inst : Field F
inst_1 : Ring E
inst_2 : CommRing K
inst_3 : IsDomain K
inst_4 : Algebra F E
inst_5 : Algebra F K
inst_6 : FiniteDimensional F E
f g : E →ₐ[F] K
h :
  ∀
    (x :
      (↑(range (ι := Fin (Module.finrank F E)) (⇑(Module.finBasis F E) : (a : Fin (Module.finrank F E)) → E)) :
        Type u_4)),
    Eq (α := { l : K // l ∈ aroots (minpoly F (↑x : E)) K }) (rootsOfMinPolyPiType F E K f x)
      (rootsOfMinPolyPiType F E K g x)
⊢ Eq (α := E →ₗ[F] K)
    (↑f : [inst_7 : FunLike (E →ₐ[F] K) E K] → [SemilinearMapClass (E →ₐ[F] K) (RingHom.id F) E K] → E →ₗ[F] K)
    (↑g : [inst_7 : FunLike (E →ₐ[F] K) E K] → [SemilinearMapClass (E →ₐ[F] K) (RingHom.id F) E K] → E →ₗ[F] K)

Tactic:
exact LinearMap.ext_on (Module.finBasis F E).span_eq fun e he =>
    Subtype.ext_iff.mp (h ⟨e, he⟩)

Premises used: LinearMap.ext_on, Module.finBasis, Module.Basis.span_eq
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
inst_3 : Nontrivial B
a : A
⊢ minpoly.{u_1, u_2} A (B := B) ((algebraMap A B : (a : A) → B) a : B) =
    HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X])

Tactic:
eq_X_sub_C_of_algebraMap_inj a (algebraMap A B).injective

Premises used: Algebra.algebraMap, minpoly.eq_X_sub_C_of_algebraMap_inj, RingHom.injective
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
inst : Field A
a : A
⊢ minpoly A a = HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X])

Tactic:
eq_X_sub_C A a

Premises used: minpoly.eq_X_sub_C
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
inst_3 : Nontrivial B
⊢ Eq (α := A[X]) (minpoly.{u_1, u_2} A (B := B) 0) X

Tactic:
simpa only [add_zero, C_0, sub_eq_add_neg, neg_zero, map_zero] using eq_X_sub_C B (0 : A)

Premises used: Polynomial.C_0, sub_eq_add_neg, map_zero, add_zero, OfNat.ofNat, neg_zero, minpoly.eq_X_sub_C
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
inst_3 : Nontrivial B
⊢ minpoly.{u_1, u_2} A (B := B) 1 = HSub.hSub (α := A[X]) X 1

Tactic:
simpa only [map_one, C_1, sub_eq_add_neg] using eq_X_sub_C B (1 : A)

Premises used: Polynomial.C_1, sub_eq_add_neg, map_one, OfNat.ofNat, minpoly.eq_X_sub_C
-- Module: Mathlib.FieldTheory.Minpoly.Field
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
⊢ Prime (M := A[X]) (minpoly A x)

Tactic:
⟨minpoly.ne_zero hx, not_isUnit A x, ?_⟩

Premises used: Prime, And.intro, minpoly.not_isUnit, minpoly.ne_zero
-- Module: Mathlib.FieldTheory.Minpoly.Field
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
refine : ∀ (a b : A[X]), minpoly A x ∣ a * b → minpoly A x ∣ a ∨ minpoly A x ∣ b
⊢ Prime (M := A[X]) (minpoly A x)

Tactic:
refine ⟨minpoly.ne_zero hx, not_isUnit A x, ?_⟩
-- Module: Mathlib.FieldTheory.Minpoly.Field
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
p q d : A[X]
h : p * q = minpoly A x * d
⊢ Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) (p * q) : B) (0 : B)

Tactic:
simp [h, aeval A x]

Premises used: minpoly.aeval
-- Module: Mathlib.FieldTheory.Minpoly.Field
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
p q d : A[X]
h : p * q = minpoly A x * d
⊢ Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) (p * q) : B) (0 : B)

Tactic:
have : Polynomial.aeval x (p * q) = 0 := by simp [h, aeval A x]
-- Module: Mathlib.FieldTheory.Minpoly.Field
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
p q d : A[X]
h : p * q = minpoly A x * d
this : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) (p * q) : B) (0 : B)
⊢ Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B) ∨
    Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) (0 : B)

Tactic:
simpa
-- Module: Mathlib.FieldTheory.Minpoly.Field
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
p q d : A[X]
h : p * q = minpoly A x * d
this : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) (p * q) : B) (0 : B)
⊢ Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B) ∨
    Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) (0 : B)

Tactic:
replace : Polynomial.aeval x p = 0 ∨ Polynomial.aeval x q = 0 := by simpa
-- Module: Mathlib.FieldTheory.Minpoly.Field
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
p q d : A[X]
h : p * q = minpoly A x * d
this :
  Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B) ∨
    Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) (0 : B)
⊢ minpoly A x ∣ p ∨ minpoly A x ∣ q

Tactic:
Or.imp (dvd A x) (dvd A x) this

Premises used: minpoly.dvd, Or.imp
-- Module: Mathlib.FieldTheory.Minpoly.Field
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
p q d : A[X]
h : p * q = minpoly A x * d
this :
  Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B) ∨
    Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) (0 : B)
⊢ minpoly A x ∣ p ∨ minpoly A x ∣ q

Tactic:
exact Or.imp (dvd A x) (dvd A x) this

Premises used: minpoly.dvd, Or.imp
-- Module: Mathlib.FieldTheory.Minpoly.Field
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
⊢ minpoly A x = HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) y : A[X])

Tactic:
have key : minpoly A x = X - C y := eq_of_monic_of_associated (monic hx) (monic_X_sub_C y)
    (associated_of_dvd_dvd ((irreducible_X_sub_C y).dvd_symm (irreducible hx) (dvd_iff_isRoot.2 h))
      (dvd_iff_isRoot.2 h))
-- Module: Mathlib.FieldTheory.Minpoly.Field
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])
⊢ Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) (minpoly A x) : B) (0 : B)

Tactic:
have := aeval A x
-- Module: Mathlib.FieldTheory.Minpoly.Field
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
rwa₅ rwa₆ rwa₇ rwa₈ : ∀ (this : (algebraMap A B : (a : A) → B) y = x), (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

Premises used: map_sub, sub_eq_zero, eq_comm, Polynomial.aeval_C, Polynomial.aeval_X
-- Module: Mathlib.FieldTheory.Minpoly.Field
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
mpr : x = 0 → coeff (minpoly A x) 0 = 0
⊢ coeff (minpoly A x) 0 = 0 ↔ x = 0

Tactic:
constructor
-- Module: Mathlib.FieldTheory.Minpoly.Field
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
⊢ IsRoot (minpoly A x) 0

Tactic:
have zero_root := zero_isRoot_of_coeff_zero_eq_zero h
-- Module: Mathlib.FieldTheory.Minpoly.Field
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
mp : Eq.{u_2 + 1} (α := B) ((algebraMap A B : (a : A) → B) 0 : B) (0 : B)
⊢ x = 0

Tactic:
rw [← root hx zero_root]

Premises used: minpoly.root
-- Module: Mathlib.FieldTheory.Minpoly.Field
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
⊢ Eq.{u_2 + 1} (α := B) ((algebraMap A B : (a : A) → B) 0 : B) (0 : B)

Tactic:
map_zero _

Premises used: map_zero
-- Module: Mathlib.FieldTheory.Minpoly.Field
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
⊢ Eq.{u_2 + 1} (α := B) ((algebraMap A B : (a : A) → B) 0 : B) (0 : B)

Tactic:
exact map_zero _

Premises used: map_zero
-- Module: Mathlib.FieldTheory.Minpoly.Field
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
hx : IsIntegral.{u_1, u_2} A (A := B) 0
⊢ coeff (minpoly.{u_1, u_2} A (B := B) 0) 0 = 0

Tactic:
simp
-- Module: Mathlib.FieldTheory.Minpoly.Field
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
contrapose : ∀ (h : coeff (minpoly A x) 0 = 0), x = 0
⊢ coeff (minpoly A x) 0 ≠ 0

Tactic:
contrapose h
-- Module: Mathlib.FieldTheory.Minpoly.Field
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

Tactic:
simpa only [hx, coeff_zero_eq_zero] using h

Premises used: minpoly.coeff_zero_eq_zero
-- Module: Mathlib.FieldTheory.Minpoly.Field
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

Tactic:
(minpoly.unique _ _ (monic_X_pow_sub_C _ hσ.orderOf_pos.ne.symm) ?_ ?_).symm

Premises used: minpoly.unique, IsOfFinOrder.orderOf_pos, Polynomial.monic_X_pow_sub_C, Ne.symm, Eq.symm, LT.lt.ne
-- Module: Mathlib.FieldTheory.Minpoly.Field
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)
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
⊢ minpoly K σ.toLinearMap = HPow.hPow (α := K[X]) X (orderOf σ) - (C : (a : K) → K[X]) 1

Tactic:
refine (minpoly.unique _ _ (monic_X_pow_sub_C _ hσ.orderOf_pos.ne.symm) ?_ ?_).symm

Premises used: minpoly.unique, IsOfFinOrder.orderOf_pos, Polynomial.monic_X_pow_sub_C, Ne.symm, Eq.symm, LT.lt.ne
-- Module: Mathlib.FieldTheory.Minpoly.Field
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 σ
⊢ 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:
simp [← AlgEquiv.pow_toLinearMap, pow_orderOf_eq_one]

Premises used: AlgEquiv.pow_toLinearMap, pow_orderOf_eq_one
-- Module: Mathlib.FieldTheory.Minpoly.Field
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)
refine_2 : ¬q.natDegree < orderOf σ
⊢ (HPow.hPow (α := K[X]) X (orderOf σ) - (C : (a : K) → K[X]) 1).degree ≤ q.degree

Tactic:
rw [degree_eq_natDegree hq.ne_zero, degree_X_pow_sub_C hσ.orderOf_pos, Nat.cast_le, ← not_lt]

Premises used: Polynomial.degree_eq_natDegree, IsOfFinOrder.orderOf_pos, Polynomial.degree_X_pow_sub_C, not_lt, Nat.cast_le, Polynomial.Monic.ne_zero
-- Module: Mathlib.FieldTheory.Minpoly.Field
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 σ
⊢ 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

Premises used: Fin.sum_univ_eq_sum_range, Polynomial.aeval_eq_sum_range'
-- Module: Mathlib.FieldTheory.Minpoly.Field
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 σ
hs₁ : Eq.{u_2 + 1} (α := L →ₗ[K] L) (∑ i : Fin (orderOf σ), q.coeff (↑i : ℕ) • σ.toLinearMap ^ (↑i : ℕ)) 0
⊢ q.natDegree < orderOf σ

Tactic:
rw [aeval_eq_sum_range' H, ← Fin.sum_univ_eq_sum_range] at hs

Premises used: Fin.sum_univ_eq_sum_range, Polynomial.aeval_eq_sum_range'
-- Module: Mathlib.FieldTheory.Minpoly.Field
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 σ
⊢ Eq.{u_2 + 1} (α := L →ₗ[K] L) (∑ x : Fin (orderOf σ), q.coeff (↑x : ℕ) • (σ ^ (↑x : ℕ)).toLinearMap) 0

Tactic:
simp_rw [← AlgEquiv.pow_toLinearMap] at hs

Premises used: AlgEquiv.pow_toLinearMap
-- Module: Mathlib.FieldTheory.Minpoly.Field
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
refine_2 : q = 0
⊢ False

Tactic:
apply hq.ne_zero

Premises used: Polynomial.Monic.ne_zero
-- Module: Mathlib.FieldTheory.Minpoly.Field
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
⊢ q = 0

Tactic:
simpa using Fintype.linearIndependent_iff.mp
      (((linearIndependent_algHom_toLinearMap' K L L).comp _ AlgEquiv.coe_algHom_injective).comp _
        (Subtype.val_injective.comp ((finEquivPowers hσ).injective)))
      (q.coeff ∘ (↑)) hs ⟨_, H⟩

Premises used: Subtype.val_injective, linearIndependent_algHom_toLinearMap', Function.comp, Fin.mk, finEquivPowers, Fin.val, Polynomial.coeff, AlgEquiv.coe_algHom_injective, Fintype.linearIndependent_iff, Function.Injective.comp, Iff.mp, Equiv.injective, LinearIndependent.comp
-- Module: Mathlib.FieldTheory.Minpoly.Field
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 σ
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)
⊢ orderOf σ =
    orderOf (G := L ≃ₐ[K] L) ((AlgEquiv.algHomUnitsEquiv K L : (a : (L →ₐ[K] L)ˣ) → L ≃ₐ[K] L) hσ.unit : L ≃ₐ[K] L)

Tactic:
rw [← MonoidHom.coe_coe, orderOf_injective, ← orderOf_units, IsOfFinOrder.val_unit]

Premises used: orderOf_units, MonoidHom.coe_coe, IsOfFinOrder.val_unit, orderOf_injective
-- Module: Mathlib.FieldTheory.Minpoly.Field
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 σ
⊢ 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:
(AlgEquiv.algHomUnitsEquiv K L).injective

Premises used: AlgEquiv.algHomUnitsEquiv, MulEquiv.injective
-- Module: Mathlib.FieldTheory.Minpoly.Field
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 σ
⊢ 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:
exact (AlgEquiv.algHomUnitsEquiv K L).injective

Premises used: AlgEquiv.algHomUnitsEquiv, MulEquiv.injective
-- Module: Mathlib.FieldTheory.Minpoly.Field
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)

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
-- Module: Mathlib.FieldTheory.Minpoly.Field
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)))
hσ₁ :
  IsOfFinOrder (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

Tactic:
rw [this, ← minpoly_algEquiv_toLinearMap]

Premises used: minpoly_algEquiv_toLinearMap
-- Module: Mathlib.FieldTheory.Minpoly.Field
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 : σ.toLinearMap = AlgEquiv.toLinearMap ((AlgEquiv.algHomUnitsEquiv K L : (a : (L →ₐ[K] L)ˣ) → L ≃ₐ[K] L) hσ.unit)
⊢ 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:
apply congr_arg

Premises used: congr_arg
-- Module: Mathlib.FieldTheory.Minpoly.Field
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 :
  ∀ (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)
⊢ σ.toLinearMap = AlgEquiv.toLinearMap ((AlgEquiv.algHomUnitsEquiv K L : (a : (L →ₐ[K] L)ˣ) → L ≃ₐ[K] L) hσ.unit)

Tactic:
ext
-- Module: Mathlib.FieldTheory.Minpoly.Field
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)
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:
simp
-- Module: Mathlib.FieldTheory.Minpoly.Field
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)
hσ₂ : 0 < orderOf σ
hσ₃ hσ₄ hσ₅ hσ₆ : IsOfFinOrder σ
⊢ IsOfFinOrder (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]

Premises used: orderOf_pos_iff
-- Module: Mathlib.FieldTheory.Minpoly.Finite
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
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) ⊤
⊢ 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⟩

Premises used: Algebra.lmul, LinearMap.exists_monic_and_natDegree_eq_and_aeval_eq_zero, DFunLike.coe
-- Module: Mathlib.FieldTheory.Minpoly.Finite
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) ⊤

Tactic:
f_deg ▸ (natDegree_le_natDegree <| minpoly.min _ _ f_monic ?_)

Premises used: Polynomial.natDegree_le_natDegree, Eq.rec, minpoly.min