-- Mathlib/FieldTheory/AbelRuffini.lean
theorem isIntegral (α : solvableByRad F E) : IsIntegral F α

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : ↥(solvableByRad F E)
n : ℕ
hn : n ≠ 0
hα : IsIntegral F (α ^ n)
p : F[X]
h1 : p ≠ 0
h2 : (aeval (α ^ n)) p = 0
⊢ (aeval α) (p.comp (X ^ n)) = 0

Tactic:
rw [aeval_comp, aeval_X_pow, h2]

Result:
no goals

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : ↥(solvableByRad F E)
⊢ IsIntegral F α

Tactic:
revert α

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ ∀ (α : ↥(solvableByRad F E)), IsIntegral F α

Proof state:
case rad
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : ↥(solvableByRad F E)
n : ℕ
hn : n ≠ 0
hα : IsIntegral F (α ^ n)
⊢ IsIntegral F α

Tactic:
obtain ⟨p, h1, h2⟩ := hα.isAlgebraic

Result:
case rad.intro.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : ↥(solvableByRad F E)
n : ℕ
hn : n ≠ 0
hα : IsIntegral F (α ^ n)
p : F[X]
h1 : p ≠ 0
h2 : (aeval (α ^ n)) p = 0
⊢ IsIntegral F α

Proof state:
case rad.intro.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : ↥(solvableByRad F E)
n : ℕ
hn : n ≠ 0
hα : IsIntegral F (α ^ n)
p : F[X]
h1 : p ≠ 0
h2 : (aeval (α ^ n)) p = 0
⊢ IsIntegral F α

Tactic:
refine IsAlgebraic.isIntegral ⟨p.comp (X ^ n),
  ⟨fun h => h1 (leadingCoeff_eq_zero.mp ?_), by rw [aeval_comp, aeval_X_pow, h2]⟩⟩

Result:
case rad.intro.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : ↥(solvableByRad F E)
n : ℕ
hn : n ≠ 0
hα : IsIntegral F (α ^ n)
p : F[X]
h1 : p ≠ 0
h2 : (aeval (α ^ n)) p = 0
h : p.comp (X ^ n) = 0
⊢ p.leadingCoeff = 0

Proof state:
case base
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ ∀ (α : F), IsIntegral F ((algebraMap F ↥(solvableByRad F E)) α)

Tactic:
exact fun _ => isIntegral_algebraMap

Result:
no goals

Proof state:
case rad
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ ∀ (α : ↥(solvableByRad F E)) (n : ℕ), n ≠ 0 → IsIntegral F (α ^ n) → IsIntegral F α

Tactic:
intro α n hn hα

Result:
case rad
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : ↥(solvableByRad F E)
n : ℕ
hn : n ≠ 0
hα : IsIntegral F (α ^ n)
⊢ IsIntegral F α

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ ∀ (α : ↥(solvableByRad F E)), IsIntegral F α

Tactic:
apply solvableByRad.induction

Result:
case base
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ ∀ (α : F), IsIntegral F ((algebraMap F ↥(solvableByRad F E)) α)

case add
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ ∀ (α β : ↥(solvableByRad F E)), IsIntegral F α → IsIntegral F β → IsIntegral F (α + β)

case neg
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ ∀ (α : ↥(solvableByRad F E)), IsIntegral F α → IsIntegral F (-α)

case mul
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ ∀ (α β : ↥(solvableByRad F E)), IsIntegral F α → IsIntegral F β → IsIntegral F (α * β)

case inv
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ ∀ (α : ↥(solvableByRad F E)), IsIntegral F α → IsIntegral F α⁻¹

case rad
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ ∀ (α : ↥(solvableByRad F E)) (n : ℕ), n ≠ 0 → IsIntegral F (α ^ n) → IsIntegral F α

Proof state:
case inv
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ ∀ (α : ↥(solvableByRad F E)), IsIntegral F α → IsIntegral F α⁻¹

Tactic:
intro α hα

Result:
case inv
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : ↥(solvableByRad F E)
hα : IsIntegral F α
⊢ IsIntegral F α⁻¹

Proof state:
case mul
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ ∀ (α β : ↥(solvableByRad F E)), IsIntegral F α → IsIntegral F β → IsIntegral F (α * β)

Tactic:
exact fun _ _ => IsIntegral.mul

Result:
no goals

Proof state:
case rad.intro.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : ↥(solvableByRad F E)
n : ℕ
hn : n ≠ 0
hα : IsIntegral F (α ^ n)
p : F[X]
h1 : p ≠ 0
h2 : (aeval (α ^ n)) p = 0
h : p.comp (X ^ n) = 0
⊢ p.leadingCoeff = 0

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

Result:
case rad.intro.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : ↥(solvableByRad F E)
n : ℕ
hn : n ≠ 0
hα : IsIntegral F (α ^ n)
p : F[X]
h1 : p ≠ 0
h2 : (aeval (α ^ n)) p = 0
h : (p.comp (X ^ n)).leadingCoeff = 0
⊢ (X ^ n).natDegree ≠ 0

Proof state:
case neg
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ ∀ (α : ↥(solvableByRad F E)), IsIntegral F α → IsIntegral F (-α)

Tactic:
exact fun _ => IsIntegral.neg

Result:
no goals

Proof state:
case rad.intro.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : ↥(solvableByRad F E)
n : ℕ
hn : n ≠ 0
hα : IsIntegral F (α ^ n)
p : F[X]
h1 : p ≠ 0
h2 : (aeval (α ^ n)) p = 0
h : (p.comp (X ^ n)).leadingCoeff = 0
⊢ (X ^ n).natDegree ≠ 0

Tactic:
rwa [natDegree_X_pow]

Result:
no goals

Proof state:
case add
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ ∀ (α β : ↥(solvableByRad F E)), IsIntegral F α → IsIntegral F β → IsIntegral F (α + β)

Tactic:
exact fun _ _ => IsIntegral.add

Result:
no goals

Proof state:
case inv
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : ↥(solvableByRad F E)
hα : IsIntegral F α
⊢ IsIntegral F α⁻¹

Tactic:
exact IsIntegral.inv hα

Result:
no goals