Physlib.Mathematics.DataStructures.FourTree.Basic

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 Mathlib.Data.Multiset.Bind
public import Mathlib.Data.Multiset.Sort

The data type FourTree

We define a tree-like structure, called FourTree, for storing values of a type α1 × α2 × α3 × α4.

It is defined recursively, with the following structure:

A leaf contains a value of type α4.

A twig contains a value of type α3, and a multiset of leafs.

A branch contains a value of type α2, and a multiset of twigs.

A trunk contains a value of type α1, and a multiset of branchs.

A FourTree contains a multiset of trunks.

@[expose] public section

A leaf contains has the data of a term of type α4.

inductive Leaf (α4 : Type)
  | leaf : α4 → Leaf α4
deriving DecidableEq

A twig has the data of a term of type α3 and a multiset of type Leaf α4.

inductive Twig (α3 α4 : Type)
  | twig : α3 → Multiset (Leaf α4) → Twig α3 α4

A branch has the data of a term of type α2 and a multiset of type Twig α3 α4.

inductive Branch (α2 α3 α4 : Type)
  | branch : α2 → Multiset (Twig α3 α4) → Branch α2 α3 α4

A trunk has the data of a term of type α1 and a multiset of type Branch α2 α3 α4.

inductive Trunk (α1 α2 α3 α4 : Type)
  | trunk : α1 → Multiset (Branch α2 α3 α4) → Trunk α1 α2 α3 α4

A FourTree has the data of a multiset of type Trunk α1 α2 α3 α4.

inductive FourTree (α1 α2 α3 α4 : Type)
  | root : Multiset (FourTree.Trunk α1 α2 α3 α4) → FourTree α1 α2 α3 α4

Repr instances for the FourTree

These instances allow the FourTree to be printed in a human-readable format, and copied and pasted.

              unsafe instance (α4 : Type) [Repr α4] : Repr (Leaf α4) where
  reprPrec x _ :=
    match x with
    | .leaf xs => "leaf " ++ reprStr xsunsafe instance (α3 α4 : Type) [Repr α3] [Repr α4] : Repr (Twig α3 α4) where
  reprPrec x _ :=
    match x with
    | .twig xs a => "twig " ++ reprStr xs ++ " " ++ reprStr aunsafe instance (α2 α3 α4: Type) [Repr α2] [Repr α3] [Repr α4] :
    Repr (Branch α2 α3 α4) where
  reprPrec x _ :=
    match x with
    | .branch xa a => "branch (" ++ reprStr xa ++ ") " ++ reprStr aunsafe instance (α1 α2 α3 α4: Type) [Repr α1] [Repr α2] [Repr α3] [Repr α4] :
    Repr (Trunk α1 α2 α3 α4) where
  reprPrec x _ :=
    match x with
    | .trunk xa a => "trunk (" ++ reprStr xa ++ ") " ++ reprStr aunsafe instance (α1 α2 α3 α4: Type) [Repr α1] [Repr α2] [Repr α3] [Repr α4] :
    Repr (FourTree α1 α2 α3 α4) where
  reprPrec x _ :=
    match x with
    | .root xs => "root " ++ reprStr xs

Conversion between FourTree and Multiset

A FourTree from a multiset of α1 × α2 × α3 × α4.

def fromMultiset {α1 α2 α3 α4 : Type} [DecidableEq α1]
    [DecidableEq α2] [DecidableEq α3] [DecidableEq α4]
    (l : Multiset (α1 × α2 × α3 × α4)) : FourTree α1 α2 α3 α4 :=
  let A1 : Multiset α1 := (l.map fun x => x.1).dedup
  root <| A1.map fun xa => trunk xa <|
    let B2 := (l.filter fun y => y.1 = xa)
    let C2 : Multiset (α2 × α3 × α4) := (B2.map fun y => y.2).dedup
    let A2 : Multiset α2 := (C2.map fun x => x.1).dedup
    A2.map fun xb => branch xb <|
      let B3 := (C2.filter fun y => y.1 = xb)
      let C3 : Multiset (α3 × α4) := (B3.map fun y => y.2).dedup
      let A3 : Multiset α3 := (C3.map fun x => x.1).dedup
      A3.map fun xc => twig xc <|
        let B4 := (C3.filter fun y => y.1 = xc)
        let C4 : Multiset α4 := (B4.map fun y => y.2).dedup
        C4.map fun xd => leaf xd

A FourTree to a multiset of α1 × α2 × α3 × α4.

def toMultiset {α1 α2 α3 α4 : Type} (T : FourTree α1 α2 α3 α4) : Multiset (α1 × α2 × α3 × α4) :=
  match T with
  | .root trunks =>
    trunks.bind fun (trunk xT branches) =>
        branches.bind fun (branch xB twigs) =>
            twigs.bind fun (twig xTw leafs) =>
                leafs.map fun (leaf xL) => (xT, xB, xTw, xL)

Cardinality of the tree

The cardinality of a Twig is the number of leafs.

def Twig.card {α3 α4 : Type} (T : Twig α3 α4) : Nat :=
  match T with
  | .twig _ leafs => leafs.card

The cardinality of a Branch is the total number of leafs.

def Branch.card {α2 α3 α4 : Type} (T : Branch α2 α3 α4) : Nat :=
  match T with
  | .branch _ twigs => (twigs.map Twig.card).sum

The cardinality of a Trunk is the total number of leafs.

def Trunk.card {α1 α2 α3 α4 : Type} (T : Trunk α1 α2 α3 α4) : Nat :=
  match T with
  | .trunk _ branches => (branches.map Branch.card).sum

The cardinality of a FourTree is the total number of leafs.

def card {α1 α2 α3 α4 : Type} (T : FourTree α1 α2 α3 α4) : Nat :=
  match T with
  | .root trunks => (trunks.map Trunk.card).sum

lemma card_eq_toMultiset_card (T : FourTree α1 α2 α3 α4s) :
    T.card = T.toMultiset.card := byα1:Typeα2:Typeα3:Typeα4s:TypeT:FourTree α1 α2 α3 α4s⊢ T.card = T.toMultiset.card
  simp only [card, toMultiset, Multiset.card_bind, Function.comp_apply, Multiset.card_map]α1:Typeα2:Typeα3:Typeα4s:TypeT:FourTree α1 α2 α3 α4s⊢ (Multiset.map Trunk.card T.1).sum =
  (Multiset.map (fun x => (Multiset.map (fun x => (Multiset.map (fun x => x.2.card) x.2).sum) x.2).sum) T.1).sum
  rflAll goals completed! 🐙

Membership of a FourTree

Based on the tree structure we can define a faster membership criterion, which is equivalent to membership based on multisets.

An element of a : α4 is a member of Leaf α4 if the underlying element of the Leaf is a.

def Leaf.mem {α4} (T : Leaf α4) (x : α4) : Prop :=
  match T with
  | .leaf xs => xs = x

instance {α4} [DecidableEq α4] (T : Leaf α4) (x : α4) : Decidable (T.mem x) :=
  inferInstanceAs (Decidable (match T with | .leaf xs => xs = x))

An element of a : α3 × α4 is a member of Twig α3 α4 if the underlying α3 element of the Twig is a.1 and a.2 is a member of one of the Leaf.

def Twig.mem (T : Twig α3 α4) (x : α3 × α4) : Prop :=
  match T with
  | .twig xs leafs => xs = x.1 ∧ ∃ leaf ∈ leafs, leaf.mem x.2

instance {α3 α4} [DecidableEq α3] [DecidableEq α4] (T : Twig α3 α4) (x : α3 × α4) :
    Decidable (T.mem x) :=
  match T with
  | .twig _ leafs =>
    haveI : Decidable (∃ leaf ∈ leafs, leaf.mem x.2) := Multiset.decidableExistsMultiset
    instDecidableAnd

An element of a : α2 × α3 × α4 is a member of Branch α2 α3 α4 if the underlying α2 element of the Branch is a.1 and a.2 is a member of one of the Twig.

def Branch.mem (T : Branch α2 α3 α4) (x : α2 × α3 × α4) : Prop :=
  match T with
  | .branch xo twigs => xo = x.1 ∧ ∃ twig ∈ twigs, twig.mem x.2

instance [DecidableEq α2] [DecidableEq α3] [DecidableEq α4] (T : Branch α2 α3 α4)
    (x : α2 × α3 × α4) : Decidable (T.mem x) :=
  match T with
  | .branch _ twigs =>
    haveI : Decidable (∃ twig ∈ twigs, twig.mem x.2) := Multiset.decidableExistsMultiset
    instDecidableAnd

An element of a : α1 × α2 × α3 × α4 is a member of Trunk α1 α2 α3 α4 if the underlying α1 element of the Trunk is a.1 and a.2 is a member of one of the Branch.

def Trunk.mem (T : Trunk α1 α2 α3 α4) (x : α1 × α2 × α3 × α4) : Prop :=
  match T with
  | .trunk xo branches => xo = x.1 ∧ ∃ branch ∈ branches, branch.mem x.2

instance [DecidableEq α1] [DecidableEq α2] [DecidableEq α3] [DecidableEq α4]
    (T : Trunk α1 α2 α3 α4) (x : α1 × α2 × α3 × α4) : Decidable (T.mem x) :=
  match T with
  | .trunk _ branches =>
    haveI : Decidable (∃ branch ∈ branches, branch.mem x.2) := Multiset.decidableExistsMultiset
    instDecidableAnd

An element of a : α1 × α2 × α3 × α4 is a member of FourTree α1 α2 α3 α4 if a is a member of one of the Trunk.

def mem (T : FourTree α1 α2 α3 α4) (x : α1 × α2 × α3 × α4) : Prop :=
  match T with
  | .root trunks => ∃ trunk ∈ trunks, trunk.mem x

              instance [DecidableEq α1] [DecidableEq α2] [DecidableEq α3] [DecidableEq α4]
    (T : FourTree α1 α2 α3 α4) (x : α1 × α2 × α3 × α4) : Decidable (T.mem x) :=
  Multiset.decidableExistsMultisetinstance : Membership (α1 × α2 × α3 × α4) (FourTree α1 α2 α3 α4) where
  mem := meminstance [DecidableEq α1] [DecidableEq α2] [DecidableEq α3] [DecidableEq α4]
    (T : FourTree α1 α2 α3 α4) (x : α1 × α2 × α3 × α4) : Decidable (x ∈ T) :=
  Multiset.decidableExistsMultiset

lemma mem_iff_mem_toMultiset (T : FourTree α1 α2 α3 α4) (x : α1 × α2 × α3 × α4) :
    x ∈ T ↔ x ∈ T.toMultiset := byα1:Typeα2:Typeα3:Typeα4:TypeT:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4⊢ x ∈ T ↔ x ∈ T.toMultiset
  have leaf_iff : ∀ (l : Leaf α4) (y : α4), l.mem y ↔ l.1 = y := by
    rintro ⟨_⟩ _α1:Typeα2:Typeα3:Typeα4:TypeT:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4a✝:α4y✝:α4⊢ (leaf a✝).mem y✝ ↔ (leaf a✝).1 = y✝α1:Typeα2:Typeα3:Typeα4:TypeT:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4leaf_iff:∀ (l : Leaf α4) (y : α4), l.mem y ↔ l.1 = y⊢ x ∈ T ↔ x ∈ T.toMultiset
    rflα1:Typeα2:Typeα3:Typeα4:TypeT:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4leaf_iff:∀ (l : Leaf α4) (y : α4), l.mem y ↔ l.1 = y⊢ x ∈ T ↔ x ∈ T.toMultisetα1:Typeα2:Typeα3:Typeα4:TypeT:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4leaf_iff:∀ (l : Leaf α4) (y : α4), l.mem y ↔ l.1 = y⊢ x ∈ T ↔ x ∈ T.toMultiset
  have twig_iff : ∀ (t : Twig α3 α4) (y : α3 × α4),
      t.mem y ↔ t.1 = y.1 ∧ ∃ l ∈ t.2, l.mem y.2 := by
    rintro ⟨_, _⟩ _α1:Typeα2:Typeα3:Typeα4:TypeT:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4leaf_iff:∀ (l : Leaf α4) (y : α4), l.mem y ↔ l.1 = ya✝¹:α3a✝:Multiset (Leaf α4)y✝:α3 × α4⊢ (twig a✝¹ a✝).mem y✝ ↔ (twig a✝¹ a✝).1 = y✝.1 ∧ ∃ l, l ∈ (twig a✝¹ a✝).2 ∧ l.mem y✝.2α1:Typeα2:Typeα3:Typeα4:TypeT:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4leaf_iff:∀ (l : Leaf α4) (y : α4), l.mem y ↔ l.1 = ytwig_iff:∀ (t : Twig α3 α4) (y : α3 × α4), t.mem y ↔ t.1 = y.1 ∧ ∃ l, l ∈ t.2 ∧ l.mem y.2⊢ x ∈ T ↔ x ∈ T.toMultiset
    rflα1:Typeα2:Typeα3:Typeα4:TypeT:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4leaf_iff:∀ (l : Leaf α4) (y : α4), l.mem y ↔ l.1 = ytwig_iff:∀ (t : Twig α3 α4) (y : α3 × α4), t.mem y ↔ t.1 = y.1 ∧ ∃ l, l ∈ t.2 ∧ l.mem y.2⊢ x ∈ T ↔ x ∈ T.toMultisetα1:Typeα2:Typeα3:Typeα4:TypeT:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4leaf_iff:∀ (l : Leaf α4) (y : α4), l.mem y ↔ l.1 = ytwig_iff:∀ (t : Twig α3 α4) (y : α3 × α4), t.mem y ↔ t.1 = y.1 ∧ ∃ l, l ∈ t.2 ∧ l.mem y.2⊢ x ∈ T ↔ x ∈ T.toMultiset
  have branch_iff : ∀ (b : Branch α2 α3 α4) (y : α2 × α3 × α4),
      b.mem y ↔ b.1 = y.1 ∧ ∃ t ∈ b.2, t.mem y.2 := by
    rintro ⟨_, _⟩ _α1:Typeα2:Typeα3:Typeα4:TypeT:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4leaf_iff:∀ (l : Leaf α4) (y : α4), l.mem y ↔ l.1 = ytwig_iff:∀ (t : Twig α3 α4) (y : α3 × α4), t.mem y ↔ t.1 = y.1 ∧ ∃ l, l ∈ t.2 ∧ l.mem y.2a✝¹:α2a✝:Multiset (Twig α3 α4)y✝:α2 × α3 × α4⊢ (branch a✝¹ a✝).mem y✝ ↔ (branch a✝¹ a✝).1 = y✝.1 ∧ ∃ t, t ∈ (branch a✝¹ a✝).2 ∧ t.mem y✝.2α1:Typeα2:Typeα3:Typeα4:TypeT:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4leaf_iff:∀ (l : Leaf α4) (y : α4), l.mem y ↔ l.1 = ytwig_iff:∀ (t : Twig α3 α4) (y : α3 × α4), t.mem y ↔ t.1 = y.1 ∧ ∃ l, l ∈ t.2 ∧ l.mem y.2branch_iff:∀ (b : Branch α2 α3 α4) (y : α2 × α3 × α4), b.mem y ↔ b.1 = y.1 ∧ ∃ t, t ∈ b.2 ∧ t.mem y.2⊢ x ∈ T ↔ x ∈ T.toMultiset
    rflα1:Typeα2:Typeα3:Typeα4:TypeT:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4leaf_iff:∀ (l : Leaf α4) (y : α4), l.mem y ↔ l.1 = ytwig_iff:∀ (t : Twig α3 α4) (y : α3 × α4), t.mem y ↔ t.1 = y.1 ∧ ∃ l, l ∈ t.2 ∧ l.mem y.2branch_iff:∀ (b : Branch α2 α3 α4) (y : α2 × α3 × α4), b.mem y ↔ b.1 = y.1 ∧ ∃ t, t ∈ b.2 ∧ t.mem y.2⊢ x ∈ T ↔ x ∈ T.toMultisetα1:Typeα2:Typeα3:Typeα4:TypeT:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4leaf_iff:∀ (l : Leaf α4) (y : α4), l.mem y ↔ l.1 = ytwig_iff:∀ (t : Twig α3 α4) (y : α3 × α4), t.mem y ↔ t.1 = y.1 ∧ ∃ l, l ∈ t.2 ∧ l.mem y.2branch_iff:∀ (b : Branch α2 α3 α4) (y : α2 × α3 × α4), b.mem y ↔ b.1 = y.1 ∧ ∃ t, t ∈ b.2 ∧ t.mem y.2⊢ x ∈ T ↔ x ∈ T.toMultiset
  have trunk_iff : ∀ (k : Trunk α1 α2 α3 α4) (y : α1 × α2 × α3 × α4),
      k.mem y ↔ k.1 = y.1 ∧ ∃ b ∈ k.2, b.mem y.2 := by
    rintro ⟨_, _⟩ _α1:Typeα2:Typeα3:Typeα4:TypeT:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4leaf_iff:∀ (l : Leaf α4) (y : α4), l.mem y ↔ l.1 = ytwig_iff:∀ (t : Twig α3 α4) (y : α3 × α4), t.mem y ↔ t.1 = y.1 ∧ ∃ l, l ∈ t.2 ∧ l.mem y.2branch_iff:∀ (b : Branch α2 α3 α4) (y : α2 × α3 × α4), b.mem y ↔ b.1 = y.1 ∧ ∃ t, t ∈ b.2 ∧ t.mem y.2a✝¹:α1a✝:Multiset (Branch α2 α3 α4)y✝:α1 × α2 × α3 × α4⊢ (trunk a✝¹ a✝).mem y✝ ↔ (trunk a✝¹ a✝).1 = y✝.1 ∧ ∃ b, b ∈ (trunk a✝¹ a✝).2 ∧ b.mem y✝.2α1:Typeα2:Typeα3:Typeα4:TypeT:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4leaf_iff:∀ (l : Leaf α4) (y : α4), l.mem y ↔ l.1 = ytwig_iff:∀ (t : Twig α3 α4) (y : α3 × α4), t.mem y ↔ t.1 = y.1 ∧ ∃ l, l ∈ t.2 ∧ l.mem y.2branch_iff:∀ (b : Branch α2 α3 α4) (y : α2 × α3 × α4), b.mem y ↔ b.1 = y.1 ∧ ∃ t, t ∈ b.2 ∧ t.mem y.2trunk_iff:∀ (k : Trunk α1 α2 α3 α4) (y : α1 × α2 × α3 × α4), k.mem y ↔ k.1 = y.1 ∧ ∃ b, b ∈ k.2 ∧ b.mem y.2⊢ x ∈ T ↔ x ∈ T.toMultiset
    rflα1:Typeα2:Typeα3:Typeα4:TypeT:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4leaf_iff:∀ (l : Leaf α4) (y : α4), l.mem y ↔ l.1 = ytwig_iff:∀ (t : Twig α3 α4) (y : α3 × α4), t.mem y ↔ t.1 = y.1 ∧ ∃ l, l ∈ t.2 ∧ l.mem y.2branch_iff:∀ (b : Branch α2 α3 α4) (y : α2 × α3 × α4), b.mem y ↔ b.1 = y.1 ∧ ∃ t, t ∈ b.2 ∧ t.mem y.2trunk_iff:∀ (k : Trunk α1 α2 α3 α4) (y : α1 × α2 × α3 × α4), k.mem y ↔ k.1 = y.1 ∧ ∃ b, b ∈ k.2 ∧ b.mem y.2⊢ x ∈ T ↔ x ∈ T.toMultisetα1:Typeα2:Typeα3:Typeα4:TypeT:FourTree α1 α2 α3 α4x:α1 × α2 × α3 × α4leaf_iff:∀ (l : Leaf α4) (y : α4), l.mem y ↔ l.1 = ytwig_iff:∀ (t : Twig α3 α4) (y : α3 × α4), t.mem y ↔ t.1 = y.1 ∧ ∃ l, l ∈ t.2 ∧ l.mem y.2branch_iff:∀ (b : Branch α2 α3 α4) (y : α2 × α3 × α4), b.mem y ↔ b.1 = y.1 ∧ ∃ t, t ∈ b.2 ∧ t.mem y.2trunk_iff:∀ (k : Trunk α1 α2 α3 α4) (y : α1 × α2 × α3 × α4), k.mem y ↔ k.1 = y.1 ∧ ∃ b, b ∈ k.2 ∧ b.mem y.2⊢ x ∈ T ↔ x ∈ T.toMultiset
  obtain ⟨trunks⟩ := Tα1:Typeα2:Typeα3:Typeα4:Typex:α1 × α2 × α3 × α4leaf_iff:∀ (l : Leaf α4) (y : α4), l.mem y ↔ l.1 = ytwig_iff:∀ (t : Twig α3 α4) (y : α3 × α4), t.mem y ↔ t.1 = y.1 ∧ ∃ l, l ∈ t.2 ∧ l.mem y.2branch_iff:∀ (b : Branch α2 α3 α4) (y : α2 × α3 × α4), b.mem y ↔ b.1 = y.1 ∧ ∃ t, t ∈ b.2 ∧ t.mem y.2trunk_iff:∀ (k : Trunk α1 α2 α3 α4) (y : α1 × α2 × α3 × α4), k.mem y ↔ k.1 = y.1 ∧ ∃ b, b ∈ k.2 ∧ b.mem y.2trunks:Multiset (Trunk α1 α2 α3 α4)⊢ x ∈ root trunks ↔ x ∈ (root trunks).toMultiset
  show (∃ trunk ∈ trunks, trunk.mem x) ↔ x ∈ (root trunks).toMultisetα1:Typeα2:Typeα3:Typeα4:Typex:α1 × α2 × α3 × α4leaf_iff:∀ (l : Leaf α4) (y : α4), l.mem y ↔ l.1 = ytwig_iff:∀ (t : Twig α3 α4) (y : α3 × α4), t.mem y ↔ t.1 = y.1 ∧ ∃ l, l ∈ t.2 ∧ l.mem y.2branch_iff:∀ (b : Branch α2 α3 α4) (y : α2 × α3 × α4), b.mem y ↔ b.1 = y.1 ∧ ∃ t, t ∈ b.2 ∧ t.mem y.2trunk_iff:∀ (k : Trunk α1 α2 α3 α4) (y : α1 × α2 × α3 × α4), k.mem y ↔ k.1 = y.1 ∧ ∃ b, b ∈ k.2 ∧ b.mem y.2trunks:Multiset (Trunk α1 α2 α3 α4)⊢ (∃ trunk, trunk ∈ trunks ∧ trunk.mem x) ↔ x ∈ (root trunks).toMultiset
  simp only [toMultiset, Multiset.mem_bind, Multiset.mem_map,
    trunk_iff, branch_iff, twig_iff, leaf_iff, Prod.ext_iff]α1:Typeα2:Typeα3:Typeα4:Typex:α1 × α2 × α3 × α4leaf_iff:∀ (l : Leaf α4) (y : α4), l.mem y ↔ l.1 = ytwig_iff:∀ (t : Twig α3 α4) (y : α3 × α4), t.mem y ↔ t.1 = y.1 ∧ ∃ l, l ∈ t.2 ∧ l.mem y.2branch_iff:∀ (b : Branch α2 α3 α4) (y : α2 × α3 × α4), b.mem y ↔ b.1 = y.1 ∧ ∃ t, t ∈ b.2 ∧ t.mem y.2trunk_iff:∀ (k : Trunk α1 α2 α3 α4) (y : α1 × α2 × α3 × α4), k.mem y ↔ k.1 = y.1 ∧ ∃ b, b ∈ k.2 ∧ b.mem y.2trunks:Multiset (Trunk α1 α2 α3 α4)⊢ (∃ trunk,
    trunk ∈ trunks ∧
      trunk.1 = x.1 ∧ ∃ b, b ∈ trunk.2 ∧ b.1 = x.2.1 ∧ ∃ t, t ∈ b.2 ∧ t.1 = x.2.2.1 ∧ ∃ l, l ∈ t.2 ∧ l.1 = x.2.2.2) ↔
  ∃ a,
    a ∈ trunks ∧
      ∃ a_1,
        a_1 ∈ a.2 ∧
          ∃ a_2, a_2 ∈ a_1.2 ∧ ∃ a_3, a_3 ∈ a_2.2 ∧ a.1 = x.1 ∧ a_1.1 = x.2.1 ∧ a_2.1 = x.2.2.1 ∧ a_3.1 = x.2.2.2
  tautoAll goals completed! 🐙

lemma mem_of_parts {T : FourTree α1 α2 α3 α4} {C : α1 × α2 × α3 × α4}
    (trunk : Trunk α1 α2 α3 α4)
    (branch : Branch α2 α3 α4)
    (twig : Twig α3 α4) (leaf : Leaf α4)
    (trunk_mem : trunk ∈ T.1) (branch_mem : branch ∈ trunk.2)
    (twig_mem : twig ∈ branch.2) (leaf_mem : leaf ∈ twig.2)
    (heq : C = (trunk.1, branch.1, twig.1, leaf.1)) :
    C ∈ T := byα1:Typeα2:Typeα3:Typeα4:TypeT:FourTree α1 α2 α3 α4C:α1 × α2 × α3 × α4trunk:Trunk α1 α2 α3 α4branch:Branch α2 α3 α4twig:Twig α3 α4leaf:Leaf α4trunk_mem:trunk ∈ T.1branch_mem:branch ∈ trunk.2twig_mem:twig ∈ branch.2leaf_mem:leaf ∈ twig.2heq:C = (trunk.1, branch.1, twig.1, leaf.1)⊢ C ∈ T
  rw [mem_iff_mem_toMultisetα1:Typeα2:Typeα3:Typeα4:TypeT:FourTree α1 α2 α3 α4C:α1 × α2 × α3 × α4trunk:Trunk α1 α2 α3 α4branch:Branch α2 α3 α4twig:Twig α3 α4leaf:Leaf α4trunk_mem:trunk ∈ T.1branch_mem:branch ∈ trunk.2twig_mem:twig ∈ branch.2leaf_mem:leaf ∈ twig.2heq:C = (trunk.1, branch.1, twig.1, leaf.1)⊢ C ∈ T.toMultisetα1:Typeα2:Typeα3:Typeα4:TypeT:FourTree α1 α2 α3 α4C:α1 × α2 × α3 × α4trunk:Trunk α1 α2 α3 α4branch:Branch α2 α3 α4twig:Twig α3 α4leaf:Leaf α4trunk_mem:trunk ∈ T.1branch_mem:branch ∈ trunk.2twig_mem:twig ∈ branch.2leaf_mem:leaf ∈ twig.2heq:C = (trunk.1, branch.1, twig.1, leaf.1)⊢ C ∈ T.toMultiset]α1:Typeα2:Typeα3:Typeα4:TypeT:FourTree α1 α2 α3 α4C:α1 × α2 × α3 × α4trunk:Trunk α1 α2 α3 α4branch:Branch α2 α3 α4twig:Twig α3 α4leaf:Leaf α4trunk_mem:trunk ∈ T.1branch_mem:branch ∈ trunk.2twig_mem:twig ∈ branch.2leaf_mem:leaf ∈ twig.2heq:C = (trunk.1, branch.1, twig.1, leaf.1)⊢ C ∈ T.toMultiset
  simp only [toMultiset, Multiset.mem_bind, Multiset.mem_map]α1:Typeα2:Typeα3:Typeα4:TypeT:FourTree α1 α2 α3 α4C:α1 × α2 × α3 × α4trunk:Trunk α1 α2 α3 α4branch:Branch α2 α3 α4twig:Twig α3 α4leaf:Leaf α4trunk_mem:trunk ∈ T.1branch_mem:branch ∈ trunk.2twig_mem:twig ∈ branch.2leaf_mem:leaf ∈ twig.2heq:C = (trunk.1, branch.1, twig.1, leaf.1)⊢ ∃ 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) = C
  exact ⟨trunk, trunk_mem, branch, branch_mem, twig, twig_mem, leaf, leaf_mem, heq.symm⟩All goals completed! 🐙