awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Real.Archimedean
Goal:
a : ℝ
ha : ∀ (k : ℕ) (_ : 0 < k), a ≤ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1
refine : ∀ (q : ℚ), LT.lt (α := ℝ) 1 (↑q : ℝ) → a ≤ (↑q : ℝ)
⊢ a ≤ 1

Tactic:
refine le_of_forall_lt_rat_imp_le ?_

Premises used: le_of_forall_lt_rat_imp_le
-- Module: Mathlib.Data.Real.Archimedean
Goal:
a : ℝ
ha : ∀ (k : ℕ) (_ : 0 < k), a ≤ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1
q : ℚ
hq : LT.lt (α := ℝ) 1 (↑q : ℝ)
⊢ 0 < q.den

Tactic:
positivity
-- Module: Mathlib.Data.Real.Archimedean
Goal:
a : ℝ
ha : ∀ (k : ℕ) (_ : 0 < k), a ≤ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1
q : ℚ
hq : LT.lt (α := ℝ) 1 (↑q : ℝ)
refine : HDiv.hDiv (α := ℝ) 1 (↑q.den : ℝ) + 1 ≤ (↑q : ℝ)
⊢ a ≤ (↑q : ℝ)

Tactic:
refine (ha q.den (by positivity)).trans ?_

Premises used: Rat.den, LE.le.trans
-- Module: Mathlib.Data.Real.Archimedean
Goal:
a : ℝ
ha : ∀ (k : ℕ) (_ : 0 < k), a ≤ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1
q : ℚ
hq : LT.lt (α := ℝ) 1 (↑q : ℝ)
⊢ LT.lt (α := ℝ) 0 (↑q.den : ℝ)

Tactic:
positivity
-- Module: Mathlib.Data.Real.Archimedean
Goal:
a : ℝ
ha : ∀ (k : ℕ) (_ : 0 < k), a ≤ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1
q : ℚ
hq : LT.lt (α := ℝ) 1 (↑q : ℝ)
rw : 1 ≤ HMul.hMul (α := ℝ) (↑q : ℝ) (↑q.den : ℝ) - (↑q.den : ℝ)
⊢ HDiv.hDiv (α := ℝ) 1 (↑q.den : ℝ) + 1 ≤ (↑q : ℝ)

Tactic:
rw [← le_sub_iff_add_le, div_le_iff₀ (by positivity), sub_mul, one_mul]

Premises used: div_le_iff₀, sub_mul, le_sub_iff_add_le, one_mul
-- Module: Mathlib.Data.Real.Archimedean
Goal:
a : ℝ
ha : ∀ (k : ℕ) (_ : 0 < k), a ≤ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1
q : ℚ
hq : LT.lt (α := ℝ) 1 (↑q : ℝ)
norm_cast : ∀ (hq : 1 < q), 1 ≤ q * (↑q.den : ℚ) - (↑q.den : ℚ)
⊢ 1 ≤ HMul.hMul (α := ℝ) (↑q : ℝ) (↑q.den : ℝ) - (↑q.den : ℝ)

Tactic:
norm_cast at hq ⊢
-- Module: Mathlib.Data.Real.Archimedean
Goal:
a : ℝ
ha : ∀ (k : ℕ) (_ : 0 < k), a ≤ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1
q : ℚ
hq : 1 < HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)
⊢ LT.lt (α := ℚ) 0 (↑q.den : ℚ)

Tactic:
positivity
-- Module: Mathlib.Data.Real.Archimedean
Goal:
a : ℝ
ha : ∀ (k : ℕ) (_ : 0 < k), a ≤ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1
q : ℚ
hq : 1 < q
⊢ LT.lt (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)

Tactic:
rw [← q.num_div_den, one_lt_div (by positivity)] at hq

Premises used: Rat.num_div_den, one_lt_div
-- Module: Mathlib.Data.Real.Archimedean
Goal:
a : ℝ
ha : ∀ (k : ℕ) (_ : 0 < k), a ≤ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1
q : ℚ
hq : LT.lt (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
rw : 1 ≤ HSub.hSub (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)
⊢ 1 ≤ q * (↑q.den : ℚ) - (↑q.den : ℚ)

Tactic:
rw [q.mul_den_eq_num]

Premises used: Rat.mul_den_eq_num
-- Module: Mathlib.Data.Real.Archimedean
Goal:
a : ℝ
ha : ∀ (k : ℕ) (_ : 0 < k), a ≤ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1
q : ℚ
hq : LT.lt (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
norm_cast : ∀ (hq : (↑q.den : ℤ) < q.num), 1 ≤ q.num - (↑q.den : ℤ)
⊢ 1 ≤ HSub.hSub (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)

Tactic:
norm_cast at hq ⊢
-- Module: Mathlib.Data.Real.Archimedean
Goal:
a : ℝ
ha : ∀ (k : ℕ) (_ : 0 < k), a ≤ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1
q : ℚ
hq : (↑q.den : ℤ) < q.num
⊢ 1 ≤ q.num - (↑q.den : ℤ)

Tactic:
lia
-- Module: Mathlib.Data.Real.Archimedean
Goal:
a : ℝ
ha : 1 < a
obtain :
  ∀ (k : ℕ) (posk : 0 < k) (hk : HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1 < a),
    ∃ (m : ℕ), HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 < a ^ m
⊢ ∃ (m : ℕ), HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 < a ^ m

Tactic:
obtain ⟨k, posk, hk⟩ : ∃ k : ℕ, 0 < k ∧ 1 / k + 1 < a := by
    contrapose! ha
    refine le_of_forall_lt_rat_imp_le ?_
    intro q hq
    refine (ha q.den (by positivity)).trans ?_
    rw [← le_sub_iff_add_le, div_le_iff₀ (by positivity), sub_mul, one_mul]
    norm_cast at hq ⊢
    rw [← q.num_div_den, one_lt_div (by positivity)] at hq
    rw [q.mul_den_eq_num]
    norm_cast at hq ⊢
    lia
-- Module: Mathlib.Data.Real.Archimedean
Goal:
a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1 < a
h : HAdd.hAdd (α := ℝ) (↑(2 * HPow.hPow (β := ℕ) k 2) : ℝ) 1 < a ^ (2 * HPow.hPow (β := ℕ) k 2)
⊢ ∃ (m : ℕ), HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 < a ^ m

Tactic:
use 2 * k ^ 2
-- Module: Mathlib.Data.Real.Archimedean
Goal:
a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1 < a
simp : 2 = HAdd.hAdd (α := ℝ) 1 1
⊢ HPow.hPow (α := ℝ) 2 (2 * k) = (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) * (↑k : ℝ) + 1) ^ (2 * k)

Tactic:
simp [posk.ne']

Premises used: LT.lt.ne'
-- Module: Mathlib.Data.Real.Archimedean
Goal:
a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1 < a
⊢ 2 = HAdd.hAdd (α := ℝ) 1 1

Tactic:
norm_num
-- Module: Mathlib.Data.Real.Archimedean
Goal:
a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1 < a
hab : HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) * (↑k : ℝ) + 1 ≤ (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ k
⊢ (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) * (↑k : ℝ) + 1) ^ (2 * k) ≤ ((HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ k) ^ (2 * k)

Tactic:
gcongr
-- Module: Mathlib.Data.Real.Archimedean
Goal:
a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1 < a
⊢ 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ)

Tactic:
simp
-- Module: Mathlib.Data.Real.Archimedean
Goal:
a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1 < a
⊢ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) * (↑k : ℝ) + 1 ≤ (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ k

Tactic:
exact mul_add_one_le_add_one_pow (by simp) _

Premises used: Real.mul_add_one_le_add_one_pow
-- Module: Mathlib.Data.Real.Archimedean
Goal:
a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1 < a
rw :
  (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ (k * (2 * k)) =
    (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ (2 * HPow.hPow (β := ℕ) k 2)
rw₁ :
  (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ (2 * (k * k)) =
    (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ (2 * HPow.hPow (β := ℕ) k 2)
rw₂ rw₃ : (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ (2 * (k * k)) = (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ (2 * (k * k))
⊢ ((HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ k) ^ (2 * k) =
    (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ (2 * HPow.hPow (β := ℕ) k 2)

Tactic:
rw [← pow_mul, mul_left_comm, sq]

Premises used: sq, mul_left_comm, pow_mul
-- Module: Mathlib.Data.Real.Archimedean
Goal:
a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1 < a
ha₁ : 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1
a₁ : 2 * HPow.hPow (β := ℕ) k 2 ≠ 0
⊢ (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ (2 * HPow.hPow (β := ℕ) k 2) < a ^ (2 * HPow.hPow (β := ℕ) k 2)

Tactic:
gcongr
-- Module: Mathlib.Data.Real.Archimedean
Goal:
a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1 < a
k₁ : HPow.hPow (α := ℝ) 2 (2 * k) = (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) * (↑k : ℝ) + 1) ^ (2 * k)
k₂ : (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) * (↑k : ℝ) + 1) ^ (2 * k) ≤ ((HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ k) ^ (2 * k)
k₃ :
  ((HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ k) ^ (2 * k) =
    (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ (2 * HPow.hPow (β := ℕ) k 2)
k₄ : (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ (2 * HPow.hPow (β := ℕ) k 2) < a ^ (2 * HPow.hPow (β := ℕ) k 2)
⊢ HAdd.hAdd (α := ℝ) (↑(2 * HPow.hPow (β := ℕ) k 2) : ℝ) 1 < a ^ (2 * HPow.hPow (β := ℕ) k 2)

Tactic:
calc
    ((2 * k ^ 2 : ℕ) + 1 : ℝ) ≤ 2 ^ (2 * k) := mod_cast Nat.two_mul_sq_add_one_le_two_pow_two_mul _
    _ = (1 / k * k + 1 : ℝ) ^ (2 * k) := by simp [posk.ne']; norm_num
    _ ≤ ((1 / k + 1) ^ k : ℝ) ^ (2 * k) := by gcongr; exact mul_add_one_le_add_one_pow (by simp) _
    _ = (1 / k + 1 : ℝ) ^ (2 * k ^ 2) := by rw [← pow_mul, mul_left_comm, sq]
    _ < a ^ (2 * k ^ 2) := by gcongr

Premises used: HMul.hMul, HDiv.hDiv, Nat.cast, Nat.two_mul_sq_add_one_le_two_pow_two_mul, HPow.hPow, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Real.Archimedean
Goal:
b : ℝ
hb : 0 < b
⊢ ∃ (n : ℕ), 0 < n ∧ (↑n : ℝ)⁻¹ < b

Tactic:
(exists_nat_gt b⁻¹).imp fun k hk ↦ ?_

Premises used: Exists.imp, Inv.inv, exists_nat_gt
-- Module: Mathlib.Data.Real.Archimedean
Goal:
b : ℝ
hb : 0 < b
refine : ∀ (k : ℕ) (hk : b⁻¹ < (↑k : ℝ)), 0 < k ∧ (↑k : ℝ)⁻¹ < b
⊢ ∃ (n : ℕ), 0 < n ∧ (↑n : ℝ)⁻¹ < b

Tactic:
refine (exists_nat_gt b⁻¹).imp fun k hk ↦ ?_

Premises used: Exists.imp, Inv.inv, exists_nat_gt
-- Module: Mathlib.Data.Real.Archimedean
Goal:
b : ℝ
hb : 0 < b
k : ℕ
hk : b⁻¹ < (↑k : ℝ)
⊢ LT.lt (α := ℝ) 0 (↑k : ℝ)

Tactic:
have := (inv_pos_of_pos hb).trans hk
-- Module: Mathlib.Data.Real.Archimedean
Goal:
b : ℝ
hb : 0 < b
k : ℕ
hk : b⁻¹ < (↑k : ℝ)
this : LT.lt (α := ℝ) 0 (↑k : ℝ)
⊢ 0 < k ∧ (↑k : ℝ)⁻¹ < b

Tactic:
⟨Nat.cast_pos.mp this, ?_⟩

Premises used: Nat.cast_pos, And.intro, Iff.mp
-- Module: Mathlib.Data.Real.Archimedean
Goal:
b : ℝ
hb : 0 < b
k : ℕ
hk : b⁻¹ < (↑k : ℝ)
this : LT.lt (α := ℝ) 0 (↑k : ℝ)
refine : (↑k : ℝ)⁻¹ < b
⊢ 0 < k ∧ (↑k : ℝ)⁻¹ < b

Tactic:
refine ⟨Nat.cast_pos.mp this, ?_⟩
-- Module: Mathlib.Data.Real.Archimedean
Goal:
b : ℝ
hb : 0 < b
k : ℕ
hk : b⁻¹ < (↑k : ℝ)
this : LT.lt (α := ℝ) 0 (↑k : ℝ)
rwa rwa₁ rwa₂ rwa₃ : b⁻¹ < (↑k : ℝ)
⊢ (↑k : ℝ)⁻¹ < b

Tactic:
rwa [inv_lt_comm₀ this hb]

Premises used: inv_lt_comm₀
-- Module: Mathlib.Data.Real.Basic
Goal:
abv : ℚ → ℚ
inst : IsAbsoluteValue abv
q : ℚ
⊢ Eq (α := Cauchy abv) (ofRat q) (↑q : Cauchy abv)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Real.Basic
Goal:
a b : Cauchy (α := ℚ) abs
rw rw₁ : a = b ↔ { cauchy := a : ℝ }.cauchy = { cauchy := b }.cauchy
⊢ { cauchy := a : ℝ } = { cauchy := b } ↔ { cauchy := a : ℝ }.cauchy = { cauchy := b }.cauchy

Tactic:
rw [ofCauchy.injEq]

Premises used: Real.ofCauchy.injEq
-- Module: Mathlib.Data.Real.Basic
Goal:
x y : ℝ
⊢ x.cauchy = y.cauchy → x = y

Tactic:
ext_cauchy_iff.2

Premises used: Iff.mpr, Real.ext_cauchy_iff
-- Module: Mathlib.Data.Real.Basic
Goal:
⊢ { cauchy := 0 : ℝ } = 0

Tactic:
zero_def.symm

Premises used: _private.0.Real.zero_def, Eq.symm
-- Module: Mathlib.Data.Real.Basic
Goal:
⊢ { cauchy := 1 : ℝ } = 1

Tactic:
one_def.symm

Premises used: _private.0.Real.one_def, Eq.symm
-- Module: Mathlib.Data.Real.Basic
Goal:
a b : Cauchy (α := ℚ) abs
⊢ { cauchy := a + b : ℝ } = { cauchy := a : ℝ } + { cauchy := b : ℝ }

Tactic:
(add_def _ _).symm

Premises used: _private.0.Real.add_def, Eq.symm
-- Module: Mathlib.Data.Real.Basic
Goal:
a : Cauchy (α := ℚ) abs
⊢ { cauchy := -a : ℝ } = -{ cauchy := a }

Tactic:
(neg_def _).symm

Premises used: Eq.symm, _private.0.Real.neg_def
-- Module: Mathlib.Data.Real.Basic
Goal:
a b : Cauchy (α := ℚ) abs
rw : { cauchy := a : ℝ } + -{ cauchy := b : ℝ } = { cauchy := a : ℝ } - { cauchy := b : ℝ }
⊢ { cauchy := a - b : ℝ } = { cauchy := a : ℝ } - { cauchy := b : ℝ }

Tactic:
rw [sub_eq_add_neg, ofCauchy_add, ofCauchy_neg]

Premises used: sub_eq_add_neg, Real.ofCauchy_add, Real.ofCauchy_neg
-- Module: Mathlib.Data.Real.Basic
Goal:
a b : Cauchy (α := ℚ) abs
⊢ { cauchy := a : ℝ } + -{ cauchy := b : ℝ } = { cauchy := a : ℝ } - { cauchy := b : ℝ }

Tactic:
rfl
-- Module: Mathlib.Data.Real.Basic
Goal:
a b : Cauchy (α := ℚ) abs
⊢ { cauchy := a * b : ℝ } = { cauchy := a : ℝ } * { cauchy := b : ℝ }

Tactic:
(mul_def _ _).symm

Premises used: _private.0.Real.mul_def, Eq.symm
-- Module: Mathlib.Data.Real.Basic
Goal:
f : Cauchy (α := ℚ) abs
rw rw₁ :
  { cauchy := f⁻¹ : ℝ } =
    match (motive := ℝ → ℝ) { cauchy := f } with
    | { cauchy := a } => { cauchy := a⁻¹ }
⊢ { cauchy := f⁻¹ : ℝ } = { cauchy := f }.inv'

Tactic:
rw [inv']

Premises used: _private.0.Real.inv'
-- Module: Mathlib.Data.Real.Basic
Goal:
rw rw₁ : { cauchy := 0 : ℝ }.cauchy = 0
⊢ zero.cauchy = 0

Tactic:
rw [zero_def]

Premises used: _private.0.Real.zero_def
-- Module: Mathlib.Data.Real.Basic
Goal:
rw rw₁ : { cauchy := 1 : ℝ }.cauchy = 1
⊢ one.cauchy = 1

Tactic:
rw [one_def]

Premises used: _private.0.Real.one_def
-- Module: Mathlib.Data.Real.Basic
Goal:
a b : Cauchy (α := ℚ) abs
rw rw₁ :
  cauchy
      (match (motive := ℝ → ℝ → ℝ) { cauchy := a : ℝ }, { cauchy := b : ℝ } with
      | { cauchy := a }, { cauchy := b } => { cauchy := a + b : ℝ }) =
    { cauchy := a : ℝ }.cauchy + { cauchy := b : ℝ }.cauchy
⊢ ({ cauchy := a : ℝ }.add { cauchy := b : ℝ }).cauchy = { cauchy := a : ℝ }.cauchy + { cauchy := b : ℝ }.cauchy

Tactic:
rw [add_def]

Premises used: _private.0.Real.add_def
-- Module: Mathlib.Data.Real.Basic
Goal:
a : Cauchy (α := ℚ) abs
rw rw₁ :
  cauchy
      (match (motive := ℝ → ℝ) { cauchy := a : ℝ } with
      | { cauchy := a } => { cauchy := -a : ℝ }) =
    -{ cauchy := a }.cauchy
⊢ { cauchy := a : ℝ }.neg.cauchy = -{ cauchy := a }.cauchy

Tactic:
rw [neg_def]

Premises used: _private.0.Real.neg_def
-- Module: Mathlib.Data.Real.Basic
Goal:
a b : Cauchy (α := ℚ) abs
rw rw₁ :
  cauchy
      (match (motive := ℝ → ℝ → ℝ) { cauchy := a : ℝ }, { cauchy := b : ℝ } with
      | { cauchy := a }, { cauchy := b } => { cauchy := a * b : ℝ }) =
    { cauchy := a : ℝ }.cauchy * { cauchy := b : ℝ }.cauchy
⊢ ({ cauchy := a : ℝ }.mul { cauchy := b : ℝ }).cauchy = { cauchy := a : ℝ }.cauchy * { cauchy := b : ℝ }.cauchy

Tactic:
rw [mul_def]

Premises used: _private.0.Real.mul_def
-- Module: Mathlib.Data.Real.Basic
Goal:
a b : Cauchy (α := ℚ) abs
rw : ({ cauchy := a : ℝ } - { cauchy := b : ℝ }).cauchy = ({ cauchy := a : ℝ } + -{ cauchy := b : ℝ }).cauchy
⊢ ({ cauchy := a : ℝ } - { cauchy := b : ℝ }).cauchy = { cauchy := a : ℝ }.cauchy - { cauchy := b : ℝ }.cauchy

Tactic:
rw [sub_eq_add_neg, ← cauchy_neg, ← cauchy_add]

Premises used: sub_eq_add_neg, Real.cauchy_neg, Real.cauchy_add
-- Module: Mathlib.Data.Real.Basic
Goal:
a b : Cauchy (α := ℚ) abs
⊢ ({ cauchy := a : ℝ } - { cauchy := b : ℝ }).cauchy = ({ cauchy := a : ℝ } + -{ cauchy := b : ℝ }).cauchy

Tactic:
rfl
-- Module: Mathlib.Data.Real.Basic
Goal:
f : Cauchy (α := ℚ) abs
rw rw₁ :
  cauchy
      (match (motive := ℝ → ℝ) { cauchy := f : ℝ } with
      | { cauchy := a } => { cauchy := a⁻¹ : ℝ }) =
    { cauchy := f }.cauchy⁻¹
⊢ { cauchy := f : ℝ }.inv'.cauchy = { cauchy := f }.cauchy⁻¹

Tactic:
rw [inv']

Premises used: _private.0.Real.inv'
-- Module: Mathlib.Data.Real.Basic
Goal:
n : ℕ
⊢ { cauchy := (↑n : Cauchy abs) : ℝ } = (↑n : ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Real.Basic
Goal:
z : ℤ
⊢ { cauchy := (↑z : Cauchy abs) : ℝ } = (↑z : ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Real.Basic
Goal:
q : ℚ≥0
⊢ { cauchy := (↑q : Cauchy abs) : ℝ } = (↑q : ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Real.Basic
Goal:
q : ℚ
⊢ { cauchy := (↑q : Cauchy abs) : ℝ } = (↑q : ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Real.Basic
Goal:
n : ℕ
⊢ cauchy (↑n : ℝ) = (↑n : Cauchy abs)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Real.Basic
Goal:
z : ℤ
⊢ cauchy (↑z : ℝ) = (↑z : Cauchy abs)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Real.Basic
Goal:
q : ℚ≥0
⊢ cauchy (↑q : ℝ) = (↑q : Cauchy abs)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Real.Basic
Goal:
q : ℚ
⊢ cauchy (↑q : ℝ) = (↑q : Cauchy abs)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Real.Basic
Goal:
x a b c : ℝ
a₁ : (a + b + c).cauchy = (a + (b + c)).cauchy
⊢ a + b + c = a + (b + c)

Tactic:
apply ext_cauchy

Premises used: Real.ext_cauchy
-- Module: Mathlib.Data.Real.Basic
Goal:
x a b c : ℝ
⊢ (a + b + c).cauchy = (a + (b + c)).cauchy

Tactic:
simp only [cauchy_add, add_assoc]

Premises used: add_assoc, Real.cauchy_add
-- Module: Mathlib.Data.Real.Basic
Goal:
x a : ℝ
a₁ : (0 + a).cauchy = a.cauchy
⊢ 0 + a = a

Tactic:
apply ext_cauchy

Premises used: Real.ext_cauchy
-- Module: Mathlib.Data.Real.Basic
Goal:
x a : ℝ
⊢ (0 + a).cauchy = a.cauchy

Tactic:
simp [cauchy_add, cauchy_zero]

Premises used: Real.cauchy_add, Real.cauchy_zero
-- Module: Mathlib.Data.Real.Basic
Goal:
x a : ℝ
a₁ : (a + 0).cauchy = a.cauchy
⊢ a + 0 = a

Tactic:
apply ext_cauchy

Premises used: Real.ext_cauchy
-- Module: Mathlib.Data.Real.Basic
Goal:
x a : ℝ
⊢ (a + 0).cauchy = a.cauchy

Tactic:
simp [cauchy_add, cauchy_zero]

Premises used: Real.cauchy_add, Real.cauchy_zero
-- Module: Mathlib.Data.Real.Basic
Goal:
x a b : ℝ
a₁ : (a + b).cauchy = (b + a).cauchy
⊢ a + b = b + a

Tactic:
apply ext_cauchy

Premises used: Real.ext_cauchy
-- Module: Mathlib.Data.Real.Basic
Goal:
x a b : ℝ
⊢ (a + b).cauchy = (b + a).cauchy

Tactic:
simp only [cauchy_add, add_comm]

Premises used: add_comm, Real.cauchy_add
-- Module: Mathlib.Data.Real.Basic
Goal:
x a b c : ℝ
a₁ : (a * b * c).cauchy = (a * (b * c)).cauchy
⊢ a * b * c = a * (b * c)

Tactic:
apply ext_cauchy

Premises used: Real.ext_cauchy
-- Module: Mathlib.Data.Real.Basic
Goal:
x a b c : ℝ
⊢ (a * b * c).cauchy = (a * (b * c)).cauchy

Tactic:
simp only [cauchy_mul, mul_assoc]

Premises used: mul_assoc, Real.cauchy_mul
-- Module: Mathlib.Data.Real.Basic
Goal:
x a : ℝ
a₁ : (1 * a).cauchy = a.cauchy
⊢ 1 * a = a

Tactic:
apply ext_cauchy

Premises used: Real.ext_cauchy
-- Module: Mathlib.Data.Real.Basic
Goal:
x a : ℝ
⊢ (1 * a).cauchy = a.cauchy

Tactic:
simp [cauchy_mul, cauchy_one]

Premises used: Real.cauchy_one, Real.cauchy_mul
-- Module: Mathlib.Data.Real.Basic
Goal:
x a : ℝ
a₁ : (a * 1).cauchy = a.cauchy
⊢ a * 1 = a

Tactic:
apply ext_cauchy

Premises used: Real.ext_cauchy
-- Module: Mathlib.Data.Real.Basic
Goal:
x a : ℝ
⊢ (a * 1).cauchy = a.cauchy

Tactic:
simp [cauchy_mul, cauchy_one]

Premises used: Real.cauchy_one, Real.cauchy_mul
-- Module: Mathlib.Data.Real.Basic
Goal:
x a : ℝ
a₁ : (0 * a).cauchy = cauchy 0
⊢ 0 * a = 0

Tactic:
apply ext_cauchy

Premises used: Real.ext_cauchy
-- Module: Mathlib.Data.Real.Basic
Goal:
x a : ℝ
⊢ (0 * a).cauchy = cauchy 0

Tactic:
simp [cauchy_mul, cauchy_zero]

Premises used: Real.cauchy_zero, Real.cauchy_mul
-- Module: Mathlib.Data.Real.Basic
Goal:
x a : ℝ
a₁ : (a * 0).cauchy = cauchy 0
⊢ a * 0 = 0

Tactic:
apply ext_cauchy

Premises used: Real.ext_cauchy
-- Module: Mathlib.Data.Real.Basic
Goal:
x a : ℝ
⊢ (a * 0).cauchy = cauchy 0

Tactic:
simp [cauchy_mul, cauchy_zero]

Premises used: Real.cauchy_zero, Real.cauchy_mul
-- Module: Mathlib.Data.Real.Basic
Goal:
x a b c : ℝ
a₁ : (a * (b + c)).cauchy = (a * b + a * c).cauchy
⊢ a * (b + c) = a * b + a * c

Tactic:
apply ext_cauchy

Premises used: Real.ext_cauchy
-- Module: Mathlib.Data.Real.Basic
Goal:
x a b c : ℝ
⊢ (a * (b + c)).cauchy = (a * b + a * c).cauchy

Tactic:
simp only [cauchy_add, cauchy_mul, mul_add]

Premises used: Real.cauchy_add, mul_add, Real.cauchy_mul
-- Module: Mathlib.Data.Real.Basic
Goal:
x a b c : ℝ
a₁ : ((a + b) * c).cauchy = (a * c + b * c).cauchy
⊢ (a + b) * c = a * c + b * c

Tactic:
apply ext_cauchy

Premises used: Real.ext_cauchy
-- Module: Mathlib.Data.Real.Basic
Goal:
x a b c : ℝ
⊢ ((a + b) * c).cauchy = (a * c + b * c).cauchy

Tactic:
simp only [cauchy_add, cauchy_mul, add_mul]

Premises used: add_mul, Real.cauchy_add, Real.cauchy_mul
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
a : { cauchy := (↑0 : Cauchy abs) : ℝ }.cauchy = cauchy 0
⊢ { cauchy := (↑0 : Cauchy abs) : ℝ } = 0

Tactic:
apply ext_cauchy

Premises used: Real.ext_cauchy
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
⊢ { cauchy := (↑0 : Cauchy abs) : ℝ }.cauchy = cauchy 0

Tactic:
simp [cauchy_zero]

Premises used: Real.cauchy_zero
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
n : ℕ
a : { cauchy := (↑(n + 1) : Cauchy abs) : ℝ }.cauchy = ({ cauchy := (↑n : Cauchy abs) : ℝ } + 1).cauchy
⊢ { cauchy := (↑(n + 1) : Cauchy abs) : ℝ } = { cauchy := (↑n : Cauchy abs) : ℝ } + 1

Tactic:
apply ext_cauchy

Premises used: Real.ext_cauchy
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
n : ℕ
⊢ { cauchy := (↑(n + 1) : Cauchy abs) : ℝ }.cauchy = ({ cauchy := (↑n : Cauchy abs) : ℝ } + 1).cauchy

Tactic:
simp [cauchy_one, cauchy_add]

Premises used: Real.cauchy_add, Real.cauchy_one
-- Module: Mathlib.Data.Real.Basic
Goal:
x a : ℝ
a₁ : (-a + a).cauchy = cauchy 0
⊢ -a + a = 0

Tactic:
apply ext_cauchy

Premises used: Real.ext_cauchy
-- Module: Mathlib.Data.Real.Basic
Goal:
x a : ℝ
⊢ (-a + a).cauchy = cauchy 0

Tactic:
simp [cauchy_add, cauchy_neg, cauchy_zero]

Premises used: Real.cauchy_neg, Real.cauchy_add, Real.cauchy_zero
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
z : ℕ
a : { cauchy := (↑(Int.negSucc z) : Cauchy abs) : ℝ }.cauchy = cauchy (-(↑(z + 1) : ℝ))
⊢ { cauchy := (↑(Int.negSucc z) : Cauchy abs) : ℝ } = -(↑(z + 1) : ℝ)

Tactic:
apply ext_cauchy

Premises used: Real.ext_cauchy
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
z : ℕ
⊢ { cauchy := (↑(Int.negSucc z) : Cauchy abs) : ℝ }.cauchy = cauchy (-(↑(z + 1) : ℝ))

Tactic:
simp [cauchy_neg, cauchy_natCast]

Premises used: Real.cauchy_natCast, Real.cauchy_neg
-- Module: Mathlib.Data.Real.Basic
Goal:
x a b : ℝ
a₁ : (a * b).cauchy = (b * a).cauchy
⊢ a * b = b * a

Tactic:
apply ext_cauchy

Premises used: Real.ext_cauchy
-- Module: Mathlib.Data.Real.Basic
Goal:
x a b : ℝ
⊢ (a * b).cauchy = (b * a).cauchy

Tactic:
simp only [cauchy_mul, mul_comm]

Premises used: mul_comm, Real.cauchy_mul
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
⊢ Ring ℝ

Tactic:
infer_instance
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
⊢ CommSemiring ℝ

Tactic:
infer_instance
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
⊢ Semiring ℝ

Tactic:
infer_instance
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
⊢ CommMonoidWithZero ℝ

Tactic:
infer_instance
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
⊢ MonoidWithZero ℝ

Tactic:
infer_instance
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
⊢ AddCommGroup ℝ

Tactic:
infer_instance
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
⊢ AddGroup ℝ

Tactic:
infer_instance
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
⊢ AddCommMonoid ℝ

Tactic:
infer_instance
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
⊢ AddMonoid ℝ

Tactic:
infer_instance
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
⊢ AddLeftCancelSemigroup ℝ

Tactic:
infer_instance
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
⊢ AddRightCancelSemigroup ℝ

Tactic:
infer_instance
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
⊢ AddCommSemigroup ℝ

Tactic:
infer_instance
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
⊢ AddSemigroup ℝ

Tactic:
infer_instance
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
⊢ CommMonoid ℝ

Tactic:
infer_instance
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
⊢ Monoid ℝ

Tactic:
infer_instance
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
⊢ CommSemigroup ℝ

Tactic:
infer_instance
-- Module: Mathlib.Data.Real.Basic
Goal:
x : ℝ
⊢ Semigroup ℝ

Tactic:
infer_instance
-- Module: Mathlib.Data.Real.Basic
Goal:
f g : CauSeq ℚ abs
⊢ mk f = mk g ↔ f ≈ g

Tactic:
ext_cauchy_iff.trans CauSeq.Completion.mk_eq

Premises used: Iff.trans, CauSeq.Completion.mk_eq, Real.ext_cauchy_iff
-- Module: Mathlib.Data.Real.Basic
Goal:
f g : CauSeq ℚ abs
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
⊢ { cauchy := ⟦f⟧ }.lt { cauchy := ⟦g⟧ } ↔ f < g

Tactic:
rw [lt_def]

Premises used: _private.0.Real.lt_def
-- Module: Mathlib.Data.Real.Basic
Goal:
f g : CauSeq ℚ abs
⊢ (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:
rfl
-- Module: Mathlib.Data.Real.Basic
Goal:
f g : CauSeq ℚ abs
⊢ mk f < mk g ↔ f < g

Tactic:
lt_cauchy

Premises used: Real.lt_cauchy, CauSeq.Completion.mk, Real.mk
-- Module: Mathlib.Data.Real.Basic
Goal:
rw : mk 0 = { cauchy := 0 }
⊢ mk 0 = 0

Tactic:
rw [← ofCauchy_zero]

Premises used: Real.ofCauchy_zero
-- Module: Mathlib.Data.Real.Basic
Goal:
⊢ mk 0 = { cauchy := 0 }

Tactic:
rfl
-- Module: Mathlib.Data.Real.Basic
Goal:
rw : mk 1 = { cauchy := 1 }
⊢ mk 1 = 1

Tactic:
rw [← ofCauchy_one]

Premises used: Real.ofCauchy_one
-- Module: Mathlib.Data.Real.Basic
Goal:
⊢ mk 1 = { cauchy := 1 }

Tactic:
rfl
-- Module: Mathlib.Data.Real.Basic
Goal:
f g : CauSeq ℚ abs
⊢ mk (f + g) = mk f + mk g

Tactic:
simp [mk, ← ofCauchy_add]

Premises used: Real.ofCauchy_add, Real.mk
-- Module: Mathlib.Data.Real.Basic
Goal:
f g : CauSeq ℚ abs
⊢ mk (f * g) = mk f * mk g

Tactic:
simp [mk, ← ofCauchy_mul]

Premises used: Real.ofCauchy_mul, Real.mk
-- Module: Mathlib.Data.Real.Basic
Goal:
f : CauSeq ℚ abs
⊢ mk (-f) = -mk f

Tactic:
simp [mk, ← ofCauchy_neg]

Premises used: Real.ofCauchy_neg, Real.mk
-- Module: Mathlib.Data.Real.Basic
Goal:
f : CauSeq ℚ abs
rw : 0 < f ↔ f.Pos
⊢ 0 < mk f ↔ f.Pos

Tactic:
rw [← mk_zero, mk_lt]

Premises used: Real.mk_lt, Real.mk_zero
-- Module: Mathlib.Data.Real.Basic
Goal:
f : CauSeq ℚ abs
⊢ 0 < f ↔ f.Pos

Tactic:
iff_of_eq (congr_arg Pos (sub_zero f))

Premises used: CauSeq.Pos, sub_zero, congr_arg, iff_of_eq