awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : 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₀ + HSMul.hSMul (β := F) b ((T : (a : F) → F) x₀ : F) = 0
hx₀ : ¬x₀ = 0
hb : b = 0
this : a ≠ 0
⊢ (T : (a : F) → F) x₀ = T.rayleighQuotient x₀ • x₀

Tactic:
absurd ?_ hx₀

Premises used: absurd
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : 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₀ + HSMul.hSMul (β := F) b ((T : (a : F) → F) x₀ : F) = 0
hx₀ : ¬x₀ = 0
hb : b = 0
this : a ≠ 0
pos : x₀ = 0
⊢ (T : (a : F) → F) x₀ = T.rayleighQuotient x₀ • x₀

Tactic:
refine absurd ?_ hx₀

Premises used: absurd
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : 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₀ + HSMul.hSMul (β := F) b ((T : (a : F) → F) x₀ : F) = 0
hx₀ : ¬x₀ = 0
hb : b = 0
this : a ≠ 0
pos : Eq.{u_3 + 1} (α := F) ((fun (x : F) ↦ a • x) x₀) ((fun (x : F) ↦ a • x) 0)
⊢ x₀ = 0

Tactic:
apply smul_right_injective F this

Premises used: smul_right_injective
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : 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₀ + HSMul.hSMul (β := F) b ((T : (a : F) → F) x₀ : F) = 0
hx₀ : ¬x₀ = 0
hb : b = 0
this : a ≠ 0
⊢ Eq.{u_3 + 1} (α := F) ((fun (x : F) ↦ a • x) x₀) ((fun (x : F) ↦ a • x) 0)

Tactic:
simpa [hb] using h₂
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : 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₀ + HSMul.hSMul (β := F) b ((T : (a : F) → F) x₀ : F) = 0
hx₀ : ¬x₀ = 0
hb : ¬b = 0
match_scalars : 1 - b⁻¹ * (b * 1) = 0
match_scalars₁ : -(-b⁻¹ * a * 1 + b⁻¹ * (a * 1)) = 0
⊢ HAdd.hAdd (α := F) ((T : (a : F) → F) x₀ : F) (HSMul.hSMul (β := F) b⁻¹ 0) -
      ((-b⁻¹ * a) • x₀ + b⁻¹ • (a • x₀ + HSMul.hSMul (β := F) b ((T : (a : F) → F) x₀ : F))) =
    0

Tactic:
match_scalars
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : 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₀ + HSMul.hSMul (β := F) b ((T : (a : F) → F) x₀ : F) = 0
hx₀ : ¬x₀ = 0
hb : ¬b = 0
⊢ 1 - b⁻¹ * (b * 1) = 0

Tactic:
field
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : 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₀ + HSMul.hSMul (β := F) b ((T : (a : F) → F) x₀ : F) = 0
hx₀ : ¬x₀ = 0
hb : ¬b = 0
⊢ -(-b⁻¹ * a * 1 + b⁻¹ * (a * 1)) = 0

Tactic:
field
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : 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₀ + HSMul.hSMul (β := F) b ((T : (a : F) → F) x₀ : F) = 0
hx₀ : ¬x₀ = 0
hb : ¬b = 0
a₁ :
  HAdd.hAdd (α := F) ((T : (a : F) → F) x₀ : F) (HSMul.hSMul (β := F) b⁻¹ 0) -
      ((-b⁻¹ * a) • x₀ + b⁻¹ • (a • x₀ + HSMul.hSMul (β := F) b ((T : (a : F) → F) x₀ : F))) =
    0
⊢ (T : (a : F) → F) x₀ = (-b⁻¹ * a) • x₀

Tactic:
linear_combination (norm := match_scalars <;> field) b⁻¹ • h₂
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : 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₀ + HSMul.hSMul (β := F) b ((T : (a : F) → F) x₀ : F) = 0
hx₀ : ¬x₀ = 0
hb : ¬b = 0
⊢ (T : (a : F) → F) x₀ = (-b⁻¹ * a) • x₀

Tactic:
have hc : T x₀ = (-b⁻¹ * a) • x₀ := by
    linear_combination (norm := match_scalars <;> field) b⁻¹ • h₂
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : 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₀ + HSMul.hSMul (β := F) b ((T : (a : F) → F) x₀ : F) = 0
hx₀ : ¬x₀ = 0
hb : ¬b = 0
hc : (T : (a : F) → F) x₀ = (-b⁻¹ * a) • x₀
⊢ let c := -b⁻¹ * a;
  (T : (a : F) → F) x₀ = c • x₀

Tactic:
set c : ℝ := -b⁻¹ * a
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : 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₀ + HSMul.hSMul (β := F) b ((T : (a : F) → F) x₀ : F) = 0
hx₀ : ¬x₀ = 0
hb : ¬b = 0
c : ℝ := -b⁻¹ * a
hc : (T : (a : F) → F) x₀ = c • x₀
⊢ (T : (a : F) → F) x₀ = c • x₀

Tactic:
hc
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : 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₀ + HSMul.hSMul (β := F) b ((T : (a : F) → F) x₀ : F) = 0
hx₀ : ¬x₀ = 0
hb : ¬b = 0
c : ℝ := -b⁻¹ * a
hc : (T : (a : F) → F) x₀ = c • x₀
h : T.rayleighQuotient x₀ = c
⊢ (T : (a : F) → F) x₀ = T.rayleighQuotient x₀ • x₀

Tactic:
convert! hc
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : 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₀ + HSMul.hSMul (β := F) b ((T : (a : F) → F) x₀ : F) = 0
hx₀ : ¬x₀ = 0
hb : ¬b = 0
c : ℝ := -b⁻¹ * a
hc : (T : (a : F) → F) x₀ = c • x₀
⊢ T.rayleighQuotient x₀ = c

Tactic:
simpa [field, inner_smul_left, mul_comm a] using congr_arg (fun x => ⟪x, x₀⟫_ℝ) hc

Premises used: Real, Inner.inner, congr_arg, mul_comm, inner_smul_left
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
this : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
hSA : Membership.mem (γ := AddSubgroup (E →L[ℝ] E)) (selfAdjoint (E →L[ℝ] E)) (↑⋯.toSelfAdjoint : E →L[ℝ] E) := ⋯
⊢ (T : (a : E) → E) x₀ = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(T.rayleighQuotient x₀) : 𝕜) x₀

Tactic:
hSA.eq_smul_self_of_isLocalExtrOn_real hextr

Premises used: IsSelfAdjoint.eq_smul_self_of_isLocalExtrOn_real, ContinuousLinearMap.reApplyInnerSelf
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
this : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
hSA : Membership.mem (γ := AddSubgroup (E →L[ℝ] E)) (selfAdjoint (E →L[ℝ] E)) (↑⋯.toSelfAdjoint : E →L[ℝ] E) := ⋯
⊢ (T : (a : E) → E) x₀ = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(T.rayleighQuotient x₀) : 𝕜) x₀

Tactic:
exact hSA.eq_smul_self_of_isLocalExtrOn_real hextr

Premises used: IsSelfAdjoint.eq_smul_self_of_isLocalExtrOn_real
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
⊢ HasEigenvector (↑T : E →ₗ[𝕜] E) (↑(T.rayleighQuotient x₀) : 𝕜) x₀

Tactic:
⟨?_, hx₀⟩

Premises used: Module.End.HasUnifEigenvector, And.intro
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
refine :
  Membership.mem (γ := Submodule 𝕜 E)
    ((genEigenspace (↑T : E →ₗ[𝕜] E) (↑(T.rayleighQuotient x₀) : 𝕜) : (a : ℕ∞) → Submodule 𝕜 E) 1 : Submodule 𝕜 E) x₀
⊢ HasEigenvector (↑T : E →ₗ[𝕜] E) (↑(T.rayleighQuotient x₀) : 𝕜) x₀

Tactic:
refine ⟨?_, hx₀⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
rw : ((↑T : E →ₗ[𝕜] E) : (a : E) → E) x₀ = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(T.rayleighQuotient x₀) : 𝕜) x₀
⊢ Membership.mem (γ := Submodule 𝕜 E)
    ((genEigenspace (↑T : E →ₗ[𝕜] E) (↑(T.rayleighQuotient x₀) : 𝕜) : (a : ℕ∞) → Submodule 𝕜 E) 1 : Submodule 𝕜 E) x₀

Tactic:
rw [Module.End.mem_eigenspace_iff]

Premises used: Module.End.mem_eigenspace_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
⊢ ((↑T : E →ₗ[𝕜] E) : (a : E) → E) x₀ = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(T.rayleighQuotient x₀) : 𝕜) x₀

Tactic:
hT.eq_smul_self_of_isLocalExtrOn hextr

Premises used: IsSelfAdjoint.eq_smul_self_of_isLocalExtrOn
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
⊢ ((↑T : E →ₗ[𝕜] E) : (a : E) → E) x₀ = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(T.rayleighQuotient x₀) : 𝕜) x₀

Tactic:
exact hT.eq_smul_self_of_isLocalExtrOn hextr

Premises used: IsSelfAdjoint.eq_smul_self_of_isLocalExtrOn
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMaxOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
⊢ HasEigenvector (↑T : E →ₗ[𝕜] E) (↑(T.rayleighQuotient x₀) : 𝕜) x₀

Tactic:
hT.hasEigenvector_of_isLocalExtrOn hx₀ (Or.inr hextr.localize)

Premises used: IsMaxOn.localize, IsSelfAdjoint.hasEigenvector_of_isLocalExtrOn, Or.inr
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMaxOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
h : ⨆ (x : { x : E // x ≠ 0 }), T.rayleighQuotient (↑x : E) = T.rayleighQuotient x₀
⊢ HasEigenvector (↑T : E →ₗ[𝕜] E) (↑(⨆ (x : { x : E // x ≠ 0 }), T.rayleighQuotient (↑x : E)) : 𝕜) x₀

Tactic:
convert! hT.hasEigenvector_of_isLocalExtrOn hx₀ (Or.inr hextr.localize)

Premises used: IsMaxOn.localize, IsSelfAdjoint.hasEigenvector_of_isLocalExtrOn, Or.inr
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMaxOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
⊢ 0 < ‖x₀‖

Tactic:
simp [hx₀]
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMaxOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
⊢ 0 < ‖x₀‖

Tactic:
have hx₀' : 0 < ‖x₀‖ := by simp [hx₀]
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMaxOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀' : 0 < ‖x₀‖
⊢ Membership.mem (γ := Set E) (sphere 0 ‖x₀‖) x₀

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMaxOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀' : 0 < ‖x₀‖
⊢ Membership.mem (γ := Set E) (sphere 0 ‖x₀‖) x₀

Tactic:
have hx₀'' : x₀ ∈ sphere (0 : E) ‖x₀‖ := by simp
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMaxOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀' : 0 < ‖x₀‖
hx₀'' : Membership.mem (γ := Set E) (sphere 0 ‖x₀‖) x₀
h : ⨆ (x : (↑(sphere 0 ‖x₀‖) : Type u_2)), T.rayleighQuotient (↑x : E) = T.rayleighQuotient x₀
⊢ ⨆ (x : { x : E // x ≠ 0 }), T.rayleighQuotient (↑x : E) = T.rayleighQuotient x₀

Tactic:
rw [T.iSup_rayleigh_eq_iSup_rayleigh_sphere hx₀']

Premises used: ContinuousLinearMap.iSup_rayleigh_eq_iSup_rayleigh_sphere
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMaxOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀' : 0 < ‖x₀‖
hx₀'' : Membership.mem (γ := Set E) (sphere 0 ‖x₀‖) x₀
⊢ ⨆ (x : (↑(sphere 0 ‖x₀‖) : Type u_2)), T.rayleighQuotient (↑x : E) = T.rayleighQuotient x₀

Tactic:
IsMaxOn.iSup_eq hx₀'' ?_

Premises used: IsMaxOn.iSup_eq
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMaxOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀' : 0 < ‖x₀‖
hx₀'' : Membership.mem (γ := Set E) (sphere 0 ‖x₀‖) x₀
h : IsMaxOn T.rayleighQuotient (sphere 0 ‖x₀‖) x₀
⊢ ⨆ (x : (↑(sphere 0 ‖x₀‖) : Type u_2)), T.rayleighQuotient (↑x : E) = T.rayleighQuotient x₀

Tactic:
refine IsMaxOn.iSup_eq hx₀'' ?_

Premises used: IsMaxOn.iSup_eq
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMaxOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀' : 0 < ‖x₀‖
hx₀'' : Membership.mem (γ := Set E) (sphere 0 ‖x₀‖) x₀
x : E
hx : Membership.mem (γ := Set E) (sphere 0 ‖x₀‖) x
⊢ ‖x‖ = ‖x₀‖

Tactic:
simpa using hx
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMaxOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀' : 0 < ‖x₀‖
hx₀'' : Membership.mem (γ := Set E) (sphere 0 ‖x₀‖) x₀
x : E
hx : Membership.mem (γ := Set E) (sphere 0 ‖x₀‖) x
⊢ ‖x‖ = ‖x₀‖

Tactic:
have : ‖x‖ = ‖x₀‖ := by simpa using hx
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMaxOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀' : 0 < ‖x₀‖
hx₀'' : Membership.mem (γ := Set E) (sphere 0 ‖x₀‖) x₀
x : E
hx : Membership.mem (γ := Set E) (sphere 0 ‖x₀‖) x
this : ‖x‖ = ‖x₀‖
h : T.reApplyInnerSelf x / HPow.hPow (β := ℕ) ‖x₀‖ 2 ≤ T.reApplyInnerSelf x₀ / HPow.hPow (β := ℕ) ‖x₀‖ 2
⊢ T.reApplyInnerSelf x / HPow.hPow (β := ℕ) ‖x‖ 2 ≤ T.reApplyInnerSelf x₀ / HPow.hPow (β := ℕ) ‖x₀‖ 2

Tactic:
rw [this]
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMaxOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀' : 0 < ‖x₀‖
hx₀'' : Membership.mem (γ := Set E) (sphere 0 ‖x₀‖) x₀
x : E
hx : Membership.mem (γ := Set E) (sphere 0 ‖x₀‖) x
this : ‖x‖ = ‖x₀‖
h : T.reApplyInnerSelf x ≤ T.reApplyInnerSelf x₀
⊢ T.reApplyInnerSelf x / HPow.hPow (β := ℕ) ‖x₀‖ 2 ≤ T.reApplyInnerSelf x₀ / HPow.hPow (β := ℕ) ‖x₀‖ 2

Tactic:
gcongr
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMaxOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀' : 0 < ‖x₀‖
hx₀'' : Membership.mem (γ := Set E) (sphere 0 ‖x₀‖) x₀
x : E
hx : Membership.mem (γ := Set E) (sphere 0 ‖x₀‖) x
this : ‖x‖ = ‖x₀‖
⊢ T.reApplyInnerSelf x ≤ T.reApplyInnerSelf x₀

Tactic:
hextr hx

Premises used: Set.Mem
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMaxOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀' : 0 < ‖x₀‖
hx₀'' : Membership.mem (γ := Set E) (sphere 0 ‖x₀‖) x₀
x : E
hx : Membership.mem (γ := Set E) (sphere 0 ‖x₀‖) x
this : ‖x‖ = ‖x₀‖
⊢ T.reApplyInnerSelf x ≤ T.reApplyInnerSelf x₀

Tactic:
exact hextr hx
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMinOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
⊢ HasEigenvector (↑T : E →ₗ[𝕜] E) (↑(T.rayleighQuotient x₀) : 𝕜) x₀

Tactic:
hT.hasEigenvector_of_isLocalExtrOn hx₀ (Or.inl hextr.localize)

Premises used: IsSelfAdjoint.hasEigenvector_of_isLocalExtrOn, Or.inl, IsMinOn.localize
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMinOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
h : ⨅ (x : { x : E // x ≠ 0 }), T.rayleighQuotient (↑x : E) = T.rayleighQuotient x₀
⊢ HasEigenvector (↑T : E →ₗ[𝕜] E) (↑(⨅ (x : { x : E // x ≠ 0 }), T.rayleighQuotient (↑x : E)) : 𝕜) x₀

Tactic:
convert! hT.hasEigenvector_of_isLocalExtrOn hx₀ (Or.inl hextr.localize)

Premises used: IsSelfAdjoint.hasEigenvector_of_isLocalExtrOn, Or.inl, IsMinOn.localize
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMinOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
⊢ 0 < ‖x₀‖

Tactic:
simp [hx₀]
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMinOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
⊢ 0 < ‖x₀‖

Tactic:
have hx₀' : 0 < ‖x₀‖ := by simp [hx₀]
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMinOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀' : 0 < ‖x₀‖
⊢ Membership.mem (γ := Set E) (sphere 0 ‖x₀‖) x₀

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMinOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀' : 0 < ‖x₀‖
⊢ Membership.mem (γ := Set E) (sphere 0 ‖x₀‖) x₀

Tactic:
have hx₀'' : x₀ ∈ sphere (0 : E) ‖x₀‖ := by simp
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMinOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀' : 0 < ‖x₀‖
hx₀'' : Membership.mem (γ := Set E) (sphere 0 ‖x₀‖) x₀
h : ⨅ (x : (↑(sphere 0 ‖x₀‖) : Type u_2)), T.rayleighQuotient (↑x : E) = T.rayleighQuotient x₀
⊢ ⨅ (x : { x : E // x ≠ 0 }), T.rayleighQuotient (↑x : E) = T.rayleighQuotient x₀

Tactic:
rw [T.iInf_rayleigh_eq_iInf_rayleigh_sphere hx₀']

Premises used: ContinuousLinearMap.iInf_rayleigh_eq_iInf_rayleigh_sphere
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMinOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀' : 0 < ‖x₀‖
hx₀'' : Membership.mem (γ := Set E) (sphere 0 ‖x₀‖) x₀
⊢ ⨅ (x : (↑(sphere 0 ‖x₀‖) : Type u_2)), T.rayleighQuotient (↑x : E) = T.rayleighQuotient x₀

Tactic:
IsMinOn.iInf_eq hx₀'' ?_

Premises used: IsMinOn.iInf_eq
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMinOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀' : 0 < ‖x₀‖
hx₀'' : Membership.mem (γ := Set E) (sphere 0 ‖x₀‖) x₀
h : IsMinOn T.rayleighQuotient (sphere 0 ‖x₀‖) x₀
⊢ ⨅ (x : (↑(sphere 0 ‖x₀‖) : Type u_2)), T.rayleighQuotient (↑x : E) = T.rayleighQuotient x₀

Tactic:
refine IsMinOn.iInf_eq hx₀'' ?_

Premises used: IsMinOn.iInf_eq
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMinOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀' : 0 < ‖x₀‖
hx₀'' : Membership.mem (γ := Set E) (sphere 0 ‖x₀‖) x₀
x : E
hx : Membership.mem (γ := Set E) (sphere 0 ‖x₀‖) x
⊢ ‖x‖ = ‖x₀‖

Tactic:
simpa using hx
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMinOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀' : 0 < ‖x₀‖
hx₀'' : Membership.mem (γ := Set E) (sphere 0 ‖x₀‖) x₀
x : E
hx : Membership.mem (γ := Set E) (sphere 0 ‖x₀‖) x
⊢ ‖x‖ = ‖x₀‖

Tactic:
have : ‖x‖ = ‖x₀‖ := by simpa using hx