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
u v : ℚ
x y : M
hu : HSMul.hSMul (β := M) u.num 1 < u.den • x
hv : HSMul.hSMul (β := M) v.num 1 < v.den • y
hu' : HSMul.hSMul (β := M) (u.num * (↑v.den : ℤ)) 1 < HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) • x
suffices :
  HSMul.hSMul (β := M) ((u + v).num * (↑u.den : ℤ) * (↑v.den : ℤ)) 1 <
    HSMul.hSMul (α := ℤ) (↑(u + v).den : ℤ) (HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) • (x + y))
⊢ HSMul.hSMul (β := M) (u + v).num 1 < (u + v).den • (x + y)

Tactic:
suffices ((u + v).num * u.den * v.den) • 1 <
      ((u + v).den : ℤ) • (u.den * v.den : ℤ) • (x + y) by
    refine (mul_smul_one_lt_iff (mul_pos u.den_pos v.den_pos)).mp ?_
    rwa [Nat.cast_mul, ← mul_assoc, mul_comm _ ((u + v).den : ℤ), ← smul_eq_mul ((u + v).den : ℤ),
      smul_assoc]
-- 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
u v : ℚ
x y : M
hu : HSMul.hSMul (β := M) u.num 1 < u.den • x
hv : HSMul.hSMul (β := M) v.num 1 < v.den • y
hu' : HSMul.hSMul (β := M) (u.num * (↑v.den : ℤ)) 1 < HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) • x
rw :
  HSMul.hSMul (α := ℤ) (↑(u + v).den : ℤ) (HSMul.hSMul (β := M) (u.num * (↑v.den : ℤ) + v.num * (↑u.den : ℤ)) 1) <
    HSMul.hSMul (α := ℤ) (↑(u + v).den : ℤ) (HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) • (x + y))
⊢ HSMul.hSMul (β := M) ((u + v).num * (↑u.den : ℤ) * (↑v.den : ℤ)) 1 <
    HSMul.hSMul (α := ℤ) (↑(u + v).den : ℤ) (HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) • (x + y))

Tactic:
rw [Rat.add_num_den', mul_comm, ← smul_smul]

Premises used: smul_smul, mul_comm, Rat.add_num_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
u v : ℚ
x y : M
hu : HSMul.hSMul (β := M) u.num 1 < u.den • x
hv : HSMul.hSMul (β := M) v.num 1 < v.den • y
hu' : HSMul.hSMul (β := M) (u.num * (↑v.den : ℤ)) 1 < HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) • x
⊢ LT.lt (α := ℤ) 0 (↑(u + v).den : ℤ)

Tactic:
simpa using (u + v).den_pos

Premises used: HAdd.hAdd, Rat.den_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
u v : ℚ
x y : M
hu : HSMul.hSMul (β := M) u.num 1 < u.den • x
hv : HSMul.hSMul (β := M) v.num 1 < v.den • y
hu' : HSMul.hSMul (β := M) (u.num * (↑v.den : ℤ)) 1 < HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) • x
rw :
  HSMul.hSMul (β := M) (u.num * (↑v.den : ℤ) + v.num * (↑u.den : ℤ)) 1 <
    HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) • (x + y)
⊢ HSMul.hSMul (α := ℤ) (↑(u + v).den : ℤ) (HSMul.hSMul (β := M) (u.num * (↑v.den : ℤ) + v.num * (↑u.den : ℤ)) 1) <
    HSMul.hSMul (α := ℤ) (↑(u + v).den : ℤ) (HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) • (x + y))

Tactic:
rw [smul_lt_smul_iff_of_pos_left (by simpa using (u + v).den_pos)]

Premises used: smul_lt_smul_iff_of_pos_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
u v : ℚ
x y : M
hu : HSMul.hSMul (β := M) u.num 1 < u.den • x
hv : HSMul.hSMul (β := M) v.num 1 < v.den • y
hu' : HSMul.hSMul (β := M) (u.num * (↑v.den : ℤ)) 1 < HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) • x
rw :
  HSMul.hSMul (β := M) (u.num * (↑v.den : ℤ)) 1 + HSMul.hSMul (β := M) (v.num * (↑u.den : ℤ)) 1 <
    HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) • x + HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) • y
⊢ HSMul.hSMul (β := M) (u.num * (↑v.den : ℤ) + v.num * (↑u.den : ℤ)) 1 <
    HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) • (x + y)

Tactic:
rw [add_smul, smul_add]

Premises used: add_smul, 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
u v : ℚ
x y : M
hu : HSMul.hSMul (β := M) u.num 1 < u.den • x
hv : HSMul.hSMul (β := M) v.num 1 < v.den • y
hu' : HSMul.hSMul (β := M) (u.num * (↑v.den : ℤ)) 1 < HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) • x
⊢ HSMul.hSMul (β := M) (u.num * (↑v.den : ℤ)) 1 + HSMul.hSMul (β := M) (v.num * (↑u.den : ℤ)) 1 <
    HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) • x + HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) • y

Tactic:
add_lt_add hu' ((mul_smul_one_lt_iff u.den_pos).mpr hv)

Premises used: Iff.mpr, mul_smul_one_lt_iff, add_lt_add, Rat.den_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
u v : ℚ
x y : M
hu : HSMul.hSMul (β := M) u.num 1 < u.den • x
hv : HSMul.hSMul (β := M) v.num 1 < v.den • y
hu' : HSMul.hSMul (β := M) (u.num * (↑v.den : ℤ)) 1 < HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) • x
⊢ HSMul.hSMul (β := M) (u.num * (↑v.den : ℤ)) 1 + HSMul.hSMul (β := M) (v.num * (↑u.den : ℤ)) 1 <
    HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) • x + HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) • y

Tactic:
exact add_lt_add hu' ((mul_smul_one_lt_iff u.den_pos).mpr hv)

Premises used: Iff.mpr, mul_smul_one_lt_iff, add_lt_add, Rat.den_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
num : ℤ
den : ℕ
x : M
h : HSMul.hSMul (β := M) num 1 ≤ den • x
n : ℤ
hn : x ≤ HSMul.hSMul (β := M) n 1
⊢ LT.lt.{u_1} (α := M) 0 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
num : ℤ
den : ℕ
x : M
h : HSMul.hSMul (β := M) num 1 ≤ den • x
n : ℤ
hn : x ≤ HSMul.hSMul (β := M) n 1
refine : den • x ≤ HSMul.hSMul (β := M) (n * (↑den : ℤ)) 1
⊢ num ≤ n * (↑den : ℤ)

Tactic:
refine le_of_smul_le_smul_right (h.trans ?_) (by simp)

Premises used: le_of_smul_le_smul_right, LE.le.trans
-- 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
num : ℤ
den : ℕ
x : M
h : HSMul.hSMul (β := M) num 1 ≤ den • x
n : ℤ
hn : x ≤ HSMul.hSMul (β := M) n 1
rw : den • x ≤ HSMul.hSMul (α := ℤ) (↑den : ℤ) (HSMul.hSMul (β := M) n 1)
⊢ den • x ≤ HSMul.hSMul (β := M) (n * (↑den : ℤ)) 1

Tactic:
rw [mul_comm, ← smul_smul]

Premises used: smul_smul, mul_comm
-- 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
num : ℤ
den : ℕ
x : M
h : HSMul.hSMul (β := M) num 1 ≤ den • x
n : ℤ
hn : x ≤ HSMul.hSMul (β := M) n 1
⊢ den • x ≤ HSMul.hSMul (α := ℤ) (↑den : ℤ) (HSMul.hSMul (β := M) n 1)

Tactic:
simpa using nsmul_le_nsmul_right hn den

Premises used: nsmul_le_nsmul_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
num : ℤ
den : ℕ
hden : den ≠ 0
x : M
rw : HSMul.hSMul (β := M) (mkRat num den).num 1 < (mkRat num den).den • x ↔ HSMul.hSMul (β := M) num 1 < den • x
⊢ mkRat num den ∈ ratLt x ↔ HSMul.hSMul (β := M) num 1 < den • x

Tactic:
rw [Set.mem_setOf]

Premises used: Set.mem_setOf
-- 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
num : ℤ
den : ℕ
hden : den ≠ 0
x : M
⊢ mkRat num den =
    {
      num :=
        Rat.num
          (Decidable.rec (motive := fun (x : Decidable (den = 0)) ↦ ℚ)
            (fun (h : ¬den = 0) ↦ (fun (den_nz : ¬den = 0) ↦ Rat.normalize num den den_nz) h)
            (fun (h : den = 0) ↦
              (fun (den_nz : den = 0) ↦
                  { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 : ℚ })
                h)
            (instDecidableEqNat den 0)),
      den :=
        Rat.den
          (Decidable.rec (motive := fun (x : Decidable (den = 0)) ↦ ℚ)
            (fun (h : ¬den = 0) ↦ (fun (den_nz : ¬den = 0) ↦ Rat.normalize num den den_nz) h)
            (fun (h : den = 0) ↦
              (fun (den_nz : den = 0) ↦
                  { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 : ℚ })
                h)
            (instDecidableEqNat den 0)),
      den_nz := ⋯, reduced := ⋯ }

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
num : ℤ
den : ℕ
hden : den ≠ 0
x : M
obtain :
  ∀ (m : ℕ) (hm0 : m ≠ 0)
    (hnum :
      num =
        Rat.num
            (Decidable.rec (motive := fun (x : Decidable (den = 0)) ↦ ℚ)
              (fun (h : ¬den = 0) ↦ (fun (den_nz : ¬den = 0) ↦ Rat.normalize num den den_nz) h)
              (fun (h : den = 0) ↦
                (fun (den_nz : den = 0) ↦
                    { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 : ℚ })
                  h)
              (instDecidableEqNat den 0)) *
          (↑m : ℤ))
    (hden :
      den =
        Rat.den
            (Decidable.rec (motive := fun (x : Decidable (den = 0)) ↦ ℚ)
              (fun (h : ¬den = 0) ↦ (fun (den_nz : ¬den = 0) ↦ Rat.normalize num den den_nz) h)
              (fun (h : den = 0) ↦
                (fun (den_nz : den = 0) ↦
                    { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 : ℚ })
                  h)
              (instDecidableEqNat den 0)) *
          m),
    HSMul.hSMul (β := M) (mkRat num den).num 1 < (mkRat num den).den • x ↔ HSMul.hSMul (β := M) num 1 < den • x
⊢ HSMul.hSMul (β := M) (mkRat num den).num 1 < (mkRat num den).den • x ↔ HSMul.hSMul (β := M) num 1 < den • x

Tactic:
obtain ⟨m, hm0, hnum, hden⟩ := Rat.mkRat_num_den hden (show mkRat num den = _ by rfl)

Premises used: Rat.mkRat_num_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
num : ℤ
den : ℕ
hden_1 : den ≠ 0
x : M
m : ℕ
hm0 : m ≠ 0
hnum :
  num =
    Rat.num
        (Decidable.rec (motive := fun (x : Decidable (den = 0)) ↦ ℚ)
          (fun (h : ¬den = 0) ↦ (fun (den_nz : ¬den = 0) ↦ Rat.normalize num den den_nz) h)
          (fun (h : den = 0) ↦
            (fun (den_nz : den = 0) ↦
                { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 : ℚ })
              h)
          (instDecidableEqNat den 0)) *
      (↑m : ℤ)
hden :
  den =
    Rat.den
        (Decidable.rec (motive := fun (x : Decidable (den = 0)) ↦ ℚ)
          (fun (h : ¬den = 0) ↦ (fun (den_nz : ¬den = 0) ↦ Rat.normalize num den den_nz) h)
          (fun (h : den = 0) ↦
            (fun (den_nz : den = 0) ↦
                { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 : ℚ })
              h)
          (instDecidableEqNat den 0)) *
      m
rw :
  m •
    HSMul.hSMul (β := M)
      (Rat.num
        (Decidable.rec (motive := fun (x : Decidable (den = 0)) ↦ ℚ)
          (fun (h : ¬den = 0) ↦ (fun (den_nz : ¬den = 0) ↦ Rat.normalize num den den_nz) h)
          (fun (h : den = 0) ↦
            (fun (den_nz : den = 0) ↦
                { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 : ℚ })
              h)
          (instDecidableEqNat den 0)))
      1
| HSMul.hSMul (β := M) num 1

Tactic:
rw [hnum, mul_comm, ← smul_smul, natCast_zsmul]

Premises used: smul_smul, mul_comm, 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
num : ℤ
den : ℕ
hden_1 : den ≠ 0
x : M
m : ℕ
hm0 : m ≠ 0
hnum :
  num =
    Rat.num
        (Decidable.rec (motive := fun (x : Decidable (den = 0)) ↦ ℚ)
          (fun (h : ¬den = 0) ↦ (fun (den_nz : ¬den = 0) ↦ Rat.normalize num den den_nz) h)
          (fun (h : den = 0) ↦
            (fun (den_nz : den = 0) ↦
                { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 : ℚ })
              h)
          (instDecidableEqNat den 0)) *
      (↑m : ℤ)
hden :
  den =
    Rat.den
        (Decidable.rec (motive := fun (x : Decidable (den = 0)) ↦ ℚ)
          (fun (h : ¬den = 0) ↦ (fun (den_nz : ¬den = 0) ↦ Rat.normalize num den den_nz) h)
          (fun (h : den = 0) ↦
            (fun (den_nz : den = 0) ↦
                { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 : ℚ })
              h)
          (instDecidableEqNat den 0)) *
      m
conv :
  HSMul.hSMul (β := M) (mkRat num den).num 1 < (mkRat num den).den • x ↔
    m •
        HSMul.hSMul (β := M)
          (Rat.num
            (Decidable.rec (motive := fun (x : Decidable (den = 0)) ↦ ℚ)
              (fun (h : ¬den = 0) ↦ (fun (den_nz : ¬den = 0) ↦ Rat.normalize num den den_nz) h)
              (fun (h : den = 0) ↦
                (fun (den_nz : den = 0) ↦
                    { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 : ℚ })
                  h)
              (instDecidableEqNat den 0)))
          1 <
      den • x
⊢ HSMul.hSMul (β := M) (mkRat num den).num 1 < (mkRat num den).den • x ↔ HSMul.hSMul (β := M) num 1 < den • x

Tactic:
conv in num • 1 => rw [hnum, mul_comm, ← smul_smul, natCast_zsmul]

Premises used: smul_smul, mul_comm, 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
num : ℤ
den : ℕ
hden_1 : den ≠ 0
x : M
m : ℕ
hm0 : m ≠ 0
hnum :
  num =
    Rat.num
        (Decidable.rec (motive := fun (x : Decidable (den = 0)) ↦ ℚ)
          (fun (h : ¬den = 0) ↦ (fun (den_nz : ¬den = 0) ↦ Rat.normalize num den den_nz) h)
          (fun (h : den = 0) ↦
            (fun (den_nz : den = 0) ↦
                { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 : ℚ })
              h)
          (instDecidableEqNat den 0)) *
      (↑m : ℤ)
hden :
  den =
    Rat.den
        (Decidable.rec (motive := fun (x : Decidable (den = 0)) ↦ ℚ)
          (fun (h : ¬den = 0) ↦ (fun (den_nz : ¬den = 0) ↦ Rat.normalize num den den_nz) h)
          (fun (h : den = 0) ↦
            (fun (den_nz : den = 0) ↦
                { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 : ℚ })
              h)
          (instDecidableEqNat den 0)) *
      m
rw :
  m •
    Rat.den
        (Decidable.rec (motive := fun (x : Decidable (den = 0)) ↦ ℚ)
          (fun (h : ¬den = 0) ↦ (fun (den_nz : ¬den = 0) ↦ Rat.normalize num den den_nz) h)
          (fun (h : den = 0) ↦
            (fun (den_nz : den = 0) ↦
                { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 : ℚ })
              h)
          (instDecidableEqNat den 0)) •
      x
| den • x

Tactic:
rw [hden, mul_comm, ← smul_smul]

Premises used: smul_smul, mul_comm
-- 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
num : ℤ
den : ℕ
hden_1 : den ≠ 0
x : M
m : ℕ
hm0 : m ≠ 0
hnum :
  num =
    Rat.num
        (Decidable.rec (motive := fun (x : Decidable (den = 0)) ↦ ℚ)
          (fun (h : ¬den = 0) ↦ (fun (den_nz : ¬den = 0) ↦ Rat.normalize num den den_nz) h)
          (fun (h : den = 0) ↦
            (fun (den_nz : den = 0) ↦
                { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 : ℚ })
              h)
          (instDecidableEqNat den 0)) *
      (↑m : ℤ)
hden :
  den =
    Rat.den
        (Decidable.rec (motive := fun (x : Decidable (den = 0)) ↦ ℚ)
          (fun (h : ¬den = 0) ↦ (fun (den_nz : ¬den = 0) ↦ Rat.normalize num den den_nz) h)
          (fun (h : den = 0) ↦
            (fun (den_nz : den = 0) ↦
                { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 : ℚ })
              h)
          (instDecidableEqNat den 0)) *
      m
conv :
  HSMul.hSMul (β := M) (mkRat num den).num 1 < (mkRat num den).den • x ↔
    m •
        HSMul.hSMul (β := M)
          (Rat.num
            (Decidable.rec (motive := fun (x : Decidable (den = 0)) ↦ ℚ)
              (fun (h : ¬den = 0) ↦ (fun (den_nz : ¬den = 0) ↦ Rat.normalize num den den_nz) h)
              (fun (h : den = 0) ↦
                (fun (den_nz : den = 0) ↦
                    { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 : ℚ })
                  h)
              (instDecidableEqNat den 0)))
          1 <
      m •
        Rat.den
            (Decidable.rec (motive := fun (x : Decidable (den = 0)) ↦ ℚ)
              (fun (h : ¬den = 0) ↦ (fun (den_nz : ¬den = 0) ↦ Rat.normalize num den den_nz) h)
              (fun (h : den = 0) ↦
                (fun (den_nz : den = 0) ↦
                    { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 : ℚ })
                  h)
              (instDecidableEqNat den 0)) •
          x
⊢ HSMul.hSMul (β := M) (mkRat num den).num 1 < (mkRat num den).den • x ↔
    m •
        HSMul.hSMul (β := M)
          (Rat.num
            (Decidable.rec (motive := fun (x : Decidable (den = 0)) ↦ ℚ)
              (fun (h : ¬den = 0) ↦ (fun (den_nz : ¬den = 0) ↦ Rat.normalize num den den_nz) h)
              (fun (h : den = 0) ↦
                (fun (den_nz : den = 0) ↦
                    { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 : ℚ })
                  h)
              (instDecidableEqNat den 0)))
          1 <
      den • x

Tactic:
conv in den • x => rw [hden, mul_comm, ← smul_smul]

Premises used: smul_smul, mul_comm
-- 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
num : ℤ
den : ℕ
hden_1 : den ≠ 0
x : M
m : ℕ
hm0 : m ≠ 0
hnum :
  num =
    Rat.num
        (Decidable.rec (motive := fun (x : Decidable (den = 0)) ↦ ℚ)
          (fun (h : ¬den = 0) ↦ (fun (den_nz : ¬den = 0) ↦ Rat.normalize num den den_nz) h)
          (fun (h : den = 0) ↦
            (fun (den_nz : den = 0) ↦
                { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 : ℚ })
              h)
          (instDecidableEqNat den 0)) *
      (↑m : ℤ)
hden :
  den =
    Rat.den
        (Decidable.rec (motive := fun (x : Decidable (den = 0)) ↦ ℚ)
          (fun (h : ¬den = 0) ↦ (fun (den_nz : ¬den = 0) ↦ Rat.normalize num den den_nz) h)
          (fun (h : den = 0) ↦
            (fun (den_nz : den = 0) ↦
                { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 : ℚ })
              h)
          (instDecidableEqNat den 0)) *
      m
⊢ HSMul.hSMul (β := M) (mkRat num den).num 1 < (mkRat num den).den • x ↔
    m •
        HSMul.hSMul (β := M)
          (Rat.num
            (Decidable.rec (motive := fun (x : Decidable (den = 0)) ↦ ℚ)
              (fun (h : ¬den = 0) ↦ (fun (den_nz : ¬den = 0) ↦ Rat.normalize num den den_nz) h)
              (fun (h : den = 0) ↦
                (fun (den_nz : den = 0) ↦
                    { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 : ℚ })
                  h)
              (instDecidableEqNat den 0)))
          1 <
      m •
        Rat.den
            (Decidable.rec (motive := fun (x : Decidable (den = 0)) ↦ ℚ)
              (fun (h : ¬den = 0) ↦ (fun (den_nz : ¬den = 0) ↦ Rat.normalize num den den_nz) h)
              (fun (h : den = 0) ↦
                (fun (den_nz : den = 0) ↦
                    { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 : ℚ })
                  h)
              (instDecidableEqNat den 0)) •
          x

Tactic:
(smul_lt_smul_iff_of_pos_left (Nat.zero_lt_of_ne_zero hm0)).symm

Premises used: Nat.zero_lt_of_ne_zero, smul_lt_smul_iff_of_pos_left, Iff.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
num : ℤ
den : ℕ
hden_1 : den ≠ 0
x : M
m : ℕ
hm0 : m ≠ 0
hnum :
  num =
    Rat.num
        (Decidable.rec (motive := fun (x : Decidable (den = 0)) ↦ ℚ)
          (fun (h : ¬den = 0) ↦ (fun (den_nz : ¬den = 0) ↦ Rat.normalize num den den_nz) h)
          (fun (h : den = 0) ↦
            (fun (den_nz : den = 0) ↦
                { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 : ℚ })
              h)
          (instDecidableEqNat den 0)) *
      (↑m : ℤ)
hden :
  den =
    Rat.den
        (Decidable.rec (motive := fun (x : Decidable (den = 0)) ↦ ℚ)
          (fun (h : ¬den = 0) ↦ (fun (den_nz : ¬den = 0) ↦ Rat.normalize num den den_nz) h)
          (fun (h : den = 0) ↦
            (fun (den_nz : den = 0) ↦
                { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 : ℚ })
              h)
          (instDecidableEqNat den 0)) *
      m
⊢ HSMul.hSMul (β := M) (mkRat num den).num 1 < (mkRat num den).den • x ↔
    m •
        HSMul.hSMul (β := M)
          (Rat.num
            (Decidable.rec (motive := fun (x : Decidable (den = 0)) ↦ ℚ)
              (fun (h : ¬den = 0) ↦ (fun (den_nz : ¬den = 0) ↦ Rat.normalize num den den_nz) h)
              (fun (h : den = 0) ↦
                (fun (den_nz : den = 0) ↦
                    { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 : ℚ })
                  h)
              (instDecidableEqNat den 0)))
          1 <
      m •
        Rat.den
            (Decidable.rec (motive := fun (x : Decidable (den = 0)) ↦ ℚ)
              (fun (h : ¬den = 0) ↦ (fun (den_nz : ¬den = 0) ↦ Rat.normalize num den den_nz) h)
              (fun (h : den = 0) ↦
                (fun (den_nz : den = 0) ↦
                    { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 : ℚ })
                  h)
              (instDecidableEqNat den 0)) •
          x

Tactic:
exact (smul_lt_smul_iff_of_pos_left (Nat.zero_lt_of_ne_zero hm0)).symm

Premises used: Nat.zero_lt_of_ne_zero, smul_lt_smul_iff_of_pos_left, Iff.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 : M
obtain : ∀ (n : ℕ) (hn : x ≤ HSMul.hSMul (β := M) n 1), BddAbove (ratLt x)
⊢ BddAbove (ratLt x)

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

Premises used: zero_lt_one, Archimedean.arch
-- 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
h : (↑n : ℚ) ∈ upperBounds (ratLt x)
⊢ BddAbove (ratLt x)

Tactic:
use n
-- 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 :
  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 : ℤ)
⊢ 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 : ℚ } ≤ (↑n : ℚ)

Tactic:
rw [Rat.le_iff]

Premises used: Rat.le_iff