Timeroot · October 15, 2021 23:12 · Oct 15, 2021
diff --git a/sim_option_rec.lean b/sim_option_rec.lean
@@ -0,0 +1,47 @@
+/- Define a "nonzero" type -/
+import algebra.group
+universe u
+variables {M : Type*}
+structure nonzero (α : Type u) [C : has_zero α] :=
+(val : α)
+(not_zero : val ≠ 0)
+namespace nonzero
+variable [has_zero M]
+instance : has_coe (nonzero M) M := ⟨val⟩
+@[ext] theorem ext : function.injective (coe : nonzero M → M)
+| ⟨v, h₁⟩ ⟨v', h₂⟩ e := by change v = v' at e; subst v'
+@[simp] theorem mk_coe (u : nonzero M) (h₁) : mk (u : M) h₁ = u := ext rfl
+@[simp] lemma val_eq_coe (a : nonzero M) : a.val = (↑a : M) := rfl
+end nonzero
+
+/-- The meat starts here -/
+
+@[reducible, simp] --a new structure where we forcibly add "0"
+def with0 (T : Type*) := option T
+
+@[reducible, simp] --a new has_mul where we forcibly remove "0"
+def drop0 (T : Type*) [has_zero T] := nonzero T
+
+instance : has_zero (with0 M) := { zero := none }
+
+open classical
+local attribute [instance] prop_decidable
+
+noncomputable def iso [sl : has_zero M]: with0 (drop0 M) ≃ M :=
+{
+to_fun := λ a, option.rec_on a 0 nonzero.val,
+inv_fun := λ a, dite (a=0) (λ _, none) (λ h, option.some (nonzero.mk a h)),
+left_inv := begin
+    intro a, cases a; simp, cases a, contradiction,
+  end,
+right_inv := begin
+    intro a, by_cases a=0,
+      {
+        simp [h],
+        sorry
+      },{
+        simp [h],
+        sorry,
+      }
+  end
+}