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)
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
left : q ∈ s
hq :
  IsSolvable.{u_1}
    (HSub.hSub (β := p.SplittingField[X]) (HPow.hPow (α := p.SplittingField[X]) X n)
        ((C : (a : p.SplittingField) → p.SplittingField[X]) q : p.SplittingField[X])).Gal
⊢ 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

Tactic:
rw [sub_comp, X_comp, C_comp]

Premises used: Polynomial.X_comp, Polynomial.C_comp, Polynomial.sub_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))
q : p.SplittingField
left : q ∈ s
⊢ IsSolvable.{u_1}
    (HSub.hSub (β := p.SplittingField[X]) (HPow.hPow (α := p.SplittingField[X]) X n)
        ((C : (a : p.SplittingField) → p.SplittingField[X]) q : p.SplittingField[X])).Gal

Tactic:
gal_X_pow_sub_C_isSolvable n q

Premises used: gal_X_pow_sub_C_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
left : q ∈ s
⊢ IsSolvable.{u_1}
    (HSub.hSub (β := p.SplittingField[X]) (HPow.hPow (α := p.SplittingField[X]) X n)
        ((C : (a : p.SplittingField) → p.SplittingField[X]) q : p.SplittingField[X])).Gal

Tactic:
exact gal_X_pow_sub_C_isSolvable n q

Premises used: gal_X_pow_sub_C_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 y z : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
hy : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) y
hz : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) z
hx' : IsSolvable.{u_1} (Gal (minpoly F x))
hy' : IsSolvable.{u_1} (Gal (minpoly F y))
hz' : Membership.mem (γ := IntermediateField F E) F⟮x, y⟯ z
p : F[X] := minpoly F x
q : F[X] := minpoly F y
⊢ Splits (R := (p * q).SplittingField) (Polynomial.map (algebraMap F (p * q).SplittingField) (p * q))

Tactic:
have hpq := SplittingField.splits (p * q)
-- 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 y z : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
hy : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) y
hz : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) z
hx' : IsSolvable.{u_1} (Gal (minpoly F x))
hy' : IsSolvable.{u_1} (Gal (minpoly F y))
hz' : Membership.mem (γ := IntermediateField F E) F⟮x, y⟯ z
p : F[X] := minpoly F x
q : F[X] := minpoly F y
hpq : Splits (R := (p * q).SplittingField) (Polynomial.map (algebraMap F (p * q).SplittingField) (p * q))
⊢ Splits (R := (p * q).SplittingField) (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F x)) ∧
    Splits (R := (p * q).SplittingField) (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F y))

Tactic:
rw [Polynomial.map_mul,
    splits_mul_iff (map_ne_zero (minpoly.ne_zero (isIntegral_of_mem_solvableByRad hx)))
      (map_ne_zero (minpoly.ne_zero (isIntegral_of_mem_solvableByRad hy)))] at hpq

Premises used: Polynomial.map_mul, Polynomial.splits_mul_iff, Polynomial.map_ne_zero, 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
y z : E
hy : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) y
hz : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) z
hy' : IsSolvable.{u_1} (Gal (minpoly F y))
q : F[X] := minpoly F y
a : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) a
hx' : IsSolvable.{u_1} (Gal (minpoly F a))
hz' : Membership.mem (γ := IntermediateField F E) F⟮a, y⟯ z
p : F[X] := minpoly F a
hpq :
  Splits (R := (p * q).SplittingField) (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F a)) ∧
    Splits (R := (p * q).SplittingField) (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F y))
⊢ IsIntegral F a ∧
    Splits (R := (p * q).SplittingField) (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F a))

Tactic:
⟨isIntegral_of_mem_solvableByRad hx, hpq.1⟩

Premises used: And.left, And.intro, 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
y z : E
hy : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) y
hz : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) z
hy' : IsSolvable.{u_1} (Gal (minpoly F y))
q : F[X] := minpoly F y
a : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) a
hx' : IsSolvable.{u_1} (Gal (minpoly F a))
hz' : Membership.mem (γ := IntermediateField F E) F⟮a, y⟯ z
p : F[X] := minpoly F a
hpq :
  Splits (R := (p * q).SplittingField) (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F a)) ∧
    Splits (R := (p * q).SplittingField) (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F y))
⊢ IsIntegral F a ∧
    Splits (R := (p * q).SplittingField) (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F a))

Tactic:
exact ⟨isIntegral_of_mem_solvableByRad hx, hpq.1⟩
-- 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 z : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
hz : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) z
hx' : IsSolvable.{u_1} (Gal (minpoly F x))
p : F[X] := minpoly F x
a : E
hy : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) a
hy' : IsSolvable.{u_1} (Gal (minpoly F a))
hz' : Membership.mem (γ := IntermediateField F E) F⟮x, a⟯ z
q : F[X] := minpoly F a
hpq :
  Splits (R := (p * q).SplittingField) (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F x)) ∧
    Splits (R := (p * q).SplittingField) (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F a))
⊢ IsIntegral F a ∧
    Splits (R := (p * q).SplittingField) (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F a))

Tactic:
⟨isIntegral_of_mem_solvableByRad hy, hpq.2⟩

Premises used: And.right, And.intro, 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 z : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
hz : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) z
hx' : IsSolvable.{u_1} (Gal (minpoly F x))
p : F[X] := minpoly F x
a : E
hy : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) a
hy' : IsSolvable.{u_1} (Gal (minpoly F a))
hz' : Membership.mem (γ := IntermediateField F E) F⟮x, a⟯ z
q : F[X] := minpoly F a
hpq :
  Splits (R := (p * q).SplittingField) (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F x)) ∧
    Splits (R := (p * q).SplittingField) (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F a))
⊢ IsIntegral F a ∧
    Splits (R := (p * q).SplittingField) (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F a))

Tactic:
exact ⟨isIntegral_of_mem_solvableByRad hy, hpq.2⟩
-- 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 y z : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
hy : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) y
hz : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) z
hx' : IsSolvable.{u_1} (Gal (minpoly F x))
hy' : IsSolvable.{u_1} (Gal (minpoly F y))
hz' : Membership.mem (γ := IntermediateField F E) F⟮x, y⟯ z
p : F[X] := minpoly F x
q : F[X] := minpoly F y
hpq :
  Splits (R := (p * q).SplittingField) (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F x)) ∧
    Splits (R := (p * q).SplittingField) (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F y))
have : ∀ (f : AlgHom.{u_1, u_2, u_1} F (↥F⟮x, y⟯) (p * q).SplittingField), IsSolvable.{u_1} (Gal (minpoly F z))
⊢ IsSolvable.{u_1} (Gal (minpoly F z))

Tactic:
have f : ↥F⟮x, y⟯ →ₐ[F] (p * q).SplittingField :=
    Classical.choice <| nonempty_algHom_adjoin_of_splits <| by
      rintro a (rfl | rfl)
      · exact ⟨isIntegral_of_mem_solvableByRad hx, hpq.1⟩
      · exact ⟨isIntegral_of_mem_solvableByRad hy, hpq.2⟩
-- 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 y z : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
hy : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) y
hz : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) z
hx' : IsSolvable.{u_1} (Gal (minpoly F x))
hy' : IsSolvable.{u_1} (Gal (minpoly F y))
hz' : Membership.mem (γ := IntermediateField F E) F⟮x, y⟯ z
p : F[X] := minpoly F x
q : F[X] := minpoly F y
hpq :
  Splits (R := (p * q).SplittingField) (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F x)) ∧
    Splits (R := (p * q).SplittingField) (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F y))
f : AlgHom.{u_1, u_2, u_1} F (↥F⟮x, y⟯) (p * q).SplittingField
⊢ Eq (α := F[X]) (minpoly F z)
    (minpoly F (B := (p * q).SplittingField)
      ((f : (a : ↥F⟮x, y⟯) → (p * q).SplittingField)
          (Subtype.mk (p := fun (x_1 : E) ↦ Membership.mem (γ := IntermediateField F E) F⟮x, y⟯ x_1) z hz') :
        (p * q).SplittingField))

Tactic:
minpoly.eq_of_irreducible_of_monic
      (minpoly.irreducible (isIntegral_of_mem_solvableByRad hz)) ?_
      (minpoly.monic (isIntegral_of_mem_solvableByRad hz))

Premises used: minpoly.monic, minpoly.eq_of_irreducible_of_monic, minpoly.irreducible, 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 y z : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
hy : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) y
hz : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) z
hx' : IsSolvable.{u_1} (Gal (minpoly F x))
hy' : IsSolvable.{u_1} (Gal (minpoly F y))
hz' : Membership.mem (γ := IntermediateField F E) F⟮x, y⟯ z
p : F[X] := minpoly F x
q : F[X] := minpoly F y
hpq :
  Splits (R := (p * q).SplittingField) (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F x)) ∧
    Splits (R := (p * q).SplittingField) (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F y))
f : AlgHom.{u_1, u_2, u_1} F (↥F⟮x, y⟯) (p * q).SplittingField
refine :
  Eq (α := (p * q).SplittingField)
    (((aeval
            ((f : (a : ↥F⟮x, y⟯) → (p * q).SplittingField)
              (Subtype.mk (p := fun (x_1 : E) ↦ Membership.mem (γ := IntermediateField F E) F⟮x, y⟯ x_1) z hz')) :
          F[X] →ₐ[F] (p * q).SplittingField) :
        (a : F[X]) → (p * q).SplittingField)
      (minpoly F z))
    0
⊢ Eq (α := F[X]) (minpoly F z)
    (minpoly F (B := (p * q).SplittingField)
      ((f : (a : ↥F⟮x, y⟯) → (p * q).SplittingField)
          (Subtype.mk (p := fun (x_1 : E) ↦ Membership.mem (γ := IntermediateField F E) F⟮x, y⟯ x_1) z hz') :
        (p * q).SplittingField))

Tactic:
refine minpoly.eq_of_irreducible_of_monic
      (minpoly.irreducible (isIntegral_of_mem_solvableByRad hz)) ?_
      (minpoly.monic (isIntegral_of_mem_solvableByRad hz))

Premises used: minpoly.monic, minpoly.eq_of_irreducible_of_monic, minpoly.irreducible, 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 y z : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
hy : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) y
hz : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) z
hx' : IsSolvable.{u_1} (Gal (minpoly F x))
hy' : IsSolvable.{u_1} (Gal (minpoly F y))
hz' : Membership.mem (γ := IntermediateField F E) F⟮x, y⟯ z
p : F[X] := minpoly F x
q : F[X] := minpoly F y
hpq :
  Splits (R := (p * q).SplittingField) (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F x)) ∧
    Splits (R := (p * q).SplittingField) (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F y))
f : AlgHom.{u_1, u_2, u_1} F (↥F⟮x, y⟯) (p * q).SplittingField
rw :
  Eq.{u_2 + 1} (α := ↥F⟮x, y⟯)
    ((aeval (Subtype.mk (p := fun (x_1 : E) ↦ Membership.mem (γ := IntermediateField F E) F⟮x, y⟯ x_1) z hz') :
          (a : F[X]) → ↥F⟮x, y⟯)
        (minpoly F z) :
      ↥F⟮x, y⟯)
    (0 : ↥F⟮x, y⟯)
⊢ Eq (α := (p * q).SplittingField)
    (((aeval
            ((f : (a : ↥F⟮x, y⟯) → (p * q).SplittingField)
              (Subtype.mk (p := fun (x_1 : E) ↦ Membership.mem (γ := IntermediateField F E) F⟮x, y⟯ x_1) z hz')) :
          F[X] →ₐ[F] (p * q).SplittingField) :
        (a : F[X]) → (p * q).SplittingField)
      (minpoly F z))
    0

Tactic:
rw [aeval_algHom_apply, map_eq_zero]

Premises used: map_eq_zero, Polynomial.aeval_algHom_apply
-- 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 y z : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
hy : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) y
hz : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) z
hx' : IsSolvable.{u_1} (Gal (minpoly F x))
hy' : IsSolvable.{u_1} (Gal (minpoly F y))
hz' : Membership.mem (γ := IntermediateField F E) F⟮x, y⟯ z
p : F[X] := minpoly F x
q : F[X] := minpoly F y
hpq :
  Splits (R := (p * q).SplittingField) (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F x)) ∧
    Splits (R := (p * q).SplittingField) (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F y))
f : AlgHom.{u_1, u_2, u_1} F (↥F⟮x, y⟯) (p * q).SplittingField
a :
  Eq (α := E)
    ((algebraMap (↥F⟮x, y⟯) E : (a : ↥F⟮x, y⟯) → E)
        ((aeval (Subtype.mk (p := fun (x_1 : E) ↦ Membership.mem (γ := IntermediateField F E) F⟮x, y⟯ x_1) z hz') :
              (a : F[X]) → ↥F⟮x, y⟯)
            (minpoly F z) :
          ↥F⟮x, y⟯) :
      E)
    ((algebraMap (↥F⟮x, y⟯) E : (a : ↥F⟮x, y⟯) → E) 0 : E)
⊢ Eq.{u_2 + 1} (α := ↥F⟮x, y⟯)
    ((aeval (Subtype.mk (p := fun (x_1 : E) ↦ Membership.mem (γ := IntermediateField F E) F⟮x, y⟯ x_1) z hz') :
          (a : F[X]) → ↥F⟮x, y⟯)
        (minpoly F z) :
      ↥F⟮x, y⟯)
    (0 : ↥F⟮x, y⟯)

Tactic:
apply (algebraMap (↥F⟮x, y⟯) E).injective

Premises used: Algebra.algebraMap, Membership.mem, Subtype, Insert.insert, RingHom.injective, IntermediateField.adjoin, Singleton.singleton
-- 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 y z : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
hy : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) y
hz : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) z
hx' : IsSolvable.{u_1} (Gal (minpoly F x))
hy' : IsSolvable.{u_1} (Gal (minpoly F y))
hz' : Membership.mem (γ := IntermediateField F E) F⟮x, y⟯ z
p : F[X] := minpoly F x
q : F[X] := minpoly F y
hpq :
  Splits (R := (p * q).SplittingField) (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F x)) ∧
    Splits (R := (p * q).SplittingField) (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F y))
f : AlgHom.{u_1, u_2, u_1} F (↥F⟮x, y⟯) (p * q).SplittingField
⊢ Eq (α := E)
    ((algebraMap (↥F⟮x, y⟯) E : (a : ↥F⟮x, y⟯) → E)
        ((aeval (Subtype.mk (p := fun (x_1 : E) ↦ Membership.mem (γ := IntermediateField F E) F⟮x, y⟯ x_1) z hz') :
              (a : F[X]) → ↥F⟮x, y⟯)
            (minpoly F z) :
          ↥F⟮x, y⟯) :
      E)
    ((algebraMap (↥F⟮x, y⟯) E : (a : ↥F⟮x, y⟯) → E) 0 : E)

Tactic:
simp [← aeval_algebraMap_apply]

Premises used: Polynomial.aeval_algebraMap_apply
-- 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 y z : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
hy : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) y
hz : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) z
hx' : IsSolvable.{u_1} (Gal (minpoly F x))
hy' : IsSolvable.{u_1} (Gal (minpoly F y))
hz' : Membership.mem (γ := IntermediateField F E) F⟮x, y⟯ z
p : F[X] := minpoly F x
q : F[X] := minpoly F y
hpq :
  Splits (R := (p * q).SplittingField) (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F x)) ∧
    Splits (R := (p * q).SplittingField) (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F y))
f : AlgHom.{u_1, u_2, u_1} F (↥F⟮x, y⟯) (p * q).SplittingField
⊢ Eq (α := F[X]) (minpoly F z)
    (minpoly F (B := (p * q).SplittingField)
      ((f : (a : ↥F⟮x, y⟯) → (p * q).SplittingField)
          (Subtype.mk (p := fun (x_1 : E) ↦ Membership.mem (γ := IntermediateField F E) F⟮x, y⟯ x_1) z hz') :
        (p * q).SplittingField))

Tactic:
have key : minpoly F z = minpoly F (f ⟨z, hz'⟩) := by
    refine minpoly.eq_of_irreducible_of_monic
      (minpoly.irreducible (isIntegral_of_mem_solvableByRad hz)) ?_
      (minpoly.monic (isIntegral_of_mem_solvableByRad hz))
    rw [aeval_algHom_apply, map_eq_zero]
    apply (algebraMap (↥F⟮x, y⟯) E).injective
    simp [← aeval_algebraMap_apply]
-- 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 y z : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
hy : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) y
hz : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) z
hx' : IsSolvable.{u_1} (Gal (minpoly F x))
hy' : IsSolvable.{u_1} (Gal (minpoly F y))
hz' : Membership.mem (γ := IntermediateField F E) F⟮x, y⟯ z
p : F[X] := minpoly F x
q : F[X] := minpoly F y
hpq :
  Splits (R := (p * q).SplittingField) (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F x)) ∧
    Splits (R := (p * q).SplittingField) (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F y))
f : AlgHom.{u_1, u_2, u_1} F (↥F⟮x, y⟯) (p * q).SplittingField
key :
  Eq (α := F[X]) (minpoly F z)
    (minpoly F (B := (p * q).SplittingField)
      ((f : (a : ↥F⟮x, y⟯) → (p * q).SplittingField)
          (Subtype.mk (p := fun (x_1 : E) ↦ Membership.mem (γ := IntermediateField F E) F⟮x, y⟯ x_1) z hz') :
        (p * q).SplittingField))
rw :
  IsSolvable.{u_1}
    (Gal
      (minpoly F (B := (p * q).SplittingField)
        ((f : (a : ↥F⟮x, y⟯) → (p * q).SplittingField)
            (Subtype.mk (p := fun (x_1 : E) ↦ Membership.mem (γ := IntermediateField F E) F⟮x, y⟯ x_1) z hz') :
          (p * q).SplittingField)))
⊢ IsSolvable.{u_1} (Gal (minpoly F z))

Tactic:
rw [key]
-- 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 y z : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
hy : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) y
hz : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) z
hx' : IsSolvable.{u_1} (Gal (minpoly F x))
hy' : IsSolvable.{u_1} (Gal (minpoly F y))
hz' : Membership.mem (γ := IntermediateField F E) F⟮x, y⟯ z
p : F[X] := minpoly F x
q : F[X] := minpoly F y
hpq :
  Splits (R := (p * q).SplittingField) (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F x)) ∧
    Splits (R := (p * q).SplittingField) (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F y))
f : AlgHom.{u_1, u_2, u_1} F (↥F⟮x, y⟯) (p * q).SplittingField
key :
  Eq (α := F[X]) (minpoly F z)
    (minpoly F (B := (p * q).SplittingField)
      ((f : (a : ↥F⟮x, y⟯) → (p * q).SplittingField)
          (Subtype.mk (p := fun (x_1 : E) ↦ Membership.mem (γ := IntermediateField F E) F⟮x, y⟯ x_1) z hz') :
        (p * q).SplittingField))
⊢ IsSolvable.{u_1}
    (Gal
      (minpoly F (B := (p * q).SplittingField)
        ((f : (a : ↥F⟮x, y⟯) → (p * q).SplittingField)
            (Subtype.mk (p := fun (x_1 : E) ↦ Membership.mem (γ := IntermediateField F E) F⟮x, y⟯ x_1) z hz') :
          (p * q).SplittingField)))

Tactic:
gal_isSolvable_of_splits ⟨Normal.splits ?_ (f ⟨z, hz'⟩)⟩ (gal_mul_isSolvable hx' hy')

Premises used: Normal.splits, Subtype.mk, Fact.mk, gal_mul_isSolvable, gal_isSolvable_of_splits, DFunLike.coe