English
Two Pi-cons expressions with a dependent map φ are equal if they agree on corresponding arguments via f, preserving the Pi-structure.
Русский
Два выражения Pi.cons, оформленных через отображение φ, равны при согласовании по соответствующим аргументам через f, сохраняющее структуру Pi.
LaTeX
$$$(\\text{Pi.cons } m a (\\phi b) (\\text{...})) = (\\text{fun } a'\\; ha' \\mapsto φ (f a' ha'))$$$
Lean4
theorem cons_map (b : δ a) (f : ∀ a' ∈ m, δ a') {δ' : α → Sort*} (φ : ∀ ⦃a'⦄, δ a' → δ' a') :
Pi.cons _ _ (φ b) (fun a' ha' ↦ φ (f a' ha')) = (fun a' ha' ↦ φ ((cons _ _ b f) a' ha')) :=
by
ext a' ha'
refine (congrArg₂ _ ?_ rfl).trans (apply_dite (@φ _) (a' = a) _ _).symm
ext rfl
rfl
