awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Tree (goal)
Goal:
x : Tree Unit
n : ℕ
base : ∀ {n : ℕ}, nil ∈ treesOfNumNodesEq n ↔ numNodes (α := Unit) nil = n
⊢ x ∈ treesOfNumNodesEq n ↔ x.numNodes = n
have ind : ∀ (x y : Tree Unit),
  (∀ {n : ℕ}, x ∈ treesOfNumNodesEq n ↔ x.numNodes = n) →
    (∀ {n : ℕ}, y ∈ treesOfNumNodesEq n ↔ y.numNodes = n) →
      ∀ {n : ℕ}, node () x y ∈ treesOfNumNodesEq n ↔ (node () x y).numNodes = n
Tactic: induction x using Tree.unitRecOn generalizing n
Cleared hypotheses: x, n
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Tree (goal)
Goal:
n : ℕ
⊢ nil ∈ treesOfNumNodesEq n ↔ numNodes (α := Unit) nil = n
have base : nil ∈ treesOfNumNodesEq 0 ↔ numNodes (α := Unit) nil = 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Tree (goal)
Goal:
n : ℕ
base : nil ∈ treesOfNumNodesEq 0 ↔ numNodes (α := Unit) nil = 0
⊢ nil ∈ treesOfNumNodesEq n ↔ numNodes (α := Unit) nil = n
have base₁ : ∀ (n : ℕ), nil ∈ treesOfNumNodesEq (n + 1) ↔ numNodes (α := Unit) nil = n + 1
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Tree (goal)
Goal:
x y : Tree Unit
h : ∀ {n : ℕ}, x ∈ treesOfNumNodesEq n ↔ x.numNodes = n
h_1 : ∀ {n : ℕ}, y ∈ treesOfNumNodesEq n ↔ y.numNodes = n
n : ℕ
⊢ node () x y ∈ treesOfNumNodesEq n ↔ (node () x y).numNodes = n
have ind : node () x y ∈ treesOfNumNodesEq 0 ↔ (node () x y).numNodes = 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Tree (goal)
Goal:
x y : Tree Unit
h : ∀ {n : ℕ}, x ∈ treesOfNumNodesEq n ↔ x.numNodes = n
h_1 : ∀ {n : ℕ}, y ∈ treesOfNumNodesEq n ↔ y.numNodes = n
n : ℕ
ind : node () x y ∈ treesOfNumNodesEq 0 ↔ (node () x y).numNodes = 0
⊢ node () x y ∈ treesOfNumNodesEq n ↔ (node () x y).numNodes = n
have ind₁ : ∀ (n : ℕ), node () x y ∈ treesOfNumNodesEq (n + 1) ↔ (node () x y).numNodes = n + 1
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Tree (goal)
Goal:
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
⊢ #(treesOfNumNodesEq (n + 1)) = catalan (n + 1)
have hi : Eq (α := ℕ)
  (∑ u ∈ @antidiagonal _ Nat.instAddMonoid _ n, #(pairwiseNode (treesOfNumNodesEq u.1) (treesOfNumNodesEq u.2)))
  (∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ n, catalan ij.1 * catalan ij.2)
Tactic: rw [treesOfNumNodesEq_succ, card_biUnion, catalan_succ']
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Tree (goal)
Goal:
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
hi :
  Eq (α := ℕ)
    (∑ u ∈ @antidiagonal _ Nat.instAddMonoid _ n, #(pairwiseNode (treesOfNumNodesEq u.1) (treesOfNumNodesEq u.2)))
    (∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ n, catalan ij.1 * catalan ij.2)
⊢ #(treesOfNumNodesEq (n + 1)) = catalan (n + 1)
have hi₁ : (↑(@antidiagonal _ Nat.instAddMonoid _ n) : Set (ℕ × ℕ)).PairwiseDisjoint (α := Finset (Tree Unit)) fun (ij : ℕ × ℕ) ↦
  pairwiseNode (treesOfNumNodesEq ij.1) (treesOfNumNodesEq ij.2)
Tactic: rw [treesOfNumNodesEq_succ, card_biUnion, catalan_succ']
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Tree (goal)
Goal:
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
⊢ Eq (α := ℕ)
    (∑ u ∈ @antidiagonal _ Nat.instAddMonoid _ n, #(pairwiseNode (treesOfNumNodesEq u.1) (treesOfNumNodesEq u.2)))
    (∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ n, catalan ij.1 * catalan ij.2)
have hi : ∀ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
  #(pairwiseNode (treesOfNumNodesEq x.1) (treesOfNumNodesEq x.2)) = catalan x.1 * catalan x.2
Tactic: apply sum_congr rfl
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Tree (goal)
Goal:
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
i j : ℕ
H : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ n
⊢ #(pairwiseNode (treesOfNumNodesEq (i, j).1) (treesOfNumNodesEq (i, j).2)) = catalan (i, j).1 * catalan (i, j).2
have hi : #(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)]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Tree (goal)
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
⊢ #(pairwiseNode (treesOfNumNodesEq (i, j).1) (treesOfNumNodesEq (i, j).2)) = catalan (i, j).1 * catalan (i, j).2
have hi₁ : #(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)]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Tree (goal)
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
⊢ #(pairwiseNode (treesOfNumNodesEq (i, j).1) (treesOfNumNodesEq (i, j).2)) = catalan (i, j).1 * catalan (i, j).2
have hi₂ : catalan (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)]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Tree (goal)
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
⊢ #(pairwiseNode (treesOfNumNodesEq (i, j).1) (treesOfNumNodesEq (i, j).2)) = catalan (i, j).1 * catalan (i, j).2
have hi₃ : catalan (i, j).1 * catalan (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)]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Tree (goal)
Goal:
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
⊢ (↑(@antidiagonal _ Nat.instAddMonoid _ n) : Set (ℕ × ℕ)).PairwiseDisjoint (α := Finset (Tree Unit)) fun (ij : ℕ × ℕ) ↦
    pairwiseNode (treesOfNumNodesEq ij.1) (treesOfNumNodesEq ij.2)
have 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)
Tactic: simp_rw [Set.PairwiseDisjoint, Set.Pairwise, disjoint_left]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Tree (goal)
Goal:
n : ℕ
⊢ #(treesOfNumNodesEq n) = catalan n
have hz : #(treesOfNumNodesEq 0) = catalan 0
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Tree (goal)
Goal:
n : ℕ
hz : #(treesOfNumNodesEq 0) = catalan 0
⊢ #(treesOfNumNodesEq n) = catalan n
have hi : ∀ (n : ℕ) (ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m), #(treesOfNumNodesEq (n + 1)) = catalan (n + 1)
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
| n
have rw : ∑ i : Fin c.length, c.blocksFun i
Tactic: rw [← c.blocks_sum, ← ofFn_blocksFun, sum_ofFn]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
⊢ ∑ i : Fin c.length, c.blocksFun i = n
have conv_rhs : ∑ i : Fin c.length, c.blocksFun i = n
Tactic: conv_rhs => rw [← c.blocks_sum, ← ofFn_blocksFun, sum_ofFn]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
conv_rhs : ∑ i : Fin c.length, c.blocksFun i = n
⊢ ∑ i : Fin c.length, c.blocksFun i = n
have conv_rhs₁ : Eq (α := ℕ) (∑ i : Fin c.length, c.blocksFun i) (∑ i : Fin c.length, c.blocksFun i)
Tactic: conv_rhs => rw [← c.blocks_sum, ← ofFn_blocksFun, sum_ofFn]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
i : ℕ
h : i ∈ c.blocks
⊢ i ≤ n
have rw : i ≤ c.blocks.sum
Tactic: rw [← c.blocks_sum]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
| n
have rw : c.blocks.sum
Tactic: rw [← c.blocks_sum]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
⊢ c.length ≤ n
have conv_rhs : c.length ≤ c.blocks.sum
Tactic: conv_rhs => rw [← c.blocks_sum]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
⊢ c.blocks = [] ↔ n = 0
have mp : c.blocks = [] → n = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
mp : c.blocks = [] → n = 0
⊢ c.blocks = [] ↔ n = 0
have mpr : n = 0 → c.blocks = []
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
c : Composition 0
⊢ c.blocks = []
have mpr : c.blocks.length ≤ 0
Tactic: rw [← length_eq_zero_iff, ← nonpos_iff_eq_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
i : ℕ
h : c.length ≤ i
⊢ (take i c.blocks).sum = n
have h₁ : take i c.blocks = c.blocks
Tactic: convert! c.blocks_sum
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
i : ℕ
| n
have rw : (take i c.blocks).sum + (drop i c.blocks).sum
Tactic: rw [← c.blocks_sum, ← sum_take_add_sum_drop _ i]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
i : ℕ
⊢ c.sizeUpTo i ≤ n
have conv_rhs : c.sizeUpTo i ≤ (take i c.blocks).sum + (drop i c.blocks).sum
Tactic: conv_rhs => rw [← c.blocks_sum, ← sum_take_add_sum_drop _ i]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
i : ℕ
h : i < c.length
⊢ (take (i + 1) c.blocks).sum =
    (take i c.blocks).sum + getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) c.blocks i h
have 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
Tactic: rw [sum_take_succ _ _ h]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
i : ℕ
h : i < c.length
⊢ c.sizeUpTo i < c.sizeUpTo (i + 1)
have rw : c.sizeUpTo i < c.sizeUpTo i + getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) c.blocks i h
Tactic: rw [c.sizeUpTo_succ h]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
⊢ 0 ∈ c.boundaries
have 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)
Tactic: simp only [boundaries, Finset.mem_univ, Finset.mem_map]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
⊢ Fin.last n ∈ c.boundaries
have 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
Tactic: simp only [boundaries, Finset.mem_univ, Finset.mem_map]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
⊢ c.boundaries.orderEmbOfFin ⋯ = c.boundary
have 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))
Tactic: refine (Finset.orderEmbOfFin_unique' _ ?_).symm
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (hypothesis)
Goal:
n : ℕ
c : Composition n
j : ℕ
h : j < n
⊢ ∃ (i : ℕ), j < c.sizeUpTo (i + 1) ∧ i < c.length
have length_pos : 0 < c.blocks.length
Tactic: have length_pos := length_pos_of_sum_pos (blocks c) (h.pos.trans_eq c.blocks_sum.symm)
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
j : ℕ
h : j < n
length_pos : 0 < c.blocks.length
⊢ ∃ (i : ℕ), j < c.sizeUpTo (i + 1) ∧ i < c.length
have refine : j < c.sizeUpTo (c.length.pred + 1)
Tactic: refine ⟨_, ?_, Nat.pred_lt length_pos.ne'⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (hypothesis)
Goal:
n : ℕ
c : Composition n
j : ℕ
h : j < n
length_pos : 0 < c.blocks.length
⊢ j < c.sizeUpTo (c.length.pred + 1)
have this : c.length - 1 + 1 = c.length
Tactic: have : c.length - 1 + 1 = c.length := Nat.succ_pred_eq_of_pos length_pos
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
j : Fin n
⊢ c.sizeUpTo (↑(c.index j) : ℕ) ≤ (↑j : ℕ)
have by_contra! : ∀ (H : (↑j : ℕ) < c.sizeUpTo (↑(c.index j) : ℕ)), False
Tactic: by_contra! H
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length := c.index j
H : (↑j : ℕ) < c.sizeUpTo (↑i : ℕ)
⊢ 0 < (↑i : ℕ)
have by_contra! : ∀ (i_pos : (↑i : ℕ) ≤ 0), False
Tactic: by_contra! i_pos
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length := c.index j
H : (↑j : ℕ) < c.sizeUpTo (↑i : ℕ)
i_pos : (↑i : ℕ) ≤ 0
⊢ False
have revert : ∀ (H : (↑j : ℕ) < c.sizeUpTo (↑i : ℕ)), False
Tactic: revert H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (hypothesis)
Goal:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length := c.index j
H : (↑j : ℕ) < c.sizeUpTo (↑i : ℕ)
⊢ False
have i_pos : 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (hypothesis)
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
⊢ False
have i₁_lt_i : i₁ < (↑i : ℕ)
Tactic: have i₁_lt_i : i₁ < i := Nat.pred_lt (ne_of_gt i_pos)
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (hypothesis)
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 : ℕ)
⊢ False
have i₁_succ : i₁ + 1 = (↑i : ℕ)
Tactic: have i₁_succ : i₁ + 1 = i := Nat.succ_pred_eq_of_pos i_pos
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (hypothesis)
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 : ℕ)
⊢ False
have this : ¬((↑j : ℕ) < c.sizeUpTo (i₁ + 1) ∧ i₁ < c.length)
Tactic: have := Nat.find_min (c.index_exists j.2) i₁_lt_i
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
j : Fin n
⊢ (↑j : ℕ) - c.sizeUpTo (↑(c.index j) : ℕ) < c.blocksFun (c.index j)
have rw : (↑j : ℕ) < c.sizeUpTo ((↑(c.index j) : ℕ) + 1)
Tactic: rw [tsub_lt_iff_right, add_comm, ← sizeUpTo_succ']
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
j : Fin n
rw : (↑j : ℕ) < c.sizeUpTo ((↑(c.index j) : ℕ) + 1)
⊢ (↑j : ℕ) - c.sizeUpTo (↑(c.index j) : ℕ) < c.blocksFun (c.index j)
have rw₁ : c.sizeUpTo (↑(c.index j) : ℕ) ≤ (↑j : ℕ)
Tactic: rw [tsub_lt_iff_right, add_comm, ← sizeUpTo_succ']
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
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
have rw : (↑((c.embedding (c.index j) : (a : Fin (c.blocksFun (c.index j))) → Fin n) (c.invEmbedding j)) : ℕ) = (↑j : ℕ)
Tactic: rw [Fin.ext_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
⊢ Membership.mem (γ := Set (Fin n))
      (Set.range (ι := Fin (c.blocksFun i)) (⇑(c.embedding i) : (a : Fin (c.blocksFun i)) → Fin n)) j ↔
    c.sizeUpTo (↑i : ℕ) ≤ (↑j : ℕ) ∧ (↑j : ℕ) < c.sizeUpTo (↑i : ℕ).succ
have mp : Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (c.blocksFun i)) (⇑(c.embedding i) : (a : Fin (c.blocksFun i)) → Fin n)) j →
  c.sizeUpTo (↑i : ℕ) ≤ (↑j : ℕ) ∧ (↑j : ℕ) < c.sizeUpTo (↑i : ℕ).succ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
mp :
  Membership.mem (γ := Set (Fin n))
      (Set.range (ι := Fin (c.blocksFun i)) (⇑(c.embedding i) : (a : Fin (c.blocksFun i)) → Fin n)) j →
    c.sizeUpTo (↑i : ℕ) ≤ (↑j : ℕ) ∧ (↑j : ℕ) < c.sizeUpTo (↑i : ℕ).succ
⊢ Membership.mem (γ := Set (Fin n))
      (Set.range (ι := Fin (c.blocksFun i)) (⇑(c.embedding i) : (a : Fin (c.blocksFun i)) → Fin n)) j ↔
    c.sizeUpTo (↑i : ℕ) ≤ (↑j : ℕ) ∧ (↑j : ℕ) < c.sizeUpTo (↑i : ℕ).succ
have mpr : c.sizeUpTo (↑i : ℕ) ≤ (↑j : ℕ) ∧ (↑j : ℕ) < c.sizeUpTo (↑i : ℕ).succ →
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (c.blocksFun i)) (⇑(c.embedding i) : (a : Fin (c.blocksFun i)) → Fin n)) j
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (c.blocksFun i)) (⇑(c.embedding i) : (a : Fin (c.blocksFun i)) → Fin n)) j
⊢ c.sizeUpTo (↑i : ℕ) ≤ (↑j : ℕ) ∧ (↑j : ℕ) < c.sizeUpTo (↑i : ℕ).succ
have mp : ∀ (k : Fin (c.blocksFun i)) (hk : (c.embedding i : (a : Fin (c.blocksFun i)) → Fin n) k = j),
  c.sizeUpTo (↑i : ℕ) ≤ (↑j : ℕ) ∧ (↑j : ℕ) < c.sizeUpTo (↑i : ℕ).succ
Tactic: rcases Set.mem_range.2 h with ⟨k, hk⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (hypothesis)
Goal:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (c.blocksFun i)) (⇑(c.embedding i) : (a : Fin (c.blocksFun i)) → Fin n)) j
k : Fin (c.blocksFun i)
hk : (c.embedding i : (a : Fin (c.blocksFun i)) → Fin n) k = j
⊢ c.sizeUpTo (↑i : ℕ) ≤ (↑j : ℕ) ∧ (↑j : ℕ) < c.sizeUpTo (↑i : ℕ).succ
have hk₁ : (↑((c.embedding i : (a : Fin (c.blocksFun i)) → Fin n) k) : ℕ) = (↑j : ℕ)
Tactic: rw [Fin.ext_iff] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (c.blocksFun i)) (⇑(c.embedding i) : (a : Fin (c.blocksFun i)) → Fin n)) j
k : Fin (c.blocksFun i)
hk : c.sizeUpTo (↑i : ℕ) + (↑k : ℕ) = (↑j : ℕ)
⊢ c.sizeUpTo (↑i : ℕ) ≤ (↑j : ℕ) ∧ (↑j : ℕ) < c.sizeUpTo (↑i : ℕ).succ
have mp : c.sizeUpTo (↑i : ℕ) ≤ c.sizeUpTo (↑i : ℕ) + (↑k : ℕ) ∧ c.sizeUpTo (↑i : ℕ) + (↑k : ℕ) < c.sizeUpTo (↑i : ℕ).succ
Tactic: rw [← hk]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : c.sizeUpTo (↑i : ℕ) ≤ (↑j : ℕ) ∧ (↑j : ℕ) < c.sizeUpTo (↑i : ℕ).succ
⊢ ∃ (y : Fin (c.blocksFun i)), (c.embedding i : (a : Fin (c.blocksFun i)) → Fin n) y = j
have mpr : (↑j : ℕ) - c.sizeUpTo (↑i : ℕ) < c.blocksFun i
Tactic: refine ⟨⟨j - c.sizeUpTo i, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : c.sizeUpTo (↑i : ℕ) ≤ (↑j : ℕ) ∧ (↑j : ℕ) < c.sizeUpTo (↑i : ℕ).succ
mpr : (↑j : ℕ) - c.sizeUpTo (↑i : ℕ) < c.blocksFun i
⊢ ∃ (y : Fin (c.blocksFun i)), (c.embedding i : (a : Fin (c.blocksFun i)) → Fin n) y = j
have mpr₁ : (c.embedding i : (a : Fin (c.blocksFun i)) → Fin n) ⟨(↑j : ℕ) - c.sizeUpTo (↑i : ℕ), sorry⟩ = j
Tactic: refine ⟨⟨j - c.sizeUpTo i, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : c.sizeUpTo (↑i : ℕ) ≤ (↑j : ℕ) ∧ (↑j : ℕ) < c.sizeUpTo (↑i : ℕ).succ
⊢ (↑j : ℕ) - c.sizeUpTo (↑i : ℕ) < c.blocksFun i
have mpr : (↑j : ℕ) < c.sizeUpTo ((↑i : ℕ) + 1)
Tactic: rw [tsub_lt_iff_left, ← sizeUpTo_succ']
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : c.sizeUpTo (↑i : ℕ) ≤ (↑j : ℕ) ∧ (↑j : ℕ) < c.sizeUpTo (↑i : ℕ).succ
mpr : (↑j : ℕ) < c.sizeUpTo ((↑i : ℕ) + 1)
⊢ (↑j : ℕ) - c.sizeUpTo (↑i : ℕ) < c.blocksFun i
have mpr₁ : c.sizeUpTo (↑i : ℕ) ≤ (↑j : ℕ)
Tactic: rw [tsub_lt_iff_left, ← sizeUpTo_succ']
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : c.sizeUpTo (↑i : ℕ) ≤ (↑j : ℕ) ∧ (↑j : ℕ) < c.sizeUpTo (↑i : ℕ).succ
⊢ (c.embedding i : (a : Fin (c.blocksFun i)) → Fin n) ⟨(↑j : ℕ) - c.sizeUpTo (↑i : ℕ), ⋯⟩ = j
have mpr : (↑((c.embedding i : (a : Fin (c.blocksFun i)) → Fin n) (⟨(↑j : ℕ) - c.sizeUpTo (↑i : ℕ), sorry⟩ : Fin (c.blocksFun i))) :
    ℕ) =
  (↑j : ℕ)
Tactic: rw [Fin.ext_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
i₁ i₂ : Fin c.length
h : i₁ ≠ i₂
⊢ _root_.Disjoint (α := Set (Fin n))
    (Set.range (ι := Fin (c.blocksFun i₁)) (⇑(c.embedding i₁) : (a : Fin (c.blocksFun i₁)) → Fin n))
    (Set.range (ι := Fin (c.blocksFun i₂)) (⇑(c.embedding i₂) : (a : Fin (c.blocksFun i₂)) → Fin n))
have inr : ∀
  (this :
    ∀ {n : ℕ} (c : Composition n) {i₁ i₂ : Fin c.length} (h : i₁ ≠ i₂) (h' : i₁ < i₂),
      _root_.Disjoint (α := Set (Fin n))
        (Set.range (ι := Fin (c.blocksFun i₁)) (⇑(c.embedding i₁) : (a : Fin (c.blocksFun i₁)) → Fin n))
        (Set.range (ι := Fin (c.blocksFun i₂)) (⇑(c.embedding i₂) : (a : Fin (c.blocksFun i₂)) → Fin n)))
  (h' : ¬i₁ < i₂),
  _root_.Disjoint (α := Set (Fin n))
    (Set.range (ι := Fin (c.blocksFun i₁)) (⇑(c.embedding i₁) : (a : Fin (c.blocksFun i₁)) → Fin n))
    (Set.range (ι := Fin (c.blocksFun i₂)) (⇑(c.embedding i₂) : (a : Fin (c.blocksFun i₂)) → Fin n))
Tactic: wlog h' : i₁ < i₂