awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Module ℚ≥0 α
inst_4 : PosSMulMono ℚ≥0 α
s : Finset ι
f : ι → α
⊢ LE.le.{u_2} (α := α) |𝔼 i ∈ s, f i| (𝔼 i ∈ s, |f i|)

Tactic:
le_expect_of_subadditive abs_zero abs_add_le (fun _ ↦ abs_nnqsmul _)

Premises used: abs_nnqsmul, Nat.cast, Inv.inv, abs_zero, abs_add_le, Finset.le_expect_of_subadditive
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
R : Type u_3
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
inst_4 : Module ℚ≥0 R
inst_5 : PosSMulMono ℚ≥0 R
s : Finset ι
f g : ι → R
simp :
  (HPow.hPow (α := ℚ≥0) (β := ℕ) (↑(#s) : ℚ≥0) 2)⁻¹ • HPow.hPow (α := R) (β := ℕ) (∑ x ∈ s, f x * g x) 2 ≤
    (HPow.hPow (α := ℚ≥0) (β := ℕ) (↑(#s) : ℚ≥0) 2)⁻¹ •
      HMul.hMul (α := R) (∑ x ∈ s, HPow.hPow (β := ℕ) (f x) 2) (∑ x ∈ s, HPow.hPow (β := ℕ) (g x) 2)
⊢ HPow.hPow (α := R) (β := ℕ) (𝔼 i ∈ s, f i * g i) 2 ≤
    HMul.hMul (α := R) (𝔼 i ∈ s, HPow.hPow (β := ℕ) (f i) 2) (𝔼 i ∈ s, HPow.hPow (β := ℕ) (g i) 2)

Tactic:
simp only [expect, smul_pow, inv_pow, smul_mul_smul_comm, ← sq]

Premises used: Finset.expect, smul_mul_smul_comm, sq, inv_pow, smul_pow
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
R : Type u_3
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
inst_4 : Module ℚ≥0 R
inst_5 : PosSMulMono ℚ≥0 R
s : Finset ι
f g : ι → R
hb :
  HPow.hPow (α := R) (β := ℕ) (∑ x ∈ s, f x * g x) 2 ≤
    HMul.hMul (α := R) (∑ x ∈ s, HPow.hPow (β := ℕ) (f x) 2) (∑ x ∈ s, HPow.hPow (β := ℕ) (g x) 2)
⊢ (HPow.hPow (α := ℚ≥0) (β := ℕ) (↑(#s) : ℚ≥0) 2)⁻¹ • HPow.hPow (α := R) (β := ℕ) (∑ x ∈ s, f x * g x) 2 ≤
    (HPow.hPow (α := ℚ≥0) (β := ℕ) (↑(#s) : ℚ≥0) 2)⁻¹ •
      HMul.hMul (α := R) (∑ x ∈ s, HPow.hPow (β := ℕ) (f x) 2) (∑ x ∈ s, HPow.hPow (β := ℕ) (g x) 2)

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
R : Type u_3
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
inst_4 : Module ℚ≥0 R
inst_5 : PosSMulMono ℚ≥0 R
s : Finset ι
f g : ι → R
⊢ HPow.hPow (α := R) (β := ℕ) (∑ x ∈ s, f x * g x) 2 ≤
    HMul.hMul (α := R) (∑ x ∈ s, HPow.hPow (β := ℕ) (f x) 2) (∑ x ∈ s, HPow.hPow (β := ℕ) (g x) 2)

Tactic:
sum_mul_sq_le_sq_mul_sq ..

Premises used: Finset.sum_mul_sq_le_sq_mul_sq
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
R : Type u_3
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
inst_4 : Module ℚ≥0 R
inst_5 : PosSMulMono ℚ≥0 R
s : Finset ι
f g : ι → R
⊢ HPow.hPow (α := R) (β := ℕ) (∑ x ∈ s, f x * g x) 2 ≤
    HMul.hMul (α := R) (∑ x ∈ s, HPow.hPow (β := ℕ) (f x) 2) (∑ x ∈ s, HPow.hPow (β := ℕ) (g x) 2)

Tactic:
exact sum_mul_sq_le_sq_mul_sq ..

Premises used: Finset.sum_mul_sq_le_sq_mul_sq
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype ι
inst_1 : AddCommMonoid α
inst_2 : PartialOrder α
inst_3 : IsOrderedAddMonoid α
inst_4 : Module ℚ≥0 α
f : ι → α
hf : 0 ≤ f
⊢ ∀ (i : ι), Membership.mem (γ := Finset ι) univ i → 0 ≤ f i

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype ι
inst_1 : AddCommMonoid α
inst_2 : PartialOrder α
inst_3 : IsOrderedAddMonoid α
inst_4 : Module ℚ≥0 α
f : ι → α
hf : 0 ≤ f
rw : (∀ (i : ι), Membership.mem (γ := Finset ι) univ i → f i = 0) ↔ f = 0
⊢ Eq.{u_2 + 1} (α := α) (𝔼 i : ι, f i) 0 ↔ f = 0

Tactic:
rw [Finset.expect_eq_zero_iff_of_nonneg (by aesop)]

Premises used: Finset.expect_eq_zero_iff_of_nonneg
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype ι
inst_1 : AddCommMonoid α
inst_2 : PartialOrder α
inst_3 : IsOrderedAddMonoid α
inst_4 : Module ℚ≥0 α
f : ι → α
hf : 0 ≤ f
⊢ (∀ (i : ι), Membership.mem (γ := Finset ι) univ i → f i = 0) ↔ f = 0

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype ι
inst_1 : AddCommMonoid α
inst_2 : PartialOrder α
inst_3 : IsOrderedAddMonoid α
inst_4 : Module ℚ≥0 α
f : ι → α
hf : f ≤ 0
⊢ ∀ (i : ι), Membership.mem (γ := Finset ι) univ i → f i ≤ 0

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype ι
inst_1 : AddCommMonoid α
inst_2 : PartialOrder α
inst_3 : IsOrderedAddMonoid α
inst_4 : Module ℚ≥0 α
f : ι → α
hf : f ≤ 0
rw : (∀ (i : ι), Membership.mem (γ := Finset ι) univ i → f i = 0) ↔ f = 0
⊢ Eq.{u_2 + 1} (α := α) (𝔼 i : ι, f i) 0 ↔ f = 0

Tactic:
rw [Finset.expect_eq_zero_iff_of_nonpos (by aesop)]

Premises used: Finset.expect_eq_zero_iff_of_nonpos
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype ι
inst_1 : AddCommMonoid α
inst_2 : PartialOrder α
inst_3 : IsOrderedAddMonoid α
inst_4 : Module ℚ≥0 α
f : ι → α
hf : f ≤ 0
⊢ (∀ (i : ι), Membership.mem (γ := Finset ι) univ i → f i = 0) ↔ f = 0

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
R : Type u_3
n : ℕ
a : ℕ → ℚ
⊢ LE.le (α := ℚ) 0 (𝔼 j ∈ range n, HPow.hPow (β := ℕ) (a j) 2)

Tactic:
positivity
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
R : Type u_3
a : ULift.{2, 0} ℕ → ℚ
s : Finset (ULift.{2, 0} ℕ)
⊢ LE.le (α := ℚ) 0 (𝔼 j ∈ s, HPow.hPow (β := ℕ) (a j) 2)

Tactic:
positivity
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
R : Type u_3
n : ℕ
a : ℕ → ℚ
⊢ LE.le (α := ℚ) 0
    (𝔼 j : Fin 8, 𝔼 i ∈ range n, (HPow.hPow (β := ℕ) (a (↑j : ℕ)) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑i : ℚ) 2))

Tactic:
positivity
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
R : Type u_3
n : ℕ
a : ℕ → ℚ
⊢ LT.lt (α := ℚ) 0 (𝔼 j : Fin (n + 1), (HPow.hPow (β := ℕ) (a (↑j : ℕ)) 2 + 1))

Tactic:
positivity
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
R : Type u_3
a : ℕ → ℚ
⊢ LT.lt (α := ℚ) 0 (𝔼 j ∈ {1}, (HPow.hPow (β := ℕ) (a j) 2 + 1))

Tactic:
positivity
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
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)
⊢ f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)

Tactic:
le_trans
    (Multiset.le_prod_nonempty_of_submultiplicative_on_pred f p h_mul hp_mul _ ?_ ?_) ?_

Premises used: Multiset.le_prod_nonempty_of_submultiplicative_on_pred, le_trans
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
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
refine_3 : (Multiset.map f (Multiset.map (fun (i : ι) ↦ g i) s.val)).prod ≤ ∏ i ∈ s, f (g i)
⊢ f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)

Tactic:
refine le_trans
    (Multiset.le_prod_nonempty_of_submultiplicative_on_pred f p h_mul hp_mul _ ?_ ?_) ?_

Premises used: Multiset.le_prod_nonempty_of_submultiplicative_on_pred, le_trans
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
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)
⊢ Ne.{u_4 + 1} (α := Multiset M) (Multiset.map (fun (i : ι) ↦ g i) s.val) ∅

Tactic:
simp [hs_nonempty.ne_empty]

Premises used: Finset.Nonempty.ne_empty
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
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)
⊢ ∀ (a : M), Membership.mem (γ := Multiset M) (Multiset.map (fun (i : ι) ↦ g i) s.val) a → p a

Tactic:
Multiset.forall_mem_map_iff.mpr hs

Premises used: Iff.mpr, Multiset.forall_mem_map_iff
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
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)
⊢ ∀ (a : M), Membership.mem (γ := Multiset M) (Multiset.map (fun (i : ι) ↦ g i) s.val) a → p a

Tactic:
exact Multiset.forall_mem_map_iff.mpr hs

Premises used: Iff.mpr, Multiset.forall_mem_map_iff
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
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)
⊢ (Multiset.map f (Multiset.map (fun (i : ι) ↦ g i) s.val)).prod ≤ ∏ i ∈ s, f (g i)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
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
h_mul : ∀ (x y : M), f (x * y) ≤ f x * f y
s : Finset ι
hs : s.Nonempty
g : ι → M
⊢ f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)

Tactic:
le_prod_nonempty_of_submultiplicative_on_pred f (fun _ ↦ True) (fun x y _ _ ↦ h_mul x y)
    (fun _ _ _ _ ↦ trivial) g s hs fun _ _ ↦ trivial

Premises used: Finset.le_prod_nonempty_of_submultiplicative_on_pred, trivial, True
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
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)
inr : ∀ (hs_nonempty : s.Nonempty), f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)
⊢ f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)

Tactic:
rcases eq_empty_or_nonempty s with (rfl | hs_nonempty)

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
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
hs : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → p (g i)
⊢ f (∏ i ∈ ∅, g i) ≤ ∏ i ∈ ∅, f (g i)

Tactic:
simp [h_one]
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
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)
hs_nonempty : s.Nonempty
⊢ f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)

Tactic:
le_prod_nonempty_of_submultiplicative_on_pred f p h_mul hp_mul g s hs_nonempty hs

Premises used: Finset.le_prod_nonempty_of_submultiplicative_on_pred
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
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)
hs_nonempty : s.Nonempty
⊢ f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)

Tactic:
exact le_prod_nonempty_of_submultiplicative_on_pred f p h_mul hp_mul g s hs_nonempty hs

Premises used: Finset.le_prod_nonempty_of_submultiplicative_on_pred
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
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
h_one : f 1 ≤ 1
h_mul : ∀ (x y : M), f (x * y) ≤ f x * f y
s : Finset ι
g : ι → M
⊢ (Multiset.map f (Multiset.map (fun (i : ι) ↦ g i) s.val)).prod ≤ ∏ i ∈ s, f (g i)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
N : Type u_5
inst : CommMonoid N
inst_1 : Preorder N
f g : ι → N
s : Finset ι
inst_2 : MulLeftMono N
h : ∀ i ∈ s, f i ≤ g i
⊢ LE.le.{u_5} (α := N) (∏ i ∈ s, f i) (∏ i ∈ s, g i)

Tactic:
Multiset.prod_map_le_prod_map f g h

Premises used: Finset.prod, Multiset.prod_map_le_prod_map
-- 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
h : ∀ i ∈ s, 1 ≤ f i
rw rw₁ : LE.le.{u_5} (α := N) 1 1
⊢ LE.le.{u_5} (α := N) 1 (∏ i ∈ s, 1)

Tactic:
rw [prod_const_one]

Premises used: Finset.prod_const_one
-- 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
h : ∀ (i : ι), 1 ≤ f i
⊢ LE.le.{u_5} (α := N) 1 (∏ i ∈ s, f i)

Tactic:
Finset.one_le_prod' fun i _ ↦ h i

Premises used: Finset.one_le_prod'
-- 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
h : ∀ i ∈ s, f i ≤ 1
rw rw₁ : Eq.{u_5 + 1} (α := N) 1 1
⊢ Eq.{u_5 + 1} (α := N) (∏ i ∈ s, 1) 1

Tactic:
rw [prod_const_one]

Premises used: Finset.prod_const_one
-- 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 t : Finset ι
inst_2 : MulLeftMono N
h : s ⊆ t
hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i
⊢ ∀ i ∈ t \ s, 1 ≤ f i

Tactic:
simpa only [mem_sdiff, and_imp]

Premises used: and_imp, Finset.mem_sdiff
-- 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 t : Finset ι
inst_2 : MulLeftMono N
h : s ⊆ t
hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i
⊢ HMul.hMul (α := N) (∏ i ∈ t \ s, f i) (∏ i ∈ s, f i) = ∏ i ∈ t \ s ∪ s, f i

Tactic:
(prod_union sdiff_disjoint).symm

Premises used: Finset.prod_union, Eq.symm, Finset.sdiff_disjoint
-- 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 t : Finset ι
inst_2 : MulLeftMono N
h : s ⊆ t
hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i
rw rw₁ : Eq.{u_5 + 1} (α := N) (∏ i ∈ t, f i) (∏ i ∈ t, f i)
⊢ Eq.{u_5 + 1} (α := N) (∏ i ∈ t \ s ∪ s, f i) (∏ i ∈ t, f i)

Tactic:
rw [sdiff_union_of_subset h]

Premises used: Finset.sdiff_union_of_subset
-- 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 t : Finset ι
inst_2 : MulLeftMono N
h : s ⊆ t
hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i
i : Eq.{u_5 + 1} (α := N) (∏ i ∈ t \ s ∪ s, f i) (∏ i ∈ t, f i)
⊢ LE.le.{u_5} (α := N) (∏ i ∈ 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]

Premises used: Finset.prod_union, le_mul_of_one_le_left', Finset.prod, SDiff.sdiff, Finset.one_le_prod', Eq.symm, Finset.sdiff_disjoint
-- 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 t : Finset ι
inst_2 : MulLeftMono N
h : s ⊆ t
hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i
classical : Eq.{u_5 + 1} (α := N) (∏ i ∈ t \ s ∪ s, f i) (∏ i ∈ t, f i)
⊢ LE.le.{u_5} (α := N) (∏ i ∈ 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]

Premises used: Finset.prod_union, le_mul_of_one_le_left', Finset.one_le_prod', Eq.symm, Finset.sdiff_disjoint
-- 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 t : Finset ι
inst_2 : MulLeftMono N
h : s ⊆ t
hf : ∀ i ∈ t, i ∉ s → f i ≤ 1
⊢ LE.le.{u_5} (α := N) (∏ i ∈ t, f i) (∏ i ∈ s, f i)

Tactic:
prod_le_prod_of_subset_of_one_le' (N := Nᵒᵈ) h hf

Premises used: Finset.prod_le_prod_of_subset_of_one_le', OrderDual
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
N : Type u_5
inst : CommMonoid N
inst_1 : Preorder N
f : ι → N
inst_2 : MulLeftMono N
hf : ∀ (x : ι), 1 ≤ f x
⊢ Monotone.{u_1, u_5} (β := N) fun (s : Finset ι) ↦ ∏ x ∈ s, f x

Tactic:
fun _ _ hst ↦ prod_le_prod_of_subset_of_one_le' hst fun x _ _ ↦ hf x

Premises used: Monotone, 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
inst_2 : MulLeftMono N
hf : ∀ (x : ι), f x ≤ 1
x x_1 : Finset ι
hst : x ≤ x_1
⊢ ∀ i ∈ x_1, i ∉ x → f i ≤ 1

Tactic:
simp [hf]
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
N : Type u_5
inst : CommMonoid N
inst_1 : Preorder N
f : ι → N
inst_2 : MulLeftMono N
inst_3 : Fintype ι
s : Finset ι
w : ∀ (x : ι), 1 ≤ f x
⊢ LE.le.{u_5} (α := N) (∏ x ∈ s, f x) (∏ x : ι, f x)

Tactic:
prod_le_prod_of_subset_of_one_le' (subset_univ s) fun a _ _ ↦ w a

Premises used: Finset.prod_le_prod_of_subset_of_one_le', Finset.subset_univ
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
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)

Tactic:
Finset.induction_on s
      (fun _ ↦ ⟨fun _ _ h ↦ False.elim (Finset.notMem_empty _ h), fun _ ↦ rfl⟩) ?_

Premises used: Finset.induction_on
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
N : Type u_5
inst : CommMonoid N
inst_1 : PartialOrder N
f : ι → N
s : Finset ι
inst_2 : MulLeftMono N
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)
⊢ (∀ i ∈ s, 1 ≤ f i) → (Eq.{u_5 + 1} (α := N) (∏ i ∈ s, f i) 1 ↔ ∀ i ∈ s, f i = 1)

Tactic:
refine Finset.induction_on s
      (fun _ ↦ ⟨fun _ _ h ↦ False.elim (Finset.notMem_empty _ h), fun _ ↦ rfl⟩) ?_
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
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
⊢ ∀ i ∈ s, 1 ≤ f i

Tactic:
have : ∀ i ∈ s, 1 ≤ f i := fun _ ↦ H _ ∘ mem_insert_of_mem
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
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
rw₃ rw₄ : (f a = 1 ∧ ∀ 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

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]

Premises used: mul_eq_one_iff_of_one_le, Finset.prod_insert, Finset.mem_insert_self, Finset.forall_mem_insert, Finset.one_le_prod'
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
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
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
⊢ (∀ i ∈ s, 1 ≤ f i) → (Eq.{u_5 + 1} (α := N) (∏ i ∈ s, f i) 1 ↔ ∀ i ∈ 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]

Premises used: Finset.forall_mem_insert
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
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
⊢ LE.le.{u_5} (α := N) 1 (∏ x ∈ s, f x)

Tactic:
have hsum : 1 ≤ ∏ x ∈ s, f x := one_le_prod' hf
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
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)
rw : (∃ (x : ι), ¬(x ∈ s → f x = 1)) ↔ ∃ x ∈ s, 1 < f x
⊢ LT.lt.{u_5} (α := N) 1 (∏ x ∈ s, f x) ↔ ∃ x ∈ s, 1 < f x

Tactic:
rw [hsum.lt_iff_ne', Ne, prod_eq_one_iff_of_one_le' hf, not_forall]

Premises used: Ne, Finset.prod_eq_one_iff_of_one_le', LE.le.lt_iff_ne', Classical.not_forall
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
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)
⊢ (∃ (x : ι), ¬(x ∈ s → f x = 1)) ↔ ∃ x ∈ s, 1 < f x

Tactic:
simp +contextual [← exists_prop, -exists_const_iff, hf _ _ |>.lt_iff_ne']

Premises used: exists_prop, exists_const_iff, LE.le.lt_iff_ne'
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
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, f i ≤ 1) → (Eq.{u_5 + 1} (α := N) (∏ i ∈ s, f i) 1 ↔ ∀ i ∈ s, f i = 1)

Tactic:
prod_eq_one_iff_of_one_le' (N := Nᵒᵈ)

Premises used: Finset.prod_eq_one_iff_of_one_le', OrderDual
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
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, f x ≤ 1
⊢ LT.lt.{u_5} (α := N) (∏ x ∈ s, f x) 1 ↔ ∃ x ∈ s, f x < 1

Tactic:
one_lt_prod_iff_of_one_le (N := Nᵒᵈ) hf

Premises used: Finset.one_lt_prod_iff_of_one_le, OrderDual