awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Optimization.ValuedCSP
Goal:
D : Type u_1
C : Type u_3
inst : AddCommMonoid C
inst_1 : PartialOrder C
inst_2 : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
contr :
  HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])
sharp :
  HSMul.hSMul (α := ℕ) (β := C) 2
      (Multiset.sum (Multiset.map (fun (x : Fin (Nat.succ 0).succ → D) ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]]))) <
    HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
impos :
  HSMul.hSMul (α := ℕ) (β := C) 2 (Multiset.sum (Multiset.map (fun (x : (Fin 2 → D) → D) ↦ f ![a, b]) ω)) <
    ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])
rhs_swap : ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b]) = HSMul.hSMul (α := ℕ) 2 (ω.size • f ![a, b])
⊢ Multiset.sum (Multiset.map (fun (x : (Fin 2 → D) → D) ↦ f ![a, b]) ω) = ω.size • f ![a, b]

Tactic:
have distrib : (ω.map (fun _ => f ![a, b])).sum = ω.size • f ![a, b] := by simp
-- Module: Mathlib.Combinatorics.Optimization.ValuedCSP
Goal:
D : Type u_1
C : Type u_3
inst : AddCommMonoid C
inst_1 : PartialOrder C
inst_2 : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
contr :
  HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])
sharp :
  HSMul.hSMul (α := ℕ) (β := C) 2
      (Multiset.sum (Multiset.map (fun (x : Fin (Nat.succ 0).succ → D) ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]]))) <
    HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
impos :
  HSMul.hSMul (α := ℕ) (β := C) 2 (Multiset.sum (Multiset.map (fun (x : (Fin 2 → D) → D) ↦ f ![a, b]) ω)) <
    ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])
rhs_swap : ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b]) = HSMul.hSMul (α := ℕ) 2 (ω.size • f ![a, b])
distrib : Multiset.sum (Multiset.map (fun (x : (Fin 2 → D) → D) ↦ f ![a, b]) ω) = ω.size • f ![a, b]
⊢ HSMul.hSMul (α := ℕ) 2 (ω.size • f ![a, b]) < HSMul.hSMul (α := ℕ) 2 (ω.size • f ![a, b])

Tactic:
rw [rhs_swap, distrib] at impos
-- Module: Mathlib.Combinatorics.Optimization.ValuedCSP
Goal:
D : Type u_1
C : Type u_3
inst : AddCommMonoid C
inst_1 : PartialOrder C
inst_2 : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
contr :
  HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])
sharp :
  HSMul.hSMul (α := ℕ) (β := C) 2
      (Multiset.sum (Multiset.map (fun (x : Fin (Nat.succ 0).succ → D) ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]]))) <
    HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
impos :
  HSMul.hSMul (α := ℕ) (β := C) 2 (Multiset.sum (Multiset.map (fun (x : (Fin 2 → D) → D) ↦ f ![a, b]) ω)) <
    ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])
rhs_swap : ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b]) = HSMul.hSMul (α := ℕ) 2 (ω.size • f ![a, b])
distrib : Multiset.sum (Multiset.map (fun (x : (Fin 2 → D) → D) ↦ f ![a, b]) ω) = ω.size • f ![a, b]
impos₁ : HSMul.hSMul (α := ℕ) 2 (ω.size • f ![a, b]) < HSMul.hSMul (α := ℕ) 2 (ω.size • f ![a, b])
⊢ ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b]) = HSMul.hSMul (α := ℕ) 2 (ω.size • f ![a, b])

Tactic:
rw [rhs_swap, distrib] at impos
-- Module: Mathlib.Combinatorics.Optimization.ValuedCSP
Goal:
D : Type u_1
C : Type u_3
inst : AddCommMonoid C
inst_1 : PartialOrder C
inst_2 : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
contr :
  HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])
sharp :
  HSMul.hSMul (α := ℕ) (β := C) 2
      (Multiset.sum (Multiset.map (fun (x : Fin (Nat.succ 0).succ → D) ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]]))) <
    HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
impos :
  HSMul.hSMul (α := ℕ) (β := C) 2 (Multiset.sum (Multiset.map (fun (x : (Fin 2 → D) → D) ↦ f ![a, b]) ω)) <
    ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])
rhs_swap : ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b]) = HSMul.hSMul (α := ℕ) 2 (ω.size • f ![a, b])
distrib : Multiset.sum (Multiset.map (fun (x : (Fin 2 → D) → D) ↦ f ![a, b]) ω) = ω.size • f ![a, b]
impos₁ : HSMul.hSMul (α := ℕ) 2 (ω.size • f ![a, b]) < HSMul.hSMul (α := ℕ) 2 (ω.size • f ![a, b])
rhs_swap₁ : ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b]) = HSMul.hSMul (α := ℕ) 2 (ω.size • f ![a, b])
⊢ Multiset.sum (Multiset.map (fun (x : (Fin 2 → D) → D) ↦ f ![a, b]) ω) = ω.size • f ![a, b]

Tactic:
rw [rhs_swap, distrib] at impos
-- Module: Mathlib.Combinatorics.Optimization.ValuedCSP
Goal:
D : Type u_1
C : Type u_3
inst : AddCommMonoid C
inst_1 : PartialOrder C
inst_2 : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
contr :
  HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])
sharp :
  HSMul.hSMul (α := ℕ) (β := C) 2
      (Multiset.sum (Multiset.map (fun (x : Fin (Nat.succ 0).succ → D) ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]]))) <
    HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
impos : HSMul.hSMul (α := ℕ) 2 (ω.size • f ![a, b]) < HSMul.hSMul (α := ℕ) 2 (ω.size • f ![a, b])
rhs_swap : ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b]) = HSMul.hSMul (α := ℕ) 2 (ω.size • f ![a, b])
distrib : Multiset.sum (Multiset.map (fun (x : (Fin 2 → D) → D) ↦ f ![a, b]) ω) = ω.size • f ![a, b]
⊢ False

Tactic:
ne_of_lt impos rfl

Premises used: ne_of_lt, rfl
-- Module: Mathlib.Combinatorics.Optimization.ValuedCSP
Goal:
D : Type u_1
C : Type u_3
inst : AddCommMonoid C
inst_1 : PartialOrder C
inst_2 : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
contr :
  HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])
sharp :
  HSMul.hSMul (α := ℕ) (β := C) 2
      (Multiset.sum (Multiset.map (fun (x : Fin (Nat.succ 0).succ → D) ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]]))) <
    HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
impos : HSMul.hSMul (α := ℕ) 2 (ω.size • f ![a, b]) < HSMul.hSMul (α := ℕ) 2 (ω.size • f ![a, b])
rhs_swap : ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b]) = HSMul.hSMul (α := ℕ) 2 (ω.size • f ![a, b])
distrib : Multiset.sum (Multiset.map (fun (x : (Fin 2 → D) → D) ↦ f ![a, b]) ω) = ω.size • f ![a, b]
⊢ False

Tactic:
exact ne_of_lt impos rfl

Premises used: ne_of_lt, rfl
-- Module: Mathlib.Combinatorics.Pigeonhole
Goal:
α : Type u
β : Type v
M : Type w
inst : DecidableEq β
s : Finset α
t : Finset β
f : α → β
w : α → M
b : M
inst_1 : AddCommMonoid M
inst_2 : LinearOrder M
inst_3 : IsOrderedCancelAddMonoid M
hf : ∀ a ∈ s, f a ∈ t
hb : #t • b < ∑ x ∈ s, w x
⊢ LT.lt.{w} (α := M) (∑ i ∈ t, b) (∑ i ∈ t, ∑ x ∈ s with f x = i, w x)

Tactic:
simpa only [sum_fiberwise_of_maps_to hf, sum_const]

Premises used: Finset.sum_fiberwise_of_maps_to, Finset.sum_const
-- Module: Mathlib.Combinatorics.Pigeonhole
Goal:
α : Type u
β : Type v
M : Type w
inst : DecidableEq β
s : Finset α
t : Finset β
f : α → β
w : α → M
b : M
inst_1 : AddCommMonoid M
inst_2 : LinearOrder M
inst_3 : IsOrderedCancelAddMonoid M
hf : ∀ a ∈ s, f a ∈ t
hb : ∑ x ∈ s, w x < #t • b
⊢ ∃ y ∈ t, ∑ x ∈ s with f x = y, w x < b

Tactic:
exists_lt_sum_fiber_of_maps_to_of_nsmul_lt_sum (M := Mᵒᵈ) hf hb

Premises used: Finset.exists_lt_sum_fiber_of_maps_to_of_nsmul_lt_sum, OrderDual
-- Module: Mathlib.Combinatorics.Pigeonhole
Goal:
α : Type u
β : Type v
M : Type w
inst : DecidableEq β
s : Finset α
t : Finset β
f : α → β
w : α → M
b : M
inst_1 : AddCommMonoid M
inst_2 : LinearOrder M
inst_3 : IsOrderedCancelAddMonoid M
ht : ∀ y ∉ t, LE.le.{w} (α := M) (∑ x ∈ s with f x = y, w x) 0
hb : #t • b < ∑ x ∈ s, w x
⊢ LT.lt.{w} (α := M) (∑ _y ∈ t, b) (∑ x ∈ s, w x)

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Pigeonhole
Goal:
α : Type u
β : Type v
M : Type w
inst : DecidableEq β
s : Finset α
t : Finset β
f : α → β
w : α → M
b : M
inst_1 : AddCommMonoid M
inst_2 : LinearOrder M
inst_3 : IsOrderedCancelAddMonoid M
ht : ∀ y ∉ t, LE.le.{w} (α := M) 0 (∑ x ∈ s with f x = y, w x)
hb : ∑ x ∈ s, w x < #t • b
⊢ ∃ y ∈ t, ∑ x ∈ s with f x = y, w x < b

Tactic:
exists_lt_sum_fiber_of_sum_fiber_nonpos_of_nsmul_lt_sum (M := Mᵒᵈ) ht hb

Premises used: Finset.exists_lt_sum_fiber_of_sum_fiber_nonpos_of_nsmul_lt_sum, OrderDual
-- Module: Mathlib.Combinatorics.Pigeonhole
Goal:
α : Type u
β : Type v
M : Type w
inst : DecidableEq β
s : Finset α
t : Finset β
f : α → β
w : α → M
b : M
inst_1 : AddCommMonoid M
inst_2 : LinearOrder M
inst_3 : IsOrderedCancelAddMonoid M
hf : ∀ a ∈ s, f a ∈ t
ht : t.Nonempty
hb : #t • b ≤ ∑ x ∈ s, w x
⊢ LE.le.{w} (α := M) (∑ i ∈ t, b) (∑ i ∈ t, ∑ x ∈ s with f x = i, w x)

Tactic:
simpa only [sum_fiberwise_of_maps_to hf, sum_const]

Premises used: Finset.sum_fiberwise_of_maps_to, Finset.sum_const
-- Module: Mathlib.Combinatorics.Pigeonhole
Goal:
α : Type u
β : Type v
M : Type w
inst : DecidableEq β
s : Finset α
t : Finset β
f : α → β
w : α → M
b : M
inst_1 : AddCommMonoid M
inst_2 : LinearOrder M
inst_3 : IsOrderedCancelAddMonoid M
hf : ∀ a ∈ s, f a ∈ t
ht : t.Nonempty
hb : ∑ x ∈ s, w x ≤ #t • b
⊢ ∃ y ∈ t, ∑ x ∈ s with f x = y, w x ≤ b

Tactic:
exists_le_sum_fiber_of_maps_to_of_nsmul_le_sum (M := Mᵒᵈ) hf ht hb

Premises used: OrderDual, Finset.exists_le_sum_fiber_of_maps_to_of_nsmul_le_sum
-- Module: Mathlib.Combinatorics.Pigeonhole
Goal:
α : Type u
β : Type v
M : Type w
inst : DecidableEq β
s : Finset α
t : Finset β
f : α → β
w : α → M
b : M
inst_1 : AddCommMonoid M
inst_2 : LinearOrder M
inst_3 : IsOrderedCancelAddMonoid M
hf : ∀ y ∉ t, LE.le.{w} (α := M) (∑ x ∈ s with f x = y, w x) 0
ht : t.Nonempty
hb : #t • b ≤ ∑ x ∈ s, w x
⊢ LE.le.{w} (α := M) (∑ _y ∈ t, b) (∑ x ∈ s, w x)

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Pigeonhole
Goal:
α : Type u
β : Type v
M : Type w
inst : DecidableEq β
s : Finset α
t : Finset β
f : α → β
w : α → M
b : M
inst_1 : AddCommMonoid M
inst_2 : LinearOrder M
inst_3 : IsOrderedCancelAddMonoid M
hf : ∀ y ∉ t, LE.le.{w} (α := M) 0 (∑ x ∈ s with f x = y, w x)
ht : t.Nonempty
hb : ∑ x ∈ s, w x ≤ #t • b
⊢ ∃ y ∈ t, ∑ x ∈ s with f x = y, w x ≤ b

Tactic:
exists_le_sum_fiber_of_sum_fiber_nonpos_of_nsmul_le_sum (M := Mᵒᵈ) hf ht hb

Premises used: Finset.exists_le_sum_fiber_of_sum_fiber_nonpos_of_nsmul_le_sum, OrderDual
-- Module: Mathlib.Combinatorics.Pigeonhole
Goal:
α : Type u
β : Type v
M : Type w
inst : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : M
inst_1 : CommSemiring M
inst_2 : LinearOrder M
inst_3 : IsStrictOrderedRing M
hf : ∀ a ∈ s, f a ∈ t
ht : #t • b < (↑(#s) : M)
simp_rw : ∀ (ht : #t • b < ∑ x ∈ s, 1), ∃ y ∈ t, b < ∑ x ∈ s with f x = y, 1
⊢ ∃ y ∈ t, b < (↑(#({x ∈ s | f x = y})) : M)

Tactic:
simp_rw [cast_card] at ht ⊢

Premises used: Finset.cast_card
-- Module: Mathlib.Combinatorics.Pigeonhole
Goal:
α : Type u
β : Type v
M : Type w
inst : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : M
inst_1 : CommSemiring M
inst_2 : LinearOrder M
inst_3 : IsStrictOrderedRing M
hf : ∀ a ∈ s, f a ∈ t
ht : #t • b < ∑ x ∈ s, 1
⊢ ∃ y ∈ t, b < ∑ x ∈ s with f x = y, 1

Tactic:
exists_lt_sum_fiber_of_maps_to_of_nsmul_lt_sum hf ht

Premises used: Finset.exists_lt_sum_fiber_of_maps_to_of_nsmul_lt_sum
-- Module: Mathlib.Combinatorics.Pigeonhole
Goal:
α : Type u
β : Type v
M : Type w
inst : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : M
inst_1 : CommSemiring M
inst_2 : LinearOrder M
inst_3 : IsStrictOrderedRing M
hf : ∀ a ∈ s, f a ∈ t
ht : #t • b < ∑ x ∈ s, 1
⊢ ∃ y ∈ t, b < ∑ x ∈ s with f x = y, 1

Tactic:
exact exists_lt_sum_fiber_of_maps_to_of_nsmul_lt_sum hf ht

Premises used: Finset.exists_lt_sum_fiber_of_maps_to_of_nsmul_lt_sum
-- Module: Mathlib.Combinatorics.Pigeonhole
Goal:
α : Type u
β : Type v
inst : DecidableEq β
s : Finset α
t : Finset β
f : α → β
n : ℕ
hf : ∀ a ∈ s, f a ∈ t
hn : #t * n < #s
⊢ ∃ y ∈ t, n < #({x ∈ s | f x = y})

Tactic:
exists_lt_card_fiber_of_nsmul_lt_card_of_maps_to hf hn

Premises used: Finset.exists_lt_card_fiber_of_nsmul_lt_card_of_maps_to
-- Module: Mathlib.Combinatorics.Pigeonhole
Goal:
α : Type u
β : Type v
M : Type w
inst : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : M
inst_1 : CommSemiring M
inst_2 : LinearOrder M
inst_3 : IsStrictOrderedRing M
ht : (↑(#s) : M) < #t • b
simp_rw : ∀ (ht : ∑ x ∈ s, 1 < #t • b), ∃ y ∈ t, ∑ x ∈ s with f x = y, 1 < b
⊢ ∃ y ∈ t, (↑(#({x ∈ s | f x = y})) : M) < b

Tactic:
simp_rw [cast_card] at ht ⊢

Premises used: Finset.cast_card
-- Module: Mathlib.Combinatorics.Pigeonhole
Goal:
α : Type u
β : Type v
M : Type w
inst : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : M
inst_1 : CommSemiring M
inst_2 : LinearOrder M
inst_3 : IsStrictOrderedRing M
ht : ∑ x ∈ s, 1 < #t • b
⊢ ∃ y ∈ t, ∑ x ∈ s with f x = y, 1 < b

Tactic:
exists_sum_fiber_lt_of_sum_fiber_nonneg_of_sum_lt_nsmul
      (fun _ _ => sum_nonneg fun _ _ => zero_le_one) ht

Premises used: Finset.sum_nonneg, zero_le_one, Finset.exists_sum_fiber_lt_of_sum_fiber_nonneg_of_sum_lt_nsmul
-- Module: Mathlib.Combinatorics.Pigeonhole
Goal:
α : Type u
β : Type v
M : Type w
inst : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : M
inst_1 : CommSemiring M
inst_2 : LinearOrder M
inst_3 : IsStrictOrderedRing M
ht : ∑ x ∈ s, 1 < #t • b
⊢ ∃ y ∈ t, ∑ x ∈ s with f x = y, 1 < b

Tactic:
exact
    exists_sum_fiber_lt_of_sum_fiber_nonneg_of_sum_lt_nsmul
      (fun _ _ => sum_nonneg fun _ _ => zero_le_one) ht

Premises used: Finset.sum_nonneg, zero_le_one, Finset.exists_sum_fiber_lt_of_sum_fiber_nonneg_of_sum_lt_nsmul
-- Module: Mathlib.Combinatorics.Pigeonhole
Goal:
α : Type u
β : Type v
inst : DecidableEq β
s : Finset α
t : Finset β
f : α → β
n : ℕ
hn : #s < #t * n
⊢ ∃ y ∈ t, #({x ∈ s | f x = y}) < n

Tactic:
exists_card_fiber_lt_of_card_lt_nsmul hn

Premises used: Finset.exists_card_fiber_lt_of_card_lt_nsmul
-- Module: Mathlib.Combinatorics.Pigeonhole
Goal:
α : Type u
β : Type v
M : Type w
inst : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : M
inst_1 : CommSemiring M
inst_2 : LinearOrder M
inst_3 : IsStrictOrderedRing M
hf : ∀ a ∈ s, f a ∈ t
ht : t.Nonempty
hb : #t • b ≤ (↑(#s) : M)
simp_rw : ∀ (hb : #t • b ≤ ∑ x ∈ s, 1), ∃ y ∈ t, b ≤ ∑ x ∈ s with f x = y, 1
⊢ ∃ y ∈ t, b ≤ (↑(#({x ∈ s | f x = y})) : M)

Tactic:
simp_rw [cast_card] at hb ⊢

Premises used: Finset.cast_card
-- Module: Mathlib.Combinatorics.Pigeonhole
Goal:
α : Type u
β : Type v
M : Type w
inst : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : M
inst_1 : CommSemiring M
inst_2 : LinearOrder M
inst_3 : IsStrictOrderedRing M
hf : ∀ a ∈ s, f a ∈ t
ht : t.Nonempty
hb : #t • b ≤ ∑ x ∈ s, 1
⊢ ∃ y ∈ t, b ≤ ∑ x ∈ s with f x = y, 1

Tactic:
exists_le_sum_fiber_of_maps_to_of_nsmul_le_sum hf ht hb

Premises used: Finset.exists_le_sum_fiber_of_maps_to_of_nsmul_le_sum
-- Module: Mathlib.Combinatorics.Pigeonhole
Goal:
α : Type u
β : Type v
M : Type w
inst : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : M
inst_1 : CommSemiring M
inst_2 : LinearOrder M
inst_3 : IsStrictOrderedRing M
hf : ∀ a ∈ s, f a ∈ t
ht : t.Nonempty
hb : #t • b ≤ ∑ x ∈ s, 1
⊢ ∃ y ∈ t, b ≤ ∑ x ∈ s with f x = y, 1

Tactic:
exact exists_le_sum_fiber_of_maps_to_of_nsmul_le_sum hf ht hb

Premises used: Finset.exists_le_sum_fiber_of_maps_to_of_nsmul_le_sum
-- Module: Mathlib.Combinatorics.Pigeonhole
Goal:
α : Type u
β : Type v
inst : DecidableEq β
s : Finset α
t : Finset β
f : α → β
n : ℕ
hf : ∀ a ∈ s, f a ∈ t
ht : t.Nonempty
hn : #t * n ≤ #s
⊢ ∃ y ∈ t, n ≤ #({x ∈ s | f x = y})

Tactic:
exists_le_card_fiber_of_nsmul_le_card_of_maps_to hf ht hn

Premises used: Finset.exists_le_card_fiber_of_nsmul_le_card_of_maps_to
-- Module: Mathlib.Combinatorics.Pigeonhole
Goal:
α : Type u
β : Type v
M : Type w
inst : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : M
inst_1 : CommSemiring M
inst_2 : LinearOrder M
inst_3 : IsStrictOrderedRing M
ht : t.Nonempty
hb : (↑(#s) : M) ≤ #t • b
simp_rw : ∀ (hb : ∑ x ∈ s, 1 ≤ #t • b), ∃ y ∈ t, ∑ x ∈ s with f x = y, 1 ≤ b
⊢ ∃ y ∈ t, (↑(#({x ∈ s | f x = y})) : M) ≤ b

Tactic:
simp_rw [cast_card] at hb ⊢

Premises used: Finset.cast_card
-- Module: Mathlib.Combinatorics.Pigeonhole
Goal:
α : Type u
β : Type v
M : Type w
inst : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : M
inst_1 : CommSemiring M
inst_2 : LinearOrder M
inst_3 : IsStrictOrderedRing M
ht : t.Nonempty
hb : ∑ x ∈ s, 1 ≤ #t • b
⊢ ∃ y ∈ t, ∑ x ∈ s with f x = y, 1 ≤ b

Tactic:
exists_sum_fiber_le_of_sum_fiber_nonneg_of_sum_le_nsmul
      (fun _ _ => sum_nonneg fun _ _ => zero_le_one) ht hb

Premises used: Finset.exists_sum_fiber_le_of_sum_fiber_nonneg_of_sum_le_nsmul, Finset.sum_nonneg, zero_le_one
-- Module: Mathlib.Combinatorics.Pigeonhole
Goal:
α : Type u
β : Type v
M : Type w
inst : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : M
inst_1 : CommSemiring M
inst_2 : LinearOrder M
inst_3 : IsStrictOrderedRing M
ht : t.Nonempty
hb : ∑ x ∈ s, 1 ≤ #t • b
⊢ ∃ y ∈ t, ∑ x ∈ s with f x = y, 1 ≤ b

Tactic:
refine
    exists_sum_fiber_le_of_sum_fiber_nonneg_of_sum_le_nsmul
      (fun _ _ => sum_nonneg fun _ _ => zero_le_one) ht hb

Premises used: Finset.exists_sum_fiber_le_of_sum_fiber_nonneg_of_sum_le_nsmul, Finset.sum_nonneg, zero_le_one
-- Module: Mathlib.Combinatorics.Pigeonhole
Goal:
α : Type u
β : Type v
inst : DecidableEq β
s : Finset α
t : Finset β
f : α → β
n : ℕ
ht : t.Nonempty
hn : #s ≤ #t * n
⊢ ∃ y ∈ t, #({x ∈ s | f x = y}) ≤ n

Tactic:
exists_card_fiber_le_of_card_le_nsmul ht hn

Premises used: Finset.exists_card_fiber_le_of_card_le_nsmul
-- Module: Mathlib.Combinatorics.Pigeonhole
Goal:
α : Type u
β : Type v
M : Type w
inst : DecidableEq β
inst_1 : Fintype α
inst_2 : Fintype β
f : α → β
w : α → M
b : M
inst_3 : AddCommMonoid M
inst_4 : LinearOrder M
inst_5 : IsOrderedCancelAddMonoid M
hb : card β • b < ∑ x : α, w x
⊢ ∃ (y : β), b < ∑ x : α with f x = y, w x

Tactic:
let ⟨y, _, hy⟩ := exists_lt_sum_fiber_of_maps_to_of_nsmul_lt_sum (fun _ _ => mem_univ _) hb
  ⟨y, hy⟩

Premises used: Finset.mem_univ, Finset.univ, _private.0.Fintype.exists_lt_sum_fiber_of_nsmul_lt_sum.match_1, Exists, Finset.exists_lt_sum_fiber_of_maps_to_of_nsmul_lt_sum, LT.lt, Exists.intro, Finset.filter, Eq, Finset.sum
-- Module: Mathlib.Combinatorics.Pigeonhole
Goal:
α : Type u
β : Type v
M : Type w
inst : DecidableEq β
inst_1 : Fintype α
inst_2 : Fintype β
f : α → β
w : α → M
b : M
inst_3 : AddCommMonoid M
inst_4 : LinearOrder M
inst_5 : IsOrderedCancelAddMonoid M
inst_6 : Nonempty β
hb : card β • b ≤ ∑ x : α, w x
⊢ ∃ (y : β), b ≤ ∑ x : α with f x = y, w x

Tactic:
let ⟨y, _, hy⟩ :=
    exists_le_sum_fiber_of_maps_to_of_nsmul_le_sum (fun _ _ => mem_univ _) univ_nonempty hb
  ⟨y, hy⟩

Premises used: Finset.mem_univ, Finset.univ, Exists, Finset.univ_nonempty, LE.le, Exists.intro, Finset.filter, Finset.exists_le_sum_fiber_of_maps_to_of_nsmul_le_sum, Eq, _private.0.Fintype.exists_le_sum_fiber_of_nsmul_le_sum.match_1, Finset.sum
-- Module: Mathlib.Combinatorics.Pigeonhole
Goal:
α : Type u
β : Type v
M : Type w
inst : DecidableEq β
inst_1 : Fintype α
inst_2 : Fintype β
f : α → β
w : α → M
b : M
inst_3 : AddCommMonoid M
inst_4 : LinearOrder M
inst_5 : IsOrderedCancelAddMonoid M
hb : ∑ x : α, w x < card β • b
⊢ ∃ (y : β), ∑ x : α with f x = y, w x < b

Tactic:
exists_lt_sum_fiber_of_nsmul_lt_sum (M := Mᵒᵈ) _ hb

Premises used: OrderDual, Fintype.exists_lt_sum_fiber_of_nsmul_lt_sum
-- Module: Mathlib.Combinatorics.Pigeonhole
Goal:
α : Type u
β : Type v
M : Type w
inst : DecidableEq β
inst_1 : Fintype α
inst_2 : Fintype β
f : α → β
w : α → M
b : M
inst_3 : AddCommMonoid M
inst_4 : LinearOrder M
inst_5 : IsOrderedCancelAddMonoid M
inst_6 : Nonempty β
hb : ∑ x : α, w x ≤ card β • b
⊢ ∃ (y : β), ∑ x : α with f x = y, w x ≤ b

Tactic:
exists_le_sum_fiber_of_nsmul_le_sum (M := Mᵒᵈ) _ hb

Premises used: OrderDual, Fintype.exists_le_sum_fiber_of_nsmul_le_sum
-- Module: Mathlib.Combinatorics.Pigeonhole
Goal:
α : Type u
β : Type v
M : Type w
inst : DecidableEq β
inst_1 : Fintype α
inst_2 : Fintype β
f : α → β
b : M
inst_3 : CommSemiring M
inst_4 : LinearOrder M
inst_5 : IsStrictOrderedRing M
hb : card β • b < (↑(card α) : M)
⊢ ∃ (y : β), b < (↑(Finset.card.{u} (α := α) {x : α | f x = y}) : M)

Tactic:
let ⟨y, _, h⟩ := exists_lt_card_fiber_of_nsmul_lt_card_of_maps_to (fun _ _ => mem_univ _) hb
  ⟨y, h⟩

Premises used: Finset.mem_univ, Finset.univ, Exists, Nat.cast, _private.0.Fintype.exists_lt_card_fiber_of_nsmul_lt_card.match_1, LT.lt, Finset.exists_lt_card_fiber_of_nsmul_lt_card_of_maps_to, Exists.intro, Finset.card, Finset.filter, Eq
-- Module: Mathlib.Combinatorics.Pigeonhole
Goal:
α : Type u
β : Type v
inst : DecidableEq β
inst_1 : Fintype α
inst_2 : Fintype β
f : α → β
n : ℕ
hn : card β * n < card α
⊢ ∃ (y : β), n < Finset.card.{u} (α := α) {x : α | f x = y}

Tactic:
exists_lt_card_fiber_of_nsmul_lt_card _ hn

Premises used: Fintype.exists_lt_card_fiber_of_nsmul_lt_card
-- Module: Mathlib.Combinatorics.Pigeonhole
Goal:
α : Type u
β : Type v
M : Type w
inst : DecidableEq β
inst_1 : Fintype α
inst_2 : Fintype β
f : α → β
b : M
inst_3 : CommSemiring M
inst_4 : LinearOrder M
inst_5 : IsStrictOrderedRing M
hb : (↑(card α) : M) < card β • b
⊢ ∃ (y : β), (↑(Finset.card.{u} (α := α) {x : α | f x = y}) : M) < b

Tactic:
let ⟨y, _, h⟩ := Finset.exists_card_fiber_lt_of_card_lt_nsmul (f := f) hb
  ⟨y, h⟩

Premises used: Finset.exists_card_fiber_lt_of_card_lt_nsmul, Finset.univ, _private.0.Fintype.exists_card_fiber_lt_of_card_lt_nsmul.match_1, Exists, Nat.cast, LT.lt, Exists.intro, Finset.card, Finset.filter, Eq
-- Module: Mathlib.Combinatorics.Pigeonhole
Goal:
α : Type u
β : Type v
inst : DecidableEq β
inst_1 : Fintype α
inst_2 : Fintype β
f : α → β
n : ℕ
hn : card α < card β * n
⊢ ∃ (y : β), Finset.card.{u} (α := α) {x : α | f x = y} < n

Tactic:
exists_card_fiber_lt_of_card_lt_nsmul _ hn

Premises used: Fintype.exists_card_fiber_lt_of_card_lt_nsmul
-- Module: Mathlib.Combinatorics.Pigeonhole
Goal:
α : Type u
β : Type v
M : Type w
inst : DecidableEq β
inst_1 : Fintype α
inst_2 : Fintype β
f : α → β
b : M
inst_3 : CommSemiring M
inst_4 : LinearOrder M
inst_5 : IsStrictOrderedRing M
inst_6 : Nonempty β
hb : card β • b ≤ (↑(card α) : M)
⊢ ∃ (y : β), b ≤ (↑(Finset.card.{u} (α := α) {x : α | f x = y}) : M)

Tactic:
let ⟨y, _, h⟩ :=
    exists_le_card_fiber_of_nsmul_le_card_of_maps_to (fun _ _ => mem_univ _) univ_nonempty hb
  ⟨y, h⟩

Premises used: Finset.mem_univ, Finset.univ, _private.0.Fintype.exists_le_card_fiber_of_nsmul_le_card.match_1, Exists, Finset.univ_nonempty, LE.le, Nat.cast, Finset.exists_le_card_fiber_of_nsmul_le_card_of_maps_to, Exists.intro, Finset.card, Finset.filter, Eq
-- Module: Mathlib.Combinatorics.Pigeonhole
Goal:
α : Type u
β : Type v
inst : DecidableEq β
inst_1 : Fintype α
inst_2 : Fintype β
f : α → β
n : ℕ
inst_3 : Nonempty β
hn : card β * n ≤ card α
⊢ ∃ (y : β), n ≤ Finset.card.{u} (α := α) {x : α | f x = y}

Tactic:
exists_le_card_fiber_of_nsmul_le_card _ hn

Premises used: Fintype.exists_le_card_fiber_of_nsmul_le_card
-- Module: Mathlib.Combinatorics.Pigeonhole
Goal:
α : Type u
β : Type v
M : Type w
inst : DecidableEq β
inst_1 : Fintype α
inst_2 : Fintype β
f : α → β
b : M
inst_3 : CommSemiring M
inst_4 : LinearOrder M
inst_5 : IsStrictOrderedRing M
inst_6 : Nonempty β
hb : (↑(card α) : M) ≤ card β • b
⊢ ∃ (y : β), (↑(Finset.card.{u} (α := α) {x : α | f x = y}) : M) ≤ b

Tactic:
let ⟨y, _, h⟩ := Finset.exists_card_fiber_le_of_card_le_nsmul univ_nonempty hb
  ⟨y, h⟩

Premises used: Finset.univ, Exists, Finset.univ_nonempty, LE.le, Nat.cast, _private.0.Fintype.exists_card_fiber_le_of_card_le_nsmul.match_1, Finset.exists_card_fiber_le_of_card_le_nsmul, Exists.intro, Finset.card, Finset.filter, Eq