awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
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))
⊢ _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 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))
Tactic: wlog h' : i₁ < i₂
Cleared hypotheses: i₁, i₂, h
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n_1 : ℕ
c_1 : Composition n_1
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))
have 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
Tactic: by_contra d
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
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))
⊢ False
have 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
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
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (hypothesis)
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
⊢ False
have A : (↑i₁ : ℕ).succ ≤ (↑i₂ : ℕ)
Tactic: have A : (i₁ : ℕ).succ ≤ i₂ := Nat.succ_le_of_lt h'
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
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₂ : ℕ)
⊢ False
have apply : (↑x : ℕ) < (↑x : ℕ)
Tactic: apply lt_irrefl (x : ℕ)
-- 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: classical
    wlog h' : i₁ < i₂
    · exact (this c h.symm (h.lt_or_gt.resolve_left h')).symm
    by_contra d
    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
    have A : (i₁ : ℕ).succ ≤ i₂ := Nat.succ_le_of_lt h'
    apply lt_irrefl (x : ℕ)
    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
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
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))
⊢ _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 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))
Tactic: classical
    wlog h' : i₁ < i₂
    · exact (this c h.symm (h.lt_or_gt.resolve_left h')).symm
    by_contra d
    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
    have A : (i₁ : ℕ).succ ≤ i₂ := Nat.succ_le_of_lt h'
    apply lt_irrefl (x : ℕ)
    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
Cleared hypotheses: i₁, i₂, h
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
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 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))
have wlog₂ : ∀ {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))),
  False
Tactic: classical
    wlog h' : i₁ < i₂
    · exact (this c h.symm (h.lt_or_gt.resolve_left h')).symm
    by_contra d
    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
    have A : (i₁ : ℕ).succ ≤ i₂ := Nat.succ_le_of_lt h'
    apply lt_irrefl (x : ℕ)
    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
Cleared hypotheses: i₁, i₂, h
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
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 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))
wlog₂ :
  ∀ {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))),
    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))
have wlog₃ : ∀ {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),
  False
Tactic: classical
    wlog h' : i₁ < i₂
    · exact (this c h.symm (h.lt_or_gt.resolve_left h')).symm
    by_contra d
    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
    have A : (i₁ : ℕ).succ ≤ i₂ := Nat.succ_le_of_lt h'
    apply lt_irrefl (x : ℕ)
    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
Cleared hypotheses: i₁, i₂, h
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (hypothesis)
Goal:
n : ℕ
c : Composition n
j : Fin n
⊢ 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
have 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)
Tactic: have : c.embedding (c.index j) (c.invEmbedding j) ∈ Set.range (c.embedding (c.index j)) :=
    Set.mem_range_self _
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
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)
⊢ 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
have 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
Tactic: rwa [c.embedding_comp_inv j] at this
Cleared hypotheses: this
-- 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 ↔
    i = c.index j
have 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
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 →
    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 ↔
    i = c.index j
have 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
Tactic: constructor
-- 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 →
    i = c.index j
have mp : ¬i = c.index j → j ∉ Set.range (ι := Fin (c.blocksFun i)) (⇑(c.embedding i) : (a : Fin (c.blocksFun i)) → Fin n)
Tactic: rw [← not_imp_not]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
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 i)) (⇑(c.embedding i) : (a : Fin (c.blocksFun i)) → Fin n)) j
have 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
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
i : Fin c.length
j : Fin (c.blocksFun i)
⊢ c.index ((c.embedding i : (a : Fin (c.blocksFun i)) → Fin n) j) = i
have symm : i = c.index ((c.embedding i : (a : Fin (c.blocksFun i)) → Fin n) j)
Tactic: symm
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
i : Fin c.length
j : Fin (c.blocksFun i)
⊢ i = c.index ((c.embedding i : (a : Fin (c.blocksFun i)) → Fin n) j)
have 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)
Tactic: rw [← mem_range_embedding_iff']
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
i : Fin c.length
j : Fin (c.blocksFun i)
⊢ (↑(c.invEmbedding ((c.embedding i : (a : Fin (c.blocksFun i)) → Fin n) j)) : ℕ) = (↑j : ℕ)
have 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 : ℕ)
Tactic: simp_rw [coe_invEmbedding, index_embedding, coe_embedding, add_tsub_cancel_left]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
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 : ℕ)
⊢ (↑(c.invEmbedding ((c.embedding i : (a : Fin (c.blocksFun i)) → Fin n) j)) : ℕ) = (↑j : ℕ)
have simp_rw₁ : (↑((c.embedding i : (a : Fin (c.blocksFun i)) → Fin n) j) : ℕ) - c.sizeUpTo (↑i : ℕ) = (↑j : ℕ)
Tactic: simp_rw [coe_invEmbedding, index_embedding, coe_embedding, add_tsub_cancel_left]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
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 : ℕ)
⊢ (↑(c.invEmbedding ((c.embedding i : (a : Fin (c.blocksFun i)) → Fin n) j)) : ℕ) = (↑j : ℕ)
have simp_rw₂ : c.sizeUpTo (↑i : ℕ) + (↑j : ℕ) - c.sizeUpTo (↑i : ℕ) = (↑j : ℕ)
Tactic: simp_rw [coe_invEmbedding, index_embedding, coe_embedding, add_tsub_cancel_left]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
x : (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))
        x) =
    x
have 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)
Tactic: rcases x with ⟨i, y⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
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)
have 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)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
i : Fin c.length
y : Fin (c.blocksFun i)
⊢ 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)
have h : c.index ((c.embedding i : (a : Fin (c.blocksFun i)) → Fin n) y) = i
Tactic: congr
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
i : Fin c.length
y : Fin (c.blocksFun i)
h : c.index ((c.embedding i : (a : Fin (c.blocksFun i)) → Fin n) y) = i
⊢ 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)
have 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
Tactic: congr
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
i : Fin c.length
y : Fin (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
have h : (↑(c.invEmbedding ((c.embedding i : (a : Fin (c.blocksFun i)) → Fin n) y)) : ℕ) = (↑y : ℕ)
Tactic: rw [Fin.heq_ext_iff]