awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
x : (i : Fin c.length) × Fin (c.blocksFun i)
rcases :
  ∀ (i : Fin c.length) (y : Fin (c.blocksFun i)),
    Eq (α := (i : Fin c.length) × Fin (c.blocksFun i))
      ((fun (j : Fin n) ↦
          (Sigma.mk (β := fun (i : Fin c.length) ↦ Fin (c.blocksFun i)) (c.index j) (c.invEmbedding j) :
            (i : Fin c.length) × Fin (c.blocksFun i)))
        ((fun (x : (i : Fin c.length) × Fin (c.blocksFun i)) ↦
            ((c.embedding (x.fst (β := fun (i : Fin c.length) ↦ Fin (c.blocksFun i))) :
                  (a : Fin (c.blocksFun x.fst)) → Fin n)
                (x.snd (β := fun (i : Fin c.length) ↦ Fin (c.blocksFun i))) :
              Fin n))
          (Sigma.mk (β := fun (i : Fin c.length) ↦ Fin (c.blocksFun i)) i y)))
      (Sigma.mk (β := fun (i : Fin c.length) ↦ Fin (c.blocksFun i)) i y)
⊢ (fun (j : Fin n) ↦
        (Sigma.mk (β := fun (i : Fin c.length) ↦ Fin (c.blocksFun i)) (c.index j) (c.invEmbedding j) :
          (i : Fin c.length) × Fin (c.blocksFun i)))
      ((fun (x : (i : Fin c.length) × Fin (c.blocksFun i)) ↦
          ((c.embedding (x.fst (β := fun (i : Fin c.length) ↦ Fin (c.blocksFun i))) :
                (a : Fin (c.blocksFun x.fst)) → Fin n)
              (x.snd (β := fun (i : Fin c.length) ↦ Fin (c.blocksFun i))) :
            Fin n))
        x) =
    x

Tactic:
rcases x with ⟨i, y⟩
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
i : Fin c.length
y : Fin (c.blocksFun i)
dsimp :
  Eq (α := (i : Fin c.length) × Fin (c.blocksFun i))
    (Sigma.mk (β := fun (i : Fin c.length) ↦ Fin (c.blocksFun i))
      (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)))
    (Sigma.mk (β := fun (i : Fin c.length) ↦ Fin (c.blocksFun i)) i y)
⊢ Eq (α := (i : Fin c.length) × Fin (c.blocksFun i))
    ((fun (j : Fin n) ↦
        (Sigma.mk (β := fun (i : Fin c.length) ↦ Fin (c.blocksFun i)) (c.index j) (c.invEmbedding j) :
          (i : Fin c.length) × Fin (c.blocksFun i)))
      ((fun (x : (i : Fin c.length) × Fin (c.blocksFun i)) ↦
          ((c.embedding (x.fst (β := fun (i : Fin c.length) ↦ Fin (c.blocksFun i))) :
                (a : Fin (c.blocksFun x.fst)) → Fin n)
              (x.snd (β := fun (i : Fin c.length) ↦ Fin (c.blocksFun i))) :
            Fin n))
        (Sigma.mk (β := fun (i : Fin c.length) ↦ Fin (c.blocksFun i)) i y)))
    (Sigma.mk (β := fun (i : Fin c.length) ↦ Fin (c.blocksFun i)) i y)

Tactic:
dsimp
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
i : Fin c.length
y : Fin (c.blocksFun i)
h : c.index ((c.embedding i : (a : Fin (c.blocksFun i)) → Fin n) y) = i
h₁ :
  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
⊢ Eq (α := (i : Fin c.length) × Fin (c.blocksFun i))
    (Sigma.mk (β := fun (i : Fin c.length) ↦ Fin (c.blocksFun i))
      (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)))
    (Sigma.mk (β := fun (i : Fin c.length) ↦ Fin (c.blocksFun i)) i y)

Tactic:
congr
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
i : Fin c.length
y : Fin (c.blocksFun i)
⊢ c.index ((c.embedding i : (a : Fin (c.blocksFun i)) → Fin n) y) = i

Tactic:
c.index_embedding _ _

Premises used: Composition.index_embedding
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
i : Fin c.length
y : Fin (c.blocksFun i)
⊢ c.index ((c.embedding i : (a : Fin (c.blocksFun i)) → Fin n) y) = i

Tactic:
exact c.index_embedding _ _

Premises used: Composition.index_embedding
-- Module: Mathlib.Combinatorics.Enumerative.Composition
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 : ℕ)
h₁ : c.blocksFun (c.index ((c.embedding i : (a : Fin (c.blocksFun i)) → Fin n) y)) = c.blocksFun i
⊢ 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

Tactic:
rw [Fin.heq_ext_iff]

Premises used: Fin.heq_ext_iff
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
i : Fin c.length
y : Fin (c.blocksFun i)
⊢ (↑(c.invEmbedding ((c.embedding i : (a : Fin (c.blocksFun i)) → Fin n) y)) : ℕ) = (↑y : ℕ)

Tactic:
c.invEmbedding_comp _ _

Premises used: Composition.invEmbedding_comp
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
i : Fin c.length
y : Fin (c.blocksFun i)
⊢ (↑(c.invEmbedding ((c.embedding i : (a : Fin (c.blocksFun i)) → Fin n) y)) : ℕ) = (↑y : ℕ)

Tactic:
exact c.invEmbedding_comp _ _

Premises used: Composition.invEmbedding_comp
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
i : Fin c.length
y : Fin (c.blocksFun i)
h h₁ : c.blocksFun i = c.blocksFun i
⊢ c.blocksFun (c.index ((c.embedding i : (a : Fin (c.blocksFun i)) → Fin n) y)) = c.blocksFun i

Tactic:
rw [c.index_embedding]

Premises used: Composition.index_embedding
-- Module: Mathlib.Combinatorics.Enumerative.Composition
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₂ : ℕ)
refl :
  ∀ (c₂ : Composition n₁) (i₂ : Fin c₂.length) (hc : c₁.blocks = c₂.blocks) (hi : (↑i₁ : ℕ) = (↑i₂ : ℕ)),
    c₁.blocksFun i₁ = c₂.blocksFun i₂
⊢ c₁.blocksFun i₁ = c₂.blocksFun i₂

Tactic:
cases hn
-- Module: Mathlib.Combinatorics.Enumerative.Composition
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₁ = c₂

Tactic:
rw [← Composition.ext_iff] at hc

Premises used: Composition.ext_iff
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n₁ : ℕ
c₁ : Composition n₁
i₁ : Fin c₁.length
c₂ : Composition n₁
i₂ : Fin c₂.length
hc : c₁.blocks = c₂.blocks
hi : (↑i₁ : ℕ) = (↑i₂ : ℕ)
hc₁ : c₁ = c₂
⊢ (↑i₁ : ℕ) = (↑i₂ : ℕ)

Tactic:
rw [← Composition.ext_iff] at hc

Premises used: Composition.ext_iff
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n₁ : ℕ
c₁ : Composition n₁
i₁ : Fin c₁.length
c₂ : Composition n₁
i₂ : Fin c₂.length
hc : c₁ = c₂
hi : (↑i₁ : ℕ) = (↑i₂ : ℕ)
refl : ∀ (i₂ : Fin c₁.length) (hi : (↑i₁ : ℕ) = (↑i₂ : ℕ)), c₁.blocksFun i₁ = c₁.blocksFun i₂
⊢ c₁.blocksFun i₁ = c₂.blocksFun i₂

Tactic:
cases hc
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n₁ : ℕ
c₁ : Composition n₁
i₁ i₂ : Fin c₁.length
hi : (↑i₁ : ℕ) = (↑i₂ : ℕ)
refl : i₁ = i₂
⊢ c₁.blocksFun i₁ = c₁.blocksFun i₂

Tactic:
congr
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n₁ : ℕ
c₁ : Composition n₁
i₁ i₂ : Fin c₁.length
hi refl refl₁ refl₂ refl₃ : (↑i₁ : ℕ) = (↑i₂ : ℕ)
⊢ i₁ = i₂

Tactic:
rwa [Fin.ext_iff]

Premises used: Fin.ext_iff
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
c c' : (n : ℕ) × Composition n
H : c = c'
rw rw₁ : c'.snd (β := fun (n : ℕ) ↦ Composition n).blocks = c'.snd (β := fun (n : ℕ) ↦ Composition n).blocks
⊢ c.snd (β := fun (n : ℕ) ↦ Composition n).blocks = c'.snd (β := fun (n : ℕ) ↦ Composition n).blocks

Tactic:
rw [H]
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
c c' : (n : ℕ) × Composition n
refine :
  ∀ (H : c.snd (β := fun (n : ℕ) ↦ Composition n).blocks = c'.snd (β := fun (n : ℕ) ↦ Composition n).blocks), c = c'
⊢ c = c' ↔ c.snd (β := fun (n : ℕ) ↦ Composition n).blocks = c'.snd (β := fun (n : ℕ) ↦ Composition n).blocks

Tactic:
refine ⟨fun H => by rw [H], fun H => ?_⟩
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
c c' : (n : ℕ) × Composition n
H : c.snd (β := fun (n : ℕ) ↦ Composition n).blocks = c'.snd (β := fun (n : ℕ) ↦ Composition n).blocks
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'
⊢ c = c'

Tactic:
rcases c with ⟨n, c⟩
-- Module: Mathlib.Combinatorics.Enumerative.Composition
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
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'
⊢ Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c = c'

Tactic:
rcases c' with ⟨n', c'⟩
-- Module: Mathlib.Combinatorics.Enumerative.Composition
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
rw₂ rw₃ :
  (Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n' c').snd (β := fun (n : ℕ) ↦ Composition n).blocks.sum = c'.blocks.sum
⊢ n = n'

Tactic:
rw [← c.blocks_sum, ← c'.blocks_sum, H]

Premises used: Composition.blocks_sum
-- Module: Mathlib.Combinatorics.Enumerative.Composition
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'

Tactic:
have : n = n' := by rw [← c.blocks_sum, ← c'.blocks_sum, H]
-- Module: Mathlib.Combinatorics.Enumerative.Composition
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'
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'
⊢ Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c = Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n' c'

Tactic:
induction this
-- Module: Mathlib.Combinatorics.Enumerative.Composition
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
refl : c = c'
⊢ Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c = Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c'

Tactic:
congr
-- Module: Mathlib.Combinatorics.Enumerative.Composition
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
refl : c.blocks = c'.blocks
⊢ c = c'

Tactic:
ext1
-- Module: Mathlib.Combinatorics.Enumerative.Composition
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.blocks = c'.blocks

Tactic:
H
-- Module: Mathlib.Combinatorics.Enumerative.Composition
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.blocks = c'.blocks

Tactic:
exact H
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
A : Type u_1
inst : CommMonoid A
a : Fin n → A
x : Composition n
⊢ Eq.{u_1 + 1} (α := A)
    (∏ i : Fin x.length, ∏ j : Fin (x.blocksFun i), a ((x.embedding i : (a : Fin (x.blocksFun i)) → Fin n) j))
    (∏ i : Fin n, a i)

Tactic:
simpa [Finset.prod_sigma', Finset.univ_sigma_univ] using x.blocksFinEquiv.prod_comp a

Premises used: Composition.blocksFinEquiv, Finset.univ_sigma_univ, Equiv.prod_comp, Finset.prod_sigma'
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 : ℕ
c : Composition n_1
n i : ℕ
hi : Membership.mem (γ := List ℕ) (replicate n 1) i
⊢ 0 < i

Tactic:
simp [List.eq_of_mem_replicate hi]

Premises used: List.eq_of_mem_replicate
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 : ℕ
c : Composition n_1
n : ℕ
⊢ sum (replicate n 1) = n

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
⊢ (ones n).length = n

Tactic:
List.length_replicate

Premises used: List.length_replicate
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
⊢ (ones n).blocks = replicate n 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
i : Fin (ones n).length
⊢ (ones n).blocksFun i = 1

Tactic:
simp only [blocksFun, ones, get_eq_getElem, getElem_replicate]

Premises used: List.get_eq_getElem, Composition.blocksFun, List.getElem_replicate, Composition.ones
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n i : ℕ
⊢ (ones n).sizeUpTo i = min i n

Tactic:
simp [sizeUpTo, ones_blocks, take_replicate]

Premises used: Composition.ones_blocks, List.take_replicate, Composition.sizeUpTo
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
i : Fin (ones n).length
h : 0 < (ones n).blocksFun i
h₁ :
  (↑(((ones n).embedding i : (a : Fin ((ones n).blocksFun i)) → Fin n) (⟨0, h⟩ : Fin ((ones n).blocksFun i))) : ℕ) =
    (↑(⟨(↑i : ℕ), ⋯⟩ : Fin n) : ℕ)
⊢ ((ones n).embedding i : (a : Fin ((ones n).blocksFun i)) → Fin n) ⟨0, h⟩ = (⟨(↑i : ℕ), ⋯⟩ : Fin n)

Tactic:
ext
-- Module: Mathlib.Combinatorics.Enumerative.Composition
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⟩ : Fin ((ones n).blocksFun i))) : ℕ) =
    (↑(⟨(↑i : ℕ), ⋯⟩ : Fin n) : ℕ)

Tactic:
simpa using i.2.le

Premises used: Fin.isLt, LT.lt.le
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
mp : c = ones n → ∀ i ∈ c.blocks, i = 1
mpr : (∀ i ∈ c.blocks, i = 1) → c = ones n
⊢ c = ones n ↔ ∀ i ∈ c.blocks, i = 1

Tactic:
constructor
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
⊢ ∀ i ∈ (ones n).blocks, i = 1

Tactic:
fun i => eq_of_mem_replicate

Premises used: List.eq_of_mem_replicate
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
⊢ ∀ i ∈ (ones n).blocks, i = 1

Tactic:
exact fun i => eq_of_mem_replicate

Premises used: List.eq_of_mem_replicate
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
H : ∀ i ∈ c.blocks, i = 1
mpr : c.blocks = (ones n).blocks
⊢ c = ones n

Tactic:
ext1
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
H : ∀ i ∈ c.blocks, i = 1
⊢ c.blocks = replicate c.blocks.length 1

Tactic:
have A : c.blocks = replicate c.blocks.length 1 := eq_replicate_of_mem H
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
H : ∀ i ∈ c.blocks, i = 1
A : c.blocks = replicate c.blocks.length 1
rw : sum (replicate c.blocks.length 1)
| n

Tactic:
rw [← c.blocks_sum, A]

Premises used: Composition.blocks_sum
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
H : ∀ i ∈ c.blocks, i = 1
A : c.blocks = replicate c.blocks.length 1
conv_rhs : c.blocks.length = sum (replicate c.blocks.length 1)
⊢ c.blocks.length = n

Tactic:
conv_rhs => rw [← c.blocks_sum, A]

Premises used: Composition.blocks_sum
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
H : ∀ i ∈ c.blocks, i = 1
A : c.blocks = replicate c.blocks.length 1
⊢ c.blocks.length = sum (replicate c.blocks.length 1)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
H : ∀ i ∈ c.blocks, i = 1
A : c.blocks = replicate c.blocks.length 1
⊢ c.blocks.length = n

Tactic:
have : c.blocks.length = n := by
      conv_rhs => rw [← c.blocks_sum, A]
      simp
-- Module: Mathlib.Combinatorics.Enumerative.Composition
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
mpr₂ mpr₃ : Eq (α := List ℕ) (replicate n 1) (replicate n 1)
⊢ c.blocks = (ones n).blocks

Tactic:
rw [A, this, ones_blocks]

Premises used: Composition.ones_blocks
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
⊢ c ≠ ones n ↔ ∃ i ∈ c.blocks, 1 < i

Tactic:
(not_congr eq_ones_iff).trans ?_

Premises used: Composition.eq_ones_iff, Iff.trans, not_congr
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
refine : (¬∀ i ∈ c.blocks, i = 1) ↔ ∃ i ∈ c.blocks, 1 < i
⊢ c ≠ ones n ↔ ∃ i ∈ c.blocks, 1 < i

Tactic:
refine (not_congr eq_ones_iff).trans ?_

Premises used: Composition.eq_ones_iff, Iff.trans, not_congr
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
j : ℕ
hj : j ∈ c.blocks
⊢ j = 1 ↔ j ≤ 1

Tactic:
simp [le_antisymm_iff, c.one_le_blocks hj]

Premises used: Composition.one_le_blocks, le_antisymm_iff
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
⊢ ∀ 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]
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
this : ∀ j ∈ c.blocks, j = 1 ↔ j ≤ 1
⊢ (¬∀ i ∈ c.blocks, i = 1) ↔ ∃ i ∈ c.blocks, 1 < i

Tactic:
simp +contextual [this]
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
mp : c = ones n → c.length = n
mpr : c.length = n → c = ones n
⊢ c = ones n ↔ c.length = n

Tactic:
constructor
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
⊢ (ones n).length = n

Tactic:
ones_length n

Premises used: Composition.ones_length
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
⊢ (ones n).length = n

Tactic:
exact ones_length n

Premises used: Composition.ones_length
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
mpr : ¬c = ones n → ¬c.length = n
⊢ c.length = n → c = ones n

Tactic:
contrapose
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
mpr : n < n
⊢ False

Tactic:
apply lt_irrefl n

Premises used: lt_irrefl
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
⊢ n = ∑ i : Fin c.length, 1

Tactic:
simp [length_n]
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
⊢ ∃ i ∈ c.blocks, 1 < i

Tactic:
ne_ones_iff.1 H

Premises used: Composition.ne_ones_iff, Iff.mp
-- Module: Mathlib.Combinatorics.Enumerative.Composition
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)

Tactic:
obtain ⟨i, hi, i_blocks⟩ : ∃ i ∈ c.blocks, 1 < i := ne_ones_iff.1 H

Premises used: Composition.blocks, Composition.ne_ones_iff, Iff.mp
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
i : ℕ
hi : i ∈ c.blocks
i_blocks : 1 < i
⊢ ∃ (y : Fin c.length), c.blocksFun y = i

Tactic:
rw [← ofFn_blocksFun, mem_ofFn' c.blocksFun, Set.mem_range] at hi

Premises used: Composition.ofFn_blocksFun, Set.mem_range, Composition.blocksFun, List.mem_ofFn'
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
i : ℕ
hi : i ∈ c.blocks
i_blocks : 1 < i
hi₁ : ∃ (y : Fin c.length), c.blocksFun y = i
⊢ 1 < i

Tactic:
rw [← ofFn_blocksFun, mem_ofFn' c.blocksFun, Set.mem_range] at hi

Premises used: Composition.ofFn_blocksFun, Set.mem_range, Composition.blocksFun, List.mem_ofFn'
-- Module: Mathlib.Combinatorics.Enumerative.Composition
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
obtain :
  ∀ (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)

Tactic:
obtain ⟨j : Fin c.length, hj : c.blocksFun j = i⟩ := hi

Premises used: Composition.length, Fin
-- Module: Mathlib.Combinatorics.Enumerative.Composition
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
⊢ 1 < c.blocksFun j

Tactic:
rw [← hj] at i_blocks
-- Module: Mathlib.Combinatorics.Enumerative.Composition
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
i_blocks₁ : 1 < c.blocksFun j
⊢ c.blocksFun j = i

Tactic:
rw [← hj] at i_blocks
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
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:
Finset.sum_lt_sum (fun i _ => one_le_blocksFun c i) ⟨j, Finset.mem_univ _, i_blocks⟩

Premises used: Finset.mem_univ, And.intro, Exists.intro, Finset.sum_lt_sum, Composition.one_le_blocksFun
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
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:
exact Finset.sum_lt_sum (fun i _ => one_le_blocksFun c i) ⟨j, Finset.mem_univ _, i_blocks⟩

Premises used: Finset.mem_univ, And.intro, Exists.intro, Finset.sum_lt_sum, Composition.one_le_blocksFun