Theorem: ENat.tsum_one' (Matroid/ForMathlib/ENatTopology.lean)

State before:
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
⊢ ∑' (i : ↑s), 1 ↑i = s.encard
Tactic:
obtain (hfin | hinf) := s.finite_or_infinite
State after:
case inl
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hfin : s.Finite
⊢ ∑' (i : ↑s), 1 ↑i = s.encard

case inr
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hinf : s.Infinite
⊢ ∑' (i : ↑s), 1 ↑i = s.encard

State before:
case inr
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hinf : s.Infinite
⊢ ∑' (i : ↑s), 1 ↑i = s.encard
Tactic:
rw [hinf.encard_eq, ENat.tsum_subtype_eq_top_of_inter_support_infinite]
State after:
case inr
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hinf : s.Infinite
⊢ (s ∩ support 1).Infinite

State before:
case inr
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hinf : s.Infinite
⊢ (s ∩ support 1).Infinite
Tactic:
simpa
State after:
no goals

State before:
case inl
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hfin : s.Finite
⊢ ∑' (i : ↑s), 1 ↑i = s.encard
Tactic:
have := hfin.fintype
State after:
case inl
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hfin : s.Finite
this : Fintype ↑s
⊢ ∑' (i : ↑s), 1 ↑i = s.encard

State before:
case inl
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hfin : s.Finite
this : Fintype ↑s
⊢ ∑' (i : ↑s), 1 ↑i = s.encard
Tactic:
convert tsum_eq_sum (β := s) (f := (1 : s → ℕ∞)) (s := Finset.univ) (by simp)
State after:
case h.e'_3
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hfin : s.Finite
this : Fintype ↑s
⊢ s.encard = ∑ b : ↑s, 1 b

State before:
case h.e'_3
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hfin : s.Finite
this : Fintype ↑s
⊢ s.encard = ∑ b : ↑s, 1 b
Tactic:
simp only [Pi.one_apply, Finset.sum_const, nsmul_eq_mul, mul_one,
  encard_eq_coe_toFinset_card, toFinset_card, Nat.cast_inj]
State after:
case h.e'_3
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hfin : s.Finite
this : Fintype ↑s
⊢ Fintype.card ↑s = Finset.univ.card

State before:
case h.e'_3
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hfin : s.Finite
this : Fintype ↑s
⊢ Fintype.card ↑s = Finset.univ.card
Tactic:
rfl
State after:
no goals

State before:
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hfin : s.Finite
this : Fintype ↑s
⊢ ∀ b ∉ Finset.univ, 1 b = 0
Tactic:
simp
State after:
no goals