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

State before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
inst✝ : CompleteLattice α
f : ℕ∞ → α
⊢ ⨅ x, ⨅ (_ : x ≠ ⊤), f x = ⨅ x, f ↑x
Tactic:
rw [iInf_subtype', cinfi_ne_top]
State after:
no goals