case h.h
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m : Multiset α
a : α
f : (a' : α) → a' ∈ a ::ₘ m → δ a'
a' : α
h' : a' ∈ a ::ₘ m
⊢ Pi.cons m a (f a (_ : a ∈ a ::ₘ m)) (fun a' ha' => f a' (_ : a' ∈ a ::ₘ m)) a' h' = f a' h'
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m : Multiset α
a : α
f : (a' : α) → a' ∈ a ::ₘ m → δ a'
⊢ (Pi.cons m a (f a (_ : a ∈ a ::ₘ m)) fun a' ha' => f a' (_ : a' ∈ a ::ₘ m)) = f
ext (a' h')
case pos
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m : Multiset α
a : α
f : (a' : α) → a' ∈ a ::ₘ m → δ a'
a' : α
h' : a' ∈ a ::ₘ m
h : a' = a
⊢ Pi.cons m a (f a (_ : a ∈ a ::ₘ m)) (fun a' ha' => f a' (_ : a' ∈ a ::ₘ m)) a' h' = f a' h'

case neg
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m : Multiset α
a : α
f : (a' : α) → a' ∈ a ::ₘ m → δ a'
a' : α
h' : a' ∈ a ::ₘ m
h : ¬a' = a
⊢ Pi.cons m a (f a (_ : a ∈ a ::ₘ m)) (fun a' ha' => f a' (_ : a' ∈ a ::ₘ m)) a' h' = f a' h'
case h.h
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m : Multiset α
a : α
f : (a' : α) → a' ∈ a ::ₘ m → δ a'
a' : α
h' : a' ∈ a ::ₘ m
⊢ Pi.cons m a (f a (_ : a ∈ a ::ₘ m)) (fun a' ha' => f a' (_ : a' ∈ a ::ₘ m)) a' h' = f a' h'
by_cases h : a' = a
case pos
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m : Multiset α
a' : α
f : (a'_1 : α) → a'_1 ∈ a' ::ₘ m → δ a'_1
h' : a' ∈ a' ::ₘ m
⊢ Pi.cons m a' (f a' (_ : a' ∈ a' ::ₘ m)) (fun a'_1 ha' => f a'_1 (_ : a'_1 ∈ a' ::ₘ m)) a' h' = f a' h'
case pos
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m : Multiset α
a : α
f : (a' : α) → a' ∈ a ::ₘ m → δ a'
a' : α
h' : a' ∈ a ::ₘ m
h : a' = a
⊢ Pi.cons m a (f a (_ : a ∈ a ::ₘ m)) (fun a' ha' => f a' (_ : a' ∈ a ::ₘ m)) a' h' = f a' h'
subst h
no goals
case pos
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m : Multiset α
a' : α
f : (a'_1 : α) → a'_1 ∈ a' ::ₘ m → δ a'_1
h' : a' ∈ a' ::ₘ m
⊢ Pi.cons m a' (f a' (_ : a' ∈ a' ::ₘ m)) (fun a'_1 ha' => f a'_1 (_ : a'_1 ∈ a' ::ₘ m)) a' h' = f a' h'
rw [Pi.cons_same]
no goals
case neg
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m : Multiset α
a : α
f : (a' : α) → a' ∈ a ::ₘ m → δ a'
a' : α
h' : a' ∈ a ::ₘ m
h : ¬a' = a
⊢ Pi.cons m a (f a (_ : a ∈ a ::ₘ m)) (fun a' ha' => f a' (_ : a' ∈ a ::ₘ m)) a' h' = f a' h'
rw [Pi.cons_ne _ h]