partial order tactic

Stream: new members

[Joseph Qian]

Hi everyone,
I'm an undergraduate student at the University of Washington, and I have been working with some other students to write a tactic that applies transitivity over a partially ordered set, e.g.

example (a b c : α) [PartialOrder α] (hab : a ≤ b) (hbc : b ≤ c) : a ≤ c := by  partiarith

The tactic works now and we are almost ready to submit a pull request. Do we need to do anything before we submit the PR? Thanks.

[Louis Cabarion]

How does it compare to the order tactic?

import Mathlib
example (a b c : α) [PartialOrder α] (hab : a ≤ b) (hbc : b ≤ c) : a ≤ c := by
  order