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

import Mathlib

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

def area_by_leaf_count (count : Float) := (count * 2 - 1) ^ 2

def area_equiv_leaf_count (area : Float) := (area.sqrt - 1) ^ 2

def Tree.area : Tree -> Float
| .leaf => area_by_leaf_count 0
| .branch children =>
  have : (children.map Tree.area |>.map area_equiv_leaf_count) = children.map (area_equiv_leaf_count ∘ Tree.area) := List.map_map
  -- children.map Tree.area |>.map area_equiv_leaf_count |>.sum
  children.map (area_equiv_leaf_count ∘ Tree.area) |>.sum