awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
N : Type u_5
inst : CommMonoid N
inst_1 : Preorder N
f : ι → N
s : Finset ι
inst_2 : MulLeftMono N
hf : ∀ i ∈ s, 1 ≤ f i
a : ι
h : a ∈ s
⊢ f a ≤ ∏ x ∈ s, f x

Tactic:
calc
    f a = ∏ i ∈ {a}, f i := (prod_singleton _ _).symm
    _ ≤ ∏ i ∈ s, f i :=
      prod_le_prod_of_subset_of_one_le' (singleton_subset_iff.2 h) fun i hi _ ↦ hf i hi

Premises used: Iff.mpr, Trans.trans, Finset.prod_singleton, Finset.singleton_subset_iff, Finset.prod_le_prod_of_subset_of_one_le', Eq.symm
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
N : Type u_5
inst : CommMonoid N
inst_1 : Preorder N
f : ι → N
s : Finset ι
inst_2 : MulLeftMono N
i j : ι
hf : ∀ i ∈ s, 1 ≤ f i
hi : i ∈ s
hj : j ∈ s
hne : i ≠ j
⊢ i ∉ {j}

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
N : Type u_5
inst : CommMonoid N
inst_1 : Preorder N
f : ι → N
s : Finset ι
inst_2 : MulLeftMono N
i j : ι
hf : ∀ i ∈ s, 1 ≤ f i
hi : i ∈ s
hj : j ∈ s
hne : i ≠ j
rw : f i * f j = f i * ∏ x ∈ {j}, f x
rw₁ rw₂ : f i * f j = f i * f j
⊢ f i * f j = ∏ k ∈ cons i {j} ⋯, f k

Tactic:
rw [prod_cons, prod_singleton]

Premises used: Finset.prod_singleton, Finset.prod_cons
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
N : Type u_5
inst : CommMonoid N
inst_1 : Preorder N
f : ι → N
s : Finset ι
inst_2 : MulLeftMono N
i j : ι
hf : ∀ i ∈ s, 1 ≤ f i
hi : i ∈ s
hj : j ∈ s
hne : i ≠ j
⊢ LE.le.{u_5} (α := N) (∏ k ∈ cons i {j} ⋯, f k) (∏ k ∈ s, f k)

Tactic:
prod_le_prod_of_subset_of_one_le' ?_ fun k hk _ ↦ hf k hk

Premises used: Finset.prod_le_prod_of_subset_of_one_le'
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
N : Type u_5
inst : CommMonoid N
inst_1 : Preorder N
f : ι → N
s : Finset ι
inst_2 : MulLeftMono N
i j : ι
hf : ∀ i ∈ s, 1 ≤ f i
hi : i ∈ s
hj : j ∈ s
hne : i ≠ j
refine : cons i {j} ⋯ ⊆ s
⊢ LE.le.{u_5} (α := N) (∏ k ∈ cons i {j} ⋯, f k) (∏ k ∈ s, f k)

Tactic:
refine prod_le_prod_of_subset_of_one_le' ?_ fun k hk _ ↦ hf k hk

Premises used: Finset.prod_le_prod_of_subset_of_one_le'
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
N : Type u_5
inst : CommMonoid N
inst_1 : Preorder N
f : ι → N
s : Finset ι
inst_2 : MulLeftMono N
i j : ι
hf : ∀ i ∈ s, 1 ≤ f i
hi : i ∈ s
hj : j ∈ s
hne : i ≠ j
⊢ cons i {j} ⋯ ⊆ s

Tactic:
simp [cons_subset, *]

Premises used: Finset.cons_subset
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
N : Type u_5
inst : CommMonoid N
inst_1 : Preorder N
inst_2 : MulLeftMono N
s : Finset ι
f : ι → N
n : N
h : ∀ x ∈ s, f x ≤ n
⊢ s.prod f ≤ n ^ #s

Tactic:
(Multiset.prod_le_pow_card (s.val.map f) n ?_).trans ?_

Premises used: Multiset.map, Finset.val, Finset.prod, LE.le.trans, Multiset.prod_le_pow_card
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
N : Type u_5
inst : CommMonoid N
inst_1 : Preorder N
inst_2 : MulLeftMono N
s : Finset ι
f : ι → N
n : N
h : ∀ x ∈ s, f x ≤ n
refine_1 : ∀ x ∈ Multiset.map f s.val, x ≤ n
refine_2 : n ^ (Multiset.map f s.val).card ≤ n ^ #s
⊢ s.prod f ≤ n ^ #s

Tactic:
refine (Multiset.prod_le_pow_card (s.val.map f) n ?_).trans ?_

Premises used: Multiset.map, Finset.val, LE.le.trans, Multiset.prod_le_pow_card
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
N : Type u_5
inst : CommMonoid N
inst_1 : Preorder N
inst_2 : MulLeftMono N
s : Finset ι
f : ι → N
n : N
h : ∀ x ∈ s, f x ≤ n
⊢ ∀ x ∈ Multiset.map f s.val, x ≤ n

Tactic:
simpa using h
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
N : Type u_5
inst : CommMonoid N
inst_1 : Preorder N
inst_2 : MulLeftMono N
s : Finset ι
f : ι → N
n : N
h : ∀ x ∈ s, f x ≤ n
⊢ n ^ (Multiset.map f s.val).card ≤ n ^ #s

Tactic:
simp
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
N : Type u_5
inst : CommMonoid N
inst_1 : Preorder N
inst_2 : MulLeftMono N
s : Finset ι
f : ι → N
n : N
h : ∀ x ∈ s, n ≤ f x
⊢ n ^ #s ≤ s.prod f

Tactic:
Finset.prod_le_pow_card (N := Nᵒᵈ) _ _ _ h

Premises used: OrderDual, Finset.prod_le_pow_card
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
β : Type u_3
inst : DecidableEq β
s : Finset ι
f : ι → Finset β
n : ℕ
h : ∀ a ∈ s, #(f a) ≤ n
⊢ #(s.biUnion f) ≤ #s * n

Tactic:
card_biUnion_le.trans <| sum_le_card_nsmul _ _ _ h

Premises used: Finset.sum_le_card_nsmul, Finset.card_biUnion_le, LE.le.trans
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
N : Type u_5
inst : CommMonoid N
inst_1 : Preorder N
s : Finset ι
ι' : Type u_9
inst_2 : DecidableEq ι'
inst_3 : MulLeftMono N
t : Finset ι'
g : ι → ι'
f : ι → N
h : ∀ y ∉ t, LE.le.{u_5} (α := N) 1 (∏ x ∈ s with g x = y, f x)
⊢ LE.le.{u_5} (α := N) (∏ y ∈ t, ∏ x ∈ s with g x = y, f x) (∏ x ∈ s, f x)

Tactic:
calc
    (∏ y ∈ t, ∏ x ∈ s with g x = y, f x) ≤
        ∏ y ∈ t ∪ s.image g, ∏ x ∈ s with g x = y, f x :=
      prod_le_prod_of_subset_of_one_le' subset_union_left fun y _ ↦ h y
    _ = ∏ x ∈ s, f x :=
      prod_fiberwise_of_maps_to (fun _ hx ↦ mem_union.2 <| Or.inr <| mem_image_of_mem _ hx) _

Premises used: Iff.mpr, Trans.trans, Finset.prod_fiberwise_of_maps_to, Finset.subset_union_left, Finset.prod_le_prod_of_subset_of_one_le', Finset.mem_union, Finset.mem_image_of_mem, Or.inr
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
N : Type u_5
inst : CommMonoid N
inst_1 : Preorder N
s : Finset ι
ι' : Type u_9
inst_2 : DecidableEq ι'
inst_3 : MulLeftMono N
t : Finset ι'
g : ι → ι'
f : ι → N
h : ∀ y ∉ t, LE.le.{u_5} (α := N) (∏ x ∈ s with g x = y, f x) 1
⊢ LE.le.{u_5} (α := N) (∏ x ∈ s, f x) (∏ y ∈ t, ∏ x ∈ s with g x = y, f x)

Tactic:
prod_fiberwise_le_prod_of_one_le_prod_fiber' (N := Nᵒᵈ) h

Premises used: Finset.prod_fiberwise_le_prod_of_one_le_prod_fiber', OrderDual
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
N : Type u_5
inst : CommMonoid N
inst_1 : Preorder N
s : Finset ι
ι' : Type u_9
inst_2 : DecidableEq ι'
inst_3 : MulLeftMono N
g : ι → ι'
f : ι' → N
hf : ∀ u ∈ image g s, 1 ≤ f u
rw : LE.le.{u_5} (α := N) (∏ u ∈ image g s, f u) (∏ b ∈ image g s, f b ^ #({a ∈ s | g a = b}))
⊢ LE.le.{u_5} (α := N) (∏ u ∈ image g s, f u) (∏ u ∈ s, f (g u))

Tactic:
rw [prod_comp f g]

Premises used: Finset.prod_comp
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
N : Type u_5
inst : CommMonoid N
inst_1 : Preorder N
s : Finset ι
ι' : Type u_9
inst_2 : DecidableEq ι'
inst_3 : MulLeftMono N
g : ι → ι'
f : ι' → N
hf : ∀ u ∈ image g s, 1 ≤ f u
⊢ LE.le.{u_5} (α := N) (∏ u ∈ image g s, f u) (∏ b ∈ image g s, f b ^ #({a ∈ s | g a = b}))

Tactic:
prod_le_prod' fun a hag ↦ ?_

Premises used: Finset.prod_le_prod'
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
N : Type u_5
inst : CommMonoid N
inst_1 : Preorder N
s : Finset ι
ι' : Type u_9
inst_2 : DecidableEq ι'
inst_3 : MulLeftMono N
g : ι → ι'
f : ι' → N
hf : ∀ u ∈ image g s, 1 ≤ f u
refine : ∀ (a : ι') (hag : a ∈ image g s), f a ≤ f a ^ #({a_1 ∈ s | g a_1 = a})
⊢ LE.le.{u_5} (α := N) (∏ u ∈ image g s, f u) (∏ b ∈ image g s, f b ^ #({a ∈ s | g a = b}))

Tactic:
refine prod_le_prod' fun a hag ↦ ?_

Premises used: Finset.prod_le_prod'
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
N : Type u_5
inst : CommMonoid N
inst_1 : Preorder N
s : Finset ι
ι' : Type u_9
inst_2 : DecidableEq ι'
inst_3 : MulLeftMono N
g : ι → ι'
f : ι' → N
hf : ∀ u ∈ image g s, 1 ≤ f u
a : ι'
hag : a ∈ image g s
obtain : ∀ (i : ι) (hi : i ∈ s) (hig : g i = a), f a ≤ f a ^ #({a_1 ∈ s | g a_1 = a})
⊢ f a ≤ f a ^ #({a_1 ∈ s | g a_1 = a})

Tactic:
obtain ⟨i, hi, hig⟩ := Finset.mem_image.mp hag

Premises used: Finset.mem_image, Iff.mp
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
N : Type u_5
inst : CommMonoid N
inst_1 : Preorder N
s : Finset ι
ι' : Type u_9
inst_2 : DecidableEq ι'
inst_3 : MulLeftMono N
g : ι → ι'
f : ι' → N
hf : ∀ u ∈ image g s, 1 ≤ f u
a : ι'
hag : a ∈ image g s
i : ι
hi : i ∈ s
hig : g i = a
apply : #({a_1 ∈ s | g a_1 = a}) ≠ 0
⊢ f a ≤ f a ^ #({a_1 ∈ s | g a_1 = a})

Tactic:
apply le_self_pow (hf a hag)

Premises used: le_self_pow
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
N : Type u_5
inst : CommMonoid N
inst_1 : Preorder N
s : Finset ι
ι' : Type u_9
inst_2 : DecidableEq ι'
inst_3 : MulLeftMono N
g : ι → ι'
f : ι' → N
hf : ∀ u ∈ image g s, 1 ≤ f u
a : ι'
hag : a ∈ image g s
i : ι
hi : i ∈ s
hig : g i = a
rw : {a_1 ∈ s | g a_1 = a}.Nonempty
⊢ #({a_1 ∈ s | g a_1 = a}) ≠ 0

Tactic:
rw [← Nat.pos_iff_ne_zero, card_pos]

Premises used: Nat.pos_iff_ne_zero, Finset.card_pos
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
N : Type u_5
inst : CommMonoid N
inst_1 : Preorder N
s : Finset ι
ι' : Type u_9
inst_2 : DecidableEq ι'
inst_3 : MulLeftMono N
g : ι → ι'
f : ι' → N
hf : ∀ u ∈ image g s, 1 ≤ f u
a : ι'
hag : a ∈ image g s
i : ι
hi : i ∈ s
hig : g i = a
⊢ {a_1 ∈ s | g a_1 = a}.Nonempty

Tactic:
⟨i, mem_filter.mpr ⟨hi, hig⟩⟩

Premises used: Iff.mpr, And.intro, Exists.intro, Finset.Nonempty, Finset.mem_filter
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
N : Type u_5
inst : CommMonoid N
inst_1 : Preorder N
s : Finset ι
ι' : Type u_9
inst_2 : DecidableEq ι'
inst_3 : MulLeftMono N
g : ι → ι'
f : ι' → N
hf : ∀ u ∈ image g s, 1 ≤ f u
a : ι'
hag : a ∈ image g s
i : ι
hi : i ∈ s
hig : g i = a
⊢ {a_1 ∈ s | g a_1 = a}.Nonempty

Tactic:
exact ⟨i, mem_filter.mpr ⟨hi, hig⟩⟩
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : AddCommMonoid β
inst_2 : Preorder β
inst_3 : AddLeftMono β
s : Finset ι
f : ι → α
g : α → β
h_one : g 1 ≤ 0
h_mul : ∀ (a b : α), g (a * b) ≤ g a + g b
⊢ g (∏ x ∈ s, f x) ≤ ∑ x ∈ s, g (f x)

Tactic:
(Multiset.apply_prod_le_sum_map _ _ h_one h_mul).trans_eq ?_

Premises used: LE.le.trans_eq, Multiset.apply_prod_le_sum_map, Finset.prod
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : AddCommMonoid β
inst_2 : Preorder β
inst_3 : AddLeftMono β
s : Finset ι
f : ι → α
g : α → β
h_one : g 1 ≤ 0
h_mul : ∀ (a b : α), g (a * b) ≤ g a + g b
refine : (Multiset.map g (Multiset.map (fun (x : ι) ↦ f x) s.val)).sum = ∑ x ∈ s, g (f x)
⊢ g (∏ x ∈ s, f x) ≤ ∑ x ∈ s, g (f x)

Tactic:
refine (Multiset.apply_prod_le_sum_map _ _ h_one h_mul).trans_eq ?_

Premises used: LE.le.trans_eq, Multiset.apply_prod_le_sum_map
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : AddCommMonoid β
inst_2 : Preorder β
inst_3 : AddLeftMono β
s : Finset ι
f : ι → α
g : α → β
h_one : g 1 ≤ 0
h_mul : ∀ (a b : α), g (a * b) ≤ g a + g b
rw : (Multiset.map (g ∘ fun (x : ι) ↦ f x) s.val).sum = ∑ x ∈ s, g (f x)
rw₁ : Eq.{u_3 + 1} (α := β) (Multiset.sum (Multiset.map (fun (x : ι) ↦ g (f x)) s.val)) (∑ x ∈ s, g (f x))
rw₂ rw₃ : Eq.{u_3 + 1} (α := β) (∑ a ∈ s, g (f a)) (∑ x ∈ s, g (f x))
⊢ (Multiset.map g (Multiset.map (fun (x : ι) ↦ f x) s.val)).sum = ∑ x ∈ s, g (f x)

Tactic:
rw [Multiset.map_map, Function.comp_def, Finset.sum_map_val]

Premises used: Function.comp_def, Multiset.map_map, Finset.sum_map_val
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : AddCommMonoid β
inst_2 : Preorder β
inst_3 : AddLeftMono β
s : Finset ι
f : ι → α
g : α → β
h_one : 0 ≤ g 1
h_mul : ∀ (a b : α), g a + g b ≤ g (a * b)
⊢ ∑ x ∈ s, g (f x) ≤ g (∏ x ∈ s, f x)

Tactic:
s.apply_prod_le_sum_apply (β := βᵒᵈ) g h_one h_mul

Premises used: Finset.apply_prod_le_sum_apply, OrderDual
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
f g : ι → M
s : Finset ι
⊢ max (s.prod f) (s.prod g) ≤ ∏ i ∈ s, max (f i) (g i)

Tactic:
Multiset.max_prod_le

Premises used: Finset.prod, Multiset.max_prod_le
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
f g : ι → M
s : Finset ι
⊢ ∏ i ∈ s, min (f i) (g i) ≤ min (s.prod f) (s.prod g)

Tactic:
Multiset.prod_min_le

Premises used: Finset.prod, Multiset.prod_min_le
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
G : Type u_9
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
f : ι → G
s : Finset ι
⊢ LE.le.{u_9} (α := G) |∑ i ∈ s, f i| (∑ i ∈ s, |f i|)

Tactic:
le_sum_of_subadditive _ abs_zero.le abs_add_le s f

Premises used: Finset.le_sum_of_subadditive
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
G : Type u_9
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : AddLeftMono G
f : ι → G
s : Finset ι
hf : ∀ i ∈ s, 0 ≤ f i
rw rw₁ : Eq.{u_9 + 1} (α := G) (∑ i ∈ s, f i) (∑ i ∈ s, f i)
⊢ Eq.{u_9 + 1} (α := G) |∑ i ∈ s, f i| (∑ i ∈ s, f i)

Tactic:
rw [abs_of_nonneg (Finset.sum_nonneg hf)]

Premises used: Finset.sum_nonneg, abs_of_nonneg
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
G : Type u_9
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : AddLeftMono G
f : ι → G
s : Finset ι
hf : ∀ (i : ι), 0 ≤ f i
rw rw₁ : Eq.{u_9 + 1} (α := G) (∑ i ∈ s, f i) (∑ i ∈ s, f i)
⊢ Eq.{u_9 + 1} (α := G) |∑ i ∈ s, f i| (∑ i ∈ s, f i)

Tactic:
rw [abs_of_nonneg (Finset.sum_nonneg' hf)]

Premises used: Finset.sum_nonneg', abs_of_nonneg
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
inst_1 : LE α
inst_2 : MulLeftMono α
s : Finset ι
f : ι → α
empty :
  MulLECancellable.{u_2} (α := α) (∏ i ∈ ∅, f i) ↔
    ∀ ⦃i : ι⦄, Membership.mem (γ := Finset ι) ∅ i → MulLECancellable (f i)
cons :
  ∀ (a : ι) (s : Finset ι) (h : a ∉ s),
    (MulLECancellable.{u_2} (α := α) (∏ i ∈ s, f i) ↔ ∀ ⦃i : ι⦄, i ∈ s → MulLECancellable (f i)) →
      (MulLECancellable.{u_2} (α := α) (∏ i ∈ Finset.cons a s h, f i) ↔
        ∀ ⦃i : ι⦄, i ∈ Finset.cons a s h → MulLECancellable (f i))
⊢ MulLECancellable.{u_2} (α := α) (∏ i ∈ s, f i) ↔ ∀ ⦃i : ι⦄, i ∈ s → MulLECancellable (f i)

Tactic:
induction s using Finset.cons_induction
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
inst_1 : LE α
inst_2 : MulLeftMono α
s : Finset ι
f : ι → α
⊢ MulLECancellable.{u_2} (α := α) (∏ i ∈ ∅, f i) ↔
    ∀ ⦃i : ι⦄, Membership.mem (γ := Finset ι) ∅ i → MulLECancellable (f i)

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
inst_1 : LE α
inst_2 : MulLeftMono α
s : Finset ι
f : ι → α
a : ι
s_1 : Finset ι
h : a ∉ s_1
h_1 : MulLECancellable.{u_2} (α := α) (∏ i ∈ s_1, f i) ↔ ∀ ⦃i : ι⦄, i ∈ s_1 → MulLECancellable (f i)
⊢ MulLECancellable.{u_2} (α := α) (∏ i ∈ cons a s_1 h, f i) ↔ ∀ ⦃i : ι⦄, i ∈ cons a s_1 h → MulLECancellable (f i)

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
f : α → β
s : Finset α
t : Finset β
Hf : ∀ a ∈ s, f a ∈ t
n : ℕ
hn : ∀ b ∈ t, #({a ∈ s | f a = b}) ≤ n
⊢ ∑ _b ∈ t, n = n * #t

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
f : α → β
s : Finset α
n : ℕ
hn : ∀ b ∈ image f s, #({a ∈ s | f a = b}) ≤ n
⊢ #s ≤ n * #(image f s)

Tactic:
card_le_mul_card_image_of_maps_to (fun _ ↦ mem_image_of_mem _) n hn

Premises used: Finset.card_le_mul_card_image_of_maps_to, Finset.mem_image_of_mem
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
f : α → β
s : Finset α
t : Finset β
Hf : ∀ a ∈ s, f a ∈ t
n : ℕ
hn : ∀ b ∈ t, n ≤ #({a ∈ s | f a = b})
⊢ n * #t = ∑ _a ∈ t, n

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
f : α → β
s : Finset α
t : Finset β
Hf : ∀ a ∈ s, f a ∈ t
n : ℕ
hn : ∀ b ∈ t, n ≤ #({a ∈ s | f a = b})
rw rw₁ : #s = #s
⊢ ∑ b ∈ t, #({a ∈ s | f a = b}) = #s

Tactic:
rw [← card_eq_sum_card_fiberwise Hf]

Premises used: Finset.card_eq_sum_card_fiberwise
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
f : α → β
s : Finset α
n : ℕ
hn : ∀ b ∈ image f s, n ≤ #({a ∈ s | f a = b})
⊢ n * #(image f s) ≤ #s

Tactic:
mul_card_image_le_card_of_maps_to (fun _ ↦ mem_image_of_mem _) n hn

Premises used: Finset.mul_card_image_le_card_of_maps_to, Finset.mem_image_of_mem
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
inst : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ a ∈ s, #({b ∈ B | a ∈ b}) ≤ n
⊢ ∑ t ∈ B, #(s ∩ t) ≤ #s * n

Tactic:
le_trans ?_ (s.sum_le_card_nsmul _ _ h)

Premises used: Finset.sum_le_card_nsmul, le_trans
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
inst : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ a ∈ s, #({b ∈ B | a ∈ b}) ≤ n
refine : LE.le (α := ℕ) (∑ t ∈ B, #(s ∩ t)) (∑ x ∈ s, #({b ∈ B | x ∈ b}))
⊢ ∑ t ∈ B, #(s ∩ t) ≤ #s * n

Tactic:
refine le_trans ?_ (s.sum_le_card_nsmul _ _ h)

Premises used: Finset.sum_le_card_nsmul, le_trans
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
inst : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ a ∈ s, #({b ∈ B | a ∈ b}) ≤ n
simp_rw : LE.le (α := ℕ) (∑ x ∈ B, ∑ a ∈ s, if a ∈ x then 1 else 0) (∑ x ∈ s, ∑ a ∈ B, if x ∈ a then 1 else 0)
⊢ LE.le (α := ℕ) (∑ t ∈ B, #(s ∩ t)) (∑ x ∈ s, #({b ∈ B | x ∈ b}))

Tactic:
simp_rw [← filter_mem_eq_inter, card_eq_sum_ones, sum_filter]

Premises used: Finset.card_eq_sum_ones, Finset.sum_filter, Finset.filter_mem_eq_inter
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
inst : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ a ∈ s, #({b ∈ B | a ∈ b}) ≤ n
⊢ LE.le (α := ℕ) (∑ x ∈ B, ∑ a ∈ s, if a ∈ x then 1 else 0) (∑ x ∈ s, ∑ a ∈ B, if x ∈ a then 1 else 0)

Tactic:
sum_comm.le

Premises used: Eq.le, Finset.sum_comm
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
inst : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ a ∈ s, #({b ∈ B | a ∈ b}) ≤ n
⊢ LE.le (α := ℕ) (∑ x ∈ B, ∑ a ∈ s, if a ∈ x then 1 else 0) (∑ x ∈ s, ∑ a ∈ B, if x ∈ a then 1 else 0)

Tactic:
exact sum_comm.le

Premises used: Eq.le, Finset.sum_comm
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
inst : DecidableEq α
B : Finset (Finset α)
n : ℕ
inst_1 : Fintype α
h : ∀ (a : α), #({b ∈ B | a ∈ b}) ≤ n
⊢ Eq (α := ℕ) (∑ s ∈ B, #s) (∑ s ∈ B, #(univ ∩ s))

Tactic:
simp_rw [univ_inter]

Premises used: Finset.univ_inter
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
inst : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ a ∈ s, n ≤ #({b ∈ B | a ∈ b})
apply : LE.le (α := ℕ) (∑ x ∈ s, #({b ∈ B | x ∈ b})) (∑ t ∈ B, #(s ∩ t))
⊢ #s * n ≤ ∑ t ∈ B, #(s ∩ t)

Tactic:
apply (s.card_nsmul_le_sum _ _ h).trans

Premises used: Finset.card_nsmul_le_sum, LE.le.trans
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
inst : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ a ∈ s, n ≤ #({b ∈ B | a ∈ b})
simp_rw : LE.le (α := ℕ) (∑ x ∈ s, ∑ a ∈ B, if x ∈ a then 1 else 0) (∑ x ∈ B, ∑ a ∈ s, if a ∈ x then 1 else 0)
⊢ LE.le (α := ℕ) (∑ x ∈ s, #({b ∈ B | x ∈ b})) (∑ t ∈ B, #(s ∩ t))

Tactic:
simp_rw [← filter_mem_eq_inter, card_eq_sum_ones, sum_filter]

Premises used: Finset.card_eq_sum_ones, Finset.sum_filter, Finset.filter_mem_eq_inter
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
inst : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ a ∈ s, n ≤ #({b ∈ B | a ∈ b})
⊢ LE.le (α := ℕ) (∑ x ∈ s, ∑ a ∈ B, if x ∈ a then 1 else 0) (∑ x ∈ B, ∑ a ∈ s, if a ∈ x then 1 else 0)

Tactic:
sum_comm.le

Premises used: Eq.le, Finset.sum_comm
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
inst : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ a ∈ s, n ≤ #({b ∈ B | a ∈ b})
⊢ LE.le (α := ℕ) (∑ x ∈ s, ∑ a ∈ B, if x ∈ a then 1 else 0) (∑ x ∈ B, ∑ a ∈ s, if a ∈ x then 1 else 0)

Tactic:
exact sum_comm.le

Premises used: Eq.le, Finset.sum_comm
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
inst : DecidableEq α
B : Finset (Finset α)
n : ℕ
inst_1 : Fintype α
h : ∀ (a : α), n ≤ #({b ∈ B | a ∈ b})
⊢ Eq (α := ℕ) (∑ s ∈ B, #(univ ∩ s)) (∑ s ∈ B, #s)

Tactic:
simp_rw [univ_inter]

Premises used: Finset.univ_inter
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
inst : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ a ∈ s, #({b ∈ B | a ∈ b}) = n
⊢ ∑ t ∈ B, #(s ∩ t) = #s * n

Tactic:
(sum_card_inter_le fun a ha ↦ (h a ha).le).antisymm (le_sum_card_inter fun a ha ↦ (h a ha).ge)

Premises used: Eq.ge, Finset.sum_card_inter_le, LE.le.antisymm, Eq.le, Finset.le_sum_card_inter
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
inst : DecidableEq α
B : Finset (Finset α)
n : ℕ
inst_1 : Fintype α
h : ∀ (a : α), #({b ∈ B | a ∈ b}) = n
simp_rw : ∑ s ∈ B, #s = card.{u_2} (α := α) univ * n
simp_rw₁ : Eq (α := ℕ) (∑ s ∈ B, #s) (∑ t ∈ B, #(univ ∩ t))
⊢ ∑ s ∈ B, #s = Fintype.card α * n

Tactic:
simp_rw [Fintype.card, ← sum_card_inter fun a _ ↦ h a, univ_inter]

Premises used: Finset.sum_card_inter, Fintype.card, Finset.univ_inter
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : DecidableEq α
s : Finset ι
f : ι → Finset α
hs : (↑s : Set ι).PairwiseDisjoint f
hf : ∀ i ∈ s, (f i).Nonempty
rw : LE.le (α := ℕ) (∑ x ∈ s, 1) (∑ u ∈ s, #(f u))
⊢ #s ≤ #(s.biUnion f)

Tactic:
rw [card_biUnion hs, card_eq_sum_ones]

Premises used: Finset.card_eq_sum_ones, Finset.card_biUnion
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : DecidableEq α
s : Finset ι
f : ι → Finset α
hs : (↑s : Set ι).PairwiseDisjoint f
hf : ∀ i ∈ s, (f i).Nonempty
⊢ LE.le (α := ℕ) (∑ x ∈ s, 1) (∑ u ∈ s, #(f u))

Tactic:
sum_le_sum fun i hi ↦ (hf i hi).card_pos

Premises used: Finset.Nonempty.card_pos, Finset.sum_le_sum
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : DecidableEq α
s : Finset ι
f : ι → Finset α
hs : (↑s : Set ι).PairwiseDisjoint f
hf : ∀ i ∈ s, (f i).Nonempty
⊢ LE.le (α := ℕ) (∑ x ∈ s, 1) (∑ u ∈ s, #(f u))

Tactic:
exact sum_le_sum fun i hi ↦ (hf i hi).card_pos

Premises used: Finset.sum_le_sum
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : DecidableEq α
s : Finset ι
f : ι → Finset α
hs : (↑s : Set ι).PairwiseDisjoint f
rw : #({a ∈ s | ¬f a = ∅}) + #({i ∈ s | f i = ∅}) ≤ #(s.biUnion f) + #({i ∈ s | f i = ∅})
⊢ #s ≤ #(s.biUnion f) + #({i ∈ s | f i = ∅})

Tactic:
rw [← Finset.card_filter_add_card_filter_not fun i ↦ f i = ∅, add_comm]

Premises used: add_comm, Finset.card_filter_add_card_filter_not, EmptyCollection.emptyCollection, Eq
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : DecidableEq α
s : Finset ι
f : ι → Finset α
hs : (↑s : Set ι).PairwiseDisjoint f
grw : #({i ∈ s | f i ≠ ∅}.biUnion f) + #({i ∈ s | f i = ∅}) ≤ #(s.biUnion f) + #({i ∈ s | f i = ∅})
grw₁ grw₂ : #(s.biUnion f) + #({i ∈ s | f i = ∅}) ≤ #(s.biUnion f) + #({i ∈ s | f i = ∅})
⊢ #({a ∈ s | ¬f a = ∅}) + #({i ∈ s | f i = ∅}) ≤ #(s.biUnion f) + #({i ∈ s | f i = ∅})

Tactic:
grw [card_le_card_biUnion (hs.subset <| filter_subset _ _) fun i hi ↦
    nonempty_of_ne_empty (mem_filter.1 hi).2, filter_subset]

Premises used: Finset.card_le_card_biUnion, Finset.filter_subset, Set.PairwiseDisjoint.subset, And.right, Iff.mp, Finset.mem_filter, Finset.nonempty_of_ne_empty