-- Mathlib/FieldTheory/AbelRuffini.lean
theorem induction (P : solvableByRad F E → Prop)
    (base : ∀ α : F, P (algebraMap F (solvableByRad F E) α))
    (add : ∀ α β : solvableByRad F E, P α → P β → P (α + β))
    (neg : ∀ α : solvableByRad F E, P α → P (-α))
    (mul : ∀ α β : solvableByRad F E, P α → P β → P (α * β))
    (inv : ∀ α : solvableByRad F E, P α → P α⁻¹)
    (rad : ∀ α : solvableByRad F E, ∀ n : ℕ, n ≠ 0 → P (α ^ n) → P α) (α : solvableByRad F E) :
    P α

Proof state:
case add
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
P : ↥(solvableByRad F E) → Prop
base : ∀ (α : F), P ((algebraMap F ↥(solvableByRad F E)) α)
add : ∀ (α β : ↥(solvableByRad F E)), P α → P β → P (α + β)
neg : ∀ (α : ↥(solvableByRad F E)), P α → P (-α)
mul : ∀ (α β : ↥(solvableByRad F E)), P α → P β → P (α * β)
inv : ∀ (α : ↥(solvableByRad F E)), P α → P α⁻¹
rad : ∀ (α : ↥(solvableByRad F E)) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
⊢ ∀ (α β : E),
    IsSolvableByRad F α →
      IsSolvableByRad F β → (∃ β, ↑β = α ∧ P β) → (∃ β_1, ↑β_1 = β ∧ P β_1) → ∃ β_1, ↑β_1 = α + β ∧ P β_1

Tactic:
intro α β _ _ Pα Pβ

Result:
case add
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
P : ↥(solvableByRad F E) → Prop
base : ∀ (α : F), P ((algebraMap F ↥(solvableByRad F E)) α)
add : ∀ (α β : ↥(solvableByRad F E)), P α → P β → P (α + β)
neg : ∀ (α : ↥(solvableByRad F E)), P α → P (-α)
mul : ∀ (α β : ↥(solvableByRad F E)), P α → P β → P (α * β)
inv : ∀ (α : ↥(solvableByRad F E)), P α → P α⁻¹
rad : ∀ (α : ↥(solvableByRad F E)) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
α β : E
a✝¹ : IsSolvableByRad F α
a✝ : IsSolvableByRad F β
Pα : ∃ β, ↑β = α ∧ P β
Pβ : ∃ β_1, ↑β_1 = β ∧ P β_1
⊢ ∃ β_1, ↑β_1 = α + β ∧ P β_1

Proof state:
case rad.intro.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
P : ↥(solvableByRad F E) → Prop
base : ∀ (α : F), P ((algebraMap F ↥(solvableByRad F E)) α)
add : ∀ (α β : ↥(solvableByRad F E)), P α → P β → P (α + β)
neg : ∀ (α : ↥(solvableByRad F E)), P α → P (-α)
mul : ∀ (α β : ↥(solvableByRad F E)), P α → P β → P (α * β)
inv : ∀ (α : ↥(solvableByRad F E)), P α → P α⁻¹
rad : ∀ (α : ↥(solvableByRad F E)) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
α : E
n : ℕ
hn : n ≠ 0
hα : IsSolvableByRad F (α ^ n)
α₀ : ↥(solvableByRad F E)
hα₀ : ↑α₀ = α ^ n
Pα : P α₀
⊢ ∃ β, ↑β = α ∧ P β

Tactic:
refine ⟨⟨α, IsSolvableByRad.rad α n hn hα⟩, rfl, rad _ n hn ?_⟩

Result:
case rad.intro.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
P : ↥(solvableByRad F E) → Prop
base : ∀ (α : F), P ((algebraMap F ↥(solvableByRad F E)) α)
add : ∀ (α β : ↥(solvableByRad F E)), P α → P β → P (α + β)
neg : ∀ (α : ↥(solvableByRad F E)), P α → P (-α)
mul : ∀ (α β : ↥(solvableByRad F E)), P α → P β → P (α * β)
inv : ∀ (α : ↥(solvableByRad F E)), P α → P α⁻¹
rad : ∀ (α : ↥(solvableByRad F E)) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
α : E
n : ℕ
hn : n ≠ 0
hα : IsSolvableByRad F (α ^ n)
α₀ : ↥(solvableByRad F E)
hα₀ : ↑α₀ = α ^ n
Pα : P α₀
⊢ P (⟨α, ⋯⟩ ^ n)

Proof state:
case inv
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
P : ↥(solvableByRad F E) → Prop
base : ∀ (α : F), P ((algebraMap F ↥(solvableByRad F E)) α)
add : ∀ (α β : ↥(solvableByRad F E)), P α → P β → P (α + β)
neg : ∀ (α : ↥(solvableByRad F E)), P α → P (-α)
mul : ∀ (α β : ↥(solvableByRad F E)), P α → P β → P (α * β)
inv : ∀ (α : ↥(solvableByRad F E)), P α → P α⁻¹
rad : ∀ (α : ↥(solvableByRad F E)) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
α : E
a✝ : IsSolvableByRad F α
Pα : ∃ β, ↑β = α ∧ P β
⊢ ∃ β, ↑β = α⁻¹ ∧ P β

Tactic:
obtain ⟨α₀, hα₀, Pα⟩ := Pα

Result:
case inv.intro.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
P : ↥(solvableByRad F E) → Prop
base : ∀ (α : F), P ((algebraMap F ↥(solvableByRad F E)) α)
add : ∀ (α β : ↥(solvableByRad F E)), P α → P β → P (α + β)
neg : ∀ (α : ↥(solvableByRad F E)), P α → P (-α)
mul : ∀ (α β : ↥(solvableByRad F E)), P α → P β → P (α * β)
inv : ∀ (α : ↥(solvableByRad F E)), P α → P α⁻¹
rad : ∀ (α : ↥(solvableByRad F E)) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
α : E
a✝ : IsSolvableByRad F α
α₀ : ↥(solvableByRad F E)
hα₀ : ↑α₀ = α
Pα : P α₀
⊢ ∃ β, ↑β = α⁻¹ ∧ P β

Proof state:
case inv.intro.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
P : ↥(solvableByRad F E) → Prop
base : ∀ (α : F), P ((algebraMap F ↥(solvableByRad F E)) α)
add : ∀ (α β : ↥(solvableByRad F E)), P α → P β → P (α + β)
neg : ∀ (α : ↥(solvableByRad F E)), P α → P (-α)
mul : ∀ (α β : ↥(solvableByRad F E)), P α → P β → P (α * β)
inv : ∀ (α : ↥(solvableByRad F E)), P α → P α⁻¹
rad : ∀ (α : ↥(solvableByRad F E)) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
α : E
a✝ : IsSolvableByRad F α
α₀ : ↥(solvableByRad F E)
hα₀ : ↑α₀ = α
Pα : P α₀
⊢ ∃ β, ↑β = α⁻¹ ∧ P β

Tactic:
exact ⟨α₀⁻¹, by rw [← hα₀]; rfl, inv α₀ Pα⟩

Result:
no goals

Proof state:
case neg
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
P : ↥(solvableByRad F E) → Prop
base : ∀ (α : F), P ((algebraMap F ↥(solvableByRad F E)) α)
add : ∀ (α β : ↥(solvableByRad F E)), P α → P β → P (α + β)
neg : ∀ (α : ↥(solvableByRad F E)), P α → P (-α)
mul : ∀ (α β : ↥(solvableByRad F E)), P α → P β → P (α * β)
inv : ∀ (α : ↥(solvableByRad F E)), P α → P α⁻¹
rad : ∀ (α : ↥(solvableByRad F E)) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
⊢ ∀ (α : E), IsSolvableByRad F α → (∃ β, ↑β = α ∧ P β) → ∃ β, ↑β = -α ∧ P β

Tactic:
intro α _ Pα

Result:
case neg
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
P : ↥(solvableByRad F E) → Prop
base : ∀ (α : F), P ((algebraMap F ↥(solvableByRad F E)) α)
add : ∀ (α β : ↥(solvableByRad F E)), P α → P β → P (α + β)
neg : ∀ (α : ↥(solvableByRad F E)), P α → P (-α)
mul : ∀ (α β : ↥(solvableByRad F E)), P α → P β → P (α * β)
inv : ∀ (α : ↥(solvableByRad F E)), P α → P α⁻¹
rad : ∀ (α : ↥(solvableByRad F E)) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
α : E
a✝ : IsSolvableByRad F α
Pα : ∃ β, ↑β = α ∧ P β
⊢ ∃ β, ↑β = -α ∧ P β

Proof state:
case rad.intro.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
P : ↥(solvableByRad F E) → Prop
base : ∀ (α : F), P ((algebraMap F ↥(solvableByRad F E)) α)
add : ∀ (α β : ↥(solvableByRad F E)), P α → P β → P (α + β)
neg : ∀ (α : ↥(solvableByRad F E)), P α → P (-α)
mul : ∀ (α β : ↥(solvableByRad F E)), P α → P β → P (α * β)
inv : ∀ (α : ↥(solvableByRad F E)), P α → P α⁻¹
rad : ∀ (α : ↥(solvableByRad F E)) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
α : E
n : ℕ
hn : n ≠ 0
hα : IsSolvableByRad F (α ^ n)
α₀ : ↥(solvableByRad F E)
hα₀ : ↑α₀ = α ^ n
Pα : P α₀
⊢ P (⟨α, ⋯⟩ ^ n)

Tactic:
convert Pα

Result:
case h.e'_1
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
P : ↥(solvableByRad F E) → Prop
base : ∀ (α : F), P ((algebraMap F ↥(solvableByRad F E)) α)
add : ∀ (α β : ↥(solvableByRad F E)), P α → P β → P (α + β)
neg : ∀ (α : ↥(solvableByRad F E)), P α → P (-α)
mul : ∀ (α β : ↥(solvableByRad F E)), P α → P β → P (α * β)
inv : ∀ (α : ↥(solvableByRad F E)), P α → P α⁻¹
rad : ∀ (α : ↥(solvableByRad F E)) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
α : E
n : ℕ
hn : n ≠ 0
hα : IsSolvableByRad F (α ^ n)
α₀ : ↥(solvableByRad F E)
hα₀ : ↑α₀ = α ^ n
Pα : P α₀
⊢ ⟨α, ⋯⟩ ^ n = α₀