-- 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 ℕ
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 ∈ Finset.range (m + 1)

Tactic:
rw [Finset.mem_range]

Result:
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

Proof state:
case mpr
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:
intro hs

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.Infinite
⊢ ¬Tendsto (fun n => ∑ k ∈ Finset.range n, s.indicator (fun x => r) k) atTop atTop

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
⊢ t ⊆ Finset.range (m + 1)

Tactic:
intro i i_t

Result:
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 ∈ Finset.range (m + 1)

Proof state:
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

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) _)

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 → Tendsto (fun n => ∑ k ∈ Finset.range n, s.indicator (fun x => r) k) atTop atTop

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.Infinite
⊢ ¬Tendsto (fun n => ∑ k ∈ Finset.range n, s.indicator (fun x => r) k) atTop atTop

Tactic:
rw [not_infinite] at hs

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
⊢ ¬Tendsto (fun n => ∑ k ∈ Finset.range n, s.indicator (fun x => r) k) atTop atTop

Proof state:
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

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

Result:
no goals

Proof state:
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

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

Result:
no goals

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
h : t ⊆ Finset.range (m + 1)
⊢ n' • r = ∑ i ∈ Finset.range (m + 1), (↑t).indicator (fun x => r) i

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

Result:
no goals

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
⊢ ¬Tendsto (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]

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 : R), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ Nat.card ↑s • r

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 = ∑ i ∈ Finset.range (m + 1), (↑t).indicator (fun x => r) i

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)

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
h : t ⊆ Finset.range (m + 1)
⊢ 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 ℕ
⊢ Tendsto (fun n => ∑ k ∈ Finset.range n, s.indicator (fun x => r) k) atTop atTop → s.Infinite

Tactic:
contrapose

Result:
case mpr
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

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
⊢ ∃ a, n ≤ ∑ k ∈ Finset.range a, s.indicator (fun x => r) k

Tactic:
refine ⟨m + 1, hn'.le.trans ?_⟩

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 ≤ ∑ k ∈ Finset.range (m + 1), s.indicator (fun x => r) k