awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
inst : Field F
n : ℕ
x : F
hx : ¬x = 0
neg : (HPow.hPow (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField[X]) X n - 1).Splits
⊢ (map (RingHom.id (HPow.hPow (α := F[X]) X n - 1).SplittingField)
      (HPow.hPow (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField[X]) X n - 1)).Splits

Tactic:
rw [map_id]

Premises used: Polynomial.map_id
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
inst : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ 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))

Tactic:
have key := SplittingField.splits (X ^ n - 1 : F[X])
-- Module: Mathlib.FieldTheory.AbelRuffini
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
neg₃ neg₄ neg₅ 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
⊢ (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

Premises used: Polynomial.map_one, Polynomial.map_pow, Polynomial.map_X, Polynomial.map_sub
-- 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
s : IntermediateField F E
H : ∀ (x : E) (n : ℕ), n ≠ 0 → x ^ n ∈ s → x ∈ s
⊢ solvableByRad F E ≤ s

Tactic:
sInf_le H

Premises used: Set.Mem, sInf_le
-- 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
n : ℕ
hn : n ≠ 0
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) (x ^ n)
⊢ Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x

Tactic:
grind [solvableByRad]

Premises used: 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
⊢ LE.le (α := IntermediateField F E) (solvableByRad F E) (algebraicClosure F E)

Tactic:
solvableByRad_le fun x n hn hx ↦ ?_

Premises used: solvableByRad_le
-- 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
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
⊢ LE.le (α := IntermediateField F E) (solvableByRad F E) (algebraicClosure F E)

Tactic:
refine solvableByRad_le fun x n hn hx ↦ ?_

Premises used: solvableByRad_le
-- 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
n : ℕ
hn : n ≠ 0
hx : Membership.mem (γ := IntermediateField F E) (algebraicClosure F E) (x ^ n)
rw : ∀ (hx : IsAlgebraic F (x ^ n)), IsAlgebraic F x
⊢ Membership.mem (γ := IntermediateField F E) (algebraicClosure F E) x

Tactic:
rw [mem_algebraicClosure_iff] at hx ⊢

Premises used: mem_algebraicClosure_iff
-- 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
n : ℕ
hn : n ≠ 0
hx : IsAlgebraic F (x ^ n)
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
⊢ IsAlgebraic F x

Tactic:
obtain ⟨p, h1, h2⟩ := hx
-- 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
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

Tactic:
⟨p.comp (X ^ n), ⟨fun h ↦ h1 (leadingCoeff_eq_zero.mp ?_), ?_⟩⟩

Premises used: IsAlgebraic, HPow.hPow, And.intro, Exists.intro, Iff.mp, Polynomial.X, Polynomial.comp, Polynomial.leadingCoeff_eq_zero
-- 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
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
refine_2 : Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) (p.comp (HPow.hPow (α := F[X]) X n)) : E) (0 : E)
⊢ IsAlgebraic F x

Tactic:
refine ⟨p.comp (X ^ n), ⟨fun h ↦ h1 (leadingCoeff_eq_zero.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
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
refine_1 : ∀ (h : (p.comp (HPow.hPow (α := F[X]) X n)).leadingCoeff = 0), (HPow.hPow (α := F[X]) X n).natDegree ≠ 0
⊢ p.leadingCoeff = 0

Tactic:
rwa [← leadingCoeff_eq_zero, leadingCoeff_comp, leadingCoeff_X_pow, one_pow, mul_one] at h

Premises used: one_pow, Polynomial.leadingCoeff_X_pow, Polynomial.leadingCoeff_comp, mul_one, Polynomial.leadingCoeff_eq_zero
-- 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
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)).leadingCoeff = 0
refine_1 refine_1₁ refine_1₂ refine_1₃ : 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
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)
⊢ Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) (p.comp (HPow.hPow (α := F[X]) X n)) : E) (0 : E)

Tactic:
simpa [aeval_comp]

Premises used: Polynomial.aeval_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
⊢ Subalgebra.IsAlgebraic (IntermediateField.toSubalgebra (solvableByRad F E))

Tactic:
fun _ hx ↦ mem_algebraicClosure_iff.1 (solvableByRad_le_algClosure _ _ hx)

Premises used: mem_algebraicClosure_iff, solvableByRad_le_algClosure, Subalgebra.IsAlgebraic, 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
⊢ IsIntegral F x

Tactic:
(isAlgebraic_solvableByRad _ hx).isIntegral

Premises used: IsAlgebraic.isIntegral, isAlgebraic_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
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
let : motive x hx
⊢ motive x hx

Tactic:
let s : Subalgebra F E :=
  { carrier := {x | ∃ hx : x ∈ solvableByRad F E, motive x hx}
    algebraMap_mem' a := ⟨algebraMap_mem _ a, mem a⟩
    add_mem' := fun ⟨ha, ha'⟩ ⟨hb, hb'⟩ ↦ ⟨add_mem ha hb, add _ _ ha hb ha' hb'⟩
    mul_mem' := fun ⟨ha, ha'⟩ ⟨hb, hb'⟩ ↦ ⟨mul_mem ha hb, mul _ _ ha hb ha' hb'⟩ }
-- 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
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
a : Membership.mem (γ := Subalgebra F E) (IntermediateField.toSubalgebra (solvableByRad F E)) x
⊢ IsAlgebraic F x

Tactic:
apply isAlgebraic_solvableByRad

Premises used: isAlgebraic_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
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
⊢ Membership.mem (γ := Subalgebra F E) (IntermediateField.toSubalgebra (solvableByRad F E)) x

Tactic:
hx

Premises used: Set.Mem
-- 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
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
⊢ Membership.mem (γ := Subalgebra F E) (IntermediateField.toSubalgebra (solvableByRad F E)) x

Tactic:
exact hx
-- 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
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' := ⋯ }
t : IntermediateField F E := Subalgebra.IsAlgebraic.toIntermediateField (S := s) ⋯
x : E
n : ℕ
hn : n ≠ 0
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) (x ^ n)
hx' : motive (x ^ n) hx
⊢ x ∈ t

Tactic:
⟨rad_mem hn hx, rad _ _ hn hx hx'⟩

Premises used: Set.Mem, setOf, solvableByRad.rad_mem, Exists.intro
-- 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
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' := ⋯ }
t : IntermediateField F E := Subalgebra.IsAlgebraic.toIntermediateField (S := s) ⋯
x : E
n : ℕ
hn : n ≠ 0
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) (x ^ n)
hx' : motive (x ^ n) hx
⊢ x ∈ t

Tactic:
exact ⟨rad_mem hn hx, rad _ _ hn hx hx'⟩
-- 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
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) ⋯
⊢ ∀ (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'⟩
-- 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
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) ⋯
ht : ∀ (x : E) (n : ℕ) (hn : n ≠ 0), x ^ n ∈ t → x ∈ t
⊢ Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x

Tactic:
obtain ⟨_, h⟩ := solvableByRad_le (s := t) ht hx

Premises used: solvableByRad_le
-- 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
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) ⋯
ht : ∀ (x : E) (n : ℕ) (hn : n ≠ 0), x ^ n ∈ t → x ∈ t
w : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
⊢ motive x w

Tactic:
obtain ⟨_, h⟩ := solvableByRad_le (s := t) ht hx

Premises used: solvableByRad_le
-- 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
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) ⋯
ht : ∀ (x : E) (n : ℕ) (hn : n ≠ 0), x ^ n ∈ t → x ∈ t
w : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
h : motive x w
⊢ motive x hx

Tactic:
h
-- 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
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) ⋯
ht : ∀ (x : E) (n : ℕ) (hn : n ≠ 0), x ^ n ∈ t → x ∈ t
w : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
h : motive x w
⊢ motive x hx

Tactic:
exact h