awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Module ℚ≥0 α
s : Finset ι
f : ι → α
inst_4 : PosSMulMono ℚ≥0 α
a : α
hs : s.Nonempty
h : ∀ x ∈ s, f x ≤ a
rw : ∑ i ∈ s, (fun (i : ι) ↦ f i) i ≤ #s • a
⊢ ∑ i ∈ s, (fun (i : ι) ↦ f i) i ≤ HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0) a

Tactic:
rw [Nat.cast_smul_eq_nsmul]

Premises used: Nat.cast_smul_eq_nsmul
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Module ℚ≥0 α
s : Finset ι
f : ι → α
inst_4 : PosSMulMono ℚ≥0 α
a : α
hs : s.Nonempty
h : ∀ x ∈ s, f x ≤ a
⊢ ∑ i ∈ s, (fun (i : ι) ↦ f i) i ≤ #s • a

Tactic:
sum_le_card_nsmul _ _ _ h

Premises used: Finset.sum_le_card_nsmul
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Module ℚ≥0 α
s : Finset ι
f : ι → α
inst_4 : PosSMulMono ℚ≥0 α
a : α
hs : s.Nonempty
h : ∀ x ∈ s, f x ≤ a
⊢ ∑ i ∈ s, (fun (i : ι) ↦ f i) i ≤ #s • a

Tactic:
exact sum_le_card_nsmul _ _ _ h

Premises used: Finset.sum_le_card_nsmul
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Module ℚ≥0 α
s : Finset ι
f : ι → α
inst_4 : PosSMulMono ℚ≥0 α
a : α
hs : s.Nonempty
h : ∀ x ∈ s, a ≤ f x
rw : #s • a ≤ ∑ i ∈ s, (fun (i : ι) ↦ f i) i
⊢ HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0) a ≤ ∑ i ∈ s, (fun (i : ι) ↦ f i) i

Tactic:
rw [Nat.cast_smul_eq_nsmul]

Premises used: Nat.cast_smul_eq_nsmul
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Module ℚ≥0 α
s : Finset ι
f : ι → α
inst_4 : PosSMulMono ℚ≥0 α
a : α
hs : s.Nonempty
h : ∀ x ∈ s, a ≤ f x
⊢ #s • a ≤ ∑ i ∈ s, (fun (i : ι) ↦ f i) i

Tactic:
card_nsmul_le_sum _ _ _ h

Premises used: Finset.card_nsmul_le_sum
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Module ℚ≥0 α
s : Finset ι
f : ι → α
inst_4 : PosSMulMono ℚ≥0 α
a : α
hs : s.Nonempty
h : ∀ x ∈ s, a ≤ f x
⊢ #s • a ≤ ∑ i ∈ s, (fun (i : ι) ↦ f i) i

Tactic:
exact card_nsmul_le_sum _ _ _ h

Premises used: Finset.card_nsmul_le_sum
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Module ℚ≥0 α
s : Finset ι
f : ι → α
inst_4 : PosSMulMono ℚ≥0 α
hf : ∀ i ∈ s, 0 ≤ f i
⊢ LE.le (α := ℚ≥0) 0 (↑(#s) : ℚ≥0)⁻¹

Tactic:
positivity
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
inst_2 : AddCommMonoid N
inst_3 : PartialOrder N
inst_4 : IsOrderedAddMonoid N
inst_5 : Module ℚ≥0 N
inst_6 : PosSMulMono ℚ≥0 N
m : M → N
p : M → Prop
f : ι → M
s : Finset ι
h_add : ∀ (a b : M), p a → p b → m (a + b) ≤ m a + m b
hp_add : ∀ (a b : M), p a → p b → p (a + b)
h_div : ∀ (n : ℕ) (a : M), p a → m (HSMul.hSMul (α := ℚ≥0) (↑n : ℚ≥0)⁻¹ a) = HSMul.hSMul (α := ℚ≥0) (↑n : ℚ≥0)⁻¹ (m a)
hs_nonempty : s.Nonempty
hs : ∀ i ∈ s, p (f i)
simp :
  HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ (m (∑ x ∈ s, f x)) ≤
    HSMul.hSMul (α := ℚ≥0) (β := N) (↑(#s) : ℚ≥0)⁻¹ (∑ x ∈ s, m (f x))
⊢ m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i)

Tactic:
simp only [expect, h_div _ _ (sum_induction_nonempty _ _ hp_add hs_nonempty hs)]

Premises used: Finset.sum_induction_nonempty, Finset.expect
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
inst_2 : AddCommMonoid N
inst_3 : PartialOrder N
inst_4 : IsOrderedAddMonoid N
inst_5 : Module ℚ≥0 N
inst_6 : PosSMulMono ℚ≥0 N
m : M → N
p : M → Prop
f : ι → M
s : Finset ι
h_add : ∀ (a b : M), p a → p b → m (a + b) ≤ m a + m b
hp_add : ∀ (a b : M), p a → p b → p (a + b)
h_div : ∀ (n : ℕ) (a : M), p a → m (HSMul.hSMul (α := ℚ≥0) (↑n : ℚ≥0)⁻¹ a) = HSMul.hSMul (α := ℚ≥0) (↑n : ℚ≥0)⁻¹ (m a)
hs_nonempty : s.Nonempty
hs : ∀ i ∈ s, p (f i)
⊢ LE.le (α := ℚ≥0) 0 (↑(#s) : ℚ≥0)⁻¹

Tactic:
positivity
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
inst_2 : AddCommMonoid N
inst_3 : PartialOrder N
inst_4 : IsOrderedAddMonoid N
inst_5 : Module ℚ≥0 N
inst_6 : PosSMulMono ℚ≥0 N
m : M → N
p : M → Prop
f : ι → M
s : Finset ι
h_add : ∀ (a b : M), p a → p b → m (a + b) ≤ m a + m b
hp_add : ∀ (a b : M), p a → p b → p (a + b)
h_div : ∀ (n : ℕ) (a : M), p a → m (HSMul.hSMul (α := ℚ≥0) (↑n : ℚ≥0)⁻¹ a) = HSMul.hSMul (α := ℚ≥0) (↑n : ℚ≥0)⁻¹ (m a)
hs_nonempty : s.Nonempty
hs : ∀ i ∈ s, p (f i)
⊢ HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ (m (∑ x ∈ s, f x)) ≤
    HSMul.hSMul (α := ℚ≥0) (β := N) (↑(#s) : ℚ≥0)⁻¹ (∑ x ∈ s, m (f x))

Tactic:
exact smul_le_smul_of_nonneg_left
    (le_sum_nonempty_of_subadditive_on_pred _ _ h_add hp_add _ _ hs_nonempty hs) <| by positivity

Premises used: Finset.le_sum_nonempty_of_subadditive_on_pred, smul_le_smul_of_nonneg_left
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
inst_2 : AddCommMonoid N
inst_3 : PartialOrder N
inst_4 : IsOrderedAddMonoid N
inst_5 : Module ℚ≥0 N
inst_6 : PosSMulMono ℚ≥0 N
f : ι → M
s : Finset ι
m : M → N
h_mul : ∀ (a b : M), m (a + b) ≤ m a + m b
h_div : ∀ (n : ℕ) (a : M), m (HSMul.hSMul (α := ℚ≥0) (↑n : ℚ≥0)⁻¹ a) = HSMul.hSMul (α := ℚ≥0) (↑n : ℚ≥0)⁻¹ (m a)
hs : s.Nonempty
⊢ ∀ (a b : M), (fun (x : M) ↦ True) a → (fun (x : M) ↦ True) b → m (a + b) ≤ m a + m b

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
inst_2 : AddCommMonoid N
inst_3 : PartialOrder N
inst_4 : IsOrderedAddMonoid N
inst_5 : Module ℚ≥0 N
inst_6 : PosSMulMono ℚ≥0 N
f : ι → M
s : Finset ι
m : M → N
h_mul : ∀ (a b : M), m (a + b) ≤ m a + m b
h_div : ∀ (n : ℕ) (a : M), m (HSMul.hSMul (α := ℚ≥0) (↑n : ℚ≥0)⁻¹ a) = HSMul.hSMul (α := ℚ≥0) (↑n : ℚ≥0)⁻¹ (m a)
hs : s.Nonempty
⊢ ∀ (a b : M), (fun (x : M) ↦ True) a → (fun (x : M) ↦ True) b → (fun (x : M) ↦ True) (a + b)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
inst_2 : AddCommMonoid N
inst_3 : PartialOrder N
inst_4 : IsOrderedAddMonoid N
inst_5 : Module ℚ≥0 N
inst_6 : PosSMulMono ℚ≥0 N
f : ι → M
s : Finset ι
m : M → N
h_mul : ∀ (a b : M), m (a + b) ≤ m a + m b
h_div : ∀ (n : ℕ) (a : M), m (HSMul.hSMul (α := ℚ≥0) (↑n : ℚ≥0)⁻¹ a) = HSMul.hSMul (α := ℚ≥0) (↑n : ℚ≥0)⁻¹ (m a)
hs : s.Nonempty
⊢ ∀ (n : ℕ) (a : M),
    (fun (x : M) ↦ True) a → m (HSMul.hSMul (α := ℚ≥0) (↑n : ℚ≥0)⁻¹ a) = HSMul.hSMul (α := ℚ≥0) (↑n : ℚ≥0)⁻¹ (m a)

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
inst_2 : AddCommMonoid N
inst_3 : PartialOrder N
inst_4 : IsOrderedAddMonoid N
inst_5 : Module ℚ≥0 N
inst_6 : PosSMulMono ℚ≥0 N
f : ι → M
s : Finset ι
m : M → N
h_mul : ∀ (a b : M), m (a + b) ≤ m a + m b
h_div : ∀ (n : ℕ) (a : M), m (HSMul.hSMul (α := ℚ≥0) (↑n : ℚ≥0)⁻¹ a) = HSMul.hSMul (α := ℚ≥0) (↑n : ℚ≥0)⁻¹ (m a)
hs : s.Nonempty
⊢ ∀ i ∈ s, (fun (x : M) ↦ True) (f i)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
inst_2 : AddCommMonoid N
inst_3 : PartialOrder N
inst_4 : IsOrderedAddMonoid N
inst_5 : Module ℚ≥0 N
inst_6 : PosSMulMono ℚ≥0 N
m : M → N
p : M → Prop
f : ι → M
s : Finset ι
h_zero : m 0 = 0
h_add : ∀ (a b : M), p a → p b → m (a + b) ≤ m a + m b
hp_add : ∀ (a b : M), p a → p b → p (a + b)
h_div : ∀ (n : ℕ) (a : M), p a → m (HSMul.hSMul (α := ℚ≥0) (↑n : ℚ≥0)⁻¹ a) = HSMul.hSMul (α := ℚ≥0) (↑n : ℚ≥0)⁻¹ (m a)
hs : ∀ i ∈ s, p (f i)
inl : ∀ (hs : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → p (f i)), m (𝔼 i ∈ ∅, f i) ≤ 𝔼 i ∈ ∅, m (f i)
inr : ∀ (hs_nonempty : s.Nonempty), m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i)
⊢ m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i)

Tactic:
obtain rfl | hs_nonempty := s.eq_empty_or_nonempty

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
inst_2 : AddCommMonoid N
inst_3 : PartialOrder N
inst_4 : IsOrderedAddMonoid N
inst_5 : Module ℚ≥0 N
inst_6 : PosSMulMono ℚ≥0 N
m : M → N
p : M → Prop
f : ι → M
h_zero : m 0 = 0
h_add : ∀ (a b : M), p a → p b → m (a + b) ≤ m a + m b
hp_add : ∀ (a b : M), p a → p b → p (a + b)
h_div : ∀ (n : ℕ) (a : M), p a → m (HSMul.hSMul (α := ℚ≥0) (↑n : ℚ≥0)⁻¹ a) = HSMul.hSMul (α := ℚ≥0) (↑n : ℚ≥0)⁻¹ (m a)
hs : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → p (f i)
⊢ m (𝔼 i ∈ ∅, f i) ≤ 𝔼 i ∈ ∅, m (f i)

Tactic:
simp [h_zero]
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
inst_2 : AddCommMonoid N
inst_3 : PartialOrder N
inst_4 : IsOrderedAddMonoid N
inst_5 : Module ℚ≥0 N
inst_6 : PosSMulMono ℚ≥0 N
m : M → N
p : M → Prop
f : ι → M
s : Finset ι
h_zero : m 0 = 0
h_add : ∀ (a b : M), p a → p b → m (a + b) ≤ m a + m b
hp_add : ∀ (a b : M), p a → p b → p (a + b)
h_div : ∀ (n : ℕ) (a : M), p a → m (HSMul.hSMul (α := ℚ≥0) (↑n : ℚ≥0)⁻¹ a) = HSMul.hSMul (α := ℚ≥0) (↑n : ℚ≥0)⁻¹ (m a)
hs : ∀ i ∈ s, p (f i)
hs_nonempty : s.Nonempty
⊢ m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i)

Tactic:
le_expect_nonempty_of_subadditive_on_pred h_add hp_add h_div hs_nonempty hs

Premises used: Finset.le_expect_nonempty_of_subadditive_on_pred
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
inst_2 : AddCommMonoid N
inst_3 : PartialOrder N
inst_4 : IsOrderedAddMonoid N
inst_5 : Module ℚ≥0 N
inst_6 : PosSMulMono ℚ≥0 N
m : M → N
p : M → Prop
f : ι → M
s : Finset ι
h_zero : m 0 = 0
h_add : ∀ (a b : M), p a → p b → m (a + b) ≤ m a + m b
hp_add : ∀ (a b : M), p a → p b → p (a + b)
h_div : ∀ (n : ℕ) (a : M), p a → m (HSMul.hSMul (α := ℚ≥0) (↑n : ℚ≥0)⁻¹ a) = HSMul.hSMul (α := ℚ≥0) (↑n : ℚ≥0)⁻¹ (m a)
hs : ∀ i ∈ s, p (f i)
hs_nonempty : s.Nonempty
⊢ m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i)

Tactic:
exact le_expect_nonempty_of_subadditive_on_pred h_add hp_add h_div hs_nonempty hs

Premises used: Finset.le_expect_nonempty_of_subadditive_on_pred
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
inst_2 : AddCommMonoid N
inst_3 : PartialOrder N
inst_4 : IsOrderedAddMonoid N
inst_5 : Module ℚ≥0 N
inst_6 : PosSMulMono ℚ≥0 N
m : M → N
f : ι → M
s : Finset ι
h_zero : m 0 = 0
h_add : ∀ (a b : M), m (a + b) ≤ m a + m b
h_div : ∀ (n : ℕ) (a : M), m (HSMul.hSMul (α := ℚ≥0) (↑n : ℚ≥0)⁻¹ a) = HSMul.hSMul (α := ℚ≥0) (↑n : ℚ≥0)⁻¹ (m a)
⊢ ∀ (a b : M), (fun (x : M) ↦ True) a → (fun (x : M) ↦ True) b → m (a + b) ≤ m a + m b

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
inst_2 : AddCommMonoid N
inst_3 : PartialOrder N
inst_4 : IsOrderedAddMonoid N
inst_5 : Module ℚ≥0 N
inst_6 : PosSMulMono ℚ≥0 N
m : M → N
f : ι → M
s : Finset ι
h_zero : m 0 = 0
h_add : ∀ (a b : M), m (a + b) ≤ m a + m b
h_div : ∀ (n : ℕ) (a : M), m (HSMul.hSMul (α := ℚ≥0) (↑n : ℚ≥0)⁻¹ a) = HSMul.hSMul (α := ℚ≥0) (↑n : ℚ≥0)⁻¹ (m a)
⊢ ∀ (a b : M), (fun (x : M) ↦ True) a → (fun (x : M) ↦ True) b → (fun (x : M) ↦ True) (a + b)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
inst_2 : AddCommMonoid N
inst_3 : PartialOrder N
inst_4 : IsOrderedAddMonoid N
inst_5 : Module ℚ≥0 N
inst_6 : PosSMulMono ℚ≥0 N
m : M → N
f : ι → M
s : Finset ι
h_zero : m 0 = 0
h_add : ∀ (a b : M), m (a + b) ≤ m a + m b
h_div : ∀ (n : ℕ) (a : M), m (HSMul.hSMul (α := ℚ≥0) (↑n : ℚ≥0)⁻¹ a) = HSMul.hSMul (α := ℚ≥0) (↑n : ℚ≥0)⁻¹ (m a)
⊢ ∀ (n : ℕ) (a : M),
    (fun (x : M) ↦ True) a → m (HSMul.hSMul (α := ℚ≥0) (↑n : ℚ≥0)⁻¹ a) = HSMul.hSMul (α := ℚ≥0) (↑n : ℚ≥0)⁻¹ (m a)

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
inst_2 : AddCommMonoid N
inst_3 : PartialOrder N
inst_4 : IsOrderedAddMonoid N
inst_5 : Module ℚ≥0 N
inst_6 : PosSMulMono ℚ≥0 N
m : M → N
f : ι → M
s : Finset ι
h_zero : m 0 = 0
h_add : ∀ (a b : M), m (a + b) ≤ m a + m b
h_div : ∀ (n : ℕ) (a : M), m (HSMul.hSMul (α := ℚ≥0) (↑n : ℚ≥0)⁻¹ a) = HSMul.hSMul (α := ℚ≥0) (↑n : ℚ≥0)⁻¹ (m a)
⊢ ∀ i ∈ s, (fun (x : M) ↦ True) (f i)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Module ℚ≥0 α
inst_4 : PosSMulStrictMono ℚ≥0 α
s : Finset ι
f g : ι → α
hfg : ∀ i ∈ s, f i ≤ g i
hfg' : ∃ i ∈ s, f i < g i
obtain : ∀ (i : ι) (hi : i ∈ s), LT.lt (α := ℚ≥0) 0 (↑(#s) : ℚ≥0)⁻¹
⊢ LT.lt (α := ℚ≥0) 0 (↑(#s) : ℚ≥0)⁻¹

Tactic:
obtain ⟨i, hi, -⟩ := hfg'
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Module ℚ≥0 α
inst_4 : PosSMulStrictMono ℚ≥0 α
s : Finset ι
f g : ι → α
hfg : ∀ i ∈ s, f i ≤ g i
i : ι
hi : i ∈ s
⊢ s.Nonempty

Tactic:
have : s.Nonempty := ⟨i, hi⟩
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Module ℚ≥0 α
inst_4 : PosSMulStrictMono ℚ≥0 α
s : Finset ι
f g : ι → α
hfg : ∀ i ∈ s, f i ≤ g i
i : ι
hi : i ∈ s
this : s.Nonempty
⊢ LT.lt (α := ℚ≥0) 0 (↑(#s) : ℚ≥0)⁻¹

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Module ℚ≥0 α
inst_4 : PosSMulStrictMono ℚ≥0 α
s : Finset ι
f : ι → α
a : α
hle : ∀ x ∈ s, f x ≤ a
hlt : ∃ x ∈ s, f x < a
rw : LT.lt.{u_2} (α := α) (𝔼 i ∈ s, f i) (𝔼 _i ∈ s, a)
⊢ 𝔼 i ∈ s, f i < a

Tactic:
rw [← expect_const (hlt.imp (fun _ => And.left)) a]

Premises used: Finset.expect_const, Exists.imp, And.left
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Module ℚ≥0 α
inst_4 : PosSMulStrictMono ℚ≥0 α
s : Finset ι
f : ι → α
a : α
hle : ∀ x ∈ s, f x ≤ a
hlt : ∃ x ∈ s, f x < a
⊢ LT.lt.{u_2} (α := α) (𝔼 i ∈ s, f i) (𝔼 _i ∈ s, a)

Tactic:
expect_lt_expect hle hlt

Premises used: Finset.expect_lt_expect
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Module ℚ≥0 α
inst_4 : PosSMulStrictMono ℚ≥0 α
s : Finset ι
f : ι → α
a : α
hle : ∀ x ∈ s, f x ≤ a
hlt : ∃ x ∈ s, f x < a
⊢ LT.lt.{u_2} (α := α) (𝔼 i ∈ s, f i) (𝔼 _i ∈ s, a)

Tactic:
exact expect_lt_expect hle hlt

Premises used: Finset.expect_lt_expect
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Module ℚ≥0 α
inst_4 : PosSMulStrictMono ℚ≥0 α
s : Finset ι
f : ι → α
a : α
hle : ∀ x ∈ s, a ≤ f x
hlt : ∃ x ∈ s, a < f x
rw : LT.lt.{u_2} (α := α) (𝔼 _i ∈ s, a) (𝔼 i ∈ s, f i)
⊢ a < 𝔼 i ∈ s, f i

Tactic:
rw [← expect_const (hlt.imp (fun _ => And.left)) a]

Premises used: Finset.expect_const, Exists.imp, And.left
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Module ℚ≥0 α
inst_4 : PosSMulStrictMono ℚ≥0 α
s : Finset ι
f : ι → α
a : α
hle : ∀ x ∈ s, a ≤ f x
hlt : ∃ x ∈ s, a < f x
⊢ LT.lt.{u_2} (α := α) (𝔼 _i ∈ s, a) (𝔼 i ∈ s, f i)

Tactic:
expect_lt_expect hle hlt

Premises used: Finset.expect_lt_expect
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Module ℚ≥0 α
inst_4 : PosSMulStrictMono ℚ≥0 α
s : Finset ι
f : ι → α
a : α
hle : ∀ x ∈ s, a ≤ f x
hlt : ∃ x ∈ s, a < f x
⊢ LT.lt.{u_2} (α := α) (𝔼 _i ∈ s, a) (𝔼 i ∈ s, f i)

Tactic:
exact expect_lt_expect hle hlt

Premises used: Finset.expect_lt_expect
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Module ℚ≥0 α
inst_4 : PosSMulStrictMono ℚ≥0 α
s : Finset ι
f : ι → α
h : ∀ i ∈ s, 0 ≤ f i
hs : ∃ i ∈ s, 0 < f i
⊢ LT.lt.{u_2} (α := α) 0 (𝔼 i ∈ s, f i)

Tactic:
(expect_const_zero _).symm.trans_lt <| expect_lt_expect h hs

Premises used: Finset.expect_const_zero, Finset.expect_lt_expect, Eq.trans_lt, Eq.symm
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Module ℚ≥0 α
inst_4 : PosSMulStrictMono ℚ≥0 α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 < f i
hs : s.Nonempty
⊢ LT.lt.{u_2} (α := α) 0 (𝔼 i ∈ s, f i)

Tactic:
smul_pos (inv_pos.2 <| mod_cast hs.card_pos) <| sum_pos hf hs

Premises used: Iff.mpr, Finset.expect, congrArg, Nat.cast_lt._simp_1, cast, Finset.sum_pos, Finset.Nonempty.card_pos, inv_pos, Nat.cast, LT.lt, Finset.card, congrFun', smul_pos, Nat.cast_zero, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Module ℚ≥0 α
inst_4 : PosSMulMono ℚ≥0 α
s : Finset ι
f g : ι → α
h : LT.lt.{u_2} (α := α) (𝔼 i ∈ s, g i) (𝔼 i ∈ s, f i)
contrapose! : ∀ (h : ∀ (x : ι) (_ : x ∈ s), f x ≤ g x), LE.le.{u_2} (α := α) (𝔼 i ∈ s, f i) (𝔼 i ∈ s, g i)
⊢ ∃ x ∈ s, g x < f x

Tactic:
contrapose! h
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Module ℚ≥0 α
inst_4 : PosSMulMono ℚ≥0 α
s : Finset ι
f g : ι → α
h : ∀ (x : ι) (_ : x ∈ s), f x ≤ g x
⊢ LE.le.{u_2} (α := α) (𝔼 i ∈ s, f i) (𝔼 i ∈ s, g i)

Tactic:
expect_le_expect h

Premises used: Finset.expect_le_expect
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Module ℚ≥0 α
inst_4 : PosSMulMono ℚ≥0 α
s : Finset ι
f g : ι → α
h : ∀ (x : ι) (_ : x ∈ s), f x ≤ g x
⊢ LE.le.{u_2} (α := α) (𝔼 i ∈ s, f i) (𝔼 i ∈ s, g i)

Tactic:
exact expect_le_expect h

Premises used: Finset.expect_le_expect
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Module ℚ≥0 α
inst_4 : PosSMulMono ℚ≥0 α
s : Finset ι
f : ι → α
a : α
hs : s.Nonempty
h : a < 𝔼 i ∈ s, f i
contrapose! : ∀ (h : ∀ (x : ι) (_ : x ∈ s), f x ≤ a), 𝔼 i ∈ s, f i ≤ a
⊢ ∃ x ∈ s, a < f x

Tactic:
contrapose! h
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Module ℚ≥0 α
inst_4 : PosSMulMono ℚ≥0 α
s : Finset ι
f : ι → α
a : α
hs : s.Nonempty
h : ∀ (x : ι) (_ : x ∈ s), f x ≤ a
⊢ 𝔼 i ∈ s, f i ≤ a

Tactic:
expect_le hs h

Premises used: Finset.expect_le
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Module ℚ≥0 α
inst_4 : PosSMulMono ℚ≥0 α
s : Finset ι
f : ι → α
a : α
hs : s.Nonempty
h : ∀ (x : ι) (_ : x ∈ s), f x ≤ a
⊢ 𝔼 i ∈ s, f i ≤ a

Tactic:
exact expect_le hs h

Premises used: Finset.expect_le
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Module ℚ≥0 α
inst_4 : PosSMulMono ℚ≥0 α
s : Finset ι
f : ι → α
a : α
hs : s.Nonempty
h : 𝔼 i ∈ s, f i < a
contrapose! : ∀ (h : ∀ (x : ι) (_ : x ∈ s), a ≤ f x), a ≤ 𝔼 i ∈ s, f i
⊢ ∃ x ∈ s, f x < a

Tactic:
contrapose! h
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Module ℚ≥0 α
inst_4 : PosSMulMono ℚ≥0 α
s : Finset ι
f : ι → α
a : α
hs : s.Nonempty
h : ∀ (x : ι) (_ : x ∈ s), a ≤ f x
⊢ a ≤ 𝔼 i ∈ s, f i

Tactic:
le_expect hs h

Premises used: Finset.le_expect
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Module ℚ≥0 α
inst_4 : PosSMulMono ℚ≥0 α
s : Finset ι
f : ι → α
a : α
hs : s.Nonempty
h : ∀ (x : ι) (_ : x ∈ s), a ≤ f x
⊢ a ≤ 𝔼 i ∈ s, f i

Tactic:
exact le_expect hs h

Premises used: Finset.le_expect
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Module ℚ≥0 α
inst_4 : PosSMulStrictMono ℚ≥0 α
s : Finset ι
f g : ι → α
hs : s.Nonempty
h : LE.le.{u_2} (α := α) (𝔼 i ∈ s, g i) (𝔼 i ∈ s, f i)
obtain : ∀ (w : ι) (hx : w ∈ s), ∃ x ∈ s, g x ≤ f x
⊢ ∃ x ∈ s, g x ≤ f x

Tactic:
obtain ⟨_, hx⟩ := hs
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Module ℚ≥0 α
inst_4 : PosSMulStrictMono ℚ≥0 α
s : Finset ι
f g : ι → α
h : LE.le.{u_2} (α := α) (𝔼 i ∈ s, g i) (𝔼 i ∈ s, f i)
w : ι
hx : w ∈ s
contrapose! : ∀ (h : ∀ (x : ι) (_ : x ∈ s), f x < g x), LT.lt.{u_2} (α := α) (𝔼 i ∈ s, f i) (𝔼 i ∈ s, g i)
⊢ ∃ x ∈ s, g x ≤ f x

Tactic:
contrapose! h
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Module ℚ≥0 α
inst_4 : PosSMulStrictMono ℚ≥0 α
s : Finset ι
f g : ι → α
w : ι
hx : w ∈ s
h : ∀ (x : ι) (_ : x ∈ s), f x < g x
⊢ LT.lt.{u_2} (α := α) (𝔼 i ∈ s, f i) (𝔼 i ∈ s, g i)

Tactic:
expect_lt_expect (fun _ hx ↦ le_of_lt (h _ hx)) ⟨_, ⟨hx, h _ hx⟩⟩

Premises used: le_of_lt, Finset.expect_lt_expect, And.intro, Exists.intro
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Module ℚ≥0 α
inst_4 : PosSMulStrictMono ℚ≥0 α
s : Finset ι
f g : ι → α
w : ι
hx : w ∈ s
h : ∀ (x : ι) (_ : x ∈ s), f x < g x
⊢ LT.lt.{u_2} (α := α) (𝔼 i ∈ s, f i) (𝔼 i ∈ s, g i)

Tactic:
exact expect_lt_expect (fun _ hx ↦ le_of_lt (h _ hx)) ⟨_, ⟨hx, h _ hx⟩⟩

Premises used: le_of_lt, Finset.expect_lt_expect, And.intro, Exists.intro
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Module ℚ≥0 α
inst_4 : PosSMulStrictMono ℚ≥0 α
a : α
s : Finset ι
f : ι → α
hs : s.Nonempty
h rwa rwa₁ rwa₂ rwa₃ : a ≤ 𝔼 i ∈ s, f i
⊢ LE.le.{u_2} (α := α) (𝔼 i ∈ s, a) (𝔼 i ∈ s, f i)

Tactic:
rwa [expect_const hs _]

Premises used: Finset.expect_const
-- Module: Mathlib.Algebra.Order.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Module ℚ≥0 α
inst_4 : PosSMulStrictMono ℚ≥0 α
a : α
s : Finset ι
f : ι → α
hs : s.Nonempty
h rwa rwa₁ rwa₂ rwa₃ : 𝔼 i ∈ s, f i ≤ a
⊢ LE.le.{u_2} (α := α) (𝔼 i ∈ s, f i) (𝔼 i ∈ s, a)

Tactic:
rwa [expect_const hs _]

Premises used: Finset.expect_const