Theorem: Function.update_piSplitAt_symm (ForML/PiEquiv.lean)

State before:
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : DecidableEq ι
i✝ : ι
p : ι → Prop
inst✝² : DecidablePred p
α : ι → Type u_3
inst✝¹ : (j : ι) → NormedAddCommGroup (α j)
inst✝ : (j : ι) → NormedSpace 𝕜 (α j)
i : ι
a u : α i
x : (j : { j // j ≠ i }) → α ↑j
⊢ update ((Equiv.piSplitAt i α).symm (a, x)) i u = (Equiv.piSplitAt i α).symm (u, x)
Tactic:
ext j
State after:
case h
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : DecidableEq ι
i✝ : ι
p : ι → Prop
inst✝² : DecidablePred p
α : ι → Type u_3
inst✝¹ : (j : ι) → NormedAddCommGroup (α j)
inst✝ : (j : ι) → NormedSpace 𝕜 (α j)
i : ι
a u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
⊢ update ((Equiv.piSplitAt i α).symm (a, x)) i u j = (Equiv.piSplitAt i α).symm (u, x) j

State before:
case h
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : DecidableEq ι
i✝ : ι
p : ι → Prop
inst✝² : DecidablePred p
α : ι → Type u_3
inst✝¹ : (j : ι) → NormedAddCommGroup (α j)
inst✝ : (j : ι) → NormedSpace 𝕜 (α j)
i : ι
a u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
⊢ update ((Equiv.piSplitAt i α).symm (a, x)) i u j = (Equiv.piSplitAt i α).symm (u, x) j
Tactic:
by_cases h : j = i
State after:
case pos
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : DecidableEq ι
i✝ : ι
p : ι → Prop
inst✝² : DecidablePred p
α : ι → Type u_3
inst✝¹ : (j : ι) → NormedAddCommGroup (α j)
inst✝ : (j : ι) → NormedSpace 𝕜 (α j)
i : ι
a u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
h : j = i
⊢ update ((Equiv.piSplitAt i α).symm (a, x)) i u j = (Equiv.piSplitAt i α).symm (u, x) j

case neg
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : DecidableEq ι
i✝ : ι
p : ι → Prop
inst✝² : DecidablePred p
α : ι → Type u_3
inst✝¹ : (j : ι) → NormedAddCommGroup (α j)
inst✝ : (j : ι) → NormedSpace 𝕜 (α j)
i : ι
a u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
h : ¬j = i
⊢ update ((Equiv.piSplitAt i α).symm (a, x)) i u j = (Equiv.piSplitAt i α).symm (u, x) j

State before:
case pos
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : DecidableEq ι
i✝ : ι
p : ι → Prop
inst✝² : DecidablePred p
α : ι → Type u_3
inst✝¹ : (j : ι) → NormedAddCommGroup (α j)
inst✝ : (j : ι) → NormedSpace 𝕜 (α j)
i : ι
a u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
h : j = i
⊢ update ((Equiv.piSplitAt i α).symm (a, x)) i u j = (Equiv.piSplitAt i α).symm (u, x) j

case neg
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : DecidableEq ι
i✝ : ι
p : ι → Prop
inst✝² : DecidablePred p
α : ι → Type u_3
inst✝¹ : (j : ι) → NormedAddCommGroup (α j)
inst✝ : (j : ι) → NormedSpace 𝕜 (α j)
i : ι
a u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
h : ¬j = i
⊢ update ((Equiv.piSplitAt i α).symm (a, x)) i u j = (Equiv.piSplitAt i α).symm (u, x) j
Tactic:
. rw [h]; simp
State after:
case neg
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : DecidableEq ι
i✝ : ι
p : ι → Prop
inst✝² : DecidablePred p
α : ι → Type u_3
inst✝¹ : (j : ι) → NormedAddCommGroup (α j)
inst✝ : (j : ι) → NormedSpace 𝕜 (α j)
i : ι
a u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
h : ¬j = i
⊢ update ((Equiv.piSplitAt i α).symm (a, x)) i u j = (Equiv.piSplitAt i α).symm (u, x) j

State before:
case neg
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : DecidableEq ι
i✝ : ι
p : ι → Prop
inst✝² : DecidablePred p
α : ι → Type u_3
inst✝¹ : (j : ι) → NormedAddCommGroup (α j)
inst✝ : (j : ι) → NormedSpace 𝕜 (α j)
i : ι
a u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
h : ¬j = i
⊢ update ((Equiv.piSplitAt i α).symm (a, x)) i u j = (Equiv.piSplitAt i α).symm (u, x) j
Tactic:
. simp [h]
State after:
no goals

State before:
case pos
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : DecidableEq ι
i✝ : ι
p : ι → Prop
inst✝² : DecidablePred p
α : ι → Type u_3
inst✝¹ : (j : ι) → NormedAddCommGroup (α j)
inst✝ : (j : ι) → NormedSpace 𝕜 (α j)
i : ι
a u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
h : j = i
⊢ update ((Equiv.piSplitAt i α).symm (a, x)) i u j = (Equiv.piSplitAt i α).symm (u, x) j
Tactic:
rw [h]
State after:
case pos
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : DecidableEq ι
i✝ : ι
p : ι → Prop
inst✝² : DecidablePred p
α : ι → Type u_3
inst✝¹ : (j : ι) → NormedAddCommGroup (α j)
inst✝ : (j : ι) → NormedSpace 𝕜 (α j)
i : ι
a u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
h : j = i
⊢ update ((Equiv.piSplitAt i α).symm (a, x)) i u i = (Equiv.piSplitAt i α).symm (u, x) i

State before:
case pos
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : DecidableEq ι
i✝ : ι
p : ι → Prop
inst✝² : DecidablePred p
α : ι → Type u_3
inst✝¹ : (j : ι) → NormedAddCommGroup (α j)
inst✝ : (j : ι) → NormedSpace 𝕜 (α j)
i : ι
a u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
h : j = i
⊢ update ((Equiv.piSplitAt i α).symm (a, x)) i u i = (Equiv.piSplitAt i α).symm (u, x) i
Tactic:
simp
State after:
no goals

State before:
case neg
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : DecidableEq ι
i✝ : ι
p : ι → Prop
inst✝² : DecidablePred p
α : ι → Type u_3
inst✝¹ : (j : ι) → NormedAddCommGroup (α j)
inst✝ : (j : ι) → NormedSpace 𝕜 (α j)
i : ι
a u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
h : ¬j = i
⊢ update ((Equiv.piSplitAt i α).symm (a, x)) i u j = (Equiv.piSplitAt i α).symm (u, x) j
Tactic:
simp [h]
State after:
no goals