-- Mathlib/Algebra/Order/Archimedean/IndicatorCard.lean
lemma sum_indicator_eventually_eq_card {α : Type*} [AddCommMonoid α] (a : α) {s : Set ℕ}
    (hs : s.Finite) :
    ∀ᶠ n in atTop, ∑ k ∈ Finset.range n, s.indicator (fun _ ↦ a) k = (Nat.card s) • a

Proof state:
α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset, s.indicator (fun x => a) x = a
⊢ ∀ᶠ (n : ℕ) in atTop, ∑ k ∈ Finset.range n, s.indicator (fun x => a) k = Nat.card ↑s • a

Tactic:
rw [Nat.card_eq_card_finite_toFinset hs, ← sum_eq_card_nsmul key, eventually_atTop]

Result:
α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset, s.indicator (fun x => a) x = a
⊢ ∃ a_1, ∀ b ≥ a_1, ∑ k ∈ Finset.range b, s.indicator (fun x => a) k = ∑ a_3 ∈ hs.toFinset, s.indicator (fun x => a) a_3

Proof state:
α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
⊢ ∀ x ∈ hs.toFinset, s.indicator (fun x => a) x = a

Tactic:
intro x hx

Result:
α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
x : ℕ
hx : x ∈ hs.toFinset
⊢ s.indicator (fun x => a) x = a

Proof state:
case intro.refine_1
α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset, 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)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
⊢ ∀ᶠ (n : ℕ) in atTop, ∑ k ∈ Finset.range n, s.indicator (fun x => a) k = Nat.card ↑s • a

Tactic:
have key : ∀ x ∈ hs.toFinset, s.indicator (fun _ ↦ a) x = a := by
  intro x hx
  rw [indicator_of_mem (hs.mem_toFinset.1 hx) (fun _ ↦ a)]

Result:
α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset, s.indicator (fun x => a) x = a
⊢ ∀ᶠ (n : ℕ) in atTop, ∑ k ∈ Finset.range n, s.indicator (fun x => a) k = Nat.card ↑s • a

Proof state:
case intro.refine_2
α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset, 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 → s.indicator (fun x => a) x = 0

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

Result:
no goals

Proof state:
case intro
α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset, s.indicator (fun x => a) x = a
m : ℕ
hm : m ∈ upperBounds s
⊢ ∃ a_1, ∀ b ≥ a_1, ∑ k ∈ Finset.range b, s.indicator (fun x => a) k = ∑ a_3 ∈ hs.toFinset, s.indicator (fun x => a) a_3

Tactic:
refine ⟨m + 1, fun n n_m ↦ (sum_subset ?_ ?_).symm⟩ <;> intro x <;> rw [hs.mem_toFinset]

Result:
case intro.refine_1
α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset, s.indicator (fun x => a) x = a
m : ℕ
hm : m ∈ upperBounds s
n : ℕ
n_m : n ≥ m + 1
x : ℕ
⊢ x ∈ s → x ∈ Finset.range n

case intro.refine_2
α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset, 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 → s.indicator (fun x => a) x = 0

Proof state:
α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset, s.indicator (fun x => a) x = a
⊢ ∃ a_1, ∀ b ≥ a_1, ∑ k ∈ Finset.range b, s.indicator (fun x => a) k = ∑ a_3 ∈ hs.toFinset, s.indicator (fun x => a) a_3

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

Result:
case intro
α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset, s.indicator (fun x => a) x = a
m : ℕ
hm : m ∈ upperBounds s
⊢ ∃ a_1, ∀ b ≥ a_1, ∑ k ∈ Finset.range b, s.indicator (fun x => a) k = ∑ a_3 ∈ hs.toFinset, s.indicator (fun x => a) a_3

Proof state:
case intro.refine_1
α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset, s.indicator (fun x => a) x = a
m : ℕ
hm : m ∈ upperBounds s
n : ℕ
n_m : n ≥ m + 1
x : ℕ
⊢ x ∈ s → x ∈ Finset.range n

Tactic:
rw [Finset.mem_range]

Result:
case intro.refine_1
α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset, s.indicator (fun x => a) x = a
m : ℕ
hm : m ∈ upperBounds s
n : ℕ
n_m : n ≥ m + 1
x : ℕ
⊢ x ∈ s → x < n

Proof state:
α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
x : ℕ
hx : x ∈ hs.toFinset
⊢ s.indicator (fun x => a) x = a

Tactic:
rw [indicator_of_mem (hs.mem_toFinset.1 hx) (fun _ ↦ a)]

Result:
no goals