-- Mathlib/Algebra/Order/CompleteField.lean
theorem inducedMap_rat (q : ℚ) : inducedMap α β (q : α) = q

Proof state:
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
q : ℚ
⊢ inducedMap α β ↑q = ↑q

Tactic:
refine csSup_eq_of_forall_le_of_forall_lt_exists_gt
  (cutMap_nonempty β (q : α)) (fun x h => ?_) fun w h => ?_

Result:
case refine_1
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
q : ℚ
x : β
h : x ∈ cutMap β ↑q
⊢ x ≤ ↑q

case refine_2
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
q : ℚ
w : β
h : w < ↑q
⊢ ∃ a ∈ cutMap β ↑q, w < a

Proof state:
case refine_1
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
q : ℚ
x : β
h : x ∈ cutMap β ↑q
⊢ x ≤ ↑q

Tactic:
rw [cutMap_coe] at h

Result:
case refine_1
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
q : ℚ
x : β
h : x ∈ Rat.cast '' {r | ↑r < ↑q}
⊢ x ≤ ↑q

Proof state:
case refine_1.intro.intro
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
q r : ℚ
h : r ∈ {r | ↑r < ↑q}
⊢ ↑r ≤ ↑q

Tactic:
exact le_of_lt h

Result:
no goals

Proof state:
case refine_2
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
q : ℚ
w : β
h : w < ↑q
⊢ ∃ a ∈ cutMap β ↑q, w < a

Tactic:
obtain ⟨q', hwq, hq⟩ := exists_rat_btwn h

Result:
case refine_2.intro.intro
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
q : ℚ
w : β
h : w < ↑q
q' : ℚ
hwq : w < ↑q'
hq : ↑q' < ↑q
⊢ ∃ a ∈ cutMap β ↑q, w < a

Proof state:
case refine_2.intro.intro
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
q : ℚ
w : β
h : w < ↑q
q' : ℚ
hwq : w < ↑q'
hq : ↑q' < ↑q
⊢ ∃ a ∈ Rat.cast '' {r | ↑r < ↑q}, w < a

Tactic:
exact ⟨q', ⟨_, hq, rfl⟩, hwq⟩

Result:
no goals

Proof state:
case refine_1
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
q : ℚ
x : β
h : x ∈ Rat.cast '' {r | ↑r < ↑q}
⊢ x ≤ ↑q

Tactic:
obtain ⟨r, h, rfl⟩ := h

Result:
case refine_1.intro.intro
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
q r : ℚ
h : r ∈ {r | ↑r < ↑q}
⊢ ↑r ≤ ↑q

Proof state:
case refine_2.intro.intro
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
q : ℚ
w : β
h : w < ↑q
q' : ℚ
hwq : w < ↑q'
hq : ↑q' < ↑q
⊢ ∃ a ∈ cutMap β ↑q, w < a

Tactic:
rw [cutMap_coe]

Result:
case refine_2.intro.intro
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
q : ℚ
w : β
h : w < ↑q
q' : ℚ
hwq : w < ↑q'
hq : ↑q' < ↑q
⊢ ∃ a ∈ Rat.cast '' {r | ↑r < ↑q}, w < a