mkProdEquiv

Mathlib.Tactic.ProdAssoc

URI: https://scilib.ai/kg/mathlib#Lean.Expr.mkProdEquiv

Lean4

/-- Construct the equivalence between iterated products of the same type, associated
in possibly different ways. -/
def mkProdEquiv (a b : Expr) : MetaM Expr := do
  let some u := (← whnfD <| ← inferType a).type? |
    throwError "Not a type{indentExpr a}"
  let some v := (← whnfD <| ← inferType b).type? |
    throwError "Not a type{indentExpr b}"
  return
    mkAppN (.const ``Equiv.mk [.succ u, .succ v])
      #[a, b, ← mkProdFun a b, ← mkProdFun b a, .app (.const ``rfl [.succ u]) a, .app (.const ``rfl [.succ v]) b]

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru