fix: removed (incorrect) test for symm, trans attributes (#857)

Fixes error I made: introducing a test for `symm` and `trans` attributes to check that the lemmas were "genuinely" symm/trans lemmas. However the tests had false positives, e.g. #855 (which has been added to the tests).

This short commit removes the tests. They were not present in `mathlib3` anyway and the worst that happens if a lemma is incorrectly labelled is that the `symm` tactic tries and fails with this.

As a warning it may be useful to have a test, but it should have no false positives. For now it seems the best approach is to drop the test.

Author: siddhartha-gadgil

Mathlib/Tactic/Relation/Symm.lean

@@ -32,10 +32,9 @@ initialize registerBuiltinAttribute {
     let (xs, _, targetTy) ← withReducible <| forallMetaTelescopeReducing declTy
     let fail := throwError
       "@[symm] attribute only applies to lemmas proving x ∼ y → y ∼ x, got {declTy}"
-    let some finalHyp := xs.back? | fail
-    let .app (.app rel lhs) rhs := targetTy | fail
-    let flip := .app (.app rel rhs) lhs
-    let .true ← withNewMCtxDepth <| isDefEqGuarded flip (← inferType finalHyp) | fail
+    let some _ := xs.back? | fail
+    let targetTy ← reduce targetTy
+    let .app (.app rel _) _ := targetTy | fail
     let key ← withReducible <| DiscrTree.mkPath rel
     symmExt.add (decl, key) kind
 }

Mathlib/Tactic/Relation/Trans.lean

@@ -32,14 +32,11 @@ initialize registerBuiltinAttribute {
     let (xs, _, targetTy) ← withReducible <| forallMetaTelescopeReducing declTy
     let fail := throwError
       "@[trans] attribute only applies to lemmas proving x ∼ y → y ∼ z → x ∼ z, got {declTy}"
-    let .app (.app rel x₂) z₂ := targetTy | fail
+    let .app (.app rel _) _ := targetTy | fail
     let some yzHyp := xs.back? | fail
     let some xyHyp := xs.pop.back? | fail
-    let .app (.app rel₂ y₂) z₁ ← inferType yzHyp | fail
-    let .app (.app rel₁ x₁) y₁ ← inferType xyHyp | fail
-    let .true ← withNewMCtxDepth <|
-      isDefEq x₁ x₂ <&&> isDefEq y₁ y₂ <&&> isDefEq z₁ z₂ <&&>
-      isDefEq rel rel₁ <&&> isDefEq rel rel₂ | fail
+    let .app (.app _ _) _ ← inferType yzHyp | fail
+    let .app (.app _ _) _ ← inferType xyHyp | fail
     let key ← withReducible <| DiscrTree.mkPath rel
     transExt.add (decl, key) kind
 }

test/symm.lean

@@ -1,6 +1,7 @@
 import Mathlib.Tactic.Relation.Symm
 import Std.Tactic.ShowTerm
-
+import Mathlib.Algebra.Hom.Group
+import Mathlib.Logic.Equiv.Basic
 -- testing that the attribute is recognized
 @[symm] def eq_symm {α : Type} (a b : α) : a = b → b = a := Eq.symm
 
@@ -13,3 +14,23 @@ def sameParity : Nat → Nat → Prop
 @[symm] def sameParity_symm (n m : Nat) : sameParity n m → sameParity m n := Eq.symm
 
 example (a b : Nat) : sameParity a b → sameParity b a := by intros; symm; assumption
+
+
+def MulHom.inverse [Mul M] [Mul N] (f : M →ₙ* N) (g : N → M) (h₁ : Function.LeftInverse g f)
+    (h₂ : Function.RightInverse g f) : N →ₙ* M where
+  toFun := g
+  map_mul' x y :=
+    calc
+      g (x * y) = g (f (g x) * f (g y)) := by rw [h₂ x, h₂ y]
+      _ = g (f (g x * g y)) := by rw [f.map_mul]
+      _ = g x * g y := h₁ _
+
+structure MulEquiv (M N : Type u) [Mul M] [Mul N] extends M ≃ N, M →ₙ* N
+
+#check @MulEquiv
+
+infixl:25 " ≃* " => MulEquiv
+
+@[symm]
+def foo_symm {M N : Type _} [Mul M] [Mul N] (h : M ≃* N) : N ≃* M :=
+  { h.toEquiv.symm with map_mul' := (h.toMulHom.inverse h.toEquiv.symm h.left_inv h.right_inv).map_mul }