α : Type u_1
α' : Type u_2
ι : Type u_3
f : α → α'
l : Line α ι
x : α
⊢ (fun i => f (Option.getD (idxFun l i) x)) = f ∘ fun i => Option.getD (idxFun l i) x
α : Type u_1
α' : Type u_2
ι : Type u_3
f : α → α'
l : Line α ι
x : α
⊢ (fun x i => Option.getD (idxFun (map f l) i) x) (f x) = f ∘ (fun x i => Option.getD (idxFun l i) x) x
simp only [Line.apply, Line.map, Option.getD_map]
no goals
α : Type u_1
α' : Type u_2
ι : Type u_3
f : α → α'
l : Line α ι
x : α
⊢ (fun i => f (Option.getD (idxFun l i) x)) = f ∘ fun i => Option.getD (idxFun l i) x
rfl