awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ι
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 rw₁ 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 (ι → 𝕜))
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 (ι → 𝕜))
rw₄ :
  ∀ (i : ι) (k : 𝕜),
    Eq.{u_4 + 1} (α := E)
      (((↑b.repr.symm : EuclideanSpace 𝕜 ι →ₗ[𝕜] E) ∘ₗ
              (↑(LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (ι → 𝕜))) : (ι → 𝕜) →ₗ[𝕜] WithLp 2 (ι → 𝕜)) :
            (a : (i : ι) → 𝕜) → E)
          (Pi.single (M := fun (i : ι) ↦ 𝕜) i k) :
        E)
      (((↑b'.repr.symm : EuclideanSpace 𝕜 ι →ₗ[𝕜] E) ∘ₗ
              (↑(LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (ι → 𝕜))) : (ι → 𝕜) →ₗ[𝕜] WithLp 2 (ι → 𝕜)) :
            (a : (i : ι) → 𝕜) → E)
          (Pi.single (M := fun (i : ι) ↦ 𝕜) i k) :
        E)
⊢ (↑b.repr.symm : EuclideanSpace 𝕜 ι →ₗ[𝕜] E) = (↑b'.repr.symm : EuclideanSpace 𝕜 ι →ₗ[𝕜] E)
have rw₅ : ∀ (i : ι) (k : 𝕜) (this : k = HSMul.hSMul (β := 𝕜) k 1),
  Eq.{u_4 + 1} (α := E)
    (((↑b.repr.symm : EuclideanSpace 𝕜 ι →ₗ[𝕜] E) ∘ₗ
            (↑(LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (ι → 𝕜))) : (ι → 𝕜) →ₗ[𝕜] WithLp 2 (ι → 𝕜)) :
          (a : (i : ι) → 𝕜) → E)
        (Pi.single (M := fun (i : ι) ↦ 𝕜) i k) :
      E)
    (((↑b'.repr.symm : EuclideanSpace 𝕜 ι →ₗ[𝕜] E) ∘ₗ
            (↑(LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (ι → 𝕜))) : (ι → 𝕜) →ₗ[𝕜] WithLp 2 (ι → 𝕜)) :
          (a : (i : ι) → 𝕜) → E)
        (Pi.single (M := fun (i : ι) ↦ 𝕜) i k) :
      E)
Tactic: classical
        rw [← LinearMap.cancel_right (WithLp.linearEquiv 2 𝕜 (_ → 𝕜)).symm.surjective]
        simp +instances only
        refine LinearMap.pi_ext fun i k => ?_
        have : k = k • (1 : 𝕜) := by rw [smul_eq_mul, mul_one]
        rw [this, Pi.single_smul]
        replace h := congr_fun h i
        simp only [LinearEquiv.comp_coe, map_smul, LinearEquiv.coe_coe, LinearEquiv.trans_apply,
          coe_symm_linearEquiv, PiLp.toLp_single,
          LinearIsometryEquiv.coe_symm_toLinearEquiv] at h ⊢
        rw [h]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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 ι
e : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι
⊢ Eq (α := (a : ι) → E) (⇑{ repr := e : OrthonormalBasis ι 𝕜 E } : (a : ι) → E) fun (i : ι) ↦
    (e.symm : (a : EuclideanSpace 𝕜 ι) → E) (EuclideanSpace.single i 1)
have dsimp : Eq (α := (a : ι) → E) (fun (i : ι) ↦ EquivLike.coe e.symm (EuclideanSpace.single i 1)) fun (i : ι) ↦
  EquivLike.coe e.symm (EuclideanSpace.single i 1)
Tactic: dsimp only [DFunLike.coe]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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 ι
e : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι
⊢ Eq (α := (a : ι) → E) (fun (i : ι) ↦ EquivLike.coe e.symm (EuclideanSpace.single i 1)) fun (i : ι) ↦
    EquivLike.coe e.symm (EuclideanSpace.single i 1)
have h : ∀ (x : ι), EquivLike.coe e.symm (EuclideanSpace.single x 1) = EquivLike.coe e.symm (EuclideanSpace.single x 1)
Tactic: funext
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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 ι
b : OrthonormalBasis ι 𝕜 E
i : ι
⊢ Eq (α := EuclideanSpace 𝕜 ι) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) ((b : (a : ι) → E) i) : EuclideanSpace 𝕜 ι)
    (EuclideanSpace.single i 1 : EuclideanSpace 𝕜 ι)
have rw : Eq (α := EuclideanSpace 𝕜 ι)
  ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) ((b.repr.symm : (a : EuclideanSpace 𝕜 ι) → E) (EuclideanSpace.single i 1)) :
    EuclideanSpace 𝕜 ι)
  (EuclideanSpace.single i 1 : EuclideanSpace 𝕜 ι)
Tactic: rw [← b.repr_symm_single i, LinearIsometryEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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 ι
b : OrthonormalBasis ι 𝕜 E
i : ι
rw :
  Eq (α := EuclideanSpace 𝕜 ι)
    ((b.repr : (a : E) → EuclideanSpace 𝕜 ι)
        ((b.repr.symm : (a : EuclideanSpace 𝕜 ι) → E) (EuclideanSpace.single i 1)) :
      EuclideanSpace 𝕜 ι)
    (EuclideanSpace.single i 1 : EuclideanSpace 𝕜 ι)
⊢ Eq (α := EuclideanSpace 𝕜 ι) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) ((b : (a : ι) → E) i) : EuclideanSpace 𝕜 ι)
    (EuclideanSpace.single i 1 : EuclideanSpace 𝕜 ι)
have rw₁ : Eq (α := EuclideanSpace 𝕜 ι) (EuclideanSpace.single i 1) (EuclideanSpace.single i 1)
Tactic: rw [← b.repr_symm_single i, LinearIsometryEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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
v : E
i : ι
⊢ ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) v) i = ⟪(b : (a : ι) → E) i, v⟫
have rw : ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) v) i =
  HMul.hMul (α := 𝕜) (β := (fun (x : ι) ↦ 𝕜) i) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) 1 : 𝕜)
    (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) v) i : (fun (x : ι) ↦ 𝕜) i)
Tactic: rw [← b.repr.inner_map_map (b i) v, b.repr_self i, EuclideanSpace.inner_single_left]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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
v : E
i : ι
⊢ ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) v) i = ⟪(b : (a : ι) → E) i, v⟫
have rw : ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) v) i =
  inner 𝕜 (E := EuclideanSpace 𝕜 ι) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) ((b : (a : ι) → E) i) : EuclideanSpace 𝕜 ι)
    ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) v : EuclideanSpace 𝕜 ι)
Tactic: classical
    rw [← b.repr.inner_map_map (b i) v, b.repr_self i, EuclideanSpace.inner_single_left]
    simp only [one_mul, map_one]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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
v : E
i : ι
rw :
  ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) v) i =
    inner 𝕜 (E := EuclideanSpace 𝕜 ι)
      ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) ((b : (a : ι) → E) i) : EuclideanSpace 𝕜 ι)
      ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) v : EuclideanSpace 𝕜 ι)
⊢ ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) v) i = ⟪(b : (a : ι) → E) i, v⟫
have rw₁ : ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) v) i =
  inner 𝕜 (E := EuclideanSpace 𝕜 ι) (EuclideanSpace.single i 1) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) v)
Tactic: classical
    rw [← b.repr.inner_map_map (b i) v, b.repr_self i, EuclideanSpace.inner_single_left]
    simp only [one_mul, map_one]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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
v : E
i : ι
rw :
  ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) v) i =
    inner 𝕜 (E := EuclideanSpace 𝕜 ι)
      ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) ((b : (a : ι) → E) i) : EuclideanSpace 𝕜 ι)
      ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) v : EuclideanSpace 𝕜 ι)
rw₁ :
  ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) v) i =
    inner 𝕜 (E := EuclideanSpace 𝕜 ι) (EuclideanSpace.single i 1) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) v)
⊢ ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) v) i = ⟪(b : (a : ι) → E) i, v⟫
have rw₂ : ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) v) i =
  HMul.hMul (α := 𝕜) (β := (fun (x : ι) ↦ 𝕜) i) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) 1 : 𝕜)
    (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) v) i : (fun (x : ι) ↦ 𝕜) i)
Tactic: classical
    rw [← b.repr.inner_map_map (b i) v, b.repr_self i, EuclideanSpace.inner_single_left]
    simp only [one_mul, map_one]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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
⊢ Orthonormal.{u_3, u_4, u_1} 𝕜 (E := E) (ι := ι) (⇑b : (a : ι) → E)
have rw : ∀ (i j : ι), inner.{u_3, u_4} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((b : (a : ι) → E) j : E) = if i = j then 1 else 0
Tactic: rw [orthonormal_iff_ite]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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
i j : ι
⊢ inner.{u_3, u_4} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((b : (a : ι) → E) j : E) = if i = j then 1 else 0
have rw : inner 𝕜 (E := EuclideanSpace 𝕜 ι) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) ((b : (a : ι) → E) i) : EuclideanSpace 𝕜 ι)
    ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) ((b : (a : ι) → E) j) : EuclideanSpace 𝕜 ι) =
  if i = j then 1 else 0
Tactic: rw [← b.repr.inner_map_map (b i) (b j), b.repr_self i, b.repr_self j,
      EuclideanSpace.inner_single_left, PiLp.single_apply, map_one, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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
i j : ι
rw :
  inner 𝕜 (E := EuclideanSpace 𝕜 ι) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) ((b : (a : ι) → E) i) : EuclideanSpace 𝕜 ι)
      ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) ((b : (a : ι) → E) j) : EuclideanSpace 𝕜 ι) =
    if i = j then 1 else 0
⊢ inner.{u_3, u_4} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((b : (a : ι) → E) j : E) = if i = j then 1 else 0
have rw₁ : inner 𝕜 (E := EuclideanSpace 𝕜 ι) (EuclideanSpace.single i 1)
    ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) ((b : (a : ι) → E) j)) =
  if i = j then 1 else 0
Tactic: rw [← b.repr.inner_map_map (b i) (b j), b.repr_self i, b.repr_self j,
      EuclideanSpace.inner_single_left, PiLp.single_apply, map_one, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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
i j : ι
rw :
  inner 𝕜 (E := EuclideanSpace 𝕜 ι) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) ((b : (a : ι) → E) i) : EuclideanSpace 𝕜 ι)
      ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) ((b : (a : ι) → E) j) : EuclideanSpace 𝕜 ι) =
    if i = j then 1 else 0
rw₁ :
  inner 𝕜 (E := EuclideanSpace 𝕜 ι) (EuclideanSpace.single i 1)
      ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) ((b : (a : ι) → E) j)) =
    if i = j then 1 else 0
⊢ inner.{u_3, u_4} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((b : (a : ι) → E) j : E) = if i = j then 1 else 0
have rw₂ : inner 𝕜 (E := EuclideanSpace 𝕜 ι) (EuclideanSpace.single i 1) (EuclideanSpace.single j 1) = if i = j then 1 else 0
Tactic: rw [← b.repr.inner_map_map (b i) (b j), b.repr_self i, b.repr_self j,
      EuclideanSpace.inner_single_left, PiLp.single_apply, map_one, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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
i j : ι
rw :
  inner 𝕜 (E := EuclideanSpace 𝕜 ι) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) ((b : (a : ι) → E) i) : EuclideanSpace 𝕜 ι)
      ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) ((b : (a : ι) → E) j) : EuclideanSpace 𝕜 ι) =
    if i = j then 1 else 0
rw₁ :
  inner 𝕜 (E := EuclideanSpace 𝕜 ι) (EuclideanSpace.single i 1)
      ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) ((b : (a : ι) → E) j)) =
    if i = j then 1 else 0
rw₂ : inner 𝕜 (E := EuclideanSpace 𝕜 ι) (EuclideanSpace.single i 1) (EuclideanSpace.single j 1) = if i = j then 1 else 0
⊢ inner.{u_3, u_4} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((b : (a : ι) → E) j : E) = if i = j then 1 else 0
have rw₃ : HMul.hMul (α := 𝕜) (β := (fun (x : ι) ↦ 𝕜) i) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) 1 : 𝕜)
    (ofLp (EuclideanSpace.single j 1) i : (fun (x : ι) ↦ 𝕜) i) =
  if i = j then 1 else 0
Tactic: rw [← b.repr.inner_map_map (b i) (b j), b.repr_self i, b.repr_self j,
      EuclideanSpace.inner_single_left, PiLp.single_apply, map_one, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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
i j : ι
rw :
  inner 𝕜 (E := EuclideanSpace 𝕜 ι) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) ((b : (a : ι) → E) i) : EuclideanSpace 𝕜 ι)
      ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) ((b : (a : ι) → E) j) : EuclideanSpace 𝕜 ι) =
    if i = j then 1 else 0
rw₁ :
  inner 𝕜 (E := EuclideanSpace 𝕜 ι) (EuclideanSpace.single i 1)
      ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) ((b : (a : ι) → E) j)) =
    if i = j then 1 else 0
rw₂ : inner 𝕜 (E := EuclideanSpace 𝕜 ι) (EuclideanSpace.single i 1) (EuclideanSpace.single j 1) = if i = j then 1 else 0
rw₃ :
  HMul.hMul (α := 𝕜) (β := (fun (x : ι) ↦ 𝕜) i) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) 1 : 𝕜)
      (ofLp (EuclideanSpace.single j 1) i : (fun (x : ι) ↦ 𝕜) i) =
    if i = j then 1 else 0
⊢ inner.{u_3, u_4} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((b : (a : ι) → E) j : E) = if i = j then 1 else 0
have rw₄ : HMul.hMul (α := 𝕜) (β := (fun (x : ι) ↦ 𝕜) i) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) 1 : 𝕜) (if i = j then 1 else 0 : 𝕜) =
  if i = j then 1 else 0
Tactic: rw [← b.repr.inner_map_map (b i) (b j), b.repr_self i, b.repr_self j,
      EuclideanSpace.inner_single_left, PiLp.single_apply, map_one, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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
i j : ι
rw :
  inner 𝕜 (E := EuclideanSpace 𝕜 ι) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) ((b : (a : ι) → E) i) : EuclideanSpace 𝕜 ι)
      ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) ((b : (a : ι) → E) j) : EuclideanSpace 𝕜 ι) =
    if i = j then 1 else 0
rw₁ :
  inner 𝕜 (E := EuclideanSpace 𝕜 ι) (EuclideanSpace.single i 1)
      ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) ((b : (a : ι) → E) j)) =
    if i = j then 1 else 0
rw₂ : inner 𝕜 (E := EuclideanSpace 𝕜 ι) (EuclideanSpace.single i 1) (EuclideanSpace.single j 1) = if i = j then 1 else 0
rw₃ :
  HMul.hMul (α := 𝕜) (β := (fun (x : ι) ↦ 𝕜) i) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) 1 : 𝕜)
      (ofLp (EuclideanSpace.single j 1) i : (fun (x : ι) ↦ 𝕜) i) =
    if i = j then 1 else 0
rw₄ :
  HMul.hMul (α := 𝕜) (β := (fun (x : ι) ↦ 𝕜) i) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) 1 : 𝕜) (if i = j then 1 else 0 : 𝕜) =
    if i = j then 1 else 0
⊢ inner.{u_3, u_4} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((b : (a : ι) → E) j : E) = if i = j then 1 else 0
have rw₅ : HMul.hMul (α := 𝕜) 1 (if i = j then 1 else 0) = if i = j then 1 else 0
Tactic: rw [← b.repr.inner_map_map (b i) (b j), b.repr_self i, b.repr_self j,
      EuclideanSpace.inner_single_left, PiLp.single_apply, map_one, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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
i j : ι
rw :
  inner 𝕜 (E := EuclideanSpace 𝕜 ι) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) ((b : (a : ι) → E) i) : EuclideanSpace 𝕜 ι)
      ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) ((b : (a : ι) → E) j) : EuclideanSpace 𝕜 ι) =
    if i = j then 1 else 0
rw₁ :
  inner 𝕜 (E := EuclideanSpace 𝕜 ι) (EuclideanSpace.single i 1)
      ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) ((b : (a : ι) → E) j)) =
    if i = j then 1 else 0
rw₂ : inner 𝕜 (E := EuclideanSpace 𝕜 ι) (EuclideanSpace.single i 1) (EuclideanSpace.single j 1) = if i = j then 1 else 0
rw₃ :
  HMul.hMul (α := 𝕜) (β := (fun (x : ι) ↦ 𝕜) i) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) 1 : 𝕜)
      (ofLp (EuclideanSpace.single j 1) i : (fun (x : ι) ↦ 𝕜) i) =
    if i = j then 1 else 0
rw₄ :
  HMul.hMul (α := 𝕜) (β := (fun (x : ι) ↦ 𝕜) i) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) 1 : 𝕜) (if i = j then 1 else 0 : 𝕜) =
    if i = j then 1 else 0
rw₅ : HMul.hMul (α := 𝕜) 1 (if i = j then 1 else 0) = if i = j then 1 else 0
⊢ inner.{u_3, u_4} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((b : (a : ι) → E) j : E) = if i = j then 1 else 0
have rw₆ : Eq.{u_3 + 1} (α := 𝕜) (if i = j then 1 else 0) (if i = j then 1 else 0)
Tactic: rw [← b.repr.inner_map_map (b i) (b j), b.repr_self i, b.repr_self j,
      EuclideanSpace.inner_single_left, PiLp.single_apply, map_one, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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
⊢ Orthonormal.{u_3, u_4, u_1} 𝕜 (E := E) (ι := ι) (⇑b : (a : ι) → E)
have rw : ∀ (i j : ι), inner.{u_3, u_4} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((b : (a : ι) → E) j : E) = if i = j then 1 else 0
Tactic: classical
    rw [orthonormal_iff_ite]
    intro i j
    rw [← b.repr.inner_map_map (b i) (b j), b.repr_self i, b.repr_self j,
      EuclideanSpace.inner_single_left, PiLp.single_apply, map_one, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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 ι
b : OrthonormalBasis ι 𝕜 E
i j : ι
⊢ inner.{u_3, u_4} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((b : (a : ι) → E) j : E) = if i = j then 1 else 0
have pos : ∀ (h : i = j), inner.{u_3, u_4} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((b : (a : ι) → E) j : E) = if i = j then 1 else 0
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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 ι
b : OrthonormalBasis ι 𝕜 E
i j : ι
pos :
  ∀ (h : i = j),
    inner.{u_3, u_4} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((b : (a : ι) → E) j : E) = if i = j then 1 else 0
⊢ inner.{u_3, u_4} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((b : (a : ι) → E) j : E) = if i = j then 1 else 0
have neg : ∀ (h : ¬i = j), inner.{u_3, u_4} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((b : (a : ι) → E) j : E) = if i = j then 1 else 0
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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
⊢ ∑ i : ι,
      HSMul.hSMul.{u_3, u_4, u_4} (α := (fun (x : ι) ↦ 𝕜) i) (β := E)
        (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) x) i) ((b : (a : ι) → E) i : E) =
    x
have simp_rw : ∑ x_1 : ι,
    HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (β := E)
      ((((b.toBasis.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜) : (a : ι) → 𝕜) x_1 : 𝕜) ((b.toBasis : (a : ι) → E) x_1 : E) =
  x
Tactic: simp_rw [← b.coe_toBasis_repr_apply, ← b.coe_toBasis]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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
⊢ ∑ i : ι, HSMul.hSMul (β := E) ⟪(b : (a : ι) → E) i, x⟫_𝕜 ((b : (a : ι) → E) i : E) = x
have nth_rw : Eq.{u_4 + 1} (α := E) (∑ i : ι, HSMul.hSMul (β := E) ⟪(b : (a : ι) → E) i, x⟫_𝕜 ((b : (a : ι) → E) i : E))
  (∑ i : ι,
    HSMul.hSMul.{u_3, u_4, u_4} (α := (fun (x : ι) ↦ 𝕜) i) (β := E)
      (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) x) i) ((b : (a : ι) → E) i : E))
Tactic: nth_rw 2 [← (b.sum_repr x)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (hypothesis)
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 y : E
⊢ ∑ i : ι, ⟪x, (b : (a : ι) → E) i⟫ * ⟪(b : (a : ι) → E) i, y⟫ = ⟪x, y⟫
have this : Eq.{u_3 + 1} (α := 𝕜)
  ((((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) : (a : E) → 𝕜)
      (∑ i : ι,
        HSMul.hSMul.{u_3, u_4, u_4} (α := (fun (x : ι) ↦ 𝕜) i) (β := E)
          (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) y) i) ((b : (a : ι) → E) i : E)) :
    𝕜)
  ((((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) : (a : E) → 𝕜) y : 𝕜)
Tactic: have := congr_arg (innerSL 𝕜 x) (b.sum_repr y)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (hypothesis)
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 y : E
this :
  Eq.{u_3 + 1} (α := 𝕜)
    ((((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) : (a : E) → 𝕜)
        (∑ i : ι,
          HSMul.hSMul.{u_3, u_4, u_4} (α := (fun (x : ι) ↦ 𝕜) i) (β := E)
            (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) y) i) ((b : (a : ι) → E) i : E)) :
      𝕜)
    ((((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) : (a : E) → 𝕜) y : 𝕜)
⊢ ∑ i : ι, ⟪x, (b : (a : ι) → E) i⟫ * ⟪(b : (a : ι) → E) i, y⟫ = ⟪x, y⟫
have this₁ : Eq.{u_3 + 1} (α := 𝕜)
  (∑ x_1 : ι,
      (((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) : (a : E) → 𝕜)
        (HSMul.hSMul.{u_3, u_4, u_4} (α := (fun (x : ι) ↦ 𝕜) x_1) (β := E)
          (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) y) x_1) ((b : (a : ι) → E) x_1 : E)) :
    𝕜)
  ((((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) : (a : E) → 𝕜) y : 𝕜)
Tactic: rw [map_sum] at this
Cleared hypotheses: this