awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
x : L
c : ConjRootClass K L
⊢ Eq.{u_2 + 1} (α := L) ((aeval x : (a : K[X]) → L) c.minpoly : L) (0 : L) ↔ mk K x = c
have h : ∀ (x_1 : L),
  Eq.{u_2 + 1} (α := L) ((aeval x : (a : K[X]) → L) (ConjRootClass.minpoly (mk K x_1)) : L) (0 : L) ↔
    Eq (α := ConjRootClass K L) (mk K x) (mk K x_1)
Tactic: induction c
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
c : ConjRootClass K L
⊢ c.minpoly.rootSet L = c.carrier
have h : ∀ (x : L), x ∈ c.minpoly.rootSet L ↔ x ∈ c.carrier
Tactic: ext x
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
c : ConjRootClass K L
x : L
⊢ x ∈ c.minpoly.rootSet L ↔ x ∈ c.carrier
have h : c.minpoly ≠ 0 ∧ mk K x = c ↔ mk K x = c
Tactic: rw [mem_carrier, mem_rootSet, aeval_minpoly_iff x c]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
c : ConjRootClass K L
⊢ c.minpoly.Separable
have h : ∀ (x : L), Separable (ConjRootClass.minpoly (mk K x))
Tactic: induction c
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
c : ConjRootClass K L
inst_4 : Fintype (↑c.carrier : Type u_2)
⊢ c.minpoly.aroots L = c.carrier.toFinset.val
have simp_rw : c.minpoly.aroots L = (c.minpoly.rootSet L).toFinset.val
Tactic: simp_rw [← rootSet_minpoly_eq_carrier, rootSet_def, Finset.toFinset_coe, Multiset.toFinset_val,
    c.nodup_aroots_minpoly.dedup]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
c : ConjRootClass K L
inst_4 : Fintype (↑c.carrier : Type u_2)
simp_rw : c.minpoly.aroots L = (c.minpoly.rootSet L).toFinset.val
⊢ c.minpoly.aroots L = c.carrier.toFinset.val
have simp_rw₁ : c.minpoly.aroots L = (↑(c.minpoly.aroots L).toFinset : Set L).toFinset.val
Tactic: simp_rw [← rootSet_minpoly_eq_carrier, rootSet_def, Finset.toFinset_coe, Multiset.toFinset_val,
    c.nodup_aroots_minpoly.dedup]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
c : ConjRootClass K L
inst_4 : Fintype (↑c.carrier : Type u_2)
simp_rw : c.minpoly.aroots L = (c.minpoly.rootSet L).toFinset.val
simp_rw₁ : c.minpoly.aroots L = (↑(c.minpoly.aroots L).toFinset : Set L).toFinset.val
⊢ c.minpoly.aroots L = c.carrier.toFinset.val
have simp_rw₂ : c.minpoly.aroots L = (c.minpoly.aroots L).toFinset.val
Tactic: simp_rw [← rootSet_minpoly_eq_carrier, rootSet_def, Finset.toFinset_coe, Multiset.toFinset_val,
    c.nodup_aroots_minpoly.dedup]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
c : ConjRootClass K L
inst_4 : Fintype (↑c.carrier : Type u_2)
simp_rw : c.minpoly.aroots L = (c.minpoly.rootSet L).toFinset.val
simp_rw₁ : c.minpoly.aroots L = (↑(c.minpoly.aroots L).toFinset : Set L).toFinset.val
simp_rw₂ : c.minpoly.aroots L = (c.minpoly.aroots L).toFinset.val
⊢ c.minpoly.aroots L = c.carrier.toFinset.val
have simp_rw₃ : c.minpoly.aroots L = (c.minpoly.aroots L).dedup
Tactic: simp_rw [← rootSet_minpoly_eq_carrier, rootSet_def, Finset.toFinset_coe, Multiset.toFinset_val,
    c.nodup_aroots_minpoly.dedup]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
c : ConjRootClass K L
inst_4 : Fintype (↑c.carrier : Type u_2)
⊢ c.minpoly.aroots L = c.carrier.toFinset.val
have simp_rw : c.minpoly.aroots L = (c.minpoly.rootSet L).toFinset.val
Tactic: classical
  simp_rw [← rootSet_minpoly_eq_carrier, rootSet_def, Finset.toFinset_coe, Multiset.toFinset_val,
    c.nodup_aroots_minpoly.dedup]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
c : ConjRootClass K L
inst_4 : Fintype (↑c.carrier : Type u_2)
simp_rw : c.minpoly.aroots L = (c.minpoly.rootSet L).toFinset.val
⊢ c.minpoly.aroots L = c.carrier.toFinset.val
have simp_rw₁ : c.minpoly.aroots L = (↑(c.minpoly.aroots L).toFinset : Set L).toFinset.val
Tactic: classical
  simp_rw [← rootSet_minpoly_eq_carrier, rootSet_def, Finset.toFinset_coe, Multiset.toFinset_val,
    c.nodup_aroots_minpoly.dedup]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
c : ConjRootClass K L
inst_4 : Fintype (↑c.carrier : Type u_2)
simp_rw : c.minpoly.aroots L = (c.minpoly.rootSet L).toFinset.val
simp_rw₁ : c.minpoly.aroots L = (↑(c.minpoly.aroots L).toFinset : Set L).toFinset.val
⊢ c.minpoly.aroots L = c.carrier.toFinset.val
have simp_rw₂ : c.minpoly.aroots L = (c.minpoly.aroots L).toFinset.val
Tactic: classical
  simp_rw [← rootSet_minpoly_eq_carrier, rootSet_def, Finset.toFinset_coe, Multiset.toFinset_val,
    c.nodup_aroots_minpoly.dedup]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
c : ConjRootClass K L
inst_4 : Fintype (↑c.carrier : Type u_2)
simp_rw : c.minpoly.aroots L = (c.minpoly.rootSet L).toFinset.val
simp_rw₁ : c.minpoly.aroots L = (↑(c.minpoly.aroots L).toFinset : Set L).toFinset.val
simp_rw₂ : c.minpoly.aroots L = (c.minpoly.aroots L).toFinset.val
⊢ c.minpoly.aroots L = c.carrier.toFinset.val
have simp_rw₃ : c.minpoly.aroots L = (c.minpoly.aroots L).dedup
Tactic: classical
  simp_rw [← rootSet_minpoly_eq_carrier, rootSet_def, Finset.toFinset_coe, Multiset.toFinset_val,
    c.nodup_aroots_minpoly.dedup]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
inst_4 : Normal K L
c : ConjRootClass K L
inst_5 : Fintype (↑c.carrier : Type u_2)
⊢ Eq (α := L[X]) (map (algebraMap K L) c.minpoly)
    (∏ x ∈ c.carrier.toFinset, HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X]))
have simp_rw : Eq (α := L[X]) (map (algebraMap K L) c.minpoly)
  (Multiset.prod
    (Multiset.map (fun (x : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X]))
      (c.minpoly.aroots L).dedup))
Tactic: simp_rw [← rootSet_minpoly_eq_carrier, Finset.prod_eq_multiset_prod, rootSet_def,
    Finset.toFinset_coe, Multiset.toFinset_val]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
inst_4 : Normal K L
c : ConjRootClass K L
inst_5 : Fintype (↑c.carrier : Type u_2)
⊢ Eq (α := L[X]) (map (algebraMap K L) c.minpoly)
    (Multiset.prod
      (Multiset.map (fun (x : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X]))
        (c.minpoly.aroots L).dedup))
have rw : (roots (map (algebraMap K L) c.minpoly)).card = natDegree (map (algebraMap K L) c.minpoly)
Tactic: rw [Multiset.dedup_eq_self.mpr (nodup_roots c.separable_minpoly.map),
    prod_multiset_X_sub_C_of_monic_of_roots_card_eq (c.monic_minpoly.map _)]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
inst_4 : Normal K L
c : ConjRootClass K L
inst_5 : Fintype (↑c.carrier : Type u_2)
⊢ (roots (map (algebraMap K L) c.minpoly)).card = natDegree (map (algebraMap K L) c.minpoly)
have rw : Splits (map (algebraMap K L) c.minpoly)
Tactic: rw [← splits_iff_card_roots]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
inst_4 : Normal K L
c : ConjRootClass K L
inst_5 : Fintype (↑c.carrier : Type u_2)
⊢ Eq (α := L[X]) (map (algebraMap K L) c.minpoly)
    (∏ x ∈ c.carrier.toFinset, HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X]))
have simp_rw : Eq (α := L[X]) (map (algebraMap K L) c.minpoly)
  (∏ x ∈ (c.minpoly.rootSet L).toFinset, HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X]))
Tactic: classical
  simp_rw [← rootSet_minpoly_eq_carrier, Finset.prod_eq_multiset_prod, rootSet_def,
    Finset.toFinset_coe, Multiset.toFinset_val]
  rw [Multiset.dedup_eq_self.mpr (nodup_roots c.separable_minpoly.map),
    prod_multiset_X_sub_C_of_monic_of_roots_card_eq (c.monic_minpoly.map _)]
  rw [← splits_iff_card_roots]
  exact c.splits_minpoly
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
inst_4 : Normal K L
c : ConjRootClass K L
inst_5 : Fintype (↑c.carrier : Type u_2)
simp_rw :
  Eq (α := L[X]) (map (algebraMap K L) c.minpoly)
    (∏ x ∈ (c.minpoly.rootSet L).toFinset, HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X]))
⊢ Eq (α := L[X]) (map (algebraMap K L) c.minpoly)
    (∏ x ∈ c.carrier.toFinset, HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X]))
have simp_rw₁ : Eq (α := L[X]) (map (algebraMap K L) c.minpoly)
  (Multiset.prod
    (Multiset.map (fun (x : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X]))
      (c.minpoly.rootSet L).toFinset.val))
Tactic: classical
  simp_rw [← rootSet_minpoly_eq_carrier, Finset.prod_eq_multiset_prod, rootSet_def,
    Finset.toFinset_coe, Multiset.toFinset_val]
  rw [Multiset.dedup_eq_self.mpr (nodup_roots c.separable_minpoly.map),
    prod_multiset_X_sub_C_of_monic_of_roots_card_eq (c.monic_minpoly.map _)]
  rw [← splits_iff_card_roots]
  exact c.splits_minpoly
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
inst_4 : Normal K L
c : ConjRootClass K L
inst_5 : Fintype (↑c.carrier : Type u_2)
simp_rw :
  Eq (α := L[X]) (map (algebraMap K L) c.minpoly)
    (∏ x ∈ (c.minpoly.rootSet L).toFinset, HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X]))
simp_rw₁ :
  Eq (α := L[X]) (map (algebraMap K L) c.minpoly)
    (Multiset.prod
      (Multiset.map (fun (x : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X]))
        (c.minpoly.rootSet L).toFinset.val))
⊢ Eq (α := L[X]) (map (algebraMap K L) c.minpoly)
    (∏ x ∈ c.carrier.toFinset, HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X]))
have simp_rw₂ : Eq (α := L[X]) (map (algebraMap K L) c.minpoly)
  (Multiset.prod
    (Multiset.map (fun (x : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X]))
      (↑(c.minpoly.aroots L).toFinset : Set L).toFinset.val))
Tactic: classical
  simp_rw [← rootSet_minpoly_eq_carrier, Finset.prod_eq_multiset_prod, rootSet_def,
    Finset.toFinset_coe, Multiset.toFinset_val]
  rw [Multiset.dedup_eq_self.mpr (nodup_roots c.separable_minpoly.map),
    prod_multiset_X_sub_C_of_monic_of_roots_card_eq (c.monic_minpoly.map _)]
  rw [← splits_iff_card_roots]
  exact c.splits_minpoly
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
inst_4 : Normal K L
c : ConjRootClass K L
inst_5 : Fintype (↑c.carrier : Type u_2)
simp_rw :
  Eq (α := L[X]) (map (algebraMap K L) c.minpoly)
    (∏ x ∈ (c.minpoly.rootSet L).toFinset, HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X]))
simp_rw₁ :
  Eq (α := L[X]) (map (algebraMap K L) c.minpoly)
    (Multiset.prod
      (Multiset.map (fun (x : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X]))
        (c.minpoly.rootSet L).toFinset.val))
simp_rw₂ :
  Eq (α := L[X]) (map (algebraMap K L) c.minpoly)
    (Multiset.prod
      (Multiset.map (fun (x : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X]))
        (↑(c.minpoly.aroots L).toFinset : Set L).toFinset.val))
⊢ Eq (α := L[X]) (map (algebraMap K L) c.minpoly)
    (∏ x ∈ c.carrier.toFinset, HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X]))
have simp_rw₃ : Eq (α := L[X]) (map (algebraMap K L) c.minpoly)
  (Multiset.prod
    (Multiset.map (fun (x : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X]))
      (c.minpoly.aroots L).toFinset.val))
Tactic: classical
  simp_rw [← rootSet_minpoly_eq_carrier, Finset.prod_eq_multiset_prod, rootSet_def,
    Finset.toFinset_coe, Multiset.toFinset_val]
  rw [Multiset.dedup_eq_self.mpr (nodup_roots c.separable_minpoly.map),
    prod_multiset_X_sub_C_of_monic_of_roots_card_eq (c.monic_minpoly.map _)]
  rw [← splits_iff_card_roots]
  exact c.splits_minpoly
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
inst_4 : Normal K L
c : ConjRootClass K L
inst_5 : Fintype (↑c.carrier : Type u_2)
simp_rw :
  Eq (α := L[X]) (map (algebraMap K L) c.minpoly)
    (∏ x ∈ (c.minpoly.rootSet L).toFinset, HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X]))
simp_rw₁ :
  Eq (α := L[X]) (map (algebraMap K L) c.minpoly)
    (Multiset.prod
      (Multiset.map (fun (x : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X]))
        (c.minpoly.rootSet L).toFinset.val))
simp_rw₂ :
  Eq (α := L[X]) (map (algebraMap K L) c.minpoly)
    (Multiset.prod
      (Multiset.map (fun (x : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X]))
        (↑(c.minpoly.aroots L).toFinset : Set L).toFinset.val))
simp_rw₃ :
  Eq (α := L[X]) (map (algebraMap K L) c.minpoly)
    (Multiset.prod
      (Multiset.map (fun (x : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X]))
        (c.minpoly.aroots L).toFinset.val))
⊢ Eq (α := L[X]) (map (algebraMap K L) c.minpoly)
    (∏ x ∈ c.carrier.toFinset, HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X]))
have simp_rw₄ : Eq (α := L[X]) (map (algebraMap K L) c.minpoly)
  (Multiset.prod
    (Multiset.map (fun (x : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X]))
      (c.minpoly.aroots L).dedup))
Tactic: classical
  simp_rw [← rootSet_minpoly_eq_carrier, Finset.prod_eq_multiset_prod, rootSet_def,
    Finset.toFinset_coe, Multiset.toFinset_val]
  rw [Multiset.dedup_eq_self.mpr (nodup_roots c.separable_minpoly.map),
    prod_multiset_X_sub_C_of_monic_of_roots_card_eq (c.monic_minpoly.map _)]
  rw [← splits_iff_card_roots]
  exact c.splits_minpoly
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
inst_4 : Normal K L
c : ConjRootClass K L
inst_5 : Fintype (↑c.carrier : Type u_2)
simp_rw :
  Eq (α := L[X]) (map (algebraMap K L) c.minpoly)
    (∏ x ∈ (c.minpoly.rootSet L).toFinset, HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X]))
simp_rw₁ :
  Eq (α := L[X]) (map (algebraMap K L) c.minpoly)
    (Multiset.prod
      (Multiset.map (fun (x : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X]))
        (c.minpoly.rootSet L).toFinset.val))
simp_rw₂ :
  Eq (α := L[X]) (map (algebraMap K L) c.minpoly)
    (Multiset.prod
      (Multiset.map (fun (x : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X]))
        (↑(c.minpoly.aroots L).toFinset : Set L).toFinset.val))
simp_rw₃ :
  Eq (α := L[X]) (map (algebraMap K L) c.minpoly)
    (Multiset.prod
      (Multiset.map (fun (x : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X]))
        (c.minpoly.aroots L).toFinset.val))
simp_rw₄ :
  Eq (α := L[X]) (map (algebraMap K L) c.minpoly)
    (Multiset.prod
      (Multiset.map (fun (x : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X]))
        (c.minpoly.aroots L).dedup))
⊢ Eq (α := L[X]) (map (algebraMap K L) c.minpoly)
    (∏ x ∈ c.carrier.toFinset, HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X]))
have simp_rw₅ : (roots (map (algebraMap K L) c.minpoly)).card = natDegree (map (algebraMap K L) c.minpoly)
Tactic: classical
  simp_rw [← rootSet_minpoly_eq_carrier, Finset.prod_eq_multiset_prod, rootSet_def,
    Finset.toFinset_coe, Multiset.toFinset_val]
  rw [Multiset.dedup_eq_self.mpr (nodup_roots c.separable_minpoly.map),
    prod_multiset_X_sub_C_of_monic_of_roots_card_eq (c.monic_minpoly.map _)]
  rw [← splits_iff_card_roots]
  exact c.splits_minpoly
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
inst_4 : Normal K L
c : ConjRootClass K L
inst_5 : Fintype (↑c.carrier : Type u_2)
simp_rw :
  Eq (α := L[X]) (map (algebraMap K L) c.minpoly)
    (∏ x ∈ (c.minpoly.rootSet L).toFinset, HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X]))
simp_rw₁ :
  Eq (α := L[X]) (map (algebraMap K L) c.minpoly)
    (Multiset.prod
      (Multiset.map (fun (x : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X]))
        (c.minpoly.rootSet L).toFinset.val))
simp_rw₂ :
  Eq (α := L[X]) (map (algebraMap K L) c.minpoly)
    (Multiset.prod
      (Multiset.map (fun (x : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X]))
        (↑(c.minpoly.aroots L).toFinset : Set L).toFinset.val))
simp_rw₃ :
  Eq (α := L[X]) (map (algebraMap K L) c.minpoly)
    (Multiset.prod
      (Multiset.map (fun (x : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X]))
        (c.minpoly.aroots L).toFinset.val))
simp_rw₄ :
  Eq (α := L[X]) (map (algebraMap K L) c.minpoly)
    (Multiset.prod
      (Multiset.map (fun (x : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X]))
        (c.minpoly.aroots L).dedup))
simp_rw₅ : (roots (map (algebraMap K L) c.minpoly)).card = natDegree (map (algebraMap K L) c.minpoly)
⊢ Eq (α := L[X]) (map (algebraMap K L) c.minpoly)
    (∏ x ∈ c.carrier.toFinset, HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X]))
have simp_rw₆ : Splits (map (algebraMap K L) c.minpoly)
Tactic: classical
  simp_rw [← rootSet_minpoly_eq_carrier, Finset.prod_eq_multiset_prod, rootSet_def,
    Finset.toFinset_coe, Multiset.toFinset_val]
  rw [Multiset.dedup_eq_self.mpr (nodup_roots c.separable_minpoly.map),
    prod_multiset_X_sub_C_of_monic_of_roots_card_eq (c.monic_minpoly.map _)]
  rw [← splits_iff_card_roots]
  exact c.splits_minpoly
-- 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 : Algebra A B
x : B
p : A[X]
pmonic : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
pmin :
  ∀ (q : A[X]),
    q.Monic → Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) (0 : B) → p.degree ≤ q.degree
⊢ p = minpoly A x
have hx : IsIntegral A x
Tactic: have hx : IsIntegral A x := ⟨p, pmonic, hp⟩
-- 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
p : A[X]
pmonic : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
pmin :
  ∀ (q : A[X]),
    q.Monic → Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) (0 : B) → p.degree ≤ q.degree
hx : IsIntegral A x
⊢ p = minpoly A x
have symm : minpoly A x = p
Tactic: symm
-- 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
p : A[X]
pmonic : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
pmin :
  ∀ (q : A[X]),
    q.Monic → Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) (0 : B) → p.degree ≤ q.degree
hx : IsIntegral A x
⊢ minpoly A x = p
have h : minpoly A x - p = 0
Tactic: apply eq_of_sub_eq_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 : B
p : A[X]
pmonic : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
pmin :
  ∀ (q : A[X]),
    q.Monic → Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) (0 : B) → p.degree ≤ q.degree
hx : IsIntegral A x
⊢ minpoly A x - p = 0
have h : ∀ (hnz : ¬minpoly A x - p = 0), False
Tactic: by_contra hnz
-- 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
p : A[X]
pmonic : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
pmin :
  ∀ (q : A[X]),
    q.Monic → Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) (0 : B) → p.degree ≤ q.degree
hx : IsIntegral A x
hnz : ¬minpoly A x - p = 0
⊢ False
have h : (minpoly A x - p).degree < degree (minpoly A x)
Tactic: apply degree_le_of_ne_zero A x hnz (by simp [hp]) |>.not_gt
-- 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
p : A[X]
pmonic : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
pmin :
  ∀ (q : A[X]),
    q.Monic → Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) (0 : B) → p.degree ≤ q.degree
hx : IsIntegral A x
hnz : ¬minpoly A x - p = 0
⊢ (minpoly A x - p).degree < degree (minpoly A x)
have h : leadingCoeff (minpoly A x) = p.leadingCoeff
Tactic: apply degree_sub_lt _ (minpoly.ne_zero hx)
-- 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
p : A[X]
pmonic : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
pmin :
  ∀ (q : A[X]),
    q.Monic → Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) (0 : B) → p.degree ≤ q.degree
hx : IsIntegral A x
hnz : ¬minpoly A x - p = 0
h : leadingCoeff (minpoly A x) = p.leadingCoeff
⊢ (minpoly A x - p).degree < degree (minpoly A x)
have apply : degree (minpoly A x) = p.degree
Tactic: apply degree_sub_lt _ (minpoly.ne_zero hx)
-- 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
p : A[X]
pmonic : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
pmin :
  ∀ (q : A[X]),
    q.Monic → Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) (0 : B) → p.degree ≤ q.degree
hx : IsIntegral A x
hnz : ¬minpoly A x - p = 0
⊢ leadingCoeff (minpoly A x) = p.leadingCoeff
have h : 1 = p.leadingCoeff
Tactic: rw [(monic hx).leadingCoeff, pmonic.leadingCoeff]