awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
n : Type u_7
inst : Fintype n
r : ℝ
hr : 0 ≤ r
h :
  ∀ (x : EuclideanSpace ℝ n),
    Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.ball 0 r) x ↔
      Membership.mem (γ := Set (EuclideanSpace ℝ n))
        {x : EuclideanSpace ℝ n | ∑ i : n, HPow.hPow (β := ℕ) (x.ofLp i) 2 < HPow.hPow (β := ℕ) r 2} x
⊢ Eq.{u_7 + 1} (α := Set (EuclideanSpace ℝ n)) (Metric.ball 0 r)
    {x : EuclideanSpace ℝ n | ∑ i : n, HPow.hPow (β := ℕ) (x.ofLp i) 2 < HPow.hPow (β := ℕ) r 2}

Tactic:
ext x
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
n : Type u_7
inst : Fintype n
r : ℝ
hr : 0 ≤ r
x : EuclideanSpace ℝ n
⊢ LE.le (α := ℝ) 0 (∑ i : n, HPow.hPow (β := ℕ) (x.ofLp i) 2)

Tactic:
have : (0 : ℝ) ≤ ∑ i, x i ^ 2 := Finset.sum_nonneg fun _ _ => sq_nonneg _
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
n : Type u_7
inst : Fintype n
r : ℝ
hr : 0 ≤ r
x : EuclideanSpace ℝ n
this : LE.le (α := ℝ) 0 (∑ i : n, HPow.hPow (β := ℕ) (x.ofLp i) 2)
h h₁ :
  Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.ball 0 r) x ↔
    Membership.mem (γ := Set (EuclideanSpace ℝ n))
      {x : EuclideanSpace ℝ n | ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 < HPow.hPow (β := ℕ) r 2} x
h₂ :
  Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.ball 0 r) x ↔
    ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 < HPow.hPow (β := ℕ) r 2
h₃ : ‖x‖ < r ↔ ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 < HPow.hPow (β := ℕ) r 2
h₄ :
  √(∑ x_1 : n, HPow.hPow (β := ℕ) ‖x.ofLp x_1‖ 2) < r ↔
    ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 < HPow.hPow (β := ℕ) r 2
h₅ :
  √(∑ x_1 : n, HPow.hPow (β := ℕ) |x.ofLp x_1| 2) < r ↔
    ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 < HPow.hPow (β := ℕ) r 2
h₆ :
  √(∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2) < r ↔
    ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 < HPow.hPow (β := ℕ) r 2
⊢ Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.ball 0 r) x ↔
    Membership.mem (γ := Set (EuclideanSpace ℝ n))
      {x : EuclideanSpace ℝ n | ∑ i : n, HPow.hPow (β := ℕ) (x.ofLp i) 2 < HPow.hPow (β := ℕ) r 2} x

Tactic:
simp_rw [mem_setOf, mem_ball_zero_iff, norm_eq, norm_eq_abs, sq_abs, sqrt_lt this hr]

Premises used: Set.mem_setOf, EuclideanSpace.norm_eq, sq_abs, Real.sqrt_lt, Real.norm_eq_abs, mem_ball_zero_iff
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
n : Type u_7
inst : Fintype n
r : ℝ
hr : 0 ≤ r
h :
  ∀ (x : EuclideanSpace ℝ n),
    Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.closedBall 0 r) x ↔
      Membership.mem (γ := Set (EuclideanSpace ℝ n))
        {x : EuclideanSpace ℝ n | ∑ i : n, HPow.hPow (β := ℕ) (x.ofLp i) 2 ≤ HPow.hPow (β := ℕ) r 2} x
⊢ Eq.{u_7 + 1} (α := Set (EuclideanSpace ℝ n)) (Metric.closedBall 0 r)
    {x : EuclideanSpace ℝ n | ∑ i : n, HPow.hPow (β := ℕ) (x.ofLp i) 2 ≤ HPow.hPow (β := ℕ) r 2}

Tactic:
ext
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
n : Type u_7
inst : Fintype n
r : ℝ
hr : 0 ≤ r
x : EuclideanSpace ℝ n
h h₁ :
  Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.closedBall 0 r) x ↔
    Membership.mem (γ := Set (EuclideanSpace ℝ n))
      {x : EuclideanSpace ℝ n | ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 ≤ HPow.hPow (β := ℕ) r 2} x
h₂ :
  Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.closedBall 0 r) x ↔
    ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 ≤ HPow.hPow (β := ℕ) r 2
h₃ : ‖x‖ ≤ r ↔ ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 ≤ HPow.hPow (β := ℕ) r 2
h₄ :
  √(∑ x_1 : n, HPow.hPow (β := ℕ) ‖x.ofLp x_1‖ 2) ≤ r ↔
    ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 ≤ HPow.hPow (β := ℕ) r 2
h₅ :
  √(∑ x_1 : n, HPow.hPow (β := ℕ) |x.ofLp x_1| 2) ≤ r ↔
    ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 ≤ HPow.hPow (β := ℕ) r 2
h₆ :
  √(∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2) ≤ r ↔
    ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 ≤ HPow.hPow (β := ℕ) r 2
⊢ Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.closedBall 0 r) x ↔
    Membership.mem (γ := Set (EuclideanSpace ℝ n))
      {x : EuclideanSpace ℝ n | ∑ i : n, HPow.hPow (β := ℕ) (x.ofLp i) 2 ≤ HPow.hPow (β := ℕ) r 2} x

Tactic:
simp_rw [mem_setOf, mem_closedBall_zero_iff, norm_eq, norm_eq_abs, sq_abs, sqrt_le_left hr]

Premises used: Set.mem_setOf, EuclideanSpace.norm_eq, Real.sqrt_le_left, sq_abs, mem_closedBall_zero_iff, Real.norm_eq_abs
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
n : Type u_7
inst : Fintype n
r : ℝ
hr : 0 ≤ r
h :
  ∀ (x : EuclideanSpace ℝ n),
    Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.sphere 0 r) x ↔
      Membership.mem (γ := Set (EuclideanSpace ℝ n))
        {x : EuclideanSpace ℝ n | ∑ i : n, HPow.hPow (β := ℕ) (x.ofLp i) 2 = HPow.hPow (β := ℕ) r 2} x
⊢ Eq.{u_7 + 1} (α := Set (EuclideanSpace ℝ n)) (Metric.sphere 0 r)
    {x : EuclideanSpace ℝ n | ∑ i : n, HPow.hPow (β := ℕ) (x.ofLp i) 2 = HPow.hPow (β := ℕ) r 2}

Tactic:
ext x
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
n : Type u_7
inst : Fintype n
r : ℝ
hr : 0 ≤ r
x : EuclideanSpace ℝ n
this : LE.le (α := ℝ) 0 (∑ i : n, HPow.hPow (β := ℕ) (x.ofLp i) 2)
h h₁ :
  Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.sphere 0 r) x ↔
    Membership.mem (γ := Set (EuclideanSpace ℝ n))
      {x : EuclideanSpace ℝ n | ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 = HPow.hPow (β := ℕ) r 2} x
h₂ :
  Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.sphere 0 r) x ↔
    ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 = HPow.hPow (β := ℕ) r 2
h₃ : ‖x‖ = r ↔ ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 = HPow.hPow (β := ℕ) r 2
h₄ :
  √(∑ x_1 : n, HPow.hPow (β := ℕ) ‖x.ofLp x_1‖ 2) = r ↔
    ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 = HPow.hPow (β := ℕ) r 2
h₅ :
  √(∑ x_1 : n, HPow.hPow (β := ℕ) |x.ofLp x_1| 2) = r ↔
    ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 = HPow.hPow (β := ℕ) r 2
h₆ :
  √(∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2) = r ↔
    ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 = HPow.hPow (β := ℕ) r 2
⊢ Membership.mem (γ := Set (EuclideanSpace ℝ n)) (Metric.sphere 0 r) x ↔
    Membership.mem (γ := Set (EuclideanSpace ℝ n))
      {x : EuclideanSpace ℝ n | ∑ i : n, HPow.hPow (β := ℕ) (x.ofLp i) 2 = HPow.hPow (β := ℕ) r 2} x

Tactic:
simp_rw [mem_setOf, mem_sphere_zero_iff_norm, norm_eq, norm_eq_abs, sq_abs,
    Real.sqrt_eq_iff_eq_sq this hr]

Premises used: Real.sqrt_eq_iff_eq_sq, mem_sphere_zero_iff_norm, Set.mem_setOf, EuclideanSpace.norm_eq, sq_abs, Real.norm_eq_abs
-- 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 : Nonempty ι
⊢ Infinite (EuclideanSpace 𝕜 ι)

Tactic:
Module.Free.infinite 𝕜 _

Premises used: Module.Free.infinite
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype ι
⊢ finrank 𝕜 (WithLp 2 (ι → 𝕜)) = finrank 𝕜 (ι → 𝕜)

Tactic:
(WithLp.linearEquiv 2 𝕜 (ι → 𝕜)).finrank_eq

Premises used: LinearEquiv.finrank_eq, OfNat.ofNat, WithLp.linearEquiv
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype ι
h : Fintype.card ι = finrank 𝕜 (ι → 𝕜)
⊢ finrank 𝕜 (EuclideanSpace 𝕜 ι) = Fintype.card ι

Tactic:
convert! (WithLp.linearEquiv 2 𝕜 (ι → 𝕜)).finrank_eq

Premises used: LinearEquiv.finrank_eq, OfNat.ofNat, WithLp.linearEquiv
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype ι
⊢ Fintype.card ι = finrank 𝕜 (ι → 𝕜)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
n : ℕ
⊢ finrank 𝕜 (EuclideanSpace 𝕜 (Fin n)) = n

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 ι
n : ℕ
⊢ Fact (finrank 𝕜 (EuclideanSpace 𝕜 (Fin n)) = n)

Tactic:
⟨finrank_euclideanSpace_fin⟩

Premises used: Fact.mk, finrank_euclideanSpace_fin
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype ι
x y : EuclideanSpace 𝕜 ι
⊢ ⟪x, y⟫ = y.ofLp ⬝ᵥ star x.ofLp

Tactic:
rfl

Premises used: dotProduct, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype ι
x y : ι → 𝕜
⊢ inner 𝕜 (E := WithLp 2 (ι → 𝕜)) (toLp 2 x) (toLp 2 y) = y ⬝ᵥ star x

Tactic:
rfl

Premises used: dotProduct, rfl
-- 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 ι
I J : Finset ι'
hIJ : I ⊆ J
x y : EuclideanSpace.{u_3, u_2} 𝕜 ↥J
h :
  ∀ (i : ↥I),
    ofLp (p := 2) (toLp 2 (Finset.restrict₂ («π» := fun (x : ι') ↦ 𝕜) hIJ (x + y).ofLp)) i =
      (HAdd.hAdd (α := EuclideanSpace.{u_3, u_2} 𝕜 ↥I) (β := EuclideanSpace.{u_3, u_2} 𝕜 ↥I)
            (toLp 2 (Finset.restrict₂ («π» := fun (x : ι') ↦ 𝕜) hIJ x.ofLp) :
              WithLp 2 ((i : ↥I) → (fun (x : ↥I) ↦ 𝕜) i))
            (toLp 2 (Finset.restrict₂ («π» := fun (x : ι') ↦ 𝕜) hIJ y.ofLp) :
              WithLp 2 ((i : ↥I) → (fun (x : ↥I) ↦ 𝕜) i))).ofLp
        i
⊢ toLp 2 (Finset.restrict₂ («π» := fun (x : ι') ↦ 𝕜) hIJ (x + y).ofLp) =
    HAdd.hAdd (α := EuclideanSpace.{u_3, u_2} 𝕜 ↥I) (β := EuclideanSpace.{u_3, u_2} 𝕜 ↥I)
      (toLp 2 (Finset.restrict₂ («π» := fun (x : ι') ↦ 𝕜) hIJ x.ofLp) : WithLp 2 ((i : ↥I) → (fun (x : ↥I) ↦ 𝕜) i))
      (toLp 2 (Finset.restrict₂ («π» := fun (x : ι') ↦ 𝕜) hIJ y.ofLp) : WithLp 2 ((i : ↥I) → (fun (x : ↥I) ↦ 𝕜) i))

Tactic:
ext
-- 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 ι
I J : Finset ι'
hIJ : I ⊆ J
x y : EuclideanSpace.{u_3, u_2} 𝕜 ↥J
i : ↥I
⊢ ofLp (p := 2) (toLp 2 (Finset.restrict₂ («π» := fun (x : ι') ↦ 𝕜) hIJ (x + y).ofLp)) i =
    (HAdd.hAdd (α := EuclideanSpace.{u_3, u_2} 𝕜 ↥I) (β := EuclideanSpace.{u_3, u_2} 𝕜 ↥I)
          (toLp 2 (Finset.restrict₂ («π» := fun (x : ι') ↦ 𝕜) hIJ x.ofLp) : WithLp 2 ((i : ↥I) → (fun (x : ↥I) ↦ 𝕜) i))
          (toLp 2 (Finset.restrict₂ («π» := fun (x : ι') ↦ 𝕜) hIJ y.ofLp) :
            WithLp 2 ((i : ↥I) → (fun (x : ↥I) ↦ 𝕜) i))).ofLp
      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 ι
I J : Finset ι'
hIJ : I ⊆ J
m : 𝕜
x : EuclideanSpace.{u_3, u_2} 𝕜 ↥J
h :
  ∀ (i : ↥I),
    ofLp (p := 2) (toLp 2 (Finset.restrict₂ («π» := fun (x : ι') ↦ 𝕜) hIJ (m • x).ofLp)) i =
      (HSMul.hSMul (α := 𝕜) (β := EuclideanSpace.{u_3, u_2} 𝕜 ↥I) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) m : 𝕜)
            (toLp 2 (Finset.restrict₂ («π» := fun (x : ι') ↦ 𝕜) hIJ x.ofLp) :
              WithLp 2 ((i : ↥I) → (fun (x : ↥I) ↦ 𝕜) i))).ofLp
        i
⊢ toLp 2 (Finset.restrict₂ («π» := fun (x : ι') ↦ 𝕜) hIJ (m • x).ofLp) =
    HSMul.hSMul (α := 𝕜) (β := EuclideanSpace.{u_3, u_2} 𝕜 ↥I) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) m : 𝕜)
      (toLp 2 (Finset.restrict₂ («π» := fun (x : ι') ↦ 𝕜) hIJ x.ofLp) : WithLp 2 ((i : ↥I) → (fun (x : ↥I) ↦ 𝕜) i))

Tactic:
ext
-- 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 ι
I J : Finset ι'
hIJ : I ⊆ J
m : 𝕜
x : EuclideanSpace.{u_3, u_2} 𝕜 ↥J
i : ↥I
⊢ ofLp (p := 2) (toLp 2 (Finset.restrict₂ («π» := fun (x : ι') ↦ 𝕜) hIJ (m • x).ofLp)) i =
    (HSMul.hSMul (α := 𝕜) (β := EuclideanSpace.{u_3, u_2} 𝕜 ↥I) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) m : 𝕜)
          (toLp 2 (Finset.restrict₂ («π» := fun (x : ι') ↦ 𝕜) hIJ x.ofLp) :
            WithLp 2 ((i : ↥I) → (fun (x : ↥I) ↦ 𝕜) i))).ofLp
      i

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
I J : Finset ι'
hIJ : I ⊆ J
x : EuclideanSpace.{u_3, u_2} 𝕜 ↥J
i : ↥I
⊢ ofLp (p := 2) ((restrict₂ hIJ : (a : EuclideanSpace 𝕜 ↥J) → EuclideanSpace 𝕜 ↥I) x) i =
    x.ofLp (Subtype.mk (p := fun (x : ι') ↦ x ∈ J) (↑i : ι') ⋯)

Tactic:
rfl

Premises used: Finset.restrict₂, rfl
-- 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
refine :
  ∀ (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⟫
⊢ E ≃ₗᵢ[𝕜] PiLp.{u_1, u_4} 2 fun (i : ι) ↦ ↥(V i)

Tactic:
refine LinearEquiv.isometryOfInner ((e₂.symm.trans e₁).trans
    (WithLp.linearEquiv 2 𝕜 (Π i, V i)).symm) ?_

Premises used: LinearEquiv.symm, LinearEquiv.isometryOfInner, OfNat.ofNat, LinearEquiv.trans, WithLp.linearEquiv
-- 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
simp :
  inner 𝕜 (E := PiLp.{u_1, u_4} 2 fun (i : ι) ↦ ↥(V i))
      ((LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 ((i : ι) → ↥(V i))) :
            (a : (i : ι) → ↥(V i)) → PiLp 2 fun (i : ι) ↦ ↥(V i))
          ((e₁ : (a : ⨁ (i : ι), ↥(V i)) → (i : ι) → ↥(V i))
            ((e₂.symm : (a : E) → ⨁ (i : ι), ↥(V i)) v₀ : ⨁ (i : ι), ↥(V i))) :
        PiLp.{u_1, u_4} 2 fun (i : ι) ↦ ↥(V i))
      ((LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 ((i : ι) → ↥(V i))) :
            (a : (i : ι) → ↥(V i)) → PiLp 2 fun (i : ι) ↦ ↥(V i))
          ((e₁ : (a : ⨁ (i : ι), ↥(V i)) → (i : ι) → ↥(V i))
            ((e₂.symm : (a : E) → ⨁ (i : ι), ↥(V i)) w₀ : ⨁ (i : ι), ↥(V i))) :
        PiLp.{u_1, u_4} 2 fun (i : ι) ↦ ↥(V i)) =
    ⟪v₀, w₀⟫
⊢ 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))
          v₀ :
        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))
          w₀ :
        PiLp.{u_1, u_4} 2 fun (i : ι) ↦ ↥(V i)) =
    ⟪v₀, w₀⟫

Tactic:
simp only [LinearEquiv.trans_apply]

Premises used: LinearEquiv.trans_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 ι
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
⊢ inner 𝕜 (E := PiLp.{u_1, u_4} 2 fun (i : ι) ↦ ↥(V i))
      (toLp 2
          ((e₁ : (a : ⨁ (i : ι), ↥(V i)) → (i : ι) → ↥(V i))
            ((e₂.symm : (a : E) → ⨁ (i : ι), ↥(V i)) v₀ : ⨁ (i : ι), ↥(V i))) :
        WithLp 2 ((i : ι) → (fun (i : ι) ↦ ↥(V i)) i))
      (toLp 2
          ((e₁ : (a : ⨁ (i : ι), ↥(V i)) → (i : ι) → ↥(V i))
            ((e₂.symm : (a : E) → ⨁ (i : ι), ↥(V i)) w₀ : ⨁ (i : ι), ↥(V i))) :
        WithLp 2 ((i : ι) → (fun (i : ι) ↦ ↥(V i)) i)) =
    inner.{u_3, u_4} 𝕜 (E := E)
      ((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)) v₀ : ⨁ (i : ι), ↥(V i))))) :
            ⨁ (i : ι), ↥(V i)) :
        E)
      ((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)) :
        E)

Tactic:
this (toLp 2 (e₁ (e₂.symm v₀))) (toLp 2 (e₁ (e₂.symm w₀)))

Premises used: LinearEquiv.symm, WithLp.toLp, 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 ι
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
h :
  v₀ =
    (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)) v₀ : ⨁ (i : ι), ↥(V i))))) :
        ⨁ (i : ι), ↥(V i))
h₁ :
  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))
⊢ inner 𝕜 (E := PiLp.{u_1, u_4} 2 fun (i : ι) ↦ ↥(V i))
      ((LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 ((i : ι) → ↥(V i))) :
            (a : (i : ι) → ↥(V i)) → PiLp 2 fun (i : ι) ↦ ↥(V i))
          ((e₁ : (a : ⨁ (i : ι), ↥(V i)) → (i : ι) → ↥(V i))
            ((e₂.symm : (a : E) → ⨁ (i : ι), ↥(V i)) v₀ : ⨁ (i : ι), ↥(V i))) :
        PiLp.{u_1, u_4} 2 fun (i : ι) ↦ ↥(V i))
      ((LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 ((i : ι) → ↥(V i))) :
            (a : (i : ι) → ↥(V i)) → PiLp 2 fun (i : ι) ↦ ↥(V i))
          ((e₁ : (a : ⨁ (i : ι), ↥(V i)) → (i : ι) → ↥(V i))
            ((e₂.symm : (a : E) → ⨁ (i : ι), ↥(V i)) w₀ : ⨁ (i : ι), ↥(V i))) :
        PiLp.{u_1, u_4} 2 fun (i : ι) ↦ ↥(V i)) =
    ⟪v₀, w₀⟫

Tactic:
convert! this (toLp 2 (e₁ (e₂.symm v₀))) (toLp 2 (e₁ (e₂.symm w₀)))

Premises used: LinearEquiv.symm, WithLp.toLp, 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 ι
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
⊢ v₀ =
    (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)) v₀ : ⨁ (i : ι), ↥(V i))))) :
        ⨁ (i : ι), ↥(V i))

Tactic:
simp