-- Mathlib/Analysis/InnerProductSpace/Rayleigh.lean
theorem eq_smul_self_of_isLocalExtrOn_real (hT : IsSelfAdjoint T) {x₀ : F}
    (hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere (0 : F) ‖x₀‖) x₀) :
    T x₀ = T.rayleighQuotient x₀ • x₀

Proof state:
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
T : F →L[ℝ] F
hT : IsSelfAdjoint T
x₀ : F
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
a b : ℝ
h₁ : (a, b) ≠ 0
h₂ : a • x₀ + b • T x₀ = 0
hx₀ : ¬x₀ = 0
hb : ¬b = 0
c : ℝ := -b⁻¹ * a
⊢ b * (b⁻¹ * a) = a

Tactic:
field_simp [mul_comm]

Result:
no goals

Proof state:
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
T : F →L[ℝ] F
hT : IsSelfAdjoint T
x₀ : F
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
⊢ T x₀ = T.rayleighQuotient x₀ • x₀

Tactic:
obtain ⟨a, b, h₁, h₂⟩ := hT.linearly_dependent_of_isLocalExtrOn hextr

Result:
case intro.intro.intro
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
T : F →L[ℝ] F
hT : IsSelfAdjoint T
x₀ : F
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
a b : ℝ
h₁ : (a, b) ≠ 0
h₂ : a • x₀ + b • T x₀ = 0
⊢ T x₀ = T.rayleighQuotient x₀ • x₀

Proof state:
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
T : F →L[ℝ] F
hT : IsSelfAdjoint T
x₀ : F
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
a b : ℝ
h₁ : (a, b) ≠ 0
h₂ : a • x₀ + b • T x₀ = 0
hx₀ : ¬x₀ = 0
hb : ¬b = 0
c : ℝ := -b⁻¹ * a
this : b * (b⁻¹ * a) = a
⊢ T x₀ = c • x₀

Tactic:
apply smul_right_injective F hb

Result:
case a
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
T : F →L[ℝ] F
hT : IsSelfAdjoint T
x₀ : F
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
a b : ℝ
h₁ : (a, b) ≠ 0
h₂ : a • x₀ + b • T x₀ = 0
hx₀ : ¬x₀ = 0
hb : ¬b = 0
c : ℝ := -b⁻¹ * a
this : b * (b⁻¹ * a) = a
⊢ (fun x => b • x) (T x₀) = (fun x => b • x) (c • x₀)

Proof state:
case h.e'_3.h.e'_5
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
T : F →L[ℝ] F
hT : IsSelfAdjoint T
x₀ : F
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
a b : ℝ
h₁ : (a, b) ≠ 0
h₂ : a • x₀ + b • T x₀ = 0
hx₀ : ¬x₀ = 0
hb : ¬b = 0
c : ℝ := -b⁻¹ * a
hc : T x₀ = c • x₀
this : ⟪T x₀, x₀⟫_ℝ = c * (‖x₀‖ * ‖x₀‖)
⊢ T.reApplyInnerSelf x₀ = c * (‖x₀‖ * ‖x₀‖)

Tactic:
exact this

Result:
no goals

Proof state:
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
T : F →L[ℝ] F
hT : IsSelfAdjoint T
x₀ : F
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
a b : ℝ
h₁ : (a, b) ≠ 0
h₂ : a • x₀ + b • T x₀ = 0
hx₀ : ¬x₀ = 0
hb : b = 0
⊢ a ≠ 0

Tactic:
simpa [hb] using h₁

Result:
no goals

Proof state:
case pos
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
T : F →L[ℝ] F
hT : IsSelfAdjoint T
x₀ : F
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
a b : ℝ
h₁ : (a, b) ≠ 0
h₂ : a • x₀ + b • T x₀ = 0
hx₀ : ¬x₀ = 0
hb : b = 0
this : a ≠ 0
⊢ T x₀ = T.rayleighQuotient x₀ • x₀

Tactic:
refine absurd ?_ hx₀

Result:
case pos
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
T : F →L[ℝ] F
hT : IsSelfAdjoint T
x₀ : F
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
a b : ℝ
h₁ : (a, b) ≠ 0
h₂ : a • x₀ + b • T x₀ = 0
hx₀ : ¬x₀ = 0
hb : b = 0
this : a ≠ 0
⊢ x₀ = 0

Proof state:
case neg
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
T : F →L[ℝ] F
hT : IsSelfAdjoint T
x₀ : F
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
a b : ℝ
h₁ : (a, b) ≠ 0
h₂ : a • x₀ + b • T x₀ = 0
hx₀ : ¬x₀ = 0
hb : ¬b = 0
c : ℝ := -b⁻¹ * a
hc : T x₀ = c • x₀
⊢ T x₀ = T.rayleighQuotient x₀ • x₀

Tactic:
convert hc

Result:
case h.e'_3.h.e'_5
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
T : F →L[ℝ] F
hT : IsSelfAdjoint T
x₀ : F
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
a b : ℝ
h₁ : (a, b) ≠ 0
h₂ : a • x₀ + b • T x₀ = 0
hx₀ : ¬x₀ = 0
hb : ¬b = 0
c : ℝ := -b⁻¹ * a
hc : T x₀ = c • x₀
⊢ T.rayleighQuotient x₀ = c

Proof state:
case neg
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
T : F →L[ℝ] F
hT : IsSelfAdjoint T
x₀ : F
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
a b : ℝ
h₁ : (a, b) ≠ 0
h₂ : a • x₀ + b • T x₀ = 0
hx₀ : ¬x₀ = 0
hb : ¬b = 0
c : ℝ := -b⁻¹ * a
⊢ T x₀ = T.rayleighQuotient x₀ • x₀

Tactic:
have hc : T x₀ = c • x₀ := by
  have : b * (b⁻¹ * a) = a := by field_simp [mul_comm]
  apply smul_right_injective F hb
  simp [c, eq_neg_of_add_eq_zero_left h₂, ← mul_smul, this]

Result:
case neg
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
T : F →L[ℝ] F
hT : IsSelfAdjoint T
x₀ : F
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
a b : ℝ
h₁ : (a, b) ≠ 0
h₂ : a • x₀ + b • T x₀ = 0
hx₀ : ¬x₀ = 0
hb : ¬b = 0
c : ℝ := -b⁻¹ * a
hc : T x₀ = c • x₀
⊢ T x₀ = T.rayleighQuotient x₀ • x₀

Proof state:
case h.e'_3.h.e'_5
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
T : F →L[ℝ] F
hT : IsSelfAdjoint T
x₀ : F
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
a b : ℝ
h₁ : (a, b) ≠ 0
h₂ : a • x₀ + b • T x₀ = 0
hx₀ : ¬x₀ = 0
hb : ¬b = 0
c : ℝ := -b⁻¹ * a
hc : T x₀ = c • x₀
⊢ T.rayleighQuotient x₀ = c

Tactic:
have := congr_arg (fun x => ⟪x, x₀⟫_ℝ) hc

Result:
case h.e'_3.h.e'_5
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
T : F →L[ℝ] F
hT : IsSelfAdjoint T
x₀ : F
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
a b : ℝ
h₁ : (a, b) ≠ 0
h₂ : a • x₀ + b • T x₀ = 0
hx₀ : ¬x₀ = 0
hb : ¬b = 0
c : ℝ := -b⁻¹ * a
hc : T x₀ = c • x₀
this : (fun x => ⟪x, x₀⟫_ℝ) (T x₀) = (fun x => ⟪x, x₀⟫_ℝ) (c • x₀)
⊢ T.rayleighQuotient x₀ = c

Proof state:
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
T : F →L[ℝ] F
hT : IsSelfAdjoint T
x₀ : F
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
a b : ℝ
h₁ : (a, b) ≠ 0
h₂ : a • x₀ + b • T x₀ = 0
hx₀ : ¬x₀ = 0
hb : ¬b = 0
c : ℝ := -b⁻¹ * a
⊢ T x₀ = c • x₀

Tactic:
have : b * (b⁻¹ * a) = a := by field_simp [mul_comm]

Result:
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
T : F →L[ℝ] F
hT : IsSelfAdjoint T
x₀ : F
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
a b : ℝ
h₁ : (a, b) ≠ 0
h₂ : a • x₀ + b • T x₀ = 0
hx₀ : ¬x₀ = 0
hb : ¬b = 0
c : ℝ := -b⁻¹ * a
this : b * (b⁻¹ * a) = a
⊢ T x₀ = c • x₀

Proof state:
case pos.a
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
T : F →L[ℝ] F
hT : IsSelfAdjoint T
x₀ : F
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
a b : ℝ
h₁ : (a, b) ≠ 0
h₂ : a • x₀ + b • T x₀ = 0
hx₀ : ¬x₀ = 0
hb : b = 0
this : a ≠ 0
⊢ (fun x => a • x) x₀ = (fun x => a • x) 0

Tactic:
simpa [hb] using h₂

Result:
no goals

Proof state:
case pos
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
T : F →L[ℝ] F
hT : IsSelfAdjoint T
x₀ : F
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
a b : ℝ
h₁ : (a, b) ≠ 0
h₂ : a • x₀ + b • T x₀ = 0
hx₀ : x₀ = 0
⊢ T x₀ = T.rayleighQuotient x₀ • x₀

Tactic:
simp [hx₀]

Result:
no goals