-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Model.lean
theorem toListModel_updateBucket [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α]
    {m : Raw₀ α β} (hm : Raw.WFImp m.1) {a : α} {f : AssocList α β → AssocList α β}
    {g : List ((a : α) × β a) → List ((a : α) × β a)} (hfg : ∀ {l}, Perm (f l).toList (g l.toList))
    (hg₁ : ∀ {l l'}, DistinctKeys l → Perm l l' → Perm (g l) (g l'))
    (hg₂ : ∀ {l l'}, containsKey a l' = false → g (l ++ l') = g l ++ l') :
    Perm (toListModel (updateBucket m.1.buckets m.2 a f)) (g (toListModel m.1.2))

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : PartialEquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
hm : Raw.WFImp m.val
a : α
f : AssocList α β → AssocList α β
g : List ((a : α) × β a) → List ((a : α) × β a)
hfg : ∀ {l : AssocList α β}, (f l).toList.Perm (g l.toList)
hg₁ : ∀ {l l' : List ((a : α) × β a)}, DistinctKeys l → l.Perm l' → (g l).Perm (g l')
hg₂ : ∀ {l l' : List ((a : α) × β a)}, containsKey a l' = false → g (l ++ l') = g l ++ l'
⊢ (toListModel (updateBucket m.val.buckets ⋯ a f)).Perm (g (toListModel m.val.buckets))

Tactic:
obtain ⟨l, h₁, h₂, h₃⟩ := exists_bucket_of_update m.1.buckets m.2 a f

Result:
case intro.intro.intro
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : PartialEquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
hm : Raw.WFImp m.val
a : α
f : AssocList α β → AssocList α β
g : List ((a : α) × β a) → List ((a : α) × β a)
hfg : ∀ {l : AssocList α β}, (f l).toList.Perm (g l.toList)
hg₁ : ∀ {l l' : List ((a : α) × β a)}, DistinctKeys l → l.Perm l' → (g l).Perm (g l')
hg₂ : ∀ {l l' : List ((a : α) × β a)}, containsKey a l' = false → g (l ++ l') = g l ++ l'
l : List ((a : α) × β a)
h₁ : (toListModel m.val.buckets).Perm ((bucket m.val.buckets ⋯ a).toList ++ l)
h₂ : (toListModel (updateBucket m.val.buckets ⋯ a f)).Perm ((f (bucket m.val.buckets ⋯ a)).toList ++ l)
h₃ : ∀ [inst : LawfulHashable α], IsHashSelf m.val.buckets → ∀ (k' : α), hash a = hash k' → containsKey k' l = false
⊢ (toListModel (updateBucket m.val.buckets ⋯ a f)).Perm (g (toListModel m.val.buckets))

Proof state:
case intro.intro.intro
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : PartialEquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
hm : Raw.WFImp m.val
a : α
f : AssocList α β → AssocList α β
g : List ((a : α) × β a) → List ((a : α) × β a)
hfg : ∀ {l : AssocList α β}, (f l).toList.Perm (g l.toList)
hg₁ : ∀ {l l' : List ((a : α) × β a)}, DistinctKeys l → l.Perm l' → (g l).Perm (g l')
hg₂ : ∀ {l l' : List ((a : α) × β a)}, containsKey a l' = false → g (l ++ l') = g l ++ l'
l : List ((a : α) × β a)
h₁ : (toListModel m.val.buckets).Perm ((bucket m.val.buckets ⋯ a).toList ++ l)
h₂ : (toListModel (updateBucket m.val.buckets ⋯ a f)).Perm ((f (bucket m.val.buckets ⋯ a)).toList ++ l)
h₃ : ∀ [inst : LawfulHashable α], IsHashSelf m.val.buckets → ∀ (k' : α), hash a = hash k' → containsKey k' l = false
⊢ ((f (bucket m.val.buckets ⋯ a)).toList ++ l).Perm (g ((bucket m.val.buckets ⋯ a).toList ++ l))

Tactic:
refine Perm.append_right l hfg |>.trans ?_

Result:
case intro.intro.intro
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : PartialEquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
hm : Raw.WFImp m.val
a : α
f : AssocList α β → AssocList α β
g : List ((a : α) × β a) → List ((a : α) × β a)
hfg : ∀ {l : AssocList α β}, (f l).toList.Perm (g l.toList)
hg₁ : ∀ {l l' : List ((a : α) × β a)}, DistinctKeys l → l.Perm l' → (g l).Perm (g l')
hg₂ : ∀ {l l' : List ((a : α) × β a)}, containsKey a l' = false → g (l ++ l') = g l ++ l'
l : List ((a : α) × β a)
h₁ : (toListModel m.val.buckets).Perm ((bucket m.val.buckets ⋯ a).toList ++ l)
h₂ : (toListModel (updateBucket m.val.buckets ⋯ a f)).Perm ((f (bucket m.val.buckets ⋯ a)).toList ++ l)
h₃ : ∀ [inst : LawfulHashable α], IsHashSelf m.val.buckets → ∀ (k' : α), hash a = hash k' → containsKey k' l = false
⊢ (g (bucket m.val.buckets ⋯ a).toList ++ l).Perm (g ((bucket m.val.buckets ⋯ a).toList ++ l))

Proof state:
case intro.intro.intro
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : PartialEquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
hm : Raw.WFImp m.val
a : α
f : AssocList α β → AssocList α β
g : List ((a : α) × β a) → List ((a : α) × β a)
hfg : ∀ {l : AssocList α β}, (f l).toList.Perm (g l.toList)
hg₁ : ∀ {l l' : List ((a : α) × β a)}, DistinctKeys l → l.Perm l' → (g l).Perm (g l')
hg₂ : ∀ {l l' : List ((a : α) × β a)}, containsKey a l' = false → g (l ++ l') = g l ++ l'
l : List ((a : α) × β a)
h₁ : (toListModel m.val.buckets).Perm ((bucket m.val.buckets ⋯ a).toList ++ l)
h₂ : (toListModel (updateBucket m.val.buckets ⋯ a f)).Perm ((f (bucket m.val.buckets ⋯ a)).toList ++ l)
h₃ : ∀ [inst : LawfulHashable α], IsHashSelf m.val.buckets → ∀ (k' : α), hash a = hash k' → containsKey k' l = false
⊢ (g (bucket m.val.buckets ⋯ a).toList ++ l).Perm (g ((bucket m.val.buckets ⋯ a).toList ++ l))

Tactic:
rw [hg₂]

Result:
case intro.intro.intro
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : PartialEquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
hm : Raw.WFImp m.val
a : α
f : AssocList α β → AssocList α β
g : List ((a : α) × β a) → List ((a : α) × β a)
hfg : ∀ {l : AssocList α β}, (f l).toList.Perm (g l.toList)
hg₁ : ∀ {l l' : List ((a : α) × β a)}, DistinctKeys l → l.Perm l' → (g l).Perm (g l')
hg₂ : ∀ {l l' : List ((a : α) × β a)}, containsKey a l' = false → g (l ++ l') = g l ++ l'
l : List ((a : α) × β a)
h₁ : (toListModel m.val.buckets).Perm ((bucket m.val.buckets ⋯ a).toList ++ l)
h₂ : (toListModel (updateBucket m.val.buckets ⋯ a f)).Perm ((f (bucket m.val.buckets ⋯ a)).toList ++ l)
h₃ : ∀ [inst : LawfulHashable α], IsHashSelf m.val.buckets → ∀ (k' : α), hash a = hash k' → containsKey k' l = false
⊢ containsKey a l = false

Proof state:
case intro.intro.intro
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : PartialEquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
hm : Raw.WFImp m.val
a : α
f : AssocList α β → AssocList α β
g : List ((a : α) × β a) → List ((a : α) × β a)
hfg : ∀ {l : AssocList α β}, (f l).toList.Perm (g l.toList)
hg₁ : ∀ {l l' : List ((a : α) × β a)}, DistinctKeys l → l.Perm l' → (g l).Perm (g l')
hg₂ : ∀ {l l' : List ((a : α) × β a)}, containsKey a l' = false → g (l ++ l') = g l ++ l'
l : List ((a : α) × β a)
h₁ : (toListModel m.val.buckets).Perm ((bucket m.val.buckets ⋯ a).toList ++ l)
h₂ : (toListModel (updateBucket m.val.buckets ⋯ a f)).Perm ((f (bucket m.val.buckets ⋯ a)).toList ++ l)
h₃ : ∀ [inst : LawfulHashable α], IsHashSelf m.val.buckets → ∀ (k' : α), hash a = hash k' → containsKey k' l = false
⊢ containsKey a l = false

Tactic:
exact h₃ hm.buckets_hash_self _ rfl

Result:
no goals