-- Mathlib/Analysis/InnerProductSpace/Rayleigh.lean
theorem image_rayleigh_eq_image_rayleigh_sphere {r : ℝ} (hr : 0 < r) :
    rayleighQuotient T '' {0}ᶜ = rayleighQuotient T '' sphere 0 r

Proof state:
case h.mp.intro.intro.refine_2
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
a : ℝ
x : E
hx : x ≠ 0
hxT : T.rayleighQuotient x = a
this✝ : ‖x‖ ≠ 0
c : 𝕜 := ↑‖x‖⁻¹ * ↑r
this : c ≠ 0
⊢ T.rayleighQuotient x = a

Tactic:
exact hxT

Result:
no goals

Proof state:
case h.mp
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
a : ℝ
⊢ a ∈ T.rayleighQuotient '' {0}ᶜ → a ∈ T.rayleighQuotient '' sphere 0 r

Tactic:
rintro ⟨x, hx : x ≠ 0, hxT⟩

Result:
case h.mp.intro.intro
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
a : ℝ
x : E
hx : x ≠ 0
hxT : T.rayleighQuotient x = a
⊢ a ∈ T.rayleighQuotient '' sphere 0 r

Proof state:
case h.mpr.intro.intro
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
a : ℝ
x : E
hx : x ∈ sphere 0 r
hxT : T.rayleighQuotient x = a
⊢ a ∈ T.rayleighQuotient '' {0}ᶜ

Tactic:
exact ⟨x, ne_zero_of_mem_sphere hr.ne' ⟨x, hx⟩, hxT⟩

Result:
no goals

Proof state:
case h.mp.intro.intro
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
a : ℝ
x : E
hx : x ≠ 0
hxT : T.rayleighQuotient x = a
this✝ : ‖x‖ ≠ 0
c : 𝕜 := ↑‖x‖⁻¹ * ↑r
this : c ≠ 0
⊢ a ∈ T.rayleighQuotient '' sphere 0 r

Tactic:
refine ⟨c • x, ?_, ?_⟩

Result:
case h.mp.intro.intro.refine_1
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
a : ℝ
x : E
hx : x ≠ 0
hxT : T.rayleighQuotient x = a
this✝ : ‖x‖ ≠ 0
c : 𝕜 := ↑‖x‖⁻¹ * ↑r
this : c ≠ 0
⊢ c • x ∈ sphere 0 r

case h.mp.intro.intro.refine_2
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
a : ℝ
x : E
hx : x ≠ 0
hxT : T.rayleighQuotient x = a
this✝ : ‖x‖ ≠ 0
c : 𝕜 := ↑‖x‖⁻¹ * ↑r
this : c ≠ 0
⊢ T.rayleighQuotient (c • x) = a

Proof state:
case h.mp.intro.intro
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
a : ℝ
x : E
hx : x ≠ 0
hxT : T.rayleighQuotient x = a
this : ‖x‖ ≠ 0
⊢ a ∈ T.rayleighQuotient '' sphere 0 r

Tactic:
let c : 𝕜 := ↑‖x‖⁻¹ * r

Result:
case h.mp.intro.intro
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
a : ℝ
x : E
hx : x ≠ 0
hxT : T.rayleighQuotient x = a
this : ‖x‖ ≠ 0
c : 𝕜 := ↑‖x‖⁻¹ * ↑r
⊢ a ∈ T.rayleighQuotient '' sphere 0 r

Proof state:
case h.mp.intro.intro.refine_2
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
a : ℝ
x : E
hx : x ≠ 0
hxT : T.rayleighQuotient x = a
this✝ : ‖x‖ ≠ 0
c : 𝕜 := ↑‖x‖⁻¹ * ↑r
this : c ≠ 0
⊢ T.rayleighQuotient (c • x) = a

Tactic:
rw [T.rayleigh_smul x this]

Result:
case h.mp.intro.intro.refine_2
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
a : ℝ
x : E
hx : x ≠ 0
hxT : T.rayleighQuotient x = a
this✝ : ‖x‖ ≠ 0
c : 𝕜 := ↑‖x‖⁻¹ * ↑r
this : c ≠ 0
⊢ T.rayleighQuotient x = a

Proof state:
case h.mpr
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
a : ℝ
⊢ a ∈ T.rayleighQuotient '' sphere 0 r → a ∈ T.rayleighQuotient '' {0}ᶜ

Tactic:
rintro ⟨x, hx, hxT⟩

Result:
case h.mpr.intro.intro
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
a : ℝ
x : E
hx : x ∈ sphere 0 r
hxT : T.rayleighQuotient x = a
⊢ a ∈ T.rayleighQuotient '' {0}ᶜ

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
⊢ T.rayleighQuotient '' {0}ᶜ = T.rayleighQuotient '' sphere 0 r

Tactic:
ext a

Result:
case h
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
a : ℝ
⊢ a ∈ T.rayleighQuotient '' {0}ᶜ ↔ a ∈ T.rayleighQuotient '' sphere 0 r

Proof state:
case h.mp.intro.intro
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
a : ℝ
x : E
hx : x ≠ 0
hxT : T.rayleighQuotient x = a
this : ‖x‖ ≠ 0
c : 𝕜 := ↑‖x‖⁻¹ * ↑r
⊢ a ∈ T.rayleighQuotient '' sphere 0 r

Tactic:
have : c ≠ 0 := by simp [c, hx, hr.ne']

Result:
case h.mp.intro.intro
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
a : ℝ
x : E
hx : x ≠ 0
hxT : T.rayleighQuotient x = a
this✝ : ‖x‖ ≠ 0
c : 𝕜 := ↑‖x‖⁻¹ * ↑r
this : c ≠ 0
⊢ a ∈ T.rayleighQuotient '' sphere 0 r

Proof state:
case h.mp.intro.intro
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
a : ℝ
x : E
hx : x ≠ 0
hxT : T.rayleighQuotient x = a
⊢ a ∈ T.rayleighQuotient '' sphere 0 r

Tactic:
have : ‖x‖ ≠ 0 := by simp [hx]

Result:
case h.mp.intro.intro
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
a : ℝ
x : E
hx : x ≠ 0
hxT : T.rayleighQuotient x = a
this : ‖x‖ ≠ 0
⊢ a ∈ T.rayleighQuotient '' sphere 0 r

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
a : ℝ
x : E
hx : x ≠ 0
hxT : T.rayleighQuotient x = a
this : ‖x‖ ≠ 0
c : 𝕜 := ↑‖x‖⁻¹ * ↑r
⊢ c ≠ 0

Tactic:
simp [c, hx, hr.ne']

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
a : ℝ
x : E
hx : x ≠ 0
hxT : T.rayleighQuotient x = a
⊢ ‖x‖ ≠ 0

Tactic:
simp [hx]

Result:
no goals

Proof state:
case h
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
a : ℝ
⊢ a ∈ T.rayleighQuotient '' {0}ᶜ ↔ a ∈ T.rayleighQuotient '' sphere 0 r

Tactic:
constructor

Result:
case h.mp
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
a : ℝ
⊢ a ∈ T.rayleighQuotient '' {0}ᶜ → a ∈ T.rayleighQuotient '' sphere 0 r

case h.mpr
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
a : ℝ
⊢ a ∈ T.rayleighQuotient '' sphere 0 r → a ∈ T.rayleighQuotient '' {0}ᶜ

Proof state:
case h.mp.intro.intro.refine_1
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
a : ℝ
x : E
hx : x ≠ 0
hxT : T.rayleighQuotient x = a
this✝ : ‖x‖ ≠ 0
c : 𝕜 := ↑‖x‖⁻¹ * ↑r
this : c ≠ 0
⊢ c • x ∈ sphere 0 r

Tactic:
field_simp [c, norm_smul, abs_of_pos hr]

Result:
no goals