awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (hypothesis)
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
⊢ T.rayleighQuotient x₀ ≤ T.rayleighQuotient x
have this : ‖x‖ = ‖x₀‖
Tactic: have : ‖x‖ = ‖x₀‖ := by simpa using hx
-- 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
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₀ / HPow.hPow (β := ℕ) ‖x₀‖ 2 ≤ T.reApplyInnerSelf x / HPow.hPow (β := ℕ) ‖x‖ 2
have h : T.reApplyInnerSelf x₀ / HPow.hPow (β := ℕ) ‖x₀‖ 2 ≤ T.reApplyInnerSelf x / HPow.hPow (β := ℕ) ‖x₀‖ 2
Tactic: rw [this]
-- 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
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₀ / HPow.hPow (β := ℕ) ‖x₀‖ 2 ≤ T.reApplyInnerSelf x / HPow.hPow (β := ℕ) ‖x₀‖ 2
have h : T.reApplyInnerSelf x₀ ≤ T.reApplyInnerSelf x
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (hypothesis)
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
⊢ HasEigenvalue T
    (↑(⨆ (x : { x : E // x ≠ 0 }),
          HDiv.hDiv (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) (↑x : E), (↑x : E)⟫_𝕜 : ℝ)
            (HPow.hPow (β := ℕ) ‖(↑x : E)‖ 2)) :
      𝕜)
have this : ProperSpace E
Tactic: haveI := FiniteDimensional.proper_rclike 𝕜 E
-- 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
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
⊢ HasEigenvalue T
    (↑(⨆ (x : { x : E // x ≠ 0 }),
          HDiv.hDiv (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) (↑x : E), (↑x : E)⟫_𝕜 : ℝ)
            (HPow.hPow (β := ℕ) ‖(↑x : E)‖ 2)) :
      𝕜)
have 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)) :
      𝕜)
Tactic: obtain ⟨x, hx⟩ : ∃ x : E, x ≠ 0 := exists_ne 0
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (hypothesis)
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
⊢ HasEigenvalue T
    (↑(⨆ (x : { x : E // x ≠ 0 }),
          HDiv.hDiv (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) (↑x : E), (↑x : E)⟫_𝕜 : ℝ)
            (HPow.hPow (β := ℕ) ‖(↑x : E)‖ 2)) :
      𝕜)
have H₁ : IsCompact.{u_2} (X := E) (sphere 0 ‖x‖)
Tactic: have H₁ : IsCompact (sphere (0 : E) ‖x‖) := isCompact_sphere _ _
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (hypothesis)
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‖)
⊢ HasEigenvalue T
    (↑(⨆ (x : { x : E // x ≠ 0 }),
          HDiv.hDiv (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) (↑x : E), (↑x : E)⟫_𝕜 : ℝ)
            (HPow.hPow (β := ℕ) ‖(↑x : E)‖ 2)) :
      𝕜)
have H₂ : Set.Nonempty.{u_2} (α := E) (sphere 0 ‖x‖)
Tactic: have H₂ : (sphere (0 : E) ‖x‖).Nonempty := ⟨x, by simp⟩
-- 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
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‖)
⊢ HasEigenvalue T
    (↑(⨆ (x : { x : E // x ≠ 0 }),
          HDiv.hDiv (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) (↑x : E), (↑x : E)⟫_𝕜 : ℝ)
            (HPow.hPow (β := ℕ) ‖(↑x : E)‖ 2)) :
      𝕜)
have 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)) :
      𝕜)
Tactic: obtain ⟨x₀, hx₀', hTx₀⟩ :=
    H₁.exists_isMaxOn H₂ T'.val.reApplyInnerSelf_continuous.continuousOn
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (hypothesis)
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₀
⊢ HasEigenvalue T
    (↑(⨆ (x : { x : E // x ≠ 0 }),
          HDiv.hDiv (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) (↑x : E), (↑x : E)⟫_𝕜 : ℝ)
            (HPow.hPow (β := ℕ) ‖(↑x : E)‖ 2)) :
      𝕜)
have hx₀ : ‖x₀‖ = ‖x‖
Tactic: have hx₀ : ‖x₀‖ = ‖x‖ := by simpa using hx₀'
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (hypothesis)
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‖
⊢ HasEigenvalue T
    (↑(⨆ (x : { x : E // x ≠ 0 }),
          HDiv.hDiv (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) (↑x : E), (↑x : E)⟫_𝕜 : ℝ)
            (HPow.hPow (β := ℕ) ‖(↑x : E)‖ 2)) :
      𝕜)
have this₁ : 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₀
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (hypothesis)
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
have this₁ : ‖x₀‖ ≠ 0
Tactic: have : ‖x₀‖ ≠ 0 := by simp only [hx₀, norm_eq_zero, hx, Ne, not_false_iff]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (hypothesis)
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₀
⊢ HasEigenvalue T
    (↑(⨆ (x : { x : E // x ≠ 0 }),
          HDiv.hDiv (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) (↑x : E), (↑x : E)⟫_𝕜 : ℝ)
            (HPow.hPow (β := ℕ) ‖(↑x : E)‖ 2)) :
      𝕜)
have hx₀_ne : 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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (hypothesis)
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
⊢ HasEigenvalue T
    (↑(⨅ (x : { x : E // x ≠ 0 }),
          HDiv.hDiv (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) (↑x : E), (↑x : E)⟫_𝕜 : ℝ)
            (HPow.hPow (β := ℕ) ‖(↑x : E)‖ 2)) :
      𝕜)
have this : ProperSpace E
Tactic: haveI := FiniteDimensional.proper_rclike 𝕜 E
-- 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
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
⊢ HasEigenvalue T
    (↑(⨅ (x : { x : E // x ≠ 0 }),
          HDiv.hDiv (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) (↑x : E), (↑x : E)⟫_𝕜 : ℝ)
            (HPow.hPow (β := ℕ) ‖(↑x : E)‖ 2)) :
      𝕜)
have 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)) :
      𝕜)
Tactic: obtain ⟨x, hx⟩ : ∃ x : E, x ≠ 0 := exists_ne 0
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (hypothesis)
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
⊢ HasEigenvalue T
    (↑(⨅ (x : { x : E // x ≠ 0 }),
          HDiv.hDiv (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) (↑x : E), (↑x : E)⟫_𝕜 : ℝ)
            (HPow.hPow (β := ℕ) ‖(↑x : E)‖ 2)) :
      𝕜)
have H₁ : IsCompact.{u_2} (X := E) (sphere 0 ‖x‖)
Tactic: have H₁ : IsCompact (sphere (0 : E) ‖x‖) := isCompact_sphere _ _
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (hypothesis)
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‖)
⊢ HasEigenvalue T
    (↑(⨅ (x : { x : E // x ≠ 0 }),
          HDiv.hDiv (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) (↑x : E), (↑x : E)⟫_𝕜 : ℝ)
            (HPow.hPow (β := ℕ) ‖(↑x : E)‖ 2)) :
      𝕜)
have H₂ : Set.Nonempty.{u_2} (α := E) (sphere 0 ‖x‖)
Tactic: have H₂ : (sphere (0 : E) ‖x‖).Nonempty := ⟨x, by simp⟩
-- 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
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‖)
⊢ HasEigenvalue T
    (↑(⨅ (x : { x : E // x ≠ 0 }),
          HDiv.hDiv (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) (↑x : E), (↑x : E)⟫_𝕜 : ℝ)
            (HPow.hPow (β := ℕ) ‖(↑x : E)‖ 2)) :
      𝕜)
have 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)) :
      𝕜)
Tactic: obtain ⟨x₀, hx₀', hTx₀⟩ :=
    H₁.exists_isMinOn H₂ T'.val.reApplyInnerSelf_continuous.continuousOn
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (hypothesis)
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₀
⊢ HasEigenvalue T
    (↑(⨅ (x : { x : E // x ≠ 0 }),
          HDiv.hDiv (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) (↑x : E), (↑x : E)⟫_𝕜 : ℝ)
            (HPow.hPow (β := ℕ) ‖(↑x : E)‖ 2)) :
      𝕜)
have hx₀ : ‖x₀‖ = ‖x‖
Tactic: have hx₀ : ‖x₀‖ = ‖x‖ := by simpa using hx₀'
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (hypothesis)
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‖
⊢ HasEigenvalue T
    (↑(⨅ (x : { x : E // x ≠ 0 }),
          HDiv.hDiv (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) (↑x : E), (↑x : E)⟫_𝕜 : ℝ)
            (HPow.hPow (β := ℕ) ‖(↑x : E)‖ 2)) :
      𝕜)
have this₁ : 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₀
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (hypothesis)
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
have this₁ : ‖x₀‖ ≠ 0
Tactic: have : ‖x₀‖ ≠ 0 := by simp only [hx₀, norm_eq_zero, hx, Ne, not_false_iff]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (hypothesis)
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₀
⊢ HasEigenvalue T
    (↑(⨅ (x : { x : E // x ≠ 0 }),
          HDiv.hDiv (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) (↑x : E), (↑x : E)⟫_𝕜 : ℝ)
            (HPow.hPow (β := ℕ) ‖(↑x : E)‖ 2)) :
      𝕜)
have hx₀_ne : 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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Reproducing (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
X : Type u_2
V : Type u_3
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
H : Type u_4
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
inst_5 : RKHS 𝕜 H X V
x : X
⊢ Continuous.{u_4, u_3} (Y := V) fun (f : H) ↦ (f : (a : X) → V) x
have simp_rw : Continuous.{u_4, u_3} (Y := V) fun (f : H) ↦ (coeCLM 𝕜 : (a : H) → X → V) f x
Tactic: simp_rw [← coeCLM_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Reproducing (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
X : Type u_2
V : Type u_3
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
H : Type u_4
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
inst_5 : RKHS 𝕜 H X V
inst_6 : CompleteSpace H
inst_7 : CompleteSpace V
x : X
⊢ norm (E := V →L[𝕜] V) (kernel H x x) = HPow.hPow (β := ℕ) (norm (E := V →L[𝕜] H) (kerFun H x)) 2
have rw : norm (E := V →L[𝕜] V) (kernel H x x) = norm (E := V →L[𝕜] H) (kerFun H x) * norm (E := V →L[𝕜] H) (kerFun H x)
Tactic: rw [sq, ← ContinuousLinearMap.norm_adjoint_comp_self, kernel_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Reproducing (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
X : Type u_2
V : Type u_3
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
H : Type u_4
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
inst_5 : RKHS 𝕜 H X V
inst_6 : CompleteSpace H
inst_7 : CompleteSpace V
x : X
rw : norm (E := V →L[𝕜] V) (kernel H x x) = norm (E := V →L[𝕜] H) (kerFun H x) * norm (E := V →L[𝕜] H) (kerFun H x)
⊢ norm (E := V →L[𝕜] V) (kernel H x x) = HPow.hPow (β := ℕ) (norm (E := V →L[𝕜] H) (kerFun H x)) 2
have rw₁ : norm (E := V →L[𝕜] V) (kernel H x x) =
  norm (E := V →L[𝕜] V) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] H) → H →L[𝕜] V) (kerFun H x)) (kerFun H x))
Tactic: rw [sq, ← ContinuousLinearMap.norm_adjoint_comp_self, kernel_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Reproducing (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
X : Type u_2
V : Type u_3
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
H : Type u_4
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
inst_5 : RKHS 𝕜 H X V
inst_6 : CompleteSpace H
inst_7 : CompleteSpace V
x : X
rw : norm (E := V →L[𝕜] V) (kernel H x x) = norm (E := V →L[𝕜] H) (kerFun H x) * norm (E := V →L[𝕜] H) (kerFun H x)
rw₁ :
  norm (E := V →L[𝕜] V) (kernel H x x) =
    norm (E := V →L[𝕜] V)
      (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] H) → H →L[𝕜] V) (kerFun H x)) (kerFun H x))
⊢ norm (E := V →L[𝕜] V) (kernel H x x) = HPow.hPow (β := ℕ) (norm (E := V →L[𝕜] H) (kerFun H x)) 2
have rw₂ : norm (E := V →L[𝕜] V) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] H) → H →L[𝕜] V) (kerFun H x)) (kerFun H x)) =
  norm (E := V →L[𝕜] V) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] H) → H →L[𝕜] V) (kerFun H x)) (kerFun H x))
Tactic: rw [sq, ← ContinuousLinearMap.norm_adjoint_comp_self, kernel_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Reproducing (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
X : Type u_2
V : Type u_3
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
H : Type u_4
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
inst_5 : RKHS 𝕜 H X V
inst_6 : CompleteSpace H
inst_7 : CompleteSpace V
x : X
⊢ norm (E := V →L[𝕜] H) (kerFun H x) = √(norm (E := V →L[𝕜] V) (kernel H x x))
have rw : norm (E := V →L[𝕜] H) (kerFun H x) = √(HPow.hPow (β := ℕ) (norm (E := V →L[𝕜] H) (kerFun H x)) 2)
Tactic: rw [norm_kernel_eq_norm_kerFun_sq, Real.sqrt_sq (norm_nonneg _)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Reproducing (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
X : Type u_2
V : Type u_3
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
H : Type u_4
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
inst_5 : RKHS 𝕜 H X V
inst_6 : CompleteSpace H
inst_7 : CompleteSpace V
x : X
rw : norm (E := V →L[𝕜] H) (kerFun H x) = √(HPow.hPow (β := ℕ) (norm (E := V →L[𝕜] H) (kerFun H x)) 2)
⊢ norm (E := V →L[𝕜] H) (kerFun H x) = √(norm (E := V →L[𝕜] V) (kernel H x x))
have rw₁ : norm (E := V →L[𝕜] H) (kerFun H x) = norm (E := V →L[𝕜] H) (kerFun H x)
Tactic: rw [norm_kernel_eq_norm_kerFun_sq, Real.sqrt_sq (norm_nonneg _)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Reproducing (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
X : Type u_2
V : Type u_3
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
H : Type u_4
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
inst_5 : RKHS 𝕜 H X V
inst_6 : CompleteSpace H
inst_7 : CompleteSpace V
x y : X
⊢ norm (E := V →L[𝕜] V) (kernel H x y) ≤
    √(norm (E := V →L[𝕜] V) (kernel H x x)) * √(norm (E := V →L[𝕜] V) (kernel H y y))
have grw : norm (E := H →L[𝕜] V) ((adjoint : (a : V →L[𝕜] H) → H →L[𝕜] V) (kerFun H x) : H →L[𝕜] V) *
    norm (E := V →L[𝕜] H) (kerFun H y) ≤
  √(norm (E := V →L[𝕜] V) (kernel H x x)) * √(norm (E := V →L[𝕜] V) (kernel H y y))
Tactic: grw [kernel_apply, opNorm_comp_le]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Reproducing (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
X : Type u_2
V : Type u_3
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
H : Type u_4
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
inst_5 : RKHS 𝕜 H X V
inst_6 : CompleteSpace H
inst_7 : CompleteSpace V
x y : X
⊢ HPow.hPow (β := ℕ) (norm (E := V →L[𝕜] V) (kernel H x y)) 2 ≤
    norm (E := V →L[𝕜] V) (kernel H x x) * norm (E := V →L[𝕜] V) (kernel H y y)
have grw : HPow.hPow (β := ℕ) (√(norm (E := V →L[𝕜] V) (kernel H x x)) * √(norm (E := V →L[𝕜] V) (kernel H y y))) 2 ≤
  norm (E := V →L[𝕜] V) (kernel H x x) * norm (E := V →L[𝕜] V) (kernel H y y)
Tactic: grw [norm_kernel_le]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Reproducing (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
X : Type u_2
V : Type u_3
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
H : Type u_4
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
inst_5 : RKHS 𝕜 H X V
inst_6 : CompleteSpace H
inst_7 : CompleteSpace V
⊢ Eq.{u_4 + 1} (α := Submodule 𝕜 H)
    (topologicalClosure (span 𝕜 {x : H | ∃ (x_1 : X) (v : V), (kerFun H x_1 : (a : V) → H) v = x})) ⊤
have refine : ∀ (f : H)
  (fin :
    Membership.mem (γ := Submodule 𝕜 H)
      (topologicalClosure (span 𝕜 {x : H | ∃ (x_1 : X) (v : V), (kerFun H x_1 : (a : V) → H) v = x}))ᗮ f)
  (x : X), Eq.{u_3 + 1} (α := V) ((f : (a : X) → V) x : V) ((0 : (a : X) → V) x : V)
Tactic: refine (orthogonal_eq_bot_iff.mp ((Submodule.eq_bot_iff _).mpr fun f fin ↦ DFunLike.ext f 0 ?_))