-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
theorem mul_eq_one_iff : s * t = 1 ↔ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1

Proof state:
case refine_1.intro
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
⊢ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1

Tactic:
obtain ⟨b, hb⟩ := hst.of_image2_right

Result:
case refine_1.intro.intro
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
b : α
hb : b ∈ t
⊢ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1

Proof state:
case refine_1.intro.intro
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
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

Tactic:
refine ⟨a, b, ?_, ?_, H ha hb⟩ <;> refine eq_singleton_iff_unique_mem.2 ⟨‹_›, fun x hx => ?_⟩

Result:
case refine_1.intro.intro.refine_1
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
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
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
x : α
hx : x ∈ t
⊢ x = b

Proof state:
case refine_1.intro.intro
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
b : α
hb : b ∈ t
⊢ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1

Tactic:
have H : ∀ {a b}, a ∈ s → b ∈ t → a * b = (1 : α) := fun {a b} ha hb =>
  h.subset <| mem_image2_of_mem ha hb

Result:
case refine_1.intro.intro
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
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

Proof state:
case refine_1
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
⊢ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1

Tactic:
have hst : (s * t).Nonempty := h.symm.subst one_nonempty

Result:
case refine_1
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
⊢ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1

Proof state:
case refine_2
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
⊢ (∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1) → s * t = 1

Tactic:
rintro ⟨b, c, rfl, rfl, h⟩

Result:
case refine_2.intro.intro.intro.intro
α : Type u_2
inst✝ : DivisionMonoid α
b c : α
h : b * c = 1
⊢ {b} * {c} = 1

Proof state:
case refine_1.intro.intro.refine_1
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
x : α
hx : x ∈ s
⊢ x = a

Tactic:
exact (eq_inv_of_mul_eq_one_left <| H hx hb).trans (inv_eq_of_mul_eq_one_left <| H ha hb)

Result:
no goals

Proof state:
case refine_2.intro.intro.intro.intro
α : Type u_2
inst✝ : DivisionMonoid α
b c : α
h : b * c = 1
⊢ {b} * {c} = 1

Tactic:
rw [singleton_mul_singleton, h, singleton_one]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
⊢ s * t = 1 ↔ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1

Tactic:
refine ⟨fun h => ?_, ?_⟩

Result:
case refine_1
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
⊢ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1

case refine_2
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
⊢ (∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1) → s * t = 1

Proof state:
case refine_1.intro.intro.refine_2
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
x : α
hx : x ∈ t
⊢ x = b

Tactic:
exact (eq_inv_of_mul_eq_one_right <| H ha hx).trans (inv_eq_of_mul_eq_one_right <| H ha hb)

Result:
no goals

Proof state:
case refine_1
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
⊢ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1

Tactic:
obtain ⟨a, ha⟩ := hst.of_image2_left

Result:
case refine_1.intro
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
⊢ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1