no goals
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
n : ℕ
hn : ∀ (a : ℕ), a ∈ {n | map f ⊥ ≤ P ^ n} → a ≤ n
⊢ Nat.succ n ∈ {n | map f ⊥ ≤ P ^ n}
simp