Theorem: ENat.tsum_eq_top_of_support_infinite (Matroid/ForMathlib/ENatTopology.lean)

State before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
⊢ ∑' (a : α), f a = ⊤
Tactic:
rw [ENat.tsum_eq_iSup_sum, iSup_eq_top]
State after:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
⊢ ∀ b < ⊤, ∃ i, b < ∑ a ∈ i, f a

State before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
⊢ ∀ b < ⊤, ∃ i, b < ∑ a ∈ i, f a
Tactic:
intro b hb
State after:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
b : ℕ∞
hb : b < ⊤
⊢ ∃ i, b < ∑ a ∈ i, f a

State before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
b : ℕ∞
hb : b < ⊤
⊢ ∃ i, b < ∑ a ∈ i, f a
Tactic:
lift b to ℕ using hb.ne
State after:
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
b : ℕ
hb : ↑b < ⊤
⊢ ∃ i, ↑b < ∑ a ∈ i, f a

State before:
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
b : ℕ
hb : ↑b < ⊤
⊢ ∃ i, ↑b < ∑ a ∈ i, f a
Tactic:
obtain ⟨s, hss, hsc⟩ := exists_subset_encard_eq ((add_one_le_of_lt hb).trans_eq hf.encard_eq.symm)
State after:
case intro.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
b : ℕ
hb : ↑b < ⊤
s : Set α
hss : s ⊆ support f
hsc : s.encard = ↑b + 1
⊢ ∃ i, ↑b < ∑ a ∈ i, f a

State before:
case intro.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
b : ℕ
hb : ↑b < ⊤
s : Set α
hss : s ⊆ support f
hsc : s.encard = ↑b + 1
⊢ ∃ i, ↑b < ∑ a ∈ i, f a
Tactic:
rw [← Nat.cast_one, ← Nat.cast_add] at hsc
State after:
case intro.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
b : ℕ
hb : ↑b < ⊤
s : Set α
hss : s ⊆ support f
hsc : s.encard = ↑(b + 1)
⊢ ∃ i, ↑b < ∑ a ∈ i, f a

State before:
case intro.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
b : ℕ
hb : ↑b < ⊤
s : Set α
hss : s ⊆ support f
hsc : s.encard = ↑(b + 1)
⊢ ∃ i, ↑b < ∑ a ∈ i, f a
Tactic:
set s' := (finite_of_encard_eq_coe hsc).toFinset
State after:
case intro.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
b : ℕ
hb : ↑b < ⊤
s : Set α
hss : s ⊆ support f
hsc : s.encard = ↑(b + 1)
s' : Finset α := ⋯.toFinset
⊢ ∃ i, ↑b < ∑ a ∈ i, f a

State before:
case intro.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
b : ℕ
hb : ↑b < ⊤
s : Set α
hss : s ⊆ support f
hsc : s.encard = ↑(b + 1)
s' : Finset α := ⋯.toFinset
⊢ ∃ i, ↑b < ∑ a ∈ i, f a
Tactic:
refine ⟨s', lt_of_lt_of_le ?_ (Finset.sum_le_sum (show ∀ i ∈ s', 1 ≤ f i from ?_))  ⟩
State after:
case intro.intro.intro.refine_1
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
b : ℕ
hb : ↑b < ⊤
s : Set α
hss : s ⊆ support f
hsc : s.encard = ↑(b + 1)
s' : Finset α := ⋯.toFinset
⊢ ↑b < ∑ i ∈ s', 1

case intro.intro.intro.refine_2
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
b : ℕ
hb : ↑b < ⊤
s : Set α
hss : s ⊆ support f
hsc : s.encard = ↑(b + 1)
s' : Finset α := ⋯.toFinset
⊢ ∀ i ∈ s', 1 ≤ f i

State before:
case intro.intro.intro.refine_2
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
b : ℕ
hb : ↑b < ⊤
s : Set α
hss : s ⊆ support f
hsc : s.encard = ↑(b + 1)
s' : Finset α := ⋯.toFinset
⊢ ∀ i ∈ s', 1 ≤ f i
Tactic:
simp only [Finite.mem_toFinset, ENat.one_le_iff_ne_zero, s']
State after:
case intro.intro.intro.refine_2
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
b : ℕ
hb : ↑b < ⊤
s : Set α
hss : s ⊆ support f
hsc : s.encard = ↑(b + 1)
s' : Finset α := ⋯.toFinset
⊢ ∀ i ∈ s, f i ≠ 0

State before:
case intro.intro.intro.refine_2
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
b : ℕ
hb : ↑b < ⊤
s : Set α
hss : s ⊆ support f
hsc : s.encard = ↑(b + 1)
s' : Finset α := ⋯.toFinset
⊢ ∀ i ∈ s, f i ≠ 0
Tactic:
exact hss
State after:
no goals

State before:
case intro.intro.intro.refine_1
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
b : ℕ
hb : ↑b < ⊤
s : Set α
hss : s ⊆ support f
hsc : s.encard = ↑(b + 1)
s' : Finset α := ⋯.toFinset
⊢ ↑b < ∑ i ∈ s', 1
Tactic:
rw [Finset.sum_const, nsmul_eq_mul, mul_one,
  ← (finite_of_encard_eq_coe hsc).encard_eq_coe_toFinset_card, hsc, Nat.cast_lt]
State after:
case intro.intro.intro.refine_1
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
b : ℕ
hb : ↑b < ⊤
s : Set α
hss : s ⊆ support f
hsc : s.encard = ↑(b + 1)
s' : Finset α := ⋯.toFinset
⊢ b < b + 1

State before:
case intro.intro.intro.refine_1
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
b : ℕ
hb : ↑b < ⊤
s : Set α
hss : s ⊆ support f
hsc : s.encard = ↑(b + 1)
s' : Finset α := ⋯.toFinset
⊢ b < b + 1
Tactic:
exact Nat.lt.base b
State after:
no goals