English
If a > 0 and b is strictly less than (inducedMap α β a)^2, there exists c ∈ cutMap β (a^2) with b < c.
Русский
Пусть a > 0 и b строго меньше (inducedMap α β a)^2; тогда существует c ∈ cutMap β (a^2) такое, что b < c.
LaTeX
$$$ a > 0 \wedge b < (\mathrm{inducedMap} \alpha \beta a)^2 \Rightarrow \exists c \in cutMap \beta (a^2),\; b < c $$$
Lean4
/-- Preparatory lemma for `inducedOrderRingHom`. -/
theorem exists_mem_cutMap_mul_self_of_lt_inducedMap_mul_self (ha : 0 < a) (b : β)
(hba : b < inducedMap α β a * inducedMap α β a) : ∃ c ∈ cutMap β (a * a), b < c :=
by
obtain hb | hb := lt_or_ge b 0
· refine ⟨0, ?_, hb⟩
rw [← Rat.cast_zero, coe_mem_cutMap_iff, Rat.cast_zero]
exact mul_self_pos.2 ha.ne'
obtain ⟨q, hq, hbq, hqa⟩ := exists_rat_pow_btwn two_ne_zero hba (hb.trans_lt hba)
rw [← cast_pow] at hbq
refine ⟨(q ^ 2 : ℚ), coe_mem_cutMap_iff.2 ?_, hbq⟩
rw [pow_two] at hqa ⊢
push_cast
obtain ⟨q', hq', hqa'⟩ := lt_inducedMap_iff.1 (lt_of_mul_self_lt_mul_self₀ (inducedMap_nonneg ha.le) hqa)
exact mul_self_lt_mul_self (mod_cast hq.le) (hqa'.trans' <| by assumption_mod_cast)
