A Lean proof of the chocolate tablet theorem

ChocoTablet.lean

-- Chocolate Bar Theorem 🍫, as illustrated in https://www.instagram.com/p/CzGr1yfAHFB/
-- Credits: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Formulating.20the.20chocolate.20bar.20theorem
-- Run on https://live.lean-lang.org/

inductive ChocoTablet : Nat -> Nat -> Type where
  | square : ChocoTablet 1 1
  | hJoin : ChocoTablet a b -> ChocoTablet a b' -> ChocoTablet a (b + b')
  | vJoin : ChocoTablet a b -> ChocoTablet a' b -> ChocoTablet (a + a') b

def ChocoTablet.cuts : ChocoTablet a b -> Nat
  | square => 0
  | hJoin tablet1 tablet2 => tablet1.cuts + tablet2.cuts + 1
  | vJoin tablet1 tablet2 => tablet1.cuts + tablet2.cuts + 1

theorem ChocoTablet.size_cuts_equation: ∀ tablet : ChocoTablet a b, tablet.cuts + 1 = a * b
  | square => rfl
  | hJoin tablet1 tablet2 => by
    rw [cuts, Nat.mul_add, Nat.add_assoc, Nat.add_add_add_comm,
        <-size_cuts_equation, <-size_cuts_equation]
  | vJoin tablet1 tablet2 => by
    rw [cuts, Nat.add_mul, Nat.add_assoc, Nat.add_add_add_comm,
        <-size_cuts_equation, <-size_cuts_equation]

#print ChocoTablet.size_cuts_equation