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
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
⊢ ∃ x_1 ∈ ratLt x, ∃ y_1 ∈ ratLt y, x_1 + y_1 = a
have 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
Tactic: obtain ⟨m, ⟨hm1, hm2⟩, _⟩ := existsUnique_add_zsmul_mem_Ico zero_lt_one 0 (k • a.den • x - 1)
-- 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)
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
have h₁ : mkRat m (k * a.den) ∈ ratLt x
Tactic: refine ⟨mkRat m (k * a.den), ?_, mkRat (k * a.num - m) (k * a.den), ?_, ?_⟩
-- 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)
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
⊢ ∃ x_1 ∈ ratLt x, ∃ y_1 ∈ ratLt y, x_1 + y_1 = a
have h₂ : mkRat ((↑k : ℤ) * a.num - m) (k * a.den) ∈ ratLt y
Tactic: refine ⟨mkRat m (k * a.den), ?_, mkRat (k * a.num - m) (k * a.den), ?_, ?_⟩
-- 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)
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
⊢ ∃ x_1 ∈ ratLt x, ∃ y_1 ∈ ratLt y, x_1 + y_1 = a
have h₃ : mkRat m (k * a.den) + mkRat ((↑k : ℤ) * a.num - m) (k * a.den) = a
Tactic: refine ⟨mkRat m (k * a.den), ?_, mkRat (k * a.num - m) (k * a.den), ?_, ?_⟩
-- 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)
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
⊢ mkRat m (k * a.den) ∈ ratLt x
have h₁ : HSMul.hSMul (β := M) m 1 < k • a.den • x
Tactic: rw [mkRat_mem_ratLt hka0, ← 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 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
have 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
Tactic: rw [smul_add, smul_sub, smul_add, le_sub_iff_add_le, ← sub_le_iff_le_add] at hk
Cleared hypotheses: hk, hk0, hka0, m, right, hm1, hm2
-- 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 • 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) ≤ k • a.den • x - 1
have rw : 1 + (k • HSMul.hSMul (β := M) a.num 1 - k • a.den • y) + 1 ≤ k • a.den • x
Tactic: rw [le_sub_iff_add_le]
-- 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 • 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 ≤ k • a.den • x
have 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
Tactic: convert! hk using 1
-- 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
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
⊢ mkRat ((↑k : ℤ) * a.num - m) (k * a.den) ∈ ratLt y
have hk' : 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
-- 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
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
⊢ mkRat ((↑k : ℤ) * a.num - m) (k * a.den) ∈ ratLt y
have this : 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)
-- 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)
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
⊢ mkRat m (k * a.den) + mkRat ((↑k : ℤ) * a.num - m) (k * a.den) = a
have h₁ : mkRat (m + ((↑k : ℤ) * a.num - m)) (k * a.den) = a
Tactic: rw [Rat.mkRat_add_mkRat_of_den _ _ hka0]
-- 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)
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
⊢ mkRat (m + ((↑k : ℤ) * a.num - m)) (k * a.den) = a
have h₁ : mkRat ((↑k : ℤ) * a.num) (k * a.den) = a
Tactic: rw [add_sub_cancel, Rat.mkRat_mul_left hk0, Rat.mkRat_num_den']
-- 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)
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
⊢ mkRat (m + ((↑k : ℤ) * a.num - m)) (k * a.den) = a
have h₂ : mkRat a.num a.den = a
Tactic: rw [add_sub_cancel, Rat.mkRat_mul_left hk0, Rat.mkRat_num_den']
-- 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)
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
⊢ mkRat (m + ((↑k : ℤ) * a.num - m)) (k * a.den) = a
have h₃ : a = a
Tactic: rw [add_sub_cancel, Rat.mkRat_mul_left hk0, Rat.mkRat_num_den']
-- 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 u : ℚ
hu : u ∈ ratLt x
v : ℚ
hv : v ∈ ratLt y
huv : u + v = a
⊢ a ∈ ratLt (x + y)
have h : u + v ∈ ratLt (x + y)
Tactic: rw [← huv]
-- 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 u : ℚ
hu : u ∈ ratLt x
v : ℚ
hv : v ∈ ratLt y
huv : u + v = a
⊢ u + v ∈ ratLt (x + y)
have 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)
Tactic: rw [Set.mem_setOf_eq] at hu hv ⊢
Cleared hypotheses: hu, v, hv, huv
-- 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 rw : (⇑(Rat.castHom ℝ) : (a : ℚ) → ℝ) '' ratLt (x + y) = ratLt' x + ratLt' y
Tactic: rw [ratLt', ratLt_add, Set.image_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
inst_6 : Archimedean M
x y : M
rw : (⇑(Rat.castHom ℝ) : (a : ℚ) → ℝ) '' ratLt (x + y) = ratLt' x + ratLt' y
⊢ ratLt' (x + y) = ratLt' x + ratLt' y
have rw₁ : (⇑(Rat.castHom ℝ) : (a : ℚ) → ℝ) '' (ratLt x + ratLt y) = ratLt' x + ratLt' y
Tactic: rw [ratLt', ratLt_add, Set.image_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
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
⊢ ratLt' (x + y) = ratLt' x + ratLt' y
have rw₂ : HAdd.hAdd (α := Set ℝ) ((⇑(Rat.castHom ℝ) : (a : ℚ) → ℝ) '' ratLt x) ((⇑(Rat.castHom ℝ) : (a : ℚ) → ℝ) '' ratLt y) =
  ratLt' x + ratLt' y
Tactic: rw [ratLt', ratLt_add, Set.image_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
inst_6 : Archimedean M
⊢ embedRealFun.{u_1} (M := M) 0 = 0
have a : embedRealFun.{u_1} (M := M) 0 ≤ 0
Tactic: apply le_antisymm
-- 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
a : embedRealFun.{u_1} (M := M) 0 ≤ 0
⊢ embedRealFun.{u_1} (M := M) 0 = 0
have a₁ : 0 ≤ embedRealFun.{u_1} (M := M) 0
Tactic: apply le_antisymm
-- 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
⊢ embedRealFun.{u_1} (M := M) 0 ≤ 0
have a : ∀ b ∈ ratLt'.{u_1} (M := M) 0, b ≤ 0
Tactic: apply csSup_le (ratLt'_nonempty 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 : ℝ
⊢ Membership.mem (γ := Set ℝ)
      (Set.image (α := ℚ) (⇑(Rat.castHom ℝ) : (a : ℚ) → ℝ)
        {r : ℚ | HSMul.hSMul (β := M) r.num 1 < HSMul.hSMul (β := M) r.den 0})
      x →
    x ≤ 0
have a : ∀ (y : ℚ), HSMul.hSMul (β := M) y.num 1 < 0 → (↑y : ℝ) = x → x ≤ 0
Tactic: suffices ∀ (y : ℚ), y.num • (1 : M) < 0 → y = x → x ≤ 0 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 : ℝ
y : ℚ
hy : HSMul.hSMul (β := M) y.num 1 < 0
hyx : (↑y : ℝ) = x
⊢ x ≤ 0
have a : y.num ≤ 0
Tactic: rw [← hyx, Rat.cast_nonpos, ← Rat.num_nonpos]
-- 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
⊢ 0 ≤ embedRealFun.{u_1} (M := M) 0
have a : ∀ b ∈ upperBounds (ratLt'.{u_1} (M := M) 0), 0 ≤ b
Tactic: rw [le_csSup_iff (ratLt'_bddAbove (0 : M)) (ratLt'_nonempty 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 : ℝ
⊢ (∀ x_1 ∈ ratLt'.{u_1} (M := M) 0, x_1 ≤ x) → 0 ≤ x
have a : (∀ (y : ℚ), HSMul.hSMul (β := M) y.num 1 < 0 → (↑y : ℝ) ≤ x) → 0 ≤ x
Tactic: suffices (∀ (y : ℚ), y.num • (1 : M) < 0 → y ≤ x) → 0 ≤ x by simpa using this
-- 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 : ℝ
h : ∀ (y : ℚ), HSMul.hSMul (β := M) y.num 1 < 0 → (↑y : ℝ) ≤ x
⊢ 0 ≤ x
have h' : ∀ (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
-- 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 : ℝ
h : ∀ (y : ℚ), HSMul.hSMul (β := M) y.num 1 < 0 → (↑y : ℝ) ≤ x
h' : ∀ (y : ℚ) (hy : y < 0), (↑y : ℝ) ≤ x
⊢ 0 ≤ x
have a : ∀ (h' : x < 0), ∃ y < 0, x < (↑y : ℝ)
Tactic: contrapose! 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 : ℝ
h : ∀ (y : ℚ), HSMul.hSMul (β := M) y.num 1 < 0 → (↑y : ℝ) ≤ x
h' : x < 0
⊢ ∃ y < 0, x < (↑y : ℝ)
have a : ∀ (y : ℚ) (hxy : x < (↑y : ℝ)) (hy : LT.lt (α := ℝ) (↑y : ℝ) 0), ∃ y < 0, x < (↑y : ℝ)
Tactic: obtain ⟨y, hxy, hy⟩ := exists_rat_btwn 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
⊢ embedRealFun (x + y) = embedRealFun x + embedRealFun y
have rw : sSup (ratLt' (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)]
-- 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
rw : sSup (ratLt' (x + y)) = embedRealFun x + embedRealFun y
⊢ embedRealFun (x + y) = embedRealFun x + embedRealFun y
have rw₁ : sSup (ratLt' x + ratLt' y) = embedRealFun x + embedRealFun y
Tactic: rw [embedRealFun, ratLt'_add, csSup_add (ratLt'_nonempty x) (ratLt'_bddAbove x)
    (ratLt'_nonempty y) (ratLt'_bddAbove y)]
-- 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
rw : sSup (ratLt' (x + y)) = embedRealFun x + embedRealFun y
rw₁ : sSup (ratLt' x + ratLt' y) = embedRealFun x + embedRealFun y
⊢ embedRealFun (x + y) = embedRealFun x + embedRealFun y
have rw₂ : sSup (ratLt' x) + sSup (ratLt' y) = embedRealFun x + embedRealFun y
Tactic: rw [embedRealFun, ratLt'_add, csSup_add (ratLt'_nonempty x) (ratLt'_bddAbove x)
    (ratLt'_nonempty y) (ratLt'_bddAbove y)]
-- 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
h : x < y
⊢ embedRealFun x < embedRealFun y
have hyz : 0 < y - x
Tactic: have hyz : 0 < y - x := sub_pos.mpr h
-- 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
h : x < y
hyz : 0 < y - x
⊢ embedRealFun x < embedRealFun y
have hy : y = y - x + x
Tactic: have hy : y = y - x + x := (sub_add_cancel y x).symm
-- 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
h : x < y
hyz : 0 < y - x
hy : y = y - x + x
⊢ embedRealFun x < embedRealFun y
have a : 0 < embedRealFun y - embedRealFun x
Tactic: apply lt_of_sub_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
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
⊢ 0 < embedRealFun y - embedRealFun x
have a : 0 < embedRealFun (y - x)
Tactic: rw [hy, embedRealFun_add, add_sub_cancel_right]
-- 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
h : x < y
hyz : 0 < y - x
hy : y = y - x + x
⊢ 0 < embedRealFun (y - x)
have a : ∀ (n : ℕ) (hn : 1 ≤ n • (y - x)), 0 < embedRealFun (y - x)
Tactic: obtain ⟨n, hn⟩ := Archimedean.arch 1 hyz