-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Model.lean
theorem updateBucket [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α]
    {m : Array (AssocList α β)} {h : 0 < m.size} {a : α} {f : AssocList α β → AssocList α β}
    (hf : ∀ l p, p ∈ (f l).toList → containsKey p.1 l.toList ∨ hash p.1 = hash a)
    (hm : IsHashSelf m) : IsHashSelf (updateBucket m h a f)

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

Tactic:
rcases hf _ _ hp with (hf|hf)

Result:
case inl
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : PartialEquivBEq α
inst✝ : LawfulHashable α
m : Array (AssocList α β)
h : 0 < m.size
a : α
f : AssocList α β → AssocList α β
hf✝ :
  ∀ (l : AssocList α β) (p : (a : α) × β a), p ∈ (f l).toList → containsKey p.fst l.toList = true ∨ hash p.fst = hash a
hm : IsHashSelf m
h' : HashesTo m[(mkIdx m.size h (hash a)).val].toList (mkIdx m.size h (hash a)).val.toNat m.size
x✝ : 0 < m.size
p : (a : α) × β a
hp : p ∈ (f m[(mkIdx m.size h (hash a)).val]).toList
hf : containsKey p.fst m[(mkIdx m.size h (hash a)).val].toList = true
⊢ (mkIdx m.size x✝ (hash p.fst)).val.toNat = (mkIdx m.size h (hash a)).val.toNat

case inr
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : PartialEquivBEq α
inst✝ : LawfulHashable α
m : Array (AssocList α β)
h : 0 < m.size
a : α
f : AssocList α β → AssocList α β
hf✝ :
  ∀ (l : AssocList α β) (p : (a : α) × β a), p ∈ (f l).toList → containsKey p.fst l.toList = true ∨ hash p.fst = hash a
hm : IsHashSelf m
h' : HashesTo m[(mkIdx m.size h (hash a)).val].toList (mkIdx m.size h (hash a)).val.toNat m.size
x✝ : 0 < m.size
p : (a : α) × β a
hp : p ∈ (f m[(mkIdx m.size h (hash a)).val]).toList
hf : hash p.fst = hash a
⊢ (mkIdx m.size x✝ (hash p.fst)).val.toNat = (mkIdx m.size h (hash a)).val.toNat

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

Tactic:
rw [← h'.hash_self h _ hq₁, hash_eq hq₂]

Result:
no goals

Proof state:
case inl
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : PartialEquivBEq α
inst✝ : LawfulHashable α
m : Array (AssocList α β)
h : 0 < m.size
a : α
f : AssocList α β → AssocList α β
hf✝ :
  ∀ (l : AssocList α β) (p : (a : α) × β a), p ∈ (f l).toList → containsKey p.fst l.toList = true ∨ hash p.fst = hash a
hm : IsHashSelf m
h' : HashesTo m[(mkIdx m.size h (hash a)).val].toList (mkIdx m.size h (hash a)).val.toNat m.size
x✝ : 0 < m.size
p : (a : α) × β a
hp : p ∈ (f m[(mkIdx m.size h (hash a)).val]).toList
hf : containsKey p.fst m[(mkIdx m.size h (hash a)).val].toList = true
⊢ (mkIdx m.size x✝ (hash p.fst)).val.toNat = (mkIdx m.size h (hash a)).val.toNat

Tactic:
rw [containsKey_eq_true_iff_exists_mem] at hf

Result:
case inl
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : PartialEquivBEq α
inst✝ : LawfulHashable α
m : Array (AssocList α β)
h : 0 < m.size
a : α
f : AssocList α β → AssocList α β
hf✝ :
  ∀ (l : AssocList α β) (p : (a : α) × β a), p ∈ (f l).toList → containsKey p.fst l.toList = true ∨ hash p.fst = hash a
hm : IsHashSelf m
h' : HashesTo m[(mkIdx m.size h (hash a)).val].toList (mkIdx m.size h (hash a)).val.toNat m.size
x✝ : 0 < m.size
p : (a : α) × β a
hp : p ∈ (f m[(mkIdx m.size h (hash a)).val]).toList
hf : ∃ p_1, p_1 ∈ m[(mkIdx m.size h (hash a)).val].toList ∧ (p_1.fst == p.fst) = true
⊢ (mkIdx m.size x✝ (hash p.fst)).val.toNat = (mkIdx m.size h (hash a)).val.toNat

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : PartialEquivBEq α
inst✝ : LawfulHashable α
m : Array (AssocList α β)
h : 0 < m.size
a : α
f : AssocList α β → AssocList α β
hf :
  ∀ (l : AssocList α β) (p : (a : α) × β a), p ∈ (f l).toList → containsKey p.fst l.toList = true ∨ hash p.fst = hash a
hm : IsHashSelf m
⊢ IsHashSelf
    (match mkIdx m.size h (hash a) with
    | ⟨i, h⟩ => m.uset i (f m[i]) h)

Tactic:
refine IsHashSelf.uset (fun h' => ⟨fun _ p hp => ?_⟩) hm

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

Proof state:
case inl
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : PartialEquivBEq α
inst✝ : LawfulHashable α
m : Array (AssocList α β)
h : 0 < m.size
a : α
f : AssocList α β → AssocList α β
hf✝ :
  ∀ (l : AssocList α β) (p : (a : α) × β a), p ∈ (f l).toList → containsKey p.fst l.toList = true ∨ hash p.fst = hash a
hm : IsHashSelf m
h' : HashesTo m[(mkIdx m.size h (hash a)).val].toList (mkIdx m.size h (hash a)).val.toNat m.size
x✝ : 0 < m.size
p : (a : α) × β a
hp : p ∈ (f m[(mkIdx m.size h (hash a)).val]).toList
hf : ∃ p_1, p_1 ∈ m[(mkIdx m.size h (hash a)).val].toList ∧ (p_1.fst == p.fst) = true
⊢ (mkIdx m.size x✝ (hash p.fst)).val.toNat = (mkIdx m.size h (hash a)).val.toNat

Tactic:
rcases hf with ⟨q, hq₁, hq₂⟩

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