awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
A : Type u_1
inst : Field A
B : Type u_3
inst_1 : Ring B
inst_2 : Algebra A B
x : B
⊢ minpoly A (-x) = HPow.hPow (α := A[X]) (-1) (natDegree (minpoly A x)) * Polynomial.comp (minpoly A x) (-X)
have pos : ∀ (hx : IsIntegral A x),
  minpoly A (-x) = HPow.hPow (α := A[X]) (-1) (natDegree (minpoly A x)) * Polynomial.comp (minpoly A x) (-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 : Ring B
inst_2 : Algebra A B
x : B
pos :
  ∀ (hx : IsIntegral A x),
    minpoly A (-x) = HPow.hPow (α := A[X]) (-1) (natDegree (minpoly A x)) * Polynomial.comp (minpoly A x) (-X)
⊢ minpoly A (-x) = HPow.hPow (α := A[X]) (-1) (natDegree (minpoly A x)) * Polynomial.comp (minpoly A x) (-X)
have neg₁ : ∀ (hx : ¬IsIntegral A x),
  minpoly A (-x) = HPow.hPow (α := A[X]) (-1) (natDegree (minpoly A x)) * Polynomial.comp (minpoly A x) (-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 : Ring B
inst_2 : Algebra A B
x : B
hx : IsIntegral A x
⊢ minpoly A (-x) = HPow.hPow (α := A[X]) (-1) (natDegree (minpoly A x)) * Polynomial.comp (minpoly A x) (-X)
have pos : Eq.{u_3 + 1} (α := B)
  ((Polynomial.aeval (-x) : (a : A[X]) → B)
      (HPow.hPow (α := A[X]) (-1) (natDegree (minpoly A x)) * Polynomial.comp (minpoly A x) (-X)) :
    B)
  (0 : B)
Tactic: refine (minpoly.unique _ _ ((minpoly.monic hx).neg_one_pow_natDegree_mul_comp_neg_X)
        ?_ 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 : Ring B
inst_2 : Algebra A B
x : B
hx : IsIntegral A x
pos :
  Eq.{u_3 + 1} (α := B)
    ((Polynomial.aeval (-x) : (a : A[X]) → B)
        (HPow.hPow (α := A[X]) (-1) (natDegree (minpoly A x)) * Polynomial.comp (minpoly A x) (-X)) :
      B)
    (0 : B)
⊢ minpoly A (-x) = HPow.hPow (α := A[X]) (-1) (natDegree (minpoly A x)) * Polynomial.comp (minpoly A x) (-X)
have pos₁ : ∀ (q : A[X]) (qmo : q.Monic) (hq : Eq.{u_3 + 1} (α := B) ((Polynomial.aeval (-x) : (a : A[X]) → B) q : B) (0 : B)),
  (HPow.hPow (α := A[X]) (-1) (natDegree (minpoly A x)) * Polynomial.comp (minpoly A x) (-X)).degree ≤ q.degree
Tactic: refine (minpoly.unique _ _ ((minpoly.monic hx).neg_one_pow_natDegree_mul_comp_neg_X)
        ?_ 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 : Ring B
inst_2 : Algebra A B
x : B
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq : Eq.{u_3 + 1} (α := B) ((Polynomial.aeval (-x) : (a : A[X]) → B) q : B) (0 : B)
⊢ (HPow.hPow (α := A[X]) (-1) (natDegree (minpoly A x)) * Polynomial.comp (minpoly A x) (-X)).degree ≤ q.degree
have this : Eq.{u_3 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) (HPow.hPow (α := A[X]) (-1) q.natDegree * q.comp (-X)) : B)
  (0 : B)
Tactic: have : (Polynomial.aeval x) ((-1) ^ q.natDegree * q.comp (-X)) = 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 : Ring B
inst_2 : Algebra A B
x : B
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq : Eq.{u_3 + 1} (α := B) ((Polynomial.aeval (-x) : (a : A[X]) → B) q : B) (0 : B)
this :
  Eq.{u_3 + 1} (α := B)
    ((Polynomial.aeval x : (a : A[X]) → B) (HPow.hPow (α := A[X]) (-1) q.natDegree * q.comp (-X)) : B) (0 : B)
⊢ (HPow.hPow (α := A[X]) (-1) (natDegree (minpoly A x)) * Polynomial.comp (minpoly A x) (-X)).degree ≤ q.degree
have H : degree (minpoly A x) ≤ (HPow.hPow (α := A[X]) (-1) q.natDegree * q.comp (-X)).degree
Tactic: have H := minpoly.min A x qmo.neg_one_pow_natDegree_mul_comp_neg_X 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 : Ring B
inst_2 : Algebra A B
x : B
hx : ¬IsIntegral A x
⊢ minpoly A (-x) = HPow.hPow (α := A[X]) (-1) (natDegree (minpoly A x)) * Polynomial.comp (minpoly A x) (-X)
have neg₁ : 0 = HPow.hPow (α := A[X]) (-1) (natDegree.{u_1} (R := A) 0) * 0
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 : Ring B
inst_2 : Algebra A B
x : B
hx : ¬IsIntegral A x
neg₁ : 0 = HPow.hPow (α := A[X]) (-1) (natDegree.{u_1} (R := A) 0) * 0
⊢ minpoly A (-x) = HPow.hPow (α := A[X]) (-1) (natDegree (minpoly A x)) * Polynomial.comp (minpoly A x) (-X)
have neg₂ : ¬IsIntegral A (-x)
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
R : Type u_3
S : Type u_4
T : Type u_5
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : Ring S
inst_4 : Ring T
inst_5 : IsDomain S
inst_6 : IsDomain T
inst_7 : Algebra R S
inst_8 : Algebra A T
inst_9 : Algebra.IsIntegral R S
f : R ≃+* A
g : S ≃+* T
hcomp :
  Eq (α := R →+* T) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A T) (↑f : R →+* A))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : S →+* T) (algebraMap R S))
x : S
⊢ Eq (α := A[X]) (map (↑f : R →+* A) (minpoly R x)) (minpoly.{u_1, u_5} A (B := T) ((g : (a : S) → T) x : T))
have refine_1 : Irreducible (M := A[X]) (map (↑f : R →+* A) (minpoly R x))
Tactic: refine minpoly.eq_of_irreducible_of_monic ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
A : Type u_1
inst : Field A
R : Type u_3
S : Type u_4
T : Type u_5
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : Ring S
inst_4 : Ring T
inst_5 : IsDomain S
inst_6 : IsDomain T
inst_7 : Algebra R S
inst_8 : Algebra A T
inst_9 : Algebra.IsIntegral R S
f : R ≃+* A
g : S ≃+* T
hcomp :
  Eq (α := R →+* T) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A T) (↑f : R →+* A))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : S →+* T) (algebraMap R S))
x : S
refine_1 : Irreducible (M := A[X]) (map (↑f : R →+* A) (minpoly R x))
⊢ Eq (α := A[X]) (map (↑f : R →+* A) (minpoly R x)) (minpoly.{u_1, u_5} A (B := T) ((g : (a : S) → T) x : T))
have refine_2 : Eq.{u_5 + 1} (α := T)
  (((Polynomial.aeval ((g : (a : S) → T) x) : A[X] →ₐ[A] T) : (a : A[X]) → T) (map (↑f : R →+* A) (minpoly R x)) : T)
  (0 : T)
Tactic: refine minpoly.eq_of_irreducible_of_monic ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
A : Type u_1
inst : Field A
R : Type u_3
S : Type u_4
T : Type u_5
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : Ring S
inst_4 : Ring T
inst_5 : IsDomain S
inst_6 : IsDomain T
inst_7 : Algebra R S
inst_8 : Algebra A T
inst_9 : Algebra.IsIntegral R S
f : R ≃+* A
g : S ≃+* T
hcomp :
  Eq (α := R →+* T) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A T) (↑f : R →+* A))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : S →+* T) (algebraMap R S))
x : S
refine_1 : Irreducible (M := A[X]) (map (↑f : R →+* A) (minpoly R x))
refine_2 :
  Eq.{u_5 + 1} (α := T)
    (((Polynomial.aeval ((g : (a : S) → T) x) : A[X] →ₐ[A] T) : (a : A[X]) → T) (map (↑f : R →+* A) (minpoly R x)) : T)
    (0 : T)
⊢ Eq (α := A[X]) (map (↑f : R →+* A) (minpoly R x)) (minpoly.{u_1, u_5} A (B := T) ((g : (a : S) → T) x : T))
have refine_3 : Monic (map (↑f : R →+* A) (minpoly R x))
Tactic: refine minpoly.eq_of_irreducible_of_monic ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
A : Type u_1
inst : Field A
R : Type u_3
S : Type u_4
T : Type u_5
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : Ring S
inst_4 : Ring T
inst_5 : IsDomain S
inst_6 : IsDomain T
inst_7 : Algebra R S
inst_8 : Algebra A T
inst_9 : Algebra.IsIntegral R S
f : R ≃+* A
g : S ≃+* T
hcomp :
  Eq (α := R →+* T) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A T) (↑f : R →+* A))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : S →+* T) (algebraMap R S))
x : S
⊢ Irreducible (M := A[X]) (map (↑f : R →+* A) (minpoly R x))
have refine_1 : Irreducible (M := R[X]) (minpoly R x)
Tactic: rw [← mapEquiv_apply, MulEquiv.irreducible_iff]
-- 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_1 : B
F : Type u_3
E : Type u_4
K : Type u_5
inst_3 : Field F
inst_4 : Ring E
inst_5 : CommRing K
inst_6 : IsDomain K
inst_7 : Algebra F E
inst_8 : Algebra F K
inst_9 : FiniteDimensional F E
φ : E →ₐ[F] K
x : (↑(range (ι := Fin (Module.finrank F E)) (⇑(Module.finBasis F E) : (a : Fin (Module.finrank F E)) → E)) : Type u_4)
⊢ Membership.mem (α := K) (aroots (minpoly F (↑x : E)) K) ((φ : (a : E) → K) (↑x : E) : K)
have rw : eval₂ (algebraMap F K) ((φ : (a : E) → K) (↑x : E)) (minpoly F (↑x : E)) = 0
Tactic: rw [mem_roots_map (minpoly.ne_zero_of_finite F x.val),
      ← aeval_def, aeval_algHom_apply, minpoly.aeval, map_zero]
-- 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_1 : B
F : Type u_3
E : Type u_4
K : Type u_5
inst_3 : Field F
inst_4 : Ring E
inst_5 : CommRing K
inst_6 : IsDomain K
inst_7 : Algebra F E
inst_8 : Algebra F K
inst_9 : FiniteDimensional F E
φ : E →ₐ[F] K
x : (↑(range (ι := Fin (Module.finrank F E)) (⇑(Module.finBasis F E) : (a : Fin (Module.finrank F E)) → E)) : Type u_4)
rw : eval₂ (algebraMap F K) ((φ : (a : E) → K) (↑x : E)) (minpoly F (↑x : E)) = 0
⊢ Membership.mem (α := K) (aroots (minpoly F (↑x : E)) K) ((φ : (a : E) → K) (↑x : E) : K)
have rw₁ : Eq.{u_5 + 1} (α := K)
  (((Polynomial.aeval ((φ : (a : E) → K) (↑x : E)) : F[X] →ₐ[F] K) : (a : F[X]) → K) (minpoly F (↑x : E)) : K) (0 : K)
Tactic: rw [mem_roots_map (minpoly.ne_zero_of_finite F x.val),
      ← aeval_def, aeval_algHom_apply, minpoly.aeval, map_zero]
-- 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_1 : B
F : Type u_3
E : Type u_4
K : Type u_5
inst_3 : Field F
inst_4 : Ring E
inst_5 : CommRing K
inst_6 : IsDomain K
inst_7 : Algebra F E
inst_8 : Algebra F K
inst_9 : FiniteDimensional F E
φ : E →ₐ[F] K
x : (↑(range (ι := Fin (Module.finrank F E)) (⇑(Module.finBasis F E) : (a : Fin (Module.finrank F E)) → E)) : Type u_4)
rw : eval₂ (algebraMap F K) ((φ : (a : E) → K) (↑x : E)) (minpoly F (↑x : E)) = 0
rw₁ :
  Eq.{u_5 + 1} (α := K)
    (((Polynomial.aeval ((φ : (a : E) → K) (↑x : E)) : F[X] →ₐ[F] K) : (a : F[X]) → K) (minpoly F (↑x : E)) : K) (0 : K)
⊢ Membership.mem (α := K) (aroots (minpoly F (↑x : E)) K) ((φ : (a : E) → K) (↑x : E) : K)
have rw₂ : Eq.{u_5 + 1} (α := K) ((φ : (a : E) → K) ((Polynomial.aeval (↑x : E) : (a : F[X]) → E) (minpoly F (↑x : E)) : E) : K)
  (0 : K)
Tactic: rw [mem_roots_map (minpoly.ne_zero_of_finite F x.val),
      ← aeval_def, aeval_algHom_apply, minpoly.aeval, map_zero]
-- 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_1 : B
F : Type u_3
E : Type u_4
K : Type u_5
inst_3 : Field F
inst_4 : Ring E
inst_5 : CommRing K
inst_6 : IsDomain K
inst_7 : Algebra F E
inst_8 : Algebra F K
inst_9 : FiniteDimensional F E
φ : E →ₐ[F] K
x : (↑(range (ι := Fin (Module.finrank F E)) (⇑(Module.finBasis F E) : (a : Fin (Module.finrank F E)) → E)) : Type u_4)
rw : eval₂ (algebraMap F K) ((φ : (a : E) → K) (↑x : E)) (minpoly F (↑x : E)) = 0
rw₁ :
  Eq.{u_5 + 1} (α := K)
    (((Polynomial.aeval ((φ : (a : E) → K) (↑x : E)) : F[X] →ₐ[F] K) : (a : F[X]) → K) (minpoly F (↑x : E)) : K) (0 : K)
rw₂ :
  Eq.{u_5 + 1} (α := K) ((φ : (a : E) → K) ((Polynomial.aeval (↑x : E) : (a : F[X]) → E) (minpoly F (↑x : E)) : E) : K)
    (0 : K)
⊢ Membership.mem (α := K) (aroots (minpoly F (↑x : E)) K) ((φ : (a : E) → K) (↑x : E) : K)
have rw₃ : Eq.{u_5 + 1} (α := K) ((φ : (a : E) → K) 0 : K) (0 : K)
Tactic: rw [mem_roots_map (minpoly.ne_zero_of_finite F x.val),
      ← aeval_def, aeval_algHom_apply, minpoly.aeval, map_zero]
-- 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_1 : B
F : Type u_3
E : Type u_4
K : Type u_5
inst_3 : Field F
inst_4 : Ring E
inst_5 : CommRing K
inst_6 : IsDomain K
inst_7 : Algebra F E
inst_8 : Algebra F K
inst_9 : FiniteDimensional F E
φ : E →ₐ[F] K
x : (↑(range (ι := Fin (Module.finrank F E)) (⇑(Module.finBasis F E) : (a : Fin (Module.finrank F E)) → E)) : Type u_4)
rw : eval₂ (algebraMap F K) ((φ : (a : E) → K) (↑x : E)) (minpoly F (↑x : E)) = 0
rw₁ :
  Eq.{u_5 + 1} (α := K)
    (((Polynomial.aeval ((φ : (a : E) → K) (↑x : E)) : F[X] →ₐ[F] K) : (a : F[X]) → K) (minpoly F (↑x : E)) : K) (0 : K)
rw₂ :
  Eq.{u_5 + 1} (α := K) ((φ : (a : E) → K) ((Polynomial.aeval (↑x : E) : (a : F[X]) → E) (minpoly F (↑x : E)) : E) : K)
    (0 : K)
rw₃ : Eq.{u_5 + 1} (α := K) ((φ : (a : E) → K) 0 : K) (0 : K)
⊢ Membership.mem (α := K) (aroots (minpoly F (↑x : E)) K) ((φ : (a : E) → K) (↑x : E) : K)
have rw₄ : Eq.{u_5 + 1} (α := K) 0 0
Tactic: rw [mem_roots_map (minpoly.ne_zero_of_finite F x.val),
      ← aeval_def, aeval_algHom_apply, minpoly.aeval, map_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
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 :
  Eq (α :=
    (x :
        (↑(range (ι := Fin (Module.finrank F E)) (⇑(Module.finBasis F E) : (a : Fin (Module.finrank F E)) → E)) :
          Type u_4)) →
      { l : K // l ∈ aroots (minpoly F (↑x : E)) K })
    (rootsOfMinPolyPiType F E K f) (rootsOfMinPolyPiType F E K g)
this :
  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)
⊢ f = g
have rwa : ∀
  (this :
    Eq (α := (a : E) → K)
      (⇑(↑f : [inst_7 : FunLike (E →ₐ[F] K) E K] → [SemilinearMapClass (E →ₐ[F] K) (RingHom.id F) E K] → E →ₗ[F] K) :
        (a : E) → K)
      (⇑(↑g : [inst_7 : FunLike (E →ₐ[F] K) E K] → [SemilinearMapClass (E →ₐ[F] K) (RingHom.id F) E K] → E →ₗ[F] K) :
        (a : E) → K)),
  Eq (α := (a : E) → K) (⇑f : (a : E) → K) (⇑g : (a : E) → K)
Tactic: rwa [DFunLike.ext'_iff] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
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 :
  Eq (α :=
    (x :
        (↑(range (ι := Fin (Module.finrank F E)) (⇑(Module.finBasis F E) : (a : Fin (Module.finrank F E)) → E)) :
          Type u_4)) →
      { l : K // l ∈ aroots (minpoly F (↑x : E)) K })
    (rootsOfMinPolyPiType F E K f) (rootsOfMinPolyPiType F E K g)
⊢ f = g
have suffices : 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: suffices (f : E →ₗ[F] K) = (g : E →ₗ[F] K) by rwa [DFunLike.ext'_iff] at this ⊢
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (hypothesis)
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 :
  Eq (α :=
    (x :
        (↑(range (ι := Fin (Module.finrank F E)) (⇑(Module.finBasis F E) : (a : Fin (Module.finrank F E)) → E)) :
          Type u_4)) →
      { l : K // l ∈ aroots (minpoly F (↑x : E)) K })
    (rootsOfMinPolyPiType F E K f) (rootsOfMinPolyPiType F E K g)
⊢ 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)
have 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)
Tactic: rw [funext_iff] at h
Cleared hypotheses: 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
⊢ Prime (M := A[X]) (minpoly A x)
have refine : ∀ (a b : A[X]), minpoly A x ∣ a * b → minpoly A x ∣ a ∨ minpoly A x ∣ b
Tactic: refine ⟨minpoly.ne_zero hx, not_isUnit A x, ?_⟩
-- 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
p q d : A[X]
h : p * q = minpoly A x * d
⊢ minpoly A x ∣ p ∨ minpoly A x ∣ q
have this : 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]
-- 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
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)
⊢ minpoly A x ∣ p ∨ minpoly A x ∣ q
have 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)
Tactic: replace : Polynomial.aeval x p = 0 ∨ Polynomial.aeval x q = 0 := by simpa
Cleared hypotheses: this
-- 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
y : A
h : IsRoot (minpoly A x) y
⊢ (algebraMap A B : (a : A) → B) y = x
have key : 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))
-- 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
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])
⊢ (algebraMap A B : (a : A) → B) y = x
have this : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) (minpoly A x) : B) (0 : B)
Tactic: have := aeval A x
-- 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)
⊢ (algebraMap A B : (a : A) → B) y = x
have 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
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
⊢ (algebraMap A B : (a : A) → B) y = x
have 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
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
⊢ (algebraMap A B : (a : A) → B) y = x
have 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
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
⊢ (algebraMap A B : (a : A) → B) y = x
have rwa₃ : ∀ (this : HSub.hSub (β := B) x ((algebraMap A B : (a : A) → B) y : B) = 0), (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