awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.IndicatorCard (hypothesis)
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : PartialOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : AddLeftStrictMono R
inst_4 : Archimedean R
r : R
h : 0 < r
s : Set ℕ
⊢ s.Infinite →
    Tendsto.{0, u_1} (β := R) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, s.indicator (fun (x : ℕ) ↦ r) k) atTop atTop
have h_mono : Monotone.{0, u_1} (β := R) fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, s.indicator (fun (x : ℕ) ↦ r) k
Tactic: have h_mono : Monotone fun n ↦ ∑ k ∈ Finset.range n, s.indicator (fun _ ↦ r) k := by
      refine (sum_mono_set_of_nonneg ?_).comp range_mono
      exact (fun _ ↦ indicator_nonneg (fun _ _ ↦ h.le) _)
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.IndicatorCard (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : PartialOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : AddLeftStrictMono R
inst_4 : Archimedean R
r : R
h : 0 < r
s : Set ℕ
h_mono : Monotone.{0, u_1} (β := R) fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, s.indicator (fun (x : ℕ) ↦ r) k
⊢ s.Infinite →
    Tendsto.{0, u_1} (β := R) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, s.indicator (fun (x : ℕ) ↦ r) k) atTop atTop
have mp : s.Infinite → ∀ (b : R), ∃ (a : ℕ), b ≤ ∑ k ∈ Finset.range a, s.indicator (fun (x : ℕ) ↦ r) k
Tactic: rw [h_mono.tendsto_atTop_atTop_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.IndicatorCard (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : PartialOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : AddLeftStrictMono R
inst_4 : Archimedean R
r : R
h : 0 < r
s : Set ℕ
h_mono : Monotone.{0, u_1} (β := R) fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, s.indicator (fun (x : ℕ) ↦ r) k
hs : s.Infinite
n : R
⊢ ∃ (a : ℕ), n ≤ ∑ k ∈ Finset.range a, s.indicator (fun (x : ℕ) ↦ r) k
have mp : ∀ (n' : ℕ) (hn' : n < n' • r), ∃ (a : ℕ), n ≤ ∑ k ∈ Finset.range a, s.indicator (fun (x : ℕ) ↦ r) k
Tactic: obtain ⟨n', hn'⟩ := exists_lt_nsmul h n
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.IndicatorCard (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : PartialOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : AddLeftStrictMono R
inst_4 : Archimedean R
r : R
h : 0 < r
s : Set ℕ
h_mono : Monotone.{0, u_1} (β := R) fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, s.indicator (fun (x : ℕ) ↦ r) k
hs : s.Infinite
n : R
n' : ℕ
hn' : n < n' • r
⊢ ∃ (a : ℕ), n ≤ ∑ k ∈ Finset.range a, s.indicator (fun (x : ℕ) ↦ r) k
have mp : ∀ (t : Finset ℕ) (t_s : (↑t : Set ℕ) ⊆ s) (t_card : #t = n'),
  ∃ (a : ℕ), n ≤ ∑ k ∈ Finset.range a, s.indicator (fun (x : ℕ) ↦ r) k
Tactic: obtain ⟨t, t_s, t_card⟩ := hs.exists_subset_card_eq n'
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.IndicatorCard (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : PartialOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : AddLeftStrictMono R
inst_4 : Archimedean R
r : R
h : 0 < r
s : Set ℕ
h_mono : Monotone.{0, u_1} (β := R) fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, s.indicator (fun (x : ℕ) ↦ r) k
hs : s.Infinite
n : R
n' : ℕ
hn' : n < n' • r
t : Finset ℕ
t_s : (↑t : Set ℕ) ⊆ s
t_card : #t = n'
⊢ ∃ (a : ℕ), n ≤ ∑ k ∈ Finset.range a, s.indicator (fun (x : ℕ) ↦ r) k
have mp : ∀ (m : ℕ) (hm : m ∈ upperBounds (↑t : Set ℕ)), ∃ (a : ℕ), n ≤ ∑ k ∈ Finset.range a, s.indicator (fun (x : ℕ) ↦ r) k
Tactic: obtain ⟨m, hm⟩ := t.bddAbove
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.IndicatorCard (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : PartialOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : AddLeftStrictMono R
inst_4 : Archimedean R
r : R
h : 0 < r
s : Set ℕ
h_mono : Monotone.{0, u_1} (β := R) fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, s.indicator (fun (x : ℕ) ↦ r) k
hs : s.Infinite
n : R
n' : ℕ
hn' : n < n' • r
t : Finset ℕ
t_s : (↑t : Set ℕ) ⊆ s
t_card : #t = n'
m : ℕ
hm : m ∈ upperBounds (↑t : Set ℕ)
⊢ ∃ (a : ℕ), n ≤ ∑ k ∈ Finset.range a, s.indicator (fun (x : ℕ) ↦ r) k
have h₁ : n ≤ ∑ k ∈ Finset.range (m + 1), s.indicator (fun (x : ℕ) ↦ r) k
Tactic: use m + 1
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.IndicatorCard (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : PartialOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : AddLeftStrictMono R
inst_4 : Archimedean R
r : R
h : 0 < r
s : Set ℕ
h_mono : Monotone.{0, u_1} (β := R) fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, s.indicator (fun (x : ℕ) ↦ r) k
hs : s.Infinite
n : R
n' : ℕ
hn' : n < n' • r
t : Finset ℕ
t_s : (↑t : Set ℕ) ⊆ s
t_card : #t = n'
m : ℕ
hm : m ∈ upperBounds (↑t : Set ℕ)
⊢ n ≤ ∑ k ∈ Finset.range (m + 1), s.indicator (fun (x : ℕ) ↦ r) k
have h₁ : n' • r ≤ ∑ k ∈ Finset.range (m + 1), (↑t : Set ℕ).indicator (fun (x : ℕ) ↦ r) k
Tactic: grw [hn', ← t_s]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.IndicatorCard (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : PartialOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : AddLeftStrictMono R
inst_4 : Archimedean R
r : R
h : 0 < r
s : Set ℕ
h_mono : Monotone.{0, u_1} (β := R) fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, s.indicator (fun (x : ℕ) ↦ r) k
hs : s.Infinite
n : R
n' : ℕ
hn' : n < n' • r
t : Finset ℕ
t_s : (↑t : Set ℕ) ⊆ s
t_card : #t = n'
m : ℕ
hm : m ∈ upperBounds (↑t : Set ℕ)
i : ℕ
i_t : i ∈ t
⊢ i ∈ Finset.range (m + 1)
have rw : i < m + 1
Tactic: rw [Finset.mem_range]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.IndicatorCard (hypothesis)
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : PartialOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : AddLeftStrictMono R
inst_4 : Archimedean R
r : R
h : 0 < r
s : Set ℕ
h_mono : Monotone.{0, u_1} (β := R) fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, s.indicator (fun (x : ℕ) ↦ r) k
hs : s.Infinite
n : R
n' : ℕ
hn' : n < n' • r
t : Finset ℕ
t_s : (↑t : Set ℕ) ⊆ s
t_card : #t = n'
m : ℕ
hm : m ∈ upperBounds (↑t : Set ℕ)
⊢ n' • r ≤ ∑ k ∈ Finset.range (m + 1), (↑t : Set ℕ).indicator (fun (x : ℕ) ↦ r) k
have h₁ : t ⊆ Finset.range (m + 1)
Tactic: have h : t ⊆ Finset.range (m + 1) := by
      intro i i_t
      rw [Finset.mem_range]
      exact (hm i_t).trans_lt (lt_add_one m)
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.IndicatorCard (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : PartialOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : AddLeftStrictMono R
inst_4 : Archimedean R
r : R
h_1 : 0 < r
s : Set ℕ
h_mono : Monotone.{0, u_1} (β := R) fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, s.indicator (fun (x : ℕ) ↦ r) k
hs : s.Infinite
n : R
n' : ℕ
hn' : n < n' • r
t : Finset ℕ
t_s : (↑t : Set ℕ) ⊆ s
t_card : #t = n'
m : ℕ
hm : m ∈ upperBounds (↑t : Set ℕ)
h : t ⊆ Finset.range (m + 1)
⊢ n' • r ≤ ∑ k ∈ Finset.range (m + 1), (↑t : Set ℕ).indicator (fun (x : ℕ) ↦ r) k
have h₁ : n' • r ≤ ∑ i ∈ t, r
Tactic: rw [sum_indicator_subset (fun _ ↦ r) h, sum_eq_card_nsmul (fun _ _ ↦ rfl), t_card]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.IndicatorCard (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : PartialOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : AddLeftStrictMono R
inst_4 : Archimedean R
r : R
h_1 : 0 < r
s : Set ℕ
h_mono : Monotone.{0, u_1} (β := R) fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, s.indicator (fun (x : ℕ) ↦ r) k
hs : s.Infinite
n : R
n' : ℕ
hn' : n < n' • r
t : Finset ℕ
t_s : (↑t : Set ℕ) ⊆ s
t_card : #t = n'
m : ℕ
hm : m ∈ upperBounds (↑t : Set ℕ)
h : t ⊆ Finset.range (m + 1)
h₁ : n' • r ≤ ∑ i ∈ t, r
⊢ n' • r ≤ ∑ k ∈ Finset.range (m + 1), (↑t : Set ℕ).indicator (fun (x : ℕ) ↦ r) k
have h₂ : n' • r ≤ #t • r
Tactic: rw [sum_indicator_subset (fun _ ↦ r) h, sum_eq_card_nsmul (fun _ _ ↦ rfl), t_card]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.IndicatorCard (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : PartialOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : AddLeftStrictMono R
inst_4 : Archimedean R
r : R
h_1 : 0 < r
s : Set ℕ
h_mono : Monotone.{0, u_1} (β := R) fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, s.indicator (fun (x : ℕ) ↦ r) k
hs : s.Infinite
n : R
n' : ℕ
hn' : n < n' • r
t : Finset ℕ
t_s : (↑t : Set ℕ) ⊆ s
t_card : #t = n'
m : ℕ
hm : m ∈ upperBounds (↑t : Set ℕ)
h : t ⊆ Finset.range (m + 1)
h₁ : n' • r ≤ ∑ i ∈ t, r
h₂ : n' • r ≤ #t • r
⊢ n' • r ≤ ∑ k ∈ Finset.range (m + 1), (↑t : Set ℕ).indicator (fun (x : ℕ) ↦ r) k
have h₃ : n' • r ≤ n' • r
Tactic: rw [sum_indicator_subset (fun _ ↦ r) h, sum_eq_card_nsmul (fun _ _ ↦ rfl), t_card]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.IndicatorCard (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : PartialOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : AddLeftStrictMono R
inst_4 : Archimedean R
r : R
h : 0 < r
s : Set ℕ
⊢ Tendsto.{0, u_1} (β := R) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, s.indicator (fun (x : ℕ) ↦ r) k) atTop atTop →
    s.Infinite
have mpr : s.Finite → ¬Tendsto.{0, u_1} (β := R) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, s.indicator (fun (x : ℕ) ↦ r) k) atTop atTop
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.IndicatorCard (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : PartialOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : AddLeftStrictMono R
inst_4 : Archimedean R
r : R
h : 0 < r
s : Set ℕ
hs : s.Finite
⊢ ¬Tendsto.{0, u_1} (β := R) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, s.indicator (fun (x : ℕ) ↦ r) k) atTop atTop
have mpr : ¬∀ (b : R), ∃ (i : ℕ), ∀ (a : ℕ), i ≤ a → b ≤ Nat.card (↑s : Type) • r
Tactic: rw [tendsto_congr' (sum_indicator_eventually_eq_card r hs), tendsto_atTop_atTop]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.IndicatorCard (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : PartialOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : AddLeftStrictMono R
inst_4 : Archimedean R
r : R
h : 0 < r
s : Set ℕ
hs : s.Finite
⊢ ¬∀ (b : R), ∃ (i : ℕ), ∀ (a : ℕ), i ≤ a → b ≤ Nat.card (↑s : Type) • r
have mpr : ∃ (b : R), ∀ (i : ℕ), ∃ (a : ℕ), i ≤ a ∧ ¬b ≤ Nat.card (↑s : Type) • r
Tactic: push Not
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.IndicatorCard (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : PartialOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : AddLeftStrictMono R
inst_4 : Archimedean R
r : R
h : 0 < r
s : Set ℕ
hs : s.Finite
⊢ ∃ (b : R), ∀ (i : ℕ), ∃ (a : ℕ), i ≤ a ∧ ¬b ≤ Nat.card (↑s : Type) • r
have mpr : ∀ (m : ℕ) (hm : Nat.card (↑s : Type) • r < m • r),
  ∃ (b : R), ∀ (i : ℕ), ∃ (a : ℕ), i ≤ a ∧ ¬b ≤ Nat.card (↑s : Type) • r
Tactic: obtain ⟨m, hm⟩ := exists_lt_nsmul h (Nat.card s • r)
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.IndicatorCard (goal)
Goal:
α : Type u_1
R : Type u_2
inst : AddCommMonoid R
inst_1 : PartialOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : AddLeftStrictMono R
inst_4 : Archimedean R
r : R
h : 0 < r
s : ℕ → Set α
⊢ limsup s atTop =
    {ω : α |
      Tendsto.{0, u_2} (β := R) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, (s k).indicator (fun (x : α) ↦ r) ω) atTop atTop}
have nth_rw : Eq.{u_1 + 1} (α := Set α) {x : α | Set.Infinite (α := ℕ) {n : ℕ | x ∈ s n}}
  {ω : α |
    Tendsto.{0, u_2} (β := R) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, (s k).indicator (fun (x : α) ↦ r) ω) atTop atTop}
Tactic: nth_rw 1 [← Nat.cofinite_eq_atTop, cofinite.limsup_set_eq]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.IndicatorCard (goal)
Goal:
α : Type u_1
R : Type u_2
inst : AddCommMonoid R
inst_1 : PartialOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : AddLeftStrictMono R
inst_4 : Archimedean R
r : R
h : 0 < r
s : ℕ → Set α
⊢ Eq.{u_1 + 1} (α := Set α) {x : α | Set.Infinite (α := ℕ) {n : ℕ | x ∈ s n}}
    {ω : α |
      Tendsto.{0, u_2} (β := R) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, (s k).indicator (fun (x : α) ↦ r) ω) atTop atTop}
have h₁ : ∀ (ω : α),
  Membership.mem (γ := Set α) {x : α | Set.Infinite (α := ℕ) {n : ℕ | x ∈ s n}} ω ↔
    Membership.mem (γ := Set α)
      {ω : α |
        Tendsto.{0, u_2} (β := R) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, (s k).indicator (fun (x : α) ↦ r) ω) atTop atTop}
      ω
Tactic: ext ω
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.IndicatorCard (goal)
Goal:
α : Type u_1
R : Type u_2
inst : AddCommMonoid R
inst_1 : PartialOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : AddLeftStrictMono R
inst_4 : Archimedean R
r : R
h : 0 < r
s : ℕ → Set α
ω : α
⊢ Membership.mem (γ := Set α) {x : α | Set.Infinite (α := ℕ) {n : ℕ | x ∈ s n}} ω ↔
    Membership.mem (γ := Set α)
      {ω : α |
        Tendsto.{0, u_2} (β := R) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, (s k).indicator (fun (x : α) ↦ r) ω) atTop atTop}
      ω
have h₁ : Tendsto.{0, u_2} (β := R) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, indicator {n : ℕ | ω ∈ s n} (fun (x : ℕ) ↦ r) k) atTop
    atTop =
  Tendsto.{0, u_2} (β := R) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, (s k).indicator (fun (x : α) ↦ r) ω) atTop atTop
Tactic: rw [mem_setOf_eq, mem_setOf_eq, infinite_iff_tendsto_sum_indicator_atTop h, iff_eq_eq]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Submonoid (goal)
Goal:
M : Type u_1
S : Type u_2
inst : SetLike S M
inst_1 : CommMonoid M
inst_2 : PartialOrder M
inst_3 : SubmonoidClass S M
inst_4 : MulArchimedean M
H : S
⊢ MulArchimedean.{u_1} ↥H
have arch : ∀ (x : ↥H) {y : ↥H}, 1 < y → ∃ (n : ℕ), x ≤ y ^ n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Submonoid (goal)
Goal:
M : Type u_1
S : Type u_2
inst : SetLike S M
inst_1 : CommMonoid M
inst_2 : PartialOrder M
inst_3 : SubmonoidClass S M
inst_4 : MulArchimedean M
H : S
x y : ↥H
⊢ 1 < y → ∃ (n : ℕ), x ≤ y ^ n
have arch : 1 < (↑y : M) → ∃ (n : ℕ), x ≤ y ^ n
Tactic: simp only [← Subtype.coe_lt_coe, OneMemClass.coe_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Expect (goal)
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 ≤ HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0) a
have rw : ∑ i ∈ s, (fun (i : ι) ↦ f i) i ≤ #s • a
Tactic: rw [Nat.cast_smul_eq_nsmul]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Expect (goal)
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
⊢ HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0) a ≤ ∑ i ∈ s, (fun (i : ι) ↦ f i) i
have rw : #s • a ≤ ∑ i ∈ s, (fun (i : ι) ↦ f i) i
Tactic: rw [Nat.cast_smul_eq_nsmul]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Expect (goal)
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)
⊢ m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i)
have simp : HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ (m (∑ x ∈ s, f x)) ≤
  HSMul.hSMul (α := ℚ≥0) (β := N) (↑(#s) : ℚ≥0)⁻¹ (∑ x ∈ s, m (f x))
Tactic: simp only [expect, h_div _ _ (sum_induction_nonempty _ _ hp_add hs_nonempty hs)]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Expect (goal)
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)
⊢ m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i)
have inl : ∀ (hs : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → p (f i)), m (𝔼 i ∈ ∅, f i) ≤ 𝔼 i ∈ ∅, m (f i)
Tactic: obtain rfl | hs_nonempty := s.eq_empty_or_nonempty
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Expect (goal)
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)
⊢ m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i)
have inr : ∀ (hs_nonempty : s.Nonempty), m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i)
Tactic: obtain rfl | hs_nonempty := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Expect (goal)
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
⊢ LT.lt (α := ℚ≥0) 0 (↑(#s) : ℚ≥0)⁻¹
have obtain : ∀ (i : ι) (hi : i ∈ s), LT.lt (α := ℚ≥0) 0 (↑(#s) : ℚ≥0)⁻¹
Tactic: obtain ⟨i, hi, -⟩ := hfg'
Cleared hypotheses: hfg'
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Expect (hypothesis)
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
⊢ LT.lt (α := ℚ≥0) 0 (↑(#s) : ℚ≥0)⁻¹
have this : s.Nonempty
Tactic: have : s.Nonempty := ⟨i, hi⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Expect (goal)
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
⊢ 𝔼 i ∈ s, f i < a
have rw : LT.lt.{u_2} (α := α) (𝔼 i ∈ s, f i) (𝔼 _i ∈ s, a)
Tactic: rw [← expect_const (hlt.imp (fun _ => And.left)) a]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Expect (goal)
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
⊢ a < 𝔼 i ∈ s, f i
have rw : LT.lt.{u_2} (α := α) (𝔼 _i ∈ s, a) (𝔼 i ∈ s, f i)
Tactic: rw [← expect_const (hlt.imp (fun _ => And.left)) a]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Expect (goal)
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)
⊢ ∃ x ∈ s, g x < f x
have contrapose! : ∀ (h : ∀ (x : ι) (_ : x ∈ s), f x ≤ g x), LE.le.{u_2} (α := α) (𝔼 i ∈ s, f i) (𝔼 i ∈ s, g i)
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Expect (goal)
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
⊢ ∃ x ∈ s, a < f x
have contrapose! : ∀ (h : ∀ (x : ι) (_ : x ∈ s), f x ≤ a), 𝔼 i ∈ s, f i ≤ a
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Expect (goal)
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
⊢ ∃ x ∈ s, f x < a
have contrapose! : ∀ (h : ∀ (x : ι) (_ : x ∈ s), a ≤ f x), a ≤ 𝔼 i ∈ s, f i
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Expect (goal)
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)
⊢ ∃ x ∈ s, g x ≤ f x
have obtain : ∀ (w : ι) (hx : w ∈ s), ∃ x ∈ s, g x ≤ f x
Tactic: obtain ⟨_, hx⟩ := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Expect (goal)
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
⊢ ∃ x ∈ s, g x ≤ f x
have contrapose! : ∀ (h : ∀ (x : ι) (_ : x ∈ s), f x < g x), LT.lt.{u_2} (α := α) (𝔼 i ∈ s, f i) (𝔼 i ∈ s, g i)
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Expect (goal)
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) (β := ℕ) (𝔼 i ∈ s, f i * g i) 2 ≤
    HMul.hMul (α := R) (𝔼 i ∈ s, HPow.hPow (β := ℕ) (f i) 2) (𝔼 i ∈ s, HPow.hPow (β := ℕ) (g i) 2)
have 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)
Tactic: simp only [expect, smul_pow, inv_pow, smul_mul_smul_comm, ← sq]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Expect (goal)
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 (α := ℚ≥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)
have 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)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Expect (goal)
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
⊢ Eq.{u_2 + 1} (α := α) (𝔼 i : ι, f i) 0 ↔ f = 0
have rw : (∀ (i : ι), Membership.mem (γ := Finset ι) univ i → f i = 0) ↔ f = 0
Tactic: rw [Finset.expect_eq_zero_iff_of_nonneg (by aesop)]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Expect (goal)
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
⊢ Eq.{u_2 + 1} (α := α) (𝔼 i : ι, f i) 0 ↔ f = 0
have rw : (∀ (i : ι), Membership.mem (γ := Finset ι) univ i → f i = 0) ↔ f = 0
Tactic: rw [Finset.expect_eq_zero_iff_of_nonpos (by aesop)]
-- 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)
⊢ f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)
have refine_1 : Ne.{u_4 + 1} (α := Multiset M) (Multiset.map (fun (i : ι) ↦ g i) s.val) ∅
Tactic: refine le_trans
    (Multiset.le_prod_nonempty_of_submultiplicative_on_pred f p h_mul hp_mul _ ?_ ?_) ?_