n : ℕ
c : Composition n
j : Fin n
this : ↑(embedding c (index c j)) (invEmbedding c j) ∈ Set.range ↑(embedding c (index c j))
⊢ j ∈ Set.range ↑(embedding c (index c j))
n : ℕ
c : Composition n
j : Fin n
⊢ j ∈ Set.range ↑(embedding c (index c j))
have : c.embedding (c.index j) (c.invEmbedding j) ∈ Set.range (c.embedding (c.index j)) :=
  Set.mem_range_self _
n : ℕ
c : Composition n
j : Fin n
this : j ∈ Set.range ↑(embedding c (index c j))
⊢ j ∈ Set.range ↑(embedding c (index c j))
n : ℕ
c : Composition n
j : Fin n
this : ↑(embedding c (index c j)) (invEmbedding c j) ∈ Set.range ↑(embedding c (index c j))
⊢ j ∈ Set.range ↑(embedding c (index c j))
rw [c.embedding_comp_inv j] at this
no goals
n : ℕ
c : Composition n
j : Fin n
this : j ∈ Set.range ↑(embedding c (index c j))
⊢ j ∈ Set.range ↑(embedding c (index c j))
assumption