case pos
α : Type u_1
β : Type ?u.59597
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a : α
h : a < 1
⊢ ∃ b, b * b ≤ a

case neg
α : Type u_1
β : Type ?u.59597
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a : α
h : ¬a < 1
⊢ ∃ b, b * b ≤ a
α : Type u_1
β : Type ?u.59597
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a : α
⊢ ∃ b, b * b ≤ a
by_cases h:a < 1
case pos
α : Type u_1
β : Type ?u.59597
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a : α
h : a < 1
⊢ a * a ≤ a
case pos
α : Type u_1
β : Type ?u.59597
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a : α
h : a < 1
⊢ ∃ b, b * b ≤ a
use a
case pos
α : Type u_1
β : Type ?u.59597
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a : α
h : a < 1
this : a * a < a * 1
⊢ a * a ≤ a
case pos
α : Type u_1
β : Type ?u.59597
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a : α
h : a < 1
⊢ a * a ≤ a
have : a * a < a * 1 := mul_lt_mul_left' h a
case pos
α : Type u_1
β : Type ?u.59597
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a : α
h : a < 1
this : a * a < a
⊢ a * a ≤ a
case pos
α : Type u_1
β : Type ?u.59597
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a : α
h : a < 1
this : a * a < a * 1
⊢ a * a ≤ a
rw [mul_one] at this
no goals
case pos
α : Type u_1
β : Type ?u.59597
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a : α
h : a < 1
this : a * a < a
⊢ a * a ≤ a
exact le_of_lt this
case neg
α : Type u_1
β : Type ?u.59597
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a : α
h : ¬a < 1
⊢ 1 * 1 ≤ a
case neg
α : Type u_1
β : Type ?u.59597
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a : α
h : ¬a < 1
⊢ ∃ b, b * b ≤ a
use 1
case neg
α : Type u_1
β : Type ?u.59597
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a : α
h : 1 ≤ a
⊢ 1 * 1 ≤ a
case neg
α : Type u_1
β : Type ?u.59597
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a : α
h : ¬a < 1
⊢ 1 * 1 ≤ a
push_neg  at h
no goals
case neg
α : Type u_1
β : Type ?u.59597
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a : α
h : 1 ≤ a
⊢ 1 * 1 ≤ a
rwa [mul_one]