awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₀
H : IsLocalExtrOn T.reApplyInnerSelf {x : F | HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) ‖x₀‖ 2} x₀
⊢ ∃ (a : ℝ) (b : ℝ), (a, b) ≠ 0 ∧ a • x₀ + HSMul.hSMul (β := F) b ((T : (a : F) → F) x₀ : F) = 0
have 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
Tactic: obtain ⟨a, b, h₁, h₂⟩ :=
    IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt_1d H (hasStrictFDerivAt_norm_sq x₀)
      (hT.isSymmetric.hasStrictFDerivAt_reApplyInnerSelf x₀)
-- 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₀
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
have refine : a • x₀ + HSMul.hSMul (β := F) b ((T : (a : F) → F) x₀ : F) = 0
Tactic: refine ⟨a, b, h₁, ?_⟩
-- 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₀
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 • x₀ + HSMul.hSMul (β := F) b ((T : (a : F) → F) x₀ : F) = 0
have 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)
Tactic: apply (InnerProductSpace.toDualMap ℝ F).injective
-- 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₀
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 (α := 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)
have 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
Tactic: simp only [LinearIsometry.map_add, LinearIsometry.map_zero]
-- 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₀
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
⊢ 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
have 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
Tactic: simp only [map_smulₛₗ _, RCLike.conj_to_real]
-- 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₀
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
⊢ 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
have 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
Tactic: change a • innerSL ℝ x₀ + b • innerSL ℝ (T x₀) = 0
-- 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₀
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
⊢ 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
have 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)
Tactic: apply smul_right_injective (F →L[ℝ] ℝ) (two_ne_zero : (2 : ℝ) ≠ 0)
-- 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₀
⊢ (T : (a : F) → F) x₀ = T.rayleighQuotient x₀ • x₀
have 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₀
Tactic: obtain ⟨a, b, h₁, h₂⟩ := hT.linearly_dependent_of_isLocalExtrOn 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₀
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₀
have pos : ∀ (hx₀ : x₀ = 0), (T : (a : F) → F) x₀ = T.rayleighQuotient x₀ • x₀
Tactic: by_cases hx₀ : x₀ = 0
-- 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₀
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₀
⊢ (T : (a : F) → F) x₀ = T.rayleighQuotient x₀ • x₀
have neg : ∀ (hx₀ : ¬x₀ = 0), (T : (a : F) → F) x₀ = T.rayleighQuotient x₀ • x₀
Tactic: by_cases hx₀ : x₀ = 0
-- 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₀
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₀
have pos : ∀ (hb : b = 0), (T : (a : F) → F) x₀ = T.rayleighQuotient x₀ • x₀
Tactic: by_cases hb : b = 0
-- 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₀
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₀
⊢ (T : (a : F) → F) x₀ = T.rayleighQuotient x₀ • x₀
have neg : ∀ (hb : ¬b = 0), (T : (a : F) → F) x₀ = T.rayleighQuotient x₀ • x₀
Tactic: by_cases hb : b = 0
-- 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 : ℝ
h₁ : (a, b) ≠ 0
h₂ : a • x₀ + HSMul.hSMul (β := F) b ((T : (a : F) → F) x₀ : F) = 0
hx₀ : ¬x₀ = 0
hb : b = 0
⊢ (T : (a : F) → F) x₀ = T.rayleighQuotient x₀ • x₀
have this : a ≠ 0
Tactic: have : a ≠ 0 := by simpa [hb] using h₁
-- 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₀
a b : ℝ
h₁ : (a, b) ≠ 0
h₂ : a • x₀ + HSMul.hSMul (β := F) b ((T : (a : F) → F) x₀ : F) = 0
hx₀ : ¬x₀ = 0
hb : b = 0
this : a ≠ 0
⊢ (T : (a : F) → F) x₀ = T.rayleighQuotient x₀ • x₀
have pos : x₀ = 0
Tactic: refine absurd ?_ hx₀
-- 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₀
a b : ℝ
h₁ : (a, b) ≠ 0
h₂ : a • x₀ + HSMul.hSMul (β := F) b ((T : (a : F) → F) x₀ : F) = 0
hx₀ : ¬x₀ = 0
hb : b = 0
this : a ≠ 0
⊢ x₀ = 0
have pos : Eq.{u_3 + 1} (α := F) ((fun (x : F) ↦ a • x) x₀) ((fun (x : F) ↦ a • x) 0)
Tactic: apply smul_right_injective F this
-- 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₀
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
⊢ HAdd.hAdd (α := F) ((T : (a : F) → F) x₀ : F) (HSMul.hSMul (β := F) b⁻¹ 0) -
      ((-b⁻¹ * a) • x₀ + b⁻¹ • (a • x₀ + HSMul.hSMul (β := F) b ((T : (a : F) → F) x₀ : F))) =
    0
have match_scalars : 1 - b⁻¹ * (b * 1) = 0
Tactic: match_scalars
-- 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₀
a b : ℝ
h₁ : (a, b) ≠ 0
h₂ : a • x₀ + HSMul.hSMul (β := F) b ((T : (a : F) → F) x₀ : F) = 0
hx₀ : ¬x₀ = 0
hb : ¬b = 0
match_scalars : 1 - b⁻¹ * (b * 1) = 0
⊢ HAdd.hAdd (α := F) ((T : (a : F) → F) x₀ : F) (HSMul.hSMul (β := F) b⁻¹ 0) -
      ((-b⁻¹ * a) • x₀ + b⁻¹ • (a • x₀ + HSMul.hSMul (β := F) b ((T : (a : F) → F) x₀ : F))) =
    0
have match_scalars₁ : -(-b⁻¹ * a * 1 + b⁻¹ * (a * 1)) = 0
Tactic: match_scalars
-- 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₀
a b : ℝ
h₁ : (a, b) ≠ 0
h₂ : a • x₀ + HSMul.hSMul (β := F) b ((T : (a : F) → F) x₀ : F) = 0
hx₀ : ¬x₀ = 0
hb : ¬b = 0
⊢ (T : (a : F) → F) x₀ = (-b⁻¹ * a) • x₀
have a₁ : HAdd.hAdd (α := F) ((T : (a : F) → F) x₀ : F) (HSMul.hSMul (β := F) b⁻¹ 0) -
    ((-b⁻¹ * a) • x₀ + b⁻¹ • (a • x₀ + HSMul.hSMul (β := F) b ((T : (a : F) → F) x₀ : F))) =
  0
Tactic: linear_combination (norm := match_scalars <;> field) b⁻¹ • h₂
-- 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 : ℝ
h₁ : (a, b) ≠ 0
h₂ : a • x₀ + HSMul.hSMul (β := F) b ((T : (a : F) → F) x₀ : F) = 0
hx₀ : ¬x₀ = 0
hb : ¬b = 0
⊢ (T : (a : F) → F) x₀ = T.rayleighQuotient x₀ • x₀
have hc : (T : (a : F) → F) x₀ = (-b⁻¹ * a) • x₀
Tactic: have hc : T x₀ = (-b⁻¹ * a) • x₀ := by
    linear_combination (norm := match_scalars <;> field) b⁻¹ • h₂
-- 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₀
a b : ℝ
h₁ : (a, b) ≠ 0
h₂ : a • x₀ + HSMul.hSMul (β := F) b ((T : (a : F) → F) x₀ : F) = 0
hx₀ : ¬x₀ = 0
hb : ¬b = 0
c : ℝ := -b⁻¹ * a
hc : (T : (a : F) → F) x₀ = c • x₀
⊢ (T : (a : F) → F) x₀ = T.rayleighQuotient x₀ • x₀
have h : T.rayleighQuotient x₀ = c
Tactic: convert! hc
-- 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 : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
⊢ HasEigenvector (↑T : E →ₗ[𝕜] E) (↑(T.rayleighQuotient x₀) : 𝕜) x₀
have refine : Membership.mem (γ := Submodule 𝕜 E)
  ((genEigenspace (↑T : E →ₗ[𝕜] E) (↑(T.rayleighQuotient x₀) : 𝕜) : (a : ℕ∞) → Submodule 𝕜 E) 1 : Submodule 𝕜 E) x₀
Tactic: refine ⟨?_, 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 : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
⊢ Membership.mem (γ := Submodule 𝕜 E)
    ((genEigenspace (↑T : E →ₗ[𝕜] E) (↑(T.rayleighQuotient x₀) : 𝕜) : (a : ℕ∞) → Submodule 𝕜 E) 1 : Submodule 𝕜 E) x₀
have rw : ((↑T : E →ₗ[𝕜] E) : (a : E) → E) x₀ = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(T.rayleighQuotient x₀) : 𝕜) x₀
Tactic: rw [Module.End.mem_eigenspace_iff]
-- 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 : IsMaxOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
⊢ HasEigenvector (↑T : E →ₗ[𝕜] E) (↑(⨆ (x : { x : E // x ≠ 0 }), T.rayleighQuotient (↑x : E)) : 𝕜) x₀
have h : ⨆ (x : { x : E // x ≠ 0 }), T.rayleighQuotient (↑x : E) = T.rayleighQuotient x₀
Tactic: convert! hT.hasEigenvector_of_isLocalExtrOn hx₀ (Or.inr hextr.localize)
-- 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 : IsMaxOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
⊢ ⨆ (x : { x : E // x ≠ 0 }), T.rayleighQuotient (↑x : E) = T.rayleighQuotient x₀
have hx₀' : 0 < ‖x₀‖
Tactic: have hx₀' : 0 < ‖x₀‖ := by simp [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 : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMaxOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀' : 0 < ‖x₀‖
⊢ ⨆ (x : { x : E // x ≠ 0 }), T.rayleighQuotient (↑x : E) = T.rayleighQuotient x₀
have hx₀'' : Membership.mem (γ := Set E) (sphere 0 ‖x₀‖) x₀
Tactic: have hx₀'' : x₀ ∈ sphere (0 : E) ‖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 : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMaxOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀' : 0 < ‖x₀‖
hx₀'' : Membership.mem (γ := Set E) (sphere 0 ‖x₀‖) x₀
⊢ ⨆ (x : { x : E // x ≠ 0 }), T.rayleighQuotient (↑x : E) = T.rayleighQuotient x₀
have h : ⨆ (x : (↑(sphere 0 ‖x₀‖) : Type u_2)), T.rayleighQuotient (↑x : E) = T.rayleighQuotient x₀
Tactic: rw [T.iSup_rayleigh_eq_iSup_rayleigh_sphere 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 : IsMaxOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀' : 0 < ‖x₀‖
hx₀'' : Membership.mem (γ := Set E) (sphere 0 ‖x₀‖) x₀
⊢ ⨆ (x : (↑(sphere 0 ‖x₀‖) : Type u_2)), T.rayleighQuotient (↑x : E) = T.rayleighQuotient x₀
have h : IsMaxOn T.rayleighQuotient (sphere 0 ‖x₀‖) x₀
Tactic: refine IsMaxOn.iSup_eq 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 : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMaxOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀' : 0 < ‖x₀‖
hx₀'' : Membership.mem (γ := Set E) (sphere 0 ‖x₀‖) x₀
x : E
hx : Membership.mem (γ := Set E) (sphere 0 ‖x₀‖) x
⊢ 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 : IsMaxOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀' : 0 < ‖x₀‖
hx₀'' : Membership.mem (γ := Set E) (sphere 0 ‖x₀‖) x₀
x : E
hx : Membership.mem (γ := Set E) (sphere 0 ‖x₀‖) x
this : ‖x‖ = ‖x₀‖
⊢ T.reApplyInnerSelf x / 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 : IsMaxOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀' : 0 < ‖x₀‖
hx₀'' : Membership.mem (γ := Set E) (sphere 0 ‖x₀‖) x₀
x : E
hx : Membership.mem (γ := Set E) (sphere 0 ‖x₀‖) x
this : ‖x‖ = ‖x₀‖
⊢ T.reApplyInnerSelf x / 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 (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₀
⊢ HasEigenvector (↑T : E →ₗ[𝕜] E) (↑(⨅ (x : { x : E // x ≠ 0 }), T.rayleighQuotient (↑x : E)) : 𝕜) x₀
have h : ⨅ (x : { x : E // x ≠ 0 }), T.rayleighQuotient (↑x : E) = T.rayleighQuotient x₀
Tactic: convert! hT.hasEigenvector_of_isLocalExtrOn hx₀ (Or.inl hextr.localize)
-- 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₀
⊢ ⨅ (x : { x : E // x ≠ 0 }), T.rayleighQuotient (↑x : E) = T.rayleighQuotient x₀
have hx₀' : 0 < ‖x₀‖
Tactic: have hx₀' : 0 < ‖x₀‖ := by simp [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 : 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₀‖
⊢ ⨅ (x : { x : E // x ≠ 0 }), T.rayleighQuotient (↑x : E) = T.rayleighQuotient x₀
have hx₀'' : Membership.mem (γ := Set E) (sphere 0 ‖x₀‖) x₀
Tactic: have hx₀'' : x₀ ∈ sphere (0 : E) ‖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 : 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 : { x : E // x ≠ 0 }), T.rayleighQuotient (↑x : E) = T.rayleighQuotient x₀
have h : ⨅ (x : (↑(sphere 0 ‖x₀‖) : Type u_2)), T.rayleighQuotient (↑x : E) = T.rayleighQuotient x₀
Tactic: rw [T.iInf_rayleigh_eq_iInf_rayleigh_sphere 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 : (↑(sphere 0 ‖x₀‖) : Type u_2)), T.rayleighQuotient (↑x : E) = T.rayleighQuotient x₀
have h : IsMinOn T.rayleighQuotient (sphere 0 ‖x₀‖) x₀
Tactic: refine IsMinOn.iInf_eq hx₀'' ?_