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 : M
n : ℕ
hn : x ≤ HSMul.hSMul (β := M) n 1
num : ℤ
den : ℕ
den_nz : den ≠ 0
reduced : num.natAbs.Coprime den
this : HSMul.hSMul (β := M) num 1 < den • x → num ≤ HMul.hMul (α := ℤ) (↑n : ℤ) (↑den : ℤ)
⊢ Membership.mem (γ := Set ℚ) {r : ℚ | HSMul.hSMul (β := M) r.num 1 < r.den • x}
      { num := num, den := den, den_nz := den_nz, reduced := reduced : ℚ } →
    { num := num, den := den, den_nz := den_nz, reduced := reduced : ℚ }.num * (↑(Rat.den (↑n : ℚ)) : ℤ) ≤
      Rat.num (↑n : ℚ) * (↑{ num := num, den := den, den_nz := den_nz, reduced := reduced }.den : ℤ)

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 : M
n : ℕ
hn : x ≤ HSMul.hSMul (β := M) n 1
num : ℤ
den : ℕ
den_nz : den ≠ 0
reduced : num.natAbs.Coprime den
h : HSMul.hSMul (β := M) num 1 < den • x → num ≤ HMul.hMul (α := ℤ) (↑n : ℤ) (↑den : ℤ)
⊢ Membership.mem (γ := Set ℚ) {r : ℚ | HSMul.hSMul (β := M) r.num 1 < r.den • x}
      { num := num, den := den, den_nz := den_nz, reduced := reduced : ℚ } →
    { num := num, den := den, den_nz := den_nz, reduced := reduced : ℚ }.num * (↑(Rat.den (↑n : ℚ)) : ℤ) ≤
      Rat.num (↑n : ℚ) * (↑{ num := num, den := den, den_nz := den_nz, reduced := reduced }.den : ℤ)

Tactic:
suffices num • 1 < den • x → num ≤ n * den 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 : M
n : ℕ
hn : x ≤ HSMul.hSMul (β := M) n 1
num : ℤ
den : ℕ
den_nz : den ≠ 0
reduced : num.natAbs.Coprime den
h : HSMul.hSMul (β := M) num 1 < den • x
⊢ x ≤ HSMul.hSMul (α := ℤ) (β := M) (↑n : ℤ) 1

Tactic:
simpa using hn
-- 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
n : ℕ
hn : x ≤ HSMul.hSMul (β := M) n 1
num : ℤ
den : ℕ
den_nz : den ≠ 0
reduced : num.natAbs.Coprime den
h : HSMul.hSMul (β := M) num 1 < den • x
⊢ num ≤ HMul.hMul (α := ℤ) (↑n : ℤ) (↑den : ℤ)

Tactic:
exact num_le_nat_mul_den h.le (by simpa using hn)

Premises used: LT.lt.le, num_le_nat_mul_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 : M
inl : ∀ (hneg : x < 0), (ratLt x).Nonempty
inr : (ratLt.{u_1} (M := M) 0).Nonempty
inr₁ : ∀ (hxpos : 0 < x), (ratLt x).Nonempty
⊢ (ratLt x).Nonempty

Tactic:
obtain hneg | rfl | hxpos := lt_trichotomy x 0

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- 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
hneg : x < 0
inl : ∀ (n : ℕ) (hn : -x - x ≤ HSMul.hSMul (β := M) n 1), (ratLt x).Nonempty
⊢ (ratLt x).Nonempty

Tactic:
obtain ⟨n, hn⟩ := Archimedean.arch (-x - x) zero_lt_one

Premises used: HSub.hSub, zero_lt_one, Archimedean.arch, Neg.neg
-- 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
hneg : x < 0
n : ℕ
hn : -x - x ≤ HSMul.hSMul (β := M) n 1
h : Rat.ofInt (-(↑n : ℤ)) ∈ ratLt x
⊢ (ratLt x).Nonempty

Tactic:
use Rat.ofInt (-n)

Premises used: Nat.cast, Rat.ofInt, Neg.neg
-- 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
hneg : x < 0
n : ℕ
hn : -x - x ≤ HSMul.hSMul (β := M) n 1
this : -HSMul.hSMul (β := M) n 1 < x
⊢ Rat.ofInt (-(↑n : ℤ)) ∈ ratLt 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 : M
hneg : x < 0
n : ℕ
hn : -x - x ≤ HSMul.hSMul (β := M) n 1
h : -HSMul.hSMul (β := M) n 1 < x
⊢ Rat.ofInt (-(↑n : ℤ)) ∈ ratLt x

Tactic:
suffices -(n • 1) < 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 : M
hneg : x < 0
n : ℕ
hn : -x - x ≤ HSMul.hSMul (β := M) n 1
⊢ -x < -x - x

Tactic:
simpa using hneg
-- 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
hneg : x < 0
n : ℕ
hn : -x - x ≤ HSMul.hSMul (β := M) n 1
⊢ -HSMul.hSMul (β := M) n 1 < x

Tactic:
exact neg_lt.mpr (lt_of_lt_of_le (by simpa using hneg) hn)

Premises used: Iff.mpr, neg_lt, lt_of_lt_of_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
⊢ Rat.ofInt (-1) ∈ ratLt.{u_1} (M := M) 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
⊢ (ratLt.{u_1} (M := M) 0).Nonempty

Tactic:
exact ⟨Rat.ofInt (-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 : M
hxpos : 0 < x
inr : ∀ (n : ℕ) (hn : 1 ≤ n • x), (ratLt x).Nonempty
⊢ (ratLt x).Nonempty

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

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 : M
hxpos : 0 < x
n : ℕ
hn : 1 ≤ n • 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 : M
hxpos : 0 < x
n : ℕ
hn : 1 ≤ n • 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 : M
hxpos : 0 < x
n : ℕ
hn : 1 ≤ n • x
h : { num := 1, den := n + 1, den_nz := ⋯, reduced := ⋯ : ℚ } ∈ ratLt x
⊢ (ratLt x).Nonempty

Tactic:
use Rat.mk' 1 (n + 1) (by simp) (by simp)

Premises used: HAdd.hAdd, Rat.mk', 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 : M
hxpos : 0 < x
n : ℕ
hn : 1 ≤ n • 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 : M
hxpos : 0 < x
n : ℕ
hn : 1 ≤ n • x
⊢ { num := 1, den := n + 1, den_nz := ⋯, reduced := ⋯ : ℚ } ∈ ratLt x

Tactic:
simpa using hn.trans_lt <| (nsmul_lt_nsmul_iff_left hxpos).mpr (by simp)

Premises used: Iff.mpr, nsmul_lt_nsmul_iff_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 : ∀ (a : ℚ), a ∈ ratLt (x + y) ↔ a ∈ ratLt x + ratLt y
⊢ ratLt (x + y) = ratLt x + ratLt y

Tactic:
ext a
-- 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 : a ∈ ratLt (x + y) → ∃ x_1 ∈ ratLt x, ∃ y_1 ∈ ratLt y, x_1 + y_1 = a
h₁ : (∃ x_1 ∈ ratLt x, ∃ y_1 ∈ ratLt y, x_1 + y_1 = a) → a ∈ ratLt (x + y)
⊢ a ∈ ratLt (x + y) ↔ ∃ x_1 ∈ ratLt x, ∃ y_1 ∈ ratLt y, x_1 + y_1 = a

Tactic:
constructor
-- 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 : a ∈ ratLt (x + y)
⊢ HSMul.hSMul (β := M) a.num 1 < a.den • (x + y)

Tactic:
rw [Set.mem_setOf_eq] at h

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 : ℚ
h : HSMul.hSMul (β := M) a.num 1 < a.den • (x + y)
h₁ :
  ∀ (k : ℕ) (hk : HAdd.hAdd (α := M) 1 1 ≤ k • (a.den • (x + y) - HSMul.hSMul (β := M) a.num 1)),
    ∃ x_1 ∈ ratLt x, ∃ y_1 ∈ ratLt y, x_1 + y_1 = a
⊢ ∃ x_1 ∈ ratLt x, ∃ y_1 ∈ ratLt y, x_1 + y_1 = a

Tactic:
obtain ⟨k, hk⟩ := Archimedean.arch (1 + 1) <| sub_pos.mpr h

Premises used: Iff.mpr, sub_pos, HAdd.hAdd, 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
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)
contrapose! : ∀ (hk : k = 0), k • (a.den • (x + y) - HSMul.hSMul (β := M) a.num 1) < HAdd.hAdd (α := M) 1 1
⊢ k ≠ 0

Tactic:
contrapose! hk
-- 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 : k = 0
⊢ k • (a.den • (x + y) - HSMul.hSMul (β := M) a.num 1) < HAdd.hAdd (α := M) 1 1

Tactic:
simp [hk]
-- 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)
⊢ k ≠ 0

Tactic:
have hk0 : k ≠ 0 := by
      contrapose! hk
      simp [hk]
-- 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
⊢ k * a.den ≠ 0

Tactic:
have hka0 : k * a.den ≠ 0 := mul_ne_zero hk0 a.den_ne_zero
-- 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
h₁ :
  ∀ (m : ℤ),
    (∀ (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), ∃ x_1 ∈ ratLt x, ∃ y_1 ∈ ratLt y, x_1 + y_1 = a
⊢ ∃ x_1 ∈ ratLt x, ∃ y_1 ∈ ratLt y, x_1 + y_1 = a

Tactic:
obtain ⟨m, ⟨hm1, hm2⟩, _⟩ := existsUnique_add_zsmul_mem_Ico zero_lt_one 0 (k • a.den • x - 1)

Premises used: HSub.hSub, Rat.den, existsUnique_add_zsmul_mem_Ico, zero_lt_one, HSMul.hSMul, 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
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
⊢ ∃ x_1 ∈ ratLt x, ∃ y_1 ∈ ratLt y, x_1 + y_1 = a

Tactic:
⟨mkRat m (k * a.den), ?_, mkRat (k * a.num - m) (k * a.den), ?_, ?_⟩

Premises used: Rat.num, HMul.hMul, HSub.hSub, Rat.den, Nat.cast, mkRat, And.intro, Exists.intro
-- 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.den) ∈ ratLt x
h₂ : mkRat ((↑k : ℤ) * a.num - m) (k * a.den) ∈ ratLt y
h₃ : mkRat m (k * a.den) + mkRat ((↑k : ℤ) * a.num - m) (k * a.den) = a
⊢ ∃ x_1 ∈ ratLt x, ∃ y_1 ∈ ratLt y, x_1 + y_1 = a

Tactic:
refine ⟨mkRat m (k * a.den), ?_, mkRat (k * a.num - m) (k * a.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₁ : HSMul.hSMul (β := M) m 1 < k • a.den • x
⊢ mkRat m (k * a.den) ∈ ratLt x

Tactic:
rw [mkRat_mem_ratLt hka0, ← smul_smul]

Premises used: smul_smul, Archimedean.mkRat_mem_ratLt
-- 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
⊢ HSMul.hSMul (β := M) m 1 < k • a.den • x

Tactic:
simpa using hm2
-- 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
rw :
  ∀ (hk : HAdd.hAdd (α := M) 1 1 + k • HSMul.hSMul (β := M) a.num 1 - k • a.den • y ≤ k • a.den • x) (hk0 : k ≠ 0)
    (hka0 : k * a.den ≠ 0) (m : ℤ),
    (∀ (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),
        1 + (k • HSMul.hSMul (β := M) a.num 1 - k • a.den • y) ≤ k • a.den • x - 1
⊢ 1 + (k • HSMul.hSMul (β := M) a.num 1 - k • a.den • y) ≤ k • a.den • x - 1

Tactic:
rw [smul_add, smul_sub, smul_add, le_sub_iff_add_le, ← sub_le_iff_le_add] at hk

Premises used: sub_le_iff_le_add, smul_sub, le_sub_iff_add_le, 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 : ℚ
h : HSMul.hSMul (β := M) a.num 1 < a.den • (x + y)
k : ℕ
hk : HAdd.hAdd (α := M) 1 1 + k • HSMul.hSMul (β := M) a.num 1 - k • a.den • y ≤ k • a.den • x
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
rw : 1 + (k • HSMul.hSMul (β := M) a.num 1 - k • a.den • y) + 1 ≤ k • a.den • x
⊢ 1 + (k • HSMul.hSMul (β := M) a.num 1 - k • a.den • y) ≤ k • a.den • x - 1

Tactic:
rw [le_sub_iff_add_le]

Premises used: le_sub_iff_add_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 y : M
a : ℚ
h : HSMul.hSMul (β := M) a.num 1 < a.den • (x + y)
k : ℕ
hk : HAdd.hAdd (α := M) 1 1 + k • HSMul.hSMul (β := M) a.num 1 - k • a.den • y ≤ k • a.den • x
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
⊢ HAdd.hAdd (α := M) 1 1 + k • HSMul.hSMul (β := M) a.num 1 - k • a.den • y ≤ k • a.den • x

Tactic:
hk
-- 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 • HSMul.hSMul (β := M) a.num 1 - k • a.den • y ≤ k • a.den • x
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₁ :
  1 + (k • HSMul.hSMul (β := M) a.num 1 - k • a.den • y) + 1 =
    HAdd.hAdd (α := M) 1 1 + k • HSMul.hSMul (β := M) a.num 1 - k • a.den • y
⊢ 1 + (k • HSMul.hSMul (β := M) a.num 1 - k • a.den • y) + 1 ≤ k • a.den • x

Tactic:
convert! hk using 1
-- 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 • HSMul.hSMul (β := M) a.num 1 - k • a.den • y ≤ k • a.den • x
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
⊢ 1 + (k • HSMul.hSMul (β := M) a.num 1 - k • a.den • y) + 1 =
    HAdd.hAdd (α := M) 1 1 + k • HSMul.hSMul (β := M) a.num 1 - k • a.den • y

Tactic:
abel
-- 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
⊢ 1 + (k • HSMul.hSMul (β := M) a.num 1 - k • a.den • y) ≤ k • a.den • x - 1

Tactic:
have hk' : 1 + (k • a.num • 1 - k • a.den • y) ≤ k • a.den • x - 1 := by
        rw [smul_add, smul_sub, smul_add, le_sub_iff_add_le, ← sub_le_iff_le_add] at hk
        rw [le_sub_iff_add_le]
        convert! hk using 1
        abel
-- 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
⊢ 1 + (k • HSMul.hSMul (β := M) a.num 1 - k • a.den • y) ≤ HSMul.hSMul (β := M) m 1

Tactic:
simpa using hk'.trans hm1

Premises used: LE.le.trans