awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x y : E
this :
  Eq.{u_3 + 1} (α := 𝕜)
    (∑ x_1 : ι,
        (((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) : (a : E) → 𝕜)
          (HSMul.hSMul.{u_3, u_4, u_4} (α := (fun (x : ι) ↦ 𝕜) x_1) (β := E)
            (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) y) x_1) ((b : (a : ι) → E) x_1 : E)) :
      𝕜)
    ((((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) : (a : E) → 𝕜) y : 𝕜)
⊢ ∑ i : ι, ⟪x, (b : (a : ι) → E) i⟫ * ⟪(b : (a : ι) → E) i, y⟫ = ⟪x, y⟫
have h : ∀ (x_1 : ι),
  Membership.mem (γ := Finset ι) Finset.univ x_1 →
    ⟪x, (b : (a : ι) → E) x_1⟫ * ⟪(b : (a : ι) → E) x_1, y⟫ =
      (((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) : (a : E) → 𝕜)
        (HSMul.hSMul.{u_3, u_4, u_4} (α := (fun (x : ι) ↦ 𝕜) x_1) (β := E)
          (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) y) x_1) ((b : (a : ι) → E) x_1 : E))
Tactic: convert! this
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x y : E
this :
  Eq.{u_3 + 1} (α := 𝕜)
    (∑ x_2 : ι,
        (((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) : (a : E) → 𝕜)
          (HSMul.hSMul.{u_3, u_4, u_4} (α := (fun (x : ι) ↦ 𝕜) x_2) (β := E)
            (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) y) x_2) ((b : (a : ι) → E) x_2 : E)) :
      𝕜)
    ((((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) : (a : E) → 𝕜) y : 𝕜)
x_1 : ι
h : Membership.mem (γ := Finset ι) Finset.univ x_1
⊢ ⟪x, (b : (a : ι) → E) x_1⟫ * ⟪(b : (a : ι) → E) x_1, y⟫ =
    (((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) : (a : E) → 𝕜)
      (HSMul.hSMul.{u_3, u_4, u_4} (α := (fun (x : ι) ↦ 𝕜) x_1) (β := E)
        (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) y) x_1) ((b : (a : ι) → E) x_1 : E))
have h : ⟪(b : (a : ι) → E) x_1, y⟫ * ⟪x, (b : (a : ι) → E) x_1⟫ =
  HSMul.hSMul (β := 𝕜) ⟪(b : (a : ι) → E) x_1, y⟫
    ((((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) : (a : E) → 𝕜) ((b : (a : ι) → E) x_1 : E) : 𝕜)
Tactic: rw [map_smul, b.repr_apply_apply, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
⊢ ∑ i : ι, HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) i, x⟫‖ 2 = HPow.hPow (β := ℕ) ‖x‖ 2
have rw : ∑ i : ι, HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) i, x⟫‖ 2 =
  HPow.hPow (β := ℕ) (√(∑ x_1 : ι, (re : (a : 𝕜) → ℝ) (⟪x, (b : (a : ι) → E) x_1⟫ * ⟪(b : (a : ι) → E) x_1, x⟫))) 2
Tactic: rw [@norm_eq_sqrt_re_inner 𝕜, ← OrthonormalBasis.sum_inner_mul_inner b x x, map_sum]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
⊢ ∑ i : ι, HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) i, x⟫‖ 2 =
    HPow.hPow (β := ℕ) (√(∑ x_1 : ι, (re : (a : 𝕜) → ℝ) (⟪x, (b : (a : ι) → E) x_1⟫ * ⟪(b : (a : ι) → E) x_1, x⟫))) 2
have simp_rw : ∑ i : ι, HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) i, x⟫‖ 2 =
  HPow.hPow (β := ℕ) (√(∑ x_1 : ι, HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) x_1, x⟫‖ 2)) 2
Tactic: simp_rw [inner_mul_symm_re_eq_norm, norm_mul, ← inner_conj_symm x, starRingEnd_apply,
    norm_star, ← pow_two]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
⊢ ∑ i : ι, HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) i, x⟫‖ 2 =
    HPow.hPow (β := ℕ) (√(∑ x_1 : ι, HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) x_1, x⟫‖ 2)) 2
have rw : LE.le (α := ℝ) 0 (∑ x_1 : ι, HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) x_1, x⟫‖ 2)
Tactic: rw [Real.sq_sqrt]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
⊢ ∑ i : ι, HPow.hPow (β := ℕ) ‖⟪x, (b : (a : ι) → E) i⟫‖ 2 = HPow.hPow (β := ℕ) ‖x‖ 2
have h : ∀ (i : ι), HPow.hPow (β := ℕ) ‖⟪x, (b : (a : ι) → E) i⟫‖ 2 = HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) i, x⟫‖ 2
Tactic: convert! sum_sq_norm_inner_right b x using 2 with i -
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
i : ι
⊢ HPow.hPow (β := ℕ) ‖⟪x, (b : (a : ι) → E) i⟫‖ 2 = HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) i, x⟫‖ 2
have h : HPow.hPow (β := ℕ) (Norm.norm (E := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(b : (a : ι) → E) i, x⟫ : 𝕜)) 2 =
  HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) i, x⟫‖ 2
Tactic: rw [← inner_conj_symm, RCLike.norm_conj]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
i : ι
h :
  HPow.hPow (β := ℕ) (Norm.norm (E := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(b : (a : ι) → E) i, x⟫ : 𝕜)) 2 =
    HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) i, x⟫‖ 2
⊢ HPow.hPow (β := ℕ) ‖⟪x, (b : (a : ι) → E) i⟫‖ 2 = HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) i, x⟫‖ 2
have h₁ : HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) i, x⟫‖ 2 = HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) i, x⟫‖ 2
Tactic: rw [← inner_conj_symm, RCLike.norm_conj]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
inst : Fintype ι
E : Type u_7
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
b : OrthonormalBasis ι ℝ E
x : E
⊢ ∑ i : ι, HPow.hPow (β := ℕ) ⟪(b : (a : ι) → E) i, x⟫ 2 = HPow.hPow (β := ℕ) ‖x‖ 2
have rw : Eq (α := ℝ) (∑ i : ι, HPow.hPow (β := ℕ) ⟪(b : (a : ι) → E) i, x⟫ 2)
  (∑ i : ι, HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) i, x⟫‖ 2)
Tactic: rw [← b.sum_sq_norm_inner_right]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_7
E : Type u_8
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fintype ι
b : OrthonormalBasis ι ℝ E
x : E
⊢ ∑ i : ι, HPow.hPow (β := ℕ) ⟪x, (b : (a : ι) → E) i⟫ 2 = HPow.hPow (β := ℕ) ‖x‖ 2
have simp_rw : Eq (α := ℝ) (∑ i : ι, HPow.hPow (β := ℕ) ⟪x, (b : (a : ι) → E) i⟫ 2)
  (∑ i : ι, HPow.hPow (β := ℕ) ⟪(b : (a : ι) → E) i, x⟫ 2)
Tactic: simp_rw [← b.sum_sq_inner_right, real_inner_comm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
⊢ ‖x‖ = √(∑ i : ι, HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) i, x⟫‖ 2)
have rw : ‖x‖ = √(HPow.hPow (β := ℕ) ‖x‖ 2)
Tactic: rw [sum_sq_norm_inner_right, Real.sqrt_sq (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
rw : ‖x‖ = √(HPow.hPow (β := ℕ) ‖x‖ 2)
⊢ ‖x‖ = √(∑ i : ι, HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) i, x⟫‖ 2)
have rw₁ : ‖x‖ = ‖x‖
Tactic: rw [sum_sq_norm_inner_right, Real.sqrt_sq (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
⊢ √(∑ i : ι, HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) i, x⟫‖ 2) ≤
    √(∑ x_1 : ι, HPow.hPow (α := ℝ) (β := ℕ) (⨆ (j : ι), ‖⟪(b : (a : ι) → E) j, x⟫‖) 2)
have a : ∀ (i : ι),
  Membership.mem (γ := Finset ι) Finset.univ i → ‖⟪(b : (a : ι) → E) i, x⟫‖ ≤ ⨆ (j : ι), ‖⟪(b : (a : ι) → E) j, x⟫‖
Tactic: gcongr with i
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
⊢ √(∑ x_1 : ι, HPow.hPow (α := ℝ) (β := ℕ) (⨆ (j : ι), ‖⟪(b : (a : ι) → E) j, x⟫‖) 2) =
    √(↑(Fintype.card ι) : ℝ) * ⨆ (i : ι), ‖⟪(b : (a : ι) → E) i, x⟫‖
have simp : √(↑(Fintype.card ι) : ℝ) * √(HPow.hPow (α := ℝ) (β := ℕ) (⨆ (j : ι), ‖⟪(b : (a : ι) → E) j, x⟫‖) 2) =
  √(↑(Fintype.card ι) : ℝ) * ⨆ (j : ι), ‖⟪(b : (a : ι) → E) j, x⟫‖
Tactic: simp only [Finset.sum_const, Finset.card_univ, nsmul_eq_mul, Nat.cast_nonneg, Real.sqrt_mul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
⊢ √(↑(Fintype.card ι) : ℝ) * √(HPow.hPow (α := ℝ) (β := ℕ) (⨆ (j : ι), ‖⟪(b : (a : ι) → E) j, x⟫‖) 2) =
    √(↑(Fintype.card ι) : ℝ) * ⨆ (j : ι), ‖⟪(b : (a : ι) → E) j, x⟫‖
have e_a : √(HPow.hPow (α := ℝ) (β := ℕ) (⨆ (j : ι), ‖⟪(b : (a : ι) → E) j, x⟫‖) 2) = ⨆ (j : ι), ‖⟪(b : (a : ι) → E) j, x⟫‖
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
⊢ √(HPow.hPow (α := ℝ) (β := ℕ) (⨆ (j : ι), ‖⟪(b : (a : ι) → E) j, x⟫‖) 2) = ⨆ (j : ι), ‖⟪(b : (a : ι) → E) j, x⟫‖
have e_a : LE.le (α := ℝ) 0 (⨆ (j : ι), ‖⟪(b : (a : ι) → E) j, x⟫‖)
Tactic: rw [Real.sqrt_sq]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
⊢ LE.le (α := ℝ) 0 (⨆ (j : ι), ‖⟪(b : (a : ι) → E) j, x⟫‖)
have e_a : IsEmpty ι → LE.le (α := ℝ) 0 (⨆ (j : ι), ‖⟪(b : (a : ι) → E) j, x⟫‖)
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
e_a : IsEmpty ι → LE.le (α := ℝ) 0 (⨆ (j : ι), ‖⟪(b : (a : ι) → E) j, x⟫‖)
⊢ LE.le (α := ℝ) 0 (⨆ (j : ι), ‖⟪(b : (a : ι) → E) j, x⟫‖)
have e_a₁ : Nonempty ι → LE.le (α := ℝ) 0 (⨆ (j : ι), ‖⟪(b : (a : ι) → E) j, x⟫‖)
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
⊢ ‖x‖ ≤ √(↑(Fintype.card ι) : ℝ) * ⨆ (i : ι), ‖⟪(b : (a : ι) → E) i, x⟫‖
have calc : ‖x‖ = √(∑ i : ι, HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) i, x⟫‖ 2)
Tactic: calc ‖x‖
  _ = √(∑ i, ‖⟪b i, x⟫‖ ^ 2) := by rw [sum_sq_norm_inner_right, Real.sqrt_sq (by positivity)]
  _ ≤ √(∑ _ : ι, (⨆ j, ‖⟪b j, x⟫‖) ^ 2) := by
    gcongr with i
    exact le_ciSup (f := fun j ↦ ‖⟪b j, x⟫‖) (by simp) i
  _ = √(Fintype.card ι) * ⨆ i, ‖⟪b i, x⟫‖ := by
    simp only [Finset.sum_const, Finset.card_univ, nsmul_eq_mul, Nat.cast_nonneg, Real.sqrt_mul]
    congr
    rw [Real.sqrt_sq]
    cases isEmpty_or_nonempty ι
    · simp
    · exact le_ciSup_of_le (by simp) (Nonempty.some inferInstance) (by positivity)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
calc : ‖x‖ = √(∑ i : ι, HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) i, x⟫‖ 2)
⊢ ‖x‖ ≤ √(↑(Fintype.card ι) : ℝ) * ⨆ (i : ι), ‖⟪(b : (a : ι) → E) i, x⟫‖
have calc₁ : √(∑ i : ι, HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) i, x⟫‖ 2) ≤
  √(∑ x_1 : ι, HPow.hPow (α := ℝ) (β := ℕ) (⨆ (j : ι), ‖⟪(b : (a : ι) → E) j, x⟫‖) 2)
Tactic: calc ‖x‖
  _ = √(∑ i, ‖⟪b i, x⟫‖ ^ 2) := by rw [sum_sq_norm_inner_right, Real.sqrt_sq (by positivity)]
  _ ≤ √(∑ _ : ι, (⨆ j, ‖⟪b j, x⟫‖) ^ 2) := by
    gcongr with i
    exact le_ciSup (f := fun j ↦ ‖⟪b j, x⟫‖) (by simp) i
  _ = √(Fintype.card ι) * ⨆ i, ‖⟪b i, x⟫‖ := by
    simp only [Finset.sum_const, Finset.card_univ, nsmul_eq_mul, Nat.cast_nonneg, Real.sqrt_mul]
    congr
    rw [Real.sqrt_sq]
    cases isEmpty_or_nonempty ι
    · simp
    · exact le_ciSup_of_le (by simp) (Nonempty.some inferInstance) (by positivity)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
calc : ‖x‖ = √(∑ i : ι, HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) i, x⟫‖ 2)
calc₁ :
  √(∑ i : ι, HPow.hPow (β := ℕ) ‖⟪(b : (a : ι) → E) i, x⟫‖ 2) ≤
    √(∑ x_1 : ι, HPow.hPow (α := ℝ) (β := ℕ) (⨆ (j : ι), ‖⟪(b : (a : ι) → E) j, x⟫‖) 2)
⊢ ‖x‖ ≤ √(↑(Fintype.card ι) : ℝ) * ⨆ (i : ι), ‖⟪(b : (a : ι) → E) i, x⟫‖
have calc₂ : √(∑ x_1 : ι, HPow.hPow (α := ℝ) (β := ℕ) (⨆ (j : ι), ‖⟪(b : (a : ι) → E) j, x⟫‖) 2) =
  √(↑(Fintype.card ι) : ℝ) * ⨆ (i : ι), ‖⟪(b : (a : ι) → E) i, x⟫‖
Tactic: calc ‖x‖
  _ = √(∑ i, ‖⟪b i, x⟫‖ ^ 2) := by rw [sum_sq_norm_inner_right, Real.sqrt_sq (by positivity)]
  _ ≤ √(∑ _ : ι, (⨆ j, ‖⟪b j, x⟫‖) ^ 2) := by
    gcongr with i
    exact le_ciSup (f := fun j ↦ ‖⟪b j, x⟫‖) (by simp) i
  _ = √(Fintype.card ι) * ⨆ i, ‖⟪b i, x⟫‖ := by
    simp only [Finset.sum_const, Finset.card_univ, nsmul_eq_mul, Nat.cast_nonneg, Real.sqrt_mul]
    congr
    rw [Real.sqrt_sq]
    cases isEmpty_or_nonempty ι
    · simp
    · exact le_ciSup_of_le (by simp) (Nonempty.some inferInstance) (by positivity)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
U : Submodule 𝕜 E
inst_4 : U.HasOrthogonalProjection
b : OrthonormalBasis.{u_1, u_3, u_4} ι 𝕜 ↥U
⊢ U.orthogonalProjection =
    ∑ i : ι,
      (((InnerProductSpace.rankOne 𝕜 : (a : ↥U) → E →L⋆[𝕜] E →L[𝕜] ↥U) ((b : (a : ι) → ↥U) i : ↥U) :
            E →L⋆[𝕜] E →L[𝕜] ↥U) :
          (a : E) → E →L[𝕜] ↥U)
        (↑((b : (a : ι) → ↥U) i) : E)
have h : ∀ (x : E),
  Eq.{u_4 + 1} (α := E) (↑((U.orthogonalProjection : (a : E) → ↥U) x) : E)
    (↑((∑ i : ι,
              (((InnerProductSpace.rankOne 𝕜 : (a : ↥U) → E →L⋆[𝕜] E →L[𝕜] ↥U) ((b : (a : ι) → ↥U) i : ↥U) :
                    E →L⋆[𝕜] E →L[𝕜] ↥U) :
                  (a : E) → E →L[𝕜] ↥U)
                (↑((b : (a : ι) → ↥U) i) : E) :
            (a : E) → ↥U)
          x) :
      E)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
U : Submodule 𝕜 E
inst_4 : U.HasOrthogonalProjection
b : OrthonormalBasis.{u_1, u_3, u_4} ι 𝕜 ↥U
⊢ U.starProjection =
    ∑ i : ι,
      (((InnerProductSpace.rankOne 𝕜 : (a : E) → E →L⋆[𝕜] E →L[𝕜] E) (↑((b : (a : ι) → ↥U) i) : E) :
            E →L⋆[𝕜] E →L[𝕜] E) :
          (a : E) → E →L[𝕜] E)
        (↑((b : (a : ι) → ↥U) i) : E)
have h : ∀ (x : E),
  Eq (α := E) ((U.starProjection : (a : E) → E) x : E)
    ((∑ i : ι,
            (((InnerProductSpace.rankOne 𝕜 : (a : E) → E →L⋆[𝕜] E →L[𝕜] E) (↑((b : (a : ι) → ↥U) i) : E) :
                  E →L⋆[𝕜] E →L[𝕜] E) :
                (a : E) → E →L[𝕜] E)
              (↑((b : (a : ι) → ↥U) i) : E) :
          (a : E) → E)
        x :
      E)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
⊢ Eq (α := E →L[𝕜] E)
    (∑ i : ι,
      (((InnerProductSpace.rankOne 𝕜 : (a : E) → E →L⋆[𝕜] E →L[𝕜] E) ((b : (a : ι) → E) i : E) : E →L⋆[𝕜] E →L[𝕜] E) :
          (a : E) → E →L[𝕜] E)
        ((b : (a : ι) → E) i : E))
    (ContinuousLinearMap.id 𝕜 E)
have h : ∀ (x : E),
  Eq (α := E)
    ((∑ i : ι,
            (((InnerProductSpace.rankOne 𝕜 : (a : E) → E →L⋆[𝕜] E →L[𝕜] E) ((b : (a : ι) → E) i : E) :
                  E →L⋆[𝕜] E →L[𝕜] E) :
                (a : E) → E →L[𝕜] E)
              ((b : (a : ι) → E) i : E) :
          (a : E) → E)
        x :
      E)
    ((ContinuousLinearMap.id 𝕜 E : (a : E) → E) x : E)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (hypothesis)
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : Fintype ι
v : Basis ι 𝕜 E
hv : Orthonormal.{u_3, u_4, u_1} 𝕜 (E := E) (ι := ι) (⇑v : (a : ι) → E)
x y : E
p : EuclideanSpace 𝕜 ι := toLp 2 ((v.equivFun : (a : E) → ι → 𝕜) x)
q : EuclideanSpace 𝕜 ι := toLp 2 ((v.equivFun : (a : E) → ι → 𝕜) y)
⊢ inner 𝕜 (E := EuclideanSpace 𝕜 ι)
      ((v.equivFun ≪≫ₗ LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (ι → 𝕜)) : (a : E) → EuclideanSpace 𝕜 ι) x :
        EuclideanSpace 𝕜 ι)
      ((v.equivFun ≪≫ₗ LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (ι → 𝕜)) : (a : E) → EuclideanSpace 𝕜 ι) y :
        EuclideanSpace 𝕜 ι) =
    ⟪x, y⟫
have key : ⟪p, q⟫ =
  inner.{u_3, u_4} 𝕜 (E := E) (∑ i : ι, HSMul.hSMul (β := E) (p.ofLp i) ((v : (a : ι) → E) i : E))
    (∑ i : ι, HSMul.hSMul (β := E) (q.ofLp i) ((v : (a : ι) → E) i : E))
Tactic: have key : ⟪p, q⟫ = ⟪∑ i, p i • v i, ∑ i, q i • v i⟫ := by
          simp [inner_sum, inner_smul_right, hv.inner_left_fintype, PiLp.inner_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : Fintype ι
v : Basis ι 𝕜 E
hv : Orthonormal.{u_3, u_4, u_1} 𝕜 (E := E) (ι := ι) (⇑v : (a : ι) → E)
x y : E
p : EuclideanSpace 𝕜 ι := toLp 2 ((v.equivFun : (a : E) → ι → 𝕜) x)
q : EuclideanSpace 𝕜 ι := toLp 2 ((v.equivFun : (a : E) → ι → 𝕜) y)
key :
  ⟪p, q⟫ =
    inner.{u_3, u_4} 𝕜 (E := E) (∑ i : ι, HSMul.hSMul (β := E) (p.ofLp i) ((v : (a : ι) → E) i : E))
      (∑ i : ι, HSMul.hSMul (β := E) (q.ofLp i) ((v : (a : ι) → E) i : E))
⊢ inner 𝕜 (E := EuclideanSpace 𝕜 ι)
      ((v.equivFun ≪≫ₗ LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (ι → 𝕜)) : (a : E) → EuclideanSpace 𝕜 ι) x :
        EuclideanSpace 𝕜 ι)
      ((v.equivFun ≪≫ₗ LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (ι → 𝕜)) : (a : E) → EuclideanSpace 𝕜 ι) y :
        EuclideanSpace 𝕜 ι) =
    ⟪x, y⟫
have h : x = ∑ i : ι, HSMul.hSMul (β := E) (p.ofLp i) ((v : (a : ι) → E) i : E)
Tactic: convert! key
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : Fintype ι
v : Basis ι 𝕜 E
hv : Orthonormal.{u_3, u_4, u_1} 𝕜 (E := E) (ι := ι) (⇑v : (a : ι) → E)
x y : E
p : EuclideanSpace 𝕜 ι := toLp 2 ((v.equivFun : (a : E) → ι → 𝕜) x)
q : EuclideanSpace 𝕜 ι := toLp 2 ((v.equivFun : (a : E) → ι → 𝕜) y)
key :
  ⟪p, q⟫ =
    inner.{u_3, u_4} 𝕜 (E := E) (∑ i : ι, HSMul.hSMul (β := E) (p.ofLp i) ((v : (a : ι) → E) i : E))
      (∑ i : ι, HSMul.hSMul (β := E) (q.ofLp i) ((v : (a : ι) → E) i : E))
h : x = ∑ i : ι, HSMul.hSMul (β := E) (p.ofLp i) ((v : (a : ι) → E) i : E)
⊢ inner 𝕜 (E := EuclideanSpace 𝕜 ι)
      ((v.equivFun ≪≫ₗ LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (ι → 𝕜)) : (a : E) → EuclideanSpace 𝕜 ι) x :
        EuclideanSpace 𝕜 ι)
      ((v.equivFun ≪≫ₗ LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (ι → 𝕜)) : (a : E) → EuclideanSpace 𝕜 ι) y :
        EuclideanSpace 𝕜 ι) =
    ⟪x, y⟫
have h₁ : y = ∑ i : ι, HSMul.hSMul (β := E) (q.ofLp i) ((v : (a : ι) → E) i : E)
Tactic: convert! key
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : Fintype ι
v : Basis ι 𝕜 E
hv : Orthonormal.{u_3, u_4, u_1} 𝕜 (E := E) (ι := ι) (⇑v : (a : ι) → E)
x y : E
p : EuclideanSpace 𝕜 ι := toLp 2 ((v.equivFun : (a : E) → ι → 𝕜) x)
q : EuclideanSpace 𝕜 ι := toLp 2 ((v.equivFun : (a : E) → ι → 𝕜) y)
key :
  ⟪p, q⟫ =
    inner.{u_3, u_4} 𝕜 (E := E) (∑ i : ι, HSMul.hSMul (β := E) (p.ofLp i) ((v : (a : ι) → E) i : E))
      (∑ i : ι, HSMul.hSMul (β := E) (q.ofLp i) ((v : (a : ι) → E) i : E))
⊢ x = ∑ i : ι, HSMul.hSMul (β := E) (p.ofLp i) ((v : (a : ι) → E) i : E)
have h : Eq.{u_4 + 1} (α := E) ((v.equivFun.symm : (a : ι → 𝕜) → E) ((v.equivFun : (a : E) → ι → 𝕜) x : ι → 𝕜) : E)
  (∑ i : ι, HSMul.hSMul (β := E) (p.ofLp i) ((v : (a : ι) → E) i : E) : E)
Tactic: rw [← v.equivFun.symm_apply_apply x, v.equivFun_symm_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : Fintype ι
v : Basis ι 𝕜 E
hv : Orthonormal.{u_3, u_4, u_1} 𝕜 (E := E) (ι := ι) (⇑v : (a : ι) → E)
x y : E
p : EuclideanSpace 𝕜 ι := toLp 2 ((v.equivFun : (a : E) → ι → 𝕜) x)
q : EuclideanSpace 𝕜 ι := toLp 2 ((v.equivFun : (a : E) → ι → 𝕜) y)
key :
  ⟪p, q⟫ =
    inner.{u_3, u_4} 𝕜 (E := E) (∑ i : ι, HSMul.hSMul (β := E) (p.ofLp i) ((v : (a : ι) → E) i : E))
      (∑ i : ι, HSMul.hSMul (β := E) (q.ofLp i) ((v : (a : ι) → E) i : E))
h :
  Eq.{u_4 + 1} (α := E) ((v.equivFun.symm : (a : ι → 𝕜) → E) ((v.equivFun : (a : E) → ι → 𝕜) x : ι → 𝕜) : E)
    (∑ i : ι, HSMul.hSMul (β := E) (p.ofLp i) ((v : (a : ι) → E) i : E) : E)
⊢ x = ∑ i : ι, HSMul.hSMul (β := E) (p.ofLp i) ((v : (a : ι) → E) i : E)
have h₁ : Eq.{u_4 + 1} (α := E)
  (∑ i : ι,
    HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (β := E) ((v.equivFun : (a : E) → ι → 𝕜) x i : 𝕜) ((v : (a : ι) → E) i : E))
  (∑ i : ι, HSMul.hSMul (β := E) (p.ofLp i) ((v : (a : ι) → E) i : E))
Tactic: rw [← v.equivFun.symm_apply_apply x, v.equivFun_symm_apply]