case mp
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
⊢ j ∈ Set.range ↑(embedding c i) → i = index c j

case mpr
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
⊢ i = index c j → j ∈ Set.range ↑(embedding c i)
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
⊢ j ∈ Set.range ↑(embedding c i) ↔ i = index c j
constructor
case mp
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
⊢ ¬i = index c j → ¬j ∈ Set.range ↑(embedding c i)
case mp
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
⊢ j ∈ Set.range ↑(embedding c i) → i = index c j
rw [← not_imp_not]
case mp
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : ¬i = index c j
⊢ ¬j ∈ Set.range ↑(embedding c i)
case mp
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
⊢ ¬i = index c j → ¬j ∈ Set.range ↑(embedding c i)
intro h
no goals
case mp
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : ¬i = index c j
⊢ ¬j ∈ Set.range ↑(embedding c i)
exact Set.disjoint_right.1 (c.disjoint_range h) (c.mem_range_embedding j)
case mpr
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : i = index c j
⊢ j ∈ Set.range ↑(embedding c i)
case mpr
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
⊢ i = index c j → j ∈ Set.range ↑(embedding c i)
intro h
case mpr
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : i = index c j
⊢ j ∈ Set.range ↑(embedding c (index c j))
case mpr
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : i = index c j
⊢ j ∈ Set.range ↑(embedding c i)
rw [h]
no goals
case mpr
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : i = index c j
⊢ j ∈ Set.range ↑(embedding c (index c j))
exact c.mem_range_embedding j