-- Mathlib/Algebra/Order/CompleteField.lean
theorem le_inducedMap_mul_self_of_mem_cutMap (ha : 0 < a) (b : β) (hb : b ∈ cutMap β (a * a)) :
    b ≤ inducedMap α β a * inducedMap α β a

Proof state:
case intro.intro
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
a : α
ha : 0 < a
q : ℚ
hb : q ∈ {t | ↑t < a * a}
⊢ ↑q ≤ inducedMap α β a * inducedMap α β a

Tactic:
obtain ⟨q', hq', hqq', hqa⟩ := exists_rat_pow_btwn two_ne_zero hb (mul_self_pos.2 ha.ne')

Result:
case intro.intro.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
a : α
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

Proof state:
case intro.intro.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
a : α
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

Tactic:
trans (q' : β) ^ 2

Result:
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
a : α
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

α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
a : α
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

Proof state:
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
a : α
ha : 0 < a
b : β
hb : b ∈ cutMap β (a * a)
⊢ b ≤ inducedMap α β a * inducedMap α β a

Tactic:
obtain ⟨q, hb, rfl⟩ := hb

Result:
case intro.intro
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
a : α
ha : 0 < a
q : ℚ
hb : q ∈ {t | ↑t < a * a}
⊢ ↑q ≤ inducedMap α β a * inducedMap α β a

Proof state:
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
a : α
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

Tactic:
exact mod_cast hqq'.le

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
a : α
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

Tactic:
exact mul_self_le_mul_self (mod_cast hq'.le)
  (le_csSup (cutMap_bddAbove β a) <|
    coe_mem_cutMap_iff.2 <| lt_of_mul_self_lt_mul_self₀ ha.le hqa)

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
a : α
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

Tactic:
rw [pow_two] at hqa ⊢

Result:
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
a : α
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