Projects.Util.Data.Trie.Raw0

source

inductive Trie.Raw₀ (α : Type u_1) (β : Type u_2) [DecidableEq α] [Hashable α] :

Type (max u_1 u_2)

mk {α : Type u_1} {β : Type u_2} [DecidableEq α] [Hashable α] : Option β → (mp : Std.DHashMap.Raw α fun (x : α) => Raw₀ α β) → Raw₀ α β

Instances For

source

def Trie.Raw₀.val {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] :

Raw₀ α β → Option β

Equations

(Trie.Raw₀.mk val mp).val = val

Instances For

source

def Trie.Raw₀.mp {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] :

Raw₀ α β → Std.DHashMap.Raw α fun (x : α) => Raw₀ α β

Equations

(Trie.Raw₀.mk val mp).mp = mp

Instances For

source

@[simp]

theorem Trie.Raw₀.val_mk {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {val : Option β} {mp : Std.DHashMap.Raw α fun (x : α) => Raw₀ α β} :

(mk val mp).val = val

source

@[simp]

theorem Trie.Raw₀.mp_mk {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {val : Option β} {mp : Std.DHashMap.Raw α fun (x : α) => Raw₀ α β} :

(mk val mp).mp = mp

source

def Trie.Raw₀.isEmpty {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (t : Raw₀ α β) :

Prop

Equations

t.isEmpty = (t.val = none ∧ t.mp.isEmpty = true)

Instances For

source

@[instance_reducible]

instance Trie.Raw₀.instDecidableIsEmpty {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t : Raw₀ α β} :

Decidable t.isEmpty

Equations

Trie.Raw₀.instDecidableIsEmpty = match h : t.val.isNone && t.mp.isEmpty with | true => isTrue ⋯ | false => isFalse ⋯

source

class inductive Trie.Raw₀.WF {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] :

Raw₀ α β → Prop

mk {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {val : Option β} {mp : Std.DHashMap.Raw α fun (x : α) => Raw₀ α β} : mp.WF → (∀ {k : α} {t : Raw₀ α β}, mp.get? k = some t → ¬t.isEmpty) → (∀ {k : α} {t : Raw₀ α β}, mp.get? k = some t → t.WF) → (Raw₀.mk val mp).WF

Instances

source

@[simp]

theorem Trie.Raw₀.WF.mp {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t : Raw₀ α β} [wf : t.WF] :

t.mp.WF

source

theorem Trie.Raw₀.WF.get1? {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t : Raw₀ α β} [wf : t.WF] {k : α} {t' : Raw₀ α β} (h : t.mp.get? k = some t') :

t'.WF

source

theorem Trie.Raw₀.WF.not_empty_get? {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t : Raw₀ α β} [wf : t.WF] {k : α} {t' : Raw₀ α β} (h : t.mp.get? k = some t') :

¬t'.isEmpty

source

theorem Trie.Raw₀.rec_2_eq {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {arr : Array (Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β)} {M₁ : Raw₀ α β → Sort u_3} {M₂ : (Std.DHashMap.Raw α fun (x : α) => Raw₀ α β) → Sort u_3} {M₃ : Array (Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β) → Sort u_3} {M₄ : List (Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β) → Sort u_3} {M₅ : (Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β) → Sort u_3} {H₁ : (a : Option β) → (mp : Std.DHashMap.Raw α fun (x : α) => Raw₀ α β) → M₂ mp → M₁ (mk a mp)} {H₂ : (size : ℕ) → (buckets : Array (Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β)) → M₃ buckets → M₂ { size := size, buckets := buckets }} {H₃ : (toList : List (Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β)) → M₄ toList → M₃ { toList := toList }} {H₄ : M₄ []} {H₅ : (head : Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β) → (tail : List (Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β)) → M₅ head → M₄ tail → M₄ (head :: tail)} {H₆ : M₅ Std.DHashMap.Internal.AssocList.nil} {H₇ : (key : α) → (value : (fun (x : α) => Raw₀ α β) key) → (tail : Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β) → M₁ value → M₅ tail → M₅ (Std.DHashMap.Internal.AssocList.cons key value tail)} :

rec_2 H₁ H₂ H₃ H₄ H₅ H₆ H₇ arr = H₃ arr.toList (rec_3 H₁ H₂ H₃ H₄ H₅ H₆ H₇ arr.toList)

source

theorem Trie.Raw₀.rec_3_eq {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {xs : List (Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β)} {M₁ : Raw₀ α β → Sort u_3} {M₂ : (Std.DHashMap.Raw α fun (x : α) => Raw₀ α β) → Sort u_3} {M₃ : Array (Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β) → Sort u_3} {M₄ : List (Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β) → Sort u_3} {M₅ : (Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β) → Sort u_3} {H₁ : (a : Option β) → (mp : Std.DHashMap.Raw α fun (x : α) => Raw₀ α β) → M₂ mp → M₁ (mk a mp)} {H₂ : (size : ℕ) → (buckets : Array (Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β)) → M₃ buckets → M₂ { size := size, buckets := buckets }} {H₃ : (toList : List (Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β)) → M₄ toList → M₃ { toList := toList }} {H₄ : M₄ []} {H₅ : (head : Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β) → (tail : List (Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β)) → M₅ head → M₄ tail → M₄ (head :: tail)} {H₆ : M₅ Std.DHashMap.Internal.AssocList.nil} {H₇ : (key : α) → (value : (fun (x : α) => Raw₀ α β) key) → (tail : Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β) → M₁ value → M₅ tail → M₅ (Std.DHashMap.Internal.AssocList.cons key value tail)} :

rec_3 H₁ H₂ H₃ H₄ H₅ H₆ H₇ xs = List.rec H₄ (fun (x : Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β) (xs : List (Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β)) (acc : M₄ xs) => H₅ x xs (rec_4 H₁ H₂ H₃ H₄ H₅ H₆ H₇ x) acc) xs

source

theorem Trie.Raw₀.rec_4_eq {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {xs : Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β} {M₁ : Raw₀ α β → Sort u_3} {M₂ : (Std.DHashMap.Raw α fun (x : α) => Raw₀ α β) → Sort u_3} {M₃ : Array (Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β) → Sort u_3} {M₄ : List (Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β) → Sort u_3} {M₅ : Sort u_3} {H₁ : (a : Option β) → (mp : Std.DHashMap.Raw α fun (x : α) => Raw₀ α β) → M₂ mp → M₁ (mk a mp)} {H₂ : (size : ℕ) → (buckets : Array (Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β)) → M₃ buckets → M₂ { size := size, buckets := buckets }} {H₃ : (toList : List (Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β)) → M₄ toList → M₃ { toList := toList }} {H₄ : M₄ []} {H₅ : (head : Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β) → (tail : List (Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β)) → M₅ → M₄ tail → M₄ (head :: tail)} {H₆ : M₅} {H₇ : (key : α) → (value : (fun (x : α) => Raw₀ α β) key) → (Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β) → M₁ value → M₅ → M₅} :

rec_4 H₁ H₂ H₃ H₄ H₅ H₆ H₇ xs = List.rec H₆ (fun (x : (_ : α) × Raw₀ α β) (xs : List ((_ : α) × Raw₀ α β)) (acc : M₅) => H₇ x.fst x.snd (Std.DHashMap.Internal.AssocList.ofList xs) (rec H₁ H₂ H₃ H₄ H₅ H₆ H₇ x.snd) acc) xs.toList

source

noncomputable def Trie.Raw₀.depthAux {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (t : Raw₀ α β) :

ℕ

Equations

t.depthAux = (fun (motive_1 : Trie.Raw₀ α β → Type) (motive_2 : (Std.DHashMap.Raw α fun (x : α) => Trie.Raw₀ α β) → Type) (motive_3 : Array (Std.DHashMap.Internal.AssocList α fun (x : α) => Trie.Raw₀ α β) → Type) (motive_4 : List (Std.DHashMap.Internal.AssocList α fun (x : α) => Trie.Raw₀ α β) → Type) (motive_5 : (Std.DHashMap.Internal.AssocList α fun (x : α) => Trie.Raw₀ α β) → Type) => t.recOn) (fun (x : Trie.Raw₀ α β) => ℕ) (fun (x : Std.DHashMap.Raw α fun (x : α) => Trie.Raw₀ α β) => ℕ) (fun (x : Array (Std.DHashMap.Internal.AssocList α fun (x : α) => Trie.Raw₀ α β)) => ℕ) (fun (x : List (Std.DHashMap.Internal.AssocList α fun (x : α) => Trie.Raw₀ α β)) => ℕ) (fun (x : Std.DHashMap.Internal.AssocList α fun (x : α) => Trie.Raw₀ α β) => ℕ) (fun (x : Option β) (x_1 : Std.DHashMap.Raw α fun (x : α) => Trie.Raw₀ α β) (n : ℕ) => n) (fun (x : ℕ) (x_1 : Array (Std.DHashMap.Internal.AssocList α fun (x : α) => Trie.Raw₀ α β)) (n : ℕ) => n) (fun (x : List (Std.DHashMap.Internal.AssocList α fun (x : α) => Trie.Raw₀ α β)) (n : ℕ) => n) 0 (fun (x : Std.DHashMap.Internal.AssocList α fun (x : α) => Trie.Raw₀ α β) (x_1 : List (Std.DHashMap.Internal.AssocList α fun (x : α) => Trie.Raw₀ α β)) (n m : ℕ) => max n m) 0 fun (x : α) (x_1 : Trie.Raw₀ α β) (x_2 : Std.DHashMap.Internal.AssocList α fun (x : α) => Trie.Raw₀ α β) (n m : ℕ) => max (n + 1) m

Instances For

source

theorem Trie.Raw₀.depthAux_le {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t : Raw₀ α β} [wf : t.WF] {k : α} {t' : Raw₀ α β} (h : t.mp.get? k = some t') :

t'.depthAux < t.depthAux

source

theorem Trie.Raw₀.depthAux_le_mk {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {val : Option β} {mp : Std.DHashMap.Raw α fun (x : α) => Raw₀ α β} (wf : (mk val mp).WF) {k : α} {t : Raw₀ α β} (h : mp.get? k = some t) :

t.depthAux < (mk val mp).depthAux

source

@[irreducible]

def Trie.Raw₀.recAux {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {γ : Raw₀ α β → Sort u_3} (t : Raw₀ α β) (wf : t.WF) (motive : (val : Option β) → (mp : Std.DHashMap.Raw α fun (x : α) => Raw₀ α β) → mp.WF → ((i : α) → (t : Raw₀ α β) → mp.get? i = some t → γ t) → γ (mk val mp)) :

γ t

Equations

(Trie.Raw₀.mk val mp).recAux wf_2 motive = motive val mp ⋯ fun (i : α) (t : Trie.Raw₀ α β) (h : mp.get? i = some t) => t.recAux ⋯ motive

Instances For

source

def Trie.Raw₀.rec' {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {γ : Raw₀ α β → Sort u_3} (t : Raw₀ α β) [wf : t.WF] (motive : (val : Option β) → (mp : Std.DHashMap.Raw α fun (x : α) => Raw₀ α β) → mp.WF → ((i : α) → (t : Raw₀ α β) → mp.get? i = some t → γ t) → γ (mk val mp)) :

γ t

Equations

t.rec' motive = t.recAux wf motive

Instances For

source

def Trie.Raw₀.depth {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (t : Raw₀ α β) [wf : t.WF] :

ℕ

Equations

t.depth = t.rec' fun (x : Option β) (mp : Std.DHashMap.Raw α fun (x : α) => Trie.Raw₀ α β) (h₁ : mp.WF) (f : (i : α) → (t : Trie.Raw₀ α β) → mp.get? i = some t → ℕ) => (fun (x : ℕ → (i : α) → (x : Trie.Raw₀ α β) → mp.get? i = some x → ℕ) => mp.foldWith h₁ x 0) fun (acc : ℕ) (i : α) (x : Trie.Raw₀ α β) (h₂ : mp.get? i = some x) => max acc (1 + f i x h₂)

Instances For

source

def Trie.Raw₀.empty {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] :

Raw₀ α β

Equations

Trie.Raw₀.empty = Trie.Raw₀.mk none ∅

Instances For

source

@[instance_reducible]

instance Trie.Raw₀.instEmptyCollection {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] :

EmptyCollection (Raw₀ α β)

Equations

Trie.Raw₀.instEmptyCollection = { emptyCollection := Trie.Raw₀.empty }

source

theorem Trie.Raw₀.empty_def {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] :

∅ = mk none ∅

source

instance Trie.Raw₀.instWFEmptyCollection {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] :

∅.WF

source

@[simp]

theorem Trie.Raw₀.rec'_mk {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {γ : Raw₀ α β → Sort u_3} {val : Option β} {mp : Std.DHashMap.Raw α fun (x : α) => Raw₀ α β} [wf : (mk val mp).WF] {motive : (val : Option β) → (mp : Std.DHashMap.Raw α fun (x : α) => Raw₀ α β) → mp.WF → ((i : α) → (t : Raw₀ α β) → mp.get? i = some t → γ t) → γ (mk val mp)} :

(mk val mp).rec' motive = motive val mp ⋯ fun (x : α) (t : Raw₀ α β) (h : mp.get? x = some t) => t.rec' motive

source

@[simp]

theorem Trie.Raw₀.depth_mk {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {val : Option β} {mp : Std.DHashMap.Raw α fun (x : α) => Raw₀ α β} [wf : (mk val mp).WF] :

(mk val mp).depth = mp.foldWith ⋯ (fun (acc : ℕ) (x : α) (t' : Raw₀ α β) (h : mp.get? x = some t') => max acc (1 + t'.depth)) 0

source

@[simp]

theorem Trie.Raw₀.depth_empty {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] :

∅.depth = 0

source

theorem Trie.Raw₀.depth_lt {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t : Raw₀ α β} [wf : t.WF] {k : α} {t' : Raw₀ α β} (h : t.mp.get? k = some t') :

t'.depth < t.depth

source

theorem Trie.Raw₀.WF.of_mem_toList {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t : Raw₀ α β} {p : (_ : α) × Raw₀ α β} [wf : t.WF] (h : p ∈ t.mp.toList) :

p.snd.WF

source

theorem Trie.Raw₀.wf_iff {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t : Raw₀ α β} :

t.WF ↔ t.mp.WF ∧ ∀ (k : α) (t₁ : Raw₀ α β), t.mp.get? k = some t₁ → t₁.WF ∧ ¬t₁.isEmpty

source

def Trie.Raw₀.setVal {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (t : Raw₀ α β) (val : Option β) :

Raw₀ α β

Equations

t.setVal val = Trie.Raw₀.mk val t.mp

Instances For

source

@[simp]

theorem Trie.Raw₀.setVal_mk {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {val val₁ : Option β} {mp : Std.DHashMap.Raw α fun (x : α) => Raw₀ α β} :

(mk val mp).setVal val₁ = mk val₁ mp

source

@[simp]

instance Trie.Raw₀.instWFSetVal {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t : Raw₀ α β} {x : Option β} [wf : t.WF] :

(t.setVal x).WF

source

@[simp]

theorem Trie.Raw₀.val_setVal {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t : Raw₀ α β} {val : Option β} :

(t.setVal val).val = val

source

@[simp]

theorem Trie.Raw₀.mp_setVal {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t : Raw₀ α β} {val : Option β} :

(t.setVal val).mp = t.mp

source

def Trie.Raw₀.erase1 {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (t : Raw₀ α β) (i : α) :

Raw₀ α β

Equations

t.erase1 i = Trie.Raw₀.mk t.val (t.mp.erase i)

Instances For

source

@[simp]

theorem Trie.Raw₀.erase1_mk {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {val : Option β} {mp : Std.DHashMap.Raw α fun (x : α) => Raw₀ α β} {i : α} :

(mk val mp).erase1 i = mk val (mp.erase i)

source

@[simp]

theorem Trie.Raw₀.val_erase1 {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t : Raw₀ α β} {i : α} :

(t.erase1 i).val = t.val

source

@[simp]

theorem Trie.Raw₀.mp_erase1 {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t : Raw₀ α β} {i : α} :

(t.erase1 i).mp = t.mp.erase i

source

@[simp]

instance Trie.Raw₀.instWFErase1 {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t : Raw₀ α β} {i : α} [wf : t.WF] :

(t.erase1 i).WF

source

def Trie.Raw₀.insert1 {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (t : Raw₀ α β) (i : α) (t₁ : Raw₀ α β) :

Raw₀ α β

Equations

t.insert1 i t₁ = if t₁.isEmpty then t.erase1 i else Trie.Raw₀.mk t.val (t.mp.insert i t₁)

Instances For

source

theorem Trie.Raw₀.insert1_mk {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {val : Option β} {mp : Std.DHashMap.Raw α fun (x : α) => Raw₀ α β} {i : α} {t₁ : Raw₀ α β} :

(mk val mp).insert1 i t₁ = mk val (if t₁.isEmpty then mp.erase i else mp.insert i t₁)

source

@[simp]

theorem Trie.Raw₀.val_insert1 {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t : Raw₀ α β} {i : α} {t₁ : Raw₀ α β} :

(t.insert1 i t₁).val = t.val

source

theorem Trie.Raw₀.mp_insert1 {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t t₁ : Raw₀ α β} {i : α} :

(t.insert1 i t₁).mp = if t₁.isEmpty then t.mp.erase i else t.mp.insert i t₁

source

@[simp]

instance Trie.Raw₀.instWFInsert1 {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t t₁ : Raw₀ α β} {i : α} [wf : t.WF] [wf₁ : t₁.WF] :

(t.insert1 i t₁).WF

source

def Trie.Raw₀.get1? {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (t : Raw₀ α β) (i : α) :

Option (Raw₀ α β)

Equations

t.get1? i = t.mp.get? i

Instances For

source

theorem Trie.Raw₀.get1?_erase1 {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t : Raw₀ α β} {i j : α} [wf : t.WF] :

(t.erase1 i).get1? j = if i = j then none else t.get1? j

source

theorem Trie.Raw₀.get1?_insert1 {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t : Raw₀ α β} {i j : α} {t₁ : Raw₀ α β} [wf : t.WF] :

(t.insert1 i t₁).get1? j = if i = j then if t₁.isEmpty then none else some t₁ else t.get1? j

source

@[simp]

theorem Trie.Raw₀.get1?_erase1_eq_some_iff {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t t₁ : Raw₀ α β} {i j : α} [wf : t.WF] :

(t.erase1 i).get1? j = some t₁ ↔ i ≠ j ∧ t.get1? j = some t₁