equivalence of propositions dependent on equal terms

Stream: lean4

[Bhakti Shah]

slightly dumb question because i've run into this before but i also might be missing something super obvious:
if i have P : A -> Prop and I have a proof of a = b where a, b : A, can I get a proof of P a -> P b in some easy way?
i can provide a concrete example if that makes it easier but I was curious more generally about this situation in lean (if there was a way to easily deal with the whole dependent type shenanigans). Thanks!

[Kyle Miller]

Here are some options. The latter ones need to have an expected type available:

example (P : A → Prop) (h : a = b) : P a = P b := congrArg P h

example (P : A → Prop) (h : a = b) : P a → P b := cast (congrArg P h)

example (P : A → Prop) (h : a = b) : P a → P b := (congrArg P h).mp

example (P : A → Prop) (h : a = b) (ha : P a) : P b := h ▸ ha

example (P : A → Prop) (h : a = b) (ha : P a) : P b := Eq.rec ha h

example (P : A → Prop) (h : a = b) : P a → P b := Eq.recOn h

[Bhakti Shah]

that is super helpful thank you :)

[Scott Morrison]

Don't forget subst h.

[Kyle Miller]

Sure, if we want tactic proofs:

example (P : A → Prop) (h : a = b) : P a → P b := by subst h; exact id
example (P : A → Prop) (h : a = b) (ha : P a) : P b := by subst h; exact ha
example (P : A → Prop) (h : a = b) : P a → P b := by cases h; exact id
example (P : A → Prop) (h : a = b) (ha : P a) : P b := by cases h; exact ha
example (P : A → Prop) (h : a = b) (ha : P a) : P b := by subst_vars; exact ha
example (P : A → Prop) (h : a = b) (ha : P a) : P b := by simp_all

[Ruben Van de Velde]

Tactic proofs? In this economy?