M : Type u_1
inst✝ : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
⊢ S ≤ leftInv (leftInv S)
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
⊢ leftInv (leftInv S) = S
refine' le_antisymm S.leftInv_leftInv_le _
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : M
hx : x ∈ S
⊢ x ∈ leftInv (leftInv S)
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
⊢ S ≤ leftInv (leftInv S)
intro x hx
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : M
hx : x ∈ S
this : x = ↑(IsUnit.unit (_ : x ∈ IsUnit.submonoid M))⁻¹⁻¹
⊢ x ∈ leftInv (leftInv S)
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : M
hx : x ∈ S
⊢ x ∈ leftInv (leftInv S)
have : x = ((hS hx).unit⁻¹⁻¹ : Mˣ) := by
  rw [inv_inv (hS hx).unit]
  rfl
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : M
hx : x ∈ S
this : x = ↑(IsUnit.unit (_ : x ∈ IsUnit.submonoid M))⁻¹⁻¹
⊢ ↑(IsUnit.unit (_ : x ∈ IsUnit.submonoid M))⁻¹⁻¹ ∈ leftInv (leftInv S)
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : M
hx : x ∈ S
this : x = ↑(IsUnit.unit (_ : x ∈ IsUnit.submonoid M))⁻¹⁻¹
⊢ x ∈ leftInv (leftInv S)
rw [this]
no goals
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : M
hx : x ∈ S
this : x = ↑(IsUnit.unit (_ : x ∈ IsUnit.submonoid M))⁻¹⁻¹
⊢ ↑(IsUnit.unit (_ : x ∈ IsUnit.submonoid M))⁻¹⁻¹ ∈ leftInv (leftInv S)
exact S.leftInv.unit_mem_leftInv _ (S.unit_mem_leftInv _ hx)
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : M
hx : x ∈ S
⊢ x = ↑(IsUnit.unit (_ : x ∈ IsUnit.submonoid M))
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : M
hx : x ∈ S
⊢ x = ↑(IsUnit.unit (_ : x ∈ IsUnit.submonoid M))⁻¹⁻¹
rw [inv_inv (hS hx).unit]
no goals
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : M
hx : x ∈ S
⊢ x = ↑(IsUnit.unit (_ : x ∈ IsUnit.submonoid M))
rfl