-- Mathlib/FieldTheory/AbelRuffini.lean
theorem induction2 {α β γ : solvableByRad F E} (hγ : γ ∈ F⟮α, β⟯) (hα : P α) (hβ : P β) : P γ

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α β γ : ↥(solvableByRad F E)
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
⊢ P γ

Tactic:
let p := minpoly F α

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α β γ : ↥(solvableByRad F E)
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
p : F[X] := minpoly F α
⊢ P γ

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α β γ : ↥(solvableByRad F E)
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
p : F[X] := minpoly F α
q : F[X] := minpoly F β
hpq :
  Splits (algebraMap F (p * q).SplittingField) (minpoly F α) ∧
    Splits (algebraMap F (p * q).SplittingField) (minpoly F β)
f : ↥F⟮α, β⟯ →ₐ[F] (p * q).SplittingField := Classical.choice ⋯
⊢ (aeval (f ⟨γ, hγ⟩)) (minpoly F γ) = 0

Tactic:
suffices aeval (⟨γ, hγ⟩ : F⟮α, β⟯) (minpoly F γ) = 0 by
  rw [aeval_algHom_apply, this, map_zero]

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α β γ : ↥(solvableByRad F E)
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
p : F[X] := minpoly F α
q : F[X] := minpoly F β
hpq :
  Splits (algebraMap F (p * q).SplittingField) (minpoly F α) ∧
    Splits (algebraMap F (p * q).SplittingField) (minpoly F β)
f : ↥F⟮α, β⟯ →ₐ[F] (p * q).SplittingField := Classical.choice ⋯
⊢ (aeval ⟨γ, hγ⟩) (minpoly F γ) = 0

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α β γ : ↥(solvableByRad F E)
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
p : F[X] := minpoly F α
q : F[X] := minpoly F β
⊢ P γ

Tactic:
have hpq := Polynomial.splits_of_splits_mul _
  (mul_ne_zero (minpoly.ne_zero (isIntegral α)) (minpoly.ne_zero (isIntegral β)))
  (SplittingField.splits (p * q))

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α β γ : ↥(solvableByRad F E)
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
p : F[X] := minpoly F α
q : F[X] := minpoly F β
hpq :
  Splits (algebraMap F (p * q).SplittingField) (minpoly F α) ∧
    Splits (algebraMap F (p * q).SplittingField) (minpoly F β)
⊢ P γ

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α β γ : ↥(solvableByRad F E)
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
p : F[X] := minpoly F α
q : F[X] := minpoly F β
hpq :
  Splits (algebraMap F (p * q).SplittingField) (minpoly F α) ∧
    Splits (algebraMap F (p * q).SplittingField) (minpoly F β)
x : ↥(solvableByRad F E)
hx : x = α ∨ x = β
⊢ IsIntegral F x ∧ Splits (algebraMap F (p * q).SplittingField) (minpoly F x)

Tactic:
cases hx with rw [hx]
| inl hx => exact ⟨isIntegral α, hpq.1⟩
| inr hx => exact ⟨isIntegral β, hpq.2⟩

Result:
no goals

Proof state:
case a
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α β γ : ↥(solvableByRad F E)
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
p : F[X] := minpoly F α
q : F[X] := minpoly F β
hpq :
  Splits (algebraMap F (p * q).SplittingField) (minpoly F α) ∧
    Splits (algebraMap F (p * q).SplittingField) (minpoly F β)
f : ↥F⟮α, β⟯ →ₐ[F] (p * q).SplittingField := Classical.choice ⋯
⊢ (aeval ⟨γ, hγ⟩) (minpoly F γ) = 0

Tactic:
apply Subtype.val_injective

Result:
case a.a
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α β γ : ↥(solvableByRad F E)
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
p : F[X] := minpoly F α
q : F[X] := minpoly F β
hpq :
  Splits (algebraMap F (p * q).SplittingField) (minpoly F α) ∧
    Splits (algebraMap F (p * q).SplittingField) (minpoly F β)
f : ↥F⟮α, β⟯ →ₐ[F] (p * q).SplittingField := Classical.choice ⋯
⊢ ↑((aeval ⟨γ, hγ⟩) (minpoly F γ)) = ↑0

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α β γ : ↥(solvableByRad F E)
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
p : F[X] := minpoly F α
q : F[X] := minpoly F β
hpq :
  Splits (algebraMap F (p * q).SplittingField) (minpoly F α) ∧
    Splits (algebraMap F (p * q).SplittingField) (minpoly F β)
f : ↥F⟮α, β⟯ →ₐ[F] (p * q).SplittingField := Classical.choice ⋯
⊢ (aeval ⟨γ, hγ⟩) (minpoly F γ) = 0

Tactic:
apply (algebraMap (↥F⟮α, β⟯) (solvableByRad F E)).injective

Result:
case a
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α β γ : ↥(solvableByRad F E)
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
p : F[X] := minpoly F α
q : F[X] := minpoly F β
hpq :
  Splits (algebraMap F (p * q).SplittingField) (minpoly F α) ∧
    Splits (algebraMap F (p * q).SplittingField) (minpoly F β)
f : ↥F⟮α, β⟯ →ₐ[F] (p * q).SplittingField := Classical.choice ⋯
⊢ (algebraMap ↥F⟮α, β⟯ ↥(solvableByRad F E)) ((aeval ⟨γ, hγ⟩) (minpoly F γ)) =
    (algebraMap ↥F⟮α, β⟯ ↥(solvableByRad F E)) 0

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α β γ : ↥(solvableByRad F E)
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
p : F[X] := minpoly F α
⊢ P γ

Tactic:
let q := minpoly F β

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α β γ : ↥(solvableByRad F E)
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
p : F[X] := minpoly F α
q : F[X] := minpoly F β
⊢ P γ

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α β γ : ↥(solvableByRad F E)
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
p : F[X] := minpoly F α
q : F[X] := minpoly F β
hpq :
  Splits (algebraMap F (p * q).SplittingField) (minpoly F α) ∧
    Splits (algebraMap F (p * q).SplittingField) (minpoly F β)
⊢ ∀ s ∈ {α, β}, IsIntegral F s ∧ Splits (algebraMap F (p * q).SplittingField) (minpoly F s)

Tactic:
intro x hx

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α β γ : ↥(solvableByRad F E)
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
p : F[X] := minpoly F α
q : F[X] := minpoly F β
hpq :
  Splits (algebraMap F (p * q).SplittingField) (minpoly F α) ∧
    Splits (algebraMap F (p * q).SplittingField) (minpoly F β)
x : ↥(solvableByRad F E)
hx : x ∈ {α, β}
⊢ IsIntegral F x ∧ Splits (algebraMap F (p * q).SplittingField) (minpoly F x)

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α β γ : ↥(solvableByRad F E)
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
p : F[X] := minpoly F α
q : F[X] := minpoly F β
hpq :
  Splits (algebraMap F (p * q).SplittingField) (minpoly F α) ∧
    Splits (algebraMap F (p * q).SplittingField) (minpoly F β)
f : ↥F⟮α, β⟯ →ₐ[F] (p * q).SplittingField := Classical.choice ⋯
key : minpoly F γ = minpoly F (f ⟨γ, hγ⟩)
⊢ P γ

Tactic:
rw [P, key]

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α β γ : ↥(solvableByRad F E)
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
p : F[X] := minpoly F α
q : F[X] := minpoly F β
hpq :
  Splits (algebraMap F (p * q).SplittingField) (minpoly F α) ∧
    Splits (algebraMap F (p * q).SplittingField) (minpoly F β)
f : ↥F⟮α, β⟯ →ₐ[F] (p * q).SplittingField := Classical.choice ⋯
key : minpoly F γ = minpoly F (f ⟨γ, hγ⟩)
⊢ IsSolvable (minpoly F (f ⟨γ, hγ⟩)).Gal