dsimp [comp]
n : Nat
x y : Permutation n
i : Nat
h : i < n
⊢ (comp x y)[i] = x[↑y[i]]
n : Nat
x y : Permutation n
i : Nat
h : i < n
⊢ (ofFn (fun i => x[↑y[↑i]]) (_ : ∀ (i j : Fin n), (fun i => x[↑y[↑i]]) i = (fun i => x[↑y[↑i]]) j → i = j))[i] =
    x[↑y[i]]