case refine_1
α : Type ?u.1425
G : Type u_1
A : Type ?u.1431
S✝ : Type ?u.1434
inst✝¹ : Group G
inst✝ : AddGroup A
s S : Set G
x : G
hx : x ∈ (closure S).toSubmonoid
⊢ x ∈ Submonoid.closure (S ∪ S⁻¹)

case refine_2
α : Type ?u.1425
G : Type u_1
A : Type ?u.1431
S✝ : Type ?u.1434
inst✝¹ : Group G
inst✝ : AddGroup A
s S : Set G
⊢ S ∪ S⁻¹ ⊆ ↑(closure S).toSubmonoid
α : Type ?u.1425
G : Type u_1
A : Type ?u.1431
S✝ : Type ?u.1434
inst✝¹ : Group G
inst✝ : AddGroup A
s S : Set G
⊢ (closure S).toSubmonoid = Submonoid.closure (S ∪ S⁻¹)
refine le_antisymm (fun x hx => ?_) (Submonoid.closure_le.2 ?_)
case refine_1
α : Type ?u.1425
G : Type u_1
A : Type ?u.1431
S✝ : Type ?u.1434
inst✝¹ : Group G
inst✝ : AddGroup A
s S : Set G
x✝ : G
hx✝ : x✝ ∈ (closure S).toSubmonoid
x : G
hx : x ∈ Submonoid.closure (S ∪ S⁻¹)
⊢ x⁻¹ ∈ Submonoid.closure (S ∪ S⁻¹)
case refine_1
α : Type ?u.1425
G : Type u_1
A : Type ?u.1431
S✝ : Type ?u.1434
inst✝¹ : Group G
inst✝ : AddGroup A
s S : Set G
x : G
hx : x ∈ (closure S).toSubmonoid
⊢ x ∈ Submonoid.closure (S ∪ S⁻¹)
refine'
  closure_induction hx
    (fun x hx => Submonoid.closure_mono (subset_union_left S S⁻¹) (Submonoid.subset_closure hx))
    (Submonoid.one_mem _) (fun x y hx hy => Submonoid.mul_mem _ hx hy) fun x hx => _
no goals
case refine_1
α : Type ?u.1425
G : Type u_1
A : Type ?u.1431
S✝ : Type ?u.1434
inst✝¹ : Group G
inst✝ : AddGroup A
s S : Set G
x✝ : G
hx✝ : x✝ ∈ (closure S).toSubmonoid
x : G
hx : x ∈ Submonoid.closure (S ∪ S⁻¹)
⊢ x⁻¹ ∈ Submonoid.closure (S ∪ S⁻¹)
rwa [← Submonoid.mem_closure_inv, Set.union_inv, inv_inv, Set.union_comm]
no goals
case refine_2
α : Type ?u.1425
G : Type u_1
A : Type ?u.1431
S✝ : Type ?u.1434
inst✝¹ : Group G
inst✝ : AddGroup A
s S : Set G
⊢ S ∪ S⁻¹ ⊆ ↑(closure S).toSubmonoid
simp only [true_and_iff, coe_toSubmonoid, union_subset_iff, subset_closure, inv_subset_closure]