awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : PerfectField k
inst_4 : Algebra.EssFiniteType k K
h : CharZero k
s : Finset K
hs : Eq (α := IntermediateField k K) (adjoin k (↑s : Set K)) ⊤
this : Algebra.IsAlgebraic (↥(Algebra.adjoin k (↑s : Set K))) K
t : Finset K
hts : (↑t : Set K) ⊆ (↑s : Set K)
ht :
  IsTranscendenceBasis.{u_2, u_1, u_2} (ι := { x : K // x ∈ (↑t : Set K) }) k
    (Subtype.val (p := fun (x : K) ↦ x ∈ (↑t : Set K)))
⊢ Algebra.IsAlgebraic (↥(adjoin k (↑t : Set K))) K
have h : ∀ (x : K),
  (↑t : Set K) = Set.range (ι := { x : K // x ∈ (↑t : Set K) }) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑t : Set K)))
Tactic: convert! ht.isAlgebraic_field
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : PerfectField k
inst_4 : Algebra.EssFiniteType k K
h_1 : CharZero k
s : Finset K
hs : Eq (α := IntermediateField k K) (adjoin k (↑s : Set K)) ⊤
this : Algebra.IsAlgebraic (↥(Algebra.adjoin k (↑s : Set K))) K
t : Finset K
hts : (↑t : Set K) ⊆ (↑s : Set K)
ht :
  IsTranscendenceBasis.{u_2, u_1, u_2} (ι := { x : K // x ∈ (↑t : Set K) }) k
    (Subtype.val (p := fun (x : K) ↦ x ∈ (↑t : Set K)))
h :
  ∀ (x : K),
    (↑t : Set K) = Set.range (ι := { x : K // x ∈ (↑t : Set K) }) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑t : Set K)))
⊢ Algebra.IsAlgebraic (↥(adjoin k (↑t : Set K))) K
have h₁ : ↥(adjoin k (↑t : Set K)) =
    ↥(adjoin k (Set.range (ι := { x : K // x ∈ (↑t : Set K) }) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑t : Set K))))) →
  (↑t : Set K) = Set.range (ι := { x : K // x ∈ (↑t : Set K) }) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑t : Set K)))
Tactic: convert! ht.isAlgebraic_field
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : PerfectField k
inst_4 : Algebra.EssFiniteType k K
h_1 : CharZero k
s : Finset K
hs : Eq (α := IntermediateField k K) (adjoin k (↑s : Set K)) ⊤
this : Algebra.IsAlgebraic (↥(Algebra.adjoin k (↑s : Set K))) K
t : Finset K
hts : (↑t : Set K) ⊆ (↑s : Set K)
ht :
  IsTranscendenceBasis.{u_2, u_1, u_2} (ι := { x : K // x ∈ (↑t : Set K) }) k
    (Subtype.val (p := fun (x : K) ↦ x ∈ (↑t : Set K)))
h :
  ∀ (x : K),
    (↑t : Set K) = Set.range (ι := { x : K // x ∈ (↑t : Set K) }) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑t : Set K)))
h₁ :
  ↥(adjoin k (↑t : Set K)) =
      ↥(adjoin k (Set.range (ι := { x : K // x ∈ (↑t : Set K) }) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑t : Set K))))) →
    (↑t : Set K) = Set.range (ι := { x : K // x ∈ (↑t : Set K) }) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑t : Set K)))
⊢ Algebra.IsAlgebraic (↥(adjoin k (↑t : Set K))) K
have h₂ : ↥(adjoin k (↑t : Set K)) =
    ↥(adjoin k (Set.range (ι := { x : K // x ∈ (↑t : Set K) }) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑t : Set K))))) →
  HEq.{u_2 + 1} (α := CommRing ↥(adjoin k (↑t : Set K))) Field.toCommRing (β :=
      CommRing
        ↥(adjoin k
            (Set.range (ι := { x : K // x ∈ (↑t : Set K) }) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑t : Set K))))))
      Field.toCommRing →
    (↑t : Set K) = Set.range (ι := { x : K // x ∈ (↑t : Set K) }) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑t : Set K)))
Tactic: convert! ht.isAlgebraic_field
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (hypothesis)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : PerfectField k
inst_4 : Algebra.EssFiniteType k K
h : CharZero k
s : Finset K
hs : Eq (α := IntermediateField k K) (adjoin k (↑s : Set K)) ⊤
this : Algebra.IsAlgebraic (↥(Algebra.adjoin k (↑s : Set K))) K
t : Finset K
hts : (↑t : Set K) ⊆ (↑s : Set K)
ht :
  IsTranscendenceBasis.{u_2, u_1, u_2} (ι := { x : K // x ∈ (↑t : Set K) }) k
    (Subtype.val (p := fun (x : K) ↦ x ∈ (↑t : Set K)))
⊢ ∃ (s : Finset K),
    IsTranscendenceBasis.{u_2, u_1, u_2} (ι := ↥s) k (Subtype.val (p := fun (x : K) ↦ x ∈ s)) ∧
      Algebra.IsSeparable (↥(adjoin k (↑s : Set K))) K
have this₁ : Algebra.IsAlgebraic (↥(adjoin k (↑t : Set K))) K
Tactic: have : Algebra.IsAlgebraic (IntermediateField.adjoin k (t : Set K)) K := by
      convert! ht.isAlgebraic_field <;> simp
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (hypothesis)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : PerfectField k
inst_4 : Algebra.EssFiniteType k K
p : ℕ
hp : Fact (Nat.Prime p)
hpk : CharP k p
⊢ ∃ (s : Finset K),
    IsTranscendenceBasis.{u_2, u_1, u_2} (ι := ↥s) k (Subtype.val (p := fun (x : K) ↦ x ∈ s)) ∧
      Algebra.IsSeparable (↥(adjoin k (↑s : Set K))) K
have this : ExpChar k p
Tactic: have : ExpChar k p := .prime hp.out
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (hypothesis)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : PerfectField k
inst_4 : Algebra.EssFiniteType k K
p : ℕ
hp : Fact (Nat.Prime p)
hpk : CharP k p
this : ExpChar k p
⊢ ∃ (s : Finset K),
    IsTranscendenceBasis.{u_2, u_1, u_2} (ι := ↥s) k (Subtype.val (p := fun (x : K) ↦ x ∈ s)) ∧
      Algebra.IsSeparable (↥(adjoin k (↑s : Set K))) K
have this₁ : CharP K p
Tactic: have : CharP K p := .of_ringHom_of_ne_zero (algebraMap k K) p hp.out.ne_zero
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : PerfectField k
inst_4 : Algebra.EssFiniteType k K
p : ℕ
hp : Fact (Nat.Prime p)
hpk : CharP k p
this_1 : ExpChar k p
this : CharP K p
⊢ ∃ (s : Finset K),
    IsTranscendenceBasis.{u_2, u_1, u_2} (ι := ↥s) k (Subtype.val (p := fun (x : K) ↦ x ∈ s)) ∧
      Algebra.IsSeparable (↥(adjoin k (↑s : Set K))) K
have inr : ∀ (s : Finset K) (hs : LinearIndepOn k id (↑s : Set K)), LinearIndepOn k (M := K) (fun (x : K) ↦ x ^ p) (↑s : Set K)
Tactic: refine exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_essFiniteType
    p hp.out fun s hs ↦ ?_
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : PerfectField k
inst_4 : Algebra.EssFiniteType k K
p : ℕ
hp : Fact (Nat.Prime p)
hpk : CharP k p
this_1 : ExpChar k p
this : CharP K p
s : Finset K
hs : LinearIndepOn k id (↑s : Set K)
⊢ LinearIndepOn k (M := K) (fun (x : K) ↦ x ^ p) (↑s : Set K)
have inr : ∀ (r : k), Eq (α := k) ((RingEquiv.symm (frobeniusEquiv k p) : (a : k) → k) r : k) (0 : k) → r = 0
Tactic: apply hs.map_of_injective_injective (frobeniusEquiv k p).symm (frobenius K p).toAddMonoidHom
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : PerfectField k
inst_4 : Algebra.EssFiniteType k K
p : ℕ
hp : Fact (Nat.Prime p)
hpk : CharP k p
this_1 : ExpChar k p
this : CharP K p
s : Finset K
hs : LinearIndepOn k id (↑s : Set K)
inr : ∀ (r : k), Eq (α := k) ((RingEquiv.symm (frobeniusEquiv k p) : (a : k) → k) r : k) (0 : k) → r = 0
⊢ LinearIndepOn k (M := K) (fun (x : K) ↦ x ^ p) (↑s : Set K)
have inr₁ : ∀ (m : K), Eq (α := K) (((RingHom.toAddMonoidHom (frobenius K p) : K →+ K) : (a : K) → K) m : K) (0 : K) → m = 0
Tactic: apply hs.map_of_injective_injective (frobeniusEquiv k p).symm (frobenius K p).toAddMonoidHom
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : PerfectField k
inst_4 : Algebra.EssFiniteType k K
p : ℕ
hp : Fact (Nat.Prime p)
hpk : CharP k p
this_1 : ExpChar k p
this : CharP K p
s : Finset K
hs : LinearIndepOn k id (↑s : Set K)
inr : ∀ (r : k), Eq (α := k) ((RingEquiv.symm (frobeniusEquiv k p) : (a : k) → k) r : k) (0 : k) → r = 0
inr₁ : ∀ (m : K), Eq (α := K) (((RingHom.toAddMonoidHom (frobenius K p) : K →+ K) : (a : K) → K) m : K) (0 : K) → m = 0
⊢ LinearIndepOn k (M := K) (fun (x : K) ↦ x ^ p) (↑s : Set K)
have inr₂ : ∀ (r : k) (m : K),
  ((RingHom.toAddMonoidHom (frobenius K p) : K →+ K) : (a : K) → K)
      (HSMul.hSMul (α := k) ((RingEquiv.symm (frobeniusEquiv k p) : (a : k) → k) r : k) m) =
    HSMul.hSMul (β := K) r (((RingHom.toAddMonoidHom (frobenius K p) : K →+ K) : (a : K) → K) m : K)
Tactic: apply hs.map_of_injective_injective (frobeniusEquiv k p).symm (frobenius K p).toAddMonoidHom
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (goal)
Goal:
K : Type v
inst : Field K
f : K[X]
⊢ Irreducible.{v} (M := K[X])
    (if H : ∃ (g : K[X]), Irreducible g ∧ g ∣ f then Classical.choose (p := fun (x : K[X]) ↦ Irreducible x ∧ x ∣ f) H
    else X)
have pos : ∀ (H : ∃ (g : K[X]), Irreducible g ∧ g ∣ f),
  Irreducible (Classical.choose (p := fun (x : K[X]) ↦ Irreducible x ∧ x ∣ f) H)
Tactic: split_ifs with H
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (goal)
Goal:
K : Type v
inst : Field K
f : K[X]
pos :
  ∀ (H : ∃ (g : K[X]), Irreducible g ∧ g ∣ f),
    Irreducible (Classical.choose (p := fun (x : K[X]) ↦ Irreducible x ∧ x ∣ f) H)
⊢ Irreducible.{v} (M := K[X])
    (if H : ∃ (g : K[X]), Irreducible g ∧ g ∣ f then Classical.choose (p := fun (x : K[X]) ↦ Irreducible x ∧ x ∣ f) H
    else X)
have neg : ∀ (H : ¬∃ (g : K[X]), Irreducible g ∧ g ∣ f), Irreducible.{v} (M := K[X]) X
Tactic: split_ifs with H
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (goal)
Goal:
K : Type v
inst : Field K
f : K[X]
hf1 : ¬IsUnit f
⊢ f.factor ∣ f
have pos : ∀ (hf2 : f = 0), f.factor ∣ f
Tactic: by_cases hf2 : f = 0
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (goal)
Goal:
K : Type v
inst : Field K
f : K[X]
hf1 : ¬IsUnit f
pos : ∀ (hf2 : f = 0), f.factor ∣ f
⊢ f.factor ∣ f
have neg : ∀ (hf2 : ¬f = 0), f.factor ∣ f
Tactic: by_cases hf2 : f = 0
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (goal)
Goal:
K : Type v
inst : Field K
f : K[X]
hf1 : ¬IsUnit f
hf2 : f = 0
⊢ f.factor ∣ f
have pos : Dvd.dvd.{v} (α := K[X]) (factor 0) 0
Tactic: rw [hf2]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (goal)
Goal:
K : Type v
inst : Field K
f : K[X]
hf1 : ¬IsUnit f
hf2 : ¬f = 0
⊢ f.factor ∣ f
have neg : Classical.choose (p := fun (x : K[X]) ↦ Irreducible x ∧ x ∣ f) sorry ∣ f
Tactic: rw [factor, dif_pos (WfDvdMonoid.exists_irreducible_factor hf1 hf2)]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (goal)
Goal:
K : Type v
inst : Field K
f g : K[X]
⊢ IsCoprime f g ↔
    ∀ {A : Type v} [inst_1 : CommRing A] [IsDomain A] [inst_3 : Algebra K A] (a : A),
      Ne (α := A) ((aeval a : (a : K[X]) → A) f : A) (0 : A) ∨ Ne (α := A) ((aeval a : (a : K[X]) → A) g : A) (0 : A)
have refine_1 : ∀
  (h :
    ∀ {A : Type v} [inst_1 : CommRing A] [IsDomain A] [inst_3 : Algebra K A] (a : A),
      Ne (α := A) ((aeval a : (a : K[X]) → A) f : A) (0 : A) ∨ Ne (α := A) ((aeval a : (a : K[X]) → A) g : A) (0 : A)),
  ¬(f = 0 ∧ g = 0)
Tactic: refine ⟨fun h => aeval_ne_zero_of_isCoprime h, fun h => isCoprime_of_dvd _ _ ?_ fun x hx _ => ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (goal)
Goal:
K : Type v
inst : Field K
f g : K[X]
refine_1 :
  ∀
    (h :
      ∀ {A : Type v} [inst_1 : CommRing A] [IsDomain A] [inst_3 : Algebra K A] (a : A),
        Ne (α := A) ((aeval a : (a : K[X]) → A) f : A) (0 : A) ∨
          Ne (α := A) ((aeval a : (a : K[X]) → A) g : A) (0 : A)),
    ¬(f = 0 ∧ g = 0)
⊢ IsCoprime f g ↔
    ∀ {A : Type v} [inst_1 : CommRing A] [IsDomain A] [inst_3 : Algebra K A] (a : A),
      Ne (α := A) ((aeval a : (a : K[X]) → A) f : A) (0 : A) ∨ Ne (α := A) ((aeval a : (a : K[X]) → A) g : A) (0 : A)
have refine_2 : ∀
  (h :
    ∀ {A : Type v} [inst_1 : CommRing A] [IsDomain A] [inst_3 : Algebra K A] (a : A),
      Ne (α := A) ((aeval a : (a : K[X]) → A) f : A) (0 : A) ∨ Ne (α := A) ((aeval a : (a : K[X]) → A) g : A) (0 : A))
  (x : K[X]) (hx : Membership.mem (γ := Set K[X]) (nonunits K[X]) x), x ≠ 0 → x ∣ f → ¬x ∣ g
Tactic: refine ⟨fun h => aeval_ne_zero_of_isCoprime h, fun h => isCoprime_of_dvd _ _ ?_ fun x hx _ => ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (hypothesis)
Goal:
K : Type v
inst : Field K
f g : K[X]
h :
  ∀ {A : Type v} [inst_1 : CommRing A] [IsDomain A] [inst_3 : Algebra K A] (a : A),
    Ne (α := A) ((aeval a : (a : K[X]) → A) f : A) (0 : A) ∨ Ne (α := A) ((aeval a : (a : K[X]) → A) g : A) (0 : A)
⊢ ¬(f = 0 ∧ g = 0)
have h₁ : Ne (α := K) ((aeval 0 : (a : K[X]) → K) f : K) (0 : K) ∨ Ne (α := K) ((aeval 0 : (a : K[X]) → K) g : K) (0 : K)
Tactic: replace h := @h K _ _ _ 0
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (goal)
Goal:
K : Type v
inst : Field K
f g : K[X]
h : Ne (α := K) ((aeval 0 : (a : K[X]) → K) f : K) (0 : K) ∨ Ne (α := K) ((aeval 0 : (a : K[X]) → K) g : K) (0 : K)
⊢ ¬(f = 0 ∧ g = 0)
have refine_1 : ∀ (h : f = 0 ∧ g = 0),
  Eq (α := K) ((aeval 0 : (a : K[X]) → K) f : K) (0 : K) ∧ Eq (α := K) ((aeval 0 : (a : K[X]) → K) g : K) (0 : K)
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (goal)
Goal:
K : Type v
inst : Field K
f g : K[X]
h : f = 0 ∧ g = 0
⊢ Eq (α := K) ((aeval 0 : (a : K[X]) → K) f : K) (0 : K) ∧ Eq (α := K) ((aeval 0 : (a : K[X]) → K) g : K) (0 : K)
have refine_1 : Eq.{v + 1} (α := K) ((aeval 0 : (a : K[X]) → K) 0 : K) (0 : K) ∧ Eq (α := K) ((aeval 0 : (a : K[X]) → K) g : K) (0 : K)
Tactic: rw [h.left, h.right, map_zero, and_self]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (goal)
Goal:
K : Type v
inst : Field K
f g : K[X]
h : f = 0 ∧ g = 0
refine_1 :
  Eq.{v + 1} (α := K) ((aeval 0 : (a : K[X]) → K) 0 : K) (0 : K) ∧
    Eq (α := K) ((aeval 0 : (a : K[X]) → K) g : K) (0 : K)
⊢ Eq (α := K) ((aeval 0 : (a : K[X]) → K) f : K) (0 : K) ∧ Eq (α := K) ((aeval 0 : (a : K[X]) → K) g : K) (0 : K)
have refine_1₁ : Eq.{v + 1} (α := K) ((aeval 0 : (a : K[X]) → K) 0 : K) (0 : K) ∧
  Eq.{v + 1} (α := K) ((aeval 0 : (a : K[X]) → K) 0 : K) (0 : K)
Tactic: rw [h.left, h.right, map_zero, and_self]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (goal)
Goal:
K : Type v
inst : Field K
f g : K[X]
h : f = 0 ∧ g = 0
refine_1 :
  Eq.{v + 1} (α := K) ((aeval 0 : (a : K[X]) → K) 0 : K) (0 : K) ∧
    Eq (α := K) ((aeval 0 : (a : K[X]) → K) g : K) (0 : K)
refine_1₁ :
  Eq.{v + 1} (α := K) ((aeval 0 : (a : K[X]) → K) 0 : K) (0 : K) ∧
    Eq.{v + 1} (α := K) ((aeval 0 : (a : K[X]) → K) 0 : K) (0 : K)
⊢ Eq (α := K) ((aeval 0 : (a : K[X]) → K) f : K) (0 : K) ∧ Eq (α := K) ((aeval 0 : (a : K[X]) → K) g : K) (0 : K)
have refine_1₂ : Eq.{v + 1} (α := K) 0 0 ∧ Eq.{v + 1} (α := K) 0 0
Tactic: rw [h.left, h.right, map_zero, and_self]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (goal)
Goal:
K : Type v
inst : Field K
f g : K[X]
h : f = 0 ∧ g = 0
refine_1 :
  Eq.{v + 1} (α := K) ((aeval 0 : (a : K[X]) → K) 0 : K) (0 : K) ∧
    Eq (α := K) ((aeval 0 : (a : K[X]) → K) g : K) (0 : K)
refine_1₁ :
  Eq.{v + 1} (α := K) ((aeval 0 : (a : K[X]) → K) 0 : K) (0 : K) ∧
    Eq.{v + 1} (α := K) ((aeval 0 : (a : K[X]) → K) 0 : K) (0 : K)
refine_1₂ : Eq.{v + 1} (α := K) 0 0 ∧ Eq.{v + 1} (α := K) 0 0
⊢ Eq (α := K) ((aeval 0 : (a : K[X]) → K) f : K) (0 : K) ∧ Eq (α := K) ((aeval 0 : (a : K[X]) → K) g : K) (0 : K)
have refine_1₃ : Eq.{v + 1} (α := K) 0 0
Tactic: rw [h.left, h.right, map_zero, and_self]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (hypothesis)
Goal:
K : Type v
inst : Field K
x : K[X]
hx : Membership.mem (γ := Set K[X]) (nonunits K[X]) x
h_1 : x ≠ 0
w w_1 : K[X]
h :
  ∀ {A : Type v} [inst_1 : CommRing A] [IsDomain A] [inst_3 : Algebra K A] (a : A),
    Ne (α := A) ((aeval a : (a : K[X]) → A) (x * w) : A) (0 : A) ∨
      Ne (α := A) ((aeval a : (a : K[X]) → A) (x * w_1) : A) (0 : A)
⊢ False
have h₁ : ¬(Eq (α := AdjoinRoot x.factor)
      ((aeval (AdjoinRoot.root x.factor) : (a : K[X]) → AdjoinRoot x.factor) (x * w) : AdjoinRoot x.factor)
      (0 : AdjoinRoot x.factor) ∧
    Eq (α := AdjoinRoot x.factor)
      ((aeval (AdjoinRoot.root x.factor) : (a : K[X]) → AdjoinRoot x.factor) (x * w_1) : AdjoinRoot x.factor)
      (0 : AdjoinRoot x.factor))
Tactic: replace h := not_and_or.mpr <| h <| AdjoinRoot.root x.factor
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (goal)
Goal:
K : Type v
inst : Field K
f : K[X]
hf : f.natDegree ≠ 0
⊢ HSub.hSub (α := (AdjoinRoot f.factor)[X]) (β := (AdjoinRoot f.factor)[X]) X
        ((C : (a : AdjoinRoot f.factor) → (AdjoinRoot f.factor)[X]) (AdjoinRoot.root f.factor) :
          (AdjoinRoot f.factor)[X]) *
      f.removeFactor =
    map (AdjoinRoot.of f.factor) f
have let : ∀ (g : K[X]) (hg : f = f.factor * g),
  HSub.hSub (α := (AdjoinRoot f.factor)[X]) (β := (AdjoinRoot f.factor)[X]) X
        ((C : (a : AdjoinRoot f.factor) → (AdjoinRoot f.factor)[X]) (AdjoinRoot.root f.factor) :
          (AdjoinRoot f.factor)[X]) *
      f.removeFactor =
    map (AdjoinRoot.of f.factor) f
Tactic: let ⟨g, hg⟩ := factor_dvd_of_natDegree_ne_zero hf
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (goal)
Goal:
K : Type v
inst : Field K
f : K[X]
hf : f.natDegree ≠ 0
g : K[X]
hg : f = f.factor * g
⊢ HSub.hSub (α := (AdjoinRoot f.factor)[X]) (β := (AdjoinRoot f.factor)[X]) X
        ((C : (a : AdjoinRoot f.factor) → (AdjoinRoot f.factor)[X]) (AdjoinRoot.root f.factor) :
          (AdjoinRoot f.factor)[X]) *
      f.removeFactor =
    map (AdjoinRoot.of f.factor) f
have apply : (map (AdjoinRoot.of f.factor) f).IsRoot (AdjoinRoot.root f.factor)
Tactic: apply (mul_divByMonic_eq_iff_isRoot
    (R := AdjoinRoot f.factor) (a := AdjoinRoot.root f.factor)).mpr
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (goal)
Goal:
K : Type v
inst : Field K
f : K[X]
hf : f.natDegree ≠ 0
g : K[X]
hg : f = f.factor * g
⊢ (map (AdjoinRoot.of f.factor) f).IsRoot (AdjoinRoot.root f.factor)
have rw : eval (AdjoinRoot.root f.factor) (map (AdjoinRoot.of f.factor) f) = 0
Tactic: rw [IsRoot.def, eval_map, hg, eval₂_mul, ← hg, AdjoinRoot.eval₂_root, zero_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (goal)
Goal:
K : Type v
inst : Field K
f : K[X]
hf : f.natDegree ≠ 0
g : K[X]
hg : f = f.factor * g
rw : eval (AdjoinRoot.root f.factor) (map (AdjoinRoot.of f.factor) f) = 0
⊢ (map (AdjoinRoot.of f.factor) f).IsRoot (AdjoinRoot.root f.factor)
have rw₁ : eval₂ (AdjoinRoot.of f.factor) (AdjoinRoot.root f.factor) f = 0
Tactic: rw [IsRoot.def, eval_map, hg, eval₂_mul, ← hg, AdjoinRoot.eval₂_root, zero_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (goal)
Goal:
K : Type v
inst : Field K
f : K[X]
hf : f.natDegree ≠ 0
g : K[X]
hg : f = f.factor * g
rw : eval (AdjoinRoot.root f.factor) (map (AdjoinRoot.of f.factor) f) = 0
rw₁ : eval₂ (AdjoinRoot.of f.factor) (AdjoinRoot.root f.factor) f = 0
⊢ (map (AdjoinRoot.of f.factor) f).IsRoot (AdjoinRoot.root f.factor)
have rw₂ : eval₂ (AdjoinRoot.of (f.factor * g).factor) (AdjoinRoot.root (f.factor * g).factor) (f.factor * g) = 0
Tactic: rw [IsRoot.def, eval_map, hg, eval₂_mul, ← hg, AdjoinRoot.eval₂_root, zero_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (goal)
Goal:
K : Type v
inst : Field K
f : K[X]
hf : f.natDegree ≠ 0
g : K[X]
hg : f = f.factor * g
rw : eval (AdjoinRoot.root f.factor) (map (AdjoinRoot.of f.factor) f) = 0
rw₁ : eval₂ (AdjoinRoot.of f.factor) (AdjoinRoot.root f.factor) f = 0
rw₂ : eval₂ (AdjoinRoot.of (f.factor * g).factor) (AdjoinRoot.root (f.factor * g).factor) (f.factor * g) = 0
⊢ (map (AdjoinRoot.of f.factor) f).IsRoot (AdjoinRoot.root f.factor)
have rw₃ : eval₂ (AdjoinRoot.of (f.factor * g).factor) (AdjoinRoot.root (f.factor * g).factor) f.factor *
    eval₂ (AdjoinRoot.of (f.factor * g).factor) (AdjoinRoot.root (f.factor * g).factor) g =
  0
Tactic: rw [IsRoot.def, eval_map, hg, eval₂_mul, ← hg, AdjoinRoot.eval₂_root, zero_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (goal)
Goal:
K : Type v
inst : Field K
f : K[X]
hf : f.natDegree ≠ 0
g : K[X]
hg : f = f.factor * g
rw : eval (AdjoinRoot.root f.factor) (map (AdjoinRoot.of f.factor) f) = 0
rw₁ : eval₂ (AdjoinRoot.of f.factor) (AdjoinRoot.root f.factor) f = 0
rw₂ : eval₂ (AdjoinRoot.of (f.factor * g).factor) (AdjoinRoot.root (f.factor * g).factor) (f.factor * g) = 0
rw₃ :
  eval₂ (AdjoinRoot.of (f.factor * g).factor) (AdjoinRoot.root (f.factor * g).factor) f.factor *
      eval₂ (AdjoinRoot.of (f.factor * g).factor) (AdjoinRoot.root (f.factor * g).factor) g =
    0
⊢ (map (AdjoinRoot.of f.factor) f).IsRoot (AdjoinRoot.root f.factor)
have rw₄ : eval₂ (AdjoinRoot.of f.factor) (AdjoinRoot.root f.factor) f.factor *
    eval₂ (AdjoinRoot.of f.factor) (AdjoinRoot.root f.factor) g =
  0
Tactic: rw [IsRoot.def, eval_map, hg, eval₂_mul, ← hg, AdjoinRoot.eval₂_root, zero_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (goal)
Goal:
K : Type v
inst : Field K
f : K[X]
hf : f.natDegree ≠ 0
g : K[X]
hg : f = f.factor * g
rw : eval (AdjoinRoot.root f.factor) (map (AdjoinRoot.of f.factor) f) = 0
rw₁ : eval₂ (AdjoinRoot.of f.factor) (AdjoinRoot.root f.factor) f = 0
rw₂ : eval₂ (AdjoinRoot.of (f.factor * g).factor) (AdjoinRoot.root (f.factor * g).factor) (f.factor * g) = 0
rw₃ :
  eval₂ (AdjoinRoot.of (f.factor * g).factor) (AdjoinRoot.root (f.factor * g).factor) f.factor *
      eval₂ (AdjoinRoot.of (f.factor * g).factor) (AdjoinRoot.root (f.factor * g).factor) g =
    0
rw₄ :
  eval₂ (AdjoinRoot.of f.factor) (AdjoinRoot.root f.factor) f.factor *
      eval₂ (AdjoinRoot.of f.factor) (AdjoinRoot.root f.factor) g =
    0
⊢ (map (AdjoinRoot.of f.factor) f).IsRoot (AdjoinRoot.root f.factor)
have rw₅ : 0 * eval₂ (AdjoinRoot.of f.factor) (AdjoinRoot.root f.factor) g = 0
Tactic: rw [IsRoot.def, eval_map, hg, eval₂_mul, ← hg, AdjoinRoot.eval₂_root, zero_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (goal)
Goal:
K : Type v
inst : Field K
f : K[X]
hf : f.natDegree ≠ 0
g : K[X]
hg : f = f.factor * g
rw : eval (AdjoinRoot.root f.factor) (map (AdjoinRoot.of f.factor) f) = 0
rw₁ : eval₂ (AdjoinRoot.of f.factor) (AdjoinRoot.root f.factor) f = 0
rw₂ : eval₂ (AdjoinRoot.of (f.factor * g).factor) (AdjoinRoot.root (f.factor * g).factor) (f.factor * g) = 0
rw₃ :
  eval₂ (AdjoinRoot.of (f.factor * g).factor) (AdjoinRoot.root (f.factor * g).factor) f.factor *
      eval₂ (AdjoinRoot.of (f.factor * g).factor) (AdjoinRoot.root (f.factor * g).factor) g =
    0
rw₄ :
  eval₂ (AdjoinRoot.of f.factor) (AdjoinRoot.root f.factor) f.factor *
      eval₂ (AdjoinRoot.of f.factor) (AdjoinRoot.root f.factor) g =
    0
rw₅ : 0 * eval₂ (AdjoinRoot.of f.factor) (AdjoinRoot.root f.factor) g = 0
⊢ (map (AdjoinRoot.of f.factor) f).IsRoot (AdjoinRoot.root f.factor)
have rw₆ : Eq.{v + 1} (α := AdjoinRoot f.factor) 0 0
Tactic: rw [IsRoot.def, eval_map, hg, eval₂_mul, ← hg, AdjoinRoot.eval₂_root, zero_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (goal)
Goal:
K : Type v
inst : Field K
f : K[X]
⊢ f.removeFactor.natDegree = f.natDegree - 1
have rw : (map (AdjoinRoot.of f.factor) f /ₘ
      HSub.hSub (α := (AdjoinRoot f.factor)[X]) (β := (AdjoinRoot f.factor)[X]) X
        ((C : (a : AdjoinRoot f.factor) → (AdjoinRoot f.factor)[X]) (AdjoinRoot.root f.factor) :
          (AdjoinRoot f.factor)[X])).natDegree =
  f.natDegree - 1
Tactic: rw [removeFactor, natDegree_divByMonic _ (monic_X_sub_C _), natDegree_map, natDegree_X_sub_C]