awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
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 + v).num 1 < (u + v).den • (x + y)
have 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))
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]
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
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 + v).num * (↑u.den : ℤ) * (↑v.den : ℤ)) 1 <
    HSMul.hSMul (α := ℤ) (↑(u + v).den : ℤ) (HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) • (x + y))
have 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))
Tactic: rw [Rat.add_num_den', mul_comm, ← smul_smul]
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
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 (α := ℤ) (↑(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))
have rw : HSMul.hSMul (β := M) (u.num * (↑v.den : ℤ) + v.num * (↑u.den : ℤ)) 1 <
  HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) • (x + y)
Tactic: rw [smul_lt_smul_iff_of_pos_left (by simpa using (u + v).den_pos)]
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
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 : ℤ) + v.num * (↑u.den : ℤ)) 1 <
    HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) • (x + y)
have 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
Tactic: rw [add_smul, smul_add]
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
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
⊢ num ≤ n * (↑den : ℤ)
have refine : den • x ≤ HSMul.hSMul (β := M) (n * (↑den : ℤ)) 1
Tactic: refine le_of_smul_le_smul_right (h.trans ?_) (by simp)
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
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 (β := M) (n * (↑den : ℤ)) 1
have rw : den • x ≤ HSMul.hSMul (α := ℤ) (↑den : ℤ) (HSMul.hSMul (β := M) n 1)
Tactic: rw [mul_comm, ← smul_smul]
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
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 ∈ ratLt x ↔ HSMul.hSMul (β := M) num 1 < den • x
have rw : HSMul.hSMul (β := M) (mkRat num den).num 1 < (mkRat num den).den • x ↔ HSMul.hSMul (β := M) num 1 < den • x
Tactic: rw [Set.mem_setOf]
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
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
⊢ HSMul.hSMul (β := M) (mkRat num den).num 1 < (mkRat num den).den • x ↔ HSMul.hSMul (β := M) num 1 < den • x
have 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
Tactic: obtain ⟨m, hm0, hnum, hden⟩ := Rat.mkRat_num_den hden (show mkRat num den = _ by rfl)
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
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) num 1
have 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
Tactic: rw [hnum, mul_comm, ← smul_smul, natCast_zsmul]
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
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 ↔ HSMul.hSMul (β := M) num 1 < den • x
have 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
Tactic: conv in num • 1 => rw [hnum, mul_comm, ← smul_smul, natCast_zsmul]
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
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
| den • x
have 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
Tactic: rw [hden, mul_comm, ← smul_smul]
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
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 <
      den • x
have 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
Tactic: conv in den • x => rw [hden, mul_comm, ← smul_smul]
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
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)
have obtain : ∀ (n : ℕ) (hn : x ≤ HSMul.hSMul (β := M) n 1), BddAbove (ratLt x)
Tactic: obtain ⟨n, hn⟩ := Archimedean.arch x zero_lt_one
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
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
⊢ BddAbove (ratLt x)
have h : (↑n : ℚ) ∈ upperBounds (ratLt x)
Tactic: use n
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
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
⊢ 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 : ℚ)
have 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 : ℤ)
Tactic: rw [Rat.le_iff]
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
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
⊢ 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 : ℤ)
have h : HSMul.hSMul (β := M) num 1 < den • x → num ≤ HMul.hMul (α := ℤ) (↑n : ℤ) (↑den : ℤ)
Tactic: suffices num • 1 < den • x → num ≤ n * den by simpa using this
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
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
have inl : ∀ (hneg : x < 0), (ratLt x).Nonempty
Tactic: obtain hneg | rfl | hxpos := lt_trichotomy x 0
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
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
⊢ (ratLt x).Nonempty
have inr : (ratLt.{u_1} (M := M) 0).Nonempty
Tactic: obtain hneg | rfl | hxpos := lt_trichotomy x 0
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
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
⊢ (ratLt x).Nonempty
have inr₁ : ∀ (hxpos : 0 < x), (ratLt x).Nonempty
Tactic: obtain hneg | rfl | hxpos := lt_trichotomy x 0
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
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
⊢ (ratLt x).Nonempty
have inl : ∀ (n : ℕ) (hn : -x - x ≤ HSMul.hSMul (β := M) n 1), (ratLt x).Nonempty
Tactic: obtain ⟨n, hn⟩ := Archimedean.arch (-x - x) zero_lt_one
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
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
⊢ (ratLt x).Nonempty
have h : Rat.ofInt (-(↑n : ℤ)) ∈ ratLt x
Tactic: use Rat.ofInt (-n)
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
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
⊢ Rat.ofInt (-(↑n : ℤ)) ∈ ratLt x
have h : -HSMul.hSMul (β := M) n 1 < x
Tactic: suffices -(n • 1) < x by simpa using this
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
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
⊢ (ratLt x).Nonempty
have inr : ∀ (n : ℕ) (hn : 1 ≤ n • x), (ratLt x).Nonempty
Tactic: obtain ⟨n, hn⟩ := Archimedean.arch 1 hxpos
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
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
⊢ (ratLt x).Nonempty
have h : { num := 1, den := n + 1, den_nz := sorry, reduced := sorry : ℚ } ∈ ratLt x
Tactic: use Rat.mk' 1 (n + 1) (by simp) (by simp)
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
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
⊢ ratLt (x + y) = ratLt x + ratLt y
have h : ∀ (a : ℚ), a ∈ ratLt (x + y) ↔ a ∈ ratLt x + ratLt y
Tactic: ext a
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
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 : ℚ
⊢ a ∈ ratLt (x + y) ↔ ∃ x_1 ∈ ratLt x, ∃ y_1 ∈ ratLt y, x_1 + y_1 = a
have h : a ∈ ratLt (x + y) → ∃ x_1 ∈ ratLt x, ∃ y_1 ∈ ratLt y, x_1 + y_1 = a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
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
⊢ a ∈ ratLt (x + y) ↔ ∃ x_1 ∈ ratLt x, ∃ y_1 ∈ ratLt y, x_1 + y_1 = a
have h₁ : (∃ x_1 ∈ ratLt x, ∃ y_1 ∈ ratLt y, x_1 + y_1 = a) → a ∈ ratLt (x + y)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (hypothesis)
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
have h₁ : HSMul.hSMul (β := M) a.num 1 < a.den • (x + y)
Tactic: rw [Set.mem_setOf_eq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
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)
⊢ ∃ x_1 ∈ ratLt x, ∃ y_1 ∈ ratLt y, x_1 + y_1 = a
have 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
Tactic: obtain ⟨k, hk⟩ := Archimedean.arch (1 + 1) <| sub_pos.mpr h
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
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
have contrapose! : ∀ (hk : k = 0), k • (a.den • (x + y) - HSMul.hSMul (β := M) a.num 1) < HAdd.hAdd (α := M) 1 1
Tactic: contrapose! hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (hypothesis)
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)
⊢ ∃ x_1 ∈ ratLt x, ∃ y_1 ∈ ratLt y, x_1 + y_1 = a
have hk0 : k ≠ 0
Tactic: have hk0 : k ≠ 0 := by
      contrapose! hk
      simp [hk]
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (hypothesis)
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
⊢ ∃ x_1 ∈ ratLt x, ∃ y_1 ∈ ratLt y, x_1 + y_1 = a
have hka0 : k * a.den ≠ 0
Tactic: have hka0 : k * a.den ≠ 0 := mul_ne_zero hk0 a.den_ne_zero