awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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 : ι ≃ ι'
⊢ OrthonormalBasis.toBasis (b.reindex e) = b.toBasis.reindex e

Tactic:
Basis.eq_ofRepr_eq_repr fun _ ↦ congr_fun rfl

Premises used: Module.Basis.eq_ofRepr_eq_repr, congr_fun, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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 : ι ≃ ι'
⊢ Eq (α := (a : ι') → E) (⇑(b.reindex e) : (a : ι') → E)
    (comp.{u_2 + 1, u_1 + 1, u_4 + 1} (β := ι) (⇑b : (a : ι) → E) (⇑e.symm : (a : ι') → ι))

Tactic:
funext (b.reindex_apply e)

Premises used: OrthonormalBasis.reindex_apply, funext
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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⟫
rw₃ rw₄ :
  ⟪(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'))

Tactic:
rw [OrthonormalBasis.repr_apply_apply, b.repr_apply_apply, OrthonormalBasis.coe_reindex,
    comp_apply]

Premises used: OrthonormalBasis.coe_reindex, OrthonormalBasis.repr_apply_apply, Function.comp_apply
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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⟫
rw₃ rw₄ :
  ⟪(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'))

Tactic:
classical
  rw [OrthonormalBasis.repr_apply_apply, b.repr_apply_apply, OrthonormalBasis.coe_reindex,
    comp_apply]

Premises used: OrthonormalBasis.coe_reindex, OrthonormalBasis.repr_apply_apply, Function.comp_apply
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype ι
inst_2 : DecidableEq ι
i : ι
⊢ Eq (α := EuclideanSpace 𝕜 ι) ((basisFun ι 𝕜 : (a : ι) → EuclideanSpace 𝕜 ι) i : EuclideanSpace 𝕜 ι)
    (single i 1 : EuclideanSpace 𝕜 ι)

Tactic:
PiLp.basisFun_apply _ _ _ _

Premises used: PiLp.single, Function.update, PiLp.basisFun_apply, Pi.single, dite
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype ι
x : EuclideanSpace 𝕜 ι
i : ι
⊢ ofLp (p := 2) ((OrthonormalBasis.repr (basisFun ι 𝕜) : (a : EuclideanSpace 𝕜 ι) → EuclideanSpace 𝕜 ι) x) i = x.ofLp i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype ι
x : EuclideanSpace 𝕜 ι
i : ι
⊢ ⟪(basisFun ι 𝕜 : (a : ι) → EuclideanSpace 𝕜 ι) i, x⟫ = x.ofLp i

Tactic:
simp [← OrthonormalBasis.repr_apply_apply]

Premises used: OrthonormalBasis.repr_apply_apply
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
inst : Fintype ι
x : EuclideanSpace ℝ ι
i : ι
rw : inner ℝ ((basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i) x = x.ofLp i
rw₁ rw₂ : x.ofLp i = x.ofLp i
⊢ inner ℝ x ((basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i) = x.ofLp i

Tactic:
rw [real_inner_comm, basisFun_inner]

Premises used: EuclideanSpace.basisFun_inner, real_inner_comm
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype ι
⊢ Eq (α := Basis ι 𝕜 (EuclideanSpace 𝕜 ι)) (OrthonormalBasis.toBasis (basisFun ι 𝕜)) (PiLp.basisFun 2 𝕜 ι)

Tactic:
rfl

Premises used: PiLp.basisFun, LinearEquiv.trans, rfl, OrthonormalBasis.toBasis, WithLp.linearEquiv
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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 : ι ≃ ι'
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)
⊢ (b.equiv b' e).symm = b'.equiv b e.symm

Tactic:
apply b'.toBasis.ext_linearIsometryEquiv

Premises used: Module.Basis.ext_linearIsometryEquiv, OrthonormalBasis.toBasis
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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_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:
simp [OrthonormalBasis.equiv]

Premises used: OrthonormalBasis.equiv
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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')

Tactic:
simp only [OrthonormalBasis.equiv, LinearIsometryEquiv.trans_apply, OrthonormalBasis.repr_self]

Premises used: OrthonormalBasis.repr_self, OrthonormalBasis.equiv, LinearIsometryEquiv.trans_apply
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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')

Tactic:
DFunLike.congr rfl ?_

Premises used: DFunLike.congr, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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 : ι
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 𝕜 ι')
⊢ 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:
refine DFunLike.congr rfl ?_

Premises used: DFunLike.congr, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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 : ι
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 : 𝕜)
⊢ 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:
ext j
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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 : ι
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:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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 𝕜 ι')
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 : 𝕜)
⊢ 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')

Tactic:
classical
  simp only [OrthonormalBasis.equiv, LinearIsometryEquiv.trans_apply, OrthonormalBasis.repr_self]
  refine DFunLike.congr rfl ?_
  ext j
  simp

Premises used: DFunLike.congr, OrthonormalBasis.repr_self, OrthonormalBasis.equiv, LinearIsometryEquiv.trans_apply, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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
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)
⊢ b.equiv b (Equiv.refl ι) = LinearIsometryEquiv.refl 𝕜 E

Tactic:
apply b.toBasis.ext_linearIsometryEquiv

Premises used: Module.Basis.ext_linearIsometryEquiv, OrthonormalBasis.toBasis
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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 : ι),
    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:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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
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'))
⊢ 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')

Tactic:
nth_rw 1 [← b.sum_repr x, map_sum]

Premises used: map_sum, OrthonormalBasis.sum_repr
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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'))
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'))
⊢ 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:
simp_rw [map_smul, equiv_apply_basis]

Premises used: OrthonormalBasis.equiv_apply_basis, map_smul
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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))
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))
⊢ 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)

Tactic:
simp_rw [equiv_apply, EuclideanSpace.basisFun_repr, Equiv.refl_apply]

Premises used: Equiv.refl_apply, OrthonormalBasis.equiv_apply, EuclideanSpace.basisFun_repr
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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
simp_rw simp_rw₁ :
  Eq (α := (a : EuclideanSpace 𝕜 ι) → E)
    (⇑(OrthonormalBasis.equiv (EuclideanSpace.basisFun ι 𝕜) b (Equiv.refl ι)) : (a : EuclideanSpace 𝕜 ι) → E)
    fun (x : EuclideanSpace 𝕜 ι) ↦ ∑ x_1 : ι, HSMul.hSMul (β := E) (x.ofLp x_1) ((b : (a : ι) → E) x_1 : E)
⊢ Eq (α := (a : EuclideanSpace 𝕜 ι) → E)
    (⇑(OrthonormalBasis.equiv (EuclideanSpace.basisFun ι 𝕜) b (Equiv.refl ι)) : (a : EuclideanSpace 𝕜 ι) → E)
    fun (x : EuclideanSpace 𝕜 ι) ↦ ∑ i : ι, HSMul.hSMul (β := E) (x.ofLp i) ((b : (a : ι) → E) i : E)

Tactic:
simp_rw [← equiv_apply_euclideanSpace]

Premises used: OrthonormalBasis.equiv_apply_euclideanSpace
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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 ι
rw :
  ∀ (i j : Fin 2),
    inner ℝ (E := ℂ) ((basisOneI : (a : Fin 2) → ℂ) i : ℂ) ((basisOneI : (a : Fin 2) → ℂ) j : ℂ) =
      if i = j then 1 else 0
⊢ Orthonormal ℝ (E := ℂ) (ι := Fin 2) (⇑basisOneI : (a : Fin 2) → ℂ)

Tactic:
rw [orthonormal_iff_ite]

Premises used: orthonormal_iff_ite
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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
1 :
  ∀ (j : Fin 2),
    inner ℝ (E := ℂ) ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) : ℂ)
        ((basisOneI : (a : Fin 2) → ℂ) j : ℂ) =
      if (fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩ = 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

Tactic:
fin_cases i
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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
0 :
  inner ℝ (E := ℂ) ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) : ℂ)
      ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) : ℂ) =
    if Eq (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) then 1 else 0
h :
  inner ℝ (E := ℂ) ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) : ℂ)
      ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) : ℂ) =
    if Eq (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) then 1 else 0
⊢ 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

Tactic:
fin_cases j
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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
1 :
  inner ℝ (E := ℂ) ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) : ℂ)
      ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) : ℂ) =
    if Eq (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) then 1 else 0
h :
  inner ℝ (E := ℂ) ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) : ℂ)
      ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) : ℂ) =
    if Eq (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) then 1 else 0
⊢ inner ℝ (E := ℂ) ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) : ℂ)
      ((basisOneI : (a : Fin 2) → ℂ) j : ℂ) =
    if (fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩ = j then 1 else 0

Tactic:
fin_cases j
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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 ι
⊢ inner ℝ (E := ℂ) ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) : ℂ)
      ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) : ℂ) =
    if Eq (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) then 1 else 0

Tactic:
simp [real_inner_eq_re_inner]

Premises used: real_inner_eq_re_inner