Theorem: Equiv.piSplitAt_symm_apply_eq_update_zero (ForML/MultilinearDeriv.lean)

State before:
𝕜 : 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)
⊢ (piSplitAt i D).symm x = Function.update ((piSplitAt i D).symm (0, x.2)) i x.1
Tactic:
ext j
State after:
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 : ι
⊢ (piSplitAt i D).symm x j = Function.update ((piSplitAt i D).symm (0, x.2)) i x.1 j

State before:
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 : ι
⊢ (piSplitAt i D).symm x j = Function.update ((piSplitAt i D).symm (0, x.2)) i x.1 j
Tactic:
simp [Equiv.piSplitAt_symm_apply]
State after:
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) }) =
    Function.update ((piSplitAt i D).symm (0, x.2)) i x.1 j

State before:
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) }) =
    Function.update ((piSplitAt i D).symm (0, x.2)) i x.1 j
Tactic:
rw [Function.update]
State after:
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

State before:
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
Tactic:
by_cases h : j = i <;> simp [h]
State after:
no goals