rw [Trichotomy] at *
case right
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
hStrich : Trichotomy (S p.1 q.1) (S q.1 p.1) (p.1 = q.1)
hTtrich : Trichotomy (T p.2 q.2) (T q.2 p.2) (p.2 = q.2)
⊢ Trichotomy (S p.1 q.1 ∨ p.1 = q.1 ∧ T p.2 q.2) (S q.1 p.1 ∨ q.1 = p.1 ∧ T q.2 p.2) (p = q)
case right
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
hStrich :
  ¬S p.1 q.1 ∧ ¬S q.1 p.1 ∧ p.1 = q.1 ∨ ¬S p.1 q.1 ∧ S q.1 p.1 ∧ ¬p.1 = q.1 ∨ S p.1 q.1 ∧ ¬S q.1 p.1 ∧ ¬p.1 = q.1
hTtrich :
  ¬T p.2 q.2 ∧ ¬T q.2 p.2 ∧ p.2 = q.2 ∨ ¬T p.2 q.2 ∧ T q.2 p.2 ∧ ¬p.2 = q.2 ∨ T p.2 q.2 ∧ ¬T q.2 p.2 ∧ ¬p.2 = q.2
⊢ ¬(S p.1 q.1 ∨ p.1 = q.1 ∧ T p.2 q.2) ∧ ¬(S q.1 p.1 ∨ q.1 = p.1 ∧ T q.2 p.2) ∧ p = q ∨
    ¬(S p.1 q.1 ∨ p.1 = q.1 ∧ T p.2 q.2) ∧ (S q.1 p.1 ∨ q.1 = p.1 ∧ T q.2 p.2) ∧ ¬p = q ∨
      (S p.1 q.1 ∨ p.1 = q.1 ∧ T p.2 q.2) ∧ ¬(S q.1 p.1 ∨ q.1 = p.1 ∧ T q.2 p.2) ∧ ¬p = q