Proving a Prop that has a match

Stream: lean4

[Op From The Start]

I am working on making the surreal numbers in Lean from scratch. I came across a problem when trying to write proofs for propositions that are defined using match statements. I boiled down the problem into this MVE:

import Mathlib.SetTheory.Ordinal.Basic
import Mathlib.SetTheory.Ordinal.Arithmetic
import Init.Prelude
import Mathlib.Init.Logic
import Mathlib.Order.SuccPred.Basic

inductive Maxx: Ordinal.{u} → Type (u+1)
| mk (a b: Ordinal) : Maxx (max a b)

theorem max_succ_max : {α β : Ordinal} → max (Order.succ (max α β)) β = Order.succ (max α β) := by
  intro a b
  rw [succ_max, max_assoc, max_eq_left_of_lt (Order.lt_succ b)]

def succ {a: Ordinal} (m: Maxx a) : Maxx (Order.succ a) :=
  match m with
    | Maxx.mk a2 b => (max_succ_max) ▸ Maxx.mk ((max a2 b)+1) (b)

def zerom : Maxx 0 := (Ordinal.max_zero_right 0) ▸ Maxx.mk 0 0
def onem : Maxx 1 := (Ordinal.max_zero_right 1) ▸ Maxx.mk 1 0

def is_eq {a b: Ordinal} (m1: Maxx a) (m2: Maxx b) : Prop :=
  match m1 with
  | Maxx.mk m1a m1b =>
    match m2 with
    | Maxx.mk m2a m2b => m1a=m2a ∧ m1b=m2b

theorem m_succ_zero_eq_one : is_eq (succ zerom) onem := by
  rw [is_eq, succ, zerom, onem]
  split
  . case _ am mx mxl mxr maxmx heq =>
    split
    . case _ an nx nxl nxr maxnx heq2 =>
      apply And.intro

I am having trouble proving anything from here, as I have hypotheses

am : Ordinal.{u_1}
mx : Maxx am
mxl mxr : Ordinal.{u_1}
maxmx : Order.succ 0 = max mxl mxr
heq : HEq
  (match 0, zerom.proof_1 ▸ Maxx.mk 0 0 with
  | .(max a2 b), Maxx.mk a2 b => ⋯ ▸ Maxx.mk (max a2 b + 1) b)
  (Maxx.mk mxl mxr)
an : Ordinal.{u_1}
nx : Maxx an
nxl nxr : Ordinal.{u_1}
maxnx : 1 = max nxl nxr
heq2 : HEq (onem.proof_1 ▸ Maxx.mk 1 0) (Maxx.mk nxl nxr)

And want to destructure the match here, but I do not know how. I also want to know how to show that proof ▸ Maxx.mk objects are always still Maxx.mk, but I don't know how. It is basically true by definition since zerom is Maxx.mk 0 0, onem is Maxx.mk 1 0, and succ adds one to the first term. How can I prove m_succ_zero_eq_one?

[Ted Hwa]

The normal way to destructure match hypotheses is split at heq but in this case you get an error saying that something isn't type correct and you need to generalize a discriminant manually. Someone more knowledgeable than me will need to explain how to do that or if you need a different approach altogether.

I'll just say that the Maxx (max a b) on the right side of the inductive definition, and the presence of things like zerom.proof_1, look weird to me.