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