feat: add isExclusiveUnsafe

src/Init/Ext.lean

@@ -24,16 +24,15 @@ syntax extFlat := atomic("(" &"flat" " := " &"false" ")")
 /--
 Registers an extensionality theorem.
 
-* When `@[ext]` is applied to a theorem, the theorem is registered for the `ext` tactic, and it generates an "`ext_iff`" theorem.
+* When `@[ext]` is applied to a structure, it generates `.ext` and `.ext_iff` theorems and registers
+  them for the `ext` tactic.
+
+* When `@[ext]` is applied to a theorem, the theorem is registered for the `ext` tactic, and it generates an `ext_iff` theorem.
   The name of the theorem is from adding the suffix `_iff` to the theorem name.
 
-* When `@[ext]` is applied to a structure, it generates an `.ext` theorem and applies the `@[ext]` attribute to it.
-  The result is an `.ext` and an `.ext_iff` theorem with the `.ext` theorem registered for the `ext` tactic.
+* An optional natural number argument, e.g. `@[ext 9000]`, specifies a priority for the lemma. Higher-priority lemmas are chosen first, and the default is `1000`.
 
-* An optional natural number argument, e.g. `@[ext 9000]`, specifies a priority for the `ext` lemma.
-  Higher-priority lemmas are chosen first, and the default is `1000`.
-
-* The flag `@[ext (iff := false)]` disables generating an `ext_iff` theorem.
+* The flag `@[ext (iff := false)]` prevents it from generating an `ext_iff` theorem.
 
 * The flag `@[ext (flat := false)]` causes generated structure extensionality theorems to show inherited fields based on their representation,
   rather than flattening the parents' fields into the lemma's equality hypotheses.

src/Lean/Elab/App.lean

@@ -742,10 +742,7 @@ def mkMotive (discrs : Array Expr) (expectedType : Expr): MetaM Expr := do
     let motiveBody ← kabstract motive discr
     /- We use `transform (usedLetOnly := true)` to eliminate unnecessary let-expressions. -/
     let discrType ← transform (usedLetOnly := true) (← instantiateMVars (← inferType discr))
-    let motive := Lean.mkLambda (← mkFreshBinderName) BinderInfo.default discrType motiveBody
-    unless (← isTypeCorrect motive) do
-      throwError "failed to elaborate eliminator, motive is not type correct:{indentD motive}"
-    return motive
+    return Lean.mkLambda (← mkFreshBinderName) BinderInfo.default discrType motiveBody
 
 /-- If the eliminator is over-applied, we "revert" the extra arguments. -/
 def revertArgs (args : List Arg) (f : Expr) (expectedType : Expr) : TermElabM (Expr × Expr) :=

src/Lean/Elab/Tactic/Basic.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
-import Lean.Meta.Tactic.Util
 import Lean.Elab.Term
 
 namespace Lean.Elab
@@ -399,19 +398,12 @@ def ensureHasNoMVars (e : Expr) : TacticM Unit := do
   if e.hasExprMVar then
     throwError "tactic failed, resulting expression contains metavariables{indentExpr e}"
 
-/--
-Closes main goal using the given expression.
-If `checkUnassigned == true`, then `val` must not contain unassigned metavariables.
-Returns `true` if `val` was successfully used to close the goal.
--/
-def closeMainGoal (tacName : Name) (val : Expr) (checkUnassigned := true): TacticM Unit := do
+/-- Close main goal using the given expression. If `checkUnassigned == true`, then `val` must not contain unassigned metavariables. -/
+def closeMainGoal (val : Expr) (checkUnassigned := true): TacticM Unit := do
   if checkUnassigned then
     ensureHasNoMVars val
-  let mvarId ← getMainGoal
-  if (← mvarId.checkedAssign val) then
-    replaceMainGoal []
-  else
-    throwTacticEx tacName mvarId m!"attempting to close the goal using{indentExpr val}\nthis is often due occurs-check failure"
+  (← getMainGoal).assign val
+  replaceMainGoal []
 
 @[inline] def liftMetaMAtMain (x : MVarId → MetaM α) : TacticM α := do
   withMainContext do x (← getMainGoal)

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -56,9 +56,9 @@ def elabTermEnsuringType (stx : Syntax) (expectedType? : Option Expr) (mayPostpo
     return e
 
 /-- Try to close main goal using `x target`, where `target` is the type of the main goal.  -/
-def closeMainGoalUsing (tacName : Name) (x : Expr → TacticM Expr) (checkUnassigned := true) : TacticM Unit :=
+def closeMainGoalUsing (x : Expr → TacticM Expr) (checkUnassigned := true) : TacticM Unit :=
   withMainContext do
-    closeMainGoal (tacName := tacName) (checkUnassigned := checkUnassigned) (← x (← getMainTarget))
+    closeMainGoal (checkUnassigned := checkUnassigned) (← x (← getMainTarget))
 
 def logUnassignedAndAbort (mvarIds : Array MVarId) : TacticM Unit := do
    if (← Term.logUnassignedUsingErrorInfos mvarIds) then
@@ -68,14 +68,13 @@ def filterOldMVars (mvarIds : Array MVarId) (mvarCounterSaved : Nat) : MetaM (Ar
   let mctx ← getMCtx
   return mvarIds.filter fun mvarId => (mctx.getDecl mvarId |>.index) >= mvarCounterSaved
 
-@[builtin_tactic «exact»] def evalExact : Tactic := fun stx => do
+@[builtin_tactic «exact»] def evalExact : Tactic := fun stx =>
   match stx with
-  | `(tactic| exact $e) =>
-    closeMainGoalUsing `exact (checkUnassigned := false) fun type => do
-      let mvarCounterSaved := (← getMCtx).mvarCounter
-      let r ← elabTermEnsuringType e type
-      logUnassignedAndAbort (← filterOldMVars (← getMVars r) mvarCounterSaved)
-      return r
+  | `(tactic| exact $e) => closeMainGoalUsing (checkUnassigned := false) fun type => do
+    let mvarCounterSaved := (← getMCtx).mvarCounter
+    let r ← elabTermEnsuringType e type
+    logUnassignedAndAbort (← filterOldMVars (← getMVars r) mvarCounterSaved)
+    return r
   | _ => throwUnsupportedSyntax
 
 def sortMVarIdArrayByIndex [MonadMCtx m] [Monad m] (mvarIds : Array MVarId) : m (Array MVarId) := do
@@ -394,7 +393,7 @@ private partial def blameDecideReductionFailure (inst : Expr) : MetaM Expr := do
   return inst
 
 @[builtin_tactic Lean.Parser.Tactic.decide] def evalDecide : Tactic := fun _ =>
-  closeMainGoalUsing `decide fun expectedType => do
+  closeMainGoalUsing fun expectedType => do
     let expectedType ← preprocessPropToDecide expectedType
     let d ← mkDecide expectedType
     let d ← instantiateMVars d
@@ -473,7 +472,7 @@ private def mkNativeAuxDecl (baseName : Name) (type value : Expr) : TermElabM Na
   pure auxName
 
 @[builtin_tactic Lean.Parser.Tactic.nativeDecide] def evalNativeDecide : Tactic := fun _ =>
-  closeMainGoalUsing `nativeDecide fun expectedType => do
+  closeMainGoalUsing fun expectedType => do
     let expectedType ← preprocessPropToDecide expectedType
     let d ← mkDecide expectedType
     let auxDeclName ← mkNativeAuxDecl `_nativeDecide (Lean.mkConst `Bool) d

src/Lean/Elab/Tactic/Ext.lean

@@ -74,16 +74,16 @@ def mkExtIffType (extThmName : Name) : MetaM Expr := withLCtx {} {} do
     let some (_, x, y) := ty.eq? | failNotEq
     let some xIdx := args.findIdx? (· == x) | failNotEq
     let some yIdx := args.findIdx? (· == y) | failNotEq
-    unless xIdx + 1 == yIdx do
+    unless xIdx == yIdx + 1 || xIdx + 1 == yIdx do
       throwError "expecting {x} and {y} to be consecutive arguments"
-    let startIdx := yIdx + 1
+    let startIdx := max xIdx yIdx + 1
     let toRevert := args[startIdx:].toArray
     let fvars ← toRevert.foldlM (init := {}) (fun st e => return collectFVars st (← inferType e))
     for fvar in toRevert do
       unless ← Meta.isProof fvar do
-        throwError "argument {fvar} is not a proof, which is not supported for arguments after {x} and {y}"
+        throwError "argument {fvar} is not a proof, which is not supported"
       if fvars.fvarSet.contains fvar.fvarId! then
-        throwError "argument {fvar} is depended upon, which is not supported for arguments after {x} and {y}"
+        throwError "argument {fvar} is depended upon, which is not supported"
     let conj := mkAndN (← toRevert.mapM (inferType ·)).toList
     -- Make everything implicit except for inst implicits
     let mut newBis := #[]
@@ -104,31 +104,27 @@ def realizeExtTheorem (structName : Name) (flat : Bool) : Elab.Command.CommandEl
     throwError "'{structName}' is not a structure"
   let extName := structName.mkStr "ext"
   unless (← getEnv).contains extName do
-    try
-      Elab.Command.liftTermElabM <| withoutErrToSorry <| withDeclName extName do
-        let type ← mkExtType structName flat
-        let pf ← withSynthesize do
-          let indVal ← getConstInfoInduct structName
-          let params := Array.mkArray indVal.numParams (← `(_))
-          Elab.Term.elabTermEnsuringType (expectedType? := type) (implicitLambda := false)
-            -- introduce the params, do cases on 'x' and 'y', and then substitute each equation
-            (← `(by intro $params* {..} {..}; intros; subst_eqs; rfl))
-        let pf ← instantiateMVars pf
-        if pf.hasMVar then throwError "(internal error) synthesized ext proof contains metavariables{indentD pf}"
-        let info ← getConstInfo structName
-        addDecl <| Declaration.thmDecl {
-          name := extName
-          type
-          value := pf
-          levelParams := info.levelParams
-        }
-        modifyEnv fun env => addProtected env extName
-        Lean.addDeclarationRanges extName {
-          range := ← getDeclarationRange (← getRef)
-          selectionRange := ← getDeclarationRange (← getRef) }
-    catch e =>
-      throwError m!"\
-        Failed to generate an 'ext' theorem for '{MessageData.ofConstName structName}': {e.toMessageData}"
+    Elab.Command.liftTermElabM <| withoutErrToSorry <| withDeclName extName do
+      let type ← mkExtType structName flat
+      let pf ← withSynthesize do
+        let indVal ← getConstInfoInduct structName
+        let params := Array.mkArray indVal.numParams (← `(_))
+        Elab.Term.elabTermEnsuringType (expectedType? := type) (implicitLambda := false)
+          -- introduce the params, do cases on 'x' and 'y', and then substitute each equation
+          (← `(by intro $params* {..} {..}; intros; subst_eqs; rfl))
+      let pf ← instantiateMVars pf
+      if pf.hasMVar then throwError "(internal error) synthesized ext proof contains metavariables{indentD pf}"
+      let info ← getConstInfo structName
+      addDecl <| Declaration.thmDecl {
+        name := extName
+        type
+        value := pf
+        levelParams := info.levelParams
+      }
+      modifyEnv fun env => addProtected env extName
+      Lean.addDeclarationRanges extName {
+        range := ← getDeclarationRange (← getRef)
+        selectionRange := ← getDeclarationRange (← getRef) }
   return extName
 
 /--
@@ -142,35 +138,29 @@ def realizeExtIffTheorem (extName : Name) : Elab.Command.CommandElabM Name := do
     | .str n s => .str n (s ++ "_iff")
     | _ => .str extName "ext_iff"
   unless (← getEnv).contains extIffName do
-    try
-      let info ← getConstInfo extName
-      Elab.Command.liftTermElabM <| withoutErrToSorry <| withDeclName extIffName do
-        let type ← mkExtIffType extName
-        let pf ← withSynthesize do
-          Elab.Term.elabTermEnsuringType (expectedType? := type) <| ← `(by
-            intros
-            refine ⟨?_, ?_⟩
-            · intro h; cases h; and_intros <;> (intros; first | rfl | simp | fail "Failed to prove converse of ext theorem")
-            · intro; (repeat cases ‹_ ∧ _›); apply $(mkCIdent extName) <;> assumption)
-        let pf ← instantiateMVars pf
-        if pf.hasMVar then throwError "(internal error) synthesized ext_iff proof contains metavariables{indentD pf}"
-        addDecl <| Declaration.thmDecl {
-          name := extIffName
-          type
-          value := pf
-          levelParams := info.levelParams
-        }
-        -- 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) }
-    catch e =>
-      throwError m!"\
-        Failed to generate an 'ext_iff' theorem from '{MessageData.ofConstName extName}': {e.toMessageData}\n\
-        \n\
-        Try '@[ext (iff := false)]' to prevent generating an 'ext_iff' theorem."
+    let info ← getConstInfo extName
+    Elab.Command.liftTermElabM <| withoutErrToSorry <| withDeclName extIffName do
+      let type ← mkExtIffType extName
+      let pf ← withSynthesize do
+        Elab.Term.elabTermEnsuringType (expectedType? := type) <| ← `(by
+          intros
+          refine ⟨?_, ?_⟩
+          · intro h; cases h; and_intros <;> (intros; first | rfl | simp | fail "Failed to prove converse of ext theorem")
+          · intro; (repeat cases ‹_ ∧ _›); apply $(mkCIdent extName) <;> assumption)
+      let pf ← instantiateMVars pf
+      if pf.hasMVar then throwError "(internal error) synthesized ext_iff proof contains metavariables{indentD pf}"
+      addDecl <| Declaration.thmDecl {
+        name := extIffName
+        type
+        value := pf
+        levelParams := info.levelParams
+      }
+      -- 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
 
 

src/Lean/Meta/Basic.lean

@@ -1865,13 +1865,9 @@ abbrev isDefEqGuarded (t s : Expr) : MetaM Bool :=
 def isDefEqNoConstantApprox (t s : Expr) : MetaM Bool :=
   approxDefEq <| isDefEq t s
 
-/--
-Returns `true` if `mvarId := val` was successfully assigned.
-This method uses the same assignment validation performed by `isDefEq`, but it does not check whether the types match.
--/
--- Remark: this method is implemented at `ExprDefEq`
-@[extern "lean_checked_assign"]
-opaque _root_.Lean.MVarId.checkedAssign (mvarId : MVarId) (val : Expr) : MetaM Bool
+/-- Shorthand for `isDefEq (mkMVar mvarId) val` -/
+def _root_.Lean.MVarId.checkedAssign (mvarId : MVarId) (val : Expr) : MetaM Bool :=
+  isDefEq (mkMVar mvarId) val
 
 /--
   Eta expand the given expression.

src/Lean/Meta/ExprDefEq.lean

@@ -1046,15 +1046,6 @@ def checkAssignment (mvarId : MVarId) (fvars : Array Expr) (v : Expr) : MetaM (O
       return none
     return some v
 
--- Implementation for `_root_.Lean.MVarId.checkedAssign`
-@[export lean_checked_assign]
-def checkedAssignImpl (mvarId : MVarId) (val : Expr) : MetaM Bool := do
-  if let some val ← checkAssignment mvarId #[] val then
-    mvarId.assign val
-    return true
-  else
-    return false
-
 private def processAssignmentFOApproxAux (mvar : Expr) (args : Array Expr) (v : Expr) : MetaM Bool :=
   match v with
   | .mdata _ e   => processAssignmentFOApproxAux mvar args e

src/Lean/Util/PtrSet.lean

@@ -6,7 +6,6 @@ Authors: Leonardo de Moura
 prelude
 import Init.Data.Hashable
 import Lean.Data.HashSet
-import Lean.Data.HashMap
 
 namespace Lean
 
@@ -34,22 +33,4 @@ unsafe abbrev PtrSet.insert (s : PtrSet α) (a : α) : PtrSet α :=
 unsafe abbrev PtrSet.contains (s : PtrSet α) (a : α) : Bool :=
   HashSet.contains s { value := a }
 
-/--
-Map of pointers. It is a low-level auxiliary datastructure used for traversing DAGs.
--/
-unsafe def PtrMap (α : Type) (β : Type) :=
-  HashMap (Ptr α) β
-
-unsafe def mkPtrMap {α β : Type} (capacity : Nat := 64) : PtrMap α β :=
-  mkHashMap capacity
-
-unsafe abbrev PtrMap.insert (s : PtrMap α β) (a : α) (b : β) : PtrMap α β :=
-  HashMap.insert s { value := a } b
-
-unsafe abbrev PtrMap.contains (s : PtrMap α β) (a : α) : Bool :=
-  HashMap.contains s { value := a }
-
-unsafe abbrev PtrMap.find? (s : PtrMap α β) (a : α) : Option β :=
-  HashMap.find? s { value := a }
-
 end Lean

src/Lean/Util/ReplaceExpr.lean

@@ -5,59 +5,74 @@ Authors: Leonardo de Moura, Gabriel Ebner, Sebastian Ullrich
 -/
 prelude
 import Lean.Expr
-import Lean.Util.PtrSet
 
 namespace Lean
 namespace Expr
 
 namespace ReplaceImpl
 
-unsafe abbrev ReplaceM := StateM (PtrMap Expr Expr)
+structure Cache where
+  size : USize
+  -- First `size` elements are the keys.
+  -- Second `size` elements are the results.
+  keysResults : Array NonScalar -- Either Expr or Unit (disjoint memory representation)
 
-unsafe def cache (key : Expr) (exclusive : Bool)  (result : Expr) : ReplaceM Expr := do
-  unless exclusive do
-    modify (·.insert key result)
+unsafe def Cache.new (e : Expr) : Cache :=
+  -- scale size with approximate number of subterms up to 8k
+  -- make sure size is coprime with power of two for collision avoidance
+  let size := (1 <<< min (max e.approxDepth.toUSize 1) 13) - 1
+  { size, keysResults := mkArray (2 * size).toNat (unsafeCast ()) }
+
+@[inline]
+unsafe def Cache.keyIdx (c : Cache) (key : Expr) : USize :=
+  ptrAddrUnsafe key % c.size
+
+@[inline]
+unsafe def Cache.resultIdx (c : Cache) (key : Expr) : USize :=
+  c.keyIdx key + c.size
+
+@[inline]
+unsafe def Cache.hasResultFor (c : Cache) (key : Expr) : Bool :=
+  have : (c.keyIdx key).toNat < c.keysResults.size := lcProof
+  ptrEq (unsafeCast key) c.keysResults[c.keyIdx key]
+
+@[inline]
+unsafe def Cache.getResultFor (c : Cache) (key : Expr) : Expr :=
+  have : (c.resultIdx key).toNat < c.keysResults.size := lcProof
+  unsafeCast c.keysResults[c.resultIdx key]
+
+unsafe def Cache.store (c : Cache) (key result : Expr) : Cache :=
+  { c with keysResults := c.keysResults
+    |>.uset (c.keyIdx key) (unsafeCast key) lcProof
+    |>.uset (c.resultIdx key) (unsafeCast result) lcProof }
+
+abbrev ReplaceM := StateM Cache
+
+@[inline]
+unsafe def cache (key : Expr) (result : Expr) : ReplaceM Expr := do
+  modify (·.store key result)
   pure result
 
 @[specialize]
 unsafe def replaceUnsafeM (f? : Expr → Option Expr) (e : Expr) : ReplaceM Expr := do
   let rec @[specialize] visit (e : Expr) := do
-    /-
-    TODO: We need better control over RC operations to ensure
-    the following (unsafe) optimization is correctly applied.
-    Optimization goal: only cache results for shared objects.
-
-    The main problem is that the current code generator ignores borrow annotations
-    for code written in Lean. These annotations are only taken into account for extern functions.
-
-    Moveover, the borrow inference heuristic currently tags `e` as "owned" since it may be stored
-    in the cache and is used in "update" functions.
-    Thus, when visiting `e` sub-expressions the code generator increases their RC
-    because we are recursively invoking `visit` :(
-
-    Thus, to fix this issue, we must
-    1- Take borrow annotations into account for code written in Lean.
-    2- Mark `e` is borrowed (i.e., `(e : @& Expr)`)
-    -/
-    let excl := isExclusiveUnsafe e
-    unless excl do
-      if let some result := (← get).find? e then
-        return result
-    match f? e with
-      | some eNew => cache e excl eNew
+    if (← get).hasResultFor e then
+      return (← get).getResultFor e
+    else match f? e with
+      | some eNew => cache e eNew
       | none      => match e with
-        | .forallE _ d b _   => cache e excl <| e.updateForallE! (← visit d) (← visit b)
-        | .lam _ d b _       => cache e excl <| e.updateLambdaE! (← visit d) (← visit b)
-        | .mdata _ b         => cache e excl <| e.updateMData! (← visit b)
-        | .letE _ t v b _    => cache e excl <| e.updateLet! (← visit t) (← visit v) (← visit b)
-        | .app f a           => cache e excl <| e.updateApp! (← visit f) (← visit a)
-        | .proj _ _ b        => cache e excl <| e.updateProj! (← visit b)
-        | e                  => return e
+        | Expr.forallE _ d b _   => cache e <| e.updateForallE! (← visit d) (← visit b)
+        | Expr.lam _ d b _       => cache e <| e.updateLambdaE! (← visit d) (← visit b)
+        | Expr.mdata _ b         => cache e <| e.updateMData! (← visit b)
+        | Expr.letE _ t v b _    => cache e <| e.updateLet! (← visit t) (← visit v) (← visit b)
+        | Expr.app f a           => cache e <| e.updateApp! (← visit f) (← visit a)
+        | Expr.proj _ _ b        => cache e <| e.updateProj! (← visit b)
+        | e                      => pure e
   visit e
 
 @[inline]
 unsafe def replaceUnsafe (f? : Expr → Option Expr) (e : Expr) : Expr :=
-  (replaceUnsafeM f? e).run' mkPtrMap
+  (replaceUnsafeM f? e).run' (Cache.new e)
 
 end ReplaceImpl
 

tests/lean/elabAsElim.lean

@@ -87,12 +87,3 @@ noncomputable def f : Nat → Nat :=
 
 example : ∀ x, x ≥ 0 :=
   Nat.rec (Nat.le_refl 0) (fun _ ih => Nat.le_succ_of_le ih)
-
-@[elab_as_elim]
-def Foo.induction {P : (α : Type) → Prop} (α : Type) : P α := sorry
-
-example {n : Type} {T : n} : T = T := Foo.induction n -- motive is not type correct
-
-example {n : Type} : {T : n} → T = T := Foo.induction n -- motive is not type correct
-
-example {n : Type} : {T : n} → T = T := @(Foo.induction n)

tests/lean/elabAsElim.lean.expected.out

@@ -1,8 +1,3 @@
 elabAsElim.lean:9:2-9:14: error: failed to elaborate eliminator, insufficient number of arguments, expected type:
   Nat
 elabAsElim.lean:26:2-26:24: error: failed to elaborate eliminator, unused named arguments: [a]
-elabAsElim.lean:92:4-92:17: warning: declaration uses 'sorry'
-elabAsElim.lean:94:38-94:53: error: failed to elaborate eliminator, motive is not type correct:
-  fun x => T = T
-elabAsElim.lean:96:40-96:55: error: failed to elaborate eliminator, motive is not type correct:
-  fun x => T✝ = T✝

tests/lean/run/2243.lean

@@ -2,7 +2,7 @@ import Lean
 
 open Lean Elab Tactic in
 elab "exact_false" : tactic =>
-  closeMainGoal `exact_false (mkConst ``Bool.false)
+  closeMainGoal (mkConst ``Bool.false)
 
 def f (b : Bool := by exact_false) : Nat := bif b then 1 else 0
 

tests/lean/run/4773.lean

@@ -1,11 +0,0 @@
-/--
-error: tactic 'exact' failed, attempting to close the goal using
-  ?loop
-this is often due occurs-check failure
-case loop
-⊢ False
--/
-#guard_msgs in
-example : False := by
-  refine ?loop
-  exact ?loop

tests/lean/run/ext.lean

@@ -138,35 +138,3 @@ attribute [local ext] Subsingleton.elim
 /-- info: Subsingleton.elim_iff.{u} {α : Sort u} [h : Subsingleton α] {a b : α} : a = b ↔ True -/
 #guard_msgs in #check Subsingleton.elim_iff
 end
-
-
-/-!
-More informative error (issue #4758)
--/
-
-/--
-warning: declaration uses 'sorry'
----
-error: Failed to generate an 'ext_iff' theorem from 'weird_prod_ext': argument f is not a proof, which is not supported for arguments after p and q
-
-Try '@[ext (iff := false)]' to prevent generating an 'ext_iff' theorem.
--/
-#guard_msgs in
-@[ext]
-theorem weird_prod_ext (p q : α × β)
-    (f : α → α') (g : β → β') -- (hf : Function.Injective f) (hg : Function.Injective g)
-    (h : f p.1 = f q.1) (h' : g p.2 = g q.2) :
-  p = q := sorry
-
-/--
-error: Failed to generate an 'ext_iff' theorem from 'ext'': argument h1 is depended upon, which is not supported for arguments after p and q
-
-Try '@[ext (iff := false)]' to prevent generating an 'ext_iff' theorem.
--/
-#guard_msgs in
-@[ext]
-theorem Sigma.ext' {β : α → Type _} (p q : (i : α) × β i)
-    (h1 : p.1 = q.1)
-    (h2 : h1 ▸ p.2 = q.2) :
-    p = q := by
-  cases p; cases q; cases h1; cases h2; rfl