English
A specialized ext lemma: equality of two Σ-elements over a dependent type is determined by equal first coordinates and equal second coordinates.
Русский
Уточнённое лемма-расширение: равенство двух элементов Σ(а, Subtype(p a)) определяется равенством первых координат и равенством вторых.
LaTeX
$$@[ext]\ntheorem subtype_ext {β : Type*} {p : α → β → Prop} : \forall {x0 x1 : Σ a, Subtype (p a)}, x0.fst = x1.fst → (x0.snd : β) = x1.snd → x0 = x1$$
Lean4
/-- A specialized ext lemma for equality of sigma types over an indexed subtype. -/
@[ext]
theorem subtype_ext {β : Type*} {p : α → β → Prop} :
∀ {x₀ x₁ : Σ a, Subtype (p a)}, x₀.fst = x₁.fst → (x₀.snd : β) = x₁.snd → x₀ = x₁
| ⟨_, _, _⟩, ⟨_, _, _⟩, rfl, rfl => rfl
