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

Tactic:
rw [← hα₀, ← 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 α
a✝ : IsSolvableByRad F β
α₀ : ↥(solvableByRad F E)
hα₀ : ↑α₀ = α
Pα : P α₀
β₀ : ↥(solvableByRad F E)
hβ₀ : ↑β₀ = β
Pβ : P β₀
⊢ ↑(α₀ * β₀) = ↑α₀ * ↑β₀

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
a✝ : IsSolvableByRad F α
Pα : ∃ β, ↑β = α ∧ P β
⊢ ∃ β, ↑β = -α ∧ P β

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

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

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

Tactic:
rw [← hα₀, ← 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 α
a✝ : IsSolvableByRad F β
α₀ : ↥(solvableByRad F E)
hα₀ : ↑α₀ = α
Pα : P α₀
β₀ : ↥(solvableByRad F E)
hβ₀ : ↑β₀ = β
Pβ : 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
a✝¹ : IsSolvableByRad F α
a✝ : IsSolvableByRad F β
Pα : ∃ β, ↑β = α ∧ P β
Pβ : ∃ β_1, ↑β_1 = β ∧ P β_1
⊢ ∃ β_1, ↑β_1 = α + β ∧ P β_1

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

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

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