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/

import Mathlib.Data.Nat.Basic


inductive ChocoTablet : Nat -> Nat -> Type where
  | square : ChocoTablet 1 1
  | hJoin {a b b' : Nat} : ChocoTablet a b -> ChocoTablet a b' -> ChocoTablet a (b + b')
  | vJoin {a a' b : Nat} : 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

def ChocoTablet.size(_ : ChocoTablet a b) : Nat := a * b

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

#print ChocoTablet.size_cuts_equation