-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem CompositionAsSet.toComposition_boundaries (c : CompositionAsSet n) :
    c.toComposition.boundaries = c.boundaries

Proof state:
case h.mp.intro.intro.refine_1
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : Fin (c.toComposition.length + 1)
left✝ : i ∈ Finset.univ
hi : c.toComposition.boundary.toEmbedding i = j
⊢ ↑i < c.boundaries.card

Tactic:
simpa [c.card_boundaries_eq_succ_length] using i.2

Result:
no goals

Proof state:
case h.mp.intro.intro.refine_2
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : Fin (c.toComposition.length + 1)
left✝ : i ∈ Finset.univ
hi : c.toComposition.boundary.toEmbedding i = j
⊢ (take (↑i) c.blocks).sum = ↑j

Tactic:
simp [Composition.boundary, Composition.sizeUpTo, ← hi]

Result:
no goals

Proof state:
case h
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
⊢ (∃ a ∈ Finset.univ, c.toComposition.boundary.toEmbedding a = j) ↔ ∃ i < c.boundaries.card, (take i c.blocks).sum = ↑j

Tactic:
constructor

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

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

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

Tactic:
rintro ⟨i, _, hi⟩

Result:
case h.mp.intro.intro
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : Fin (c.toComposition.length + 1)
left✝ : i ∈ Finset.univ
hi : c.toComposition.boundary.toEmbedding i = j
⊢ ∃ i < c.boundaries.card, (take i c.blocks).sum = ↑j

Proof state:
case h.mpr.intro.intro
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : ℕ
i_lt : i < c.boundaries.card
hi : (take i c.blocks).sum = ↑j
⊢ ∃ a ∈ Finset.univ, c.toComposition.boundary.toEmbedding a = j

Tactic:
refine ⟨i, by simp, ?_⟩

Result:
case h.mpr.intro.intro
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : ℕ
i_lt : i < c.boundaries.card
hi : (take i c.blocks).sum = ↑j
⊢ c.toComposition.boundary.toEmbedding ↑i = j

Proof state:
case h
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
⊢ j ∈ c.toComposition.boundaries ↔ j ∈ c.boundaries

Tactic:
simp only [c.mem_boundaries_iff_exists_blocks_sum_take_eq, Composition.boundaries, Finset.mem_map]

Result:
case h
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
⊢ (∃ a ∈ Finset.univ, c.toComposition.boundary.toEmbedding a = j) ↔ ∃ i < c.boundaries.card, (take i c.blocks).sum = ↑j

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

Tactic:
rintro ⟨i, i_lt, hi⟩

Result:
case h.mpr.intro.intro
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : ℕ
i_lt : i < c.boundaries.card
hi : (take i c.blocks).sum = ↑j
⊢ ∃ a ∈ Finset.univ, c.toComposition.boundary.toEmbedding a = j

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

Tactic:
rw [c.card_boundaries_eq_succ_length] at i_lt

Result:
case h.mpr.intro.intro
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : ℕ
i_lt : i < c.length + 1
hi : (take i c.blocks).sum = ↑j
⊢ c.toComposition.boundary.toEmbedding ↑i = j

Proof state:
case h.mp.intro.intro
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : Fin (c.toComposition.length + 1)
left✝ : i ∈ Finset.univ
hi : c.toComposition.boundary.toEmbedding i = j
⊢ ∃ i < c.boundaries.card, (take i c.blocks).sum = ↑j

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

Result:
case h.mp.intro.intro.refine_1
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : Fin (c.toComposition.length + 1)
left✝ : i ∈ Finset.univ
hi : c.toComposition.boundary.toEmbedding i = j
⊢ ↑i < c.boundaries.card

case h.mp.intro.intro.refine_2
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : Fin (c.toComposition.length + 1)
left✝ : i ∈ Finset.univ
hi : c.toComposition.boundary.toEmbedding i = j
⊢ (take (↑i) c.blocks).sum = ↑j

Proof state:
case h.mpr.intro.intro
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : ℕ
i_lt : i < c.length + 1
hi : (take i c.blocks).sum = ↑j
⊢ c.toComposition.boundary.toEmbedding ↑i = j

Tactic:
simp [Composition.boundary, Nat.mod_eq_of_lt i_lt, Composition.sizeUpTo, hi]

Result:
no goals

Proof state:
n : ℕ
c : CompositionAsSet n
⊢ c.toComposition.boundaries = c.boundaries

Tactic:
ext j

Result:
case h
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
⊢ j ∈ c.toComposition.boundaries ↔ j ∈ c.boundaries

Proof state:
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : ℕ
i_lt : i < c.boundaries.card
hi : (take i c.blocks).sum = ↑j
⊢ ↑i ∈ Finset.univ

Tactic:
simp

Result:
no goals