-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Model.lean
theorem updateAllBuckets [BEq α] [Hashable α] [LawfulHashable α] {m : Array (AssocList α β)}
    {f : AssocList α β → AssocList α δ} (hf : ∀ l p, p ∈ (f l).toList → containsKey p.1 l.toList)
    (hm : IsHashSelf m) : IsHashSelf (updateAllBuckets m f)

Proof state:
α : Type u
β : α → Type v
δ : α → Type w
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
m : Array (AssocList α β)
f : AssocList α β → AssocList α δ
hf : ∀ (l : AssocList α β) (p : (a : α) × δ a), p ∈ (f l).toList → containsKey p.fst l.toList = true
hm : IsHashSelf m
j : Nat
hj : j < (Array.map f m).size
h : 0 < m.size
p : (a : α) × δ a
hp : p ∈ (f m[j]).toList
⊢ (mkIdx m.size h (hash p.fst)).val.toNat = j

Tactic:
rcases containsKey_eq_true_iff_exists_mem.1 (hf _ _ hp) with ⟨q, hq₁, hq₂⟩

Result:
case intro.intro
α : Type u
β : α → Type v
δ : α → Type w
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
m : Array (AssocList α β)
f : AssocList α β → AssocList α δ
hf : ∀ (l : AssocList α β) (p : (a : α) × δ a), p ∈ (f l).toList → containsKey p.fst l.toList = true
hm : IsHashSelf m
j : Nat
hj : j < (Array.map f m).size
h : 0 < m.size
p : (a : α) × δ a
hp : p ∈ (f m[j]).toList
q : (a : α) × β a
hq₁ : q ∈ m[j].toList
hq₂ : (q.fst == p.fst) = true
⊢ (mkIdx m.size h (hash p.fst)).val.toNat = j

Proof state:
α : Type u
β : α → Type v
δ : α → Type w
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
m : Array (AssocList α β)
f : AssocList α β → AssocList α δ
hf : ∀ (l : AssocList α β) (p : (a : α) × δ a), p ∈ (f l).toList → containsKey p.fst l.toList = true
hm : IsHashSelf m
⊢ IsHashSelf (Array.map f m)

Tactic:
refine ⟨fun j hj => ?_⟩

Result:
α : Type u
β : α → Type v
δ : α → Type w
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
m : Array (AssocList α β)
f : AssocList α β → AssocList α δ
hf : ∀ (l : AssocList α β) (p : (a : α) × δ a), p ∈ (f l).toList → containsKey p.fst l.toList = true
hm : IsHashSelf m
j : Nat
hj : j < (Array.map f m).size
⊢ HashesTo (Array.map f m)[j].toList j (Array.map f m).size

Proof state:
α : Type u
β : α → Type v
δ : α → Type w
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
m : Array (AssocList α β)
f : AssocList α β → AssocList α δ
hf : ∀ (l : AssocList α β) (p : (a : α) × δ a), p ∈ (f l).toList → containsKey p.fst l.toList = true
hm : IsHashSelf m
⊢ IsHashSelf (Internal.updateAllBuckets m f)

Tactic:
rw [Internal.updateAllBuckets]

Result:
α : Type u
β : α → Type v
δ : α → Type w
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
m : Array (AssocList α β)
f : AssocList α β → AssocList α δ
hf : ∀ (l : AssocList α β) (p : (a : α) × δ a), p ∈ (f l).toList → containsKey p.fst l.toList = true
hm : IsHashSelf m
⊢ IsHashSelf (Array.map f m)

Proof state:
α : Type u
β : α → Type v
δ : α → Type w
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
m : Array (AssocList α β)
f : AssocList α β → AssocList α δ
hf : ∀ (l : AssocList α β) (p : (a : α) × δ a), p ∈ (f l).toList → containsKey p.fst l.toList = true
hm : IsHashSelf m
j : Nat
hj : j < (Array.map f m).size
⊢ HashesTo (Array.map f m)[j].toList j (Array.map f m).size

Tactic:
simp only [Array.getElem_map, Array.size_map]

Result:
α : Type u
β : α → Type v
δ : α → Type w
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
m : Array (AssocList α β)
f : AssocList α β → AssocList α δ
hf : ∀ (l : AssocList α β) (p : (a : α) × δ a), p ∈ (f l).toList → containsKey p.fst l.toList = true
hm : IsHashSelf m
j : Nat
hj : j < (Array.map f m).size
⊢ HashesTo (f m[j]).toList j m.size

Proof state:
case intro.intro
α : Type u
β : α → Type v
δ : α → Type w
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
m : Array (AssocList α β)
f : AssocList α β → AssocList α δ
hf : ∀ (l : AssocList α β) (p : (a : α) × δ a), p ∈ (f l).toList → containsKey p.fst l.toList = true
hm : IsHashSelf m
j : Nat
hj : j < (Array.map f m).size
h : 0 < m.size
p : (a : α) × δ a
hp : p ∈ (f m[j]).toList
q : (a : α) × β a
hq₁ : q ∈ m[j].toList
hq₂ : (q.fst == p.fst) = true
⊢ (mkIdx m.size h (hash p.fst)).val.toNat = j

Tactic:
rw [← hash_eq hq₂, (hm.hashes_to _ _).hash_self _ _ hq₁]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
δ : α → Type w
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
m : Array (AssocList α β)
f : AssocList α β → AssocList α δ
hf : ∀ (l : AssocList α β) (p : (a : α) × δ a), p ∈ (f l).toList → containsKey p.fst l.toList = true
hm : IsHashSelf m
j : Nat
hj : j < (Array.map f m).size
⊢ HashesTo (f m[j]).toList j m.size

Tactic:
refine ⟨fun h p hp => ?_⟩

Result:
α : Type u
β : α → Type v
δ : α → Type w
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
m : Array (AssocList α β)
f : AssocList α β → AssocList α δ
hf : ∀ (l : AssocList α β) (p : (a : α) × δ a), p ∈ (f l).toList → containsKey p.fst l.toList = true
hm : IsHashSelf m
j : Nat
hj : j < (Array.map f m).size
h : 0 < m.size
p : (a : α) × δ a
hp : p ∈ (f m[j]).toList
⊢ (mkIdx m.size h (hash p.fst)).val.toNat = j