feat(data/sigma/basic): add a more convenient ext lemma for equality …

…of sigma types over subtypes (#6257)

src/data/sigma/basic.lean

@@ -39,6 +39,16 @@ by { cases x₀, cases x₁, cases h₀, cases h₁, refl }
 lemma ext_iff {x₀ x₁ : sigma β} : x₀ = x₁ ↔ x₀.1 = x₁.1 ∧ x₀.2 == x₁.2 :=
 by { cases x₀, cases x₁, exact sigma.mk.inj_iff }
 
+/-- A specialized ext lemma for equality of sigma types over an indexed subtype. -/
+@[ext]
+lemma subtype_ext {β : Type*} {p : α → β → Prop} :
+  ∀ {x₀ x₁ : Σ a, subtype (p a)}, x₀.fst = x₁.fst → (x₀.snd : β) = x₁.snd → x₀ = x₁
+| ⟨a₀, b₀, hb₀⟩ ⟨a₁, b₁, hb₁⟩ rfl rfl := rfl
+
+lemma subtype_ext_iff {β : Type*} {p : α → β → Prop} {x₀ x₁ : Σ a, subtype (p a)} :
+  x₀ = x₁ ↔ x₀.fst = x₁.fst ∧ (x₀.snd : β) = x₁.snd :=
+⟨λ h, h ▸ ⟨rfl, rfl⟩, λ ⟨h₁, h₂⟩, subtype_ext h₁ h₂⟩
+
 @[simp] theorem «forall» {p : (Σ a, β a) → Prop} :
   (∀ x, p x) ↔ (∀ a b, p ⟨a, b⟩) :=
 ⟨assume h a b, h ⟨a, b⟩, assume h ⟨a, b⟩, h a b⟩
@@ -139,6 +149,16 @@ by { cases x₀, cases x₁, cases h₀, cases h₁, refl }
 lemma ext_iff {x₀ x₁ : psigma β} : x₀ = x₁ ↔ x₀.1 = x₁.1 ∧ x₀.2 == x₁.2 :=
 by { cases x₀, cases x₁, exact psigma.mk.inj_iff }
 
+/-- A specialized ext lemma for equality of psigma types over an indexed subtype. -/
+@[ext]
+lemma subtype_ext {β : Sort*} {p : α → β → Prop} :
+  ∀ {x₀ x₁ : Σ' a, subtype (p a)}, x₀.fst = x₁.fst → (x₀.snd : β) = x₁.snd → x₀ = x₁
+| ⟨a₀, b₀, hb₀⟩ ⟨a₁, b₁, hb₁⟩ rfl rfl := rfl
+
+lemma subtype_ext_iff {β : Sort*} {p : α → β → Prop} {x₀ x₁ : Σ' a, subtype (p a)} :
+  x₀ = x₁ ↔ x₀.fst = x₁.fst ∧ (x₀.snd : β) = x₁.snd :=
+⟨λ h, h ▸ ⟨rfl, rfl⟩, λ ⟨h₁, h₂⟩, subtype_ext h₁ h₂⟩
+
 variables {α₁ : Sort*} {α₂ : Sort*} {β₁ : α₁ → Sort*} {β₂ : α₂ → Sort*}
 
 /-- Map the left and right components of a sigma -/