awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
η : Type u_7
inst : Fintype η
inst_1 : DecidableEq η
ι : η → Type u_8
inst_2 : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst_3 : RCLike 𝕜
E : η → Type u_10
inst_4 : (i : η) → NormedAddCommGroup (E i)
inst_5 : (i : η) → InnerProductSpace.{u_9, u_10} 𝕜 (E i)
B : (i : η) → OrthonormalBasis.{u_8, u_9, u_10} (ι i) 𝕜 (E i)
j : (i : η) × ι i
h :
  ∀ (k : η),
    Eq.{u_10 + 1} (α := E k)
      (ofLp (p := 2) ((Pi.orthonormalBasis (ι := ι) (E := E) B : (a : (i : η) × ι i) → PiLp 2 E) j) k : E k)
      (ofLp (p := 2)
          (PiLp.single 2 (β := E) (j.fst (β := fun (i : η) ↦ ι i))
            ((B (j.fst (β := fun (i : η) ↦ ι i)) : (a : ι j.fst) → E j.fst) (j.snd (β := fun (i : η) ↦ ι i))))
          k :
        E k)
h₁ :
  ∀ (k i : η) (j : ι i),
    Eq.{u_10 + 1} (α := E k)
      (ofLp (p := 2)
          ((Pi.orthonormalBasis (ι := ι) (E := E) B : (a : (i : η) × ι i) → PiLp 2 E)
            (Sigma.mk (β := fun (i : η) ↦ ι i) i j))
          k :
        E k)
      (ofLp (p := 2)
          (PiLp.single 2 (β := E) ((Sigma.mk (β := fun (i : η) ↦ ι i) i j).fst (β := fun (i : η) ↦ ι i))
            ((B ((Sigma.mk (β := fun (i : η) ↦ ι i) i j).fst (β := fun (i : η) ↦ ι i)) :
                (a : ι ⟨i, j⟩.fst) → E ⟨i, j⟩.fst)
              ((Sigma.mk (β := fun (i : η) ↦ ι i) i j).snd (β := fun (i : η) ↦ ι i))))
          k :
        E k)
h₂ :
  ∀ (k i : η) (j : ι i),
    Eq.{u_10 + 1} (α := E k)
      (((B k).repr.symm : (a : EuclideanSpace 𝕜 (ι k)) → E k)
          (toLp 2 (Pi.single (M := fun (j : η) ↦ (y : ι j) → 𝕜) i (Pi.single (M := fun (x : ι i) ↦ 𝕜) j 1) k)) :
        E k)
      (Pi.single (M := E) i ((B i : (a : ι i) → E i) j) k : E k)
h₃ :
  ∀ (i : η) (j : ι i),
    Eq.{u_10 + 1} (α := E i)
      (((B i).repr.symm : (a : EuclideanSpace 𝕜 (ι i)) → E i)
          (toLp 2 (Pi.single (M := fun (j : η) ↦ (y : ι j) → 𝕜) i (Pi.single (M := fun (x : ι i) ↦ 𝕜) j 1) i)) :
        E i)
      (Pi.single (M := E) i ((B i : (a : ι i) → E i) j) i : E i)
⊢ Eq (α := PiLp 2 E) ((Pi.orthonormalBasis (ι := ι) (E := E) B : (a : (i : η) × ι i) → PiLp 2 E) j : PiLp 2 E)
    (PiLp.single 2 (β := E) (j.fst (β := fun (i : η) ↦ ι i))
        ((B (j.fst (β := fun (i : η) ↦ ι i)) : (a : ι j.fst) → E j.fst) (j.snd (β := fun (i : η) ↦ ι i))) :
      PiLp 2 E)
have h₄ : ∀ (k i : η) (j : ι i) (hi : i ≠ k),
  Eq.{u_10 + 1} (α := E k)
    (((B k).repr.symm : (a : EuclideanSpace 𝕜 (ι k)) → E k)
        (toLp 2 (Pi.single (M := fun (j : η) ↦ (y : ι j) → 𝕜) i (Pi.single (M := fun (x : ι i) ↦ 𝕜) j 1) k)) :
      E k)
    (Pi.single (M := E) i ((B i : (a : ι i) → E i) j) k : E k)
Tactic: classical
  ext k
  obtain ⟨i, j⟩ := j
  simp only [Pi.orthonormalBasis, coe_ofRepr, LinearIsometryEquiv.symm_trans,
    LinearIsometryEquiv.symm_symm, LinearIsometryEquiv.piLpCongrRight_symm,
    LinearIsometryEquiv.trans_apply, LinearIsometryEquiv.piLpCongrRight_apply,
    LinearIsometryEquiv.piLpCurry_apply, PiLp.ofLp_single, PiLp.toLp_apply,
    Sigma.curry_single (γ := fun _ _ => 𝕜)]
  obtain rfl | hi := Decidable.eq_or_ne i k
  · simp
  · simp [hi]
Cleared hypotheses: 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 ι
v : ι → E
hon : Orthonormal 𝕜 v
hsp : LE.le (α := Submodule 𝕜 E) ⊤ (span 𝕜 (range v))
⊢ (⇑(OrthonormalBasis.mk hon hsp) : (a : ι) → E) = v
have rw : (⇑((Basis.mk sorry hsp).toOrthonormalBasis sorry) : (a : ι) → E) = v
Tactic: rw [OrthonormalBasis.mk, _root_.Module.Basis.coe_toOrthonormalBasis, Basis.coe_mk]
-- 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 ι
v : ι → E
hon : Orthonormal 𝕜 v
hsp : LE.le (α := Submodule 𝕜 E) ⊤ (span 𝕜 (range v))
rw : (⇑((Basis.mk ⋯ hsp).toOrthonormalBasis ⋯) : (a : ι) → E) = v
⊢ (⇑(OrthonormalBasis.mk hon hsp) : (a : ι) → E) = v
have rw₁ : (⇑(Basis.mk sorry hsp) : (a : ι) → E) = v
Tactic: rw [OrthonormalBasis.mk, _root_.Module.Basis.coe_toOrthonormalBasis, Basis.coe_mk]
-- 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 ι
v : ι → E
hon : Orthonormal 𝕜 v
hsp : LE.le (α := Submodule 𝕜 E) ⊤ (span 𝕜 (range v))
rw : (⇑((Basis.mk ⋯ hsp).toOrthonormalBasis ⋯) : (a : ι) → E) = v
rw₁ : (⇑(Basis.mk ⋯ hsp) : (a : ι) → E) = v
⊢ (⇑(OrthonormalBasis.mk hon hsp) : (a : ι) → E) = v
have rw₂ : v = v
Tactic: rw [OrthonormalBasis.mk, _root_.Module.Basis.coe_toOrthonormalBasis, Basis.coe_mk]
-- 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 ι
v : ι → E
hon : Orthonormal 𝕜 v
hsp : LE.le (α := Submodule 𝕜 E) ⊤ (span 𝕜 (range v))
⊢ (⇑(OrthonormalBasis.mk hon hsp) : (a : ι) → E) = v
have classical : (⇑((Basis.mk sorry hsp).toOrthonormalBasis sorry) : (a : ι) → E) = v
Tactic: classical rw [OrthonormalBasis.mk, _root_.Module.Basis.coe_toOrthonormalBasis, Basis.coe_mk]
-- 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 ι
v : ι → E
hon : Orthonormal 𝕜 v
hsp : LE.le (α := Submodule 𝕜 E) ⊤ (span 𝕜 (range v))
classical : (⇑((Basis.mk ⋯ hsp).toOrthonormalBasis ⋯) : (a : ι) → E) = v
⊢ (⇑(OrthonormalBasis.mk hon hsp) : (a : ι) → E) = v
have classical₁ : (⇑(Basis.mk sorry hsp) : (a : ι) → E) = v
Tactic: classical rw [OrthonormalBasis.mk, _root_.Module.Basis.coe_toOrthonormalBasis, Basis.coe_mk]
-- 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 ι
v : ι → E
hon : Orthonormal 𝕜 v
hsp : LE.le (α := Submodule 𝕜 E) ⊤ (span 𝕜 (range v))
classical : (⇑((Basis.mk ⋯ hsp).toOrthonormalBasis ⋯) : (a : ι) → E) = v
classical₁ : (⇑(Basis.mk ⋯ hsp) : (a : ι) → E) = v
⊢ (⇑(OrthonormalBasis.mk hon hsp) : (a : ι) → E) = v
have classical₂ : v = v
Tactic: classical rw [OrthonormalBasis.mk, _root_.Module.Basis.coe_toOrthonormalBasis, Basis.coe_mk]
-- 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 ι
v : ι → E
inst_8 : DecidableEq E
v' : ι' → E
h : Orthonormal 𝕜 v'
s : Finset ι'
e₀' : Basis.{u_2, u_3, u_4} (↥s) 𝕜 ↥(span 𝕜 (range (ι := ↥s) (v' ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)))) :=
  Basis.span ⋯
⊢ Orthonormal.{u_3, u_4, u_2} 𝕜 (E := ↥(span 𝕜 (range (ι := ↥s) (v' ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s))))) (ι :=
    ↥s) (⇑e₀' : (a : ↥s) → ↥(span 𝕜 (range (v' ∘ Subtype.val))))
have h₁ : ∀ (x : ↥s),
  (↑((e₀' : (a : ↥s) → ↥(span 𝕜 (range (v' ∘ Subtype.val)))) x) : E) = (v' ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)) x
Tactic: convert! orthonormal_span (h.comp ((↑) : s → ι') Subtype.val_injective)
-- 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 ι
v : ι → E
inst_8 : DecidableEq E
v' : ι' → E
h : Orthonormal 𝕜 v'
s : Finset ι'
e₀' : Basis.{u_2, u_3, u_4} (↥s) 𝕜 ↥(span 𝕜 (range (ι := ↥s) (v' ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)))) :=
  Basis.span ⋯
e₀ : OrthonormalBasis.{u_2, u_3, u_4} (↥s) 𝕜
  ↥(span 𝕜 (range (ι := ↥s) (v' ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)))) :=
  OrthonormalBasis.mk ⋯ ⋯
⊢ Eq (α := Submodule 𝕜 E) (span 𝕜 (↑(Finset.image v' s) : Set E))
    (span 𝕜 (range (ι := ↥s) (v' ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s))))
have rw : Eq (α := Submodule 𝕜 E) (span 𝕜 (range fun (x : (↑(↑s : Set ι') : Type u_2)) ↦ v' (↑x : ι')))
  (span 𝕜 (range (ι := ↥s) (v' ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s))))
Tactic: rw [Finset.coe_image, image_eq_range]
-- 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 ι
v : ι → E
hon : Orthonormal 𝕜 v
hsp : Eq (α := Submodule 𝕜 E) (span 𝕜 (range v))ᗮ ⊥
⊢ LE.le (α := Submodule 𝕜 E) ⊤ (span 𝕜 (range v))
have refine : Eq (α := Submodule 𝕜 E) (span 𝕜 (range v)) ⊤
Tactic: refine Eq.ge ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (hypothesis)
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : Fintype ι
v : ι → E
hon : Orthonormal 𝕜 v
hsp : Eq (α := Submodule 𝕜 E) (span 𝕜 (range v))ᗮ ⊥
⊢ Eq (α := Submodule 𝕜 E) (span 𝕜 (range v)) ⊤
have this : FiniteDimensional.{u_3, u_4} 𝕜 ↥(span 𝕜 (range v))
Tactic: haveI : FiniteDimensional 𝕜 (span 𝕜 (range v)) :=
        FiniteDimensional.span_of_finite 𝕜 (finite_range v)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (hypothesis)
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : Fintype ι
v : ι → E
hon : Orthonormal 𝕜 v
hsp : Eq (α := Submodule 𝕜 E) (span 𝕜 (range v))ᗮ ⊥
this : FiniteDimensional.{u_3, u_4} 𝕜 ↥(span 𝕜 (range v))
⊢ Eq (α := Submodule 𝕜 E) (span 𝕜 (range v)) ⊤
have this₁ : CompleteSpace.{u_4} ↥(span 𝕜 (range v))
Tactic: haveI : CompleteSpace (span 𝕜 (range v)) := FiniteDimensional.complete 𝕜 _
-- 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 ι
v : ι → E
hon : Orthonormal 𝕜 v
hsp : Eq (α := Submodule 𝕜 E) (span 𝕜 (range v))ᗮ ⊥
this_1 : FiniteDimensional.{u_3, u_4} 𝕜 ↥(span 𝕜 (range v))
this : CompleteSpace.{u_4} ↥(span 𝕜 (range v))
⊢ Eq (α := Submodule 𝕜 E) (span 𝕜 (range v)) ⊤
have rwa : ∀ (hsp : Eq (α := Submodule 𝕜 E) (span 𝕜 (range v)) ⊤) (this : FiniteDimensional.{u_3, u_4} 𝕜 ↥(span 𝕜 (range v)))
  (this : CompleteSpace.{u_4} ↥(span 𝕜 (range v))), Eq (α := Submodule 𝕜 E) (span 𝕜 (range v)) ⊤
Tactic: rwa [orthogonal_eq_bot_iff] at hsp
Cleared hypotheses: hsp, this_1, this
-- 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
inst_3 : Fintype ι
inst_4 : Fintype ι'
b : OrthonormalBasis ι 𝕜 E
e : ι ≃ ι'
i' : ι'
⊢ Eq.{u_4 + 1} (α := E) ((b.reindex e : (a : ι') → E) i' : E) ((b : (a : ι) → E) ((e.symm : (a : ι') → ι) i' : ι) : E)
have dsimp : Eq.{u_4 + 1} (α := E) (({ repr := b.repr.trans (LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e) } : (a : ι') → E) i' : E)
  ((b : (a : ι) → E) ((e.symm : (a : ι') → ι) i' : ι) : E)
Tactic: dsimp [reindex]
-- 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
inst_3 : Fintype ι
inst_4 : Fintype ι'
b : OrthonormalBasis ι 𝕜 E
e : ι ≃ ι'
i' : ι'
⊢ Eq.{u_4 + 1} (α := E) (({ repr := b.repr.trans (LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e) } : (a : ι') → E) i' : E)
    ((b : (a : ι) → E) ((e.symm : (a : ι') → ι) i' : ι) : E)
have rw : Eq.{u_4 + 1} (α := E)
  ((fun (i : ι') ↦
        ((LinearIsometryEquiv.symm (b.repr.trans (LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e)) :
              (a : EuclideanSpace 𝕜 ι') → E)
            (EuclideanSpace.single i 1) :
          E))
      i' :
    E)
  ((b : (a : ι) → E) ((e.symm : (a : ι') → ι) i' : ι) : E)
Tactic: rw [coe_ofRepr]
-- 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
inst_3 : Fintype ι
inst_4 : Fintype ι'
b : OrthonormalBasis ι 𝕜 E
e : ι ≃ ι'
i' : ι'
⊢ Eq.{u_4 + 1} (α := E)
    ((fun (i : ι') ↦
          ((LinearIsometryEquiv.symm (b.repr.trans (LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e)) :
                (a : EuclideanSpace 𝕜 ι') → E)
              (EuclideanSpace.single i 1) :
            E))
        i' :
      E)
    ((b : (a : ι) → E) ((e.symm : (a : ι') → ι) i' : ι) : E)
have dsimp : Eq.{u_4 + 1} (α := E)
  ((b.repr.symm : (a : EuclideanSpace 𝕜 ι) → E)
      ((LinearIsometryEquiv.symm (LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e) :
            (a : EuclideanSpace 𝕜 ι') → EuclideanSpace 𝕜 ι)
          (EuclideanSpace.single i' 1) :
        EuclideanSpace 𝕜 ι) :
    E)
  ((b : (a : ι) → E) ((e.symm : (a : ι') → ι) i' : ι) : E)
Tactic: dsimp
-- 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
inst_3 : Fintype ι
inst_4 : Fintype ι'
b : OrthonormalBasis ι 𝕜 E
e : ι ≃ ι'
i' : ι'
⊢ Eq.{u_4 + 1} (α := E)
    ((b.repr.symm : (a : EuclideanSpace 𝕜 ι) → E)
        ((LinearIsometryEquiv.symm (LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e) :
              (a : EuclideanSpace 𝕜 ι') → EuclideanSpace 𝕜 ι)
            (EuclideanSpace.single i' 1) :
          EuclideanSpace 𝕜 ι) :
      E)
    ((b : (a : ι) → E) ((e.symm : (a : ι') → ι) i' : ι) : E)
have rw : Eq.{u_4 + 1} (α := E)
  ((b.repr.symm : (a : EuclideanSpace 𝕜 ι) → E)
      ((LinearIsometryEquiv.symm (LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e) :
            (a : EuclideanSpace 𝕜 ι') → EuclideanSpace 𝕜 ι)
          (EuclideanSpace.single i' 1) :
        EuclideanSpace 𝕜 ι) :
    E)
  ((b.repr.symm : (a : EuclideanSpace 𝕜 ι) → E)
      (EuclideanSpace.single ((e.symm : (a : ι') → ι) i') 1 : EuclideanSpace 𝕜 ι) :
    E)
Tactic: rw [← b.repr_symm_single, LinearIsometryEquiv.piLpCongrLeft_symm,
      EuclideanSpace.piLpCongrLeft_single]
-- 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
inst_3 : Fintype ι
inst_4 : Fintype ι'
b : OrthonormalBasis ι 𝕜 E
e : ι ≃ ι'
i' : ι'
rw :
  Eq.{u_4 + 1} (α := E)
    ((b.repr.symm : (a : EuclideanSpace 𝕜 ι) → E)
        ((LinearIsometryEquiv.symm (LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e) :
              (a : EuclideanSpace 𝕜 ι') → EuclideanSpace 𝕜 ι)
            (EuclideanSpace.single i' 1) :
          EuclideanSpace 𝕜 ι) :
      E)
    ((b.repr.symm : (a : EuclideanSpace 𝕜 ι) → E)
        (EuclideanSpace.single ((e.symm : (a : ι') → ι) i') 1 : EuclideanSpace 𝕜 ι) :
      E)
⊢ Eq.{u_4 + 1} (α := E)
    ((b.repr.symm : (a : EuclideanSpace 𝕜 ι) → E)
        ((LinearIsometryEquiv.symm (LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e) :
              (a : EuclideanSpace 𝕜 ι') → EuclideanSpace 𝕜 ι)
            (EuclideanSpace.single i' 1) :
          EuclideanSpace 𝕜 ι) :
      E)
    ((b : (a : ι) → E) ((e.symm : (a : ι') → ι) i' : ι) : E)
have rw₁ : Eq.{u_4 + 1} (α := E)
  ((b.repr.symm : (a : EuclideanSpace 𝕜 ι) → E)
      ((LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e.symm : (a : EuclideanSpace 𝕜 ι') → EuclideanSpace 𝕜 ι)
          (EuclideanSpace.single i' 1) :
        EuclideanSpace 𝕜 ι) :
    E)
  ((b.repr.symm : (a : EuclideanSpace 𝕜 ι) → E)
      (EuclideanSpace.single ((e.symm : (a : ι') → ι) i') 1 : EuclideanSpace 𝕜 ι) :
    E)
Tactic: rw [← b.repr_symm_single, LinearIsometryEquiv.piLpCongrLeft_symm,
      EuclideanSpace.piLpCongrLeft_single]
-- 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
inst_3 : Fintype ι
inst_4 : Fintype ι'
b : OrthonormalBasis ι 𝕜 E
e : ι ≃ ι'
i' : ι'
rw :
  Eq.{u_4 + 1} (α := E)
    ((b.repr.symm : (a : EuclideanSpace 𝕜 ι) → E)
        ((LinearIsometryEquiv.symm (LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e) :
              (a : EuclideanSpace 𝕜 ι') → EuclideanSpace 𝕜 ι)
            (EuclideanSpace.single i' 1) :
          EuclideanSpace 𝕜 ι) :
      E)
    ((b.repr.symm : (a : EuclideanSpace 𝕜 ι) → E)
        (EuclideanSpace.single ((e.symm : (a : ι') → ι) i') 1 : EuclideanSpace 𝕜 ι) :
      E)
rw₁ :
  Eq.{u_4 + 1} (α := E)
    ((b.repr.symm : (a : EuclideanSpace 𝕜 ι) → E)
        ((LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e.symm : (a : EuclideanSpace 𝕜 ι') → EuclideanSpace 𝕜 ι)
            (EuclideanSpace.single i' 1) :
          EuclideanSpace 𝕜 ι) :
      E)
    ((b.repr.symm : (a : EuclideanSpace 𝕜 ι) → E)
        (EuclideanSpace.single ((e.symm : (a : ι') → ι) i') 1 : EuclideanSpace 𝕜 ι) :
      E)
⊢ Eq.{u_4 + 1} (α := E)
    ((b.repr.symm : (a : EuclideanSpace 𝕜 ι) → E)
        ((LinearIsometryEquiv.symm (LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e) :
              (a : EuclideanSpace 𝕜 ι') → EuclideanSpace 𝕜 ι)
            (EuclideanSpace.single i' 1) :
          EuclideanSpace 𝕜 ι) :
      E)
    ((b : (a : ι) → E) ((e.symm : (a : ι') → ι) i' : ι) : E)
have rw₂ : Eq.{u_4 + 1} (α := E)
  ((b.repr.symm : (a : EuclideanSpace 𝕜 ι) → E)
      (EuclideanSpace.single ((e.symm : (a : ι') → ι) i') 1 : EuclideanSpace 𝕜 ι) :
    E)
  ((b.repr.symm : (a : EuclideanSpace 𝕜 ι) → E)
      (EuclideanSpace.single ((e.symm : (a : ι') → ι) i') 1 : EuclideanSpace 𝕜 ι) :
    E)
Tactic: rw [← b.repr_symm_single, LinearIsometryEquiv.piLpCongrLeft_symm,
      EuclideanSpace.piLpCongrLeft_single]
-- 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
inst_3 : Fintype ι
inst_4 : Fintype ι'
b : OrthonormalBasis ι 𝕜 E
e : ι ≃ ι'
i' : ι'
⊢ Eq.{u_4 + 1} (α := E) ((b.reindex e : (a : ι') → E) i' : E) ((b : (a : ι) → E) ((e.symm : (a : ι') → ι) i' : ι) : E)
have dsimp : Eq.{u_4 + 1} (α := E) (({ repr := b.repr.trans (LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e) } : (a : ι') → E) i' : E)
  ((b : (a : ι) → E) ((e.symm : (a : ι') → ι) i' : ι) : E)
Tactic: classical
    dsimp [reindex]
    rw [coe_ofRepr]
    dsimp
    rw [← b.repr_symm_single, LinearIsometryEquiv.piLpCongrLeft_symm,
      EuclideanSpace.piLpCongrLeft_single]
-- 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
inst_3 : Fintype ι
inst_4 : Fintype ι'
b : OrthonormalBasis ι 𝕜 E
e : ι ≃ ι'
i' : ι'
dsimp :
  Eq.{u_4 + 1} (α := E) (({ repr := b.repr.trans (LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e) } : (a : ι') → E) i' : E)
    ((b : (a : ι) → E) ((e.symm : (a : ι') → ι) i' : ι) : E)
⊢ Eq.{u_4 + 1} (α := E) ((b.reindex e : (a : ι') → E) i' : E) ((b : (a : ι) → E) ((e.symm : (a : ι') → ι) i' : ι) : E)
have dsimp₁ : Eq.{u_4 + 1} (α := E)
  ((fun (i : ι') ↦
        ((LinearIsometryEquiv.symm (b.repr.trans (LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e)) :
              (a : EuclideanSpace 𝕜 ι') → E)
            (EuclideanSpace.single i 1) :
          E))
      i' :
    E)
  ((b : (a : ι) → E) ((e.symm : (a : ι') → ι) i' : ι) : E)
Tactic: classical
    dsimp [reindex]
    rw [coe_ofRepr]
    dsimp
    rw [← b.repr_symm_single, LinearIsometryEquiv.piLpCongrLeft_symm,
      EuclideanSpace.piLpCongrLeft_single]
-- 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
inst_3 : Fintype ι
inst_4 : Fintype ι'
b : OrthonormalBasis ι 𝕜 E
e : ι ≃ ι'
i' : ι'
dsimp :
  Eq.{u_4 + 1} (α := E) (({ repr := b.repr.trans (LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e) } : (a : ι') → E) i' : E)
    ((b : (a : ι) → E) ((e.symm : (a : ι') → ι) i' : ι) : E)
dsimp₁ :
  Eq.{u_4 + 1} (α := E)
    ((fun (i : ι') ↦
          ((LinearIsometryEquiv.symm (b.repr.trans (LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e)) :
                (a : EuclideanSpace 𝕜 ι') → E)
              (EuclideanSpace.single i 1) :
            E))
        i' :
      E)
    ((b : (a : ι) → E) ((e.symm : (a : ι') → ι) i' : ι) : E)
⊢ Eq.{u_4 + 1} (α := E) ((b.reindex e : (a : ι') → E) i' : E) ((b : (a : ι) → E) ((e.symm : (a : ι') → ι) i' : ι) : E)
have dsimp₂ : Eq.{u_4 + 1} (α := E)
  ((b.repr.symm : (a : EuclideanSpace 𝕜 ι) → E)
      ((LinearIsometryEquiv.symm (LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e) :
            (a : EuclideanSpace 𝕜 ι') → EuclideanSpace 𝕜 ι)
          (EuclideanSpace.single i' 1) :
        EuclideanSpace 𝕜 ι) :
    E)
  ((b : (a : ι) → E) ((e.symm : (a : ι') → ι) i' : ι) : E)
Tactic: classical
    dsimp [reindex]
    rw [coe_ofRepr]
    dsimp
    rw [← b.repr_symm_single, LinearIsometryEquiv.piLpCongrLeft_symm,
      EuclideanSpace.piLpCongrLeft_single]
-- 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
inst_3 : Fintype ι
inst_4 : Fintype ι'
b : OrthonormalBasis ι 𝕜 E
e : ι ≃ ι'
x : E
i' : ι'
⊢ Eq.{u_3 + 1} (α := (fun (x : ι') ↦ 𝕜) i') (ofLp (p := 2) ((repr (b.reindex e) : (a : E) → EuclideanSpace 𝕜 ι') x) i')
    (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) x) ((e.symm : (a : ι') → ι) i'))
have rw : ⟪(b.reindex e : (a : ι') → E) i', x⟫ =
  ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) x) ((e.symm : (a : ι') → ι) i')
Tactic: rw [OrthonormalBasis.repr_apply_apply, b.repr_apply_apply, OrthonormalBasis.coe_reindex,
    comp_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
inst_3 : Fintype ι
inst_4 : Fintype ι'
b : OrthonormalBasis ι 𝕜 E
e : ι ≃ ι'
x : E
i' : ι'
rw :
  ⟪(b.reindex e : (a : ι') → E) i', x⟫ =
    ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) x) ((e.symm : (a : ι') → ι) i')
⊢ Eq.{u_3 + 1} (α := (fun (x : ι') ↦ 𝕜) i') (ofLp (p := 2) ((repr (b.reindex e) : (a : E) → EuclideanSpace 𝕜 ι') x) i')
    (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) x) ((e.symm : (a : ι') → ι) i'))
have rw₁ : ⟪(b.reindex e : (a : ι') → E) i', x⟫ = ⟪(b : (a : ι) → E) ((e.symm : (a : ι') → ι) i' : ι), x⟫
Tactic: rw [OrthonormalBasis.repr_apply_apply, b.repr_apply_apply, OrthonormalBasis.coe_reindex,
    comp_apply]