case mp
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
⊢ j ∈ c.boundaries → ∃ i, i < Finset.card c.boundaries ∧ sum (take i (blocks c)) = ↑j

case mpr
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
⊢ (∃ i, i < Finset.card c.boundaries ∧ sum (take i (blocks c)) = ↑j) → j ∈ c.boundaries
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
⊢ j ∈ c.boundaries ↔ ∃ i, i < Finset.card c.boundaries ∧ sum (take i (blocks c)) = ↑j
constructor
case mp
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
⊢ ∃ i, i < Finset.card c.boundaries ∧ sum (take i (blocks c)) = ↑j
case mp
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
⊢ j ∈ c.boundaries → ∃ i, i < Finset.card c.boundaries ∧ sum (take i (blocks c)) = ↑j
intro hj
case mp.intro
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
i : Fin (Finset.card c.boundaries)
hi :
  ↑(Finset.orderIsoOfFin c.boundaries (_ : Finset.card c.boundaries = Finset.card c.boundaries)) i =
    { val := j, property := hj }
⊢ ∃ i, i < Finset.card c.boundaries ∧ sum (take i (blocks c)) = ↑j
case mp
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
⊢ ∃ i, i < Finset.card c.boundaries ∧ sum (take i (blocks c)) = ↑j
rcases(c.boundaries.orderIsoOfFin rfl).surjective ⟨j, hj⟩ with ⟨i, hi⟩
case mp.intro
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
i : Fin (Finset.card c.boundaries)
hi :
  ↑(↑(Finset.orderIsoOfFin c.boundaries (_ : Finset.card c.boundaries = Finset.card c.boundaries)) i) =
    ↑{ val := j, property := hj }
⊢ ∃ i, i < Finset.card c.boundaries ∧ sum (take i (blocks c)) = ↑j
case mp.intro
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
i : Fin (Finset.card c.boundaries)
hi :
  ↑(Finset.orderIsoOfFin c.boundaries (_ : Finset.card c.boundaries = Finset.card c.boundaries)) i =
    { val := j, property := hj }
⊢ ∃ i, i < Finset.card c.boundaries ∧ sum (take i (blocks c)) = ↑j
rw [Subtype.ext_iff, Subtype.coe_mk] at hi
case mp.intro
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
i : Fin (Finset.card c.boundaries)
hi :
  ↑(↑(Finset.orderIsoOfFin c.boundaries (_ : Finset.card c.boundaries = Finset.card c.boundaries)) i) =
    ↑{ val := j, property := hj }
⊢ sum (take (↑i) (blocks c)) = ↑j
case mp.intro
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
i : Fin (Finset.card c.boundaries)
hi :
  ↑(↑(Finset.orderIsoOfFin c.boundaries (_ : Finset.card c.boundaries = Finset.card c.boundaries)) i) =
    ↑{ val := j, property := hj }
⊢ ∃ i, i < Finset.card c.boundaries ∧ sum (take i (blocks c)) = ↑j
refine' ⟨i.1, i.2, _⟩
case mp.intro
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
i : Fin (Finset.card c.boundaries)
hi : ↑(Finset.orderEmbOfFin c.boundaries (_ : Finset.card c.boundaries = Finset.card c.boundaries)) i = j
⊢ sum (take (↑i) (blocks c)) = ↑j
case mp.intro
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
i : Fin (Finset.card c.boundaries)
hi :
  ↑(↑(Finset.orderIsoOfFin c.boundaries (_ : Finset.card c.boundaries = Finset.card c.boundaries)) i) =
    ↑{ val := j, property := hj }
⊢ sum (take (↑i) (blocks c)) = ↑j
dsimp at hi
case mp.intro
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
i : Fin (Finset.card c.boundaries)
hi : ↑(Finset.orderEmbOfFin c.boundaries (_ : Finset.card c.boundaries = Finset.card c.boundaries)) i = j
⊢ ↑(↑(boundary c) { val := ↑i, isLt := (_ : ↑i < Finset.card c.boundaries) }) =
    ↑(↑(Finset.orderEmbOfFin c.boundaries (_ : Finset.card c.boundaries = Finset.card c.boundaries)) i)
case mp.intro
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
i : Fin (Finset.card c.boundaries)
hi : ↑(Finset.orderEmbOfFin c.boundaries (_ : Finset.card c.boundaries = Finset.card c.boundaries)) i = j
⊢ sum (take (↑i) (blocks c)) = ↑j
rw [← hi, c.blocks_partial_sum i.2]
no goals
case mp.intro
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
i : Fin (Finset.card c.boundaries)
hi : ↑(Finset.orderEmbOfFin c.boundaries (_ : Finset.card c.boundaries = Finset.card c.boundaries)) i = j
⊢ ↑(↑(boundary c) { val := ↑i, isLt := (_ : ↑i < Finset.card c.boundaries) }) =
    ↑(↑(Finset.orderEmbOfFin c.boundaries (_ : Finset.card c.boundaries = Finset.card c.boundaries)) i)
rfl
case mpr.intro.intro
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : ℕ
hi : i < Finset.card c.boundaries
H : sum (take i (blocks c)) = ↑j
⊢ j ∈ c.boundaries
case mpr
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
⊢ (∃ i, i < Finset.card c.boundaries ∧ sum (take i (blocks c)) = ↑j) → j ∈ c.boundaries
rintro ⟨i, hi, H⟩
case h.e'_4
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : ℕ
hi : i < Finset.card c.boundaries
H : sum (take i (blocks c)) = ↑j
⊢ j =
    ↑(↑(Finset.orderIsoOfFin c.boundaries (_ : Finset.card c.boundaries = Finset.card c.boundaries))
        { val := i, isLt := hi })
case mpr.intro.intro
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : ℕ
hi : i < Finset.card c.boundaries
H : sum (take i (blocks c)) = ↑j
⊢ j ∈ c.boundaries
convert (c.boundaries.orderIsoOfFin rfl ⟨i, hi⟩).2
case h.e'_4
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : ℕ
hi : i < Finset.card c.boundaries
H : sum (take i (blocks c)) = ↑j
this : ↑(boundary c) { val := i, isLt := hi } = j
⊢ j =
    ↑(↑(Finset.orderIsoOfFin c.boundaries (_ : Finset.card c.boundaries = Finset.card c.boundaries))
        { val := i, isLt := hi })
case h.e'_4
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : ℕ
hi : i < Finset.card c.boundaries
H : sum (take i (blocks c)) = ↑j
⊢ j =
    ↑(↑(Finset.orderIsoOfFin c.boundaries (_ : Finset.card c.boundaries = Finset.card c.boundaries))
        { val := i, isLt := hi })
have : c.boundary ⟨i, hi⟩ = j := by rwa [Fin.ext_iff, ← c.blocks_partial_sum hi]
no goals
case h.e'_4
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : ℕ
hi : i < Finset.card c.boundaries
H : sum (take i (blocks c)) = ↑j
this : ↑(boundary c) { val := i, isLt := hi } = j
⊢ j =
    ↑(↑(Finset.orderIsoOfFin c.boundaries (_ : Finset.card c.boundaries = Finset.card c.boundaries))
        { val := i, isLt := hi })
exact this.symm
no goals
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : ℕ
hi : i < Finset.card c.boundaries
H : sum (take i (blocks c)) = ↑j
⊢ ↑(boundary c) { val := i, isLt := hi } = j
rwa [Fin.ext_iff, ← c.blocks_partial_sum hi]