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 ι
v : Basis ι 𝕜 E
hv : Orthonormal.{u_3, u_4, u_1} 𝕜 (E := E) (ι := ι) (⇑v : (a : ι) → E)
x y : E
p : EuclideanSpace 𝕜 ι := toLp 2 ((v.equivFun : (a : E) → ι → 𝕜) x)
q : EuclideanSpace 𝕜 ι := toLp 2 ((v.equivFun : (a : E) → ι → 𝕜) y)
key :
  ⟪p, q⟫ =
    inner.{u_3, u_4} 𝕜 (E := E) (∑ i : ι, HSMul.hSMul (β := E) (p.ofLp i) ((v : (a : ι) → E) i : E))
      (∑ i : ι, HSMul.hSMul (β := E) (q.ofLp i) ((v : (a : ι) → E) i : E))
⊢ y = ∑ i : ι, HSMul.hSMul (β := E) (q.ofLp i) ((v : (a : ι) → E) i : E)
have h : Eq.{u_4 + 1} (α := E) ((v.equivFun.symm : (a : ι → 𝕜) → E) ((v.equivFun : (a : E) → ι → 𝕜) y : ι → 𝕜) : E)
  (∑ i : ι, HSMul.hSMul (β := E) (q.ofLp i) ((v : (a : ι) → E) i : E) : E)
Tactic: rw [← v.equivFun.symm_apply_apply y, v.equivFun_symm_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 ι
v : Basis ι 𝕜 E
hv : Orthonormal.{u_3, u_4, u_1} 𝕜 (E := E) (ι := ι) (⇑v : (a : ι) → E)
x y : E
p : EuclideanSpace 𝕜 ι := toLp 2 ((v.equivFun : (a : E) → ι → 𝕜) x)
q : EuclideanSpace 𝕜 ι := toLp 2 ((v.equivFun : (a : E) → ι → 𝕜) y)
key :
  ⟪p, q⟫ =
    inner.{u_3, u_4} 𝕜 (E := E) (∑ i : ι, HSMul.hSMul (β := E) (p.ofLp i) ((v : (a : ι) → E) i : E))
      (∑ i : ι, HSMul.hSMul (β := E) (q.ofLp i) ((v : (a : ι) → E) i : E))
h :
  Eq.{u_4 + 1} (α := E) ((v.equivFun.symm : (a : ι → 𝕜) → E) ((v.equivFun : (a : E) → ι → 𝕜) y : ι → 𝕜) : E)
    (∑ i : ι, HSMul.hSMul (β := E) (q.ofLp i) ((v : (a : ι) → E) i : E) : E)
⊢ y = ∑ i : ι, HSMul.hSMul (β := E) (q.ofLp i) ((v : (a : ι) → E) i : E)
have h₁ : Eq.{u_4 + 1} (α := E)
  (∑ i : ι,
    HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (β := E) ((v.equivFun : (a : E) → ι → 𝕜) y i : 𝕜) ((v : (a : ι) → E) i : E))
  (∑ i : ι, HSMul.hSMul (β := E) (q.ofLp i) ((v : (a : ι) → E) i : E))
Tactic: rw [← v.equivFun.symm_apply_apply y, v.equivFun_symm_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 ι
v : Basis ι 𝕜 E
hv : Orthonormal.{u_3, u_4, u_1} 𝕜 (E := E) (ι := ι) (⇑v : (a : ι) → E)
⊢ OrthonormalBasis.toBasis (v.toOrthonormalBasis hv) = v
have simp : Basis.ofEquivFun
    (LinearEquiv.trans (M₂ := EuclideanSpace 𝕜 ι) (module_M₂ := WithLp.instModule 2 𝕜 ((i : ι) → 𝕜)) (σ₂₃ :=
      RingHom.id 𝕜) (σ₃₂ := RingHom.id 𝕜) (re₁₂ := sorry) (re₂₃ := sorry) (re₂₁ := sorry) (re₃₂ := sorry)
      (v.equivFun.trans (σ₂₃ := RingHom.id 𝕜) (σ₃₂ := RingHom.id 𝕜) (re₂₃ := sorry) (re₃₂ := sorry)
        (LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (ι → 𝕜))))
      (WithLp.linearEquiv 2 𝕜 (ι → 𝕜))) =
  v
Tactic: simp only [OrthonormalBasis.toBasis, Basis.toOrthonormalBasis,
    LinearEquiv.isometryOfInner_toLinearEquiv]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
v : Basis ι 𝕜 E
hv : Orthonormal.{u_3, u_4, u_1} 𝕜 (E := E) (ι := ι) (⇑v : (a : ι) → E)
⊢ Eq (α := (a : ι) → E) (⇑(v.toOrthonormalBasis hv) : (a : ι) → E)
    (⇑(OrthonormalBasis.toBasis (v.toOrthonormalBasis hv)) : (a : ι) → E)
have rw : Eq (α := (a : ι) → E) (⇑(v.toOrthonormalBasis hv) : (a : ι) → E) (⇑(v.toOrthonormalBasis hv) : (a : ι) → E)
Tactic: rw [OrthonormalBasis.coe_toBasis]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
v : Basis ι 𝕜 E
hv : Orthonormal.{u_3, u_4, u_1} 𝕜 (E := E) (ι := ι) (⇑v : (a : ι) → E)
⊢ Eq (α := (a : ι) → E) (⇑(v.toOrthonormalBasis hv) : (a : ι) → E)
    (⇑(OrthonormalBasis.toBasis (v.toOrthonormalBasis hv)) : (a : ι) → E)
have classical : Eq (α := (a : ι) → E) (⇑(v.toOrthonormalBasis hv) : (a : ι) → E) (⇑(v.toOrthonormalBasis hv) : (a : ι) → E)
Tactic: classical rw [OrthonormalBasis.coe_toBasis]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_7
𝕜 : Type u_8
inst : Unique ι
inst_1 : RCLike 𝕜
⊢ Eq (α := (a : ι) → 𝕜) (⇑(OrthonormalBasis.singleton ι 𝕜) : (a : ι) → 𝕜) 1
have h : ∀ (x : ι), Eq.{u_8 + 1} (α := 𝕜) ((OrthonormalBasis.singleton ι 𝕜 : (a : ι) → 𝕜) x : 𝕜) (1 x : 𝕜)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
η : Type u_7
inst : Fintype η
ι : η → Type u_8
inst_1 : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst_2 : RCLike 𝕜
E : η → Type u_10
inst_3 : (i : η) → NormedAddCommGroup (E i)
inst_4 : (i : η) → InnerProductSpace.{u_9, u_10} 𝕜 (E i)
B : (i : η) → OrthonormalBasis.{u_8, u_9, u_10} (ι i) 𝕜 (E i)
⊢ Eq (α := Basis ((i : η) × ι i) 𝕜 (PiLp 2 E)) (OrthonormalBasis.toBasis (Pi.orthonormalBasis (ι := ι) (E := E) B))
    (Basis.map (M := (j : η) → E j) (Pi.basis (ιs := ι) (Ms := E) fun (i : η) ↦ (B i).toBasis)
      (LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 ((j : η) → E j))))
have a : ∀ (i : (i : η) × ι i) (i_1 : η),
  Eq.{u_10 + 1} (α := E i_1)
    (ofLp (p := 2)
      ((OrthonormalBasis.toBasis (Pi.orthonormalBasis (ι := ι) (E := E) B) : (a : (i : η) × ι i) → PiLp 2 E) i) i_1)
    (ofLp (p := 2)
      ((Basis.map (M := (j : η) → E j) (Pi.basis (ιs := ι) (Ms := E) fun (i : η) ↦ (B i).toBasis)
            (LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 ((j : η) → E j))) :
          (a : (i : η) × ι i) → PiLp 2 E)
        i)
      i_1)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
η : Type u_7
inst : Fintype η
inst_1 : DecidableEq η
ι : η → Type u_8
inst_2 : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst_3 : RCLike 𝕜
E : η → Type u_10
inst_4 : (i : η) → NormedAddCommGroup (E i)
inst_5 : (i : η) → InnerProductSpace.{u_9, u_10} 𝕜 (E i)
B : (i : η) → OrthonormalBasis.{u_8, u_9, u_10} (ι i) 𝕜 (E i)
j : (i : η) × ι i
⊢ Eq (α := PiLp 2 E) ((Pi.orthonormalBasis (ι := ι) (E := E) B : (a : (i : η) × ι i) → PiLp 2 E) j : PiLp 2 E)
    (PiLp.single 2 (β := E) (j.fst (β := fun (i : η) ↦ ι i))
        ((B (j.fst (β := fun (i : η) ↦ ι i)) : (a : ι j.fst) → E j.fst) (j.snd (β := fun (i : η) ↦ ι i))) :
      PiLp 2 E)
have h : ∀ (k : η),
  Eq.{u_10 + 1} (α := E k)
    (ofLp (p := 2) ((Pi.orthonormalBasis (ι := ι) (E := E) B : (a : (i : η) × ι i) → PiLp 2 E) j) k : E k)
    (ofLp (p := 2)
        (PiLp.single 2 (β := E) (j.fst (β := fun (i : η) ↦ ι i))
          ((B (j.fst (β := fun (i : η) ↦ ι i)) : (a : ι j.fst) → E j.fst) (j.snd (β := fun (i : η) ↦ ι i))))
        k :
      E k)
Tactic: ext k
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
η : Type u_7
inst : Fintype η
inst_1 : DecidableEq η
ι : η → Type u_8
inst_2 : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst_3 : RCLike 𝕜
E : η → Type u_10
inst_4 : (i : η) → NormedAddCommGroup (E i)
inst_5 : (i : η) → InnerProductSpace.{u_9, u_10} 𝕜 (E i)
B : (i : η) → OrthonormalBasis.{u_8, u_9, u_10} (ι i) 𝕜 (E i)
j : (i : η) × ι i
k : η
⊢ Eq.{u_10 + 1} (α := E k)
    (ofLp (p := 2) ((Pi.orthonormalBasis (ι := ι) (E := E) B : (a : (i : η) × ι i) → PiLp 2 E) j) k : E k)
    (ofLp (p := 2)
        (PiLp.single 2 (β := E) (j.fst (β := fun (i : η) ↦ ι i))
          ((B (j.fst (β := fun (i : η) ↦ ι i)) : (a : ι j.fst) → E j.fst) (j.snd (β := fun (i : η) ↦ ι i))))
        k :
      E k)
have h : ∀ (i : η) (j : ι i),
  Eq.{u_10 + 1} (α := E k)
    (ofLp (p := 2)
        ((Pi.orthonormalBasis (ι := ι) (E := E) B : (a : (i : η) × ι i) → PiLp 2 E)
          (Sigma.mk (β := fun (i : η) ↦ ι i) i j))
        k :
      E k)
    (ofLp (p := 2)
        (PiLp.single 2 (β := E) ((Sigma.mk (β := fun (i : η) ↦ ι i) i j).fst (β := fun (i : η) ↦ ι i))
          ((B ((Sigma.mk (β := fun (i : η) ↦ ι i) i j).fst (β := fun (i : η) ↦ ι i)) :
              (a : ι ⟨i, j⟩.fst) → E ⟨i, j⟩.fst)
            ((Sigma.mk (β := fun (i : η) ↦ ι i) i j).snd (β := fun (i : η) ↦ ι i))))
        k :
      E k)
Tactic: obtain ⟨i, j⟩ := j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
η : Type u_7
inst : Fintype η
inst_1 : DecidableEq η
ι : η → Type u_8
inst_2 : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst_3 : RCLike 𝕜
E : η → Type u_10
inst_4 : (i : η) → NormedAddCommGroup (E i)
inst_5 : (i : η) → InnerProductSpace.{u_9, u_10} 𝕜 (E i)
B : (i : η) → OrthonormalBasis.{u_8, u_9, u_10} (ι i) 𝕜 (E i)
k i : η
j : ι i
⊢ Eq.{u_10 + 1} (α := E k)
    (ofLp (p := 2)
        ((Pi.orthonormalBasis (ι := ι) (E := E) B : (a : (i : η) × ι i) → PiLp 2 E)
          (Sigma.mk (β := fun (i : η) ↦ ι i) i j))
        k :
      E k)
    (ofLp (p := 2)
        (PiLp.single 2 (β := E) ((Sigma.mk (β := fun (i : η) ↦ ι i) i j).fst (β := fun (i : η) ↦ ι i))
          ((B ((Sigma.mk (β := fun (i : η) ↦ ι i) i j).fst (β := fun (i : η) ↦ ι i)) :
              (a : ι ⟨i, j⟩.fst) → E ⟨i, j⟩.fst)
            ((Sigma.mk (β := fun (i : η) ↦ ι i) i j).snd (β := fun (i : η) ↦ ι i))))
        k :
      E k)
have h : Eq.{u_10 + 1} (α := E k)
  (((B k).repr.symm : (a : EuclideanSpace 𝕜 (ι k)) → E k)
      (toLp 2 (Pi.single (M := fun (j : η) ↦ (y : ι j) → 𝕜) i (Pi.single (M := fun (x : ι i) ↦ 𝕜) j 1) k)) :
    E k)
  (Pi.single (M := E) i ((B i : (a : ι i) → E i) j) k : E k)
Tactic: simp only [Pi.orthonormalBasis, coe_ofRepr, LinearIsometryEquiv.symm_trans,
    LinearIsometryEquiv.symm_symm, LinearIsometryEquiv.piLpCongrRight_symm,
    LinearIsometryEquiv.trans_apply, LinearIsometryEquiv.piLpCongrRight_apply,
    LinearIsometryEquiv.piLpCurry_apply, PiLp.ofLp_single, PiLp.toLp_apply,
    Sigma.curry_single (γ := fun _ _ => 𝕜)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
η : Type u_7
inst : Fintype η
inst_1 : DecidableEq η
ι : η → Type u_8
inst_2 : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst_3 : RCLike 𝕜
E : η → Type u_10
inst_4 : (i : η) → NormedAddCommGroup (E i)
inst_5 : (i : η) → InnerProductSpace.{u_9, u_10} 𝕜 (E i)
B : (i : η) → OrthonormalBasis.{u_8, u_9, u_10} (ι i) 𝕜 (E i)
k i : η
j : ι i
⊢ Eq.{u_10 + 1} (α := E k)
    (((B k).repr.symm : (a : EuclideanSpace 𝕜 (ι k)) → E k)
        (toLp 2 (Pi.single (M := fun (j : η) ↦ (y : ι j) → 𝕜) i (Pi.single (M := fun (x : ι i) ↦ 𝕜) j 1) k)) :
      E k)
    (Pi.single (M := E) i ((B i : (a : ι i) → E i) j) k : E k)
have h : Eq.{u_10 + 1} (α := E i)
  (((B i).repr.symm : (a : EuclideanSpace 𝕜 (ι i)) → E i)
      (toLp 2 (Pi.single (M := fun (j : η) ↦ (y : ι j) → 𝕜) i (Pi.single (M := fun (x : ι i) ↦ 𝕜) j 1) i)) :
    E i)
  (Pi.single (M := E) i ((B i : (a : ι i) → E i) j) i : E i)
Tactic: obtain rfl | hi := Decidable.eq_or_ne i k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
η : Type u_7
inst : Fintype η
inst_1 : DecidableEq η
ι : η → Type u_8
inst_2 : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst_3 : RCLike 𝕜
E : η → Type u_10
inst_4 : (i : η) → NormedAddCommGroup (E i)
inst_5 : (i : η) → InnerProductSpace.{u_9, u_10} 𝕜 (E i)
B : (i : η) → OrthonormalBasis.{u_8, u_9, u_10} (ι i) 𝕜 (E i)
k i : η
j : ι i
h :
  Eq.{u_10 + 1} (α := E i)
    (((B i).repr.symm : (a : EuclideanSpace 𝕜 (ι i)) → E i)
        (toLp 2 (Pi.single (M := fun (j : η) ↦ (y : ι j) → 𝕜) i (Pi.single (M := fun (x : ι i) ↦ 𝕜) j 1) i)) :
      E i)
    (Pi.single (M := E) i ((B i : (a : ι i) → E i) j) i : E i)
⊢ Eq.{u_10 + 1} (α := E k)
    (((B k).repr.symm : (a : EuclideanSpace 𝕜 (ι k)) → E k)
        (toLp 2 (Pi.single (M := fun (j : η) ↦ (y : ι j) → 𝕜) i (Pi.single (M := fun (x : ι i) ↦ 𝕜) j 1) k)) :
      E k)
    (Pi.single (M := E) i ((B i : (a : ι i) → E i) j) k : E k)
have h₁ : ∀ (hi : i ≠ k),
  Eq.{u_10 + 1} (α := E k)
    (((B k).repr.symm : (a : EuclideanSpace 𝕜 (ι k)) → E k)
        (toLp 2 (Pi.single (M := fun (j : η) ↦ (y : ι j) → 𝕜) i (Pi.single (M := fun (x : ι i) ↦ 𝕜) j 1) k)) :
      E k)
    (Pi.single (M := E) i ((B i : (a : ι i) → E i) j) k : E k)
Tactic: obtain rfl | hi := Decidable.eq_or_ne i k
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
η : Type u_7
inst : Fintype η
inst_1 : DecidableEq η
ι : η → Type u_8
inst_2 : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst_3 : RCLike 𝕜
E : η → Type u_10
inst_4 : (i : η) → NormedAddCommGroup (E i)
inst_5 : (i : η) → InnerProductSpace.{u_9, u_10} 𝕜 (E i)
B : (i : η) → OrthonormalBasis.{u_8, u_9, u_10} (ι i) 𝕜 (E i)
j : (i : η) × ι i
⊢ Eq (α := PiLp 2 E) ((Pi.orthonormalBasis (ι := ι) (E := E) B : (a : (i : η) × ι i) → PiLp 2 E) j : PiLp 2 E)
    (PiLp.single 2 (β := E) (j.fst (β := fun (i : η) ↦ ι i))
        ((B (j.fst (β := fun (i : η) ↦ ι i)) : (a : ι j.fst) → E j.fst) (j.snd (β := fun (i : η) ↦ ι i))) :
      PiLp 2 E)
have h : ∀ (k : η),
  Eq.{u_10 + 1} (α := E k)
    (ofLp (p := 2) ((Pi.orthonormalBasis (ι := ι) (E := E) B : (a : (i : η) × ι i) → PiLp 2 E) j) k : E k)
    (ofLp (p := 2)
        (PiLp.single 2 (β := E) (j.fst (β := fun (i : η) ↦ ι i))
          ((B (j.fst (β := fun (i : η) ↦ ι i)) : (a : ι j.fst) → E j.fst) (j.snd (β := fun (i : η) ↦ ι i))))
        k :
      E k)
Tactic: classical
  ext k
  obtain ⟨i, j⟩ := j
  simp only [Pi.orthonormalBasis, coe_ofRepr, LinearIsometryEquiv.symm_trans,
    LinearIsometryEquiv.symm_symm, LinearIsometryEquiv.piLpCongrRight_symm,
    LinearIsometryEquiv.trans_apply, LinearIsometryEquiv.piLpCongrRight_apply,
    LinearIsometryEquiv.piLpCurry_apply, PiLp.ofLp_single, PiLp.toLp_apply,
    Sigma.curry_single (γ := fun _ _ => 𝕜)]
  obtain rfl | hi := Decidable.eq_or_ne i k
  · simp
  · simp [hi]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
η : Type u_7
inst : Fintype η
inst_1 : DecidableEq η
ι : η → Type u_8
inst_2 : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst_3 : RCLike 𝕜
E : η → Type u_10
inst_4 : (i : η) → NormedAddCommGroup (E i)
inst_5 : (i : η) → InnerProductSpace.{u_9, u_10} 𝕜 (E i)
B : (i : η) → OrthonormalBasis.{u_8, u_9, u_10} (ι i) 𝕜 (E i)
j : (i : η) × ι i
h :
  ∀ (k : η),
    Eq.{u_10 + 1} (α := E k)
      (ofLp (p := 2) ((Pi.orthonormalBasis (ι := ι) (E := E) B : (a : (i : η) × ι i) → PiLp 2 E) j) k : E k)
      (ofLp (p := 2)
          (PiLp.single 2 (β := E) (j.fst (β := fun (i : η) ↦ ι i))
            ((B (j.fst (β := fun (i : η) ↦ ι i)) : (a : ι j.fst) → E j.fst) (j.snd (β := fun (i : η) ↦ ι i))))
          k :
        E k)
⊢ Eq (α := PiLp 2 E) ((Pi.orthonormalBasis (ι := ι) (E := E) B : (a : (i : η) × ι i) → PiLp 2 E) j : PiLp 2 E)
    (PiLp.single 2 (β := E) (j.fst (β := fun (i : η) ↦ ι i))
        ((B (j.fst (β := fun (i : η) ↦ ι i)) : (a : ι j.fst) → E j.fst) (j.snd (β := fun (i : η) ↦ ι i))) :
      PiLp 2 E)
have h₁ : ∀ (k i : η) (j : ι i),
  Eq.{u_10 + 1} (α := E k)
    (ofLp (p := 2)
        ((Pi.orthonormalBasis (ι := ι) (E := E) B : (a : (i : η) × ι i) → PiLp 2 E)
          (Sigma.mk (β := fun (i : η) ↦ ι i) i j))
        k :
      E k)
    (ofLp (p := 2)
        (PiLp.single 2 (β := E) ((Sigma.mk (β := fun (i : η) ↦ ι i) i j).fst (β := fun (i : η) ↦ ι i))
          ((B ((Sigma.mk (β := fun (i : η) ↦ ι i) i j).fst (β := fun (i : η) ↦ ι i)) :
              (a : ι ⟨i, j⟩.fst) → E ⟨i, j⟩.fst)
            ((Sigma.mk (β := fun (i : η) ↦ ι i) i j).snd (β := fun (i : η) ↦ ι i))))
        k :
      E k)
Tactic: classical
  ext k
  obtain ⟨i, j⟩ := j
  simp only [Pi.orthonormalBasis, coe_ofRepr, LinearIsometryEquiv.symm_trans,
    LinearIsometryEquiv.symm_symm, LinearIsometryEquiv.piLpCongrRight_symm,
    LinearIsometryEquiv.trans_apply, LinearIsometryEquiv.piLpCongrRight_apply,
    LinearIsometryEquiv.piLpCurry_apply, PiLp.ofLp_single, PiLp.toLp_apply,
    Sigma.curry_single (γ := fun _ _ => 𝕜)]
  obtain rfl | hi := Decidable.eq_or_ne i k
  · simp
  · simp [hi]
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
η : Type u_7
inst : Fintype η
inst_1 : DecidableEq η
ι : η → Type u_8
inst_2 : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst_3 : RCLike 𝕜
E : η → Type u_10
inst_4 : (i : η) → NormedAddCommGroup (E i)
inst_5 : (i : η) → InnerProductSpace.{u_9, u_10} 𝕜 (E i)
B : (i : η) → OrthonormalBasis.{u_8, u_9, u_10} (ι i) 𝕜 (E i)
j : (i : η) × ι i
h :
  ∀ (k : η),
    Eq.{u_10 + 1} (α := E k)
      (ofLp (p := 2) ((Pi.orthonormalBasis (ι := ι) (E := E) B : (a : (i : η) × ι i) → PiLp 2 E) j) k : E k)
      (ofLp (p := 2)
          (PiLp.single 2 (β := E) (j.fst (β := fun (i : η) ↦ ι i))
            ((B (j.fst (β := fun (i : η) ↦ ι i)) : (a : ι j.fst) → E j.fst) (j.snd (β := fun (i : η) ↦ ι i))))
          k :
        E k)
h₁ :
  ∀ (k i : η) (j : ι i),
    Eq.{u_10 + 1} (α := E k)
      (ofLp (p := 2)
          ((Pi.orthonormalBasis (ι := ι) (E := E) B : (a : (i : η) × ι i) → PiLp 2 E)
            (Sigma.mk (β := fun (i : η) ↦ ι i) i j))
          k :
        E k)
      (ofLp (p := 2)
          (PiLp.single 2 (β := E) ((Sigma.mk (β := fun (i : η) ↦ ι i) i j).fst (β := fun (i : η) ↦ ι i))
            ((B ((Sigma.mk (β := fun (i : η) ↦ ι i) i j).fst (β := fun (i : η) ↦ ι i)) :
                (a : ι ⟨i, j⟩.fst) → E ⟨i, j⟩.fst)
              ((Sigma.mk (β := fun (i : η) ↦ ι i) i j).snd (β := fun (i : η) ↦ ι i))))
          k :
        E k)
⊢ Eq (α := PiLp 2 E) ((Pi.orthonormalBasis (ι := ι) (E := E) B : (a : (i : η) × ι i) → PiLp 2 E) j : PiLp 2 E)
    (PiLp.single 2 (β := E) (j.fst (β := fun (i : η) ↦ ι i))
        ((B (j.fst (β := fun (i : η) ↦ ι i)) : (a : ι j.fst) → E j.fst) (j.snd (β := fun (i : η) ↦ ι i))) :
      PiLp 2 E)
have h₂ : ∀ (k i : η) (j : ι i),
  Eq.{u_10 + 1} (α := E k)
    (((B k).repr.symm : (a : EuclideanSpace 𝕜 (ι k)) → E k)
        (toLp 2 (Pi.single (M := fun (j : η) ↦ (y : ι j) → 𝕜) i (Pi.single (M := fun (x : ι i) ↦ 𝕜) j 1) k)) :
      E k)
    (Pi.single (M := E) i ((B i : (a : ι i) → E i) j) k : E k)
Tactic: classical
  ext k
  obtain ⟨i, j⟩ := j
  simp only [Pi.orthonormalBasis, coe_ofRepr, LinearIsometryEquiv.symm_trans,
    LinearIsometryEquiv.symm_symm, LinearIsometryEquiv.piLpCongrRight_symm,
    LinearIsometryEquiv.trans_apply, LinearIsometryEquiv.piLpCongrRight_apply,
    LinearIsometryEquiv.piLpCurry_apply, PiLp.ofLp_single, PiLp.toLp_apply,
    Sigma.curry_single (γ := fun _ _ => 𝕜)]
  obtain rfl | hi := Decidable.eq_or_ne i k
  · simp
  · simp [hi]
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
η : Type u_7
inst : Fintype η
inst_1 : DecidableEq η
ι : η → Type u_8
inst_2 : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst_3 : RCLike 𝕜
E : η → Type u_10
inst_4 : (i : η) → NormedAddCommGroup (E i)
inst_5 : (i : η) → InnerProductSpace.{u_9, u_10} 𝕜 (E i)
B : (i : η) → OrthonormalBasis.{u_8, u_9, u_10} (ι i) 𝕜 (E i)
j : (i : η) × ι i
h :
  ∀ (k : η),
    Eq.{u_10 + 1} (α := E k)
      (ofLp (p := 2) ((Pi.orthonormalBasis (ι := ι) (E := E) B : (a : (i : η) × ι i) → PiLp 2 E) j) k : E k)
      (ofLp (p := 2)
          (PiLp.single 2 (β := E) (j.fst (β := fun (i : η) ↦ ι i))
            ((B (j.fst (β := fun (i : η) ↦ ι i)) : (a : ι j.fst) → E j.fst) (j.snd (β := fun (i : η) ↦ ι i))))
          k :
        E k)
h₁ :
  ∀ (k i : η) (j : ι i),
    Eq.{u_10 + 1} (α := E k)
      (ofLp (p := 2)
          ((Pi.orthonormalBasis (ι := ι) (E := E) B : (a : (i : η) × ι i) → PiLp 2 E)
            (Sigma.mk (β := fun (i : η) ↦ ι i) i j))
          k :
        E k)
      (ofLp (p := 2)
          (PiLp.single 2 (β := E) ((Sigma.mk (β := fun (i : η) ↦ ι i) i j).fst (β := fun (i : η) ↦ ι i))
            ((B ((Sigma.mk (β := fun (i : η) ↦ ι i) i j).fst (β := fun (i : η) ↦ ι i)) :
                (a : ι ⟨i, j⟩.fst) → E ⟨i, j⟩.fst)
              ((Sigma.mk (β := fun (i : η) ↦ ι i) i j).snd (β := fun (i : η) ↦ ι i))))
          k :
        E k)
h₂ :
  ∀ (k i : η) (j : ι i),
    Eq.{u_10 + 1} (α := E k)
      (((B k).repr.symm : (a : EuclideanSpace 𝕜 (ι k)) → E k)
          (toLp 2 (Pi.single (M := fun (j : η) ↦ (y : ι j) → 𝕜) i (Pi.single (M := fun (x : ι i) ↦ 𝕜) j 1) k)) :
        E k)
      (Pi.single (M := E) i ((B i : (a : ι i) → E i) j) k : E k)
⊢ Eq (α := PiLp 2 E) ((Pi.orthonormalBasis (ι := ι) (E := E) B : (a : (i : η) × ι i) → PiLp 2 E) j : PiLp 2 E)
    (PiLp.single 2 (β := E) (j.fst (β := fun (i : η) ↦ ι i))
        ((B (j.fst (β := fun (i : η) ↦ ι i)) : (a : ι j.fst) → E j.fst) (j.snd (β := fun (i : η) ↦ ι i))) :
      PiLp 2 E)
have h₃ : ∀ (i : η) (j : ι i),
  Eq.{u_10 + 1} (α := E i)
    (((B i).repr.symm : (a : EuclideanSpace 𝕜 (ι i)) → E i)
        (toLp 2 (Pi.single (M := fun (j : η) ↦ (y : ι j) → 𝕜) i (Pi.single (M := fun (x : ι i) ↦ 𝕜) j 1) i)) :
      E i)
    (Pi.single (M := E) i ((B i : (a : ι i) → E i) j) i : E i)
Tactic: classical
  ext k
  obtain ⟨i, j⟩ := j
  simp only [Pi.orthonormalBasis, coe_ofRepr, LinearIsometryEquiv.symm_trans,
    LinearIsometryEquiv.symm_symm, LinearIsometryEquiv.piLpCongrRight_symm,
    LinearIsometryEquiv.trans_apply, LinearIsometryEquiv.piLpCongrRight_apply,
    LinearIsometryEquiv.piLpCurry_apply, PiLp.ofLp_single, PiLp.toLp_apply,
    Sigma.curry_single (γ := fun _ _ => 𝕜)]
  obtain rfl | hi := Decidable.eq_or_ne i k
  · simp
  · simp [hi]
Cleared hypotheses: j