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

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 : (a : α) → (l : AssocList α β) → AssocList.contains a l = true → γ a
g : (a : α) → (l : List ((a : α) × β a)) → containsKey a l = true → γ a
hfg : ∀ {a : α} {l : AssocList α β} {h : AssocList.contains a l = true}, f a l h = g a l.toList ⋯
hg₁ :
  ∀ {l l' : List ((a : α) × β a)} {a : α} {h : containsKey a l = true},
    DistinctKeys l → ∀ (hl' : l.Perm l'), g a l h = g a l' ⋯
h : AssocList.contains a (bucket m.val.buckets ⋯ a) = true
h' : containsKey a (toListModel m.val.buckets) = true
hg₂ :
  ∀ {l l' : List ((a : α) × β a)} {a : α} {h : containsKey a (l ++ l') = true} (hl' : containsKey a l' = false),
    g a (l ++ l') h = g a l ⋯
⊢ f a (bucket m.val.buckets ⋯ a) h = g a (toListModel m.val.buckets) h'

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 : (a : α) → (l : AssocList α β) → AssocList.contains a l = true → γ a
g : (a : α) → (l : List ((a : α) × β a)) → containsKey a l = true → γ a
hfg : ∀ {a : α} {l : AssocList α β} {h : AssocList.contains a l = true}, f a l h = g a l.toList ⋯
hg₁ :
  ∀ {l l' : List ((a : α) × β a)} {a : α} {h : containsKey a l = true},
    DistinctKeys l → ∀ (hl' : l.Perm l'), g a l h = g a l' ⋯
h : AssocList.contains a (bucket m.val.buckets ⋯ a) = true
h' : containsKey a (toListModel m.val.buckets) = true
hg₂ :
  ∀ {l l' : List ((a : α) × β a)} {a : α} {h : containsKey a (l ++ l') = true} (hl' : containsKey a l' = false),
    g a (l ++ l') h = g a 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 a (bucket m.val.buckets ⋯ a) h = g a (toListModel m.val.buckets) h'

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 : (a : α) → (l : AssocList α β) → AssocList.contains a l = true → γ a
g : (a : α) → (l : List ((a : α) × β a)) → containsKey a l = true → γ a
hfg : ∀ {a : α} {l : AssocList α β} {h : AssocList.contains a l = true}, f a l h = g a l.toList ⋯
hg₁ :
  ∀ {l l' : List ((a : α) × β a)} {a : α} {h : containsKey a l = true},
    DistinctKeys l → ∀ (hl' : l.Perm l'), g a l h = g a l' ⋯
h : AssocList.contains a (bucket m.val.buckets ⋯ a) = true
h' : containsKey a (toListModel m.val.buckets) = true
hg₂ :
  ∀ {l l' : List ((a : α) × β a)} {a : α} {h : containsKey a (l ++ l') = true} (hl' : containsKey a l' = false),
    g a (l ++ l') h = g a 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 a (bucket m.val.buckets ⋯ a) h = g a ((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 : (a : α) → (l : AssocList α β) → AssocList.contains a l = true → γ a
g : (a : α) → (l : List ((a : α) × β a)) → containsKey a l = true → γ a
hfg : ∀ {a : α} {l : AssocList α β} {h : AssocList.contains a l = true}, f a l h = g a l.toList ⋯
hg₁ :
  ∀ {l l' : List ((a : α) × β a)} {a : α} {h : containsKey a l = true},
    DistinctKeys l → ∀ (hl' : l.Perm l'), g a l h = g a l' ⋯
h : AssocList.contains a (bucket m.val.buckets ⋯ a) = true
h' : containsKey a (toListModel m.val.buckets) = true
hg₂ :
  ∀ {l l' : List ((a : α) × β a)} {a : α} {h : containsKey a (l ++ l') = true} (hl' : containsKey a l' = false),
    g a (l ++ l') h = g a 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

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 : (a : α) → (l : AssocList α β) → AssocList.contains a l = true → γ a
g : (a : α) → (l : List ((a : α) × β a)) → containsKey a l = true → γ a
hfg : ∀ {a : α} {l : AssocList α β} {h : AssocList.contains a l = true}, f a l h = g a l.toList ⋯
hg₁ :
  ∀ {l l' : List ((a : α) × β a)} {a : α} {h : containsKey a l = true},
    DistinctKeys l → ∀ (hl' : l.Perm l'), g a l h = g a l' ⋯
h : AssocList.contains a (bucket m.val.buckets ⋯ a) = true
h' : containsKey a (toListModel m.val.buckets) = true
hg₂ :
  ∀ {l l' : List ((a : α) × β a)} {a : α} {h : containsKey a (l ++ l') = true} (hl' : containsKey a l' = false),
    g a (l ++ l') h = g a 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