Map make filter Map flatten find?

theorem map_make_filterMap_flatten_find?  [BEq α] [BEq β] [LawfulBEq α] [LawfulBEq β]  [DecidableEq γ] [LT γ] [DecidableLT γ] [StrictLT γ]  {m : Map α β}  {k : α} {v : β} {k' : γ} {v' : κ}  {f : α × β → Option (List (γ × κ))}  (hfind : m.find? k = .some v)  (hkv : ∃ l, f (k, v) = .some l ∧ l.find? (λ x => x.1 == k') = .some (k', v'))  (hf : ∀ kv, (∃ l, f kv = .some l ∧ (l.find? (λ x => x.1 == k')).isSome) → kv.1 = k) :  (Map.make (m.toList.filterMap f).flatten).find? k' = .some v':= by  rw [← Map.list_find?_iff_make_find?]  simp only [List.find?_flatten]  cases m with | mk l =>  simp only [List.find?_isSome, beq_iff_eq, Prod.exists, exists_and_right, exists_eq_right,    forall_exists_index, and_imp, Prod.forall, Map.find?, Map.toList_mk_id] at *  split at hfind  rotate_left; contradiction  rename_i heq  simp only [Option.some.injEq] at hfind  simp only [hfind] at heq  have := List.find?_some heq  simp only [beq_iff_eq] at this  simp only [this] at heq  induction l with  | nil => contradiction  | cons hd tl ih =>    simp only [List.find?] at heq    split at heq    · simp only [Option.some.injEq] at heq      have ⟨fkv, hfkv, hfind_fkv⟩ := hkv      simp only [List.filterMap, heq, hfkv]      simp only [List.findSome?, hfind_fkv]    · rename_i hne_hd_key      simp only [List.filterMap]      split      · exact ih heq      · rename_i l' hhd        simp only [beq_eq_false_iff_ne, ne_eq] at hne_hd_key        have := hf hd.fst hd.snd        have :          (∃ l, f hd = some l ∧ (List.find? (fun x => x.fst == k') l).isSome = true) → False        := by          intros h          replace ⟨l, h, h'⟩ := h          apply hne_hd_key          apply this l h          simp_all only [forall_const, Option.some.injEq, imp_false, forall_eq', List.find?_isSome,            beq_iff_eq, Prod.exists, exists_and_right, exists_eq_right, exists_false]          rw [List.find?_isSome] at h'          simp_all        simp only [          imp_false, not_exists, not_and,        ] at this        have hfind_l' := this l' hhd        simp only [List.findSome?]        split        · rename_i heq          simp only [heq] at hfind_l'          simp at hfind_l'        · exact ih heq