awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x a b c : ℝ
⊢ a + b + c = a + (b + c)
have a₁ : (a + b + c).cauchy = (a + (b + c)).cauchy
Tactic: apply ext_cauchy
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x a : ℝ
⊢ 0 + a = a
have a₁ : (0 + a).cauchy = a.cauchy
Tactic: apply ext_cauchy
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x a : ℝ
⊢ a + 0 = a
have a₁ : (a + 0).cauchy = a.cauchy
Tactic: apply ext_cauchy
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x a b : ℝ
⊢ a + b = b + a
have a₁ : (a + b).cauchy = (b + a).cauchy
Tactic: apply ext_cauchy
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x a b c : ℝ
⊢ a * b * c = a * (b * c)
have a₁ : (a * b * c).cauchy = (a * (b * c)).cauchy
Tactic: apply ext_cauchy
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x a : ℝ
⊢ 1 * a = a
have a₁ : (1 * a).cauchy = a.cauchy
Tactic: apply ext_cauchy
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x a : ℝ
⊢ a * 1 = a
have a₁ : (a * 1).cauchy = a.cauchy
Tactic: apply ext_cauchy
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x a : ℝ
⊢ 0 * a = 0
have a₁ : (0 * a).cauchy = cauchy 0
Tactic: apply ext_cauchy
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x a : ℝ
⊢ a * 0 = 0
have a₁ : (a * 0).cauchy = cauchy 0
Tactic: apply ext_cauchy
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x a b c : ℝ
⊢ a * (b + c) = a * b + a * c
have a₁ : (a * (b + c)).cauchy = (a * b + a * c).cauchy
Tactic: apply ext_cauchy
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x a b c : ℝ
⊢ (a + b) * c = a * c + b * c
have a₁ : ((a + b) * c).cauchy = (a * c + b * c).cauchy
Tactic: apply ext_cauchy
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x : ℝ
⊢ { cauchy := (↑0 : Cauchy abs) : ℝ } = 0
have a : { cauchy := (↑0 : Cauchy abs) : ℝ }.cauchy = cauchy 0
Tactic: apply ext_cauchy
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x : ℝ
n : ℕ
⊢ { cauchy := (↑(n + 1) : Cauchy abs) : ℝ } = { cauchy := (↑n : Cauchy abs) : ℝ } + 1
have a : { cauchy := (↑(n + 1) : Cauchy abs) : ℝ }.cauchy = ({ cauchy := (↑n : Cauchy abs) : ℝ } + 1).cauchy
Tactic: apply ext_cauchy
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x a : ℝ
⊢ -a + a = 0
have a₁ : (-a + a).cauchy = cauchy 0
Tactic: apply ext_cauchy
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x : ℝ
z : ℕ
⊢ { cauchy := (↑(Int.negSucc z) : Cauchy abs) : ℝ } = -(↑(z + 1) : ℝ)
have a : { cauchy := (↑(Int.negSucc z) : Cauchy abs) : ℝ }.cauchy = cauchy (-(↑(z + 1) : ℝ))
Tactic: apply ext_cauchy
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x a b : ℝ
⊢ a * b = b * a
have a₁ : (a * b).cauchy = (b * a).cauchy
Tactic: apply ext_cauchy
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
f g : CauSeq ℚ abs
⊢ { cauchy := ⟦f⟧ }.lt { cauchy := ⟦g⟧ } ↔ f < g
have rw : (match (motive := ℝ → ℝ → Prop) { cauchy := ⟦f⟧ }, { cauchy := ⟦g⟧ } with
  | { cauchy := x }, { cauchy := y } =>
    Quotient.liftOn₂ x y (fun (x1 x2 : CauSeq ℚ abs) ↦ x1 < x2) definition._proof_1✝) ↔
  f < g
Tactic: rw [lt_def]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
⊢ mk 0 = 0
have rw : mk 0 = { cauchy := 0 }
Tactic: rw [← ofCauchy_zero]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
⊢ mk 1 = 1
have rw : mk 1 = { cauchy := 1 }
Tactic: rw [← ofCauchy_one]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
f : CauSeq ℚ abs
⊢ 0 < mk f ↔ f.Pos
have rw : 0 < f ↔ f.Pos
Tactic: rw [← mk_zero, mk_lt]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
f g : CauSeq ℚ abs
⊢ mk f ≤ mk g ↔ f ≤ g
have simp : f < g ∨ f ≈ g ↔ f ≤ g
Tactic: simp only [le_def', mk_lt, mk_eq]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
C : ℝ → Prop
x : ℝ
h : ∀ (y : CauSeq ℚ abs), C (mk y)
⊢ C x
have obtain : ∀ (x : Cauchy (α := ℚ) abs), C { cauchy := x }
Tactic: obtain ⟨x⟩ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
C : ℝ → Prop
h : ∀ (y : CauSeq ℚ abs), C (mk y)
x : Cauchy (α := ℚ) abs
⊢ C { cauchy := x }
have h₁ : ∀ (a : CauSeq ℚ abs), C { cauchy := Quot.mk (⇑equiv : CauSeq ℚ abs → CauSeq ℚ abs → Prop) a }
Tactic: induction x using Quot.induction_on
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x a : ℝ
⊢ a ≤ a
have h : ∀ (y : CauSeq ℚ abs), mk y ≤ mk y
Tactic: induction a using Real.ind_mk
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x : ℝ
y : CauSeq ℚ abs
⊢ mk y ≤ mk y
have h : y ≤ y
Tactic: rw [mk_le]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x a b c : ℝ
⊢ a ≤ b → b ≤ c → a ≤ c
have h : ∀ (y : CauSeq ℚ abs), mk y ≤ b → b ≤ c → mk y ≤ c
Tactic: induction a using Real.ind_mk
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x b c : ℝ
y : CauSeq ℚ abs
⊢ mk y ≤ b → b ≤ c → mk y ≤ c
have h : ∀ (y_1 : CauSeq ℚ abs), mk y ≤ mk y_1 → mk y_1 ≤ c → mk y ≤ c
Tactic: induction b using Real.ind_mk
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x c : ℝ
y y_1 : CauSeq ℚ abs
⊢ mk y ≤ mk y_1 → mk y_1 ≤ c → mk y ≤ c
have h : ∀ (y_2 : CauSeq ℚ abs), mk y ≤ mk y_1 → mk y_1 ≤ mk y_2 → mk y ≤ mk y_2
Tactic: induction c using Real.ind_mk
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x a b : ℝ
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a
have h : ∀ (y : CauSeq ℚ abs), mk y < b ↔ mk y ≤ b ∧ ¬b ≤ mk y
Tactic: induction a using Real.ind_mk
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x b : ℝ
y : CauSeq ℚ abs
⊢ mk y < b ↔ mk y ≤ b ∧ ¬b ≤ mk y
have h : ∀ (y_1 : CauSeq ℚ abs), mk y < mk y_1 ↔ mk y ≤ mk y_1 ∧ ¬mk y_1 ≤ mk y
Tactic: induction b using Real.ind_mk
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x a b : ℝ
⊢ a ≤ b → b ≤ a → a = b
have h : ∀ (y : CauSeq ℚ abs), mk y ≤ b → b ≤ mk y → mk y = b
Tactic: induction a using Real.ind_mk
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x b : ℝ
y : CauSeq ℚ abs
⊢ mk y ≤ b → b ≤ mk y → mk y = b
have h : ∀ (y_1 : CauSeq ℚ abs), mk y ≤ mk y_1 → mk y_1 ≤ mk y → mk y = mk y_1
Tactic: induction b using Real.ind_mk
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x y : ℚ
⊢ LT.lt (α := ℝ) (↑x : ℝ) (↑y : ℝ) ↔ x < y
have rw : LT.lt (α := CauSeq ℚ abs) (const abs x) (const abs y) ↔ x < y
Tactic: rw [← mk_const, ← mk_const, mk_lt]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
⊢ LT.lt (α := ℝ) 0 1
have h : Eq (α := ℝ) 0 (↑0 : ℝ)
Tactic: convert! ratCast_lt.2 zero_lt_one
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
h : Eq (α := ℝ) 0 (↑0 : ℝ)
⊢ LT.lt (α := ℝ) 0 1
have h₁ : Eq (α := ℝ) 1 (↑1 : ℝ)
Tactic: convert! ratCast_lt.2 zero_lt_one
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x : ℝ
⊢ ∀ (a b : ℝ), a ≤ b → ∀ (c : ℝ), a + c ≤ b + c
have simp : ∀ (a b : ℝ), a = b ∨ a < b → ∀ (c : ℝ), a + c = b + c ∨ a + c < b + c
Tactic: simp only [le_iff_eq_or_lt]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x a b : ℝ
h : a < b
⊢ ∀ (c : ℝ), a + c = b + c ∨ a + c < b + c
have inr : ∀ (c : ℝ), a + c < b + c
Tactic: refine fun c => Or.inr ?_
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x : ℝ
a b : CauSeq ℚ abs
h : mk a < mk b
c : CauSeq ℚ abs
⊢ mk a + mk c < mk b + mk c
have inr : a < b → a + c < b + c
Tactic: simp only [mk_lt, ← mk_add] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Real.Basic (hypothesis)
Goal:
x : ℝ
a b c : CauSeq ℚ abs
h : a < b
⊢ a + c < b + c
have h : (b - a).Pos
Tactic: change Pos _ at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x c : ℝ
a b : CauSeq ℚ abs
h : mk a < mk b
⊢ mk a + c < mk b + c
have inr : ∀ (c : CauSeq ℚ abs), mk a + mk c < mk b + mk 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]
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x b c : ℝ
a : CauSeq ℚ abs
h : mk a < b
⊢ mk a + c < b + c
have inr : ∀ (b : CauSeq ℚ abs), mk a < mk b → mk a + c < mk 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]
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x a b : ℝ
h : a < b
c : ℝ
⊢ a + c < b + c
have inr : ∀ (a : CauSeq ℚ abs), mk a < b → mk 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]
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x a b : ℝ
⊢ 0 < a → 0 < b → 0 < a * b
have h : ∀ (y : CauSeq ℚ abs), 0 < mk y → 0 < b → 0 < mk y * b
Tactic: induction a using Real.ind_mk
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x b : ℝ
y : CauSeq ℚ abs
⊢ 0 < mk y → 0 < b → 0 < mk y * b
have h : ∀ (y_1 : CauSeq ℚ abs), 0 < mk y → 0 < mk y_1 → 0 < mk y * mk y_1
Tactic: induction b using Real.ind_mk
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
a b : CauSeq ℚ abs
⊢ { cauchy := ⟦a ⊔ b⟧ : ℝ } = { cauchy := ⟦a⟧ }.sup { cauchy := ⟦b⟧ }
have 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) sorry x y }
Tactic: rw [sup_def]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
a b : CauSeq ℚ abs
⊢ { cauchy := ⟦a ⊓ b⟧ : ℝ } = { cauchy := ⟦a⟧ }.inf { cauchy := ⟦b⟧ }
have 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) sorry x y }
Tactic: rw [inf_def]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x a b : ℝ
⊢ a ≤ a ⊔ b
have h : ∀ (y : CauSeq ℚ abs), mk y ≤ mk y ⊔ b
Tactic: induction a using Real.ind_mk
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x b : ℝ
y : CauSeq ℚ abs
⊢ mk y ≤ mk y ⊔ b
have h : ∀ (y_1 : CauSeq ℚ abs), mk y ≤ mk y ⊔ mk y_1
Tactic: induction b using Real.ind_mk
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x : ℝ
y y_1 : CauSeq ℚ abs
⊢ mk y ≤ mk y ⊔ mk y_1
have h : y ≤ y ⊔ y_1
Tactic: rw [← mk_sup, mk_le]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x a b : ℝ
⊢ b ≤ a ⊔ b
have h : ∀ (y : CauSeq ℚ abs), b ≤ mk y ⊔ b
Tactic: induction a using Real.ind_mk
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x b : ℝ
y : CauSeq ℚ abs
⊢ b ≤ mk y ⊔ b
have h : ∀ (y_1 : CauSeq ℚ abs), mk y_1 ≤ mk y ⊔ mk y_1
Tactic: induction b using Real.ind_mk
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x : ℝ
y y_1 : CauSeq ℚ abs
⊢ mk y_1 ≤ mk y ⊔ mk y_1
have h : y_1 ≤ y ⊔ y_1
Tactic: rw [← mk_sup, mk_le]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x a b c : ℝ
⊢ a ≤ c → b ≤ c → a ⊔ b ≤ c
have h : ∀ (y : CauSeq ℚ abs), mk y ≤ c → b ≤ c → mk y ⊔ b ≤ c
Tactic: induction a using Real.ind_mk
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x b c : ℝ
y : CauSeq ℚ abs
⊢ mk y ≤ c → b ≤ c → mk y ⊔ b ≤ c
have h : ∀ (y_1 : CauSeq ℚ abs), mk y ≤ c → mk y_1 ≤ c → mk y ⊔ mk y_1 ≤ c
Tactic: induction b using Real.ind_mk
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x c : ℝ
y y_1 : CauSeq ℚ abs
⊢ mk y ≤ c → mk y_1 ≤ c → mk y ⊔ mk y_1 ≤ c
have h : ∀ (y_2 : CauSeq ℚ abs), mk y ≤ mk y_2 → mk y_1 ≤ mk y_2 → mk y ⊔ mk y_1 ≤ mk y_2
Tactic: induction c using Real.ind_mk
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x : ℝ
y y_1 y_2 : CauSeq ℚ abs
⊢ mk y ≤ mk y_2 → mk y_1 ≤ mk y_2 → mk y ⊔ mk y_1 ≤ mk y_2
have h : y ≤ y_2 → y_1 ≤ y_2 → y ⊔ y_1 ≤ y_2
Tactic: simp_rw [← mk_sup, mk_le]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x a b : ℝ
⊢ a ⊓ b ≤ a
have h : ∀ (y : CauSeq ℚ abs), mk y ⊓ b ≤ mk y
Tactic: induction a using Real.ind_mk
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x b : ℝ
y : CauSeq ℚ abs
⊢ mk y ⊓ b ≤ mk y
have h : ∀ (y_1 : CauSeq ℚ abs), mk y ⊓ mk y_1 ≤ mk y
Tactic: induction b using Real.ind_mk
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x : ℝ
y y_1 : CauSeq ℚ abs
⊢ mk y ⊓ mk y_1 ≤ mk y
have h : y ⊓ y_1 ≤ y
Tactic: rw [← mk_inf, mk_le]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x a b : ℝ
⊢ a ⊓ b ≤ b
have h : ∀ (y : CauSeq ℚ abs), mk y ⊓ b ≤ b
Tactic: induction a using Real.ind_mk
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x b : ℝ
y : CauSeq ℚ abs
⊢ mk y ⊓ b ≤ b
have h : ∀ (y_1 : CauSeq ℚ abs), mk y ⊓ mk y_1 ≤ mk y_1
Tactic: induction b using Real.ind_mk
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x : ℝ
y y_1 : CauSeq ℚ abs
⊢ mk y ⊓ mk y_1 ≤ mk y_1
have h : y ⊓ y_1 ≤ y_1
Tactic: rw [← mk_inf, mk_le]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x a b c : ℝ
⊢ a ≤ b → a ≤ c → a ≤ b ⊓ c
have h : ∀ (y : CauSeq ℚ abs), mk y ≤ b → mk y ≤ c → mk y ≤ b ⊓ c
Tactic: induction a using Real.ind_mk
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x b c : ℝ
y : CauSeq ℚ abs
⊢ mk y ≤ b → mk y ≤ c → mk y ≤ b ⊓ c
have h : ∀ (y_1 : CauSeq ℚ abs), mk y ≤ mk y_1 → mk y ≤ c → mk y ≤ mk y_1 ⊓ c
Tactic: induction b using Real.ind_mk
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x c : ℝ
y y_1 : CauSeq ℚ abs
⊢ mk y ≤ mk y_1 → mk y ≤ c → mk y ≤ mk y_1 ⊓ c
have h : ∀ (y_2 : CauSeq ℚ abs), mk y ≤ mk y_1 → mk y ≤ mk y_2 → mk y ≤ mk y_1 ⊓ mk y_2
Tactic: induction c using Real.ind_mk
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x : ℝ
y y_1 y_2 : CauSeq ℚ abs
⊢ mk y ≤ mk y_1 → mk y ≤ mk y_2 → mk y ≤ mk y_1 ⊓ mk y_2
have h : y ≤ y_1 → y ≤ y_2 → y ≤ y_1 ⊓ y_2
Tactic: simp_rw [← mk_inf, mk_le]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x a b c : ℝ
⊢ (a ⊔ b) ⊓ (a ⊔ c) ≤ a ⊔ b ⊓ c
have h : ∀ (y : CauSeq ℚ abs), (mk y ⊔ b) ⊓ (mk y ⊔ c) ≤ mk y ⊔ b ⊓ c
Tactic: induction a using Real.ind_mk
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x b c : ℝ
y : CauSeq ℚ abs
⊢ (mk y ⊔ b) ⊓ (mk y ⊔ c) ≤ mk y ⊔ b ⊓ c
have h : ∀ (y_1 : CauSeq ℚ abs), (mk y ⊔ mk y_1) ⊓ (mk y ⊔ c) ≤ mk y ⊔ mk y_1 ⊓ c
Tactic: induction b using Real.ind_mk
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x c : ℝ
y y_1 : CauSeq ℚ abs
⊢ (mk y ⊔ mk y_1) ⊓ (mk y ⊔ c) ≤ mk y ⊔ mk y_1 ⊓ c
have h : ∀ (y_2 : CauSeq ℚ abs), (mk y ⊔ mk y_1) ⊓ (mk y ⊔ mk y_2) ≤ mk y ⊔ mk y_1 ⊓ mk y_2
Tactic: induction c using Real.ind_mk
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x : ℝ
y y_1 y_2 : CauSeq ℚ abs
⊢ (mk y ⊔ mk y_1) ⊓ (mk y ⊔ mk y_2) ≤ mk y ⊔ mk y_1 ⊓ mk y_2
have h : (mk y ⊔ mk y_1) ⊓ (mk y ⊔ mk y_2) = mk y ⊔ mk y_1 ⊓ mk y_2
Tactic: apply Eq.le
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x : ℝ
y y_1 y_2 : CauSeq ℚ abs
⊢ (mk y ⊔ mk y_1) ⊓ (mk y ⊔ mk y_2) = mk y ⊔ mk y_1 ⊓ mk y_2
have h : mk ((y ⊔ y_1) ⊓ (y ⊔ y_2)) = mk (y ⊔ y_1 ⊓ y_2)
Tactic: simp only [← mk_sup, ← mk_inf]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x a b : ℝ
⊢ a ≤ b ∨ b ≤ a
have h : ∀ (y : CauSeq ℚ abs), mk y ≤ b ∨ b ≤ mk y
Tactic: induction a using Real.ind_mk
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x b : ℝ
y : CauSeq ℚ abs
⊢ mk y ≤ b ∨ b ≤ mk y
have h : ∀ (y_1 : CauSeq ℚ abs), mk y ≤ mk y_1 ∨ mk y_1 ≤ mk y
Tactic: induction b using Real.ind_mk
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
f g : Cauchy (α := ℚ) abs
⊢ { cauchy := f / g : ℝ } = { cauchy := f : ℝ } / { cauchy := g : ℝ }
have simp_rw : { cauchy := f * g⁻¹ : ℝ } = { cauchy := f : ℝ } * { cauchy := g : ℝ }⁻¹
Tactic: simp_rw [div_eq_mul_inv, ofCauchy_mul, ofCauchy_inv]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
f g : Cauchy (α := ℚ) abs
simp_rw : { cauchy := f * g⁻¹ : ℝ } = { cauchy := f : ℝ } * { cauchy := g : ℝ }⁻¹
⊢ { cauchy := f / g : ℝ } = { cauchy := f : ℝ } / { cauchy := g : ℝ }
have simp_rw₁ : { cauchy := f : ℝ } * { cauchy := g⁻¹ : ℝ } = { cauchy := f : ℝ } * { cauchy := g : ℝ }⁻¹
Tactic: simp_rw [div_eq_mul_inv, ofCauchy_mul, ofCauchy_inv]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x : ℝ
a : Cauchy (α := ℚ) abs
h : { cauchy := a : ℝ } ≠ 0
⊢ { cauchy := a : ℝ } * { cauchy := a : ℝ }⁻¹ = 1
have rw : { cauchy := a : ℝ }⁻¹ * { cauchy := a : ℝ } = 1
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x : ℝ
a : Cauchy (α := ℚ) abs
h : { cauchy := a : ℝ } ≠ 0
⊢ { cauchy := a : ℝ }⁻¹ * { cauchy := a : ℝ } = 1
have simp : ∀ (h : ¬a = 0), a⁻¹ * a = 1
Tactic: simp only [← ofCauchy_inv, ← ofCauchy_mul, ← ofCauchy_one, ← ofCauchy_zero,
      Ne, ofCauchy.injEq] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x : ℝ
q : ℚ≥0
⊢ (↑q : ℝ) = HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ)
have rw : { cauchy := (↑q : Cauchy abs) : ℝ } = HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ)
Tactic: rw [← ofCauchy_nnratCast, NNRat.cast_def, ofCauchy_div, ofCauchy_natCast, ofCauchy_natCast]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x : ℝ
q : ℚ≥0
rw : { cauchy := (↑q : Cauchy abs) : ℝ } = HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ)
⊢ (↑q : ℝ) = HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ)
have rw₁ : { cauchy := HDiv.hDiv (α := Cauchy (α := ℚ) abs) (↑q.num : Cauchy abs) (↑q.den : Cauchy abs) : ℝ } =
  HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ)
Tactic: rw [← ofCauchy_nnratCast, NNRat.cast_def, ofCauchy_div, ofCauchy_natCast, ofCauchy_natCast]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
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 : ℝ)
⊢ (↑q : ℝ) = HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ)
have rw₂ : { cauchy := (↑q.num : Cauchy abs) : ℝ } / { cauchy := (↑q.den : Cauchy abs) : ℝ } =
  HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ)
Tactic: rw [← ofCauchy_nnratCast, NNRat.cast_def, ofCauchy_div, ofCauchy_natCast, ofCauchy_natCast]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
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 : ℝ)
⊢ (↑q : ℝ) = HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ)
have rw₃ : (↑q.num : ℝ) / { cauchy := (↑q.den : Cauchy abs) : ℝ } = HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ)
Tactic: rw [← ofCauchy_nnratCast, NNRat.cast_def, ofCauchy_div, ofCauchy_natCast, ofCauchy_natCast]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
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 : ℝ)
⊢ (↑q : ℝ) = HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ)
have rw₄ : HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ) = HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ)
Tactic: rw [← ofCauchy_nnratCast, NNRat.cast_def, ofCauchy_div, ofCauchy_natCast, ofCauchy_natCast]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x : ℝ
q : ℚ
⊢ (↑q : ℝ) = HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ)
have rw : { cauchy := (↑q : Cauchy abs) : ℝ } = HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ)
Tactic: rw [← ofCauchy_ratCast, Rat.cast_def, ofCauchy_div, ofCauchy_natCast, ofCauchy_intCast]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x : ℝ
q : ℚ
rw : { cauchy := (↑q : Cauchy abs) : ℝ } = HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ)
⊢ (↑q : ℝ) = HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ)
have rw₁ : { cauchy := HDiv.hDiv (α := Cauchy (α := ℚ) abs) (↑q.num : Cauchy abs) (↑q.den : Cauchy abs) : ℝ } =
  HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ)
Tactic: rw [← ofCauchy_ratCast, Rat.cast_def, ofCauchy_div, ofCauchy_natCast, ofCauchy_intCast]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
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 : ℝ)
⊢ (↑q : ℝ) = HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ)
have rw₂ : { cauchy := (↑q.num : Cauchy abs) : ℝ } / { cauchy := (↑q.den : Cauchy abs) : ℝ } =
  HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ)
Tactic: rw [← ofCauchy_ratCast, Rat.cast_def, ofCauchy_div, ofCauchy_natCast, ofCauchy_intCast]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
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 : ℝ)
⊢ (↑q : ℝ) = HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ)
have rw₃ : { cauchy := (↑q.num : Cauchy abs) : ℝ } / (↑q.den : ℝ) = HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ)
Tactic: rw [← ofCauchy_ratCast, Rat.cast_def, ofCauchy_div, ofCauchy_natCast, ofCauchy_intCast]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
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 : ℝ)
⊢ (↑q : ℝ) = HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ)
have rw₄ : HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ) = HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ)
Tactic: rw [← ofCauchy_ratCast, Rat.cast_def, ofCauchy_div, ofCauchy_natCast, ofCauchy_intCast]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x : ℝ
f : CauSeq ℚ abs
h : ∃ (i : ℕ), ∀ j ≥ i, x ≤ (↑((↑f : ℕ → ℚ) j) : ℝ)
⊢ x ≤ mk f
have h₁ : ∀ (y : CauSeq ℚ abs) (h : ∃ (i : ℕ), ∀ j ≥ i, mk y ≤ (↑((↑f : ℕ → ℚ) j) : ℝ)), mk y ≤ mk f
Tactic: induction x using Real.ind_mk
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x : ℝ
f y : CauSeq ℚ abs
h : ∃ (i : ℕ), ∀ j ≥ i, mk y ≤ (↑((↑f : ℕ → ℚ) j) : ℝ)
⊢ mk y ≤ mk f
have h₁ : ¬mk f < mk y
Tactic: apply le_of_not_gt
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x : ℝ
f y : CauSeq ℚ abs
h : ∃ (i : ℕ), ∀ j ≥ i, mk y ≤ (↑((↑f : ℕ → ℚ) j) : ℝ)
⊢ ¬mk f < mk y
have h₁ : ¬f < y
Tactic: rw [mk_lt]