Physlib.Mathematics.DataStructures.FourTree.UniqueMap

Imports

/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.Mathematics.DataStructures.FourTree.Basic

Unique maps for `FourTree`

We define the uniqueMap4 and uniqueMap3 functions for FourTree. For a given f : α4 → α4 or f : α3 → α3, these functions the elements of a FourTree, and leave only new elements which are not already present in the tree (if the tree has no duplicates).

@[expose] public section

uniqueMap4

Given a map f : α4 → α4 the map from Leaf α4 → Leaf α4 mapping the underlying elements.

def Leaf.uniqueMap4 : Leaf α4 → Leaf α4
  | .leaf x => .leaf (f x)

Given a map f : α4 → α4 the map from Twig α3 α4 → Twig α3 α4 mapping the underlying leafs and deleting any that appear in the original Twig.

def Twig.uniqueMap4 (T : Twig α3 α4) : Twig α3 α4 :=
  match T with
  | .twig xs leafs =>
    let leafFinst := leafs.map (fun l => match l with
      | .leaf ys => ys)
    let sub : Multiset α4 := leafFinst.filterMap (fun ys =>
      if ¬ f ys ∈ leafFinst then
        some (f ys)
      else
        none)
    .twig xs (sub.map (fun ys => .leaf ys))

Given a map f : α4 → α4 the map from Branch α2 α3 α4 → Branch α2 α3 α4 mapping the underlying leafs and deleting any that appear in the original Twig.

def Branch.uniqueMap4 (T : Branch α2 α3 α4) :
    Branch α2 α3 α4:=
  match T with
  | .branch xo twigs =>
    .branch xo (twigs.map fun ts => (Twig.uniqueMap4 f ts))

Given a map f : α4 → α4 the map from Trunk α1 α2 α3 α4 → Trunk α1 α2 α3 α4 mapping the underlying leafs and deleting any that appear in the original Twig.

def Trunk.uniqueMap4 (T : Trunk α1 α2 α3 α4) : Trunk α1 α2 α3 α4 :=
  match T with
  | .trunk xo branches =>
    .trunk xo (branches.map fun bs => (Branch.uniqueMap4 f bs))

Given a map f : α4 → α4 the map from FourTree α1 α2 α3 α4 → FourTree α1 α2 α3 α4 mapping the underlying leafs and deleting any that appear in the original twig of that leaf.

def uniqueMap4 (T : FourTree α1 α2 α3 α4) : FourTree α1 α2 α3 α4 :=
  match T with
  | .root trunks =>
    .root (trunks.map fun ts => (ts.uniqueMap4 f))

lemma map_mem_uniqueMap4 {T : FourTree α1 α2 α3 α4}
    (x : α1 × α2 × α3 × α4) (hx : x ∈ T) (f : α4 → α4) :
    (x.1, x.2.1, x.2.2.1, f x.2.2.2) ∈ T.uniqueMap4 f ∨
    (x.1, x.2.1, x.2.2.1, f x.2.2.2) ∈ T := byα1:Typeα2:Typeα3:Typeα4:Typeinst✝:DecidableEq α4T:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4hx:x ∈ Tf:α4 → α4⊢ (x.1, x.2.1, x.2.2.1, f x.2.2.2) ∈ uniqueMap4 f T ∨ (x.1, x.2.1, x.2.2.1, f x.2.2.2) ∈ T
  by_cases hnotMem : (x.1, x.2.1, x.2.2.1, f x.2.2.2) ∈ Tposα1:Typeα2:Typeα3:Typeα4:Typeinst✝:DecidableEq α4T:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4hx:x ∈ Tf:α4 → α4hnotMem:(x.1, x.2.1, x.2.2.1, f x.2.2.2) ∈ T⊢ (x.1, x.2.1, x.2.2.1, f x.2.2.2) ∈ uniqueMap4 f T ∨ (x.1, x.2.1, x.2.2.1, f x.2.2.2) ∈ Tnegα1:Typeα2:Typeα3:Typeα4:Typeinst✝:DecidableEq α4T:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4hx:x ∈ Tf:α4 → α4hnotMem:¬(x.1, x.2.1, x.2.2.1, f x.2.2.2) ∈ T⊢ (x.1, x.2.1, x.2.2.1, f x.2.2.2) ∈ uniqueMap4 f T ∨ (x.1, x.2.1, x.2.2.1, f x.2.2.2) ∈ T
  ·posα1:Typeα2:Typeα3:Typeα4:Typeinst✝:DecidableEq α4T:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4hx:x ∈ Tf:α4 → α4hnotMem:(x.1, x.2.1, x.2.2.1, f x.2.2.2) ∈ T⊢ (x.1, x.2.1, x.2.2.1, f x.2.2.2) ∈ uniqueMap4 f T ∨ (x.1, x.2.1, x.2.2.1, f x.2.2.2) ∈ T simp [hnotMem]All goals completed! 🐙
  leftnegα1:Typeα2:Typeα3:Typeα4:Typeinst✝:DecidableEq α4T:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4hx:x ∈ Tf:α4 → α4hnotMem:¬(x.1, x.2.1, x.2.2.1, f x.2.2.2) ∈ T⊢ (x.1, x.2.1, x.2.2.1, f x.2.2.2) ∈ uniqueMap4 f T
  simp [mem_iff_mem_toMultiset, toMultiset] at hxnegα1:Typeα2:Typeα3:Typeα4:Typeinst✝:DecidableEq α4T:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4f:α4 → α4hnotMem:¬(x.1, x.2.1, x.2.2.1, f x.2.2.2) ∈ Thx:∃ a, a ∈ T.1 ∧ ∃ a_1, a_1 ∈ a.2 ∧ ∃ a_2, a_2 ∈ a_1.2 ∧ ∃ a_3, a_3 ∈ a_2.2 ∧ (a.1, a_1.1, a_2.1, a_3.1) = x⊢ (x.1, x.2.1, x.2.2.1, f x.2.2.2) ∈ uniqueMap4 f T
  obtain ⟨trunk, htrunk, branch, hbranch, twig, htwig, leaf, hleaf, heq⟩ := hxnegα1:Typeα2:Typeα3:Typeα4:Typeinst✝:DecidableEq α4T:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4f:α4 → α4hnotMem:¬(x.1, x.2.1, x.2.2.1, f x.2.2.2) ∈ Ttrunk:Trunk α1 α2 α3 α4htrunk:trunk ∈ T.1branch:Branch α2 α3 α4hbranch:branch ∈ trunk.2twig:Twig α3 α4htwig:twig ∈ branch.2leaf:Leaf α4hleaf:leaf ∈ twig.2heq:(trunk.1, branch.1, twig.1, leaf.1) = x⊢ (x.1, x.2.1, x.2.2.1, f x.2.2.2) ∈ uniqueMap4 f T
  apply mem_of_parts (trunk.uniqueMap4 f) (branch.uniqueMap4 f) (twig.uniqueMap4 f)
    (.leaf (f leaf.1))neg.trunk_memα1:Typeα2:Typeα3:Typeα4:Typeinst✝:DecidableEq α4T:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4f:α4 → α4hnotMem:¬(x.1, x.2.1, x.2.2.1, f x.2.2.2) ∈ Ttrunk:Trunk α1 α2 α3 α4htrunk:trunk ∈ T.1branch:Branch α2 α3 α4hbranch:branch ∈ trunk.2twig:Twig α3 α4htwig:twig ∈ branch.2leaf:Leaf α4hleaf:leaf ∈ twig.2heq:(trunk.1, branch.1, twig.1, leaf.1) = x⊢ Trunk.uniqueMap4 f trunk ∈ (uniqueMap4 f T).1neg.branch_memα1:Typeα2:Typeα3:Typeα4:Typeinst✝:DecidableEq α4T:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4f:α4 → α4hnotMem:¬(x.1, x.2.1, x.2.2.1, f x.2.2.2) ∈ Ttrunk:Trunk α1 α2 α3 α4htrunk:trunk ∈ T.1branch:Branch α2 α3 α4hbranch:branch ∈ trunk.2twig:Twig α3 α4htwig:twig ∈ branch.2leaf:Leaf α4hleaf:leaf ∈ twig.2heq:(trunk.1, branch.1, twig.1, leaf.1) = x⊢ Branch.uniqueMap4 f branch ∈ (Trunk.uniqueMap4 f trunk).2neg.twig_memα1:Typeα2:Typeα3:Typeα4:Typeinst✝:DecidableEq α4T:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4f:α4 → α4hnotMem:¬(x.1, x.2.1, x.2.2.1, f x.2.2.2) ∈ Ttrunk:Trunk α1 α2 α3 α4htrunk:trunk ∈ T.1branch:Branch α2 α3 α4hbranch:branch ∈ trunk.2twig:Twig α3 α4htwig:twig ∈ branch.2leaf:Leaf α4hleaf:leaf ∈ twig.2heq:(trunk.1, branch.1, twig.1, leaf.1) = x⊢ Twig.uniqueMap4 f twig ∈ (Branch.uniqueMap4 f branch).2neg.leaf_memα1:Typeα2:Typeα3:Typeα4:Typeinst✝:DecidableEq α4T:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4f:α4 → α4hnotMem:¬(x.1, x.2.1, x.2.2.1, f x.2.2.2) ∈ Ttrunk:Trunk α1 α2 α3 α4htrunk:trunk ∈ T.1branch:Branch α2 α3 α4hbranch:branch ∈ trunk.2twig:Twig α3 α4htwig:twig ∈ branch.2leaf:Leaf α4hleaf:leaf ∈ twig.2heq:(trunk.1, branch.1, twig.1, leaf.1) = x⊢ Leaf.leaf (f leaf.1) ∈ (Twig.uniqueMap4 f twig).2neg.heqα1:Typeα2:Typeα3:Typeα4:Typeinst✝:DecidableEq α4T:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4f:α4 → α4hnotMem:¬(x.1, x.2.1, x.2.2.1, f x.2.2.2) ∈ Ttrunk:Trunk α1 α2 α3 α4htrunk:trunk ∈ T.1branch:Branch α2 α3 α4hbranch:branch ∈ trunk.2twig:Twig α3 α4htwig:twig ∈ branch.2leaf:Leaf α4hleaf:leaf ∈ twig.2heq:(trunk.1, branch.1, twig.1, leaf.1) = x⊢ (x.1, x.2.1, x.2.2.1, f x.2.2.2) =
  ((Trunk.uniqueMap4 f trunk).1, (Branch.uniqueMap4 f branch).1, (Twig.uniqueMap4 f twig).1, (Leaf.leaf (f leaf.1)).1)
  ·neg.trunk_memα1:Typeα2:Typeα3:Typeα4:Typeinst✝:DecidableEq α4T:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4f:α4 → α4hnotMem:¬(x.1, x.2.1, x.2.2.1, f x.2.2.2) ∈ Ttrunk:Trunk α1 α2 α3 α4htrunk:trunk ∈ T.1branch:Branch α2 α3 α4hbranch:branch ∈ trunk.2twig:Twig α3 α4htwig:twig ∈ branch.2leaf:Leaf α4hleaf:leaf ∈ twig.2heq:(trunk.1, branch.1, twig.1, leaf.1) = x⊢ Trunk.uniqueMap4 f trunk ∈ (uniqueMap4 f T).1 exact Multiset.mem_map_of_mem _ htrunkAll goals completed! 🐙
  ·neg.branch_memα1:Typeα2:Typeα3:Typeα4:Typeinst✝:DecidableEq α4T:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4f:α4 → α4hnotMem:¬(x.1, x.2.1, x.2.2.1, f x.2.2.2) ∈ Ttrunk:Trunk α1 α2 α3 α4htrunk:trunk ∈ T.1branch:Branch α2 α3 α4hbranch:branch ∈ trunk.2twig:Twig α3 α4htwig:twig ∈ branch.2leaf:Leaf α4hleaf:leaf ∈ twig.2heq:(trunk.1, branch.1, twig.1, leaf.1) = x⊢ Branch.uniqueMap4 f branch ∈ (Trunk.uniqueMap4 f trunk).2 exact Multiset.mem_map_of_mem _ hbranchAll goals completed! 🐙
  ·neg.twig_memα1:Typeα2:Typeα3:Typeα4:Typeinst✝:DecidableEq α4T:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4f:α4 → α4hnotMem:¬(x.1, x.2.1, x.2.2.1, f x.2.2.2) ∈ Ttrunk:Trunk α1 α2 α3 α4htrunk:trunk ∈ T.1branch:Branch α2 α3 α4hbranch:branch ∈ trunk.2twig:Twig α3 α4htwig:twig ∈ branch.2leaf:Leaf α4hleaf:leaf ∈ twig.2heq:(trunk.1, branch.1, twig.1, leaf.1) = x⊢ Twig.uniqueMap4 f twig ∈ (Branch.uniqueMap4 f branch).2 exact Multiset.mem_map_of_mem _ htwigAll goals completed! 🐙
  ·neg.leaf_memα1:Typeα2:Typeα3:Typeα4:Typeinst✝:DecidableEq α4T:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4f:α4 → α4hnotMem:¬(x.1, x.2.1, x.2.2.1, f x.2.2.2) ∈ Ttrunk:Trunk α1 α2 α3 α4htrunk:trunk ∈ T.1branch:Branch α2 α3 α4hbranch:branch ∈ trunk.2twig:Twig α3 α4htwig:twig ∈ branch.2leaf:Leaf α4hleaf:leaf ∈ twig.2heq:(trunk.1, branch.1, twig.1, leaf.1) = x⊢ Leaf.leaf (f leaf.1) ∈ (Twig.uniqueMap4 f twig).2 simp [Twig.uniqueMap4, -existsAndEq]neg.leaf_memα1:Typeα2:Typeα3:Typeα4:Typeinst✝:DecidableEq α4T:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4f:α4 → α4hnotMem:¬(x.1, x.2.1, x.2.2.1, f x.2.2.2) ∈ Ttrunk:Trunk α1 α2 α3 α4htrunk:trunk ∈ T.1branch:Branch α2 α3 α4hbranch:branch ∈ trunk.2twig:Twig α3 α4htwig:twig ∈ branch.2leaf:Leaf α4hleaf:leaf ∈ twig.2heq:(trunk.1, branch.1, twig.1, leaf.1) = x⊢ ∃ a, a ∈ twig.2 ∧ (∀ (x : Leaf α4), x ∈ twig.2 → ¬x.1 = f a.1) ∧ f a.1 = f leaf.1
    refine ⟨leaf, hleaf, ?_, rfl⟩neg.leaf_memα1:Typeα2:Typeα3:Typeα4:Typeinst✝:DecidableEq α4T:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4f:α4 → α4hnotMem:¬(x.1, x.2.1, x.2.2.1, f x.2.2.2) ∈ Ttrunk:Trunk α1 α2 α3 α4htrunk:trunk ∈ T.1branch:Branch α2 α3 α4hbranch:branch ∈ trunk.2twig:Twig α3 α4htwig:twig ∈ branch.2leaf:Leaf α4hleaf:leaf ∈ twig.2heq:(trunk.1, branch.1, twig.1, leaf.1) = x⊢ ∀ (x : Leaf α4), x ∈ twig.2 → ¬x.1 = f leaf.1
    intro y hy hnneg.leaf_memα1:Typeα2:Typeα3:Typeα4:Typeinst✝:DecidableEq α4T:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4f:α4 → α4hnotMem:¬(x.1, x.2.1, x.2.2.1, f x.2.2.2) ∈ Ttrunk:Trunk α1 α2 α3 α4htrunk:trunk ∈ T.1branch:Branch α2 α3 α4hbranch:branch ∈ trunk.2twig:Twig α3 α4htwig:twig ∈ branch.2leaf:Leaf α4hleaf:leaf ∈ twig.2heq:(trunk.1, branch.1, twig.1, leaf.1) = xy:Leaf α4hy:y ∈ twig.2hn:y.1 = f leaf.1⊢ False
    exact hnotMem
      (mem_of_parts trunk branch twig y htrunk hbranch htwig hy (byα1:Typeα2:Typeα3:Typeα4:Typeinst✝:DecidableEq α4T:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4f:α4 → α4hnotMem:¬(x.1, x.2.1, x.2.2.1, f x.2.2.2) ∈ Ttrunk:Trunk α1 α2 α3 α4htrunk:trunk ∈ T.1branch:Branch α2 α3 α4hbranch:branch ∈ trunk.2twig:Twig α3 α4htwig:twig ∈ branch.2leaf:Leaf α4hleaf:leaf ∈ twig.2heq:(trunk.1, branch.1, twig.1, leaf.1) = xy:Leaf α4hy:y ∈ twig.2hn:y.1 = f leaf.1⊢ (x.1, x.2.1, x.2.2.1, f x.2.2.2) = (trunk.1, branch.1, twig.1, y.1) subst heqα1:Typeα2:Typeα3:Typeα4:Typeinst✝:DecidableEq α4T:FourTree α1 α2 α3 α4f:α4 → α4trunk:Trunk α1 α2 α3 α4htrunk:trunk ∈ T.1branch:Branch α2 α3 α4hbranch:branch ∈ trunk.2twig:Twig α3 α4htwig:twig ∈ branch.2leaf:Leaf α4hleaf:leaf ∈ twig.2y:Leaf α4hy:y ∈ twig.2hn:y.1 = f leaf.1hnotMem:¬((trunk.1, branch.1, twig.1, leaf.1).1, (trunk.1, branch.1, twig.1, leaf.1).2.1,
      (trunk.1, branch.1, twig.1, leaf.1).2.2.1, f (trunk.1, branch.1, twig.1, leaf.1).2.2.2) ∈
    T⊢ ((trunk.1, branch.1, twig.1, leaf.1).1, (trunk.1, branch.1, twig.1, leaf.1).2.1,
    (trunk.1, branch.1, twig.1, leaf.1).2.2.1, f (trunk.1, branch.1, twig.1, leaf.1).2.2.2) =
  (trunk.1, branch.1, twig.1, y.1); simp [hn]All goals completed! 🐙))
  ·neg.heqα1:Typeα2:Typeα3:Typeα4:Typeinst✝:DecidableEq α4T:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4f:α4 → α4hnotMem:¬(x.1, x.2.1, x.2.2.1, f x.2.2.2) ∈ Ttrunk:Trunk α1 α2 α3 α4htrunk:trunk ∈ T.1branch:Branch α2 α3 α4hbranch:branch ∈ trunk.2twig:Twig α3 α4htwig:twig ∈ branch.2leaf:Leaf α4hleaf:leaf ∈ twig.2heq:(trunk.1, branch.1, twig.1, leaf.1) = x⊢ (x.1, x.2.1, x.2.2.1, f x.2.2.2) =
  ((Trunk.uniqueMap4 f trunk).1, (Branch.uniqueMap4 f branch).1, (Twig.uniqueMap4 f twig).1, (Leaf.leaf (f leaf.1)).1) subst heqneg.heqα1:Typeα2:Typeα3:Typeα4:Typeinst✝:DecidableEq α4T:FourTree α1 α2 α3 α4f:α4 → α4trunk:Trunk α1 α2 α3 α4htrunk:trunk ∈ T.1branch:Branch α2 α3 α4hbranch:branch ∈ trunk.2twig:Twig α3 α4htwig:twig ∈ branch.2leaf:Leaf α4hleaf:leaf ∈ twig.2hnotMem:¬((trunk.1, branch.1, twig.1, leaf.1).1, (trunk.1, branch.1, twig.1, leaf.1).2.1,
      (trunk.1, branch.1, twig.1, leaf.1).2.2.1, f (trunk.1, branch.1, twig.1, leaf.1).2.2.2) ∈
    T⊢ ((trunk.1, branch.1, twig.1, leaf.1).1, (trunk.1, branch.1, twig.1, leaf.1).2.1,
    (trunk.1, branch.1, twig.1, leaf.1).2.2.1, f (trunk.1, branch.1, twig.1, leaf.1).2.2.2) =
  ((Trunk.uniqueMap4 f trunk).1, (Branch.uniqueMap4 f branch).1, (Twig.uniqueMap4 f twig).1, (Leaf.leaf (f leaf.1)).1)
    simp [Trunk.uniqueMap4, Branch.uniqueMap4, Twig.uniqueMap4]All goals completed! 🐙



lemma exists_of_mem_uniqueMap4 {T : FourTree α1 α2 α3 α4}
    (C : α1 × α2 × α3 × α4) (h : C ∈ T.uniqueMap4 f) :
    ∃ qHd qHu Q5 Q10, C = (qHd, qHu, Q5, f Q10) ∧ (qHd, qHu, Q5, Q10) ∈ T := byα1:Typeα2:Typeα3:Typeα4:Typeinst✝:DecidableEq α4f:α4 → α4T:FourTree α1 α2 α3 α4C:α1 × α2 × α3 × α4h:C ∈ uniqueMap4 f T⊢ ∃ qHd qHu Q5 Q10, C = (qHd, qHu, Q5, f Q10) ∧ (qHd, qHu, Q5, Q10) ∈ T
  rw [mem_iff_mem_toMultisetα1:Typeα2:Typeα3:Typeα4:Typeinst✝:DecidableEq α4f:α4 → α4T:FourTree α1 α2 α3 α4C:α1 × α2 × α3 × α4h:C ∈ (uniqueMap4 f T).toMultiset⊢ ∃ qHd qHu Q5 Q10, C = (qHd, qHu, Q5, f Q10) ∧ (qHd, qHu, Q5, Q10) ∈ Tα1:Typeα2:Typeα3:Typeα4:Typeinst✝:DecidableEq α4f:α4 → α4T:FourTree α1 α2 α3 α4C:α1 × α2 × α3 × α4h:C ∈ (uniqueMap4 f T).toMultiset⊢ ∃ qHd qHu Q5 Q10, C = (qHd, qHu, Q5, f Q10) ∧ (qHd, qHu, Q5, Q10) ∈ T] at hα1:Typeα2:Typeα3:Typeα4:Typeinst✝:DecidableEq α4f:α4 → α4T:FourTree α1 α2 α3 α4C:α1 × α2 × α3 × α4h:C ∈ (uniqueMap4 f T).toMultiset⊢ ∃ qHd qHu Q5 Q10, C = (qHd, qHu, Q5, f Q10) ∧ (qHd, qHu, Q5, Q10) ∈ T
  simp [toMultiset] at hα1:Typeα2:Typeα3:Typeα4:Typeinst✝:DecidableEq α4f:α4 → α4T:FourTree α1 α2 α3 α4C:α1 × α2 × α3 × α4h:∃ a,
  a ∈ (uniqueMap4 f T).1 ∧ ∃ a_1, a_1 ∈ a.2 ∧ ∃ a_2, a_2 ∈ a_1.2 ∧ ∃ a_3, a_3 ∈ a_2.2 ∧ (a.1, a_1.1, a_2.1, a_3.1) = C⊢ ∃ qHd qHu Q5 Q10, C = (qHd, qHu, Q5, f Q10) ∧ (qHd, qHu, Q5, Q10) ∈ T
  obtain ⟨trunkI, trunkI_mem, branchI, branchI_mem, twigI, twigI_mem,
    leafI, leafI_mem, heq⟩ := hα1:Typeα2:Typeα3:Typeα4:Typeinst✝:DecidableEq α4f:α4 → α4T:FourTree α1 α2 α3 α4C:α1 × α2 × α3 × α4trunkI:Trunk α1 α2 α3 α4trunkI_mem:trunkI ∈ (uniqueMap4 f T).1branchI:Branch α2 α3 α4branchI_mem:branchI ∈ trunkI.2twigI:Twig α3 α4twigI_mem:twigI ∈ branchI.2leafI:Leaf α4leafI_mem:leafI ∈ twigI.2heq:(trunkI.1, branchI.1, twigI.1, leafI.1) = C⊢ ∃ qHd qHu Q5 Q10, C = (qHd, qHu, Q5, f Q10) ∧ (qHd, qHu, Q5, Q10) ∈ T
  -- obtaining trunkT
  simp [uniqueMap4] at trunkI_memα1:Typeα2:Typeα3:Typeα4:Typeinst✝:DecidableEq α4f:α4 → α4T:FourTree α1 α2 α3 α4C:α1 × α2 × α3 × α4trunkI:Trunk α1 α2 α3 α4branchI:Branch α2 α3 α4branchI_mem:branchI ∈ trunkI.2twigI:Twig α3 α4twigI_mem:twigI ∈ branchI.2leafI:Leaf α4leafI_mem:leafI ∈ twigI.2heq:(trunkI.1, branchI.1, twigI.1, leafI.1) = CtrunkI_mem:∃ a, a ∈ T.1 ∧ Trunk.uniqueMap4 f a = trunkI⊢ ∃ qHd qHu Q5 Q10, C = (qHd, qHu, Q5, f Q10) ∧ (qHd, qHu, Q5, Q10) ∈ T
  obtain ⟨trunkT, trunkT_mem, rfl⟩ := trunkI_memα1:Typeα2:Typeα3:Typeα4:Typeinst✝:DecidableEq α4f:α4 → α4T:FourTree α1 α2 α3 α4C:α1 × α2 × α3 × α4branchI:Branch α2 α3 α4twigI:Twig α3 α4twigI_mem:twigI ∈ branchI.2leafI:Leaf α4leafI_mem:leafI ∈ twigI.2trunkT:Trunk α1 α2 α3 α4trunkT_mem:trunkT ∈ T.1branchI_mem:branchI ∈ (Trunk.uniqueMap4 f trunkT).2heq:((Trunk.uniqueMap4 f trunkT).1, branchI.1, twigI.1, leafI.1) = C⊢ ∃ qHd qHu Q5 Q10, C = (qHd, qHu, Q5, f Q10) ∧ (qHd, qHu, Q5, Q10) ∈ T
  -- obtaining branchT
  simp [Trunk.uniqueMap4] at branchI_memα1:Typeα2:Typeα3:Typeα4:Typeinst✝:DecidableEq α4f:α4 → α4T:FourTree α1 α2 α3 α4C:α1 × α2 × α3 × α4branchI:Branch α2 α3 α4twigI:Twig α3 α4twigI_mem:twigI ∈ branchI.2leafI:Leaf α4leafI_mem:leafI ∈ twigI.2trunkT:Trunk α1 α2 α3 α4trunkT_mem:trunkT ∈ T.1heq:((Trunk.uniqueMap4 f trunkT).1, branchI.1, twigI.1, leafI.1) = CbranchI_mem:∃ a, a ∈ trunkT.2 ∧ Branch.uniqueMap4 f a = branchI⊢ ∃ qHd qHu Q5 Q10, C = (qHd, qHu, Q5, f Q10) ∧ (qHd, qHu, Q5, Q10) ∈ T
  obtain ⟨branchT, branchT_mem, rfl⟩ := branchI_memα1:Typeα2:Typeα3:Typeα4:Typeinst✝:DecidableEq α4f:α4 → α4T:FourTree α1 α2 α3 α4C:α1 × α2 × α3 × α4twigI:Twig α3 α4leafI:Leaf α4leafI_mem:leafI ∈ twigI.2trunkT:Trunk α1 α2 α3 α4trunkT_mem:trunkT ∈ T.1branchT:Branch α2 α3 α4branchT_mem:branchT ∈ trunkT.2twigI_mem:twigI ∈ (Branch.uniqueMap4 f branchT).2heq:((Trunk.uniqueMap4 f trunkT).1, (Branch.uniqueMap4 f branchT).1, twigI.1, leafI.1) = C⊢ ∃ qHd qHu Q5 Q10, C = (qHd, qHu, Q5, f Q10) ∧ (qHd, qHu, Q5, Q10) ∈ T
  -- obtaining twigT
  simp only [Branch.uniqueMap4, Multiset.mem_map] at twigI_memα1:Typeα2:Typeα3:Typeα4:Typeinst✝:DecidableEq α4f:α4 → α4T:FourTree α1 α2 α3 α4C:α1 × α2 × α3 × α4twigI:Twig α3 α4leafI:Leaf α4leafI_mem:leafI ∈ twigI.2trunkT:Trunk α1 α2 α3 α4trunkT_mem:trunkT ∈ T.1branchT:Branch α2 α3 α4branchT_mem:branchT ∈ trunkT.2heq:((Trunk.uniqueMap4 f trunkT).1, (Branch.uniqueMap4 f branchT).1, twigI.1, leafI.1) = CtwigI_mem:∃ a, a ∈ branchT.2 ∧ Twig.uniqueMap4 f a = twigI⊢ ∃ qHd qHu Q5 Q10, C = (qHd, qHu, Q5, f Q10) ∧ (qHd, qHu, Q5, Q10) ∈ T
  obtain ⟨twigT, twigT_mem, rfl⟩ := twigI_memα1:Typeα2:Typeα3:Typeα4:Typeinst✝:DecidableEq α4f:α4 → α4T:FourTree α1 α2 α3 α4C:α1 × α2 × α3 × α4leafI:Leaf α4trunkT:Trunk α1 α2 α3 α4trunkT_mem:trunkT ∈ T.1branchT:Branch α2 α3 α4branchT_mem:branchT ∈ trunkT.2twigT:Twig α3 α4twigT_mem:twigT ∈ branchT.2leafI_mem:leafI ∈ (Twig.uniqueMap4 f twigT).2heq:((Trunk.uniqueMap4 f trunkT).1, (Branch.uniqueMap4 f branchT).1, (Twig.uniqueMap4 f twigT).1, leafI.1) = C⊢ ∃ qHd qHu Q5 Q10, C = (qHd, qHu, Q5, f Q10) ∧ (qHd, qHu, Q5, Q10) ∈ T
  -- obtaining leafT
  simp only [Twig.uniqueMap4, Multiset.mem_map, Multiset.mem_filterMap,
    Option.ite_none_right_eq_some, Option.some.injEq, exists_exists_and_eq_and] at leafI_memα1:Typeα2:Typeα3:Typeα4:Typeinst✝:DecidableEq α4f:α4 → α4T:FourTree α1 α2 α3 α4C:α1 × α2 × α3 × α4leafI:Leaf α4trunkT:Trunk α1 α2 α3 α4trunkT_mem:trunkT ∈ T.1branchT:Branch α2 α3 α4branchT_mem:branchT ∈ trunkT.2twigT:Twig α3 α4twigT_mem:twigT ∈ branchT.2heq:((Trunk.uniqueMap4 f trunkT).1, (Branch.uniqueMap4 f branchT).1, (Twig.uniqueMap4 f twigT).1, leafI.1) = CleafI_mem:∃ a, (∃ a_1, a_1 ∈ twigT.2 ∧ (¬∃ a, a ∈ twigT.2 ∧ a.1 = f a_1.1) ∧ f a_1.1 = a) ∧ Leaf.leaf a = leafI⊢ ∃ qHd qHu Q5 Q10, C = (qHd, qHu, Q5, f Q10) ∧ (qHd, qHu, Q5, Q10) ∈ T
  obtain ⟨Q10, ⟨leafT, leafT_mem, hQ10⟩, hPresent⟩ := leafI_memα1:Typeα2:Typeα3:Typeα4:Typeinst✝:DecidableEq α4f:α4 → α4T:FourTree α1 α2 α3 α4C:α1 × α2 × α3 × α4leafI:Leaf α4trunkT:Trunk α1 α2 α3 α4trunkT_mem:trunkT ∈ T.1branchT:Branch α2 α3 α4branchT_mem:branchT ∈ trunkT.2twigT:Twig α3 α4twigT_mem:twigT ∈ branchT.2heq:((Trunk.uniqueMap4 f trunkT).1, (Branch.uniqueMap4 f branchT).1, (Twig.uniqueMap4 f twigT).1, leafI.1) = CQ10:α4hPresent:Leaf.leaf Q10 = leafIleafT:Leaf α4leafT_mem:leafT ∈ twigT.2hQ10:(¬∃ a, a ∈ twigT.2 ∧ a.1 = f leafT.1) ∧ f leafT.1 = Q10⊢ ∃ qHd qHu Q5 Q10, C = (qHd, qHu, Q5, f Q10) ∧ (qHd, qHu, Q5, Q10) ∈ T
  subst heqα1:Typeα2:Typeα3:Typeα4:Typeinst✝:DecidableEq α4f:α4 → α4T:FourTree α1 α2 α3 α4leafI:Leaf α4trunkT:Trunk α1 α2 α3 α4trunkT_mem:trunkT ∈ T.1branchT:Branch α2 α3 α4branchT_mem:branchT ∈ trunkT.2twigT:Twig α3 α4twigT_mem:twigT ∈ branchT.2Q10:α4hPresent:Leaf.leaf Q10 = leafIleafT:Leaf α4leafT_mem:leafT ∈ twigT.2hQ10:(¬∃ a, a ∈ twigT.2 ∧ a.1 = f leafT.1) ∧ f leafT.1 = Q10⊢ ∃ qHd qHu Q5 Q10,
  ((Trunk.uniqueMap4 f trunkT).1, (Branch.uniqueMap4 f branchT).1, (Twig.uniqueMap4 f twigT).1, leafI.1) =
      (qHd, qHu, Q5, f Q10) ∧
    (qHd, qHu, Q5, Q10) ∈ T
  refine ⟨trunkT.1, branchT.1, twigT.1, leafT.1, ?_,
    mem_of_parts trunkT branchT twigT leafT trunkT_mem branchT_mem twigT_mem leafT_mem rfl⟩α1:Typeα2:Typeα3:Typeα4:Typeinst✝:DecidableEq α4f:α4 → α4T:FourTree α1 α2 α3 α4leafI:Leaf α4trunkT:Trunk α1 α2 α3 α4trunkT_mem:trunkT ∈ T.1branchT:Branch α2 α3 α4branchT_mem:branchT ∈ trunkT.2twigT:Twig α3 α4twigT_mem:twigT ∈ branchT.2Q10:α4hPresent:Leaf.leaf Q10 = leafIleafT:Leaf α4leafT_mem:leafT ∈ twigT.2hQ10:(¬∃ a, a ∈ twigT.2 ∧ a.1 = f leafT.1) ∧ f leafT.1 = Q10⊢ ((Trunk.uniqueMap4 f trunkT).1, (Branch.uniqueMap4 f branchT).1, (Twig.uniqueMap4 f twigT).1, leafI.1) =
  (trunkT.1, branchT.1, twigT.1, f leafT.1)
  rw [← hPresentα1:Typeα2:Typeα3:Typeα4:Typeinst✝:DecidableEq α4f:α4 → α4T:FourTree α1 α2 α3 α4leafI:Leaf α4trunkT:Trunk α1 α2 α3 α4trunkT_mem:trunkT ∈ T.1branchT:Branch α2 α3 α4branchT_mem:branchT ∈ trunkT.2twigT:Twig α3 α4twigT_mem:twigT ∈ branchT.2Q10:α4hPresent:Leaf.leaf Q10 = leafIleafT:Leaf α4leafT_mem:leafT ∈ twigT.2hQ10:(¬∃ a, a ∈ twigT.2 ∧ a.1 = f leafT.1) ∧ f leafT.1 = Q10⊢ ((Trunk.uniqueMap4 f trunkT).1, (Branch.uniqueMap4 f branchT).1, (Twig.uniqueMap4 f twigT).1, (Leaf.leaf Q10).1) =
  (trunkT.1, branchT.1, twigT.1, f leafT.1)α1:Typeα2:Typeα3:Typeα4:Typeinst✝:DecidableEq α4f:α4 → α4T:FourTree α1 α2 α3 α4leafI:Leaf α4trunkT:Trunk α1 α2 α3 α4trunkT_mem:trunkT ∈ T.1branchT:Branch α2 α3 α4branchT_mem:branchT ∈ trunkT.2twigT:Twig α3 α4twigT_mem:twigT ∈ branchT.2Q10:α4hPresent:Leaf.leaf Q10 = leafIleafT:Leaf α4leafT_mem:leafT ∈ twigT.2hQ10:(¬∃ a, a ∈ twigT.2 ∧ a.1 = f leafT.1) ∧ f leafT.1 = Q10⊢ ((Trunk.uniqueMap4 f trunkT).1, (Branch.uniqueMap4 f branchT).1, (Twig.uniqueMap4 f twigT).1, (Leaf.leaf Q10).1) =
  (trunkT.1, branchT.1, twigT.1, f leafT.1)]α1:Typeα2:Typeα3:Typeα4:Typeinst✝:DecidableEq α4f:α4 → α4T:FourTree α1 α2 α3 α4leafI:Leaf α4trunkT:Trunk α1 α2 α3 α4trunkT_mem:trunkT ∈ T.1branchT:Branch α2 α3 α4branchT_mem:branchT ∈ trunkT.2twigT:Twig α3 α4twigT_mem:twigT ∈ branchT.2Q10:α4hPresent:Leaf.leaf Q10 = leafIleafT:Leaf α4leafT_mem:leafT ∈ twigT.2hQ10:(¬∃ a, a ∈ twigT.2 ∧ a.1 = f leafT.1) ∧ f leafT.1 = Q10⊢ ((Trunk.uniqueMap4 f trunkT).1, (Branch.uniqueMap4 f branchT).1, (Twig.uniqueMap4 f twigT).1, (Leaf.leaf Q10).1) =
  (trunkT.1, branchT.1, twigT.1, f leafT.1)
  simp [Trunk.uniqueMap4, Branch.uniqueMap4, Twig.uniqueMap4, hQ10.2]All goals completed! 🐙

uniqueMap3

Given a map f : α3 → α3 the map from Twig α3 α4 → Twig α3 α4 mapping the underlying first value of the twig.

def Twig.uniqueMap3 (T : Twig α3 α4) : Twig α3 α4 :=
  match T with
  | .twig xs leafs => .twig (f xs) leafs

Given a map f : α3 → α3 the map from Branch α2 α3 α4 → Branch α2 α3 α4 mapping the underlying first value of the twig, and deleting any new leafs that appeared in the old branch.

def Branch.uniqueMap3 (T : Branch α2 α3 α4) : Branch α2 α3 α4 :=
  match T with
  | .branch qHu twigs =>
    let insertTwigs := twigs.map (fun (.twig Q5 leafs) => Twig.twig (f Q5)
      (leafs.filter (fun (.leaf Q10) => ¬ Branch.mem (.branch qHu twigs)
      (qHu, (f Q5), Q10))))
    .branch qHu insertTwigs

Given a map f : α3 → α3 the map from Trunk α1 α2 α3 α4 → Trunk α1 α2 α3 α4 mapping the underlying first value of the twig, and deleting any new leafs that appeared in the old branch.

def Trunk.uniqueMap3 (T : Trunk α1 α2 α3 α4) : Trunk α1 α2 α3 α4 :=
  match T with
  | .trunk qHd branches =>
    .trunk qHd (branches.map fun bs => (bs.uniqueMap3 f))

Given a map f : α3 → α3 the map from FourTree α1 α2 α3 α4 → FourTree α1 α2 α3 α4 mapping the underlying first value of the twig, and deleting any new leafs that appeared in the old branch.

def uniqueMap3 (T : FourTree α1 α2 α3 α4) : FourTree α1 α2 α3 α4:=
  match T with
  | .root trunks =>
    .root (trunks.map fun ts => (ts.uniqueMap3 f))

lemma map_mem_uniqueMap3 {T : FourTree α1 α2 α3 α4}
    (x : α1 × α2 × α3 × α4) (hx : x ∈ T) (f : α3 → α3) :
    (x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ T.uniqueMap3 f ∨
    (x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ T := byα1:Typeα2:Typeα3:Typeα4:Typeinst✝²:DecidableEq α2inst✝¹:DecidableEq α3inst✝:DecidableEq α4T:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4hx:x ∈ Tf:α3 → α3⊢ (x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ uniqueMap3 f T ∨ (x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ T
  by_cases hnotMem : (x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ Tposα1:Typeα2:Typeα3:Typeα4:Typeinst✝²:DecidableEq α2inst✝¹:DecidableEq α3inst✝:DecidableEq α4T:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4hx:x ∈ Tf:α3 → α3hnotMem:(x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ T⊢ (x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ uniqueMap3 f T ∨ (x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ Tnegα1:Typeα2:Typeα3:Typeα4:Typeinst✝²:DecidableEq α2inst✝¹:DecidableEq α3inst✝:DecidableEq α4T:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4hx:x ∈ Tf:α3 → α3hnotMem:¬(x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ T⊢ (x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ uniqueMap3 f T ∨ (x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ T
  ·posα1:Typeα2:Typeα3:Typeα4:Typeinst✝²:DecidableEq α2inst✝¹:DecidableEq α3inst✝:DecidableEq α4T:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4hx:x ∈ Tf:α3 → α3hnotMem:(x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ T⊢ (x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ uniqueMap3 f T ∨ (x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ T simp [hnotMem]All goals completed! 🐙
  leftnegα1:Typeα2:Typeα3:Typeα4:Typeinst✝²:DecidableEq α2inst✝¹:DecidableEq α3inst✝:DecidableEq α4T:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4hx:x ∈ Tf:α3 → α3hnotMem:¬(x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ T⊢ (x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ uniqueMap3 f T
  simp [mem_iff_mem_toMultiset, toMultiset] at hxnegα1:Typeα2:Typeα3:Typeα4:Typeinst✝²:DecidableEq α2inst✝¹:DecidableEq α3inst✝:DecidableEq α4T:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4f:α3 → α3hnotMem:¬(x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ Thx:∃ a, a ∈ T.1 ∧ ∃ a_1, a_1 ∈ a.2 ∧ ∃ a_2, a_2 ∈ a_1.2 ∧ ∃ a_3, a_3 ∈ a_2.2 ∧ (a.1, a_1.1, a_2.1, a_3.1) = x⊢ (x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ uniqueMap3 f T
  obtain ⟨trunk, htrunk, branch, hbranch, twig, htwig, leaf, hleaf, heq⟩ := hxnegα1:Typeα2:Typeα3:Typeα4:Typeinst✝²:DecidableEq α2inst✝¹:DecidableEq α3inst✝:DecidableEq α4T:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4f:α3 → α3hnotMem:¬(x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ Ttrunk:Trunk α1 α2 α3 α4htrunk:trunk ∈ T.1branch:Branch α2 α3 α4hbranch:branch ∈ trunk.2twig:Twig α3 α4htwig:twig ∈ branch.2leaf:Leaf α4hleaf:leaf ∈ twig.2heq:(trunk.1, branch.1, twig.1, leaf.1) = x⊢ (x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ uniqueMap3 f T
  match branch with
  | .branch qHu twigs =>α1:Typeα2:Typeα3:Typeα4:Typeinst✝²:DecidableEq α2inst✝¹:DecidableEq α3inst✝:DecidableEq α4T:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4f:α3 → α3hnotMem:¬(x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ Ttrunk:Trunk α1 α2 α3 α4htrunk:trunk ∈ T.1branch:Branch α2 α3 α4twig:Twig α3 α4leaf:Leaf α4hleaf:leaf ∈ twig.2qHu:α2twigs:Multiset (Twig α3 α4)hbranch:Branch.branch qHu twigs ∈ trunk.2htwig:twig ∈ (Branch.branch qHu twigs).2heq:(trunk.1, (Branch.branch qHu twigs).1, twig.1, leaf.1) = x⊢ (x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ uniqueMap3 f T
  match twig with
  | .twig Q5 leafs =>α1:Typeα2:Typeα3:Typeα4:Typeinst✝²:DecidableEq α2inst✝¹:DecidableEq α3inst✝:DecidableEq α4T:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4f:α3 → α3hnotMem:¬(x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ Ttrunk:Trunk α1 α2 α3 α4htrunk:trunk ∈ T.1branch:Branch α2 α3 α4twig:Twig α3 α4leaf:Leaf α4qHu:α2twigs:Multiset (Twig α3 α4)hbranch:Branch.branch qHu twigs ∈ trunk.2Q5:α3leafs:Multiset (Leaf α4)hleaf:leaf ∈ (Twig.twig Q5 leafs).2htwig:Twig.twig Q5 leafs ∈ (Branch.branch qHu twigs).2heq:(trunk.1, (Branch.branch qHu twigs).1, (Twig.twig Q5 leafs).1, leaf.1) = x⊢ (x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ uniqueMap3 f T
  apply mem_of_parts (trunk.uniqueMap3 f) ((Branch.branch qHu twigs).uniqueMap3 f)
    (.twig (f Q5) (leafs.filter (fun (.leaf Q10) =>
      ¬ Branch.mem (.branch qHu twigs) (qHu, f Q5, Q10)))) leaftrunk_memα1:Typeα2:Typeα3:Typeα4:Typeinst✝²:DecidableEq α2inst✝¹:DecidableEq α3inst✝:DecidableEq α4T:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4f:α3 → α3hnotMem:¬(x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ Ttrunk:Trunk α1 α2 α3 α4htrunk:trunk ∈ T.1branch:Branch α2 α3 α4twig:Twig α3 α4leaf:Leaf α4qHu:α2twigs:Multiset (Twig α3 α4)hbranch:Branch.branch qHu twigs ∈ trunk.2Q5:α3leafs:Multiset (Leaf α4)hleaf:leaf ∈ (Twig.twig Q5 leafs).2htwig:Twig.twig Q5 leafs ∈ (Branch.branch qHu twigs).2heq:(trunk.1, (Branch.branch qHu twigs).1, (Twig.twig Q5 leafs).1, leaf.1) = x⊢ Trunk.uniqueMap3 f trunk ∈ (uniqueMap3 f T).1branch_memα1:Typeα2:Typeα3:Typeα4:Typeinst✝²:DecidableEq α2inst✝¹:DecidableEq α3inst✝:DecidableEq α4T:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4f:α3 → α3hnotMem:¬(x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ Ttrunk:Trunk α1 α2 α3 α4htrunk:trunk ∈ T.1branch:Branch α2 α3 α4twig:Twig α3 α4leaf:Leaf α4qHu:α2twigs:Multiset (Twig α3 α4)hbranch:Branch.branch qHu twigs ∈ trunk.2Q5:α3leafs:Multiset (Leaf α4)hleaf:leaf ∈ (Twig.twig Q5 leafs).2htwig:Twig.twig Q5 leafs ∈ (Branch.branch qHu twigs).2heq:(trunk.1, (Branch.branch qHu twigs).1, (Twig.twig Q5 leafs).1, leaf.1) = x⊢ Branch.uniqueMap3 f (Branch.branch qHu twigs) ∈ (Trunk.uniqueMap3 f trunk).2twig_memα1:Typeα2:Typeα3:Typeα4:Typeinst✝²:DecidableEq α2inst✝¹:DecidableEq α3inst✝:DecidableEq α4T:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4f:α3 → α3hnotMem:¬(x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ Ttrunk:Trunk α1 α2 α3 α4htrunk:trunk ∈ T.1branch:Branch α2 α3 α4twig:Twig α3 α4leaf:Leaf α4qHu:α2twigs:Multiset (Twig α3 α4)hbranch:Branch.branch qHu twigs ∈ trunk.2Q5:α3leafs:Multiset (Leaf α4)hleaf:leaf ∈ (Twig.twig Q5 leafs).2htwig:Twig.twig Q5 leafs ∈ (Branch.branch qHu twigs).2heq:(trunk.1, (Branch.branch qHu twigs).1, (Twig.twig Q5 leafs).1, leaf.1) = x⊢ Twig.twig (f Q5)
    (Multiset.filter
      (fun x =>
        match x with
        | Leaf.leaf Q10 => ¬(Branch.branch qHu twigs).mem (qHu, f Q5, Q10))
      leafs) ∈
  (Branch.uniqueMap3 f (Branch.branch qHu twigs)).2leaf_memα1:Typeα2:Typeα3:Typeα4:Typeinst✝²:DecidableEq α2inst✝¹:DecidableEq α3inst✝:DecidableEq α4T:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4f:α3 → α3hnotMem:¬(x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ Ttrunk:Trunk α1 α2 α3 α4htrunk:trunk ∈ T.1branch:Branch α2 α3 α4twig:Twig α3 α4leaf:Leaf α4qHu:α2twigs:Multiset (Twig α3 α4)hbranch:Branch.branch qHu twigs ∈ trunk.2Q5:α3leafs:Multiset (Leaf α4)hleaf:leaf ∈ (Twig.twig Q5 leafs).2htwig:Twig.twig Q5 leafs ∈ (Branch.branch qHu twigs).2heq:(trunk.1, (Branch.branch qHu twigs).1, (Twig.twig Q5 leafs).1, leaf.1) = x⊢ leaf ∈
  (Twig.twig (f Q5)
      (Multiset.filter
        (fun x =>
          match x with
          | Leaf.leaf Q10 => ¬(Branch.branch qHu twigs).mem (qHu, f Q5, Q10))
        leafs)).2heqα1:Typeα2:Typeα3:Typeα4:Typeinst✝²:DecidableEq α2inst✝¹:DecidableEq α3inst✝:DecidableEq α4T:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4f:α3 → α3hnotMem:¬(x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ Ttrunk:Trunk α1 α2 α3 α4htrunk:trunk ∈ T.1branch:Branch α2 α3 α4twig:Twig α3 α4leaf:Leaf α4qHu:α2twigs:Multiset (Twig α3 α4)hbranch:Branch.branch qHu twigs ∈ trunk.2Q5:α3leafs:Multiset (Leaf α4)hleaf:leaf ∈ (Twig.twig Q5 leafs).2htwig:Twig.twig Q5 leafs ∈ (Branch.branch qHu twigs).2heq:(trunk.1, (Branch.branch qHu twigs).1, (Twig.twig Q5 leafs).1, leaf.1) = x⊢ (x.1, x.2.1, f x.2.2.1, x.2.2.2) =
  ((Trunk.uniqueMap3 f trunk).1, (Branch.uniqueMap3 f (Branch.branch qHu twigs)).1,
    (Twig.twig (f Q5)
        (Multiset.filter
          (fun x =>
            match x with
            | Leaf.leaf Q10 => ¬(Branch.branch qHu twigs).mem (qHu, f Q5, Q10))
          leafs)).1,
    leaf.1)
  ·trunk_memα1:Typeα2:Typeα3:Typeα4:Typeinst✝²:DecidableEq α2inst✝¹:DecidableEq α3inst✝:DecidableEq α4T:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4f:α3 → α3hnotMem:¬(x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ Ttrunk:Trunk α1 α2 α3 α4htrunk:trunk ∈ T.1branch:Branch α2 α3 α4twig:Twig α3 α4leaf:Leaf α4qHu:α2twigs:Multiset (Twig α3 α4)hbranch:Branch.branch qHu twigs ∈ trunk.2Q5:α3leafs:Multiset (Leaf α4)hleaf:leaf ∈ (Twig.twig Q5 leafs).2htwig:Twig.twig Q5 leafs ∈ (Branch.branch qHu twigs).2heq:(trunk.1, (Branch.branch qHu twigs).1, (Twig.twig Q5 leafs).1, leaf.1) = x⊢ Trunk.uniqueMap3 f trunk ∈ (uniqueMap3 f T).1 exact Multiset.mem_map_of_mem _ htrunkAll goals completed! 🐙
  ·branch_memα1:Typeα2:Typeα3:Typeα4:Typeinst✝²:DecidableEq α2inst✝¹:DecidableEq α3inst✝:DecidableEq α4T:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4f:α3 → α3hnotMem:¬(x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ Ttrunk:Trunk α1 α2 α3 α4htrunk:trunk ∈ T.1branch:Branch α2 α3 α4twig:Twig α3 α4leaf:Leaf α4qHu:α2twigs:Multiset (Twig α3 α4)hbranch:Branch.branch qHu twigs ∈ trunk.2Q5:α3leafs:Multiset (Leaf α4)hleaf:leaf ∈ (Twig.twig Q5 leafs).2htwig:Twig.twig Q5 leafs ∈ (Branch.branch qHu twigs).2heq:(trunk.1, (Branch.branch qHu twigs).1, (Twig.twig Q5 leafs).1, leaf.1) = x⊢ Branch.uniqueMap3 f (Branch.branch qHu twigs) ∈ (Trunk.uniqueMap3 f trunk).2 exact Multiset.mem_map_of_mem _ hbranchAll goals completed! 🐙
  ·twig_memα1:Typeα2:Typeα3:Typeα4:Typeinst✝²:DecidableEq α2inst✝¹:DecidableEq α3inst✝:DecidableEq α4T:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4f:α3 → α3hnotMem:¬(x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ Ttrunk:Trunk α1 α2 α3 α4htrunk:trunk ∈ T.1branch:Branch α2 α3 α4twig:Twig α3 α4leaf:Leaf α4qHu:α2twigs:Multiset (Twig α3 α4)hbranch:Branch.branch qHu twigs ∈ trunk.2Q5:α3leafs:Multiset (Leaf α4)hleaf:leaf ∈ (Twig.twig Q5 leafs).2htwig:Twig.twig Q5 leafs ∈ (Branch.branch qHu twigs).2heq:(trunk.1, (Branch.branch qHu twigs).1, (Twig.twig Q5 leafs).1, leaf.1) = x⊢ Twig.twig (f Q5)
    (Multiset.filter
      (fun x =>
        match x with
        | Leaf.leaf Q10 => ¬(Branch.branch qHu twigs).mem (qHu, f Q5, Q10))
      leafs) ∈
  (Branch.uniqueMap3 f (Branch.branch qHu twigs)).2 exact Multiset.mem_map_of_mem _ htwigAll goals completed! 🐙
  ·leaf_memα1:Typeα2:Typeα3:Typeα4:Typeinst✝²:DecidableEq α2inst✝¹:DecidableEq α3inst✝:DecidableEq α4T:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4f:α3 → α3hnotMem:¬(x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ Ttrunk:Trunk α1 α2 α3 α4htrunk:trunk ∈ T.1branch:Branch α2 α3 α4twig:Twig α3 α4leaf:Leaf α4qHu:α2twigs:Multiset (Twig α3 α4)hbranch:Branch.branch qHu twigs ∈ trunk.2Q5:α3leafs:Multiset (Leaf α4)hleaf:leaf ∈ (Twig.twig Q5 leafs).2htwig:Twig.twig Q5 leafs ∈ (Branch.branch qHu twigs).2heq:(trunk.1, (Branch.branch qHu twigs).1, (Twig.twig Q5 leafs).1, leaf.1) = x⊢ leaf ∈
  (Twig.twig (f Q5)
      (Multiset.filter
        (fun x =>
          match x with
          | Leaf.leaf Q10 => ¬(Branch.branch qHu twigs).mem (qHu, f Q5, Q10))
        leafs)).2 refine Multiset.mem_filter.mpr ⟨hleaf, ?_⟩leaf_memα1:Typeα2:Typeα3:Typeα4:Typeinst✝²:DecidableEq α2inst✝¹:DecidableEq α3inst✝:DecidableEq α4T:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4f:α3 → α3hnotMem:¬(x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ Ttrunk:Trunk α1 α2 α3 α4htrunk:trunk ∈ T.1branch:Branch α2 α3 α4twig:Twig α3 α4leaf:Leaf α4qHu:α2twigs:Multiset (Twig α3 α4)hbranch:Branch.branch qHu twigs ∈ trunk.2Q5:α3leafs:Multiset (Leaf α4)hleaf:leaf ∈ (Twig.twig Q5 leafs).2htwig:Twig.twig Q5 leafs ∈ (Branch.branch qHu twigs).2heq:(trunk.1, (Branch.branch qHu twigs).1, (Twig.twig Q5 leafs).1, leaf.1) = x⊢ match leaf with
| Leaf.leaf Q10 => ¬(Branch.branch qHu twigs).mem (qHu, f Q5, Q10)
    show ¬ (Branch.branch qHu twigs).mem (qHu, f Q5, leaf.1)leaf_memα1:Typeα2:Typeα3:Typeα4:Typeinst✝²:DecidableEq α2inst✝¹:DecidableEq α3inst✝:DecidableEq α4T:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4f:α3 → α3hnotMem:¬(x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ Ttrunk:Trunk α1 α2 α3 α4htrunk:trunk ∈ T.1branch:Branch α2 α3 α4twig:Twig α3 α4leaf:Leaf α4qHu:α2twigs:Multiset (Twig α3 α4)hbranch:Branch.branch qHu twigs ∈ trunk.2Q5:α3leafs:Multiset (Leaf α4)hleaf:leaf ∈ (Twig.twig Q5 leafs).2htwig:Twig.twig Q5 leafs ∈ (Branch.branch qHu twigs).2heq:(trunk.1, (Branch.branch qHu twigs).1, (Twig.twig Q5 leafs).1, leaf.1) = x⊢ ¬(Branch.branch qHu twigs).mem (qHu, f Q5, leaf.1)
    by_contra hnleaf_memα1:Typeα2:Typeα3:Typeα4:Typeinst✝²:DecidableEq α2inst✝¹:DecidableEq α3inst✝:DecidableEq α4T:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4f:α3 → α3hnotMem:¬(x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ Ttrunk:Trunk α1 α2 α3 α4htrunk:trunk ∈ T.1branch:Branch α2 α3 α4twig:Twig α3 α4leaf:Leaf α4qHu:α2twigs:Multiset (Twig α3 α4)hbranch:Branch.branch qHu twigs ∈ trunk.2Q5:α3leafs:Multiset (Leaf α4)hleaf:leaf ∈ (Twig.twig Q5 leafs).2htwig:Twig.twig Q5 leafs ∈ (Branch.branch qHu twigs).2heq:(trunk.1, (Branch.branch qHu twigs).1, (Twig.twig Q5 leafs).1, leaf.1) = xhn:(Branch.branch qHu twigs).mem (qHu, f Q5, leaf.1)⊢ False
    apply hnotMemleaf_memα1:Typeα2:Typeα3:Typeα4:Typeinst✝²:DecidableEq α2inst✝¹:DecidableEq α3inst✝:DecidableEq α4T:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4f:α3 → α3hnotMem:¬(x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ Ttrunk:Trunk α1 α2 α3 α4htrunk:trunk ∈ T.1branch:Branch α2 α3 α4twig:Twig α3 α4leaf:Leaf α4qHu:α2twigs:Multiset (Twig α3 α4)hbranch:Branch.branch qHu twigs ∈ trunk.2Q5:α3leafs:Multiset (Leaf α4)hleaf:leaf ∈ (Twig.twig Q5 leafs).2htwig:Twig.twig Q5 leafs ∈ (Branch.branch qHu twigs).2heq:(trunk.1, (Branch.branch qHu twigs).1, (Twig.twig Q5 leafs).1, leaf.1) = xhn:(Branch.branch qHu twigs).mem (qHu, f Q5, leaf.1)⊢ (x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ T
    subst heqleaf_memα1:Typeα2:Typeα3:Typeα4:Typeinst✝²:DecidableEq α2inst✝¹:DecidableEq α3inst✝:DecidableEq α4T:FourTree α1 α2 α3 α4f:α3 → α3trunk:Trunk α1 α2 α3 α4htrunk:trunk ∈ T.1branch:Branch α2 α3 α4twig:Twig α3 α4leaf:Leaf α4qHu:α2twigs:Multiset (Twig α3 α4)hbranch:Branch.branch qHu twigs ∈ trunk.2Q5:α3leafs:Multiset (Leaf α4)hleaf:leaf ∈ (Twig.twig Q5 leafs).2htwig:Twig.twig Q5 leafs ∈ (Branch.branch qHu twigs).2hn:(Branch.branch qHu twigs).mem (qHu, f Q5, leaf.1)hnotMem:¬((trunk.1, (Branch.branch qHu twigs).1, (Twig.twig Q5 leafs).1, leaf.1).1,
      (trunk.1, (Branch.branch qHu twigs).1, (Twig.twig Q5 leafs).1, leaf.1).2.1,
      f (trunk.1, (Branch.branch qHu twigs).1, (Twig.twig Q5 leafs).1, leaf.1).2.2.1,
      (trunk.1, (Branch.branch qHu twigs).1, (Twig.twig Q5 leafs).1, leaf.1).2.2.2) ∈
    T⊢ ((trunk.1, (Branch.branch qHu twigs).1, (Twig.twig Q5 leafs).1, leaf.1).1,
    (trunk.1, (Branch.branch qHu twigs).1, (Twig.twig Q5 leafs).1, leaf.1).2.1,
    f (trunk.1, (Branch.branch qHu twigs).1, (Twig.twig Q5 leafs).1, leaf.1).2.2.1,
    (trunk.1, (Branch.branch qHu twigs).1, (Twig.twig Q5 leafs).1, leaf.1).2.2.2) ∈
  T
    exact ⟨trunk, htrunk, rfl, .branch qHu twigs, hbranch, hn⟩All goals completed! 🐙
  ·heqα1:Typeα2:Typeα3:Typeα4:Typeinst✝²:DecidableEq α2inst✝¹:DecidableEq α3inst✝:DecidableEq α4T:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4f:α3 → α3hnotMem:¬(x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ Ttrunk:Trunk α1 α2 α3 α4htrunk:trunk ∈ T.1branch:Branch α2 α3 α4twig:Twig α3 α4leaf:Leaf α4qHu:α2twigs:Multiset (Twig α3 α4)hbranch:Branch.branch qHu twigs ∈ trunk.2Q5:α3leafs:Multiset (Leaf α4)hleaf:leaf ∈ (Twig.twig Q5 leafs).2htwig:Twig.twig Q5 leafs ∈ (Branch.branch qHu twigs).2heq:(trunk.1, (Branch.branch qHu twigs).1, (Twig.twig Q5 leafs).1, leaf.1) = x⊢ (x.1, x.2.1, f x.2.2.1, x.2.2.2) =
  ((Trunk.uniqueMap3 f trunk).1, (Branch.uniqueMap3 f (Branch.branch qHu twigs)).1,
    (Twig.twig (f Q5)
        (Multiset.filter
          (fun x =>
            match x with
            | Leaf.leaf Q10 => ¬(Branch.branch qHu twigs).mem (qHu, f Q5, Q10))
          leafs)).1,
    leaf.1) subst heqheqα1:Typeα2:Typeα3:Typeα4:Typeinst✝²:DecidableEq α2inst✝¹:DecidableEq α3inst✝:DecidableEq α4T:FourTree α1 α2 α3 α4f:α3 → α3trunk:Trunk α1 α2 α3 α4htrunk:trunk ∈ T.1branch:Branch α2 α3 α4twig:Twig α3 α4leaf:Leaf α4qHu:α2twigs:Multiset (Twig α3 α4)hbranch:Branch.branch qHu twigs ∈ trunk.2Q5:α3leafs:Multiset (Leaf α4)hleaf:leaf ∈ (Twig.twig Q5 leafs).2htwig:Twig.twig Q5 leafs ∈ (Branch.branch qHu twigs).2hnotMem:¬((trunk.1, (Branch.branch qHu twigs).1, (Twig.twig Q5 leafs).1, leaf.1).1,
      (trunk.1, (Branch.branch qHu twigs).1, (Twig.twig Q5 leafs).1, leaf.1).2.1,
      f (trunk.1, (Branch.branch qHu twigs).1, (Twig.twig Q5 leafs).1, leaf.1).2.2.1,
      (trunk.1, (Branch.branch qHu twigs).1, (Twig.twig Q5 leafs).1, leaf.1).2.2.2) ∈
    T⊢ ((trunk.1, (Branch.branch qHu twigs).1, (Twig.twig Q5 leafs).1, leaf.1).1,
    (trunk.1, (Branch.branch qHu twigs).1, (Twig.twig Q5 leafs).1, leaf.1).2.1,
    f (trunk.1, (Branch.branch qHu twigs).1, (Twig.twig Q5 leafs).1, leaf.1).2.2.1,
    (trunk.1, (Branch.branch qHu twigs).1, (Twig.twig Q5 leafs).1, leaf.1).2.2.2) =
  ((Trunk.uniqueMap3 f trunk).1, (Branch.uniqueMap3 f (Branch.branch qHu twigs)).1,
    (Twig.twig (f Q5)
        (Multiset.filter
          (fun x =>
            match x with
            | Leaf.leaf Q10 => ¬(Branch.branch qHu twigs).mem (qHu, f Q5, Q10))
          leafs)).1,
    leaf.1)
    simp [Trunk.uniqueMap3, Branch.uniqueMap3]All goals completed! 🐙



lemma exists_of_mem_uniqueMap3 {T : FourTree α1 α2 α3 α4}
    (C : α1 × α2 × α3 × α4) (h : C ∈ T.uniqueMap3 f) :
    ∃ qHd qHu Q5 Q10, C = (qHd, qHu, f Q5, Q10) ∧
      (qHd, qHu, Q5, Q10) ∈ T := byα1:Typeα2:Typeα3:Typeα4:Typeinst✝²:DecidableEq α2inst✝¹:DecidableEq α3inst✝:DecidableEq α4f:α3 → α3T:FourTree α1 α2 α3 α4C:α1 × α2 × α3 × α4h:C ∈ uniqueMap3 f T⊢ ∃ qHd qHu Q5 Q10, C = (qHd, qHu, f Q5, Q10) ∧ (qHd, qHu, Q5, Q10) ∈ T
  rw [mem_iff_mem_toMultisetα1:Typeα2:Typeα3:Typeα4:Typeinst✝²:DecidableEq α2inst✝¹:DecidableEq α3inst✝:DecidableEq α4f:α3 → α3T:FourTree α1 α2 α3 α4C:α1 × α2 × α3 × α4h:C ∈ (uniqueMap3 f T).toMultiset⊢ ∃ qHd qHu Q5 Q10, C = (qHd, qHu, f Q5, Q10) ∧ (qHd, qHu, Q5, Q10) ∈ Tα1:Typeα2:Typeα3:Typeα4:Typeinst✝²:DecidableEq α2inst✝¹:DecidableEq α3inst✝:DecidableEq α4f:α3 → α3T:FourTree α1 α2 α3 α4C:α1 × α2 × α3 × α4h:C ∈ (uniqueMap3 f T).toMultiset⊢ ∃ qHd qHu Q5 Q10, C = (qHd, qHu, f Q5, Q10) ∧ (qHd, qHu, Q5, Q10) ∈ T] at hα1:Typeα2:Typeα3:Typeα4:Typeinst✝²:DecidableEq α2inst✝¹:DecidableEq α3inst✝:DecidableEq α4f:α3 → α3T:FourTree α1 α2 α3 α4C:α1 × α2 × α3 × α4h:C ∈ (uniqueMap3 f T).toMultiset⊢ ∃ qHd qHu Q5 Q10, C = (qHd, qHu, f Q5, Q10) ∧ (qHd, qHu, Q5, Q10) ∈ T
  simp [toMultiset] at hα1:Typeα2:Typeα3:Typeα4:Typeinst✝²:DecidableEq α2inst✝¹:DecidableEq α3inst✝:DecidableEq α4f:α3 → α3T:FourTree α1 α2 α3 α4C:α1 × α2 × α3 × α4h:∃ a,
  a ∈ (uniqueMap3 f T).1 ∧ ∃ a_1, a_1 ∈ a.2 ∧ ∃ a_2, a_2 ∈ a_1.2 ∧ ∃ a_3, a_3 ∈ a_2.2 ∧ (a.1, a_1.1, a_2.1, a_3.1) = C⊢ ∃ qHd qHu Q5 Q10, C = (qHd, qHu, f Q5, Q10) ∧ (qHd, qHu, Q5, Q10) ∈ T
  obtain ⟨trunkI, trunkI_mem, branchI, branchI_mem, twigI, twigI_mem,
    leafI, leafI_mem, heq⟩ := hα1:Typeα2:Typeα3:Typeα4:Typeinst✝²:DecidableEq α2inst✝¹:DecidableEq α3inst✝:DecidableEq α4f:α3 → α3T:FourTree α1 α2 α3 α4C:α1 × α2 × α3 × α4trunkI:Trunk α1 α2 α3 α4trunkI_mem:trunkI ∈ (uniqueMap3 f T).1branchI:Branch α2 α3 α4branchI_mem:branchI ∈ trunkI.2twigI:Twig α3 α4twigI_mem:twigI ∈ branchI.2leafI:Leaf α4leafI_mem:leafI ∈ twigI.2heq:(trunkI.1, branchI.1, twigI.1, leafI.1) = C⊢ ∃ qHd qHu Q5 Q10, C = (qHd, qHu, f Q5, Q10) ∧ (qHd, qHu, Q5, Q10) ∈ T
  -- obtaining trunkT
  simp [uniqueMap3] at trunkI_memα1:Typeα2:Typeα3:Typeα4:Typeinst✝²:DecidableEq α2inst✝¹:DecidableEq α3inst✝:DecidableEq α4f:α3 → α3T:FourTree α1 α2 α3 α4C:α1 × α2 × α3 × α4trunkI:Trunk α1 α2 α3 α4branchI:Branch α2 α3 α4branchI_mem:branchI ∈ trunkI.2twigI:Twig α3 α4twigI_mem:twigI ∈ branchI.2leafI:Leaf α4leafI_mem:leafI ∈ twigI.2heq:(trunkI.1, branchI.1, twigI.1, leafI.1) = CtrunkI_mem:∃ a, a ∈ T.1 ∧ Trunk.uniqueMap3 f a = trunkI⊢ ∃ qHd qHu Q5 Q10, C = (qHd, qHu, f Q5, Q10) ∧ (qHd, qHu, Q5, Q10) ∈ T
  obtain ⟨trunkT, trunkT_mem, rfl⟩ := trunkI_memα1:Typeα2:Typeα3:Typeα4:Typeinst✝²:DecidableEq α2inst✝¹:DecidableEq α3inst✝:DecidableEq α4f:α3 → α3T:FourTree α1 α2 α3 α4C:α1 × α2 × α3 × α4branchI:Branch α2 α3 α4twigI:Twig α3 α4twigI_mem:twigI ∈ branchI.2leafI:Leaf α4leafI_mem:leafI ∈ twigI.2trunkT:Trunk α1 α2 α3 α4trunkT_mem:trunkT ∈ T.1branchI_mem:branchI ∈ (Trunk.uniqueMap3 f trunkT).2heq:((Trunk.uniqueMap3 f trunkT).1, branchI.1, twigI.1, leafI.1) = C⊢ ∃ qHd qHu Q5 Q10, C = (qHd, qHu, f Q5, Q10) ∧ (qHd, qHu, Q5, Q10) ∈ T
  -- obtaining branchT
  simp [Trunk.uniqueMap3] at branchI_memα1:Typeα2:Typeα3:Typeα4:Typeinst✝²:DecidableEq α2inst✝¹:DecidableEq α3inst✝:DecidableEq α4f:α3 → α3T:FourTree α1 α2 α3 α4C:α1 × α2 × α3 × α4branchI:Branch α2 α3 α4twigI:Twig α3 α4twigI_mem:twigI ∈ branchI.2leafI:Leaf α4leafI_mem:leafI ∈ twigI.2trunkT:Trunk α1 α2 α3 α4trunkT_mem:trunkT ∈ T.1heq:((Trunk.uniqueMap3 f trunkT).1, branchI.1, twigI.1, leafI.1) = CbranchI_mem:∃ a, a ∈ trunkT.2 ∧ Branch.uniqueMap3 f a = branchI⊢ ∃ qHd qHu Q5 Q10, C = (qHd, qHu, f Q5, Q10) ∧ (qHd, qHu, Q5, Q10) ∈ T
  obtain ⟨branchT, branchT_mem, rfl⟩ := branchI_memα1:Typeα2:Typeα3:Typeα4:Typeinst✝²:DecidableEq α2inst✝¹:DecidableEq α3inst✝:DecidableEq α4f:α3 → α3T:FourTree α1 α2 α3 α4C:α1 × α2 × α3 × α4twigI:Twig α3 α4leafI:Leaf α4leafI_mem:leafI ∈ twigI.2trunkT:Trunk α1 α2 α3 α4trunkT_mem:trunkT ∈ T.1branchT:Branch α2 α3 α4branchT_mem:branchT ∈ trunkT.2twigI_mem:twigI ∈ (Branch.uniqueMap3 f branchT).2heq:((Trunk.uniqueMap3 f trunkT).1, (Branch.uniqueMap3 f branchT).1, twigI.1, leafI.1) = C⊢ ∃ qHd qHu Q5 Q10, C = (qHd, qHu, f Q5, Q10) ∧ (qHd, qHu, Q5, Q10) ∈ T
  -- obtaining twigT
  simp only [Branch.uniqueMap3, Multiset.mem_map] at twigI_memα1:Typeα2:Typeα3:Typeα4:Typeinst✝²:DecidableEq α2inst✝¹:DecidableEq α3inst✝:DecidableEq α4f:α3 → α3T:FourTree α1 α2 α3 α4C:α1 × α2 × α3 × α4twigI:Twig α3 α4leafI:Leaf α4leafI_mem:leafI ∈ twigI.2trunkT:Trunk α1 α2 α3 α4trunkT_mem:trunkT ∈ T.1branchT:Branch α2 α3 α4branchT_mem:branchT ∈ trunkT.2heq:((Trunk.uniqueMap3 f trunkT).1, (Branch.uniqueMap3 f branchT).1, twigI.1, leafI.1) = CtwigI_mem:∃ a,
  a ∈ branchT.2 ∧
    Twig.twig (f a.1)
        (Multiset.filter (fun x => ¬(Branch.branch branchT.1 branchT.2).mem (branchT.1, f a.1, x.1)) a.2) =
      twigI⊢ ∃ qHd qHu Q5 Q10, C = (qHd, qHu, f Q5, Q10) ∧ (qHd, qHu, Q5, Q10) ∈ T
  obtain ⟨twigT, twigT_mem, rfl⟩ := twigI_memα1:Typeα2:Typeα3:Typeα4:Typeinst✝²:DecidableEq α2inst✝¹:DecidableEq α3inst✝:DecidableEq α4f:α3 → α3T:FourTree α1 α2 α3 α4C:α1 × α2 × α3 × α4leafI:Leaf α4trunkT:Trunk α1 α2 α3 α4trunkT_mem:trunkT ∈ T.1branchT:Branch α2 α3 α4branchT_mem:branchT ∈ trunkT.2twigT:Twig α3 α4twigT_mem:twigT ∈ branchT.2leafI_mem:leafI ∈
  (Twig.twig (f twigT.1)
      (Multiset.filter (fun x => ¬(Branch.branch branchT.1 branchT.2).mem (branchT.1, f twigT.1, x.1)) twigT.2)).2heq:((Trunk.uniqueMap3 f trunkT).1, (Branch.uniqueMap3 f branchT).1,
    (Twig.twig (f twigT.1)
        (Multiset.filter (fun x => ¬(Branch.branch branchT.1 branchT.2).mem (branchT.1, f twigT.1, x.1)) twigT.2)).1,
    leafI.1) =
  C⊢ ∃ qHd qHu Q5 Q10, C = (qHd, qHu, f Q5, Q10) ∧ (qHd, qHu, Q5, Q10) ∈ T
  -- obtaining leafT
  simp at leafI_memα1:Typeα2:Typeα3:Typeα4:Typeinst✝²:DecidableEq α2inst✝¹:DecidableEq α3inst✝:DecidableEq α4f:α3 → α3T:FourTree α1 α2 α3 α4C:α1 × α2 × α3 × α4leafI:Leaf α4trunkT:Trunk α1 α2 α3 α4trunkT_mem:trunkT ∈ T.1branchT:Branch α2 α3 α4branchT_mem:branchT ∈ trunkT.2twigT:Twig α3 α4twigT_mem:twigT ∈ branchT.2heq:((Trunk.uniqueMap3 f trunkT).1, (Branch.uniqueMap3 f branchT).1,
    (Twig.twig (f twigT.1)
        (Multiset.filter (fun x => ¬(Branch.branch branchT.1 branchT.2).mem (branchT.1, f twigT.1, x.1)) twigT.2)).1,
    leafI.1) =
  CleafI_mem:leafI ∈ twigT.2 ∧ ¬(Branch.branch branchT.1 branchT.2).mem (branchT.1, f twigT.1, leafI.1)⊢ ∃ qHd qHu Q5 Q10, C = (qHd, qHu, f Q5, Q10) ∧ (qHd, qHu, Q5, Q10) ∈ T
  obtain ⟨leftI_mem, h_not_mem⟩ := leafI_memα1:Typeα2:Typeα3:Typeα4:Typeinst✝²:DecidableEq α2inst✝¹:DecidableEq α3inst✝:DecidableEq α4f:α3 → α3T:FourTree α1 α2 α3 α4C:α1 × α2 × α3 × α4leafI:Leaf α4trunkT:Trunk α1 α2 α3 α4trunkT_mem:trunkT ∈ T.1branchT:Branch α2 α3 α4branchT_mem:branchT ∈ trunkT.2twigT:Twig α3 α4twigT_mem:twigT ∈ branchT.2heq:((Trunk.uniqueMap3 f trunkT).1, (Branch.uniqueMap3 f branchT).1,
    (Twig.twig (f twigT.1)
        (Multiset.filter (fun x => ¬(Branch.branch branchT.1 branchT.2).mem (branchT.1, f twigT.1, x.1)) twigT.2)).1,
    leafI.1) =
  CleftI_mem:leafI ∈ twigT.2h_not_mem:¬(Branch.branch branchT.1 branchT.2).mem (branchT.1, f twigT.1, leafI.1)⊢ ∃ qHd qHu Q5 Q10, C = (qHd, qHu, f Q5, Q10) ∧ (qHd, qHu, Q5, Q10) ∈ T
  subst heqα1:Typeα2:Typeα3:Typeα4:Typeinst✝²:DecidableEq α2inst✝¹:DecidableEq α3inst✝:DecidableEq α4f:α3 → α3T:FourTree α1 α2 α3 α4leafI:Leaf α4trunkT:Trunk α1 α2 α3 α4trunkT_mem:trunkT ∈ T.1branchT:Branch α2 α3 α4branchT_mem:branchT ∈ trunkT.2twigT:Twig α3 α4twigT_mem:twigT ∈ branchT.2leftI_mem:leafI ∈ twigT.2h_not_mem:¬(Branch.branch branchT.1 branchT.2).mem (branchT.1, f twigT.1, leafI.1)⊢ ∃ qHd qHu Q5 Q10,
  ((Trunk.uniqueMap3 f trunkT).1, (Branch.uniqueMap3 f branchT).1,
        (Twig.twig (f twigT.1)
            (Multiset.filter (fun x => ¬(Branch.branch branchT.1 branchT.2).mem (branchT.1, f twigT.1, x.1))
              twigT.2)).1,
        leafI.1) =
      (qHd, qHu, f Q5, Q10) ∧
    (qHd, qHu, Q5, Q10) ∈ T
  refine ⟨trunkT.1, branchT.1, twigT.1, leafI.1, ?_,
    mem_of_parts trunkT branchT twigT leafI trunkT_mem branchT_mem twigT_mem leftI_mem rfl⟩α1:Typeα2:Typeα3:Typeα4:Typeinst✝²:DecidableEq α2inst✝¹:DecidableEq α3inst✝:DecidableEq α4f:α3 → α3T:FourTree α1 α2 α3 α4leafI:Leaf α4trunkT:Trunk α1 α2 α3 α4trunkT_mem:trunkT ∈ T.1branchT:Branch α2 α3 α4branchT_mem:branchT ∈ trunkT.2twigT:Twig α3 α4twigT_mem:twigT ∈ branchT.2leftI_mem:leafI ∈ twigT.2h_not_mem:¬(Branch.branch branchT.1 branchT.2).mem (branchT.1, f twigT.1, leafI.1)⊢ ((Trunk.uniqueMap3 f trunkT).1, (Branch.uniqueMap3 f branchT).1,
    (Twig.twig (f twigT.1)
        (Multiset.filter (fun x => ¬(Branch.branch branchT.1 branchT.2).mem (branchT.1, f twigT.1, x.1)) twigT.2)).1,
    leafI.1) =
  (trunkT.1, branchT.1, f twigT.1, leafI.1)
  simp [Trunk.uniqueMap3, Branch.uniqueMap3]All goals completed! 🐙

Unique maps for FourTree

uniqueMap4

uniqueMap3

Unique maps for `FourTree`