case intro.intro
F : Type ?u.25469
α : Type u_1
β : Type u_2
γ : Type ?u.25478
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q✝ : ℚ
ha : 0 < a
q : ℚ
hb : q ∈ {t | ↑t < a * a}
⊢ ↑q ≤ inducedMap α β a * inducedMap α β a
F : Type ?u.25469
α : Type u_1
β : Type u_2
γ : Type ?u.25478
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b✝ : β
q : ℚ
ha : 0 < a
b : β
hb : b ∈ cutMap β (a * a)
⊢ b ≤ inducedMap α β a * inducedMap α β a
obtain ⟨q, hb, rfl⟩ := hb
case intro.intro.intro.intro.intro
F : Type ?u.25469
α : Type u_1
β : Type u_2
γ : Type ?u.25478
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q✝ : ℚ
ha : 0 < a
q : ℚ
hb : q ∈ {t | ↑t < a * a}
q' : ℚ
hq' : 0 < q'
hqq' : ↑q < ↑q' ^ 2
hqa : ↑q' ^ 2 < a * a
⊢ ↑q ≤ inducedMap α β a * inducedMap α β a
case intro.intro
F : Type ?u.25469
α : Type u_1
β : Type u_2
γ : Type ?u.25478
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q✝ : ℚ
ha : 0 < a
q : ℚ
hb : q ∈ {t | ↑t < a * a}
⊢ ↑q ≤ inducedMap α β a * inducedMap α β a
obtain ⟨q', hq', hqq', hqa⟩ := exists_rat_pow_btwn two_ne_zero hb (mul_self_pos.2 ha.ne')
F : Type ?u.25469
α : Type u_1
β : Type u_2
γ : Type ?u.25478
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q✝ : ℚ
ha : 0 < a
q : ℚ
hb : q ∈ {t | ↑t < a * a}
q' : ℚ
hq' : 0 < q'
hqq' : ↑q < ↑q' ^ 2
hqa : ↑q' ^ 2 < a * a
⊢ ↑q ≤ ↑q' ^ 2

F : Type ?u.25469
α : Type u_1
β : Type u_2
γ : Type ?u.25478
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q✝ : ℚ
ha : 0 < a
q : ℚ
hb : q ∈ {t | ↑t < a * a}
q' : ℚ
hq' : 0 < q'
hqq' : ↑q < ↑q' ^ 2
hqa : ↑q' ^ 2 < a * a
⊢ ↑q' ^ 2 ≤ inducedMap α β a * inducedMap α β a
case intro.intro.intro.intro.intro
F : Type ?u.25469
α : Type u_1
β : Type u_2
γ : Type ?u.25478
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q✝ : ℚ
ha : 0 < a
q : ℚ
hb : q ∈ {t | ↑t < a * a}
q' : ℚ
hq' : 0 < q'
hqq' : ↑q < ↑q' ^ 2
hqa : ↑q' ^ 2 < a * a
⊢ ↑q ≤ inducedMap α β a * inducedMap α β a
trans (q' : β) ^ 2
F : Type ?u.25469
α : Type u_1
β : Type u_2
γ : Type ?u.25478
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q✝ : ℚ
ha : 0 < a
q : ℚ
hb : q ∈ {t | ↑t < a * a}
q' : ℚ
hq' : 0 < q'
hqq' : ↑q < ↑q' ^ 2
hqa : ↑q' ^ 2 < a * a
⊢ ↑q' ^ 2 ≤ inducedMap α β a * inducedMap α β a
F : Type ?u.25469
α : Type u_1
β : Type u_2
γ : Type ?u.25478
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q✝ : ℚ
ha : 0 < a
q : ℚ
hb : q ∈ {t | ↑t < a * a}
q' : ℚ
hq' : 0 < q'
hqq' : ↑q < ↑q' ^ 2
hqa : ↑q' ^ 2 < a * a
⊢ ↑q ≤ ↑q' ^ 2

F : Type ?u.25469
α : Type u_1
β : Type u_2
γ : Type ?u.25478
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q✝ : ℚ
ha : 0 < a
q : ℚ
hb : q ∈ {t | ↑t < a * a}
q' : ℚ
hq' : 0 < q'
hqq' : ↑q < ↑q' ^ 2
hqa : ↑q' ^ 2 < a * a
⊢ ↑q' ^ 2 ≤ inducedMap α β a * inducedMap α β a
exact_mod_cast hqq'.le
F : Type ?u.25469
α : Type u_1
β : Type u_2
γ : Type ?u.25478
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q✝ : ℚ
ha : 0 < a
q : ℚ
hb : q ∈ {t | ↑t < a * a}
q' : ℚ
hq' : 0 < q'
hqq' : ↑q < ↑q' ^ 2
hqa : ↑q' * ↑q' < a * a
⊢ ↑q' * ↑q' ≤ inducedMap α β a * inducedMap α β a
F : Type ?u.25469
α : Type u_1
β : Type u_2
γ : Type ?u.25478
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q✝ : ℚ
ha : 0 < a
q : ℚ
hb : q ∈ {t | ↑t < a * a}
q' : ℚ
hq' : 0 < q'
hqq' : ↑q < ↑q' ^ 2
hqa : ↑q' ^ 2 < a * a
⊢ ↑q' ^ 2 ≤ inducedMap α β a * inducedMap α β a
rw [pow_two] at hqa ⊢
F : Type ?u.25469
α : Type u_1
β : Type u_2
γ : Type ?u.25478
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q✝ : ℚ
ha : 0 < a
q : ℚ
hb : q ∈ {t | ↑t < a * a}
q' : ℚ
hq' : 0 < q'
hqq' : ↑q < ↑q' ^ 2
hqa : ↑q' * ↑q' < a * a
⊢ ↑q' * ↑q' ≤ inducedMap α β a * inducedMap α β a
F : Type ?u.25469
α : Type u_1
β : Type u_2
γ : Type ?u.25478
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q✝ : ℚ
ha : 0 < a
q : ℚ
hb : q ∈ {t | ↑t < a * a}
q' : ℚ
hq' : 0 < q'
hqq' : ↑q < ↑q' ^ 2
hqa : ↑q' * ↑q' < a * a
⊢ ↑q' * ↑q' ≤ inducedMap α β a * inducedMap α β a
push_cast at hqa
no goals
F : Type ?u.25469
α : Type u_1
β : Type u_2
γ : Type ?u.25478
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q✝ : ℚ
ha : 0 < a
q : ℚ
hb : q ∈ {t | ↑t < a * a}
q' : ℚ
hq' : 0 < q'
hqq' : ↑q < ↑q' ^ 2
hqa : ↑q' * ↑q' < a * a
⊢ ↑q' * ↑q' ≤ inducedMap α β a * inducedMap α β a
exact mul_self_le_mul_self (by exact_mod_cast hq'.le)
  (le_csSup (cutMap_bddAbove β a) <|
    coe_mem_cutMap_iff.2 <| lt_of_mul_self_lt_mul_self ha.le hqa)
no goals
F : Type ?u.25469
α : Type u_1
β : Type u_2
γ : Type ?u.25478
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q✝ : ℚ
ha : 0 < a
q : ℚ
hb : q ∈ {t | ↑t < a * a}
q' : ℚ
hq' : 0 < q'
hqq' : ↑q < ↑q' ^ 2
hqa : ↑q' * ↑q' < a * a
⊢ 0 ≤ ↑q'
exact_mod_cast hq'.le