case mp
F : Type ?u.566270
α : Type u_1
β : Type ?u.566276
γ : Type ?u.566279
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DivisionMonoid α
s t : Finset α
⊢ IsUnit s → ∃ a, s = {a} ∧ IsUnit a

case mpr
F : Type ?u.566270
α : Type u_1
β : Type ?u.566276
γ : Type ?u.566279
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DivisionMonoid α
s t : Finset α
⊢ (∃ a, s = {a} ∧ IsUnit a) → IsUnit s
F : Type ?u.566270
α : Type u_1
β : Type ?u.566276
γ : Type ?u.566279
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DivisionMonoid α
s t : Finset α
⊢ IsUnit s ↔ ∃ a, s = {a} ∧ IsUnit a
constructor
case mp.intro
F : Type ?u.566270
α : Type u_1
β : Type ?u.566276
γ : Type ?u.566279
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DivisionMonoid α
t : Finset α
u : (Finset α)ˣ
⊢ ∃ a, ↑u = {a} ∧ IsUnit a
case mp
F : Type ?u.566270
α : Type u_1
β : Type ?u.566276
γ : Type ?u.566279
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DivisionMonoid α
s t : Finset α
⊢ IsUnit s → ∃ a, s = {a} ∧ IsUnit a
rintro ⟨u, rfl⟩
case mp.intro.intro.intro.intro.intro
F : Type ?u.566270
α : Type u_1
β : Type ?u.566276
γ : Type ?u.566279
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DivisionMonoid α
t : Finset α
u : (Finset α)ˣ
a b : α
ha : ↑u = {a}
hb : ↑u⁻¹ = {b}
h : a * b = 1
⊢ ∃ a, ↑u = {a} ∧ IsUnit a
case mp.intro
F : Type ?u.566270
α : Type u_1
β : Type ?u.566276
γ : Type ?u.566279
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DivisionMonoid α
t : Finset α
u : (Finset α)ˣ
⊢ ∃ a, ↑u = {a} ∧ IsUnit a
obtain ⟨a, b, ha, hb, h⟩ := Finset.mul_eq_one_iff.1 u.mul_inv
case mp.intro.intro.intro.intro.intro
F : Type ?u.566270
α : Type u_1
β : Type ?u.566276
γ : Type ?u.566279
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DivisionMonoid α
t : Finset α
u : (Finset α)ˣ
a b : α
ha : ↑u = {a}
hb : ↑u⁻¹ = {b}
h : a * b = 1
⊢ {b * a} = {1}
case mp.intro.intro.intro.intro.intro
F : Type ?u.566270
α : Type u_1
β : Type ?u.566276
γ : Type ?u.566279
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DivisionMonoid α
t : Finset α
u : (Finset α)ˣ
a b : α
ha : ↑u = {a}
hb : ↑u⁻¹ = {b}
h : a * b = 1
⊢ ∃ a, ↑u = {a} ∧ IsUnit a
refine' ⟨a, ha, ⟨a, b, h, singleton_injective _⟩, rfl⟩
case mp.intro.intro.intro.intro.intro
F : Type ?u.566270
α : Type u_1
β : Type ?u.566276
γ : Type ?u.566279
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DivisionMonoid α
t : Finset α
u : (Finset α)ˣ
a b : α
ha : ↑u = {a}
hb : ↑u⁻¹ = {b}
h : a * b = 1
⊢ ↑u⁻¹ * ↑u = {1}
case mp.intro.intro.intro.intro.intro
F : Type ?u.566270
α : Type u_1
β : Type ?u.566276
γ : Type ?u.566279
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DivisionMonoid α
t : Finset α
u : (Finset α)ˣ
a b : α
ha : ↑u = {a}
hb : ↑u⁻¹ = {b}
h : a * b = 1
⊢ {b * a} = {1}
rw [← singleton_mul_singleton, ← ha, ← hb]
no goals
case mp.intro.intro.intro.intro.intro
F : Type ?u.566270
α : Type u_1
β : Type ?u.566276
γ : Type ?u.566279
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DivisionMonoid α
t : Finset α
u : (Finset α)ˣ
a b : α
ha : ↑u = {a}
hb : ↑u⁻¹ = {b}
h : a * b = 1
⊢ ↑u⁻¹ * ↑u = {1}
exact u.inv_mul
case mpr.intro.intro
F : Type ?u.566270
α : Type u_1
β : Type ?u.566276
γ : Type ?u.566279
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DivisionMonoid α
t : Finset α
a : α
ha : IsUnit a
⊢ IsUnit {a}
case mpr
F : Type ?u.566270
α : Type u_1
β : Type ?u.566276
γ : Type ?u.566279
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DivisionMonoid α
s t : Finset α
⊢ (∃ a, s = {a} ∧ IsUnit a) → IsUnit s
rintro ⟨a, rfl, ha⟩
no goals
case mpr.intro.intro
F : Type ?u.566270
α : Type u_1
β : Type ?u.566276
γ : Type ?u.566279
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DivisionMonoid α
t : Finset α
a : α
ha : IsUnit a
⊢ IsUnit {a}
exact ha.finset