-- 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:
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 α
this : ∀ (α : E), IsSolvableByRad F α → ∃ β, ↑β = α ∧ P β
⊢ ∀ (α : ↥(solvableByRad F E)), P α

Tactic:
intro α

Result:
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 α
this : ∀ (α : E), IsSolvableByRad F α → ∃ β, ↑β = α ∧ P β
α : ↥(solvableByRad F E)
⊢ P α

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), IsSolvableByRad F α → (∃ β, ↑β = α ∧ P β) → ∃ β, ↑β = α⁻¹ ∧ P β

Tactic:
intro α _ Pα

Result:
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 β

Proof state:
case add.intro.intro.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 α
a✝ : IsSolvableByRad F β
α₀ : ↥(solvableByRad F E)
hα₀ : ↑α₀ = α
Pα : P α₀
β₀ : ↥(solvableByRad F E)
hβ₀ : ↑β₀ = β
Pβ : P β₀
⊢ ∃ β_1, ↑β_1 = α + β ∧ P β_1

Tactic:
exact ⟨α₀ + β₀, by rw [← hα₀, ← hβ₀]; rfl, add α₀ β₀ Pα Pβ⟩

Result:
no goals

Proof state:
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 α₀
⊢ ↑(-α₀) = -↑α₀

Tactic:
rfl

Result:
no goals

Proof state:
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 α₀
⊢ ↑(-α₀) = -α

Tactic:
rw [← hα₀]

Result:
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 α₀
⊢ ↑(-α₀) = -↑α₀

Proof state:
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 β
α₀ : ↥(solvableByRad F E)
hα₀ : ↑α₀ = α
Pα : P α₀
β₀ : ↥(solvableByRad F E)
hβ₀ : ↑β₀ = β
Pβ : P β₀
⊢ ↑(α₀ * β₀) = ↑α₀ * ↑β₀

Tactic:
rfl

Result:
no goals

Proof state:
case neg.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, neg α₀ Pα⟩

Result:
no goals

Proof state:
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 β
α₀ : ↥(solvableByRad F E)
hα₀ : ↑α₀ = α
Pα : P α₀
β₀ : ↥(solvableByRad F E)
hβ₀ : ↑β₀ = β
Pβ : P β₀
⊢ ↑(α₀ + β₀) = ↑α₀ + ↑β₀

Tactic:
rfl

Result:
no goals