no goals
α : Type u
inst✝¹ : Finite α
κ : Type v
inst✝ : Finite κ
ι : Type
ιfin : Fintype ι
hι : ∀ (C : (ι → α) → ULift κ), ∃ l, IsMono C l
C : (ι → α) → κ
l : Line α ι
c : ULift κ
hc : ∀ (x : α), (ULift.up ∘ C) ((fun x i => Option.getD (idxFun l i) x) x) = c
x : α
⊢ C ((fun x i => Option.getD (idxFun l i) x) x) = c.down
rw [← hc x, Function.comp_apply]