awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst_3 : CompleteSpace E
hT : IsSelfAdjoint T
h : Nontrivial E
apply : (↑‖T‖₊ : ENNReal) ≤ spectralRadius 𝕜 T
⊢ spectralRadius 𝕜 T = (↑‖T‖₊ : ENNReal)

Tactic:
apply le_antisymm (spectrum.spectralRadius_le_nnnorm T)

Premises used: le_antisymm, spectrum.spectralRadius_le_nnnorm
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst_3 : CompleteSpace E
hT : IsSelfAdjoint T
h_1 : Nontrivial E
h :
  Membership.mem (α := 𝕜) (spectrum 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜) ∨
    Membership.mem (α := 𝕜) (spectrum 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) (-‖T‖) : 𝕜)
inl :
  ∀ (h : Membership.mem (α := 𝕜) (spectrum 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜)),
    (↑‖T‖₊ : ENNReal) ≤ spectralRadius 𝕜 T
inr :
  ∀ (h : Membership.mem (α := 𝕜) (spectrum 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) (-‖T‖) : 𝕜)),
    (↑‖T‖₊ : ENNReal) ≤ spectralRadius 𝕜 T
⊢ (↑‖T‖₊ : ENNReal) ≤ spectralRadius 𝕜 T

Tactic:
rcases h with h | h
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst_3 : CompleteSpace E
hT : IsSelfAdjoint T
h_1 : Nontrivial E
h : Membership.mem (α := 𝕜) (spectrum 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜)
⊢ (↑‖T‖₊ : ENNReal) ≤ (↑(nnnorm (E := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜)) : ENNReal)

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
T : E →L[𝕜] E
inst_3 : CompleteSpace E
hT : IsSelfAdjoint T
h_1 : Nontrivial E
h : Membership.mem (α := 𝕜) (spectrum 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜)
⊢ (↑‖T‖₊ : ENNReal) ≤ spectralRadius 𝕜 T

Tactic:
exact le_trans (by simp) (le_biSup _ h)

Premises used: le_biSup, le_trans
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst_3 : CompleteSpace E
hT : IsSelfAdjoint T
h_1 : Nontrivial E
h : Membership.mem (α := 𝕜) (spectrum 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) (-‖T‖) : 𝕜)
⊢ (↑‖T‖₊ : ENNReal) ≤ (↑(nnnorm (E := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) (-‖T‖) : 𝕜)) : ENNReal)

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
T : E →L[𝕜] E
inst_3 : CompleteSpace E
hT : IsSelfAdjoint T
h_1 : Nontrivial E
h : Membership.mem (α := 𝕜) (spectrum 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) (-‖T‖) : 𝕜)
⊢ (↑‖T‖₊ : ENNReal) ≤ spectralRadius 𝕜 T

Tactic:
exact le_trans (by simp) (le_biSup _ h)

Premises used: le_biSup, le_trans
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst_3 : CompleteSpace E
hT : IsSelfAdjoint T
h : Nontrivial E
suffices :
  Membership.mem (α := 𝕜) (spectrum 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜) ∨
    Membership.mem (α := 𝕜) (spectrum 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) (-‖T‖) : 𝕜)
⊢ (↑‖T‖₊ : ENNReal) ≤ spectralRadius 𝕜 T

Tactic:
suffices h : algebraMap ℝ 𝕜 ‖T‖ ∈ spectrum 𝕜 T ∨ algebraMap ℝ 𝕜 (-‖T‖) ∈ spectrum 𝕜 T by
    rcases h with h | h <;> exact le_trans (by simp) (le_biSup _ h)
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst_3 : CompleteSpace E
hT : IsSelfAdjoint T
h : Nontrivial E
simp_rw :
  ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜) ∉ resolventSet 𝕜 T ∨
    (-(algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜) ∉ resolventSet 𝕜 T
⊢ Membership.mem (α := 𝕜) (spectrum 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜) ∨
    Membership.mem (α := 𝕜) (spectrum 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) (-‖T‖) : 𝕜)

Tactic:
simp_rw [spectrum, Set.mem_compl_iff, map_neg]

Premises used: spectrum, map_neg, Set.mem_compl_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst_3 : CompleteSpace E
hT : IsSelfAdjoint T
h : Nontrivial E
by_contra! :
  ∀
    (h :
      Membership.mem (α := 𝕜) (resolventSet 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜) ∧
        Membership.mem (α := 𝕜) (resolventSet 𝕜 T) (-(algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜)),
    False
⊢ ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜) ∉ resolventSet 𝕜 T ∨
    (-(algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜) ∉ resolventSet 𝕜 T

Tactic:
by_contra! h
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst_3 : CompleteSpace E
hT : IsSelfAdjoint T
h_1 : Nontrivial E
h :
  Membership.mem (α := 𝕜) (resolventSet 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜) ∧
    Membership.mem (α := 𝕜) (resolventSet 𝕜 T) (-(algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜)
obtain : ∀ (c : ℝ) (hc0 : c > 0) (hc : ∀ (x : E), |T.rayleighQuotient x| ≤ ‖T‖ - c), False
⊢ False

Tactic:
obtain ⟨c, hc0, hc⟩ := T.abs_rayleighQuotient_le_of_norm_mem_resolventSet h.1 h.2

Premises used: And.right, And.left, ContinuousLinearMap.abs_rayleighQuotient_le_of_norm_mem_resolventSet
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst_3 : CompleteSpace E
hT : IsSelfAdjoint T
h_1 : Nontrivial E
h :
  Membership.mem (α := 𝕜) (resolventSet 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜) ∧
    Membership.mem (α := 𝕜) (resolventSet 𝕜 T) (-(algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜)
c : ℝ
hc0 : c > 0
hc : ∀ (x : E), |T.rayleighQuotient x| ≤ ‖T‖ - c
⊢ False

Tactic:
grind [ciSup_le hc, norm_eq_iSup_rayleighQuotient T hT.isSymmetric]

Premises used: IsSelfAdjoint.isSymmetric, ContinuousLinearMap.norm_eq_iSup_rayleighQuotient, ciSup_le
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
T : F →L[ℝ] F
hT : LinearMap.IsSymmetric.{0, u_3} (𝕜 := ℝ) (E := F) (↑T : F →ₗ[ℝ] F)
x₀ : F
⊢ HasStrictFDerivAt (fun (t : F) ↦ ⟪(T : (a : F) → F) t, id t⟫_ℝ)
    (fderivInnerCLM ℝ ((T : (a : F) → F) x₀, id x₀) ∘SL T.prod (ContinuousLinearMap.id ℝ F)) x₀

Tactic:
T.hasStrictFDerivAt.inner ℝ (hasStrictFDerivAt_id x₀)

Premises used: Real, ContinuousLinearMap.hasStrictFDerivAt, HasStrictFDerivAt.inner, hasStrictFDerivAt_id
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
T : F →L[ℝ] F
hT : LinearMap.IsSymmetric.{0, u_3} (𝕜 := ℝ) (E := F) (↑T : F →ₗ[ℝ] F)
x₀ : F
h :
  Real.instAddCommGroup = Ring.toAddCommGroup →
    HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule →
      HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2
          ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) ((T : (a : F) → F) x₀ : F) : F →L[ℝ] ℝ) =
        fderivInnerCLM ℝ ((T : (a : F) → F) x₀, id x₀) ∘SL T.prod (ContinuousLinearMap.id ℝ F)
⊢ HasStrictFDerivAt T.reApplyInnerSelf
    (HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2 ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) ((T : (a : F) → F) x₀ : F) : F →L[ℝ] ℝ))
    x₀

Tactic:
convert! T.hasStrictFDerivAt.inner ℝ (hasStrictFDerivAt_id x₀) using 1

Premises used: Real, ContinuousLinearMap.hasStrictFDerivAt, HasStrictFDerivAt.inner, hasStrictFDerivAt_id
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
T : F →L[ℝ] F
hT : LinearMap.IsSymmetric.{0, u_3} (𝕜 := ℝ) (E := F) (↑T : F →ₗ[ℝ] F)
x₀ : F
e_8 : Real.instAddCommGroup = Ring.toAddCommGroup
e_9 : HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule
h :
  ∀ (y : F),
    Eq (α := ℝ)
      ((HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2
              ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) ((T : (a : F) → F) x₀ : F) : F →L[ℝ] ℝ) :
            (a : F) → ℝ)
          y :
        ℝ)
      ((fderivInnerCLM ℝ ((T : (a : F) → F) x₀, id x₀) ∘SL T.prod (ContinuousLinearMap.id ℝ F) : (a : F) → ℝ) y : ℝ)
⊢ HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2 ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) ((T : (a : F) → F) x₀ : F) : F →L[ℝ] ℝ) =
    fderivInnerCLM ℝ ((T : (a : F) → F) x₀, id x₀) ∘SL T.prod (ContinuousLinearMap.id ℝ F)

Tactic:
ext y
-- 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₀
⊢ IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀

Tactic:
hextr
-- 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₀
h : Eq.{u_3 + 1} (α := Set F) {x : F | HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) ‖x₀‖ 2} (sphere 0 ‖x₀‖)
⊢ IsLocalExtrOn T.reApplyInnerSelf {x : F | HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) ‖x₀‖ 2} x₀

Tactic:
convert! hextr
-- 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₀
h :
  ∀ (x : F),
    Membership.mem (γ := Set F) {x : F | HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) ‖x₀‖ 2} x ↔
      Membership.mem (γ := Set F) (sphere 0 ‖x₀‖) x
⊢ Eq.{u_3 + 1} (α := Set F) {x : F | HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) ‖x₀‖ 2} (sphere 0 ‖x₀‖)

Tactic:
ext x
-- 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₀
x : F
⊢ Membership.mem (γ := Set F) {x : F | HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) ‖x₀‖ 2} x ↔
    Membership.mem (γ := Set F) (sphere 0 ‖x₀‖) x

Tactic:
simp
-- 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₀
⊢ IsLocalExtrOn T.reApplyInnerSelf {x : F | HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) ‖x₀‖ 2} x₀

Tactic:
have H : IsLocalExtrOn T.reApplyInnerSelf {x : F | ‖x‖ ^ 2 = ‖x₀‖ ^ 2} x₀ := by
    convert! hextr
    ext x
    simp
-- 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₀
H : IsLocalExtrOn T.reApplyInnerSelf {x : F | HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) ‖x₀‖ 2} x₀
obtain :
  ∀ (a b : ℝ) (h₁ : (a, b) ≠ 0)
    (h₂ :
      a • HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2 ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) x₀ : F →L[ℝ] ℝ) +
          b •
            HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2
              ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) ((T : (a : F) → F) x₀ : F) : F →L[ℝ] ℝ) =
        0),
    ∃ (a : ℝ) (b : ℝ), (a, b) ≠ 0 ∧ a • x₀ + HSMul.hSMul (β := F) b ((T : (a : F) → F) x₀ : F) = 0
⊢ ∃ (a : ℝ) (b : ℝ), (a, b) ≠ 0 ∧ a • x₀ + HSMul.hSMul (β := F) b ((T : (a : F) → F) x₀ : F) = 0

Tactic:
obtain ⟨a, b, h₁, h₂⟩ :=
    IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt_1d H (hasStrictFDerivAt_norm_sq x₀)
      (hT.isSymmetric.hasStrictFDerivAt_reApplyInnerSelf x₀)

Premises used: IsSelfAdjoint.isSymmetric, LinearMap.IsSymmetric.hasStrictFDerivAt_reApplyInnerSelf, hasStrictFDerivAt_norm_sq, IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt_1d
-- 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₀
H : IsLocalExtrOn T.reApplyInnerSelf {x : F | HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) ‖x₀‖ 2} x₀
a b : ℝ
h₁ : (a, b) ≠ 0
h₂ :
  a • HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2 ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) x₀ : F →L[ℝ] ℝ) +
      b •
        HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2
          ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) ((T : (a : F) → F) x₀ : F) : F →L[ℝ] ℝ) =
    0
⊢ ∃ (a : ℝ) (b : ℝ), (a, b) ≠ 0 ∧ a • x₀ + HSMul.hSMul (β := F) b ((T : (a : F) → F) x₀ : F) = 0

Tactic:
⟨a, b, h₁, ?_⟩

Premises used: And.intro, Exists.intro
-- 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₀
H : IsLocalExtrOn T.reApplyInnerSelf {x : F | HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) ‖x₀‖ 2} x₀
a b : ℝ
h₁ : (a, b) ≠ 0
h₂ :
  a • HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2 ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) x₀ : F →L[ℝ] ℝ) +
      b •
        HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2
          ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) ((T : (a : F) → F) x₀ : F) : F →L[ℝ] ℝ) =
    0
refine : a • x₀ + HSMul.hSMul (β := F) b ((T : (a : F) → F) x₀ : F) = 0
⊢ ∃ (a : ℝ) (b : ℝ), (a, b) ≠ 0 ∧ a • x₀ + HSMul.hSMul (β := F) b ((T : (a : F) → F) x₀ : F) = 0

Tactic:
refine ⟨a, 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₀
H : IsLocalExtrOn T.reApplyInnerSelf {x : F | HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) ‖x₀‖ 2} x₀
a b : ℝ
h₁ : (a, b) ≠ 0
h₂ :
  a • HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2 ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) x₀ : F →L[ℝ] ℝ) +
      b •
        HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2
          ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) ((T : (a : F) → F) x₀ : F) : F →L[ℝ] ℝ) =
    0
a₁ :
  Eq (α := StrongDual ℝ F)
    ((toDualMap ℝ F : (a : F) → StrongDual ℝ F) (a • x₀ + HSMul.hSMul (β := F) b ((T : (a : F) → F) x₀ : F)) :
      StrongDual ℝ F)
    ((toDualMap ℝ F : (a : F) → StrongDual ℝ F) 0 : StrongDual ℝ F)
⊢ a • x₀ + HSMul.hSMul (β := F) b ((T : (a : F) → F) x₀ : F) = 0

Tactic:
apply (InnerProductSpace.toDualMap ℝ F).injective

Premises used: Real, LinearIsometry.injective, InnerProductSpace.toDualMap
-- 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₀
H : IsLocalExtrOn T.reApplyInnerSelf {x : F | HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) ‖x₀‖ 2} x₀
a b : ℝ
h₁ : (a, b) ≠ 0
h₂ :
  a • HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2 ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) x₀ : F →L[ℝ] ℝ) +
      b •
        HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2
          ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) ((T : (a : F) → F) x₀ : F) : F →L[ℝ] ℝ) =
    0
a₁ :
  HAdd.hAdd (α := StrongDual ℝ F) (β := StrongDual ℝ F)
      ((toDualMap ℝ F : (a : F) → StrongDual ℝ F) (a • x₀) : StrongDual ℝ F)
      ((toDualMap ℝ F : (a : F) → StrongDual ℝ F) (HSMul.hSMul (β := F) b ((T : (a : F) → F) x₀ : F)) :
        StrongDual ℝ F) =
    0
⊢ Eq (α := StrongDual ℝ F)
    ((toDualMap ℝ F : (a : F) → StrongDual ℝ F) (a • x₀ + HSMul.hSMul (β := F) b ((T : (a : F) → F) x₀ : F)) :
      StrongDual ℝ F)
    ((toDualMap ℝ F : (a : F) → StrongDual ℝ F) 0 : StrongDual ℝ F)

Tactic:
simp only [LinearIsometry.map_add, LinearIsometry.map_zero]

Premises used: LinearIsometry.map_add, LinearIsometry.map_zero
-- 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₀
H : IsLocalExtrOn T.reApplyInnerSelf {x : F | HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) ‖x₀‖ 2} x₀
a b : ℝ
h₁ : (a, b) ≠ 0
h₂ :
  a • HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2 ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) x₀ : F →L[ℝ] ℝ) +
      b •
        HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2
          ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) ((T : (a : F) → F) x₀ : F) : F →L[ℝ] ℝ) =
    0
a₁ :
  HSMul.hSMul (β := StrongDual ℝ F) a ((toDualMap ℝ F : (a : F) → StrongDual ℝ F) x₀ : StrongDual ℝ F) +
      HSMul.hSMul (β := StrongDual ℝ F) b
        ((toDualMap ℝ F : (a : F) → StrongDual ℝ F) ((T : (a : F) → F) x₀) : StrongDual ℝ F) =
    0
⊢ HAdd.hAdd (α := StrongDual ℝ F) (β := StrongDual ℝ F)
      ((toDualMap ℝ F : (a : F) → StrongDual ℝ F) (a • x₀) : StrongDual ℝ F)
      ((toDualMap ℝ F : (a : F) → StrongDual ℝ F) (HSMul.hSMul (β := F) b ((T : (a : F) → F) x₀ : F)) :
        StrongDual ℝ F) =
    0

Tactic:
simp only [map_smulₛₗ _, RCLike.conj_to_real]

Premises used: MulActionSemiHomClass.map_smulₛₗ, RCLike.conj_to_real
-- 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₀
H : IsLocalExtrOn T.reApplyInnerSelf {x : F | HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) ‖x₀‖ 2} x₀
a b : ℝ
h₁ : (a, b) ≠ 0
h₂ :
  a • HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2 ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) x₀ : F →L[ℝ] ℝ) +
      b •
        HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2
          ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) ((T : (a : F) → F) x₀ : F) : F →L[ℝ] ℝ) =
    0
a₁ :
  HSMul.hSMul (β := F →L[ℝ] ℝ) a ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) x₀ : F →L[ℝ] ℝ) +
      HSMul.hSMul (β := F →L[ℝ] ℝ) b ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) ((T : (a : F) → F) x₀ : F) : F →L[ℝ] ℝ) =
    0
⊢ HSMul.hSMul (β := StrongDual ℝ F) a ((toDualMap ℝ F : (a : F) → StrongDual ℝ F) x₀ : StrongDual ℝ F) +
      HSMul.hSMul (β := StrongDual ℝ F) b
        ((toDualMap ℝ F : (a : F) → StrongDual ℝ F) ((T : (a : F) → F) x₀) : StrongDual ℝ F) =
    0

Tactic:
change a • innerSL ℝ x₀ + b • innerSL ℝ (T x₀) = 0

Premises used: Real, innerSL, DFunLike.coe
-- 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₀
H : IsLocalExtrOn T.reApplyInnerSelf {x : F | HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) ‖x₀‖ 2} x₀
a b : ℝ
h₁ : (a, b) ≠ 0
h₂ :
  a • HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2 ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) x₀ : F →L[ℝ] ℝ) +
      b •
        HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2
          ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) ((T : (a : F) → F) x₀ : F) : F →L[ℝ] ℝ) =
    0
a₁ :
  Eq.{u_3 + 1} (α := F →L[ℝ] ℝ)
    ((fun (x : F →L[ℝ] ℝ) ↦ HSMul.hSMul (α := ℝ) 2 x)
      (HSMul.hSMul (β := F →L[ℝ] ℝ) a ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) x₀ : F →L[ℝ] ℝ) +
        HSMul.hSMul (β := F →L[ℝ] ℝ) b ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) ((T : (a : F) → F) x₀ : F) : F →L[ℝ] ℝ)))
    ((fun (x : F →L[ℝ] ℝ) ↦ HSMul.hSMul (α := ℝ) 2 x) 0)
⊢ HSMul.hSMul (β := F →L[ℝ] ℝ) a ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) x₀ : F →L[ℝ] ℝ) +
      HSMul.hSMul (β := F →L[ℝ] ℝ) b ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) ((T : (a : F) → F) x₀ : F) : F →L[ℝ] ℝ) =
    0

Tactic:
apply smul_right_injective (F →L[ℝ] ℝ) (two_ne_zero : (2 : ℝ) ≠ 0)

Premises used: Real, smul_right_injective, ContinuousLinearMap, two_ne_zero, RingHom.id
-- 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₀
H : IsLocalExtrOn T.reApplyInnerSelf {x : F | HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) ‖x₀‖ 2} x₀
a b : ℝ
h₁ : (a, b) ≠ 0
h₂ :
  a • HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2 ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) x₀ : F →L[ℝ] ℝ) +
      b •
        HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2
          ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) ((T : (a : F) → F) x₀ : F) : F →L[ℝ] ℝ) =
    0
⊢ Eq.{u_3 + 1} (α := F →L[ℝ] ℝ)
    ((fun (x : F →L[ℝ] ℝ) ↦ HSMul.hSMul (α := ℝ) 2 x)
      (HSMul.hSMul (β := F →L[ℝ] ℝ) a ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) x₀ : F →L[ℝ] ℝ) +
        HSMul.hSMul (β := F →L[ℝ] ℝ) b ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) ((T : (a : F) → F) x₀ : F) : F →L[ℝ] ℝ)))
    ((fun (x : F →L[ℝ] ℝ) ↦ HSMul.hSMul (α := ℝ) 2 x) 0)

Tactic:
simpa only [two_smul, smul_add, add_smul, add_zero] using h₂

Premises used: two_smul, add_smul, add_zero, smul_add
-- 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₀
obtain :
  ∀ (a b : ℝ) (h₁ : (a, b) ≠ 0) (h₂ : a • x₀ + HSMul.hSMul (β := F) b ((T : (a : F) → F) x₀ : F) = 0),
    (T : (a : F) → F) x₀ = T.rayleighQuotient x₀ • x₀
⊢ (T : (a : F) → F) x₀ = T.rayleighQuotient x₀ • x₀

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

Premises used: IsSelfAdjoint.linearly_dependent_of_isLocalExtrOn
-- 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
pos : ∀ (hx₀ : x₀ = 0), (T : (a : F) → F) x₀ = T.rayleighQuotient x₀ • x₀
neg : ∀ (hx₀ : ¬x₀ = 0), (T : (a : F) → F) x₀ = T.rayleighQuotient x₀ • x₀
⊢ (T : (a : F) → F) x₀ = T.rayleighQuotient x₀ • x₀

Tactic:
by_cases hx₀ : x₀ = 0
-- 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
⊢ (T : (a : F) → F) x₀ = T.rayleighQuotient x₀ • x₀

Tactic:
simp [hx₀]
-- 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
pos : ∀ (hb : b = 0), (T : (a : F) → F) x₀ = T.rayleighQuotient x₀ • x₀
neg : ∀ (hb : ¬b = 0), (T : (a : F) → F) x₀ = T.rayleighQuotient x₀ • x₀
⊢ (T : (a : F) → F) x₀ = T.rayleighQuotient x₀ • x₀

Tactic:
by_cases hb : b = 0
-- 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 ≠ 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
⊢ a ≠ 0

Tactic:
have : a ≠ 0 := by simpa [hb] using h₁