case mp
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
⊢ j ∈ Set.range ↑(embedding c i) → sizeUpTo c ↑i ≤ ↑j ∧ ↑j < sizeUpTo c (Nat.succ ↑i)

case mpr
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
⊢ sizeUpTo c ↑i ≤ ↑j ∧ ↑j < sizeUpTo c (Nat.succ ↑i) → j ∈ Set.range ↑(embedding c i)
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
⊢ j ∈ Set.range ↑(embedding c i) ↔ sizeUpTo c ↑i ≤ ↑j ∧ ↑j < sizeUpTo c (Nat.succ ↑i)
constructor
case mp
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : j ∈ Set.range ↑(embedding c i)
⊢ sizeUpTo c ↑i ≤ ↑j ∧ ↑j < sizeUpTo c (Nat.succ ↑i)
case mp
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
⊢ j ∈ Set.range ↑(embedding c i) → sizeUpTo c ↑i ≤ ↑j ∧ ↑j < sizeUpTo c (Nat.succ ↑i)
intro h
case mp.intro
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : j ∈ Set.range ↑(embedding c i)
k : Fin (blocksFun c i)
hk : (fun y => ↑(embedding c i) y) k = j
⊢ sizeUpTo c ↑i ≤ ↑j ∧ ↑j < sizeUpTo c (Nat.succ ↑i)
case mp
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : j ∈ Set.range ↑(embedding c i)
⊢ sizeUpTo c ↑i ≤ ↑j ∧ ↑j < sizeUpTo c (Nat.succ ↑i)
rcases Set.mem_range.2 h with ⟨k, hk⟩
case mp.intro
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : j ∈ Set.range ↑(embedding c i)
k : Fin (blocksFun c i)
hk : ↑((fun y => ↑(embedding c i) y) k) = ↑j
⊢ sizeUpTo c ↑i ≤ ↑j ∧ ↑j < sizeUpTo c (Nat.succ ↑i)
case mp.intro
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : j ∈ Set.range ↑(embedding c i)
k : Fin (blocksFun c i)
hk : (fun y => ↑(embedding c i) y) k = j
⊢ sizeUpTo c ↑i ≤ ↑j ∧ ↑j < sizeUpTo c (Nat.succ ↑i)
rw [Fin.ext_iff] at hk
case mp.intro
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : j ∈ Set.range ↑(embedding c i)
k : Fin (blocksFun c i)
hk : sizeUpTo c ↑i + ↑k = ↑j
⊢ sizeUpTo c ↑i ≤ ↑j ∧ ↑j < sizeUpTo c (Nat.succ ↑i)
case mp.intro
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : j ∈ Set.range ↑(embedding c i)
k : Fin (blocksFun c i)
hk : ↑((fun y => ↑(embedding c i) y) k) = ↑j
⊢ sizeUpTo c ↑i ≤ ↑j ∧ ↑j < sizeUpTo c (Nat.succ ↑i)
dsimp at hk
case mp.intro
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : j ∈ Set.range ↑(embedding c i)
k : Fin (blocksFun c i)
hk : sizeUpTo c ↑i + ↑k = ↑j
⊢ sizeUpTo c ↑i ≤ sizeUpTo c ↑i + ↑k ∧ sizeUpTo c ↑i + ↑k < sizeUpTo c (Nat.succ ↑i)
case mp.intro
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : j ∈ Set.range ↑(embedding c i)
k : Fin (blocksFun c i)
hk : sizeUpTo c ↑i + ↑k = ↑j
⊢ sizeUpTo c ↑i ≤ ↑j ∧ ↑j < sizeUpTo c (Nat.succ ↑i)
rw [← hk]
no goals
case mp.intro
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : j ∈ Set.range ↑(embedding c i)
k : Fin (blocksFun c i)
hk : sizeUpTo c ↑i + ↑k = ↑j
⊢ sizeUpTo c ↑i ≤ sizeUpTo c ↑i + ↑k ∧ sizeUpTo c ↑i + ↑k < sizeUpTo c (Nat.succ ↑i)
simp [sizeUpTo_succ', k.is_lt]
case mpr
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : sizeUpTo c ↑i ≤ ↑j ∧ ↑j < sizeUpTo c (Nat.succ ↑i)
⊢ j ∈ Set.range ↑(embedding c i)
case mpr
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
⊢ sizeUpTo c ↑i ≤ ↑j ∧ ↑j < sizeUpTo c (Nat.succ ↑i) → j ∈ Set.range ↑(embedding c i)
intro h
case mpr
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : sizeUpTo c ↑i ≤ ↑j ∧ ↑j < sizeUpTo c (Nat.succ ↑i)
⊢ ∃ y, ↑(embedding c i) y = j
case mpr
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : sizeUpTo c ↑i ≤ ↑j ∧ ↑j < sizeUpTo c (Nat.succ ↑i)
⊢ j ∈ Set.range ↑(embedding c i)
apply Set.mem_range.2
case mpr.refine'_1
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : sizeUpTo c ↑i ≤ ↑j ∧ ↑j < sizeUpTo c (Nat.succ ↑i)
⊢ ↑j - sizeUpTo c ↑i < blocksFun c i

case mpr.refine'_2
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : sizeUpTo c ↑i ≤ ↑j ∧ ↑j < sizeUpTo c (Nat.succ ↑i)
⊢ ↑(embedding c i) { val := ↑j - sizeUpTo c ↑i, isLt := ?mpr.refine'_1 } = j
case mpr
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : sizeUpTo c ↑i ≤ ↑j ∧ ↑j < sizeUpTo c (Nat.succ ↑i)
⊢ ∃ y, ↑(embedding c i) y = j
refine' ⟨⟨j - c.sizeUpTo i, _⟩, _⟩
case mpr.refine'_1
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : sizeUpTo c ↑i ≤ ↑j ∧ ↑j < sizeUpTo c (Nat.succ ↑i)
⊢ ↑j < sizeUpTo c (↑i + 1)

case mpr.refine'_1
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : sizeUpTo c ↑i ≤ ↑j ∧ ↑j < sizeUpTo c (Nat.succ ↑i)
⊢ sizeUpTo c ↑i ≤ ↑j
case mpr.refine'_1
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : sizeUpTo c ↑i ≤ ↑j ∧ ↑j < sizeUpTo c (Nat.succ ↑i)
⊢ ↑j - sizeUpTo c ↑i < blocksFun c i
rw [tsub_lt_iff_left, ← sizeUpTo_succ']
no goals
case mpr.refine'_1
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : sizeUpTo c ↑i ≤ ↑j ∧ ↑j < sizeUpTo c (Nat.succ ↑i)
⊢ ↑j < sizeUpTo c (↑i + 1)
exact h.2
no goals
case mpr.refine'_1
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : sizeUpTo c ↑i ≤ ↑j ∧ ↑j < sizeUpTo c (Nat.succ ↑i)
⊢ sizeUpTo c ↑i ≤ ↑j
exact h.1
case mpr.refine'_2
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : sizeUpTo c ↑i ≤ ↑j ∧ ↑j < sizeUpTo c (Nat.succ ↑i)
⊢ ↑(↑(embedding c i) { val := ↑j - sizeUpTo c ↑i, isLt := (_ : ↑j - sizeUpTo c ↑i < blocksFun c i) }) = ↑j
case mpr.refine'_2
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : sizeUpTo c ↑i ≤ ↑j ∧ ↑j < sizeUpTo c (Nat.succ ↑i)
⊢ ↑(embedding c i) { val := ↑j - sizeUpTo c ↑i, isLt := (_ : ↑j - sizeUpTo c ↑i < blocksFun c i) } = j
rw [Fin.ext_iff]
no goals
case mpr.refine'_2
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : sizeUpTo c ↑i ≤ ↑j ∧ ↑j < sizeUpTo c (Nat.succ ↑i)
⊢ ↑(↑(embedding c i) { val := ↑j - sizeUpTo c ↑i, isLt := (_ : ↑j - sizeUpTo c ↑i < blocksFun c i) }) = ↑j
exact add_tsub_cancel_of_le h.1