chore: make use of ext_iff realization now that stage0 is updated (#4694)

This is a followup to #4543. This also adds "go to definition" for
generated lemmas.

src/Init/Data/Char/Lemmas.lean

@@ -31,14 +31,9 @@ theorem utf8Size_eq (c : Char) : c.utf8Size = 1 ∨ c.utf8Size = 2 ∨ c.utf8Siz
   rw [Char.ofNat, dif_pos]
   rfl
 
--- TODO(kmill): remove ext_iff and apply [ext] to ext directly
-protected theorem ext : {a b : Char} → a.val = b.val → a = b
+@[ext] protected theorem ext : {a b : Char} → a.val = b.val → a = b
   | ⟨_,_⟩, ⟨_,_⟩, rfl => rfl
 
-protected theorem ext_iff {x y : Char} : x = y ↔ x.val = y.val := ⟨congrArg _, Char.ext⟩
-
-attribute [ext] Char.ext
-
 end Char
 
 @[deprecated Char.utf8Size (since := "2024-06-04")] abbrev String.csize := Char.utf8Size

src/Init/Data/Fin/Lemmas.lean

@@ -37,12 +37,7 @@ theorem pos_iff_nonempty {n : Nat} : 0 < n ↔ Nonempty (Fin n) :=
 
 @[simp] protected theorem eta (a : Fin n) (h : a < n) : (⟨a, h⟩ : Fin n) = a := rfl
 
--- TODO(kmill): remove ext_iff and apply [ext] to ext directly
-protected theorem ext {a b : Fin n} (h : (a : Nat) = b) : a = b := eq_of_val_eq h
-
-protected theorem ext_iff {a b : Fin n} : a = b ↔ a.1 = b.1 := val_inj.symm
-
-attribute [ext] Fin.ext
+@[ext] protected theorem ext {a b : Fin n} (h : (a : Nat) = b) : a = b := eq_of_val_eq h
 
 theorem val_ne_iff {a b : Fin n} : a.1 ≠ b.1 ↔ a ≠ b := not_congr val_inj
 

src/Init/Ext.lean

@@ -76,19 +76,8 @@ macro "ext1" xs:(colGt ppSpace rintroPat)* : tactic =>
 end Elab.Tactic.Ext
 end Lean
 
+attribute [ext] Prod PProd Sigma PSigma
 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

src/Lean/Elab/Tactic/Ext.lean

@@ -5,6 +5,7 @@ Authors: Gabriel Ebner, Mario Carneiro
 -/
 prelude
 import Init.Ext
+import Lean.Elab.DeclarationRange
 import Lean.Elab.Tactic.RCases
 import Lean.Elab.Tactic.Repeat
 import Lean.Elab.Tactic.BuiltinTactic
@@ -116,6 +117,9 @@ def realizeExtTheorem (structName : Name) (flat : Bool) : Elab.Command.CommandEl
         levelParams := info.levelParams
       }
       modifyEnv fun env => addProtected env extName
+      Lean.addDeclarationRanges extName {
+        range := ← getDeclarationRange (← getRef)
+        selectionRange := ← getDeclarationRange (← getRef) }
   return extName
 
 /--
@@ -149,6 +153,9 @@ def realizeExtIffTheorem (extName : Name) : Elab.Command.CommandElabM Name := do
       -- Only declarations in a namespace can be protected:
       unless extIffName.isAtomic do
         modifyEnv fun env => addProtected env extIffName
+      Lean.addDeclarationRanges extIffName {
+        range := ← getDeclarationRange (← getRef)
+        selectionRange := ← getDeclarationRange (← getRef) }
   return extIffName
 
 
@@ -229,7 +236,7 @@ builtin_initialize registerBuiltinAttribute {
     let flat := flatFalse?.isNone
     let mut declName := declName
     if isStructure (← getEnv) declName then
-      declName ← liftCommandElabM <| realizeExtTheorem declName flat
+      declName ← liftCommandElabM <| withRef stx <| realizeExtTheorem declName flat
     else if let some stx := flatFalse? then
       throwErrorAt stx "unexpected 'flat' configuration on @[ext] theorem"
     -- Validate and add theorem to environment extension
@@ -245,7 +252,7 @@ builtin_initialize registerBuiltinAttribute {
     extExtension.add {declName, keys, priority} kind
     -- Realize iff theorem
     if iff then
-      discard <| liftCommandElabM <| realizeExtIffTheorem declName
+      discard <| liftCommandElabM <| withRef stx <| realizeExtIffTheorem declName
   erase := fun declName => do
     let s := extExtension.getState (← getEnv)
     let s ← s.erase declName