awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (goal)
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
⊢ spectralRadius 𝕜 T = (↑‖T‖₊ : ENNReal)
have apply : (↑‖T‖₊ : ENNReal) ≤ spectralRadius 𝕜 T
Tactic: apply le_antisymm (spectrum.spectralRadius_le_nnnorm T)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (goal)
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‖) : 𝕜)
⊢ (↑‖T‖₊ : ENNReal) ≤ spectralRadius 𝕜 T
have inl : ∀ (h : Membership.mem (α := 𝕜) (spectrum 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜)),
  (↑‖T‖₊ : ENNReal) ≤ spectralRadius 𝕜 T
Tactic: rcases h with h | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (goal)
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
⊢ (↑‖T‖₊ : ENNReal) ≤ spectralRadius 𝕜 T
have inr : ∀ (h : Membership.mem (α := 𝕜) (spectrum 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) (-‖T‖) : 𝕜)),
  (↑‖T‖₊ : ENNReal) ≤ spectralRadius 𝕜 T
Tactic: rcases h with h | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (goal)
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
⊢ (↑‖T‖₊ : ENNReal) ≤ spectralRadius 𝕜 T
have suffices : Membership.mem (α := 𝕜) (spectrum 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜) ∨
  Membership.mem (α := 𝕜) (spectrum 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) (-‖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)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (goal)
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
⊢ Membership.mem (α := 𝕜) (spectrum 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜) ∨
    Membership.mem (α := 𝕜) (spectrum 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) (-‖T‖) : 𝕜)
have simp_rw : ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜) ∉ resolventSet 𝕜 T ∨
  (-(algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜) ∉ resolventSet 𝕜 T
Tactic: simp_rw [spectrum, Set.mem_compl_iff, map_neg]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (goal)
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
⊢ ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜) ∉ resolventSet 𝕜 T ∨
    (-(algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜) ∉ resolventSet 𝕜 T
have by_contra! : ∀
  (h :
    Membership.mem (α := 𝕜) (resolventSet 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜) ∧
      Membership.mem (α := 𝕜) (resolventSet 𝕜 T) (-(algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜)),
  False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (goal)
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‖ : 𝕜)
⊢ False
have obtain : ∀ (c : ℝ) (hc0 : c > 0) (hc : ∀ (x : E), |T.rayleighQuotient x| ≤ ‖T‖ - c), False
Tactic: obtain ⟨c, hc0, hc⟩ := T.abs_rayleighQuotient_le_of_norm_mem_resolventSet h.1 h.2
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (goal)
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 T.reApplyInnerSelf
    (HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2 ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) ((T : (a : F) → F) x₀ : F) : F →L[ℝ] ℝ))
    x₀
have 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)
Tactic: convert! T.hasStrictFDerivAt.inner ℝ (hasStrictFDerivAt_id x₀) using 1
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (goal)
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
⊢ 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)
have 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 : ℝ)
Tactic: ext y
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (goal)
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
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 : ℝ)
have h : HSMul.hSMul (α := ℕ) (β := ℝ) 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
Tactic: rw [ContinuousLinearMap.smul_apply, ContinuousLinearMap.comp_apply, fderivInnerCLM_apply,
    ContinuousLinearMap.prod_apply, innerSL_apply_apply, id, ContinuousLinearMap.id_apply,
    hT.apply_clm x₀ y, real_inner_comm _ x₀, two_smul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (goal)
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
y : F
h :
  HSMul.hSMul (α := ℕ) (β := ℝ) 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
⊢ 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 : ℝ)
have h₁ : HSMul.hSMul (α := ℕ) (β := ℝ) 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₀) : (a : F × F) → ℝ)
    ((T.prod (ContinuousLinearMap.id ℝ F) : (a : F) → F × F) y : F × F)
Tactic: rw [ContinuousLinearMap.smul_apply, ContinuousLinearMap.comp_apply, fderivInnerCLM_apply,
    ContinuousLinearMap.prod_apply, innerSL_apply_apply, id, ContinuousLinearMap.id_apply,
    hT.apply_clm x₀ y, real_inner_comm _ x₀, two_smul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (goal)
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
y : F
h :
  HSMul.hSMul (α := ℕ) (β := ℝ) 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
h₁ :
  HSMul.hSMul (α := ℕ) (β := ℝ) 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₀) : (a : F × F) → ℝ)
      ((T.prod (ContinuousLinearMap.id ℝ F) : (a : F) → F × F) y : F × 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 : ℝ)
have h₂ : HSMul.hSMul (α := ℕ) (β := ℝ) 2
    ((((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) ((T : (a : F) → F) x₀ : F) : F →L[ℝ] ℝ) : (a : F) → ℝ) y : ℝ) =
  inner ℝ (E := F) (((T : (a : F) → F) x₀, id x₀).1 : F)
      (((T.prod (ContinuousLinearMap.id ℝ F) : (a : F) → F × F) y).2 : F) +
    ⟪((T.prod (ContinuousLinearMap.id ℝ F) : (a : F) → F × F) y).1, (((T : (a : F) → F) x₀, id x₀) : F × F).2⟫_ℝ
Tactic: rw [ContinuousLinearMap.smul_apply, ContinuousLinearMap.comp_apply, fderivInnerCLM_apply,
    ContinuousLinearMap.prod_apply, innerSL_apply_apply, id, ContinuousLinearMap.id_apply,
    hT.apply_clm x₀ y, real_inner_comm _ x₀, two_smul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (goal)
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
y : F
h :
  HSMul.hSMul (α := ℕ) (β := ℝ) 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
h₁ :
  HSMul.hSMul (α := ℕ) (β := ℝ) 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₀) : (a : F × F) → ℝ)
      ((T.prod (ContinuousLinearMap.id ℝ F) : (a : F) → F × F) y : F × F)
h₂ :
  HSMul.hSMul (α := ℕ) (β := ℝ) 2
      ((((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) ((T : (a : F) → F) x₀ : F) : F →L[ℝ] ℝ) : (a : F) → ℝ) y : ℝ) =
    inner ℝ (E := F) (((T : (a : F) → F) x₀, id x₀).1 : F)
        (((T.prod (ContinuousLinearMap.id ℝ F) : (a : F) → F × F) y).2 : F) +
      ⟪((T.prod (ContinuousLinearMap.id ℝ F) : (a : F) → F × F) y).1, (((T : (a : F) → F) x₀, id x₀) : F × F).2⟫_ℝ
⊢ 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 : ℝ)
have h₃ : HSMul.hSMul (α := ℕ) (β := ℝ) 2
    ((((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) ((T : (a : F) → F) x₀ : F) : F →L[ℝ] ℝ) : (a : F) → ℝ) y : ℝ) =
  inner ℝ (E := F) (((T : (a : F) → F) x₀, id x₀).1 : F)
      (((T : (a : F) → F) y, (ContinuousLinearMap.id ℝ F : (a : F) → F) y).2 : F) +
    ⟪((T : (a : F) → F) y, (ContinuousLinearMap.id ℝ F : (a : F) → F) y).1, (((T : (a : F) → F) x₀, id x₀) : F × F).2⟫_ℝ
Tactic: rw [ContinuousLinearMap.smul_apply, ContinuousLinearMap.comp_apply, fderivInnerCLM_apply,
    ContinuousLinearMap.prod_apply, innerSL_apply_apply, id, ContinuousLinearMap.id_apply,
    hT.apply_clm x₀ y, real_inner_comm _ x₀, two_smul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (goal)
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
y : F
h :
  HSMul.hSMul (α := ℕ) (β := ℝ) 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
h₁ :
  HSMul.hSMul (α := ℕ) (β := ℝ) 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₀) : (a : F × F) → ℝ)
      ((T.prod (ContinuousLinearMap.id ℝ F) : (a : F) → F × F) y : F × F)
h₂ :
  HSMul.hSMul (α := ℕ) (β := ℝ) 2
      ((((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) ((T : (a : F) → F) x₀ : F) : F →L[ℝ] ℝ) : (a : F) → ℝ) y : ℝ) =
    inner ℝ (E := F) (((T : (a : F) → F) x₀, id x₀).1 : F)
        (((T.prod (ContinuousLinearMap.id ℝ F) : (a : F) → F × F) y).2 : F) +
      ⟪((T.prod (ContinuousLinearMap.id ℝ F) : (a : F) → F × F) y).1, (((T : (a : F) → F) x₀, id x₀) : F × F).2⟫_ℝ
h₃ :
  HSMul.hSMul (α := ℕ) (β := ℝ) 2
      ((((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) ((T : (a : F) → F) x₀ : F) : F →L[ℝ] ℝ) : (a : F) → ℝ) y : ℝ) =
    inner ℝ (E := F) (((T : (a : F) → F) x₀, id x₀).1 : F)
        (((T : (a : F) → F) y, (ContinuousLinearMap.id ℝ F : (a : F) → F) y).2 : F) +
      ⟪((T : (a : F) → F) y, (ContinuousLinearMap.id ℝ F : (a : F) → F) y).1,
        (((T : (a : F) → F) x₀, id x₀) : F × F).2⟫_ℝ
⊢ 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 : ℝ)
have h₄ : HSMul.hSMul (α := ℕ) 2 ⟪(T : (a : F) → F) x₀, y⟫_ℝ =
  inner ℝ (E := F) (((T : (a : F) → F) x₀, id x₀).1 : F)
      (((T : (a : F) → F) y, (ContinuousLinearMap.id ℝ F : (a : F) → F) y).2 : F) +
    ⟪((T : (a : F) → F) y, (ContinuousLinearMap.id ℝ F : (a : F) → F) y).1, (((T : (a : F) → F) x₀, id x₀) : F × F).2⟫_ℝ
Tactic: rw [ContinuousLinearMap.smul_apply, ContinuousLinearMap.comp_apply, fderivInnerCLM_apply,
    ContinuousLinearMap.prod_apply, innerSL_apply_apply, id, ContinuousLinearMap.id_apply,
    hT.apply_clm x₀ y, real_inner_comm _ x₀, two_smul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (goal)
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
y : F
h :
  HSMul.hSMul (α := ℕ) (β := ℝ) 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
h₁ :
  HSMul.hSMul (α := ℕ) (β := ℝ) 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₀) : (a : F × F) → ℝ)
      ((T.prod (ContinuousLinearMap.id ℝ F) : (a : F) → F × F) y : F × F)
h₂ :
  HSMul.hSMul (α := ℕ) (β := ℝ) 2
      ((((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) ((T : (a : F) → F) x₀ : F) : F →L[ℝ] ℝ) : (a : F) → ℝ) y : ℝ) =
    inner ℝ (E := F) (((T : (a : F) → F) x₀, id x₀).1 : F)
        (((T.prod (ContinuousLinearMap.id ℝ F) : (a : F) → F × F) y).2 : F) +
      ⟪((T.prod (ContinuousLinearMap.id ℝ F) : (a : F) → F × F) y).1, (((T : (a : F) → F) x₀, id x₀) : F × F).2⟫_ℝ
h₃ :
  HSMul.hSMul (α := ℕ) (β := ℝ) 2
      ((((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) ((T : (a : F) → F) x₀ : F) : F →L[ℝ] ℝ) : (a : F) → ℝ) y : ℝ) =
    inner ℝ (E := F) (((T : (a : F) → F) x₀, id x₀).1 : F)
        (((T : (a : F) → F) y, (ContinuousLinearMap.id ℝ F : (a : F) → F) y).2 : F) +
      ⟪((T : (a : F) → F) y, (ContinuousLinearMap.id ℝ F : (a : F) → F) y).1,
        (((T : (a : F) → F) x₀, id x₀) : F × F).2⟫_ℝ
h₄ :
  HSMul.hSMul (α := ℕ) 2 ⟪(T : (a : F) → F) x₀, y⟫_ℝ =
    inner ℝ (E := F) (((T : (a : F) → F) x₀, id x₀).1 : F)
        (((T : (a : F) → F) y, (ContinuousLinearMap.id ℝ F : (a : F) → F) y).2 : F) +
      ⟪((T : (a : F) → F) y, (ContinuousLinearMap.id ℝ F : (a : F) → F) y).1,
        (((T : (a : F) → F) x₀, id x₀) : F × F).2⟫_ℝ
⊢ 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 : ℝ)
have h₅ : HSMul.hSMul (α := ℕ) 2 ⟪(T : (a : F) → F) x₀, y⟫_ℝ =
  inner ℝ (E := F) (((T : (a : F) → F) x₀, x₀).1 : F)
      (((T : (a : F) → F) y, (ContinuousLinearMap.id ℝ F : (a : F) → F) y).2 : F) +
    ⟪((T : (a : F) → F) y, (ContinuousLinearMap.id ℝ F : (a : F) → F) y).1, (((T : (a : F) → F) x₀, x₀) : F × F).2⟫_ℝ
Tactic: rw [ContinuousLinearMap.smul_apply, ContinuousLinearMap.comp_apply, fderivInnerCLM_apply,
    ContinuousLinearMap.prod_apply, innerSL_apply_apply, id, ContinuousLinearMap.id_apply,
    hT.apply_clm x₀ y, real_inner_comm _ x₀, two_smul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (goal)
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
y : F
h :
  HSMul.hSMul (α := ℕ) (β := ℝ) 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
h₁ :
  HSMul.hSMul (α := ℕ) (β := ℝ) 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₀) : (a : F × F) → ℝ)
      ((T.prod (ContinuousLinearMap.id ℝ F) : (a : F) → F × F) y : F × F)
h₂ :
  HSMul.hSMul (α := ℕ) (β := ℝ) 2
      ((((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) ((T : (a : F) → F) x₀ : F) : F →L[ℝ] ℝ) : (a : F) → ℝ) y : ℝ) =
    inner ℝ (E := F) (((T : (a : F) → F) x₀, id x₀).1 : F)
        (((T.prod (ContinuousLinearMap.id ℝ F) : (a : F) → F × F) y).2 : F) +
      ⟪((T.prod (ContinuousLinearMap.id ℝ F) : (a : F) → F × F) y).1, (((T : (a : F) → F) x₀, id x₀) : F × F).2⟫_ℝ
h₃ :
  HSMul.hSMul (α := ℕ) (β := ℝ) 2
      ((((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) ((T : (a : F) → F) x₀ : F) : F →L[ℝ] ℝ) : (a : F) → ℝ) y : ℝ) =
    inner ℝ (E := F) (((T : (a : F) → F) x₀, id x₀).1 : F)
        (((T : (a : F) → F) y, (ContinuousLinearMap.id ℝ F : (a : F) → F) y).2 : F) +
      ⟪((T : (a : F) → F) y, (ContinuousLinearMap.id ℝ F : (a : F) → F) y).1,
        (((T : (a : F) → F) x₀, id x₀) : F × F).2⟫_ℝ
h₄ :
  HSMul.hSMul (α := ℕ) 2 ⟪(T : (a : F) → F) x₀, y⟫_ℝ =
    inner ℝ (E := F) (((T : (a : F) → F) x₀, id x₀).1 : F)
        (((T : (a : F) → F) y, (ContinuousLinearMap.id ℝ F : (a : F) → F) y).2 : F) +
      ⟪((T : (a : F) → F) y, (ContinuousLinearMap.id ℝ F : (a : F) → F) y).1,
        (((T : (a : F) → F) x₀, id x₀) : F × F).2⟫_ℝ
h₅ :
  HSMul.hSMul (α := ℕ) 2 ⟪(T : (a : F) → F) x₀, y⟫_ℝ =
    inner ℝ (E := F) (((T : (a : F) → F) x₀, x₀).1 : F)
        (((T : (a : F) → F) y, (ContinuousLinearMap.id ℝ F : (a : F) → F) y).2 : F) +
      ⟪((T : (a : F) → F) y, (ContinuousLinearMap.id ℝ F : (a : F) → F) y).1, (((T : (a : F) → F) x₀, x₀) : F × F).2⟫_ℝ
⊢ 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 : ℝ)
have h₆ : HSMul.hSMul (α := ℕ) 2 ⟪(T : (a : F) → F) x₀, y⟫_ℝ =
  ⟪((T : (a : F) → F) x₀, x₀).1, (((T : (a : F) → F) y, y) : F × F).2⟫_ℝ +
    ⟪((T : (a : F) → F) y, y).1, (((T : (a : F) → F) x₀, x₀) : F × F).2⟫_ℝ
Tactic: rw [ContinuousLinearMap.smul_apply, ContinuousLinearMap.comp_apply, fderivInnerCLM_apply,
    ContinuousLinearMap.prod_apply, innerSL_apply_apply, id, ContinuousLinearMap.id_apply,
    hT.apply_clm x₀ y, real_inner_comm _ x₀, two_smul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (goal)
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₀
have h : Eq.{u_3 + 1} (α := Set F) {x : F | HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) ‖x₀‖ 2} (sphere 0 ‖x₀‖)
Tactic: convert! hextr
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (goal)
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₀
⊢ Eq.{u_3 + 1} (α := Set F) {x : F | HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) ‖x₀‖ 2} (sphere 0 ‖x₀‖)
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (hypothesis)
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 : ℝ), (a, b) ≠ 0 ∧ a • x₀ + HSMul.hSMul (β := F) b ((T : (a : F) → F) x₀ : F) = 0
have H : 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