-- Mathlib/Algebra/Order/Archimedean/IndicatorCard.lean
lemma infinite_iff_tendsto_sum_indicator_atTop {R : Type*} [OrderedAddCommMonoid R]
    [AddLeftStrictMono R] [Archimedean R] {r : R} (h : 0 < r) {s : Set ℕ} :
    s.Infinite ↔ atTop.Tendsto (fun n ↦ ∑ k ∈ Finset.range n, s.indicator (fun _ ↦ r) k) atTop

Proof state:
R : Type u_1
inst✝² : OrderedAddCommMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
⊢ s.Infinite ↔ Tendsto (fun n => ∑ k ∈ Finset.range n, s.indicator (fun x => r) k) atTop atTop

Tactic:
constructor

Result:
case mp
R : Type u_1
inst✝² : OrderedAddCommMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
⊢ s.Infinite → Tendsto (fun n => ∑ k ∈ Finset.range n, s.indicator (fun x => r) k) atTop atTop

case mpr
R : Type u_1
inst✝² : OrderedAddCommMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
⊢ Tendsto (fun n => ∑ k ∈ Finset.range n, s.indicator (fun x => r) k) atTop atTop → s.Infinite

Proof state:
case mp.intro.intro.intro.intro
R : Type u_1
inst✝² : OrderedAddCommMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
h_mono : Monotone 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 ⊆ s
t_card : #t = n'
m : ℕ
hm : m ∈ upperBounds ↑t
⊢ n' • r ≤ ∑ k ∈ Finset.range (m + 1), s.indicator (fun x => r) k

Tactic:
apply (sum_le_sum fun i _ ↦ (indicator_le_indicator_of_subset t_s (fun _ ↦ h.le)) i).trans_eq'

Result:
case mp.intro.intro.intro.intro
R : Type u_1
inst✝² : OrderedAddCommMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
h_mono : Monotone 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 ⊆ s
t_card : #t = n'
m : ℕ
hm : m ∈ upperBounds ↑t
⊢ n' • r = ∑ i ∈ Finset.range (m + 1), (↑t).indicator (fun x => r) i

Proof state:
case mpr
R : Type u_1
inst✝² : OrderedAddCommMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
hs : s.Finite
⊢ ∃ b, ∀ (i : ℕ), ∃ a, i ≤ a ∧ ¬b ≤ Nat.card ↑s • r

Tactic:
obtain ⟨m, hm⟩ := exists_lt_nsmul h (Nat.card s • r)

Result:
case mpr.intro
R : Type u_1
inst✝² : OrderedAddCommMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
hs : s.Finite
m : ℕ
hm : Nat.card ↑s • r < m • r
⊢ ∃ b, ∀ (i : ℕ), ∃ a, i ≤ a ∧ ¬b ≤ Nat.card ↑s • r

Proof state:
case mp
R : Type u_1
inst✝² : OrderedAddCommMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
h_mono : Monotone fun n => ∑ k ∈ Finset.range n, s.indicator (fun x => r) k
⊢ s.Infinite → Tendsto (fun n => ∑ k ∈ Finset.range n, s.indicator (fun x => r) k) atTop atTop

Tactic:
rw [h_mono.tendsto_atTop_atTop_iff]

Result:
case mp
R : Type u_1
inst✝² : OrderedAddCommMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
h_mono : Monotone fun n => ∑ k ∈ Finset.range n, s.indicator (fun x => r) k
⊢ s.Infinite → ∀ (b : R), ∃ a, b ≤ ∑ k ∈ Finset.range a, s.indicator (fun x => r) k

Proof state:
case mp
R : Type u_1
inst✝² : OrderedAddCommMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
h_mono : Monotone 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

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

Result:
case mp.intro
R : Type u_1
inst✝² : OrderedAddCommMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
h_mono : Monotone 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

Proof state:
case mp
R : Type u_1
inst✝² : OrderedAddCommMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
h_mono : Monotone fun n => ∑ k ∈ Finset.range n, s.indicator (fun x => r) k
⊢ s.Infinite → ∀ (b : R), ∃ a, b ≤ ∑ k ∈ Finset.range a, s.indicator (fun x => r) k

Tactic:
intro hs n

Result:
case mp
R : Type u_1
inst✝² : OrderedAddCommMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
h_mono : Monotone 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

Proof state:
case mpr
R : Type u_1
inst✝² : OrderedAddCommMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
hs : s.Finite
⊢ ¬∀ (b : R), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ Nat.card ↑s • r

Tactic:
push_neg

Result:
case mpr
R : Type u_1
inst✝² : OrderedAddCommMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
hs : s.Finite
⊢ ∃ b, ∀ (i : ℕ), ∃ a, i ≤ a ∧ ¬b ≤ Nat.card ↑s • r

Proof state:
case mp.intro.intro.intro
R : Type u_1
inst✝² : OrderedAddCommMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
h_mono : Monotone 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 ⊆ s
t_card : #t = n'
⊢ ∃ a, n ≤ ∑ k ∈ Finset.range a, s.indicator (fun x => r) k

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

Result:
case mp.intro.intro.intro.intro
R : Type u_1
inst✝² : OrderedAddCommMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
h_mono : Monotone 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 ⊆ s
t_card : #t = n'
m : ℕ
hm : m ∈ upperBounds ↑t
⊢ ∃ a, n ≤ ∑ k ∈ Finset.range a, s.indicator (fun x => r) k

Proof state:
R : Type u_1
inst✝² : OrderedAddCommMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
h_mono : Monotone 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 ⊆ s
t_card : #t = n'
m : ℕ
hm : m ∈ upperBounds ↑t
i : ℕ
i_t : i ∈ t
⊢ i < m + 1

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

Result:
no goals

Proof state:
R : Type u_1
inst✝² : OrderedAddCommMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
⊢ Monotone fun n => ∑ k ∈ Finset.range n, s.indicator (fun x => r) k

Tactic:
refine (sum_mono_set_of_nonneg ?_).comp range_mono

Result:
R : Type u_1
inst✝² : OrderedAddCommMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
⊢ ∀ (x : ℕ), 0 ≤ s.indicator (fun x => r) x

Proof state:
case mp.intro
R : Type u_1
inst✝² : OrderedAddCommMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
h_mono : Monotone 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

Tactic:
obtain ⟨t, t_s, t_card⟩ := hs.exists_subset_card_eq n'

Result:
case mp.intro.intro.intro
R : Type u_1
inst✝² : OrderedAddCommMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
h_mono : Monotone 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 ⊆ s
t_card : #t = n'
⊢ ∃ a, n ≤ ∑ k ∈ Finset.range a, s.indicator (fun x => r) k