-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem mem_boundaries_iff_exists_blocks_sum_take_eq {j : Fin (n + 1)} :
    j ∈ c.boundaries ↔ ∃ i < c.boundaries.card, (c.blocks.take i).sum = j

Proof state:
case mp.intro
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
i : Fin c.boundaries.card
hi : ↑((c.boundaries.orderIsoOfFin ⋯) i) = ↑⟨j, hj⟩
⊢ ∃ i < c.boundaries.card, (take i c.blocks).sum = ↑j

Tactic:
refine ⟨i.1, i.2, ?_⟩

Result:
case mp.intro
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
i : Fin c.boundaries.card
hi : ↑((c.boundaries.orderIsoOfFin ⋯) i) = ↑⟨j, hj⟩
⊢ (take (↑i) c.blocks).sum = ↑j

Proof state:
case h.e'_5
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : ℕ
hi : i < c.boundaries.card
H : (take i c.blocks).sum = ↑j
this : c.boundary ⟨i, hi⟩ = j
⊢ j = ↑((c.boundaries.orderIsoOfFin ⋯) ⟨i, hi⟩)

Tactic:
exact this.symm

Result:
no goals

Proof state:
case mp.intro
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
i : Fin c.boundaries.card
hi : (c.boundaries.orderEmbOfFin ⋯) i = j
⊢ ↑(c.boundary ⟨↑i, ⋯⟩) = ↑((c.boundaries.orderEmbOfFin ⋯) i)

Tactic:
rfl

Result:
no goals

Proof state:
case h.e'_5
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : ℕ
hi : i < c.boundaries.card
H : (take i c.blocks).sum = ↑j
⊢ j = ↑((c.boundaries.orderIsoOfFin ⋯) ⟨i, hi⟩)

Tactic:
have : c.boundary ⟨i, hi⟩ = j := by rwa [Fin.ext_iff, ← c.blocks_partial_sum hi]

Result:
case h.e'_5
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : ℕ
hi : i < c.boundaries.card
H : (take i c.blocks).sum = ↑j
this : c.boundary ⟨i, hi⟩ = j
⊢ j = ↑((c.boundaries.orderIsoOfFin ⋯) ⟨i, hi⟩)

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

Tactic:
intro hj

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

Proof state:
case mp.intro
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
i : Fin c.boundaries.card
hi : ↑((c.boundaries.orderIsoOfFin ⋯) i) = ↑⟨j, hj⟩
⊢ (take (↑i) c.blocks).sum = ↑j

Tactic:
dsimp at hi

Result:
case mp.intro
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
i : Fin c.boundaries.card
hi : (c.boundaries.orderEmbOfFin ⋯) i = j
⊢ (take (↑i) c.blocks).sum = ↑j

Proof state:
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
⊢ j ∈ c.boundaries ↔ ∃ i < c.boundaries.card, (take i c.blocks).sum = ↑j

Tactic:
constructor

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

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

Proof state:
case mp.intro
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
i : Fin c.boundaries.card
hi : (c.boundaries.orderIsoOfFin ⋯) i = ⟨j, hj⟩
⊢ ∃ i < c.boundaries.card, (take i c.blocks).sum = ↑j

Tactic:
rw [Subtype.ext_iff, Subtype.coe_mk] at hi

Result:
case mp.intro
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
i : Fin c.boundaries.card
hi : ↑((c.boundaries.orderIsoOfFin ⋯) i) = ↑⟨j, hj⟩
⊢ ∃ i < c.boundaries.card, (take i c.blocks).sum = ↑j

Proof state:
case mp.intro
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
i : Fin c.boundaries.card
hi : (c.boundaries.orderEmbOfFin ⋯) i = j
⊢ (take (↑i) c.blocks).sum = ↑j

Tactic:
rw [← hi, c.blocks_partial_sum i.2]

Result:
case mp.intro
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
i : Fin c.boundaries.card
hi : (c.boundaries.orderEmbOfFin ⋯) i = j
⊢ ↑(c.boundary ⟨↑i, ⋯⟩) = ↑((c.boundaries.orderEmbOfFin ⋯) i)

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

Tactic:
rcases (c.boundaries.orderIsoOfFin rfl).surjective ⟨j, hj⟩ with ⟨i, hi⟩

Result:
case mp.intro
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
i : Fin c.boundaries.card
hi : (c.boundaries.orderIsoOfFin ⋯) i = ⟨j, hj⟩
⊢ ∃ i < c.boundaries.card, (take i c.blocks).sum = ↑j

Proof state:
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : ℕ
hi : i < c.boundaries.card
H : (take i c.blocks).sum = ↑j
⊢ c.boundary ⟨i, hi⟩ = j

Tactic:
rwa [Fin.ext_iff, ← c.blocks_partial_sum hi]

Result:
no goals

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

Tactic:
rintro ⟨i, hi, H⟩

Result:
case mpr.intro.intro
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : ℕ
hi : i < c.boundaries.card
H : (take i c.blocks).sum = ↑j
⊢ j ∈ c.boundaries

Proof state:
case mpr.intro.intro
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : ℕ
hi : i < c.boundaries.card
H : (take i c.blocks).sum = ↑j
⊢ j ∈ c.boundaries

Tactic:
convert (c.boundaries.orderIsoOfFin rfl ⟨i, hi⟩).2

Result:
case h.e'_5
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : ℕ
hi : i < c.boundaries.card
H : (take i c.blocks).sum = ↑j
⊢ j = ↑((c.boundaries.orderIsoOfFin ⋯) ⟨i, hi⟩)