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 ι
inst_8 : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily.{u_3, u_4, u_1, u_4} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
e₁ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] (i : ι) → ↥(V i) := linearEquivFunOnFintype 𝕜 ι fun (i : ι) ↦ ↥(V i)
e₂ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] E := LinearEquiv.ofBijective (coeLinearMap V) hV
v w : PiLp.{u_1, u_4} 2 fun (i : ι) ↦ ↥(V i)
e_a :
  Eq.{u_1 + 1} (α := Finset ι) Finset.univ
    (Multiset.toFinset
      (↑(Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ v.ofLp i = 0) (Finset.val Finset.univ) ⋯) :
        Multiset ι))
⊢ 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 ∨ w.ofLp i = 0) (Finset.val Finset.univ) sorry) :
      Multiset ι))
Tactic: congr
-- 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 ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily.{u_3, u_4, u_1, u_4} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
w : PiLp.{u_1, u_4} 2 fun (i : ι) ↦ ↥(V i)
e₁ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] (i : ι) → ↥(V i) := linearEquivFunOnFintype 𝕜 ι fun (i : ι) ↦ ↥(V i)
e₂ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] E := LinearEquiv.ofBijective (coeLinearMap V) hV
⊢ Eq.{u_4 + 1} (α := E)
    ((LinearIsometryEquiv.symm (hV.isometryL2OfOrthogonalFamily hV') : (a : PiLp 2 fun (i : ι) ↦ ↥(V i)) → E) w : E)
    (∑ i : ι, (↑(w.ofLp i) : E) : E)
have suffices : ∀ (v : ⨁ (i : ι), ↥(V i)),
  Eq.{u_4 + 1} (α := E) ((e₂ : (a : ⨁ (i : ι), ↥(V i)) → E) v : E)
    (∑ i : ι, (↑((e₁ : (a : ⨁ (i : ι), ↥(V i)) → (i : ι) → ↥(V i)) v i) : E) : E)
Tactic: suffices ∀ v : ⨁ i, V i, e₂ v = ∑ i, e₁ v i by exact this (e₁.symm w)
-- 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 ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily.{u_3, u_4, u_1, u_4} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
w : PiLp.{u_1, u_4} 2 fun (i : ι) ↦ ↥(V i)
let let₁ let₂ let₃ :
  Eq.{u_4 + 1} (α := E)
    ((LinearIsometryEquiv.symm (hV.isometryL2OfOrthogonalFamily hV') : (a : PiLp 2 fun (i : ι) ↦ ↥(V i)) → E) w : E)
    (∑ i : ι, (↑(w.ofLp i) : E) : E)
⊢ Eq.{u_4 + 1} (α := E)
    ((LinearIsometryEquiv.symm (hV.isometryL2OfOrthogonalFamily hV') : (a : PiLp 2 fun (i : ι) ↦ ↥(V i)) → E) w : E)
    (∑ i : ι, (↑(w.ofLp i) : E) : E)
have let₄ : let e₁ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] (i : ι) → ↥(V i) := linearEquivFunOnFintype 𝕜 ι fun (i : ι) ↦ ↥(V i);
let e₂ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] E := LinearEquiv.ofBijective (coeLinearMap V) hV;
∀ (v : ⨁ (i : ι), ↥(V i)),
  Eq.{u_4 + 1} (α := E) ((e₂ : (a : ⨁ (i : ι), ↥(V i)) → E) v : E)
    (∑ i : ι, (↑((e₁ : (a : ⨁ (i : ι), ↥(V i)) → (i : ι) → ↥(V i)) v i) : E) : E)
Tactic: classical
    let e₁ := DirectSum.linearEquivFunOnFintype 𝕜 ι fun i => V i
    let e₂ := LinearEquiv.ofBijective (DirectSum.coeLinearMap V) hV
    suffices ∀ v : ⨁ i, V i, e₂ v = ∑ i, e₁ v i by exact this (e₁.symm w)
    simp [e₁, e₂, DirectSum.coeLinearMap, DirectSum.toModule, DFinsupp.lsum,
      DFinsupp.sumAddHom_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
inst_1 : DecidableEq ι
inst_2 : Fintype ι
⊢ Orthonormal 𝕜 (E := EuclideanSpace 𝕜 ι) fun (i : ι) ↦ single i 1
have simp_rw : ∀ (i j : ι), True
Tactic: simp_rw [orthonormal_iff_ite, EuclideanSpace.inner_single_left, map_one, one_mul,
    PiLp.single_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 ι
f g : OrthonormalBasis ι 𝕜 E
h : f.repr = g.repr
⊢ f = g
have ofRepr : ∀ (repr : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι) (h : { repr := repr : OrthonormalBasis ι 𝕜 E }.repr = g.repr),
  { repr := repr : OrthonormalBasis ι 𝕜 E } = g
Tactic: cases f
Cleared hypotheses: f, 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 ι
g : OrthonormalBasis ι 𝕜 E
repr : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι
h : { repr := repr : OrthonormalBasis ι 𝕜 E }.repr = g.repr
⊢ { repr := repr : OrthonormalBasis ι 𝕜 E } = g
have ofRepr : ∀ (repr_1 : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι) (h : { repr := repr : OrthonormalBasis ι 𝕜 E }.repr = { repr := repr_1 }.repr),
  { repr := repr : OrthonormalBasis ι 𝕜 E } = { repr := repr_1 }
Tactic: cases g
Cleared hypotheses: g, h
-- 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')
⊢ (↑b.repr.symm : EuclideanSpace 𝕜 ι →ₗ[𝕜] E) = (↑b'.repr.symm : EuclideanSpace 𝕜 ι →ₗ[𝕜] E)
have 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 (ι → 𝕜))
Tactic: rw [← LinearMap.cancel_right (WithLp.linearEquiv 2 𝕜 (_ → 𝕜)).symm.surjective]
-- 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')
⊢ (↑b.repr.symm : EuclideanSpace 𝕜 ι →ₗ[𝕜] E) ∘ₗ
      (↑(LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (ι → 𝕜))) : (ι → 𝕜) →ₗ[𝕜] WithLp 2 (ι → 𝕜)) =
    (↑b'.repr.symm : EuclideanSpace 𝕜 ι →ₗ[𝕜] E) ∘ₗ
      (↑(LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (ι → 𝕜))) : (ι → 𝕜) →ₗ[𝕜] WithLp 2 (ι → 𝕜))
have refine : ∀ (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)
Tactic: refine LinearMap.pi_ext fun i k => ?_
-- 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')
i : ι
k : 𝕜
⊢ k = HSMul.hSMul (β := 𝕜) k 1
have rw : k = k * 1
Tactic: rw [smul_eq_mul, mul_one]
-- 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')
i : ι
k : 𝕜
rw : k = k * 1
⊢ k = HSMul.hSMul (β := 𝕜) k 1
have rw₁ : k = k
Tactic: rw [smul_eq_mul, mul_one]
-- 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 ι
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')
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)
have this : k = HSMul.hSMul (β := 𝕜) k 1
Tactic: have : k = k • (1 : 𝕜) := by rw [smul_eq_mul, mul_one]
-- 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')
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)
have rw : Eq.{u_4 + 1} (α := E)
  (((↑b.repr.symm : EuclideanSpace 𝕜 ι →ₗ[𝕜] E) ∘ₗ
          (↑(LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (ι → 𝕜))) : (ι → 𝕜) →ₗ[𝕜] WithLp 2 (ι → 𝕜)) :
        (a : (i : ι) → 𝕜) → E)
      (HSMul.hSMul (β := (j : ι) → 𝕜) k (Pi.single (M := fun (i : ι) ↦ 𝕜) i 1)) :
    E)
  (((↑b'.repr.symm : EuclideanSpace 𝕜 ι →ₗ[𝕜] E) ∘ₗ
          (↑(LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (ι → 𝕜))) : (ι → 𝕜) →ₗ[𝕜] WithLp 2 (ι → 𝕜)) :
        (a : (i : ι) → 𝕜) → E)
      (HSMul.hSMul (β := (j : ι) → 𝕜) k (Pi.single (M := fun (i : ι) ↦ 𝕜) i 1)) :
    E)
Tactic: rw [this, Pi.single_smul]
-- 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 ι
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')
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)
        (HSMul.hSMul (β := (j : ι) → 𝕜) k (Pi.single (M := fun (i : ι) ↦ 𝕜) i 1)) :
      E)
    (((↑b'.repr.symm : EuclideanSpace 𝕜 ι →ₗ[𝕜] E) ∘ₗ
            (↑(LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (ι → 𝕜))) : (ι → 𝕜) →ₗ[𝕜] WithLp 2 (ι → 𝕜)) :
          (a : (i : ι) → 𝕜) → E)
        (HSMul.hSMul (β := (j : ι) → 𝕜) k (Pi.single (M := fun (i : ι) ↦ 𝕜) i 1)) :
      E)
have h₁ : Eq.{u_4 + 1} (α := E)
  ((fun (b : OrthonormalBasis ι 𝕜 E) (i : ι) ↦
      ((b.repr.symm : (a : EuclideanSpace 𝕜 ι) → E) (EuclideanSpace.single i 1) : E))
    b i)
  ((fun (b : OrthonormalBasis ι 𝕜 E) (i : ι) ↦
      ((b.repr.symm : (a : EuclideanSpace 𝕜 ι) → E) (EuclideanSpace.single i 1) : E))
    b' i)
Tactic: replace h := congr_fun h i
Cleared hypotheses: h
-- 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
i : ι
k : 𝕜
this : k = HSMul.hSMul (β := 𝕜) k 1
h :
  Eq.{u_4 + 1} (α := E)
    ((fun (b : OrthonormalBasis ι 𝕜 E) (i : ι) ↦
        ((b.repr.symm : (a : EuclideanSpace 𝕜 ι) → E) (EuclideanSpace.single i 1) : E))
      b i)
    ((fun (b : OrthonormalBasis ι 𝕜 E) (i : ι) ↦
        ((b.repr.symm : (a : EuclideanSpace 𝕜 ι) → E) (EuclideanSpace.single i 1) : E))
      b' i)
⊢ Eq.{u_4 + 1} (α := E)
    (((↑b.repr.symm : EuclideanSpace 𝕜 ι →ₗ[𝕜] E) ∘ₗ
            (↑(LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (ι → 𝕜))) : (ι → 𝕜) →ₗ[𝕜] WithLp 2 (ι → 𝕜)) :
          (a : (i : ι) → 𝕜) → E)
        (HSMul.hSMul (β := (j : ι) → 𝕜) k (Pi.single (M := fun (i : ι) ↦ 𝕜) i 1)) :
      E)
    (((↑b'.repr.symm : EuclideanSpace 𝕜 ι →ₗ[𝕜] E) ∘ₗ
            (↑(LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (ι → 𝕜))) : (ι → 𝕜) →ₗ[𝕜] WithLp 2 (ι → 𝕜)) :
          (a : (i : ι) → 𝕜) → E)
        (HSMul.hSMul (β := (j : ι) → 𝕜) k (Pi.single (M := fun (i : ι) ↦ 𝕜) i 1)) :
      E)
have simp : HSMul.hSMul (β := E) k ((b.repr.symm : (a : WithLp 2 (ι → 𝕜)) → E) (PiLp.single 2 (β := fun (i : ι) ↦ 𝕜) i 1) : E) =
  HSMul.hSMul (β := E) k ((b'.repr.symm : (a : WithLp 2 (ι → 𝕜)) → E) (PiLp.single 2 (β := fun (i : ι) ↦ 𝕜) i 1) : E)
Tactic: 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 ⊢
-- 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
i : ι
k : 𝕜
this : k = HSMul.hSMul (β := 𝕜) k 1
h :
  Eq.{u_4 + 1} (α := E) ((b.repr.symm : (a : EuclideanSpace 𝕜 ι) → E) (EuclideanSpace.single i 1) : E)
    ((b'.repr.symm : (a : EuclideanSpace 𝕜 ι) → E) (EuclideanSpace.single i 1) : E)
⊢ HSMul.hSMul (β := E) k ((b.repr.symm : (a : WithLp 2 (ι → 𝕜)) → E) (PiLp.single 2 (β := fun (i : ι) ↦ 𝕜) i 1) : E) =
    HSMul.hSMul (β := E) k ((b'.repr.symm : (a : WithLp 2 (ι → 𝕜)) → E) (PiLp.single 2 (β := fun (i : ι) ↦ 𝕜) i 1) : E)
have rw : HSMul.hSMul (β := E) k ((b'.repr.symm : (a : EuclideanSpace 𝕜 ι) → E) (EuclideanSpace.single i 1) : E) =
  HSMul.hSMul (β := E) k ((b'.repr.symm : (a : WithLp 2 (ι → 𝕜)) → E) (PiLp.single 2 (β := fun (i : ι) ↦ 𝕜) i 1) : E)
Tactic: rw [h]
-- 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')
⊢ (↑b.repr.symm : EuclideanSpace 𝕜 ι →ₗ[𝕜] E) = (↑b'.repr.symm : EuclideanSpace 𝕜 ι →ₗ[𝕜] E)
have 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 (ι → 𝕜))
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_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 (ι → 𝕜))
⊢ (↑b.repr.symm : EuclideanSpace 𝕜 ι →ₗ[𝕜] E) = (↑b'.repr.symm : EuclideanSpace 𝕜 ι →ₗ[𝕜] E)
have 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)
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]