Theorem: Lean.PersistentHashMap.WF.nodupKeys (Lean4Lean/Verify/Axioms.lean)

State before:
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
inst✝ : Std.HashMap.LawfulHashable α
m : PersistentHashMap α β
h : WF m
⊢ List.NodupKeys (toList' m)
Tactic:
induction h with
| empty => simp; exact .nil
| insert h1 h2 ih =>
  rw [h2.find?_eq] at h1
  refine (h2.toList'_insert _ _ h1).nodupKeys_iff.2 (List.nodupKeys_cons.2 ⟨?_, ih⟩)
  rintro ⟨a, b⟩ h3 rfl
  cases h1.symm.trans (ih.lookup_eq_some.2 h3)
State after:
no goals

State before:
case empty
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
inst✝ : Std.HashMap.LawfulHashable α
m : PersistentHashMap α β
⊢ List.NodupKeys (toList' PersistentHashMap.empty)
Tactic:
simp
State after:
case empty
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
inst✝ : Std.HashMap.LawfulHashable α
m : PersistentHashMap α β
⊢ List.NodupKeys []

State before:
case empty
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
inst✝ : Std.HashMap.LawfulHashable α
m : PersistentHashMap α β
⊢ List.NodupKeys []
Tactic:
exact .nil
State after:
no goals

State before:
case insert
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
inst✝ : Std.HashMap.LawfulHashable α
m m✝ : PersistentHashMap α β
a✝ : α
b✝ : β
h1 : find? m✝ a✝ = none
h2 : WF m✝
ih : List.NodupKeys (toList' m✝)
⊢ List.NodupKeys (toList' (PersistentHashMap.insert m✝ a✝ b✝))
Tactic:
rw [h2.find?_eq] at h1
State after:
case insert
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
inst✝ : Std.HashMap.LawfulHashable α
m m✝ : PersistentHashMap α β
a✝ : α
b✝ : β
h1 : List.lookup a✝ (toList' m✝) = none
h2 : WF m✝
ih : List.NodupKeys (toList' m✝)
⊢ List.NodupKeys (toList' (PersistentHashMap.insert m✝ a✝ b✝))

State before:
case insert
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
inst✝ : Std.HashMap.LawfulHashable α
m m✝ : PersistentHashMap α β
a✝ : α
b✝ : β
h1 : List.lookup a✝ (toList' m✝) = none
h2 : WF m✝
ih : List.NodupKeys (toList' m✝)
⊢ List.NodupKeys (toList' (PersistentHashMap.insert m✝ a✝ b✝))
Tactic:
refine (h2.toList'_insert _ _ h1).nodupKeys_iff.2 (List.nodupKeys_cons.2 ⟨?_, ih⟩)
State after:
case insert
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
inst✝ : Std.HashMap.LawfulHashable α
m m✝ : PersistentHashMap α β
a✝ : α
b✝ : β
h1 : List.lookup a✝ (toList' m✝) = none
h2 : WF m✝
ih : List.NodupKeys (toList' m✝)
⊢ ∀ (a' : α × β), a' ∈ toList' m✝ → (a✝, b✝).fst ≠ a'.fst

State before:
case insert
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
inst✝ : Std.HashMap.LawfulHashable α
m m✝ : PersistentHashMap α β
a✝ : α
b✝ : β
h1 : List.lookup a✝ (toList' m✝) = none
h2 : WF m✝
ih : List.NodupKeys (toList' m✝)
⊢ ∀ (a' : α × β), a' ∈ toList' m✝ → (a✝, b✝).fst ≠ a'.fst
Tactic:
rintro ⟨a, b⟩ h3 rfl
State after:
case insert.mk
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
inst✝ : Std.HashMap.LawfulHashable α
m m✝ : PersistentHashMap α β
a✝ : α
b✝ : β
h1 : List.lookup a✝ (toList' m✝) = none
h2 : WF m✝
ih : List.NodupKeys (toList' m✝)
b : β
h3 : ((a✝, b✝).fst, b) ∈ toList' m✝
⊢ False

State before:
case insert.mk
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
inst✝ : Std.HashMap.LawfulHashable α
m m✝ : PersistentHashMap α β
a✝ : α
b✝ : β
h1 : List.lookup a✝ (toList' m✝) = none
h2 : WF m✝
ih : List.NodupKeys (toList' m✝)
b : β
h3 : ((a✝, b✝).fst, b) ∈ toList' m✝
⊢ False
Tactic:
cases h1.symm.trans (ih.lookup_eq_some.2 h3)
State after:
no goals