awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.AbelRuffini
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
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
⊢ False

Tactic:
rcases comp_eq_zero_iff.mp h with h' | h'

Premises used: Polynomial.comp_eq_zero_iff, Iff.mp
-- Module: Mathlib.FieldTheory.AbelRuffini
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' : p = 0
⊢ False

Tactic:
minpoly.ne_zero (isIntegral_of_mem_solvableByRad (pow_mem hx n)) h'

Premises used: pow_mem, minpoly.ne_zero, isIntegral_of_mem_solvableByRad
-- Module: Mathlib.FieldTheory.AbelRuffini
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' : p = 0
⊢ False

Tactic:
exact minpoly.ne_zero (isIntegral_of_mem_solvableByRad (pow_mem hx n)) h'

Premises used: pow_mem, minpoly.ne_zero, isIntegral_of_mem_solvableByRad
-- Module: Mathlib.FieldTheory.AbelRuffini
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
rw₂ rw₃ : n = n
⊢ n = 0

Tactic:
rw [← @natDegree_C F, ← h'.2, natDegree_X_pow]

Premises used: Polynomial.natDegree_C, And.right, Polynomial.natDegree_X_pow
-- Module: Mathlib.FieldTheory.AbelRuffini
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)
⊢ False

Tactic:
exact hn (by rw [← @natDegree_C F, ← h'.2, natDegree_X_pow])
-- Module: Mathlib.FieldTheory.AbelRuffini
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)
⊢ 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])
-- Module: Mathlib.FieldTheory.AbelRuffini
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)))
hq : IsSolvable.{u_1} (p.comp (HPow.hPow (α := F[X]) X n)).Gal
q : F[X]
⊢ IsSolvable.{u_1} (Gal (minpoly F x))

Tactic:
apply gal_isSolvable_of_splits

Premises used: gal_isSolvable_of_splits
-- Module: Mathlib.FieldTheory.AbelRuffini
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)
rw₂ rw₃ : Eq.{u_2 + 1} (α := E) 0 0
⊢ Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) (p.comp (HPow.hPow (α := F[X]) X n)) : E) (0 : E)

Tactic:
rw [aeval_comp, aeval_X_pow, minpoly.aeval]

Premises used: Polynomial.aeval_X_pow, Polynomial.aeval_comp, minpoly.aeval
-- Module: Mathlib.FieldTheory.AbelRuffini
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
⊢ 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:
exact ⟨(SplittingField.splits (p.comp (X ^ n))).of_dvd (map_ne_zero hp)
      ((map_dvd_map' _).mpr (minpoly.dvd F x (by rw [aeval_comp, aeval_X_pow, minpoly.aeval])))⟩
-- Module: Mathlib.FieldTheory.AbelRuffini
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

Tactic:
gal_isSolvable_tower p (p.comp (X ^ n)) ?_ hα ?_

Premises used: HPow.hPow, Polynomial.X, Polynomial.comp, gal_isSolvable_tower
-- Module: Mathlib.FieldTheory.AbelRuffini
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)
hq₁ :
  IsSolvable.{u_1}
    (Gal (F := p.SplittingField) (map (algebraMap F p.SplittingField) (p.comp (HPow.hPow (α := F[X]) X n))))
⊢ IsSolvable.{u_1} (p.comp (HPow.hPow (α := F[X]) X n)).Gal

Tactic:
refine gal_isSolvable_tower p (p.comp (X ^ n)) ?_ hα ?_

Premises used: HPow.hPow, Polynomial.X, Polynomial.comp, gal_isSolvable_tower
-- Module: Mathlib.FieldTheory.AbelRuffini
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
rwa rwa₁ rwa₂ rwa₃ : n ≠ 0
⊢ (HPow.hPow (α := F[X]) X n).natDegree ≠ 0

Tactic:
rwa [natDegree_X_pow]

Premises used: Polynomial.natDegree_X_pow
-- Module: Mathlib.FieldTheory.AbelRuffini
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
⊢ 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:
exact Gal.splits_in_splittingField_of_comp _ _ (by rwa [natDegree_X_pow])

Premises used: Polynomial.Gal.splits_in_splittingField_of_comp
-- Module: Mathlib.FieldTheory.AbelRuffini
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 :
  ∀ (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))))
⊢ 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)

Premises used: Polynomial.splits_iff_exists_multiset, Polynomial.SplittingField.splits, Iff.mp
-- Module: Mathlib.FieldTheory.AbelRuffini
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))
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
⊢ IsSolvable.{u_1}
    (Gal (F := p.SplittingField) (map (algebraMap F p.SplittingField) (p.comp (HPow.hPow (α := F[X]) X n))))

Tactic:
rw [map_comp, Polynomial.map_pow, map_X, hs, mul_comp, C_comp]

Premises used: Polynomial.map_pow, Polynomial.map_X, Polynomial.C_comp, Polynomial.mul_comp, Polynomial.map_comp
-- Module: Mathlib.FieldTheory.AbelRuffini
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))
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
⊢ 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:
apply gal_mul_isSolvable (gal_C_isSolvable _)

Premises used: gal_C_isSolvable, gal_mul_isSolvable
-- Module: Mathlib.FieldTheory.AbelRuffini
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))
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))))
⊢ 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:
rw [multiset_prod_comp]

Premises used: Polynomial.multiset_prod_comp
-- Module: Mathlib.FieldTheory.AbelRuffini
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))
hq :
  ∀ (p_1 : p.SplittingField[X]),
    Membership.mem (γ := Multiset p.SplittingField[X])
        (Multiset.map (fun (p_2 : p.SplittingField[X]) ↦ p_2.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))
        p_1 →
      IsSolvable.{u_1} p_1.Gal
⊢ 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:
apply gal_prod_isSolvable

Premises used: gal_prod_isSolvable
-- Module: Mathlib.FieldTheory.AbelRuffini
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))
q : p.SplittingField[X]
hq :
  Membership.mem (γ := Multiset p.SplittingField[X])
    (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))
    q
⊢ ∃ (a : p.SplittingField[X]),
    Membership.mem (γ := Multiset p.SplittingField[X])
        (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)
        a ∧
      a.comp (HPow.hPow (α := p.SplittingField[X]) X n) = q

Tactic:
rw [Multiset.mem_map] at hq

Premises used: Multiset.mem_map
-- Module: Mathlib.FieldTheory.AbelRuffini
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))
q : p.SplittingField[X]
hq :
  ∃ (a : p.SplittingField[X]),
    Membership.mem (γ := Multiset p.SplittingField[X])
        (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)
        a ∧
      a.comp (HPow.hPow (α := p.SplittingField[X]) X n) = q
hq₁ :
  ∀ (q : p.SplittingField[X])
    (hq :
      Membership.mem (γ := Multiset p.SplittingField[X])
        (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)
        q),
    IsSolvable.{u_1} (q.comp (HPow.hPow (α := p.SplittingField[X]) X n)).Gal
⊢ IsSolvable.{u_1} q.Gal

Tactic:
obtain ⟨q, hq, rfl⟩ := hq

Premises used: rfl
-- Module: Mathlib.FieldTheory.AbelRuffini
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))
q : p.SplittingField[X]
hq :
  Membership.mem (γ := Multiset p.SplittingField[X])
    (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)
    q
⊢ ∃ a ∈ s,
    HSub.hSub (α := p.SplittingField[X]) (β := p.SplittingField[X]) X
        ((C : (a : p.SplittingField) → p.SplittingField[X]) a : p.SplittingField[X]) =
      q

Tactic:
rw [Multiset.mem_map] at hq

Premises used: Multiset.mem_map
-- Module: Mathlib.FieldTheory.AbelRuffini
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))
q : p.SplittingField[X]
hq :
  ∃ a ∈ s,
    HSub.hSub (α := p.SplittingField[X]) (β := p.SplittingField[X]) X
        ((C : (a : p.SplittingField) → p.SplittingField[X]) a : p.SplittingField[X]) =
      q
hq₁ :
  ∀ q ∈ s,
    IsSolvable.{u_1}
      ((HSub.hSub (α := p.SplittingField[X]) (β := p.SplittingField[X]) X
              ((C : (a : p.SplittingField) → p.SplittingField[X]) q : p.SplittingField[X])).comp
          (HPow.hPow (α := p.SplittingField[X]) X n)).Gal
⊢ IsSolvable.{u_1} (q.comp (HPow.hPow (α := p.SplittingField[X]) X n)).Gal

Tactic:
obtain ⟨q, _, rfl⟩ := hq

Premises used: rfl