awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Enumerative.Composition
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
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
⊢ 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
-- Module: Mathlib.Combinatorics.Enumerative.Composition
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
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
⊢ c.sizeUpTo (↑i : ℕ) ≤ (↑j : ℕ) ∧ (↑j : ℕ) < c.sizeUpTo (↑i : ℕ).succ

Tactic:
rcases Set.mem_range.2 h with ⟨k, hk⟩

Premises used: Iff.mpr, Set.mem_range
-- Module: Mathlib.Combinatorics.Enumerative.Composition
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.embedding i : (a : Fin (c.blocksFun i)) → Fin n) k) : ℕ) = (↑j : ℕ)

Tactic:
rw [Fin.ext_iff] at hk

Premises used: Fin.ext_iff
-- Module: Mathlib.Combinatorics.Enumerative.Composition
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 : ℕ)
mp : c.sizeUpTo (↑i : ℕ) ≤ c.sizeUpTo (↑i : ℕ) + (↑k : ℕ) ∧ c.sizeUpTo (↑i : ℕ) + (↑k : ℕ) < c.sizeUpTo (↑i : ℕ).succ
⊢ c.sizeUpTo (↑i : ℕ) ≤ (↑j : ℕ) ∧ (↑j : ℕ) < c.sizeUpTo (↑i : ℕ).succ

Tactic:
rw [← hk]
-- Module: Mathlib.Combinatorics.Enumerative.Composition
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 : ℕ) ≤ c.sizeUpTo (↑i : ℕ) + (↑k : ℕ) ∧ c.sizeUpTo (↑i : ℕ) + (↑k : ℕ) < c.sizeUpTo (↑i : ℕ).succ

Tactic:
simp [sizeUpTo_succ', k.is_lt]

Premises used: Fin.is_lt, Composition.sizeUpTo_succ'
-- Module: Mathlib.Combinatorics.Enumerative.Composition
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

Tactic:
⟨⟨j - c.sizeUpTo i, ?_⟩, ?_⟩

Premises used: HSub.hSub, Fin.mk, Fin.val, Exists.intro, Composition.sizeUpTo
-- Module: Mathlib.Combinatorics.Enumerative.Composition
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
mpr₁ : (c.embedding i : (a : Fin (c.blocksFun i)) → Fin n) ⟨(↑j : ℕ) - c.sizeUpTo (↑i : ℕ), ⋯⟩ = j
⊢ ∃ (y : Fin (c.blocksFun i)), (c.embedding i : (a : Fin (c.blocksFun i)) → Fin n) y = j

Tactic:
refine ⟨⟨j - c.sizeUpTo i, ?_⟩, ?_⟩
-- Module: Mathlib.Combinatorics.Enumerative.Composition
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)
mpr₁ : c.sizeUpTo (↑i : ℕ) ≤ (↑j : ℕ)
⊢ (↑j : ℕ) - c.sizeUpTo (↑i : ℕ) < c.blocksFun i

Tactic:
rw [tsub_lt_iff_left, ← sizeUpTo_succ']

Premises used: Composition.sizeUpTo_succ', tsub_lt_iff_left
-- Module: Mathlib.Combinatorics.Enumerative.Composition
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 : ℕ) + 1)

Tactic:
h.2

Premises used: And.right
-- Module: Mathlib.Combinatorics.Enumerative.Composition
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 : ℕ) + 1)

Tactic:
exact h.2

Premises used: And.right
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : c.sizeUpTo (↑i : ℕ) ≤ (↑j : ℕ) ∧ (↑j : ℕ) < c.sizeUpTo (↑i : ℕ).succ
⊢ c.sizeUpTo (↑i : ℕ) ≤ (↑j : ℕ)

Tactic:
h.1

Premises used: And.left
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : c.sizeUpTo (↑i : ℕ) ≤ (↑j : ℕ) ∧ (↑j : ℕ) < c.sizeUpTo (↑i : ℕ).succ
⊢ c.sizeUpTo (↑i : ℕ) ≤ (↑j : ℕ)

Tactic:
exact h.1

Premises used: And.left
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : c.sizeUpTo (↑i : ℕ) ≤ (↑j : ℕ) ∧ (↑j : ℕ) < c.sizeUpTo (↑i : ℕ).succ
mpr :
  (↑((c.embedding i : (a : Fin (c.blocksFun i)) → Fin n) (⟨(↑j : ℕ) - c.sizeUpTo (↑i : ℕ), ⋯⟩ : Fin (c.blocksFun i))) :
      ℕ) =
    (↑j : ℕ)
⊢ (c.embedding i : (a : Fin (c.blocksFun i)) → Fin n) ⟨(↑j : ℕ) - c.sizeUpTo (↑i : ℕ), ⋯⟩ = j

Tactic:
rw [Fin.ext_iff]

Premises used: Fin.ext_iff
-- Module: Mathlib.Combinatorics.Enumerative.Composition
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 : ℕ), ⋯⟩ : Fin (c.blocksFun i))) :
      ℕ) =
    (↑j : ℕ)

Tactic:
add_tsub_cancel_of_le h.1

Premises used: And.left, add_tsub_cancel_of_le
-- Module: Mathlib.Combinatorics.Enumerative.Composition
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 : ℕ), ⋯⟩ : Fin (c.blocksFun i))) :
      ℕ) =
    (↑j : ℕ)

Tactic:
exact add_tsub_cancel_of_le h.1

Premises used: And.left, add_tsub_cancel_of_le
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
i₁ i₂ : Fin c.length
h : i₁ ≠ i₂
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))
wlog :
  ∀ {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))
⊢ _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₂
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
i₁ i₂ : Fin c.length
h : i₁ ≠ i₂
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:
(this c h.symm (h.lt_or_gt.resolve_left h')).symm

Premises used: Or.resolve_left, Ne.symm, Disjoint.symm, Ne.lt_or_gt
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
i₁ i₂ : Fin c.length
h : i₁ ≠ i₂
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:
exact (this c h.symm (h.lt_or_gt.resolve_left h')).symm

Premises used: Or.resolve_left, Ne.symm, Disjoint.symm, Ne.lt_or_gt
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 : ℕ
c_1 : Composition n_1
n : ℕ
c : Composition n
i₁ i₂ : Fin c.length
h : i₁ ≠ i₂
h' : i₁ < i₂
by_contra :
  ∀
    (d :
      ¬_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))),
    False
⊢ _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:
by_contra d
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 : ℕ
c_1 : Composition n_1
n : ℕ
c : Composition n
i₁ i₂ : Fin c.length
h : i₁ ≠ i₂
h' : i₁ < i₂
d :
  ¬_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))
⊢ ∃ (x : Fin n),
    Membership.mem (γ := Set (Fin n))
        (Set.range (ι := Fin (c.blocksFun i₁)) (⇑(c.embedding i₁) : (a : Fin (c.blocksFun i₁)) → Fin n)) x ∧
      Membership.mem (γ := Set (Fin n))
        (Set.range (ι := Fin (c.blocksFun i₂)) (⇑(c.embedding i₂) : (a : Fin (c.blocksFun i₂)) → Fin n)) x

Tactic:
Set.not_disjoint_iff.1 d

Premises used: Set.not_disjoint_iff, Iff.mp
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 : ℕ
c_1 : Composition n_1
n : ℕ
c : Composition n
i₁ i₂ : Fin c.length
h : i₁ ≠ i₂
h' : i₁ < i₂
d :
  ¬_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))
obtain :
  ∀ (x : Fin n)
    (hx₁ :
      Membership.mem (γ := Set (Fin n))
        (Set.range (ι := Fin (c.blocksFun i₁)) (⇑(c.embedding i₁) : (a : Fin (c.blocksFun i₁)) → Fin n)) x)
    (hx₂ :
      Membership.mem (γ := Set (Fin n))
        (Set.range (ι := Fin (c.blocksFun i₂)) (⇑(c.embedding i₂) : (a : Fin (c.blocksFun i₂)) → Fin n)) x),
    False
⊢ False

Tactic:
obtain ⟨x, hx₁, hx₂⟩ :
      ∃ x : Fin n, x ∈ Set.range (c.embedding i₁) ∧ x ∈ Set.range (c.embedding i₂) :=
      Set.not_disjoint_iff.1 d

Premises used: Set.not_disjoint_iff, Composition.embedding, Iff.mp, Set.range, Fin, DFunLike.coe
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 : ℕ
c_1 : Composition n_1
n : ℕ
c : Composition n
i₁ i₂ : Fin c.length
h : i₁ ≠ i₂
h' : i₁ < i₂
d :
  ¬_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))
x : Fin n
hx₁ :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (c.blocksFun i₁)) (⇑(c.embedding i₁) : (a : Fin (c.blocksFun i₁)) → Fin n)) x
hx₂ :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (c.blocksFun i₂)) (⇑(c.embedding i₂) : (a : Fin (c.blocksFun i₂)) → Fin n)) x
⊢ (↑i₁ : ℕ).succ ≤ (↑i₂ : ℕ)

Tactic:
have A : (i₁ : ℕ).succ ≤ i₂ := Nat.succ_le_of_lt h'
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 : ℕ
c_1 : Composition n_1
n : ℕ
c : Composition n
i₁ i₂ : Fin c.length
h : i₁ ≠ i₂
h' : i₁ < i₂
d :
  ¬_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))
x : Fin n
hx₁ :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (c.blocksFun i₁)) (⇑(c.embedding i₁) : (a : Fin (c.blocksFun i₁)) → Fin n)) x
hx₂ :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (c.blocksFun i₂)) (⇑(c.embedding i₂) : (a : Fin (c.blocksFun i₂)) → Fin n)) x
A : (↑i₁ : ℕ).succ ≤ (↑i₂ : ℕ)
apply : (↑x : ℕ) < (↑x : ℕ)
⊢ False

Tactic:
apply lt_irrefl (x : ℕ)

Premises used: lt_irrefl, Fin.val
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 : ℕ
c_1 : Composition n_1
n : ℕ
c : Composition n
i₁ i₂ : Fin c.length
h : i₁ ≠ i₂
h' : i₁ < i₂
d :
  ¬_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))
x : Fin n
hx₁ :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (c.blocksFun i₁)) (⇑(c.embedding i₁) : (a : Fin (c.blocksFun i₁)) → Fin n)) x
hx₂ :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (c.blocksFun i₂)) (⇑(c.embedding i₂) : (a : Fin (c.blocksFun i₂)) → Fin n)) x
A : (↑i₁ : ℕ).succ ≤ (↑i₂ : ℕ)
⊢ (↑x : ℕ) < c.sizeUpTo (↑i₁ : ℕ).succ

Tactic:
(c.mem_range_embedding_iff.1 hx₁).2

Premises used: And.right, Iff.mp, Composition.mem_range_embedding_iff
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 : ℕ
c_1 : Composition n_1
n : ℕ
c : Composition n
i₁ i₂ : Fin c.length
h : i₁ ≠ i₂
h' : i₁ < i₂
d :
  ¬_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))
x : Fin n
hx₁ :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (c.blocksFun i₁)) (⇑(c.embedding i₁) : (a : Fin (c.blocksFun i₁)) → Fin n)) x
hx₂ :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (c.blocksFun i₂)) (⇑(c.embedding i₂) : (a : Fin (c.blocksFun i₂)) → Fin n)) x
A : (↑i₁ : ℕ).succ ≤ (↑i₂ : ℕ)
⊢ c.sizeUpTo (↑i₁ : ℕ).succ ≤ c.sizeUpTo (↑i₂ : ℕ)

Tactic:
monotone_sum_take _ A

Premises used: List.monotone_sum_take, Composition.sizeUpTo
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 : ℕ
c_1 : Composition n_1
n : ℕ
c : Composition n
i₁ i₂ : Fin c.length
h : i₁ ≠ i₂
h' : i₁ < i₂
d :
  ¬_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))
x : Fin n
hx₁ :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (c.blocksFun i₁)) (⇑(c.embedding i₁) : (a : Fin (c.blocksFun i₁)) → Fin n)) x
hx₂ :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (c.blocksFun i₂)) (⇑(c.embedding i₂) : (a : Fin (c.blocksFun i₂)) → Fin n)) x
A : (↑i₁ : ℕ).succ ≤ (↑i₂ : ℕ)
⊢ c.sizeUpTo (↑i₂ : ℕ) ≤ (↑x : ℕ)

Tactic:
(c.mem_range_embedding_iff.1 hx₂).1

Premises used: And.left, Iff.mp, Composition.mem_range_embedding_iff
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 : ℕ
c_1 : Composition n_1
n : ℕ
c : Composition n
i₁ i₂ : Fin c.length
h : i₁ ≠ i₂
h' : i₁ < i₂
d :
  ¬_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))
x : Fin n
hx₁ :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (c.blocksFun i₁)) (⇑(c.embedding i₁) : (a : Fin (c.blocksFun i₁)) → Fin n)) x
hx₂ :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (c.blocksFun i₂)) (⇑(c.embedding i₂) : (a : Fin (c.blocksFun i₂)) → Fin n)) x
A : (↑i₁ : ℕ).succ ≤ (↑i₂ : ℕ)
⊢ (↑x : ℕ) < (↑x : ℕ)

Tactic:
calc
      (x : ℕ) < c.sizeUpTo (i₁ : ℕ).succ := (c.mem_range_embedding_iff.1 hx₁).2
      _ ≤ c.sizeUpTo (i₂ : ℕ) := monotone_sum_take _ A
      _ ≤ x := (c.mem_range_embedding_iff.1 hx₂).1

Premises used: Fin.val, List.monotone_sum_take, And.right, And.left, Iff.mp, Nat.succ, Composition.sizeUpTo, Composition.mem_range_embedding_iff
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
j : Fin n
⊢ Membership.mem (α := Fin n) (γ := Set (Fin n))
    (Set.range (ι := Fin (c.blocksFun (c.index j)))
      (⇑(c.embedding (c.index j)) : (a : Fin (c.blocksFun (c.index j))) → Fin n))
    ((c.embedding (c.index j) : (a : Fin (c.blocksFun (c.index j))) → Fin n) (c.invEmbedding j) : Fin n)

Tactic:
have : c.embedding (c.index j) (c.invEmbedding j) ∈ Set.range (c.embedding (c.index j)) :=
    Set.mem_range_self _
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
j : Fin n
this :
  Membership.mem (α := Fin n) (γ := Set (Fin n))
    (Set.range (ι := Fin (c.blocksFun (c.index j)))
      (⇑(c.embedding (c.index j)) : (a : Fin (c.blocksFun (c.index j))) → Fin n))
    ((c.embedding (c.index j) : (a : Fin (c.blocksFun (c.index j))) → Fin n) (c.invEmbedding j) : Fin n)
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (this :
      Membership.mem (γ := Set (Fin n))
        (Set.range (ι := Fin (c.blocksFun (c.index j)))
          (⇑(c.embedding (c.index j)) : (a : Fin (c.blocksFun (c.index j))) → Fin n))
        j),
    Membership.mem (γ := Set (Fin n))
      (Set.range (ι := Fin (c.blocksFun (c.index j)))
        (⇑(c.embedding (c.index j)) : (a : Fin (c.blocksFun (c.index j))) → Fin n))
      j
⊢ Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (c.blocksFun (c.index j)))
      (⇑(c.embedding (c.index j)) : (a : Fin (c.blocksFun (c.index j))) → Fin n))
    j

Tactic:
rwa [c.embedding_comp_inv j] at this

Premises used: Composition.embedding_comp_inv
-- Module: Mathlib.Combinatorics.Enumerative.Composition
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 →
    i = c.index j
mpr :
  i = c.index j →
    Membership.mem (γ := Set (Fin n))
      (Set.range (ι := Fin (c.blocksFun i)) (⇑(c.embedding i) : (a : Fin (c.blocksFun i)) → Fin n)) j
⊢ Membership.mem (γ := Set (Fin n))
      (Set.range (ι := Fin (c.blocksFun i)) (⇑(c.embedding i) : (a : Fin (c.blocksFun i)) → Fin n)) j ↔
    i = c.index j

Tactic:
constructor
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
mp : ¬i = c.index j → j ∉ Set.range (ι := Fin (c.blocksFun i)) (⇑(c.embedding i) : (a : Fin (c.blocksFun i)) → Fin n)
⊢ Membership.mem (γ := Set (Fin n))
      (Set.range (ι := Fin (c.blocksFun i)) (⇑(c.embedding i) : (a : Fin (c.blocksFun i)) → Fin n)) j →
    i = c.index j

Tactic:
rw [← not_imp_not]

Premises used: not_imp_not
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : ¬i = c.index j
⊢ j ∉ Set.range (ι := Fin (c.blocksFun i)) (⇑(c.embedding i) : (a : Fin (c.blocksFun i)) → Fin n)

Tactic:
Set.disjoint_right.1 (c.disjoint_range h) (c.mem_range_embedding j)

Premises used: Set.disjoint_right, Composition.mem_range_embedding, Iff.mp, Composition.disjoint_range
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : ¬i = c.index j
⊢ j ∉ Set.range (ι := Fin (c.blocksFun i)) (⇑(c.embedding i) : (a : Fin (c.blocksFun i)) → Fin n)

Tactic:
exact Set.disjoint_right.1 (c.disjoint_range h) (c.mem_range_embedding j)

Premises used: Set.disjoint_right, Composition.mem_range_embedding, Iff.mp, Composition.disjoint_range
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : i = c.index j
mpr :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (c.blocksFun (c.index j)))
      (⇑(c.embedding (c.index j)) : (a : Fin (c.blocksFun (c.index j))) → Fin n))
    j
⊢ Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (c.blocksFun i)) (⇑(c.embedding i) : (a : Fin (c.blocksFun i)) → Fin n)) j

Tactic:
rw [h]
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : i = c.index j
⊢ Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (c.blocksFun (c.index j)))
      (⇑(c.embedding (c.index j)) : (a : Fin (c.blocksFun (c.index j))) → Fin n))
    j

Tactic:
c.mem_range_embedding j

Premises used: Composition.mem_range_embedding
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : i = c.index j
⊢ Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (c.blocksFun (c.index j)))
      (⇑(c.embedding (c.index j)) : (a : Fin (c.blocksFun (c.index j))) → Fin n))
    j

Tactic:
exact c.mem_range_embedding j

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

Tactic:
symm
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
i : Fin c.length
j : Fin (c.blocksFun i)
rw :
  Membership.mem (α := Fin n) (γ := Set (Fin n))
    (Set.range (ι := Fin (c.blocksFun i)) (⇑(c.embedding i) : (a : Fin (c.blocksFun i)) → Fin n))
    ((c.embedding i : (a : Fin (c.blocksFun i)) → Fin n) j : Fin n)
⊢ i = c.index ((c.embedding i : (a : Fin (c.blocksFun i)) → Fin n) j)

Tactic:
rw [← mem_range_embedding_iff']

Premises used: Composition.mem_range_embedding_iff'
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
i : Fin c.length
j : Fin (c.blocksFun i)
⊢ Membership.mem (α := Fin n) (γ := Set (Fin n))
    (Set.range (ι := Fin (c.blocksFun i)) (⇑(c.embedding i) : (a : Fin (c.blocksFun i)) → Fin n))
    ((c.embedding i : (a : Fin (c.blocksFun i)) → Fin n) j : Fin n)

Tactic:
apply Set.mem_range_self

Premises used: Set.mem_range_self
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
i : Fin c.length
j : Fin (c.blocksFun i)
simp_rw :
  (↑((c.embedding i : (a : Fin (c.blocksFun i)) → Fin n) j) : ℕ) -
      c.sizeUpTo (↑(c.index ((c.embedding i : (a : Fin (c.blocksFun i)) → Fin n) j)) : ℕ) =
    (↑j : ℕ)
simp_rw₁ : (↑((c.embedding i : (a : Fin (c.blocksFun i)) → Fin n) j) : ℕ) - c.sizeUpTo (↑i : ℕ) = (↑j : ℕ)
simp_rw₂ : c.sizeUpTo (↑i : ℕ) + (↑j : ℕ) - c.sizeUpTo (↑i : ℕ) = (↑j : ℕ)
⊢ (↑(c.invEmbedding ((c.embedding i : (a : Fin (c.blocksFun i)) → Fin n) j)) : ℕ) = (↑j : ℕ)

Tactic:
simp_rw [coe_invEmbedding, index_embedding, coe_embedding, add_tsub_cancel_left]

Premises used: Composition.index_embedding, add_tsub_cancel_left, Composition.coe_invEmbedding, Composition.coe_embedding