awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : CompleteSpace E
h : Kᗮᗮ = ⊤
mp : Kᗮᗮᗮ = ⊥
mp₁ : Eq.{u_2 + 1} (α := Submodule 𝕜 E) ⊤ᗮ ⊥
⊢ Kᗮ = ⊥
have mp₂ : Eq.{u_2 + 1} (α := Submodule 𝕜 E) ⊥ ⊥
Tactic: rw [← Submodule.triorthogonal_eq_orthogonal, h, Submodule.top_orthogonal_eq_bot]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : CompleteSpace E
h : Kᗮ = ⊥
⊢ Kᗮᗮ = ⊤
have mpr : Eq.{u_2 + 1} (α := Submodule 𝕜 E) ⊥ᗮ ⊤
Tactic: rw [h, Submodule.bot_orthogonal_eq_top]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : CompleteSpace E
h : Kᗮ = ⊥
mpr : Eq.{u_2 + 1} (α := Submodule 𝕜 E) ⊥ᗮ ⊤
⊢ Kᗮᗮ = ⊤
have mpr₁ : Eq.{u_2 + 1} (α := Submodule 𝕜 E) ⊤ ⊤
Tactic: rw [h, Submodule.bot_orthogonal_eq_top]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
x : E
⊢ Eq (α := ↥K) ((K.orthogonalProjection : (a : E) → ↥K) x : ↥K) ((K.projectionOnto Kᗮ ⋯ : (a : E) → ↥K) x : ↥K)
have this : IsCompl K Kᗮ
Tactic: have : IsCompl K Kᗮ := Submodule.isCompl_orthogonal_of_hasOrthogonalProjection
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
x : E
this : IsCompl K Kᗮ
| ((K.orthogonalProjection : (a : E) → ↥K) x : ↥K)
have rw : ((K.orthogonalProjection : (a : E) → ↥K)
    (HAdd.hAdd (α := E) (β := E) ((K.projection Kᗮ this : (a : E) → E) x : E)
      ((Kᗮ.projection K sorry : (a : E) → E) x : E)) :
  ↥K)
Tactic: rw [← projection_add_projection_eq_self this x]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
x : E
this : IsCompl K Kᗮ
⊢ Eq (α := ↥K) ((K.orthogonalProjection : (a : E) → ↥K) x : ↥K) ((K.projectionOnto Kᗮ ⋯ : (a : E) → ↥K) x : ↥K)
have conv_lhs : Eq (α := ↥K)
  ((K.orthogonalProjection : (a : E) → ↥K)
      (HAdd.hAdd (α := E) (β := E) ((K.projection Kᗮ this : (a : E) → E) x : E)
        ((Kᗮ.projection K sorry : (a : E) → E) x : E)) :
    ↥K)
  ((K.projectionOnto Kᗮ sorry : (a : E) → ↥K) x : ↥K)
Tactic: conv_lhs => rw [← projection_add_projection_eq_self this x]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
x : E
this : IsCompl K Kᗮ
⊢ Eq (α := ↥K)
    ((K.orthogonalProjection : (a : E) → ↥K)
        (HAdd.hAdd (α := E) (β := E) ((K.projection Kᗮ this : (a : E) → E) x : E)
          ((Kᗮ.projection K ⋯ : (a : E) → E) x : E)) :
      ↥K)
    ((K.projectionOnto Kᗮ ⋯ : (a : E) → ↥K) x : ↥K)
have simp_rw : Eq (α := ↥K)
  ((K.orthogonalProjection : (a : E) → ↥K)
      (HAdd.hAdd (α := E) (↑((K.projectionOnto Kᗮ this : (a : E) → ↥K) x) : E)
        (↑((Kᗮ.projectionOnto K sorry : (a : E) → ↥Kᗮ) x) : E)) :
    ↥K)
  ((K.projectionOnto Kᗮ sorry : (a : E) → ↥K) x : ↥K)
Tactic: simp_rw [projection_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
x : E
this : IsCompl K Kᗮ
⊢ Eq (α := ↥K)
    ((K.orthogonalProjection : (a : E) → ↥K)
        (HAdd.hAdd (α := E) (↑((K.projectionOnto Kᗮ this : (a : E) → ↥K) x) : E)
          (↑((Kᗮ.projectionOnto K ⋯ : (a : E) → ↥Kᗮ) x) : E)) :
      ↥K)
    ((K.projectionOnto Kᗮ ⋯ : (a : E) → ↥K) x : ↥K)
have rw : HAdd.hAdd (α := ↥K) ((K.orthogonalProjection : (a : E) → ↥K) (↑((K.projectionOnto Kᗮ this : (a : E) → ↥K) x) : E))
    ((K.orthogonalProjection : (a : E) → ↥K) (↑((Kᗮ.projectionOnto K sorry : (a : E) → ↥Kᗮ) x) : E)) =
  (K.projectionOnto Kᗮ sorry : (a : E) → ↥K) x
Tactic: rw [map_add, orthogonalProjection_mem_subspace_eq_self,
    orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero (Submodule.coe_mem _), add_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
x : E
this : IsCompl K Kᗮ
rw :
  HAdd.hAdd (α := ↥K) ((K.orthogonalProjection : (a : E) → ↥K) (↑((K.projectionOnto Kᗮ this : (a : E) → ↥K) x) : E))
      ((K.orthogonalProjection : (a : E) → ↥K) (↑((Kᗮ.projectionOnto K ⋯ : (a : E) → ↥Kᗮ) x) : E)) =
    (K.projectionOnto Kᗮ ⋯ : (a : E) → ↥K) x
⊢ Eq (α := ↥K)
    ((K.orthogonalProjection : (a : E) → ↥K)
        (HAdd.hAdd (α := E) (↑((K.projectionOnto Kᗮ this : (a : E) → ↥K) x) : E)
          (↑((Kᗮ.projectionOnto K ⋯ : (a : E) → ↥Kᗮ) x) : E)) :
      ↥K)
    ((K.projectionOnto Kᗮ ⋯ : (a : E) → ↥K) x : ↥K)
have rw₁ : HAdd.hAdd (α := ↥K) (β := ↥K) ((K.projectionOnto Kᗮ this : (a : E) → ↥K) x : ↥K)
    ((K.orthogonalProjection : (a : E) → ↥K) (↑((Kᗮ.projectionOnto K sorry : (a : E) → ↥Kᗮ) x) : E) : ↥K) =
  (K.projectionOnto Kᗮ sorry : (a : E) → ↥K) x
Tactic: rw [map_add, orthogonalProjection_mem_subspace_eq_self,
    orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero (Submodule.coe_mem _), add_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
x : E
this : IsCompl K Kᗮ
rw :
  HAdd.hAdd (α := ↥K) ((K.orthogonalProjection : (a : E) → ↥K) (↑((K.projectionOnto Kᗮ this : (a : E) → ↥K) x) : E))
      ((K.orthogonalProjection : (a : E) → ↥K) (↑((Kᗮ.projectionOnto K ⋯ : (a : E) → ↥Kᗮ) x) : E)) =
    (K.projectionOnto Kᗮ ⋯ : (a : E) → ↥K) x
rw₁ :
  HAdd.hAdd (α := ↥K) (β := ↥K) ((K.projectionOnto Kᗮ this : (a : E) → ↥K) x : ↥K)
      ((K.orthogonalProjection : (a : E) → ↥K) (↑((Kᗮ.projectionOnto K ⋯ : (a : E) → ↥Kᗮ) x) : E) : ↥K) =
    (K.projectionOnto Kᗮ ⋯ : (a : E) → ↥K) x
⊢ Eq (α := ↥K)
    ((K.orthogonalProjection : (a : E) → ↥K)
        (HAdd.hAdd (α := E) (↑((K.projectionOnto Kᗮ this : (a : E) → ↥K) x) : E)
          (↑((Kᗮ.projectionOnto K ⋯ : (a : E) → ↥Kᗮ) x) : E)) :
      ↥K)
    ((K.projectionOnto Kᗮ ⋯ : (a : E) → ↥K) x : ↥K)
have rw₂ : HAdd.hAdd (α := ↥K) (β := ↥K) ((K.projectionOnto Kᗮ this : (a : E) → ↥K) x : ↥K) (0 : ↥K) =
  (K.projectionOnto Kᗮ sorry : (a : E) → ↥K) x
Tactic: rw [map_add, orthogonalProjection_mem_subspace_eq_self,
    orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero (Submodule.coe_mem _), add_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
x : E
this : IsCompl K Kᗮ
rw :
  HAdd.hAdd (α := ↥K) ((K.orthogonalProjection : (a : E) → ↥K) (↑((K.projectionOnto Kᗮ this : (a : E) → ↥K) x) : E))
      ((K.orthogonalProjection : (a : E) → ↥K) (↑((Kᗮ.projectionOnto K ⋯ : (a : E) → ↥Kᗮ) x) : E)) =
    (K.projectionOnto Kᗮ ⋯ : (a : E) → ↥K) x
rw₁ :
  HAdd.hAdd (α := ↥K) (β := ↥K) ((K.projectionOnto Kᗮ this : (a : E) → ↥K) x : ↥K)
      ((K.orthogonalProjection : (a : E) → ↥K) (↑((Kᗮ.projectionOnto K ⋯ : (a : E) → ↥Kᗮ) x) : E) : ↥K) =
    (K.projectionOnto Kᗮ ⋯ : (a : E) → ↥K) x
rw₂ :
  HAdd.hAdd (α := ↥K) (β := ↥K) ((K.projectionOnto Kᗮ this : (a : E) → ↥K) x : ↥K) (0 : ↥K) =
    (K.projectionOnto Kᗮ ⋯ : (a : E) → ↥K) x
⊢ Eq (α := ↥K)
    ((K.orthogonalProjection : (a : E) → ↥K)
        (HAdd.hAdd (α := E) (↑((K.projectionOnto Kᗮ this : (a : E) → ↥K) x) : E)
          (↑((Kᗮ.projectionOnto K ⋯ : (a : E) → ↥Kᗮ) x) : E)) :
      ↥K)
    ((K.projectionOnto Kᗮ ⋯ : (a : E) → ↥K) x : ↥K)
have rw₃ : Eq (α := ↥K) ((K.projectionOnto Kᗮ this : (a : E) → ↥K) x : ↥K) ((K.projectionOnto Kᗮ sorry : (a : E) → ↥K) x : ↥K)
Tactic: rw [map_add, orthogonalProjection_mem_subspace_eq_self,
    orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero (Submodule.coe_mem _), add_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : ClosedSubmodule 𝕜 E
inst_3 : (↑K : Submodule 𝕜 E).HasOrthogonalProjection
⊢ Kᗮᗮ = K
have carrier : ∀ (x : E), x ∈ (↑Kᗮᗮ : Submodule 𝕜 E).carrier ↔ x ∈ (↑K : Submodule 𝕜 E).carrier
Tactic: ext x
-- 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
x : E
c : 𝕜
hc : c ≠ 0
⊢ T.rayleighQuotient (c • x) = T.rayleighQuotient x
have pos : ∀ (hx : x = 0), T.rayleighQuotient (c • x) = T.rayleighQuotient x
Tactic: by_cases hx : x = 0
-- 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
x : E
c : 𝕜
hc : c ≠ 0
pos : ∀ (hx : x = 0), T.rayleighQuotient (c • x) = T.rayleighQuotient x
⊢ T.rayleighQuotient (c • x) = T.rayleighQuotient x
have neg : ∀ (hx : ¬x = 0), T.rayleighQuotient (c • x) = T.rayleighQuotient x
Tactic: by_cases hx : x = 0
-- 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
r : ℝ
hr : 0 < r
⊢ T.rayleighQuotient '' {0}ᶜ = T.rayleighQuotient '' sphere 0 r
have h : ∀ (a : ℝ), a ∈ T.rayleighQuotient '' {0}ᶜ ↔ a ∈ T.rayleighQuotient '' sphere 0 r
Tactic: ext a
-- 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
r : ℝ
hr : 0 < r
a : ℝ
⊢ a ∈ T.rayleighQuotient '' {0}ᶜ ↔ a ∈ T.rayleighQuotient '' sphere 0 r
have h : a ∈ T.rayleighQuotient '' {0}ᶜ → a ∈ T.rayleighQuotient '' sphere 0 r
Tactic: constructor
-- 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
r : ℝ
hr : 0 < r
a : ℝ
h : a ∈ T.rayleighQuotient '' {0}ᶜ → a ∈ T.rayleighQuotient '' sphere 0 r
⊢ a ∈ T.rayleighQuotient '' {0}ᶜ ↔ a ∈ T.rayleighQuotient '' sphere 0 r
have h₁ : a ∈ T.rayleighQuotient '' sphere 0 r → a ∈ T.rayleighQuotient '' {0}ᶜ
Tactic: constructor
-- 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
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
a : ℝ
x : E
hx : x ≠ 0
hxT : T.rayleighQuotient x = a
c : 𝕜 := HMul.hMul (α := 𝕜) (↑‖x‖⁻¹ : 𝕜) (↑r : 𝕜)
⊢ a ∈ T.rayleighQuotient '' sphere 0 r
have this : c ≠ 0
Tactic: have : c ≠ 0 := by simp [c, hx, hr.ne']
-- 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
r : ℝ
hr : 0 < r
a : ℝ
x : E
hx : x ≠ 0
hxT : T.rayleighQuotient x = a
c : 𝕜 := HMul.hMul (α := 𝕜) (↑‖x‖⁻¹ : 𝕜) (↑r : 𝕜)
this : c ≠ 0
⊢ a ∈ T.rayleighQuotient '' sphere 0 r
have h : Membership.mem (γ := Set E) (sphere 0 r) (c • x)
Tactic: refine ⟨c • x, ?_, ?_⟩
-- 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
r : ℝ
hr : 0 < r
a : ℝ
x : E
hx : x ≠ 0
hxT : T.rayleighQuotient x = a
c : 𝕜 := HMul.hMul (α := 𝕜) (↑‖x‖⁻¹ : 𝕜) (↑r : 𝕜)
this : c ≠ 0
h : Membership.mem (γ := Set E) (sphere 0 r) (c • x)
⊢ a ∈ T.rayleighQuotient '' sphere 0 r
have h₁ : T.rayleighQuotient (c • x) = a
Tactic: refine ⟨c • x, ?_, ?_⟩
-- 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
x : E
⊢ |T.rayleighQuotient x| ≤ ‖T‖
have grw : ‖T‖ * (HPow.hPow (β := ℕ) ‖x‖ 2 / HPow.hPow (β := ℕ) ‖x‖ 2) ≤ ‖T‖
Tactic: grw [rayleighQuotient, reApplyInnerSelf_apply, abs_div, abs_sq, abs_re_le_norm,
    norm_inner_le_norm, le_opNorm, mul_assoc, ← sq, mul_div_assoc]
-- 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
T : E →L[𝕜] E
hT : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)
M : ℝ := ⨆ (x : E), |T.rayleighQuotient x|
⊢ ‖T‖ = M
have nonneg : 0 ≤ M
Tactic: have nonneg : 0 ≤ M := le_ciSup_of_le T.bddAbove_rayleighQuotient 0 (abs_nonneg _)
-- 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
T : E →L[𝕜] E
hT : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)
M : ℝ := ⨆ (x : E), |T.rayleighQuotient x|
nonneg : 0 ≤ M
x : E
⊢ |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
have hM : |T.rayleighQuotient x| ≤ M
Tactic: have hM : |T.rayleighQuotient x| ≤ M := le_ciSup T.bddAbove_rayleighQuotient x
-- 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
hT : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)
M : ℝ := ⨆ (x : E), |T.rayleighQuotient x|
nonneg : 0 ≤ M
x : E
hM : |T.rayleighQuotient x| ≤ M
⊢ |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
have pos : ∀ (hx : 0 < HPow.hPow (β := ℕ) ‖x‖ 2), |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
Tactic: by_cases hx : 0 < ‖x‖ ^ 2
-- 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
hT : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)
M : ℝ := ⨆ (x : E), |T.rayleighQuotient x|
nonneg : 0 ≤ M
x : E
hM : |T.rayleighQuotient x| ≤ M
pos :
  ∀ (hx : 0 < HPow.hPow (β := ℕ) ‖x‖ 2), |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
⊢ |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
have neg : ∀ (hx : ¬0 < HPow.hPow (β := ℕ) ‖x‖ 2), |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
Tactic: by_cases hx : 0 < ‖x‖ ^ 2
-- 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
hT : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)
M : ℝ := ⨆ (x : E), |T.rayleighQuotient x|
nonneg : 0 ≤ M
x : E
hM : |T.rayleighQuotient x| ≤ M
hx : 0 < HPow.hPow (β := ℕ) ‖x‖ 2
⊢ |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
have pos : ∀ (hM : |T.reApplyInnerSelf x / HPow.hPow (β := ℕ) ‖x‖ 2| ≤ M) (hx : 0 < HPow.hPow (β := ℕ) ‖x‖ 2),
  |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
Tactic: rwa [rayleighQuotient, abs_div, abs_sq, reApplyInnerSelf, div_le_iff₀ hx] at hM
Cleared hypotheses: hM, 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
T : E →L[𝕜] E
hT : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)
M : ℝ := ⨆ (x : E), |T.rayleighQuotient x|
nonneg : 0 ≤ M
x : E
hM : |T.rayleighQuotient x| ≤ M
hx : 0 < HPow.hPow (β := ℕ) ‖x‖ 2
pos :
  ∀ (hM : |T.reApplyInnerSelf x / HPow.hPow (β := ℕ) ‖x‖ 2| ≤ M) (hx : 0 < HPow.hPow (β := ℕ) ‖x‖ 2),
    |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
⊢ |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
have pos₁ : ∀ (hM : |T.reApplyInnerSelf x| / |HPow.hPow (β := ℕ) ‖x‖ 2| ≤ M) (hx : 0 < HPow.hPow (β := ℕ) ‖x‖ 2),
  |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
Tactic: rwa [rayleighQuotient, abs_div, abs_sq, reApplyInnerSelf, div_le_iff₀ hx] at hM
Cleared hypotheses: hM, 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
T : E →L[𝕜] E
hT : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)
M : ℝ := ⨆ (x : E), |T.rayleighQuotient x|
nonneg : 0 ≤ M
x : E
hM : |T.rayleighQuotient x| ≤ M
hx : 0 < HPow.hPow (β := ℕ) ‖x‖ 2
pos :
  ∀ (hM : |T.reApplyInnerSelf x / HPow.hPow (β := ℕ) ‖x‖ 2| ≤ M) (hx : 0 < HPow.hPow (β := ℕ) ‖x‖ 2),
    |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
pos₁ :
  ∀ (hM : |T.reApplyInnerSelf x| / |HPow.hPow (β := ℕ) ‖x‖ 2| ≤ M) (hx : 0 < HPow.hPow (β := ℕ) ‖x‖ 2),
    |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
⊢ |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
have pos₂ : ∀ (hM : |T.reApplyInnerSelf x| / HPow.hPow (β := ℕ) ‖x‖ 2 ≤ M) (hx : 0 < HPow.hPow (β := ℕ) ‖x‖ 2),
  |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
Tactic: rwa [rayleighQuotient, abs_div, abs_sq, reApplyInnerSelf, div_le_iff₀ hx] at hM
Cleared hypotheses: hM, 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
T : E →L[𝕜] E
hT : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)
M : ℝ := ⨆ (x : E), |T.rayleighQuotient x|
nonneg : 0 ≤ M
x : E
hM : |T.rayleighQuotient x| ≤ M
hx : 0 < HPow.hPow (β := ℕ) ‖x‖ 2
pos :
  ∀ (hM : |T.reApplyInnerSelf x / HPow.hPow (β := ℕ) ‖x‖ 2| ≤ M) (hx : 0 < HPow.hPow (β := ℕ) ‖x‖ 2),
    |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
pos₁ :
  ∀ (hM : |T.reApplyInnerSelf x| / |HPow.hPow (β := ℕ) ‖x‖ 2| ≤ M) (hx : 0 < HPow.hPow (β := ℕ) ‖x‖ 2),
    |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
pos₂ :
  ∀ (hM : |T.reApplyInnerSelf x| / HPow.hPow (β := ℕ) ‖x‖ 2 ≤ M) (hx : 0 < HPow.hPow (β := ℕ) ‖x‖ 2),
    |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
⊢ |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
have pos₃ : ∀ (hM : HDiv.hDiv (α := ℝ) (|(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| : ℝ) (HPow.hPow (β := ℕ) ‖x‖ 2) ≤ M)
  (hx : 0 < HPow.hPow (β := ℕ) ‖x‖ 2), |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
Tactic: rwa [rayleighQuotient, abs_div, abs_sq, reApplyInnerSelf, div_le_iff₀ hx] at hM
Cleared hypotheses: hM, 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
T : E →L[𝕜] E
hT : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)
M : ℝ := ⨆ (x : E), |T.rayleighQuotient x|
nonneg : 0 ≤ M
x : E
hM : |T.rayleighQuotient x| ≤ M
hx : 0 < HPow.hPow (β := ℕ) ‖x‖ 2
pos :
  ∀ (hM : |T.reApplyInnerSelf x / HPow.hPow (β := ℕ) ‖x‖ 2| ≤ M) (hx : 0 < HPow.hPow (β := ℕ) ‖x‖ 2),
    |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
pos₁ :
  ∀ (hM : |T.reApplyInnerSelf x| / |HPow.hPow (β := ℕ) ‖x‖ 2| ≤ M) (hx : 0 < HPow.hPow (β := ℕ) ‖x‖ 2),
    |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
pos₂ :
  ∀ (hM : |T.reApplyInnerSelf x| / HPow.hPow (β := ℕ) ‖x‖ 2 ≤ M) (hx : 0 < HPow.hPow (β := ℕ) ‖x‖ 2),
    |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
pos₃ :
  ∀ (hM : HDiv.hDiv (α := ℝ) (|(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| : ℝ) (HPow.hPow (β := ℕ) ‖x‖ 2) ≤ M)
    (hx : 0 < HPow.hPow (β := ℕ) ‖x‖ 2), |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
⊢ |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
have pos₄ : ∀ (hM : |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2)
  (hx : 0 < HPow.hPow (β := ℕ) ‖x‖ 2), |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
Tactic: rwa [rayleighQuotient, abs_div, abs_sq, reApplyInnerSelf, div_le_iff₀ hx] at hM
Cleared hypotheses: hM, 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
T : E →L[𝕜] E
hT : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)
M : ℝ := ⨆ (x : E), |T.rayleighQuotient x|
nonneg : 0 ≤ M
⊢ ‖T‖ = M
have hM : ∀ (x : E), |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
Tactic: have hM x : |re ⟪T x, x⟫| ≤ M * ‖x‖ ^ 2 := by
    have hM : |T.rayleighQuotient x| ≤ M := le_ciSup T.bddAbove_rayleighQuotient x
    by_cases hx : 0 < ‖x‖ ^ 2
    · rwa [rayleighQuotient, abs_div, abs_sq, reApplyInnerSelf, div_le_iff₀ hx] at hM
    · simp_all
-- 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
hT : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)
M : ℝ := ⨆ (x : E), |T.rayleighQuotient x|
nonneg : 0 ≤ M
hM : ∀ (x : E), |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
⊢ ‖T‖ = M
have refine : ‖T‖ ≤ M
Tactic: refine le_antisymm ?_ (ciSup_le T.rayleighQuotient_le_norm)
-- 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
hT : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)
M : ℝ := ⨆ (x : E), |T.rayleighQuotient x|
nonneg : 0 ≤ M
hM : ∀ (x : E), |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
⊢ ‖T‖ ≤ M
have refine : ∀ (x y : E) (hx : ‖x‖ = 1) (hy : ‖y‖ = 1), (re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, y⟫_𝕜 ≤ M
Tactic: refine opNorm_le_of_re_inner_le nonneg fun x y hx hy ↦ ?_
-- 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
hT : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)
M : ℝ := ⨆ (x : E), |T.rayleighQuotient x|
nonneg : 0 ≤ M
hM : ∀ (x : E), |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
x y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ (re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, y⟫_𝕜 ≤ M
have transitivity : (re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, y⟫_𝕜 ≤ M * (HPow.hPow (β := ℕ) ‖x + y‖ 2 + HPow.hPow (β := ℕ) ‖x - y‖ 2) / 4
Tactic: transitivity M * (‖x + y‖ ^ 2 + ‖x - y‖ ^ 2) / 4