Theorem: Lean.PersistentHashMap.toList'_empty (Lean4Lean/Verify/Axioms.lean)

State before:
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
⊢ toList' empty = []
Tactic:
have this n : @Node.toList' α β (.entries ⟨.replicate n .null⟩) = [] := by
  simp [Node.toList']
  induction n <;> simp [*]
State after:
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
this : ∀ (n : Nat), Node.toList' (Node.entries { data := List.replicate n Entry.null }) = []
⊢ toList' empty = []

State before:
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
this : ∀ (n : Nat), Node.toList' (Node.entries { data := List.replicate n Entry.null }) = []
⊢ toList' empty = []
Tactic:
apply this
State after:
no goals

State before:
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
n : Nat
⊢ Node.toList' (Node.entries { data := List.replicate n Entry.null }) = []
Tactic:
simp [Node.toList']
State after:
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
n : Nat
⊢ Node.rec_2 (fun x => id) (fun ks xs x => List.zip ks.data xs.data) (fun x => id) [] (fun x x l1 l2 => l1 ++ l2)
      (fun a b => [(a, b)]) (fun x => id) [] (List.replicate n Entry.null) =
    []

State before:
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
n : Nat
⊢ Node.rec_2 (fun x => id) (fun ks xs x => List.zip ks.data xs.data) (fun x => id) [] (fun x x l1 l2 => l1 ++ l2)
      (fun a b => [(a, b)]) (fun x => id) [] (List.replicate n Entry.null) =
    []
Tactic:
induction n <;> simp [*]
State after:
no goals