awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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
i : ι
⊢ (↑(W₀.sum (β := G) (lp.single (E := G) 2)) : (i : ι) → G i) i = (W₀ : (a : ι) → G a) i

Tactic:
simp +contextual [DFinsupp.sum, lp.single_apply]

Premises used: DFinsupp.sum, lp.single_apply
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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 (α := Submodule 𝕜 E) ⊤ (topologicalClosure (span 𝕜 (Set.range v)))

Tactic:
hsp
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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)))
h :
  Eq (α := Submodule 𝕜 E)
    (⨆ (i : ι),
      LinearMap.range (R := 𝕜) (M := 𝕜) (τ₁₂ := RingHom.id 𝕜)
        (LinearIsometry.toLinearMap (LinearIsometry.toSpanSingleton 𝕜 E ⋯)))
    (span 𝕜 (Set.range v))
⊢ LE.le.{u_3} (α := Submodule 𝕜 E) ⊤
    (topologicalClosure
      (⨆ (i : ι),
        LinearMap.range (R := 𝕜) (M := 𝕜) (τ₁₂ := RingHom.id 𝕜)
          (LinearIsometry.toLinearMap (LinearIsometry.toSpanSingleton 𝕜 E ⋯))))

Tactic:
convert! hsp
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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)))
⊢ Eq (α := Submodule 𝕜 E)
    (⨆ (i : ι),
      LinearMap.range (R := 𝕜) (M := 𝕜) (τ₁₂ := RingHom.id 𝕜)
        (LinearIsometry.toLinearMap (LinearIsometry.toSpanSingleton 𝕜 E ⋯)))
    (span 𝕜 (Set.range v))

Tactic:
simp [← LinearMap.span_singleton_eq_range, ← Submodule.span_iUnion]

Premises used: Submodule.span_iUnion, LinearMap.span_singleton_eq_range
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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ᗮ)
true : CompleteSpace.{u_3} ↥(bif Bool.true then K else Kᗮ)
⊢ CompleteSpace.{u_3} ↥(bif b then K else Kᗮ)

Tactic:
cases b
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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
⊢ CompleteSpace.{u_3} ↥(bif false then K else Kᗮ)

Tactic:
instOrthogonalCompleteSpace K

Premises used: Set.Mem, Submodule.instOrthogonalCompleteSpace
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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
⊢ CompleteSpace.{u_3} ↥(bif false then K else Kᗮ)

Tactic:
exact instOrthogonalCompleteSpace K

Premises used: Submodule.instOrthogonalCompleteSpace
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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
⊢ CompleteSpace.{u_3} ↥(bif false then K else Kᗮ)

Tactic:
first | exact instOrthogonalCompleteSpace K | assumption

Premises used: Submodule.instOrthogonalCompleteSpace
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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
⊢ CompleteSpace.{u_3} ↥(bif true then K else Kᗮ)

Tactic:
instOrthogonalCompleteSpace K

Premises used: Submodule.instOrthogonalCompleteSpace
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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
⊢ CompleteSpace.{u_3} ↥(bif true then K else Kᗮ)

Tactic:
assumption
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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
⊢ CompleteSpace.{u_3} ↥(bif true then K else Kᗮ)

Tactic:
first | exact instOrthogonalCompleteSpace K | assumption

Premises used: Submodule.instOrthogonalCompleteSpace
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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ᗮ)

Tactic:
have : ∀ b, CompleteSpace (↥(cond b K Kᗮ)) := by
    intro b
    cases b <;> first | exact instOrthogonalCompleteSpace K | assumption
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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ₗᵢ

Tactic:
IsHilbertSum.mkInternal _ K.orthogonalFamily_self ?_

Premises used: IsHilbertSum.mkInternal, Submodule.orthogonalFamily_self
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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ᗮ)
refine : LE.le.{u_3} (α := Submodule 𝕜 E) ⊤ (topologicalClosure (⨆ (i : Bool), bif i 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ₗᵢ

Tactic:
refine IsHilbertSum.mkInternal _ K.orthogonalFamily_self ?_

Premises used: IsHilbertSum.mkInternal, Submodule.orthogonalFamily_self
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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ᗮ))

Tactic:
le_trans ?_ (Submodule.le_topologicalClosure _)

Premises used: Submodule.le_topologicalClosure, le_trans
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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ᗮ)
refine : LE.le.{u_3} (α := Submodule 𝕜 E) ⊤ (⨆ (i : Bool), bif i then K else Kᗮ)
⊢ LE.le.{u_3} (α := Submodule 𝕜 E) ⊤ (topologicalClosure (⨆ (i : Bool), bif i then K else Kᗮ))

Tactic:
refine le_trans ?_ (Submodule.le_topologicalClosure _)

Premises used: Submodule.le_topologicalClosure, le_trans
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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ᗮ)
rw : ⊤ ≤ K ⊔ Kᗮ
⊢ LE.le.{u_3} (α := Submodule 𝕜 E) ⊤ (⨆ (i : Bool), bif i then K else Kᗮ)

Tactic:
rw [iSup_bool_eq, cond, cond]

Premises used: cond, iSup_bool_eq
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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ᗮ

Tactic:
Codisjoint.top_le ?_

Premises used: Set.Mem, Codisjoint.top_le
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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ᗮ)
refine : Codisjoint K Kᗮ
⊢ ⊤ ≤ K ⊔ Kᗮ

Tactic:
refine Codisjoint.top_le ?_

Premises used: Codisjoint.top_le
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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ᗮ)
⊢ Codisjoint K Kᗮ

Tactic:
Submodule.isCompl_orthogonal_of_hasOrthogonalProjection.codisjoint

Premises used: Submodule.isCompl_orthogonal_of_hasOrthogonalProjection, IsCompl.codisjoint
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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ᗮ)
⊢ Codisjoint K Kᗮ

Tactic:
exact Submodule.isCompl_orthogonal_of_hasOrthogonalProjection.codisjoint

Premises used: Submodule.isCompl_orthogonal_of_hasOrthogonalProjection, IsCompl.codisjoint
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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₂ })
e_repr : b₁ = b₂
⊢ { repr := b₁ : HilbertBasis ι 𝕜 E } = { repr := b₂ }

Tactic:
congr
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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₂ })
e_repr : b₁.symm = b₂.symm
⊢ b₁ = b₂

Tactic:
apply LinearIsometryEquiv.symm_bijective.injective

Premises used: LinearIsometryEquiv.symm_bijective, Function.Bijective.injective
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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₂ })
e_repr : (↑b₁.symm : ↥(lp (fun (x : ι) ↦ 𝕜) 2) ≃L[𝕜] E) = (↑b₂.symm : ↥(lp (fun (x : ι) ↦ 𝕜) 2) ≃L[𝕜] E)
⊢ b₁.symm = b₂.symm

Tactic:
apply LinearIsometryEquiv.toContinuousLinearEquiv_injective

Premises used: LinearIsometryEquiv.toContinuousLinearEquiv_injective
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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₂ })
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)
⊢ (↑b₁.symm : ↥(lp (fun (x : ι) ↦ 𝕜) 2) ≃L[𝕜] E) = (↑b₂.symm : ↥(lp (fun (x : ι) ↦ 𝕜) 2) ≃L[𝕜] E)

Tactic:
apply ContinuousLinearEquiv.coe_injective

Premises used: ContinuousLinearEquiv.coe_injective
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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)

Tactic:
lp.ext_continuousLinearMap (ENNReal.ofNat_ne_top (n := nat_lit 2)) fun i => ?_

Premises used: ENNReal.ofNNReal, ENNReal.ofNat_ne_top, Set.Mem, setOf, NNReal.mk, lp.ext_continuousLinearMap, CauSeq.Completion.mk, WithTop.some
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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₂ })
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)
⊢ (↑(↑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:
refine lp.ext_continuousLinearMap (ENNReal.ofNat_ne_top (n := nat_lit 2)) fun i => ?_

Premises used: ENNReal.ofNat_ne_top, lp.ext_continuousLinearMap
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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 : ι
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)
⊢ (↑(↑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:
ext
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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 : ι
⊢ 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:
congr_fun h i

Premises used: Set.Mem, setOf, lp.single, congr_fun
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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 : ι
⊢ 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:
exact congr_fun h i

Premises used: congr_fun
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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 : ι
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)
⊢ 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)

Tactic:
dsimp +instances [instFunLike]

Premises used: HilbertBasis.instFunLike
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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.repr.symm : (a : ↥(lp (fun (x : ι) ↦ 𝕜) 2)) → E) (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i 1) : E)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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.repr.symm : (a : ↥(lp (fun (x : ι) ↦ 𝕜) 2)) → E) (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i 1) : E)

Tactic:
convert! rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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 (α := ↥(lp (fun (x : ι) ↦ 𝕜) 2))
    ((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) ((b : (a : ι) → E) i) : ↥(lp (fun (x : ι) ↦ 𝕜) 2))
    (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i 1 : ↥(lp (fun (x : ι) ↦ 𝕜) 2))

Tactic:
simp only [LinearIsometryEquiv.apply_symm_apply, ← b.repr_symm_single]

Premises used: LinearIsometryEquiv.apply_symm_apply, HilbertBasis.repr_symm_single
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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 := 𝕜) 1 ((↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) v) : (i : ι) → 𝕜) i)
⊢ (↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) v) : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i = ⟪(b : (a : ι) → E) i, v⟫

Tactic:
rw [← b.repr.inner_map_map (b i) v, b.repr_self, lp.inner_single_left]

Premises used: HilbertBasis.repr, LinearIsometryEquiv.inner_map_map, lp.inner_single_left, HilbertBasis.repr_self, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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 =
    inner 𝕜 (E := 𝕜) 1 ((↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) v) : (i : ι) → 𝕜) i)

Tactic:
simp