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
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')
simp :
  (↑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) ∘ₗ
      (↑(LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (ι → 𝕜))) : (ι → 𝕜) →ₗ[𝕜] WithLp 2 (ι → 𝕜)) =
    (↑b'.repr.symm : EuclideanSpace 𝕜 ι →ₗ[𝕜] E) ∘ₗ
      (↑(LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (ι → 𝕜))) : (ι → 𝕜) →ₗ[𝕜] WithLp 2 (ι → 𝕜))

Tactic:
simp +instances only
-- 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 ι
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 (ι → 𝕜))

Tactic:
LinearMap.pi_ext fun i k => ?_

Premises used: LinearMap.pi_ext
-- 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 ι
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')
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)
⊢ (↑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:
refine LinearMap.pi_ext fun i k => ?_

Premises used: LinearMap.pi_ext
-- 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 ι
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
rw₁ rw₂ : k = k
⊢ k = HSMul.hSMul (β := 𝕜) k 1

Tactic:
rw [smul_eq_mul, mul_one]

Premises used: smul_eq_mul, mul_one
-- 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 ι
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

Tactic:
have : k = k • (1 : 𝕜) := by rw [smul_eq_mul, mul_one]
-- 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 ι
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
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)
⊢ 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:
rw [this, Pi.single_smul]

Premises used: Pi.single_smul
-- 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 ι
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)
    ((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
-- 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 ι
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)
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)
⊢ 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:
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 ⊢

Premises used: PiLp.toLp_single, LinearEquiv.trans_apply, LinearIsometryEquiv.coe_symm_toLinearEquiv, LinearEquiv.comp_coe, WithLp.coe_symm_linearEquiv, LinearEquiv.coe_coe, map_smul
-- 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 ι
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)
rw 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)
⊢ 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:
rw [h]
-- 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 ι
inst_4 : DecidableEq ι
e : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι
dsimp :
  Eq (α := (a : ι) → E) (fun (i : ι) ↦ EquivLike.coe e.symm (EuclideanSpace.single i 1)) fun (i : ι) ↦
    EquivLike.coe e.symm (EuclideanSpace.single i 1)
⊢ Eq (α := (a : ι) → E) (⇑{ repr := e : OrthonormalBasis ι 𝕜 E } : (a : ι) → E) fun (i : ι) ↦
    (e.symm : (a : EuclideanSpace 𝕜 ι) → E) (EuclideanSpace.single i 1)

Tactic:
dsimp only [DFunLike.coe]

Premises used: DFunLike.coe
-- 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 ι
inst_4 : DecidableEq ι
e : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι
h : ∀ (x : ι), EquivLike.coe e.symm (EuclideanSpace.single x 1) = EquivLike.coe e.symm (EuclideanSpace.single x 1)
⊢ Eq (α := (a : ι) → E) (fun (i : ι) ↦ EquivLike.coe e.symm (EuclideanSpace.single i 1)) fun (i : ι) ↦
    EquivLike.coe e.symm (EuclideanSpace.single i 1)

Tactic:
funext
-- 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 ι
inst_4 : DecidableEq ι
e : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι
x : ι
⊢ EquivLike.coe e.symm (EuclideanSpace.single x 1) = EquivLike.coe e.symm (EuclideanSpace.single x 1)

Tactic:
congr!
-- 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 ι
inst_4 : DecidableEq ι
b : OrthonormalBasis ι 𝕜 E
i : ι
⊢ EquivLike.coe b.repr.symm (EuclideanSpace.single i 1) = EquivLike.coe b.repr.symm (EuclideanSpace.single i 1)

Tactic:
congr!
-- 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 ι
inst_4 : DecidableEq ι
b : OrthonormalBasis ι 𝕜 E
i : ι
rw :
  Eq (α := EuclideanSpace 𝕜 ι)
    ((b.repr : (a : E) → EuclideanSpace 𝕜 ι)
        ((b.repr.symm : (a : EuclideanSpace 𝕜 ι) → E) (EuclideanSpace.single i 1)) :
      EuclideanSpace 𝕜 ι)
    (EuclideanSpace.single i 1 : EuclideanSpace 𝕜 ι)
rw₁ rw₂ : Eq (α := EuclideanSpace 𝕜 ι) (EuclideanSpace.single i 1) (EuclideanSpace.single i 1)
⊢ Eq (α := EuclideanSpace 𝕜 ι) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) ((b : (a : ι) → E) i) : EuclideanSpace 𝕜 ι)
    (EuclideanSpace.single i 1 : EuclideanSpace 𝕜 ι)

Tactic:
rw [← b.repr_symm_single i, LinearIsometryEquiv.apply_symm_apply]

Premises used: LinearIsometryEquiv.apply_symm_apply, OrthonormalBasis.repr_symm_single
-- 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
v : E
i : ι
rw :
  ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) v) i =
    HMul.hMul (α := 𝕜) (β := (fun (x : ι) ↦ 𝕜) i) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) 1 : 𝕜)
      (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) v) i : (fun (x : ι) ↦ 𝕜) i)
⊢ ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) v) i = ⟪(b : (a : ι) → E) i, v⟫

Tactic:
rw [← b.repr.inner_map_map (b i) v, b.repr_self i, EuclideanSpace.inner_single_left]

Premises used: EuclideanSpace.inner_single_left, OrthonormalBasis.repr_self, OrthonormalBasis.repr, LinearIsometryEquiv.inner_map_map, DFunLike.coe
-- 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
v : E
i : ι
⊢ ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) v) i =
    HMul.hMul (α := 𝕜) (β := (fun (x : ι) ↦ 𝕜) i) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) 1 : 𝕜)
      (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) v) i : (fun (x : ι) ↦ 𝕜) i)

Tactic:
simp only [one_mul, map_one]

Premises used: map_one, one_mul
-- 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
v : E
i : ι
rw :
  ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) v) i =
    inner 𝕜 (E := EuclideanSpace 𝕜 ι)
      ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) ((b : (a : ι) → E) i) : EuclideanSpace 𝕜 ι)
      ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) v : EuclideanSpace 𝕜 ι)
rw₁ :
  ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) v) i =
    inner 𝕜 (E := EuclideanSpace 𝕜 ι) (EuclideanSpace.single i 1) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) v)
rw₂ rw₃ rw₄ :
  ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) v) i =
    HMul.hMul (α := 𝕜) (β := (fun (x : ι) ↦ 𝕜) i) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) 1 : 𝕜)
      (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) v) i : (fun (x : ι) ↦ 𝕜) i)
⊢ ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) v) i = ⟪(b : (a : ι) → E) i, v⟫

Tactic:
classical
    rw [← b.repr.inner_map_map (b i) v, b.repr_self i, EuclideanSpace.inner_single_left]
    simp only [one_mul, map_one]

Premises used: EuclideanSpace.inner_single_left, OrthonormalBasis.repr, LinearIsometryEquiv.inner_map_map, map_one, DFunLike.coe, one_mul
-- 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
rw :
  ∀ (i j : ι), inner.{u_3, u_4} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((b : (a : ι) → E) j : E) = if i = j then 1 else 0
⊢ Orthonormal.{u_3, u_4, u_1} 𝕜 (E := E) (ι := ι) (⇑b : (a : ι) → E)

Tactic:
rw [orthonormal_iff_ite]

Premises used: orthonormal_iff_ite
-- 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 j : ι
rw :
  inner 𝕜 (E := EuclideanSpace 𝕜 ι) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) ((b : (a : ι) → E) i) : EuclideanSpace 𝕜 ι)
      ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) ((b : (a : ι) → E) j) : EuclideanSpace 𝕜 ι) =
    if i = j then 1 else 0
rw₁ :
  inner 𝕜 (E := EuclideanSpace 𝕜 ι) (EuclideanSpace.single i 1)
      ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) ((b : (a : ι) → E) j)) =
    if i = j then 1 else 0
rw₂ : inner 𝕜 (E := EuclideanSpace 𝕜 ι) (EuclideanSpace.single i 1) (EuclideanSpace.single j 1) = if i = j then 1 else 0
rw₃ :
  HMul.hMul (α := 𝕜) (β := (fun (x : ι) ↦ 𝕜) i) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) 1 : 𝕜)
      (ofLp (EuclideanSpace.single j 1) i : (fun (x : ι) ↦ 𝕜) i) =
    if i = j then 1 else 0
rw₄ :
  HMul.hMul (α := 𝕜) (β := (fun (x : ι) ↦ 𝕜) i) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) 1 : 𝕜) (if i = j then 1 else 0 : 𝕜) =
    if i = j then 1 else 0
rw₅ : HMul.hMul (α := 𝕜) 1 (if i = j then 1 else 0) = if i = j then 1 else 0
rw₆ rw₇ : Eq.{u_3 + 1} (α := 𝕜) (if i = j then 1 else 0) (if i = j then 1 else 0)
⊢ inner.{u_3, u_4} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((b : (a : ι) → E) j : E) = if i = j then 1 else 0

Tactic:
rw [← b.repr.inner_map_map (b i) (b j), b.repr_self i, b.repr_self j,
      EuclideanSpace.inner_single_left, PiLp.single_apply, map_one, one_mul]

Premises used: EuclideanSpace.inner_single_left, OrthonormalBasis.repr_self, OrthonormalBasis.repr, PiLp.single_apply, LinearIsometryEquiv.inner_map_map, map_one, DFunLike.coe, one_mul
-- 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
rw rw₁ rw₂ rw₃ :
  ∀ (i j : ι), inner.{u_3, u_4} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((b : (a : ι) → E) j : E) = if i = j then 1 else 0
⊢ Orthonormal.{u_3, u_4, u_1} 𝕜 (E := E) (ι := ι) (⇑b : (a : ι) → E)

Tactic:
classical
    rw [orthonormal_iff_ite]
    intro i j
    rw [← b.repr.inner_map_map (b i) (b j), b.repr_self i, b.repr_self j,
      EuclideanSpace.inner_single_left, PiLp.single_apply, map_one, one_mul]

Premises used: EuclideanSpace.inner_single_left, PiLp.single_apply, map_one, orthonormal_iff_ite, one_mul
-- 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 : ι
⊢ Norm.norm.{u_4} (E := E) ((b : (a : ι) → E) i : E) = 1

Tactic:
b.orthonormal.norm_eq_one i

Premises used: Orthonormal.norm_eq_one, OrthonormalBasis.orthonormal
-- 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 : ι
⊢ nnnorm.{u_4} (E := E) ((b : (a : ι) → E) i : E) = 1

Tactic:
b.orthonormal.nnnorm_eq_one i

Premises used: Orthonormal.nnnorm_eq_one, OrthonormalBasis.orthonormal
-- 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 : ι
⊢ enorm.{u_4} (E := E) ((b : (a : ι) → E) i : E) = 1

Tactic:
b.orthonormal.enorm_eq_one i

Premises used: OrthonormalBasis.orthonormal, Orthonormal.enorm_eq_one
-- 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 j : ι
hij : i ≠ j
⊢ inner.{u_3, u_4} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((b : (a : ι) → E) j : E) = 0

Tactic:
b.orthonormal.inner_eq_zero hij

Premises used: OrthonormalBasis.orthonormal, Orthonormal.inner_eq_zero
-- 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 : ι
⊢ inner.{u_3, u_4} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((b : (a : ι) → E) i : E) = 1

Tactic:
simp
-- 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 ι
inst_4 : DecidableEq ι
b : OrthonormalBasis ι 𝕜 E
i j : ι
pos :
  ∀ (h : i = j),
    inner.{u_3, u_4} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((b : (a : ι) → E) j : E) = if i = j then 1 else 0
neg :
  ∀ (h : ¬i = j),
    inner.{u_3, u_4} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((b : (a : ι) → E) j : E) = if i = j then 1 else 0
⊢ inner.{u_3, u_4} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((b : (a : ι) → E) j : E) = if i = j then 1 else 0

Tactic:
by_cases h : i = j
-- 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 ι
inst_4 : DecidableEq ι
b : OrthonormalBasis ι 𝕜 E
i j : ι
h : i = j
⊢ inner.{u_3, u_4} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((b : (a : ι) → E) j : E) = if i = j then 1 else 0

Tactic:
simp [h]
-- 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 ι
inst_4 : DecidableEq ι
b : OrthonormalBasis ι 𝕜 E
i j : ι
h : ¬i = j
⊢ inner.{u_3, u_4} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((b : (a : ι) → E) j : E) = if i = j then 1 else 0

Tactic:
simp [h]
-- 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
⊢ Eq (α := (a : ι) → E) (⇑b.toBasis : (a : ι) → E) (⇑b : (a : ι) → E)

Tactic:
rfl

Premises used: PiLp.single, Function.update, Pi.single, dite, 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
⊢ b.toBasis.equivFun = b.repr.toLinearEquiv ≪≫ₗ WithLp.linearEquiv 2 𝕜 (ι → 𝕜)

Tactic:
Basis.equivFun_ofEquivFun _

Premises used: Module.Basis.equivFun_ofEquivFun, OrthonormalBasis.toBasis