# Question about default definitions in fields

In Unclarity about Preorder class in Lean4 I asked why the third and fourth field (lt and lt_iff_le_not_le) in the definition of MyPreorder below would both be necessary, as one follows from the other as far as I can see. The answer was that this happens because there is no clear preference over defining LE or LT - hence the fourth line - and that the third line is there for convenience, as a default definition.

However, if I next want to build a product preorder, it seems that I do need to repeat the definition of lt, even though it was expected to be a default? At least, if I leave it out, the assumptions at the end of the proof do not get resolved properly anymore. Notably, Lean does not ask me to define lt, it just doesn't recognize that I mean the default definition aparently.

class MyPreorder.{u} (α : Type u) extends LE α, LT α :=
(le_refl : ∀ a : α, a ≤ a)
(le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c)
(lt := λ a b => a ≤ b ∧ ¬ b ≤ a) -- default definition introduced for convenience
(lt_iff_le_not_le : ∀ a b : α, a < b ↔ (a ≤ b ∧ ¬ b ≤ a)) -- expected relation between lt and le

instance MyProd_Preorder [P : MyPreorder α] [Q : MyPreorder β] : MyPreorder (Prod α β) where
le := fun x y => x.fst ≤ y.fst ∧ x.snd ≤ y.snd
lt := λ a b => a ≤ b ∧ ¬ b ≤ a -- WHY DO I HAVE TO REPEAT THE DEFAULT ?
le_refl := by
intros
constructor
. apply P.le_refl
. apply Q.le_refl
le_trans := by
intros x y z
intros a b
have ineq1 := And.left a
have ineq2 := And.right a
have ineq3 := And.left b
have ineq4 := And.right b
constructor
. apply P.le_trans _ _ _ ineq1 ineq3
. apply Q.le_trans _ _ _ ineq2 ineq4
lt_iff_le_not_le := by
intros x y
constructor
. intro
assumption
. intro
assumption

I'm not entirely sure however whether this is really the problem, or it's just my inability in Lean. A related attempt to just derive lt_iff_le_not_le from the definition of lt also fails. So perhaps I'm doing something different wrong...

class AnotherPreorder.{u} (α : Type u) extends LE α, LT α :=
(le_refl : ∀ a : α, a ≤ a)
(le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c)
(lt := λ a b => a ≤ b ∧ ¬ b ≤ a) -- default definition introduced for convenience
-- I've left out the iff relation from this definition, in order to try to derive it...

example (α : Type u) [P : AnotherPreorder α] : ∀ a b : α, a < b ↔ (a ≤ b ∧ ¬ b ≤ a) := by
intros a b
constructor
. intro
assumption -- these fail miserably, and I don't understand why, as they do work in the other example...
. intro
assumption -- these fail miserably, and I don't understand why, as they do work in the other example...
$$`$$
• You first example isn't type checking for me. Are you sure it is correct? Sep 22 at 14:37
• Ah, you are right, when I run it in complete isolation the example doesn't type check. I've by now also figured out a few steps towards my solution because of this. Sep 22 at 15:22