Question about default definitions in fields

Question

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...
```

Answer 1

Thanks to Jason Rute his comment, I think I can now answer my own question partially. I figured out that my example does not typecheck in isolation, whereas it did in my sandbox file because there was an import that defined instProdLE under the hood. My definition of lt in the MyProd_Preorder took that instance in order to determine the type of the definition.

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?