-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem isHashSelf_updateBucket_alter [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β}
    (h : Raw.WFImp m.1) {a : α} {f : Option (β a) → Option (β a)} :
    IsHashSelf (updateBucket m.1.buckets m.2 a (AssocList.alter a f))

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
l : AssocList α β
p : (a : α) × β a
hp : p ∈ (AssocList.alter a f l).toList
⊢ containsKey p.fst l.toList = true ∨ hash p.fst = hash a

Tactic:
rw [AssocList.toList_alter.mem_iff] at hp

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
l : AssocList α β
p : (a : α) × β a
hp : p ∈ alterKey a f l.toList
⊢ containsKey p.fst l.toList = true ∨ hash p.fst = hash a

Proof state:
case pos
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h✝ : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
l : AssocList α β
p : (a : α) × β a
hp : p ∈ alterKey a f l.toList
h : p.fst = a
⊢ containsKey p.fst l.toList = true ∨ hash p.fst = hash a

Tactic:
exact .inr <| congrArg hash h

Result:
no goals

Proof state:
case neg
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h✝ : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
l : AssocList α β
p : (a : α) × β a
hp : p ∈ alterKey a f l.toList
h : ¬p.fst = a
⊢ containsKey p.fst l.toList = true ∨ hash p.fst = hash a

Tactic:
rw [mem_alterKey_of_key_ne _ h] at hp

Result:
case neg
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h✝ : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
l : AssocList α β
p : (a : α) × β a
hp : p ∈ l.toList
h : ¬p.fst = a
⊢ containsKey p.fst l.toList = true ∨ hash p.fst = hash a

Proof state:
case neg
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h✝ : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
l : AssocList α β
p : (a : α) × β a
hp : p ∈ l.toList
h : ¬p.fst = a
⊢ containsKey p.fst l.toList = true ∨ hash p.fst = hash a

Tactic:
exact .inl <| containsKey_of_mem hp

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
⊢ IsHashSelf (updateBucket m.val.buckets ⋯ a (AssocList.alter a f))

Tactic:
apply h.buckets_hash_self.updateBucket (fun l p hp => ?_)

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
l : AssocList α β
p : (a : α) × β a
hp : p ∈ (AssocList.alter a f l).toList
⊢ containsKey p.fst l.toList = true ∨ hash p.fst = hash a

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
l : AssocList α β
p : (a : α) × β a
hp : p ∈ alterKey a f l.toList
⊢ containsKey p.fst l.toList = true ∨ hash p.fst = hash a

Tactic:
by_cases h : p.fst = a

Result:
case pos
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h✝ : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
l : AssocList α β
p : (a : α) × β a
hp : p ∈ alterKey a f l.toList
h : p.fst = a
⊢ containsKey p.fst l.toList = true ∨ hash p.fst = hash a

case neg
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h✝ : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
l : AssocList α β
p : (a : α) × β a
hp : p ∈ alterKey a f l.toList
h : ¬p.fst = a
⊢ containsKey p.fst l.toList = true ∨ hash p.fst = hash a