Theorem: Equiv.piSplitAt_symm_zero_add_single (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 : ι
u : α i
x : (j : { j // j ≠ i }) → α ↑j
⊢ (piSplitAt i α).symm (0, x) + Pi.single i u = (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 : ι
u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
⊢ ((piSplitAt i α).symm (0, x) + Pi.single i u) j = (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 : ι
u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
⊢ ((piSplitAt i α).symm (0, x) + Pi.single i u) j = (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 : ι
u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
h : j = i
⊢ ((piSplitAt i α).symm (0, x) + Pi.single i u) j = (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 : ι
u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
h : ¬j = i
⊢ ((piSplitAt i α).symm (0, x) + Pi.single i u) j = (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 : ι
u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
h : j = i
⊢ ((piSplitAt i α).symm (0, x) + Pi.single i u) j = (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 : ι
u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
h : ¬j = i
⊢ ((piSplitAt i α).symm (0, x) + Pi.single i u) j = (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 : ι
u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
h : ¬j = i
⊢ ((piSplitAt i α).symm (0, x) + Pi.single i u) j = (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 : ι
u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
h : ¬j = i
⊢ ((piSplitAt i α).symm (0, x) + Pi.single i u) j = (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 : ι
u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
h : j = i
⊢ ((piSplitAt i α).symm (0, x) + Pi.single i u) j = (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 : ι
u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
h : j = i
⊢ ((piSplitAt i α).symm (0, x) + Pi.single i u) i = (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 : ι
u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
h : j = i
⊢ ((piSplitAt i α).symm (0, x) + Pi.single i u) i = (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 : ι
u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
h : ¬j = i
⊢ ((piSplitAt i α).symm (0, x) + Pi.single i u) j = (piSplitAt i α).symm (u, x) j
Tactic:
simp [h]
State after:
no goals