feat: subst notation (heq ▸ h) tries both orientation (#4046)

even when rewriting the type of `h` becuase there is no expected type.

(When there is an expected type, it already tried both orientations.)

Also feeble attempt to include this information in the docstring without
writing half a manual chapter.

src/Lean/Elab/BuiltinNotation.lean

@@ -388,7 +388,7 @@ private def withLocalIdentFor (stx : Term) (e : Expr) (k : Term → TermElabM Ex
                return (← mkEqRec motive h (← mkEqSymm heq), none)
          let motive ← mkMotive lhs expectedAbst
          if badMotive?.isSome || !(← isTypeCorrect motive) then
-           -- Before failing try tos use `subst`
+           -- Before failing try to use `subst`
            if ← (isSubstCandidate lhs rhs <||> isSubstCandidate rhs lhs) then
              withLocalIdentFor heqStx heq fun heqStx => do
                let h ← instantiateMVars h
@@ -408,9 +408,13 @@ private def withLocalIdentFor (stx : Term) (e : Expr) (k : Term → TermElabM Ex
        | none =>
          let h ← elabTerm hStx none
          let hType ← inferType h
-         let hTypeAbst ← kabstract hType lhs
+         let mut hTypeAbst ← kabstract hType lhs
          unless hTypeAbst.hasLooseBVars do
-           throwError "invalid `▸` notation, the equality{indentExpr heq}\nhas type {indentExpr heqType}\nbut its left hand side is not mentioned in the type{indentExpr hType}"
+           hTypeAbst ← kabstract hType rhs
+           unless hTypeAbst.hasLooseBVars do
+             throwError "invalid `▸` notation, the equality{indentExpr heq}\nhas type {indentExpr heqType}\nbut neither side of the equality is mentioned in the type{indentExpr hType}"
+           heq ← mkEqSymm heq
+           (lhs, rhs) := (rhs, lhs)
          let motive ← mkMotive lhs hTypeAbst
          unless (← isTypeCorrect motive) do
            throwError "invalid `▸` notation, failed to compute motive for the substitution"

src/Lean/Parser/Term.lean

@@ -807,6 +807,10 @@ It is especially useful for avoiding parentheses with repeated applications.
 Given `h : a = b` and `e : p a`, the term `h ▸ e` has type `p b`.
 You can also view `h ▸ e` as a "type casting" operation
 where you change the type of `e` by using `h`.
+
+The macro tries both orientations of `h`. If the context provides an
+expected type, it rewrites the expeced type, else it rewrites the type of e`.
+
 See the Chapter "Quantifiers and Equality" in the manual
 "Theorem Proving in Lean" for additional information.
 -/

tests/lean/substFails.lean

@@ -2,13 +2,15 @@ def foo := 3
 def bar := 4
 
 def ex1  (heq : foo = bar) (P : Nat → Prop) (h : P foo)         := heq ▸ h
+#check ex1
 def ex2  (heq : foo = bar) (P : Nat → Prop) (h : P foo) : P 4   := heq ▸ h -- error
 def ex3  (heq : foo = bar) (P : Nat → Prop) (h : P foo) : P bar := heq ▸ h
 def ex4  (heq : foo = bar) (P : Nat → Prop) (h : P 3)           := heq ▸ h -- error
 def ex5  (heq : foo = bar) (P : Nat → Prop) (h : P 3)   : P 4   := heq ▸ h -- error
 def ex6  (heq : foo = bar) (P : Nat → Prop) (h : P 3)   : P bar := heq ▸ h
 
-def ex7  (heq : bar = foo) (P : Nat → Prop) (h : P foo)         := heq ▸ h -- error
+def ex7  (heq : bar = foo) (P : Nat → Prop) (h : P foo)         := heq ▸ h
+#check ex7
 def ex8  (heq : bar = foo) (P : Nat → Prop) (h : P foo) : P 4   := heq ▸ h -- error
 def ex9  (heq : bar = foo) (P : Nat → Prop) (h : P foo) : P bar := heq ▸ h
 def ex10 (heq : bar = foo) (P : Nat → Prop) (h : P 3)           := heq ▸ h -- error

tests/lean/substFails.lean.expected.out

@@ -1,43 +1,39 @@
-substFails.lean:5:67-5:74: error: invalid `▸` notation, expected result type of cast is 
+ex1 (heq : foo = bar) (P : Nat → Prop) (h : P foo) : P bar
+substFails.lean:6:67-6:74: error: invalid `▸` notation, expected result type of cast is 
   P 4
 however, the equality 
   heq
 of type 
   foo = bar
 does not contain the expected result type on either the left or the right hand side
-substFails.lean:7:67-7:74: error: invalid `▸` notation, the equality
+substFails.lean:8:67-8:74: error: invalid `▸` notation, the equality
   heq
 has type 
   foo = bar
-but its left hand side is not mentioned in the type
+but neither side of the equality is mentioned in the type
   P 3
-substFails.lean:8:67-8:74: error: invalid `▸` notation, expected result type of cast is 
+substFails.lean:9:67-9:74: error: invalid `▸` notation, expected result type of cast is 
   P 4
 however, the equality 
   heq
 of type 
   foo = bar
 does not contain the expected result type on either the left or the right hand side
-substFails.lean:11:67-11:74: error: invalid `▸` notation, the equality
-  heq
-has type 
-  bar = foo
-but its left hand side is not mentioned in the type
-  P foo
-substFails.lean:12:67-12:74: error: invalid `▸` notation, expected result type of cast is 
+ex7 (heq : bar = foo) (P : Nat → Prop) (h : P foo) : P bar
+substFails.lean:14:67-14:74: error: invalid `▸` notation, expected result type of cast is 
   P 4
 however, the equality 
   heq
 of type 
   bar = foo
 does not contain the expected result type on either the left or the right hand side
-substFails.lean:14:67-14:74: error: invalid `▸` notation, the equality
+substFails.lean:16:67-16:74: error: invalid `▸` notation, the equality
   heq
 has type 
   bar = foo
-but its left hand side is not mentioned in the type
+but neither side of the equality is mentioned in the type
   P 3
-substFails.lean:15:67-15:74: error: invalid `▸` notation, expected result type of cast is 
+substFails.lean:17:67-17:74: error: invalid `▸` notation, expected result type of cast is 
   P 4
 however, the equality 
   heq