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
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
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 : 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
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 : 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
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 : 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
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 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
inst_4 : Nontrivial E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
⊢ ProperSpace E

Tactic:
haveI := FiniteDimensional.proper_rclike 𝕜 E
-- 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 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
inst_4 : Nontrivial E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
this : ProperSpace E
T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint
⊢ ∃ (x : E), x ≠ 0

Tactic:
exists_ne 0

Premises used: exists_ne, OfNat.ofNat
-- 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 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
inst_4 : Nontrivial E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
this : ProperSpace E
T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint
obtain :
  ∀ (x : E) (hx : x ≠ 0),
    HasEigenvalue T
      (↑(⨆ (x : { x : E // x ≠ 0 }),
            HDiv.hDiv (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) (↑x : E), (↑x : E)⟫_𝕜 : ℝ)
              (HPow.hPow (β := ℕ) ‖(↑x : E)‖ 2)) :
        𝕜)
⊢ HasEigenvalue T
    (↑(⨆ (x : { x : E // x ≠ 0 }),
          HDiv.hDiv (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) (↑x : E), (↑x : E)⟫_𝕜 : ℝ)
            (HPow.hPow (β := ℕ) ‖(↑x : E)‖ 2)) :
      𝕜)

Tactic:
obtain ⟨x, hx⟩ : ∃ x : E, x ≠ 0 := exists_ne 0

Premises used: exists_ne, OfNat.ofNat
-- 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 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
inst_4 : Nontrivial E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
this : ProperSpace E
T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint
x : E
hx : x ≠ 0
⊢ IsCompact.{u_2} (X := E) (sphere 0 ‖x‖)

Tactic:
have H₁ : IsCompact (sphere (0 : E) ‖x‖) := isCompact_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 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
inst_4 : Nontrivial E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
this : ProperSpace E
T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint
x : E
hx : x ≠ 0
H₁ : IsCompact.{u_2} (X := E) (sphere 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 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
inst_4 : Nontrivial E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
this : ProperSpace E
T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint
x : E
hx : x ≠ 0
H₁ : IsCompact.{u_2} (X := E) (sphere 0 ‖x‖)
⊢ Set.Nonempty.{u_2} (α := E) (sphere 0 ‖x‖)

Tactic:
have H₂ : (sphere (0 : E) ‖x‖).Nonempty := ⟨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 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
inst_4 : Nontrivial E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
this : ProperSpace E
T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint
x : E
hx : x ≠ 0
H₁ : IsCompact.{u_2} (X := E) (sphere 0 ‖x‖)
H₂ : Set.Nonempty.{u_2} (α := E) (sphere 0 ‖x‖)
obtain :
  ∀ (x₀ : E) (hx₀' : Membership.mem (γ := Set E) (sphere 0 ‖x‖) x₀)
    (hTx₀ : IsMaxOn (↑T' : E →L[𝕜] E).reApplyInnerSelf (sphere 0 ‖x‖) x₀),
    HasEigenvalue T
      (↑(⨆ (x : { x : E // x ≠ 0 }),
            HDiv.hDiv (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) (↑x : E), (↑x : E)⟫_𝕜 : ℝ)
              (HPow.hPow (β := ℕ) ‖(↑x : E)‖ 2)) :
        𝕜)
⊢ HasEigenvalue T
    (↑(⨆ (x : { x : E // x ≠ 0 }),
          HDiv.hDiv (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) (↑x : E), (↑x : E)⟫_𝕜 : ℝ)
            (HPow.hPow (β := ℕ) ‖(↑x : E)‖ 2)) :
      𝕜)

Tactic:
obtain ⟨x₀, hx₀', hTx₀⟩ :=
    H₁.exists_isMaxOn H₂ T'.val.reApplyInnerSelf_continuous.continuousOn

Premises used: Continuous.continuousOn, ContinuousLinearMap.reApplyInnerSelf_continuous, Subtype.val, IsCompact.exists_isMaxOn
-- 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 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
inst_4 : Nontrivial E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
this : ProperSpace E
T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint
x : E
hx : x ≠ 0
H₁ : IsCompact.{u_2} (X := E) (sphere 0 ‖x‖)
H₂ : Set.Nonempty.{u_2} (α := E) (sphere 0 ‖x‖)
x₀ : E
hx₀' : Membership.mem (γ := Set E) (sphere 0 ‖x‖) x₀
hTx₀ : IsMaxOn (↑T' : E →L[𝕜] E).reApplyInnerSelf (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 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
inst_4 : Nontrivial E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
this : ProperSpace E
T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint
x : E
hx : x ≠ 0
H₁ : IsCompact.{u_2} (X := E) (sphere 0 ‖x‖)
H₂ : Set.Nonempty.{u_2} (α := E) (sphere 0 ‖x‖)
x₀ : E
hx₀' : Membership.mem (γ := Set E) (sphere 0 ‖x‖) x₀
hTx₀ : IsMaxOn (↑T' : E →L[𝕜] E).reApplyInnerSelf (sphere 0 ‖x‖) x₀
⊢ ‖x₀‖ = ‖x‖

Tactic:
have hx₀ : ‖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 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
inst_4 : Nontrivial E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
this : ProperSpace E
T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint
x : E
hx : x ≠ 0
H₁ : IsCompact.{u_2} (X := E) (sphere 0 ‖x‖)
H₂ : Set.Nonempty.{u_2} (α := E) (sphere 0 ‖x‖)
x₀ : E
hx₀' : Membership.mem (γ := Set E) (sphere 0 ‖x‖) x₀
hTx₀ : IsMaxOn (↑T' : E →L[𝕜] E).reApplyInnerSelf (sphere 0 ‖x‖) x₀
hx₀ : ‖x₀‖ = ‖x‖
⊢ IsMaxOn (↑T' : E →L[𝕜] E).reApplyInnerSelf (sphere 0 ‖x₀‖) x₀

Tactic:
simpa only [← hx₀] using hTx₀
-- 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 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
inst_4 : Nontrivial E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
this : ProperSpace E
T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint
x : E
hx : x ≠ 0
H₁ : IsCompact.{u_2} (X := E) (sphere 0 ‖x‖)
H₂ : Set.Nonempty.{u_2} (α := E) (sphere 0 ‖x‖)
x₀ : E
hx₀' : Membership.mem (γ := Set E) (sphere 0 ‖x‖) x₀
hTx₀ : IsMaxOn (↑T' : E →L[𝕜] E).reApplyInnerSelf (sphere 0 ‖x‖) x₀
hx₀ : ‖x₀‖ = ‖x‖
⊢ IsMaxOn (↑T' : E →L[𝕜] E).reApplyInnerSelf (sphere 0 ‖x₀‖) x₀

Tactic:
have : IsMaxOn T'.val.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀ := by simpa only [← hx₀] using hTx₀
-- 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 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
inst_4 : Nontrivial E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
this_1 : ProperSpace E
T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint
x : E
hx : x ≠ 0
H₁ : IsCompact.{u_2} (X := E) (sphere 0 ‖x‖)
H₂ : Set.Nonempty.{u_2} (α := E) (sphere 0 ‖x‖)
x₀ : E
hx₀' : Membership.mem (γ := Set E) (sphere 0 ‖x‖) x₀
hTx₀ : IsMaxOn (↑T' : E →L[𝕜] E).reApplyInnerSelf (sphere 0 ‖x‖) x₀
hx₀ : ‖x₀‖ = ‖x‖
this : IsMaxOn (↑T' : E →L[𝕜] E).reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
⊢ ‖x₀‖ ≠ 0

Tactic:
simp only [hx₀, norm_eq_zero, hx, Ne, not_false_iff]

Premises used: norm_eq_zero, Ne, not_false_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 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
inst_4 : Nontrivial E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
this_1 : ProperSpace E
T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint
x : E
hx : x ≠ 0
H₁ : IsCompact.{u_2} (X := E) (sphere 0 ‖x‖)
H₂ : Set.Nonempty.{u_2} (α := E) (sphere 0 ‖x‖)
x₀ : E
hx₀' : Membership.mem (γ := Set E) (sphere 0 ‖x‖) x₀
hTx₀ : IsMaxOn (↑T' : E →L[𝕜] E).reApplyInnerSelf (sphere 0 ‖x‖) x₀
hx₀ : ‖x₀‖ = ‖x‖
this : IsMaxOn (↑T' : E →L[𝕜] E).reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
⊢ ‖x₀‖ ≠ 0

Tactic:
have : ‖x₀‖ ≠ 0 := by simp only [hx₀, norm_eq_zero, hx, Ne, not_false_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 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
inst_4 : Nontrivial E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
this_1 : ProperSpace E
T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint
x : E
hx : x ≠ 0
H₁ : IsCompact.{u_2} (X := E) (sphere 0 ‖x‖)
H₂ : Set.Nonempty.{u_2} (α := E) (sphere 0 ‖x‖)
x₀ : E
hx₀' : Membership.mem (γ := Set E) (sphere 0 ‖x‖) x₀
hTx₀ : IsMaxOn (↑T' : E →L[𝕜] E).reApplyInnerSelf (sphere 0 ‖x‖) x₀
hx₀ : ‖x₀‖ = ‖x‖
this_2 : IsMaxOn (↑T' : E →L[𝕜] E).reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
this : ‖x₀‖ ≠ 0
⊢ x₀ ≠ 0

Tactic:
simpa [← norm_eq_zero, Ne]

Premises used: norm_eq_zero, Ne
-- 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 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
inst_4 : Nontrivial E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
this_1 : ProperSpace E
T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint
x : E
hx : x ≠ 0
H₁ : IsCompact.{u_2} (X := E) (sphere 0 ‖x‖)
H₂ : Set.Nonempty.{u_2} (α := E) (sphere 0 ‖x‖)
x₀ : E
hx₀' : Membership.mem (γ := Set E) (sphere 0 ‖x‖) x₀
hTx₀ : IsMaxOn (↑T' : E →L[𝕜] E).reApplyInnerSelf (sphere 0 ‖x‖) x₀
hx₀ : ‖x₀‖ = ‖x‖
this : IsMaxOn (↑T' : E →L[𝕜] E).reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
⊢ x₀ ≠ 0

Tactic:
have hx₀_ne : x₀ ≠ 0 := by
    have : ‖x₀‖ ≠ 0 := by simp only [hx₀, norm_eq_zero, hx, Ne, not_false_iff]
    simpa [← norm_eq_zero, Ne]
-- 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 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
inst_4 : Nontrivial E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
this_1 : ProperSpace E
T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint
x : E
hx : x ≠ 0
H₁ : IsCompact.{u_2} (X := E) (sphere 0 ‖x‖)
H₂ : Set.Nonempty.{u_2} (α := E) (sphere 0 ‖x‖)
x₀ : E
hx₀' : Membership.mem (γ := Set E) (sphere 0 ‖x‖) x₀
hTx₀ : IsMaxOn (↑T' : E →L[𝕜] E).reApplyInnerSelf (sphere 0 ‖x‖) x₀
hx₀ : ‖x₀‖ = ‖x‖
this : IsMaxOn (↑T' : E →L[𝕜] E).reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀_ne : x₀ ≠ 0
⊢ HasEigenvalue T
    (↑(⨆ (x : { x : E // x ≠ 0 }),
          HDiv.hDiv (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) (↑x : E), (↑x : E)⟫_𝕜 : ℝ)
            (HPow.hPow (β := ℕ) ‖(↑x : E)‖ 2)) :
      𝕜)

Tactic:
hasEigenvalue_of_hasEigenvector (T'.prop.hasEigenvector_of_isMaxOn hx₀_ne this)

Premises used: IsSelfAdjoint.hasEigenvector_of_isMaxOn, Module.End.hasEigenvalue_of_hasEigenvector, Subtype.prop
-- 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 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
inst_4 : Nontrivial E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
this_1 : ProperSpace E
T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint
x : E
hx : x ≠ 0
H₁ : IsCompact.{u_2} (X := E) (sphere 0 ‖x‖)
H₂ : Set.Nonempty.{u_2} (α := E) (sphere 0 ‖x‖)
x₀ : E
hx₀' : Membership.mem (γ := Set E) (sphere 0 ‖x‖) x₀
hTx₀ : IsMaxOn (↑T' : E →L[𝕜] E).reApplyInnerSelf (sphere 0 ‖x‖) x₀
hx₀ : ‖x₀‖ = ‖x‖
this : IsMaxOn (↑T' : E →L[𝕜] E).reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀_ne : x₀ ≠ 0
⊢ HasEigenvalue T
    (↑(⨆ (x : { x : E // x ≠ 0 }),
          HDiv.hDiv (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) (↑x : E), (↑x : E)⟫_𝕜 : ℝ)
            (HPow.hPow (β := ℕ) ‖(↑x : E)‖ 2)) :
      𝕜)

Tactic:
exact hasEigenvalue_of_hasEigenvector (T'.prop.hasEigenvector_of_isMaxOn hx₀_ne this)

Premises used: IsSelfAdjoint.hasEigenvector_of_isMaxOn, Module.End.hasEigenvalue_of_hasEigenvector, Subtype.prop
-- 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 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
inst_4 : Nontrivial E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
this : ProperSpace E
T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint
obtain :
  ∀ (x : E) (hx : x ≠ 0),
    HasEigenvalue T
      (↑(⨅ (x : { x : E // x ≠ 0 }),
            HDiv.hDiv (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) (↑x : E), (↑x : E)⟫_𝕜 : ℝ)
              (HPow.hPow (β := ℕ) ‖(↑x : E)‖ 2)) :
        𝕜)
⊢ HasEigenvalue T
    (↑(⨅ (x : { x : E // x ≠ 0 }),
          HDiv.hDiv (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) (↑x : E), (↑x : E)⟫_𝕜 : ℝ)
            (HPow.hPow (β := ℕ) ‖(↑x : E)‖ 2)) :
      𝕜)

Tactic:
obtain ⟨x, hx⟩ : ∃ x : E, x ≠ 0 := exists_ne 0

Premises used: exists_ne, OfNat.ofNat
-- 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 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
inst_4 : Nontrivial E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
this : ProperSpace E
T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint
x : E
hx : x ≠ 0
H₁ : IsCompact.{u_2} (X := E) (sphere 0 ‖x‖)
H₂ : Set.Nonempty.{u_2} (α := E) (sphere 0 ‖x‖)
obtain :
  ∀ (x₀ : E) (hx₀' : Membership.mem (γ := Set E) (sphere 0 ‖x‖) x₀)
    (hTx₀ : IsMinOn (↑T' : E →L[𝕜] E).reApplyInnerSelf (sphere 0 ‖x‖) x₀),
    HasEigenvalue T
      (↑(⨅ (x : { x : E // x ≠ 0 }),
            HDiv.hDiv (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) (↑x : E), (↑x : E)⟫_𝕜 : ℝ)
              (HPow.hPow (β := ℕ) ‖(↑x : E)‖ 2)) :
        𝕜)
⊢ HasEigenvalue T
    (↑(⨅ (x : { x : E // x ≠ 0 }),
          HDiv.hDiv (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) (↑x : E), (↑x : E)⟫_𝕜 : ℝ)
            (HPow.hPow (β := ℕ) ‖(↑x : E)‖ 2)) :
      𝕜)

Tactic:
obtain ⟨x₀, hx₀', hTx₀⟩ :=
    H₁.exists_isMinOn H₂ T'.val.reApplyInnerSelf_continuous.continuousOn

Premises used: Continuous.continuousOn, IsCompact.exists_isMinOn, ContinuousLinearMap.reApplyInnerSelf_continuous, Subtype.val
-- 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 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
inst_4 : Nontrivial E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
this : ProperSpace E
T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint
x : E
hx : x ≠ 0
H₁ : IsCompact.{u_2} (X := E) (sphere 0 ‖x‖)
H₂ : Set.Nonempty.{u_2} (α := E) (sphere 0 ‖x‖)
x₀ : E
hx₀' : Membership.mem (γ := Set E) (sphere 0 ‖x‖) x₀
hTx₀ : IsMinOn (↑T' : E →L[𝕜] E).reApplyInnerSelf (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 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
inst_4 : Nontrivial E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
this : ProperSpace E
T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint
x : E
hx : x ≠ 0
H₁ : IsCompact.{u_2} (X := E) (sphere 0 ‖x‖)
H₂ : Set.Nonempty.{u_2} (α := E) (sphere 0 ‖x‖)
x₀ : E
hx₀' : Membership.mem (γ := Set E) (sphere 0 ‖x‖) x₀
hTx₀ : IsMinOn (↑T' : E →L[𝕜] E).reApplyInnerSelf (sphere 0 ‖x‖) x₀
⊢ ‖x₀‖ = ‖x‖

Tactic:
have hx₀ : ‖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 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
inst_4 : Nontrivial E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
this : ProperSpace E
T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint
x : E
hx : x ≠ 0
H₁ : IsCompact.{u_2} (X := E) (sphere 0 ‖x‖)
H₂ : Set.Nonempty.{u_2} (α := E) (sphere 0 ‖x‖)
x₀ : E
hx₀' : Membership.mem (γ := Set E) (sphere 0 ‖x‖) x₀
hTx₀ : IsMinOn (↑T' : E →L[𝕜] E).reApplyInnerSelf (sphere 0 ‖x‖) x₀
hx₀ : ‖x₀‖ = ‖x‖
⊢ IsMinOn (↑T' : E →L[𝕜] E).reApplyInnerSelf (sphere 0 ‖x₀‖) x₀

Tactic:
simpa only [← hx₀] using hTx₀
-- 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 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
inst_4 : Nontrivial E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
this : ProperSpace E
T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint
x : E
hx : x ≠ 0
H₁ : IsCompact.{u_2} (X := E) (sphere 0 ‖x‖)
H₂ : Set.Nonempty.{u_2} (α := E) (sphere 0 ‖x‖)
x₀ : E
hx₀' : Membership.mem (γ := Set E) (sphere 0 ‖x‖) x₀
hTx₀ : IsMinOn (↑T' : E →L[𝕜] E).reApplyInnerSelf (sphere 0 ‖x‖) x₀
hx₀ : ‖x₀‖ = ‖x‖
⊢ IsMinOn (↑T' : E →L[𝕜] E).reApplyInnerSelf (sphere 0 ‖x₀‖) x₀

Tactic:
have : IsMinOn T'.val.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀ := by simpa only [← hx₀] using hTx₀
-- 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 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
inst_4 : Nontrivial E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
this_1 : ProperSpace E
T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint
x : E
hx : x ≠ 0
H₁ : IsCompact.{u_2} (X := E) (sphere 0 ‖x‖)
H₂ : Set.Nonempty.{u_2} (α := E) (sphere 0 ‖x‖)
x₀ : E
hx₀' : Membership.mem (γ := Set E) (sphere 0 ‖x‖) x₀
hTx₀ : IsMinOn (↑T' : E →L[𝕜] E).reApplyInnerSelf (sphere 0 ‖x‖) x₀
hx₀ : ‖x₀‖ = ‖x‖
this : IsMinOn (↑T' : E →L[𝕜] E).reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
⊢ ‖x₀‖ ≠ 0

Tactic:
simp only [hx₀, norm_eq_zero, hx, Ne, not_false_iff]

Premises used: norm_eq_zero, Ne, not_false_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 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
inst_4 : Nontrivial E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
this_1 : ProperSpace E
T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint
x : E
hx : x ≠ 0
H₁ : IsCompact.{u_2} (X := E) (sphere 0 ‖x‖)
H₂ : Set.Nonempty.{u_2} (α := E) (sphere 0 ‖x‖)
x₀ : E
hx₀' : Membership.mem (γ := Set E) (sphere 0 ‖x‖) x₀
hTx₀ : IsMinOn (↑T' : E →L[𝕜] E).reApplyInnerSelf (sphere 0 ‖x‖) x₀
hx₀ : ‖x₀‖ = ‖x‖
this : IsMinOn (↑T' : E →L[𝕜] E).reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
⊢ ‖x₀‖ ≠ 0

Tactic:
have : ‖x₀‖ ≠ 0 := by simp only [hx₀, norm_eq_zero, hx, Ne, not_false_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 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
inst_4 : Nontrivial E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
this_1 : ProperSpace E
T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint
x : E
hx : x ≠ 0
H₁ : IsCompact.{u_2} (X := E) (sphere 0 ‖x‖)
H₂ : Set.Nonempty.{u_2} (α := E) (sphere 0 ‖x‖)
x₀ : E
hx₀' : Membership.mem (γ := Set E) (sphere 0 ‖x‖) x₀
hTx₀ : IsMinOn (↑T' : E →L[𝕜] E).reApplyInnerSelf (sphere 0 ‖x‖) x₀
hx₀ : ‖x₀‖ = ‖x‖
this_2 : IsMinOn (↑T' : E →L[𝕜] E).reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
this : ‖x₀‖ ≠ 0
⊢ x₀ ≠ 0

Tactic:
simpa [← norm_eq_zero, Ne]

Premises used: norm_eq_zero, Ne
-- 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 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
inst_4 : Nontrivial E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
this_1 : ProperSpace E
T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint
x : E
hx : x ≠ 0
H₁ : IsCompact.{u_2} (X := E) (sphere 0 ‖x‖)
H₂ : Set.Nonempty.{u_2} (α := E) (sphere 0 ‖x‖)
x₀ : E
hx₀' : Membership.mem (γ := Set E) (sphere 0 ‖x‖) x₀
hTx₀ : IsMinOn (↑T' : E →L[𝕜] E).reApplyInnerSelf (sphere 0 ‖x‖) x₀
hx₀ : ‖x₀‖ = ‖x‖
this : IsMinOn (↑T' : E →L[𝕜] E).reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
⊢ x₀ ≠ 0

Tactic:
have hx₀_ne : x₀ ≠ 0 := by
    have : ‖x₀‖ ≠ 0 := by simp only [hx₀, norm_eq_zero, hx, Ne, not_false_iff]
    simpa [← norm_eq_zero, Ne]
-- 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 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
inst_4 : Nontrivial E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
this_1 : ProperSpace E
T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint
x : E
hx : x ≠ 0
H₁ : IsCompact.{u_2} (X := E) (sphere 0 ‖x‖)
H₂ : Set.Nonempty.{u_2} (α := E) (sphere 0 ‖x‖)
x₀ : E
hx₀' : Membership.mem (γ := Set E) (sphere 0 ‖x‖) x₀
hTx₀ : IsMinOn (↑T' : E →L[𝕜] E).reApplyInnerSelf (sphere 0 ‖x‖) x₀
hx₀ : ‖x₀‖ = ‖x‖
this : IsMinOn (↑T' : E →L[𝕜] E).reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀_ne : x₀ ≠ 0
⊢ HasEigenvalue T
    (↑(⨅ (x : { x : E // x ≠ 0 }),
          HDiv.hDiv (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) (↑x : E), (↑x : E)⟫_𝕜 : ℝ)
            (HPow.hPow (β := ℕ) ‖(↑x : E)‖ 2)) :
      𝕜)

Tactic:
hasEigenvalue_of_hasEigenvector (T'.prop.hasEigenvector_of_isMinOn hx₀_ne this)

Premises used: Module.End.hasEigenvalue_of_hasEigenvector, Subtype.prop, IsSelfAdjoint.hasEigenvector_of_isMinOn