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
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')
rw₁ : ⟪(b.reindex e : (a : ι') → E) i', x⟫ = ⟪(b : (a : ι) → E) ((e.symm : (a : ι') → ι) i' : ι), x⟫
⊢ 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₂ : ⟪comp.{u_2 + 1, u_1 + 1, u_4 + 1} (β := ι) (⇑b : (a : ι) → E) (⇑e.symm : (a : ι') → ι) 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]
-- 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')
rw₁ : ⟪(b.reindex e : (a : ι') → E) i', x⟫ = ⟪(b : (a : ι) → E) ((e.symm : (a : ι') → ι) i' : ι), x⟫
rw₂ :
  ⟪comp.{u_2 + 1, u_1 + 1, u_4 + 1} (β := ι) (⇑b : (a : ι) → E) (⇑e.symm : (a : ι') → ι) i', x⟫ =
    ⟪(b : (a : ι) → E) ((e.symm : (a : ι') → ι) i' : ι), x⟫
⊢ 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 : (a : ι) → E) ((e.symm : (a : ι') → ι) 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]
-- 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: classical
  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: classical
  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')
rw₁ : ⟪(b.reindex e : (a : ι') → E) i', x⟫ = ⟪(b : (a : ι) → E) ((e.symm : (a : ι') → ι) i' : ι), x⟫
⊢ 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₂ : ⟪comp.{u_2 + 1, u_1 + 1, u_4 + 1} (β := ι) (⇑b : (a : ι) → E) (⇑e.symm : (a : ι') → ι) i', x⟫ =
  ⟪(b : (a : ι) → E) ((e.symm : (a : ι') → ι) i' : ι), x⟫
Tactic: classical
  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')
rw₁ : ⟪(b.reindex e : (a : ι') → E) i', x⟫ = ⟪(b : (a : ι) → E) ((e.symm : (a : ι') → ι) i' : ι), x⟫
rw₂ :
  ⟪comp.{u_2 + 1, u_1 + 1, u_4 + 1} (β := ι) (⇑b : (a : ι) → E) (⇑e.symm : (a : ι') → ι) i', x⟫ =
    ⟪(b : (a : ι) → E) ((e.symm : (a : ι') → ι) i' : ι), x⟫
⊢ 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 : (a : ι) → E) ((e.symm : (a : ι') → ι) i' : ι), x⟫ = ⟪(b : (a : ι) → E) ((e.symm : (a : ι') → ι) i' : ι), x⟫
Tactic: classical
  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
inst : Fintype ι
x : EuclideanSpace ℝ ι
i : ι
⊢ inner ℝ x ((basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i) = x.ofLp i
have rw : inner ℝ ((basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i) x = x.ofLp i
Tactic: rw [real_inner_comm, basisFun_inner]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
inst : Fintype ι
x : EuclideanSpace ℝ ι
i : ι
rw : inner ℝ ((basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i) x = x.ofLp i
⊢ inner ℝ x ((basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i) = x.ofLp i
have rw₁ : x.ofLp i = x.ofLp i
Tactic: rw [real_inner_comm, basisFun_inner]
-- 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 ι
E' : Type u_7
inst_4 : Fintype ι'
inst_5 : NormedAddCommGroup E'
inst_6 : InnerProductSpace 𝕜 E'
b : OrthonormalBasis ι 𝕜 E
b' : OrthonormalBasis ι' 𝕜 E'
e : ι ≃ ι'
⊢ (b.equiv b' e).symm = b'.equiv b e.symm
have apply : ∀ (i : ι'),
  Eq.{u_4 + 1} (α := E) (((b.equiv b' e).symm : (a : E') → E) ((b'.toBasis : (a : ι') → E') i : E') : E)
    ((b'.equiv b e.symm : (a : E') → E) ((b'.toBasis : (a : ι') → E') i : E') : E)
Tactic: apply b'.toBasis.ext_linearIsometryEquiv
-- 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 ι
E' : Type u_7
inst_4 : Fintype ι'
inst_5 : NormedAddCommGroup E'
inst_6 : InnerProductSpace 𝕜 E'
b : OrthonormalBasis ι 𝕜 E
b' : OrthonormalBasis ι' 𝕜 E'
e : ι ≃ ι'
i : ι
⊢ Eq.{u_7 + 1} (α := E') ((b.equiv b' e : (a : E) → E') ((b : (a : ι) → E) i : E) : E')
    ((b' : (a : ι') → E') ((e : (a : ι) → ι') i : ι') : E')
have simp : Eq.{u_7 + 1} (α := E')
  ((b'.repr.symm : (a : PiLp 2 fun (x : ι') ↦ 𝕜) → E')
      ((LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e : (a : EuclideanSpace 𝕜 ι) → PiLp 2 fun (x : ι') ↦ 𝕜)
          (EuclideanSpace.single i 1) :
        PiLp.{u_2, u_3} 2 fun (x : ι') ↦ 𝕜) :
    E')
  ((b' : (a : ι') → E') ((e : (a : ι) → ι') i : ι') : E')
Tactic: simp only [OrthonormalBasis.equiv, LinearIsometryEquiv.trans_apply, OrthonormalBasis.repr_self]
-- 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 ι
E' : Type u_7
inst_4 : Fintype ι'
inst_5 : NormedAddCommGroup E'
inst_6 : InnerProductSpace 𝕜 E'
b : OrthonormalBasis ι 𝕜 E
b' : OrthonormalBasis ι' 𝕜 E'
e : ι ≃ ι'
i : ι
⊢ Eq.{u_7 + 1} (α := E')
    ((b'.repr.symm : (a : PiLp 2 fun (x : ι') ↦ 𝕜) → E')
        ((LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e : (a : EuclideanSpace 𝕜 ι) → PiLp 2 fun (x : ι') ↦ 𝕜)
            (EuclideanSpace.single i 1) :
          PiLp.{u_2, u_3} 2 fun (x : ι') ↦ 𝕜) :
      E')
    ((b' : (a : ι') → E') ((e : (a : ι) → ι') i : ι') : E')
have refine : Eq (α := PiLp.{u_2, u_3} 2 fun (x : ι') ↦ 𝕜)
  ((LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e : (a : EuclideanSpace 𝕜 ι) → PiLp 2 fun (x : ι') ↦ 𝕜)
      (EuclideanSpace.single i 1) :
    PiLp.{u_2, u_3} 2 fun (x : ι') ↦ 𝕜)
  (EuclideanSpace.single ((e : (a : ι) → ι') i) 1 : EuclideanSpace 𝕜 ι')
Tactic: refine DFunLike.congr rfl ?_
-- 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 ι
E' : Type u_7
inst_4 : Fintype ι'
inst_5 : NormedAddCommGroup E'
inst_6 : InnerProductSpace 𝕜 E'
b : OrthonormalBasis ι 𝕜 E
b' : OrthonormalBasis ι' 𝕜 E'
e : ι ≃ ι'
i : ι
⊢ Eq (α := PiLp.{u_2, u_3} 2 fun (x : ι') ↦ 𝕜)
    ((LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e : (a : EuclideanSpace 𝕜 ι) → PiLp 2 fun (x : ι') ↦ 𝕜)
        (EuclideanSpace.single i 1) :
      PiLp.{u_2, u_3} 2 fun (x : ι') ↦ 𝕜)
    (EuclideanSpace.single ((e : (a : ι) → ι') i) 1 : EuclideanSpace 𝕜 ι')
have h : ∀ (j : ι'),
  Eq.{u_3 + 1} (α := 𝕜)
    (ofLp (p := 2)
        ((LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e : (a : EuclideanSpace 𝕜 ι) → PiLp 2 fun (x : ι') ↦ 𝕜)
          (EuclideanSpace.single i 1))
        j :
      𝕜)
    (ofLp (p := 2) (EuclideanSpace.single ((e : (a : ι) → ι') i) 1) j : 𝕜)
Tactic: ext j
-- 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 ι
E' : Type u_7
inst_4 : Fintype ι'
inst_5 : NormedAddCommGroup E'
inst_6 : InnerProductSpace 𝕜 E'
b : OrthonormalBasis ι 𝕜 E
b' : OrthonormalBasis ι' 𝕜 E'
e : ι ≃ ι'
i : ι
⊢ Eq.{u_7 + 1} (α := E') ((b.equiv b' e : (a : E) → E') ((b : (a : ι) → E) i : E) : E')
    ((b' : (a : ι') → E') ((e : (a : ι) → ι') i : ι') : E')
have simp : Eq.{u_7 + 1} (α := E')
  ((b'.repr.symm : (a : PiLp 2 fun (x : ι') ↦ 𝕜) → E')
      ((LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e : (a : EuclideanSpace 𝕜 ι) → PiLp 2 fun (x : ι') ↦ 𝕜)
          (EuclideanSpace.single i 1) :
        PiLp.{u_2, u_3} 2 fun (x : ι') ↦ 𝕜) :
    E')
  ((b' : (a : ι') → E') ((e : (a : ι) → ι') i : ι') : E')
Tactic: classical
  simp only [OrthonormalBasis.equiv, LinearIsometryEquiv.trans_apply, OrthonormalBasis.repr_self]
  refine DFunLike.congr rfl ?_
  ext j
  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
inst_3 : Fintype ι
E' : Type u_7
inst_4 : Fintype ι'
inst_5 : NormedAddCommGroup E'
inst_6 : InnerProductSpace 𝕜 E'
b : OrthonormalBasis ι 𝕜 E
b' : OrthonormalBasis ι' 𝕜 E'
e : ι ≃ ι'
i : ι
simp :
  Eq.{u_7 + 1} (α := E')
    ((b'.repr.symm : (a : PiLp 2 fun (x : ι') ↦ 𝕜) → E')
        ((LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e : (a : EuclideanSpace 𝕜 ι) → PiLp 2 fun (x : ι') ↦ 𝕜)
            (EuclideanSpace.single i 1) :
          PiLp.{u_2, u_3} 2 fun (x : ι') ↦ 𝕜) :
      E')
    ((b' : (a : ι') → E') ((e : (a : ι) → ι') i : ι') : E')
⊢ Eq.{u_7 + 1} (α := E') ((b.equiv b' e : (a : E) → E') ((b : (a : ι) → E) i : E) : E')
    ((b' : (a : ι') → E') ((e : (a : ι) → ι') i : ι') : E')
have simp₁ : Eq (α := PiLp.{u_2, u_3} 2 fun (x : ι') ↦ 𝕜)
  ((LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e : (a : EuclideanSpace 𝕜 ι) → PiLp 2 fun (x : ι') ↦ 𝕜)
      (EuclideanSpace.single i 1) :
    PiLp.{u_2, u_3} 2 fun (x : ι') ↦ 𝕜)
  (EuclideanSpace.single ((e : (a : ι) → ι') i) 1 : EuclideanSpace 𝕜 ι')
Tactic: classical
  simp only [OrthonormalBasis.equiv, LinearIsometryEquiv.trans_apply, OrthonormalBasis.repr_self]
  refine DFunLike.congr rfl ?_
  ext j
  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
inst_3 : Fintype ι
E' : Type u_7
inst_4 : Fintype ι'
inst_5 : NormedAddCommGroup E'
inst_6 : InnerProductSpace 𝕜 E'
b : OrthonormalBasis ι 𝕜 E
b' : OrthonormalBasis ι' 𝕜 E'
e : ι ≃ ι'
i : ι
simp :
  Eq.{u_7 + 1} (α := E')
    ((b'.repr.symm : (a : PiLp 2 fun (x : ι') ↦ 𝕜) → E')
        ((LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e : (a : EuclideanSpace 𝕜 ι) → PiLp 2 fun (x : ι') ↦ 𝕜)
            (EuclideanSpace.single i 1) :
          PiLp.{u_2, u_3} 2 fun (x : ι') ↦ 𝕜) :
      E')
    ((b' : (a : ι') → E') ((e : (a : ι) → ι') i : ι') : E')
simp₁ :
  Eq (α := PiLp.{u_2, u_3} 2 fun (x : ι') ↦ 𝕜)
    ((LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e : (a : EuclideanSpace 𝕜 ι) → PiLp 2 fun (x : ι') ↦ 𝕜)
        (EuclideanSpace.single i 1) :
      PiLp.{u_2, u_3} 2 fun (x : ι') ↦ 𝕜)
    (EuclideanSpace.single ((e : (a : ι) → ι') i) 1 : EuclideanSpace 𝕜 ι')
⊢ Eq.{u_7 + 1} (α := E') ((b.equiv b' e : (a : E) → E') ((b : (a : ι) → E) i : E) : E')
    ((b' : (a : ι') → E') ((e : (a : ι) → ι') i : ι') : E')
have h : ∀ (j : ι'),
  Eq.{u_3 + 1} (α := 𝕜)
    (ofLp (p := 2)
        ((LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e : (a : EuclideanSpace 𝕜 ι) → PiLp 2 fun (x : ι') ↦ 𝕜)
          (EuclideanSpace.single i 1))
        j :
      𝕜)
    (ofLp (p := 2) (EuclideanSpace.single ((e : (a : ι) → ι') i) 1) j : 𝕜)
Tactic: classical
  simp only [OrthonormalBasis.equiv, LinearIsometryEquiv.trans_apply, OrthonormalBasis.repr_self]
  refine DFunLike.congr rfl ?_
  ext j
  simp
-- 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
⊢ b.equiv b (Equiv.refl ι) = LinearIsometryEquiv.refl 𝕜 E
have apply : ∀ (i : ι),
  Eq (α := E) ((b.equiv b (Equiv.refl ι) : (a : E) → E) ((b.toBasis : (a : ι) → E) i : E) : E)
    ((LinearIsometryEquiv.refl 𝕜 E : (a : E) → E) ((b.toBasis : (a : ι) → E) i : E) : E)
Tactic: apply b.toBasis.ext_linearIsometryEquiv
-- 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 ι
E' : Type u_7
inst_4 : Fintype ι'
inst_5 : NormedAddCommGroup E'
inst_6 : InnerProductSpace 𝕜 E'
b : OrthonormalBasis ι 𝕜 E
b' : OrthonormalBasis ι' 𝕜 E'
e : ι ≃ ι'
x : E
⊢ Eq.{u_7 + 1} (α := E') ((b.equiv b' e : (a : E) → E') x : E')
    (∑ i : ι,
        HSMul.hSMul.{u_3, u_7, u_7} (α := (fun (x : ι) ↦ 𝕜) i) (β := E')
          (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) x) i)
          ((b' : (a : ι') → E') ((e : (a : ι) → ι') i : ι') : E') :
      E')
have nth_rw : Eq.{u_7 + 1} (α := E')
  (∑ x_1 : ι,
    (b.equiv b' e : (a : E) → E')
      (HSMul.hSMul.{u_3, u_4, u_4} (α := (fun (x : ι) ↦ 𝕜) x_1) (β := E)
        (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) x) x_1) ((b : (a : ι) → E) x_1 : E)))
  (∑ i : ι,
    HSMul.hSMul.{u_3, u_7, u_7} (α := (fun (x : ι) ↦ 𝕜) i) (β := E')
      (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) x) i)
      ((b' : (a : ι') → E') ((e : (a : ι) → ι') i : ι') : E'))
Tactic: nth_rw 1 [← b.sum_repr x, map_sum]
-- 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 ι
E' : Type u_7
inst_4 : Fintype ι'
inst_5 : NormedAddCommGroup E'
inst_6 : InnerProductSpace 𝕜 E'
b : OrthonormalBasis ι 𝕜 E
b' : OrthonormalBasis ι' 𝕜 E'
e : ι ≃ ι'
x : E
simp_rw simp_rw₁ :
  Eq.{u_7 + 1} (α := E')
    (∑ x_1 : ι,
      (b.equiv b' e : (a : E) → E')
        (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (β := E) (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) x) x_1)
          ((b : (a : ι) → E) x_1 : E)))
    (∑ x_1 : ι,
      HSMul.hSMul.{u_3, u_7, u_7} (α := 𝕜) (β := E') (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) x) x_1)
        ((b' : (a : ι') → E') ((e : (a : ι) → ι') x_1 : ι') : E'))
⊢ Eq.{u_7 + 1} (α := E')
    (∑ x_1 : ι,
      (b.equiv b' e : (a : E) → E')
        (HSMul.hSMul.{u_3, u_4, u_4} (α := (fun (x : ι) ↦ 𝕜) x_1) (β := E)
          (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) x) x_1) ((b : (a : ι) → E) x_1 : E)))
    (∑ i : ι,
      HSMul.hSMul.{u_3, u_7, u_7} (α := (fun (x : ι) ↦ 𝕜) i) (β := E')
        (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) x) i)
        ((b' : (a : ι') → E') ((e : (a : ι) → ι') i : ι') : E'))
have simp_rw₂ : Eq.{u_7 + 1} (α := E')
  (∑ x_1 : ι,
    HSMul.hSMul.{u_3, u_7, u_7} (α := 𝕜) (β := E') (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) x) x_1)
      ((b.equiv b' e : (a : E) → E') ((b : (a : ι) → E) x_1 : E) : E'))
  (∑ x_1 : ι,
    HSMul.hSMul.{u_3, u_7, u_7} (α := 𝕜) (β := E') (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) x) x_1)
      ((b' : (a : ι') → E') ((e : (a : ι) → ι') x_1 : ι') : E'))
Tactic: simp_rw [map_smul, equiv_apply_basis]
-- 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 : EuclideanSpace 𝕜 ι
simp_rw simp_rw₁ :
  Eq.{u_4 + 1} (α := E)
    ((OrthonormalBasis.equiv (EuclideanSpace.basisFun ι 𝕜) b (Equiv.refl ι) : (a : EuclideanSpace 𝕜 ι) → E) x : E)
    (∑ x_1 : ι, HSMul.hSMul (β := E) (x.ofLp x_1) ((b : (a : ι) → E) x_1 : E) : E)
⊢ Eq.{u_4 + 1} (α := E)
    ((OrthonormalBasis.equiv (EuclideanSpace.basisFun ι 𝕜) b (Equiv.refl ι) : (a : EuclideanSpace 𝕜 ι) → E) x : E)
    (∑ i : ι, HSMul.hSMul (β := E) (x.ofLp i) ((b : (a : ι) → E) i : E) : E)
have simp_rw₂ : Eq.{u_4 + 1} (α := E)
  (∑ x_1 : ι,
    HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (β := E)
      (ofLp (p := 2) ((repr (EuclideanSpace.basisFun ι 𝕜) : (a : EuclideanSpace 𝕜 ι) → EuclideanSpace 𝕜 ι) x) x_1)
      ((b : (a : ι) → E) ((Equiv.refl ι : (a : ι) → ι) x_1 : ι) : E))
  (∑ x_1 : ι, HSMul.hSMul (β := E) (x.ofLp x_1) ((b : (a : ι) → E) x_1 : E))
Tactic: simp_rw [equiv_apply, EuclideanSpace.basisFun_repr, Equiv.refl_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
x : EuclideanSpace 𝕜 ι
simp_rw simp_rw₁ :
  Eq.{u_4 + 1} (α := E)
    ((OrthonormalBasis.equiv (EuclideanSpace.basisFun ι 𝕜) b (Equiv.refl ι) : (a : EuclideanSpace 𝕜 ι) → E) x : E)
    (∑ x_1 : ι, HSMul.hSMul (β := E) (x.ofLp x_1) ((b : (a : ι) → E) x_1 : E) : E)
simp_rw₂ :
  Eq.{u_4 + 1} (α := E)
    (∑ x_1 : ι,
      HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (β := E)
        (ofLp (p := 2) ((repr (EuclideanSpace.basisFun ι 𝕜) : (a : EuclideanSpace 𝕜 ι) → EuclideanSpace 𝕜 ι) x) x_1)
        ((b : (a : ι) → E) ((Equiv.refl ι : (a : ι) → ι) x_1 : ι) : E))
    (∑ x_1 : ι, HSMul.hSMul (β := E) (x.ofLp x_1) ((b : (a : ι) → E) x_1 : E))
⊢ Eq.{u_4 + 1} (α := E)
    ((OrthonormalBasis.equiv (EuclideanSpace.basisFun ι 𝕜) b (Equiv.refl ι) : (a : EuclideanSpace 𝕜 ι) → E) x : E)
    (∑ i : ι, HSMul.hSMul (β := E) (x.ofLp i) ((b : (a : ι) → E) i : E) : E)
have simp_rw₃ : Eq.{u_4 + 1} (α := E)
  (∑ x_1 : ι, HSMul.hSMul (β := E) (x.ofLp x_1) ((b : (a : ι) → E) ((Equiv.refl ι : (a : ι) → ι) x_1 : ι) : E))
  (∑ x_1 : ι, HSMul.hSMul (β := E) (x.ofLp x_1) ((b : (a : ι) → E) x_1 : E))
Tactic: simp_rw [equiv_apply, EuclideanSpace.basisFun_repr, Equiv.refl_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 ι
⊢ Orthonormal ℝ (E := ℂ) (ι := Fin 2) (⇑basisOneI : (a : Fin 2) → ℂ)
have rw : ∀ (i j : Fin 2),
  inner ℝ (E := ℂ) ((basisOneI : (a : Fin 2) → ℂ) i : ℂ) ((basisOneI : (a : Fin 2) → ℂ) j : ℂ) = 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_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 : Fin 2
⊢ ∀ (j : Fin 2),
    inner ℝ (E := ℂ) ((basisOneI : (a : Fin 2) → ℂ) i : ℂ) ((basisOneI : (a : Fin 2) → ℂ) j : ℂ) =
      if i = j then 1 else 0
have 0 : ∀ (j : Fin 2),
  inner ℝ (E := ℂ) ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) : ℂ)
      ((basisOneI : (a : Fin 2) → ℂ) j : ℂ) =
    if (fun (i : Fin 2) ↦ i) ⟨0, sorry⟩ = j then 1 else 0
Tactic: fin_cases i
Cleared hypotheses: 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 ι
i : Fin 2
0 :
  ∀ (j : Fin 2),
    inner ℝ (E := ℂ) ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) : ℂ)
        ((basisOneI : (a : Fin 2) → ℂ) j : ℂ) =
      if (fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩ = j then 1 else 0
⊢ ∀ (j : Fin 2),
    inner ℝ (E := ℂ) ((basisOneI : (a : Fin 2) → ℂ) i : ℂ) ((basisOneI : (a : Fin 2) → ℂ) j : ℂ) =
      if i = j then 1 else 0
have 1 : ∀ (j : Fin 2),
  inner ℝ (E := ℂ) ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) : ℂ)
      ((basisOneI : (a : Fin 2) → ℂ) j : ℂ) =
    if (fun (i : Fin 2) ↦ i) ⟨1, sorry⟩ = j then 1 else 0
Tactic: fin_cases i
Cleared hypotheses: 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 ι
j : Fin 2
⊢ inner ℝ (E := ℂ) ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) : ℂ)
      ((basisOneI : (a : Fin 2) → ℂ) j : ℂ) =
    if (fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩ = j then 1 else 0
have 0 : inner ℝ (E := ℂ) ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) : ℂ)
    ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) : ℂ) =
  if Eq (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) then 1 else 0
Tactic: fin_cases j
Cleared hypotheses: j