English
If there is an equivalence e between index types and h says lift(#f(i)) = lift(#g(e(i))) for all i, then the lifted cardinalities of the dependent products are equal: lift(#Π i, f i) = lift(#Π i, g i).
Русский
Если между индексными множествами существует эквивелентность e и для всех i выполнено lift(#f(i)) = lift(#g(e(i))), тогда подъёмные кардиналы зависимых произведений совпадают: lift(#Π i, f i) = lift(#Π i, g i).
LaTeX
$$$ \forall {\iota : Type u} {\iota' : Type v} {f : \iota → Type w} {g : \iota' → Type w'} (e : \iota ≃ \iota'),(\forall i, \operatorname{lift}.\#(f i) = \operatorname{lift}.\#(g (e i))) : \operatorname{lift}(\#(\Pi i, f i)) = \operatorname{lift}(\#(\Pi i, g i))$$$
Lean4
theorem mk_pi_congr_lift {ι : Type v} {ι' : Type v'} {f : ι → Type w} {g : ι' → Type w'} (e : ι ≃ ι')
(h : ∀ i, lift.{w'} #(f i) = lift.{w} #(g (e i))) : lift.{max v' w'} #(Π i, f i) = lift.{max v w} #(Π i, g i) :=
Cardinal.lift_mk_eq'.2 ⟨.piCongr e fun i ↦ Classical.choice <| Cardinal.lift_mk_eq'.1 (h i)⟩
