case refine_1
F : Type ?u.20995
α : Type u_2
β : Type u_1
γ : Type ?u.21004
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
h : ↑q < inducedMap α β a
⊢ ↑q < a

case refine_2
F : Type ?u.20995
α : Type u_2
β : Type u_1
γ : Type ?u.21004
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
hq : ↑q < a
⊢ ↑q < inducedMap α β a
F : Type ?u.20995
α : Type u_2
β : Type u_1
γ : Type ?u.21004
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
⊢ ↑q < inducedMap α β a ↔ ↑q < a
refine ⟨fun h => ?_, fun hq => ?_⟩
case refine_1
F : Type ?u.20995
α : Type u_2
β : Type u_1
γ : Type ?u.21004
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
h : inducedMap α β ↑q < inducedMap α β a
⊢ ↑q < a
case refine_1
F : Type ?u.20995
α : Type u_2
β : Type u_1
γ : Type ?u.21004
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
h : ↑q < inducedMap α β a
⊢ ↑q < a
rw [← inducedMap_rat α] at h
no goals
case refine_1
F : Type ?u.20995
α : Type u_2
β : Type u_1
γ : Type ?u.21004
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
h : inducedMap α β ↑q < inducedMap α β a
⊢ ↑q < a
exact (inducedMap_mono α β).reflect_lt h
case refine_2.intro.intro
F : Type ?u.20995
α : Type u_2
β : Type u_1
γ : Type ?u.21004
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
hq✝ : ↑q < a
q' : ℚ
hq : ↑q < ↑q'
hqa : ↑q' < a
⊢ ↑q < inducedMap α β a
case refine_2
F : Type ?u.20995
α : Type u_2
β : Type u_1
γ : Type ?u.21004
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
hq : ↑q < a
⊢ ↑q < inducedMap α β a
obtain ⟨q', hq, hqa⟩ := exists_rat_btwn hq
case refine_2.intro.intro
F : Type ?u.20995
α : Type u_2
β : Type u_1
γ : Type ?u.21004
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
hq✝ : ↑q < a
q' : ℚ
hq : ↑q < ↑q'
hqa : ↑q' < a
⊢ ↑q < ↑q'
case refine_2.intro.intro
F : Type ?u.20995
α : Type u_2
β : Type u_1
γ : Type ?u.21004
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
hq✝ : ↑q < a
q' : ℚ
hq : ↑q < ↑q'
hqa : ↑q' < a
⊢ ↑q < inducedMap α β a
apply lt_csSup_of_lt (cutMap_bddAbove β a) (coe_mem_cutMap_iff.mpr hqa)
no goals
case refine_2.intro.intro
F : Type ?u.20995
α : Type u_2
β : Type u_1
γ : Type ?u.21004
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
hq✝ : ↑q < a
q' : ℚ
hq : ↑q < ↑q'
hqa : ↑q' < a
⊢ ↑q < ↑q'
exact_mod_cast hq