F : Type ?u.261734
α : Type u_1
β : Type ?u.261740
γ : Type ?u.261743
δ : Type ?u.261746
ε : Type ?u.261749
inst✝ : Monoid α
f g : Filter α
s✝ : Set α
a : α
m n : ℕ
hf : 1 ≤ f
s : Set α
⊢ s ∈ f * ⊤ → s ∈ ⊤
F : Type ?u.261734
α : Type u_1
β : Type ?u.261740
γ : Type ?u.261743
δ : Type ?u.261746
ε : Type ?u.261749
inst✝ : Monoid α
f g : Filter α
s : Set α
a : α
m n : ℕ
hf : 1 ≤ f
⊢ f * ⊤ = ⊤
refine' top_le_iff.1 fun s => _
F : Type ?u.261734
α : Type u_1
β : Type ?u.261740
γ : Type ?u.261743
δ : Type ?u.261746
ε : Type ?u.261749
inst✝ : Monoid α
f g : Filter α
s✝ : Set α
a : α
m n : ℕ
hf : 1 ≤ f
s : Set α
⊢ (∃ t₁, t₁ ∈ f ∧ t₁ * univ ⊆ s) → s = univ
F : Type ?u.261734
α : Type u_1
β : Type ?u.261740
γ : Type ?u.261743
δ : Type ?u.261746
ε : Type ?u.261749
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.261734
α : Type u_1
β : Type ?u.261740
γ : Type ?u.261743
δ : Type ?u.261746
ε : Type ?u.261749
inst✝ : Monoid α
f g : Filter α
s✝ : Set α
a : α
m n : ℕ
hf : 1 ≤ f
s t : Set α
ht : t ∈ f
hs : t * univ ⊆ s
⊢ s = univ
F : Type ?u.261734
α : Type u_1
β : Type ?u.261740
γ : Type ?u.261743
δ : Type ?u.261746
ε : Type ?u.261749
inst✝ : Monoid α
f g : Filter α
s✝ : Set α
a : α
m n : ℕ
hf : 1 ≤ f
s : Set α
⊢ (∃ t₁, t₁ ∈ f ∧ t₁ * univ ⊆ s) → s = univ
rintro ⟨t, ht, hs⟩
no goals
case intro.intro
F : Type ?u.261734
α : Type u_1
β : Type ?u.261740
γ : Type ?u.261743
δ : Type ?u.261746
ε : Type ?u.261749
inst✝ : Monoid α
f g : Filter α
s✝ : Set α
a : α
m n : ℕ
hf : 1 ≤ f
s t : Set α
ht : t ∈ f
hs : t * univ ⊆ s
⊢ s = univ
rwa [mul_univ_of_one_mem (mem_one.1 <| hf ht), univ_subset_iff] at hs