I'm bad at Lean oops

Changes

1 changed files (+18/-9)

• Tree.lean
  • @@ -1,17 +1,26 @@
    - import Mathlib + -- import Mathlib - namespace blah + -- namespace blah inductive Tree | leaf | branch (children : List Tree) - def area_by_leaf_count (count : Float) := (count * 2 - 1) ^ 2 + def f x := (x - 1) ^ 2 - def area_equiv_leaf_count (area : Float) := (area.sqrt - 1) ^ 2 + #check id - def Tree.area : Tree -> Float - | .leaf => area_by_leaf_count 0 + 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 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 + -- 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