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

State before:
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
⊢ ∑' (a : ↑s), f ↑a = ⊤ ↔ (s ∩ support f).Infinite ∨ ∃ a ∈ s, f a = ⊤
Tactic:
simp_rw [ENat.tsum_eq_top_iff, Subtype.exists, exists_prop]
State after:
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
⊢ ((support fun a => f ↑a).Infinite ∨ ∃ a ∈ s, f a = ⊤) ↔ (s ∩ support f).Infinite ∨ ∃ a ∈ s, f a = ⊤

State before:
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
⊢ ((support fun a => f ↑a).Infinite ∨ ∃ a ∈ s, f a = ⊤) ↔ (s ∩ support f).Infinite ∨ ∃ a ∈ s, f a = ⊤
Tactic:
convert Iff.rfl
State after:
case h.e'_2.h.e'_1.h.a
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
⊢ (s ∩ support f).Finite ↔ (support fun a => f ↑a).Finite

State before:
case h.e'_2.h.e'_1.h.a
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
⊢ (s ∩ support f).Finite ↔ (support fun a => f ↑a).Finite
Tactic:
simp_rw [← Set.finite_coe_iff]
State after:
case h.e'_2.h.e'_1.h.a
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
⊢ Finite ↑(s ∩ support f) ↔ Finite ↑(support fun a => f ↑a)

State before:
case h.e'_2.h.e'_1.h.a
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
⊢ Finite ↑(s ∩ support f) ↔ Finite ↑(support fun a => f ↑a)
Tactic:
exact Bijective.finite_iff (f := fun i ↦ ⟨⟨i,i.2.1⟩, i.2.2⟩)
  ⟨by rintro ⟨i, hi⟩ ⟨j, hj⟩ hij; simpa using hij, by rintro ⟨⟨i,his⟩, hi⟩; use ⟨i, ⟨his, hi⟩⟩⟩
State after:
no goals

State before:
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
⊢ Injective fun i => ⟨⟨↑i, ⋯⟩, ⋯⟩
Tactic:
rintro ⟨i, hi⟩ ⟨j, hj⟩ hij
State after:
case mk.mk
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
i : α
hi : i ∈ s ∩ support f
j : α
hj : j ∈ s ∩ support f
hij : (fun i => ⟨⟨↑i, ⋯⟩, ⋯⟩) ⟨i, hi⟩ = (fun i => ⟨⟨↑i, ⋯⟩, ⋯⟩) ⟨j, hj⟩
⊢ ⟨i, hi⟩ = ⟨j, hj⟩

State before:
case mk.mk
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
i : α
hi : i ∈ s ∩ support f
j : α
hj : j ∈ s ∩ support f
hij : (fun i => ⟨⟨↑i, ⋯⟩, ⋯⟩) ⟨i, hi⟩ = (fun i => ⟨⟨↑i, ⋯⟩, ⋯⟩) ⟨j, hj⟩
⊢ ⟨i, hi⟩ = ⟨j, hj⟩
Tactic:
simpa using hij
State after:
no goals

State before:
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
⊢ Surjective fun i => ⟨⟨↑i, ⋯⟩, ⋯⟩
Tactic:
rintro ⟨⟨i,his⟩, hi⟩
State after:
case mk.mk
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
i : α
his : i ∈ s
hi : ⟨i, his⟩ ∈ support fun a => f ↑a
⊢ ∃ a, (fun i => ⟨⟨↑i, ⋯⟩, ⋯⟩) a = ⟨⟨i, his⟩, hi⟩

State before:
case mk.mk
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
i : α
his : i ∈ s
hi : ⟨i, his⟩ ∈ support fun a => f ↑a
⊢ ∃ a, (fun i => ⟨⟨↑i, ⋯⟩, ⋯⟩) a = ⟨⟨i, his⟩, hi⟩
Tactic:
use ⟨i, ⟨his, hi⟩⟩
State after:
no goals