awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard
Goal:
α : Type u_1
inst : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset (s := s), s.indicator (fun (x : ℕ) ↦ a) x = a
obtain :
  ∀ (m : ℕ) (hm : m ∈ upperBounds s),
    ∃ (a_1 : ℕ),
      ∀ b ≥ a_1,
        Eq.{u_1 + 1} (α := α) (∑ k ∈ Finset.range b, s.indicator (fun (x : ℕ) ↦ a) k)
          (∑ a_3 ∈ hs.toFinset (s := s), s.indicator (fun (x : ℕ) ↦ a) a_3)
⊢ ∃ (a_1 : ℕ),
    ∀ b ≥ a_1,
      Eq.{u_1 + 1} (α := α) (∑ k ∈ Finset.range b, s.indicator (fun (x : ℕ) ↦ a) k)
        (∑ a_3 ∈ hs.toFinset (s := s), s.indicator (fun (x : ℕ) ↦ a) a_3)

Tactic:
obtain ⟨m, hm⟩ := hs.bddAbove

Premises used: Set.Finite.bddAbove
-- Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard
Goal:
α : Type u_1
inst : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset (s := s), s.indicator (fun (x : ℕ) ↦ a) x = a
m : ℕ
hm : m ∈ upperBounds s
⊢ ∃ (a_1 : ℕ),
    ∀ b ≥ a_1,
      Eq.{u_1 + 1} (α := α) (∑ k ∈ Finset.range b, s.indicator (fun (x : ℕ) ↦ a) k)
        (∑ a_3 ∈ hs.toFinset (s := s), s.indicator (fun (x : ℕ) ↦ a) a_3)

Tactic:
⟨m + 1, fun n n_m ↦ (sum_subset ?_ ?_).symm⟩

Premises used: HAdd.hAdd, Finset.sum_subset, Exists.intro, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard
Goal:
α : Type u_1
inst : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset (s := s), s.indicator (fun (x : ℕ) ↦ a) x = a
m : ℕ
hm : m ∈ upperBounds s
refine_1 : ∀ (n : ℕ) (n_m : n ≥ m + 1), hs.toFinset (s := s) ⊆ Finset.range n
refine_2 :
  ∀ (n : ℕ) (n_m : n ≥ m + 1),
    ∀ x ∈ Finset.range n, x ∉ hs.toFinset (s := s) → Eq.{u_1 + 1} (α := α) (s.indicator (fun (x : ℕ) ↦ a) x) 0
⊢ ∃ (a_1 : ℕ),
    ∀ b ≥ a_1,
      Eq.{u_1 + 1} (α := α) (∑ k ∈ Finset.range b, s.indicator (fun (x : ℕ) ↦ a) k)
        (∑ a_3 ∈ hs.toFinset (s := s), s.indicator (fun (x : ℕ) ↦ a) a_3)

Tactic:
refine ⟨m + 1, fun n n_m ↦ (sum_subset ?_ ?_).symm⟩
-- Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard
Goal:
α : Type u_1
inst : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset (s := s), s.indicator (fun (x : ℕ) ↦ a) x = a
m : ℕ
hm : m ∈ upperBounds s
n : ℕ
n_m : n ≥ m + 1
x : ℕ
refine_1 : x ∈ s → x ∈ Finset.range n
⊢ x ∈ hs.toFinset (s := s) → x ∈ Finset.range n

Tactic:
rw [hs.mem_toFinset]

Premises used: Set.Finite.mem_toFinset
-- Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard
Goal:
α : Type u_1
inst : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset (s := s), s.indicator (fun (x : ℕ) ↦ a) x = a
m : ℕ
hm : m ∈ upperBounds s
n : ℕ
n_m : n ≥ m + 1
x : ℕ
refine_2 : x ∈ Finset.range n → x ∉ s → Eq.{u_1 + 1} (α := α) (s.indicator (fun (x : ℕ) ↦ a) x) 0
⊢ x ∈ Finset.range n → x ∉ hs.toFinset (s := s) → Eq.{u_1 + 1} (α := α) (s.indicator (fun (x : ℕ) ↦ a) x) 0

Tactic:
rw [hs.mem_toFinset]

Premises used: Set.Finite.mem_toFinset
-- Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard
Goal:
α : Type u_1
inst : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset (s := s), s.indicator (fun (x : ℕ) ↦ a) x = a
m : ℕ
hm : m ∈ upperBounds s
n : ℕ
n_m : n ≥ m + 1
x : ℕ
refine_1 : x ∈ s → x < n
⊢ x ∈ s → x ∈ Finset.range n

Tactic:
rw [Finset.mem_range]

Premises used: Finset.mem_range
-- Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard
Goal:
α : Type u_1
inst : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset (s := s), s.indicator (fun (x : ℕ) ↦ a) x = a
m : ℕ
hm : m ∈ upperBounds s
n : ℕ
n_m : n ≥ m + 1
x : ℕ
⊢ x ∈ s → x < n

Tactic:
fun x_s ↦ ((mem_upperBounds.1 hm) x x_s).trans_lt (Nat.lt_of_succ_le n_m)

Premises used: Nat.lt_of_succ_le, Iff.mp, LE.le.trans_lt, mem_upperBounds
-- Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard
Goal:
α : Type u_1
inst : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset (s := s), s.indicator (fun (x : ℕ) ↦ a) x = a
m : ℕ
hm : m ∈ upperBounds s
n : ℕ
n_m : n ≥ m + 1
x : ℕ
⊢ x ∈ s → x < n

Tactic:
exact fun x_s ↦ ((mem_upperBounds.1 hm) x x_s).trans_lt (Nat.lt_of_succ_le n_m)

Premises used: Nat.lt_of_succ_le, Iff.mp, LE.le.trans_lt, mem_upperBounds
-- Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard
Goal:
α : Type u_1
inst : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset (s := s), s.indicator (fun (x : ℕ) ↦ a) x = a
m : ℕ
hm : m ∈ upperBounds s
n : ℕ
n_m : n ≥ m + 1
x : ℕ
⊢ x ∈ Finset.range n → x ∉ s → Eq.{u_1 + 1} (α := α) (s.indicator (fun (x : ℕ) ↦ a) x) 0

Tactic:
fun _ x_s ↦ indicator_of_notMem x_s (fun _ ↦ a)

Premises used: Set.indicator_of_notMem
-- Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard
Goal:
α : Type u_1
inst : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset (s := s), s.indicator (fun (x : ℕ) ↦ a) x = a
m : ℕ
hm : m ∈ upperBounds s
n : ℕ
n_m : n ≥ m + 1
x : ℕ
⊢ x ∈ Finset.range n → x ∉ s → Eq.{u_1 + 1} (α := α) (s.indicator (fun (x : ℕ) ↦ a) x) 0

Tactic:
exact fun _ x_s ↦ indicator_of_notMem x_s (fun _ ↦ a)

Premises used: Set.indicator_of_notMem
-- Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard
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 ℕ
mp :
  s.Infinite →
    Tendsto.{0, u_1} (β := R) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, s.indicator (fun (x : ℕ) ↦ r) k) atTop atTop
mpr :
  Tendsto.{0, u_1} (β := R) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, s.indicator (fun (x : ℕ) ↦ r) k) atTop atTop →
    s.Infinite
⊢ s.Infinite ↔
    Tendsto.{0, u_1} (β := R) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, s.indicator (fun (x : ℕ) ↦ r) k) atTop atTop

Tactic:
constructor
-- Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard
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 ℕ
⊢ Monotone.{0, u_1} (β := R) fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, s.indicator (fun (x : ℕ) ↦ r) k

Tactic:
(sum_mono_set_of_nonneg ?_).comp range_mono

Premises used: Multiset.sum, Multiset.foldr, Monotone.comp, Finset.range_mono, Finset.sum_mono_set_of_nonneg, Finset.sum
-- Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard
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 ℕ
refine : ∀ (x : ℕ), LE.le.{u_1} (α := R) 0 (s.indicator (fun (x : ℕ) ↦ r) x)
⊢ Monotone.{0, u_1} (β := R) fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, s.indicator (fun (x : ℕ) ↦ r) k

Tactic:
refine (sum_mono_set_of_nonneg ?_).comp range_mono

Premises used: Monotone.comp, Finset.range_mono, Finset.sum_mono_set_of_nonneg
-- Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard
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 ℕ
⊢ ∀ (x : ℕ), LE.le.{u_1} (α := R) 0 (s.indicator (fun (x : ℕ) ↦ r) x)

Tactic:
(fun _ ↦ indicator_nonneg (fun _ _ ↦ h.le) _)

Premises used: LT.lt.le, Set.indicator_nonneg
-- Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard
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 ℕ
⊢ ∀ (x : ℕ), LE.le.{u_1} (α := R) 0 (s.indicator (fun (x : ℕ) ↦ r) x)

Tactic:
exact (fun _ ↦ indicator_nonneg (fun _ _ ↦ h.le) _)

Premises used: LT.lt.le, Set.indicator_nonneg
-- Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard
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 ℕ
⊢ 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) _)
-- Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard
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
mp : s.Infinite → ∀ (b : R), ∃ (a : ℕ), b ≤ ∑ k ∈ Finset.range a, 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

Tactic:
rw [h_mono.tendsto_atTop_atTop_iff]

Premises used: Monotone.tendsto_atTop_atTop_iff
-- Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard
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
mp : ∀ (n' : ℕ) (hn' : n < n' • r), ∃ (a : ℕ), n ≤ ∑ k ∈ Finset.range a, s.indicator (fun (x : ℕ) ↦ r) k
⊢ ∃ (a : ℕ), n ≤ ∑ k ∈ Finset.range a, s.indicator (fun (x : ℕ) ↦ r) k

Tactic:
obtain ⟨n', hn'⟩ := exists_lt_nsmul h n

Premises used: exists_lt_nsmul
-- Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard
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
mp :
  ∀ (t : Finset ℕ) (t_s : (↑t : Set ℕ) ⊆ s) (t_card : #t = n'),
    ∃ (a : ℕ), n ≤ ∑ k ∈ Finset.range a, s.indicator (fun (x : ℕ) ↦ r) k
⊢ ∃ (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'

Premises used: Set.Infinite.exists_subset_card_eq
-- Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard
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'
mp : ∀ (m : ℕ) (hm : m ∈ upperBounds (↑t : Set ℕ)), ∃ (a : ℕ), n ≤ ∑ k ∈ Finset.range a, s.indicator (fun (x : ℕ) ↦ r) k
⊢ ∃ (a : ℕ), n ≤ ∑ k ∈ Finset.range a, s.indicator (fun (x : ℕ) ↦ r) k

Tactic:
obtain ⟨m, hm⟩ := t.bddAbove

Premises used: Finset.bddAbove
-- Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard
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 ℕ)
h₁ : n ≤ ∑ k ∈ Finset.range (m + 1), s.indicator (fun (x : ℕ) ↦ r) k
⊢ ∃ (a : ℕ), n ≤ ∑ k ∈ Finset.range a, s.indicator (fun (x : ℕ) ↦ r) k

Tactic:
use m + 1
-- Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard
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 ℕ)
h₁ : n' • r ≤ ∑ k ∈ Finset.range (m + 1), (↑t : Set ℕ).indicator (fun (x : ℕ) ↦ r) k
⊢ n ≤ ∑ k ∈ Finset.range (m + 1), s.indicator (fun (x : ℕ) ↦ r) k

Tactic:
grw [hn', ← t_s]
-- Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard
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
rw : i < m + 1
⊢ i ∈ Finset.range (m + 1)

Tactic:
rw [Finset.mem_range]

Premises used: Finset.mem_range
-- Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard
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 < m + 1

Tactic:
(hm i_t).trans_lt (lt_add_one m)

Premises used: lt_add_one, LE.le.trans_lt
-- Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard
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 < m + 1

Tactic:
exact (hm i_t).trans_lt (lt_add_one m)

Premises used: lt_add_one, LE.le.trans_lt
-- Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard
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 ℕ)
⊢ 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)
-- Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard
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
h₃ h₄ : n' • r ≤ n' • r
⊢ n' • r ≤ ∑ k ∈ Finset.range (m + 1), (↑t : Set ℕ).indicator (fun (x : ℕ) ↦ r) k

Tactic:
rw [sum_indicator_subset (fun _ ↦ r) h, sum_eq_card_nsmul (fun _ _ ↦ rfl), t_card]

Premises used: Finset.sum_indicator_subset, Finset.sum_eq_card_nsmul, rfl
-- Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard
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 ℕ
mpr :
  s.Finite →
    ¬Tendsto.{0, u_1} (β := R) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, s.indicator (fun (x : ℕ) ↦ r) k) atTop atTop
⊢ Tendsto.{0, u_1} (β := R) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, s.indicator (fun (x : ℕ) ↦ r) k) atTop atTop →
    s.Infinite

Tactic:
contrapose!
-- Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard
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
mpr : ¬∀ (b : R), ∃ (i : ℕ), ∀ (a : ℕ), i ≤ a → b ≤ Nat.card (↑s : Type) • r
⊢ ¬Tendsto.{0, u_1} (β := R) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, s.indicator (fun (x : ℕ) ↦ r) k) atTop atTop

Tactic:
rw [tendsto_congr' (sum_indicator_eventually_eq_card r hs), tendsto_atTop_atTop]

Premises used: Set.sum_indicator_eventually_eq_card, Filter.tendsto_atTop_atTop, Filter.tendsto_congr'
-- Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard
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
mpr : ∃ (b : R), ∀ (i : ℕ), ∃ (a : ℕ), i ≤ a ∧ ¬b ≤ Nat.card (↑s : Type) • r
⊢ ¬∀ (b : R), ∃ (i : ℕ), ∀ (a : ℕ), i ≤ a → b ≤ Nat.card (↑s : Type) • r

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard
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
mpr :
  ∀ (m : ℕ) (hm : Nat.card (↑s : Type) • r < m • r),
    ∃ (b : R), ∀ (i : ℕ), ∃ (a : ℕ), i ≤ a ∧ ¬b ≤ Nat.card (↑s : Type) • 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)

Premises used: exists_lt_nsmul, Set.Elem, Nat.card, HSMul.hSMul
-- Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard
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
m : ℕ
hm : Nat.card (↑s : Type) • r < m • r
⊢ ∃ (b : R), ∀ (i : ℕ), ∃ (a : ℕ), i ≤ a ∧ ¬b ≤ Nat.card (↑s : Type) • r

Tactic:
⟨m • r, fun n ↦ ⟨n, le_refl n, not_le_of_gt hm⟩⟩

Premises used: le_refl, And.intro, Exists.intro, HSMul.hSMul, not_le_of_gt
-- Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard
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
m : ℕ
hm : Nat.card (↑s : Type) • r < m • r
⊢ ∃ (b : R), ∀ (i : ℕ), ∃ (a : ℕ), i ≤ a ∧ ¬b ≤ Nat.card (↑s : Type) • r

Tactic:
exact ⟨m • r, fun n ↦ ⟨n, le_refl n, not_le_of_gt hm⟩⟩
-- Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard
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 α
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}
⊢ limsup s atTop =
    {ω : α |
      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]

Premises used: Filter.cofinite.limsup_set_eq, Nat.cofinite_eq_atTop
-- Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard
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 α
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}
        ω
⊢ 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:
ext ω
-- Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard
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 α
ω : α
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
⊢ 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:
rw [mem_setOf_eq, mem_setOf_eq, infinite_iff_tendsto_sum_indicator_atTop h, iff_eq_eq]

Premises used: Set.mem_setOf_eq, Set.infinite_iff_tendsto_sum_indicator_atTop, iff_eq_eq
-- Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard
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 α
ω : α
⊢ 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:
congr
-- Module: Mathlib.Algebra.Order.Archimedean.Submonoid
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
arch : ∀ (x : ↥H) {y : ↥H}, 1 < y → ∃ (n : ℕ), x ≤ y ^ n
⊢ MulArchimedean.{u_1} ↥H

Tactic:
constructor
-- Module: Mathlib.Algebra.Order.Archimedean.Submonoid
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
arch : 1 < (↑y : M) → ∃ (n : ℕ), x ≤ y ^ n
⊢ 1 < y → ∃ (n : ℕ), x ≤ y ^ n

Tactic:
simp only [← Subtype.coe_lt_coe, OneMemClass.coe_one]

Premises used: OneMemClass.coe_one, Subtype.coe_lt_coe
-- Module: Mathlib.Algebra.Order.Archimedean.Submonoid
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 : M) → ∃ (n : ℕ), x ≤ y ^ n

Tactic:
MulArchimedean.arch x.val

Premises used: Subtype.val, MulArchimedean.arch
-- Module: Mathlib.Algebra.Order.Archimedean.Submonoid
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 : M) → ∃ (n : ℕ), x ≤ y ^ n

Tactic:
exact MulArchimedean.arch x.val

Premises used: Subtype.val, MulArchimedean.arch
-- 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 : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
⊢ Eq.{u_2 + 1} (α := α) (𝔼 i ∈ s, f i) 0 ↔ ∀ i ∈ s, f i = 0

Tactic:
simp +contextual [expect, sum_eq_zero_iff_of_nonneg hf]

Premises used: Finset.expect, Finset.sum_eq_zero_iff_of_nonneg
-- 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 : ι → α
hf : ∀ i ∈ s, f i ≤ 0
⊢ Eq.{u_2 + 1} (α := α) (𝔼 i ∈ s, f i) 0 ↔ ∀ i ∈ s, f i = 0

Tactic:
simp +contextual [expect, sum_eq_zero_iff_of_nonpos hf]

Premises used: Finset.expect, Finset.sum_eq_zero_iff_of_nonpos
-- 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 g : ι → α
inst_4 : PosSMulMono ℚ≥0 α
hfg : ∀ i ∈ s, f i ≤ g i
⊢ LE.le (α := ℚ≥0) 0 (↑(#s) : ℚ≥0)⁻¹

Tactic:
positivity