case refine'_1
F : Type ?u.80713
α : Type u_1
β : Type ?u.80719
γ : Type ?u.80722
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
⊢ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1

case refine'_2
F : Type ?u.80713
α : Type u_1
β : Type ?u.80719
γ : Type ?u.80722
inst✝ : DivisionMonoid α
s t : Set α
⊢ (∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1) → s * t = 1
F : Type ?u.80713
α : Type u_1
β : Type ?u.80719
γ : Type ?u.80722
inst✝ : DivisionMonoid α
s t : Set α
⊢ s * t = 1 ↔ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1
refine' ⟨fun h => _, _⟩
case refine'_1
F : Type ?u.80713
α : Type u_1
β : Type ?u.80719
γ : Type ?u.80722
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : Set.Nonempty (s * t)
⊢ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1
case refine'_1
F : Type ?u.80713
α : Type u_1
β : Type ?u.80719
γ : Type ?u.80722
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
⊢ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1
have hst : (s * t).Nonempty := h.symm.subst one_nonempty
case refine'_1.intro
F : Type ?u.80713
α : Type u_1
β : Type ?u.80719
γ : Type ?u.80722
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : Set.Nonempty (s * t)
a : α
ha : a ∈ s
⊢ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1
case refine'_1
F : Type ?u.80713
α : Type u_1
β : Type ?u.80719
γ : Type ?u.80722
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : Set.Nonempty (s * t)
⊢ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1
obtain ⟨a, ha⟩ := hst.of_image2_left
case refine'_1.intro.intro
F : Type ?u.80713
α : Type u_1
β : Type ?u.80719
γ : Type ?u.80722
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : Set.Nonempty (s * t)
a : α
ha : a ∈ s
b : α
hb : b ∈ t
⊢ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1
case refine'_1.intro
F : Type ?u.80713
α : Type u_1
β : Type ?u.80719
γ : Type ?u.80722
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : Set.Nonempty (s * t)
a : α
ha : a ∈ s
⊢ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1
obtain ⟨b, hb⟩ := hst.of_image2_right
case refine'_1.intro.intro
F : Type ?u.80713
α : Type u_1
β : Type ?u.80719
γ : Type ?u.80722
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : Set.Nonempty (s * t)
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
⊢ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1
case refine'_1.intro.intro
F : Type ?u.80713
α : Type u_1
β : Type ?u.80719
γ : Type ?u.80722
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : Set.Nonempty (s * t)
a : α
ha : a ∈ s
b : α
hb : b ∈ t
⊢ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1
have H : ∀ {a b}, a ∈ s → b ∈ t → a * b = (1 : α) := fun {a b} ha hb =>
  h.subset <| mem_image2_of_mem ha hb
case refine'_1.intro.intro.refine'_1
F : Type ?u.80713
α : Type u_1
β : Type ?u.80719
γ : Type ?u.80722
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : Set.Nonempty (s * t)
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
x : α
hx : x ∈ s
⊢ x = a

case refine'_1.intro.intro.refine'_2
F : Type ?u.80713
α : Type u_1
β : Type ?u.80719
γ : Type ?u.80722
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : Set.Nonempty (s * t)
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
x : α
hx : x ∈ t
⊢ x = b
case refine'_1.intro.intro
F : Type ?u.80713
α : Type u_1
β : Type ?u.80719
γ : Type ?u.80722
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : Set.Nonempty (s * t)
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
⊢ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1
refine' ⟨a, b, _, _, H ha hb⟩ <;> refine' eq_singleton_iff_unique_mem.2 ⟨‹_›, fun x hx => _⟩
no goals
case refine'_1.intro.intro.refine'_1
F : Type ?u.80713
α : Type u_1
β : Type ?u.80719
γ : Type ?u.80722
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : Set.Nonempty (s * t)
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
x : α
hx : x ∈ s
⊢ x = a
exact (eq_inv_of_mul_eq_one_left <| H hx hb).trans (inv_eq_of_mul_eq_one_left <| H ha hb)
no goals
case refine'_1.intro.intro.refine'_2
F : Type ?u.80713
α : Type u_1
β : Type ?u.80719
γ : Type ?u.80722
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : Set.Nonempty (s * t)
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
x : α
hx : x ∈ t
⊢ x = b
exact (eq_inv_of_mul_eq_one_right <| H ha hx).trans (inv_eq_of_mul_eq_one_right <| H ha hb)
case refine'_2.intro.intro.intro.intro
F : Type ?u.80713
α : Type u_1
β : Type ?u.80719
γ : Type ?u.80722
inst✝ : DivisionMonoid α
b c : α
h : b * c = 1
⊢ {b} * {c} = 1
case refine'_2
F : Type ?u.80713
α : Type u_1
β : Type ?u.80719
γ : Type ?u.80722
inst✝ : DivisionMonoid α
s t : Set α
⊢ (∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1) → s * t = 1
rintro ⟨b, c, rfl, rfl, h⟩
no goals
case refine'_2.intro.intro.intro.intro
F : Type ?u.80713
α : Type u_1
β : Type ?u.80719
γ : Type ?u.80722
inst✝ : DivisionMonoid α
b c : α
h : b * c = 1
⊢ {b} * {c} = 1
rw [singleton_mul_singleton, h, singleton_one]