awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
rw : Fintype.card (Composition n) = Fintype.card (CompositionAsSet n)
⊢ Fintype.card (Composition n) = HPow.hPow (α := ℕ) 2 (n - 1)

Tactic:
rw [← compositionAsSet_card n]

Premises used: compositionAsSet_card
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
⊢ Fintype.card (Composition n) = Fintype.card (CompositionAsSet n)

Tactic:
Fintype.card_congr (compositionEquiv n)

Premises used: Fintype.card_congr, compositionEquiv
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
⊢ Fintype.card (Composition n) = Fintype.card (CompositionAsSet n)

Tactic:
exact Fintype.card_congr (compositionEquiv n)

Premises used: Fintype.card_congr, compositionEquiv
-- Module: Mathlib.Combinatorics.Enumerative.DoubleCounting
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
t : Finset β
a : α
inst : DecidablePred (r a)
⊢ bipartiteBelow (swap (φ := fun (a : α) (a_1 : β) ↦ Prop) r) t a = bipartiteAbove r t a

Tactic:
rfl

Premises used: Finset.bipartiteAbove, rfl
-- Module: Mathlib.Combinatorics.Enumerative.DoubleCounting
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
b : β
inst : (a : α) → Decidable (r a b)
⊢ bipartiteAbove (swap (φ := fun (a : α) (a_1 : β) ↦ Prop) r) s b = bipartiteBelow r s b

Tactic:
rfl

Premises used: Finset.bipartiteBelow, rfl
-- Module: Mathlib.Combinatorics.Enumerative.DoubleCounting
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
b : β
inst : (a : α) → Decidable (r a b)
⊢ (↑(bipartiteBelow r s b) : Set α) = {a : α | a ∈ s ∧ r a b}

Tactic:
coe_filter _ _

Premises used: Finset.coe_filter, setOf
-- Module: Mathlib.Combinatorics.Enumerative.DoubleCounting
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
t : Finset β
a : α
inst : DecidablePred (r a)
⊢ (↑(bipartiteAbove r t a) : Set β) = {b : β | b ∈ t ∧ r a b}

Tactic:
coe_filter _ _

Premises used: Finset.coe_filter, setOf
-- Module: Mathlib.Combinatorics.Enumerative.DoubleCounting
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
b : β
inst : (a : α) → Decidable (r a b)
a : α
⊢ a ∈ bipartiteBelow r s b ↔ a ∈ s ∧ r a b

Tactic:
mem_filter

Premises used: Set.Mem, setOf, Finset.mem_filter
-- Module: Mathlib.Combinatorics.Enumerative.DoubleCounting
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
t : Finset β
a : α
inst : DecidablePred (r a)
b : β
⊢ b ∈ bipartiteAbove r t a ↔ b ∈ t ∧ r a b

Tactic:
mem_filter

Premises used: Set.Mem, setOf, Finset.mem_filter
-- Module: Mathlib.Combinatorics.Enumerative.DoubleCounting
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)
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)
⊢ 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)

Tactic:
simp_rw [bipartiteAbove, bipartiteBelow, prod_filter]

Premises used: Finset.bipartiteAbove, Finset.prod_filter, Finset.bipartiteBelow
-- Module: Mathlib.Combinatorics.Enumerative.DoubleCounting
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) (∏ 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:
prod_comm

Premises used: Finset.prod_comm
-- Module: Mathlib.Combinatorics.Enumerative.DoubleCounting
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) (∏ 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:
exact prod_comm

Premises used: Finset.prod_comm
-- Module: Mathlib.Combinatorics.Enumerative.DoubleCounting
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
inst : (a : α) → (b : β) → Decidable (r a b)
simp_rw : Eq (α := ℕ) (∑ x ∈ s, ∑ x ∈ bipartiteAbove r t x, 1) (∑ x ∈ t, ∑ x ∈ bipartiteBelow r s x, 1)
⊢ Eq (α := ℕ) (∑ a ∈ s, #(bipartiteAbove r t a)) (∑ b ∈ t, #(bipartiteBelow r s b))

Tactic:
simp_rw [card_eq_sum_ones, sum_sum_bipartiteAbove_eq_sum_sum_bipartiteBelow]

Premises used: Finset.card_eq_sum_ones, Finset.sum_sum_bipartiteAbove_eq_sum_sum_bipartiteBelow
-- Module: Mathlib.Combinatorics.Enumerative.DoubleCounting
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
norm_cast : Eq.{u_1 + 1} (α := R) (↑(∑ x ∈ s, #(bipartiteAbove r t x)) : R) (↑(∑ x ∈ t, #(bipartiteBelow r s x)) : R)
⊢ Eq.{u_1 + 1} (α := R) (∑ a ∈ s, (↑(#(bipartiteAbove r t a)) : R)) (∑ b ∈ t, (↑(#(bipartiteBelow r s b)) : R))

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.Enumerative.DoubleCounting
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
rw rw₁ : Eq.{u_1 + 1} (α := R) (↑(∑ b ∈ t, #(bipartiteBelow r s b)) : R) (↑(∑ x ∈ t, #(bipartiteBelow r s x)) : R)
⊢ Eq.{u_1 + 1} (α := R) (↑(∑ x ∈ s, #(bipartiteAbove r t x)) : R) (↑(∑ x ∈ t, #(bipartiteBelow r s x)) : R)

Tactic:
rw [sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow]

Premises used: Finset.sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow
-- Module: Mathlib.Combinatorics.Enumerative.DoubleCounting
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)
hn : ∀ b ∈ t, n ≤ (↑(#(bipartiteBelow r s b)) : R)
hm : ∀ a ∈ s, (↑(#(bipartiteAbove r t a)) : R) ≤ m
⊢ #t • n ≤ #s • m

Tactic:
card_nsmul_le_card_nsmul (swap r) hn hm

Premises used: Function.swap, Finset.card_nsmul_le_card_nsmul
-- Module: Mathlib.Combinatorics.Enumerative.DoubleCounting
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
rw rw₁ : #s • m = #s • m
⊢ #s • m = ∑ _a ∈ s, m

Tactic:
rw [sum_const]

Premises used: Finset.sum_const
-- Module: Mathlib.Combinatorics.Enumerative.DoubleCounting
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
norm_cast : Eq (α := ℕ) (∑ x ∈ s, #(bipartiteAbove r t x)) (∑ x ∈ t, #(bipartiteBelow r s x))
⊢ Eq.{u_1 + 1} (α := R) (∑ a ∈ s, (↑(#(bipartiteAbove r t a)) : R)) (∑ b ∈ t, (↑(#(bipartiteBelow r s b)) : R))

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.Enumerative.DoubleCounting
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
rw rw₁ : Eq (α := ℕ) (∑ b ∈ t, #(bipartiteBelow r s b)) (∑ x ∈ t, #(bipartiteBelow r s x))
⊢ Eq (α := ℕ) (∑ x ∈ s, #(bipartiteAbove r t x)) (∑ x ∈ t, #(bipartiteBelow r s x))

Tactic:
rw [sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow]

Premises used: Finset.sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow
-- Module: Mathlib.Combinatorics.Enumerative.DoubleCounting
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
norm_cast : Eq (α := ℕ) (∑ x ∈ s, #(bipartiteAbove r t x)) (∑ x ∈ t, #(bipartiteBelow r s x))
⊢ Eq.{u_1 + 1} (α := R) (∑ a ∈ s, (↑(#(bipartiteAbove r t a)) : R)) (∑ b ∈ t, (↑(#(bipartiteBelow r s b)) : R))

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.Enumerative.DoubleCounting
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
rw rw₁ : Eq (α := ℕ) (∑ b ∈ t, #(bipartiteBelow r s b)) (∑ x ∈ t, #(bipartiteBelow r s x))
⊢ Eq (α := ℕ) (∑ x ∈ s, #(bipartiteAbove r t x)) (∑ x ∈ t, #(bipartiteBelow r s x))

Tactic:
rw [sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow]

Premises used: Finset.sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow
-- Module: Mathlib.Combinatorics.Enumerative.DoubleCounting
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
hn : ∀ b ∈ t, n < (↑(#(bipartiteBelow r s b)) : R)
hm : ∀ a ∈ s, (↑(#(bipartiteAbove r t a)) : R) ≤ m
⊢ #t • n < #s • m

Tactic:
card_nsmul_lt_card_nsmul_of_lt_of_le (swap r) ht hn hm

Premises used: Function.swap, Finset.card_nsmul_lt_card_nsmul_of_lt_of_le
-- Module: Mathlib.Combinatorics.Enumerative.DoubleCounting
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
hn : ∀ b ∈ t, n ≤ (↑(#(bipartiteBelow r s b)) : R)
hm : ∀ a ∈ s, (↑(#(bipartiteAbove r t a)) : R) < m
⊢ #t • n < #s • m

Tactic:
card_nsmul_lt_card_nsmul_of_le_of_lt (swap r) hs hn hm

Premises used: Function.swap, Finset.card_nsmul_lt_card_nsmul_of_le_of_lt
-- Module: Mathlib.Combinatorics.Enumerative.DoubleCounting
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
m n : ℕ
inst : (a : α) → (b : β) → Decidable (r a b)
hm : ∀ a ∈ s, m ≤ #(bipartiteAbove r t a)
hn : ∀ b ∈ t, #(bipartiteBelow r s b) ≤ n
⊢ #s * m ≤ #t * n

Tactic:
card_nsmul_le_card_nsmul _ hm hn

Premises used: Finset.card_nsmul_le_card_nsmul
-- Module: Mathlib.Combinatorics.Enumerative.DoubleCounting
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
m n : ℕ
inst : (a : α) → (b : β) → Decidable (r a b)
hn : ∀ b ∈ t, n ≤ #(bipartiteBelow r s b)
hm : ∀ a ∈ s, #(bipartiteAbove r t a) ≤ m
⊢ #t * n ≤ #s * m

Tactic:
card_nsmul_le_card_nsmul' _ hn hm

Premises used: Finset.card_nsmul_le_card_nsmul'
-- Module: Mathlib.Combinatorics.Enumerative.DoubleCounting
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
m n : ℕ
inst : (a : α) → (b : β) → Decidable (r a b)
hm : ∀ a ∈ s, #(bipartiteAbove r t a) = m
hn : ∀ b ∈ t, #(bipartiteBelow r s b) = n
⊢ #s * m = #t * n

Tactic:
(card_mul_le_card_mul _ (fun a ha ↦ (hm a ha).ge) fun b hb ↦ (hn b hb).le).antisymm <|
    card_mul_le_card_mul' _ (fun a ha ↦ (hn a ha).ge) fun b hb ↦ (hm b hb).le

Premises used: Eq.ge, LE.le.antisymm, Eq.le, Finset.card_mul_le_card_mul, Finset.card_mul_le_card_mul'
-- Module: Mathlib.Combinatorics.Enumerative.DoubleCounting
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 * 1
⊢ #s ≤ #t

Tactic:
rw [← mul_one #s, ← mul_one #t]

Premises used: Finset.card, mul_one
-- Module: Mathlib.Combinatorics.Enumerative.DoubleCounting
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
rw : Set.Nonempty.{u_3} (α := β) {b : β | b ∈ t ∧ r a b}
⊢ (bipartiteAbove r t a).Nonempty

Tactic:
rw [← coe_nonempty, coe_bipartiteAbove]

Premises used: Finset.coe_nonempty, Finset.coe_bipartiteAbove
-- Module: Mathlib.Combinatorics.Enumerative.DoubleCounting
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
⊢ Set.Nonempty.{u_3} (α := β) {b : β | b ∈ t ∧ r a b}

Tactic:
hs _ h

Premises used: Set.Mem, setOf, Set.Nonempty
-- Module: Mathlib.Combinatorics.Enumerative.DoubleCounting
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
⊢ Set.Nonempty.{u_3} (α := β) {b : β | b ∈ t ∧ r a b}

Tactic:
exact hs _ h
-- Module: Mathlib.Combinatorics.Enumerative.DoubleCounting
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
simp_rw : ∀ (a : α), a ∈ s ∧ r a b → ∀ (b_1 : α), b_1 ∈ s ∧ r b_1 b → a = b_1
⊢ ∀ a ∈ bipartiteBelow r s b, ∀ b_1 ∈ bipartiteBelow r s b, a = b_1

Tactic:
simp_rw [mem_bipartiteBelow]

Premises used: Finset.mem_bipartiteBelow
-- Module: Mathlib.Combinatorics.Enumerative.DoubleCounting
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 : α), a ∈ s ∧ r a b → ∀ (b_1 : α), b_1 ∈ s ∧ r b_1 b → a = b_1

Tactic:
ht _ h

Premises used: Set.Mem, setOf, Set.Subsingleton
-- Module: Mathlib.Combinatorics.Enumerative.DoubleCounting
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 : α), a ∈ s ∧ r a b → ∀ (b_1 : α), b_1 ∈ s ∧ r b_1 b → a = b_1

Tactic:
exact ht _ h
-- Module: Mathlib.Combinatorics.Enumerative.DoubleCounting
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 * 1 ≤ #t * 1

Tactic:
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))

Premises used: Iff.mpr, Finset.card_le_one, Finset.card_mul_le_card_mul, Finset.card_pos
-- Module: Mathlib.Combinatorics.Enumerative.DoubleCounting
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
rw₁ rw₂ rw₃ : #s * 1 ≤ #t * 1
⊢ #s ≤ #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))

Premises used: Finset.card, mul_one
-- Module: Mathlib.Combinatorics.Enumerative.DoubleCounting
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
ht : ∀ b ∈ t, ∃ a ∈ s, r a b
hs : ∀ a ∈ s, Set.Subsingleton.{u_3} (α := β) {b : β | b ∈ t ∧ r a b}
⊢ #t ≤ #s

Tactic:
card_le_card_of_forall_subsingleton (swap r) ht hs

Premises used: Function.swap, Finset.card_le_card_of_forall_subsingleton
-- Module: Mathlib.Combinatorics.Enumerative.DoubleCounting
Goal:
α : Type u_2
β : Type u_3
inst : Fintype α
inst_1 : Fintype β
r : α → β → Prop
h₁ : LeftTotal r
h₂ : LeftUnique r
⊢ ∀ (a : α), Membership.mem (γ := Finset α) univ a → ∃ (b : β), Membership.mem (γ := Finset β) univ b ∧ r a b

Tactic:
simpa using h₁
-- Module: Mathlib.Combinatorics.Enumerative.DoubleCounting
Goal:
α : Type u_2
β : Type u_3
inst : Fintype α
inst_1 : Fintype β
r : α → β → Prop
h₁ : RightTotal r
h₂ : RightUnique r
⊢ ∀ (b : β), Membership.mem (γ := Finset β) univ b → ∃ (a : α), Membership.mem (γ := Finset α) univ a ∧ r a b

Tactic:
simpa using h₁
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
s : DyckStep
U : DyckStep.U = DyckStep.U ∨ DyckStep.U = DyckStep.D
D : DyckStep.D = DyckStep.U ∨ DyckStep.D = DyckStep.D
⊢ s = DyckStep.U ∨ s = DyckStep.D

Tactic:
cases s
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
U U₁ : ¬DyckStep.U = DyckStep.U → DyckStep.U = D
⊢ DyckStep.U = DyckStep.U ∨ DyckStep.U = D

Tactic:
tauto
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
D D₁ D₂ D₃ D₄ : ¬DyckStep.D = U → DyckStep.D = DyckStep.D
⊢ DyckStep.D = U ∨ DyckStep.D = DyckStep.D

Tactic:
tauto
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
⊢ count U ((↑p : List DyckStep) ++ (↑q : List DyckStep)) = count D ((↑p : List DyckStep) ++ (↑q : List DyckStep))

Tactic:
simp only [count_append, p.count_U_eq_count_D, q.count_U_eq_count_D]

Premises used: DyckWord.count_U_eq_count_D, List.count_append
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
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))
⊢ ∀ (i : ℕ),
    count D (take i ((↑p : List DyckStep) ++ (↑q : List DyckStep))) ≤
      count U (take i ((↑p : List DyckStep) ++ (↑q : List DyckStep)))

Tactic:
simp only [take_append, count_append]

Premises used: List.take_append, List.count_append
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
⊢ ∀ (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:
fun _ ↦ add_le_add (p.count_D_le_count_U _) (q.count_D_le_count_U _)

Premises used: add_le_add, DyckWord.count_D_le_count_U, HSub.hSub, DyckWord.toList, List.length
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
⊢ ∀ (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:
exact fun _ ↦ add_le_add (p.count_D_le_count_U _) (q.count_D_le_count_U _)

Premises used: add_le_add, DyckWord.count_D_le_count_U
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
⊢ count U [] = count D []

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
⊢ ∀ (i : ℕ), count D (take i []) ≤ count U (take i [])

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q r : DyckWord
toList : (↑(p + q + r) : List DyckStep) = (↑(p + (q + r)) : List DyckStep)
⊢ p + q + r = p + (q + r)

Tactic:
ext1
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q r : DyckWord
⊢ (↑(p + q + r) : List DyckStep) = (↑(p + (q + r)) : List DyckStep)

Tactic:
apply append_assoc

Premises used: List.append_assoc
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
toList : (↑(0 + p) : List DyckStep) = (↑p : List DyckStep)
⊢ 0 + p = p

Tactic:
ext1
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
⊢ (↑(0 + p) : List DyckStep) = (↑p : List DyckStep)

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
toList : (↑(p + 0) : List DyckStep) = (↑p : List DyckStep)
⊢ p + 0 = p

Tactic:
ext1
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
⊢ (↑(p + 0) : List DyckStep) = (↑p : List DyckStep)

Tactic:
append_nil _

Premises used: List.append_nil
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
⊢ (↑(p + 0) : List DyckStep) = (↑p : List DyckStep)

Tactic:
exact append_nil _

Premises used: List.append_nil
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q r : DyckWord
h : Eq (α := DyckWord) ((fun (x : DyckWord) ↦ p + x) q) ((fun (x : DyckWord) ↦ p + x) r)
rw :
  ∀ (h : (↑((fun (x : DyckWord) ↦ p + x) q) : List DyckStep) = (↑((fun (x : DyckWord) ↦ p + x) r) : List DyckStep)),
    (↑q : List DyckStep) = (↑r : List DyckStep)
⊢ q = r

Tactic:
rw [DyckWord.ext_iff] at *

Premises used: DyckWord.ext_iff
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q r : DyckWord
h : (↑((fun (x : DyckWord) ↦ p + x) q) : List DyckStep) = (↑((fun (x : DyckWord) ↦ p + x) r) : List DyckStep)
⊢ (↑q : List DyckStep) = (↑r : List DyckStep)

Tactic:
append_cancel_left h

Premises used: List.append_cancel_left
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q r : DyckWord
h : (↑((fun (x : DyckWord) ↦ p + x) q) : List DyckStep) = (↑((fun (x : DyckWord) ↦ p + x) r) : List DyckStep)
⊢ (↑q : List DyckStep) = (↑r : List DyckStep)

Tactic:
exact append_cancel_left h

Premises used: List.append_cancel_left
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q r : DyckWord
h : Eq (α := DyckWord) ((fun (x : DyckWord) ↦ x + p) q) ((fun (x : DyckWord) ↦ x + p) r)
rw :
  ∀ (h : (↑((fun (x : DyckWord) ↦ x + p) q) : List DyckStep) = (↑((fun (x : DyckWord) ↦ x + p) r) : List DyckStep)),
    (↑q : List DyckStep) = (↑r : List DyckStep)
⊢ q = r

Tactic:
rw [DyckWord.ext_iff] at *

Premises used: DyckWord.ext_iff
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q r : DyckWord
h : (↑((fun (x : DyckWord) ↦ x + p) q) : List DyckStep) = (↑((fun (x : DyckWord) ↦ x + p) r) : List DyckStep)
⊢ (↑q : List DyckStep) = (↑r : List DyckStep)

Tactic:
append_cancel_right h

Premises used: List.append_cancel_right
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q r : DyckWord
h : (↑((fun (x : DyckWord) ↦ x + p) q) : List DyckStep) = (↑((fun (x : DyckWord) ↦ x + p) r) : List DyckStep)
⊢ (↑q : List DyckStep) = (↑r : List DyckStep)

Tactic:
exact append_cancel_right h

Premises used: List.append_cancel_right
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
rw : (↑p : List DyckStep) = [] ↔ (↑p : List DyckStep) = (↑0 : List DyckStep)
⊢ (↑p : List DyckStep) = [] ↔ p = 0

Tactic:
rw [DyckWord.ext_iff]

Premises used: DyckWord.ext_iff
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
⊢ (↑p : List DyckStep) = [] ↔ (↑p : List DyckStep) = (↑0 : List DyckStep)

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
⊢ (↑p : List DyckStep) ≠ [] ↔ p ≠ 0

Tactic:
toList_eq_nil.ne

Premises used: DyckWord.toList_eq_nil, Iff.ne
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p_1 q : DyckWord
p : AddUnits DyckWord
obtain :
  ∀ (a b : DyckWord) (h : a + b = 0) (neg_val : b + a = 0),
    { val := a, neg := b, val_neg := h, neg_val := neg_val : AddUnits DyckWord } = default
⊢ p = default

Tactic:
obtain ⟨a, b, h, -⟩ := p
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q a b : DyckWord
h : a + b = 0
neg_val : b + a = 0
⊢ (↑a : List DyckStep) = []

Tactic:
obtain ⟨ha, hb⟩ := append_eq_nil_iff.mp (toList_eq_nil.mpr h)

Premises used: Iff.mpr, DyckWord.toList_eq_nil, List.append_eq_nil_iff, Iff.mp
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q a b : DyckWord
h : a + b = 0
neg_val : b + a = 0
ha : (↑a : List DyckStep) = []
⊢ (↑b : List DyckStep) = []

Tactic:
obtain ⟨ha, hb⟩ := append_eq_nil_iff.mp (toList_eq_nil.mpr h)

Premises used: Iff.mpr, DyckWord.toList_eq_nil, List.append_eq_nil_iff, Iff.mp