awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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
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)
⊢ 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)

Tactic:
ext
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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
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:
simp [b.orthogonalProjection_apply_eq_sum]

Premises used: OrthonormalBasis.orthogonalProjection_apply_eq_sum
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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
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)
⊢ 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)

Tactic:
ext
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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
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:
simp [starProjection, b.orthogonalProjection_eq_sum_rankOne]

Premises used: OrthonormalBasis.orthogonalProjection_eq_sum_rankOne, Submodule.starProjection
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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
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)
⊢ 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)

Tactic:
ext
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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
⊢ 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:
simp [b.sum_repr']

Premises used: OrthonormalBasis.sum_repr'
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
G : Type u_7
inst_4 : NormedAddCommGroup G
inst_5 : InnerProductSpace 𝕜 G
b : OrthonormalBasis ι 𝕜 E
L : E ≃ₗᵢ[𝕜] G
i : ι
⊢ Eq.{u_7 + 1} (α := G) ((b.map L : (a : ι) → G) i : G) ((L : (a : E) → G) ((b : (a : ι) → E) i : E) : G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
G : Type u_7
inst_4 : NormedAddCommGroup G
inst_5 : InnerProductSpace 𝕜 G
b : OrthonormalBasis ι 𝕜 E
L : E ≃ₗᵢ[𝕜] G
⊢ (b.map L).toBasis = b.toBasis.map L.toLinearEquiv

Tactic:
rfl

Premises used: Module.Basis.ofEquivFun, LinearEquiv.symm, Module.Basis.map, LinearEquiv.toEquiv, LinearEquiv.trans, rfl, OrthonormalBasis.toBasis
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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)
⊢ ⟪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:
simp [inner_sum, inner_smul_right, hv.inner_left_fintype, PiLp.inner_apply]

Premises used: inner_sum, Orthonormal.inner_left_fintype, inner_smul_right, PiLp.inner_apply
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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)
⊢ ⟪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]
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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))
⊢ ⟪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:
key
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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)
h₁ : y = ∑ 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⟫

Tactic:
convert! key
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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)
h₁ 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))
⊢ x = ∑ i : ι, HSMul.hSMul (β := E) (p.ofLp i) ((v : (a : ι) → E) i : E)

Tactic:
rw [← v.equivFun.symm_apply_apply x, v.equivFun_symm_apply]

Premises used: Module.Basis.equivFun_symm_apply, LinearEquiv.symm_apply_apply, Module.Basis.equivFun
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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) → ι → 𝕜) y : ι → 𝕜) : E)
    (∑ i : ι, HSMul.hSMul (β := E) (q.ofLp i) ((v : (a : ι) → E) i : E) : E)
h₁ h₂ :
  Eq.{u_4 + 1} (α := E)
    (∑ i : ι,
      HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (β := E) ((v.equivFun : (a : E) → ι → 𝕜) y i : 𝕜) ((v : (a : ι) → E) i : E))
    (∑ i : ι, HSMul.hSMul (β := E) (q.ofLp i) ((v : (a : ι) → E) i : E))
⊢ y = ∑ i : ι, HSMul.hSMul (β := E) (q.ofLp i) ((v : (a : ι) → E) i : E)

Tactic:
rw [← v.equivFun.symm_apply_apply y, v.equivFun_symm_apply]

Premises used: Module.Basis.equivFun_symm_apply, LinearEquiv.symm_apply_apply, Module.Basis.equivFun
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
v : Basis ι 𝕜 E
hv : Orthonormal.{u_3, u_4, u_1} 𝕜 (E := E) (ι := ι) (⇑v : (a : ι) → E)
⊢ Eq (α := (a : E) → EuclideanSpace 𝕜 ι) (⇑(repr (v.toOrthonormalBasis hv)) : (a : E) → EuclideanSpace 𝕜 ι)
    (⇑(v.equivFun ≪≫ₗ LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (ι → 𝕜))) : (a : E) → WithLp 2 (ι → 𝕜))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
v : Basis ι 𝕜 E
hv : Orthonormal.{u_3, u_4, u_1} 𝕜 (E := E) (ι := ι) (⇑v : (a : ι) → E)
⊢ Eq (α := (a : EuclideanSpace 𝕜 ι) → E)
    (⇑(LinearIsometryEquiv.symm (repr (v.toOrthonormalBasis hv))) : (a : EuclideanSpace 𝕜 ι) → E)
    (⇑(WithLp.linearEquiv 2 𝕜 (ι → 𝕜) ≪≫ₗ v.equivFun.symm) : (a : WithLp 2 (ι → 𝕜)) → E)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
v : Basis ι 𝕜 E
hv : Orthonormal.{u_3, u_4, u_1} 𝕜 (E := E) (ι := ι) (⇑v : (a : ι) → E)
simp :
  Basis.ofEquivFun
      (LinearEquiv.trans (M₂ := EuclideanSpace 𝕜 ι) (module_M₂ := WithLp.instModule 2 𝕜 ((i : ι) → 𝕜)) (σ₂₃ :=
        RingHom.id 𝕜) (σ₃₂ := RingHom.id 𝕜) (re₁₂ := ⋯) (re₂₃ := ⋯) (re₂₁ := ⋯) (re₃₂ := ⋯)
        (v.equivFun.trans (σ₂₃ := RingHom.id 𝕜) (σ₃₂ := RingHom.id 𝕜) (re₂₃ := ⋯) (re₃₂ := ⋯)
          (LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (ι → 𝕜))))
        (WithLp.linearEquiv 2 𝕜 (ι → 𝕜))) =
    v
⊢ OrthonormalBasis.toBasis (v.toOrthonormalBasis hv) = v

Tactic:
simp only [OrthonormalBasis.toBasis, Basis.toOrthonormalBasis,
    LinearEquiv.isometryOfInner_toLinearEquiv]

Premises used: LinearEquiv.isometryOfInner_toLinearEquiv, Module.Basis.toOrthonormalBasis, OrthonormalBasis.toBasis
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
v : Basis ι 𝕜 E
hv : Orthonormal.{u_3, u_4, u_1} 𝕜 (E := E) (ι := ι) (⇑v : (a : ι) → E)
⊢ Basis.ofEquivFun
      (LinearEquiv.trans (M₂ := EuclideanSpace 𝕜 ι) (module_M₂ := WithLp.instModule 2 𝕜 ((i : ι) → 𝕜)) (σ₂₃ :=
        RingHom.id 𝕜) (σ₃₂ := RingHom.id 𝕜) (re₁₂ := ⋯) (re₂₃ := ⋯) (re₂₁ := ⋯) (re₃₂ := ⋯)
        (v.equivFun.trans (σ₂₃ := RingHom.id 𝕜) (σ₃₂ := RingHom.id 𝕜) (re₂₃ := ⋯) (re₃₂ := ⋯)
          (LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (ι → 𝕜))))
        (WithLp.linearEquiv 2 𝕜 (ι → 𝕜))) =
    v

Tactic:
v.ofEquivFun_equivFun

Premises used: Module.Basis.ofEquivFun_equivFun, LinearEquiv.toEquiv, LinearEquiv.trans, Module.Basis.equivFun
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
v : Basis ι 𝕜 E
hv : Orthonormal.{u_3, u_4, u_1} 𝕜 (E := E) (ι := ι) (⇑v : (a : ι) → E)
⊢ Basis.ofEquivFun
      (LinearEquiv.trans (M₂ := EuclideanSpace 𝕜 ι) (module_M₂ := WithLp.instModule 2 𝕜 ((i : ι) → 𝕜)) (σ₂₃ :=
        RingHom.id 𝕜) (σ₃₂ := RingHom.id 𝕜) (re₁₂ := ⋯) (re₂₃ := ⋯) (re₂₁ := ⋯) (re₃₂ := ⋯)
        (v.equivFun.trans (σ₂₃ := RingHom.id 𝕜) (σ₃₂ := RingHom.id 𝕜) (re₂₃ := ⋯) (re₃₂ := ⋯)
          (LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (ι → 𝕜))))
        (WithLp.linearEquiv 2 𝕜 (ι → 𝕜))) =
    v

Tactic:
exact v.ofEquivFun_equivFun

Premises used: Module.Basis.ofEquivFun_equivFun
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
v : Basis ι 𝕜 E
hv : Orthonormal.{u_3, u_4, u_1} 𝕜 (E := E) (ι := ι) (⇑v : (a : ι) → E)
rw rw₁ : Eq (α := (a : ι) → E) (⇑(v.toOrthonormalBasis hv) : (a : ι) → E) (⇑(v.toOrthonormalBasis hv) : (a : ι) → E)
⊢ Eq (α := (a : ι) → E) (⇑(v.toOrthonormalBasis hv) : (a : ι) → E)
    (⇑(OrthonormalBasis.toBasis (v.toOrthonormalBasis hv)) : (a : ι) → E)

Tactic:
rw [OrthonormalBasis.coe_toBasis]

Premises used: OrthonormalBasis.coe_toBasis
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
v : Basis ι 𝕜 E
hv : Orthonormal.{u_3, u_4, u_1} 𝕜 (E := E) (ι := ι) (⇑v : (a : ι) → E)
classical classical₁ :
  Eq (α := (a : ι) → E) (⇑(v.toOrthonormalBasis hv) : (a : ι) → E) (⇑(v.toOrthonormalBasis hv) : (a : ι) → E)
⊢ Eq (α := (a : ι) → E) (⇑(v.toOrthonormalBasis hv) : (a : ι) → E)
    (⇑(OrthonormalBasis.toBasis (v.toOrthonormalBasis hv)) : (a : ι) → E)

Tactic:
classical rw [OrthonormalBasis.coe_toBasis]

Premises used: OrthonormalBasis.coe_toBasis
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
v : Basis ι 𝕜 E
hv : Orthonormal.{u_3, u_4, u_1} 𝕜 (E := E) (ι := ι) (⇑v : (a : ι) → E)
⊢ Eq (α := (a : ι) → E) (⇑(OrthonormalBasis.toBasis (v.toOrthonormalBasis hv)) : (a : ι) → E) (⇑v : (a : ι) → E)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι_1 : Type u_1
ι' : Type u_2
𝕜_1 : Type u_3
inst : RCLike 𝕜_1
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜_1 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 ι_1
ι : Type u_7
𝕜 : Type u_8
inst_8 : Unique ι
inst_9 : RCLike 𝕜
⊢ Orthonormal.{u_8, u_8, u_7} 𝕜 (E := 𝕜) (ι := ι) (⇑(Basis.singleton ι 𝕜) : (a : ι) → 𝕜)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_7
𝕜 : Type u_8
inst : Unique ι
inst_1 : RCLike 𝕜
i : ι
⊢ Eq.{u_8 + 1} (α := 𝕜) ((OrthonormalBasis.singleton ι 𝕜 : (a : ι) → 𝕜) i : 𝕜) (1 : 𝕜)

Tactic:
Basis.singleton_apply _ _ _

Premises used: Function.update, Pi.single, dite, Module.Basis.singleton_apply
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_7
𝕜 : Type u_8
inst : Unique ι
inst_1 : RCLike 𝕜
x : 𝕜
i : ι
⊢ ofLp (p := 2) ((repr (OrthonormalBasis.singleton ι 𝕜) : (a : 𝕜) → EuclideanSpace 𝕜 ι) x) i = x

Tactic:
Basis.singleton_repr _ _ _ _

Premises used: Function.update, Module.Basis.singleton_repr, Pi.single, dite
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_7
𝕜 : Type u_8
inst : Unique ι
inst_1 : RCLike 𝕜
h : ∀ (x : ι), Eq.{u_8 + 1} (α := 𝕜) ((OrthonormalBasis.singleton ι 𝕜 : (a : ι) → 𝕜) x : 𝕜) (1 x : 𝕜)
⊢ Eq (α := (a : ι) → 𝕜) (⇑(OrthonormalBasis.singleton ι 𝕜) : (a : ι) → 𝕜) 1

Tactic:
ext
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_7
𝕜 : Type u_8
inst : Unique ι
inst_1 : RCLike 𝕜
x : ι
⊢ Eq.{u_8 + 1} (α := 𝕜) ((OrthonormalBasis.singleton ι 𝕜 : (a : ι) → 𝕜) x : 𝕜) (1 x : 𝕜)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_7
𝕜 : Type u_8
inst : Unique ι
inst_1 : RCLike 𝕜
⊢ Eq (α := Basis ι 𝕜 𝕜) (OrthonormalBasis.toBasis (OrthonormalBasis.singleton ι 𝕜)) (Basis.singleton ι 𝕜)

Tactic:
Basis.toBasis_toOrthonormalBasis _ _

Premises used: Module.Basis.toBasis_toOrthonormalBasis, OrthonormalBasis.singleton
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
η : Type u_7
inst : Fintype η
ι : η → Type u_8
inst_1 : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst_2 : RCLike 𝕜
E : η → Type u_10
inst_3 : (i : η) → NormedAddCommGroup (E i)
inst_4 : (i : η) → InnerProductSpace.{u_9, u_10} 𝕜 (E i)
B : (i : η) → OrthonormalBasis.{u_8, u_9, u_10} (ι i) 𝕜 (E i)
a :
  ∀ (i : (i : η) × ι i) (i_1 : η),
    Eq.{u_10 + 1} (α := E i_1)
      (ofLp (p := 2)
        ((OrthonormalBasis.toBasis (Pi.orthonormalBasis (ι := ι) (E := E) B) : (a : (i : η) × ι i) → PiLp 2 E) i) i_1)
      (ofLp (p := 2)
        ((Basis.map (M := (j : η) → E j) (Pi.basis (ιs := ι) (Ms := E) fun (i : η) ↦ (B i).toBasis)
              (LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 ((j : η) → E j))) :
            (a : (i : η) × ι i) → PiLp 2 E)
          i)
        i_1)
⊢ Eq (α := Basis ((i : η) × ι i) 𝕜 (PiLp 2 E)) (OrthonormalBasis.toBasis (Pi.orthonormalBasis (ι := ι) (E := E) B))
    (Basis.map (M := (j : η) → E j) (Pi.basis (ιs := ι) (Ms := E) fun (i : η) ↦ (B i).toBasis)
      (LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 ((j : η) → E j))))

Tactic:
ext
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
η : Type u_7
inst : Fintype η
ι : η → Type u_8
inst_1 : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst_2 : RCLike 𝕜
E : η → Type u_10
inst_3 : (i : η) → NormedAddCommGroup (E i)
inst_4 : (i : η) → InnerProductSpace.{u_9, u_10} 𝕜 (E i)
B : (i : η) → OrthonormalBasis.{u_8, u_9, u_10} (ι i) 𝕜 (E i)
i : (i : η) × ι i
i_1 : η
⊢ Eq.{u_10 + 1} (α := E i_1)
    (ofLp (p := 2)
      ((OrthonormalBasis.toBasis (Pi.orthonormalBasis (ι := ι) (E := E) B) : (a : (i : η) × ι i) → PiLp 2 E) i) i_1)
    (ofLp (p := 2)
      ((Basis.map (M := (j : η) → E j) (Pi.basis (ιs := ι) (Ms := E) fun (i : η) ↦ (B i).toBasis)
            (LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 ((j : η) → E j))) :
          (a : (i : η) × ι i) → PiLp 2 E)
        i)
      i_1)

Tactic:
rfl
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
η : Type u_7
inst : Fintype η
inst_1 : DecidableEq η
ι : η → Type u_8
inst_2 : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst_3 : RCLike 𝕜
E : η → Type u_10
inst_4 : (i : η) → NormedAddCommGroup (E i)
inst_5 : (i : η) → InnerProductSpace.{u_9, u_10} 𝕜 (E i)
B : (i : η) → OrthonormalBasis.{u_8, u_9, u_10} (ι i) 𝕜 (E i)
j : (i : η) × ι i
h :
  ∀ (k : η),
    Eq.{u_10 + 1} (α := E k)
      (ofLp (p := 2) ((Pi.orthonormalBasis (ι := ι) (E := E) B : (a : (i : η) × ι i) → PiLp 2 E) j) k : E k)
      (ofLp (p := 2)
          (PiLp.single 2 (β := E) (j.fst (β := fun (i : η) ↦ ι i))
            ((B (j.fst (β := fun (i : η) ↦ ι i)) : (a : ι j.fst) → E j.fst) (j.snd (β := fun (i : η) ↦ ι i))))
          k :
        E k)
⊢ Eq (α := PiLp 2 E) ((Pi.orthonormalBasis (ι := ι) (E := E) B : (a : (i : η) × ι i) → PiLp 2 E) j : PiLp 2 E)
    (PiLp.single 2 (β := E) (j.fst (β := fun (i : η) ↦ ι i))
        ((B (j.fst (β := fun (i : η) ↦ ι i)) : (a : ι j.fst) → E j.fst) (j.snd (β := fun (i : η) ↦ ι i))) :
      PiLp 2 E)

Tactic:
ext k