case h
α : Type u_1
ι : Type u_2
ι' : Type u_3
v : ι → α
l : Line α ι'
x : α
i : ι ⊕ ι'
⊢ (fun x i => Option.getD (idxFun (vertical v l) i) x) x i = Sum.elim v ((fun x i => Option.getD (idxFun l i) x) x) i
α : Type u_1
ι : Type u_2
ι' : Type u_3
v : ι → α
l : Line α ι'
x : α
⊢ (fun x i => Option.getD (idxFun (vertical v l) i) x) x = Sum.elim v ((fun x i => Option.getD (idxFun l i) x) x)
funext i
no goals
case h
α : Type u_1
ι : Type u_2
ι' : Type u_3
v : ι → α
l : Line α ι'
x : α
i : ι ⊕ ι'
⊢ (fun x i => Option.getD (idxFun (vertical v l) i) x) x i = Sum.elim v ((fun x i => Option.getD (idxFun l i) x) x) i
cases i <;> rfl