case inl
α : Type u_1
a b c d : α
inst✝³ : MulOneClass α
inst✝² : Zero α
inst✝¹ : LinearOrder α
inst✝ : PosMulStrictMono α
a0 : 0 < a
ha : a < 1
⊢ ∃ b, b * b ≤ a

case inr
α : Type u_1
a b c d : α
inst✝³ : MulOneClass α
inst✝² : Zero α
inst✝¹ : LinearOrder α
inst✝ : PosMulStrictMono α
a0 : 0 < a
ha : 1 ≤ a
⊢ ∃ b, b * b ≤ a
α : Type u_1
a b c d : α
inst✝³ : MulOneClass α
inst✝² : Zero α
inst✝¹ : LinearOrder α
inst✝ : PosMulStrictMono α
a0 : 0 < a
⊢ ∃ b, b * b ≤ a
obtain ha | ha := lt_or_le a 1
no goals
case inl
α : Type u_1
a b c d : α
inst✝³ : MulOneClass α
inst✝² : Zero α
inst✝¹ : LinearOrder α
inst✝ : PosMulStrictMono α
a0 : 0 < a
ha : a < 1
⊢ ∃ b, b * b ≤ a
exact ⟨a, (mul_lt_of_lt_one_right a0 ha).le⟩
no goals
case inr
α : Type u_1
a b c d : α
inst✝³ : MulOneClass α
inst✝² : Zero α
inst✝¹ : LinearOrder α
inst✝ : PosMulStrictMono α
a0 : 0 < a
ha : 1 ≤ a
⊢ ∃ b, b * b ≤ a
exact ⟨1, by rwa [mul_one]⟩
no goals
α : Type u_1
a b c d : α
inst✝³ : MulOneClass α
inst✝² : Zero α
inst✝¹ : LinearOrder α
inst✝ : PosMulStrictMono α
a0 : 0 < a
ha : 1 ≤ a
⊢ 1 * 1 ≤ a
rwa [mul_one]