F : Type ?u.195336
α : Type u_1
β : Type ?u.195342
γ : Type ?u.195345
δ : Type ?u.195348
ε : Type ?u.195351
inst✝ : Monoid α
f g : Filter α
s : Set α
a : α
m n : ℕ
hs : s ∈ f
⊢ 1 ∈ f ^ 0
F : Type ?u.195336
α : Type u_1
β : Type ?u.195342
γ : Type ?u.195345
δ : Type ?u.195348
ε : Type ?u.195351
inst✝ : Monoid α
f g : Filter α
s : Set α
a : α
m n : ℕ
hs : s ∈ f
⊢ s ^ 0 ∈ f ^ 0
rw [pow_zero]
no goals
F : Type ?u.195336
α : Type u_1
β : Type ?u.195342
γ : Type ?u.195345
δ : Type ?u.195348
ε : Type ?u.195351
inst✝ : Monoid α
f g : Filter α
s : Set α
a : α
m n : ℕ
hs : s ∈ f
⊢ 1 ∈ f ^ 0
exact one_mem_one
F : Type ?u.195336
α : Type u_1
β : Type ?u.195342
γ : Type ?u.195345
δ : Type ?u.195348
ε : Type ?u.195351
inst✝ : Monoid α
f g : Filter α
s : Set α
a : α
m n✝ : ℕ
hs : s ∈ f
n : ℕ
⊢ s * s ^ n ∈ f ^ (n + 1)
F : Type ?u.195336
α : Type u_1
β : Type ?u.195342
γ : Type ?u.195345
δ : Type ?u.195348
ε : Type ?u.195351
inst✝ : Monoid α
f g : Filter α
s : Set α
a : α
m n✝ : ℕ
hs : s ∈ f
n : ℕ
⊢ s ^ (n + 1) ∈ f ^ (n + 1)
rw [pow_succ]
no goals
F : Type ?u.195336
α : Type u_1
β : Type ?u.195342
γ : Type ?u.195345
δ : Type ?u.195348
ε : Type ?u.195351
inst✝ : Monoid α
f g : Filter α
s : Set α
a : α
m n✝ : ℕ
hs : s ∈ f
n : ℕ
⊢ s * s ^ n ∈ f ^ (n + 1)
exact mul_mem_mul hs (pow_mem_pow hs n)