[GOAL]
α✝ α : Type u
inst✝ : OrderedCommGroup α
a b c : α
bc : a * b ≤ a * c
⊢ b ≤ c
[PROOFSTEP]
simpa using mul_le_mul_left' bc a⁻¹
[GOAL]
α✝ α : Type u
inst✝ : OrderedCommGroup α
a b c : α
bc : swap (fun x x_1 => x * x_1) a b ≤ swap (fun x x_1 => x * x_1) a c
⊢ b ≤ c
[PROOFSTEP]
simpa using mul_le_mul_right' bc a⁻¹
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
⊢ a⁻¹ ≤ 1 ↔ 1 ≤ a
[PROOFSTEP]
rw [← mul_le_mul_iff_left a]
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
⊢ a * a⁻¹ ≤ a * 1 ↔ 1 ≤ a
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
⊢ 1 ≤ a⁻¹ ↔ a ≤ 1
[PROOFSTEP]
rw [← mul_le_mul_iff_left a]
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
⊢ a * 1 ≤ a * a⁻¹ ↔ a ≤ 1
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
⊢ b ≤ a⁻¹ * c ↔ a * b ≤ c
[PROOFSTEP]
rw [← mul_le_mul_iff_left a]
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
⊢ a * b ≤ a * (a⁻¹ * c) ↔ a * b ≤ c
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
⊢ b⁻¹ * a ≤ c ↔ a ≤ b * c
[PROOFSTEP]
rw [← mul_le_mul_iff_left b, mul_inv_cancel_left]
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
⊢ a * a⁻¹ ≤ a * b ↔ 1 ≤ a * b
[PROOFSTEP]
rw [mul_inv_self]
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
⊢ b * a ≤ b * b⁻¹ ↔ b * a ≤ 1
[PROOFSTEP]
rw [mul_inv_self]
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
⊢ 1 ≤ b⁻¹ * a ↔ b ≤ a
[PROOFSTEP]
rw [← mul_le_mul_iff_left b, mul_one, mul_inv_cancel_left]
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
⊢ b ≤ a * 1 ↔ b ≤ a
[PROOFSTEP]
rw [mul_one]
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c : α
⊢ 1 < a⁻¹ ↔ a < 1
[PROOFSTEP]
rw [← mul_lt_mul_iff_left a, mul_inv_self, mul_one]
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c : α
⊢ a⁻¹ < 1 ↔ 1 < a
[PROOFSTEP]
rw [← mul_lt_mul_iff_left a, mul_inv_self, mul_one]
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c : α
⊢ b < a⁻¹ * c ↔ a * b < c
[PROOFSTEP]
rw [← mul_lt_mul_iff_left a]
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c : α
⊢ a * b < a * (a⁻¹ * c) ↔ a * b < c
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c : α
⊢ b⁻¹ * a < c ↔ a < b * c
[PROOFSTEP]
rw [← mul_lt_mul_iff_left b, mul_inv_cancel_left]
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c : α
⊢ a * a⁻¹ < a * b ↔ 1 < a * b
[PROOFSTEP]
rw [mul_inv_self]
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c : α
⊢ b * a < b * b⁻¹ ↔ b * a < 1
[PROOFSTEP]
rw [mul_inv_self]
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c : α
⊢ 1 < b⁻¹ * a ↔ b < a
[PROOFSTEP]
rw [← mul_lt_mul_iff_left b, mul_one, mul_inv_cancel_left]
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c : α
⊢ b < a * 1 ↔ b < a
[PROOFSTEP]
rw [mul_one]
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ a⁻¹ ≤ 1 ↔ 1 ≤ a
[PROOFSTEP]
rw [← mul_le_mul_iff_right a]
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ a⁻¹ * a ≤ 1 * a ↔ 1 ≤ a
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ 1 ≤ a⁻¹ ↔ a ≤ 1
[PROOFSTEP]
rw [← mul_le_mul_iff_right a]
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ 1 * a ≤ a⁻¹ * a ↔ a ≤ 1
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ a⁻¹ * a ≤ b * a ↔ 1 ≤ b * a
[PROOFSTEP]
rw [inv_mul_self]
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ a * b ≤ b⁻¹ * b ↔ a * b ≤ 1
[PROOFSTEP]
rw [inv_mul_self]
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ a * b⁻¹ * b ≤ c * b ↔ a ≤ c * b
[PROOFSTEP]
rw [inv_mul_cancel_right]
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ c * b ≤ a * b⁻¹ * b ↔ c * b ≤ a
[PROOFSTEP]
rw [inv_mul_cancel_right]
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ a ≤ 1 * b ↔ a ≤ b
[PROOFSTEP]
rw [one_mul]
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ 1 ≤ a * b⁻¹ ↔ b ≤ a
[PROOFSTEP]
rw [← mul_le_mul_iff_right b, one_mul, inv_mul_cancel_right]
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ b ≤ 1 * a ↔ b ≤ a
[PROOFSTEP]
rw [one_mul]
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c : α
⊢ a⁻¹ < 1 ↔ 1 < a
[PROOFSTEP]
rw [← mul_lt_mul_iff_right a, inv_mul_self, one_mul]
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c : α
⊢ 1 < a⁻¹ ↔ a < 1
[PROOFSTEP]
rw [← mul_lt_mul_iff_right a, inv_mul_self, one_mul]
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c : α
⊢ a⁻¹ * a < b * a ↔ 1 < b * a
[PROOFSTEP]
rw [inv_mul_self]
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c : α
⊢ a * b < b⁻¹ * b ↔ a * b < 1
[PROOFSTEP]
rw [inv_mul_self]
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c : α
⊢ a * b⁻¹ < c ↔ a < c * b
[PROOFSTEP]
rw [← mul_lt_mul_iff_right b, inv_mul_cancel_right]
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c : α
⊢ c * b < a * b⁻¹ * b ↔ c * b < a
[PROOFSTEP]
rw [inv_mul_cancel_right]
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c : α
⊢ a * b⁻¹ < 1 ↔ a < b
[PROOFSTEP]
rw [← mul_lt_mul_iff_right b, inv_mul_cancel_right, one_mul]
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c : α
⊢ 1 < a * b⁻¹ ↔ b < a
[PROOFSTEP]
rw [← mul_lt_mul_iff_right b, one_mul, inv_mul_cancel_right]
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c : α
⊢ b < 1 * a ↔ b < a
[PROOFSTEP]
rw [one_mul]
[GOAL]
α : Type u
inst✝³ : Group α
inst✝² : LE α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
⊢ a⁻¹ ≤ b⁻¹ ↔ b ≤ a
[PROOFSTEP]
rw [← mul_le_mul_iff_left a, ← mul_le_mul_iff_right b]
[GOAL]
α : Type u
inst✝³ : Group α
inst✝² : LE α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
⊢ a * a⁻¹ * b ≤ a * b⁻¹ * b ↔ b ≤ a
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝³ : Group α
inst✝² : LE α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
⊢ a * b⁻¹ ≤ d⁻¹ * c ↔ d * a ≤ c * b
[PROOFSTEP]
rw [← mul_le_mul_iff_left d, ← mul_le_mul_iff_right b, mul_inv_cancel_left, mul_assoc, inv_mul_cancel_right]
[GOAL]
α : Type u
inst✝³ : Group α
inst✝² : LE α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a✝ b✝ c d a b : α
⊢ a / b ≤ a ↔ 1 ≤ b
[PROOFSTEP]
simp [div_eq_mul_inv]
[GOAL]
α : Type u
inst✝³ : Group α
inst✝² : LE α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a✝ b✝ c d a b : α
⊢ a ≤ a / b ↔ b ≤ 1
[PROOFSTEP]
simp [div_eq_mul_inv]
[GOAL]
α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c d : α
⊢ a⁻¹ < b⁻¹ ↔ b < a
[PROOFSTEP]
rw [← mul_lt_mul_iff_left a, ← mul_lt_mul_iff_right b]
[GOAL]
α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c d : α
⊢ a * a⁻¹ * b < a * b⁻¹ * b ↔ b < a
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c d : α
⊢ a⁻¹ < b ↔ b⁻¹ < a
[PROOFSTEP]
rw [← inv_lt_inv_iff, inv_inv]
[GOAL]
α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c d : α
⊢ a < b⁻¹ ↔ b < a⁻¹
[PROOFSTEP]
rw [← inv_lt_inv_iff, inv_inv]
[GOAL]
α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c d : α
⊢ a * b⁻¹ < d⁻¹ * c ↔ d * a < c * b
[PROOFSTEP]
rw [← mul_lt_mul_iff_left d, ← mul_lt_mul_iff_right b, mul_inv_cancel_left, mul_assoc, inv_mul_cancel_right]
[GOAL]
α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a✝ b✝ c d a b : α
⊢ a / b < a ↔ 1 < b
[PROOFSTEP]
simp [div_eq_mul_inv]
[GOAL]
α : Type u
inst✝² : CommGroup α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
⊢ c⁻¹ * a ≤ b ↔ a ≤ b * c
[PROOFSTEP]
rw [inv_mul_le_iff_le_mul, mul_comm]
[GOAL]
α : Type u
inst✝² : CommGroup α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
⊢ a * b⁻¹ ≤ c ↔ a ≤ b * c
[PROOFSTEP]
rw [← inv_mul_le_iff_le_mul, mul_comm]
[GOAL]
α : Type u
inst✝² : CommGroup α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
⊢ a * b⁻¹ ≤ c * d⁻¹ ↔ a * d ≤ c * b
[PROOFSTEP]
rw [mul_comm c, mul_inv_le_inv_mul_iff, mul_comm]
[GOAL]
α : Type u
inst✝² : CommGroup α
inst✝¹ : LT α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c d : α
⊢ c⁻¹ * a < b ↔ a < b * c
[PROOFSTEP]
rw [inv_mul_lt_iff_lt_mul, mul_comm]
[GOAL]
α : Type u
inst✝² : CommGroup α
inst✝¹ : LT α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c d : α
⊢ a * b⁻¹ < c ↔ a < b * c
[PROOFSTEP]
rw [← inv_mul_lt_iff_lt_mul, mul_comm]
[GOAL]
α : Type u
inst✝² : CommGroup α
inst✝¹ : LT α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c d : α
⊢ a * b⁻¹ < c * d⁻¹ ↔ a * d < c * b
[PROOFSTEP]
rw [mul_comm c, mul_inv_lt_inv_mul_iff, mul_comm]
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c✝ d c : α
⊢ a / c ≤ b / c ↔ a ≤ b
[PROOFSTEP]
simpa only [div_eq_mul_inv] using mul_le_mul_iff_right _
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
⊢ 1 ≤ a / b ↔ b ≤ a
[PROOFSTEP]
rw [← mul_le_mul_iff_right b, one_mul, div_eq_mul_inv, inv_mul_cancel_right]
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
⊢ a / b ≤ 1 ↔ a ≤ b
[PROOFSTEP]
rw [← mul_le_mul_iff_right b, one_mul, div_eq_mul_inv, inv_mul_cancel_right]
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
⊢ a ≤ c / b ↔ a * b ≤ c
[PROOFSTEP]
rw [← mul_le_mul_iff_right b, div_eq_mul_inv, inv_mul_cancel_right]
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
⊢ a / c ≤ b ↔ a ≤ b * c
[PROOFSTEP]
rw [← mul_le_mul_iff_right c, div_eq_mul_inv, inv_mul_cancel_right]
[GOAL]
α : Type u
inst✝³ : Group α
inst✝² : LE α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a✝ b c a : α
⊢ a / b ≤ a / c ↔ c ≤ b
[PROOFSTEP]
rw [div_eq_mul_inv, div_eq_mul_inv, ← mul_le_mul_iff_left a⁻¹, inv_mul_cancel_left, inv_mul_cancel_left, inv_le_inv_iff]
[GOAL]
α : Type u
inst✝² : CommGroup α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
⊢ a / b ≤ c / d ↔ a * d ≤ c * b
[PROOFSTEP]
simpa only [div_eq_mul_inv] using mul_inv_le_mul_inv_iff'
[GOAL]
α : Type u
inst✝² : CommGroup α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
⊢ b ≤ c / a ↔ a * b ≤ c
[PROOFSTEP]
rw [le_div_iff_mul_le, mul_comm]
[GOAL]
α : Type u
inst✝² : CommGroup α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
⊢ a / b ≤ c ↔ a ≤ b * c
[PROOFSTEP]
rw [div_le_iff_le_mul, mul_comm]
[GOAL]
α : Type u
inst✝² : CommGroup α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
⊢ a⁻¹ ≤ b / c ↔ c ≤ a * b
[PROOFSTEP]
rw [inv_le_div_iff_le_mul, mul_comm]
[GOAL]
α : Type u
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
hab : a ≤ b
hcd : c ≤ d
⊢ a / d ≤ b / c
[PROOFSTEP]
rw [div_eq_mul_inv, div_eq_mul_inv, mul_comm b, mul_inv_le_inv_mul_iff, mul_comm]
[GOAL]
α : Type u
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
hab : a ≤ b
hcd : c ≤ d
⊢ a * c ≤ b * d
[PROOFSTEP]
exact mul_le_mul' hab hcd
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c✝ d c : α
⊢ a / c < b / c ↔ a < b
[PROOFSTEP]
simpa only [div_eq_mul_inv] using mul_lt_mul_iff_right _
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c d : α
⊢ 1 < a / b ↔ b < a
[PROOFSTEP]
rw [← mul_lt_mul_iff_right b, one_mul, div_eq_mul_inv, inv_mul_cancel_right]
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c d : α
⊢ a / b < 1 ↔ a < b
[PROOFSTEP]
rw [← mul_lt_mul_iff_right b, one_mul, div_eq_mul_inv, inv_mul_cancel_right]
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c d : α
⊢ a < c / b ↔ a * b < c
[PROOFSTEP]
rw [← mul_lt_mul_iff_right b, div_eq_mul_inv, inv_mul_cancel_right]
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c d : α
⊢ a / c < b ↔ a < b * c
[PROOFSTEP]
rw [← mul_lt_mul_iff_right c, div_eq_mul_inv, inv_mul_cancel_right]
[GOAL]
α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a✝ b c a : α
⊢ a / b < a / c ↔ c < b
[PROOFSTEP]
rw [div_eq_mul_inv, div_eq_mul_inv, ← mul_lt_mul_iff_left a⁻¹, inv_mul_cancel_left, inv_mul_cancel_left, inv_lt_inv_iff]
[GOAL]
α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c : α
⊢ a⁻¹ < b / c ↔ c < a * b
[PROOFSTEP]
rw [div_eq_mul_inv, lt_mul_inv_iff_mul_lt, inv_mul_lt_iff_lt_mul]
[GOAL]
α : Type u
inst✝² : CommGroup α
inst✝¹ : LT α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c d : α
⊢ a / b < c / d ↔ a * d < c * b
[PROOFSTEP]
simpa only [div_eq_mul_inv] using mul_inv_lt_mul_inv_iff'
[GOAL]
α : Type u
inst✝² : CommGroup α
inst✝¹ : LT α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c d : α
⊢ b < c / a ↔ a * b < c
[PROOFSTEP]
rw [lt_div_iff_mul_lt, mul_comm]
[GOAL]
α : Type u
inst✝² : CommGroup α
inst✝¹ : LT α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c d : α
⊢ a / b < c ↔ a < b * c
[PROOFSTEP]
rw [div_lt_iff_lt_mul, mul_comm]
[GOAL]
α : Type u
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c d : α
hab : a < b
hcd : c < d
⊢ a / d < b / c
[PROOFSTEP]
rw [div_eq_mul_inv, div_eq_mul_inv, mul_comm b, mul_inv_lt_inv_mul_iff, mul_comm]
[GOAL]
α : Type u
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c d : α
hab : a < b
hcd : c < d
⊢ a * c < b * d
[PROOFSTEP]
exact mul_lt_mul_of_lt_of_lt hab hcd
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ cmp (a / b) 1 = cmp a b
[PROOFSTEP]
rw [← cmp_mul_right' _ _ b, one_mul, div_mul_cancel']
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
h : ∀ (ε : α), 1 < ε → a < b * ε
h₁ : b < a
⊢ a < a
[PROOFSTEP]
simpa using h _ (lt_inv_mul_iff_lt.mpr h₁)
[GOAL]
α : Type u
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
⊢ a / b ≤ a⁻¹ * b ↔ a ≤ b
[PROOFSTEP]
rw [div_eq_mul_inv, mul_inv_le_inv_mul_iff]
[GOAL]
α : Type u
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
⊢ a * a ≤ b * b ↔ a ≤ b
[PROOFSTEP]
exact ⟨fun h => not_lt.mp fun k => not_lt.mpr h (mul_lt_mul_of_lt_of_lt k k), fun h => mul_le_mul' h h⟩
[GOAL]
α✝ : Type u
inst✝⁵ : Group α✝
inst✝⁴ : LinearOrder α✝
inst✝³ : CovariantClass α✝ α✝ (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a✝ b✝ c : α✝
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a / b ≤ b / a ↔ a ≤ b
[PROOFSTEP]
rw [div_eq_mul_inv b, mul_comm]
[GOAL]
α✝ : Type u
inst✝⁵ : Group α✝
inst✝⁴ : LinearOrder α✝
inst✝³ : CovariantClass α✝ α✝ (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a✝ b✝ c : α✝
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a / b ≤ a⁻¹ * b ↔ a ≤ b
[PROOFSTEP]
exact div_le_inv_mul_iff
[GOAL]
α : Type u
inst✝¹ : LinearOrderedCommGroup α
a b c : α
inst✝ : Nontrivial α
⊢ ∃ a, 1 < a
[PROOFSTEP]
obtain ⟨y, hy⟩ := Decidable.exists_ne (1 : α)
[GOAL]
case intro
α : Type u
inst✝¹ : LinearOrderedCommGroup α
a b c : α
inst✝ : Nontrivial α
y : α
hy : y ≠ 1
⊢ ∃ a, 1 < a
[PROOFSTEP]
obtain h | h := hy.lt_or_lt
[GOAL]
case intro.inl
α : Type u
inst✝¹ : LinearOrderedCommGroup α
a b c : α
inst✝ : Nontrivial α
y : α
hy : y ≠ 1
h : y < 1
⊢ ∃ a, 1 < a
[PROOFSTEP]
exact ⟨y⁻¹, one_lt_inv'.mpr h⟩
[GOAL]
case intro.inr
α : Type u
inst✝¹ : LinearOrderedCommGroup α
a b c : α
inst✝ : Nontrivial α
y : α
hy : y ≠ 1
h : 1 < y
⊢ ∃ a, 1 < a
[PROOFSTEP]
exact ⟨y, h⟩
[GOAL]
α : Type u
inst✝¹ : LinearOrderedCommGroup α
a b c : α
inst✝ : Nontrivial α
⊢ ∀ (a : α), ∃ b, a < b
[PROOFSTEP]
obtain ⟨y, hy⟩ : ∃ a : α, 1 < a := exists_one_lt'
[GOAL]
case intro
α : Type u
inst✝¹ : LinearOrderedCommGroup α
a b c : α
inst✝ : Nontrivial α
y : α
hy : 1 < y
⊢ ∀ (a : α), ∃ b, a < b
[PROOFSTEP]
exact fun a => ⟨a * y, lt_mul_of_one_lt_right' a hy⟩
[GOAL]
α : Type u
inst✝¹ : LinearOrderedCommGroup α
a b c : α
inst✝ : Nontrivial α
⊢ ∀ (a : α), ∃ b, b < a
[PROOFSTEP]
obtain ⟨y, hy⟩ : ∃ a : α, 1 < a := exists_one_lt'
[GOAL]
case intro
α : Type u
inst✝¹ : LinearOrderedCommGroup α
a b c : α
inst✝ : Nontrivial α
y : α
hy : 1 < y
⊢ ∀ (a : α), ∃ b, b < a
[PROOFSTEP]
exact fun a => ⟨a / y, (div_lt_self_iff a).mpr hy⟩
[GOAL]
α✝ : Type u
α : Type u_1
inst✝ : AddCommGroup α
C : PositiveCone α
src✝ : AddCommGroup α := inst✝
a : α
⊢ a ≤ a
[PROOFSTEP]
simp [C.zero_nonneg]
[GOAL]
α✝ : Type u
α : Type u_1
inst✝ : AddCommGroup α
C : PositiveCone α
src✝ : AddCommGroup α := inst✝
a b c : α
nab : a ≤ b
nbc : b ≤ c
⊢ a ≤ c
[PROOFSTEP]
simpa [← sub_add_sub_cancel] using C.add_nonneg nbc nab
[GOAL]
α✝ : Type u
α : Type u_1
inst✝ : AddCommGroup α
C : PositiveCone α
src✝ : AddCommGroup α := inst✝
a b : α
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a
[PROOFSTEP]
simp [C.pos_iff]
[GOAL]
α✝ : Type u
α : Type u_1
inst✝ : AddCommGroup α
C : PositiveCone α
src✝ : AddCommGroup α := inst✝
a b : α
nab : a ≤ b
nba : b ≤ a
⊢ PositiveCone.nonneg C (-(a - b))
[PROOFSTEP]
rwa [neg_sub]
[GOAL]
α✝ : Type u
α : Type u_1
inst✝ : AddCommGroup α
C : PositiveCone α
src✝ : AddCommGroup α := inst✝
a b : α
nab : a ≤ b
c : α
⊢ c + a ≤ c + b
[PROOFSTEP]
simpa using nab
[GOAL]
α✝ : Type u
α : Type u_1
inst✝ : AddCommGroup α
C : TotalPositiveCone α
src✝ : OrderedAddCommGroup α := OrderedAddCommGroup.mkOfPositiveCone C.toPositiveCone
a b : α
⊢ a ≤ b ∨ b ≤ a
[PROOFSTEP]
simpa [neg_sub] using C.nonneg_total (b - a)


[GOAL]
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 1 ≤ a
h : m ≤ n
⊢ a ^ m ≤ a ^ n
[PROOFSTEP]
have ha₀ : 0 < a := one_pos.trans_le ha
[GOAL]
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 1 ≤ a
h : m ≤ n
ha₀ : 0 < a
⊢ a ^ m ≤ a ^ n
[PROOFSTEP]
lift n - m to ℕ using sub_nonneg.2 h with k hk
[GOAL]
case intro
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 1 ≤ a
h : m ≤ n
ha₀ : 0 < a
k : ℕ
hk : ↑k = n - m
⊢ a ^ m ≤ a ^ n
[PROOFSTEP]
calc
  a ^ m = a ^ m * 1 := (mul_one _).symm
  _ ≤ a ^ m * a ^ k := (mul_le_mul_of_nonneg_left (one_le_pow_of_one_le ha _) (zpow_nonneg ha₀.le _))
  _ = a ^ n := by rw [← zpow_ofNat, ← zpow_add₀ ha₀.ne', hk, add_sub_cancel'_right]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 1 ≤ a
h : m ≤ n
ha₀ : 0 < a
k : ℕ
hk : ↑k = n - m
⊢ a ^ m * a ^ k = a ^ n
[PROOFSTEP]
rw [← zpow_ofNat, ← zpow_add₀ ha₀.ne', hk, add_sub_cancel'_right]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedSemifield α
a✝ b c d e : α
m n✝ : ℤ
a : ℕ
h : 0 < a
n : ℤ
⊢ 0 < ↑a ^ n
[PROOFSTEP]
apply zpow_pos_of_pos
[GOAL]
case ha
α : Type u_1
inst✝ : LinearOrderedSemifield α
a✝ b c d e : α
m n✝ : ℤ
a : ℕ
h : 0 < a
n : ℤ
⊢ 0 < ↑a
[PROOFSTEP]
exact_mod_cast h
[GOAL]
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
h₀ : 0 < a
h₁ : a ≠ 1
⊢ Injective ((fun x x_1 => x ^ x_1) a)
[PROOFSTEP]
rcases h₁.lt_or_lt with (H | H)
[GOAL]
case inl
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
h₀ : 0 < a
h₁ : a ≠ 1
H : a < 1
⊢ Injective ((fun x x_1 => x ^ x_1) a)
[PROOFSTEP]
exact (zpow_strictAnti h₀ H).injective
[GOAL]
case inr
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
h₀ : 0 < a
h₁ : a ≠ 1
H : 1 < a
⊢ Injective ((fun x x_1 => x ^ x_1) a)
[PROOFSTEP]
exact (zpow_strictMono H).injective
[GOAL]
α : Type u_1
inst✝ : LinearOrderedSemifield α
a✝ b✝ c✝ d e : α
m n : ℤ
x : α
hx : 1 < x
a b c : ℤ
⊢ x ^ (-c) ≤ max (x ^ (-a)) (x ^ (-b)) ↔ min a b ≤ c
[PROOFSTEP]
simp_rw [le_max_iff, min_le_iff, zpow_le_iff_le hx, neg_le_neg_iff]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ b c d : α
n : ℤ
a : α
⊢ 0 ≤ a ^ 2
[PROOFSTEP]
convert zpow_bit0_nonneg a 1
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
h : a ≠ 0
⊢ 0 < a ^ 2
[PROOFSTEP]
convert zpow_bit0_pos h 1
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hn : n ≠ 0
⊢ 0 < a ^ bit0 n → a ≠ 0
[PROOFSTEP]
rintro h rfl
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
b c d : α
n : ℤ
hn : n ≠ 0
h : 0 < 0 ^ bit0 n
⊢ False
[PROOFSTEP]
refine' (zero_zpow _ _).not_gt h
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
b c d : α
n : ℤ
hn : n ≠ 0
h : 0 < 0 ^ bit0 n
⊢ bit0 n ≠ 0
[PROOFSTEP]
rwa [bit0_ne_zero]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
h : a < 0
⊢ a ^ bit1 n < 0
[PROOFSTEP]
rw [bit1, zpow_add_one₀ h.ne]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
h : a < 0
⊢ a ^ bit0 n * a < 0
[PROOFSTEP]
exact mul_neg_of_pos_of_neg (zpow_bit0_pos h.ne _) h
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
⊢ a ^ bit1 n ≤ 0 ↔ a ≤ 0
[PROOFSTEP]
rw [le_iff_lt_or_eq, le_iff_lt_or_eq, zpow_bit1_neg_iff, zpow_eq_zero_iff (Int.bit1_ne_zero n)]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ b c d : α
n : ℤ
hn : Even n
a : α
⊢ 0 ≤ a ^ n
[PROOFSTEP]
obtain ⟨k, rfl⟩ := hn
[GOAL]
case intro
α : Type u_1
inst✝ : LinearOrderedField α
a✝ b c d a : α
k : ℤ
⊢ 0 ≤ a ^ (k + k)
[PROOFSTEP]
exact zpow_bit0_nonneg _ _
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hn : Even n
h : n ≠ 0
⊢ 0 < a ^ n ↔ a ≠ 0
[PROOFSTEP]
obtain ⟨k, rfl⟩ := hn
[GOAL]
case intro
α : Type u_1
inst✝ : LinearOrderedField α
a b c d : α
k : ℤ
h : k + k ≠ 0
⊢ 0 < a ^ (k + k) ↔ a ≠ 0
[PROOFSTEP]
exact zpow_bit0_pos_iff (by rintro rfl; simp at h )
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a b c d : α
k : ℤ
h : k + k ≠ 0
⊢ k ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a b c d : α
h : 0 + 0 ≠ 0
⊢ False
[PROOFSTEP]
simp at h
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hn : Odd n
⊢ a ^ n < 0 ↔ a < 0
[PROOFSTEP]
cases' hn with k hk
[GOAL]
case intro
α : Type u_1
inst✝ : LinearOrderedField α
a b c d : α
n k : ℤ
hk : n = 2 * k + 1
⊢ a ^ n < 0 ↔ a < 0
[PROOFSTEP]
simpa only [hk, two_mul] using zpow_bit1_neg_iff
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hn : Odd n
⊢ 0 ≤ a ^ n ↔ 0 ≤ a
[PROOFSTEP]
cases' hn with k hk
[GOAL]
case intro
α : Type u_1
inst✝ : LinearOrderedField α
a b c d : α
n k : ℤ
hk : n = 2 * k + 1
⊢ 0 ≤ a ^ n ↔ 0 ≤ a
[PROOFSTEP]
simpa only [hk, two_mul] using zpow_bit1_nonneg_iff
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hn : Odd n
⊢ a ^ n ≤ 0 ↔ a ≤ 0
[PROOFSTEP]
cases' hn with k hk
[GOAL]
case intro
α : Type u_1
inst✝ : LinearOrderedField α
a b c d : α
n k : ℤ
hk : n = 2 * k + 1
⊢ a ^ n ≤ 0 ↔ a ≤ 0
[PROOFSTEP]
simpa only [hk, two_mul] using zpow_bit1_nonpos_iff
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hn : Odd n
⊢ 0 < a ^ n ↔ 0 < a
[PROOFSTEP]
cases' hn with k hk
[GOAL]
case intro
α : Type u_1
inst✝ : LinearOrderedField α
a b c d : α
n k : ℤ
hk : n = 2 * k + 1
⊢ 0 < a ^ n ↔ 0 < a
[PROOFSTEP]
simpa only [hk, two_mul] using zpow_bit1_pos_iff
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ b c d : α
n p : ℤ
hp : Even p
a : α
⊢ |a| ^ p = a ^ p
[PROOFSTEP]
cases' abs_choice a with h h
[GOAL]
case inl
α : Type u_1
inst✝ : LinearOrderedField α
a✝ b c d : α
n p : ℤ
hp : Even p
a : α
h : |a| = a
⊢ |a| ^ p = a ^ p
[PROOFSTEP]
simp only [h, hp.neg_zpow _]
[GOAL]
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a✝ b c d : α
n p : ℤ
hp : Even p
a : α
h : |a| = -a
⊢ |a| ^ p = a ^ p
[PROOFSTEP]
simp only [h, hp.neg_zpow _]


[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommSemigroup β
f : α → β
n m : α
⊢ f (min n m) * f (max n m) = f n * f m
[PROOFSTEP]
cases' le_total n m with h h
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommSemigroup β
f : α → β
n m : α
h : n ≤ m
⊢ f (min n m) * f (max n m) = f n * f m
[PROOFSTEP]
simp [h, mul_comm]
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommSemigroup β
f : α → β
n m : α
h : m ≤ n
⊢ f (min n m) * f (max n m) = f n * f m
[PROOFSTEP]
simp [h, mul_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : Mul α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a₁ a₂ b₁ b₂ : α
⊢ a₁ * b₁ < a₂ * b₂ → a₁ < a₂ ∨ b₁ < b₂
[PROOFSTEP]
contrapose!
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : Mul α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a₁ a₂ b₁ b₂ : α
⊢ a₂ ≤ a₁ ∧ b₂ ≤ b₁ → a₂ * b₂ ≤ a₁ * b₁
[PROOFSTEP]
exact fun h => mul_le_mul' h.1 h.2
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : Mul α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a₁ a₂ b₁ b₂ : α
⊢ a₁ * b₁ ≤ a₂ * b₂ → a₁ ≤ a₂ ∨ b₁ < b₂
[PROOFSTEP]
contrapose!
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : Mul α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a₁ a₂ b₁ b₂ : α
⊢ a₂ < a₁ ∧ b₂ ≤ b₁ → a₂ * b₂ < a₁ * b₁
[PROOFSTEP]
exact fun h => mul_lt_mul_of_lt_of_le h.1 h.2
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : Mul α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a₁ a₂ b₁ b₂ : α
⊢ a₁ * b₁ ≤ a₂ * b₂ → a₁ < a₂ ∨ b₁ ≤ b₂
[PROOFSTEP]
contrapose!
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : Mul α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a₁ a₂ b₁ b₂ : α
⊢ a₂ ≤ a₁ ∧ b₂ < b₁ → a₂ * b₂ < a₁ * b₁
[PROOFSTEP]
exact fun h => mul_lt_mul_of_le_of_lt h.1 h.2
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : Mul α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a₁ a₂ b₁ b₂ : α
⊢ a₁ * b₁ ≤ a₂ * b₂ → a₁ ≤ a₂ ∨ b₁ ≤ b₂
[PROOFSTEP]
contrapose!
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : Mul α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a₁ a₂ b₁ b₂ : α
⊢ a₂ < a₁ ∧ b₂ < b₁ → a₂ * b₂ < a₁ * b₁
[PROOFSTEP]
exact fun h => mul_lt_mul_of_lt_of_lt h.1 h.2
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : Mul α
inst✝³ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝² : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
⊢ a₁ * b₁ < a₂ * b₂ ↔ a₁ < a₂ ∨ b₁ < b₂
[PROOFSTEP]
refine' ⟨lt_or_lt_of_mul_lt_mul, fun h => _⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : Mul α
inst✝³ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝² : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
h : a₁ < a₂ ∨ b₁ < b₂
⊢ a₁ * b₁ < a₂ * b₂
[PROOFSTEP]
cases' h with ha' hb'
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : Mul α
inst✝³ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝² : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
ha' : a₁ < a₂
⊢ a₁ * b₁ < a₂ * b₂
[PROOFSTEP]
exact mul_lt_mul_of_lt_of_le ha' hb
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : Mul α
inst✝³ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝² : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
hb' : b₁ < b₂
⊢ a₁ * b₁ < a₂ * b₂
[PROOFSTEP]
exact mul_lt_mul_of_le_of_lt ha hb'


[GOAL]
α : Type u
β✝ : Type u_1
inst✝³ : OrderedCommMonoid α
β : Type u_2
inst✝² : One β
inst✝¹ : Mul β
inst✝ : Pow β ℕ
f : β → α
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : β), f (x * y) = f x * f y
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
src✝¹ : PartialOrder β := PartialOrder.lift f hf
src✝ : CommMonoid β := Injective.commMonoid f hf one mul npow
a b : β
ab : a ≤ b
c : β
⊢ f (c * a) ≤ f (c * b)
[PROOFSTEP]
rw [mul, mul]
[GOAL]
α : Type u
β✝ : Type u_1
inst✝³ : OrderedCommMonoid α
β : Type u_2
inst✝² : One β
inst✝¹ : Mul β
inst✝ : Pow β ℕ
f : β → α
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : β), f (x * y) = f x * f y
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
src✝¹ : PartialOrder β := PartialOrder.lift f hf
src✝ : CommMonoid β := Injective.commMonoid f hf one mul npow
a b : β
ab : a ≤ b
c : β
⊢ f c * f a ≤ f c * f b
[PROOFSTEP]
apply mul_le_mul_left'
[GOAL]
case bc
α : Type u
β✝ : Type u_1
inst✝³ : OrderedCommMonoid α
β : Type u_2
inst✝² : One β
inst✝¹ : Mul β
inst✝ : Pow β ℕ
f : β → α
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : β), f (x * y) = f x * f y
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
src✝¹ : PartialOrder β := PartialOrder.lift f hf
src✝ : CommMonoid β := Injective.commMonoid f hf one mul npow
a b : β
ab : a ≤ b
c : β
⊢ f a ≤ f b
[PROOFSTEP]
exact ab
[GOAL]
α : Type u
β : Type u_1
inst✝⁴ : Mul α
inst✝³ : LinearOrder α
inst✝² : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b a0 b0 : α
ha : a0 ≤ a
hb : b0 ≤ b
ab : a * b ≤ a0 * b0
⊢ a = a0 ∧ b = b0
[PROOFSTEP]
haveI := Mul.to_covariantClass_right α
[GOAL]
α : Type u
β : Type u_1
inst✝⁴ : Mul α
inst✝³ : LinearOrder α
inst✝² : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b a0 b0 : α
ha : a0 ≤ a
hb : b0 ≤ b
ab : a * b ≤ a0 * b0
this : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
⊢ a = a0 ∧ b = b0
[PROOFSTEP]
have ha' : ¬a0 * b0 < a * b → ¬a0 < a := mt (mul_lt_mul_of_lt_of_le · hb)
[GOAL]
α : Type u
β : Type u_1
inst✝⁴ : Mul α
inst✝³ : LinearOrder α
inst✝² : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b a0 b0 : α
ha : a0 ≤ a
hb : b0 ≤ b
ab : a * b ≤ a0 * b0
this : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
ha' : ¬a0 * b0 < a * b → ¬a0 < a
⊢ a = a0 ∧ b = b0
[PROOFSTEP]
have hb' : ¬a0 * b0 < a * b → ¬b0 < b := mt (mul_lt_mul_of_le_of_lt ha ·)
[GOAL]
α : Type u
β : Type u_1
inst✝⁴ : Mul α
inst✝³ : LinearOrder α
inst✝² : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b a0 b0 : α
ha : a0 ≤ a
hb : b0 ≤ b
ab : a * b ≤ a0 * b0
this : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
ha' : ¬a0 * b0 < a * b → ¬a0 < a
hb' : ¬a0 * b0 < a * b → ¬b0 < b
⊢ a = a0 ∧ b = b0
[PROOFSTEP]
push_neg at ha' hb'
[GOAL]
α : Type u
β : Type u_1
inst✝⁴ : Mul α
inst✝³ : LinearOrder α
inst✝² : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b a0 b0 : α
ha : a0 ≤ a
hb : b0 ≤ b
ab : a * b ≤ a0 * b0
this : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
ha' : a * b ≤ a0 * b0 → a ≤ a0
hb' : a * b ≤ a0 * b0 → b ≤ b0
⊢ a = a0 ∧ b = b0
[PROOFSTEP]
exact ⟨ha.antisymm' (ha' ab), hb.antisymm' (hb' ab)⟩