Theorem: ENat.Finite.tsum_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 α
hs : s.Finite
⊢ ∑' (x : ↑s), f ↑x = ⊤ ↔ ∃ a ∈ s, f a = ⊤
Tactic:
refine' ⟨hs.induction_on (by simp) @fun a s' has' _ IH htop ↦ _,
  fun ⟨a, has, ha⟩ ↦ ENat.tsum_eq_top_of_eq_top ⟨⟨a, has⟩, ha⟩⟩
State after:
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hs : s.Finite
a : α
s' : Set α
has' : a ∉ s'
x✝ : s'.Finite
IH : ∑' (x : ↑s'), f ↑x = ⊤ → ∃ a ∈ s', f a = ⊤
htop : ∑' (x : ↑(insert a s')), f ↑x = ⊤
⊢ ∃ a_1 ∈ insert a s', f a_1 = ⊤

State before:
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hs : s.Finite
a : α
s' : Set α
has' : a ∉ s'
x✝ : s'.Finite
IH : ∑' (x : ↑s'), f ↑x = ⊤ → ∃ a ∈ s', f a = ⊤
htop : ∑' (x : ↑(insert a s')), f ↑x = ⊤
⊢ ∃ a_1 ∈ insert a s', f a_1 = ⊤
Tactic:
obtain (ht | hne) := eq_or_ne (f a) ⊤
State after:
case inl
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hs : s.Finite
a : α
s' : Set α
has' : a ∉ s'
x✝ : s'.Finite
IH : ∑' (x : ↑s'), f ↑x = ⊤ → ∃ a ∈ s', f a = ⊤
htop : ∑' (x : ↑(insert a s')), f ↑x = ⊤
ht : f a = ⊤
⊢ ∃ a_1 ∈ insert a s', f a_1 = ⊤

case inr
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hs : s.Finite
a : α
s' : Set α
has' : a ∉ s'
x✝ : s'.Finite
IH : ∑' (x : ↑s'), f ↑x = ⊤ → ∃ a ∈ s', f a = ⊤
htop : ∑' (x : ↑(insert a s')), f ↑x = ⊤
hne : f a ≠ ⊤
⊢ ∃ a_1 ∈ insert a s', f a_1 = ⊤

State before:
case inr
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hs : s.Finite
a : α
s' : Set α
has' : a ∉ s'
x✝ : s'.Finite
IH : ∑' (x : ↑s'), f ↑x = ⊤ → ∃ a ∈ s', f a = ⊤
htop : ∑' (x : ↑(insert a s')), f ↑x = ⊤
hne : f a ≠ ⊤
⊢ ∃ a_1 ∈ insert a s', f a_1 = ⊤
Tactic:
rw [ENat.tsum_insert has', WithTop.add_eq_top, or_iff_right hne] at htop
State after:
case inr
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hs : s.Finite
a : α
s' : Set α
has' : a ∉ s'
x✝ : s'.Finite
IH : ∑' (x : ↑s'), f ↑x = ⊤ → ∃ a ∈ s', f a = ⊤
htop : ∑' (x : ↑s'), f ↑x = ⊤
hne : f a ≠ ⊤
⊢ ∃ a_1 ∈ insert a s', f a_1 = ⊤

State before:
case inr
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hs : s.Finite
a : α
s' : Set α
has' : a ∉ s'
x✝ : s'.Finite
IH : ∑' (x : ↑s'), f ↑x = ⊤ → ∃ a ∈ s', f a = ⊤
htop : ∑' (x : ↑s'), f ↑x = ⊤
hne : f a ≠ ⊤
⊢ ∃ a_1 ∈ insert a s', f a_1 = ⊤
Tactic:
obtain ⟨b, hbs, hbtop⟩ := IH htop
State after:
case inr.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hs : s.Finite
a : α
s' : Set α
has' : a ∉ s'
x✝ : s'.Finite
IH : ∑' (x : ↑s'), f ↑x = ⊤ → ∃ a ∈ s', f a = ⊤
htop : ∑' (x : ↑s'), f ↑x = ⊤
hne : f a ≠ ⊤
b : α
hbs : b ∈ s'
hbtop : f b = ⊤
⊢ ∃ a_1 ∈ insert a s', f a_1 = ⊤

State before:
case inr.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hs : s.Finite
a : α
s' : Set α
has' : a ∉ s'
x✝ : s'.Finite
IH : ∑' (x : ↑s'), f ↑x = ⊤ → ∃ a ∈ s', f a = ⊤
htop : ∑' (x : ↑s'), f ↑x = ⊤
hne : f a ≠ ⊤
b : α
hbs : b ∈ s'
hbtop : f b = ⊤
⊢ ∃ a_1 ∈ insert a s', f a_1 = ⊤
Tactic:
exact ⟨b, Or.inr hbs, hbtop⟩
State after:
no goals

State before:
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hs : s.Finite
⊢ ∑' (x : ↑∅), f ↑x = ⊤ → ∃ a ∈ ∅, f a = ⊤
Tactic:
simp
State after:
no goals

State before:
case inl
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hs : s.Finite
a : α
s' : Set α
has' : a ∉ s'
x✝ : s'.Finite
IH : ∑' (x : ↑s'), f ↑x = ⊤ → ∃ a ∈ s', f a = ⊤
htop : ∑' (x : ↑(insert a s')), f ↑x = ⊤
ht : f a = ⊤
⊢ ∃ a_1 ∈ insert a s', f a_1 = ⊤
Tactic:
exact ⟨a, mem_insert _ _, ht⟩
State after:
no goals