case refine'_1
F : Type ?u.290745
α : Type u_1
β : Type ?u.290751
γ : Type ?u.290754
δ : Type ?u.290757
ε : Type ?u.290760
inst✝ : DivisionMonoid α
f g : Filter α
hfg : f * g = 1
⊢ ∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1

case refine'_2
F : Type ?u.290745
α : Type u_1
β : Type ?u.290751
γ : Type ?u.290754
δ : Type ?u.290757
ε : Type ?u.290760
inst✝ : DivisionMonoid α
f g : Filter α
⊢ (∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1) → f * g = 1
F : Type ?u.290745
α : Type u_1
β : Type ?u.290751
γ : Type ?u.290754
δ : Type ?u.290757
ε : Type ?u.290760
inst✝ : DivisionMonoid α
f g : Filter α
⊢ f * g = 1 ↔ ∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1
refine' ⟨fun hfg => _, _⟩
case refine'_1.intro.intro.intro.intro
F : Type ?u.290745
α : Type u_1
β : Type ?u.290751
γ : Type ?u.290754
δ : Type ?u.290757
ε : Type ?u.290760
inst✝ : DivisionMonoid α
f g : Filter α
hfg : f * g = 1
t₁ t₂ : Set α
h₁ : t₁ ∈ f
h₂ : t₂ ∈ g
h : t₁ * t₂ ⊆ 1
⊢ ∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1
case refine'_1
F : Type ?u.290745
α : Type u_1
β : Type ?u.290751
γ : Type ?u.290754
δ : Type ?u.290757
ε : Type ?u.290760
inst✝ : DivisionMonoid α
f g : Filter α
hfg : f * g = 1
⊢ ∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1
obtain ⟨t₁, t₂, h₁, h₂, h⟩ : (1 : Set α) ∈ f * g := hfg.symm.subst one_mem_one
case refine'_1.intro.intro.intro.intro
F : Type ?u.290745
α : Type u_1
β : Type ?u.290751
γ : Type ?u.290754
δ : Type ?u.290757
ε : Type ?u.290760
inst✝ : DivisionMonoid α
f g : Filter α
hfg✝ : f * g = 1
t₁ t₂ : Set α
h₁ : t₁ ∈ f
h₂ : t₂ ∈ g
h : t₁ * t₂ ⊆ 1
hfg : NeBot (f * g)
⊢ ∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1
case refine'_1.intro.intro.intro.intro
F : Type ?u.290745
α : Type u_1
β : Type ?u.290751
γ : Type ?u.290754
δ : Type ?u.290757
ε : Type ?u.290760
inst✝ : DivisionMonoid α
f g : Filter α
hfg : f * g = 1
t₁ t₂ : Set α
h₁ : t₁ ∈ f
h₂ : t₂ ∈ g
h : t₁ * t₂ ⊆ 1
⊢ ∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1
have hfg : (f * g).NeBot := hfg.symm.subst one_neBot
case refine'_1.intro.intro.intro.intro
F : Type ?u.290745
α : Type u_1
β : Type ?u.290751
γ : Type ?u.290754
δ : Type ?u.290757
ε : Type ?u.290760
inst✝ : DivisionMonoid α
f g : Filter α
hfg✝ : f * g = 1
t₁ t₂ : Set α
h₁ : t₁ ∈ f
h₂ : t₂ ∈ g
h : ∃ a b, t₁ = {a} ∧ t₂ = {b} ∧ a * b = 1
hfg : NeBot (f * g)
⊢ ∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1
case refine'_1.intro.intro.intro.intro
F : Type ?u.290745
α : Type u_1
β : Type ?u.290751
γ : Type ?u.290754
δ : Type ?u.290757
ε : Type ?u.290760
inst✝ : DivisionMonoid α
f g : Filter α
hfg✝ : f * g = 1
t₁ t₂ : Set α
h₁ : t₁ ∈ f
h₂ : t₂ ∈ g
h : t₁ * t₂ ⊆ 1
hfg : NeBot (f * g)
⊢ ∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1
rw [(hfg.nonempty_of_mem <| mul_mem_mul h₁ h₂).subset_one_iff, Set.mul_eq_one_iff] at h
case refine'_1.intro.intro.intro.intro.intro.intro.intro.intro
F : Type ?u.290745
α : Type u_1
β : Type ?u.290751
γ : Type ?u.290754
δ : Type ?u.290757
ε : Type ?u.290760
inst✝ : DivisionMonoid α
f g : Filter α
hfg✝ : f * g = 1
hfg : NeBot (f * g)
a b : α
h₁ : {a} ∈ f
h : a * b = 1
h₂ : {b} ∈ g
⊢ ∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1
case refine'_1.intro.intro.intro.intro
F : Type ?u.290745
α : Type u_1
β : Type ?u.290751
γ : Type ?u.290754
δ : Type ?u.290757
ε : Type ?u.290760
inst✝ : DivisionMonoid α
f g : Filter α
hfg✝ : f * g = 1
t₁ t₂ : Set α
h₁ : t₁ ∈ f
h₂ : t₂ ∈ g
h : ∃ a b, t₁ = {a} ∧ t₂ = {b} ∧ a * b = 1
hfg : NeBot (f * g)
⊢ ∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1
obtain ⟨a, b, rfl, rfl, h⟩ := h
case refine'_1.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
F : Type ?u.290745
α : Type u_1
β : Type ?u.290751
γ : Type ?u.290754
δ : Type ?u.290757
ε : Type ?u.290760
inst✝ : DivisionMonoid α
f g : Filter α
hfg✝ : f * g = 1
hfg : NeBot (f * g)
a b : α
h₁ : {a} ∈ f
h : a * b = 1
h₂ : {b} ∈ g
⊢ f = pure a

case refine'_1.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
F : Type ?u.290745
α : Type u_1
β : Type ?u.290751
γ : Type ?u.290754
δ : Type ?u.290757
ε : Type ?u.290760
inst✝ : DivisionMonoid α
f g : Filter α
hfg✝ : f * g = 1
hfg : NeBot (f * g)
a b : α
h₁ : {a} ∈ f
h : a * b = 1
h₂ : {b} ∈ g
⊢ g = pure b
case refine'_1.intro.intro.intro.intro.intro.intro.intro.intro
F : Type ?u.290745
α : Type u_1
β : Type ?u.290751
γ : Type ?u.290754
δ : Type ?u.290757
ε : Type ?u.290760
inst✝ : DivisionMonoid α
f g : Filter α
hfg✝ : f * g = 1
hfg : NeBot (f * g)
a b : α
h₁ : {a} ∈ f
h : a * b = 1
h₂ : {b} ∈ g
⊢ ∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1
refine' ⟨a, b, _, _, h⟩
no goals
case refine'_1.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
F : Type ?u.290745
α : Type u_1
β : Type ?u.290751
γ : Type ?u.290754
δ : Type ?u.290757
ε : Type ?u.290760
inst✝ : DivisionMonoid α
f g : Filter α
hfg✝ : f * g = 1
hfg : NeBot (f * g)
a b : α
h₁ : {a} ∈ f
h : a * b = 1
h₂ : {b} ∈ g
⊢ f = pure a
rwa [← hfg.of_mul_left.le_pure_iff, le_pure_iff]
no goals
case refine'_1.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
F : Type ?u.290745
α : Type u_1
β : Type ?u.290751
γ : Type ?u.290754
δ : Type ?u.290757
ε : Type ?u.290760
inst✝ : DivisionMonoid α
f g : Filter α
hfg✝ : f * g = 1
hfg : NeBot (f * g)
a b : α
h₁ : {a} ∈ f
h : a * b = 1
h₂ : {b} ∈ g
⊢ g = pure b
rwa [← hfg.of_mul_right.le_pure_iff, le_pure_iff]
case refine'_2.intro.intro.intro.intro
F : Type ?u.290745
α : Type u_1
β : Type ?u.290751
γ : Type ?u.290754
δ : Type ?u.290757
ε : Type ?u.290760
inst✝ : DivisionMonoid α
a b : α
h : a * b = 1
⊢ pure a * pure b = 1
case refine'_2
F : Type ?u.290745
α : Type u_1
β : Type ?u.290751
γ : Type ?u.290754
δ : Type ?u.290757
ε : Type ?u.290760
inst✝ : DivisionMonoid α
f g : Filter α
⊢ (∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1) → f * g = 1
rintro ⟨a, b, rfl, rfl, h⟩
no goals
case refine'_2.intro.intro.intro.intro
F : Type ?u.290745
α : Type u_1
β : Type ?u.290751
γ : Type ?u.290754
δ : Type ?u.290757
ε : Type ?u.290760
inst✝ : DivisionMonoid α
a b : α
h : a * b = 1
⊢ pure a * pure b = 1
rw [pure_mul_pure, h, pure_one]