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

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

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

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

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

Tactic:
exact .inl <| containsKey_of_mem hp

Result:
no goals

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

Tactic:
rw [Const.mem_alterKey_of_key_not_beq _ h] at hp

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

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

Tactic:
exact .inr <| hash_eq h

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : EquivBEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : Raw.WFImp m.val
a : α
f : Option β → Option β
⊢ IsHashSelf (updateBucket m.val.buckets ⋯ a (AssocList.Const.alter a f))

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

Result:
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : EquivBEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : Raw.WFImp m.val
a : α
f : Option β → Option β
l : AssocList α fun x => β
p : (_ : α) × β
hp : p ∈ (AssocList.Const.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✝² : EquivBEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : Raw.WFImp m.val
a : α
f : Option β → Option β
l : AssocList α fun x => β
p : (_ : α) × β
hp : p ∈ Const.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✝² : EquivBEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h✝ : Raw.WFImp m.val
a : α
f : Option β → Option β
l : AssocList α fun x => β
p : (_ : α) × β
hp : p ∈ Const.alterKey a f l.toList
h : (p.fst == a) = true
⊢ containsKey p.fst l.toList = true ∨ hash p.fst = hash a

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

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

Tactic:
rw [Bool.not_eq_true] at h

Result:
case neg
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : EquivBEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h✝ : Raw.WFImp m.val
a : α
f : Option β → Option β
l : AssocList α fun x => β
p : (_ : α) × β
hp : p ∈ Const.alterKey a f l.toList
h : (p.fst == a) = false
⊢ containsKey p.fst l.toList = true ∨ hash p.fst = hash a