awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (hypothesis)
Goal:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
⊢ d.blocks = c.blocks
have length_eq : d.blocks.length = c.blocks.length
Tactic: have length_eq : d.blocks.length = c.blocks.length := by simp [d, blocks_length]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
⊢ d.blocks = c.blocks
have suffices : ∀ i ≤ d.blocks.length, (take i d.blocks).sum = (take i c.blocks).sum
Tactic: suffices H : ∀ i ≤ d.blocks.length, (d.blocks.take i).sum = (c.blocks.take i).sum from
    eq_of_sum_take_eq length_eq H
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (hypothesis)
Goal:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
⊢ (take i d.blocks).sum = (take i c.blocks).sum
have i_lt : i < d.boundaries.card
Tactic: have i_lt : i < d.boundaries.card := by
    simpa [CompositionAsSet.blocks, length_ofFn,
      d.card_boundaries_eq_succ_length] using Nat.lt_succ_iff.2 hi
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (hypothesis)
Goal:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
i_lt : i < d.boundaries.card
⊢ (take i d.blocks).sum = (take i c.blocks).sum
have i_lt' : i < c.boundaries.card
Tactic: have i_lt' : i < c.boundaries.card := i_lt
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
i_lt : i < d.boundaries.card
i_lt' : i < c.boundaries.card
⊢ i < c.length + 1
have rwa : ∀ (i_lt' : i < c.length + 1), i < c.length + 1
Tactic: rwa [c.card_boundaries_eq_succ_length] at i_lt'
Cleared hypotheses: i_lt'
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (hypothesis)
Goal:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
i_lt : i < d.boundaries.card
i_lt' : i < c.boundaries.card
⊢ (take i d.blocks).sum = (take i c.blocks).sum
have i_lt'' : i < c.length + 1
Tactic: have i_lt'' : i < c.length + 1 := by rwa [c.card_boundaries_eq_succ_length] at i_lt'
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (hypothesis)
Goal:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
i_lt : i < d.boundaries.card
i_lt' : i < c.boundaries.card
i_lt'' : i < c.length + 1
⊢ (take i d.blocks).sum = (take i c.blocks).sum
have A : Eq (α := Fin n.succ) ((d.boundaries.orderEmbOfFin sorry : (a : Fin d.boundaries.card) → Fin n.succ) ⟨i, i_lt⟩ : Fin n.succ)
  ((c.boundaries.orderEmbOfFin sorry : (a : Fin (c.length + 1)) → Fin (n + 1)) ⟨i, i_lt''⟩ : Fin (n + 1))
Tactic: have A :
    d.boundaries.orderEmbOfFin rfl ⟨i, i_lt⟩ =
      c.boundaries.orderEmbOfFin c.card_boundaries_eq_succ_length ⟨i, i_lt''⟩ :=
    rfl
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (hypothesis)
Goal:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
i_lt : i < d.boundaries.card
i_lt' : i < c.boundaries.card
i_lt'' : i < c.length + 1
A :
  Eq (α := Fin n.succ)
    ((d.boundaries.orderEmbOfFin ⋯ : (a : Fin d.boundaries.card) → Fin n.succ) ⟨i, i_lt⟩ : Fin n.succ)
    ((c.boundaries.orderEmbOfFin ⋯ : (a : Fin (c.length + 1)) → Fin (n + 1)) ⟨i, i_lt''⟩ : Fin (n + 1))
⊢ (take i d.blocks).sum = (take i c.blocks).sum
have B : c.sizeUpTo i = (↑((c.boundary : (a : Fin (c.length + 1)) → Fin (n + 1)) ⟨i, i_lt''⟩) : ℕ)
Tactic: have B : c.sizeUpTo i = c.boundary ⟨i, i_lt''⟩ := rfl
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
i_lt : i < d.boundaries.card
i_lt' : i < c.boundaries.card
i_lt'' : i < c.length + 1
A :
  Eq (α := Fin n.succ)
    ((d.boundaries.orderEmbOfFin ⋯ : (a : Fin d.boundaries.card) → Fin n.succ) ⟨i, i_lt⟩ : Fin n.succ)
    ((c.boundaries.orderEmbOfFin ⋯ : (a : Fin (c.length + 1)) → Fin (n + 1)) ⟨i, i_lt''⟩ : Fin (n + 1))
B : c.sizeUpTo i = (↑((c.boundary : (a : Fin (c.length + 1)) → Fin (n + 1)) ⟨i, i_lt''⟩) : ℕ)
⊢ (take i d.blocks).sum = (take i c.blocks).sum
have rw : (↑((d.boundary : (a : Fin d.boundaries.card) → Fin (n + 1)) (⟨i, i_lt⟩ : Fin d.boundaries.card)) : ℕ) =
  (take i c.blocks).sum
Tactic: rw [d.blocks_partial_sum i_lt, CompositionAsSet.boundary, ← Composition.sizeUpTo, B, A,
    c.orderEmbOfFin_boundaries]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
i_lt : i < d.boundaries.card
i_lt' : i < c.boundaries.card
i_lt'' : i < c.length + 1
A :
  Eq (α := Fin n.succ)
    ((d.boundaries.orderEmbOfFin ⋯ : (a : Fin d.boundaries.card) → Fin n.succ) ⟨i, i_lt⟩ : Fin n.succ)
    ((c.boundaries.orderEmbOfFin ⋯ : (a : Fin (c.length + 1)) → Fin (n + 1)) ⟨i, i_lt''⟩ : Fin (n + 1))
B : c.sizeUpTo i = (↑((c.boundary : (a : Fin (c.length + 1)) → Fin (n + 1)) ⟨i, i_lt''⟩) : ℕ)
rw :
  (↑((d.boundary : (a : Fin d.boundaries.card) → Fin (n + 1)) (⟨i, i_lt⟩ : Fin d.boundaries.card)) : ℕ) =
    (take i c.blocks).sum
⊢ (take i d.blocks).sum = (take i c.blocks).sum
have rw₁ : (↑((d.boundaries.orderEmbOfFin sorry : (a : Fin d.boundaries.card) → Fin (n + 1)) (⟨i, i_lt⟩ : Fin d.boundaries.card)) :
    ℕ) =
  (take i c.blocks).sum
Tactic: rw [d.blocks_partial_sum i_lt, CompositionAsSet.boundary, ← Composition.sizeUpTo, B, A,
    c.orderEmbOfFin_boundaries]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
i_lt : i < d.boundaries.card
i_lt' : i < c.boundaries.card
i_lt'' : i < c.length + 1
A :
  Eq (α := Fin n.succ)
    ((d.boundaries.orderEmbOfFin ⋯ : (a : Fin d.boundaries.card) → Fin n.succ) ⟨i, i_lt⟩ : Fin n.succ)
    ((c.boundaries.orderEmbOfFin ⋯ : (a : Fin (c.length + 1)) → Fin (n + 1)) ⟨i, i_lt''⟩ : Fin (n + 1))
B : c.sizeUpTo i = (↑((c.boundary : (a : Fin (c.length + 1)) → Fin (n + 1)) ⟨i, i_lt''⟩) : ℕ)
rw :
  (↑((d.boundary : (a : Fin d.boundaries.card) → Fin (n + 1)) (⟨i, i_lt⟩ : Fin d.boundaries.card)) : ℕ) =
    (take i c.blocks).sum
rw₁ :
  (↑((d.boundaries.orderEmbOfFin ⋯ : (a : Fin d.boundaries.card) → Fin (n + 1)) (⟨i, i_lt⟩ : Fin d.boundaries.card)) :
      ℕ) =
    (take i c.blocks).sum
⊢ (take i d.blocks).sum = (take i c.blocks).sum
have rw₂ : (↑((d.boundaries.orderEmbOfFin sorry : (a : Fin d.boundaries.card) → Fin (n + 1)) (⟨i, i_lt⟩ : Fin d.boundaries.card)) :
    ℕ) =
  c.sizeUpTo i
Tactic: rw [d.blocks_partial_sum i_lt, CompositionAsSet.boundary, ← Composition.sizeUpTo, B, A,
    c.orderEmbOfFin_boundaries]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
i_lt : i < d.boundaries.card
i_lt' : i < c.boundaries.card
i_lt'' : i < c.length + 1
A :
  Eq (α := Fin n.succ)
    ((d.boundaries.orderEmbOfFin ⋯ : (a : Fin d.boundaries.card) → Fin n.succ) ⟨i, i_lt⟩ : Fin n.succ)
    ((c.boundaries.orderEmbOfFin ⋯ : (a : Fin (c.length + 1)) → Fin (n + 1)) ⟨i, i_lt''⟩ : Fin (n + 1))
B : c.sizeUpTo i = (↑((c.boundary : (a : Fin (c.length + 1)) → Fin (n + 1)) ⟨i, i_lt''⟩) : ℕ)
rw :
  (↑((d.boundary : (a : Fin d.boundaries.card) → Fin (n + 1)) (⟨i, i_lt⟩ : Fin d.boundaries.card)) : ℕ) =
    (take i c.blocks).sum
rw₁ :
  (↑((d.boundaries.orderEmbOfFin ⋯ : (a : Fin d.boundaries.card) → Fin (n + 1)) (⟨i, i_lt⟩ : Fin d.boundaries.card)) :
      ℕ) =
    (take i c.blocks).sum
rw₂ :
  (↑((d.boundaries.orderEmbOfFin ⋯ : (a : Fin d.boundaries.card) → Fin (n + 1)) (⟨i, i_lt⟩ : Fin d.boundaries.card)) :
      ℕ) =
    c.sizeUpTo i
⊢ (take i d.blocks).sum = (take i c.blocks).sum
have rw₃ : (↑((d.boundaries.orderEmbOfFin sorry : (a : Fin d.boundaries.card) → Fin (n + 1)) (⟨i, i_lt⟩ : Fin d.boundaries.card)) :
    ℕ) =
  (↑((c.boundary : (a : Fin (c.length + 1)) → Fin (n + 1)) ⟨i, i_lt''⟩) : ℕ)
Tactic: rw [d.blocks_partial_sum i_lt, CompositionAsSet.boundary, ← Composition.sizeUpTo, B, A,
    c.orderEmbOfFin_boundaries]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
i_lt : i < d.boundaries.card
i_lt' : i < c.boundaries.card
i_lt'' : i < c.length + 1
A :
  Eq (α := Fin n.succ)
    ((d.boundaries.orderEmbOfFin ⋯ : (a : Fin d.boundaries.card) → Fin n.succ) ⟨i, i_lt⟩ : Fin n.succ)
    ((c.boundaries.orderEmbOfFin ⋯ : (a : Fin (c.length + 1)) → Fin (n + 1)) ⟨i, i_lt''⟩ : Fin (n + 1))
B : c.sizeUpTo i = (↑((c.boundary : (a : Fin (c.length + 1)) → Fin (n + 1)) ⟨i, i_lt''⟩) : ℕ)
rw :
  (↑((d.boundary : (a : Fin d.boundaries.card) → Fin (n + 1)) (⟨i, i_lt⟩ : Fin d.boundaries.card)) : ℕ) =
    (take i c.blocks).sum
rw₁ :
  (↑((d.boundaries.orderEmbOfFin ⋯ : (a : Fin d.boundaries.card) → Fin (n + 1)) (⟨i, i_lt⟩ : Fin d.boundaries.card)) :
      ℕ) =
    (take i c.blocks).sum
rw₂ :
  (↑((d.boundaries.orderEmbOfFin ⋯ : (a : Fin d.boundaries.card) → Fin (n + 1)) (⟨i, i_lt⟩ : Fin d.boundaries.card)) :
      ℕ) =
    c.sizeUpTo i
rw₃ :
  (↑((d.boundaries.orderEmbOfFin ⋯ : (a : Fin d.boundaries.card) → Fin (n + 1)) (⟨i, i_lt⟩ : Fin d.boundaries.card)) :
      ℕ) =
    (↑((c.boundary : (a : Fin (c.length + 1)) → Fin (n + 1)) ⟨i, i_lt''⟩) : ℕ)
⊢ (take i d.blocks).sum = (take i c.blocks).sum
have rw₄ : (↑((c.boundaries.orderEmbOfFin sorry : (a : Fin (c.length + 1)) → Fin (n + 1)) (⟨i, i_lt''⟩ : Fin (c.length + 1))) : ℕ) =
  (↑((c.boundary : (a : Fin (c.length + 1)) → Fin (n + 1)) ⟨i, i_lt''⟩) : ℕ)
Tactic: rw [d.blocks_partial_sum i_lt, CompositionAsSet.boundary, ← Composition.sizeUpTo, B, A,
    c.orderEmbOfFin_boundaries]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
i_lt : i < d.boundaries.card
i_lt' : i < c.boundaries.card
i_lt'' : i < c.length + 1
A :
  Eq (α := Fin n.succ)
    ((d.boundaries.orderEmbOfFin ⋯ : (a : Fin d.boundaries.card) → Fin n.succ) ⟨i, i_lt⟩ : Fin n.succ)
    ((c.boundaries.orderEmbOfFin ⋯ : (a : Fin (c.length + 1)) → Fin (n + 1)) ⟨i, i_lt''⟩ : Fin (n + 1))
B : c.sizeUpTo i = (↑((c.boundary : (a : Fin (c.length + 1)) → Fin (n + 1)) ⟨i, i_lt''⟩) : ℕ)
rw :
  (↑((d.boundary : (a : Fin d.boundaries.card) → Fin (n + 1)) (⟨i, i_lt⟩ : Fin d.boundaries.card)) : ℕ) =
    (take i c.blocks).sum
rw₁ :
  (↑((d.boundaries.orderEmbOfFin ⋯ : (a : Fin d.boundaries.card) → Fin (n + 1)) (⟨i, i_lt⟩ : Fin d.boundaries.card)) :
      ℕ) =
    (take i c.blocks).sum
rw₂ :
  (↑((d.boundaries.orderEmbOfFin ⋯ : (a : Fin d.boundaries.card) → Fin (n + 1)) (⟨i, i_lt⟩ : Fin d.boundaries.card)) :
      ℕ) =
    c.sizeUpTo i
rw₃ :
  (↑((d.boundaries.orderEmbOfFin ⋯ : (a : Fin d.boundaries.card) → Fin (n + 1)) (⟨i, i_lt⟩ : Fin d.boundaries.card)) :
      ℕ) =
    (↑((c.boundary : (a : Fin (c.length + 1)) → Fin (n + 1)) ⟨i, i_lt''⟩) : ℕ)
rw₄ :
  (↑((c.boundaries.orderEmbOfFin ⋯ : (a : Fin (c.length + 1)) → Fin (n + 1)) (⟨i, i_lt''⟩ : Fin (c.length + 1))) : ℕ) =
    (↑((c.boundary : (a : Fin (c.length + 1)) → Fin (n + 1)) ⟨i, i_lt''⟩) : ℕ)
⊢ (take i d.blocks).sum = (take i c.blocks).sum
have rw₅ : (↑((c.boundary : (a : Fin (c.length + 1)) → Fin (n + 1)) (⟨i, i_lt''⟩ : Fin (c.length + 1))) : ℕ) =
  (↑((c.boundary : (a : Fin (c.length + 1)) → Fin (n + 1)) ⟨i, i_lt''⟩) : ℕ)
Tactic: rw [d.blocks_partial_sum i_lt, CompositionAsSet.boundary, ← Composition.sizeUpTo, B, A,
    c.orderEmbOfFin_boundaries]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : CompositionAsSet n
⊢ c.toComposition.boundaries = c.boundaries
have h : ∀ (j : ℕ) (hj : j < n + 1),
  (⟨j, hj⟩ : Fin (n + 1)) ∈ c.toComposition.boundaries ↔ (⟨j, hj⟩ : Fin (n + 1)) ∈ c.boundaries
Tactic: ext ⟨j, hj⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n_1 n : ℕ
c : Composition n
⊢ (fun (c : CompositionAsSet n) ↦ c.toComposition) ((fun (c : Composition n) ↦ c.toCompositionAsSet) c) = c
have blocks : Composition.blocks (n := n)
    ((fun (c : CompositionAsSet n) ↦ c.toComposition) ((fun (c : Composition n) ↦ c.toCompositionAsSet) c)) =
  c.blocks
Tactic: ext1
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n_1 n : ℕ
c : CompositionAsSet n
⊢ (fun (c : Composition n) ↦ c.toCompositionAsSet) ((fun (c : CompositionAsSet n) ↦ c.toComposition) c) = c
have boundaries : CompositionAsSet.boundaries
    ((fun (c : Composition n) ↦ c.toCompositionAsSet) ((fun (c : CompositionAsSet n) ↦ c.toComposition) c)) =
  c.boundaries
Tactic: ext1
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
⊢ Fintype.card (Composition n) = HPow.hPow (α := ℕ) 2 (n - 1)
have rw : Fintype.card (Composition n) = Fintype.card (CompositionAsSet n)
Tactic: rw [← compositionAsSet_card n]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DoubleCounting (goal)
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
inst : CommMonoid R
f : α → β → R
inst_1 : (a : α) → (b : β) → Decidable (r a b)
⊢ Eq.{u_1 + 1} (α := R) (∏ a ∈ s, ∏ b ∈ bipartiteAbove r t a, f a b) (∏ b ∈ t, ∏ a ∈ bipartiteBelow r s b, f a b)
have simp_rw : Eq.{u_1 + 1} (α := R) (∏ x ∈ s, ∏ a ∈ t, if r x a then f x a else 1) (∏ x ∈ t, ∏ a ∈ s, if r a x then f a x else 1)
Tactic: simp_rw [bipartiteAbove, bipartiteBelow, prod_filter]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DoubleCounting (goal)
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
inst : (a : α) → (b : β) → Decidable (r a b)
⊢ Eq (α := ℕ) (∑ a ∈ s, #(bipartiteAbove r t a)) (∑ b ∈ t, #(bipartiteBelow r s b))
have simp_rw : Eq (α := ℕ) (∑ x ∈ s, ∑ x ∈ bipartiteAbove r t x, 1) (∑ x ∈ t, ∑ x ∈ bipartiteBelow r s x, 1)
Tactic: simp_rw [card_eq_sum_ones, sum_sum_bipartiteAbove_eq_sum_sum_bipartiteBelow]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DoubleCounting (goal)
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
m n : R
inst_3 : (a : α) → (b : β) → Decidable (r a b)
hm : ∀ a ∈ s, m ≤ (↑(#(bipartiteAbove r t a)) : R)
hn : ∀ b ∈ t, (↑(#(bipartiteBelow r s b)) : R) ≤ n
⊢ Eq.{u_1 + 1} (α := R) (∑ a ∈ s, (↑(#(bipartiteAbove r t a)) : R)) (∑ b ∈ t, (↑(#(bipartiteBelow r s b)) : R))
have norm_cast : Eq.{u_1 + 1} (α := R) (↑(∑ x ∈ s, #(bipartiteAbove r t x)) : R) (↑(∑ x ∈ t, #(bipartiteBelow r s x)) : R)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DoubleCounting (goal)
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
m n : R
inst_3 : (a : α) → (b : β) → Decidable (r a b)
hm : ∀ a ∈ s, m ≤ (↑(#(bipartiteAbove r t a)) : R)
hn : ∀ b ∈ t, (↑(#(bipartiteBelow r s b)) : R) ≤ n
⊢ Eq.{u_1 + 1} (α := R) (↑(∑ x ∈ s, #(bipartiteAbove r t x)) : R) (↑(∑ x ∈ t, #(bipartiteBelow r s x)) : R)
have rw : Eq.{u_1 + 1} (α := R) (↑(∑ b ∈ t, #(bipartiteBelow r s b)) : R) (↑(∑ x ∈ t, #(bipartiteBelow r s x)) : R)
Tactic: rw [sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DoubleCounting (goal)
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
r : α → β → Prop
s : Finset α
t : Finset β
m n : R
inst_3 : (a : α) → (b : β) → Decidable (r a b)
hs : s.Nonempty
hm : ∀ a ∈ s, m < (↑(#(bipartiteAbove r t a)) : R)
hn : ∀ b ∈ t, (↑(#(bipartiteBelow r s b)) : R) ≤ n
⊢ #s • m = ∑ _a ∈ s, m
have rw : #s • m = #s • m
Tactic: rw [sum_const]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DoubleCounting (goal)
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
r : α → β → Prop
s : Finset α
t : Finset β
m n : R
inst_3 : (a : α) → (b : β) → Decidable (r a b)
hs : s.Nonempty
hm : ∀ a ∈ s, m < (↑(#(bipartiteAbove r t a)) : R)
hn : ∀ b ∈ t, (↑(#(bipartiteBelow r s b)) : R) ≤ n
⊢ Eq.{u_1 + 1} (α := R) (∑ a ∈ s, (↑(#(bipartiteAbove r t a)) : R)) (∑ b ∈ t, (↑(#(bipartiteBelow r s b)) : R))
have norm_cast : Eq (α := ℕ) (∑ x ∈ s, #(bipartiteAbove r t x)) (∑ x ∈ t, #(bipartiteBelow r s x))
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DoubleCounting (goal)
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
r : α → β → Prop
s : Finset α
t : Finset β
m n : R
inst_3 : (a : α) → (b : β) → Decidable (r a b)
hs : s.Nonempty
hm : ∀ a ∈ s, m < (↑(#(bipartiteAbove r t a)) : R)
hn : ∀ b ∈ t, (↑(#(bipartiteBelow r s b)) : R) ≤ n
⊢ Eq (α := ℕ) (∑ x ∈ s, #(bipartiteAbove r t x)) (∑ x ∈ t, #(bipartiteBelow r s x))
have rw : Eq (α := ℕ) (∑ b ∈ t, #(bipartiteBelow r s b)) (∑ x ∈ t, #(bipartiteBelow r s x))
Tactic: rw [sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DoubleCounting (goal)
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
r : α → β → Prop
s : Finset α
t : Finset β
m n : R
inst_3 : (a : α) → (b : β) → Decidable (r a b)
ht : t.Nonempty
hm : ∀ a ∈ s, m ≤ (↑(#(bipartiteAbove r t a)) : R)
hn : ∀ b ∈ t, (↑(#(bipartiteBelow r s b)) : R) < n
⊢ Eq.{u_1 + 1} (α := R) (∑ a ∈ s, (↑(#(bipartiteAbove r t a)) : R)) (∑ b ∈ t, (↑(#(bipartiteBelow r s b)) : R))
have norm_cast : Eq (α := ℕ) (∑ x ∈ s, #(bipartiteAbove r t x)) (∑ x ∈ t, #(bipartiteBelow r s x))
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DoubleCounting (goal)
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
r : α → β → Prop
s : Finset α
t : Finset β
m n : R
inst_3 : (a : α) → (b : β) → Decidable (r a b)
ht : t.Nonempty
hm : ∀ a ∈ s, m ≤ (↑(#(bipartiteAbove r t a)) : R)
hn : ∀ b ∈ t, (↑(#(bipartiteBelow r s b)) : R) < n
⊢ Eq (α := ℕ) (∑ x ∈ s, #(bipartiteAbove r t x)) (∑ x ∈ t, #(bipartiteBelow r s x))
have rw : Eq (α := ℕ) (∑ b ∈ t, #(bipartiteBelow r s b)) (∑ x ∈ t, #(bipartiteBelow r s x))
Tactic: rw [sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DoubleCounting (goal)
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
hs : ∀ a ∈ s, ∃ b ∈ t, r a b
ht : ∀ b ∈ t, Set.Subsingleton.{u_2} (α := α) {a : α | a ∈ s ∧ r a b}
⊢ #s ≤ #t
have rw : #s * 1 ≤ #t * 1
Tactic: rw [← mul_one #s, ← mul_one #t]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DoubleCounting (goal)
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
hs : ∀ a ∈ s, ∃ b ∈ t, r a b
ht : ∀ b ∈ t, Set.Subsingleton.{u_2} (α := α) {a : α | a ∈ s ∧ r a b}
a : α
h : a ∈ s
⊢ (bipartiteAbove r t a).Nonempty
have rw : Set.Nonempty.{u_3} (α := β) {b : β | b ∈ t ∧ r a b}
Tactic: rw [← coe_nonempty, coe_bipartiteAbove]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DoubleCounting (goal)
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
hs : ∀ a ∈ s, ∃ b ∈ t, r a b
ht : ∀ b ∈ t, Set.Subsingleton.{u_2} (α := α) {a : α | a ∈ s ∧ r a b}
b : β
h : b ∈ t
⊢ ∀ a ∈ bipartiteBelow r s b, ∀ b_1 ∈ bipartiteBelow r s b, a = b_1
have simp_rw : ∀ (a : α), a ∈ s ∧ r a b → ∀ (b_1 : α), b_1 ∈ s ∧ r b_1 b → a = b_1
Tactic: simp_rw [mem_bipartiteBelow]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DoubleCounting (goal)
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
hs : ∀ a ∈ s, ∃ b ∈ t, r a b
ht : ∀ b ∈ t, Set.Subsingleton.{u_2} (α := α) {a : α | a ∈ s ∧ r a b}
⊢ #s ≤ #t
have rw : #s * 1 ≤ #t
Tactic: classical
    rw [← mul_one #s, ← mul_one #t]
    exact card_mul_le_card_mul r
      (fun a h ↦ card_pos.2 (by
        rw [← coe_nonempty, coe_bipartiteAbove]
        exact hs _ h : (t.bipartiteAbove r a).Nonempty))
      (fun b h ↦ card_le_one.2 (by
        simp_rw [mem_bipartiteBelow]
        exact ht _ h))
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DoubleCounting (goal)
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
hs : ∀ a ∈ s, ∃ b ∈ t, r a b
ht : ∀ b ∈ t, Set.Subsingleton.{u_2} (α := α) {a : α | a ∈ s ∧ r a b}
rw : #s * 1 ≤ #t
⊢ #s ≤ #t
have rw₁ : #s * 1 ≤ #t * 1
Tactic: classical
    rw [← mul_one #s, ← mul_one #t]
    exact card_mul_le_card_mul r
      (fun a h ↦ card_pos.2 (by
        rw [← coe_nonempty, coe_bipartiteAbove]
        exact hs _ h : (t.bipartiteAbove r a).Nonempty))
      (fun b h ↦ card_le_one.2 (by
        simp_rw [mem_bipartiteBelow]
        exact ht _ h))
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
s : DyckStep
⊢ s = U ∨ s = D
have U : U = U ∨ U = D
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
s : DyckStep
U : DyckStep.U = DyckStep.U ∨ DyckStep.U = D
⊢ s = DyckStep.U ∨ s = D
have D : D = DyckStep.U ∨ D = D
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
⊢ U = U ∨ U = D
have U : ¬U = U → U = D
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
⊢ D = U ∨ D = D
have D : ¬D = U → D = D
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p q : DyckWord
⊢ ∀ (i : ℕ),
    count D (take i ((↑p : List DyckStep) ++ (↑q : List DyckStep))) ≤
      count U (take i ((↑p : List DyckStep) ++ (↑q : List DyckStep)))
have simp : ∀ (i : ℕ),
  count D (take i (↑p : List DyckStep)) + count D (take (i - (↑p : List DyckStep).length) (↑q : List DyckStep)) ≤
    count U (take i (↑p : List DyckStep)) + count U (take (i - (↑p : List DyckStep).length) (↑q : List DyckStep))
Tactic: simp only [take_append, count_append]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p q r : DyckWord
⊢ p + q + r = p + (q + r)
have toList : (↑(p + q + r) : List DyckStep) = (↑(p + (q + r)) : List DyckStep)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p : DyckWord
⊢ 0 + p = p
have toList : (↑(0 + p) : List DyckStep) = (↑p : List DyckStep)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p : DyckWord
⊢ p + 0 = p
have toList : (↑(p + 0) : List DyckStep) = (↑p : List DyckStep)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p q r : DyckWord
h : Eq (α := DyckWord) ((fun (x : DyckWord) ↦ p + x) q) ((fun (x : DyckWord) ↦ p + x) r)
⊢ q = r
have rw : ∀ (h : (↑((fun (x : DyckWord) ↦ p + x) q) : List DyckStep) = (↑((fun (x : DyckWord) ↦ p + x) r) : List DyckStep)),
  (↑q : List DyckStep) = (↑r : List DyckStep)
Tactic: rw [DyckWord.ext_iff] at *
Cleared hypotheses: h