DeZero.congr_arg

Énoncé

∀ {α : Sort u} {β : Sort v} {a : α} {b : α} (f : α → β) (h : a = b), f a = f b

Applique la même fonction aux deux membres d’une égalité.

Axiomes consommés

Aucun. Cet énoncé se démontre à partir des seules règles du noyau — il ne coûte rien à qui accepte Lean.

Code

/-- Congruence sur l'argument. Le motif `f` est ce que le clic de l'utilisateur
déterminera au jalon 4, ce qui évite entièrement le filtrage d'ordre supérieur. -/
theorem congr_arg {α : Sort u} {β : Sort v} {a b : α} (f : α → β) (h : a = b) : f a = f b :=
  Eq.rec (motive := fun x _ => f a = f x) rfl h