Find? pair map

public theorem find?_pair_map {α β γ} [BEq α] (f : β → γ) (xs : List (α × β)) (k : α)  :  Option.map (λ x => (x.fst, f x.snd)) (List.find? (λ x => x.fst == k) xs)  =  List.find? (λ x => x.fst == k) (List.map (λ x => (x.fst, f x.snd)) xs):= by  induction xs  case nil => simp only [find?_nil, Option.map_none, map_nil]  case cons hd tl ih =>    cases h₁ : hd.fst == k <;> simp only [map_cons]    case false =>      rw [Bool.eq_false_iff, ne_eq] at h₁      have h₂ := @List.find?_cons_of_neg _        (λ (x : α × β) => x.fst == k) hd tl h₁      have h₃ := @List.find?_cons_of_neg _        (λ (x : α × γ) => x.fst == k) (hd.fst, f hd.snd)        (map (λ x => (x.fst, f x.snd)) tl)      simp only [h₁, not_false_eq_true, forall_const, reduceCtorEq] at h₃      simp only [h₂, h₃]      exact ih    case true =>      have h₂ := @List.find?_cons_of_pos _        (λ (x : α × β) => x.fst == k) hd tl h₁      have h₃ := @List.find?_cons_of_pos _        (λ (x : α × γ) => x.fst == k) (hd.fst, f hd.snd)        (map (λ x => (x.fst, f x.snd)) tl)      simp only [h₁, forall_const] at h₃      simp [h₂, h₃]