x y : ℝ
a b : CauSeq ℚ abs
⊢ { cauchy := Quotient.mk equiv (a ⊓ b) } =
    match { cauchy := Quotient.mk equiv a }, { cauchy := Quotient.mk equiv b } with
    | { cauchy := x }, { cauchy := y } =>
      { cauchy := Quotient.map₂ (fun x x_1 => x ⊓ x_1) Real.definition.proof_2✝ x y }
x y : ℝ
a b : CauSeq ℚ abs
⊢ { cauchy := Quotient.mk equiv (a ⊓ b) } = Real.inf { cauchy := Quotient.mk equiv a } { cauchy := Quotient.mk equiv b }
rw [inf_def]
no goals
x y : ℝ
a b : CauSeq ℚ abs
⊢ { cauchy := Quotient.mk equiv (a ⊓ b) } =
    match { cauchy := Quotient.mk equiv a }, { cauchy := Quotient.mk equiv b } with
    | { cauchy := x }, { cauchy := y } =>
      { cauchy := Quotient.map₂ (fun x x_1 => x ⊓ x_1) Real.definition.proof_2✝ x y }
rfl