awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Rat.Star (goal)
Goal:
n : ℕ
hn₀ : n ≠ 0
hn : Even n
⊢ Eq (α := AddSubmonoid ℚ) (closure (range fun (x : ℚ) ↦ x ^ n)) (nonneg ℚ)
have h : Eq (α := Set ℚ) (range fun (x : ℚ) ↦ x ^ n)
  (image (α := ℚ≥0) (⇑NNRat.coeHom : (a : ℚ≥0) → ℚ) (range fun (x : ℚ≥0) ↦ x ^ n))
Tactic: convert! (AddMonoidHom.map_mclosure NNRat.coeHom <| range fun x ↦ x ^ n).symm
-- Lean 4 proof step from Mathlib.Data.Rat.Star (goal)
Goal:
n : ℕ
hn₀ : n ≠ 0
hn : Even n
h :
  Eq (α := Set ℚ) (range fun (x : ℚ) ↦ x ^ n)
    (image (α := ℚ≥0) (⇑NNRat.coeHom : (a : ℚ≥0) → ℚ) (range fun (x : ℚ≥0) ↦ x ^ n))
⊢ Eq (α := AddSubmonoid ℚ) (closure (range fun (x : ℚ) ↦ x ^ n)) (nonneg ℚ)
have h₁ : Eq (α := AddSubmonoid ℚ) (nonneg ℚ) (map NNRat.coeHom (closure (range fun (x : ℚ≥0) ↦ x ^ n)))
Tactic: convert! (AddMonoidHom.map_mclosure NNRat.coeHom <| range fun x ↦ x ^ n).symm
-- Lean 4 proof step from Mathlib.Data.Rat.Star (hypothesis)
Goal:
n : ℕ
hn₀ : n ≠ 0
hn : Even n
⊢ Eq (α := Set ℚ) (range fun (x : ℚ) ↦ x ^ n)
    (image (α := ℚ≥0) (⇑NNRat.coeHom : (a : ℚ≥0) → ℚ) (range fun (x : ℚ≥0) ↦ x ^ n))
have this : ∀ (x : ℚ), ∃ (y : ℚ≥0), HPow.hPow (α := ℚ) (↑y : ℚ) n = x ^ n
Tactic: have (x : ℚ) : ∃ y : ℚ≥0, y ^ n = x ^ n := ⟨x.nnabs, by simp [hn.pow_abs]⟩
-- Lean 4 proof step from Mathlib.Data.Rat.Star (goal)
Goal:
n : ℕ
hn₀ : n ≠ 0
hn : Even n
⊢ Eq (α := AddSubmonoid ℚ) (nonneg ℚ) (map NNRat.coeHom (closure (range fun (x : ℚ≥0) ↦ x ^ n)))
have h : ∀ (x : ℚ),
  Membership.mem (γ := AddSubmonoid ℚ) (nonneg ℚ) x ↔
    Membership.mem (γ := AddSubmonoid ℚ) (map NNRat.coeHom (closure (range fun (x : ℚ≥0) ↦ x ^ n))) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
hne : s.Nonempty
hbdd : BddAbove s
⊢ ∃ (x : ℝ), IsLUB s x
have rcases : ∀ (L : ℝ) (hL : L ∈ s) (U : ℝ) (hU : U ∈ upperBounds s), ∃ (x : ℝ), IsLUB s x
Tactic: rcases hne, hbdd with ⟨⟨L, hL⟩, ⟨U, hU⟩⟩
Cleared hypotheses: hne, hbdd
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
⊢ ∀ (d : ℕ), BddAbove (α := ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)}
have obtain : ∀ (k : ℤ) (hk : U < (↑k : ℝ)) (d : ℕ), BddAbove (α := ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)}
Tactic: obtain ⟨k, hk⟩ := exists_int_gt U
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
k : ℤ
hk : U < (↑k : ℝ)
⊢ ∀ (d : ℕ), BddAbove (α := ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)}
have refine : ∀ (d : ℕ) (z : ℤ) (h : Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} z), z ≤ k * (↑d : ℤ)
Tactic: refine fun d => ⟨k * d, fun z h => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
k : ℤ
hk : U < (↑k : ℝ)
d : ℕ
z : ℤ
h : Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} z
⊢ z ≤ k * (↑d : ℤ)
have rcases : ∀ (y : ℝ) (yS : y ∈ s) (hy : (↑z : ℝ) ≤ y * (↑d : ℝ)), z ≤ k * (↑d : ℤ)
Tactic: rcases h with ⟨y, yS, hy⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
k : ℤ
hk : U < (↑k : ℝ)
d : ℕ
z : ℤ
y : ℝ
yS : y ∈ s
hy : (↑z : ℝ) ≤ y * (↑d : ℝ)
⊢ z ≤ k * (↑d : ℤ)
have refine : y * (↑d : ℝ) ≤ (↑(k * (↑d : ℤ)) : ℝ)
Tactic: refine Int.cast_le.1 (hy.trans ?_)
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
k : ℤ
hk : U < (↑k : ℝ)
d : ℕ
z : ℤ
y : ℝ
yS : y ∈ s
hy : (↑z : ℝ) ≤ y * (↑d : ℝ)
⊢ y * (↑d : ℝ) ≤ (↑(k * (↑d : ℤ)) : ℝ)
have push_cast : y * (↑d : ℝ) ≤ HMul.hMul (α := ℝ) (↑k : ℝ) (↑d : ℝ)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
k : ℤ
hk : U < (↑k : ℝ)
d : ℕ
z : ℤ
y : ℝ
yS : y ∈ s
hy : (↑z : ℝ) ≤ y * (↑d : ℝ)
⊢ y * (↑d : ℝ) ≤ HMul.hMul (α := ℝ) (↑k : ℝ) (↑d : ℝ)
have hbc : y ≤ (↑k : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (hypothesis)
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
⊢ ∃ (x : ℝ), IsLUB s x
have this : ∀ (d : ℕ), BddAbove (α := ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)}
Tactic: have : ∀ d : ℕ, BddAbove { m : ℤ | ∃ y ∈ s, (m : ℝ) ≤ y * d } := by
    obtain ⟨k, hk⟩ := exists_int_gt U
    refine fun d => ⟨k * d, fun z h => ?_⟩
    rcases h with ⟨y, yS, hy⟩
    refine Int.cast_le.1 (hy.trans ?_)
    push_cast
    gcongr
    exact (hU yS).trans hk.le
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove (α := ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)}
⊢ ∃ (x : ℝ), IsLUB s x
have choose : ∀ (f : (d : ℕ) → ℤ)
  (hf :
    ∀ (d : ℕ),
      Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} (f d) ∧
        ∀ (z : ℤ), Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} z → z ≤ f d),
  ∃ (x : ℝ), IsLUB s x
Tactic: choose f hf using fun d : ℕ =>
    Int.exists_greatest_of_bdd (this d) ⟨⌊L * d⌋, L, hL, Int.floor_le _⟩
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (hypothesis)
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove (α := ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)}
f : (d : ℕ) → ℤ
hf :
  ∀ (d : ℕ),
    Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} (f d) ∧
      ∀ (z : ℤ), Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} z → z ≤ f d
⊢ ∃ (x : ℝ), IsLUB s x
have hf₁ : ∀ n > 0, ∃ y ∈ s, (↑(HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) : ℝ) ≤ y
Tactic: have hf₁ : ∀ n > 0, ∃ y ∈ s, ((f n / n : ℚ) : ℝ) ≤ y := fun n n0 =>
    let ⟨y, yS, hy⟩ := (hf n).1
    ⟨y, yS, by simpa using (div_le_iff₀ (Nat.cast_pos.2 n0 : (_ : ℝ) < _)).2 hy⟩
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (hypothesis)
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove (α := ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)}
f : (d : ℕ) → ℤ
hf :
  ∀ (d : ℕ),
    Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} (f d) ∧
      ∀ (z : ℤ), Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} z → z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, (↑(HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) : ℝ) ≤ y
n : ℕ
n0 : n > 0
y : ℝ
yS : y ∈ s
⊢ y - (↑n : ℝ)⁻¹ < (↑(HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) : ℝ)
have this₁ : y * (↑n : ℝ) - 1 < (↑(f n) : ℝ)
Tactic: have := (Int.sub_one_lt_floor _).trans_le (Int.cast_le.2 <| (hf n).2 _ ⟨y, yS, Int.floor_le _⟩)
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this_1 : ∀ (d : ℕ), BddAbove (α := ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)}
f : (d : ℕ) → ℤ
hf :
  ∀ (d : ℕ),
    Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} (f d) ∧
      ∀ (z : ℤ), Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} z → z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, (↑(HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) : ℝ) ≤ y
n : ℕ
n0 : n > 0
y : ℝ
yS : y ∈ s
this : y * (↑n : ℝ) - 1 < (↑(f n) : ℝ)
⊢ y - (↑n : ℝ)⁻¹ < (↑(HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) : ℝ)
have simp : y - (↑n : ℝ)⁻¹ < HDiv.hDiv (α := ℝ) (↑(f n) : ℝ) (↑n : ℝ)
Tactic: simp only [Rat.cast_div, Rat.cast_intCast, Rat.cast_natCast, gt_iff_lt]
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this_1 : ∀ (d : ℕ), BddAbove (α := ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)}
f : (d : ℕ) → ℤ
hf :
  ∀ (d : ℕ),
    Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} (f d) ∧
      ∀ (z : ℤ), Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} z → z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, (↑(HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) : ℝ) ≤ y
n : ℕ
n0 : n > 0
y : ℝ
yS : y ∈ s
this : y * (↑n : ℝ) - 1 < (↑(f n) : ℝ)
⊢ y - (↑n : ℝ)⁻¹ < HDiv.hDiv (α := ℝ) (↑(f n) : ℝ) (↑n : ℝ)
have rwa : Ne (α := ℝ) (↑n : ℝ) 0
Tactic: rwa [lt_div_iff₀ (Nat.cast_pos.2 n0 : (_ : ℝ) < _), sub_mul, inv_mul_cancel₀]
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (hypothesis)
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove (α := ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)}
f : (d : ℕ) → ℤ
hf :
  ∀ (d : ℕ),
    Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} (f d) ∧
      ∀ (z : ℤ), Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} z → z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, (↑(HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) : ℝ) ≤ y
⊢ ∃ (x : ℝ), IsLUB s x
have hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n : ℝ)⁻¹ < (↑(HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) : ℝ)
Tactic: have hf₂ : ∀ n > 0, ∀ y ∈ s, (y - ((n : ℕ) : ℝ)⁻¹) < (f n / n : ℚ) := by
    intro n n0 y yS
    have := (Int.sub_one_lt_floor _).trans_le (Int.cast_le.2 <| (hf n).2 _ ⟨y, yS, Int.floor_le _⟩)
    simp only [Rat.cast_div, Rat.cast_intCast, Rat.cast_natCast, gt_iff_lt]
    rwa [lt_div_iff₀ (Nat.cast_pos.2 n0 : (_ : ℝ) < _), sub_mul, inv_mul_cancel₀]
    exact (Nat.cast_pos.2 n0).ne'
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this_1 : ∀ (d : ℕ), BddAbove (α := ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)}
f : (d : ℕ) → ℤ
hf :
  ∀ (d : ℕ),
    Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} (f d) ∧
      ∀ (z : ℤ), Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} z → z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, (↑(HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) : ℝ) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n : ℝ)⁻¹ < (↑(HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) : ℝ)
ε : ℚ
ε0 : ε > 0
this :
  ∀ j ≥ ⌈ε⁻¹⌉₊, ∀ k ≥ ⌈ε⁻¹⌉₊, HDiv.hDiv (α := ℚ) (↑(f j) : ℚ) (↑j : ℚ) - HDiv.hDiv (α := ℚ) (↑(f k) : ℚ) (↑k : ℚ) < ε
⊢ ∃ (i : ℕ),
    ∀ j ≥ i,
      |HSub.hSub (α := ℚ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) j)
            ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) i)| <
        ε
have refine : ∀ (j : ℕ) (ij : j ≥ ⌈ε⁻¹⌉₊),
  -ε <
    HSub.hSub (α := ℚ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) j)
      ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) ⌈ε⁻¹⌉₊)
Tactic: refine ⟨_, fun j ij => abs_lt.2 ⟨?_, this _ ij _ le_rfl⟩⟩
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this_1 : ∀ (d : ℕ), BddAbove (α := ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)}
f : (d : ℕ) → ℤ
hf :
  ∀ (d : ℕ),
    Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} (f d) ∧
      ∀ (z : ℤ), Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} z → z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, (↑(HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) : ℝ) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n : ℝ)⁻¹ < (↑(HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) : ℝ)
ε : ℚ
ε0 : ε > 0
this :
  ∀ j ≥ ⌈ε⁻¹⌉₊, ∀ k ≥ ⌈ε⁻¹⌉₊, HDiv.hDiv (α := ℚ) (↑(f j) : ℚ) (↑j : ℚ) - HDiv.hDiv (α := ℚ) (↑(f k) : ℚ) (↑k : ℚ) < ε
j : ℕ
ij : j ≥ ⌈ε⁻¹⌉₊
⊢ -ε <
    HSub.hSub (α := ℚ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) j)
      ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) ⌈ε⁻¹⌉₊)
have rw : HSub.hSub (α := ℚ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) ⌈ε⁻¹⌉₊)
    ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) j) <
  ε
Tactic: rw [neg_lt, neg_sub]
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove (α := ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)}
f : (d : ℕ) → ℤ
hf :
  ∀ (d : ℕ),
    Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} (f d) ∧
      ∀ (z : ℤ), Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} z → z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, (↑(HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) : ℝ) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n : ℝ)⁻¹ < (↑(HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) : ℝ)
ε : ℚ
ε0 : ε > 0
⊢ ∃ (i : ℕ),
    ∀ j ≥ i,
      |HSub.hSub (α := ℚ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) j)
            ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) i)| <
        ε
have suffices : ∀ j ≥ ⌈ε⁻¹⌉₊, ∀ k ≥ ⌈ε⁻¹⌉₊, HDiv.hDiv (α := ℚ) (↑(f j) : ℚ) (↑j : ℚ) - HDiv.hDiv (α := ℚ) (↑(f k) : ℚ) (↑k : ℚ) < ε
Tactic: suffices ∀ j ≥ ⌈ε⁻¹⌉₊, ∀ k ≥ ⌈ε⁻¹⌉₊, (f j / j - f k / k : ℚ) < ε by
      refine ⟨_, fun j ij => abs_lt.2 ⟨?_, this _ ij _ le_rfl⟩⟩
      rw [neg_lt, neg_sub]
      exact this _ le_rfl _ ij
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (hypothesis)
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove (α := ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)}
f : (d : ℕ) → ℤ
hf :
  ∀ (d : ℕ),
    Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} (f d) ∧
      ∀ (z : ℤ), Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} z → z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, (↑(HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) : ℝ) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n : ℝ)⁻¹ < (↑(HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) : ℝ)
ε : ℚ
ε0 : ε > 0
j : ℕ
ij : j ≥ ⌈ε⁻¹⌉₊
k : ℕ
ik : k ≥ ⌈ε⁻¹⌉₊
⊢ HDiv.hDiv (α := ℚ) (↑(f j) : ℚ) (↑j : ℚ) - HDiv.hDiv (α := ℚ) (↑(f k) : ℚ) (↑k : ℚ) < ε
have ij₁ : ε⁻¹ ≤ (↑j : ℚ)
Tactic: replace ij := le_trans (Nat.le_ceil _) (Nat.cast_le.2 ij)
Cleared hypotheses: ij
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (hypothesis)
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove (α := ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)}
f : (d : ℕ) → ℤ
hf :
  ∀ (d : ℕ),
    Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} (f d) ∧
      ∀ (z : ℤ), Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} z → z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, (↑(HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) : ℝ) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n : ℝ)⁻¹ < (↑(HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) : ℝ)
ε : ℚ
ε0 : ε > 0
j k : ℕ
ik : k ≥ ⌈ε⁻¹⌉₊
ij : ε⁻¹ ≤ (↑j : ℚ)
⊢ HDiv.hDiv (α := ℚ) (↑(f j) : ℚ) (↑j : ℚ) - HDiv.hDiv (α := ℚ) (↑(f k) : ℚ) (↑k : ℚ) < ε
have ik₁ : ε⁻¹ ≤ (↑k : ℚ)
Tactic: replace ik := le_trans (Nat.le_ceil _) (Nat.cast_le.2 ik)
Cleared hypotheses: ik
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (hypothesis)
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove (α := ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)}
f : (d : ℕ) → ℤ
hf :
  ∀ (d : ℕ),
    Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} (f d) ∧
      ∀ (z : ℤ), Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} z → z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, (↑(HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) : ℝ) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n : ℝ)⁻¹ < (↑(HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) : ℝ)
ε : ℚ
ε0 : ε > 0
j k : ℕ
ij : ε⁻¹ ≤ (↑j : ℚ)
ik : ε⁻¹ ≤ (↑k : ℚ)
⊢ HDiv.hDiv (α := ℚ) (↑(f j) : ℚ) (↑j : ℚ) - HDiv.hDiv (α := ℚ) (↑(f k) : ℚ) (↑k : ℚ) < ε
have j0 : 0 < j
Tactic: have j0 := Nat.cast_pos.1 ((inv_pos.2 ε0).trans_le ij)
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (hypothesis)
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove (α := ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)}
f : (d : ℕ) → ℤ
hf :
  ∀ (d : ℕ),
    Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} (f d) ∧
      ∀ (z : ℤ), Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} z → z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, (↑(HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) : ℝ) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n : ℝ)⁻¹ < (↑(HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) : ℝ)
ε : ℚ
ε0 : ε > 0
j k : ℕ
ij : ε⁻¹ ≤ (↑j : ℚ)
ik : ε⁻¹ ≤ (↑k : ℚ)
j0 : 0 < j
⊢ HDiv.hDiv (α := ℚ) (↑(f j) : ℚ) (↑j : ℚ) - HDiv.hDiv (α := ℚ) (↑(f k) : ℚ) (↑k : ℚ) < ε
have k0 : 0 < k
Tactic: have k0 := Nat.cast_pos.1 ((inv_pos.2 ε0).trans_le ik)
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove (α := ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)}
f : (d : ℕ) → ℤ
hf :
  ∀ (d : ℕ),
    Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} (f d) ∧
      ∀ (z : ℤ), Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} z → z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, (↑(HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) : ℝ) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n : ℝ)⁻¹ < (↑(HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) : ℝ)
ε : ℚ
ε0 : ε > 0
j k : ℕ
ij : ε⁻¹ ≤ (↑j : ℚ)
ik : ε⁻¹ ≤ (↑k : ℚ)
j0 : 0 < j
k0 : 0 < k
⊢ HDiv.hDiv (α := ℚ) (↑(f j) : ℚ) (↑j : ℚ) - HDiv.hDiv (α := ℚ) (↑(f k) : ℚ) (↑k : ℚ) < ε
have rcases : ∀ (y : ℝ) (yS : y ∈ s) (hy : (↑(HDiv.hDiv (α := ℚ) (↑(f j) : ℚ) (↑j : ℚ)) : ℝ) ≤ y),
  HDiv.hDiv (α := ℚ) (↑(f j) : ℚ) (↑j : ℚ) - HDiv.hDiv (α := ℚ) (↑(f k) : ℚ) (↑k : ℚ) < ε
Tactic: rcases hf₁ _ j0 with ⟨y, yS, hy⟩
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove (α := ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)}
f : (d : ℕ) → ℤ
hf :
  ∀ (d : ℕ),
    Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} (f d) ∧
      ∀ (z : ℤ), Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} z → z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, (↑(HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) : ℝ) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n : ℝ)⁻¹ < (↑(HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) : ℝ)
ε : ℚ
ε0 : ε > 0
j k : ℕ
ij : ε⁻¹ ≤ (↑j : ℚ)
ik : ε⁻¹ ≤ (↑k : ℚ)
j0 : 0 < j
k0 : 0 < k
y : ℝ
yS : y ∈ s
hy : (↑(HDiv.hDiv (α := ℚ) (↑(f j) : ℚ) (↑j : ℚ)) : ℝ) ≤ y
⊢ HDiv.hDiv (α := ℚ) (↑(f j) : ℚ) (↑j : ℚ) - HDiv.hDiv (α := ℚ) (↑(f k) : ℚ) (↑k : ℚ) < ε
have refine : LT.lt (α := ℝ) (↑(HDiv.hDiv (α := ℚ) (↑(f j) : ℚ) (↑j : ℚ) - HDiv.hDiv (α := ℚ) (↑(f k) : ℚ) (↑k : ℚ)) : ℝ)
  (↑(↑k : ℚ)⁻¹ : ℝ)
Tactic: refine lt_of_lt_of_le ((Rat.cast_lt (K := ℝ)).1 ?_) ((inv_le_comm₀ ε0 (Nat.cast_pos.2 k0)).1 ik)
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (hypothesis)
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove (α := ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)}
f : (d : ℕ) → ℤ
hf :
  ∀ (d : ℕ),
    Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} (f d) ∧
      ∀ (z : ℤ), Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} z → z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, (↑(HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) : ℝ) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n : ℝ)⁻¹ < (↑(HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) : ℝ)
⊢ ∃ (x : ℝ), IsLUB s x
have hg : IsCauSeq (α := ℚ) abs fun (n : ℕ) ↦ HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)
Tactic: have hg : IsCauSeq abs (fun n => f n / n : ℕ → ℚ) := by
    intro ε ε0
    suffices ∀ j ≥ ⌈ε⁻¹⌉₊, ∀ k ≥ ⌈ε⁻¹⌉₊, (f j / j - f k / k : ℚ) < ε by
      refine ⟨_, fun j ij => abs_lt.2 ⟨?_, this _ ij _ le_rfl⟩⟩
      rw [neg_lt, neg_sub]
      exact this _ le_rfl _ ij
    intro j ij k ik
    replace ij := le_trans (Nat.le_ceil _) (Nat.cast_le.2 ij)
    replace ik := le_trans (Nat.le_ceil _) (Nat.cast_le.2 ik)
    have j0 := Nat.cast_pos.1 ((inv_pos.2 ε0).trans_le ij)
    have k0 := Nat.cast_pos.1 ((inv_pos.2 ε0).trans_le ik)
    rcases hf₁ _ j0 with ⟨y, yS, hy⟩
    refine lt_of_lt_of_le ((Rat.cast_lt (K := ℝ)).1 ?_) ((inv_le_comm₀ ε0 (Nat.cast_pos.2 k0)).1 ik)
    simpa using sub_lt_iff_lt_add'.2 (lt_of_le_of_lt hy <| sub_lt_iff_lt_add.1 <| hf₂ _ k0 _ yS)
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove (α := ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)}
f : (d : ℕ) → ℤ
hf :
  ∀ (d : ℕ),
    Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} (f d) ∧
      ∀ (z : ℤ), Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} z → z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, (↑(HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) : ℝ) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n : ℝ)⁻¹ < (↑(HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) : ℝ)
hg : IsCauSeq (α := ℚ) abs fun (n : ℕ) ↦ HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)
g : CauSeq ℚ abs :=
  Subtype.mk (p := fun (f : ℕ → ℚ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) hg
⊢ ∃ (x : ℝ), IsLUB s x
have refine_1 : ∀ (x : ℝ) (xS : x ∈ s), x ≤ mk g
Tactic: refine ⟨mk g, ⟨fun x xS => ?_, fun y h => ?_⟩⟩
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove (α := ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)}
f : (d : ℕ) → ℤ
hf :
  ∀ (d : ℕ),
    Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} (f d) ∧
      ∀ (z : ℤ), Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} z → z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, (↑(HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) : ℝ) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n : ℝ)⁻¹ < (↑(HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) : ℝ)
hg : IsCauSeq (α := ℚ) abs fun (n : ℕ) ↦ HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)
g : CauSeq ℚ abs :=
  Subtype.mk (p := fun (f : ℕ → ℚ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) hg
refine_1 : ∀ (x : ℝ) (xS : x ∈ s), x ≤ mk g
⊢ ∃ (x : ℝ), IsLUB s x
have refine_2 : ∀ (y : ℝ) (h : y ∈ upperBounds s), mk g ≤ y
Tactic: refine ⟨mk g, ⟨fun x xS => ?_, fun y h => ?_⟩⟩
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove (α := ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)}
f : (d : ℕ) → ℤ
hf :
  ∀ (d : ℕ),
    Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} (f d) ∧
      ∀ (z : ℤ), Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} z → z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, (↑(HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) : ℝ) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n : ℝ)⁻¹ < (↑(HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) : ℝ)
hg : IsCauSeq (α := ℚ) abs fun (n : ℕ) ↦ HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)
g : CauSeq ℚ abs :=
  Subtype.mk (p := fun (f : ℕ → ℚ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) hg
x : ℝ
xS : x ∈ s
⊢ x ≤ mk g
have refine_1 : ∀ (z : ℝ) (xz : z < x), z ≤ mk g
Tactic: refine le_of_forall_lt_imp_le_of_dense fun z xz => ?_
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove (α := ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)}
f : (d : ℕ) → ℤ
hf :
  ∀ (d : ℕ),
    Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} (f d) ∧
      ∀ (z : ℤ), Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} z → z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, (↑(HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) : ℝ) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n : ℝ)⁻¹ < (↑(HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) : ℝ)
hg : IsCauSeq (α := ℚ) abs fun (n : ℕ) ↦ HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)
g : CauSeq ℚ abs :=
  Subtype.mk (p := fun (f : ℕ → ℚ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) hg
x : ℝ
xS : x ∈ s
z : ℝ
xz : z < x
⊢ z ≤ mk g
have refine_1 : ∀ (K : ℕ) (hK : (x - z)⁻¹ < (↑K : ℝ)), z ≤ mk g
Tactic: obtain ⟨K, hK⟩ := exists_nat_gt (x - z)⁻¹