1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20
21. 21
22. 22
23. 23
24. 24
25. 25
26. 26

-- import Mathlib

-- namespace blah
inductive Tree
  | leaf
  | branch (children : List Tree)

def f x := (x - 1) ^ 2

#check id

def size : Tree -> Nat
  | .leaf => 1
  | .branch children => children.map size |>.sum

def g (x : Tree) := match x with
  | .leaf => 1
  | .branch children =>
  -- have : (children.map g |>.map f) = children.map (f ∘ g) := List.map_map
  --   simp only [List.map_map]
  children.map g |>.map f |>.sum
  -- children.map (f ∘ g) |>.sum



--   simp