case intro.intro.intro.intro
F : Type ?u.314978
α : Type u_1
β : Type ?u.314984
γ : Type ?u.314987
δ : Type ?u.314990
ε : Type ?u.314993
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
m : F
f g f₁ g₁ : Filter α
f₂ g₂ : Filter β
h : NeBot f
s t₁ t₂ : Set α
h₁ : t₁ ∈ f
h₂ : t₂ ∈ f
hs : t₁ / t₂ ⊆ s
⊢ s ∈ 1
F : Type ?u.314978
α : Type u_1
β : Type ?u.314984
γ : Type ?u.314987
δ : Type ?u.314990
ε : Type ?u.314993
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
m : F
f g f₁ g₁ : Filter α
f₂ g₂ : Filter β
h : NeBot f
⊢ 1 ≤ f / f
rintro s ⟨t₁, t₂, h₁, h₂, hs⟩
case intro.intro.intro.intro.intro.intro
F : Type ?u.314978
α : Type u_1
β : Type ?u.314984
γ : Type ?u.314987
δ : Type ?u.314990
ε : Type ?u.314993
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
m : F
f g f₁ g₁ : Filter α
f₂ g₂ : Filter β
h : NeBot f
s t₁ t₂ : Set α
h₁ : t₁ ∈ f
h₂ : t₂ ∈ f
hs : t₁ / t₂ ⊆ s
a : α
ha₁ : a ∈ t₁
ha₂ : a ∈ t₂
⊢ s ∈ 1
case intro.intro.intro.intro
F : Type ?u.314978
α : Type u_1
β : Type ?u.314984
γ : Type ?u.314987
δ : Type ?u.314990
ε : Type ?u.314993
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
m : F
f g f₁ g₁ : Filter α
f₂ g₂ : Filter β
h : NeBot f
s t₁ t₂ : Set α
h₁ : t₁ ∈ f
h₂ : t₂ ∈ f
hs : t₁ / t₂ ⊆ s
⊢ s ∈ 1
obtain ⟨a, ha₁, ha₂⟩ := Set.not_disjoint_iff.1 (h.not_disjoint h₁ h₂)
case intro.intro.intro.intro.intro.intro
F : Type ?u.314978
α : Type u_1
β : Type ?u.314984
γ : Type ?u.314987
δ : Type ?u.314990
ε : Type ?u.314993
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
m : F
f g f₁ g₁ : Filter α
f₂ g₂ : Filter β
h : NeBot f
s t₁ t₂ : Set α
h₁ : t₁ ∈ f
h₂ : t₂ ∈ f
hs : t₁ / t₂ ⊆ s
a : α
ha₁ : a ∈ t₁
ha₂ : a ∈ t₂
⊢ a / a ∈ s
case intro.intro.intro.intro.intro.intro
F : Type ?u.314978
α : Type u_1
β : Type ?u.314984
γ : Type ?u.314987
δ : Type ?u.314990
ε : Type ?u.314993
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
m : F
f g f₁ g₁ : Filter α
f₂ g₂ : Filter β
h : NeBot f
s t₁ t₂ : Set α
h₁ : t₁ ∈ f
h₂ : t₂ ∈ f
hs : t₁ / t₂ ⊆ s
a : α
ha₁ : a ∈ t₁
ha₂ : a ∈ t₂
⊢ s ∈ 1
rw [mem_one, ← div_self' a]
no goals
case intro.intro.intro.intro.intro.intro
F : Type ?u.314978
α : Type u_1
β : Type ?u.314984
γ : Type ?u.314987
δ : Type ?u.314990
ε : Type ?u.314993
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
m : F
f g f₁ g₁ : Filter α
f₂ g₂ : Filter β
h : NeBot f
s t₁ t₂ : Set α
h₁ : t₁ ∈ f
h₂ : t₂ ∈ f
hs : t₁ / t₂ ⊆ s
a : α
ha₁ : a ∈ t₁
ha₂ : a ∈ t₂
⊢ a / a ∈ s
exact hs (Set.div_mem_div ha₁ ha₂)