chore: add [ext] basic theorems, add test

and_intros and subst_eqs are not builtin

clarify failure modes

Clarify docString of extCore

clarify

chore: builtin `subst_eqs` tactic

chore: builtin `ext`

src/Init.lean

@@ -31,3 +31,4 @@ import Init.Guard
 import Init.Simproc
 import Init.SizeOfLemmas
 import Init.BinderPredicates
+import Init.Ext

src/Init/Ext.lean

@@ -0,0 +1,113 @@
+/-
+Copyright (c) 2021 Gabriel Ebner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gabriel Ebner, Mario Carneiro
+-/
+prelude
+import Init.TacticsExtra
+import Init.RCases
+
+namespace Lean
+namespace Parser.Attr
+/-- Registers an extensionality 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.
+
+* 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`.
+
+* 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.
+  structures in the generated extensionality theorems. -/
+syntax (name := ext) "ext" (" (" &"flat" " := " term ")")? (ppSpace prio)? : attr
+end Parser.Attr
+
+-- TODO: rename this namespace?
+-- Remark: `ext` has scoped syntax, Mathlib may depend on the actual namespace name.
+namespace Elab.Tactic.Ext
+/--
+Creates the type of the extensionality theorem for the given structure,
+elaborating to `x.1 = y.1 → x.2 = y.2 → x = y`, for example.
+-/
+scoped syntax (name := extType) "ext_type% " term:max ppSpace ident : term
+
+/--
+Creates the type of the iff-variant of the extensionality theorem for the given structure,
+elaborating to `x = y ↔ x.1 = y.1 ∧ x.2 = y.2`, for example.
+-/
+scoped syntax (name := extIffType) "ext_iff_type% " term:max ppSpace ident : term
+
+/--
+`declare_ext_theorems_for A` declares the extensionality theorems for the structure `A`.
+
+These theorems state that two expressions with the structure type are equal if their fields are equal.
+-/
+syntax (name := declareExtTheoremFor) "declare_ext_theorems_for " ("(" &"flat" " := " term ") ")? ident (ppSpace prio)? : command
+
+macro_rules | `(declare_ext_theorems_for $[(flat := $f)]? $struct:ident $(prio)?) => do
+  let flat := f.getD (mkIdent `true)
+  let names ← Macro.resolveGlobalName struct.getId.eraseMacroScopes
+  let name ← match names.filter (·.2.isEmpty) with
+    | [] => Macro.throwError s!"unknown constant {struct.getId}"
+    | [(name, _)] => pure name
+    | _ => Macro.throwError s!"ambiguous name {struct.getId}"
+  let extName := mkIdentFrom struct (canonical := true) <| name.mkStr "ext"
+  let extIffName := mkIdentFrom struct (canonical := true) <| name.mkStr "ext_iff"
+  `(@[ext $(prio)?] protected theorem $extName:ident : ext_type% $flat $struct:ident :=
+      fun {..} {..} => by intros; subst_eqs; rfl
+    protected theorem $extIffName:ident : ext_iff_type% $flat $struct:ident :=
+      fun {..} {..} =>
+        ⟨fun h => by cases h; and_intros <;> rfl,
+         fun _ => by (repeat cases ‹_ ∧ _›); subst_eqs; rfl⟩)
+
+/--
+Applies extensionality lemmas that are registered with the `@[ext]` attribute.
+* `ext pat*` applies extensionality theorems as much as possible,
+  using the patterns `pat*` to introduce the variables in extensionality theorems using `rintro`.
+  For example, the patterns are used to name the variables introduced by lemmas such as `funext`.
+* Without patterns,`ext` applies extensionality lemmas as much
+  as possible but introduces anonymous hypotheses whenever needed.
+* `ext pat* : n` applies ext theorems only up to depth `n`.
+
+The `ext1 pat*` tactic is like `ext pat*` except that it only applies a single extensionality theorem.
+
+Unused patterns will generate warning.
+Patterns that don't match the variables will typically result in the introduction of anonymous hypotheses.
+-/
+syntax (name := ext) "ext" (colGt ppSpace rintroPat)* (" : " num)? : tactic
+
+/-- Apply a single extensionality theorem to the current goal. -/
+syntax (name := applyExtTheorem) "apply_ext_theorem" : tactic
+
+/--
+`ext1 pat*` is like `ext pat*` except that it only applies a single extensionality theorem rather
+than recursively applying as many extensionality theorems as possible.
+
+The `pat*` patterns are processed using the `rintro` tactic.
+If no patterns are supplied, then variables are introduced anonymously using the `intros` tactic.
+-/
+macro "ext1" xs:(colGt ppSpace rintroPat)* : tactic =>
+  if xs.isEmpty then `(tactic| apply_ext_theorem <;> intros)
+  else `(tactic| apply_ext_theorem <;> rintro $xs*)
+
+end Elab.Tactic.Ext
+end Lean
+
+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/Init/Tactics.lean

@@ -941,6 +941,12 @@ syntax (name := repeat1') "repeat1' " tacticSeq : tactic
 syntax "and_intros" : tactic
 macro_rules | `(tactic| and_intros) => `(tactic| repeat' refine And.intro ?_ ?_)
 
+/--
+`subst_eq` repeatedly substitutes according to the equality proof hypotheses in the context,
+replacing the left side of the equality with the right, until no more progress can be made.
+-/
+syntax (name := substEqs) "subst_eqs" : tactic
+
 /-- The `run_tac doSeq` tactic executes code in `TacticM Unit`. -/
 syntax (name := runTac) "run_tac " doSeq : tactic
 

src/Lean/Elab/Tactic.lean

@@ -26,4 +26,5 @@ import Lean.Elab.Tactic.Congr
 import Lean.Elab.Tactic.Guard
 import Lean.Elab.Tactic.RCases
 import Lean.Elab.Tactic.Repeat
+import Lean.Elab.Tactic.Ext
 import Lean.Elab.Tactic.Change

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -326,11 +326,8 @@ def forEachVar (hs : Array Syntax) (tac : MVarId → FVarId → MetaM MVarId) :
 @[builtin_tactic Lean.Parser.Tactic.substVars] def evalSubstVars : Tactic := fun _ =>
   liftMetaTactic fun mvarId => return [← substVars mvarId]
 
-/--
-`subst_eq` repeatedly substitutes according to the equality proof hypotheses in the context,
-replacing the left side of the equality with the right, until no more progress can be made.
--/
-elab "subst_eqs" : tactic => Elab.Tactic.liftMetaTactic1 (·.substEqs)
+@[builtin_tactic Lean.Parser.Tactic.substEqs] def evalSubstEqs : Tactic := fun _ =>
+  Elab.Tactic.liftMetaTactic1 (·.substEqs)
 
 /--
   Searches for a metavariable `g` s.t. `tag` is its exact name.

src/Lean/Elab/Tactic/Ext.lean

@@ -0,0 +1,269 @@
+/-
+Copyright (c) 2021 Gabriel Ebner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gabriel Ebner, Mario Carneiro
+-/
+import Lean.Elab.Tactic.RCases
+import Lean.Elab.Tactic.Repeat
+import Lean.Elab.Tactic.BuiltinTactic
+import Lean.Elab.Command
+import Lean.Linter.Util
+
+namespace Lean.Elab.Tactic.Ext
+open Meta Term
+/-- Information about an extensionality theorem, stored in the environment extension. -/
+structure ExtTheorem where
+  /-- Declaration name of the extensionality theorem. -/
+  declName : Name
+  /-- Priority of the extensionality theorem. -/
+  priority : Nat
+  /--
+  Key in the discrimination tree,
+  for the type in which the extensionality theorem holds.
+  -/
+  keys : Array DiscrTree.Key
+  deriving Inhabited, Repr, BEq, Hashable
+
+/-- The state of the `ext` extension environment -/
+structure ExtTheorems where
+  /-- The tree of `ext` extensions. -/
+  tree   : DiscrTree ExtTheorem := {}
+  /-- Erased `ext`s via `attribute [-ext]`. -/
+  erased  : PHashSet Name := {}
+  deriving Inhabited
+
+/-- Discrimation tree settings for the `ext` extension. -/
+def extExt.config : WhnfCoreConfig := {}
+
+/-- The environment extension to track `@[ext]` theorems. -/
+builtin_initialize extExtension :
+    SimpleScopedEnvExtension ExtTheorem ExtTheorems ←
+  registerSimpleScopedEnvExtension {
+    addEntry := fun { tree, erased } thm =>
+      { tree := tree.insertCore thm.keys thm, erased := erased.erase thm.declName }
+    initial := {}
+  }
+
+/-- Gets the list of `@[ext]` theorems corresponding to the key `ty`,
+ordered from high priority to low. -/
+@[inline] def getExtTheorems (ty : Expr) : MetaM (Array ExtTheorem) := do
+  let extTheorems := extExtension.getState (← getEnv)
+  let arr ← extTheorems.tree.getMatch ty extExt.config
+  let erasedArr := arr.filter fun thm => !extTheorems.erased.contains thm.declName
+  -- Using insertion sort because it is stable and the list of matches should be mostly sorted.
+  -- Most ext theorems have default priority.
+  return erasedArr.insertionSort (·.priority < ·.priority) |>.reverse
+
+/--
+Erases a name marked `ext` by adding it to the state's `erased` field and
+removing it from the state's list of `Entry`s.
+
+This is triggered by `attribute [-ext] name`.
+-/
+def ExtTheorems.eraseCore (d : ExtTheorems) (declName : Name) : ExtTheorems :=
+ { d with erased := d.erased.insert declName }
+
+/--
+  Erases a name marked as a `ext` attribute.
+  Check that it does in fact have the `ext` attribute by making sure it names a `ExtTheorem`
+  found somewhere in the state's tree, and is not erased.
+-/
+def ExtTheorems.erase [Monad m] [MonadError m] (d : ExtTheorems) (declName : Name) :
+    m ExtTheorems := do
+  unless d.tree.containsValueP (·.declName == declName) && !d.erased.contains declName do
+    throwError "'{declName}' does not have [ext] attribute"
+  return d.eraseCore declName
+
+builtin_initialize registerBuiltinAttribute {
+  name := `ext
+  descr := "Marks a theorem as an extensionality theorem"
+  add := fun declName stx kind => do
+    let `(attr| ext $[(flat := $f)]? $(prio)?) := stx
+      | throwError "unexpected @[ext] attribute {stx}"
+    if isStructure (← getEnv) declName then
+      liftCommandElabM <| Elab.Command.elabCommand <|
+        ← `(declare_ext_theorems_for $[(flat := $f)]? $(mkCIdentFrom stx declName) $[$prio]?)
+    else MetaM.run' do
+      if let some flat := f then
+        throwErrorAt flat "unexpected 'flat' config on @[ext] theorem"
+      let declTy := (← getConstInfo declName).type
+      let (_, _, declTy) ← withDefault <| forallMetaTelescopeReducing declTy
+      let failNotEq := throwError
+        "@[ext] attribute only applies to structures or theorems proving x = y, got {declTy}"
+      let some (ty, lhs, rhs) := declTy.eq? | failNotEq
+      unless lhs.isMVar && rhs.isMVar do failNotEq
+      let keys ← withReducible <| DiscrTree.mkPath ty extExt.config
+      let priority ← liftCommandElabM do Elab.liftMacroM do
+        evalPrio (prio.getD (← `(prio| default)))
+      extExtension.add {declName, keys, priority} kind
+  erase := fun declName => do
+    let s := extExtension.getState (← getEnv)
+    let s ← s.erase declName
+    modifyEnv fun env => extExtension.modifyState env fun _ => s
+}
+
+/--
+Constructs the hypotheses for the structure extensionality theorem that
+states that two structures are equal if their fields are equal.
+
+Calls the continuation `k` with the list of parameters to the structure,
+two structure variables `x` and `y`, and a list of pairs `(field, ty)`
+where `ty` is `x.field = y.field` or `HEq x.field y.field`.
+
+If `flat` parses to `true`, any fields inherited from parent structures
+are treated fields of the given structure type.
+If it is `false`, then the behind-the-scenes encoding of inherited fields
+is visible in the extensionality lemma.
+-/
+-- TODO: this is probably the wrong place to have this function
+def withExtHyps (struct : Name) (flat : Term)
+    (k : Array Expr → (x y : Expr) → Array (Name × Expr) → MetaM α) : MetaM α := do
+  let flat ← match flat with
+  | `(true) => pure true
+  | `(false) => pure false
+  | _ => throwErrorAt flat "expected 'true' or 'false'"
+  unless isStructure (← getEnv) struct do throwError "not a structure: {struct}"
+  let structC ← mkConstWithLevelParams struct
+  forallTelescope (← inferType structC) fun params _ => do
+  withNewBinderInfos (params.map (·.fvarId!, BinderInfo.implicit)) do
+  withLocalDeclD `x (mkAppN structC params) fun x => do
+  withLocalDeclD `y (mkAppN structC params) fun y => do
+    let mut hyps := #[]
+    let fields := if flat then
+      getStructureFieldsFlattened (← getEnv) struct (includeSubobjectFields := false)
+    else
+      getStructureFields (← getEnv) struct
+    for field in fields do
+      let x_f ← mkProjection x field
+      let y_f ← mkProjection y field
+      if ← isProof x_f then
+        pure ()
+      else if ← isDefEq (← inferType x_f) (← inferType y_f) then
+        hyps := hyps.push (field, ← mkEq x_f y_f)
+      else
+        hyps := hyps.push (field, ← mkHEq x_f y_f)
+    k params x y hyps
+
+/--
+Creates the type of the extensionality theorem for the given structure,
+elaborating to `x.1 = y.1 → x.2 = y.2 → x = y`, for example.
+-/
+@[builtin_term_elab extType] def elabExtType : TermElab := fun stx _ => do
+  match stx with
+  | `(ext_type%  $flat:term $struct:ident) => do
+    withExtHyps (← resolveGlobalConstNoOverloadWithInfo struct) flat fun params x y hyps => do
+      let ty := hyps.foldr (init := ← mkEq x y) fun (f, h) ty =>
+        mkForall f BinderInfo.default h ty
+      mkForallFVars (params |>.push x |>.push y) ty
+  | _ => throwUnsupportedSyntax
+
+/--
+Creates the type of the iff-variant of the extensionality theorem for the given structure,
+elaborating to `x = y ↔ x.1 = y.1 ∧ x.2 = y.2`, for example.
+-/
+@[builtin_term_elab extIffType] def elabExtIffType : TermElab := fun stx _ => do
+  match stx with
+  | `(ext_iff_type% $flat:term $struct:ident) => do
+    withExtHyps (← resolveGlobalConstNoOverloadWithInfo struct) flat fun params x y hyps => do
+      mkForallFVars (params |>.push x |>.push y) <|
+        mkIff (← mkEq x y) <| mkAndN (hyps.map (·.2)).toList
+  | _ => throwUnsupportedSyntax
+
+/-- Apply a single extensionality theorem to `goal`. -/
+def applyExtTheoremAt (goal : MVarId) : MetaM (List MVarId) := goal.withContext do
+  let tgt ← goal.getType'
+  unless tgt.isAppOfArity ``Eq 3 do
+    throwError "applyExtTheorem only applies to equations, not{indentExpr tgt}"
+  let ty := tgt.getArg! 0
+  let s ← saveState
+  for lem in ← getExtTheorems ty do
+    try
+      -- Note: We have to do this extra check to ensure that we don't apply e.g.
+      -- funext to a goal `(?a₁ : ?b) = ?a₂` to produce `(?a₁ x : ?b') = ?a₂ x`,
+      -- since this will loop.
+      -- We require that the type of the equality is not changed by the `goal.apply c` line
+      -- TODO: add flag to apply tactic to toggle unification vs. matching
+      withNewMCtxDepth do
+        let c ← mkConstWithFreshMVarLevels lem.declName
+        let (_, _, declTy) ← withDefault <| forallMetaTelescopeReducing (← inferType c)
+        guard (← isDefEq tgt declTy)
+      -- We use `newGoals := .all` as this is
+      -- more useful in practice with dependently typed arguments of `@[ext]` theorems.
+      return ← goal.apply (cfg := { newGoals := .all }) (← mkConstWithFreshMVarLevels lem.declName)
+    catch _ => s.restore
+  throwError "no applicable extensionality theorem found for{indentExpr ty}"
+
+/-- Apply a single extensionality theorem to the current goal. -/
+@[builtin_tactic applyExtTheorem] def evalApplyExtTheorem : Tactic := fun _ => do
+  liftMetaTactic applyExtTheoremAt
+
+/--
+Postprocessor for `withExt` which runs `rintro` with the given patterns when the target is a
+pi type.
+-/
+def tryIntros [Monad m] [MonadLiftT TermElabM m] (g : MVarId) (pats : List (TSyntax `rcasesPat))
+    (k : MVarId → List (TSyntax `rcasesPat) → m Nat) : m Nat := do
+  match pats with
+  | [] => k (← (g.intros : TermElabM _)).2 []
+  | p::ps =>
+    if (← (g.withContext g.getType' : TermElabM _)).isForall then
+      let mut n := 0
+      for g in ← RCases.rintro #[p] none g do
+        n := n.max (← tryIntros g ps k)
+      pure (n + 1)
+    else k g pats
+
+/--
+Applies a single extensionality theorem, using `pats` to introduce variables in the result.
+Runs continuation `k` on each subgoal.
+-/
+def withExt1 [Monad m] [MonadLiftT TermElabM m] (g : MVarId) (pats : List (TSyntax `rcasesPat))
+    (k : MVarId → List (TSyntax `rcasesPat) → m Nat) : m Nat := do
+  let mut n := 0
+  for g in ← (applyExtTheoremAt g : TermElabM _) do
+    n := n.max (← tryIntros g pats k)
+  pure n
+
+/--
+Applies extensionality theorems recursively, using `pats` to introduce variables in the result.
+Runs continuation `k` on each subgoal.
+-/
+def withExtN [Monad m] [MonadLiftT TermElabM m] [MonadExcept Exception m]
+    (g : MVarId) (pats : List (TSyntax `rcasesPat)) (k : MVarId → List (TSyntax `rcasesPat) → m Nat)
+    (depth := 1000000) (failIfUnchanged := true) : m Nat :=
+  match depth with
+  | 0 => k g pats
+  | depth+1 => do
+    if failIfUnchanged then
+      withExt1 g pats fun g pats => withExtN g pats k depth (failIfUnchanged := false)
+    else try
+      withExt1 g pats fun g pats => withExtN g pats k depth (failIfUnchanged := false)
+    catch _ => k g pats
+
+/--
+Apply extensionality theorems as much as possible, using `pats` to introduce the variables
+in extensionality theorems like `funext`. Returns a list of subgoals.
+
+This is built on top of `withExtN`, running in `TermElabM` to build the list of new subgoals.
+(And, for each goal, the patterns consumed.)
+-/
+def extCore (g : MVarId) (pats : List (TSyntax `rcasesPat))
+    (depth := 1000000) (failIfUnchanged := true) :
+    TermElabM (Nat × Array (MVarId × List (TSyntax `rcasesPat))) := do
+  StateT.run (m := TermElabM) (s := #[])
+    (withExtN g pats (fun g qs => modify (·.push (g, qs)) *> pure 0) depth failIfUnchanged)
+
+@[builtin_tactic ext] def evalExt : Tactic := fun stx => do
+  match stx with
+  | `(tactic| ext $pats* $[: $n]?) => do
+    let pats := RCases.expandRIntroPats pats
+    let depth := n.map (·.getNat) |>.getD 1000000
+    let (used, gs) ← extCore (← getMainGoal) pats.toList depth
+    if RCases.linter.unusedRCasesPattern.get (← getOptions) then
+      if used < pats.size then
+        Linter.logLint RCases.linter.unusedRCasesPattern (mkNullNode pats[used:].toArray)
+          m!"`ext` did not consume the patterns: {pats[used:]}"
+    replaceMainGoal <| gs.map (·.1) |>.toList
+  | _ => throwUnsupportedSyntax
+
+end Lean.Elab.Tactic.Ext

src/Lean/Expr.lean

@@ -1916,7 +1916,14 @@ def mkNot (p : Expr) : Expr := mkApp (mkConst ``Not) p
 def mkOr (p q : Expr) : Expr := mkApp2 (mkConst ``Or) p q
 /-- Return `p ∧ q` -/
 def mkAnd (p q : Expr) : Expr := mkApp2 (mkConst ``And) p q
+/-- Make an n-ary `And` application. `mkAndN []` returns `True`. -/
+def mkAndN : List Expr → Expr
+  | [] => mkConst ``True
+  | [p] => p
+  | p :: ps => mkAnd p (mkAndN ps)
 /-- Return `Classical.em p` -/
 def mkEM (p : Expr) : Expr := mkApp (mkConst ``Classical.em) p
+/-- Return `p ↔ q` -/
+def mkIff (p q : Expr) : Expr := mkApp2 (mkConst ``Iff) p q
 
 end Lean

tests/lean/run/ext1.lean

@@ -0,0 +1,104 @@
+axiom mySorry {α : Sort _} : α
+
+structure A (n : Nat) where
+  a : Nat
+
+example (a b : A n) : a = b ∨ True := by
+  fail_if_success
+    apply Or.inl; ext
+  exact Or.inr trivial
+
+structure B (n) extends A n where
+  b : Nat
+  h : b > 0
+  i : Fin b
+
+@[ext] structure C (n) extends B n where
+  c : Nat
+
+example (a b : C n) : a = b := by
+  ext
+  guard_target = a.a = b.a; exact mySorry
+  guard_target = a.b = b.b; exact mySorry
+  guard_target = HEq a.i b.i; exact mySorry
+  guard_target = a.c = b.c; exact mySorry
+
+@[ext (flat := false)] structure C' (n) extends B n where
+  c : Nat
+
+example (a b : C' n) : a = b := by
+  ext
+  guard_target = a.toB = b.toB; exact mySorry
+  guard_target = a.c = b.c; exact mySorry
+
+open Lean.Elab.Tactic.Ext
+example (f g : Nat × Nat → Nat) : f = g := by
+  ext ⟨x, y⟩
+  guard_target = f (x, y) = g (x, y); exact mySorry
+
+-- Check that we generate a warning if there are too many patterns.
+-- /-- warning: `ext` did not consume the patterns: [j] [linter.unusedRCasesPattern] -/
+-- #guard_msgs in
+-- example (f g : Nat → Nat) (h : f = g) : f = g := by
+--  ext i j
+--  exact h ▸ rfl
+
+-- allow more specific ext theorems
+declare_ext_theorems_for Fin
+@[ext high] theorem Fin.zero_ext (a b : Fin 0) : True → a = b := by cases a.isLt
+example (a b : Fin 0) : a = b := by ext; exact True.intro
+
+def Set (α : Type u) := α → Prop
+@[ext] structure LocalEquiv (α : Type u) (β : Type v) where
+  source : Set α
+@[ext] structure Pretrivialization {F : Type u} (proj : Z → β) extends LocalEquiv Z (β × F) where
+  baseSet : Set β
+  source_eq : source = baseSet ∘ proj
+
+structure MyUnit
+
+@[ext high] theorem MyUnit.ext1 (x y : MyUnit) (_h : 0 = 1) : x = y := rfl
+@[ext high] theorem MyUnit.ext2 (x y : MyUnit) (_h : 1 = 1) : x = y := rfl
+@[ext] theorem MyUnit.ext3 (x y : MyUnit) (_h : 2 = 1) : x = y := rfl
+
+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:
+example (f : ℕ × (ℕ → ℕ)) : f = f := by
+  ext x
+  · rfl
+  · guard_target = (f.2) x = (f.2) x
+    rfl
+
+example (f : Empty → Empty) : f = f := by
+  ext ⟨⟩
+
+@[ext] theorem ext_intros {n m : Nat} (w : ∀ n m : Nat, n = m) : n = m := by apply w
+
+example : 3 = 7 := by
+  ext : 1
+  rename_i n m
+  guard_target = n = m
+  admit
+
+example : 3 = 7 := by
+  ext n m : 1
+  guard_target = n = m
+  admit
+
+section erasing_ext_attribute
+
+def f (p : Int × Int) : Int × Int := (p.2, p.1)
+
+example : f ∘ f = id := by
+  ext ⟨a, b⟩
+  · simp [f]
+  · simp [f]
+
+attribute [-ext] Prod.ext
+
+example : f ∘ f = id := by
+  ext ⟨a, b⟩
+  simp [f]
+
+end erasing_ext_attribute