one can escape the hell?

unhell.lean

-- import Mathlib.Logic.Basic
-- import Mathlib.Tactic.GeneralizeProofs
-- import Mathlib.Logic.Function.Basic
-- import Mathlib.Tactic
-- import Aesop

inductive N where | z | s (_:N)

def plus (a b : N):N := 
  match a, b with
  | .z, n => n
  | .s a , n => .s (plus a n)


def zero_plus : plus a .z = a := by
  induction a
  rfl
  case _ x h =>
  rw [plus.eq_2]
  rw [h]

def plus_out_s_left : plus a (.s b) = .s (plus a b) := by
  cases a
  rfl
  case _ x => 
  rw [plus.eq_2]
  apply congrArg
  rw [plus.eq_2]
  apply plus_out_s_left
  

def n_plus_comm (a b:N) : plus a b = plus b a := by
  induction a
  {
    rw [plus.eq_1]
    symm
    apply zero_plus
  }
  {
    case _ k ih =>
    rw [plus.eq_2]
    rw [plus_out_s_left]
    apply congrArg
    apply ih
  }

-- def plus_symm_ty (a b:N) : Sort _ := 
def plus_symm_ty (a b:N) : Sort _ := 
  match a, b with
  | .z, _ => (plus b N.z = b) -> (plus b N.z = b -> plus a b = plus b a) -> plus a b = plus b a
  | .s k , _ => (plus k.s b = plus b k.s) -> (plus a b.s = (plus a b).s -> plus a b = plus b a) -> plus a b = plus b a


def plus_symm (a b:N): plus_symm_ty a b := by
  cases a
  {
    unfold plus_symm_ty
    simp
    intro h1 c
    let p := c h1
    exact p
  }
  {
    case _ x =>
    unfold plus_symm_ty
    intro k c
    apply c
    rw [plus.eq_2]
    apply congrArg
    rw [plus_out_s_left]
    rw [plus.eq_2]
  }
  
def plus_symm_ty_is_ : plus_symm_ty a b = (plus a b = plus b a) := by
  refine propext ?_
  apply Iff.intro
  cases a
  {
    unfold plus_symm_ty
    simp
    intro k
    let x := k zero_plus (by exact fun a => k a fun a_1 => id (Eq.symm a))
    exact x
  }
  {
    case _ m =>
    unfold plus_symm_ty
    simp
    intro k
    let x := k (by exact n_plus_comm m.s b) 
               (by exact fun a => n_plus_comm m.s b)
    exact x
  }
  {
    exact fun _ => plus_symm a b
  }

example {a b:N} : plus a b = plus b a := by
  let x := plus_symm a b
  rw [plus_symm_ty_is_] at x
  exact x