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

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

Tactic:
refine Eq.trans ?_ (hg₁ (hm.distinct.perm hl.symm) hl.symm)

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

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

Tactic:
exact hlk hm.buckets_hash_self _ rfl

Result:
no goals

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

Tactic:
obtain ⟨l, hl, hlk⟩ := exists_bucket m.1.buckets m.2 a

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

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

Tactic:
rw [hfg, hg₂]

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