awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
i : Fin c.length
y : Fin (c.blocksFun i)
h : (↑(c.invEmbedding ((c.embedding i : (a : Fin (c.blocksFun i)) → Fin n) y)) : ℕ) = (↑y : ℕ)
⊢ HEq (α := Fin (c.blocksFun (c.index ((c.embedding i : (a : Fin (c.blocksFun i)) → Fin n) y))))
    (c.invEmbedding ((c.embedding i : (a : Fin (c.blocksFun i)) → Fin n) y)) y
have h₁ : c.blocksFun (c.index ((c.embedding i : (a : Fin (c.blocksFun i)) → Fin n) y)) = c.blocksFun i
Tactic: rw [Fin.heq_ext_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
i : Fin c.length
y : Fin (c.blocksFun i)
⊢ c.blocksFun (c.index ((c.embedding i : (a : Fin (c.blocksFun i)) → Fin n) y)) = c.blocksFun i
have h : c.blocksFun i = c.blocksFun i
Tactic: rw [c.index_embedding]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n₁ n₂ : ℕ
c₁ : Composition n₁
c₂ : Composition n₂
i₁ : Fin c₁.length
i₂ : Fin c₂.length
hn : n₁ = n₂
hc : c₁.blocks = c₂.blocks
hi : (↑i₁ : ℕ) = (↑i₂ : ℕ)
⊢ c₁.blocksFun i₁ = c₂.blocksFun i₂
have refl : ∀ (c₂ : Composition n₁) (i₂ : Fin c₂.length) (hc : c₁.blocks = c₂.blocks) (hi : (↑i₁ : ℕ) = (↑i₂ : ℕ)),
  c₁.blocksFun i₁ = c₂.blocksFun i₂
Tactic: cases hn
Cleared hypotheses: n₂, c₂, i₂, hn, hc, hi
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (hypothesis)
Goal:
n₁ : ℕ
c₁ : Composition n₁
i₁ : Fin c₁.length
c₂ : Composition n₁
i₂ : Fin c₂.length
hc : c₁.blocks = c₂.blocks
hi : (↑i₁ : ℕ) = (↑i₂ : ℕ)
⊢ c₁.blocksFun i₁ = c₂.blocksFun i₂
have hc₁ : c₁ = c₂
Tactic: rw [← Composition.ext_iff] at hc
Cleared hypotheses: hc, hi
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n₁ : ℕ
c₁ : Composition n₁
i₁ : Fin c₁.length
c₂ : Composition n₁
i₂ : Fin c₂.length
hc : c₁ = c₂
hi : (↑i₁ : ℕ) = (↑i₂ : ℕ)
⊢ c₁.blocksFun i₁ = c₂.blocksFun i₂
have refl : ∀ (i₂ : Fin c₁.length) (hi : (↑i₁ : ℕ) = (↑i₂ : ℕ)), c₁.blocksFun i₁ = c₁.blocksFun i₂
Tactic: cases hc
Cleared hypotheses: c₂, i₂, hc, hi
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n₁ : ℕ
c₁ : Composition n₁
i₁ i₂ : Fin c₁.length
hi : (↑i₁ : ℕ) = (↑i₂ : ℕ)
⊢ c₁.blocksFun i₁ = c₁.blocksFun i₂
have refl : i₁ = i₂
Tactic: congr
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
c c' : (n : ℕ) × Composition n
H : c = c'
⊢ c.snd (β := fun (n : ℕ) ↦ Composition n).blocks = c'.snd (β := fun (n : ℕ) ↦ Composition n).blocks
have rw : c'.snd (β := fun (n : ℕ) ↦ Composition n).blocks = c'.snd (β := fun (n : ℕ) ↦ Composition n).blocks
Tactic: rw [H]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
c c' : (n : ℕ) × Composition n
⊢ c = c' ↔ c.snd (β := fun (n : ℕ) ↦ Composition n).blocks = c'.snd (β := fun (n : ℕ) ↦ Composition n).blocks
have refine : ∀ (H : c.snd (β := fun (n : ℕ) ↦ Composition n).blocks = c'.snd (β := fun (n : ℕ) ↦ Composition n).blocks), c = c'
Tactic: refine ⟨fun H => by rw [H], fun H => ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
c c' : (n : ℕ) × Composition n
H : c.snd (β := fun (n : ℕ) ↦ Composition n).blocks = c'.snd (β := fun (n : ℕ) ↦ Composition n).blocks
⊢ c = c'
have rcases : ∀ (n : ℕ) (c : Composition n)
  (H :
    (Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c).snd (β := fun (n : ℕ) ↦ Composition n).blocks =
      c'.snd (β := fun (n : ℕ) ↦ Composition n).blocks),
  Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c = c'
Tactic: rcases c with ⟨n, c⟩
Cleared hypotheses: c, H
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
c' : (n : ℕ) × Composition n
n : ℕ
c : Composition n
H :
  (Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c).snd (β := fun (n : ℕ) ↦ Composition n).blocks =
    c'.snd (β := fun (n : ℕ) ↦ Composition n).blocks
⊢ Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c = c'
have rcases : ∀ (n' : ℕ) (c' : Composition n')
  (H :
    (Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c).snd (β := fun (n : ℕ) ↦ Composition n).blocks =
      (Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n' c').snd (β := fun (n : ℕ) ↦ Composition n).blocks),
  Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c = Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n' c'
Tactic: rcases c' with ⟨n', c'⟩
Cleared hypotheses: c', H
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
n' : ℕ
c' : Composition n'
H :
  (Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c).snd (β := fun (n : ℕ) ↦ Composition n).blocks =
    (Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n' c').snd (β := fun (n : ℕ) ↦ Composition n).blocks
⊢ n = n'
have rw : c.blocks.sum = n'
Tactic: rw [← c.blocks_sum, ← c'.blocks_sum, H]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
n' : ℕ
c' : Composition n'
H :
  (Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c).snd (β := fun (n : ℕ) ↦ Composition n).blocks =
    (Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n' c').snd (β := fun (n : ℕ) ↦ Composition n).blocks
rw : c.blocks.sum = n'
⊢ n = n'
have rw₁ : c.blocks.sum = c'.blocks.sum
Tactic: rw [← c.blocks_sum, ← c'.blocks_sum, H]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
n' : ℕ
c' : Composition n'
H :
  (Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c).snd (β := fun (n : ℕ) ↦ Composition n).blocks =
    (Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n' c').snd (β := fun (n : ℕ) ↦ Composition n).blocks
rw : c.blocks.sum = n'
rw₁ : c.blocks.sum = c'.blocks.sum
⊢ n = n'
have rw₂ : (Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n' c').snd (β := fun (n : ℕ) ↦ Composition n).blocks.sum = c'.blocks.sum
Tactic: rw [← c.blocks_sum, ← c'.blocks_sum, H]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (hypothesis)
Goal:
n : ℕ
c : Composition n
n' : ℕ
c' : Composition n'
H :
  (Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c).snd (β := fun (n : ℕ) ↦ Composition n).blocks =
    (Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n' c').snd (β := fun (n : ℕ) ↦ Composition n).blocks
⊢ Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c = Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n' c'
have this : n = n'
Tactic: have : n = n' := by rw [← c.blocks_sum, ← c'.blocks_sum, H]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
n' : ℕ
c' : Composition n'
H :
  (Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c).snd (β := fun (n : ℕ) ↦ Composition n).blocks =
    (Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n' c').snd (β := fun (n : ℕ) ↦ Composition n).blocks
this : n = n'
⊢ Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c = Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n' c'
have refl : ∀ (c' : Composition n)
  (H :
    (Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c).snd (β := fun (n : ℕ) ↦ Composition n).blocks =
      (Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c').snd (β := fun (n : ℕ) ↦ Composition n).blocks),
  Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c = Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c'
Tactic: induction this
Cleared hypotheses: c', H, this
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
n' : ℕ
c' : Composition n
H :
  (Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c).snd (β := fun (n : ℕ) ↦ Composition n).blocks =
    (Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c').snd (β := fun (n : ℕ) ↦ Composition n).blocks
⊢ Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c = Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c'
have refl : c = c'
Tactic: congr
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
n' : ℕ
c' : Composition n
H :
  (Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c).snd (β := fun (n : ℕ) ↦ Composition n).blocks =
    (Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c').snd (β := fun (n : ℕ) ↦ Composition n).blocks
⊢ c = c'
have refl : c.blocks = c'.blocks
Tactic: ext1
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
i : Fin (ones n).length
h : 0 < (ones n).blocksFun i
⊢ ((ones n).embedding i : (a : Fin ((ones n).blocksFun i)) → Fin n) ⟨0, h⟩ = (⟨(↑i : ℕ), ⋯⟩ : Fin n)
have h₁ : (↑(((ones n).embedding i : (a : Fin ((ones n).blocksFun i)) → Fin n) (⟨0, h⟩ : Fin ((ones n).blocksFun i))) : ℕ) =
  (↑(⟨(↑i : ℕ), sorry⟩ : Fin n) : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
⊢ c = ones n ↔ ∀ i ∈ c.blocks, i = 1
have mp : c = ones n → ∀ i ∈ c.blocks, i = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
mp : c = ones n → ∀ i ∈ c.blocks, i = 1
⊢ c = ones n ↔ ∀ i ∈ c.blocks, i = 1
have mpr : (∀ i ∈ c.blocks, i = 1) → c = ones n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
H : ∀ i ∈ c.blocks, i = 1
⊢ c = ones n
have mpr : c.blocks = (ones n).blocks
Tactic: ext1
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (hypothesis)
Goal:
n : ℕ
c : Composition n
H : ∀ i ∈ c.blocks, i = 1
⊢ c.blocks = (ones n).blocks
have A : c.blocks = replicate c.blocks.length 1
Tactic: have A : c.blocks = replicate c.blocks.length 1 := eq_replicate_of_mem H
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
H : ∀ i ∈ c.blocks, i = 1
A : c.blocks = replicate c.blocks.length 1
| n
have rw : sum (replicate c.blocks.length 1)
Tactic: rw [← c.blocks_sum, A]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
H : ∀ i ∈ c.blocks, i = 1
A : c.blocks = replicate c.blocks.length 1
⊢ c.blocks.length = n
have conv_rhs : c.blocks.length = sum (replicate c.blocks.length 1)
Tactic: conv_rhs => rw [← c.blocks_sum, A]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (hypothesis)
Goal:
n : ℕ
c : Composition n
H : ∀ i ∈ c.blocks, i = 1
A : c.blocks = replicate c.blocks.length 1
⊢ c.blocks = (ones n).blocks
have this : c.blocks.length = n
Tactic: have : c.blocks.length = n := by
      conv_rhs => rw [← c.blocks_sum, A]
      simp
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
H : ∀ i ∈ c.blocks, i = 1
A : c.blocks = replicate c.blocks.length 1
this : c.blocks.length = n
⊢ c.blocks = (ones n).blocks
have mpr : replicate c.blocks.length 1 = (ones n).blocks
Tactic: rw [A, this, ones_blocks]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
H : ∀ i ∈ c.blocks, i = 1
A : c.blocks = replicate c.blocks.length 1
this : c.blocks.length = n
mpr : replicate c.blocks.length 1 = (ones n).blocks
⊢ c.blocks = (ones n).blocks
have mpr₁ : replicate n 1 = (ones n).blocks
Tactic: rw [A, this, ones_blocks]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
H : ∀ i ∈ c.blocks, i = 1
A : c.blocks = replicate c.blocks.length 1
this : c.blocks.length = n
mpr : replicate c.blocks.length 1 = (ones n).blocks
mpr₁ : replicate n 1 = (ones n).blocks
⊢ c.blocks = (ones n).blocks
have mpr₂ : Eq (α := List ℕ) (replicate n 1) (replicate n 1)
Tactic: rw [A, this, ones_blocks]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
⊢ c ≠ ones n ↔ ∃ i ∈ c.blocks, 1 < i
have refine : (¬∀ i ∈ c.blocks, i = 1) ↔ ∃ i ∈ c.blocks, 1 < i
Tactic: refine (not_congr eq_ones_iff).trans ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (hypothesis)
Goal:
n : ℕ
c : Composition n
⊢ (¬∀ i ∈ c.blocks, i = 1) ↔ ∃ i ∈ c.blocks, 1 < i
have this : ∀ j ∈ c.blocks, j = 1 ↔ j ≤ 1
Tactic: have : ∀ j ∈ c.blocks, j = 1 ↔ j ≤ 1 := fun j hj => by simp [le_antisymm_iff, c.one_le_blocks hj]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
⊢ c = ones n ↔ c.length = n
have mp : c = ones n → c.length = n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
mp : c = ones n → c.length = n
⊢ c = ones n ↔ c.length = n
have mpr : c.length = n → c = ones n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
⊢ c.length = n → c = ones n
have mpr : ¬c = ones n → ¬c.length = n
Tactic: contrapose
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
⊢ False
have mpr : n < n
Tactic: apply lt_irrefl n
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
⊢ LT.lt (α := ℕ) (∑ i : Fin c.length, 1) (∑ i : Fin c.length, c.blocksFun i)
have obtain : ∀ (i : ℕ) (hi : i ∈ c.blocks) (i_blocks : 1 < i),
  LT.lt (α := ℕ) (∑ i : Fin c.length, 1) (∑ i : Fin c.length, c.blocksFun i)
Tactic: obtain ⟨i, hi, i_blocks⟩ : ∃ i ∈ c.blocks, 1 < i := ne_ones_iff.1 H
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (hypothesis)
Goal:
n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
i : ℕ
hi : i ∈ c.blocks
i_blocks : 1 < i
⊢ LT.lt (α := ℕ) (∑ i : Fin c.length, 1) (∑ i : Fin c.length, c.blocksFun i)
have hi₁ : ∃ (y : Fin c.length), c.blocksFun y = i
Tactic: rw [← ofFn_blocksFun, mem_ofFn' c.blocksFun, Set.mem_range] at hi
Cleared hypotheses: hi, i_blocks
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
i : ℕ
hi : ∃ (y : Fin c.length), c.blocksFun y = i
i_blocks : 1 < i
⊢ LT.lt (α := ℕ) (∑ i : Fin c.length, 1) (∑ i : Fin c.length, c.blocksFun i)
have obtain : ∀ (j : Fin c.length) (hj : c.blocksFun j = i),
  LT.lt (α := ℕ) (∑ i : Fin c.length, 1) (∑ i : Fin c.length, c.blocksFun i)
Tactic: obtain ⟨j : Fin c.length, hj : c.blocksFun j = i⟩ := hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (hypothesis)
Goal:
n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
i : ℕ
i_blocks : 1 < i
j : Fin c.length
hj : c.blocksFun j = i
⊢ LT.lt (α := ℕ) (∑ i : Fin c.length, 1) (∑ i : Fin c.length, c.blocksFun i)
have i_blocks₁ : 1 < c.blocksFun j
Tactic: rw [← hj] at i_blocks
Cleared hypotheses: i_blocks, hj
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
⊢ LT.lt (α := ℕ) (∑ i : Fin c.length, 1) (∑ i : Fin c.length, c.blocksFun i)
have obtain : ∀ (i : ℕ) (hi : i ∈ c.blocks) (i_blocks : 1 < i),
  LT.lt (α := ℕ) (∑ i : Fin c.length, 1) (∑ i : Fin c.length, c.blocksFun i)
Tactic: {
        obtain ⟨i, hi, i_blocks⟩ : ∃ i ∈ c.blocks, 1 < i := ne_ones_iff.1 H
        rw [← ofFn_blocksFun, mem_ofFn' c.blocksFun, Set.mem_range] at hi
        obtain ⟨j : Fin c.length, hj : c.blocksFun j = i⟩ := hi
        rw [← hj] at i_blocks
        exact Finset.sum_lt_sum (fun i _ => one_le_blocksFun c i) ⟨j, Finset.mem_univ _, i_blocks⟩
        }
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
obtain :
  ∀ (i : ℕ) (hi : i ∈ c.blocks) (i_blocks : 1 < i),
    LT.lt (α := ℕ) (∑ i : Fin c.length, 1) (∑ i : Fin c.length, c.blocksFun i)
⊢ LT.lt (α := ℕ) (∑ i : Fin c.length, 1) (∑ i : Fin c.length, c.blocksFun i)
have obtain₁ : ∀ (i : ℕ) (hi : ∃ (y : Fin c.length), c.blocksFun y = i) (i_blocks : 1 < i),
  LT.lt (α := ℕ) (∑ i : Fin c.length, 1) (∑ i : Fin c.length, c.blocksFun i)
Tactic: {
        obtain ⟨i, hi, i_blocks⟩ : ∃ i ∈ c.blocks, 1 < i := ne_ones_iff.1 H
        rw [← ofFn_blocksFun, mem_ofFn' c.blocksFun, Set.mem_range] at hi
        obtain ⟨j : Fin c.length, hj : c.blocksFun j = i⟩ := hi
        rw [← hj] at i_blocks
        exact Finset.sum_lt_sum (fun i _ => one_le_blocksFun c i) ⟨j, Finset.mem_univ _, i_blocks⟩
        }
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
obtain :
  ∀ (i : ℕ) (hi : i ∈ c.blocks) (i_blocks : 1 < i),
    LT.lt (α := ℕ) (∑ i : Fin c.length, 1) (∑ i : Fin c.length, c.blocksFun i)
obtain₁ :
  ∀ (i : ℕ) (hi : ∃ (y : Fin c.length), c.blocksFun y = i) (i_blocks : 1 < i),
    LT.lt (α := ℕ) (∑ i : Fin c.length, 1) (∑ i : Fin c.length, c.blocksFun i)
⊢ LT.lt (α := ℕ) (∑ i : Fin c.length, 1) (∑ i : Fin c.length, c.blocksFun i)
have obtain₂ : ∀ (i : ℕ) (i_blocks : 1 < i) (j : Fin c.length) (hj : c.blocksFun j = i),
  LT.lt (α := ℕ) (∑ i : Fin c.length, 1) (∑ i : Fin c.length, c.blocksFun i)
Tactic: {
        obtain ⟨i, hi, i_blocks⟩ : ∃ i ∈ c.blocks, 1 < i := ne_ones_iff.1 H
        rw [← ofFn_blocksFun, mem_ofFn' c.blocksFun, Set.mem_range] at hi
        obtain ⟨j : Fin c.length, hj : c.blocksFun j = i⟩ := hi
        rw [← hj] at i_blocks
        exact Finset.sum_lt_sum (fun i _ => one_le_blocksFun c i) ⟨j, Finset.mem_univ _, i_blocks⟩
        }
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
obtain :
  ∀ (i : ℕ) (hi : i ∈ c.blocks) (i_blocks : 1 < i),
    LT.lt (α := ℕ) (∑ i : Fin c.length, 1) (∑ i : Fin c.length, c.blocksFun i)
obtain₁ :
  ∀ (i : ℕ) (hi : ∃ (y : Fin c.length), c.blocksFun y = i) (i_blocks : 1 < i),
    LT.lt (α := ℕ) (∑ i : Fin c.length, 1) (∑ i : Fin c.length, c.blocksFun i)
obtain₂ :
  ∀ (i : ℕ) (i_blocks : 1 < i) (j : Fin c.length) (hj : c.blocksFun j = i),
    LT.lt (α := ℕ) (∑ i : Fin c.length, 1) (∑ i : Fin c.length, c.blocksFun i)
⊢ LT.lt (α := ℕ) (∑ i : Fin c.length, 1) (∑ i : Fin c.length, c.blocksFun i)
have obtain₃ : ∀ (i : ℕ) (j : Fin c.length) (i_blocks : 1 < c.blocksFun j) (hj : c.blocksFun j = i),
  LT.lt (α := ℕ) (∑ i : Fin c.length, 1) (∑ i : Fin c.length, c.blocksFun i)
Tactic: {
        obtain ⟨i, hi, i_blocks⟩ : ∃ i ∈ c.blocks, 1 < i := ne_ones_iff.1 H
        rw [← ofFn_blocksFun, mem_ofFn' c.blocksFun, Set.mem_range] at hi
        obtain ⟨j : Fin c.length, hj : c.blocksFun j = i⟩ := hi
        rw [← hj] at i_blocks
        exact Finset.sum_lt_sum (fun i _ => one_le_blocksFun c i) ⟨j, Finset.mem_univ _, i_blocks⟩
        }
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
⊢ n < n
have n₁ : n = ∑ i : Fin c.length, 1
Tactic: calc
      n = ∑ i : Fin c.length, 1 := by simp [length_n]
      _ < ∑ i : Fin c.length, c.blocksFun i := by
        {
        obtain ⟨i, hi, i_blocks⟩ : ∃ i ∈ c.blocks, 1 < i := ne_ones_iff.1 H
        rw [← ofFn_blocksFun, mem_ofFn' c.blocksFun, Set.mem_range] at hi
        obtain ⟨j : Fin c.length, hj : c.blocksFun j = i⟩ := hi
        rw [← hj] at i_blocks
        exact Finset.sum_lt_sum (fun i _ => one_le_blocksFun c i) ⟨j, Finset.mem_univ _, i_blocks⟩
        }
      _ = n := c.sum_blocksFun
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
n₁ : n = ∑ i : Fin c.length, 1
⊢ n < n
have n₂ : LT.lt (α := ℕ) (∑ i : Fin c.length, 1) (∑ i : Fin c.length, c.blocksFun i)
Tactic: calc
      n = ∑ i : Fin c.length, 1 := by simp [length_n]
      _ < ∑ i : Fin c.length, c.blocksFun i := by
        {
        obtain ⟨i, hi, i_blocks⟩ : ∃ i ∈ c.blocks, 1 < i := ne_ones_iff.1 H
        rw [← ofFn_blocksFun, mem_ofFn' c.blocksFun, Set.mem_range] at hi
        obtain ⟨j : Fin c.length, hj : c.blocksFun j = i⟩ := hi
        rw [← hj] at i_blocks
        exact Finset.sum_lt_sum (fun i _ => one_le_blocksFun c i) ⟨j, Finset.mem_univ _, i_blocks⟩
        }
      _ = n := c.sum_blocksFun
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
h : 0 < n
i : Fin n
⊢ ((single n h).embedding 0 : (a : Fin ((single n h).blocksFun 0)) → Fin n) i = i
have h₁ : (↑(((single n h).embedding 0 : (a : Fin ((single n h).blocksFun 0)) → Fin n) i) : ℕ) = (↑i : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
h : 0 < n
c : Composition n
⊢ c = single n h ↔ c.length = 1
have mp : c = single n h → c.length = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
h : 0 < n
c : Composition n
mp : c = single n h → c.length = 1
⊢ c = single n h ↔ c.length = 1
have mpr : c.length = 1 → c = single n h
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
h : 0 < n
c : Composition n
H : c = single n h
⊢ c.length = 1
have mp : (single n h).length = 1
Tactic: rw [H]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
h : 0 < n
c : Composition n
H : c.length = 1
⊢ c = single n h
have mpr : c.blocks = (single n h).blocks
Tactic: ext1
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (hypothesis)
Goal:
n : ℕ
h : 0 < n
c : Composition n
H : c.length = 1
⊢ c.blocks = (single n h).blocks
have A : c.blocks.length = 1
Tactic: have A : c.blocks.length = 1 := H ▸ c.blocks_length
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (hypothesis)
Goal:
n : ℕ
h : 0 < n
c : Composition n
H : c.length = 1
A : c.blocks.length = 1
⊢ c.blocks = (single n h).blocks
have B : c.blocks.sum = n
Tactic: have B : c.blocks.sum = n := c.blocks_sum
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
h : 0 < n
c : Composition n
H : c.length = 1
A : c.blocks.length = 1
B : c.blocks.sum = n
⊢ c.blocks = (single n h).blocks
have mpr : ∀ (B : [c.blocks.get (⟨0, sorry⟩ : Fin c.blocks.length)].sum = n),
  [c.blocks.get (⟨0, sorry⟩ : Fin c.blocks.length)] = (single n h).blocks
Tactic: rw [eq_cons_of_length_one A] at B ⊢
Cleared hypotheses: B
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
hn : 0 < n
c : Composition n
⊢ c ≠ single n hn ↔ ∀ (i : Fin c.length), c.blocksFun i < n
have contrapose! : c = single n hn ↔ ∃ (i : Fin c.length), n ≤ c.blocksFun i
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
hn : 0 < n
c : Composition n
⊢ c = single n hn ↔ ∃ (i : Fin c.length), n ≤ c.blocksFun i
have mp : c = single n hn → ∃ (i : Fin c.length), n ≤ c.blocksFun i
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
hn : 0 < n
c : Composition n
mp : c = single n hn → ∃ (i : Fin c.length), n ≤ c.blocksFun i
⊢ c = single n hn ↔ ∃ (i : Fin c.length), n ≤ c.blocksFun i
have mpr : (∃ (i : Fin c.length), n ≤ c.blocksFun i) → c = single n hn
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
hn : 0 < n
c : Composition n
i : Fin c.length
hi : n ≤ c.blocksFun i
⊢ c = single n hn
have mpr : c.length = 1
Tactic: rw [eq_single_iff_length]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
hn : 0 < n
c : Composition n
i : Fin c.length
hi : n ≤ c.blocksFun i
j : Fin c.length
⊢ j = i
have by_contra : ∀ (ji : ¬j = i), False
Tactic: by_contra ji
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
hn : 0 < n
c : Composition n
i : Fin c.length
hi : n ≤ c.blocksFun i
j : Fin c.length
ji : ¬j = i
⊢ False
have apply : LT.lt (α := ℕ) (∑ k : Fin c.length, c.blocksFun k) (∑ k : Fin c.length, c.blocksFun k)
Tactic: apply lt_irrefl (∑ k, c.blocksFun k)