x y : ℝ
f g : CauSeq ℚ abs
⊢ (match { cauchy := Quotient.mk equiv f }, { cauchy := Quotient.mk equiv g } with
    | { cauchy := x }, { cauchy := y } => Quotient.liftOn₂ x y (fun x x_1 => x < x_1) Real.definition.proof_1✝) ↔
    f < g
x y : ℝ
f g : CauSeq ℚ abs
⊢ Real.lt { cauchy := Quotient.mk equiv f } { cauchy := Quotient.mk equiv g } ↔ f < g
rw [lt_def]
no goals
x y : ℝ
f g : CauSeq ℚ abs
⊢ (match { cauchy := Quotient.mk equiv f }, { cauchy := Quotient.mk equiv g } with
    | { cauchy := x }, { cauchy := y } => Quotient.liftOn₂ x y (fun x x_1 => x < x_1) Real.definition.proof_1✝) ↔
    f < g
rfl