[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : ConditionallyCompleteLinearOrderedField α
⊢ ∀ (x : α), ∃ n, x < ↑n
[PROOFSTEP]
by_contra' h
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : ConditionallyCompleteLinearOrderedField α
h : ∃ x, ∀ (n : ℕ), ↑n ≤ x
⊢ False
[PROOFSTEP]
obtain ⟨x, h⟩ := h
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : ConditionallyCompleteLinearOrderedField α
x : α
h : ∀ (n : ℕ), ↑n ≤ x
⊢ False
[PROOFSTEP]
have :=
  csSup_le _ _ (range_nonempty Nat.cast)
    (forall_range_iff.2 fun m => le_sub_iff_add_le.2 <| le_csSup _ _ ⟨x, forall_range_iff.2 h⟩ ⟨m + 1, Nat.cast_succ m⟩)
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : ConditionallyCompleteLinearOrderedField α
x : α
h : ∀ (n : ℕ), ↑n ≤ x
this : sSup (range Nat.cast) ≤ sSup (range fun i => ↑i) - 1
⊢ False
[PROOFSTEP]
linarith
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : LinearOrderedField α
inst✝ : DivisionRing β
a✝ a₁ a₂ : α
b : β
q : ℚ
a : α
⊢ cutMap α a = Iio a ∩ range Rat.cast
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : LinearOrderedField α
inst✝ : DivisionRing β
a✝ a₁ a₂ : α
b : β
q : ℚ
a x✝ : α
⊢ x✝ ∈ cutMap α a ↔ x✝ ∈ Iio a ∩ range Rat.cast
[PROOFSTEP]
constructor
[GOAL]
case h.mp
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : LinearOrderedField α
inst✝ : DivisionRing β
a✝ a₁ a₂ : α
b : β
q : ℚ
a x✝ : α
⊢ x✝ ∈ cutMap α a → x✝ ∈ Iio a ∩ range Rat.cast
[PROOFSTEP]
rintro ⟨q, h, rfl⟩
[GOAL]
case h.mp.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : LinearOrderedField α
inst✝ : DivisionRing β
a✝ a₁ a₂ : α
b : β
q✝ : ℚ
a : α
q : ℚ
h : q ∈ {t | ↑t < a}
⊢ ↑q ∈ Iio a ∩ range Rat.cast
[PROOFSTEP]
exact ⟨h, q, rfl⟩
[GOAL]
case h.mpr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : LinearOrderedField α
inst✝ : DivisionRing β
a✝ a₁ a₂ : α
b : β
q : ℚ
a x✝ : α
⊢ x✝ ∈ Iio a ∩ range Rat.cast → x✝ ∈ cutMap α a
[PROOFSTEP]
rintro ⟨h, q, rfl⟩
[GOAL]
case h.mpr.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : LinearOrderedField α
inst✝ : DivisionRing β
a✝ a₁ a₂ : α
b : β
q✝ : ℚ
a : α
q : ℚ
h : ↑q ∈ Iio a
⊢ ↑q ∈ cutMap α a
[PROOFSTEP]
exact ⟨q, h, rfl⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : LinearOrderedField α
inst✝ : LinearOrderedField β
a a₁ a₂ : α
b : β
q✝ q : ℚ
⊢ cutMap β ↑q = Rat.cast '' {r | ↑r < ↑q}
[PROOFSTEP]
simp_rw [cutMap, Rat.cast_lt]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
a✝ a₁ a₂ : α
b : β
q : ℚ
inst✝ : Archimedean α
a : α
⊢ BddAbove (cutMap β a)
[PROOFSTEP]
obtain ⟨q, hq⟩ := exists_rat_gt a
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
a✝ a₁ a₂ : α
b : β
q✝ : ℚ
inst✝ : Archimedean α
a : α
q : ℚ
hq : a < ↑q
⊢ BddAbove (cutMap β a)
[PROOFSTEP]
exact ⟨q, ball_image_iff.2 fun r hr => by exact_mod_cast (hq.trans' hr).le⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
a✝ a₁ a₂ : α
b : β
q✝ : ℚ
inst✝ : Archimedean α
a : α
q : ℚ
hq : a < ↑q
r : ℚ
hr : r ∈ {t | ↑t < a}
⊢ ↑r ≤ ↑q
[PROOFSTEP]
exact_mod_cast (hq.trans' hr).le
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
a✝ a₁ a₂ : α
b✝ : β
q : ℚ
inst✝ : Archimedean α
a b : α
⊢ cutMap β (a + b) = cutMap β a + cutMap β b
[PROOFSTEP]
refine (image_subset_iff.2 fun q hq => ?_).antisymm ?_
[GOAL]
case refine_1
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
a✝ a₁ a₂ : α
b✝ : β
q✝ : ℚ
inst✝ : Archimedean α
a b : α
q : ℚ
hq : q ∈ {t | ↑t < a + b}
⊢ q ∈ Rat.cast ⁻¹' (cutMap β a + cutMap β b)
[PROOFSTEP]
rw [mem_setOf_eq, ← sub_lt_iff_lt_add] at hq 
[GOAL]
case refine_1
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
a✝ a₁ a₂ : α
b✝ : β
q✝ : ℚ
inst✝ : Archimedean α
a b : α
q : ℚ
hq : ↑q - b < a
⊢ q ∈ Rat.cast ⁻¹' (cutMap β a + cutMap β b)
[PROOFSTEP]
obtain ⟨q₁, hq₁q, hq₁ab⟩ := exists_rat_btwn hq
[GOAL]
case refine_1.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
a✝ a₁ a₂ : α
b✝ : β
q✝ : ℚ
inst✝ : Archimedean α
a b : α
q : ℚ
hq : ↑q - b < a
q₁ : ℚ
hq₁q : ↑q - b < ↑q₁
hq₁ab : ↑q₁ < a
⊢ q ∈ Rat.cast ⁻¹' (cutMap β a + cutMap β b)
[PROOFSTEP]
refine ⟨q₁, q - q₁, by rwa [coe_mem_cutMap_iff], ?_, add_sub_cancel'_right _ _⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
a✝ a₁ a₂ : α
b✝ : β
q✝ : ℚ
inst✝ : Archimedean α
a b : α
q : ℚ
hq : ↑q - b < a
q₁ : ℚ
hq₁q : ↑q - b < ↑q₁
hq₁ab : ↑q₁ < a
⊢ ↑q₁ ∈ cutMap β a
[PROOFSTEP]
rwa [coe_mem_cutMap_iff]
[GOAL]
case refine_1.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
a✝ a₁ a₂ : α
b✝ : β
q✝ : ℚ
inst✝ : Archimedean α
a b : α
q : ℚ
hq : ↑q - b < a
q₁ : ℚ
hq₁q : ↑q - b < ↑q₁
hq₁ab : ↑q₁ < a
⊢ ↑q - ↑q₁ ∈ cutMap β b
[PROOFSTEP]
norm_cast
[GOAL]
case refine_1.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
a✝ a₁ a₂ : α
b✝ : β
q✝ : ℚ
inst✝ : Archimedean α
a b : α
q : ℚ
hq : ↑q - b < a
q₁ : ℚ
hq₁q : ↑q - b < ↑q₁
hq₁ab : ↑q₁ < a
⊢ ↑(q - q₁) ∈ cutMap β b
[PROOFSTEP]
rw [coe_mem_cutMap_iff]
[GOAL]
case refine_1.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
a✝ a₁ a₂ : α
b✝ : β
q✝ : ℚ
inst✝ : Archimedean α
a b : α
q : ℚ
hq : ↑q - b < a
q₁ : ℚ
hq₁q : ↑q - b < ↑q₁
hq₁ab : ↑q₁ < a
⊢ ↑(q - q₁) < b
[PROOFSTEP]
exact_mod_cast sub_lt_comm.mp hq₁q
[GOAL]
case refine_2
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
a✝ a₁ a₂ : α
b✝ : β
q : ℚ
inst✝ : Archimedean α
a b : α
⊢ cutMap β a + cutMap β b ⊆ Rat.cast '' {t | ↑t < a + b}
[PROOFSTEP]
rintro _ ⟨_, _, ⟨qa, ha, rfl⟩, ⟨qb, hb, rfl⟩, rfl⟩
[GOAL]
case refine_2.intro.intro.intro.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
a✝ a₁ a₂ : α
b✝ : β
q : ℚ
inst✝ : Archimedean α
a b : α
qa : ℚ
ha : qa ∈ {t | ↑t < a}
qb : ℚ
hb : qb ∈ {t | ↑t < b}
⊢ (fun x x_1 => x + x_1) ↑qa ↑qb ∈ Rat.cast '' {t | ↑t < a + b}
[PROOFSTEP]
refine' ⟨qa + qb, _, by norm_cast⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
a✝ a₁ a₂ : α
b✝ : β
q : ℚ
inst✝ : Archimedean α
a b : α
qa : ℚ
ha : qa ∈ {t | ↑t < a}
qb : ℚ
hb : qb ∈ {t | ↑t < b}
⊢ ↑(qa + qb) = (fun x x_1 => x + x_1) ↑qa ↑qb
[PROOFSTEP]
norm_cast
[GOAL]
case refine_2.intro.intro.intro.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
a✝ a₁ a₂ : α
b✝ : β
q : ℚ
inst✝ : Archimedean α
a b : α
qa : ℚ
ha : qa ∈ {t | ↑t < a}
qb : ℚ
hb : qb ∈ {t | ↑t < b}
⊢ qa + qb ∈ {t | ↑t < a + b}
[PROOFSTEP]
rw [mem_setOf_eq, cast_add]
[GOAL]
case refine_2.intro.intro.intro.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
a✝ a₁ a₂ : α
b✝ : β
q : ℚ
inst✝ : Archimedean α
a b : α
qa : ℚ
ha : qa ∈ {t | ↑t < a}
qb : ℚ
hb : qb ∈ {t | ↑t < b}
⊢ ↑qa + ↑qb < a + b
[PROOFSTEP]
exact add_lt_add ha hb
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
q : ℚ
⊢ inducedMap α β ↑q = ↑q
[PROOFSTEP]
refine csSup_eq_of_forall_le_of_forall_lt_exists_gt (cutMap_nonempty β (q : α)) (fun x h => ?_) fun w h => ?_
[GOAL]
case refine_1
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
q : ℚ
x : β
h : x ∈ cutMap β ↑q
⊢ x ≤ ↑q
[PROOFSTEP]
rw [cutMap_coe] at h 
[GOAL]
case refine_1
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
q : ℚ
x : β
h : x ∈ Rat.cast '' {r | ↑r < ↑q}
⊢ x ≤ ↑q
[PROOFSTEP]
obtain ⟨r, h, rfl⟩ := h
[GOAL]
case refine_1.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
q r : ℚ
h : r ∈ {r | ↑r < ↑q}
⊢ ↑r ≤ ↑q
[PROOFSTEP]
exact le_of_lt h
[GOAL]
case refine_2
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
q : ℚ
w : β
h : w < ↑q
⊢ ∃ a, a ∈ cutMap β ↑q ∧ w < a
[PROOFSTEP]
obtain ⟨q', hwq, hq⟩ := exists_rat_btwn h
[GOAL]
case refine_2.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
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
[PROOFSTEP]
rw [cutMap_coe]
[GOAL]
case refine_2.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
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
[PROOFSTEP]
exact ⟨q', ⟨_, hq, rfl⟩, hwq⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
⊢ inducedMap α β 0 = 0
[PROOFSTEP]
exact_mod_cast inducedMap_rat α β 0
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
⊢ inducedMap α β 1 = 1
[PROOFSTEP]
exact_mod_cast inducedMap_rat α β 1
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
⊢ ↑q < inducedMap α β a ↔ ↑q < a
[PROOFSTEP]
refine ⟨fun h => ?_, fun hq => ?_⟩
[GOAL]
case refine_1
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
h : ↑q < inducedMap α β a
⊢ ↑q < a
[PROOFSTEP]
rw [← inducedMap_rat α] at h 
[GOAL]
case refine_1
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
h : inducedMap α β ↑q < inducedMap α β a
⊢ ↑q < a
[PROOFSTEP]
exact (inducedMap_mono α β).reflect_lt h
[GOAL]
case refine_2
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
hq : ↑q < a
⊢ ↑q < inducedMap α β a
[PROOFSTEP]
obtain ⟨q', hq, hqa⟩ := exists_rat_btwn hq
[GOAL]
case refine_2.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
hq✝ : ↑q < a
q' : ℚ
hq : ↑q < ↑q'
hqa : ↑q' < a
⊢ ↑q < inducedMap α β a
[PROOFSTEP]
apply lt_csSup_of_lt (cutMap_bddAbove β a) (coe_mem_cutMap_iff.mpr hqa)
[GOAL]
case refine_2.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
hq✝ : ↑q < a
q' : ℚ
hq : ↑q < ↑q'
hqa : ↑q' < a
⊢ ↑q < ↑q'
[PROOFSTEP]
exact_mod_cast hq
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q✝ : ℚ
x✝ : ∃ q, b < ↑q ∧ ↑q < a
q : ℚ
hbq : b < ↑q
hqa : ↑q < a
⊢ ↑q < inducedMap α β a
[PROOFSTEP]
rwa [coe_lt_inducedMap_iff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a✝ : α
b : β
q✝ : ℚ
a : α
q : ℚ
⊢ ↑q < inducedMap β γ (inducedMap α β a) ↔ ↑q < inducedMap α γ a
[PROOFSTEP]
rw [coe_lt_inducedMap_iff, coe_lt_inducedMap_iff, Iff.comm, coe_lt_inducedMap_iff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b✝ : β
q : ℚ
b : β
⊢ inducedMap γ β (inducedMap β γ b) = b
[PROOFSTEP]
rw [inducedMap_inducedMap, inducedMap_self]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
x y : α
⊢ inducedMap α β (x + y) = inducedMap α β x + inducedMap α β y
[PROOFSTEP]
rw [inducedMap, cutMap_add]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
x y : α
⊢ sSup (cutMap β x + cutMap β y) = inducedMap α β x + inducedMap α β y
[PROOFSTEP]
exact csSup_add (cutMap_nonempty β x) (cutMap_bddAbove β x) (cutMap_nonempty β y) (cutMap_bddAbove β y)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
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
[PROOFSTEP]
obtain ⟨q, hb, rfl⟩ := hb
[GOAL]
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
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
[PROOFSTEP]
obtain ⟨q', hq', hqq', hqa⟩ := exists_rat_pow_btwn two_ne_zero hb (mul_self_pos.2 ha.ne')
[GOAL]
case intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
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
[PROOFSTEP]
trans (q' : β) ^ 2
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
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_1
α : Type u_2
β : Type u_3
γ : Type u_4
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
[PROOFSTEP]
exact_mod_cast hqq'.le
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
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
[PROOFSTEP]
rw [pow_two] at hqa ⊢
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
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
[PROOFSTEP]
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)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
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'
[PROOFSTEP]
exact_mod_cast hq'.le
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b✝ : β
q : ℚ
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
⊢ ∃ c, c ∈ cutMap β (a * a) ∧ b < c
[PROOFSTEP]
obtain hb | hb := lt_or_le b 0
[GOAL]
case inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b✝ : β
q : ℚ
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : b < 0
⊢ ∃ c, c ∈ cutMap β (a * a) ∧ b < c
[PROOFSTEP]
refine ⟨0, ?_, hb⟩
[GOAL]
case inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b✝ : β
q : ℚ
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : b < 0
⊢ 0 ∈ cutMap β (a * a)
[PROOFSTEP]
rw [← Rat.cast_zero, coe_mem_cutMap_iff, Rat.cast_zero]
[GOAL]
case inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b✝ : β
q : ℚ
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : b < 0
⊢ 0 < a * a
[PROOFSTEP]
exact mul_self_pos.2 ha.ne'
[GOAL]
case inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b✝ : β
q : ℚ
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
⊢ ∃ c, c ∈ cutMap β (a * a) ∧ b < c
[PROOFSTEP]
obtain ⟨q, hq, hbq, hqa⟩ := exists_rat_pow_btwn two_ne_zero hba (hb.trans_lt hba)
[GOAL]
case inr.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b✝ : β
q✝ : ℚ
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < ↑q ^ 2
hqa : ↑q ^ 2 < inducedMap α β a * inducedMap α β a
⊢ ∃ c, c ∈ cutMap β (a * a) ∧ b < c
[PROOFSTEP]
rw [← cast_pow] at hbq 
[GOAL]
case inr.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b✝ : β
q✝ : ℚ
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < ↑(q ^ 2)
hqa : ↑q ^ 2 < inducedMap α β a * inducedMap α β a
⊢ ∃ c, c ∈ cutMap β (a * a) ∧ b < c
[PROOFSTEP]
refine ⟨(q ^ 2 : ℚ), coe_mem_cutMap_iff.2 ?_, hbq⟩
[GOAL]
case inr.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b✝ : β
q✝ : ℚ
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < ↑(q ^ 2)
hqa : ↑q ^ 2 < inducedMap α β a * inducedMap α β a
⊢ ↑(q ^ 2) < a * a
[PROOFSTEP]
rw [pow_two] at hqa ⊢
[GOAL]
case inr.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b✝ : β
q✝ : ℚ
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < ↑(q ^ 2)
hqa : ↑q * ↑q < inducedMap α β a * inducedMap α β a
⊢ ↑(q * q) < a * a
[PROOFSTEP]
push_cast
[GOAL]
case inr.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b✝ : β
q✝ : ℚ
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < ↑(q ^ 2)
hqa : ↑q * ↑q < inducedMap α β a * inducedMap α β a
⊢ ↑q * ↑q < a * a
[PROOFSTEP]
obtain ⟨q', hq', hqa'⟩ := lt_inducedMap_iff.1 (lt_of_mul_self_lt_mul_self (inducedMap_nonneg ha.le) hqa)
[GOAL]
case inr.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b✝ : β
q✝ : ℚ
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < ↑(q ^ 2)
hqa : ↑q * ↑q < inducedMap α β a * inducedMap α β a
q' : ℚ
hq' : ↑q < ↑q'
hqa' : ↑q' < a
⊢ ↑q * ↑q < a * a
[PROOFSTEP]
exact mul_self_lt_mul_self (by exact_mod_cast hq.le) (hqa'.trans' <| by assumption_mod_cast)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b✝ : β
q✝ : ℚ
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < ↑(q ^ 2)
hqa : ↑q * ↑q < inducedMap α β a * inducedMap α β a
q' : ℚ
hq' : ↑q < ↑q'
hqa' : ↑q' < a
⊢ 0 ≤ ↑q
[PROOFSTEP]
exact_mod_cast hq.le
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b✝ : β
q✝ : ℚ
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < ↑(q ^ 2)
hqa : ↑q * ↑q < inducedMap α β a * inducedMap α β a
q' : ℚ
hq' : ↑q < ↑q'
hqa' : ↑q' < a
⊢ ↑q < ↑q'
[PROOFSTEP]
assumption_mod_cast
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
⊢ ∀ (x : α), ↑(inducedAddHom α β) (x * x) = ↑(inducedAddHom α β) x * ↑(inducedAddHom α β) x
[PROOFSTEP]
suffices : ∀ x, 0 < x → inducedAddHom α β (x * x) = inducedAddHom α β x * inducedAddHom α β x
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
this : ∀ (x : α), 0 < x → ↑(inducedAddHom α β) (x * x) = ↑(inducedAddHom α β) x * ↑(inducedAddHom α β) x
⊢ ∀ (x : α), ↑(inducedAddHom α β) (x * x) = ↑(inducedAddHom α β) x * ↑(inducedAddHom α β) x
[PROOFSTEP]
intro x
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
this : ∀ (x : α), 0 < x → ↑(inducedAddHom α β) (x * x) = ↑(inducedAddHom α β) x * ↑(inducedAddHom α β) x
x : α
⊢ ↑(inducedAddHom α β) (x * x) = ↑(inducedAddHom α β) x * ↑(inducedAddHom α β) x
[PROOFSTEP]
obtain h | rfl | h := lt_trichotomy x 0
[GOAL]
case inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
this : ∀ (x : α), 0 < x → ↑(inducedAddHom α β) (x * x) = ↑(inducedAddHom α β) x * ↑(inducedAddHom α β) x
x : α
h : x < 0
⊢ ↑(inducedAddHom α β) (x * x) = ↑(inducedAddHom α β) x * ↑(inducedAddHom α β) x
[PROOFSTEP]
convert this (-x) (neg_pos.2 h) using 1
[GOAL]
case h.e'_2
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
this : ∀ (x : α), 0 < x → ↑(inducedAddHom α β) (x * x) = ↑(inducedAddHom α β) x * ↑(inducedAddHom α β) x
x : α
h : x < 0
⊢ ↑(inducedAddHom α β) (x * x) = ↑(inducedAddHom α β) (-x * -x)
[PROOFSTEP]
rw [neg_mul, mul_neg, neg_neg]
[GOAL]
case h.e'_3
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
this : ∀ (x : α), 0 < x → ↑(inducedAddHom α β) (x * x) = ↑(inducedAddHom α β) x * ↑(inducedAddHom α β) x
x : α
h : x < 0
⊢ ↑(inducedAddHom α β) x * ↑(inducedAddHom α β) x = ↑(inducedAddHom α β) (-x) * ↑(inducedAddHom α β) (-x)
[PROOFSTEP]
simp_rw [AddMonoidHom.map_neg, neg_mul, mul_neg, neg_neg]
[GOAL]
case inr.inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
this : ∀ (x : α), 0 < x → ↑(inducedAddHom α β) (x * x) = ↑(inducedAddHom α β) x * ↑(inducedAddHom α β) x
⊢ ↑(inducedAddHom α β) (0 * 0) = ↑(inducedAddHom α β) 0 * ↑(inducedAddHom α β) 0
[PROOFSTEP]
simp only [mul_zero, AddMonoidHom.map_zero]
[GOAL]
case inr.inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
this : ∀ (x : α), 0 < x → ↑(inducedAddHom α β) (x * x) = ↑(inducedAddHom α β) x * ↑(inducedAddHom α β) x
x : α
h : 0 < x
⊢ ↑(inducedAddHom α β) (x * x) = ↑(inducedAddHom α β) x * ↑(inducedAddHom α β) x
[PROOFSTEP]
exact this x h
[GOAL]
case this
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
⊢ ∀ (x : α), 0 < x → ↑(inducedAddHom α β) (x * x) = ↑(inducedAddHom α β) x * ↑(inducedAddHom α β) x
[PROOFSTEP]
refine fun x hx => csSup_eq_of_forall_le_of_forall_lt_exists_gt (cutMap_nonempty β _) ?_ ?_
[GOAL]
case this.refine_1
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
x : α
hx : 0 < x
⊢ ∀ (a : (fun x => β) (x * x)), a ∈ cutMap β (x * x) → a ≤ ↑(inducedAddHom α β) x * ↑(inducedAddHom α β) x
[PROOFSTEP]
exact le_inducedMap_mul_self_of_mem_cutMap hx
[GOAL]
case this.refine_2
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
x : α
hx : 0 < x
⊢ ∀ (w : (fun x => β) (x * x)), w < ↑(inducedAddHom α β) x * ↑(inducedAddHom α β) x → ∃ a, a ∈ cutMap β (x * x) ∧ w < a
[PROOFSTEP]
exact exists_mem_cutMap_mul_self_of_lt_inducedMap_mul_self hx
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
src✝ : β →+*o γ := inducedOrderRingHom β γ
⊢ ∀ {a b : β},
    Equiv.toFun
          {
              toEquiv :=
                { toFun := src✝.toFun, invFun := inducedMap γ β,
                  left_inv := (_ : ∀ (b : β), inducedMap γ β (inducedMap β γ b) = b),
                  right_inv := (_ : ∀ (b : γ), inducedMap β γ (inducedMap γ β b) = b) },
              map_mul' :=
                (_ :
                  ∀ (x y : β),
                    OneHom.toFun (↑↑src✝.toRingHom) (x * y) =
                      OneHom.toFun (↑↑src✝.toRingHom) x * OneHom.toFun (↑↑src✝.toRingHom) y),
              map_add' :=
                (_ :
                  ∀ (x y : β),
                    OneHom.toFun (↑↑src✝.toRingHom) (x + y) =
                      OneHom.toFun (↑↑src✝.toRingHom) x + OneHom.toFun (↑↑src✝.toRingHom) y) }.toEquiv
          a ≤
        Equiv.toFun
          {
              toEquiv :=
                { toFun := src✝.toFun, invFun := inducedMap γ β,
                  left_inv := (_ : ∀ (b : β), inducedMap γ β (inducedMap β γ b) = b),
                  right_inv := (_ : ∀ (b : γ), inducedMap β γ (inducedMap γ β b) = b) },
              map_mul' :=
                (_ :
                  ∀ (x y : β),
                    OneHom.toFun (↑↑src✝.toRingHom) (x * y) =
                      OneHom.toFun (↑↑src✝.toRingHom) x * OneHom.toFun (↑↑src✝.toRingHom) y),
              map_add' :=
                (_ :
                  ∀ (x y : β),
                    OneHom.toFun (↑↑src✝.toRingHom) (x + y) =
                      OneHom.toFun (↑↑src✝.toRingHom) x + OneHom.toFun (↑↑src✝.toRingHom) y) }.toEquiv
          b ↔
      a ≤ b
[PROOFSTEP]
dsimp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
src✝ : β →+*o γ := inducedOrderRingHom β γ
⊢ ∀ {a b : β}, ↑(inducedOrderRingHom β γ).toRingHom a ≤ ↑(inducedOrderRingHom β γ).toRingHom b ↔ a ≤ b
[PROOFSTEP]
refine ⟨fun h => ?_, fun h => inducedMap_mono _ _ h⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
src✝ : β →+*o γ := inducedOrderRingHom β γ
a✝ b✝ : β
h : ↑(inducedOrderRingHom β γ).toRingHom a✝ ≤ ↑(inducedOrderRingHom β γ).toRingHom b✝
⊢ a✝ ≤ b✝
[PROOFSTEP]
convert inducedMap_mono γ β h
[GOAL]
case h.e'_3
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
src✝ : β →+*o γ := inducedOrderRingHom β γ
a✝ b✝ : β
h : ↑(inducedOrderRingHom β γ).toRingHom a✝ ≤ ↑(inducedOrderRingHom β γ).toRingHom b✝
⊢ a✝ = inducedMap γ β (↑(inducedOrderRingHom β γ).toRingHom a✝)
[PROOFSTEP]
rw [inducedOrderRingHom, AddMonoidHom.coe_fn_mkRingHomOfMulSelfOfTwoNeZero, inducedAddHom]
[GOAL]
case h.e'_3
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
src✝ : β →+*o γ := inducedOrderRingHom β γ
a✝ b✝ : β
h : ↑(inducedOrderRingHom β γ).toRingHom a✝ ≤ ↑(inducedOrderRingHom β γ).toRingHom b✝
⊢ a✝ =
    inducedMap γ β
      (↑{ toZeroHom := { toFun := inducedMap β γ, map_zero' := (_ : inducedMap β γ 0 = 0) },
            map_add' := (_ : ∀ (x y : β), inducedMap β γ (x + y) = inducedMap β γ x + inducedMap β γ y) }
        a✝)
[PROOFSTEP]
dsimp
[GOAL]
case h.e'_3
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
src✝ : β →+*o γ := inducedOrderRingHom β γ
a✝ b✝ : β
h : ↑(inducedOrderRingHom β γ).toRingHom a✝ ≤ ↑(inducedOrderRingHom β γ).toRingHom b✝
⊢ a✝ = inducedMap γ β (inducedMap β γ a✝)
[PROOFSTEP]
rw [inducedMap_inv_self β γ _]
[GOAL]
case h.e'_4
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
src✝ : β →+*o γ := inducedOrderRingHom β γ
a✝ b✝ : β
h : ↑(inducedOrderRingHom β γ).toRingHom a✝ ≤ ↑(inducedOrderRingHom β γ).toRingHom b✝
⊢ b✝ = inducedMap γ β (↑(inducedOrderRingHom β γ).toRingHom b✝)
[PROOFSTEP]
rw [inducedOrderRingHom, AddMonoidHom.coe_fn_mkRingHomOfMulSelfOfTwoNeZero, inducedAddHom]
[GOAL]
case h.e'_4
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
src✝ : β →+*o γ := inducedOrderRingHom β γ
a✝ b✝ : β
h : ↑(inducedOrderRingHom β γ).toRingHom a✝ ≤ ↑(inducedOrderRingHom β γ).toRingHom b✝
⊢ b✝ =
    inducedMap γ β
      (↑{ toZeroHom := { toFun := inducedMap β γ, map_zero' := (_ : inducedMap β γ 0 = 0) },
            map_add' := (_ : ∀ (x y : β), inducedMap β γ (x + y) = inducedMap β γ x + inducedMap β γ y) }
        b✝)
[PROOFSTEP]
dsimp
[GOAL]
case h.e'_4
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
src✝ : β →+*o γ := inducedOrderRingHom β γ
a✝ b✝ : β
h : ↑(inducedOrderRingHom β γ).toRingHom a✝ ≤ ↑(inducedOrderRingHom β γ).toRingHom b✝
⊢ b✝ = inducedMap γ β (inducedMap β γ b✝)
[PROOFSTEP]
rw [inducedMap_inv_self β γ _]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
R : Type u_5
S : Type u_6
inst✝¹ : OrderedRing R
inst✝ : LinearOrderedRing S
hR : ∀ (r : R), 0 ≤ r → ∃ s, s ^ 2 = r
f : R →+* S
r : R
h : 0 ≤ r
⊢ 0 ≤ ↑f r
[PROOFSTEP]
obtain ⟨s, rfl⟩ := hR r h
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
R : Type u_5
S : Type u_6
inst✝¹ : OrderedRing R
inst✝ : LinearOrderedRing S
hR : ∀ (r : R), 0 ≤ r → ∃ s, s ^ 2 = r
f : R →+* S
s : R
h : 0 ≤ s ^ 2
⊢ 0 ≤ ↑f (s ^ 2)
[PROOFSTEP]
rw [map_pow]
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
R : Type u_5
S : Type u_6
inst✝¹ : OrderedRing R
inst✝ : LinearOrderedRing S
hR : ∀ (r : R), 0 ≤ r → ∃ s, s ^ 2 = r
f : R →+* S
s : R
h : 0 ≤ s ^ 2
⊢ 0 ≤ ↑f s ^ 2
[PROOFSTEP]
apply sq_nonneg
