-- Mathlib/Data/List/Sigma.lean
theorem dlookup_map (l : List (Sigma β))
    {f : α → α'} (hf : Function.Injective f) (g : ∀ a, β a → β' (f a)) (a : α) :
    (l.map fun x => ⟨f x.1, g _ x.2⟩).dlookup (f a) = (l.dlookup a).map (g a)

Proof state:
case cons.inl
α : Type u
α' : Type u'
β : α → Type v
β' : α' → Type v'
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α → α'
hf : Function.Injective f
g : (a : α) → β a → β' (f a)
b : Sigma β
l : List (Sigma β)
IH : dlookup (f b.fst) (map (fun x => ⟨f x.fst, g x.fst x.snd⟩) l) = Option.map (g b.fst) (dlookup b.fst l)
⊢ dlookup (f b.fst) (⟨f b.fst, g b.fst b.snd⟩ :: map (fun x => ⟨f x.fst, g x.fst x.snd⟩) l) =
    Option.map (g b.fst) (dlookup b.fst (b :: l))

Tactic:
rw [dlookup_cons_eq, dlookup_cons_eq, Option.map_some']

Result:
no goals

Proof state:
case nil
α : Type u
α' : Type u'
β : α → Type v
β' : α' → Type v'
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α → α'
hf : Function.Injective f
g : (a : α) → β a → β' (f a)
a : α
⊢ dlookup (f a) (map (fun x => ⟨f x.fst, g x.fst x.snd⟩) []) = Option.map (g a) (dlookup a [])

Tactic:
rw [map_nil, dlookup_nil, dlookup_nil, Option.map_none']

Result:
no goals

Proof state:
case cons
α : Type u
α' : Type u'
β : α → Type v
β' : α' → Type v'
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α → α'
hf : Function.Injective f
g : (a : α) → β a → β' (f a)
a : α
b : Sigma β
l : List (Sigma β)
IH : dlookup (f a) (map (fun x => ⟨f x.fst, g x.fst x.snd⟩) l) = Option.map (g a) (dlookup a l)
⊢ dlookup (f a) (⟨f b.fst, g b.fst b.snd⟩ :: map (fun x => ⟨f x.fst, g x.fst x.snd⟩) l) =
    Option.map (g a) (dlookup a (b :: l))

Tactic:
obtain rfl | h := eq_or_ne a b.1

Result:
case cons.inl
α : Type u
α' : Type u'
β : α → Type v
β' : α' → Type v'
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α → α'
hf : Function.Injective f
g : (a : α) → β a → β' (f a)
b : Sigma β
l : List (Sigma β)
IH : dlookup (f b.fst) (map (fun x => ⟨f x.fst, g x.fst x.snd⟩) l) = Option.map (g b.fst) (dlookup b.fst l)
⊢ dlookup (f b.fst) (⟨f b.fst, g b.fst b.snd⟩ :: map (fun x => ⟨f x.fst, g x.fst x.snd⟩) l) =
    Option.map (g b.fst) (dlookup b.fst (b :: l))

case cons.inr
α : Type u
α' : Type u'
β : α → Type v
β' : α' → Type v'
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α → α'
hf : Function.Injective f
g : (a : α) → β a → β' (f a)
a : α
b : Sigma β
l : List (Sigma β)
IH : dlookup (f a) (map (fun x => ⟨f x.fst, g x.fst x.snd⟩) l) = Option.map (g a) (dlookup a l)
h : a ≠ b.fst
⊢ dlookup (f a) (⟨f b.fst, g b.fst b.snd⟩ :: map (fun x => ⟨f x.fst, g x.fst x.snd⟩) l) =
    Option.map (g a) (dlookup a (b :: l))

Proof state:
α : Type u
α' : Type u'
β : α → Type v
β' : α' → Type v'
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
l : List (Sigma β)
f : α → α'
hf : Function.Injective f
g : (a : α) → β a → β' (f a)
a : α
⊢ dlookup (f a) (map (fun x => ⟨f x.fst, g x.fst x.snd⟩) l) = Option.map (g a) (dlookup a l)

Tactic:
induction' l with b l IH

Result:
case nil
α : Type u
α' : Type u'
β : α → Type v
β' : α' → Type v'
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α → α'
hf : Function.Injective f
g : (a : α) → β a → β' (f a)
a : α
⊢ dlookup (f a) (map (fun x => ⟨f x.fst, g x.fst x.snd⟩) []) = Option.map (g a) (dlookup a [])

case cons
α : Type u
α' : Type u'
β : α → Type v
β' : α' → Type v'
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α → α'
hf : Function.Injective f
g : (a : α) → β a → β' (f a)
a : α
b : Sigma β
l : List (Sigma β)
IH : dlookup (f a) (map (fun x => ⟨f x.fst, g x.fst x.snd⟩) l) = Option.map (g a) (dlookup a l)
⊢ dlookup (f a) (map (fun x => ⟨f x.fst, g x.fst x.snd⟩) (b :: l)) = Option.map (g a) (dlookup a (b :: l))

Proof state:
case cons
α : Type u
α' : Type u'
β : α → Type v
β' : α' → Type v'
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α → α'
hf : Function.Injective f
g : (a : α) → β a → β' (f a)
a : α
b : Sigma β
l : List (Sigma β)
IH : dlookup (f a) (map (fun x => ⟨f x.fst, g x.fst x.snd⟩) l) = Option.map (g a) (dlookup a l)
⊢ dlookup (f a) (map (fun x => ⟨f x.fst, g x.fst x.snd⟩) (b :: l)) = Option.map (g a) (dlookup a (b :: l))

Tactic:
rw [map_cons]

Result:
case cons
α : Type u
α' : Type u'
β : α → Type v
β' : α' → Type v'
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α → α'
hf : Function.Injective f
g : (a : α) → β a → β' (f a)
a : α
b : Sigma β
l : List (Sigma β)
IH : dlookup (f a) (map (fun x => ⟨f x.fst, g x.fst x.snd⟩) l) = Option.map (g a) (dlookup a l)
⊢ dlookup (f a) (⟨f b.fst, g b.fst b.snd⟩ :: map (fun x => ⟨f x.fst, g x.fst x.snd⟩) l) =
    Option.map (g a) (dlookup a (b :: l))

Proof state:
case cons.inr
α : Type u
α' : Type u'
β : α → Type v
β' : α' → Type v'
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α → α'
hf : Function.Injective f
g : (a : α) → β a → β' (f a)
a : α
b : Sigma β
l : List (Sigma β)
IH : dlookup (f a) (map (fun x => ⟨f x.fst, g x.fst x.snd⟩) l) = Option.map (g a) (dlookup a l)
h : a ≠ b.fst
⊢ dlookup (f a) (⟨f b.fst, g b.fst b.snd⟩ :: map (fun x => ⟨f x.fst, g x.fst x.snd⟩) l) =
    Option.map (g a) (dlookup a (b :: l))

Tactic:
rw [dlookup_cons_ne _ _ h, dlookup_cons_ne _ _ (fun he => h <| hf he), IH]

Result:
no goals