awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
inst : Field F
n : ℕ
x : F
hx : ¬x = 0
key :
  Splits (R := (HPow.hPow (α := F[X]) X n - 1).SplittingField)
    (map (algebraMap F (HPow.hPow (α := F[X]) X n - 1).SplittingField) (HPow.hPow (α := F[X]) X n - 1))
neg :
  ∀
    (key :
      (HSub.hSub (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField[X])
          (map (algebraMap F (HPow.hPow (α := F[X]) X n - 1).SplittingField) (HPow.hPow (α := F[X]) X n))
          (map
            (algebraMap F (HPow.hPow (α := F[X]) X n - 1).SplittingField :
              F →+* (HPow.hPow (α := F[X]) X n - 1).SplittingField)
            1)).Splits),
    (HPow.hPow (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField[X]) X n - 1).Splits
neg₁ :
  ∀
    (key :
      (HPow.hPow (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField[X])
            (map
              (algebraMap F (HPow.hPow (α := F[X]) X n - 1).SplittingField :
                F →+* (HPow.hPow (α := F[X]) X n - 1).SplittingField)
              X)
            n -
          map
            (algebraMap F (HPow.hPow (α := F[X]) X n - 1).SplittingField :
              F →+* (HPow.hPow (α := F[X]) X n - 1).SplittingField)
            1).Splits),
    (HPow.hPow (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField[X]) X n - 1).Splits
neg₂ :
  ∀
    (key :
      (HPow.hPow (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField[X]) X n -
          map
            (algebraMap F (HPow.hPow (α := F[X]) X n - 1).SplittingField :
              F →+* (HPow.hPow (α := F[X]) X n - 1).SplittingField)
            1).Splits),
    (HPow.hPow (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField[X]) X n - 1).Splits
⊢ (HPow.hPow (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField[X]) X n - 1).Splits
have neg₃ : ∀ (key : (HPow.hPow (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField[X]) X n - 1).Splits),
  (HPow.hPow (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField[X]) X n - 1).Splits
Tactic: rwa [Polynomial.map_sub, Polynomial.map_pow, map_X,
      Polynomial.map_one] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
⊢ LE.le (α := IntermediateField F E) (solvableByRad F E) (algebraicClosure F E)
have refine : ∀ (x : E) (n : ℕ) (hn : n ≠ 0) (hx : Membership.mem (γ := IntermediateField F E) (algebraicClosure F E) (x ^ n)),
  Membership.mem (γ := IntermediateField F E) (algebraicClosure F E) x
Tactic: refine solvableByRad_le fun x n hn hx ↦ ?_
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
n : ℕ
hn : n ≠ 0
hx : Membership.mem (γ := IntermediateField F E) (algebraicClosure F E) (x ^ n)
⊢ Membership.mem (γ := IntermediateField F E) (algebraicClosure F E) x
have rw : ∀ (hx : IsAlgebraic F (x ^ n)), IsAlgebraic F x
Tactic: rw [mem_algebraicClosure_iff] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
n : ℕ
hn : n ≠ 0
hx : IsAlgebraic F (x ^ n)
⊢ IsAlgebraic F x
have obtain : ∀ (p : F[X]) (h1 : p ≠ 0) (h2 : Eq.{u_2 + 1} (α := E) ((aeval (x ^ n) : (a : F[X]) → E) p : E) (0 : E)), IsAlgebraic F x
Tactic: obtain ⟨p, h1, h2⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
n : ℕ
hn : n ≠ 0
p : F[X]
h1 : p ≠ 0
h2 : Eq.{u_2 + 1} (α := E) ((aeval (x ^ n) : (a : F[X]) → E) p : E) (0 : E)
⊢ IsAlgebraic F x
have refine_1 : ∀ (h : p.comp (HPow.hPow (α := F[X]) X n) = 0), p.leadingCoeff = 0
Tactic: refine ⟨p.comp (X ^ n), ⟨fun h ↦ h1 (leadingCoeff_eq_zero.mp ?_), ?_⟩⟩
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
n : ℕ
hn : n ≠ 0
p : F[X]
h1 : p ≠ 0
h2 : Eq.{u_2 + 1} (α := E) ((aeval (x ^ n) : (a : F[X]) → E) p : E) (0 : E)
refine_1 : ∀ (h : p.comp (HPow.hPow (α := F[X]) X n) = 0), p.leadingCoeff = 0
⊢ IsAlgebraic F x
have refine_2 : Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) (p.comp (HPow.hPow (α := F[X]) X n)) : E) (0 : E)
Tactic: refine ⟨p.comp (X ^ n), ⟨fun h ↦ h1 (leadingCoeff_eq_zero.mp ?_), ?_⟩⟩
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
n : ℕ
hn : n ≠ 0
p : F[X]
h1 : p ≠ 0
h2 : Eq.{u_2 + 1} (α := E) ((aeval (x ^ n) : (a : F[X]) → E) p : E) (0 : E)
h : p.comp (HPow.hPow (α := F[X]) X n) = 0
⊢ p.leadingCoeff = 0
have refine_1 : ∀ (h : (p.comp (HPow.hPow (α := F[X]) X n)).leadingCoeff = 0), (HPow.hPow (α := F[X]) X n).natDegree ≠ 0
Tactic: rwa [← leadingCoeff_eq_zero, leadingCoeff_comp, leadingCoeff_X_pow, one_pow, mul_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
motive : (x : E) → Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x → Prop
mem : ∀ (x : F), motive ((algebraMap F E : (a : F) → E) x) ⋯
add :
  ∀ (x y : E) (hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x)
    (hy : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) y),
    motive x hx → motive y hy → motive (x + y) ⋯
mul :
  ∀ (x y : E) (hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x)
    (hy : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) y),
    motive x hx → motive y hy → motive (x * y) ⋯
rad :
  ∀ (n : ℕ) (x : E) (hn : n ≠ 0) (hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) (x ^ n)),
    motive (x ^ n) hx → motive x ⋯
x_1 : E
hx_1 : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x_1
s : Subalgebra F E :=
  { carrier := {x : E | ∃ (hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x), motive x hx},
    mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }
x : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
hx' : motive x hx
⊢ IsAlgebraic F x
have a : Membership.mem (γ := Subalgebra F E) (IntermediateField.toSubalgebra (solvableByRad F E)) x
Tactic: apply isAlgebraic_solvableByRad
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (hypothesis)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
motive : (x : E) → Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x → Prop
mem : ∀ (x : F), motive ((algebraMap F E : (a : F) → E) x) ⋯
add :
  ∀ (x y : E) (hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x)
    (hy : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) y),
    motive x hx → motive y hy → motive (x + y) ⋯
mul :
  ∀ (x y : E) (hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x)
    (hy : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) y),
    motive x hx → motive y hy → motive (x * y) ⋯
rad :
  ∀ (n : ℕ) (x : E) (hn : n ≠ 0) (hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) (x ^ n)),
    motive (x ^ n) hx → motive x ⋯
x : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
s : Subalgebra F E :=
  { carrier := {x : E | ∃ (hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x), motive x hx},
    mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }
t : IntermediateField F E := Subalgebra.IsAlgebraic.toIntermediateField (S := s) ⋯
⊢ motive x hx
have ht : ∀ (x : E) (n : ℕ) (hn : n ≠ 0), x ^ n ∈ t → x ∈ t
Tactic: have ht (x n) (hn : n ≠ 0) : x ^ n ∈ t → x ∈ t := by
    rintro ⟨hx, hx'⟩
    exact ⟨rad_mem hn hx, rad _ _ hn hx hx'⟩
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
n : ℕ
hn : n ≠ 0
hα : IsSolvable.{u_1} (Gal (minpoly F (x ^ n)))
p : F[X] := minpoly F (x ^ n)
h : p.comp (HPow.hPow (α := F[X]) X n) = 0
⊢ False
have inl : ∀ (h' : p = 0), False
Tactic: rcases comp_eq_zero_iff.mp h with h' | h'
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
n : ℕ
hn : n ≠ 0
hα : IsSolvable.{u_1} (Gal (minpoly F (x ^ n)))
p : F[X] := minpoly F (x ^ n)
h : p.comp (HPow.hPow (α := F[X]) X n) = 0
inl : ∀ (h' : p = 0), False
⊢ False
have inr : ∀
  (h' :
    eval ((HPow.hPow (α := F[X]) X n).coeff 0) p = 0 ∧
      HPow.hPow (α := F[X]) X n = (C : (a : F) → F[X]) ((HPow.hPow (α := F[X]) X n).coeff 0)),
  False
Tactic: rcases comp_eq_zero_iff.mp h with h' | h'
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
n : ℕ
hn : n ≠ 0
hα : IsSolvable.{u_1} (Gal (minpoly F (x ^ n)))
p : F[X] := minpoly F (x ^ n)
h : p.comp (HPow.hPow (α := F[X]) X n) = 0
h' :
  eval ((HPow.hPow (α := F[X]) X n).coeff 0) p = 0 ∧
    HPow.hPow (α := F[X]) X n = (C : (a : F) → F[X]) ((HPow.hPow (α := F[X]) X n).coeff 0)
⊢ n = 0
have rw : n = natDegree.{u_1} (R := F) ((C : (a : F) → F[X]) ((HPow.hPow (α := F[X]) X n).coeff 0))
Tactic: rw [← @natDegree_C F, ← h'.2, natDegree_X_pow]
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
n : ℕ
hn : n ≠ 0
hα : IsSolvable.{u_1} (Gal (minpoly F (x ^ n)))
p : F[X] := minpoly F (x ^ n)
h : p.comp (HPow.hPow (α := F[X]) X n) = 0
h' :
  eval ((HPow.hPow (α := F[X]) X n).coeff 0) p = 0 ∧
    HPow.hPow (α := F[X]) X n = (C : (a : F) → F[X]) ((HPow.hPow (α := F[X]) X n).coeff 0)
rw : n = natDegree.{u_1} (R := F) ((C : (a : F) → F[X]) ((HPow.hPow (α := F[X]) X n).coeff 0))
⊢ n = 0
have a : F
Tactic: rw [← @natDegree_C F, ← h'.2, natDegree_X_pow]
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
n : ℕ
hn : n ≠ 0
hα : IsSolvable.{u_1} (Gal (minpoly F (x ^ n)))
p : F[X] := minpoly F (x ^ n)
h : p.comp (HPow.hPow (α := F[X]) X n) = 0
h' :
  eval ((HPow.hPow (α := F[X]) X n).coeff 0) p = 0 ∧
    HPow.hPow (α := F[X]) X n = (C : (a : F) → F[X]) ((HPow.hPow (α := F[X]) X n).coeff 0)
rw : n = natDegree.{u_1} (R := F) ((C : (a : F) → F[X]) ((HPow.hPow (α := F[X]) X n).coeff 0))
a : F
⊢ n = 0
have rw₁ : n = (HPow.hPow (α := F[X]) X n).natDegree
Tactic: rw [← @natDegree_C F, ← h'.2, natDegree_X_pow]
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
n : ℕ
hn : n ≠ 0
hα : IsSolvable.{u_1} (Gal (minpoly F (x ^ n)))
p : F[X] := minpoly F (x ^ n)
h : p.comp (HPow.hPow (α := F[X]) X n) = 0
h' :
  eval ((HPow.hPow (α := F[X]) X n).coeff 0) p = 0 ∧
    HPow.hPow (α := F[X]) X n = (C : (a : F) → F[X]) ((HPow.hPow (α := F[X]) X n).coeff 0)
rw : n = natDegree.{u_1} (R := F) ((C : (a : F) → F[X]) ((HPow.hPow (α := F[X]) X n).coeff 0))
a : F
rw₁ : n = (HPow.hPow (α := F[X]) X n).natDegree
⊢ n = 0
have rw₂ : n = n
Tactic: rw [← @natDegree_C F, ← h'.2, natDegree_X_pow]
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (hypothesis)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
n : ℕ
hn : n ≠ 0
hα : IsSolvable.{u_1} (Gal (minpoly F (x ^ n)))
p : F[X] := minpoly F (x ^ n)
⊢ IsSolvable.{u_1} (Gal (minpoly F x))
have hp : p.comp (HPow.hPow (α := F[X]) X n) ≠ 0
Tactic: have hp : p.comp (X ^ n) ≠ 0 := by
    intro h
    rcases comp_eq_zero_iff.mp h with h' | h'
    · exact minpoly.ne_zero (isIntegral_of_mem_solvableByRad (pow_mem hx n)) h'
    · exact hn (by rw [← @natDegree_C F, ← h'.2, natDegree_X_pow])
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
n : ℕ
hn : n ≠ 0
hα : IsSolvable.{u_1} (Gal (minpoly F (x ^ n)))
p : F[X] := minpoly F (x ^ n)
hp : p.comp (HPow.hPow (α := F[X]) X n) ≠ 0
⊢ IsSolvable.{u_1} (Gal (minpoly F x))
have x₁ : Fact
  (Splits (R := (p.comp (HPow.hPow (α := F[X]) X n)).SplittingField)
    (map (algebraMap F (p.comp (HPow.hPow (α := F[X]) X n)).SplittingField) (minpoly F x)))
Tactic: apply gal_isSolvable_of_splits
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
n : ℕ
hn : n ≠ 0
hα : IsSolvable.{u_1} (Gal (minpoly F (x ^ n)))
p : F[X] := minpoly F (x ^ n)
hp : p.comp (HPow.hPow (α := F[X]) X n) ≠ 0
x₁ :
  Fact
    (Splits (R := (p.comp (HPow.hPow (α := F[X]) X n)).SplittingField)
      (map (algebraMap F (p.comp (HPow.hPow (α := F[X]) X n)).SplittingField) (minpoly F x)))
⊢ IsSolvable.{u_1} (Gal (minpoly F x))
have hq : IsSolvable.{u_1} (p.comp (HPow.hPow (α := F[X]) X n)).Gal
Tactic: apply gal_isSolvable_of_splits
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
n : ℕ
hn : n ≠ 0
hα : IsSolvable.{u_1} (Gal (minpoly F (x ^ n)))
p : F[X] := minpoly F (x ^ n)
hp : p.comp (HPow.hPow (α := F[X]) X n) ≠ 0
⊢ Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) (p.comp (HPow.hPow (α := F[X]) X n)) : E) (0 : E)
have rw : Eq.{u_2 + 1} (α := E)
  (((aeval ((aeval x : (a : F[X]) → E) (HPow.hPow (α := F[X]) X n)) : F[X] →ₐ[F] E) : (a : F[X]) → E) p : E) (0 : E)
Tactic: rw [aeval_comp, aeval_X_pow, minpoly.aeval]
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
n : ℕ
hn : n ≠ 0
hα : IsSolvable.{u_1} (Gal (minpoly F (x ^ n)))
p : F[X] := minpoly F (x ^ n)
hp : p.comp (HPow.hPow (α := F[X]) X n) ≠ 0
rw :
  Eq.{u_2 + 1} (α := E)
    (((aeval ((aeval x : (a : F[X]) → E) (HPow.hPow (α := F[X]) X n)) : F[X] →ₐ[F] E) : (a : F[X]) → E) p : E) (0 : E)
⊢ Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) (p.comp (HPow.hPow (α := F[X]) X n)) : E) (0 : E)
have rw₁ : Eq.{u_2 + 1} (α := E) ((aeval (x ^ n) : (a : F[X]) → E) p : E) (0 : E)
Tactic: rw [aeval_comp, aeval_X_pow, minpoly.aeval]
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
n : ℕ
hn : n ≠ 0
hα : IsSolvable.{u_1} (Gal (minpoly F (x ^ n)))
p : F[X] := minpoly F (x ^ n)
hp : p.comp (HPow.hPow (α := F[X]) X n) ≠ 0
rw :
  Eq.{u_2 + 1} (α := E)
    (((aeval ((aeval x : (a : F[X]) → E) (HPow.hPow (α := F[X]) X n)) : F[X] →ₐ[F] E) : (a : F[X]) → E) p : E) (0 : E)
rw₁ : Eq.{u_2 + 1} (α := E) ((aeval (x ^ n) : (a : F[X]) → E) p : E) (0 : E)
⊢ Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) (p.comp (HPow.hPow (α := F[X]) X n)) : E) (0 : E)
have rw₂ : Eq.{u_2 + 1} (α := E) 0 0
Tactic: rw [aeval_comp, aeval_X_pow, minpoly.aeval]
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
n : ℕ
hn : n ≠ 0
hα : IsSolvable.{u_1} (Gal (minpoly F (x ^ n)))
p : F[X] := minpoly F (x ^ n)
hp : p.comp (HPow.hPow (α := F[X]) X n) ≠ 0
⊢ IsSolvable.{u_1} (p.comp (HPow.hPow (α := F[X]) X n)).Gal
have hq : Splits (R := (p.comp (HPow.hPow (α := F[X]) X n)).SplittingField)
  (map (algebraMap F (p.comp (HPow.hPow (α := F[X]) X n)).SplittingField) p)
Tactic: refine gal_isSolvable_tower p (p.comp (X ^ n)) ?_ hα ?_
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
n : ℕ
hn : n ≠ 0
hα : IsSolvable.{u_1} (Gal (minpoly F (x ^ n)))
p : F[X] := minpoly F (x ^ n)
hp : p.comp (HPow.hPow (α := F[X]) X n) ≠ 0
hq :
  Splits (R := (p.comp (HPow.hPow (α := F[X]) X n)).SplittingField)
    (map (algebraMap F (p.comp (HPow.hPow (α := F[X]) X n)).SplittingField) p)
⊢ IsSolvable.{u_1} (p.comp (HPow.hPow (α := F[X]) X n)).Gal
have hq₁ : IsSolvable.{u_1}
  (Gal (F := p.SplittingField) (map (algebraMap F p.SplittingField) (p.comp (HPow.hPow (α := F[X]) X n))))
Tactic: refine gal_isSolvable_tower p (p.comp (X ^ n)) ?_ hα ?_
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
n : ℕ
hn : n ≠ 0
hα : IsSolvable.{u_1} (Gal (minpoly F (x ^ n)))
p : F[X] := minpoly F (x ^ n)
hp : p.comp (HPow.hPow (α := F[X]) X n) ≠ 0
⊢ IsSolvable.{u_1}
    (Gal (F := p.SplittingField) (map (algebraMap F p.SplittingField) (p.comp (HPow.hPow (α := F[X]) X n))))
have hq : ∀ (s : Multiset p.SplittingField)
  (hs :
    map (algebraMap F p.SplittingField) p =
      HMul.hMul (α := p.SplittingField[X])
        ((C : (a : p.SplittingField) → p.SplittingField[X]) (leadingCoeff (map (algebraMap F p.SplittingField) p)))
        (Multiset.prod
          (Multiset.map
            (fun (x : p.SplittingField) ↦
              HSub.hSub (α := p.SplittingField[X]) (β := p.SplittingField[X]) X
                ((C : (a : p.SplittingField) → p.SplittingField[X]) x : p.SplittingField[X]))
            s))),
  IsSolvable.{u_1}
    (Gal (F := p.SplittingField) (map (algebraMap F p.SplittingField) (p.comp (HPow.hPow (α := F[X]) X n))))
Tactic: obtain ⟨s, hs⟩ := splits_iff_exists_multiset.1 (SplittingField.splits p)
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
n : ℕ
hn : n ≠ 0
hα : IsSolvable.{u_1} (Gal (minpoly F (x ^ n)))
p : F[X] := minpoly F (x ^ n)
hp : p.comp (HPow.hPow (α := F[X]) X n) ≠ 0
s : Multiset p.SplittingField
hs :
  map (algebraMap F p.SplittingField) p =
    HMul.hMul (α := p.SplittingField[X])
      ((C : (a : p.SplittingField) → p.SplittingField[X]) (leadingCoeff (map (algebraMap F p.SplittingField) p)))
      (Multiset.prod
        (Multiset.map
          (fun (x : p.SplittingField) ↦
            HSub.hSub (α := p.SplittingField[X]) (β := p.SplittingField[X]) X
              ((C : (a : p.SplittingField) → p.SplittingField[X]) x : p.SplittingField[X]))
          s))
⊢ IsSolvable.{u_1}
    (Gal (F := p.SplittingField) (map (algebraMap F p.SplittingField) (p.comp (HPow.hPow (α := F[X]) X n))))
have hq : IsSolvable.{u_1}
  ((C : (a : p.SplittingField) → p.SplittingField[X]) (leadingCoeff (map (algebraMap F p.SplittingField) p)) *
      comp
        (Multiset.prod
          (Multiset.map
            (fun (x : p.SplittingField) ↦
              HSub.hSub (α := p.SplittingField[X]) (β := p.SplittingField[X]) X
                ((C : (a : p.SplittingField) → p.SplittingField[X]) x : p.SplittingField[X]))
            s))
        (HPow.hPow (α := p.SplittingField[X]) X n)).Gal
Tactic: rw [map_comp, Polynomial.map_pow, map_X, hs, mul_comp, C_comp]
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
n : ℕ
hn : n ≠ 0
hα : IsSolvable.{u_1} (Gal (minpoly F (x ^ n)))
p : F[X] := minpoly F (x ^ n)
hp : p.comp (HPow.hPow (α := F[X]) X n) ≠ 0
s : Multiset p.SplittingField
hs :
  map (algebraMap F p.SplittingField) p =
    HMul.hMul (α := p.SplittingField[X])
      ((C : (a : p.SplittingField) → p.SplittingField[X]) (leadingCoeff (map (algebraMap F p.SplittingField) p)))
      (Multiset.prod
        (Multiset.map
          (fun (x : p.SplittingField) ↦
            HSub.hSub (α := p.SplittingField[X]) (β := p.SplittingField[X]) X
              ((C : (a : p.SplittingField) → p.SplittingField[X]) x : p.SplittingField[X]))
          s))
⊢ IsSolvable.{u_1}
    ((C : (a : p.SplittingField) → p.SplittingField[X]) (leadingCoeff (map (algebraMap F p.SplittingField) p)) *
        comp
          (Multiset.prod
            (Multiset.map
              (fun (x : p.SplittingField) ↦
                HSub.hSub (α := p.SplittingField[X]) (β := p.SplittingField[X]) X
                  ((C : (a : p.SplittingField) → p.SplittingField[X]) x : p.SplittingField[X]))
              s))
          (HPow.hPow (α := p.SplittingField[X]) X n)).Gal
have hq : IsSolvable.{u_1}
  (comp
      (Multiset.prod
        (Multiset.map
          (fun (x : p.SplittingField) ↦
            HSub.hSub (α := p.SplittingField[X]) (β := p.SplittingField[X]) X
              ((C : (a : p.SplittingField) → p.SplittingField[X]) x : p.SplittingField[X]))
          s))
      (HPow.hPow (α := p.SplittingField[X]) X n)).Gal
Tactic: apply gal_mul_isSolvable (gal_C_isSolvable _)
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
n : ℕ
hn : n ≠ 0
hα : IsSolvable.{u_1} (Gal (minpoly F (x ^ n)))
p : F[X] := minpoly F (x ^ n)
hp : p.comp (HPow.hPow (α := F[X]) X n) ≠ 0
s : Multiset p.SplittingField
hs :
  map (algebraMap F p.SplittingField) p =
    HMul.hMul (α := p.SplittingField[X])
      ((C : (a : p.SplittingField) → p.SplittingField[X]) (leadingCoeff (map (algebraMap F p.SplittingField) p)))
      (Multiset.prod
        (Multiset.map
          (fun (x : p.SplittingField) ↦
            HSub.hSub (α := p.SplittingField[X]) (β := p.SplittingField[X]) X
              ((C : (a : p.SplittingField) → p.SplittingField[X]) x : p.SplittingField[X]))
          s))
⊢ IsSolvable.{u_1}
    (comp
        (Multiset.prod
          (Multiset.map
            (fun (x : p.SplittingField) ↦
              HSub.hSub (α := p.SplittingField[X]) (β := p.SplittingField[X]) X
                ((C : (a : p.SplittingField) → p.SplittingField[X]) x : p.SplittingField[X]))
            s))
        (HPow.hPow (α := p.SplittingField[X]) X n)).Gal
have hq : IsSolvable.{u_1}
  (Gal (F := p.SplittingField)
    (Multiset.prod
      (Multiset.map (fun (p_1 : p.SplittingField[X]) ↦ p_1.comp (HPow.hPow (α := p.SplittingField[X]) X n))
        (Multiset.map
          (fun (x : p.SplittingField) ↦
            HSub.hSub (α := p.SplittingField[X]) (β := p.SplittingField[X]) X
              ((C : (a : p.SplittingField) → p.SplittingField[X]) x : p.SplittingField[X]))
          s))))
Tactic: rw [multiset_prod_comp]