feat: missing ext lemmas (leanprover-community#381)

zdb999 · Nov 20, 2023 · e403f68 · e403f68
1 parent 03ab63f
commit e403f68
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 2 deletions.
diff --git a/Std/Tactic/Ext.lean b/Std/Tactic/Ext.lean
@@ -202,7 +202,19 @@ syntax "ext?" (colGt ppSpace rintroPat)* (" : " num)? : tactic
 
 end Std.Tactic.Ext
 
-attribute [ext] funext propext
+attribute [ext] funext propext Subtype.eq
+
+@[ext] theorem Prod.ext : {x y : Prod α β} → x.fst = y.fst → x.snd = y.snd → x = y
+  | ⟨_,_⟩, ⟨_,_⟩, rfl, rfl => rfl
+
+@[ext] theorem PProd.ext : {x y : PProd α β} → x.fst = y.fst → x.snd = y.snd → x = y
+  | ⟨_,_⟩, ⟨_,_⟩, rfl, rfl => rfl
+
+@[ext] theorem Sigma.ext : {x y : Sigma β} → x.fst = y.fst → HEq x.snd y.snd → x = y
+  | ⟨_,_⟩, ⟨_,_⟩, rfl, .rfl => rfl
+
+@[ext] theorem PSigma.ext : {x y : PSigma β} → x.fst = y.fst → HEq x.snd y.snd → x = y
+  | ⟨_,_⟩, ⟨_,_⟩, rfl, .rfl => rfl
 
 @[ext] protected theorem PUnit.ext (x y : PUnit) : x = y := rfl
 protected theorem Unit.ext (x y : Unit) : x = y := rfl
diff --git a/test/ext.lean b/test/ext.lean
@@ -66,7 +66,6 @@ structure MyUnit
 example (x y : MyUnit) : x = y := by ext; rfl
 
 -- Check that we don't generate a warning when `x` only uses a pattern in one branch:
-attribute [ext] Prod
 example (f : ℕ × (ℕ → ℕ)) : f = f := by
   ext x
   · rfl