out_mk

Mathlib.Data.Erased

URI: https://scilib.ai/kg/mathlib#Erased.out_mk

Lean4

@[simp]
theorem out_mk {α} (a : α) : (mk a).out = a := by
  let h := (mk a).2; change Classical.choose h = a
  have := Classical.choose_spec h
  exact cast (congr_fun this a).symm rfl

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

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

Разделы

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

Аффилиация

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