-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem _root_.Pi.orthonormalBasis_apply {η : Type*} [Fintype η] [DecidableEq η] {ι : η → Type*}
    [∀ i, Fintype (ι i)] {𝕜 : Type*} [RCLike 𝕜] {E : η → Type*} [∀ i, NormedAddCommGroup (E i)]
    [∀ i, InnerProductSpace 𝕜 (E i)] (B : ∀ i, OrthonormalBasis (ι i) 𝕜 (E i))
    (j : (i : η) × (ι i)) :
    Pi.orthonormalBasis B j = (WithLp.equiv _ _).symm (Pi.single _ (B j.fst j.snd))

Proof state:
case h.mk
η : Type u_7
inst✝⁵ : Fintype η
inst✝⁴ : DecidableEq η
ι : η → Type u_8
inst✝³ : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst✝² : RCLike 𝕜
E : η → Type u_10
inst✝¹ : (i : η) → NormedAddCommGroup (E i)
inst✝ : (i : η) → InnerProductSpace 𝕜 (E i)
B : (i : η) → OrthonormalBasis (ι i) 𝕜 (E i)
k i : η
j : ι i
⊢ (Pi.orthonormalBasis B) ⟨i, j⟩ k =
    (WithLp.equiv 2 ((j : η) → E j)).symm (Pi.single ⟨i, j⟩.fst ((B ⟨i, j⟩.fst) ⟨i, j⟩.snd)) 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, WithLp.equiv_single, WithLp.equiv_symm_pi_apply,
  Sigma.curry_single (γ := fun _ _ => 𝕜)]

Result:
case h.mk
η : Type u_7
inst✝⁵ : Fintype η
inst✝⁴ : DecidableEq η
ι : η → Type u_8
inst✝³ : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst✝² : RCLike 𝕜
E : η → Type u_10
inst✝¹ : (i : η) → NormedAddCommGroup (E i)
inst✝ : (i : η) → InnerProductSpace 𝕜 (E i)
B : (i : η) → OrthonormalBasis (ι i) 𝕜 (E i)
k i : η
j : ι i
⊢ (B k).repr.symm ((WithLp.equiv 2 (ι k → 𝕜)).symm (Pi.single i (Pi.single j 1) k)) = Pi.single i ((B i) j) k

Proof state:
case h.mk.inr
η : Type u_7
inst✝⁵ : Fintype η
inst✝⁴ : DecidableEq η
ι : η → Type u_8
inst✝³ : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst✝² : RCLike 𝕜
E : η → Type u_10
inst✝¹ : (i : η) → NormedAddCommGroup (E i)
inst✝ : (i : η) → InnerProductSpace 𝕜 (E i)
B : (i : η) → OrthonormalBasis (ι i) 𝕜 (E i)
k i : η
j : ι i
hi : i ≠ k
⊢ (B k).repr.symm ((WithLp.equiv 2 (ι k → 𝕜)).symm (Pi.single i (Pi.single j 1) k)) = Pi.single i ((B i) j) k

Tactic:
simp only [Pi.single_eq_of_ne' hi, WithLp.equiv_symm_zero, _root_.map_zero]

Result:
no goals

Proof state:
η : Type u_7
inst✝⁵ : Fintype η
inst✝⁴ : DecidableEq η
ι : η → Type u_8
inst✝³ : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst✝² : RCLike 𝕜
E : η → Type u_10
inst✝¹ : (i : η) → NormedAddCommGroup (E i)
inst✝ : (i : η) → InnerProductSpace 𝕜 (E i)
B : (i : η) → OrthonormalBasis (ι i) 𝕜 (E i)
j : (i : η) × ι i
⊢ (Pi.orthonormalBasis B) j = (WithLp.equiv 2 ((j : η) → E j)).symm (Pi.single j.fst ((B j.fst) j.snd))

Tactic:
ext k

Result:
case h
η : Type u_7
inst✝⁵ : Fintype η
inst✝⁴ : DecidableEq η
ι : η → Type u_8
inst✝³ : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst✝² : RCLike 𝕜
E : η → Type u_10
inst✝¹ : (i : η) → NormedAddCommGroup (E i)
inst✝ : (i : η) → InnerProductSpace 𝕜 (E i)
B : (i : η) → OrthonormalBasis (ι i) 𝕜 (E i)
j : (i : η) × ι i
k : η
⊢ (Pi.orthonormalBasis B) j k = (WithLp.equiv 2 ((j : η) → E j)).symm (Pi.single j.fst ((B j.fst) j.snd)) k

Proof state:
case h
η : Type u_7
inst✝⁵ : Fintype η
inst✝⁴ : DecidableEq η
ι : η → Type u_8
inst✝³ : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst✝² : RCLike 𝕜
E : η → Type u_10
inst✝¹ : (i : η) → NormedAddCommGroup (E i)
inst✝ : (i : η) → InnerProductSpace 𝕜 (E i)
B : (i : η) → OrthonormalBasis (ι i) 𝕜 (E i)
j : (i : η) × ι i
k : η
⊢ (Pi.orthonormalBasis B) j k = (WithLp.equiv 2 ((j : η) → E j)).symm (Pi.single j.fst ((B j.fst) j.snd)) k

Tactic:
obtain ⟨i, j⟩ := j

Result:
case h.mk
η : Type u_7
inst✝⁵ : Fintype η
inst✝⁴ : DecidableEq η
ι : η → Type u_8
inst✝³ : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst✝² : RCLike 𝕜
E : η → Type u_10
inst✝¹ : (i : η) → NormedAddCommGroup (E i)
inst✝ : (i : η) → InnerProductSpace 𝕜 (E i)
B : (i : η) → OrthonormalBasis (ι i) 𝕜 (E i)
k i : η
j : ι i
⊢ (Pi.orthonormalBasis B) ⟨i, j⟩ k =
    (WithLp.equiv 2 ((j : η) → E j)).symm (Pi.single ⟨i, j⟩.fst ((B ⟨i, j⟩.fst) ⟨i, j⟩.snd)) k

Proof state:
case h.mk.inl
η : Type u_7
inst✝⁵ : Fintype η
inst✝⁴ : DecidableEq η
ι : η → Type u_8
inst✝³ : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst✝² : RCLike 𝕜
E : η → Type u_10
inst✝¹ : (i : η) → NormedAddCommGroup (E i)
inst✝ : (i : η) → InnerProductSpace 𝕜 (E i)
B : (i : η) → OrthonormalBasis (ι i) 𝕜 (E i)
i : η
j : ι i
⊢ (B i).repr.symm ((WithLp.equiv 2 (ι i → 𝕜)).symm (Pi.single i (Pi.single j 1) i)) = Pi.single i ((B i) j) i

Tactic:
simp only [Pi.single_eq_same, WithLp.equiv_symm_single, OrthonormalBasis.repr_symm_single]

Result:
no goals

Proof state:
case h.mk
η : Type u_7
inst✝⁵ : Fintype η
inst✝⁴ : DecidableEq η
ι : η → Type u_8
inst✝³ : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst✝² : RCLike 𝕜
E : η → Type u_10
inst✝¹ : (i : η) → NormedAddCommGroup (E i)
inst✝ : (i : η) → InnerProductSpace 𝕜 (E i)
B : (i : η) → OrthonormalBasis (ι i) 𝕜 (E i)
k i : η
j : ι i
⊢ (B k).repr.symm ((WithLp.equiv 2 (ι k → 𝕜)).symm (Pi.single i (Pi.single j 1) k)) = Pi.single i ((B i) j) k

Tactic:
obtain rfl | hi := Decidable.eq_or_ne i k

Result:
case h.mk.inl
η : Type u_7
inst✝⁵ : Fintype η
inst✝⁴ : DecidableEq η
ι : η → Type u_8
inst✝³ : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst✝² : RCLike 𝕜
E : η → Type u_10
inst✝¹ : (i : η) → NormedAddCommGroup (E i)
inst✝ : (i : η) → InnerProductSpace 𝕜 (E i)
B : (i : η) → OrthonormalBasis (ι i) 𝕜 (E i)
i : η
j : ι i
⊢ (B i).repr.symm ((WithLp.equiv 2 (ι i → 𝕜)).symm (Pi.single i (Pi.single j 1) i)) = Pi.single i ((B i) j) i

case h.mk.inr
η : Type u_7
inst✝⁵ : Fintype η
inst✝⁴ : DecidableEq η
ι : η → Type u_8
inst✝³ : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst✝² : RCLike 𝕜
E : η → Type u_10
inst✝¹ : (i : η) → NormedAddCommGroup (E i)
inst✝ : (i : η) → InnerProductSpace 𝕜 (E i)
B : (i : η) → OrthonormalBasis (ι i) 𝕜 (E i)
k i : η
j : ι i
hi : i ≠ k
⊢ (B k).repr.symm ((WithLp.equiv 2 (ι k → 𝕜)).symm (Pi.single i (Pi.single j 1) k)) = Pi.single i ((B i) j) k