awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
      (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))))
have 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
Tactic: apply gal_prod_isSolvable
-- 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)
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
⊢ IsSolvable.{u_1} q.Gal
have 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
Tactic: rw [Multiset.mem_map] at hq
Cleared hypotheses: hq
-- 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))
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
⊢ IsSolvable.{u_1} q.Gal
have 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
Tactic: obtain ⟨q, hq, rfl⟩ := hq
Cleared hypotheses: q, hq
-- 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)
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
⊢ IsSolvable.{u_1} (q.comp (HPow.hPow (α := p.SplittingField[X]) X n)).Gal
have hq₁ : ∃ 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
Cleared hypotheses: hq
-- 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))
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
⊢ IsSolvable.{u_1} (q.comp (HPow.hPow (α := p.SplittingField[X]) X n)).Gal
have 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
Tactic: obtain ⟨q, _, rfl⟩ := hq
Cleared hypotheses: q, hq
-- 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))
q : p.SplittingField
left : 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
have 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
Tactic: rw [sub_comp, X_comp, C_comp]
-- 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 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
⊢ IsSolvable.{u_1} (Gal (minpoly F z))
have hpq : Splits (R := (p * q).SplittingField) (Polynomial.map (algebraMap F (p * q).SplittingField) (p * q))
Tactic: have hpq := SplittingField.splits (p * q)
-- 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 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))
⊢ IsSolvable.{u_1} (Gal (minpoly F z))
have 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))
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
Cleared hypotheses: hpq
-- 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 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))
⊢ IsSolvable.{u_1} (Gal (minpoly F z))
have have : ∀ (f : AlgHom.{u_1, u_2, u_1} F (↥F⟮x, y⟯) (p * q).SplittingField), 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⟩
-- 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 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))
have 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
Tactic: refine minpoly.eq_of_irreducible_of_monic
      (minpoly.irreducible (isIntegral_of_mem_solvableByRad hz)) ?_
      (minpoly.monic (isIntegral_of_mem_solvableByRad hz))
-- 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 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 (α := (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
have 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⟯)
Tactic: rw [aeval_algHom_apply, map_eq_zero]
-- 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 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.{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⟯)
have 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)
Tactic: apply (algebraMap (↥F⟮x, y⟯) E).injective
-- 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 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
⊢ IsSolvable.{u_1} (Gal (minpoly F z))
have 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))
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]
-- 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 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 z))
have 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)))
Tactic: rw [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
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)))
have refine : Normal F (p * q).SplittingField
Tactic: refine gal_isSolvable_of_splits ⟨Normal.splits ?_ (f ⟨z, hz'⟩)⟩ (gal_mul_isSolvable hx' hy')
-- 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
y : F
⊢ IsSolvable.{u_1} (Gal (minpoly.{u_1, u_2} F (B := E) ((algebraMap F E : (a : F) → E) y : E)))
have mem : IsSolvable.{u_1} (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X])).Gal
Tactic: rw [minpoly.eq_X_sub_C E]
-- 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 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))
hz' : IsSolvable.{u_1} (Gal (minpoly F z))
⊢ IsSolvable.{u_1} (Gal (minpoly F (y + z)))
have apply : Membership.mem (γ := IntermediateField F E) F⟮y, z⟯ y
Tactic: apply induction_step hy hz (add_mem hy hz) hy' hz' (add_mem ..)
-- 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 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))
hz' : IsSolvable.{u_1} (Gal (minpoly F z))
apply : Membership.mem (γ := IntermediateField F E) F⟮y, z⟯ y
⊢ IsSolvable.{u_1} (Gal (minpoly F (y + z)))
have apply₁ : Membership.mem (γ := IntermediateField F E) F⟮y, z⟯ z
Tactic: apply induction_step hy hz (add_mem hy hz) hy' hz' (add_mem ..)
-- 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 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))
hz' : IsSolvable.{u_1} (Gal (minpoly F z))
⊢ Membership.mem (γ := IntermediateField F E) F⟮y, z⟯ y
have a : Membership.mem (γ := Set E) {y, z} y
Tactic: apply subset_adjoin