English
Swapping the positions of two distinct elements in a Pi-construction yields a semantically equivalent Pi-construction up to heterogeneous equality.
Русский
Поменяв местами два различных элемента в конструкторе Pi, получаем эквивалентную конструкцию Pi до гетерогенной эквивалентности.
LaTeX
$$$\\forall \\text{α, β, δ, m, a, a', b, b'},\\; \\mathrm{cons\\_swap} = \\mathrm{Pi.cons}(...).$$$
Lean4
theorem cons_swap {a a' : α} {b : δ a} {b' : δ a'} {m : Multiset α} {f : ∀ a ∈ m, δ a} (h : a ≠ a') :
Pi.cons (a' ::ₘ m) a b (Pi.cons m a' b' f) ≍ Pi.cons (a ::ₘ m) a' b' (Pi.cons m a b f) :=
by
apply hfunext rfl
simp only [heq_iff_eq]
rintro a'' _ rfl
refine hfunext (by rw [Multiset.cons_swap]) fun ha₁ ha₂ _ => ?_
rcases Decidable.ne_or_eq a'' a with (h₁ | rfl)
on_goal 1 => rcases Decidable.eq_or_ne a'' a' with (rfl | h₂)
all_goals simp [*, Pi.cons_same, Pi.cons_ne]
