Symm and Trans tactics implementation

Stream: mathlib4

[Siddhartha Gadgil]

Corrected the issue with the meaning of the argument, and also use the typeclass where available. I have stuck to the mathematical meaning of transitivity though, rather than the more general one in Trans.

Below is the new test-code. Any further suggestions @Sebastian Ullrich @Mario Carneiro ?

def nleq : Nat → Nat → Prop
| a, b => a ≤ b

@[trans] def nleqTrans {a b c : Nat} : nleq a b → nleq b c → nleq a c := Nat.le_trans

example (a b c : Nat): nleq a b → nleq b c → nleq a c := by
   intro h₁ h₂
   trans b
   assumption
   assumption

example (a b c : Nat): nleq a b → nleq b c → nleq a c := by
   intro h₁ h₂
   trans
   assumption
   assumption

-- using `Trans` typeclass
@[trans] def eqTrans {α : Type}{a b c : α}:  a = b → b = c → a = c := by
    intro h₁ h₂
    apply Eq.trans h₁ h₂


example (a b c : Nat): a = b → b = c → a = c := by
    intro h₁ h₂
    trans
    assumption
    assumption

example (a b c : Nat): a = b → b = c → a = c := by
    intro h₁ h₂
    trans b
    assumption
    assumption

example : Trans ((. ≤ . : Nat → Nat → Prop))
        (. ≤ . : Nat → Nat → Prop) (. ≤ . : Nat → Nat → Prop) := inferInstance

example (a b c : Nat): a ≤  b → b ≤  c → a ≤  c := by
   intro h₁ h₂
   trans b
   assumption
   assumption

example (a b c : Nat): a ≤  b → b ≤  c → a ≤  c := by
   intro h₁ h₂
   trans
   assumption
   assumption


example (a b c : Nat): a <  b → b <  c → a <  c := by
   intro h₁ h₂
   trans b
   assumption
   assumption

example (a b c : Nat): a <  b → b < c → a <  c := by
   intro h₁ h₂
   trans
   assumption
   assumption

[Siddhartha Gadgil]

For reference, the PR is at https://github.com/leanprover-community/mathlib4/pull/253