This proof is too hard

Changes

1 changed files (+17/-0)

• Tree.lean (new)
  • @@ -0,0 +1,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