F : Type ?u.264796
α : Type u_1
β : Type ?u.264802
γ : Type ?u.264805
δ : Type ?u.264808
ε : Type ?u.264811
inst✝ : Monoid α
f g : Filter α
s✝ : Set α
a : α
m n : ℕ
hf : 1 ≤ f
s : Set α
⊢ s ∈ ⊤ * f → s ∈ ⊤
F : Type ?u.264796
α : Type u_1
β : Type ?u.264802
γ : Type ?u.264805
δ : Type ?u.264808
ε : Type ?u.264811
inst✝ : Monoid α
f g : Filter α
s : Set α
a : α
m n : ℕ
hf : 1 ≤ f
⊢ ⊤ * f = ⊤
refine' top_le_iff.1 fun s => _
F : Type ?u.264796
α : Type u_1
β : Type ?u.264802
γ : Type ?u.264805
δ : Type ?u.264808
ε : Type ?u.264811
inst✝ : Monoid α
f g : Filter α
s✝ : Set α
a : α
m n : ℕ
hf : 1 ≤ f
s : Set α
⊢ (∃ x, x ∈ f ∧ univ * x ⊆ s) → s = univ
F : Type ?u.264796
α : Type u_1
β : Type ?u.264802
γ : Type ?u.264805
δ : Type ?u.264808
ε : Type ?u.264811
inst✝ : Monoid α
f g : Filter α
s✝ : Set α
a : α
m n : ℕ
hf : 1 ≤ f
s : Set α
⊢ s ∈ ⊤ * f → s ∈ ⊤
simp only [mem_mul, mem_top, exists_and_left, exists_eq_left]
case intro.intro
F : Type ?u.264796
α : Type u_1
β : Type ?u.264802
γ : Type ?u.264805
δ : Type ?u.264808
ε : Type ?u.264811
inst✝ : Monoid α
f g : Filter α
s✝ : Set α
a : α
m n : ℕ
hf : 1 ≤ f
s t : Set α
ht : t ∈ f
hs : univ * t ⊆ s
⊢ s = univ
F : Type ?u.264796
α : Type u_1
β : Type ?u.264802
γ : Type ?u.264805
δ : Type ?u.264808
ε : Type ?u.264811
inst✝ : Monoid α
f g : Filter α
s✝ : Set α
a : α
m n : ℕ
hf : 1 ≤ f
s : Set α
⊢ (∃ x, x ∈ f ∧ univ * x ⊆ s) → s = univ
rintro ⟨t, ht, hs⟩
no goals
case intro.intro
F : Type ?u.264796
α : Type u_1
β : Type ?u.264802
γ : Type ?u.264805
δ : Type ?u.264808
ε : Type ?u.264811
inst✝ : Monoid α
f g : Filter α
s✝ : Set α
a : α
m n : ℕ
hf : 1 ≤ f
s t : Set α
ht : t ∈ f
hs : univ * t ⊆ s
⊢ s = univ
rwa [univ_mul_of_one_mem (mem_one.1 <| hf ht), univ_subset_iff] at hs