Theorem: combineCasesGeneralized (NazgandLean4/Prop.lean)

State before:
k : ℕ+
p : ℕ → Prop
r : Prop
⊢ (∃ k₀ ∈ range ↑k, p k₀) → (r ↔ ∀ k₀ ∈ range ↑k, p k₀ → r)
Tactic:
tauto
State after:
no goals