-- Mathlib/Data/Real/Archimedean.lean
theorem iInf_Ioi_eq_iInf_rat_gt {f : ℝ → ℝ} (x : ℝ) (hf : BddBelow (f '' Ioi x))
    (hf_mono : Monotone f) : ⨅ r : Ioi x, f r = ⨅ q : { q' : ℚ // x < q' }, f q

Proof state:
case refine_2.intro.intro.refine_2
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
y : ℚ
hxy : x < ↑y
hyq : ↑y < ↑q
⊢ { q' // x < ↑q' }

Tactic:
exact ⟨y, hxy⟩

Result:
no goals

Proof state:
case intro
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
r : ℚ
hrx : x < ↑r
⊢ Nonempty { r' // x < ↑r' }

Tactic:
exact ⟨⟨r, hrx⟩⟩

Result:
no goals

Proof state:
case refine_2
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
⊢ ⨅ q, f ↑↑q ≤ f ↑q

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

Result:
case refine_2.intro.intro
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
y : ℚ
hxy : x < ↑y
hyq : ↑y < ↑q
⊢ ⨅ q, f ↑↑q ≤ f ↑q

Proof state:
case refine_1.intro.intro
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 : ↑y < ↑↑r
⊢ ⨅ r, f ↑r ≤ f ↑↑r

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

Result:
case refine_1.intro.intro
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 : ↑y < ↑↑r
⊢ ↑y < ↑↑r

Proof state:
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
⊢ Nonempty { r' // x < ↑r' }

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

Result:
case intro
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
r : ℚ
hrx : x < ↑r
⊢ Nonempty { r' // x < ↑r' }

Proof state:
case refine_2.intro.intro.refine_1.intro
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
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⟩

Result:
no goals

Proof state:
case refine_2.intro.intro.refine_1
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
y : ℚ
hxy : x < ↑y
hyq : ↑y < ↑q
⊢ BddBelow (range fun q => f ↑↑q)

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

Result:
case refine_2.intro.intro.refine_1
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
y : ℚ
hxy : x < ↑y
hyq : ↑y < ↑q
z : ℝ
⊢ (z ∈ range fun q => f ↑↑q) → Set.Nonempty.some hf ≤ z

Proof state:
case refine_2
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : ↑q ∈ Ioi x
⊢ ⨅ q, f ↑↑q ≤ f ↑q

Tactic:
rw [mem_Ioi] at hq

Result:
case refine_2
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
⊢ ⨅ q, f ↑↑q ≤ f ↑q

Proof state:
case refine_1
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
this : Nonempty { r' // x < ↑r' }
⊢ ⨅ r, f ↑r ≤ ⨅ q, f ↑↑q

Tactic:
refine le_ciInf fun r => ?_

Result:
case refine_1
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
this : Nonempty { r' // x < ↑r' }
r : { q' // x < ↑q' }
⊢ ⨅ r, f ↑r ≤ f ↑↑r

Proof state:
case refine_2
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
⊢ ⨅ q, f ↑↑q ≤ ⨅ r, f ↑r

Tactic:
refine le_ciInf fun q => ?_

Result:
case refine_2
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
⊢ ⨅ q, f ↑↑q ≤ f ↑q

Proof state:
case refine_1
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
this : Nonempty { r' // x < ↑r' }
r : { q' // x < ↑q' }
⊢ ⨅ r, f ↑r ≤ f ↑↑r

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

Result:
case refine_1.intro.intro
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 : ↑y < ↑↑r
⊢ ⨅ r, f ↑r ≤ f ↑↑r

Proof state:
case refine_2.intro.intro.refine_1.intro
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
y : ℚ
hxy : x < ↑y
hyq : ↑y < ↑q
u : { q' // x < ↑q' }
⊢ Set.Nonempty.some hf ≤ (fun q => f ↑↑q) u

Tactic:
suffices hfu : f u ∈ f '' Ioi x from hf.choose_spec hfu

Result:
case refine_2.intro.intro.refine_1.intro
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
y : ℚ
hxy : x < ↑y
hyq : ↑y < ↑q
u : { q' // x < ↑q' }
⊢ f ↑↑u ∈ f '' Ioi x

Proof state:
case refine_2.intro.intro.refine_3
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
y : ℚ
hxy : x < ↑y
hyq : ↑y < ↑q
⊢ ↑↑⟨y, hxy⟩ ≤ ↑y

Tactic:
norm_cast

Result:
no goals

Proof state:
case refine_2.intro.intro.refine_3
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
y : ℚ
hxy : x < ↑y
hyq : ↑y < ↑q
⊢ f ↑↑⟨y, hxy⟩ ≤ f ↑q

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

Result:
case refine_2.intro.intro.refine_3
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
y : ℚ
hxy : x < ↑y
hyq : ↑y < ↑q
⊢ ↑↑⟨y, hxy⟩ ≤ ↑y

Proof state:
case refine_2.intro.intro.refine_1
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
y : ℚ
hxy : x < ↑y
hyq : ↑y < ↑q
z : ℝ
⊢ (z ∈ range fun q => f ↑↑q) → Set.Nonempty.some hf ≤ z

Tactic:
rintro ⟨u, rfl⟩

Result:
case refine_2.intro.intro.refine_1.intro
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
y : ℚ
hxy : x < ↑y
hyq : ↑y < ↑q
u : { q' // x < ↑q' }
⊢ Set.Nonempty.some hf ≤ (fun q => f ↑↑q) u

Proof state:
case refine_1
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
⊢ ⨅ r, f ↑r ≤ ⨅ q, f ↑↑q

Tactic:
have : Nonempty { r' : ℚ // x < ↑r' } := by
  obtain ⟨r, hrx⟩ := exists_rat_gt x
  exact ⟨⟨r, hrx⟩⟩

Result:
case refine_1
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
this : Nonempty { r' // x < ↑r' }
⊢ ⨅ r, f ↑r ≤ ⨅ q, f ↑↑q

Proof state:
case refine_1.intro.intro
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 : ↑y < ↑↑r
⊢ ↑y < ↑↑r

Tactic:
exact_mod_cast hyr

Result:
no goals

Proof state:
case refine_2.intro.intro
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
y : ℚ
hxy : x < ↑y
hyq : ↑y < ↑q
⊢ ⨅ q, f ↑↑q ≤ f ↑q

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

Result:
case refine_2.intro.intro.refine_1
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
y : ℚ
hxy : x < ↑y
hyq : ↑y < ↑q
⊢ BddBelow (range fun q => f ↑↑q)

case refine_2.intro.intro.refine_2
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
y : ℚ
hxy : x < ↑y
hyq : ↑y < ↑q
⊢ { q' // x < ↑q' }

case refine_2.intro.intro.refine_3
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
y : ℚ
hxy : x < ↑y
hyq : ↑y < ↑q
⊢ f ↑↑?refine_2.intro.intro.refine_2 ≤ f ↑q

Proof state:
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
⊢ ⨅ r, f ↑r = ⨅ q, f ↑↑q

Tactic:
refine le_antisymm ?_ ?_

Result:
case refine_1
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
⊢ ⨅ r, f ↑r ≤ ⨅ q, f ↑↑q

case refine_2
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
⊢ ⨅ q, f ↑↑q ≤ ⨅ r, f ↑r

Proof state:
case refine_2
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
⊢ ⨅ q, f ↑↑q ≤ f ↑q

Tactic:
have hq := q.prop

Result:
case refine_2
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : ↑q ∈ Ioi x
⊢ ⨅ q, f ↑↑q ≤ f ↑q