awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Real.Archimedean
Goal:
hs : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) ∅ x → x ≤ 0
⊢ LE.le (α := ℝ) (sInf ∅) 0

Tactic:
exact sInf_empty.le

Premises used: Eq.le, Real.sInf_empty
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
hs : ∀ x ∈ s, x ≤ 0
x : ℝ
hx : x ∈ s
⊢ sInf s ≤ 0

Tactic:
sInf_nonpos' ⟨x, hx, hs _ hx⟩

Premises used: And.intro, Exists.intro, Real.sInf_nonpos'
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
hs : ∀ x ∈ s, x ≤ 0
x : ℝ
hx : x ∈ s
⊢ sInf s ≤ 0

Tactic:
exact sInf_nonpos' ⟨x, hx, hs _ hx⟩

Premises used: And.intro, Exists.intro, Real.sInf_nonpos'
-- Module: Mathlib.Data.Real.Archimedean
Goal:
ι : Sort u_1
f : ι → ℝ
hf : ∀ (i : ι), f i ≤ 0
⊢ LE.le (α := ℝ) (⨅ (i : ι), f i) 0

Tactic:
sInf_nonpos <| Set.forall_mem_range.2 hf

Premises used: Iff.mpr, iInf, Set.forall_mem_range, Real.sInf_nonpos
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
h₁ : BddBelow s
h₂ : BddAbove s
inl : ∀ (h₁ : BddBelow (α := ℝ) ∅) (h₂ : BddAbove (α := ℝ) ∅), LE.le (α := ℝ) (sInf ∅) (sSup ∅)
inr : ∀ (hne : s.Nonempty), sInf s ≤ sSup s
⊢ sInf s ≤ sSup s

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | hne)

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Data.Real.Archimedean
Goal:
h₁ : BddBelow (α := ℝ) ∅
h₂ : BddAbove (α := ℝ) ∅
inl : LE.le (α := ℝ) 0 (sSup ∅)
inl₁ inl₂ : LE.le (α := ℝ) 0 0
⊢ LE.le (α := ℝ) (sInf ∅) (sSup ∅)

Tactic:
rw [sInf_empty, sSup_empty]

Premises used: Real.sSup_empty, Real.sInf_empty
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
h₁ : BddBelow s
h₂ : BddAbove s
hne : s.Nonempty
⊢ sInf s ≤ sSup s

Tactic:
csInf_le_csSup hne h₁ h₂

Premises used: csInf_le_csSup
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
h₁ : BddBelow s
h₂ : BddAbove s
hne : s.Nonempty
⊢ sInf s ≤ sSup s

Tactic:
exact csInf_le_csSup hne h₁ h₂

Premises used: csInf_le_csSup
-- Module: Mathlib.Data.Real.Archimedean
Goal:
f : CauSeq ℝ abs
s : Set ℝ := {x : ℝ | const abs x < f}
⊢ ∃ (x : ℝ), x ∈ s

Tactic:
have lb : ∃ x, x ∈ s := exists_lt f
-- Module: Mathlib.Data.Real.Archimedean
Goal:
f : CauSeq ℝ abs
s : Set ℝ := {x : ℝ | const abs x < f}
lb : ∃ (x : ℝ), x ∈ s
⊢ ∀ (x : ℝ), f < const abs x → ∀ y ∈ s, y ≤ x

Tactic:
have ub' : ∀ x, f < const abs x → ∀ y ∈ s, y ≤ x := fun x h y yS =>
    le_of_lt <| const_lt.1 <| CauSeq.lt_trans yS h
-- Module: Mathlib.Data.Real.Archimedean
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
⊢ ∃ (x : ℝ), ∀ y ∈ s, y ≤ x

Tactic:
have ub : ∃ x, ∀ y ∈ s, y ≤ x := (exists_gt f).imp ub'
-- Module: Mathlib.Data.Real.Archimedean
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
⊢ ∃ (x : ℝ), f ≈ const abs x

Tactic:
⟨sSup s, ((lt_total _ _).resolve_left fun h => ?_).resolve_right fun h => ?_⟩

Premises used: Or.resolve_left, Exists.intro, Or.resolve_right, CauSeq.lt_total, SupSet.sSup
-- Module: Mathlib.Data.Real.Archimedean
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
refine_1 : ∀ (h : f < const abs (sSup s)), False
refine_2 : ∀ (h : const abs (sSup s) < f), False
⊢ ∃ (x : ℝ), f ≈ const abs x

Tactic:
refine ⟨sSup s, ((lt_total _ _).resolve_left fun h => ?_).resolve_right fun h => ?_⟩
-- Module: Mathlib.Data.Real.Archimedean
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
h : f < const abs (sSup s)
refine_1 : ∀ (ε : ℝ) (ε0 : ε > 0) (i : ℕ) (ih : ∀ j ≥ i, ε ≤ (↑(const abs (sSup s) - f) : ℕ → ℝ) j), False
⊢ False

Tactic:
rcases h with ⟨ε, ε0, i, ih⟩
-- Module: Mathlib.Data.Real.Archimedean
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, ε ≤ (↑(const abs (sSup s) - f) : ℕ → ℝ) j
⊢ False

Tactic:
(csSup_le lb (ub' _ ?_)).not_gt (sub_lt_self _ (half_pos ε0))

Premises used: half_pos, sub_lt_self, LE.le.not_gt, csSup_le
-- Module: Mathlib.Data.Real.Archimedean
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, ε ≤ (↑(const abs (sSup s) - f) : ℕ → ℝ) j
refine_1 : f < const abs (sSup s - ε / 2)
⊢ False

Tactic:
refine (csSup_le lb (ub' _ ?_)).not_gt (sub_lt_self _ (half_pos ε0))

Premises used: half_pos, sub_lt_self, LE.le.not_gt, csSup_le
-- Module: Mathlib.Data.Real.Archimedean
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, ε ≤ (↑(const abs (sSup s) - f) : ℕ → ℝ) j
⊢ f < const abs (sSup s - ε / 2)

Tactic:
⟨_, half_pos ε0, i, fun j ij => ?_⟩

Premises used: CauSeq.Pos, half_pos, And.intro, Exists.intro
-- Module: Mathlib.Data.Real.Archimedean
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, ε ≤ (↑(const abs (sSup s) - f) : ℕ → ℝ) j
refine_1 : ∀ (j : ℕ) (ij : j ≥ i), ε / 2 ≤ (↑(const abs (sSup s - ε / 2) - f) : ℕ → ℝ) j
⊢ f < const abs (sSup s - ε / 2)

Tactic:
refine ⟨_, half_pos ε0, i, fun j ij => ?_⟩
-- Module: Mathlib.Data.Real.Archimedean
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, ε ≤ (↑(const abs (sSup s) - f) : ℕ → ℝ) j
j : ℕ
ij : j ≥ i
refine_1 : ε ≤ sSup s - (↑f : ℕ → ℝ) j
⊢ ε / 2 ≤ (↑(const abs (sSup s - ε / 2) - f) : ℕ → ℝ) j

Tactic:
rw [sub_apply, const_apply, sub_right_comm, le_sub_iff_add_le, add_halves]

Premises used: add_halves, CauSeq.sub_apply, CauSeq.const_apply, sub_right_comm, le_sub_iff_add_le
-- Module: Mathlib.Data.Real.Archimedean
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, ε ≤ (↑(const abs (sSup s) - f) : ℕ → ℝ) j
j : ℕ
ij : j ≥ i
⊢ ε ≤ sSup s - (↑f : ℕ → ℝ) j

Tactic:
ih _ ij
-- Module: Mathlib.Data.Real.Archimedean
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, ε ≤ (↑(const abs (sSup s) - f) : ℕ → ℝ) j
j : ℕ
ij : j ≥ i
⊢ ε ≤ sSup s - (↑f : ℕ → ℝ) j

Tactic:
exact ih _ ij
-- Module: Mathlib.Data.Real.Archimedean
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
h : const abs (sSup s) < f
refine_2 : ∀ (ε : ℝ) (ε0 : ε > 0) (i : ℕ) (ih : ∀ j ≥ i, ε ≤ (↑(f - const abs (sSup s)) : ℕ → ℝ) j), False
⊢ False

Tactic:
rcases h with ⟨ε, ε0, i, ih⟩
-- Module: Mathlib.Data.Real.Archimedean
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

Tactic:
(le_csSup ub ?_).not_gt ((lt_add_iff_pos_left _).2 (half_pos ε0))

Premises used: Iff.mpr, half_pos, LE.le.not_gt, le_csSup, lt_add_iff_pos_left
-- Module: Mathlib.Data.Real.Archimedean
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
refine_2 : ε / 2 + sSup s ∈ s
⊢ False

Tactic:
refine (le_csSup ub ?_).not_gt ((lt_add_iff_pos_left _).2 (half_pos ε0))

Premises used: Iff.mpr, half_pos, LE.le.not_gt, le_csSup, lt_add_iff_pos_left
-- Module: Mathlib.Data.Real.Archimedean
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

Tactic:
⟨_, half_pos ε0, i, fun j ij => ?_⟩

Premises used: CauSeq.Pos, half_pos, Set.Mem, setOf, And.intro, Exists.intro
-- Module: Mathlib.Data.Real.Archimedean
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
refine_2 : ∀ (j : ℕ) (ij : j ≥ i), ε / 2 ≤ (↑(f - const abs (ε / 2 + sSup s)) : ℕ → ℝ) j
⊢ ε / 2 + sSup s ∈ s

Tactic:
refine ⟨_, half_pos ε0, i, fun j ij => ?_⟩
-- Module: Mathlib.Data.Real.Archimedean
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
refine_2 : ε ≤ (↑f : ℕ → ℝ) j - sSup s
⊢ ε / 2 ≤ (↑(f - const abs (ε / 2 + sSup s)) : ℕ → ℝ) j

Tactic:
rw [sub_apply, const_apply, add_comm, ← sub_sub, le_sub_iff_add_le, add_halves]

Premises used: add_halves, CauSeq.sub_apply, CauSeq.const_apply, add_comm, sub_sub, le_sub_iff_add_le
-- Module: Mathlib.Data.Real.Archimedean
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
⊢ ε ≤ (↑f : ℕ → ℝ) j - sSup s

Tactic:
ih _ ij
-- Module: Mathlib.Data.Real.Archimedean
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
⊢ ε ≤ (↑f : ℕ → ℝ) j - sSup s

Tactic:
exact ih _ ij
-- Module: Mathlib.Data.Real.Archimedean
Goal:
ι : Sort u_1
f : ι → ℝ
s : Set ℝ
a : ℝ
⊢ IsComplete ℝ abs

Tactic:
⟨cauSeq_converges⟩

Premises used: Real.cauSeq_converges, CauSeq.IsComplete.mk
-- Module: Mathlib.Data.Real.Archimedean
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 : ℚ) : ℝ))

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Data.Real.Archimedean
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 : ℚ) : ℝ))
refine_2 :
  LE.le (α := ℝ) (⨅ (q : { q' : ℚ // x < (↑q' : ℝ) }), f (↑(↑q : ℚ) : ℝ)) (⨅ (r : (↑(Ioi x) : Type)), f (↑r : ℝ))
⊢ Eq (α := ℝ) (⨅ (r : (↑(Ioi x) : Type)), f (↑r : ℝ)) (⨅ (q : { q' : ℚ // x < (↑q' : ℝ) }), f (↑(↑q : ℚ) : ℝ))

Tactic:
refine le_antisymm ?_ ?_
-- Module: Mathlib.Data.Real.Archimedean
Goal:
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
obtain : ∀ (r : ℚ) (hrx : x < (↑r : ℝ)), Nonempty { r' : ℚ // x < (↑r' : ℝ) }
⊢ Nonempty { r' : ℚ // x < (↑r' : ℝ) }

Tactic:
obtain ⟨r, hrx⟩ := exists_rat_gt x

Premises used: exists_rat_gt
-- Module: Mathlib.Data.Real.Archimedean
Goal:
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
r : ℚ
hrx : x < (↑r : ℝ)
⊢ Nonempty { r' : ℚ // x < (↑r' : ℝ) }

Tactic:
⟨⟨r, hrx⟩⟩

Premises used: Nonempty.intro, Subtype.mk
-- Module: Mathlib.Data.Real.Archimedean
Goal:
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
r : ℚ
hrx : x < (↑r : ℝ)
⊢ Nonempty { r' : ℚ // x < (↑r' : ℝ) }

Tactic:
exact ⟨⟨r, hrx⟩⟩
-- Module: Mathlib.Data.Real.Archimedean
Goal:
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
⊢ Nonempty { r' : ℚ // x < (↑r' : ℝ) }

Tactic:
have : Nonempty { r' : ℚ // x < ↑r' } := by
      obtain ⟨r, hrx⟩ := exists_rat_gt x
      exact ⟨⟨r, hrx⟩⟩
-- Module: Mathlib.Data.Real.Archimedean
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 : ℚ) : ℝ))

Tactic:
le_ciInf fun r => ?_

Premises used: le_ciInf
-- Module: Mathlib.Data.Real.Archimedean
Goal:
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
this : Nonempty { r' : ℚ // x < (↑r' : ℝ) }
refine_1 : ∀ (r : { q' : ℚ // x < (↑q' : ℝ) }), ⨅ (r : (↑(Ioi x) : Type)), f (↑r : ℝ) ≤ f (↑(↑r : ℚ) : ℝ)
⊢ LE.le (α := ℝ) (⨅ (r : (↑(Ioi x) : Type)), f (↑r : ℝ)) (⨅ (q : { q' : ℚ // x < (↑q' : ℝ) }), f (↑(↑q : ℚ) : ℝ))

Tactic:
refine le_ciInf fun r => ?_

Premises used: le_ciInf
-- Module: Mathlib.Data.Real.Archimedean
Goal:
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
this : Nonempty { r' : ℚ // x < (↑r' : ℝ) }
r : { q' : ℚ // x < (↑q' : ℝ) }
refine_1 :
  ∀ (y : ℚ) (hxy : x < (↑y : ℝ)) (hyr : LT.lt (α := ℝ) (↑y : ℝ) (↑(↑r : ℚ) : ℝ)),
    ⨅ (r : (↑(Ioi x) : Type)), f (↑r : ℝ) ≤ f (↑(↑r : ℚ) : ℝ)
⊢ ⨅ (r : (↑(Ioi x) : Type)), f (↑r : ℝ) ≤ f (↑(↑r : ℚ) : ℝ)

Tactic:
obtain ⟨y, hxy, hyr⟩ := exists_rat_btwn r.prop

Premises used: exists_rat_btwn, Subtype.prop
-- Module: Mathlib.Data.Real.Archimedean
Goal:
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
this : Nonempty { r' : ℚ // x < (↑r' : ℝ) }
r : { q' : ℚ // x < (↑q' : ℝ) }
y : ℚ
hxy : x < (↑y : ℝ)
hyr : LT.lt (α := ℝ) (↑y : ℝ) (↑(↑r : ℚ) : ℝ)
⊢ ⨅ (r : (↑(Ioi x) : Type)), f (↑r : ℝ) ≤ f (↑(↑r : ℚ) : ℝ)

Tactic:
ciInf_set_le hf (hxy.trans ?_)

Premises used: LT.lt.trans, ciInf_set_le
-- Module: Mathlib.Data.Real.Archimedean
Goal:
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
this : Nonempty { r' : ℚ // x < (↑r' : ℝ) }
r : { q' : ℚ // x < (↑q' : ℝ) }
y : ℚ
hxy : x < (↑y : ℝ)
hyr : LT.lt (α := ℝ) (↑y : ℝ) (↑(↑r : ℚ) : ℝ)
refine_1 : LT.lt (α := ℝ) (↑y : ℝ) (↑(↑r : ℚ) : ℝ)
⊢ ⨅ (r : (↑(Ioi x) : Type)), f (↑r : ℝ) ≤ f (↑(↑r : ℚ) : ℝ)

Tactic:
refine ciInf_set_le hf (hxy.trans ?_)

Premises used: LT.lt.trans, ciInf_set_le
-- Module: Mathlib.Data.Real.Archimedean
Goal:
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
this : Nonempty { r' : ℚ // x < (↑r' : ℝ) }
r : { q' : ℚ // x < (↑q' : ℝ) }
y : ℚ
hxy : x < (↑y : ℝ)
hyr : LT.lt (α := ℝ) (↑y : ℝ) (↑(↑r : ℚ) : ℝ)
⊢ LT.lt (α := ℝ) (↑y : ℝ) (↑(↑r : ℚ) : ℝ)

Tactic:
exact_mod_cast hyr
-- Module: Mathlib.Data.Real.Archimedean
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 : ℝ))

Tactic:
le_ciInf fun q => ?_

Premises used: le_ciInf
-- Module: Mathlib.Data.Real.Archimedean
Goal:
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
refine_2 : ∀ (q : (↑(Ioi x) : Type)), ⨅ (q : { q' : ℚ // x < (↑q' : ℝ) }), f (↑(↑q : ℚ) : ℝ) ≤ f (↑q : ℝ)
⊢ LE.le (α := ℝ) (⨅ (q : { q' : ℚ // x < (↑q' : ℝ) }), f (↑(↑q : ℚ) : ℝ)) (⨅ (r : (↑(Ioi x) : Type)), f (↑r : ℝ))

Tactic:
refine le_ciInf fun q => ?_

Premises used: le_ciInf
-- Module: Mathlib.Data.Real.Archimedean
Goal:
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : (↑(Ioi x) : Type)
⊢ (↑q : ℝ) ∈ Ioi x

Tactic:
have hq := q.prop
-- Module: Mathlib.Data.Real.Archimedean
Goal:
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : (↑(Ioi x) : Type)
hq : (↑q : ℝ) ∈ Ioi x
⊢ x < (↑q : ℝ)

Tactic:
rw [mem_Ioi] at hq

Premises used: Set.mem_Ioi
-- Module: Mathlib.Data.Real.Archimedean
Goal:
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : (↑(Ioi x) : Type)
hq : x < (↑q : ℝ)
refine_2 :
  ∀ (y : ℚ) (hxy : x < (↑y : ℝ)) (hyq : (↑y : ℝ) < (↑q : ℝ)),
    ⨅ (q : { q' : ℚ // x < (↑q' : ℝ) }), f (↑(↑q : ℚ) : ℝ) ≤ f (↑q : ℝ)
⊢ ⨅ (q : { q' : ℚ // x < (↑q' : ℝ) }), f (↑(↑q : ℚ) : ℝ) ≤ f (↑q : ℝ)

Tactic:
obtain ⟨y, hxy, hyq⟩ := exists_rat_btwn hq

Premises used: exists_rat_btwn
-- Module: Mathlib.Data.Real.Archimedean
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 : ℝ)

Tactic:
(ciInf_le ?_ ?_).trans ?_

Premises used: ciInf_le, LE.le.trans
-- Module: Mathlib.Data.Real.Archimedean
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' : ℝ) }
refine_2₂ : f (↑(↑(Subtype.mk (p := fun (q' : ℚ) ↦ x < (↑q' : ℝ)) y hxy) : ℚ) : ℝ) ≤ f (↑q : ℝ)
⊢ ⨅ (q : { q' : ℚ // x < (↑q' : ℝ) }), f (↑(↑q : ℚ) : ℝ) ≤ f (↑q : ℝ)

Tactic:
refine (ciInf_le ?_ ?_).trans ?_

Premises used: ciInf_le, LE.le.trans
-- Module: Mathlib.Data.Real.Archimedean
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 : ℚ) : ℝ))

Tactic:
⟨hf.some, fun z => ?_⟩

Premises used: Set.Nonempty, BddBelow, Exists.intro, Set.Nonempty.some
-- Module: Mathlib.Data.Real.Archimedean
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 :
  ∀ (z : ℝ),
    Membership.mem (γ := Set ℝ) (range fun (q : { q' : ℚ // x < (↑q' : ℝ) }) ↦ f (↑(↑q : ℚ) : ℝ)) z →
      Set.Nonempty.some (s := lowerBounds (f '' Ioi x)) hf ≤ z
⊢ BddBelow (α := ℝ) (range fun (q : { q' : ℚ // x < (↑q' : ℝ) }) ↦ f (↑(↑q : ℚ) : ℝ))

Tactic:
refine ⟨hf.some, fun z => ?_⟩
-- Module: Mathlib.Data.Real.Archimedean
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' : ℝ) }
refine_2 : f (↑(↑u : ℚ) : ℝ) ∈ f '' Ioi x
⊢ Set.Nonempty.some (s := lowerBounds (f '' Ioi x)) hf ≤ (fun (q : { q' : ℚ // x < (↑q' : ℝ) }) ↦ f (↑(↑q : ℚ) : ℝ)) u

Tactic:
suffices hfu : f u ∈ f '' Ioi x from hf.choose_spec hfu
-- Module: Mathlib.Data.Real.Archimedean
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' : ℝ) }
⊢ f (↑(↑u : ℚ) : ℝ) ∈ f '' Ioi x

Tactic:
⟨u, u.prop, rfl⟩

Premises used: Set.Mem, setOf, Rat.cast, Subtype.prop, And.intro, Exists.intro, Set.image, Subtype.val, rfl
-- Module: Mathlib.Data.Real.Archimedean
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' : ℝ) }
⊢ f (↑(↑u : ℚ) : ℝ) ∈ f '' Ioi x

Tactic:
exact ⟨u, u.prop, rfl⟩
-- Module: Mathlib.Data.Real.Archimedean
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' : ℚ // x < (↑q' : ℝ) }

Tactic:
exact ⟨y, hxy⟩
-- Module: Mathlib.Data.Real.Archimedean
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 : ℝ)

Tactic:
hf_mono (le_trans ?_ hyq.le)

Premises used: LT.lt.le, le_trans
-- Module: Mathlib.Data.Real.Archimedean
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 : LE.le (α := ℝ) (↑(↑(Subtype.mk (p := fun (q' : ℚ) ↦ x < (↑q' : ℝ)) y hxy) : ℚ) : ℝ) (↑y : ℝ)
⊢ f (↑(↑(Subtype.mk (p := fun (q' : ℚ) ↦ x < (↑q' : ℝ)) y hxy) : ℚ) : ℝ) ≤ f (↑q : ℝ)

Tactic:
refine hf_mono (le_trans ?_ hyq.le)

Premises used: LT.lt.le, le_trans
-- Module: Mathlib.Data.Real.Archimedean
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 refine_2₁ refine_2₂ refine_2₃ :
  (↑(Subtype.mk (p := fun (q' : ℚ) ↦ x < (↑q' : ℝ)) y hxy) : ℚ) ≤
    (↑(Subtype.mk (p := fun (q' : ℚ) ↦ x < (↑q' : ℝ)) y hxy) : ℚ)
⊢ LE.le (α := ℝ) (↑(↑(Subtype.mk (p := fun (q' : ℚ) ↦ x < (↑q' : ℝ)) y hxy) : ℚ) : ℝ) (↑y : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.Data.Real.Archimedean
Goal:
rw : Eq (α := Set ℝ) {x : ℝ | ∀ ⦃a : ℝ⦄, Membership.mem (γ := Set ℝ) (range fun (x : ℚ) ↦ (↑x : ℝ)) a → a ≤ x} ∅
⊢ ¬Set.Nonempty (α := ℝ) {x : ℝ | ∀ ⦃a : ℝ⦄, Membership.mem (γ := Set ℝ) (range fun (x : ℚ) ↦ (↑x : ℝ)) a → a ≤ x}

Tactic:
rw [Set.not_nonempty_iff_eq_empty]

Premises used: Set.not_nonempty_iff_eq_empty
-- Module: Mathlib.Data.Real.Archimedean
Goal:
h :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ)
        {x : ℝ | ∀ ⦃a : ℝ⦄, Membership.mem (γ := Set ℝ) (range fun (x : ℚ) ↦ (↑x : ℝ)) a → a ≤ x} x ↔
      Membership.mem (γ := Set ℝ) ∅ x
⊢ Eq (α := Set ℝ) {x : ℝ | ∀ ⦃a : ℝ⦄, Membership.mem (γ := Set ℝ) (range fun (x : ℚ) ↦ (↑x : ℝ)) a → a ≤ x} ∅

Tactic:
ext
-- Module: Mathlib.Data.Real.Archimedean
Goal:
x : ℝ
⊢ Membership.mem (γ := Set ℝ) {x : ℝ | ∀ ⦃a : ℝ⦄, Membership.mem (γ := Set ℝ) (range fun (x : ℚ) ↦ (↑x : ℝ)) a → a ≤ x}
      x ↔
    Membership.mem (γ := Set ℝ) ∅ x

Tactic:
simpa using exists_rat_gt _

Premises used: exists_rat_gt
-- Module: Mathlib.Data.Real.Archimedean
Goal:
rw : Eq (α := Set ℝ) {x : ℝ | ∀ ⦃a : ℝ⦄, Membership.mem (γ := Set ℝ) (range fun (x : ℚ) ↦ (↑x : ℝ)) a → x ≤ a} ∅
⊢ ¬Set.Nonempty (α := ℝ) {x : ℝ | ∀ ⦃a : ℝ⦄, Membership.mem (γ := Set ℝ) (range fun (x : ℚ) ↦ (↑x : ℝ)) a → x ≤ a}

Tactic:
rw [Set.not_nonempty_iff_eq_empty]

Premises used: Set.not_nonempty_iff_eq_empty
-- Module: Mathlib.Data.Real.Archimedean
Goal:
h :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ)
        {x : ℝ | ∀ ⦃a : ℝ⦄, Membership.mem (γ := Set ℝ) (range fun (x : ℚ) ↦ (↑x : ℝ)) a → x ≤ a} x ↔
      Membership.mem (γ := Set ℝ) ∅ x
⊢ Eq (α := Set ℝ) {x : ℝ | ∀ ⦃a : ℝ⦄, Membership.mem (γ := Set ℝ) (range fun (x : ℚ) ↦ (↑x : ℝ)) a → x ≤ a} ∅

Tactic:
ext
-- Module: Mathlib.Data.Real.Archimedean
Goal:
x : ℝ
⊢ Membership.mem (γ := Set ℝ) {x : ℝ | ∀ ⦃a : ℝ⦄, Membership.mem (γ := Set ℝ) (range fun (x : ℚ) ↦ (↑x : ℝ)) a → x ≤ a}
      x ↔
    Membership.mem (γ := Set ℝ) ∅ x

Tactic:
simpa using exists_rat_lt _

Premises used: exists_rat_lt
-- Module: Mathlib.Data.Real.Archimedean
Goal:
⊢ Eq (α := Set ℝ) (⋃ (r : ℚ), Iic (↑r : ℝ)) univ

Tactic:
iUnion_Iic_of_not_bddAbove_range not_bddAbove_coe

Premises used: Real.not_bddAbove_coe, iUnion_Iic_of_not_bddAbove_range
-- Module: Mathlib.Data.Real.Archimedean
Goal:
⊢ Eq (α := Set ℝ) (⋃ (r : ℚ), Iic (↑r : ℝ)) univ

Tactic:
exact iUnion_Iic_of_not_bddAbove_range not_bddAbove_coe

Premises used: Real.not_bddAbove_coe, iUnion_Iic_of_not_bddAbove_range
-- Module: Mathlib.Data.Real.Archimedean
Goal:
⊢ Eq (α := Set ℝ) (⋂ (r : ℚ), Iic (↑r : ℝ)) ∅

Tactic:
iInter_Iic_eq_empty_iff.mpr not_bddBelow_coe

Premises used: Iff.mpr, Real.not_bddBelow_coe, iInter_Iic_eq_empty_iff
-- Module: Mathlib.Data.Real.Archimedean
Goal:
⊢ Eq (α := Set ℝ) (⋂ (r : ℚ), Iic (↑r : ℝ)) ∅

Tactic:
exact iInter_Iic_eq_empty_iff.mpr not_bddBelow_coe

Premises used: Iff.mpr, Real.not_bddBelow_coe, iInter_Iic_eq_empty_iff
-- Module: Mathlib.Data.Real.Archimedean
Goal:
a : ℝ
ha : 1 < a
contrapose! : ∀ (ha : ∀ (k : ℕ) (_ : 0 < k), a ≤ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1), a ≤ 1
⊢ ∃ (k : ℕ), 0 < k ∧ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1 < a

Tactic:
contrapose! ha
-- Module: Mathlib.Data.Real.Archimedean
Goal:
a : ℝ
ha : ∀ (k : ℕ) (_ : 0 < k), a ≤ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ) + 1
⊢ a ≤ 1

Tactic:
le_of_forall_lt_rat_imp_le ?_

Premises used: le_of_forall_lt_rat_imp_le