awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
f : CauSeq ℝ abs
s : Set ℝ := {x : ℝ | const abs x < f}
lb : ∃ (x : ℝ), x ∈ s
ub' : ∀ (x : ℝ), f < const abs x → ∀ y ∈ s, y ≤ x
ub : ∃ (x : ℝ), ∀ y ∈ s, y ≤ x
ε : ℝ
ε0 : ε > 0
i : ℕ
ih : ∀ j ≥ i, ε ≤ (↑(f - const abs (sSup s)) : ℕ → ℝ) j
⊢ False
have refine_2 : ε / 2 + sSup s ∈ s
Tactic: refine (le_csSup ub ?_).not_gt ((lt_add_iff_pos_left _).2 (half_pos ε0))
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
f : CauSeq ℝ abs
s : Set ℝ := {x : ℝ | const abs x < f}
lb : ∃ (x : ℝ), x ∈ s
ub' : ∀ (x : ℝ), f < const abs x → ∀ y ∈ s, y ≤ x
ub : ∃ (x : ℝ), ∀ y ∈ s, y ≤ x
ε : ℝ
ε0 : ε > 0
i : ℕ
ih : ∀ j ≥ i, ε ≤ (↑(f - const abs (sSup s)) : ℕ → ℝ) j
⊢ ε / 2 + sSup s ∈ s
have refine_2 : ∀ (j : ℕ) (ij : j ≥ i), ε / 2 ≤ (↑(f - const abs (ε / 2 + sSup s)) : ℕ → ℝ) j
Tactic: refine ⟨_, half_pos ε0, i, fun j ij => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
f : CauSeq ℝ abs
s : Set ℝ := {x : ℝ | const abs x < f}
lb : ∃ (x : ℝ), x ∈ s
ub' : ∀ (x : ℝ), f < const abs x → ∀ y ∈ s, y ≤ x
ub : ∃ (x : ℝ), ∀ y ∈ s, y ≤ x
ε : ℝ
ε0 : ε > 0
i : ℕ
ih : ∀ j ≥ i, ε ≤ (↑(f - const abs (sSup s)) : ℕ → ℝ) j
j : ℕ
ij : j ≥ i
⊢ ε / 2 ≤ (↑(f - const abs (ε / 2 + sSup s)) : ℕ → ℝ) j
have refine_2 : ε ≤ (↑f : ℕ → ℝ) j - sSup s
Tactic: rw [sub_apply, const_apply, add_comm, ← sub_sub, le_sub_iff_add_le, add_halves]
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
⊢ Eq (α := ℝ) (⨅ (r : (↑(Ioi x) : Type)), f (↑r : ℝ)) (⨅ (q : { q' : ℚ // x < (↑q' : ℝ) }), f (↑(↑q : ℚ) : ℝ))
have refine_1 : LE.le (α := ℝ) (⨅ (r : (↑(Ioi x) : Type)), f (↑r : ℝ)) (⨅ (q : { q' : ℚ // x < (↑q' : ℝ) }), f (↑(↑q : ℚ) : ℝ))
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
refine_1 :
  LE.le (α := ℝ) (⨅ (r : (↑(Ioi x) : Type)), f (↑r : ℝ)) (⨅ (q : { q' : ℚ // x < (↑q' : ℝ) }), f (↑(↑q : ℚ) : ℝ))
⊢ Eq (α := ℝ) (⨅ (r : (↑(Ioi x) : Type)), f (↑r : ℝ)) (⨅ (q : { q' : ℚ // x < (↑q' : ℝ) }), f (↑(↑q : ℚ) : ℝ))
have refine_2 : LE.le (α := ℝ) (⨅ (q : { q' : ℚ // x < (↑q' : ℝ) }), f (↑(↑q : ℚ) : ℝ)) (⨅ (r : (↑(Ioi x) : Type)), f (↑r : ℝ))
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
⊢ Nonempty { r' : ℚ // x < (↑r' : ℝ) }
have obtain : ∀ (r : ℚ) (hrx : x < (↑r : ℝ)), Nonempty { r' : ℚ // x < (↑r' : ℝ) }
Tactic: obtain ⟨r, hrx⟩ := exists_rat_gt x
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (hypothesis)
Goal:
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
⊢ LE.le (α := ℝ) (⨅ (r : (↑(Ioi x) : Type)), f (↑r : ℝ)) (⨅ (q : { q' : ℚ // x < (↑q' : ℝ) }), f (↑(↑q : ℚ) : ℝ))
have this : Nonempty { r' : ℚ // x < (↑r' : ℝ) }
Tactic: have : Nonempty { r' : ℚ // x < ↑r' } := by
      obtain ⟨r, hrx⟩ := exists_rat_gt x
      exact ⟨⟨r, hrx⟩⟩
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
this : Nonempty { r' : ℚ // x < (↑r' : ℝ) }
⊢ LE.le (α := ℝ) (⨅ (r : (↑(Ioi x) : Type)), f (↑r : ℝ)) (⨅ (q : { q' : ℚ // x < (↑q' : ℝ) }), f (↑(↑q : ℚ) : ℝ))
have refine_1 : ∀ (r : { q' : ℚ // x < (↑q' : ℝ) }), ⨅ (r : (↑(Ioi x) : Type)), f (↑r : ℝ) ≤ f (↑(↑r : ℚ) : ℝ)
Tactic: refine le_ciInf fun r => ?_
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
this : Nonempty { r' : ℚ // x < (↑r' : ℝ) }
r : { q' : ℚ // x < (↑q' : ℝ) }
⊢ ⨅ (r : (↑(Ioi x) : Type)), f (↑r : ℝ) ≤ f (↑(↑r : ℚ) : ℝ)
have refine_1 : ∀ (y : ℚ) (hxy : x < (↑y : ℝ)) (hyr : LT.lt (α := ℝ) (↑y : ℝ) (↑(↑r : ℚ) : ℝ)),
  ⨅ (r : (↑(Ioi x) : Type)), f (↑r : ℝ) ≤ f (↑(↑r : ℚ) : ℝ)
Tactic: obtain ⟨y, hxy, hyr⟩ := exists_rat_btwn r.prop
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
⊢ LE.le (α := ℝ) (⨅ (q : { q' : ℚ // x < (↑q' : ℝ) }), f (↑(↑q : ℚ) : ℝ)) (⨅ (r : (↑(Ioi x) : Type)), f (↑r : ℝ))
have refine_2 : ∀ (q : (↑(Ioi x) : Type)), ⨅ (q : { q' : ℚ // x < (↑q' : ℝ) }), f (↑(↑q : ℚ) : ℝ) ≤ f (↑q : ℝ)
Tactic: refine le_ciInf fun q => ?_
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (hypothesis)
Goal:
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : (↑(Ioi x) : Type)
⊢ ⨅ (q : { q' : ℚ // x < (↑q' : ℝ) }), f (↑(↑q : ℚ) : ℝ) ≤ f (↑q : ℝ)
have hq : (↑q : ℝ) ∈ Ioi x
Tactic: have hq := q.prop
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (hypothesis)
Goal:
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : (↑(Ioi x) : Type)
hq : (↑q : ℝ) ∈ Ioi x
⊢ ⨅ (q : { q' : ℚ // x < (↑q' : ℝ) }), f (↑(↑q : ℚ) : ℝ) ≤ f (↑q : ℝ)
have hq₁ : x < (↑q : ℝ)
Tactic: rw [mem_Ioi] at hq
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : (↑(Ioi x) : Type)
hq : x < (↑q : ℝ)
⊢ ⨅ (q : { q' : ℚ // x < (↑q' : ℝ) }), f (↑(↑q : ℚ) : ℝ) ≤ f (↑q : ℝ)
have refine_2 : ∀ (y : ℚ) (hxy : x < (↑y : ℝ)) (hyq : (↑y : ℝ) < (↑q : ℝ)),
  ⨅ (q : { q' : ℚ // x < (↑q' : ℝ) }), f (↑(↑q : ℚ) : ℝ) ≤ f (↑q : ℝ)
Tactic: obtain ⟨y, hxy, hyq⟩ := exists_rat_btwn hq
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : (↑(Ioi x) : Type)
hq : x < (↑q : ℝ)
y : ℚ
hxy : x < (↑y : ℝ)
hyq : (↑y : ℝ) < (↑q : ℝ)
⊢ ⨅ (q : { q' : ℚ // x < (↑q' : ℝ) }), f (↑(↑q : ℚ) : ℝ) ≤ f (↑q : ℝ)
have refine_2 : BddBelow (α := ℝ) (range fun (q : { q' : ℚ // x < (↑q' : ℝ) }) ↦ f (↑(↑q : ℚ) : ℝ))
Tactic: refine (ciInf_le ?_ ?_).trans ?_
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : (↑(Ioi x) : Type)
hq : x < (↑q : ℝ)
y : ℚ
hxy : x < (↑y : ℝ)
hyq : (↑y : ℝ) < (↑q : ℝ)
refine_2 : BddBelow (α := ℝ) (range fun (q : { q' : ℚ // x < (↑q' : ℝ) }) ↦ f (↑(↑q : ℚ) : ℝ))
⊢ ⨅ (q : { q' : ℚ // x < (↑q' : ℝ) }), f (↑(↑q : ℚ) : ℝ) ≤ f (↑q : ℝ)
have refine_2₁ : { q' : ℚ // x < (↑q' : ℝ) }
Tactic: refine (ciInf_le ?_ ?_).trans ?_
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : (↑(Ioi x) : Type)
hq : x < (↑q : ℝ)
y : ℚ
hxy : x < (↑y : ℝ)
hyq : (↑y : ℝ) < (↑q : ℝ)
refine_2 : BddBelow (α := ℝ) (range fun (q : { q' : ℚ // x < (↑q' : ℝ) }) ↦ f (↑(↑q : ℚ) : ℝ))
refine_2₁ : { q' : ℚ // x < (↑q' : ℝ) }
⊢ ⨅ (q : { q' : ℚ // x < (↑q' : ℝ) }), f (↑(↑q : ℚ) : ℝ) ≤ f (↑q : ℝ)
have refine_2₂ : f (↑(↑(Subtype.mk (p := fun (q' : ℚ) ↦ x < (↑q' : ℝ)) y hxy) : ℚ) : ℝ) ≤ f (↑q : ℝ)
Tactic: refine (ciInf_le ?_ ?_).trans ?_
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : (↑(Ioi x) : Type)
hq : x < (↑q : ℝ)
y : ℚ
hxy : x < (↑y : ℝ)
hyq : (↑y : ℝ) < (↑q : ℝ)
⊢ BddBelow (α := ℝ) (range fun (q : { q' : ℚ // x < (↑q' : ℝ) }) ↦ f (↑(↑q : ℚ) : ℝ))
have refine_2 : ∀ (z : ℝ),
  Membership.mem (γ := Set ℝ) (range fun (q : { q' : ℚ // x < (↑q' : ℝ) }) ↦ f (↑(↑q : ℚ) : ℝ)) z →
    Set.Nonempty.some (s := lowerBounds (f '' Ioi x)) hf ≤ z
Tactic: refine ⟨hf.some, fun z => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : (↑(Ioi x) : Type)
hq : x < (↑q : ℝ)
y : ℚ
hxy : x < (↑y : ℝ)
hyq : (↑y : ℝ) < (↑q : ℝ)
u : { q' : ℚ // x < (↑q' : ℝ) }
⊢ Set.Nonempty.some (s := lowerBounds (f '' Ioi x)) hf ≤ (fun (q : { q' : ℚ // x < (↑q' : ℝ) }) ↦ f (↑(↑q : ℚ) : ℝ)) u
have refine_2 : f (↑(↑u : ℚ) : ℝ) ∈ f '' Ioi x
Tactic: suffices hfu : f u ∈ f '' Ioi x from hf.choose_spec hfu
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : (↑(Ioi x) : Type)
hq : x < (↑q : ℝ)
y : ℚ
hxy : x < (↑y : ℝ)
hyq : (↑y : ℝ) < (↑q : ℝ)
⊢ f (↑(↑(Subtype.mk (p := fun (q' : ℚ) ↦ x < (↑q' : ℝ)) y hxy) : ℚ) : ℝ) ≤ f (↑q : ℝ)
have refine_2 : LE.le (α := ℝ) (↑(↑(Subtype.mk (p := fun (q' : ℚ) ↦ x < (↑q' : ℝ)) y hxy) : ℚ) : ℝ) (↑y : ℝ)
Tactic: refine hf_mono (le_trans ?_ hyq.le)
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : (↑(Ioi x) : Type)
hq : x < (↑q : ℝ)
y : ℚ
hxy : x < (↑y : ℝ)
hyq : (↑y : ℝ) < (↑q : ℝ)
⊢ LE.le (α := ℝ) (↑(↑(Subtype.mk (p := fun (q' : ℚ) ↦ x < (↑q' : ℝ)) y hxy) : ℚ) : ℝ) (↑y : ℝ)
have refine_2 : (↑(Subtype.mk (p := fun (q' : ℚ) ↦ x < (↑q' : ℝ)) y hxy) : ℚ) ≤
  (↑(Subtype.mk (p := fun (q' : ℚ) ↦ x < (↑q' : ℝ)) y hxy) : ℚ)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
⊢ ¬Set.Nonempty (α := ℝ) {x : ℝ | ∀ ⦃a : ℝ⦄, Membership.mem (γ := Set ℝ) (range fun (x : ℚ) ↦ (↑x : ℝ)) a → a ≤ x}
have rw : Eq (α := Set ℝ) {x : ℝ | ∀ ⦃a : ℝ⦄, Membership.mem (γ := Set ℝ) (range fun (x : ℚ) ↦ (↑x : ℝ)) a → a ≤ x} ∅
Tactic: rw [Set.not_nonempty_iff_eq_empty]
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
⊢ Eq (α := Set ℝ) {x : ℝ | ∀ ⦃a : ℝ⦄, Membership.mem (γ := Set ℝ) (range fun (x : ℚ) ↦ (↑x : ℝ)) a → a ≤ x} ∅
have h : ∀ (x : ℝ),
  Membership.mem (γ := Set ℝ) {x : ℝ | ∀ ⦃a : ℝ⦄, Membership.mem (γ := Set ℝ) (range fun (x : ℚ) ↦ (↑x : ℝ)) a → a ≤ x}
      x ↔
    Membership.mem (γ := Set ℝ) ∅ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
⊢ ¬Set.Nonempty (α := ℝ) {x : ℝ | ∀ ⦃a : ℝ⦄, Membership.mem (γ := Set ℝ) (range fun (x : ℚ) ↦ (↑x : ℝ)) a → x ≤ a}
have rw : Eq (α := Set ℝ) {x : ℝ | ∀ ⦃a : ℝ⦄, Membership.mem (γ := Set ℝ) (range fun (x : ℚ) ↦ (↑x : ℝ)) a → x ≤ a} ∅
Tactic: rw [Set.not_nonempty_iff_eq_empty]
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
⊢ Eq (α := Set ℝ) {x : ℝ | ∀ ⦃a : ℝ⦄, Membership.mem (γ := Set ℝ) (range fun (x : ℚ) ↦ (↑x : ℝ)) a → x ≤ a} ∅
have h : ∀ (x : ℝ),
  Membership.mem (γ := Set ℝ) {x : ℝ | ∀ ⦃a : ℝ⦄, Membership.mem (γ := Set ℝ) (range fun (x : ℚ) ↦ (↑x : ℝ)) a → x ≤ a}
      x ↔
    Membership.mem (γ := Set ℝ) ∅ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
a : ℝ
ha : 1 < a
⊢ ∃ (k : ℕ), 0 < k ∧ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1 < a
have contrapose! : ∀ (ha : ∀ (k : ℕ) (_ : 0 < k), a ≤ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1), a ≤ 1
Tactic: contrapose! ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
a : ℝ
ha : ∀ (k : ℕ) (_ : 0 < k), a ≤ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1
⊢ a ≤ 1
have refine : ∀ (q : ℚ), LT.lt (α := ℝ) 1 (↑q : ℝ) → a ≤ (↑q : ℝ)
Tactic: refine le_of_forall_lt_rat_imp_le ?_
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
a : ℝ
ha : ∀ (k : ℕ) (_ : 0 < k), a ≤ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1
q : ℚ
hq : LT.lt (α := ℝ) 1 (↑q : ℝ)
⊢ a ≤ (↑q : ℝ)
have refine : HDiv.hDiv (α := ℝ) 1 (↑q.den : ℝ) + 1 ≤ (↑q : ℝ)
Tactic: refine (ha q.den (by positivity)).trans ?_
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
a : ℝ
ha : ∀ (k : ℕ) (_ : 0 < k), a ≤ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1
q : ℚ
hq : LT.lt (α := ℝ) 1 (↑q : ℝ)
⊢ HDiv.hDiv (α := ℝ) 1 (↑q.den : ℝ) + 1 ≤ (↑q : ℝ)
have rw : 1 ≤ HMul.hMul (α := ℝ) (↑q : ℝ) (↑q.den : ℝ) - (↑q.den : ℝ)
Tactic: rw [← le_sub_iff_add_le, div_le_iff₀ (by positivity), sub_mul, one_mul]
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
a : ℝ
ha : ∀ (k : ℕ) (_ : 0 < k), a ≤ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1
q : ℚ
hq : LT.lt (α := ℝ) 1 (↑q : ℝ)
⊢ 1 ≤ HMul.hMul (α := ℝ) (↑q : ℝ) (↑q.den : ℝ) - (↑q.den : ℝ)
have norm_cast : ∀ (hq : 1 < q), 1 ≤ q * (↑q.den : ℚ) - (↑q.den : ℚ)
Tactic: norm_cast at hq ⊢
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (hypothesis)
Goal:
a : ℝ
ha : ∀ (k : ℕ) (_ : 0 < k), a ≤ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1
q : ℚ
hq : 1 < q
⊢ 1 ≤ q * (↑q.den : ℚ) - (↑q.den : ℚ)
have hq₁ : LT.lt (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
Tactic: rw [← q.num_div_den, one_lt_div (by positivity)] at hq
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
a : ℝ
ha : ∀ (k : ℕ) (_ : 0 < k), a ≤ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1
q : ℚ
hq : LT.lt (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
⊢ 1 ≤ q * (↑q.den : ℚ) - (↑q.den : ℚ)
have rw : 1 ≤ HSub.hSub (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)
Tactic: rw [q.mul_den_eq_num]
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
a : ℝ
ha : ∀ (k : ℕ) (_ : 0 < k), a ≤ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1
q : ℚ
hq : LT.lt (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
⊢ 1 ≤ HSub.hSub (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)
have norm_cast : ∀ (hq : (↑q.den : ℤ) < q.num), 1 ≤ q.num - (↑q.den : ℤ)
Tactic: norm_cast at hq ⊢
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
a : ℝ
ha : 1 < a
⊢ ∃ (m : ℕ), HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 < a ^ m
have obtain : ∀ (k : ℕ) (posk : 0 < k) (hk : HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1 < a), ∃ (m : ℕ), HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 < a ^ m
Tactic: obtain ⟨k, posk, hk⟩ : ∃ k : ℕ, 0 < k ∧ 1 / k + 1 < a := by
    contrapose! ha
    refine le_of_forall_lt_rat_imp_le ?_
    intro q hq
    refine (ha q.den (by positivity)).trans ?_
    rw [← le_sub_iff_add_le, div_le_iff₀ (by positivity), sub_mul, one_mul]
    norm_cast at hq ⊢
    rw [← q.num_div_den, one_lt_div (by positivity)] at hq
    rw [q.mul_den_eq_num]
    norm_cast at hq ⊢
    lia
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1 < a
⊢ ∃ (m : ℕ), HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 < a ^ m
have h : HAdd.hAdd (α := ℝ) (↑(2 * HPow.hPow (β := ℕ) k 2) : ℝ) 1 < a ^ (2 * HPow.hPow (β := ℕ) k 2)
Tactic: use 2 * k ^ 2
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1 < a
⊢ HPow.hPow (α := ℝ) 2 (2 * k) = (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) * (↑k : ℝ) + 1) ^ (2 * k)
have simp : 2 = HAdd.hAdd (α := ℝ) 1 1
Tactic: simp [posk.ne']
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1 < a
⊢ (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) * (↑k : ℝ) + 1) ^ (2 * k) ≤ ((HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ k) ^ (2 * k)
have hab : HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) * (↑k : ℝ) + 1 ≤ (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ k
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1 < a
⊢ ((HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ k) ^ (2 * k) =
    (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ (2 * HPow.hPow (β := ℕ) k 2)
have rw : (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ (k * (2 * k)) = (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ (2 * HPow.hPow (β := ℕ) k 2)
Tactic: rw [← pow_mul, mul_left_comm, sq]
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1 < a
rw :
  (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ (k * (2 * k)) =
    (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ (2 * HPow.hPow (β := ℕ) k 2)
⊢ ((HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ k) ^ (2 * k) =
    (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ (2 * HPow.hPow (β := ℕ) k 2)
have rw₁ : (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ (2 * (k * k)) = (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ (2 * HPow.hPow (β := ℕ) k 2)
Tactic: rw [← pow_mul, mul_left_comm, sq]
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1 < a
rw :
  (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ (k * (2 * k)) =
    (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ (2 * HPow.hPow (β := ℕ) k 2)
rw₁ :
  (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ (2 * (k * k)) =
    (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ (2 * HPow.hPow (β := ℕ) k 2)
⊢ ((HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ k) ^ (2 * k) =
    (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ (2 * HPow.hPow (β := ℕ) k 2)
have rw₂ : (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ (2 * (k * k)) = (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ (2 * (k * k))
Tactic: rw [← pow_mul, mul_left_comm, sq]
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1 < a
⊢ (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ (2 * HPow.hPow (β := ℕ) k 2) < a ^ (2 * HPow.hPow (β := ℕ) k 2)
have ha₁ : 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1 < a
ha₁ : 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1
⊢ (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ (2 * HPow.hPow (β := ℕ) k 2) < a ^ (2 * HPow.hPow (β := ℕ) k 2)
have a₁ : 2 * HPow.hPow (β := ℕ) k 2 ≠ 0
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1 < a
⊢ HAdd.hAdd (α := ℝ) (↑(2 * HPow.hPow (β := ℕ) k 2) : ℝ) 1 < a ^ (2 * HPow.hPow (β := ℕ) k 2)
have k₁ : HPow.hPow (α := ℝ) 2 (2 * k) = (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) * (↑k : ℝ) + 1) ^ (2 * k)
Tactic: calc
    ((2 * k ^ 2 : ℕ) + 1 : ℝ) ≤ 2 ^ (2 * k) := mod_cast Nat.two_mul_sq_add_one_le_two_pow_two_mul _
    _ = (1 / k * k + 1 : ℝ) ^ (2 * k) := by simp [posk.ne']; norm_num
    _ ≤ ((1 / k + 1) ^ k : ℝ) ^ (2 * k) := by gcongr; exact mul_add_one_le_add_one_pow (by simp) _
    _ = (1 / k + 1 : ℝ) ^ (2 * k ^ 2) := by rw [← pow_mul, mul_left_comm, sq]
    _ < a ^ (2 * k ^ 2) := by gcongr
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1 < a
k₁ : HPow.hPow (α := ℝ) 2 (2 * k) = (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) * (↑k : ℝ) + 1) ^ (2 * k)
⊢ HAdd.hAdd (α := ℝ) (↑(2 * HPow.hPow (β := ℕ) k 2) : ℝ) 1 < a ^ (2 * HPow.hPow (β := ℕ) k 2)
have k₂ : (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) * (↑k : ℝ) + 1) ^ (2 * k) ≤ ((HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ k) ^ (2 * k)
Tactic: calc
    ((2 * k ^ 2 : ℕ) + 1 : ℝ) ≤ 2 ^ (2 * k) := mod_cast Nat.two_mul_sq_add_one_le_two_pow_two_mul _
    _ = (1 / k * k + 1 : ℝ) ^ (2 * k) := by simp [posk.ne']; norm_num
    _ ≤ ((1 / k + 1) ^ k : ℝ) ^ (2 * k) := by gcongr; exact mul_add_one_le_add_one_pow (by simp) _
    _ = (1 / k + 1 : ℝ) ^ (2 * k ^ 2) := by rw [← pow_mul, mul_left_comm, sq]
    _ < a ^ (2 * k ^ 2) := by gcongr
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1 < a
k₁ : HPow.hPow (α := ℝ) 2 (2 * k) = (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) * (↑k : ℝ) + 1) ^ (2 * k)
k₂ : (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) * (↑k : ℝ) + 1) ^ (2 * k) ≤ ((HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ k) ^ (2 * k)
⊢ HAdd.hAdd (α := ℝ) (↑(2 * HPow.hPow (β := ℕ) k 2) : ℝ) 1 < a ^ (2 * HPow.hPow (β := ℕ) k 2)
have k₃ : ((HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ k) ^ (2 * k) = (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ (2 * HPow.hPow (β := ℕ) k 2)
Tactic: calc
    ((2 * k ^ 2 : ℕ) + 1 : ℝ) ≤ 2 ^ (2 * k) := mod_cast Nat.two_mul_sq_add_one_le_two_pow_two_mul _
    _ = (1 / k * k + 1 : ℝ) ^ (2 * k) := by simp [posk.ne']; norm_num
    _ ≤ ((1 / k + 1) ^ k : ℝ) ^ (2 * k) := by gcongr; exact mul_add_one_le_add_one_pow (by simp) _
    _ = (1 / k + 1 : ℝ) ^ (2 * k ^ 2) := by rw [← pow_mul, mul_left_comm, sq]
    _ < a ^ (2 * k ^ 2) := by gcongr
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1 < a
k₁ : HPow.hPow (α := ℝ) 2 (2 * k) = (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) * (↑k : ℝ) + 1) ^ (2 * k)
k₂ : (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) * (↑k : ℝ) + 1) ^ (2 * k) ≤ ((HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ k) ^ (2 * k)
k₃ :
  ((HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ k) ^ (2 * k) =
    (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ (2 * HPow.hPow (β := ℕ) k 2)
⊢ HAdd.hAdd (α := ℝ) (↑(2 * HPow.hPow (β := ℕ) k 2) : ℝ) 1 < a ^ (2 * HPow.hPow (β := ℕ) k 2)
have k₄ : (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1) ^ (2 * HPow.hPow (β := ℕ) k 2) < a ^ (2 * HPow.hPow (β := ℕ) k 2)
Tactic: calc
    ((2 * k ^ 2 : ℕ) + 1 : ℝ) ≤ 2 ^ (2 * k) := mod_cast Nat.two_mul_sq_add_one_le_two_pow_two_mul _
    _ = (1 / k * k + 1 : ℝ) ^ (2 * k) := by simp [posk.ne']; norm_num
    _ ≤ ((1 / k + 1) ^ k : ℝ) ^ (2 * k) := by gcongr; exact mul_add_one_le_add_one_pow (by simp) _
    _ = (1 / k + 1 : ℝ) ^ (2 * k ^ 2) := by rw [← pow_mul, mul_left_comm, sq]
    _ < a ^ (2 * k ^ 2) := by gcongr
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
b : ℝ
hb : 0 < b
⊢ ∃ (n : ℕ), 0 < n ∧ (↑n : ℝ)⁻¹ < b
have refine : ∀ (k : ℕ) (hk : b⁻¹ < (↑k : ℝ)), 0 < k ∧ (↑k : ℝ)⁻¹ < b
Tactic: refine (exists_nat_gt b⁻¹).imp fun k hk ↦ ?_
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (hypothesis)
Goal:
b : ℝ
hb : 0 < b
k : ℕ
hk : b⁻¹ < (↑k : ℝ)
⊢ 0 < k ∧ (↑k : ℝ)⁻¹ < b
have this : LT.lt (α := ℝ) 0 (↑k : ℝ)
Tactic: have := (inv_pos_of_pos hb).trans hk
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
b : ℝ
hb : 0 < b
k : ℕ
hk : b⁻¹ < (↑k : ℝ)
this : LT.lt (α := ℝ) 0 (↑k : ℝ)
⊢ 0 < k ∧ (↑k : ℝ)⁻¹ < b
have refine : (↑k : ℝ)⁻¹ < b
Tactic: refine ⟨Nat.cast_pos.mp this, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
a b : Cauchy (α := ℚ) abs
⊢ { cauchy := a : ℝ } = { cauchy := b } ↔ { cauchy := a : ℝ }.cauchy = { cauchy := b }.cauchy
have rw : a = b ↔ { cauchy := a : ℝ }.cauchy = { cauchy := b }.cauchy
Tactic: rw [ofCauchy.injEq]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
a b : Cauchy (α := ℚ) abs
⊢ { cauchy := a - b : ℝ } = { cauchy := a : ℝ } - { cauchy := b : ℝ }
have rw : { cauchy := a : ℝ } + -{ cauchy := b : ℝ } = { cauchy := a : ℝ } - { cauchy := b : ℝ }
Tactic: rw [sub_eq_add_neg, ofCauchy_add, ofCauchy_neg]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
f : Cauchy (α := ℚ) abs
⊢ { cauchy := f⁻¹ : ℝ } = { cauchy := f }.inv'
have rw : { cauchy := f⁻¹ : ℝ } =
  match (motive := ℝ → ℝ) { cauchy := f } with
  | { cauchy := a } => { cauchy := a⁻¹ }
Tactic: rw [inv']
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
⊢ zero.cauchy = 0
have rw : { cauchy := 0 : ℝ }.cauchy = 0
Tactic: rw [zero_def]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
⊢ one.cauchy = 1
have rw : { cauchy := 1 : ℝ }.cauchy = 1
Tactic: rw [one_def]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
a b : Cauchy (α := ℚ) abs
⊢ ({ cauchy := a : ℝ }.add { cauchy := b : ℝ }).cauchy = { cauchy := a : ℝ }.cauchy + { cauchy := b : ℝ }.cauchy
have rw : cauchy
    (match (motive := ℝ → ℝ → ℝ) { cauchy := a : ℝ }, { cauchy := b : ℝ } with
    | { cauchy := a }, { cauchy := b } => { cauchy := a + b : ℝ }) =
  { cauchy := a : ℝ }.cauchy + { cauchy := b : ℝ }.cauchy
Tactic: rw [add_def]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
a : Cauchy (α := ℚ) abs
⊢ { cauchy := a : ℝ }.neg.cauchy = -{ cauchy := a }.cauchy
have rw : cauchy
    (match (motive := ℝ → ℝ) { cauchy := a : ℝ } with
    | { cauchy := a } => { cauchy := -a : ℝ }) =
  -{ cauchy := a }.cauchy
Tactic: rw [neg_def]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
a b : Cauchy (α := ℚ) abs
⊢ ({ cauchy := a : ℝ }.mul { cauchy := b : ℝ }).cauchy = { cauchy := a : ℝ }.cauchy * { cauchy := b : ℝ }.cauchy
have rw : cauchy
    (match (motive := ℝ → ℝ → ℝ) { cauchy := a : ℝ }, { cauchy := b : ℝ } with
    | { cauchy := a }, { cauchy := b } => { cauchy := a * b : ℝ }) =
  { cauchy := a : ℝ }.cauchy * { cauchy := b : ℝ }.cauchy
Tactic: rw [mul_def]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
a b : Cauchy (α := ℚ) abs
⊢ ({ cauchy := a : ℝ } - { cauchy := b : ℝ }).cauchy = { cauchy := a : ℝ }.cauchy - { cauchy := b : ℝ }.cauchy
have rw : ({ cauchy := a : ℝ } - { cauchy := b : ℝ }).cauchy = ({ cauchy := a : ℝ } + -{ cauchy := b : ℝ }).cauchy
Tactic: rw [sub_eq_add_neg, ← cauchy_neg, ← cauchy_add]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
f : Cauchy (α := ℚ) abs
⊢ { cauchy := f : ℝ }.inv'.cauchy = { cauchy := f }.cauchy⁻¹
have rw : cauchy
    (match (motive := ℝ → ℝ) { cauchy := f : ℝ } with
    | { cauchy := a } => { cauchy := a⁻¹ : ℝ }) =
  { cauchy := f }.cauchy⁻¹
Tactic: rw [inv']