case a
α : Type ?u.59382
G : Type u_1
M : Type ?u.59388
R : Type ?u.59391
A : Type ?u.59394
inst✝² : Monoid M
inst✝¹ : AddMonoid A
s✝ t u : Set M
inst✝ : Group G
s : Set G
⊢ closure s⁻¹ ≤ (closure s)⁻¹

case a
α : Type ?u.59382
G : Type u_1
M : Type ?u.59388
R : Type ?u.59391
A : Type ?u.59394
inst✝² : Monoid M
inst✝¹ : AddMonoid A
s✝ t u : Set M
inst✝ : Group G
s : Set G
⊢ (closure s)⁻¹ ≤ closure s⁻¹
α : Type ?u.59382
G : Type u_1
M : Type ?u.59388
R : Type ?u.59391
A : Type ?u.59394
inst✝² : Monoid M
inst✝¹ : AddMonoid A
s✝ t u : Set M
inst✝ : Group G
s : Set G
⊢ closure s⁻¹ = (closure s)⁻¹
apply le_antisymm
case a
α : Type ?u.59382
G : Type u_1
M : Type ?u.59388
R : Type ?u.59391
A : Type ?u.59394
inst✝² : Monoid M
inst✝¹ : AddMonoid A
s✝ t u : Set M
inst✝ : Group G
s : Set G
⊢ s ⊆ ↑(closure s)
case a
α : Type ?u.59382
G : Type u_1
M : Type ?u.59388
R : Type ?u.59391
A : Type ?u.59394
inst✝² : Monoid M
inst✝¹ : AddMonoid A
s✝ t u : Set M
inst✝ : Group G
s : Set G
⊢ closure s⁻¹ ≤ (closure s)⁻¹
rw [closure_le, coe_inv, ← Set.inv_subset, inv_inv]
no goals
case a
α : Type ?u.59382
G : Type u_1
M : Type ?u.59388
R : Type ?u.59391
A : Type ?u.59394
inst✝² : Monoid M
inst✝¹ : AddMonoid A
s✝ t u : Set M
inst✝ : Group G
s : Set G
⊢ s ⊆ ↑(closure s)
exact subset_closure
case a
α : Type ?u.59382
G : Type u_1
M : Type ?u.59388
R : Type ?u.59391
A : Type ?u.59394
inst✝² : Monoid M
inst✝¹ : AddMonoid A
s✝ t u : Set M
inst✝ : Group G
s : Set G
⊢ s⁻¹ ⊆ ↑(closure s⁻¹)
case a
α : Type ?u.59382
G : Type u_1
M : Type ?u.59388
R : Type ?u.59391
A : Type ?u.59394
inst✝² : Monoid M
inst✝¹ : AddMonoid A
s✝ t u : Set M
inst✝ : Group G
s : Set G
⊢ (closure s)⁻¹ ≤ closure s⁻¹
rw [inv_le, closure_le, coe_inv, ← Set.inv_subset]
no goals
case a
α : Type ?u.59382
G : Type u_1
M : Type ?u.59388
R : Type ?u.59391
A : Type ?u.59394
inst✝² : Monoid M
inst✝¹ : AddMonoid A
s✝ t u : Set M
inst✝ : Group G
s : Set G
⊢ s⁻¹ ⊆ ↑(closure s⁻¹)
exact subset_closure