awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree
Goal:
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
i j : ℕ
H : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ n
hi : #(treesOfNumNodesEq (i, j).1 ×ˢ treesOfNumNodesEq (i, j).2) = catalan (i, j).1 * catalan (i, j).2
hi₁ : #(treesOfNumNodesEq (i, j).1) * #(treesOfNumNodesEq (i, j).2) = catalan (i, j).1 * catalan (i, j).2
hi₂ : catalan (i, j).1 * #(treesOfNumNodesEq (i, j).2) = catalan (i, j).1 * catalan (i, j).2
hi₃ hi₄ : catalan (i, j).1 * catalan (i, j).2 = catalan (i, j).1 * catalan (i, j).2
⊢ #(pairwiseNode (treesOfNumNodesEq (i, j).1) (treesOfNumNodesEq (i, j).2)) = catalan (i, j).1 * catalan (i, j).2

Tactic:
rw [card_map, card_product, ih _ (fst_le H), ih _ (snd_le H)]

Premises used: Finset.card_product, Finset.card_map, Finset.antidiagonal.snd_le, Finset.antidiagonal.fst_le
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree
Goal:
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
hi :
  ∀ ⦃x : ℕ × ℕ⦄,
    x ∈ (↑(@antidiagonal _ Nat.instAddMonoid _ n) : Set (ℕ × ℕ)) →
      ∀ ⦃y : ℕ × ℕ⦄,
        y ∈ (↑(@antidiagonal _ Nat.instAddMonoid _ n) : Set (ℕ × ℕ)) →
          x ≠ y →
            ∀ ⦃a : Tree Unit⦄,
              a ∈ pairwiseNode (treesOfNumNodesEq x.1) (treesOfNumNodesEq x.2) →
                a ∉ pairwiseNode (treesOfNumNodesEq y.1) (treesOfNumNodesEq y.2)
⊢ (↑(@antidiagonal _ Nat.instAddMonoid _ n) : Set (ℕ × ℕ)).PairwiseDisjoint (α := Finset (Tree Unit)) fun (ij : ℕ × ℕ) ↦
    pairwiseNode (treesOfNumNodesEq ij.1) (treesOfNumNodesEq ij.2)

Tactic:
simp_rw [Set.PairwiseDisjoint, Set.Pairwise, disjoint_left]

Premises used: Set.PairwiseDisjoint, Set.Pairwise, Finset.disjoint_left
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree
Goal:
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
⊢ ∀ ⦃x : ℕ × ℕ⦄,
    x ∈ (↑(@antidiagonal _ Nat.instAddMonoid _ n) : Set (ℕ × ℕ)) →
      ∀ ⦃y : ℕ × ℕ⦄,
        y ∈ (↑(@antidiagonal _ Nat.instAddMonoid _ n) : Set (ℕ × ℕ)) →
          x ≠ y →
            ∀ ⦃a : Tree Unit⦄,
              a ∈ pairwiseNode (treesOfNumNodesEq x.1) (treesOfNumNodesEq x.2) →
                a ∉ pairwiseNode (treesOfNumNodesEq y.1) (treesOfNumNodesEq y.2)

Tactic:
aesop
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree
Goal:
n : ℕ
hz : #(treesOfNumNodesEq 0) = catalan 0
hi : ∀ (n : ℕ) (ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m), #(treesOfNumNodesEq (n + 1)) = catalan (n + 1)
⊢ #(treesOfNumNodesEq n) = catalan n

Tactic:
induction n using Nat.case_strong_induction_on with
  | hz => simp
  | hi n ih =>
    rw [treesOfNumNodesEq_succ, card_biUnion, catalan_succ']
    · apply sum_congr rfl
      rintro ⟨i, j⟩ H
      rw [card_map, card_product, ih _ (fst_le H), ih _ (snd_le H)]
    · simp_rw [Set.PairwiseDisjoint, Set.Pairwise, disjoint_left]
      aesop

Premises used: Nat.case_strong_induction_on, Tree.treesOfNumNodesEq_succ, Finset.card_product, Set.PairwiseDisjoint, Finset.card_map, Finset.card_biUnion, Set.Pairwise, catalan_succ', Finset.disjoint_left, Finset.sum_congr, rfl
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
⊢ c.blocks.length = c.length

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
⊢ ofFn c.blocksFun = c.blocks

Tactic:
ofFn_get _

Premises used: List.ofFn_get, Composition.blocksFun
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
rw : ∑ i : Fin c.length, c.blocksFun i
| n

Tactic:
rw [← c.blocks_sum, ← ofFn_blocksFun, sum_ofFn]

Premises used: Composition.ofFn_blocksFun, List.sum_ofFn, Composition.blocks_sum
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
conv_rhs : ∑ i : Fin c.length, c.blocksFun i = n
conv_rhs₁ : Eq (α := ℕ) (∑ i : Fin c.length, c.blocksFun i) (∑ i : Fin c.length, c.blocksFun i)
⊢ ∑ i : Fin c.length, c.blocksFun i = n

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

Premises used: Composition.ofFn_blocksFun, List.sum_ofFn, Composition.blocks_sum
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
i : Fin c.length
⊢ c.blocksFun i ∈ c.blocks

Tactic:
get_mem _ _

Premises used: Composition.blocksFun, List.get_mem
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
i : ℕ
h : i ∈ c.blocks
⊢ 1 ≤ i

Tactic:
c.blocks_pos h

Premises used: Composition.blocks_pos, Nat.lt
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
i : ℕ
h : i ∈ c.blocks
rw : i ≤ c.blocks.sum
⊢ i ≤ n

Tactic:
rw [← c.blocks_sum]

Premises used: Composition.blocks_sum
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
i : ℕ
h : i ∈ c.blocks
⊢ i ≤ c.blocks.sum

Tactic:
List.le_sum_of_mem h

Premises used: List.le_sum_of_mem
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
i : ℕ
h : i ∈ c.blocks
⊢ i ≤ c.blocks.sum

Tactic:
exact List.le_sum_of_mem h

Premises used: List.le_sum_of_mem
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
i : ℕ
h : i < c.length
⊢ 1 ≤ getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) c.blocks i h

Tactic:
c.one_le_blocks (get_mem (blocks c) _)

Premises used: Composition.blocks, Composition.one_le_blocks, List.get_mem
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
i : ℕ
h : i < c.length
⊢ 0 < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) c.blocks i h

Tactic:
c.one_le_blocks' h

Premises used: Composition.one_le_blocks', Nat.lt
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
i : Fin c.length
⊢ 1 ≤ c.blocksFun i

Tactic:
c.one_le_blocks (c.blocksFun_mem_blocks i)

Premises used: Composition.blocksFun_mem_blocks, Composition.one_le_blocks
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
i : Fin c.length
⊢ c.blocksFun i ≤ n

Tactic:
c.blocks_le <| getElem_mem _

Premises used: Composition.blocks_le, List.getElem_mem
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
rw : c.blocks.sum
| n

Tactic:
rw [← c.blocks_sum]

Premises used: Composition.blocks_sum
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
conv_rhs : c.length ≤ c.blocks.sum
⊢ c.length ≤ n

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

Premises used: Composition.blocks_sum
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
⊢ c.length ≤ c.blocks.sum

Tactic:
length_le_sum_of_one_le _ fun i hi => c.one_le_blocks hi

Premises used: List.length_le_sum_of_one_le, Composition.one_le_blocks
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
⊢ c.length ≤ c.blocks.sum

Tactic:
exact length_le_sum_of_one_le _ fun i hi => c.one_le_blocks hi

Premises used: List.length_le_sum_of_one_le, Composition.one_le_blocks
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
mp : c.blocks = [] → n = 0
mpr : n = 0 → c.blocks = []
⊢ c.blocks = [] ↔ n = 0

Tactic:
constructor
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
h : c.blocks = []
⊢ n = 0

Tactic:
simpa using congr(List.sum $h)
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
c : Composition 0
mpr : c.blocks.length ≤ 0
⊢ c.blocks = []

Tactic:
rw [← length_eq_zero_iff, ← nonpos_iff_eq_zero]

Premises used: List.length_eq_zero_iff, nonpos_iff_eq_zero
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
c : Composition 0
⊢ c.blocks.length ≤ 0

Tactic:
c.length_le

Premises used: Composition.length_le
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
c : Composition 0
⊢ c.blocks.length ≤ 0

Tactic:
exact c.length_le

Premises used: Composition.length_le
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
⊢ c.length = 0 ↔ n = 0

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
⊢ 0 < c.length ↔ 0 < n

Tactic:
simp [pos_iff_ne_zero]

Premises used: pos_iff_ne_zero
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
⊢ c.sizeUpTo 0 = 0

Tactic:
simp [sizeUpTo]

Premises used: Composition.sizeUpTo
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
i : ℕ
h : c.length ≤ i
⊢ c.blocks.sum = n

Tactic:
c.blocks_sum

Premises used: Composition.blocks_sum
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
i : ℕ
h : c.length ≤ i
h₁ : take i c.blocks = c.blocks
⊢ (take i c.blocks).sum = n

Tactic:
convert! c.blocks_sum

Premises used: Composition.blocks_sum
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
i : ℕ
h : c.length ≤ i
⊢ take i c.blocks = c.blocks

Tactic:
take_of_length_le h

Premises used: List.take_of_length_le
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
i : ℕ
h : c.length ≤ i
⊢ take i c.blocks = c.blocks

Tactic:
exact take_of_length_le h

Premises used: List.take_of_length_le
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
⊢ c.sizeUpTo c.length = n

Tactic:
c.sizeUpTo_ofLength_le c.length le_rfl

Premises used: le_rfl, Composition.length, Composition.sizeUpTo_ofLength_le
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
i : ℕ
rw : (take i c.blocks).sum + (drop i c.blocks).sum
| n

Tactic:
rw [← c.blocks_sum, ← sum_take_add_sum_drop _ i]

Premises used: Composition.blocks_sum, List.sum_take_add_sum_drop
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
i : ℕ
conv_rhs : c.sizeUpTo i ≤ (take i c.blocks).sum + (drop i c.blocks).sum
⊢ c.sizeUpTo i ≤ n

Tactic:
conv_rhs => rw [← c.blocks_sum, ← sum_take_add_sum_drop _ i]

Premises used: Composition.blocks_sum, List.sum_take_add_sum_drop
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
i : ℕ
⊢ c.sizeUpTo i ≤ (take i c.blocks).sum + (drop i c.blocks).sum

Tactic:
Nat.le_add_right _ _

Premises used: Nat.le_add_right, Composition.sizeUpTo
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
i : ℕ
⊢ c.sizeUpTo i ≤ (take i c.blocks).sum + (drop i c.blocks).sum

Tactic:
exact Nat.le_add_right _ _

Premises used: Nat.le_add_right
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
i : ℕ
h : i < c.length
rw rw₁ :
  (take i c.blocks).sum + getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) c.blocks i h =
    (take i c.blocks).sum + getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) c.blocks i h
⊢ (take (i + 1) c.blocks).sum =
    (take i c.blocks).sum + getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) c.blocks i h

Tactic:
rw [sum_take_succ _ _ h]

Premises used: List.sum_take_succ
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
i : Fin c.length
⊢ c.sizeUpTo ((↑i : ℕ) + 1) = c.sizeUpTo (↑i : ℕ) + c.blocksFun i

Tactic:
c.sizeUpTo_succ i.2

Premises used: Composition.blocksFun, Fin.isLt, Composition.sizeUpTo_succ
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
i : ℕ
h : i < c.length
rw : c.sizeUpTo i < c.sizeUpTo i + getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) c.blocks i h
⊢ c.sizeUpTo i < c.sizeUpTo (i + 1)

Tactic:
rw [c.sizeUpTo_succ h]

Premises used: Composition.sizeUpTo_succ
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
i : ℕ
h : i < c.length
⊢ c.sizeUpTo i < c.sizeUpTo i + getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) c.blocks i h

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
⊢ Monotone c.sizeUpTo

Tactic:
monotone_sum_take _

Premises used: List.monotone_sum_take, Composition.sizeUpTo
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
⊢ Eq (α := Fin (n + 1)) ((c.boundary : (a : Fin (c.length + 1)) → Fin (n + 1)) 0) 0

Tactic:
simp [boundary]

Premises used: Composition.boundary
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
⊢ (c.boundary : (a : Fin (c.length + 1)) → Fin (n + 1)) (Fin.last c.length) = Fin.last n

Tactic:
simp [boundary, Fin.ext_iff]

Premises used: Fin.ext_iff, Composition.boundary
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
⊢ c.boundaries.card = c.length + 1

Tactic:
simp [boundaries]

Premises used: Composition.boundaries
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
simp :
  ∃ (a : Fin (c.length + 1)),
    True ∧
      Eq (α := Fin n.succ)
        ((c.boundary.toEmbedding (r := fun (x1 x2 : Fin (c.length + 1)) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin (n + 1)) ↦
                x1 ≤ x2) :
              (a : Fin (c.length + 1)) → Fin n.succ)
            a :
          Fin n.succ)
        (0 : Fin n.succ)
⊢ 0 ∈ c.boundaries

Tactic:
simp only [boundaries, Finset.mem_univ, Finset.mem_map]

Premises used: Finset.mem_univ, Composition.boundaries, Finset.mem_map
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
⊢ ∃ (a : Fin (c.length + 1)),
    True ∧
      Eq (α := Fin n.succ)
        ((c.boundary.toEmbedding (r := fun (x1 x2 : Fin (c.length + 1)) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin (n + 1)) ↦
                x1 ≤ x2) :
              (a : Fin (c.length + 1)) → Fin n.succ)
            a :
          Fin n.succ)
        (0 : Fin n.succ)

Tactic:
⟨0, And.intro True.intro rfl⟩

Premises used: And.intro, Exists.intro, OfNat.ofNat, rfl, True.intro
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
⊢ ∃ (a : Fin (c.length + 1)),
    True ∧
      Eq (α := Fin n.succ)
        ((c.boundary.toEmbedding (r := fun (x1 x2 : Fin (c.length + 1)) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin (n + 1)) ↦
                x1 ≤ x2) :
              (a : Fin (c.length + 1)) → Fin n.succ)
            a :
          Fin n.succ)
        (0 : Fin n.succ)

Tactic:
exact ⟨0, And.intro True.intro rfl⟩
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
simp :
  ∃ (a : Fin (c.length + 1)),
    True ∧
      (c.boundary.toEmbedding (r := fun (x1 x2 : Fin (c.length + 1)) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin (n + 1)) ↦
              x1 ≤ x2) :
            (a : Fin (c.length + 1)) → Fin (n + 1))
          a =
        Fin.last n
⊢ Fin.last n ∈ c.boundaries

Tactic:
simp only [boundaries, Finset.mem_univ, Finset.mem_map]

Premises used: Finset.mem_univ, Composition.boundaries, Finset.mem_map
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
⊢ ∃ (a : Fin (c.length + 1)),
    True ∧
      (c.boundary.toEmbedding (r := fun (x1 x2 : Fin (c.length + 1)) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin (n + 1)) ↦
              x1 ≤ x2) :
            (a : Fin (c.length + 1)) → Fin (n + 1))
          a =
        Fin.last n

Tactic:
⟨Fin.last c.length, And.intro True.intro c.boundary_last⟩

Premises used: Composition.length, Fin.last, And.intro, Exists.intro, Composition.boundary_last, True.intro
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
⊢ ∃ (a : Fin (c.length + 1)),
    True ∧
      (c.boundary.toEmbedding (r := fun (x1 x2 : Fin (c.length + 1)) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin (n + 1)) ↦
              x1 ≤ x2) :
            (a : Fin (c.length + 1)) → Fin (n + 1))
          a =
        Fin.last n

Tactic:
exact ⟨Fin.last c.length, And.intro True.intro c.boundary_last⟩
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
⊢ c.boundaries.orderEmbOfFin ⋯ = c.boundary

Tactic:
(Finset.orderEmbOfFin_unique' _ ?_).symm

Premises used: Finset.orderEmbOfFin_unique', Eq.symm
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
refine :
  ∀ (x : Fin (c.length + 1)),
    Membership.mem (α := Fin (n + 1)) c.boundaries
      ((c.boundary : (a : Fin (c.length + 1)) → Fin (n + 1)) x : Fin (n + 1))
⊢ c.boundaries.orderEmbOfFin ⋯ = c.boundary

Tactic:
refine (Finset.orderEmbOfFin_unique' _ ?_).symm

Premises used: Finset.orderEmbOfFin_unique', Eq.symm
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
⊢ ∀ (x : Fin (c.length + 1)),
    Membership.mem (α := Fin (n + 1)) c.boundaries
      ((c.boundary : (a : Fin (c.length + 1)) → Fin (n + 1)) x : Fin (n + 1))

Tactic:
fun i => (Finset.mem_map' _).2 (Finset.mem_univ _)

Premises used: Iff.mpr, Finset.mem_univ, Set.Mem, setOf, RelEmbedding.toEmbedding, Finset.mem_map', Composition.boundary
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
⊢ ∀ (x : Fin (c.length + 1)),
    Membership.mem (α := Fin (n + 1)) c.boundaries
      ((c.boundary : (a : Fin (c.length + 1)) → Fin (n + 1)) x : Fin (n + 1))

Tactic:
exact fun i => (Finset.mem_map' _).2 (Finset.mem_univ _)

Premises used: Iff.mpr, Finset.mem_univ, Finset.mem_map'
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
i : Fin c.length
j : Fin (c.blocksFun i)
⊢ (↑((c.embedding i : (a : Fin (c.blocksFun i)) → Fin n) j) : ℕ) = c.sizeUpTo (↑i : ℕ) + (↑j : ℕ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
j : ℕ
h : j < n
⊢ 0 < c.blocks.length

Tactic:
have length_pos := length_pos_of_sum_pos (blocks c) (h.pos.trans_eq c.blocks_sum.symm)
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
j : ℕ
h : j < n
length_pos : 0 < c.blocks.length
⊢ ∃ (i : ℕ), j < c.sizeUpTo (i + 1) ∧ i < c.length

Tactic:
⟨_, ?_, Nat.pred_lt length_pos.ne'⟩

Premises used: LT.lt.ne', Nat.pred_lt, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
j : ℕ
h : j < n
length_pos : 0 < c.blocks.length
refine : j < c.sizeUpTo (c.length.pred + 1)
⊢ ∃ (i : ℕ), j < c.sizeUpTo (i + 1) ∧ i < c.length

Tactic:
refine ⟨_, ?_, Nat.pred_lt length_pos.ne'⟩
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
j : ℕ
h : j < n
length_pos : 0 < c.blocks.length
⊢ c.length - 1 + 1 = c.length

Tactic:
have : c.length - 1 + 1 = c.length := Nat.succ_pred_eq_of_pos length_pos
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
j : ℕ
h : j < n
length_pos : 0 < c.blocks.length
this : c.length - 1 + 1 = c.length
⊢ j < c.sizeUpTo (c.length.pred + 1)

Tactic:
simp [this, h]
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
j : Fin n
⊢ (↑j : ℕ) < c.sizeUpTo (↑(c.index j).succ : ℕ)

Tactic:
(Nat.find_spec (c.index_exists j.2)).1

Premises used: Composition.index_exists, Fin.isLt, And.left, Nat.find_spec
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
j : Fin n
by_contra! : ∀ (H : (↑j : ℕ) < c.sizeUpTo (↑(c.index j) : ℕ)), False
⊢ c.sizeUpTo (↑(c.index j) : ℕ) ≤ (↑j : ℕ)

Tactic:
by_contra! H
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
j : Fin n
H : (↑j : ℕ) < c.sizeUpTo (↑(c.index j) : ℕ)
⊢ let i := c.index j;
  (↑j : ℕ) < c.sizeUpTo (↑i : ℕ)

Tactic:
set i := c.index j

Premises used: Composition.index
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length := c.index j
H : (↑j : ℕ) < c.sizeUpTo (↑i : ℕ)
by_contra! : ∀ (i_pos : (↑i : ℕ) ≤ 0), False
⊢ 0 < (↑i : ℕ)

Tactic:
by_contra! i_pos
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length := c.index j
H : (↑j : ℕ) < c.sizeUpTo (↑i : ℕ)
i_pos : (↑i : ℕ) ≤ 0
revert : ∀ (H : (↑j : ℕ) < c.sizeUpTo (↑i : ℕ)), False
⊢ False

Tactic:
revert H
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length := c.index j
i_pos : (↑i : ℕ) ≤ 0
⊢ ∀ (H : (↑j : ℕ) < c.sizeUpTo (↑i : ℕ)), False

Tactic:
simp [nonpos_iff_eq_zero.1 i_pos, c.sizeUpTo_zero]

Premises used: Iff.mp, Composition.sizeUpTo_zero, nonpos_iff_eq_zero
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length := c.index j
H : (↑j : ℕ) < c.sizeUpTo (↑i : ℕ)
⊢ 0 < (↑i : ℕ)

Tactic:
have i_pos : (0 : ℕ) < i := by
    by_contra! i_pos
    revert H
    simp [nonpos_iff_eq_zero.1 i_pos, c.sizeUpTo_zero]
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length := c.index j
H : (↑j : ℕ) < c.sizeUpTo (↑i : ℕ)
i_pos : 0 < (↑i : ℕ)
i₁ : ℕ := (↑i : ℕ).pred
⊢ i₁ < (↑i : ℕ)

Tactic:
have i₁_lt_i : i₁ < i := Nat.pred_lt (ne_of_gt i_pos)
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length := c.index j
H : (↑j : ℕ) < c.sizeUpTo (↑i : ℕ)
i_pos : 0 < (↑i : ℕ)
i₁ : ℕ := (↑i : ℕ).pred
i₁_lt_i : i₁ < (↑i : ℕ)
⊢ i₁ + 1 = (↑i : ℕ)

Tactic:
have i₁_succ : i₁ + 1 = i := Nat.succ_pred_eq_of_pos i_pos
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length := c.index j
H : (↑j : ℕ) < c.sizeUpTo (↑i : ℕ)
i_pos : 0 < (↑i : ℕ)
i₁ : ℕ := (↑i : ℕ).pred
i₁_lt_i : i₁ < (↑i : ℕ)
i₁_succ : i₁ + 1 = (↑i : ℕ)
⊢ ¬((↑j : ℕ) < c.sizeUpTo (i₁ + 1) ∧ i₁ < c.length)

Tactic:
have := Nat.find_min (c.index_exists j.2) i₁_lt_i
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length := c.index j
H : (↑j : ℕ) < c.sizeUpTo (↑i : ℕ)
i_pos : 0 < (↑i : ℕ)
i₁ : ℕ := (↑i : ℕ).pred
i₁_lt_i : i₁ < (↑i : ℕ)
i₁_succ : i₁ + 1 = (↑i : ℕ)
this : ¬((↑j : ℕ) < c.sizeUpTo (i₁ + 1) ∧ i₁ < c.length)
⊢ False

Tactic:
simp_all [lt_trans i₁_lt_i (c.index j).2]

Premises used: lt_trans, Fin.isLt, Composition.index
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
j : Fin n
rw : (↑j : ℕ) < c.sizeUpTo ((↑(c.index j) : ℕ) + 1)
rw₁ : c.sizeUpTo (↑(c.index j) : ℕ) ≤ (↑j : ℕ)
⊢ (↑j : ℕ) - c.sizeUpTo (↑(c.index j) : ℕ) < c.blocksFun (c.index j)

Tactic:
rw [tsub_lt_iff_right, add_comm, ← sizeUpTo_succ']

Premises used: add_comm, Composition.sizeUpTo_succ', tsub_lt_iff_right
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
j : Fin n
⊢ (↑j : ℕ) < c.sizeUpTo ((↑(c.index j) : ℕ) + 1)

Tactic:
lt_sizeUpTo_index_succ _ _

Premises used: Nat.find, Composition.lt_sizeUpTo_index_succ
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
j : Fin n
⊢ (↑j : ℕ) < c.sizeUpTo ((↑(c.index j) : ℕ) + 1)

Tactic:
exact lt_sizeUpTo_index_succ _ _

Premises used: Composition.lt_sizeUpTo_index_succ
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
j : Fin n
⊢ c.sizeUpTo (↑(c.index j) : ℕ) ≤ (↑j : ℕ)

Tactic:
sizeUpTo_index_le _ _

Premises used: Composition.sizeUpTo_index_le
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
j : Fin n
⊢ c.sizeUpTo (↑(c.index j) : ℕ) ≤ (↑j : ℕ)

Tactic:
exact sizeUpTo_index_le _ _

Premises used: Composition.sizeUpTo_index_le
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
j : Fin n
⊢ (↑(c.invEmbedding j) : ℕ) = (↑j : ℕ) - c.sizeUpTo (↑(c.index j) : ℕ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
j : Fin n
rw : (↑((c.embedding (c.index j) : (a : Fin (c.blocksFun (c.index j))) → Fin n) (c.invEmbedding j)) : ℕ) = (↑j : ℕ)
⊢ (c.embedding (c.index j) : (a : Fin (c.blocksFun (c.index j))) → Fin n) (c.invEmbedding j) = j

Tactic:
rw [Fin.ext_iff]

Premises used: Fin.ext_iff
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
j : Fin n
⊢ (↑((c.embedding (c.index j) : (a : Fin (c.blocksFun (c.index j))) → Fin n) (c.invEmbedding j)) : ℕ) = (↑j : ℕ)

Tactic:
apply add_tsub_cancel_of_le (c.sizeUpTo_index_le j)

Premises used: Composition.sizeUpTo_index_le, add_tsub_cancel_of_le