awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Real.Basic
Goal:
f : CauSeq ℚ abs
⊢ 0 < f ↔ f.Pos

Tactic:
exact iff_of_eq (congr_arg Pos (sub_zero f))

Premises used: CauSeq.Pos, sub_zero, congr_arg, iff_of_eq
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℚ
⊢ mk (const abs x) = (↑x : ℝ)

Tactic:
rfl

Premises used: CauSeq.Completion.ofRat, CauSeq.Completion.mk, Real.mk, rfl
-- Module: Mathlib.Data.Real.Basic
Goal:
x y : ℝ
⊢ x ≤ y ↔ x < y ∨ x = y

Tactic:
iff_of_eq <| le_def _ _

Premises used: _private.0.Real.le_def, iff_of_eq
-- Module: Mathlib.Data.Real.Basic
Goal:
f g : CauSeq ℚ abs
simp : f < g ∨ f ≈ g ↔ f ≤ g
⊢ mk f ≤ mk g ↔ f ≤ g

Tactic:
simp only [le_def', mk_lt, mk_eq]

Premises used: Real.mk_lt, _private.0.Real.le_def', Real.mk_eq
-- Module: Mathlib.Data.Real.Basic
Goal:
f g : CauSeq ℚ abs
⊢ f < g ∨ f ≈ g ↔ f ≤ g

Tactic:
rfl
-- Module: Mathlib.Data.Real.Basic
Goal:
C : ℝ → Prop
x : ℝ
h : ∀ (y : CauSeq ℚ abs), C (mk y)
obtain : ∀ (x : Cauchy (α := ℚ) abs), C { cauchy := x }
⊢ C x

Tactic:
obtain ⟨x⟩ := x
-- Module: Mathlib.Data.Real.Basic
Goal:
C : ℝ → Prop
h : ∀ (y : CauSeq ℚ abs), C (mk y)
x : Cauchy (α := ℚ) abs
h₁ : ∀ (a : CauSeq ℚ abs), C { cauchy := Quot.mk (⇑equiv : CauSeq ℚ abs → CauSeq ℚ abs → Prop) a }
⊢ C { cauchy := x }

Tactic:
induction x using Quot.induction_on
-- Module: Mathlib.Data.Real.Basic
Goal:
C : ℝ → Prop
h : ∀ (y : CauSeq ℚ abs), C (mk y)
a : CauSeq ℚ abs
⊢ C { cauchy := Quot.mk (⇑equiv : CauSeq ℚ abs → CauSeq ℚ abs → Prop) a }

Tactic:
h _

Premises used: CauSeq.Completion.mk, Real.mk
-- Module: Mathlib.Data.Real.Basic
Goal:
C : ℝ → Prop
h : ∀ (y : CauSeq ℚ abs), C (mk y)
a : CauSeq ℚ abs
⊢ C { cauchy := Quot.mk (⇑equiv : CauSeq ℚ abs → CauSeq ℚ abs → Prop) a }

Tactic:
exact h _
-- Module: Mathlib.Data.Real.Basic
Goal:
x a : ℝ
h : ∀ (y : CauSeq ℚ abs), mk y ≤ mk y
⊢ a ≤ a

Tactic:
induction a using Real.ind_mk
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
y : CauSeq ℚ abs
h h₁ : y ≤ y
⊢ mk y ≤ mk y

Tactic:
rw [mk_le]

Premises used: Real.mk_le
-- Module: Mathlib.Data.Real.Basic
Goal:
x a b c : ℝ
h : ∀ (y : CauSeq ℚ abs), mk y ≤ b → b ≤ c → mk y ≤ c
⊢ a ≤ b → b ≤ c → a ≤ c

Tactic:
induction a using Real.ind_mk
-- Module: Mathlib.Data.Real.Basic
Goal:
x b c : ℝ
y : CauSeq ℚ abs
h : ∀ (y_1 : CauSeq ℚ abs), mk y ≤ mk y_1 → mk y_1 ≤ c → mk y ≤ c
⊢ mk y ≤ b → b ≤ c → mk y ≤ c

Tactic:
induction b using Real.ind_mk
-- Module: Mathlib.Data.Real.Basic
Goal:
x c : ℝ
y y_1 : CauSeq ℚ abs
h : ∀ (y_2 : CauSeq ℚ abs), mk y ≤ mk y_1 → mk y_1 ≤ mk y_2 → mk y ≤ mk y_2
⊢ mk y ≤ mk y_1 → mk y_1 ≤ c → mk y ≤ c

Tactic:
induction c using Real.ind_mk
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
y y_1 y_2 : CauSeq ℚ abs
⊢ mk y ≤ mk y_1 → mk y_1 ≤ mk y_2 → mk y ≤ mk y_2

Tactic:
simpa using le_trans

Premises used: le_trans
-- Module: Mathlib.Data.Real.Basic
Goal:
x a b : ℝ
h : ∀ (y : CauSeq ℚ abs), mk y < b ↔ mk y ≤ b ∧ ¬b ≤ mk y
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
induction a using Real.ind_mk
-- Module: Mathlib.Data.Real.Basic
Goal:
x b : ℝ
y : CauSeq ℚ abs
h : ∀ (y_1 : CauSeq ℚ abs), mk y < mk y_1 ↔ mk y ≤ mk y_1 ∧ ¬mk y_1 ≤ mk y
⊢ mk y < b ↔ mk y ≤ b ∧ ¬b ≤ mk y

Tactic:
induction b using Real.ind_mk
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
y y_1 : CauSeq ℚ abs
⊢ mk y < mk y_1 ↔ mk y ≤ mk y_1 ∧ ¬mk y_1 ≤ mk y

Tactic:
simpa using lt_iff_le_not_ge

Premises used: lt_iff_le_not_ge
-- Module: Mathlib.Data.Real.Basic
Goal:
x a b : ℝ
h : ∀ (y : CauSeq ℚ abs), mk y ≤ b → b ≤ mk y → mk y = b
⊢ a ≤ b → b ≤ a → a = b

Tactic:
induction a using Real.ind_mk
-- Module: Mathlib.Data.Real.Basic
Goal:
x b : ℝ
y : CauSeq ℚ abs
h : ∀ (y_1 : CauSeq ℚ abs), mk y ≤ mk y_1 → mk y_1 ≤ mk y → mk y = mk y_1
⊢ mk y ≤ b → b ≤ mk y → mk y = b

Tactic:
induction b using Real.ind_mk
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
y y_1 : CauSeq ℚ abs
⊢ mk y ≤ mk y_1 → mk y_1 ≤ mk y → mk y = mk y_1

Tactic:
simpa [mk_eq] using CauSeq.le_antisymm

Premises used: CauSeq.le_antisymm, Real.mk_eq
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
⊢ Preorder ℝ

Tactic:
infer_instance
-- Module: Mathlib.Data.Real.Basic
Goal:
x y : ℚ
rw : LT.lt (α := CauSeq ℚ abs) (const abs x) (const abs y) ↔ x < y
⊢ LT.lt (α := ℝ) (↑x : ℝ) (↑y : ℝ) ↔ x < y

Tactic:
rw [← mk_const, ← mk_const, mk_lt]

Premises used: Real.mk_lt, Real.mk_const
-- Module: Mathlib.Data.Real.Basic
Goal:
x y : ℚ
⊢ LT.lt (α := CauSeq ℚ abs) (const abs x) (const abs y) ↔ x < y

Tactic:
const_lt

Premises used: CauSeq.const_lt
-- Module: Mathlib.Data.Real.Basic
Goal:
x y : ℚ
⊢ LT.lt (α := CauSeq ℚ abs) (const abs x) (const abs y) ↔ x < y

Tactic:
exact const_lt

Premises used: CauSeq.const_lt
-- Module: Mathlib.Data.Real.Basic
Goal:
⊢ LT.lt (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)

Tactic:
ratCast_lt.2 zero_lt_one

Premises used: Iff.mpr, Real.ratCast_lt, zero_lt_one
-- Module: Mathlib.Data.Real.Basic
Goal:
h : Eq (α := ℝ) 0 (↑0 : ℝ)
h₁ : Eq (α := ℝ) 1 (↑1 : ℝ)
⊢ LT.lt (α := ℝ) 0 1

Tactic:
convert! ratCast_lt.2 zero_lt_one

Premises used: Iff.mpr, Real.ratCast_lt, zero_lt_one
-- Module: Mathlib.Data.Real.Basic
Goal:
⊢ Eq (α := ℝ) 0 (↑0 : ℝ)

Tactic:
simp [← ofCauchy_ratCast, ofCauchy_one, ofCauchy_zero]

Premises used: Real.ofCauchy_zero, Real.ofCauchy_ratCast, Real.ofCauchy_one
-- Module: Mathlib.Data.Real.Basic
Goal:
⊢ Eq (α := ℝ) 1 (↑1 : ℝ)

Tactic:
simp [← ofCauchy_ratCast, ofCauchy_one, ofCauchy_zero]

Premises used: Real.ofCauchy_zero, Real.ofCauchy_ratCast, Real.ofCauchy_one
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
simp : ∀ (a b : ℝ), a = b ∨ a < b → ∀ (c : ℝ), a + c = b + c ∨ a + c < b + c
⊢ ∀ (a b : ℝ), a ≤ b → ∀ (c : ℝ), a + c ≤ b + c

Tactic:
simp only [le_iff_eq_or_lt]

Premises used: le_iff_eq_or_lt
-- Module: Mathlib.Data.Real.Basic
Goal:
x a : ℝ
⊢ ∀ (c : ℝ), a + c = a + c ∨ a + c < a + c

Tactic:
simp only [lt_self_iff_false, or_false, forall_const]

Premises used: lt_self_iff_false, forall_const, or_false
-- Module: Mathlib.Data.Real.Basic
Goal:
x a b : ℝ
h : a < b
⊢ ∀ (c : ℝ), a + c = b + c ∨ a + c < b + c

Tactic:
fun c => Or.inr ?_

Premises used: Or.inr
-- Module: Mathlib.Data.Real.Basic
Goal:
x a b : ℝ
h : a < b
inr : ∀ (c : ℝ), a + c < b + c
⊢ ∀ (c : ℝ), a + c = b + c ∨ a + c < b + c

Tactic:
refine fun c => Or.inr ?_

Premises used: Or.inr
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
a b : CauSeq ℚ abs
h : mk a < mk b
c : CauSeq ℚ abs
inr : a < b → a + c < b + c
⊢ mk a + mk c < mk b + mk c

Tactic:
simp only [mk_lt, ← mk_add] at *

Premises used: Real.mk_lt, Real.mk_add
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
a b c : CauSeq ℚ abs
h : a < b
⊢ (b - a).Pos

Tactic:
change Pos _ at *

Premises used: CauSeq.Pos
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
a b c : CauSeq ℚ abs
h : (b - a).Pos
inr inr₁ inr₂ inr₃ : (b - a).Pos
⊢ (b + c - (a + c)).Pos

Tactic:
rwa [add_sub_add_right_eq_sub]

Premises used: add_sub_add_right_eq_sub
-- Module: Mathlib.Data.Real.Basic
Goal:
x c : ℝ
a b : CauSeq ℚ abs
h : mk a < mk b
inr : ∀ (c : CauSeq ℚ abs), mk a + mk c < mk b + mk c
⊢ mk a + c < mk b + c

Tactic:
induction c using Real.ind_mk with | _ c =>
      simp only [mk_lt, ← mk_add] at *
      change Pos _ at *
      rwa [add_sub_add_right_eq_sub]

Premises used: CauSeq.Pos, Real.mk_lt, Real.mk_add, add_sub_add_right_eq_sub
-- Module: Mathlib.Data.Real.Basic
Goal:
x b c : ℝ
a : CauSeq ℚ abs
h : mk a < b
inr : ∀ (b : CauSeq ℚ abs), mk a < mk b → mk a + c < mk b + c
⊢ mk a + c < b + c

Tactic:
induction b using Real.ind_mk with | _ b =>
      induction c using Real.ind_mk with | _ c =>
      simp only [mk_lt, ← mk_add] at *
      change Pos _ at *
      rwa [add_sub_add_right_eq_sub]

Premises used: CauSeq.Pos, Real.mk_lt, Real.mk_add, add_sub_add_right_eq_sub
-- Module: Mathlib.Data.Real.Basic
Goal:
x a b : ℝ
h : a < b
c : ℝ
inr : ∀ (a : CauSeq ℚ abs), mk a < b → mk a + c < b + c
⊢ a + c < b + c

Tactic:
induction a using Real.ind_mk with | _ a =>
      induction b using Real.ind_mk with | _ b =>
      induction c using Real.ind_mk with | _ c =>
      simp only [mk_lt, ← mk_add] at *
      change Pos _ at *
      rwa [add_sub_add_right_eq_sub]

Premises used: CauSeq.Pos, Real.mk_lt, Real.mk_add, add_sub_add_right_eq_sub
-- Module: Mathlib.Data.Real.Basic
Goal:
x a b : ℝ
h : ∀ (y : CauSeq ℚ abs), 0 < mk y → 0 < b → 0 < mk y * b
⊢ 0 < a → 0 < b → 0 < a * b

Tactic:
induction a using Real.ind_mk
-- Module: Mathlib.Data.Real.Basic
Goal:
x b : ℝ
y : CauSeq ℚ abs
h : ∀ (y_1 : CauSeq ℚ abs), 0 < mk y → 0 < mk y_1 → 0 < mk y * mk y_1
⊢ 0 < mk y → 0 < b → 0 < mk y * b

Tactic:
induction b using Real.ind_mk
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
y y_1 : CauSeq ℚ abs
⊢ 0 < mk y → 0 < mk y_1 → 0 < mk y * mk y_1

Tactic:
simpa only [mk_lt, mk_pos, ← mk_mul] using CauSeq.mul_pos

Premises used: CauSeq.mul_pos, Real.mk_lt, Real.mk_mul, Real.mk_pos
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
⊢ IsOrderedRing ℝ

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
⊢ IsOrderedCancelAddMonoid ℝ

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Data.Real.Basic
Goal:
a b : CauSeq ℚ abs
rw :
  { cauchy := ⟦a ⊔ b⟧ : ℝ } =
    match (motive := ℝ → ℝ → ℝ) { cauchy := ⟦a⟧ }, { cauchy := ⟦b⟧ } with
    | { cauchy := x }, { cauchy := y } => { cauchy := Quotient.map₂ (fun (x1 x2 : CauSeq ℚ abs) ↦ x1 ⊔ x2) ⋯ x y }
⊢ { cauchy := ⟦a ⊔ b⟧ : ℝ } = { cauchy := ⟦a⟧ }.sup { cauchy := ⟦b⟧ }

Tactic:
rw [sup_def]

Premises used: _private.0.Real.sup_def
-- Module: Mathlib.Data.Real.Basic
Goal:
a b : CauSeq ℚ abs
⊢ { cauchy := ⟦a ⊔ b⟧ : ℝ } =
    match (motive := ℝ → ℝ → ℝ) { cauchy := ⟦a⟧ }, { cauchy := ⟦b⟧ } with
    | { cauchy := x }, { cauchy := y } => { cauchy := Quotient.map₂ (fun (x1 x2 : CauSeq ℚ abs) ↦ x1 ⊔ x2) ⋯ x y }

Tactic:
rfl
-- Module: Mathlib.Data.Real.Basic
Goal:
a b : CauSeq ℚ abs
⊢ mk (a ⊔ b) = mk a ⊔ mk b

Tactic:
ofCauchy_sup _ _

Premises used: Real.ofCauchy_sup, CauSeq.Completion.mk, Real.mk
-- Module: Mathlib.Data.Real.Basic
Goal:
a b : CauSeq ℚ abs
rw :
  { cauchy := ⟦a ⊓ b⟧ : ℝ } =
    match (motive := ℝ → ℝ → ℝ) { cauchy := ⟦a⟧ }, { cauchy := ⟦b⟧ } with
    | { cauchy := x }, { cauchy := y } => { cauchy := Quotient.map₂ (fun (x1 x2 : CauSeq ℚ abs) ↦ x1 ⊓ x2) ⋯ x y }
⊢ { cauchy := ⟦a ⊓ b⟧ : ℝ } = { cauchy := ⟦a⟧ }.inf { cauchy := ⟦b⟧ }

Tactic:
rw [inf_def]

Premises used: _private.0.Real.inf_def
-- Module: Mathlib.Data.Real.Basic
Goal:
a b : CauSeq ℚ abs
⊢ { cauchy := ⟦a ⊓ b⟧ : ℝ } =
    match (motive := ℝ → ℝ → ℝ) { cauchy := ⟦a⟧ }, { cauchy := ⟦b⟧ } with
    | { cauchy := x }, { cauchy := y } => { cauchy := Quotient.map₂ (fun (x1 x2 : CauSeq ℚ abs) ↦ x1 ⊓ x2) ⋯ x y }

Tactic:
rfl
-- Module: Mathlib.Data.Real.Basic
Goal:
a b : CauSeq ℚ abs
⊢ mk (a ⊓ b) = mk a ⊓ mk b

Tactic:
ofCauchy_inf _ _

Premises used: CauSeq.Completion.mk, Real.mk, Real.ofCauchy_inf
-- Module: Mathlib.Data.Real.Basic
Goal:
x a b : ℝ
h : ∀ (y : CauSeq ℚ abs), mk y ≤ mk y ⊔ b
⊢ a ≤ a ⊔ b

Tactic:
induction a using Real.ind_mk
-- Module: Mathlib.Data.Real.Basic
Goal:
x b : ℝ
y : CauSeq ℚ abs
h : ∀ (y_1 : CauSeq ℚ abs), mk y ≤ mk y ⊔ mk y_1
⊢ mk y ≤ mk y ⊔ b

Tactic:
induction b using Real.ind_mk
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
y y_1 : CauSeq ℚ abs
h : y ≤ y ⊔ y_1
⊢ mk y ≤ mk y ⊔ mk y_1

Tactic:
rw [← mk_sup, mk_le]

Premises used: Real.mk_sup, Real.mk_le
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
y y_1 : CauSeq ℚ abs
⊢ y ≤ y ⊔ y_1

Tactic:
CauSeq.le_sup_left

Premises used: CauSeq.le_sup_left
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
y y_1 : CauSeq ℚ abs
⊢ y ≤ y ⊔ y_1

Tactic:
exact CauSeq.le_sup_left

Premises used: CauSeq.le_sup_left
-- Module: Mathlib.Data.Real.Basic
Goal:
x a b : ℝ
h : ∀ (y : CauSeq ℚ abs), b ≤ mk y ⊔ b
⊢ b ≤ a ⊔ b

Tactic:
induction a using Real.ind_mk
-- Module: Mathlib.Data.Real.Basic
Goal:
x b : ℝ
y : CauSeq ℚ abs
h : ∀ (y_1 : CauSeq ℚ abs), mk y_1 ≤ mk y ⊔ mk y_1
⊢ b ≤ mk y ⊔ b

Tactic:
induction b using Real.ind_mk
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
y y_1 : CauSeq ℚ abs
h : y_1 ≤ y ⊔ y_1
⊢ mk y_1 ≤ mk y ⊔ mk y_1

Tactic:
rw [← mk_sup, mk_le]

Premises used: Real.mk_sup, Real.mk_le
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
y y_1 : CauSeq ℚ abs
⊢ y_1 ≤ y ⊔ y_1

Tactic:
CauSeq.le_sup_right

Premises used: CauSeq.le_sup_right
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
y y_1 : CauSeq ℚ abs
⊢ y_1 ≤ y ⊔ y_1

Tactic:
exact CauSeq.le_sup_right

Premises used: CauSeq.le_sup_right
-- Module: Mathlib.Data.Real.Basic
Goal:
x a b c : ℝ
h : ∀ (y : CauSeq ℚ abs), mk y ≤ c → b ≤ c → mk y ⊔ b ≤ c
⊢ a ≤ c → b ≤ c → a ⊔ b ≤ c

Tactic:
induction a using Real.ind_mk
-- Module: Mathlib.Data.Real.Basic
Goal:
x b c : ℝ
y : CauSeq ℚ abs
h : ∀ (y_1 : CauSeq ℚ abs), mk y ≤ c → mk y_1 ≤ c → mk y ⊔ mk y_1 ≤ c
⊢ mk y ≤ c → b ≤ c → mk y ⊔ b ≤ c

Tactic:
induction b using Real.ind_mk
-- Module: Mathlib.Data.Real.Basic
Goal:
x c : ℝ
y y_1 : CauSeq ℚ abs
h : ∀ (y_2 : CauSeq ℚ abs), mk y ≤ mk y_2 → mk y_1 ≤ mk y_2 → mk y ⊔ mk y_1 ≤ mk y_2
⊢ mk y ≤ c → mk y_1 ≤ c → mk y ⊔ mk y_1 ≤ c

Tactic:
induction c using Real.ind_mk
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
y y_1 y_2 : CauSeq ℚ abs
h : y ≤ y_2 → y_1 ≤ y_2 → y ⊔ y_1 ≤ y_2
⊢ mk y ≤ mk y_2 → mk y_1 ≤ mk y_2 → mk y ⊔ mk y_1 ≤ mk y_2

Tactic:
simp_rw [← mk_sup, mk_le]

Premises used: Real.mk_sup, Real.mk_le
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
y y_1 y_2 : CauSeq ℚ abs
⊢ y ≤ y_2 → y_1 ≤ y_2 → y ⊔ y_1 ≤ y_2

Tactic:
CauSeq.sup_le

Premises used: CauSeq.sup_le
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
y y_1 y_2 : CauSeq ℚ abs
⊢ y ≤ y_2 → y_1 ≤ y_2 → y ⊔ y_1 ≤ y_2

Tactic:
exact CauSeq.sup_le

Premises used: CauSeq.sup_le
-- Module: Mathlib.Data.Real.Basic
Goal:
x a b : ℝ
h : ∀ (y : CauSeq ℚ abs), mk y ⊓ b ≤ mk y
⊢ a ⊓ b ≤ a

Tactic:
induction a using Real.ind_mk
-- Module: Mathlib.Data.Real.Basic
Goal:
x b : ℝ
y : CauSeq ℚ abs
h : ∀ (y_1 : CauSeq ℚ abs), mk y ⊓ mk y_1 ≤ mk y
⊢ mk y ⊓ b ≤ mk y

Tactic:
induction b using Real.ind_mk
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
y y_1 : CauSeq ℚ abs
h : y ⊓ y_1 ≤ y
⊢ mk y ⊓ mk y_1 ≤ mk y

Tactic:
rw [← mk_inf, mk_le]

Premises used: Real.mk_inf, Real.mk_le
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
y y_1 : CauSeq ℚ abs
⊢ y ⊓ y_1 ≤ y

Tactic:
CauSeq.inf_le_left

Premises used: CauSeq.inf_le_left
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
y y_1 : CauSeq ℚ abs
⊢ y ⊓ y_1 ≤ y

Tactic:
exact CauSeq.inf_le_left

Premises used: CauSeq.inf_le_left
-- Module: Mathlib.Data.Real.Basic
Goal:
x a b : ℝ
h : ∀ (y : CauSeq ℚ abs), mk y ⊓ b ≤ b
⊢ a ⊓ b ≤ b

Tactic:
induction a using Real.ind_mk
-- Module: Mathlib.Data.Real.Basic
Goal:
x b : ℝ
y : CauSeq ℚ abs
h : ∀ (y_1 : CauSeq ℚ abs), mk y ⊓ mk y_1 ≤ mk y_1
⊢ mk y ⊓ b ≤ b

Tactic:
induction b using Real.ind_mk
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
y y_1 : CauSeq ℚ abs
h : y ⊓ y_1 ≤ y_1
⊢ mk y ⊓ mk y_1 ≤ mk y_1

Tactic:
rw [← mk_inf, mk_le]

Premises used: Real.mk_inf, Real.mk_le
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
y y_1 : CauSeq ℚ abs
⊢ y ⊓ y_1 ≤ y_1

Tactic:
CauSeq.inf_le_right

Premises used: CauSeq.inf_le_right
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
y y_1 : CauSeq ℚ abs
⊢ y ⊓ y_1 ≤ y_1

Tactic:
exact CauSeq.inf_le_right

Premises used: CauSeq.inf_le_right
-- Module: Mathlib.Data.Real.Basic
Goal:
x a b c : ℝ
h : ∀ (y : CauSeq ℚ abs), mk y ≤ b → mk y ≤ c → mk y ≤ b ⊓ c
⊢ a ≤ b → a ≤ c → a ≤ b ⊓ c

Tactic:
induction a using Real.ind_mk
-- Module: Mathlib.Data.Real.Basic
Goal:
x b c : ℝ
y : CauSeq ℚ abs
h : ∀ (y_1 : CauSeq ℚ abs), mk y ≤ mk y_1 → mk y ≤ c → mk y ≤ mk y_1 ⊓ c
⊢ mk y ≤ b → mk y ≤ c → mk y ≤ b ⊓ c

Tactic:
induction b using Real.ind_mk
-- Module: Mathlib.Data.Real.Basic
Goal:
x c : ℝ
y y_1 : CauSeq ℚ abs
h : ∀ (y_2 : CauSeq ℚ abs), mk y ≤ mk y_1 → mk y ≤ mk y_2 → mk y ≤ mk y_1 ⊓ mk y_2
⊢ mk y ≤ mk y_1 → mk y ≤ c → mk y ≤ mk y_1 ⊓ c

Tactic:
induction c using Real.ind_mk
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
y y_1 y_2 : CauSeq ℚ abs
h : y ≤ y_1 → y ≤ y_2 → y ≤ y_1 ⊓ y_2
⊢ mk y ≤ mk y_1 → mk y ≤ mk y_2 → mk y ≤ mk y_1 ⊓ mk y_2

Tactic:
simp_rw [← mk_inf, mk_le]

Premises used: Real.mk_inf, Real.mk_le
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
y y_1 y_2 : CauSeq ℚ abs
⊢ y ≤ y_1 → y ≤ y_2 → y ≤ y_1 ⊓ y_2

Tactic:
CauSeq.le_inf

Premises used: CauSeq.le_inf
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
y y_1 y_2 : CauSeq ℚ abs
⊢ y ≤ y_1 → y ≤ y_2 → y ≤ y_1 ⊓ y_2

Tactic:
exact CauSeq.le_inf

Premises used: CauSeq.le_inf
-- Module: Mathlib.Data.Real.Basic
Goal:
x a b c : ℝ
h : ∀ (y : CauSeq ℚ abs), (mk y ⊔ b) ⊓ (mk y ⊔ c) ≤ mk y ⊔ b ⊓ c
⊢ (a ⊔ b) ⊓ (a ⊔ c) ≤ a ⊔ b ⊓ c

Tactic:
induction a using Real.ind_mk
-- Module: Mathlib.Data.Real.Basic
Goal:
x b c : ℝ
y : CauSeq ℚ abs
h : ∀ (y_1 : CauSeq ℚ abs), (mk y ⊔ mk y_1) ⊓ (mk y ⊔ c) ≤ mk y ⊔ mk y_1 ⊓ c
⊢ (mk y ⊔ b) ⊓ (mk y ⊔ c) ≤ mk y ⊔ b ⊓ c

Tactic:
induction b using Real.ind_mk
-- Module: Mathlib.Data.Real.Basic
Goal:
x c : ℝ
y y_1 : CauSeq ℚ abs
h : ∀ (y_2 : CauSeq ℚ abs), (mk y ⊔ mk y_1) ⊓ (mk y ⊔ mk y_2) ≤ mk y ⊔ mk y_1 ⊓ mk y_2
⊢ (mk y ⊔ mk y_1) ⊓ (mk y ⊔ c) ≤ mk y ⊔ mk y_1 ⊓ c

Tactic:
induction c using Real.ind_mk
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
y y_1 y_2 : CauSeq ℚ abs
h : (mk y ⊔ mk y_1) ⊓ (mk y ⊔ mk y_2) = mk y ⊔ mk y_1 ⊓ mk y_2
⊢ (mk y ⊔ mk y_1) ⊓ (mk y ⊔ mk y_2) ≤ mk y ⊔ mk y_1 ⊓ mk y_2

Tactic:
apply Eq.le

Premises used: Eq.le
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
y y_1 y_2 : CauSeq ℚ abs
h : mk ((y ⊔ y_1) ⊓ (y ⊔ y_2)) = mk (y ⊔ y_1 ⊓ y_2)
⊢ (mk y ⊔ mk y_1) ⊓ (mk y ⊔ mk y_2) = mk y ⊔ mk y_1 ⊓ mk y_2

Tactic:
simp only [← mk_sup, ← mk_inf]

Premises used: Real.mk_inf, Real.mk_sup
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
y y_1 y_2 : CauSeq ℚ abs
⊢ mk ((y ⊔ y_1) ⊓ (y ⊔ y_2)) = mk (y ⊔ y_1 ⊓ y_2)

Tactic:
congr_arg mk (CauSeq.sup_inf_distrib_left ..).symm

Premises used: congr_arg, Eq.symm, Real.mk, CauSeq.sup_inf_distrib_left
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
y y_1 y_2 : CauSeq ℚ abs
⊢ mk ((y ⊔ y_1) ⊓ (y ⊔ y_2)) = mk (y ⊔ y_1 ⊓ y_2)

Tactic:
exact congr_arg mk (CauSeq.sup_inf_distrib_left ..).symm

Premises used: congr_arg, Eq.symm, Real.mk, CauSeq.sup_inf_distrib_left
-- Module: Mathlib.Data.Real.Basic
Goal:
x a b : ℝ
h : ∀ (y : CauSeq ℚ abs), mk y ≤ b ∨ b ≤ mk y
⊢ a ≤ b ∨ b ≤ a

Tactic:
induction a using Real.ind_mk
-- Module: Mathlib.Data.Real.Basic
Goal:
x b : ℝ
y : CauSeq ℚ abs
h : ∀ (y_1 : CauSeq ℚ abs), mk y ≤ mk y_1 ∨ mk y_1 ≤ mk y
⊢ mk y ≤ b ∨ b ≤ mk y

Tactic:
induction b using Real.ind_mk
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
y y_1 : CauSeq ℚ abs
⊢ mk y ≤ mk y_1 ∨ mk y_1 ≤ mk y

Tactic:
simpa using CauSeq.le_total ..

Premises used: CauSeq.le_total
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
⊢ IsDomain ℝ

Tactic:
IsStrictOrderedRing.isDomain

Premises used: IsStrictOrderedRing.isDomain
-- Module: Mathlib.Data.Real.Basic
Goal:
f g : Cauchy (α := ℚ) abs
simp_rw : { cauchy := f * g⁻¹ : ℝ } = { cauchy := f : ℝ } * { cauchy := g : ℝ }⁻¹
simp_rw₁ : { cauchy := f : ℝ } * { cauchy := g⁻¹ : ℝ } = { cauchy := f : ℝ } * { cauchy := g : ℝ }⁻¹
⊢ { cauchy := f / g : ℝ } = { cauchy := f : ℝ } / { cauchy := g : ℝ }

Tactic:
simp_rw [div_eq_mul_inv, ofCauchy_mul, ofCauchy_inv]

Premises used: Real.ofCauchy_mul, div_eq_mul_inv, Real.ofCauchy_inv
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
a : Cauchy (α := ℚ) abs
h : { cauchy := a : ℝ } ≠ 0
rw : { cauchy := a : ℝ }⁻¹ * { cauchy := a : ℝ } = 1
⊢ { cauchy := a : ℝ } * { cauchy := a : ℝ }⁻¹ = 1

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
a : Cauchy (α := ℚ) abs
h : { cauchy := a : ℝ } ≠ 0
simp : ∀ (h : ¬a = 0), a⁻¹ * a = 1
⊢ { cauchy := a : ℝ }⁻¹ * { cauchy := a : ℝ } = 1

Tactic:
simp only [← ofCauchy_inv, ← ofCauchy_mul, ← ofCauchy_one, ← ofCauchy_zero,
      Ne, ofCauchy.injEq] at *

Premises used: Real.ofCauchy_zero, Real.ofCauchy_mul, Ne, Real.ofCauchy_inv, Real.ofCauchy_one, Real.ofCauchy.injEq
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
a : Cauchy (α := ℚ) abs
h : ¬a = 0
⊢ a⁻¹ * a = 1

Tactic:
CauSeq.Completion.inv_mul_cancel h

Premises used: CauSeq.Completion.inv_mul_cancel
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
a : Cauchy (α := ℚ) abs
h : ¬a = 0
⊢ a⁻¹ * a = 1

Tactic:
exact CauSeq.Completion.inv_mul_cancel h

Premises used: CauSeq.Completion.inv_mul_cancel
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
⊢ Eq (α := ℝ) 0⁻¹ 0

Tactic:
simp [← ofCauchy_zero, ← ofCauchy_inv]

Premises used: Real.ofCauchy_zero, Real.ofCauchy_inv
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
q : ℚ≥0
rw : { cauchy := (↑q : Cauchy abs) : ℝ } = HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ)
rw₁ :
  { cauchy := HDiv.hDiv (α := Cauchy (α := ℚ) abs) (↑q.num : Cauchy abs) (↑q.den : Cauchy abs) : ℝ } =
    HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ)
rw₂ :
  { cauchy := (↑q.num : Cauchy abs) : ℝ } / { cauchy := (↑q.den : Cauchy abs) : ℝ } =
    HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ)
rw₃ : (↑q.num : ℝ) / { cauchy := (↑q.den : Cauchy abs) : ℝ } = HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ)
rw₄ rw₅ : HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ) = HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ)
⊢ (↑q : ℝ) = HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ)

Tactic:
rw [← ofCauchy_nnratCast, NNRat.cast_def, ofCauchy_div, ofCauchy_natCast, ofCauchy_natCast]

Premises used: NNRat.cast_def, Real.ofCauchy_nnratCast, Real.ofCauchy_natCast, Real.ofCauchy_div
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
q : ℚ
rw : { cauchy := (↑q : Cauchy abs) : ℝ } = HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ)
rw₁ :
  { cauchy := HDiv.hDiv (α := Cauchy (α := ℚ) abs) (↑q.num : Cauchy abs) (↑q.den : Cauchy abs) : ℝ } =
    HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ)
rw₂ :
  { cauchy := (↑q.num : Cauchy abs) : ℝ } / { cauchy := (↑q.den : Cauchy abs) : ℝ } =
    HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ)
rw₃ : { cauchy := (↑q.num : Cauchy abs) : ℝ } / (↑q.den : ℝ) = HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ)
rw₄ rw₅ : HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ) = HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ)
⊢ (↑q : ℝ) = HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ)

Tactic:
rw [← ofCauchy_ratCast, Rat.cast_def, ofCauchy_div, ofCauchy_natCast, ofCauchy_intCast]

Premises used: Real.ofCauchy_natCast, Real.ofCauchy_ratCast, Rat.cast_def, Real.ofCauchy_intCast, Real.ofCauchy_div
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
⊢ DivisionRing ℝ

Tactic:
infer_instance
-- Module: Mathlib.Data.Real.Basic
Goal:
x a b : ℝ
⊢ Decidable (a < b)

Tactic:
infer_instance
-- Module: Mathlib.Data.Real.Basic
Goal:
x a b : ℝ
⊢ Decidable (a ≤ b)

Tactic:
infer_instance
-- Module: Mathlib.Data.Real.Basic
Goal:
x a b : ℝ
⊢ Decidable (a = b)

Tactic:
infer_instance
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
f : CauSeq ℚ abs
h : ∃ (i : ℕ), ∀ j ≥ i, x ≤ (↑((↑f : ℕ → ℚ) j) : ℝ)
h₁ : ∀ (y : CauSeq ℚ abs) (h : ∃ (i : ℕ), ∀ j ≥ i, mk y ≤ (↑((↑f : ℕ → ℚ) j) : ℝ)), mk y ≤ mk f
⊢ x ≤ mk f

Tactic:
induction x using Real.ind_mk
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
f y : CauSeq ℚ abs
h : ∃ (i : ℕ), ∀ j ≥ i, mk y ≤ (↑((↑f : ℕ → ℚ) j) : ℝ)
h₁ : ¬mk f < mk y
⊢ mk y ≤ mk f

Tactic:
apply le_of_not_gt

Premises used: le_of_not_gt
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
f y : CauSeq ℚ abs
h : ∃ (i : ℕ), ∀ j ≥ i, mk y ≤ (↑((↑f : ℕ → ℚ) j) : ℝ)
h₁ : ¬f < y
⊢ ¬mk f < mk y

Tactic:
rw [mk_lt]

Premises used: Real.mk_lt
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
f y : CauSeq ℚ abs
h : ∃ (i : ℕ), ∀ j ≥ i, mk y ≤ (↑((↑f : ℕ → ℚ) j) : ℝ)
K : ℚ
K0 : K > 0
hK : ∃ (i : ℕ), ∀ j ≥ i, K ≤ (↑(y - f) : ℕ → ℚ) j
h₁ :
  ∀ (i : ℕ)
    (H :
      ∀ j ≥ i,
        mk y ≤ (↑((↑f : ℕ → ℚ) j) : ℝ) ∧ K ≤ (↑(y - f) : ℕ → ℚ) j ∧ ∀ k ≥ j, |(↑f : ℕ → ℚ) k - (↑f : ℕ → ℚ) j| < K / 2),
    False
⊢ False

Tactic:
obtain ⟨i, H⟩ := exists_forall_ge_and h (exists_forall_ge_and hK (f.cauchy₃ <| half_pos K0))

Premises used: half_pos, exists_forall_ge_and, CauSeq.cauchy₃
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
f y : CauSeq ℚ abs
h : ∃ (i : ℕ), ∀ j ≥ i, mk y ≤ (↑((↑f : ℕ → ℚ) j) : ℝ)
K : ℚ
K0 : K > 0
hK : ∃ (i : ℕ), ∀ j ≥ i, K ≤ (↑(y - f) : ℕ → ℚ) j
i : ℕ
H :
  ∀ j ≥ i,
    mk y ≤ (↑((↑f : ℕ → ℚ) j) : ℝ) ∧ K ≤ (↑(y - f) : ℕ → ℚ) j ∧ ∀ k ≥ j, |(↑f : ℕ → ℚ) k - (↑f : ℕ → ℚ) j| < K / 2
h₁ : (↑((↑f : ℕ → ℚ) i) : ℝ) < mk y
⊢ False

Tactic:
apply not_lt_of_ge (H _ le_rfl).1

Premises used: le_rfl, And.left, not_lt_of_ge