[GOAL]
M : Type u_1
inst✝ : CommMonoid M
src✝ : Group { x // x ∈ IsUnit.submonoid M } := inferInstanceAs (Group { x // x ∈ IsUnit.submonoid M })
a b : { x // x ∈ IsUnit.submonoid M }
⊢ a * b = b * a
[PROOFSTEP]
convert mul_comm a b
[GOAL]
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
a _b : M
x✝¹ : a ∈ {x | ∃ y, x * ↑y = 1}
x✝ : _b ∈ {x | ∃ y, x * ↑y = 1}
a' : { x // x ∈ S }
ha : a * ↑a' = 1
b' : { x // x ∈ S }
hb : _b * ↑b' = 1
⊢ a * _b * ↑(b' * a') = 1
[PROOFSTEP]
simp only [coe_mul, ← mul_assoc, mul_assoc a, hb, mul_one, ha]
[GOAL]
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
⊢ leftInv (leftInv S) ≤ S
[PROOFSTEP]
rintro x ⟨⟨y, z, h₁⟩, h₂ : x * y = 1⟩
[GOAL]
case intro.mk.intro
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
x y : M
z : { x // x ∈ S }
h₁ : y * ↑z = 1
h₂ : x * y = 1
⊢ x ∈ S
[PROOFSTEP]
convert z.prop
[GOAL]
case h.e'_4
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
x y : M
z : { x // x ∈ S }
h₁ : y * ↑z = 1
h₂ : x * y = 1
⊢ x = ↑z
[PROOFSTEP]
rw [← mul_one x, ← h₁, ← mul_assoc, h₂, one_mul]
[GOAL]
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
⊢ leftInv (leftInv S) = S
[PROOFSTEP]
refine' le_antisymm S.leftInv_leftInv_le _
[GOAL]
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
⊢ S ≤ leftInv (leftInv S)
[PROOFSTEP]
intro x hx
[GOAL]
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : M
hx : x ∈ S
⊢ x ∈ leftInv (leftInv S)
[PROOFSTEP]
have : x = ((hS hx).unit⁻¹⁻¹ : Mˣ) := by
  rw [inv_inv (hS hx).unit]
  rfl
[GOAL]
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))⁻¹⁻¹
[PROOFSTEP]
rw [inv_inv (hS hx).unit]
[GOAL]
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))
[PROOFSTEP]
rfl
[GOAL]
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)
[PROOFSTEP]
rw [this]
[GOAL]
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)
[PROOFSTEP]
exact S.leftInv.unit_mem_leftInv _ (S.unit_mem_leftInv _ hx)
[GOAL]
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x : { x // x ∈ leftInv S }
⊢ ↑(fromLeftInv S x) * ↑x = 1
[PROOFSTEP]
rw [mul_comm, mul_fromLeftInv]
[GOAL]
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
a : { x // x ∈ leftInv S }
b : M
⊢ ↑(fromLeftInv S a) = b ↔ ↑a * b = 1
[PROOFSTEP]
rw [← IsUnit.mul_right_inj (leftInv_le_isUnit _ a.prop), S.mul_fromLeftInv, eq_comm]
[GOAL]
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : { x // x ∈ leftInv S }
⊢ ↑(OneHom.toFun { toFun := fromLeftInv S, map_one' := (_ : fromLeftInv S 1 = 1) } (x * y)) =
    ↑(OneHom.toFun { toFun := fromLeftInv S, map_one' := (_ : fromLeftInv S 1 = 1) } x *
        OneHom.toFun { toFun := fromLeftInv S, map_one' := (_ : fromLeftInv S 1 = 1) } y)
[PROOFSTEP]
rw [fromLeftInv_eq_iff, mul_comm x, Submonoid.coe_mul, Submonoid.coe_mul, mul_assoc, ← mul_assoc (x : M),
  mul_fromLeftInv, one_mul, mul_fromLeftInv]
[GOAL]
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
src✝ : { x // x ∈ leftInv S } →* { x // x ∈ S } := fromCommLeftInv S
x : { x // x ∈ S }
⊢ { x // x ∈ leftInv S }
[PROOFSTEP]
choose x' hx using hS x.prop
[GOAL]
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
src✝ : { x // x ∈ leftInv S } →* { x // x ∈ S } := fromCommLeftInv S
x : { x // x ∈ S }
x' : Mˣ
hx : ↑x' = ↑x
⊢ { x // x ∈ leftInv S }
[PROOFSTEP]
exact ⟨x'.inv, x, hx ▸ x'.inv_val⟩
[GOAL]
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
src✝ : { x // x ∈ leftInv S } →* { x // x ∈ S } := fromCommLeftInv S
x : { x // x ∈ leftInv S }
⊢ ↑((fun x =>
          (fun x' hx => { val := x'.inv, property := (_ : ∃ y, x'.inv * ↑y = 1) })
            (Classical.choose (_ : ↑x ∈ IsUnit.submonoid M))
            (_ : ↑(Classical.choose (_ : ↑x ∈ IsUnit.submonoid M)) = ↑x))
        (OneHom.toFun (↑src✝) x)) =
    ↑x
[PROOFSTEP]
dsimp only
[GOAL]
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
src✝ : { x // x ∈ leftInv S } →* { x // x ∈ S } := fromCommLeftInv S
x : { x // x ∈ leftInv S }
⊢ (Classical.choose (_ : ↑(OneHom.toFun (↑(fromCommLeftInv S)) x) ∈ IsUnit.submonoid M)).inv = ↑x
[PROOFSTEP]
generalize_proofs h
[GOAL]
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
src✝ : { x // x ∈ leftInv S } →* { x // x ∈ S } := fromCommLeftInv S
x : { x // x ∈ leftInv S }
h : ↑(OneHom.toFun (↑(fromCommLeftInv S)) x) ∈ IsUnit.submonoid M
⊢ (Classical.choose h).inv = ↑x
[PROOFSTEP]
rw [← h.choose.mul_left_inj]
[GOAL]
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
src✝ : { x // x ∈ leftInv S } →* { x // x ∈ S } := fromCommLeftInv S
x : { x // x ∈ leftInv S }
h : ↑(OneHom.toFun (↑(fromCommLeftInv S)) x) ∈ IsUnit.submonoid M
⊢ (Classical.choose h).inv * ↑(Exists.choose h) = ↑x * ↑(Exists.choose h)
[PROOFSTEP]
conv => rhs; rw [h.choose_spec]
[GOAL]
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
src✝ : { x // x ∈ leftInv S } →* { x // x ∈ S } := fromCommLeftInv S
x : { x // x ∈ leftInv S }
h : ↑(OneHom.toFun (↑(fromCommLeftInv S)) x) ∈ IsUnit.submonoid M
| (Classical.choose h).inv * ↑(Exists.choose h) = ↑x * ↑(Exists.choose h)
[PROOFSTEP]
rhs; rw [h.choose_spec]
[GOAL]
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
src✝ : { x // x ∈ leftInv S } →* { x // x ∈ S } := fromCommLeftInv S
x : { x // x ∈ leftInv S }
h : ↑(OneHom.toFun (↑(fromCommLeftInv S)) x) ∈ IsUnit.submonoid M
| (Classical.choose h).inv * ↑(Exists.choose h) = ↑x * ↑(Exists.choose h)
[PROOFSTEP]
rhs; rw [h.choose_spec]
[GOAL]
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
src✝ : { x // x ∈ leftInv S } →* { x // x ∈ S } := fromCommLeftInv S
x : { x // x ∈ leftInv S }
h : ↑(OneHom.toFun (↑(fromCommLeftInv S)) x) ∈ IsUnit.submonoid M
| (Classical.choose h).inv * ↑(Exists.choose h) = ↑x * ↑(Exists.choose h)
[PROOFSTEP]
rhs
[GOAL]
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
src✝ : { x // x ∈ leftInv S } →* { x // x ∈ S } := fromCommLeftInv S
x : { x // x ∈ leftInv S }
h : ↑(OneHom.toFun (↑(fromCommLeftInv S)) x) ∈ IsUnit.submonoid M
| ↑x * ↑(Exists.choose h)
[PROOFSTEP]
rw [h.choose_spec]
[GOAL]
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
src✝ : { x // x ∈ leftInv S } →* { x // x ∈ S } := fromCommLeftInv S
x : { x // x ∈ leftInv S }
h : ↑(OneHom.toFun (↑(fromCommLeftInv S)) x) ∈ IsUnit.submonoid M
⊢ (Classical.choose h).inv * ↑(Exists.choose h) = ↑x * ↑(OneHom.toFun (↑(fromCommLeftInv S)) x)
[PROOFSTEP]
exact h.choose.inv_val.trans (S.mul_fromLeftInv x).symm
[GOAL]
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
src✝ : { x // x ∈ leftInv S } →* { x // x ∈ S } := fromCommLeftInv S
x : { x // x ∈ S }
⊢ OneHom.toFun (↑src✝)
      ((fun x =>
          (fun x' hx => { val := x'.inv, property := (_ : ∃ y, x'.inv * ↑y = 1) })
            (Classical.choose (_ : ↑x ∈ IsUnit.submonoid M))
            (_ : ↑(Classical.choose (_ : ↑x ∈ IsUnit.submonoid M)) = ↑x))
        x) =
    x
[PROOFSTEP]
dsimp only [fromCommLeftInv]
[GOAL]
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
src✝ : { x // x ∈ leftInv S } →* { x // x ∈ S } := fromCommLeftInv S
x : { x // x ∈ S }
⊢ fromLeftInv S
      { val := (Classical.choose (_ : ↑x ∈ IsUnit.submonoid M)).inv,
        property := (_ : ∃ y, (Classical.choose (_ : ↑x ∈ IsUnit.submonoid M)).inv * ↑y = 1) } =
    x
[PROOFSTEP]
ext
[GOAL]
case a
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
src✝ : { x // x ∈ leftInv S } →* { x // x ∈ S } := fromCommLeftInv S
x : { x // x ∈ S }
⊢ ↑(fromLeftInv S
        { val := (Classical.choose (_ : ↑x ∈ IsUnit.submonoid M)).inv,
          property := (_ : ∃ y, (Classical.choose (_ : ↑x ∈ IsUnit.submonoid M)).inv * ↑y = 1) }) =
    ↑x
[PROOFSTEP]
rw [fromLeftInv_eq_iff]
[GOAL]
case a
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
src✝ : { x // x ∈ leftInv S } →* { x // x ∈ S } := fromCommLeftInv S
x : { x // x ∈ S }
⊢ ↑{ val := (Classical.choose (_ : ↑x ∈ IsUnit.submonoid M)).inv,
          property := (_ : ∃ y, (Classical.choose (_ : ↑x ∈ IsUnit.submonoid M)).inv * ↑y = 1) } *
      ↑x =
    1
[PROOFSTEP]
convert (hS x.prop).choose.inv_val
[GOAL]
case h.e'_2.h.e'_6
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
src✝ : { x // x ∈ leftInv S } →* { x // x ∈ S } := fromCommLeftInv S
x : { x // x ∈ S }
⊢ ↑x = ↑(Exists.choose (_ : ↑x ∈ IsUnit.submonoid M))
[PROOFSTEP]
exact (hS x.prop).choose_spec.symm
[GOAL]
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : { x // x ∈ leftInv S }
⊢ ↑(↑(leftInvEquiv S hS) x) * ↑x = 1
[PROOFSTEP]
simpa only [leftInvEquiv_apply, fromCommLeftInv] using fromLeftInv_mul S x
[GOAL]
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : { x // x ∈ leftInv S }
⊢ ↑x * ↑(↑(leftInvEquiv S hS) x) = 1
[PROOFSTEP]
simp only [leftInvEquiv_apply, fromCommLeftInv, mul_fromLeftInv]
[GOAL]
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : { x // x ∈ S }
⊢ ↑(↑(MulEquiv.symm (leftInvEquiv S hS)) x) * ↑x = 1
[PROOFSTEP]
convert S.mul_leftInvEquiv hS ((S.leftInvEquiv hS).symm x)
[GOAL]
case h.e'_2.h.e'_6.h.e'_3
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : { x // x ∈ S }
⊢ x = ↑(leftInvEquiv S hS) (↑(MulEquiv.symm (leftInvEquiv S hS)) x)
[PROOFSTEP]
simp
[GOAL]
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : { x // x ∈ S }
⊢ ↑x * ↑(↑(MulEquiv.symm (leftInvEquiv S hS)) x) = 1
[PROOFSTEP]
convert S.leftInvEquiv_mul hS ((S.leftInvEquiv hS).symm x)
[GOAL]
case h.e'_2.h.e'_5.h.e'_3
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : { x // x ∈ S }
⊢ x = ↑(leftInvEquiv S hS) (↑(MulEquiv.symm (leftInvEquiv S hS)) x)
[PROOFSTEP]
simp
[GOAL]
M : Type u_1
inst✝ : Group M
S : Submonoid M
x : { x // x ∈ leftInv S }
⊢ ↑(fromLeftInv S x) = (↑x)⁻¹
[PROOFSTEP]
rw [← mul_right_inj (x : M), mul_right_inv, mul_fromLeftInv]
[GOAL]
M : Type u_1
inst✝ : CommGroup M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : { x // x ∈ S }
⊢ ↑(↑(MulEquiv.symm (leftInvEquiv S hS)) x) = (↑x)⁻¹
[PROOFSTEP]
rw [← mul_right_inj (x : M), mul_right_inv, mul_leftInvEquiv_symm]
