Prove by definition of type

Stream: lean4

[Op From The Start]

See simpler example in the second post

inductive Game : Ordinal.{u} → Type (u+2)
  | mk (α β: Ordinal.{u}) (l: (αi : Ordinal.{u}) → (lt: αi < α) → (Game αi))
                          (r: (βi : Ordinal.{u}) → (lt: βi < β) → (Game βi)) : Game (max α β)
  | p (α : Ordinal.{u}) (p: α < β) (g: Game α) : Game β
   -- Couldnt use Option so im doing this
  | None : Game γ

def sur_zero : Game 0 := (Ordinal.max_zero_left 0) ▸ Game.mk 0 0
  (fun (αi: Ordinal) (p: αi<0) => absurd p (Ordinal.not_lt_zero αi))
  (fun (βi: Ordinal) (p: βi<0) => absurd p (Ordinal.not_lt_zero βi))


def sur_one : Game 1 := (Ordinal.max_zero_right 1) ▸ Game.mk 1 0
  (fun (αi: Ordinal) (p: αi<1) => Ordinal.lt_one_iff_zero.mp p ▸ sur_zero)
  (fun (βi: Ordinal) (p: βi<0) => absurd p (Ordinal.not_lt_zero βi))

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)]

-- Simplest element larger than Game α, maybe
def rsucc : {α : Ordinal} → (Game α) → (Game (Order.succ α)) := by
intro α g
match g with
 | Game.mk gα gβ glm grm =>
    have gs : Game (Order.succ (max gα gβ)) := max_succ_max ▸ Game.mk (Order.succ (max gα gβ)) gβ
      (fun (αi: Ordinal) (p: αi<(Order.succ (max gα gβ))) => by
        have αlt : αi < gα → Game αi := glm αi
        have αeq : αi >= gα → (αi < α)  → Game αi := by
          intro eq lα
          exact Game.None
        have αeqeq : (αi=α) → Game αi := by
          intro eq
          rw [eq]
          exact g

      )
      (fun (βi: Ordinal) (p: βi<gβ) => grm βi p)
  | Game.p gα p g =>
    exact @Game.p (Order.succ α) gα (lt_trans p (Order.lt_succ α)) g
  | Game.None => exact Game.None

How do I prove that max gα gβ = α in the mk case? Its definitionally true but I'm new so idk how to solve it.

[Op From The Start]

A simpler example is of the following:

inductive Summ : Nat → Type
  | mk (a b : Nat) : Summ (a+b)

def summ_adds : (s: Nat) → Summ s → Prop := fun (s: Nat) (sm: Summ s) => by
  match sm with
   | Summ.mk a b => exact a+b=s

theorem summ_adds_proof : (s: Nat) → ∀ sm: Summ s, summ_adds s sm := by
  intro s sm

How would I go about solving this?

[Eric Wieser]

  cases sm
  rw [summ_adds] -- or `rfl`

finishes the proof

[Op From The Start]

That works for that but not in my first example, I guess what I am really asking is, given that Summ structure, how can I create a proof of a+b=s within another def?