Is there an infix notation that would allow to rewrite those proofs
example (h₀ : a ≤ b) (h₁ : b < c) (h₂ : c ≤ d) (h₃ : d < e) :
a < e := lt_trans (lt_of_lt_of_le (lt_of_le_of_lt (h₀) h₁) h₂ ) h₃
example (h₀ : a ≤ b) (h₁ : b < c) (h₂ : c ≤ d) (h₃ : d < e) :
a < e := by
{ apply lt_trans,
{apply lt_of_lt_of_le,
{apply lt_of_le_of_lt, apply h₀, apply h₁}
, apply h₂},
apply h₃
}
more naturally as
example (h₀ : a ≤ b) (h₁ : b < c) (h₂ : c ≤ d) (h₃ : d < e) :
a < e := ((h₀ `lt_of_le_of_lt` h₁) `lt_of_lt_of_le` h₂) `lt_trans` h₃
You can use Lean's dot notation to make an infix version of the argument, for example
example (h₀ : a ≤ b) (h₁ : b < c) (h₂ : c ≤ d) (h₃ : d < e) :
a < e := (h₀.trans_lt h₁).trans (h₂.trans_lt h₃)
What's going on here is that the type of h₀
is le a b
(in the has_le
namespace), so h₀.trans_lt
means le.trans_lt h₀
, and you can see in order.basic
in mathlib that le.trans_lt
is just an abbreviation for lt_of_le_of_lt
.