by_cases h : j = i <;> simp [h]
case h
𝕜 : Type u_1
α : Type u_2
ι : Type u_3
inst✝¹² : DecidableEq ι
inst✝¹¹ : Fintype ι
D : ι → Type u_4
n : ℕ
E : Fin n → Type u_5
F : Type u_6
G : Type u_7
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup α
inst✝⁸ : NormedSpace 𝕜 α
inst✝⁷ : (i : ι) → NormedAddCommGroup (D i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (D i)
inst✝⁵ : (i : Fin n) → NormedAddCommGroup (E i)
inst✝⁴ : (i : Fin n) → NormedSpace 𝕜 (E i)
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
i : ι
x : D i × ((j : { j // j ≠ i }) → D ↑j)
j : ι
⊢ (if h : j = i then (_ : i = j) ▸ x.1 else x.snd { val := j, property := (_ : ¬j = i) }) =
    if h : j = i then (_ : i = j) ▸ x.1 else (piSplitAt i D).symm (0, x.2) j
no goals