case h
α : Type u_1
ι : Type u_2
ι' : Type u_3
l : Line α ι
l' : Line α ι'
x : α
i : ι ⊕ ι'
⊢ (fun x i => Option.getD (idxFun (prod l l') i) x) x i =
    Sum.elim ((fun x i => Option.getD (idxFun l i) x) x) ((fun x i => Option.getD (idxFun l' i) x) x) i
α : Type u_1
ι : Type u_2
ι' : Type u_3
l : Line α ι
l' : Line α ι'
x : α
⊢ (fun x i => Option.getD (idxFun (prod l l') i) x) x =
    Sum.elim ((fun x i => Option.getD (idxFun l i) x) x) ((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
l : Line α ι
l' : Line α ι'
x : α
i : ι ⊕ ι'
⊢ (fun x i => Option.getD (idxFun (prod l l') i) x) x i =
    Sum.elim ((fun x i => Option.getD (idxFun l i) x) x) ((fun x i => Option.getD (idxFun l' i) x) x) i
cases i <;> rfl