instCanLift

Mathlib.Tactic.Lift

URI: https://scilib.ai/kg/mathlib#Prod.instCanLift

Lean4

/-- Enable automatic handling of product types in `CanLift`. -/
instance instCanLift {α β γ δ : Type*} {coeβα condβα coeδγ condδγ} [CanLift α β coeβα condβα]
    [CanLift γ δ coeδγ condδγ] : CanLift (α × γ) (β × δ) (Prod.map coeβα coeδγ) (fun x ↦ condβα x.1 ∧ condδγ x.2) where
  prf := by
    rintro ⟨x, y⟩ ⟨hx, hy⟩
    rcases CanLift.prf (β := β) x hx with ⟨x, rfl⟩
    rcases CanLift.prf (β := δ) y hy with ⟨y, rfl⟩
    exact ⟨(x, y), by simp⟩

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

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

Разделы

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

Аффилиация

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