-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Model.lean
theorem uset [BEq α] [Hashable α] {m : Array (AssocList α β)} {i : USize} {h : i.toNat < m.size}
    {d : AssocList α β}
    (hd : HashesTo m[i].toList i.toNat m.size → HashesTo d.toList i.toNat m.size)
    (hm : IsHashSelf m) : IsHashSelf (m.uset i d h)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Array (AssocList α β)
i : USize
h : i.toNat < m.size
d : AssocList α β
hd : HashesTo m[i].toList i.toNat m.size → HashesTo d.toList i.toNat m.size
hm : IsHashSelf m
j : Nat
hj : j < (m.uset i d h).size
⊢ HashesTo (m.uset i d h)[j].toList j (m.uset i d h).size

Tactic:
simp only [Array.uset, Array.getElem_set, Array.size_set]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Array (AssocList α β)
i : USize
h : i.toNat < m.size
d : AssocList α β
hd : HashesTo m[i].toList i.toNat m.size → HashesTo d.toList i.toNat m.size
hm : IsHashSelf m
j : Nat
hj : j < (m.uset i d h).size
⊢ HashesTo (if i.toNat = j then d else m[j]).toList j m.size

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Array (AssocList α β)
i : USize
h : i.toNat < m.size
d : AssocList α β
hd : HashesTo m[i].toList i.toNat m.size → HashesTo d.toList i.toNat m.size
hm : IsHashSelf m
j : Nat
hj : j < (m.uset i d h).size
h✝ : ¬i.toNat = j
⊢ j < m.size

Tactic:
simpa using hj

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Array (AssocList α β)
i : USize
h : i.toNat < m.size
d : AssocList α β
hd : HashesTo m[i].toList i.toNat m.size → HashesTo d.toList i.toNat m.size
hm : IsHashSelf m
j : Nat
hj : j < (m.uset i d h).size
hij : i.toNat = j
⊢ HashesTo d.toList j m.size

Tactic:
exact hij ▸ (hd (hm.hashes_to _ _))

Result:
no goals

Proof state:
case isTrue
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Array (AssocList α β)
i : USize
h : i.toNat < m.size
d : AssocList α β
hd : HashesTo m[i].toList i.toNat m.size → HashesTo d.toList i.toNat m.size
hm : IsHashSelf m
j : Nat
hj : j < (m.uset i d h).size
h✝ : i.toNat = j
⊢ HashesTo d.toList j m.size

Tactic:
next hij => exact hij ▸ (hd (hm.hashes_to _ _))

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Array (AssocList α β)
i : USize
h : i.toNat < m.size
d : AssocList α β
hd : HashesTo m[i].toList i.toNat m.size → HashesTo d.toList i.toNat m.size
hm : IsHashSelf m
⊢ IsHashSelf (m.uset i d h)

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

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Array (AssocList α β)
i : USize
h : i.toNat < m.size
d : AssocList α β
hd : HashesTo m[i].toList i.toNat m.size → HashesTo d.toList i.toNat m.size
hm : IsHashSelf m
j : Nat
hj : j < (m.uset i d h).size
⊢ HashesTo (m.uset i d h)[j].toList j (m.uset i d h).size

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Array (AssocList α β)
i : USize
h : i.toNat < m.size
d : AssocList α β
hd : HashesTo m[i].toList i.toNat m.size → HashesTo d.toList i.toNat m.size
hm : IsHashSelf m
j : Nat
hj : j < (m.uset i d h).size
⊢ HashesTo (if i.toNat = j then d else m[j]).toList j m.size

Tactic:
split

Result:
case isTrue
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Array (AssocList α β)
i : USize
h : i.toNat < m.size
d : AssocList α β
hd : HashesTo m[i].toList i.toNat m.size → HashesTo d.toList i.toNat m.size
hm : IsHashSelf m
j : Nat
hj : j < (m.uset i d h).size
h✝ : i.toNat = j
⊢ HashesTo d.toList j m.size

case isFalse
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Array (AssocList α β)
i : USize
h : i.toNat < m.size
d : AssocList α β
hd : HashesTo m[i].toList i.toNat m.size → HashesTo d.toList i.toNat m.size
hm : IsHashSelf m
j : Nat
hj : j < (m.uset i d h).size
h✝ : ¬i.toNat = j
⊢ HashesTo m[j].toList j m.size

Proof state:
case isFalse
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Array (AssocList α β)
i : USize
h : i.toNat < m.size
d : AssocList α β
hd : HashesTo m[i].toList i.toNat m.size → HashesTo d.toList i.toNat m.size
hm : IsHashSelf m
j : Nat
hj : j < (m.uset i d h).size
h✝ : ¬i.toNat = j
⊢ HashesTo m[j].toList j m.size

Tactic:
exact hm.hashes_to j (by simpa using hj)

Result:
no goals