awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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
⊢ 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
have h₃ : ‖x‖ = r ↔ ∑ x_1 : n, HPow.hPow (β := ℕ) (x.ofLp x_1) 2 = HPow.hPow (β := ℕ) r 2
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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype ι
⊢ finrank 𝕜 (EuclideanSpace 𝕜 ι) = Fintype.card ι
have h : Fintype.card ι = finrank 𝕜 (ι → 𝕜)
Tactic: convert! (WithLp.linearEquiv 2 𝕜 (ι → 𝕜)).finrank_eq
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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
⊢ 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))
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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
⊢ 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))
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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
⊢ E ≃ₗᵢ[𝕜] PiLp.{u_1, u_4} 2 fun (i : ι) ↦ ↥(V i)
have 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⟫
Tactic: refine LinearEquiv.isometryOfInner ((e₂.symm.trans e₁).trans
    (WithLp.linearEquiv 2 𝕜 (Π i, V i)).symm) ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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))
      ((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₀⟫
have 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₀⟫
Tactic: simp only [LinearEquiv.trans_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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))
      ((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₀⟫
have 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))
Tactic: convert! this (toLp 2 (e₁ (e₂.symm v₀))) (toLp 2 (e₁ (e₂.symm w₀)))
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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))
⊢ 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₀⟫
have 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))
Tactic: convert! this (toLp 2 (e₁ (e₂.symm v₀))) (toLp 2 (e₁ (e₂.symm w₀)))
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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
⊢ ∀ (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⟫
have 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)
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
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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)
      ((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)
have 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))
Tactic: trans ⟪∑ i, (V i).subtypeₗᵢ (v i), ∑ i, (V i).subtypeₗᵢ (w i)⟫
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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))
⊢ ⟪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)
have 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)
Tactic: trans ⟪∑ i, (V i).subtypeₗᵢ (v i), ∑ i, (V i).subtypeₗᵢ (w i)⟫
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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)
⊢ 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)
have 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) sorry) :
      Multiset ι))
Tactic: congr