awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
⊢ Fin.last n = c.boundaries.max' ⋯

Tactic:
le_antisymm (Finset.le_max' _ _ c.getLast_mem) (Fin.le_last _)

Premises used: le_antisymm, CompositionAsSet.getLast_mem, Finset.le_max', Fin.le_last
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
⊢ Fin.last n = c.boundaries.max' ⋯

Tactic:
exact le_antisymm (Finset.le_max' _ _ c.getLast_mem) (Fin.le_last _)

Premises used: le_antisymm, CompositionAsSet.getLast_mem, Finset.le_max', Fin.le_last
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
i : Fin c.length
⊢ 0 < c.blocksFun i

Tactic:
haveI : (⟨i, c.lt_length' i⟩ : Fin c.boundaries.card) < ⟨i + 1, c.lt_length i⟩ :=
    Nat.lt_succ_self _
  lt_tsub_iff_left.mpr ((c.boundaries.orderEmbOfFin rfl).strictMono this)

Premises used: Iff.mpr, Finset.orderEmbOfFin, OrderEmbedding.strictMono, Nat.lt_succ_self, CompositionAsSet.boundaries, CompositionAsSet.blocksFun, rfl, lt_tsub_iff_left
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
⊢ c.blocks.length = c.length

Tactic:
length_ofFn

Premises used: List.length_ofFn, CompositionAsSet.blocks
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
h : 0 < c.boundaries.card
⊢ (take 0 c.blocks).sum = (↑((c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) ⟨0, h⟩) : ℕ)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
i : ℕ
IH :
  ∀ (h : i < c.boundaries.card),
    (take i c.blocks).sum = (↑((c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) ⟨i, h⟩) : ℕ)
h : i + 1 < c.boundaries.card
⊢ i + 1 < c.length + 1

Tactic:
rw [c.card_boundaries_eq_succ_length] at h

Premises used: CompositionAsSet.card_boundaries_eq_succ_length
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
i : ℕ
IH :
  ∀ (h : i < c.boundaries.card),
    (take i c.blocks).sum = (↑((c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) ⟨i, h⟩) : ℕ)
h : i + 1 < c.length + 1
⊢ i < c.blocks.length

Tactic:
simp [blocks, Nat.lt_of_succ_lt_succ h]

Premises used: CompositionAsSet.blocks, Nat.lt_of_succ_lt_succ
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
i : ℕ
IH :
  ∀ (h : i < c.boundaries.card),
    (take i c.blocks).sum = (↑((c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) ⟨i, h⟩) : ℕ)
h : i + 1 < c.boundaries.card
⊢ i < c.blocks.length

Tactic:
have A : i < c.blocks.length := by
      rw [c.card_boundaries_eq_succ_length] at h
      simp [blocks, Nat.lt_of_succ_lt_succ h]
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
i : ℕ
IH :
  ∀ (h : i < c.boundaries.card),
    (take i c.blocks).sum = (↑((c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) ⟨i, h⟩) : ℕ)
h : i + 1 < c.boundaries.card
A : i < c.blocks.length
⊢ c.blocks.length ≤ c.boundaries.card

Tactic:
simp [blocks, length]

Premises used: CompositionAsSet.blocks, CompositionAsSet.length
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
i : ℕ
IH :
  ∀ (h : i < c.boundaries.card),
    (take i c.blocks).sum = (↑((c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) ⟨i, h⟩) : ℕ)
h : i + 1 < c.boundaries.card
A : i < c.blocks.length
⊢ i < c.boundaries.card

Tactic:
have B : i < c.boundaries.card := lt_of_lt_of_le A (by simp [blocks, length])
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
i : ℕ
IH :
  ∀ (h : i < c.boundaries.card),
    (take i c.blocks).sum = (↑((c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) ⟨i, h⟩) : ℕ)
h : i + 1 < c.boundaries.card
A : i < c.blocks.length
B : i < c.boundaries.card
succ :
  (↑((c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) (⟨i, B⟩ : Fin c.boundaries.card)) : ℕ) +
      getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) c.blocks i A =
    (↑((c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) ⟨i + 1, h⟩) : ℕ)
⊢ (take (i + 1) c.blocks).sum = (↑((c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) ⟨i + 1, h⟩) : ℕ)

Tactic:
rw [sum_take_succ _ _ A, IH B]

Premises used: List.sum_take_succ
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
i : ℕ
IH :
  ∀ (h : i < c.boundaries.card),
    (take i c.blocks).sum = (↑((c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) ⟨i, h⟩) : ℕ)
h : i + 1 < c.boundaries.card
A : i < c.blocks.length
B : i < c.boundaries.card
⊢ (↑((c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) (⟨i, B⟩ : Fin c.boundaries.card)) : ℕ) +
      getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) c.blocks i A =
    (↑((c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) ⟨i + 1, h⟩) : ℕ)

Tactic:
simp [blocks, blocksFun]

Premises used: CompositionAsSet.blocks, CompositionAsSet.blocksFun
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
i : ℕ
h : i < c.boundaries.card
zero :
  ∀ (h : 0 < c.boundaries.card),
    (take 0 c.blocks).sum = (↑((c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) ⟨0, h⟩) : ℕ)
succ :
  ∀ (i : ℕ)
    (IH :
      ∀ (h : i < c.boundaries.card),
        (take i c.blocks).sum = (↑((c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) ⟨i, h⟩) : ℕ))
    (h : i + 1 < c.boundaries.card),
    (take (i + 1) c.blocks).sum = (↑((c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) ⟨i + 1, h⟩) : ℕ)
⊢ (take i c.blocks).sum = (↑((c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) ⟨i, h⟩) : ℕ)

Tactic:
induction i with
  | zero => simp
  | succ i IH =>
    have A : i < c.blocks.length := by
      rw [c.card_boundaries_eq_succ_length] at h
      simp [blocks, Nat.lt_of_succ_lt_succ h]
    have B : i < c.boundaries.card := lt_of_lt_of_le A (by simp [blocks, length])
    rw [sum_take_succ _ _ A, IH B]
    simp [blocks, blocksFun]

Premises used: CompositionAsSet.blocks, CompositionAsSet.blocksFun
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
mp : j ∈ c.boundaries → ∃ i < c.boundaries.card, (take i c.blocks).sum = (↑j : ℕ)
mpr : (∃ i < c.boundaries.card, (take i c.blocks).sum = (↑j : ℕ)) → j ∈ c.boundaries
⊢ j ∈ c.boundaries ↔ ∃ i < c.boundaries.card, (take i c.blocks).sum = (↑j : ℕ)

Tactic:
constructor
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
mp :
  ∀ (i : Fin c.boundaries.card)
    (hi :
      (c.boundaries.orderIsoOfFin ⋯ : (a : Fin c.boundaries.card) → ↥c.boundaries) i =
        Subtype.mk (p := fun (x : Fin n.succ) ↦ x ∈ c.boundaries) j hj),
    ∃ i < c.boundaries.card, (take i c.blocks).sum = (↑j : ℕ)
⊢ ∃ i < c.boundaries.card, (take i c.blocks).sum = (↑j : ℕ)

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

Premises used: Finset.orderIsoOfFin, CompositionAsSet.boundaries, OrderIso.surjective, Subtype.mk, rfl
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
i : Fin c.boundaries.card
hi :
  (c.boundaries.orderIsoOfFin ⋯ : (a : Fin c.boundaries.card) → ↥c.boundaries) i =
    Subtype.mk (p := fun (x : Fin n.succ) ↦ x ∈ c.boundaries) j hj
⊢ (↑((c.boundaries.orderIsoOfFin ⋯ : (a : Fin c.boundaries.card) → ↥c.boundaries) i) : Fin n.succ) =
    (↑(Subtype.mk (p := fun (x : Fin n.succ) ↦ x ∈ c.boundaries) j hj) : Fin n.succ)

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

Premises used: Subtype.coe_mk, Subtype.ext_iff
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
i : Fin c.boundaries.card
hi :
  (↑((c.boundaries.orderIsoOfFin ⋯ : (a : Fin c.boundaries.card) → ↥c.boundaries) i) : Fin n.succ) =
    (↑(Subtype.mk (p := fun (x : Fin n.succ) ↦ x ∈ c.boundaries) j hj) : Fin n.succ)
⊢ ∃ i < c.boundaries.card, (take i c.blocks).sum = (↑j : ℕ)

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

Premises used: Fin.isLt, Fin.val, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
i : Fin c.boundaries.card
hi :
  (↑((c.boundaries.orderIsoOfFin ⋯ : (a : Fin c.boundaries.card) → ↥c.boundaries) i) : Fin n.succ) =
    (↑(Subtype.mk (p := fun (x : Fin n.succ) ↦ x ∈ c.boundaries) j hj) : Fin n.succ)
mp : (take (↑i : ℕ) c.blocks).sum = (↑j : ℕ)
⊢ ∃ i < c.boundaries.card, (take i c.blocks).sum = (↑j : ℕ)

Tactic:
refine ⟨i.1, i.2, ?_⟩
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
i : Fin c.boundaries.card
hi : (c.boundaries.orderEmbOfFin ⋯ : (a : Fin c.boundaries.card) → Fin (n + 1)) i = j
mp :
  (↑((c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) (⟨(↑i : ℕ), ⋯⟩ : Fin c.boundaries.card)) : ℕ) =
    (↑((c.boundaries.orderEmbOfFin ⋯ : (a : Fin c.boundaries.card) → Fin (n + 1)) i) : ℕ)
⊢ (take (↑i : ℕ) c.blocks).sum = (↑j : ℕ)

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

Premises used: Fin.isLt, CompositionAsSet.blocks_partial_sum
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
i : Fin c.boundaries.card
hi : (c.boundaries.orderEmbOfFin ⋯ : (a : Fin c.boundaries.card) → Fin (n + 1)) i = j
⊢ (↑((c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) (⟨(↑i : ℕ), ⋯⟩ : Fin c.boundaries.card)) : ℕ) =
    (↑((c.boundaries.orderEmbOfFin ⋯ : (a : Fin c.boundaries.card) → Fin (n + 1)) i) : ℕ)

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : ℕ
hi : i < c.boundaries.card
H : (take i c.blocks).sum = (↑j : ℕ)
⊢ (↑((c.boundaries.orderIsoOfFin ⋯ : (a : Fin c.boundaries.card) → ↥c.boundaries) ⟨i, hi⟩) : Fin n.succ) ∈ c.boundaries

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

Premises used: Finset.orderIsoOfFin, Fin.mk, CompositionAsSet.boundaries, DFunLike.coe, rfl, Subtype.property
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : ℕ
hi : i < c.boundaries.card
H : (take i c.blocks).sum = (↑j : ℕ)
h : j = (↑((c.boundaries.orderIsoOfFin ⋯ : (a : Fin c.boundaries.card) → ↥c.boundaries) ⟨i, hi⟩) : Fin n.succ)
⊢ j ∈ c.boundaries

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

Premises used: Finset.orderIsoOfFin, Fin.mk, CompositionAsSet.boundaries, DFunLike.coe, rfl, Subtype.property
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : ℕ
hi : i < c.boundaries.card
H : (take i c.blocks).sum = (↑j : ℕ)
rwa : (↑((c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) (⟨i, hi⟩ : Fin c.boundaries.card)) : ℕ) = (↑j : ℕ)
rwa₁ rwa₂ rwa₃ rwa₄ : (take i c.blocks).sum = (↑j : ℕ)
⊢ (c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) ⟨i, hi⟩ = j

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

Premises used: Fin.ext_iff, CompositionAsSet.blocks_partial_sum
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : ℕ
hi : i < c.boundaries.card
H : (take i c.blocks).sum = (↑j : ℕ)
⊢ (c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) ⟨i, hi⟩ = j

Tactic:
have : c.boundary ⟨i, hi⟩ = j := by rwa [Fin.ext_iff, ← c.blocks_partial_sum hi]
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : ℕ
hi : i < c.boundaries.card
H : (take i c.blocks).sum = (↑j : ℕ)
this : (c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) ⟨i, hi⟩ = j
⊢ j = (↑((c.boundaries.orderIsoOfFin ⋯ : (a : Fin c.boundaries.card) → ↥c.boundaries) ⟨i, hi⟩) : Fin n.succ)

Tactic:
this.symm

Premises used: Eq.symm
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : ℕ
hi : i < c.boundaries.card
H : (take i c.blocks).sum = (↑j : ℕ)
this : (c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) ⟨i, hi⟩ = j
⊢ j = (↑((c.boundaries.orderIsoOfFin ⋯ : (a : Fin c.boundaries.card) → ↥c.boundaries) ⟨i, hi⟩) : Fin n.succ)

Tactic:
exact this.symm

Premises used: Eq.symm
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
⊢ c.blocks.length ≤ c.length

Tactic:
simp [blocks]

Premises used: CompositionAsSet.blocks
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
⊢ take c.length c.blocks = c.blocks

Tactic:
have : c.blocks.take c.length = c.blocks := take_of_length_le (by simp [blocks])
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
this : take c.length c.blocks = c.blocks
rw : (↑(Fin.last n) : ℕ) = n
⊢ c.blocks.sum = n

Tactic:
rw [← this, c.blocks_partial_sum c.length_lt_card_boundaries, c.boundary_length]

Premises used: CompositionAsSet.length_lt_card_boundaries, CompositionAsSet.blocks_partial_sum, CompositionAsSet.boundary_length
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
this : take c.length c.blocks = c.blocks
⊢ (↑(Fin.last n) : ℕ) = n

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
⊢ ∀ {i : ℕ}, i ∈ c.blocks → 0 < i

Tactic:
simp only [blocks, forall_mem_ofFn_iff, blocksFun_pos c, forall_true_iff]

Premises used: List.forall_mem_ofFn_iff, CompositionAsSet.blocksFun_pos, CompositionAsSet.blocks, forall_true_iff
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
⊢ c.toCompositionAsSet.length = c.length

Tactic:
simp [Composition.toCompositionAsSet, CompositionAsSet.length, c.card_boundaries_eq_succ_length]

Premises used: Composition.toCompositionAsSet, Composition.card_boundaries_eq_succ_length, CompositionAsSet.length
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
⊢ c.toComposition.length = c.length

Tactic:
simp [CompositionAsSet.toComposition, Composition.length]

Premises used: Composition.length, CompositionAsSet.toComposition
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
change : d.blocks = c.blocks
⊢ c.toCompositionAsSet.blocks = c.blocks

Tactic:
change d.blocks = c.blocks

Premises used: Composition.blocks, CompositionAsSet.blocks
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
⊢ d.blocks.length = c.blocks.length

Tactic:
simp [d, blocks_length]

Premises used: Composition.blocks_length
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
⊢ d.blocks.length = c.blocks.length

Tactic:
have length_eq : d.blocks.length = c.blocks.length := by simp [d, blocks_length]
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
suffices : ∀ i ≤ d.blocks.length, (take i d.blocks).sum = (take i c.blocks).sum
⊢ d.blocks = c.blocks

Tactic:
suffices H : ∀ i ≤ d.blocks.length, (d.blocks.take i).sum = (c.blocks.take i).sum from
    eq_of_sum_take_eq length_eq H
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
⊢ i < d.boundaries.card

Tactic:
simpa [CompositionAsSet.blocks, length_ofFn,
      d.card_boundaries_eq_succ_length] using Nat.lt_succ_iff.2 hi

Premises used: Iff.mpr, CompositionAsSet.card_boundaries_eq_succ_length, List.length_ofFn, CompositionAsSet.blocks, Nat.lt_succ_iff
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
⊢ i < d.boundaries.card

Tactic:
have i_lt : i < d.boundaries.card := by
    simpa [CompositionAsSet.blocks, length_ofFn,
      d.card_boundaries_eq_succ_length] using Nat.lt_succ_iff.2 hi
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
i_lt : i < d.boundaries.card
⊢ i < c.boundaries.card

Tactic:
have i_lt' : i < c.boundaries.card := i_lt
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
i_lt : i < d.boundaries.card
i_lt' : i < c.boundaries.card
rwa rwa₁ rwa₂ rwa₃ : ∀ (i_lt' : i < c.length + 1), i < c.length + 1
⊢ i < c.length + 1

Tactic:
rwa [c.card_boundaries_eq_succ_length] at i_lt'

Premises used: Composition.card_boundaries_eq_succ_length
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
i_lt : i < d.boundaries.card
i_lt' : i < c.boundaries.card
⊢ i < c.length + 1

Tactic:
have i_lt'' : i < c.length + 1 := by rwa [c.card_boundaries_eq_succ_length] at i_lt'
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
i_lt : i < d.boundaries.card
i_lt' : i < c.boundaries.card
i_lt'' : i < c.length + 1
⊢ Eq (α := Fin n.succ)
    ((d.boundaries.orderEmbOfFin ⋯ : (a : Fin d.boundaries.card) → Fin n.succ) ⟨i, i_lt⟩ : Fin n.succ)
    ((c.boundaries.orderEmbOfFin ⋯ : (a : Fin (c.length + 1)) → Fin (n + 1)) ⟨i, i_lt''⟩ : Fin (n + 1))

Tactic:
have A :
    d.boundaries.orderEmbOfFin rfl ⟨i, i_lt⟩ =
      c.boundaries.orderEmbOfFin c.card_boundaries_eq_succ_length ⟨i, i_lt''⟩ :=
    rfl
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
i_lt : i < d.boundaries.card
i_lt' : i < c.boundaries.card
i_lt'' : i < c.length + 1
A :
  Eq (α := Fin n.succ)
    ((d.boundaries.orderEmbOfFin ⋯ : (a : Fin d.boundaries.card) → Fin n.succ) ⟨i, i_lt⟩ : Fin n.succ)
    ((c.boundaries.orderEmbOfFin ⋯ : (a : Fin (c.length + 1)) → Fin (n + 1)) ⟨i, i_lt''⟩ : Fin (n + 1))
⊢ c.sizeUpTo i = (↑((c.boundary : (a : Fin (c.length + 1)) → Fin (n + 1)) ⟨i, i_lt''⟩) : ℕ)

Tactic:
have B : c.sizeUpTo i = c.boundary ⟨i, i_lt''⟩ := rfl
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
i_lt : i < d.boundaries.card
i_lt' : i < c.boundaries.card
i_lt'' : i < c.length + 1
A :
  Eq (α := Fin n.succ)
    ((d.boundaries.orderEmbOfFin ⋯ : (a : Fin d.boundaries.card) → Fin n.succ) ⟨i, i_lt⟩ : Fin n.succ)
    ((c.boundaries.orderEmbOfFin ⋯ : (a : Fin (c.length + 1)) → Fin (n + 1)) ⟨i, i_lt''⟩ : Fin (n + 1))
B : c.sizeUpTo i = (↑((c.boundary : (a : Fin (c.length + 1)) → Fin (n + 1)) ⟨i, i_lt''⟩) : ℕ)
rw :
  (↑((d.boundary : (a : Fin d.boundaries.card) → Fin (n + 1)) (⟨i, i_lt⟩ : Fin d.boundaries.card)) : ℕ) =
    (take i c.blocks).sum
rw₁ :
  (↑((d.boundaries.orderEmbOfFin ⋯ : (a : Fin d.boundaries.card) → Fin (n + 1)) (⟨i, i_lt⟩ : Fin d.boundaries.card)) :
      ℕ) =
    (take i c.blocks).sum
rw₂ :
  (↑((d.boundaries.orderEmbOfFin ⋯ : (a : Fin d.boundaries.card) → Fin (n + 1)) (⟨i, i_lt⟩ : Fin d.boundaries.card)) :
      ℕ) =
    c.sizeUpTo i
rw₃ :
  (↑((d.boundaries.orderEmbOfFin ⋯ : (a : Fin d.boundaries.card) → Fin (n + 1)) (⟨i, i_lt⟩ : Fin d.boundaries.card)) :
      ℕ) =
    (↑((c.boundary : (a : Fin (c.length + 1)) → Fin (n + 1)) ⟨i, i_lt''⟩) : ℕ)
rw₄ :
  (↑((c.boundaries.orderEmbOfFin ⋯ : (a : Fin (c.length + 1)) → Fin (n + 1)) (⟨i, i_lt''⟩ : Fin (c.length + 1))) : ℕ) =
    (↑((c.boundary : (a : Fin (c.length + 1)) → Fin (n + 1)) ⟨i, i_lt''⟩) : ℕ)
rw₅ rw₆ :
  (↑((c.boundary : (a : Fin (c.length + 1)) → Fin (n + 1)) (⟨i, i_lt''⟩ : Fin (c.length + 1))) : ℕ) =
    (↑((c.boundary : (a : Fin (c.length + 1)) → Fin (n + 1)) ⟨i, i_lt''⟩) : ℕ)
⊢ (take i d.blocks).sum = (take i c.blocks).sum

Tactic:
rw [d.blocks_partial_sum i_lt, CompositionAsSet.boundary, ← Composition.sizeUpTo, B, A,
    c.orderEmbOfFin_boundaries]

Premises used: Composition.orderEmbOfFin_boundaries, CompositionAsSet.boundary, CompositionAsSet.blocks_partial_sum, Composition.sizeUpTo
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
⊢ c.toComposition.blocks = c.blocks

Tactic:
rfl

Premises used: List.ofFn, CompositionAsSet.blocks, rfl
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
h :
  ∀ (j : ℕ) (hj : j < n + 1),
    (⟨j, hj⟩ : Fin (n + 1)) ∈ c.toComposition.boundaries ↔ (⟨j, hj⟩ : Fin (n + 1)) ∈ c.boundaries
⊢ c.toComposition.boundaries = c.boundaries

Tactic:
ext ⟨j, hj⟩
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
j : ℕ
hj : j < n + 1
⊢ (⟨j, hj⟩ : Fin (n + 1)) ∈ c.toComposition.boundaries ↔ (⟨j, hj⟩ : Fin (n + 1)) ∈ c.boundaries

Tactic:
simp [c.mem_boundaries_iff_exists_blocks_sum_take_eq, Composition.boundaries,
    c.card_boundaries_eq_succ_length, Composition.boundary, Composition.sizeUpTo, Fin.exists_iff]

Premises used: CompositionAsSet.card_boundaries_eq_succ_length, Composition.boundaries, CompositionAsSet.mem_boundaries_iff_exists_blocks_sum_take_eq, Fin.exists_iff, Composition.boundary, Composition.sizeUpTo
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
⊢ c.toCompositionAsSet.boundaries = c.boundaries

Tactic:
rfl

Premises used: Finset.map, Composition.boundaries, rfl
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 n : ℕ
c : Composition n
blocks :
  Composition.blocks (n := n)
      ((fun (c : CompositionAsSet n) ↦ c.toComposition) ((fun (c : Composition n) ↦ c.toCompositionAsSet) c)) =
    c.blocks
⊢ (fun (c : CompositionAsSet n) ↦ c.toComposition) ((fun (c : Composition n) ↦ c.toCompositionAsSet) c) = c

Tactic:
ext1
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 n : ℕ
c : Composition n
⊢ Composition.blocks (n := n)
      ((fun (c : CompositionAsSet n) ↦ c.toComposition) ((fun (c : Composition n) ↦ c.toCompositionAsSet) c)) =
    c.blocks

Tactic:
c.toCompositionAsSet_blocks

Premises used: List.ofFn, CompositionAsSet.blocks, Composition.toCompositionAsSet_blocks
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 n : ℕ
c : Composition n
⊢ Composition.blocks (n := n)
      ((fun (c : CompositionAsSet n) ↦ c.toComposition) ((fun (c : Composition n) ↦ c.toCompositionAsSet) c)) =
    c.blocks

Tactic:
exact c.toCompositionAsSet_blocks

Premises used: Composition.toCompositionAsSet_blocks
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 n : ℕ
c : CompositionAsSet n
boundaries :
  CompositionAsSet.boundaries
      ((fun (c : Composition n) ↦ c.toCompositionAsSet) ((fun (c : CompositionAsSet n) ↦ c.toComposition) c)) =
    c.boundaries
⊢ (fun (c : Composition n) ↦ c.toCompositionAsSet) ((fun (c : CompositionAsSet n) ↦ c.toComposition) c) = c

Tactic:
ext1
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 n : ℕ
c : CompositionAsSet n
⊢ CompositionAsSet.boundaries
      ((fun (c : Composition n) ↦ c.toCompositionAsSet) ((fun (c : CompositionAsSet n) ↦ c.toComposition) c)) =
    c.boundaries

Tactic:
c.toComposition_boundaries

Premises used: Finset.map, Composition.boundaries, CompositionAsSet.toComposition_boundaries
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 n : ℕ
c : CompositionAsSet n
⊢ CompositionAsSet.boundaries
      ((fun (c : Composition n) ↦ c.toCompositionAsSet) ((fun (c : CompositionAsSet n) ↦ c.toComposition) c)) =
    c.boundaries

Tactic:
exact c.toComposition_boundaries

Premises used: CompositionAsSet.toComposition_boundaries