n : ℕ
c : Composition n
i : Fin (length c)
j : Fin (blocksFun c i)
⊢ i = index c (↑(embedding c i) j)
n : ℕ
c : Composition n
i : Fin (length c)
j : Fin (blocksFun c i)
⊢ index c (↑(embedding c i) j) = i
symm
n : ℕ
c : Composition n
i : Fin (length c)
j : Fin (blocksFun c i)
⊢ ↑(embedding c i) j ∈ Set.range ↑(embedding c i)
n : ℕ
c : Composition n
i : Fin (length c)
j : Fin (blocksFun c i)
⊢ i = index c (↑(embedding c i) j)
rw [← mem_range_embedding_iff']
no goals
n : ℕ
c : Composition n
i : Fin (length c)
j : Fin (blocksFun c i)
⊢ ↑(embedding c i) j ∈ Set.range ↑(embedding c i)
apply Set.mem_range_self