n : ℕ
c : Composition n
j : Fin n
⊢ ↑(↑(embedding c (index c j)) (invEmbedding c j)) = ↑j
n : ℕ
c : Composition n
j : Fin n
⊢ ↑(embedding c (index c j)) (invEmbedding c j) = j
rw [Fin.ext_iff]
no goals
n : ℕ
c : Composition n
j : Fin n
⊢ ↑(↑(embedding c (index c j)) (invEmbedding c j)) = ↑j
apply add_tsub_cancel_of_le (c.sizeUpTo_index_le j)