From 23987022462656693c902a1f96b458b3ccc9c984 Mon Sep 17 00:00:00 2001
From: Eric <eric.1334@icloud.com>
Date: Mon, 21 Oct 2024 11:18:31 -0700
Subject: [PATCH] Prove that alpha is a subsemigroup of with_one alpha

---
 OrderedSemigroups/SemigroupToMonoid.lean | 39 ++++++++++++++++++++++++
 1 file changed, 39 insertions(+)

diff --git a/OrderedSemigroups/SemigroupToMonoid.lean b/OrderedSemigroups/SemigroupToMonoid.lean
index 299d1e8..8a6d8e9 100644
--- a/OrderedSemigroups/SemigroupToMonoid.lean
+++ b/OrderedSemigroups/SemigroupToMonoid.lean
@@ -35,6 +35,45 @@ instance : Monoid (with_one α) where
     <;> unfold_projs
     <;> simp
 
+def without_one : Subsemigroup (with_one α) where
+  carrier := {x : with_one α | ∃y : α, x = Sum.inl y}
+  mul_mem' := by
+    intro x' y' hx hy
+    obtain ⟨x, hx⟩ := hx
+    obtain ⟨y, hy⟩ := hy
+    subst_vars
+    simp
+    use (x*y)
+    unfold_projs
+    simp
+
+noncomputable def iso_without_one : α ≃* without_one (α := α) where
+  toFun x := ⟨Sum.inl x, by use x⟩
+  invFun x := by
+    obtain ⟨y, hy⟩ := x
+    use hy.choose
+  left_inv := by
+    simp [Function.LeftInverse]
+    intro x
+    set point : without_one (α := α) := ⟨Sum.inl x, by use x⟩
+    have := point.2.choose_spec
+    apply Sum.inl.inj
+    rw [←this]
+  right_inv := by
+    simp [Function.RightInverse, Function.LeftInverse]
+    intro x hx
+    obtain ⟨y, hy⟩ := hx
+    simp [hy]
+    rw [Sum.inl.injEq]
+    set point : without_one (α := α) := ⟨Sum.inl y, by use y⟩
+    have := point.2.choose_spec
+    apply Sum.inl.inj
+    rw [←this]
+  map_mul' := by
+    intro x y
+    unfold_projs
+    simp
+
 end Semigroup
 
 section CommSemigroup'