awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x y : M
a : ℚ
h : HSMul.hSMul (β := M) a.num 1 < a.den • (x + y)
k : ℕ
hk : HAdd.hAdd (α := M) 1 1 ≤ k • (a.den • (x + y) - HSMul.hSMul (β := M) a.num 1)
hk0 : k ≠ 0
hka0 : k * a.den ≠ 0
m : ℤ
right :
  ∀ (y : ℤ),
    (fun (m : ℤ) ↦ 0 + HSMul.hSMul (β := M) m 1 ∈ Set.Ico (k • a.den • x - 1) (k • a.den • x - 1 + 1)) y → y = m
hm1 : k • a.den • x - 1 ≤ 0 + HSMul.hSMul (β := M) m 1
hm2 : 0 + HSMul.hSMul (β := M) m 1 < k • a.den • x - 1 + 1
hk' : 1 + (k • HSMul.hSMul (β := M) a.num 1 - k • a.den • y) ≤ k • a.den • x - 1
⊢ k • HSMul.hSMul (β := M) a.num 1 - k • a.den • y < HSMul.hSMul (β := M) m 1

Tactic:
have : k • a.num • 1 - k • a.den • y < m • 1 :=
        lt_of_lt_of_le (lt_add_of_pos_left _ zero_lt_one) (by simpa using hk'.trans hm1)
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x y : M
a : ℚ
h : HSMul.hSMul (β := M) a.num 1 < a.den • (x + y)
k : ℕ
hk : HAdd.hAdd (α := M) 1 1 ≤ k • (a.den • (x + y) - HSMul.hSMul (β := M) a.num 1)
hk0 : k ≠ 0
hka0 : k * a.den ≠ 0
m : ℤ
right :
  ∀ (y : ℤ),
    (fun (m : ℤ) ↦ 0 + HSMul.hSMul (β := M) m 1 ∈ Set.Ico (k • a.den • x - 1) (k • a.den • x - 1 + 1)) y → y = m
hm1 : k • a.den • x - 1 ≤ 0 + HSMul.hSMul (β := M) m 1
hm2 : 0 + HSMul.hSMul (β := M) m 1 < k • a.den • x - 1 + 1
hk' : 1 + (k • HSMul.hSMul (β := M) a.num 1 - k • a.den • y) ≤ k • a.den • x - 1
this : k • HSMul.hSMul (β := M) a.num 1 - k • a.den • y < HSMul.hSMul (β := M) m 1
h₁ : k • HSMul.hSMul (β := M) a.num 1 - k • a.den • y < HSMul.hSMul (β := M) m 1
⊢ mkRat ((↑k : ℤ) * a.num - m) (k * a.den) ∈ ratLt y

Tactic:
rw [mkRat_mem_ratLt hka0, sub_smul, sub_lt_comm, ← smul_smul, ← smul_smul, natCast_zsmul]

Premises used: sub_lt_comm, sub_smul, smul_smul, Archimedean.mkRat_mem_ratLt, natCast_zsmul
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x y : M
a : ℚ
h : HSMul.hSMul (β := M) a.num 1 < a.den • (x + y)
k : ℕ
hk : HAdd.hAdd (α := M) 1 1 ≤ k • (a.den • (x + y) - HSMul.hSMul (β := M) a.num 1)
hk0 : k ≠ 0
hka0 : k * a.den ≠ 0
m : ℤ
right :
  ∀ (y : ℤ),
    (fun (m : ℤ) ↦ 0 + HSMul.hSMul (β := M) m 1 ∈ Set.Ico (k • a.den • x - 1) (k • a.den • x - 1 + 1)) y → y = m
hm1 : k • a.den • x - 1 ≤ 0 + HSMul.hSMul (β := M) m 1
hm2 : 0 + HSMul.hSMul (β := M) m 1 < k • a.den • x - 1 + 1
hk' : 1 + (k • HSMul.hSMul (β := M) a.num 1 - k • a.den • y) ≤ k • a.den • x - 1
this : k • HSMul.hSMul (β := M) a.num 1 - k • a.den • y < HSMul.hSMul (β := M) m 1
⊢ k • HSMul.hSMul (β := M) a.num 1 - k • a.den • y < HSMul.hSMul (β := M) m 1

Tactic:
this
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x y : M
a : ℚ
h : HSMul.hSMul (β := M) a.num 1 < a.den • (x + y)
k : ℕ
hk : HAdd.hAdd (α := M) 1 1 ≤ k • (a.den • (x + y) - HSMul.hSMul (β := M) a.num 1)
hk0 : k ≠ 0
hka0 : k * a.den ≠ 0
m : ℤ
right :
  ∀ (y : ℤ),
    (fun (m : ℤ) ↦ 0 + HSMul.hSMul (β := M) m 1 ∈ Set.Ico (k • a.den • x - 1) (k • a.den • x - 1 + 1)) y → y = m
hm1 : k • a.den • x - 1 ≤ 0 + HSMul.hSMul (β := M) m 1
hm2 : 0 + HSMul.hSMul (β := M) m 1 < k • a.den • x - 1 + 1
hk' : 1 + (k • HSMul.hSMul (β := M) a.num 1 - k • a.den • y) ≤ k • a.den • x - 1
this : k • HSMul.hSMul (β := M) a.num 1 - k • a.den • y < HSMul.hSMul (β := M) m 1
⊢ k • HSMul.hSMul (β := M) a.num 1 - k • a.den • y < HSMul.hSMul (β := M) m 1

Tactic:
exact this
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x y : M
a : ℚ
h : HSMul.hSMul (β := M) a.num 1 < a.den • (x + y)
k : ℕ
hk : HAdd.hAdd (α := M) 1 1 ≤ k • (a.den • (x + y) - HSMul.hSMul (β := M) a.num 1)
hk0 : k ≠ 0
hka0 : k * a.den ≠ 0
m : ℤ
right :
  ∀ (y : ℤ),
    (fun (m : ℤ) ↦ 0 + HSMul.hSMul (β := M) m 1 ∈ Set.Ico (k • a.den • x - 1) (k • a.den • x - 1 + 1)) y → y = m
hm1 : k • a.den • x - 1 ≤ 0 + HSMul.hSMul (β := M) m 1
hm2 : 0 + HSMul.hSMul (β := M) m 1 < k • a.den • x - 1 + 1
h₁ : mkRat (m + ((↑k : ℤ) * a.num - m)) (k * a.den) = a
⊢ mkRat m (k * a.den) + mkRat ((↑k : ℤ) * a.num - m) (k * a.den) = a

Tactic:
rw [Rat.mkRat_add_mkRat_of_den _ _ hka0]

Premises used: Rat.mkRat_add_mkRat_of_den
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x y : M
a : ℚ
h : HSMul.hSMul (β := M) a.num 1 < a.den • (x + y)
k : ℕ
hk : HAdd.hAdd (α := M) 1 1 ≤ k • (a.den • (x + y) - HSMul.hSMul (β := M) a.num 1)
hk0 : k ≠ 0
hka0 : k * a.den ≠ 0
m : ℤ
right :
  ∀ (y : ℤ),
    (fun (m : ℤ) ↦ 0 + HSMul.hSMul (β := M) m 1 ∈ Set.Ico (k • a.den • x - 1) (k • a.den • x - 1 + 1)) y → y = m
hm1 : k • a.den • x - 1 ≤ 0 + HSMul.hSMul (β := M) m 1
hm2 : 0 + HSMul.hSMul (β := M) m 1 < k • a.den • x - 1 + 1
h₁ : mkRat ((↑k : ℤ) * a.num) (k * a.den) = a
h₂ : mkRat a.num a.den = a
h₃ h₄ : a = a
⊢ mkRat (m + ((↑k : ℤ) * a.num - m)) (k * a.den) = a

Tactic:
rw [add_sub_cancel, Rat.mkRat_mul_left hk0, Rat.mkRat_num_den']

Premises used: Rat.mkRat_num_den', Rat.mkRat_mul_left, add_sub_cancel
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x y : M
a u : ℚ
hu : u ∈ ratLt x
v : ℚ
hv : v ∈ ratLt y
huv : u + v = a
h : u + v ∈ ratLt (x + y)
⊢ a ∈ ratLt (x + y)

Tactic:
rw [← huv]
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x y : M
a u : ℚ
hu : u ∈ ratLt x
v : ℚ
hv : v ∈ ratLt y
huv : u + v = a
h :
  ∀ (hu : HSMul.hSMul (β := M) u.num 1 < u.den • x) (v : ℚ) (hv : HSMul.hSMul (β := M) v.num 1 < v.den • y)
    (huv : u + v = a), HSMul.hSMul (β := M) (u + v).num 1 < (u + v).den • (x + y)
⊢ u + v ∈ ratLt (x + y)

Tactic:
rw [Set.mem_setOf_eq] at hu hv ⊢

Premises used: Set.mem_setOf_eq
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x y : M
a u : ℚ
hu : HSMul.hSMul (β := M) u.num 1 < u.den • x
v : ℚ
hv : HSMul.hSMul (β := M) v.num 1 < v.den • y
huv : u + v = a
⊢ HSMul.hSMul (β := M) (u + v).num 1 < (u + v).den • (x + y)

Tactic:
num_smul_one_lt_den_smul_add hu hv

Premises used: num_smul_one_lt_den_smul_add
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x y : M
a u : ℚ
hu : HSMul.hSMul (β := M) u.num 1 < u.den • x
v : ℚ
hv : HSMul.hSMul (β := M) v.num 1 < v.den • y
huv : u + v = a
⊢ HSMul.hSMul (β := M) (u + v).num 1 < (u + v).den • (x + y)

Tactic:
exact num_smul_one_lt_den_smul_add hu hv

Premises used: num_smul_one_lt_den_smul_add
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x : M
⊢ BddAbove (ratLt' x)

Tactic:
Monotone.map_bddAbove Rat.cast_mono <| ratLt_bddAbove x

Premises used: Monotone.map_bddAbove, Rat.cast_mono, Archimedean.ratLt_bddAbove
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x : M
⊢ (ratLt' x).Nonempty

Tactic:
Set.image_nonempty.mpr (ratLt_nonempty x)

Premises used: Iff.mpr, Set.image_nonempty, Archimedean.ratLt_nonempty
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x y : M
rw : (⇑(Rat.castHom ℝ) : (a : ℚ) → ℝ) '' ratLt (x + y) = ratLt' x + ratLt' y
rw₁ : (⇑(Rat.castHom ℝ) : (a : ℚ) → ℝ) '' (ratLt x + ratLt y) = ratLt' x + ratLt' y
rw₂ rw₃ :
  HAdd.hAdd (α := Set ℝ) ((⇑(Rat.castHom ℝ) : (a : ℚ) → ℝ) '' ratLt x) ((⇑(Rat.castHom ℝ) : (a : ℚ) → ℝ) '' ratLt y) =
    ratLt' x + ratLt' y
⊢ ratLt' (x + y) = ratLt' x + ratLt' y

Tactic:
rw [ratLt', ratLt_add, Set.image_add]

Premises used: Archimedean.ratLt', Archimedean.ratLt_add, Set.image_add
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
a : embedRealFun.{u_1} (M := M) 0 ≤ 0
a₁ : 0 ≤ embedRealFun.{u_1} (M := M) 0
⊢ embedRealFun.{u_1} (M := M) 0 = 0

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
a : ∀ b ∈ ratLt'.{u_1} (M := M) 0, b ≤ 0
⊢ embedRealFun.{u_1} (M := M) 0 ≤ 0

Tactic:
apply csSup_le (ratLt'_nonempty 0)

Premises used: Archimedean.ratLt'_nonempty, OfNat.ofNat, csSup_le
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x : ℝ
this : ∀ (y : ℚ), HSMul.hSMul (β := M) y.num 1 < 0 → (↑y : ℝ) = x → x ≤ 0
⊢ Membership.mem (γ := Set ℝ)
      (Set.image (α := ℚ) (⇑(Rat.castHom ℝ) : (a : ℚ) → ℝ)
        {r : ℚ | HSMul.hSMul (β := M) r.num 1 < HSMul.hSMul (β := M) r.den 0})
      x →
    x ≤ 0

Tactic:
simpa using this
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x : ℝ
a : ∀ (y : ℚ), HSMul.hSMul (β := M) y.num 1 < 0 → (↑y : ℝ) = x → x ≤ 0
⊢ Membership.mem (γ := Set ℝ)
      (Set.image (α := ℚ) (⇑(Rat.castHom ℝ) : (a : ℚ) → ℝ)
        {r : ℚ | HSMul.hSMul (β := M) r.num 1 < HSMul.hSMul (β := M) r.den 0})
      x →
    x ≤ 0

Tactic:
suffices ∀ (y : ℚ), y.num • (1 : M) < 0 → y = x → x ≤ 0 by simpa using this
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x : ℝ
y : ℚ
hy : HSMul.hSMul (β := M) y.num 1 < 0
hyx : (↑y : ℝ) = x
a : y.num ≤ 0
⊢ x ≤ 0

Tactic:
rw [← hyx, Rat.cast_nonpos, ← Rat.num_nonpos]

Premises used: Rat.cast_nonpos, Rat.num_nonpos
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x : ℝ
y : ℚ
hy : HSMul.hSMul (β := M) y.num 1 < 0
hyx : (↑y : ℝ) = x
⊢ y.num ≤ 0

Tactic:
(neg_of_smul_neg_right hy zero_le_one).le

Premises used: LT.lt.le, neg_of_smul_neg_right, zero_le_one
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x : ℝ
y : ℚ
hy : HSMul.hSMul (β := M) y.num 1 < 0
hyx : (↑y : ℝ) = x
⊢ y.num ≤ 0

Tactic:
exact (neg_of_smul_neg_right hy zero_le_one).le

Premises used: LT.lt.le, neg_of_smul_neg_right, zero_le_one
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
a : ∀ b ∈ upperBounds (ratLt'.{u_1} (M := M) 0), 0 ≤ b
⊢ 0 ≤ embedRealFun.{u_1} (M := M) 0

Tactic:
rw [le_csSup_iff (ratLt'_bddAbove (0 : M)) (ratLt'_nonempty 0)]

Premises used: le_csSup_iff, Archimedean.ratLt'_nonempty, OfNat.ofNat, Archimedean.ratLt'_bddAbove
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x : ℝ
this : (∀ (y : ℚ), HSMul.hSMul (β := M) y.num 1 < 0 → (↑y : ℝ) ≤ x) → 0 ≤ x
⊢ (∀ x_1 ∈ ratLt'.{u_1} (M := M) 0, x_1 ≤ x) → 0 ≤ x

Tactic:
simpa using this
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x : ℝ
a : (∀ (y : ℚ), HSMul.hSMul (β := M) y.num 1 < 0 → (↑y : ℝ) ≤ x) → 0 ≤ x
⊢ (∀ x_1 ∈ ratLt'.{u_1} (M := M) 0, x_1 ≤ x) → 0 ≤ x

Tactic:
suffices (∀ (y : ℚ), y.num • (1 : M) < 0 → y ≤ x) → 0 ≤ x by simpa using this
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x : ℝ
h : ∀ (y : ℚ), HSMul.hSMul (β := M) y.num 1 < 0 → (↑y : ℝ) ≤ x
y : ℚ
hy : y < 0
⊢ y.num < 0

Tactic:
simpa using hy
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x : ℝ
h : ∀ (y : ℚ), HSMul.hSMul (β := M) y.num 1 < 0 → (↑y : ℝ) ≤ x
y : ℚ
hy : y < 0
⊢ (↑y : ℝ) ≤ x

Tactic:
exact h _ <| (smul_neg_iff_of_neg_left (by simpa using hy)).mpr zero_lt_one

Premises used: Iff.mpr, zero_lt_one, smul_neg_iff_of_neg_left
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x : ℝ
h : ∀ (y : ℚ), HSMul.hSMul (β := M) y.num 1 < 0 → (↑y : ℝ) ≤ x
⊢ ∀ (y : ℚ) (hy : y < 0), (↑y : ℝ) ≤ x

Tactic:
have h' (y : ℚ) (hy : y < 0) : y ≤ x := by
      exact h _ <| (smul_neg_iff_of_neg_left (by simpa using hy)).mpr zero_lt_one
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x : ℝ
h : ∀ (y : ℚ), HSMul.hSMul (β := M) y.num 1 < 0 → (↑y : ℝ) ≤ x
h' : ∀ (y : ℚ) (hy : y < 0), (↑y : ℝ) ≤ x
a : ∀ (h' : x < 0), ∃ y < 0, x < (↑y : ℝ)
⊢ 0 ≤ x

Tactic:
contrapose! h'
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x : ℝ
h : ∀ (y : ℚ), HSMul.hSMul (β := M) y.num 1 < 0 → (↑y : ℝ) ≤ x
h' : x < 0
a : ∀ (y : ℚ) (hxy : x < (↑y : ℝ)) (hy : LT.lt (α := ℝ) (↑y : ℝ) 0), ∃ y < 0, x < (↑y : ℝ)
⊢ ∃ y < 0, x < (↑y : ℝ)

Tactic:
obtain ⟨y, hxy, hy⟩ := exists_rat_btwn h'

Premises used: exists_rat_btwn
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x : ℝ
h : ∀ (y : ℚ), HSMul.hSMul (β := M) y.num 1 < 0 → (↑y : ℝ) ≤ x
h' : x < 0
y : ℚ
hxy : x < (↑y : ℝ)
hy : LT.lt (α := ℝ) (↑y : ℝ) 0
⊢ y < 0

Tactic:
simpa using hy
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x : ℝ
h : ∀ (y : ℚ), HSMul.hSMul (β := M) y.num 1 < 0 → (↑y : ℝ) ≤ x
h' : x < 0
y : ℚ
hxy : x < (↑y : ℝ)
hy : LT.lt (α := ℝ) (↑y : ℝ) 0
⊢ ∃ y < 0, x < (↑y : ℝ)

Tactic:
exact ⟨y, by simpa using hy, hxy⟩
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x y : M
rw : sSup (ratLt' (x + y)) = embedRealFun x + embedRealFun y
rw₁ : sSup (ratLt' x + ratLt' y) = embedRealFun x + embedRealFun y
rw₂ rw₃ : sSup (ratLt' x) + sSup (ratLt' y) = embedRealFun x + embedRealFun y
⊢ embedRealFun (x + y) = embedRealFun x + embedRealFun y

Tactic:
rw [embedRealFun, ratLt'_add, csSup_add (ratLt'_nonempty x) (ratLt'_bddAbove x)
    (ratLt'_nonempty y) (ratLt'_bddAbove y)]

Premises used: Archimedean.embedRealFun, Archimedean.ratLt'_nonempty, csSup_add, Archimedean.ratLt'_add, Archimedean.ratLt'_bddAbove
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x y : M
h : x < y
⊢ 0 < y - x

Tactic:
have hyz : 0 < y - x := sub_pos.mpr h
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x y : M
h : x < y
hyz : 0 < y - x
⊢ y = y - x + x

Tactic:
have hy : y = y - x + x := (sub_add_cancel y x).symm
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x y : M
h : x < y
hyz : 0 < y - x
hy : y = y - x + x
a : 0 < embedRealFun y - embedRealFun x
⊢ embedRealFun x < embedRealFun y

Tactic:
apply lt_of_sub_pos

Premises used: lt_of_sub_pos
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x y : M
h : x < y
hyz : 0 < y - x
hy : y = y - x + x
a : 0 < embedRealFun (y - x)
⊢ 0 < embedRealFun y - embedRealFun x

Tactic:
rw [hy, embedRealFun_add, add_sub_cancel_right]

Premises used: Archimedean.embedRealFun_add, add_sub_cancel_right
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x y : M
h : x < y
hyz : 0 < y - x
hy : y = y - x + x
a : ∀ (n : ℕ) (hn : 1 ≤ n • (y - x)), 0 < embedRealFun (y - x)
⊢ 0 < embedRealFun (y - x)

Tactic:
obtain ⟨n, hn⟩ := Archimedean.arch 1 hyz

Premises used: Archimedean.arch, OfNat.ofNat
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x y : M
h : x < y
hyz : 0 < y - x
hy : y = y - x + x
n : ℕ
hn : 1 ≤ n • (y - x)
⊢ n + 1 ≠ 0

Tactic:
simp
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x y : M
h : x < y
hyz : 0 < y - x
hy : y = y - x + x
n : ℕ
hn : 1 ≤ n • (y - x)
⊢ (Int.natAbs 1).Coprime (n + 1)

Tactic:
simp
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x y : M
h : x < y
hyz : 0 < y - x
hy : y = y - x + x
n : ℕ
hn : 1 ≤ n • (y - x)
⊢ n < n + 1

Tactic:
simp
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x y : M
h : x < y
hyz : 0 < y - x
hy : y = y - x + x
n : ℕ
hn : 1 ≤ n • (y - x)
⊢ (↑{ num := 1, den := n + 1, den_nz := ⋯, reduced := ⋯ } : ℝ) ∈ ratLt' (y - x)

Tactic:
simpa using hn.trans_lt <| nsmul_lt_nsmul_left hyz (show n < n + 1 by simp)

Premises used: nsmul_lt_nsmul_left, LE.le.trans_lt
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x y : M
h : x < y
hyz : 0 < y - x
hy : y = y - x + x
n : ℕ
hn : 1 ≤ n • (y - x)
⊢ (↑{ num := 1, den := n + 1, den_nz := ⋯, reduced := ⋯ } : ℝ) ∈ ratLt' (y - x)

Tactic:
have : (Rat.mk' 1 (n + 1) (by simp) (by simp) : ℝ) ∈ ratLt' (y - x) := by
    simpa using hn.trans_lt <| nsmul_lt_nsmul_left hyz (show n < n + 1 by simp)
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x y : M
h : x < y
hyz : 0 < y - x
hy : y = y - x + x
n : ℕ
hn : 1 ≤ n • (y - x)
this : (↑{ num := 1, den := n + 1, den_nz := ⋯, reduced := ⋯ } : ℝ) ∈ ratLt' (y - x)
⊢ LT.lt (α := ℝ) 0 (↑{ num := 1, den := n + 1, den_nz := ⋯, reduced := ⋯ } : ℝ)

Tactic:
simp [← Rat.num_pos]

Premises used: Rat.num_pos
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x y : M
h : x < y
hyz : 0 < y - x
hy : y = y - x + x
n : ℕ
hn : 1 ≤ n • (y - x)
this : (↑{ num := 1, den := n + 1, den_nz := ⋯, reduced := ⋯ } : ℝ) ∈ ratLt' (y - x)
⊢ 0 < embedRealFun (y - x)

Tactic:
exact lt_csSup_of_lt (ratLt'_bddAbove (y - x)) this (by simp [← Rat.num_pos])

Premises used: HSub.hSub, lt_csSup_of_lt, Archimedean.ratLt'_bddAbove
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
a : M
⊢ (embedReal M : (a : M) → ℝ) a = embedRealFun a

Tactic:
rfl
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
⊢ Function.Injective (α := M) (β := ℝ) (⇑(embedReal M) : (a : M) → ℝ)

Tactic:
(embedRealFun_strictMono M).injective

Premises used: dite, StrictMono.injective, Archimedean.embedRealFun_strictMono
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
a : embedRealFun.{u_1} (M := M) 1 ≤ 1
a₁ : 1 ≤ embedRealFun.{u_1} (M := M) 1
⊢ embedRealFun.{u_1} (M := M) 1 = 1

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
a : ∀ b ∈ ratLt'.{u_1} (M := M) 1, b ≤ 1
⊢ embedRealFun.{u_1} (M := M) 1 ≤ 1

Tactic:
apply csSup_le (ratLt'_nonempty 1)

Premises used: Archimedean.ratLt'_nonempty, OfNat.ofNat, csSup_le