α : Sort u
β✝ : α → Sort v
α' : Sort w
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f✝ g : (a : α) → β✝ a
a✝ : α
b✝ : β✝ a✝
β : Sort u_1
f : α → β
a' : α
b : β
a : α
h2 : ∀ (h : a = a'), (_ : a' = a) ▸ b = b
⊢ update f a' b a = if a = a' then b else f a
α : Sort u
β✝ : α → Sort v
α' : Sort w
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f✝ g : (a : α) → β✝ a
a✝ : α
b✝ : β✝ a✝
β : Sort u_1
f : α → β
a' : α
b : β
a : α
⊢ update f a' b a = if a = a' then b else f a
have h2 : (h : a = a') → Eq.rec (motive := λ _ _ => β) b h.symm = b :=
  by intro h
     rw [eq_rec_constant]
α : Sort u
β✝ : α → Sort v
α' : Sort w
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f✝ g : (a : α) → β✝ a
a✝ : α
b✝ : β✝ a✝
β : Sort u_1
f : α → β
a' : α
b : β
a : α
h2 : ∀ (h : a = a'), (_ : a' = a) ▸ b = b
h3 : (fun h => (_ : a' = a) ▸ b) = fun x => b
⊢ update f a' b a = if a = a' then b else f a
α : Sort u
β✝ : α → Sort v
α' : Sort w
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f✝ g : (a : α) → β✝ a
a✝ : α
b✝ : β✝ a✝
β : Sort u_1
f : α → β
a' : α
b : β
a : α
h2 : ∀ (h : a = a'), (_ : a' = a) ▸ b = b
⊢ update f a' b a = if a = a' then b else f a
have h3 : (λ h : a = a' => Eq.rec (motive := λ _ _ => β) b h.symm) =
          (λ _ : a = a' =>  b) := funext h2
α : Sort u
β✝ : α → Sort v
α' : Sort w
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f✝¹ g : (a : α) → β✝ a
a✝ : α
b✝ : β✝ a✝
β : Sort u_1
f✝ : α → β
a' : α
b : β
a : α
h2 : ∀ (h : a = a'), (_ : a' = a) ▸ b = b
h3 : (fun h => (_ : a' = a) ▸ b) = fun x => b
f : (a = a' → β) → β := fun x => dite (a = a') x fun x => f✝ a
⊢ update f✝ a' b a = if a = a' then b else f✝ a
α : Sort u
β✝ : α → Sort v
α' : Sort w
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f✝ g : (a : α) → β✝ a
a✝ : α
b✝ : β✝ a✝
β : Sort u_1
f : α → β
a' : α
b : β
a : α
h2 : ∀ (h : a = a'), (_ : a' = a) ▸ b = b
h3 : (fun h => (_ : a' = a) ▸ b) = fun x => b
⊢ update f a' b a = if a = a' then b else f a
let f := λ x => dite (a = a') x (λ (_: ¬ a = a') => (f a))
no goals
α : Sort u
β✝ : α → Sort v
α' : Sort w
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f✝¹ g : (a : α) → β✝ a
a✝ : α
b✝ : β✝ a✝
β : Sort u_1
f✝ : α → β
a' : α
b : β
a : α
h2 : ∀ (h : a = a'), (_ : a' = a) ▸ b = b
h3 : (fun h => (_ : a' = a) ▸ b) = fun x => b
f : (a = a' → β) → β := fun x => dite (a = a') x fun x => f✝ a
⊢ update f✝ a' b a = if a = a' then b else f✝ a
exact congrArg f h3
α : Sort u
β✝ : α → Sort v
α' : Sort w
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f✝ g : (a : α) → β✝ a
a✝ : α
b✝ : β✝ a✝
β : Sort u_1
f : α → β
a' : α
b : β
a : α
h : a = a'
⊢ (_ : a' = a) ▸ b = b
α : Sort u
β✝ : α → Sort v
α' : Sort w
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f✝ g : (a : α) → β✝ a
a✝ : α
b✝ : β✝ a✝
β : Sort u_1
f : α → β
a' : α
b : β
a : α
⊢ ∀ (h : a = a'), (_ : a' = a) ▸ b = b
intro h
no goals
α : Sort u
β✝ : α → Sort v
α' : Sort w
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f✝ g : (a : α) → β✝ a
a✝ : α
b✝ : β✝ a✝
β : Sort u_1
f : α → β
a' : α
b : β
a : α
h : a = a'
⊢ (_ : a' = a) ▸ b = b
rw [eq_rec_constant]