case refine_1
F : Type ?u.17063
α : Type u_2
β : Type u_1
γ : Type ?u.17072
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
q : ℚ
x : β
h : x ∈ cutMap β ↑q
⊢ x ≤ ↑q

case refine_2
F : Type ?u.17063
α : Type u_2
β : Type u_1
γ : Type ?u.17072
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
q : ℚ
w : β
h : w < ↑q
⊢ ∃ a, a ∈ cutMap β ↑q ∧ w < a
F : Type ?u.17063
α : Type u_2
β : Type u_1
γ : Type ?u.17072
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
q : ℚ
⊢ inducedMap α β ↑q = ↑q
refine csSup_eq_of_forall_le_of_forall_lt_exists_gt
  (cutMap_nonempty β (q : α)) (fun x h => ?_) fun w h => ?_
case refine_1
F : Type ?u.17063
α : Type u_2
β : Type u_1
γ : Type ?u.17072
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
q : ℚ
x : β
h : x ∈ Rat.cast '' {r | ↑r < ↑q}
⊢ x ≤ ↑q
case refine_1
F : Type ?u.17063
α : Type u_2
β : Type u_1
γ : Type ?u.17072
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
q : ℚ
x : β
h : x ∈ cutMap β ↑q
⊢ x ≤ ↑q
rw [cutMap_coe] at h
case refine_1.intro.intro
F : Type ?u.17063
α : Type u_2
β : Type u_1
γ : Type ?u.17072
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
q r : ℚ
h : r ∈ {r | ↑r < ↑q}
⊢ ↑r ≤ ↑q
case refine_1
F : Type ?u.17063
α : Type u_2
β : Type u_1
γ : Type ?u.17072
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
q : ℚ
x : β
h : x ∈ Rat.cast '' {r | ↑r < ↑q}
⊢ x ≤ ↑q
obtain ⟨r, h, rfl⟩ := h
no goals
case refine_1.intro.intro
F : Type ?u.17063
α : Type u_2
β : Type u_1
γ : Type ?u.17072
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
q r : ℚ
h : r ∈ {r | ↑r < ↑q}
⊢ ↑r ≤ ↑q
exact le_of_lt h
case refine_2.intro.intro
F : Type ?u.17063
α : Type u_2
β : Type u_1
γ : Type ?u.17072
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
q : ℚ
w : β
h : w < ↑q
q' : ℚ
hwq : w < ↑q'
hq : ↑q' < ↑q
⊢ ∃ a, a ∈ cutMap β ↑q ∧ w < a
case refine_2
F : Type ?u.17063
α : Type u_2
β : Type u_1
γ : Type ?u.17072
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
q : ℚ
w : β
h : w < ↑q
⊢ ∃ a, a ∈ cutMap β ↑q ∧ w < a
obtain ⟨q', hwq, hq⟩ := exists_rat_btwn h
case refine_2.intro.intro
F : Type ?u.17063
α : Type u_2
β : Type u_1
γ : Type ?u.17072
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
q : ℚ
w : β
h : w < ↑q
q' : ℚ
hwq : w < ↑q'
hq : ↑q' < ↑q
⊢ ∃ a, a ∈ Rat.cast '' {r | ↑r < ↑q} ∧ w < a
case refine_2.intro.intro
F : Type ?u.17063
α : Type u_2
β : Type u_1
γ : Type ?u.17072
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
q : ℚ
w : β
h : w < ↑q
q' : ℚ
hwq : w < ↑q'
hq : ↑q' < ↑q
⊢ ∃ a, a ∈ cutMap β ↑q ∧ w < a
rw [cutMap_coe]
no goals
case refine_2.intro.intro
F : Type ?u.17063
α : Type u_2
β : Type u_1
γ : Type ?u.17072
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
q : ℚ
w : β
h : w < ↑q
q' : ℚ
hwq : w < ↑q'
hq : ↑q' < ↑q
⊢ ∃ a, a ∈ Rat.cast '' {r | ↑r < ↑q} ∧ w < a
exact ⟨q', ⟨_, hq, rfl⟩, hwq⟩