-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem isHashSelf_filterMapₘ [BEq α] [Hashable α] [ReflBEq α] [LawfulHashable α] {m : Raw₀ α β}
    {f : (a : α) → β a → Option (δ a)} (h : Raw.WFImp m.1) :
    IsHashSelf (m.filterMapₘ f).1.buckets

Proof state:
α : Type u
β : α → Type v
δ : α → Type w
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : ReflBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
f : (a : α) → β a → Option (δ a)
h : Raw.WFImp m.val
l : AssocList α β
p : (a : α) × δ a
hp : p ∈ (AssocList.filterMap f l).toList
⊢ containsKey p.fst l.toList = true

Tactic:
have hp := AssocList.toList_filterMap.mem_iff.1 hp

Result:
α : Type u
β : α → Type v
δ : α → Type w
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : ReflBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
f : (a : α) → β a → Option (δ a)
h : Raw.WFImp m.val
l : AssocList α β
p : (a : α) × δ a
hp✝ : p ∈ (AssocList.filterMap f l).toList
hp : p ∈ List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l.toList
⊢ containsKey p.fst l.toList = true

Proof state:
α : Type u
β : α → Type v
δ : α → Type w
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : ReflBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
f : (a : α) → β a → Option (δ a)
h : Raw.WFImp m.val
⊢ IsHashSelf (m.filterMapₘ f).val.buckets

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

Result:
α : Type u
β : α → Type v
δ : α → Type w
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : ReflBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
f : (a : α) → β a → Option (δ a)
h : Raw.WFImp m.val
l : AssocList α β
p : (a : α) × δ a
hp : p ∈ (AssocList.filterMap f l).toList
⊢ containsKey p.fst l.toList = true

Proof state:
case intro.intro.intro.intro
α : Type u
β : α → Type v
δ : α → Type w
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : ReflBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
f : (a : α) → β a → Option (δ a)
h : Raw.WFImp m.val
l : AssocList α β
p : (a : α) × β a
hkv : p ∈ l.toList
d : δ p.fst
hp : ⟨p.fst, d⟩ ∈ (AssocList.filterMap f l).toList
⊢ containsKey ⟨p.fst, d⟩.fst l.toList = true

Tactic:
exact containsKey_of_mem hkv

Result:
no goals

Proof state:
α : Type u
β : α → Type v
δ : α → Type w
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : ReflBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
f : (a : α) → β a → Option (δ a)
h : Raw.WFImp m.val
l : AssocList α β
p : (a : α) × δ a
hp✝ : p ∈ (AssocList.filterMap f l).toList
hp : ∃ a, a ∈ l.toList ∧ ∃ a_1, f a.fst a.snd = some a_1 ∧ ⟨a.fst, a_1⟩ = p
⊢ containsKey p.fst l.toList = true

Tactic:
obtain ⟨p, ⟨hkv, ⟨d, ⟨-, rfl⟩⟩⟩⟩ := hp

Result:
case intro.intro.intro.intro
α : Type u
β : α → Type v
δ : α → Type w
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : ReflBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
f : (a : α) → β a → Option (δ a)
h : Raw.WFImp m.val
l : AssocList α β
p : (a : α) × β a
hkv : p ∈ l.toList
d : δ p.fst
hp : ⟨p.fst, d⟩ ∈ (AssocList.filterMap f l).toList
⊢ containsKey ⟨p.fst, d⟩.fst l.toList = true

Proof state:
α : Type u
β : α → Type v
δ : α → Type w
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : ReflBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
f : (a : α) → β a → Option (δ a)
h : Raw.WFImp m.val
l : AssocList α β
p : (a : α) × δ a
hp✝ : p ∈ (AssocList.filterMap f l).toList
hp : p ∈ List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l.toList
⊢ containsKey p.fst l.toList = true

Tactic:
simp only [mem_filterMap, Option.map_eq_some'] at hp

Result:
α : Type u
β : α → Type v
δ : α → Type w
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : ReflBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
f : (a : α) → β a → Option (δ a)
h : Raw.WFImp m.val
l : AssocList α β
p : (a : α) × δ a
hp✝ : p ∈ (AssocList.filterMap f l).toList
hp : ∃ a, a ∈ l.toList ∧ ∃ a_1, f a.fst a.snd = some a_1 ∧ ⟨a.fst, a_1⟩ = p
⊢ containsKey p.fst l.toList = true