# 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, 2022 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, 2022 at 15:22

That also explains why I needed to explicitly define lt in the first place. Although in Unclarity about Preorder class in Lean4 it was mentioned that the definition of MyPreorder provides a default, that is not the default that is taken when I leave the definition of lt implicit. It turns out that, in the Lean4 core there is a definition of instLTProd which takes preference. That definition is subtly different.
Which only leaves me with the question, is there a tactic for unrolling definitions? I.e. if I've defined lt := fun x y => x something y  and the state in my proof says x < y, how can I turn it into an explicit x something y?
• Also, you should generally try to avoid getting yourself into situations where you are defining two instances for the same thing. This is called a diamond and it creates problems, especially when the instances are not definitionally equal (and worse when they are totally different as in this case). In this case you were defining two instances of < for (α × β)`. Sep 22, 2022 at 17:35