case refine'_1
F : Type ?u.310838
α : Type u_1
β : Type ?u.310844
γ : Type ?u.310847
δ : Type ?u.310850
ε : Type ?u.310853
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
m : F
f g f₁ g₁ : Filter α
f₂ g₂ : Filter β
h : 1 ≤ f / g
hfg : Disjoint f g
⊢ False

case refine'_2
F : Type ?u.310838
α : Type u_1
β : Type ?u.310844
γ : Type ?u.310847
δ : Type ?u.310850
ε : Type ?u.310853
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
m : F
f g f₁ g₁ : Filter α
f₂ g₂ : Filter β
⊢ ¬Disjoint f g → 1 ≤ f / g
F : Type ?u.310838
α : Type u_1
β : Type ?u.310844
γ : Type ?u.310847
δ : Type ?u.310850
ε : Type ?u.310853
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
m : F
f g f₁ g₁ : Filter α
f₂ g₂ : Filter β
⊢ 1 ≤ f / g ↔ ¬Disjoint f g
refine' ⟨fun h hfg => _, _⟩
case refine'_1.intro.intro.intro.intro
F : Type ?u.310838
α : Type u_1
β : Type ?u.310844
γ : Type ?u.310847
δ : Type ?u.310850
ε : Type ?u.310853
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
m : F
f g f₁ g₁ : Filter α
f₂ g₂ : Filter β
h : 1 ≤ f / g
hfg : Disjoint f g
s : Set α
hs : s ∈ f
t : Set α
ht : t ∈ g
hst : ∅ = s ∩ t
⊢ False
case refine'_1
F : Type ?u.310838
α : Type u_1
β : Type ?u.310844
γ : Type ?u.310847
δ : Type ?u.310850
ε : Type ?u.310853
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
m : F
f g f₁ g₁ : Filter α
f₂ g₂ : Filter β
h : 1 ≤ f / g
hfg : Disjoint f g
⊢ False
obtain ⟨s, hs, t, ht, hst⟩ := hfg.le_bot (mem_bot : ∅ ∈ ⊥)
no goals
case refine'_1.intro.intro.intro.intro
F : Type ?u.310838
α : Type u_1
β : Type ?u.310844
γ : Type ?u.310847
δ : Type ?u.310850
ε : Type ?u.310853
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
m : F
f g f₁ g₁ : Filter α
f₂ g₂ : Filter β
h : 1 ≤ f / g
hfg : Disjoint f g
s : Set α
hs : s ∈ f
t : Set α
ht : t ∈ g
hst : ∅ = s ∩ t
⊢ False
exact Set.one_mem_div_iff.1 (h <| div_mem_div hs ht) (disjoint_iff.2 hst.symm)
case refine'_2.intro.intro.intro.intro
F : Type ?u.310838
α : Type u_1
β : Type ?u.310844
γ : Type ?u.310847
δ : Type ?u.310850
ε : Type ?u.310853
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
m : F
f g f₁ g₁ : Filter α
f₂ g₂ : Filter β
h : ¬Disjoint f g
s t₁ t₂ : Set α
h₁ : t₁ ∈ f
h₂ : t₂ ∈ g
hs : t₁ / t₂ ⊆ s
⊢ s ∈ 1
case refine'_2
F : Type ?u.310838
α : Type u_1
β : Type ?u.310844
γ : Type ?u.310847
δ : Type ?u.310850
ε : Type ?u.310853
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
m : F
f g f₁ g₁ : Filter α
f₂ g₂ : Filter β
⊢ ¬Disjoint f g → 1 ≤ f / g
rintro h s ⟨t₁, t₂, h₁, h₂, hs⟩
no goals
case refine'_2.intro.intro.intro.intro
F : Type ?u.310838
α : Type u_1
β : Type ?u.310844
γ : Type ?u.310847
δ : Type ?u.310850
ε : Type ?u.310853
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
m : F
f g f₁ g₁ : Filter α
f₂ g₂ : Filter β
h : ¬Disjoint f g
s t₁ t₂ : Set α
h₁ : t₁ ∈ f
h₂ : t₂ ∈ g
hs : t₁ / t₂ ⊆ s
⊢ s ∈ 1
exact hs (Set.one_mem_div_iff.2 fun ht => h <| disjoint_of_disjoint_of_mem ht h₁ h₂)