awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : Preorder N
inst_3 : IsOrderedMonoid N
f : M → N
p : M → Prop
h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
hp_mul : ∀ (x y : M), p x → p y → p (x * y)
g : ι → M
s : Finset ι
hs_nonempty : s.Nonempty
hs : ∀ i ∈ s, p (g i)
refine_1 : Ne.{u_4 + 1} (α := Multiset M) (Multiset.map (fun (i : ι) ↦ g i) s.val) ∅
⊢ f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)
have refine_2 : ∀ (a : M), Membership.mem (γ := Multiset M) (Multiset.map (fun (i : ι) ↦ g i) s.val) a → p a
Tactic: refine le_trans
    (Multiset.le_prod_nonempty_of_submultiplicative_on_pred f p h_mul hp_mul _ ?_ ?_) ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : Preorder N
inst_3 : IsOrderedMonoid N
f : M → N
p : M → Prop
h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
hp_mul : ∀ (x y : M), p x → p y → p (x * y)
g : ι → M
s : Finset ι
hs_nonempty : s.Nonempty
hs : ∀ i ∈ s, p (g i)
refine_1 : Ne.{u_4 + 1} (α := Multiset M) (Multiset.map (fun (i : ι) ↦ g i) s.val) ∅
refine_2 : ∀ (a : M), Membership.mem (γ := Multiset M) (Multiset.map (fun (i : ι) ↦ g i) s.val) a → p a
⊢ f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)
have refine_3 : (Multiset.map f (Multiset.map (fun (i : ι) ↦ g i) s.val)).prod ≤ ∏ i ∈ s, f (g i)
Tactic: refine le_trans
    (Multiset.le_prod_nonempty_of_submultiplicative_on_pred f p h_mul hp_mul _ ?_ ?_) ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : Preorder N
inst_3 : IsOrderedMonoid N
f : M → N
p : M → Prop
h_one : f 1 ≤ 1
h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
hp_mul : ∀ (x y : M), p x → p y → p (x * y)
g : ι → M
s : Finset ι
hs : ∀ i ∈ s, p (g i)
⊢ f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)
have inl : ∀ (hs : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → p (g i)), f (∏ i ∈ ∅, g i) ≤ ∏ i ∈ ∅, f (g i)
Tactic: rcases eq_empty_or_nonempty s with (rfl | hs_nonempty)
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : Preorder N
inst_3 : IsOrderedMonoid N
f : M → N
p : M → Prop
h_one : f 1 ≤ 1
h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
hp_mul : ∀ (x y : M), p x → p y → p (x * y)
g : ι → M
s : Finset ι
hs : ∀ i ∈ s, p (g i)
inl : ∀ (hs : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → p (g i)), f (∏ i ∈ ∅, g i) ≤ ∏ i ∈ ∅, f (g i)
⊢ f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)
have inr : ∀ (hs_nonempty : s.Nonempty), f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)
Tactic: rcases eq_empty_or_nonempty s with (rfl | hs_nonempty)
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
Goal:
ι : Type u_1
N : Type u_5
inst : CommMonoid N
inst_1 : Preorder N
f : ι → N
s : Finset ι
inst_2 : MulLeftMono N
h : ∀ i ∈ s, 1 ≤ f i
⊢ LE.le.{u_5} (α := N) 1 (∏ i ∈ s, 1)
have rw : LE.le.{u_5} (α := N) 1 1
Tactic: rw [prod_const_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
Goal:
ι : Type u_1
N : Type u_5
inst : CommMonoid N
inst_1 : Preorder N
f : ι → N
s : Finset ι
inst_2 : MulLeftMono N
h : ∀ i ∈ s, f i ≤ 1
⊢ Eq.{u_5 + 1} (α := N) (∏ i ∈ s, 1) 1
have rw : Eq.{u_5 + 1} (α := N) 1 1
Tactic: rw [prod_const_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
Goal:
ι : Type u_1
N : Type u_5
inst : CommMonoid N
inst_1 : Preorder N
f : ι → N
s t : Finset ι
inst_2 : MulLeftMono N
h : s ⊆ t
hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i
⊢ Eq.{u_5 + 1} (α := N) (∏ i ∈ t \ s ∪ s, f i) (∏ i ∈ t, f i)
have rw : Eq.{u_5 + 1} (α := N) (∏ i ∈ t, f i) (∏ i ∈ t, f i)
Tactic: rw [sdiff_union_of_subset h]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
Goal:
ι : Type u_1
N : Type u_5
inst : CommMonoid N
inst_1 : Preorder N
f : ι → N
s t : Finset ι
inst_2 : MulLeftMono N
h : s ⊆ t
hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i
⊢ LE.le.{u_5} (α := N) (∏ i ∈ s, f i) (∏ i ∈ t, f i)
have i : Eq.{u_5 + 1} (α := N) (∏ i ∈ t \ s ∪ s, f i) (∏ i ∈ t, f i)
Tactic: calc
      ∏ i ∈ s, f i ≤ (∏ i ∈ t \ s, f i) * ∏ i ∈ s, f i :=
        le_mul_of_one_le_left' <| one_le_prod' <| by simpa only [mem_sdiff, and_imp]
      _ = ∏ i ∈ t \ s ∪ s, f i := (prod_union sdiff_disjoint).symm
      _ = ∏ i ∈ t, f i := by rw [sdiff_union_of_subset h]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
Goal:
ι : Type u_1
N : Type u_5
inst : CommMonoid N
inst_1 : Preorder N
f : ι → N
s t : Finset ι
inst_2 : MulLeftMono N
h : s ⊆ t
hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i
⊢ LE.le.{u_5} (α := N) (∏ i ∈ s, f i) (∏ i ∈ t, f i)
have classical : Eq.{u_5 + 1} (α := N) (∏ i ∈ t \ s ∪ s, f i) (∏ i ∈ t, f i)
Tactic: classical calc
      ∏ i ∈ s, f i ≤ (∏ i ∈ t \ s, f i) * ∏ i ∈ s, f i :=
        le_mul_of_one_le_left' <| one_le_prod' <| by simpa only [mem_sdiff, and_imp]
      _ = ∏ i ∈ t \ s ∪ s, f i := (prod_union sdiff_disjoint).symm
      _ = ∏ i ∈ t, f i := by rw [sdiff_union_of_subset h]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
Goal:
ι : Type u_1
N : Type u_5
inst : CommMonoid N
inst_1 : PartialOrder N
f : ι → N
s : Finset ι
inst_2 : MulLeftMono N
⊢ (∀ i ∈ s, 1 ≤ f i) → (Eq.{u_5 + 1} (α := N) (∏ i ∈ s, f i) 1 ↔ ∀ i ∈ s, f i = 1)
have refine : ∀ (a : ι) (s : Finset ι),
  a ∉ s →
    ((∀ i ∈ s, 1 ≤ f i) → (Eq.{u_5 + 1} (α := N) (∏ i ∈ s, f i) 1 ↔ ∀ i ∈ s, f i = 1)) →
      (∀ i ∈ insert a s, 1 ≤ f i) → (Eq.{u_5 + 1} (α := N) (∏ i ∈ insert a s, f i) 1 ↔ ∀ i ∈ insert a s, f i = 1)
Tactic: refine Finset.induction_on s
      (fun _ ↦ ⟨fun _ _ h ↦ False.elim (Finset.notMem_empty _ h), fun _ ↦ rfl⟩) ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (hypothesis)
Goal:
ι : Type u_1
N : Type u_5
inst : CommMonoid N
inst_1 : PartialOrder N
f : ι → N
s_1 : Finset ι
inst_2 : MulLeftMono N
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, 1 ≤ f i) → (Eq.{u_5 + 1} (α := N) (∏ i ∈ s, f i) 1 ↔ ∀ i ∈ s, f i = 1)
H : ∀ i ∈ insert a s, 1 ≤ f i
⊢ Eq.{u_5 + 1} (α := N) (∏ i ∈ insert a s, f i) 1 ↔ ∀ i ∈ insert a s, f i = 1
have this : ∀ i ∈ s, 1 ≤ f i
Tactic: have : ∀ i ∈ s, 1 ≤ f i := fun _ ↦ H _ ∘ mem_insert_of_mem
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
Goal:
ι : Type u_1
N : Type u_5
inst : CommMonoid N
inst_1 : PartialOrder N
f : ι → N
s_1 : Finset ι
inst_2 : MulLeftMono N
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, 1 ≤ f i) → (Eq.{u_5 + 1} (α := N) (∏ i ∈ s, f i) 1 ↔ ∀ i ∈ s, f i = 1)
H : ∀ i ∈ insert a s, 1 ≤ f i
this : ∀ i ∈ s, 1 ≤ f i
⊢ Eq.{u_5 + 1} (α := N) (∏ i ∈ insert a s, f i) 1 ↔ ∀ i ∈ insert a s, f i = 1
have rw : f a * ∏ x ∈ s, f x = 1 ↔ ∀ i ∈ insert a s, f i = 1
Tactic: rw [prod_insert ha, mul_eq_one_iff_of_one_le (H _ <| mem_insert_self _ _) (one_le_prod' this),
      forall_mem_insert, ih this]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
Goal:
ι : Type u_1
N : Type u_5
inst : CommMonoid N
inst_1 : PartialOrder N
f : ι → N
s_1 : Finset ι
inst_2 : MulLeftMono N
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, 1 ≤ f i) → (Eq.{u_5 + 1} (α := N) (∏ i ∈ s, f i) 1 ↔ ∀ i ∈ s, f i = 1)
H : ∀ i ∈ insert a s, 1 ≤ f i
this : ∀ i ∈ s, 1 ≤ f i
rw : f a * ∏ x ∈ s, f x = 1 ↔ ∀ i ∈ insert a s, f i = 1
⊢ Eq.{u_5 + 1} (α := N) (∏ i ∈ insert a s, f i) 1 ↔ ∀ i ∈ insert a s, f i = 1
have rw₁ : f a = 1 ∧ Eq.{u_5 + 1} (α := N) (∏ i ∈ s, f i) 1 ↔ ∀ i ∈ insert a s, f i = 1
Tactic: rw [prod_insert ha, mul_eq_one_iff_of_one_le (H _ <| mem_insert_self _ _) (one_le_prod' this),
      forall_mem_insert, ih this]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
Goal:
ι : Type u_1
N : Type u_5
inst : CommMonoid N
inst_1 : PartialOrder N
f : ι → N
s_1 : Finset ι
inst_2 : MulLeftMono N
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, 1 ≤ f i) → (Eq.{u_5 + 1} (α := N) (∏ i ∈ s, f i) 1 ↔ ∀ i ∈ s, f i = 1)
H : ∀ i ∈ insert a s, 1 ≤ f i
this : ∀ i ∈ s, 1 ≤ f i
rw : f a * ∏ x ∈ s, f x = 1 ↔ ∀ i ∈ insert a s, f i = 1
rw₁ : f a = 1 ∧ Eq.{u_5 + 1} (α := N) (∏ i ∈ s, f i) 1 ↔ ∀ i ∈ insert a s, f i = 1
⊢ Eq.{u_5 + 1} (α := N) (∏ i ∈ insert a s, f i) 1 ↔ ∀ i ∈ insert a s, f i = 1
have rw₂ : f a = 1 ∧ Eq.{u_5 + 1} (α := N) (∏ i ∈ s, f i) 1 ↔ f a = 1 ∧ ∀ x ∈ s, f x = 1
Tactic: rw [prod_insert ha, mul_eq_one_iff_of_one_le (H _ <| mem_insert_self _ _) (one_le_prod' this),
      forall_mem_insert, ih this]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
Goal:
ι : Type u_1
N : Type u_5
inst : CommMonoid N
inst_1 : PartialOrder N
f : ι → N
s_1 : Finset ι
inst_2 : MulLeftMono N
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, 1 ≤ f i) → (Eq.{u_5 + 1} (α := N) (∏ i ∈ s, f i) 1 ↔ ∀ i ∈ s, f i = 1)
H : ∀ i ∈ insert a s, 1 ≤ f i
this : ∀ i ∈ s, 1 ≤ f i
rw : f a * ∏ x ∈ s, f x = 1 ↔ ∀ i ∈ insert a s, f i = 1
rw₁ : f a = 1 ∧ Eq.{u_5 + 1} (α := N) (∏ i ∈ s, f i) 1 ↔ ∀ i ∈ insert a s, f i = 1
rw₂ : f a = 1 ∧ Eq.{u_5 + 1} (α := N) (∏ i ∈ s, f i) 1 ↔ f a = 1 ∧ ∀ x ∈ s, f x = 1
⊢ Eq.{u_5 + 1} (α := N) (∏ i ∈ insert a s, f i) 1 ↔ ∀ i ∈ insert a s, f i = 1
have rw₃ : (f a = 1 ∧ ∀ i ∈ s, f i = 1) ↔ f a = 1 ∧ ∀ x ∈ s, f x = 1
Tactic: rw [prod_insert ha, mul_eq_one_iff_of_one_le (H _ <| mem_insert_self _ _) (one_le_prod' this),
      forall_mem_insert, ih this]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
Goal:
ι : Type u_1
N : Type u_5
inst : CommMonoid N
inst_1 : PartialOrder N
f : ι → N
s : Finset ι
inst_2 : MulLeftMono N
⊢ (∀ i ∈ s, 1 ≤ f i) → (Eq.{u_5 + 1} (α := N) (∏ i ∈ s, f i) 1 ↔ ∀ i ∈ s, f i = 1)
have refine : ∀ (a : ι) (s : Finset ι),
  a ∉ s →
    ((∀ i ∈ s, 1 ≤ f i) → (Eq.{u_5 + 1} (α := N) (∏ i ∈ s, f i) 1 ↔ ∀ i ∈ s, f i = 1)) →
      (∀ i ∈ insert a s, 1 ≤ f i) → (Eq.{u_5 + 1} (α := N) (∏ i ∈ insert a s, f i) 1 ↔ ∀ i ∈ insert a s, f i = 1)
Tactic: classical
    refine Finset.induction_on s
      (fun _ ↦ ⟨fun _ _ h ↦ False.elim (Finset.notMem_empty _ h), fun _ ↦ rfl⟩) ?_
    intro a s ha ih H
    have : ∀ i ∈ s, 1 ≤ f i := fun _ ↦ H _ ∘ mem_insert_of_mem
    rw [prod_insert ha, mul_eq_one_iff_of_one_le (H _ <| mem_insert_self _ _) (one_le_prod' this),
      forall_mem_insert, ih this]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
Goal:
ι : Type u_1
N : Type u_5
inst : CommMonoid N
inst_1 : PartialOrder N
f : ι → N
s : Finset ι
inst_2 : MulLeftMono N
refine refine₁ :
  ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
    (ih : (∀ i ∈ s, 1 ≤ f i) → (Eq.{u_5 + 1} (α := N) (∏ i ∈ s, f i) 1 ↔ ∀ i ∈ s, f i = 1))
    (H : ∀ i ∈ insert a s, 1 ≤ f i), Eq.{u_5 + 1} (α := N) (∏ i ∈ insert a s, f i) 1 ↔ ∀ i ∈ insert a s, f i = 1
⊢ (∀ i ∈ s, 1 ≤ f i) → (Eq.{u_5 + 1} (α := N) (∏ i ∈ s, f i) 1 ↔ ∀ i ∈ s, f i = 1)
have refine₂ : ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
  (ih : (∀ i ∈ s, 1 ≤ f i) → (Eq.{u_5 + 1} (α := N) (∏ i ∈ s, f i) 1 ↔ ∀ i ∈ s, f i = 1))
  (H : ∀ i ∈ insert a s, 1 ≤ f i) (this : ∀ i ∈ s, 1 ≤ f i),
  Eq.{u_5 + 1} (α := N) (∏ i ∈ insert a s, f i) 1 ↔ ∀ i ∈ insert a s, f i = 1
Tactic: classical
    refine Finset.induction_on s
      (fun _ ↦ ⟨fun _ _ h ↦ False.elim (Finset.notMem_empty _ h), fun _ ↦ rfl⟩) ?_
    intro a s ha ih H
    have : ∀ i ∈ s, 1 ≤ f i := fun _ ↦ H _ ∘ mem_insert_of_mem
    rw [prod_insert ha, mul_eq_one_iff_of_one_le (H _ <| mem_insert_self _ _) (one_le_prod' this),
      forall_mem_insert, ih this]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (hypothesis)
Goal:
ι : Type u_1
N : Type u_5
inst : CommMonoid N
inst_1 : PartialOrder N
f : ι → N
s : Finset ι
inst_2 : MulLeftMono N
hf : ∀ x ∈ s, 1 ≤ f x
⊢ LT.lt.{u_5} (α := N) 1 (∏ x ∈ s, f x) ↔ ∃ x ∈ s, 1 < f x
have hsum : LE.le.{u_5} (α := N) 1 (∏ x ∈ s, f x)
Tactic: have hsum : 1 ≤ ∏ x ∈ s, f x := one_le_prod' hf
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
Goal:
ι : Type u_1
N : Type u_5
inst : CommMonoid N
inst_1 : PartialOrder N
f : ι → N
s : Finset ι
inst_2 : MulLeftMono N
hf : ∀ x ∈ s, 1 ≤ f x
hsum : LE.le.{u_5} (α := N) 1 (∏ x ∈ s, f x)
⊢ LT.lt.{u_5} (α := N) 1 (∏ x ∈ s, f x) ↔ ∃ x ∈ s, 1 < f x
have rw : (∃ (x : ι), ¬(x ∈ s → f x = 1)) ↔ ∃ x ∈ s, 1 < f x
Tactic: rw [hsum.lt_iff_ne', Ne, prod_eq_one_iff_of_one_le' hf, not_forall]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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
⊢ f i * f j = ∏ k ∈ cons i {j} ⋯, f k
have rw : f i * f j = f i * ∏ x ∈ {j}, f x
Tactic: rw [prod_cons, prod_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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
⊢ f i * f j = ∏ k ∈ cons i {j} ⋯, f k
have rw₁ : f i * f j = f i * f j
Tactic: rw [prod_cons, prod_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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)
have refine : cons i {j} sorry ⊆ s
Tactic: refine prod_le_prod_of_subset_of_one_le' ?_ fun k hk _ ↦ hf k hk
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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
have refine_1 : ∀ x ∈ Multiset.map f s.val, x ≤ n
Tactic: refine (Multiset.prod_le_pow_card (s.val.map f) n ?_).trans ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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
⊢ s.prod f ≤ n ^ #s
have refine_2 : n ^ (Multiset.map f s.val).card ≤ n ^ #s
Tactic: refine (Multiset.prod_le_pow_card (s.val.map f) n ?_).trans ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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) (∏ u ∈ s, f (g u))
have rw : LE.le.{u_5} (α := N) (∏ u ∈ image g s, f u) (∏ b ∈ image g s, f b ^ #({a ∈ s | g a = b}))
Tactic: rw [prod_comp f g]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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}))
have refine : ∀ (a : ι') (hag : a ∈ image g s), f a ≤ f a ^ #({a_1 ∈ s | g a_1 = a})
Tactic: refine prod_le_prod' fun a hag ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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
⊢ f a ≤ f a ^ #({a_1 ∈ s | g a_1 = a})
have obtain : ∀ (i : ι) (hi : i ∈ s) (hig : g i = a), f a ≤ f a ^ #({a_1 ∈ s | g a_1 = a})
Tactic: obtain ⟨i, hi, hig⟩ := Finset.mem_image.mp hag
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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
⊢ f a ≤ f a ^ #({a_1 ∈ s | g a_1 = a})
have apply : #({a_1 ∈ s | g a_1 = a}) ≠ 0
Tactic: apply le_self_pow (hf a hag)
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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}) ≠ 0
have rw : {a_1 ∈ s | g a_1 = a}.Nonempty
Tactic: rw [← Nat.pos_iff_ne_zero, card_pos]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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)
have refine : (Multiset.map g (Multiset.map (fun (x : ι) ↦ f x) s.val)).sum = ∑ x ∈ s, g (f x)
Tactic: refine (Multiset.apply_prod_le_sum_map _ _ h_one h_mul).trans_eq ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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
⊢ (Multiset.map g (Multiset.map (fun (x : ι) ↦ f x) s.val)).sum = ∑ x ∈ s, g (f x)
have rw : (Multiset.map (g ∘ fun (x : ι) ↦ f x) s.val).sum = ∑ x ∈ s, g (f x)
Tactic: rw [Multiset.map_map, Function.comp_def, Finset.sum_map_val]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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)
⊢ (Multiset.map g (Multiset.map (fun (x : ι) ↦ f x) s.val)).sum = ∑ x ∈ s, g (f x)
have rw₁ : Eq.{u_3 + 1} (α := β) (Multiset.sum (Multiset.map (fun (x : ι) ↦ g (f x)) s.val)) (∑ x ∈ s, g (f x))
Tactic: rw [Multiset.map_map, Function.comp_def, Finset.sum_map_val]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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))
⊢ (Multiset.map g (Multiset.map (fun (x : ι) ↦ f x) s.val)).sum = ∑ x ∈ s, g (f x)
have rw₂ : Eq.{u_3 + 1} (α := β) (∑ a ∈ s, g (f a)) (∑ x ∈ s, g (f x))
Tactic: rw [Multiset.map_map, Function.comp_def, Finset.sum_map_val]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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
⊢ Eq.{u_9 + 1} (α := G) |∑ i ∈ s, f i| (∑ i ∈ s, f i)
have rw : Eq.{u_9 + 1} (α := G) (∑ i ∈ s, f i) (∑ i ∈ s, f i)
Tactic: rw [abs_of_nonneg (Finset.sum_nonneg hf)]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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
⊢ Eq.{u_9 + 1} (α := G) |∑ i ∈ s, f i| (∑ i ∈ s, f i)
have rw : Eq.{u_9 + 1} (α := G) (∑ i ∈ s, f i) (∑ i ∈ s, f i)
Tactic: rw [abs_of_nonneg (Finset.sum_nonneg' hf)]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
inst_1 : LE α
inst_2 : MulLeftMono α
s : Finset ι
f : ι → α
⊢ MulLECancellable.{u_2} (α := α) (∏ i ∈ s, f i) ↔ ∀ ⦃i : ι⦄, i ∈ s → MulLECancellable (f i)
have empty : MulLECancellable.{u_2} (α := α) (∏ i ∈ ∅, f i) ↔ ∀ ⦃i : ι⦄, Membership.mem (γ := Finset ι) ∅ i → MulLECancellable (f i)
Tactic: induction s using Finset.cons_induction
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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)
⊢ MulLECancellable.{u_2} (α := α) (∏ i ∈ s, f i) ↔ ∀ ⦃i : ι⦄, i ∈ s → MulLECancellable (f i)
have cons : ∀ (a : ι) (s : Finset ι) (h : a ∉ s),
  (MulLECancellable.{u_2} (α := α) (∏ i ∈ s, f i) ↔ ∀ ⦃i : ι⦄, i ∈ s → MulLECancellable (f i)) →
    (MulLECancellable.{u_2} (α := α) (∏ i ∈ cons a s h, f i) ↔ ∀ ⦃i : ι⦄, i ∈ cons a s h → MulLECancellable (f i))
Tactic: induction s using Finset.cons_induction
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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})
⊢ ∑ b ∈ t, #({a ∈ s | f a = b}) = #s
have rw : #s = #s
Tactic: rw [← card_eq_sum_card_fiberwise Hf]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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
have refine : LE.le (α := ℕ) (∑ t ∈ B, #(s ∩ t)) (∑ x ∈ s, #({b ∈ B | x ∈ b}))
Tactic: refine le_trans ?_ (s.sum_le_card_nsmul _ _ h)
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
Goal:
α : Type u_2
inst : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ a ∈ s, #({b ∈ B | a ∈ b}) ≤ n
⊢ LE.le (α := ℕ) (∑ t ∈ B, #(s ∩ t)) (∑ x ∈ s, #({b ∈ B | x ∈ b}))
have 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)
Tactic: simp_rw [← filter_mem_eq_inter, card_eq_sum_ones, sum_filter]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
Goal:
α : Type u_2
inst : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ a ∈ s, n ≤ #({b ∈ B | a ∈ b})
⊢ #s * n ≤ ∑ t ∈ B, #(s ∩ t)
have apply : LE.le (α := ℕ) (∑ x ∈ s, #({b ∈ B | x ∈ b})) (∑ t ∈ B, #(s ∩ t))
Tactic: apply (s.card_nsmul_le_sum _ _ h).trans
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
Goal:
α : Type u_2
inst : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ a ∈ s, n ≤ #({b ∈ B | a ∈ b})
⊢ LE.le (α := ℕ) (∑ x ∈ s, #({b ∈ B | x ∈ b})) (∑ t ∈ B, #(s ∩ t))
have 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)
Tactic: simp_rw [← filter_mem_eq_inter, card_eq_sum_ones, sum_filter]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
Goal:
α : Type u_2
inst : DecidableEq α
B : Finset (Finset α)
n : ℕ
inst_1 : Fintype α
h : ∀ (a : α), #({b ∈ B | a ∈ b}) = n
⊢ ∑ s ∈ B, #s = Fintype.card α * n
have simp_rw : ∑ s ∈ B, #s = card.{u_2} (α := α) univ * n
Tactic: simp_rw [Fintype.card, ← sum_card_inter fun a _ ↦ h a, univ_inter]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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
⊢ ∑ s ∈ B, #s = Fintype.card α * n
have simp_rw₁ : Eq (α := ℕ) (∑ s ∈ B, #s) (∑ t ∈ B, #(univ ∩ t))
Tactic: simp_rw [Fintype.card, ← sum_card_inter fun a _ ↦ h a, univ_inter]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : DecidableEq α
s : Finset ι
f : ι → Finset α
hs : (↑s : Set ι).PairwiseDisjoint f
hf : ∀ i ∈ s, (f i).Nonempty
⊢ #s ≤ #(s.biUnion f)
have rw : LE.le (α := ℕ) (∑ x ∈ s, 1) (∑ u ∈ s, #(f u))
Tactic: rw [card_biUnion hs, card_eq_sum_ones]