no goals
F : Type ?u.268989
α : Type u_1
β : Type ?u.268995
γ : Type ?u.268998
δ : Type ?u.269001
ε : Type ?u.269004
inst✝ : Monoid α
f g : Filter α
s : Set α
a : α
m n✝ n : ℕ
x✝ : n + 2 ≠ 0
⊢ ⊤ ^ (n + 2) = ⊤
rw [pow_succ, top_pow n.succ_ne_zero, top_mul_top]