awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ι
inst_8 : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily.{u_3, u_4, u_1, u_4} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
e₁ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] (i : ι) → ↥(V i) := linearEquivFunOnFintype 𝕜 ι fun (i : ι) ↦ ↥(V i)
e₂ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] E := LinearEquiv.ofBijective (coeLinearMap V) hV
this :
  ∀ (v w : PiLp.{u_1, u_4} 2 fun (i : ι) ↦ ↥(V i)),
    ⟪v, w⟫ =
      inner.{u_3, u_4} 𝕜 (E := E)
        ((e₂ : (a : ⨁ (i : ι), ↥(V i)) → E)
            ((e₁.symm : (a : (i : ι) → ↥(V i)) → ⨁ (i : ι), ↥(V i)) v.ofLp : ⨁ (i : ι), ↥(V i)) :
          E)
        ((e₂ : (a : ⨁ (i : ι), ↥(V i)) → E)
            ((e₁.symm : (a : (i : ι) → ↥(V i)) → ⨁ (i : ι), ↥(V i)) w.ofLp : ⨁ (i : ι), ↥(V i)) :
          E)
v₀ w₀ : E
⊢ w₀ =
    (e₂ : (a : ⨁ (i : ι), ↥(V i)) → E)
      ((e₁.symm : (a : (i : ι) → ↥(V i)) → ⨁ (i : ι), ↥(V i))
          (ofLp (p := 2)
            (toLp 2
              ((e₁ : (a : ⨁ (i : ι), ↥(V i)) → (i : ι) → ↥(V i))
                ((e₂.symm : (a : E) → ⨁ (i : ι), ↥(V i)) w₀ : ⨁ (i : ι), ↥(V i))))) :
        ⨁ (i : ι), ↥(V i))

Tactic:
simp
-- 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 ι
inst_8 : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily.{u_3, u_4, u_1, u_4} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
e₁ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] (i : ι) → ↥(V i) := linearEquivFunOnFintype 𝕜 ι fun (i : ι) ↦ ↥(V i)
e₂ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] E := LinearEquiv.ofBijective (coeLinearMap V) hV
suffices :
  ∀ (v w : PiLp.{u_1, u_4} 2 fun (i : ι) ↦ ↥(V i)),
    ⟪v, w⟫ =
      inner.{u_3, u_4} 𝕜 (E := E)
        ((e₂ : (a : ⨁ (i : ι), ↥(V i)) → E)
            ((e₁.symm : (a : (i : ι) → ↥(V i)) → ⨁ (i : ι), ↥(V i)) v.ofLp : ⨁ (i : ι), ↥(V i)) :
          E)
        ((e₂ : (a : ⨁ (i : ι), ↥(V i)) → E)
            ((e₁.symm : (a : (i : ι) → ↥(V i)) → ⨁ (i : ι), ↥(V i)) w.ofLp : ⨁ (i : ι), ↥(V i)) :
          E)
⊢ ∀ (x y : E),
    inner 𝕜 (E := PiLp.{u_1, u_4} 2 fun (i : ι) ↦ ↥(V i))
        ((e₂.symm ≪≫ₗ e₁ ≪≫ₗ LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 ((i : ι) → ↥(V i))) :
              (a : E) → PiLp 2 fun (i : ι) ↦ ↥(V i))
            x :
          PiLp.{u_1, u_4} 2 fun (i : ι) ↦ ↥(V i))
        ((e₂.symm ≪≫ₗ e₁ ≪≫ₗ LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 ((i : ι) → ↥(V i))) :
              (a : E) → PiLp 2 fun (i : ι) ↦ ↥(V i))
            y :
          PiLp.{u_1, u_4} 2 fun (i : ι) ↦ ↥(V i)) =
      ⟪x, y⟫

Tactic:
suffices ∀ (v w : PiLp 2 fun i => V i), ⟪v, w⟫ = ⟪e₂ (e₁.symm v), e₂ (e₁.symm w)⟫ by
    intro v₀ w₀
    simp only [LinearEquiv.trans_apply]
    convert! this (toLp 2 (e₁ (e₂.symm v₀))) (toLp 2 (e₁ (e₂.symm w₀))) <;> simp
-- 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 ι
inst_8 : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily.{u_3, u_4, u_1, u_4} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
e₁ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] (i : ι) → ↥(V i) := linearEquivFunOnFintype 𝕜 ι fun (i : ι) ↦ ↥(V i)
e₂ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] E := LinearEquiv.ofBijective (coeLinearMap V) hV
v w : PiLp.{u_1, u_4} 2 fun (i : ι) ↦ ↥(V i)
trans :
  ⟪v, w⟫ =
    inner.{u_3, u_4} 𝕜 (E := E) (∑ i : ι, ((V i).subtypeₗᵢ : (a : ↥(V i)) → E) (v.ofLp i))
      (∑ i : ι, ((V i).subtypeₗᵢ : (a : ↥(V i)) → E) (w.ofLp i))
trans₁ :
  inner.{u_3, u_4} 𝕜 (E := E) (∑ i : ι, ((V i).subtypeₗᵢ : (a : ↥(V i)) → E) (v.ofLp i))
      (∑ i : ι, ((V i).subtypeₗᵢ : (a : ↥(V i)) → E) (w.ofLp i)) =
    inner.{u_3, u_4} 𝕜 (E := E)
      ((e₂ : (a : ⨁ (i : ι), ↥(V i)) → E)
          ((e₁.symm : (a : (i : ι) → ↥(V i)) → ⨁ (i : ι), ↥(V i)) v.ofLp : ⨁ (i : ι), ↥(V i)) :
        E)
      ((e₂ : (a : ⨁ (i : ι), ↥(V i)) → E)
          ((e₁.symm : (a : (i : ι) → ↥(V i)) → ⨁ (i : ι), ↥(V i)) w.ofLp : ⨁ (i : ι), ↥(V i)) :
        E)
⊢ ⟪v, w⟫ =
    inner.{u_3, u_4} 𝕜 (E := E)
      ((e₂ : (a : ⨁ (i : ι), ↥(V i)) → E)
          ((e₁.symm : (a : (i : ι) → ↥(V i)) → ⨁ (i : ι), ↥(V i)) v.ofLp : ⨁ (i : ι), ↥(V i)) :
        E)
      ((e₂ : (a : ⨁ (i : ι), ↥(V i)) → E)
          ((e₁.symm : (a : (i : ι) → ↥(V i)) → ⨁ (i : ι), ↥(V i)) w.ofLp : ⨁ (i : ι), ↥(V i)) :
        E)

Tactic:
trans ⟪∑ i, (V i).subtypeₗᵢ (v i), ∑ i, (V i).subtypeₗᵢ (w i)⟫
-- 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 ι
inst_8 : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily.{u_3, u_4, u_1, u_4} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
e₁ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] (i : ι) → ↥(V i) := linearEquivFunOnFintype 𝕜 ι fun (i : ι) ↦ ↥(V i)
e₂ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] E := LinearEquiv.ofBijective (coeLinearMap V) hV
v w : PiLp.{u_1, u_4} 2 fun (i : ι) ↦ ↥(V i)
⊢ ⟪v, w⟫ =
    inner.{u_3, u_4} 𝕜 (E := E) (∑ i : ι, ((V i).subtypeₗᵢ : (a : ↥(V i)) → E) (v.ofLp i))
      (∑ i : ι, ((V i).subtypeₗᵢ : (a : ↥(V i)) → E) (w.ofLp i))

Tactic:
simp only [sum_inner, hV'.inner_right_fintype, PiLp.inner_apply]

Premises used: sum_inner, PiLp.inner_apply, OrthogonalFamily.inner_right_fintype
-- 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 ι
inst_8 : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily.{u_3, u_4, u_1, u_4} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
e₁ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] (i : ι) → ↥(V i) := linearEquivFunOnFintype 𝕜 ι fun (i : ι) ↦ ↥(V i)
e₂ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] E := LinearEquiv.ofBijective (coeLinearMap V) hV
v w : PiLp.{u_1, u_4} 2 fun (i : ι) ↦ ↥(V i)
e_a :
  Eq.{u_1 + 1} (α := Finset ι) Finset.univ
    (Multiset.toFinset
      (↑(Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ v.ofLp i = 0) (Finset.val Finset.univ) ⋯) :
        Multiset ι))
e_a₁ :
  Eq.{u_1 + 1} (α := Finset ι) Finset.univ
    (Multiset.toFinset
      (↑(Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ w.ofLp i = 0) (Finset.val Finset.univ) ⋯) :
        Multiset ι))
⊢ inner.{u_3, u_4} 𝕜 (E := E) (∑ i : ι, ((V i).subtypeₗᵢ : (a : ↥(V i)) → E) (v.ofLp i))
      (∑ i : ι, ((V i).subtypeₗᵢ : (a : ↥(V i)) → E) (w.ofLp i)) =
    inner.{u_3, u_4} 𝕜 (E := E)
      ((e₂ : (a : ⨁ (i : ι), ↥(V i)) → E)
          ((e₁.symm : (a : (i : ι) → ↥(V i)) → ⨁ (i : ι), ↥(V i)) v.ofLp : ⨁ (i : ι), ↥(V i)) :
        E)
      ((e₂ : (a : ⨁ (i : ι), ↥(V i)) → E)
          ((e₁.symm : (a : (i : ι) → ↥(V i)) → ⨁ (i : ι), ↥(V i)) w.ofLp : ⨁ (i : ι), ↥(V i)) :
        E)

Tactic:
congr
-- 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 ι
inst_8 : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily.{u_3, u_4, u_1, u_4} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
e₁ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] (i : ι) → ↥(V i) := linearEquivFunOnFintype 𝕜 ι fun (i : ι) ↦ ↥(V i)
e₂ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] E := LinearEquiv.ofBijective (coeLinearMap V) hV
v w : PiLp.{u_1, u_4} 2 fun (i : ι) ↦ ↥(V i)
⊢ Eq.{u_1 + 1} (α := Finset ι) Finset.univ
    (Multiset.toFinset
      (↑(Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ v.ofLp i = 0) (Finset.val Finset.univ) ⋯) :
        Multiset ι))

Tactic:
simp
-- 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 ι
inst_8 : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily.{u_3, u_4, u_1, u_4} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
e₁ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] (i : ι) → ↥(V i) := linearEquivFunOnFintype 𝕜 ι fun (i : ι) ↦ ↥(V i)
e₂ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] E := LinearEquiv.ofBijective (coeLinearMap V) hV
v w : PiLp.{u_1, u_4} 2 fun (i : ι) ↦ ↥(V i)
⊢ Eq.{u_1 + 1} (α := Finset ι) Finset.univ
    (Multiset.toFinset
      (↑(Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ w.ofLp i = 0) (Finset.val Finset.univ) ⋯) :
        Multiset ι))

Tactic:
simp
-- 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 ι
inst_4 : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily.{u_3, u_4, u_1, u_4} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
w : PiLp.{u_1, u_4} 2 fun (i : ι) ↦ ↥(V i)
e₁ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] (i : ι) → ↥(V i) := linearEquivFunOnFintype 𝕜 ι fun (i : ι) ↦ ↥(V i)
e₂ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] E := LinearEquiv.ofBijective (coeLinearMap V) hV
this :
  ∀ (v : ⨁ (i : ι), ↥(V i)),
    Eq.{u_4 + 1} (α := E) ((e₂ : (a : ⨁ (i : ι), ↥(V i)) → E) v : E)
      (∑ i : ι, (↑((e₁ : (a : ⨁ (i : ι), ↥(V i)) → (i : ι) → ↥(V i)) v i) : E) : E)
⊢ Eq.{u_4 + 1} (α := E)
    ((LinearIsometryEquiv.symm (hV.isometryL2OfOrthogonalFamily hV') : (a : PiLp 2 fun (i : ι) ↦ ↥(V i)) → E) w : E)
    (∑ i : ι, (↑(w.ofLp i) : E) : E)

Tactic:
this (e₁.symm w)

Premises used: Multiset.sum, Multiset.foldr, LinearEquiv.symm, WithLp.ofLp, DFunLike.coe, Finset.sum, Trunc.lift
-- 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 ι
inst_4 : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily.{u_3, u_4, u_1, u_4} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
w : PiLp.{u_1, u_4} 2 fun (i : ι) ↦ ↥(V i)
e₁ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] (i : ι) → ↥(V i) := linearEquivFunOnFintype 𝕜 ι fun (i : ι) ↦ ↥(V i)
e₂ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] E := LinearEquiv.ofBijective (coeLinearMap V) hV
this :
  ∀ (v : ⨁ (i : ι), ↥(V i)),
    Eq.{u_4 + 1} (α := E) ((e₂ : (a : ⨁ (i : ι), ↥(V i)) → E) v : E)
      (∑ i : ι, (↑((e₁ : (a : ⨁ (i : ι), ↥(V i)) → (i : ι) → ↥(V i)) v i) : E) : E)
⊢ Eq.{u_4 + 1} (α := E)
    ((LinearIsometryEquiv.symm (hV.isometryL2OfOrthogonalFamily hV') : (a : PiLp 2 fun (i : ι) ↦ ↥(V i)) → E) w : E)
    (∑ i : ι, (↑(w.ofLp i) : E) : E)

Tactic:
exact this (e₁.symm w)

Premises used: LinearEquiv.symm, WithLp.ofLp, DFunLike.coe
-- 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 ι
inst_4 : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily.{u_3, u_4, u_1, u_4} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
w : PiLp.{u_1, u_4} 2 fun (i : ι) ↦ ↥(V i)
e₁ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] (i : ι) → ↥(V i) := linearEquivFunOnFintype 𝕜 ι fun (i : ι) ↦ ↥(V i)
e₂ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] E := LinearEquiv.ofBijective (coeLinearMap V) hV
suffices :
  ∀ (v : ⨁ (i : ι), ↥(V i)),
    Eq.{u_4 + 1} (α := E) ((e₂ : (a : ⨁ (i : ι), ↥(V i)) → E) v : E)
      (∑ i : ι, (↑((e₁ : (a : ⨁ (i : ι), ↥(V i)) → (i : ι) → ↥(V i)) v i) : E) : E)
⊢ Eq.{u_4 + 1} (α := E)
    ((LinearIsometryEquiv.symm (hV.isometryL2OfOrthogonalFamily hV') : (a : PiLp 2 fun (i : ι) ↦ ↥(V i)) → E) w : E)
    (∑ i : ι, (↑(w.ofLp i) : E) : E)

Tactic:
suffices ∀ v : ⨁ i, V i, e₂ v = ∑ i, e₁ v i by exact this (e₁.symm w)
-- 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 ι
inst_4 : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily.{u_3, u_4, u_1, u_4} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
w : PiLp.{u_1, u_4} 2 fun (i : ι) ↦ ↥(V i)
e₁ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] (i : ι) → ↥(V i) := linearEquivFunOnFintype 𝕜 ι fun (i : ι) ↦ ↥(V i)
e₂ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] E := LinearEquiv.ofBijective (coeLinearMap V) hV
⊢ ∀ (v : ⨁ (i : ι), ↥(V i)),
    Eq.{u_4 + 1} (α := E) ((e₂ : (a : ⨁ (i : ι), ↥(V i)) → E) v : E)
      (∑ i : ι, (↑((e₁ : (a : ⨁ (i : ι), ↥(V i)) → (i : ι) → ↥(V i)) v i) : E) : E)

Tactic:
simp [e₁, e₂, DirectSum.coeLinearMap, DirectSum.toModule, DFinsupp.lsum,
      DFinsupp.sumAddHom_apply]

Premises used: DFinsupp.lsum, DirectSum.toModule, DFinsupp.sumAddHom_apply, DirectSum.coeLinearMap
-- 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 ι
inst_4 : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily.{u_3, u_4, u_1, u_4} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
w : PiLp.{u_1, u_4} 2 fun (i : ι) ↦ ↥(V i)
let let₁ let₂ let₃ :
  Eq.{u_4 + 1} (α := E)
    ((LinearIsometryEquiv.symm (hV.isometryL2OfOrthogonalFamily hV') : (a : PiLp 2 fun (i : ι) ↦ ↥(V i)) → E) w : E)
    (∑ i : ι, (↑(w.ofLp i) : E) : E)
let₄ :
  let e₁ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] (i : ι) → ↥(V i) := linearEquivFunOnFintype 𝕜 ι fun (i : ι) ↦ ↥(V i);
  let e₂ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] E := LinearEquiv.ofBijective (coeLinearMap V) hV;
  ∀ (v : ⨁ (i : ι), ↥(V i)),
    Eq.{u_4 + 1} (α := E) ((e₂ : (a : ⨁ (i : ι), ↥(V i)) → E) v : E)
      (∑ i : ι, (↑((e₁ : (a : ⨁ (i : ι), ↥(V i)) → (i : ι) → ↥(V i)) v i) : E) : E)
⊢ Eq.{u_4 + 1} (α := E)
    ((LinearIsometryEquiv.symm (hV.isometryL2OfOrthogonalFamily hV') : (a : PiLp 2 fun (i : ι) ↦ ↥(V i)) → E) w : E)
    (∑ i : ι, (↑(w.ofLp i) : E) : E)

Tactic:
classical
    let e₁ := DirectSum.linearEquivFunOnFintype 𝕜 ι fun i => V i
    let e₂ := LinearEquiv.ofBijective (DirectSum.coeLinearMap V) hV
    suffices ∀ v : ⨁ i, V i, e₂ v = ∑ i, e₁ v i by exact this (e₁.symm w)
    simp [e₁, e₂, DirectSum.coeLinearMap, DirectSum.toModule, DFinsupp.lsum,
      DFinsupp.sumAddHom_apply]

Premises used: DFinsupp.lsum, DirectSum.toModule, DFinsupp.sumAddHom_apply, DirectSum.coeLinearMap
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_7
𝕜 : Type u_8
inst : RCLike 𝕜
i : ι
⊢ Eq (α := (a : EuclideanSpace 𝕜 ι) → 𝕜) (⇑(proj i) : (a : EuclideanSpace 𝕜 ι) → 𝕜) fun (x : EuclideanSpace 𝕜 ι) ↦
    x.ofLp i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
inst_1 : DecidableEq ι
i : ι
a : 𝕜
⊢ (single i a).ofLp = Pi.single (M := fun (x : ι) ↦ 𝕜) i a

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
inst_1 : DecidableEq ι
i : ι
a : 𝕜
⊢ toLp 2 (Pi.single (M := fun (x : ι) ↦ 𝕜) i a) = single i a

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
inst_1 : DecidableEq ι
i : ι
a : 𝕜
j : ι
⊢ (single i a).ofLp j = if j = i then a else 0

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
inst_1 : DecidableEq ι
i : ι
a : 𝕜
⊢ single i a = 0 ↔ a = 0

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
inst_1 : DecidableEq ι
inst_2 : Fintype ι
i : ι
a : 𝕜
v : EuclideanSpace 𝕜 ι
⊢ ⟪single i a, v⟫ = HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) a : 𝕜) (v.ofLp i)

Tactic:
simp [PiLp.inner_apply, apply_ite conj, mul_comm]

Premises used: apply_ite, mul_comm, PiLp.inner_apply, starRingEnd, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
inst_1 : DecidableEq ι
inst_2 : Fintype ι
i : ι
a : 𝕜
v : EuclideanSpace 𝕜 ι
⊢ ⟪v, single i a⟫ = a * (starRingEnd ((fun (x : ι) ↦ 𝕜) i) : (a : (fun (x : ι) ↦ 𝕜) i) → (fun (x : ι) ↦ 𝕜) i) (v.ofLp i)

Tactic:
simp [PiLp.inner_apply]

Premises used: PiLp.inner_apply
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
inst_1 : DecidableEq ι
inst_2 : Fintype ι
i : ι
a : 𝕜
⊢ ‖single i a‖ = ‖a‖

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
inst_1 : DecidableEq ι
inst_2 : Fintype ι
i : ι
a : 𝕜
⊢ ‖single i a‖₊ = ‖a‖₊

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
inst_1 : DecidableEq ι
inst_2 : Fintype ι
i : ι
a b : 𝕜
⊢ dist (single i a) (single i b) = dist a b

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
inst_1 : DecidableEq ι
inst_2 : Fintype ι
i : ι
a b : 𝕜
⊢ nndist (single i a) (single i b) = nndist a b

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
inst_1 : DecidableEq ι
inst_2 : Fintype ι
i : ι
a b : 𝕜
⊢ edist (single i a) (single i b) = edist a b

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
inst_1 : DecidableEq ι
inst_2 : Fintype ι
simp_rw : ∀ (i j : ι), True
⊢ Orthonormal 𝕜 (E := EuclideanSpace 𝕜 ι) fun (i : ι) ↦ single i 1

Tactic:
simp_rw [orthonormal_iff_ite, EuclideanSpace.inner_single_left, map_one, one_mul,
    PiLp.single_apply]

Premises used: EuclideanSpace.inner_single_left, PiLp.single_apply, map_one, orthonormal_iff_ite, one_mul
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
inst_1 : DecidableEq ι
inst_2 : Fintype ι
i j : ι
⊢ True

Tactic:
trivial
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
inst_1 : DecidableEq ι
inst_2 : Fintype ι
ι' : Type u_7
inst_3 : Fintype ι'
inst_4 : DecidableEq ι'
e : ι' ≃ ι
i' : ι'
v : 𝕜
⊢ Eq (α := PiLp.{u_1, u_3} 2 fun (x : ι) ↦ 𝕜)
    ((LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e : (a : PiLp 2 fun (x : ι') ↦ 𝕜) → PiLp 2 fun (x : ι) ↦ 𝕜)
        (single i' v) :
      PiLp.{u_1, u_3} 2 fun (x : ι) ↦ 𝕜)
    (single ((e : (a : ι') → ι) i') v : EuclideanSpace 𝕜 ι)

Tactic:
LinearIsometryEquiv.piLpCongrLeft_single e i' _

Premises used: LinearIsometryEquiv.piLpCongrLeft_single
-- 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 ι
f g : OrthonormalBasis ι 𝕜 E
h : f.repr = g.repr
ofRepr :
  ∀ (repr : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι) (h : { repr := repr : OrthonormalBasis ι 𝕜 E }.repr = g.repr),
    { repr := repr : OrthonormalBasis ι 𝕜 E } = g
⊢ f = g

Tactic:
cases f
-- 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 : OrthonormalBasis ι 𝕜 E
repr : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι
h : { repr := repr : OrthonormalBasis ι 𝕜 E }.repr = g.repr
ofRepr :
  ∀ (repr_1 : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι)
    (h : { repr := repr : OrthonormalBasis ι 𝕜 E }.repr = { repr := repr_1 }.repr),
    { repr := repr : OrthonormalBasis ι 𝕜 E } = { repr := repr_1 }
⊢ { repr := repr : OrthonormalBasis ι 𝕜 E } = g

Tactic:
cases g
-- 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 ι
repr repr_1 : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι
h : { repr := repr : OrthonormalBasis ι 𝕜 E }.repr = { repr := repr_1 }.repr
⊢ { repr := repr : OrthonormalBasis ι 𝕜 E } = { repr := repr_1 }

Tactic:
congr
-- 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 ι
b : OrthonormalBasis ι 𝕜 E
i : ι
⊢ E

Tactic:
exact b.repr.symm (EuclideanSpace.single i (1 : 𝕜))

Premises used: LinearIsometryEquiv.symm, OrthonormalBasis.repr, EuclideanSpace.single, OfNat.ofNat, DFunLike.coe
-- 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 ι
b : OrthonormalBasis ι 𝕜 E
i : ι
⊢ E

Tactic:
classical exact b.repr.symm (EuclideanSpace.single i (1 : 𝕜))
-- 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 ι
b b' : OrthonormalBasis ι 𝕜 E
h :
  Eq (α := (a : ι) → E)
    ((fun (b : OrthonormalBasis ι 𝕜 E) (i : ι) ↦
        ((b.repr.symm : (a : EuclideanSpace 𝕜 ι) → E) (EuclideanSpace.single i 1) : E))
      b)
    ((fun (b : OrthonormalBasis ι 𝕜 E) (i : ι) ↦
        ((b.repr.symm : (a : EuclideanSpace 𝕜 ι) → E) (EuclideanSpace.single i 1) : E))
      b')
rw :
  (↑b.repr.symm : EuclideanSpace 𝕜 ι →ₗ[𝕜] E) ∘ₗ
      (↑(LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (ι → 𝕜))) : (ι → 𝕜) →ₗ[𝕜] WithLp 2 (ι → 𝕜)) =
    (↑b'.repr.symm : EuclideanSpace 𝕜 ι →ₗ[𝕜] E) ∘ₗ
      (↑(LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (ι → 𝕜))) : (ι → 𝕜) →ₗ[𝕜] WithLp 2 (ι → 𝕜))
⊢ (↑b.repr.symm : EuclideanSpace 𝕜 ι →ₗ[𝕜] E) = (↑b'.repr.symm : EuclideanSpace 𝕜 ι →ₗ[𝕜] E)

Tactic:
rw [← LinearMap.cancel_right (WithLp.linearEquiv 2 𝕜 (_ → 𝕜)).symm.surjective]

Premises used: LinearEquiv.symm, LinearEquiv.surjective, LinearMap.cancel_right, OfNat.ofNat, WithLp.linearEquiv