-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem isHashSelf_reinsertAux [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α]
    (data : {d : Array (AssocList α β) // 0 < d.size}) (a : α) (b : β a) (h : IsHashSelf data.1) :
    IsHashSelf (reinsertAux hash data a b).1

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
data : { d // 0 < d.size }
a : α
b : β a
h : IsHashSelf data.val
⊢ IsHashSelf (reinsertAux hash data a b).val

Tactic:
rw [reinsertAux_eq]

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
data : { d // 0 < d.size }
a : α
b : β a
h : IsHashSelf data.val
⊢ IsHashSelf (updateBucket data.val ⋯ a fun l => AssocList.cons a b l)

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
data : { d // 0 < d.size }
a : α
b : β a
h : IsHashSelf data.val
l : AssocList α β
p : (a : α) × β a
hp : p ∈ (AssocList.cons a b l).toList
⊢ containsKey p.fst l.toList = true ∨ hash p.fst = hash a

Tactic:
simp only [AssocList.toList_cons, mem_cons] at hp

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
data : { d // 0 < d.size }
a : α
b : β a
h : IsHashSelf data.val
l : AssocList α β
p : (a : α) × β a
hp : p = ⟨a, b⟩ ∨ p ∈ l.toList
⊢ containsKey p.fst l.toList = true ∨ hash p.fst = hash a

Proof state:
case inr
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
data : { d // 0 < d.size }
a : α
b : β a
h : IsHashSelf data.val
l : AssocList α β
p : (a : α) × β a
hp : p ∈ l.toList
⊢ containsKey p.fst l.toList = true ∨ hash p.fst = hash a

Tactic:
exact Or.inl (containsKey_of_mem hp)

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
data : { d // 0 < d.size }
a : α
b : β a
h : IsHashSelf data.val
l : AssocList α β
p : (a : α) × β a
hp : p = ⟨a, b⟩ ∨ p ∈ l.toList
⊢ containsKey p.fst l.toList = true ∨ hash p.fst = hash a

Tactic:
rcases hp with (rfl|hp)

Result:
case inl
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
data : { d // 0 < d.size }
a : α
b : β a
h : IsHashSelf data.val
l : AssocList α β
⊢ containsKey ⟨a, b⟩.fst l.toList = true ∨ hash ⟨a, b⟩.fst = hash a

case inr
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
data : { d // 0 < d.size }
a : α
b : β a
h : IsHashSelf data.val
l : AssocList α β
p : (a : α) × β a
hp : p ∈ l.toList
⊢ containsKey p.fst l.toList = true ∨ hash p.fst = hash a

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
data : { d // 0 < d.size }
a : α
b : β a
h : IsHashSelf data.val
⊢ IsHashSelf (updateBucket data.val ⋯ a fun l => AssocList.cons a b l)

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

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
data : { d // 0 < d.size }
a : α
b : β a
h : IsHashSelf data.val
l : AssocList α β
p : (a : α) × β a
hp : p ∈ (AssocList.cons a b l).toList
⊢ containsKey p.fst l.toList = true ∨ hash p.fst = hash a

Proof state:
case inl
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
data : { d // 0 < d.size }
a : α
b : β a
h : IsHashSelf data.val
l : AssocList α β
⊢ containsKey ⟨a, b⟩.fst l.toList = true ∨ hash ⟨a, b⟩.fst = hash a

Tactic:
exact Or.inr rfl

Result:
no goals