Lean4
/-- Given an (in)equality `a = b` (respectively, `a ≤ b`, `a < b`), cancel nonzero (resp. positive)
factors to construct a new (in)equality which is logically equivalent to `a = b` (respectively,
`a ≤ b`, `a < b`). -/
def reduceProp (disch : ∀ {u : Level} (type : Q(Sort u)), MetaM Q($type)) (t : Expr) : AtomM Simp.Result := do
let ⟨i, _, a, b⟩ ← t.ineq?
let ⟨u, K, a⟩ ← inferTypeQ' a
let iK : Q(CommGroupWithZero $K) ← synthInstanceQ q(CommGroupWithZero $K)
trace[Tactic.field_simp]"clearing denominators in {a } ~ {b}"
match i with
| .eq =>
let ⟨a', b', pf⟩ ← reduceEqQ disch iK a b
let t' ← mkAppM `Eq #[a', b']
return { expr := t', proof? := pf }
| .le =>
let iK' : Q(PartialOrder $K) ← synthInstanceQ q(PartialOrder $K)
let iK'' : Q(PosMulStrictMono $K) ← synthInstanceQ q(PosMulStrictMono $K)
let iK''' : Q(PosMulReflectLE $K) ← synthInstanceQ q(PosMulReflectLE $K)
let iK'''' : Q(ZeroLEOneClass $K) ← synthInstanceQ q(ZeroLEOneClass $K)
let ⟨a', b', pf⟩ ← reduceLeQ disch iK iK' iK'' iK''' iK'''' a b
let t' ← mkAppM `LE.le #[a', b']
return { expr := t', proof? := pf }
| _ =>
let iK' : Q(PartialOrder $K) ← synthInstanceQ q(PartialOrder $K)
let iK'' : Q(PosMulStrictMono $K) ← synthInstanceQ q(PosMulStrictMono $K)
let iK''' : Q(PosMulReflectLT $K) ← synthInstanceQ q(PosMulReflectLT $K)
let iK'''' : Q(ZeroLEOneClass $K) ← synthInstanceQ q(ZeroLEOneClass $K)
let ⟨a', b', pf⟩ ← reduceLtQ disch iK iK' iK'' iK''' iK'''' a b
let t' ← mkAppM `LT.lt #[a', b']
return { expr := t', proof? := pf }
