Theorem: one_le_schnirelmannDensity_iff_of_zero_mem (LeanCamCombi/Mathlib/Combinatorics/Schnirelmann.lean)

State before:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
⊢ 1 ≤ schnirelmannDensity A ↔ A = Set.univ
Tactic:
rw [schnirelmannDensity_le_one.ge_iff_eq, schnirelmannDensity_eq_one_iff_of_zero_mem hA]
State after:
no goals