awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
inst_5 : CompleteSpace E
V : (i : ι) → LinearIsometry.{u_2, u_2, u_4, u_3} (RingHom.id 𝕜) (G i) E
hV : OrthogonalFamily 𝕜 G V
inst_6 : ∀ (i : ι), CompleteSpace.{u_4} (G i)
⊢ hV.linearIsometry (G := G).range = topologicalClosure (⨆ (i : ι), (V i).range)
have refine_1 : hV.linearIsometry (G := G).range ≤ topologicalClosure (⨆ (i : ι), (V i).range)
Tactic: classical
  refine le_antisymm ?_ ?_
  · rintro x ⟨f, rfl⟩
    refine mem_closure_of_tendsto (hV.hasSum_linearIsometry f) (Eventually.of_forall ?_)
    intro s
    rw [SetLike.mem_coe]
    refine sum_mem ?_
    intro i _
    refine mem_iSup_of_mem i ?_
    exact LinearMap.mem_range_self _ (f i)
  · apply topologicalClosure_minimal
    · refine iSup_le ?_
      rintro i x ⟨x, rfl⟩
      use lp.single 2 i x
      exact hV.linearIsometry_apply_single x
    exact hV.linearIsometry.isometry.isUniformInducing.isComplete_range.isClosed
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
inst_5 : CompleteSpace E
V : (i : ι) → LinearIsometry.{u_2, u_2, u_4, u_3} (RingHom.id 𝕜) (G i) E
hV : OrthogonalFamily 𝕜 G V
inst_6 : ∀ (i : ι), CompleteSpace.{u_4} (G i)
refine_1 : hV.linearIsometry (G := G).range ≤ topologicalClosure (⨆ (i : ι), (V i).range)
⊢ hV.linearIsometry (G := G).range = topologicalClosure (⨆ (i : ι), (V i).range)
have refine_2 : topologicalClosure (⨆ (i : ι), (V i).range) ≤ hV.linearIsometry (G := G).range
Tactic: classical
  refine le_antisymm ?_ ?_
  · rintro x ⟨f, rfl⟩
    refine mem_closure_of_tendsto (hV.hasSum_linearIsometry f) (Eventually.of_forall ?_)
    intro s
    rw [SetLike.mem_coe]
    refine sum_mem ?_
    intro i _
    refine mem_iSup_of_mem i ?_
    exact LinearMap.mem_range_self _ (f i)
  · apply topologicalClosure_minimal
    · refine iSup_le ?_
      rintro i x ⟨x, rfl⟩
      use lp.single 2 i x
      exact hV.linearIsometry_apply_single x
    exact hV.linearIsometry.isometry.isUniformInducing.isComplete_range.isClosed
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
inst_5 : CompleteSpace E
V : (i : ι) → LinearIsometry.{u_2, u_2, u_4, u_3} (RingHom.id 𝕜) (G i) E
inst_6 : ∀ (i : ι), CompleteSpace.{u_4} (G i)
hVortho : OrthogonalFamily 𝕜 G V
hVtotal : LE.le.{u_3} (α := Submodule 𝕜 E) ⊤ (topologicalClosure (⨆ (i : ι), (V i).range))
⊢ Function.Surjective (α := ↥(lp G 2)) (β := E) (⇑(hVortho.linearIsometry (G := G)) : (a : ↥(lp G 2)) → E)
have rw : Function.Surjective (α := ↥(lp G 2)) (β := E) (⇑hVortho.linearIsometry (G := G).toLinearMap : (a : ↥(lp G 2)) → E)
Tactic: rw [← LinearIsometry.coe_toLinearMap]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
inst_5 : CompleteSpace E
V : (i : ι) → LinearIsometry.{u_2, u_2, u_4, u_3} (RingHom.id 𝕜) (G i) E
inst_6 : DecidableEq ι
inst_7 : (i : ι) → DecidableEq (G i)
hV : IsHilbertSum 𝕜 G V
W₀ : Π₀ (i : ι), G i
⊢ (↑(W₀.sum (β := G) fun (a : ι) (b : G a) ↦
          (hV.linearIsometryEquiv (G := G) : (a : E) → ↥(lp G 2)) ((V a : (a : G a) → E) b)) :
      (i : ι) → G i) =
    (⇑W₀ : (a : ι) → G a)
have rw : (↑((hV.linearIsometryEquiv (G := G) : (a : E) → ↥(lp G 2)) (W₀.sum (β := G) fun (a : ι) ↦ (⇑(V a) : (a : G a) → E))) :
    (i : ι) → G i) =
  (⇑W₀ : (a : ι) → G a)
Tactic: rw [← map_dfinsuppSum]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
inst_5 : CompleteSpace E
V : (i : ι) → LinearIsometry.{u_2, u_2, u_4, u_3} (RingHom.id 𝕜) (G i) E
inst_6 : DecidableEq ι
inst_7 : (i : ι) → DecidableEq (G i)
hV : IsHilbertSum 𝕜 G V
W₀ : Π₀ (i : ι), G i
⊢ (↑((hV.linearIsometryEquiv (G := G) : (a : E) → ↥(lp G 2)) (W₀.sum (β := G) fun (a : ι) ↦ (⇑(V a) : (a : G a) → E))) :
      (i : ι) → G i) =
    (⇑W₀ : (a : ι) → G a)
have rw : (↑((hV.linearIsometryEquiv (G := G) : (a : E) → ↥(lp G 2))
        ((hV.linearIsometryEquiv (G := G).symm : (a : ↥(lp G 2)) → E) (W₀.sum (β := G) (lp.single (E := G) 2)))) :
    (i : ι) → G i) =
  (⇑W₀ : (a : ι) → G a)
Tactic: rw [← hV.linearIsometryEquiv_symm_apply_dfinsupp_sum_single]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
inst_5 : CompleteSpace E
V : (i : ι) → LinearIsometry.{u_2, u_2, u_4, u_3} (RingHom.id 𝕜) (G i) E
inst_6 : DecidableEq ι
inst_7 : (i : ι) → DecidableEq (G i)
hV : IsHilbertSum 𝕜 G V
W₀ : Π₀ (i : ι), G i
⊢ (↑((hV.linearIsometryEquiv (G := G) : (a : E) → ↥(lp G 2))
          ((hV.linearIsometryEquiv (G := G).symm : (a : ↥(lp G 2)) → E) (W₀.sum (β := G) (lp.single (E := G) 2)))) :
      (i : ι) → G i) =
    (⇑W₀ : (a : ι) → G a)
have rw : (↑(W₀.sum (β := G) (lp.single (E := G) 2)) : (i : ι) → G i) = (⇑W₀ : (a : ι) → G a)
Tactic: rw [LinearIsometryEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
inst_5 : CompleteSpace E
V : (i : ι) → LinearIsometry.{u_2, u_2, u_4, u_3} (RingHom.id 𝕜) (G i) E
inst_6 : DecidableEq ι
inst_7 : (i : ι) → DecidableEq (G i)
hV : IsHilbertSum 𝕜 G V
W₀ : Π₀ (i : ι), G i
⊢ (↑(W₀.sum (β := G) (lp.single (E := G) 2)) : (i : ι) → G i) = (⇑W₀ : (a : ι) → G a)
have h : ∀ (i : ι), (↑(W₀.sum (β := G) (lp.single (E := G) 2)) : (i : ι) → G i) i = (W₀ : (a : ι) → G a) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
v : ι → E
hv : Orthonormal 𝕜 v
hsp : LE.le (α := Submodule 𝕜 E) ⊤ (topologicalClosure (span 𝕜 (Set.range v)))
⊢ LE.le.{u_3} (α := Submodule 𝕜 E) ⊤
    (topologicalClosure
      (⨆ (i : ι),
        LinearMap.range (R := 𝕜) (M := 𝕜) (τ₁₂ := RingHom.id 𝕜)
          (LinearIsometry.toLinearMap (LinearIsometry.toSpanSingleton 𝕜 E ⋯))))
have h : Eq (α := Submodule 𝕜 E)
  (⨆ (i : ι),
    LinearMap.range (R := 𝕜) (M := 𝕜) (τ₁₂ := RingHom.id 𝕜)
      (LinearIsometry.toLinearMap (LinearIsometry.toSpanSingleton 𝕜 E sorry)))
  (span 𝕜 (Set.range v))
Tactic: convert! hsp
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
K : Submodule 𝕜 E
hK : CompleteSpace.{u_3} ↥K
b : Bool
⊢ CompleteSpace.{u_3} ↥(bif b then K else Kᗮ)
have false : CompleteSpace.{u_3} ↥(bif false then K else Kᗮ)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
K : Submodule 𝕜 E
hK : CompleteSpace.{u_3} ↥K
b : Bool
false : CompleteSpace.{u_3} ↥(bif Bool.false then K else Kᗮ)
⊢ CompleteSpace.{u_3} ↥(bif b then K else Kᗮ)
have true : CompleteSpace.{u_3} ↥(bif true then K else Kᗮ)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (hypothesis)
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
K : Submodule 𝕜 E
hK : CompleteSpace.{u_3} ↥K
⊢ IsHilbertSum.{0, u_2, u_3, u_3} 𝕜 (E := E) (fun (b : Bool) ↦ ↥(bif b then K else Kᗮ)) fun (b : Bool) ↦
    (bif b then K else Kᗮ).subtypeₗᵢ
have this : ∀ (b : Bool), CompleteSpace.{u_3} ↥(bif b then K else Kᗮ)
Tactic: have : ∀ b, CompleteSpace (↥(cond b K Kᗮ)) := by
    intro b
    cases b <;> first | exact instOrthogonalCompleteSpace K | assumption
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
K : Submodule 𝕜 E
hK : CompleteSpace.{u_3} ↥K
this : ∀ (b : Bool), CompleteSpace.{u_3} ↥(bif b then K else Kᗮ)
⊢ IsHilbertSum.{0, u_2, u_3, u_3} 𝕜 (E := E) (fun (b : Bool) ↦ ↥(bif b then K else Kᗮ)) fun (b : Bool) ↦
    (bif b then K else Kᗮ).subtypeₗᵢ
have refine : LE.le.{u_3} (α := Submodule 𝕜 E) ⊤ (topologicalClosure (⨆ (i : Bool), bif i then K else Kᗮ))
Tactic: refine IsHilbertSum.mkInternal _ K.orthogonalFamily_self ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
K : Submodule 𝕜 E
hK : CompleteSpace.{u_3} ↥K
this : ∀ (b : Bool), CompleteSpace.{u_3} ↥(bif b then K else Kᗮ)
⊢ LE.le.{u_3} (α := Submodule 𝕜 E) ⊤ (topologicalClosure (⨆ (i : Bool), bif i then K else Kᗮ))
have refine : LE.le.{u_3} (α := Submodule 𝕜 E) ⊤ (⨆ (i : Bool), bif i then K else Kᗮ)
Tactic: refine le_trans ?_ (Submodule.le_topologicalClosure _)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
K : Submodule 𝕜 E
hK : CompleteSpace.{u_3} ↥K
this : ∀ (b : Bool), CompleteSpace.{u_3} ↥(bif b then K else Kᗮ)
⊢ LE.le.{u_3} (α := Submodule 𝕜 E) ⊤ (⨆ (i : Bool), bif i then K else Kᗮ)
have rw : ⊤ ≤ K ⊔ Kᗮ
Tactic: rw [iSup_bool_eq, cond, cond]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
K : Submodule 𝕜 E
hK : CompleteSpace.{u_3} ↥K
this : ∀ (b : Bool), CompleteSpace.{u_3} ↥(bif b then K else Kᗮ)
⊢ ⊤ ≤ K ⊔ Kᗮ
have refine : Codisjoint K Kᗮ
Tactic: refine Codisjoint.top_le ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
b₁ b₂ : E ≃ₗᵢ[𝕜] ↥(lp (fun (x : ι) ↦ 𝕜) 2)
h :
  Eq (α := (a : ι) → E)
    ((fun (b : HilbertBasis ι 𝕜 E) (i : ι) ↦
        ((b.repr.symm : (a : ↥(lp (fun (x : ι) ↦ 𝕜) 2)) → E) (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i 1) : E))
      { repr := b₁ })
    ((fun (b : HilbertBasis ι 𝕜 E) (i : ι) ↦
        ((b.repr.symm : (a : ↥(lp (fun (x : ι) ↦ 𝕜) 2)) → E) (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i 1) : E))
      { repr := b₂ })
⊢ { repr := b₁ : HilbertBasis ι 𝕜 E } = { repr := b₂ }
have e_repr : b₁ = b₂
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
b₁ b₂ : E ≃ₗᵢ[𝕜] ↥(lp (fun (x : ι) ↦ 𝕜) 2)
h :
  Eq (α := (a : ι) → E)
    ((fun (b : HilbertBasis ι 𝕜 E) (i : ι) ↦
        ((b.repr.symm : (a : ↥(lp (fun (x : ι) ↦ 𝕜) 2)) → E) (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i 1) : E))
      { repr := b₁ })
    ((fun (b : HilbertBasis ι 𝕜 E) (i : ι) ↦
        ((b.repr.symm : (a : ↥(lp (fun (x : ι) ↦ 𝕜) 2)) → E) (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i 1) : E))
      { repr := b₂ })
⊢ b₁ = b₂
have e_repr : b₁.symm = b₂.symm
Tactic: apply LinearIsometryEquiv.symm_bijective.injective
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
b₁ b₂ : E ≃ₗᵢ[𝕜] ↥(lp (fun (x : ι) ↦ 𝕜) 2)
h :
  Eq (α := (a : ι) → E)
    ((fun (b : HilbertBasis ι 𝕜 E) (i : ι) ↦
        ((b.repr.symm : (a : ↥(lp (fun (x : ι) ↦ 𝕜) 2)) → E) (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i 1) : E))
      { repr := b₁ })
    ((fun (b : HilbertBasis ι 𝕜 E) (i : ι) ↦
        ((b.repr.symm : (a : ↥(lp (fun (x : ι) ↦ 𝕜) 2)) → E) (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i 1) : E))
      { repr := b₂ })
⊢ b₁.symm = b₂.symm
have e_repr : (↑b₁.symm : ↥(lp (fun (x : ι) ↦ 𝕜) 2) ≃L[𝕜] E) = (↑b₂.symm : ↥(lp (fun (x : ι) ↦ 𝕜) 2) ≃L[𝕜] E)
Tactic: apply LinearIsometryEquiv.toContinuousLinearEquiv_injective
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
b₁ b₂ : E ≃ₗᵢ[𝕜] ↥(lp (fun (x : ι) ↦ 𝕜) 2)
h :
  Eq (α := (a : ι) → E)
    ((fun (b : HilbertBasis ι 𝕜 E) (i : ι) ↦
        ((b.repr.symm : (a : ↥(lp (fun (x : ι) ↦ 𝕜) 2)) → E) (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i 1) : E))
      { repr := b₁ })
    ((fun (b : HilbertBasis ι 𝕜 E) (i : ι) ↦
        ((b.repr.symm : (a : ↥(lp (fun (x : ι) ↦ 𝕜) 2)) → E) (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i 1) : E))
      { repr := b₂ })
⊢ (↑b₁.symm : ↥(lp (fun (x : ι) ↦ 𝕜) 2) ≃L[𝕜] E) = (↑b₂.symm : ↥(lp (fun (x : ι) ↦ 𝕜) 2) ≃L[𝕜] E)
have e_repr : (↑(↑b₁.symm : ↥(lp (fun (x : ι) ↦ 𝕜) 2) ≃L[𝕜] E) : ↥(lp (fun (x : ι) ↦ 𝕜) 2) →L[𝕜] E) =
  (↑(↑b₂.symm : ↥(lp (fun (x : ι) ↦ 𝕜) 2) ≃L[𝕜] E) : ↥(lp (fun (x : ι) ↦ 𝕜) 2) →L[𝕜] E)
Tactic: apply ContinuousLinearEquiv.coe_injective
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
b₁ b₂ : E ≃ₗᵢ[𝕜] ↥(lp (fun (x : ι) ↦ 𝕜) 2)
h :
  Eq (α := (a : ι) → E)
    ((fun (b : HilbertBasis ι 𝕜 E) (i : ι) ↦
        ((b.repr.symm : (a : ↥(lp (fun (x : ι) ↦ 𝕜) 2)) → E) (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i 1) : E))
      { repr := b₁ })
    ((fun (b : HilbertBasis ι 𝕜 E) (i : ι) ↦
        ((b.repr.symm : (a : ↥(lp (fun (x : ι) ↦ 𝕜) 2)) → E) (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i 1) : E))
      { repr := b₂ })
⊢ (↑(↑b₁.symm : ↥(lp (fun (x : ι) ↦ 𝕜) 2) ≃L[𝕜] E) : ↥(lp (fun (x : ι) ↦ 𝕜) 2) →L[𝕜] E) =
    (↑(↑b₂.symm : ↥(lp (fun (x : ι) ↦ 𝕜) 2) ≃L[𝕜] E) : ↥(lp (fun (x : ι) ↦ 𝕜) 2) →L[𝕜] E)
have e_repr : ∀ (i : ι),
  (↑(↑b₁.symm : ↥(lp (fun (x : ι) ↦ 𝕜) 2) ≃L[𝕜] E) : ↥(lp (fun (x : ι) ↦ 𝕜) 2) →L[𝕜] E).comp (σ₁₂ := RingHom.id 𝕜)
      (lp.singleContinuousLinearMap 𝕜 (fun (x : ι) ↦ 𝕜) 2 i) =
    (↑(↑b₂.symm : ↥(lp (fun (x : ι) ↦ 𝕜) 2) ≃L[𝕜] E) : ↥(lp (fun (x : ι) ↦ 𝕜) 2) →L[𝕜] E).comp (σ₁₂ := RingHom.id 𝕜)
      (lp.singleContinuousLinearMap 𝕜 (fun (x : ι) ↦ 𝕜) 2 i)
Tactic: refine lp.ext_continuousLinearMap (ENNReal.ofNat_ne_top (n := nat_lit 2)) fun i => ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
b₁ b₂ : E ≃ₗᵢ[𝕜] ↥(lp (fun (x : ι) ↦ 𝕜) 2)
h :
  Eq (α := (a : ι) → E)
    ((fun (b : HilbertBasis ι 𝕜 E) (i : ι) ↦
        ((b.repr.symm : (a : ↥(lp (fun (x : ι) ↦ 𝕜) 2)) → E) (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i 1) : E))
      { repr := b₁ })
    ((fun (b : HilbertBasis ι 𝕜 E) (i : ι) ↦
        ((b.repr.symm : (a : ↥(lp (fun (x : ι) ↦ 𝕜) 2)) → E) (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i 1) : E))
      { repr := b₂ })
i : ι
⊢ (↑(↑b₁.symm : ↥(lp (fun (x : ι) ↦ 𝕜) 2) ≃L[𝕜] E) : ↥(lp (fun (x : ι) ↦ 𝕜) 2) →L[𝕜] E).comp (σ₁₂ := RingHom.id 𝕜)
      (lp.singleContinuousLinearMap 𝕜 (fun (x : ι) ↦ 𝕜) 2 i) =
    (↑(↑b₂.symm : ↥(lp (fun (x : ι) ↦ 𝕜) 2) ≃L[𝕜] E) : ↥(lp (fun (x : ι) ↦ 𝕜) 2) →L[𝕜] E).comp (σ₁₂ := RingHom.id 𝕜)
      (lp.singleContinuousLinearMap 𝕜 (fun (x : ι) ↦ 𝕜) 2 i)
have e_repr : Eq.{u_3 + 1} (α := E)
  (((↑(↑b₁.symm : ↥(lp (fun (x : ι) ↦ 𝕜) 2) ≃L[𝕜] E) : ↥(lp (fun (x : ι) ↦ 𝕜) 2) →L[𝕜] E).comp (σ₁₂ := RingHom.id 𝕜)
          (lp.singleContinuousLinearMap 𝕜 (fun (x : ι) ↦ 𝕜) 2 i) :
        (a : 𝕜) → E)
      1 :
    E)
  (((↑(↑b₂.symm : ↥(lp (fun (x : ι) ↦ 𝕜) 2) ≃L[𝕜] E) : ↥(lp (fun (x : ι) ↦ 𝕜) 2) →L[𝕜] E).comp (σ₁₂ := RingHom.id 𝕜)
          (lp.singleContinuousLinearMap 𝕜 (fun (x : ι) ↦ 𝕜) 2 i) :
        (a : 𝕜) → E)
      1 :
    E)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : DecidableEq ι
b : HilbertBasis ι 𝕜 E
i : ι
⊢ Eq.{u_3 + 1} (α := E)
    ((b.repr.symm : (a : ↥(lp (fun (x : ι) ↦ 𝕜) 2)) → E) (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i 1) : E)
    ((b : (a : ι) → E) i : E)
have dsimp : Eq.{u_3 + 1} (α := E) ((b.repr.symm : (a : ↥(lp (fun (x : ι) ↦ 𝕜) 2)) → E) (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i 1) : E)
  ((b.repr.symm : (a : ↥(lp (fun (x : ι) ↦ 𝕜) 2)) → E) (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i 1) : E)
Tactic: dsimp +instances [instFunLike]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
v : E
i : ι
⊢ (↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) v) : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i = ⟪(b : (a : ι) → E) i, v⟫
have rw : (↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) v) : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i =
  inner 𝕜 (E := 𝕜) 1 ((↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) v) : (i : ι) → 𝕜) i)
Tactic: rw [← b.repr.inner_map_map (b i) v, b.repr_self, lp.inner_single_left]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
v : E
i : ι
⊢ (↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) v) : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i = ⟪(b : (a : ι) → E) i, v⟫
have rw : (↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) v) : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i =
  inner 𝕜 (E := ↥(lp (fun (x : ι) ↦ 𝕜) 2))
    ((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) ((b : (a : ι) → E) i) : ↥(lp (fun (x : ι) ↦ 𝕜) 2))
    ((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) v : ↥(lp (fun (x : ι) ↦ 𝕜) 2))
Tactic: classical
  rw [← b.repr.inner_map_map (b i) v, b.repr_self, lp.inner_single_left]
  simp
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
v : E
i : ι
rw :
  (↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) v) : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i =
    inner 𝕜 (E := ↥(lp (fun (x : ι) ↦ 𝕜) 2))
      ((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) ((b : (a : ι) → E) i) : ↥(lp (fun (x : ι) ↦ 𝕜) 2))
      ((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) v : ↥(lp (fun (x : ι) ↦ 𝕜) 2))
⊢ (↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) v) : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i = ⟪(b : (a : ι) → E) i, v⟫
have rw₁ : (↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) v) : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i =
  inner 𝕜 (E := ↥(lp (fun (x : ι) ↦ 𝕜) 2)) (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i 1)
    ((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) v)
Tactic: classical
  rw [← b.repr.inner_map_map (b i) v, b.repr_self, lp.inner_single_left]
  simp
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
v : E
i : ι
rw :
  (↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) v) : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i =
    inner 𝕜 (E := ↥(lp (fun (x : ι) ↦ 𝕜) 2))
      ((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) ((b : (a : ι) → E) i) : ↥(lp (fun (x : ι) ↦ 𝕜) 2))
      ((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) v : ↥(lp (fun (x : ι) ↦ 𝕜) 2))
rw₁ :
  (↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) v) : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i =
    inner 𝕜 (E := ↥(lp (fun (x : ι) ↦ 𝕜) 2)) (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i 1)
      ((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) v)
⊢ (↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) v) : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i = ⟪(b : (a : ι) → E) i, v⟫
have rw₂ : (↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) v) : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i =
  inner 𝕜 (E := 𝕜) 1 ((↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) v) : (i : ι) → 𝕜) i)
Tactic: classical
  rw [← b.repr.inner_map_map (b i) v, b.repr_self, lp.inner_single_left]
  simp
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
⊢ Orthonormal.{u_2, u_3, u_1} 𝕜 (E := E) (ι := ι) (⇑b : (a : ι) → E)
have rw : ∀ (i j : ι), inner.{u_2, u_3} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((b : (a : ι) → E) j : E) = if i = j then 1 else 0
Tactic: rw [orthonormal_iff_ite]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
i j : ι
⊢ inner.{u_2, u_3} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((b : (a : ι) → E) j : E) = if i = j then 1 else 0
have rw : inner 𝕜 (E := 𝕜) 1 (if i = j then 1 else 0) = if i = j then 1 else 0
Tactic: rw [← b.repr.inner_map_map (b i) (b j), b.repr_self, b.repr_self, lp.inner_single_left,
    lp.single_apply, Pi.single_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
⊢ Orthonormal.{u_2, u_3, u_1} 𝕜 (E := E) (ι := ι) (⇑b : (a : ι) → E)
have rw : ∀ (i j : ι), inner.{u_2, u_3} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((b : (a : ι) → E) j : E) = if i = j then 1 else 0
Tactic: classical
  rw [orthonormal_iff_ite]
  intro i j
  rw [← b.repr.inner_map_map (b i) (b j), b.repr_self, b.repr_self, lp.inner_single_left,
    lp.single_apply, Pi.single_apply]
  simp