[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
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
h : a * b ≤ c * d
⊢ min a b ≤ max c d
[PROOFSTEP]
simp_rw [min_le_iff, le_max_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
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
h : a * b ≤ c * d
⊢ (a ≤ c ∨ a ≤ d) ∨ b ≤ c ∨ b ≤ d
[PROOFSTEP]
contrapose! h
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
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
h : (c < a ∧ d < a) ∧ c < b ∧ d < b
⊢ c * d < a * b
[PROOFSTEP]
exact mul_lt_mul_of_lt_of_lt h.1.1 h.2.2
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : MulOneClass α
inst✝¹ : LE α
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
h : a ≤ a * b
⊢ ?m.15077 h * 1 ≤ ?m.15077 h * b
[PROOFSTEP]
simpa only [mul_one]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : MulOneClass α
inst✝¹ : LE α
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
h : a * b ≤ a
⊢ ?m.15584 h * b ≤ ?m.15584 h * 1
[PROOFSTEP]
simpa only [mul_one]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : MulOneClass α
inst✝¹ : LE α
inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
h : b ≤ a * b
⊢ 1 * ?m.16128 h ≤ a * ?m.16128 h
[PROOFSTEP]
simpa only [one_mul]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : MulOneClass α
inst✝¹ : LE α
inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
h : a * b ≤ b
⊢ a * ?m.16669 h ≤ 1 * ?m.16669 h
[PROOFSTEP]
simpa only [one_mul]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : MulOneClass α
inst✝² : LE α
inst✝¹ : CovariantClass α α (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 : α
⊢ a ≤ a * b ↔ a * 1 ≤ a * b
[PROOFSTEP]
rw [mul_one]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : MulOneClass α
inst✝² : LE α
inst✝¹ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a ≤ b * a ↔ 1 * a ≤ b * a
[PROOFSTEP]
rw [one_mul]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : MulOneClass α
inst✝² : LE α
inst✝¹ : CovariantClass α α (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 : α
⊢ a * b ≤ a ↔ a * b ≤ a * 1
[PROOFSTEP]
rw [mul_one]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : MulOneClass α
inst✝² : LE α
inst✝¹ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a * b ≤ b ↔ a * b ≤ 1 * b
[PROOFSTEP]
rw [one_mul]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : MulOneClass α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b : α
h : a < a * b
⊢ ?m.21985 h * 1 < ?m.21985 h * b
[PROOFSTEP]
simpa only [mul_one]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : MulOneClass α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b : α
h : a * b < a
⊢ ?m.22488 h * b < ?m.22488 h * 1
[PROOFSTEP]
simpa only [mul_one]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : MulOneClass α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b : α
h : b < a * b
⊢ 1 * ?m.23024 h < a * ?m.23024 h
[PROOFSTEP]
simpa only [one_mul]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : MulOneClass α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b : α
h : a * b < b
⊢ a * ?m.23557 h < 1 * ?m.23557 h
[PROOFSTEP]
simpa only [one_mul]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : MulOneClass α
inst✝² : LT α
inst✝¹ : CovariantClass α α (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 : α
⊢ a < a * b ↔ a * 1 < a * b
[PROOFSTEP]
rw [mul_one]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : MulOneClass α
inst✝² : LT α
inst✝¹ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b : α
⊢ a < b * a ↔ 1 * a < b * a
[PROOFSTEP]
rw [one_mul]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : MulOneClass α
inst✝² : LT α
inst✝¹ : CovariantClass α α (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 : α
⊢ a * b < a ↔ a * b < a * 1
[PROOFSTEP]
rw [mul_one]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : MulOneClass α
inst✝² : LT α
inst✝¹ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b : α
⊢ a * b < b ↔ a * b < 1 * b
[PROOFSTEP]
rw [one_mul]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
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 : α
ha : 1 ≤ a
hb : 1 ≤ b
⊢ a = 1 ∧ b = 1 → a * b = 1
[PROOFSTEP]
rintro ⟨rfl, rfl⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
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
ha hb : 1 ≤ 1
⊢ 1 * 1 = 1
[PROOFSTEP]
rw [mul_one]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : MulOneClass α
inst✝⁴ : PartialOrder α
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' ⟨fun h ↦ _, by rintro ⟨rfl, rfl⟩; rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : MulOneClass α
inst✝⁴ : PartialOrder α
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₁ = a₂ ∧ b₁ = b₂ → a₂ * b₂ ≤ a₁ * b₁
[PROOFSTEP]
rintro ⟨rfl, rfl⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝⁵ : MulOneClass α
inst✝⁴ : PartialOrder α
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₁ b₁ : α
ha : a₁ ≤ a₁
hb : b₁ ≤ b₁
⊢ a₁ * b₁ ≤ a₁ * b₁
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : MulOneClass α
inst✝⁴ : PartialOrder α
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₂ * b₂ ≤ a₁ * b₁
⊢ a₁ = a₂ ∧ b₁ = b₂
[PROOFSTEP]
simp only [eq_iff_le_not_lt, ha, hb, true_and]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : MulOneClass α
inst✝⁴ : PartialOrder α
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₂ * b₂ ≤ a₁ * b₁
⊢ ¬a₁ < a₂ ∧ ¬b₁ < b₂
[PROOFSTEP]
refine' ⟨fun ha ↦ h.not_lt _, fun hb ↦ h.not_lt _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝⁵ : MulOneClass α
inst✝⁴ : PartialOrder α
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₂ * b₂ ≤ a₁ * b₁
ha : a₁ < a₂
⊢ a₁ * b₁ < a₂ * b₂
case refine'_2
α : Type u_1
β : Type u_2
inst✝⁵ : MulOneClass α
inst✝⁴ : PartialOrder α
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₂ * b₂ ≤ a₁ * b₁
hb : b₁ < b₂
⊢ a₁ * b₁ < a₂ * b₂
[PROOFSTEP]
{exact mul_lt_mul_of_lt_of_le ha hb
}
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝⁵ : MulOneClass α
inst✝⁴ : PartialOrder α
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₂ * b₂ ≤ a₁ * b₁
ha : a₁ < a₂
⊢ a₁ * b₁ < a₂ * b₂
[PROOFSTEP]
exact mul_lt_mul_of_lt_of_le ha hb
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝⁵ : MulOneClass α
inst✝⁴ : PartialOrder α
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₂ * b₂ ≤ a₁ * b₁
hb : b₁ < b₂
⊢ a₁ * b₁ < a₂ * b₂
[PROOFSTEP]
{exact mul_lt_mul_of_le_of_lt ha hb
}
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝⁵ : MulOneClass α
inst✝⁴ : PartialOrder α
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₂ * b₂ ≤ a₁ * b₁
hb : b₁ < b₂
⊢ a₁ * b₁ < a₂ * b₂
[PROOFSTEP]
exact mul_lt_mul_of_le_of_lt ha hb
[GOAL]
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
by_cases h : a < 1
[GOAL]
case pos
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
use a
[GOAL]
case h
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
have : a * a < a * 1 := mul_lt_mul_left' h a
[GOAL]
case h
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
rw [mul_one] at this
[GOAL]
case h
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
exact le_of_lt this
[GOAL]
case neg
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
use 1
[GOAL]
case h
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
push_neg at h
[GOAL]
case h
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
rwa [mul_one]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : Semigroup α
inst✝⁴ : PartialOrder α
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
inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
hac : a ≤ c
hbd : b ≤ d
⊢ a * b = c * d ↔ a = c ∧ b = d
[PROOFSTEP]
refine' ⟨fun h => _, fun h => congr_arg₂ (· * ·) h.1 h.2⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : Semigroup α
inst✝⁴ : PartialOrder α
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
inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
hac : a ≤ c
hbd : b ≤ d
h : a * b = c * d
⊢ a = c ∧ b = d
[PROOFSTEP]
rcases hac.eq_or_lt with (rfl | hac)
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝⁵ : Semigroup α
inst✝⁴ : PartialOrder α
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
inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b d : α
hbd : b ≤ d
hac : a ≤ a
h : a * b = a * d
⊢ a = a ∧ b = d
[PROOFSTEP]
exact ⟨rfl, mul_left_cancel'' h⟩
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝⁵ : Semigroup α
inst✝⁴ : PartialOrder α
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
inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
hac✝ : a ≤ c
hbd : b ≤ d
h : a * b = c * d
hac : a < c
⊢ a = c ∧ b = d
[PROOFSTEP]
rcases eq_or_lt_of_le hbd with (rfl | hbd)
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
inst✝⁵ : Semigroup α
inst✝⁴ : PartialOrder α
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
inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
hac✝ : a ≤ c
hac : a < c
hbd : b ≤ b
h : a * b = c * b
⊢ a = c ∧ b = b
[PROOFSTEP]
exact ⟨mul_right_cancel'' h, rfl⟩
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝⁵ : Semigroup α
inst✝⁴ : PartialOrder α
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
inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
hac✝ : a ≤ c
hbd✝ : b ≤ d
h : a * b = c * d
hac : a < c
hbd : b < d
⊢ a = c ∧ b = d
[PROOFSTEP]
exact ((Left.mul_lt_mul hac hbd).ne h).elim
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : Semigroup α
inst✝⁴ : PartialOrder α
inst✝³ : CovariantClass α α (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
inst✝¹ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
hac : a ≤ c
hbd : b ≤ d
⊢ a * b = c * d ↔ a = c ∧ b = d
[PROOFSTEP]
refine' ⟨fun h => _, fun h => congr_arg₂ (· * ·) h.1 h.2⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : Semigroup α
inst✝⁴ : PartialOrder α
inst✝³ : CovariantClass α α (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
inst✝¹ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
hac : a ≤ c
hbd : b ≤ d
h : a * b = c * d
⊢ a = c ∧ b = d
[PROOFSTEP]
rcases hac.eq_or_lt with (rfl | hac)
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝⁵ : Semigroup α
inst✝⁴ : PartialOrder α
inst✝³ : CovariantClass α α (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
inst✝¹ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b d : α
hbd : b ≤ d
hac : a ≤ a
h : a * b = a * d
⊢ a = a ∧ b = d
[PROOFSTEP]
exact ⟨rfl, mul_left_cancel'' h⟩
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝⁵ : Semigroup α
inst✝⁴ : PartialOrder α
inst✝³ : CovariantClass α α (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
inst✝¹ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
hac✝ : a ≤ c
hbd : b ≤ d
h : a * b = c * d
hac : a < c
⊢ a = c ∧ b = d
[PROOFSTEP]
rcases eq_or_lt_of_le hbd with (rfl | hbd)
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
inst✝⁵ : Semigroup α
inst✝⁴ : PartialOrder α
inst✝³ : CovariantClass α α (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
inst✝¹ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
hac✝ : a ≤ c
hac : a < c
hbd : b ≤ b
h : a * b = c * b
⊢ a = c ∧ b = b
[PROOFSTEP]
exact ⟨mul_right_cancel'' h, rfl⟩
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝⁵ : Semigroup α
inst✝⁴ : PartialOrder α
inst✝³ : CovariantClass α α (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
inst✝¹ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
hac✝ : a ≤ c
hbd✝ : b ≤ d
h : a * b = c * d
hac : a < c
hbd : b < d
⊢ a = c ∧ b = d
[PROOFSTEP]
exact ((Right.mul_lt_mul hac hbd).ne h).elim
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : LE α
a b : α
⊢ 1 * a ≤ 1 * b → a ≤ b
[PROOFSTEP]
simpa only [one_mul] using id
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : CommSemigroup α
inst✝ : PartialOrder α
a : α
ha : MulLECancellable a
b c : α
h : (fun x => x * a) b = (fun x => x * a) c
⊢ (fun x x_1 => x * x_1) a b = (fun x x_1 => x * x_1) a c
[PROOFSTEP]
dsimp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : CommSemigroup α
inst✝ : PartialOrder α
a : α
ha : MulLECancellable a
b c : α
h : (fun x => x * a) b = (fun x => x * a) c
⊢ a * b = a * c
[PROOFSTEP]
rwa [mul_comm a, mul_comm a]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LE α
inst✝¹ : CommSemigroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
ha : MulLECancellable a
⊢ b * a ≤ c * a ↔ b ≤ c
[PROOFSTEP]
rw [mul_comm b, mul_comm c, ha.mul_le_mul_iff_left]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LE α
inst✝¹ : MulOneClass α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
ha : MulLECancellable a
⊢ a ≤ a * b ↔ a * 1 ≤ a * b
[PROOFSTEP]
rw [mul_one]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LE α
inst✝¹ : MulOneClass α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
ha : MulLECancellable a
⊢ a * b ≤ a ↔ a * b ≤ a * 1
[PROOFSTEP]
rw [mul_one]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LE α
inst✝¹ : CommMonoid α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
ha : MulLECancellable a
⊢ a ≤ b * a ↔ 1 ≤ b
[PROOFSTEP]
rw [mul_comm, ha.le_mul_iff_one_le_right]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LE α
inst✝¹ : CommMonoid α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
ha : MulLECancellable a
⊢ b * a ≤ a ↔ b ≤ 1
[PROOFSTEP]
rw [mul_comm, ha.mul_le_iff_le_one_right]


[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a✝ b c d e : α
m n : ℤ
a : α
ha : 0 < a
⊢ a * 0 < a * a⁻¹
[PROOFSTEP]
simp [ne_of_gt ha, zero_lt_one]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
⊢ 0 ≤ a⁻¹ ↔ 0 ≤ a
[PROOFSTEP]
simp only [le_iff_eq_or_lt, inv_pos, zero_eq_inv]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
⊢ a⁻¹ < 0 ↔ a < 0
[PROOFSTEP]
simp only [← not_le, inv_nonneg]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
⊢ a⁻¹ ≤ 0 ↔ a ≤ 0
[PROOFSTEP]
simp only [← not_lt, inv_pos]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 < a
hb : 0 < b
⊢ 0 < a / b
[PROOFSTEP]
rw [div_eq_mul_inv]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 < a
hb : 0 < b
⊢ 0 < a * b⁻¹
[PROOFSTEP]
exact mul_pos ha (inv_pos.2 hb)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ a / b
[PROOFSTEP]
rw [div_eq_mul_inv]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ a * b⁻¹
[PROOFSTEP]
exact mul_nonneg ha (inv_nonneg.2 hb)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : a ≤ 0
hb : 0 ≤ b
⊢ a / b ≤ 0
[PROOFSTEP]
rw [div_eq_mul_inv]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : a ≤ 0
hb : 0 ≤ b
⊢ a * b⁻¹ ≤ 0
[PROOFSTEP]
exact mul_nonpos_of_nonpos_of_nonneg ha (inv_nonneg.2 hb)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 ≤ a
hb : b ≤ 0
⊢ a / b ≤ 0
[PROOFSTEP]
rw [div_eq_mul_inv]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 ≤ a
hb : b ≤ 0
⊢ a * b⁻¹ ≤ 0
[PROOFSTEP]
exact mul_nonpos_of_nonneg_of_nonpos ha (inv_nonpos.2 hb)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n✝ : ℤ
ha : 0 ≤ a
n : ℕ
⊢ 0 ≤ a ^ ↑n
[PROOFSTEP]
rw [zpow_ofNat]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n✝ : ℤ
ha : 0 ≤ a
n : ℕ
⊢ 0 ≤ a ^ n
[PROOFSTEP]
exact pow_nonneg ha _
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n✝ : ℤ
ha : 0 ≤ a
n : ℕ
⊢ 0 ≤ a ^ (-↑(n + 1))
[PROOFSTEP]
rw [zpow_neg, inv_nonneg, zpow_ofNat]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n✝ : ℤ
ha : 0 ≤ a
n : ℕ
⊢ 0 ≤ a ^ (n + 1)
[PROOFSTEP]
exact pow_nonneg ha _
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n✝ : ℤ
ha : 0 < a
n : ℕ
⊢ 0 < a ^ ↑n
[PROOFSTEP]
rw [zpow_ofNat]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n✝ : ℤ
ha : 0 < a
n : ℕ
⊢ 0 < a ^ n
[PROOFSTEP]
exact pow_pos ha _
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n✝ : ℤ
ha : 0 < a
n : ℕ
⊢ 0 < a ^ (-↑(n + 1))
[PROOFSTEP]
rw [zpow_neg, inv_pos, zpow_ofNat]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n✝ : ℤ
ha : 0 < a
n : ℕ
⊢ 0 < a ^ (n + 1)
[PROOFSTEP]
exact pow_pos ha _
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
hc : 0 < c
⊢ a ≤ b / c ↔ c * a ≤ b
[PROOFSTEP]
rw [mul_comm, le_div_iff hc]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
hb : 0 < b
h : a / b ≤ c
⊢ a = a / b * b
[PROOFSTEP]
rw [div_mul_cancel _ (ne_of_lt hb).symm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
hb : 0 < b
h : a ≤ c * b
⊢ c * b / b = c
[PROOFSTEP]
refine' (div_eq_iff (ne_of_gt hb)).mpr rfl
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
hb : 0 < b
⊢ a / b ≤ c ↔ a ≤ b * c
[PROOFSTEP]
rw [mul_comm, div_le_iff hb]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
hc : 0 < c
⊢ a < b / c ↔ c * a < b
[PROOFSTEP]
rw [mul_comm, lt_div_iff hc]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
hc : 0 < c
⊢ b / c < a ↔ b < c * a
[PROOFSTEP]
rw [mul_comm, div_lt_iff hc]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
h : 0 < b
⊢ b⁻¹ * a ≤ c ↔ a ≤ b * c
[PROOFSTEP]
rw [inv_eq_one_div, mul_comm, ← div_eq_mul_one_div]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
h : 0 < b
⊢ a / b ≤ c ↔ a ≤ b * c
[PROOFSTEP]
exact div_le_iff' h
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
h : 0 < b
⊢ b⁻¹ * a ≤ c ↔ a ≤ c * b
[PROOFSTEP]
rw [inv_mul_le_iff h, mul_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
h : 0 < b
⊢ a * b⁻¹ ≤ c ↔ a ≤ b * c
[PROOFSTEP]
rw [mul_comm, inv_mul_le_iff h]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
h : 0 < b
⊢ a * b⁻¹ ≤ c ↔ a ≤ c * b
[PROOFSTEP]
rw [mul_comm, inv_mul_le_iff' h]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a✝ b c d e : α
m n : ℤ
a : α
h : a = 0
⊢ a / a ≤ 1
[PROOFSTEP]
simp [h]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a✝ b c d e : α
m n : ℤ
a : α
h : ¬a = 0
⊢ a / a ≤ 1
[PROOFSTEP]
simp [h]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
h : 0 < b
⊢ b⁻¹ * a < c ↔ a < b * c
[PROOFSTEP]
rw [inv_eq_one_div, mul_comm, ← div_eq_mul_one_div]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
h : 0 < b
⊢ a / b < c ↔ a < b * c
[PROOFSTEP]
exact div_lt_iff' h
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
h : 0 < b
⊢ b⁻¹ * a < c ↔ a < c * b
[PROOFSTEP]
rw [inv_mul_lt_iff h, mul_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
h : 0 < b
⊢ a * b⁻¹ < c ↔ a < b * c
[PROOFSTEP]
rw [mul_comm, inv_mul_lt_iff h]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
h : 0 < b
⊢ a * b⁻¹ < c ↔ a < c * b
[PROOFSTEP]
rw [mul_comm, inv_mul_lt_iff' h]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 < a
⊢ a⁻¹ ≤ b ↔ 1 ≤ b * a
[PROOFSTEP]
rw [inv_eq_one_div]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 < a
⊢ 1 / a ≤ b ↔ 1 ≤ b * a
[PROOFSTEP]
exact div_le_iff ha
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 < a
⊢ a⁻¹ ≤ b ↔ 1 ≤ a * b
[PROOFSTEP]
rw [inv_eq_one_div]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 < a
⊢ 1 / a ≤ b ↔ 1 ≤ a * b
[PROOFSTEP]
exact div_le_iff' ha
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 < a
⊢ a⁻¹ < b ↔ 1 < b * a
[PROOFSTEP]
rw [inv_eq_one_div]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 < a
⊢ 1 / a < b ↔ 1 < b * a
[PROOFSTEP]
exact div_lt_iff ha
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 < a
⊢ a⁻¹ < b ↔ 1 < a * b
[PROOFSTEP]
rw [inv_eq_one_div]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 < a
⊢ 1 / a < b ↔ 1 < a * b
[PROOFSTEP]
exact div_lt_iff' ha
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
hb : 0 ≤ b
hc : 0 ≤ c
h : a ≤ c * b
⊢ a / b ≤ c
[PROOFSTEP]
rcases eq_or_lt_of_le hb with (rfl | hb')
[GOAL]
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a c d e : α
m n : ℤ
hc : 0 ≤ c
hb : 0 ≤ 0
h : a ≤ c * 0
⊢ a / 0 ≤ c
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
hb : 0 ≤ b
hc : 0 ≤ c
h : a ≤ c * b
hb' : 0 < b
⊢ a / b ≤ c
[PROOFSTEP]
simp [hc]
[GOAL]
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
hb : 0 ≤ b
hc : 0 ≤ c
h : a ≤ c * b
hb' : 0 < b
⊢ a / b ≤ c
[PROOFSTEP]
rwa [div_le_iff hb']
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
hb : 0 ≤ b
hc : 0 ≤ c
h : a ≤ b / c
⊢ a * c ≤ b
[PROOFSTEP]
obtain rfl | hc := hc.eq_or_lt
[GOAL]
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b d e : α
m n : ℤ
hb : 0 ≤ b
hc : 0 ≤ 0
h : a ≤ b / 0
⊢ a * 0 ≤ b
[PROOFSTEP]
simpa using hb
[GOAL]
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
hb : 0 ≤ b
hc✝ : 0 ≤ c
h : a ≤ b / c
hc : 0 < c
⊢ a * c ≤ b
[PROOFSTEP]
rwa [le_div_iff hc] at h
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
h : a ≤ b
hb : 0 ≤ b
⊢ a ≤ 1 * b
[PROOFSTEP]
rwa [one_mul]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 < a
h : a ≤ b
⊢ b⁻¹ ≤ a⁻¹
[PROOFSTEP]
rwa [← one_div a, le_div_iff' ha, ← div_eq_mul_inv, div_le_iff (ha.trans_le h), one_mul]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 < a
hb : 0 < b
⊢ a⁻¹ ≤ b⁻¹ ↔ b ≤ a
[PROOFSTEP]
rw [← one_div, div_le_iff ha, ← div_eq_inv_mul, le_div_iff hb, one_mul]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 < a
hb : 0 < b
⊢ a⁻¹ ≤ b ↔ b⁻¹ ≤ a
[PROOFSTEP]
rw [← inv_le_inv hb (inv_pos.2 ha), inv_inv]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 < a
hb : 0 < b
⊢ a ≤ b⁻¹ ↔ b ≤ a⁻¹
[PROOFSTEP]
rw [← inv_le_inv (inv_pos.2 hb) ha, inv_inv]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 1 < a
⊢ a⁻¹ < 1
[PROOFSTEP]
rwa [inv_lt (zero_lt_one.trans ha) zero_lt_one, inv_one]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
h₁ : 0 < a
h₂ : a < 1
⊢ 1 < a⁻¹
[PROOFSTEP]
rwa [lt_inv (@zero_lt_one α _ _ _ _ _) h₁, inv_one]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 1 ≤ a
⊢ a⁻¹ ≤ 1
[PROOFSTEP]
rwa [inv_le (zero_lt_one.trans_le ha) zero_lt_one, inv_one]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
h₁ : 0 < a
h₂ : a ≤ 1
⊢ 1 ≤ a⁻¹
[PROOFSTEP]
rwa [le_inv (@zero_lt_one α _ _ _ _ _) h₁, inv_one]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
⊢ a⁻¹ < 1 ↔ a ≤ 0 ∨ 1 < a
[PROOFSTEP]
cases' le_or_lt a 0 with ha ha
[GOAL]
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : a ≤ 0
⊢ a⁻¹ < 1 ↔ a ≤ 0 ∨ 1 < a
[PROOFSTEP]
simp [ha, (inv_nonpos.2 ha).trans_lt zero_lt_one]
[GOAL]
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 < a
⊢ a⁻¹ < 1 ↔ a ≤ 0 ∨ 1 < a
[PROOFSTEP]
simp only [ha.not_le, false_or_iff, inv_lt_one_iff_of_pos ha]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
⊢ a⁻¹ ≤ 1 ↔ a ≤ 0 ∨ 1 ≤ a
[PROOFSTEP]
rcases em (a = 1) with (rfl | ha)
[GOAL]
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
b c d e : α
m n : ℤ
⊢ 1⁻¹ ≤ 1 ↔ 1 ≤ 0 ∨ 1 ≤ 1
[PROOFSTEP]
simp [le_rfl]
[GOAL]
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : ¬a = 1
⊢ a⁻¹ ≤ 1 ↔ a ≤ 0 ∨ 1 ≤ a
[PROOFSTEP]
simp only [Ne.le_iff_lt (Ne.symm ha), Ne.le_iff_lt (mt inv_eq_one.1 ha), inv_lt_one_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
hc : 0 ≤ c
h : a ≤ b
⊢ a / c ≤ b / c
[PROOFSTEP]
rw [div_eq_mul_one_div a c, div_eq_mul_one_div b c]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
hc : 0 ≤ c
h : a ≤ b
⊢ a * (1 / c) ≤ b * (1 / c)
[PROOFSTEP]
exact mul_le_mul_of_nonneg_right h (one_div_nonneg.2 hc)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 ≤ a
hc : 0 < c
h : c ≤ b
⊢ a / b ≤ a / c
[PROOFSTEP]
rw [div_eq_mul_inv, div_eq_mul_inv]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 ≤ a
hc : 0 < c
h : c ≤ b
⊢ a * b⁻¹ ≤ a * c⁻¹
[PROOFSTEP]
exact mul_le_mul_of_nonneg_left ((inv_le_inv (hc.trans_le h) hc).mpr h) ha
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
hc : 0 < c
h : a < b
⊢ a / c < b / c
[PROOFSTEP]
rw [div_eq_mul_one_div a c, div_eq_mul_one_div b c]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
hc : 0 < c
h : a < b
⊢ a * (1 / c) < b * (1 / c)
[PROOFSTEP]
exact mul_lt_mul_of_pos_right h (one_div_pos.2 hc)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ a / b < a / c ↔ c < b
[PROOFSTEP]
simp only [div_eq_mul_inv, mul_lt_mul_left ha, inv_lt_inv hb hc]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
b0 : 0 < b
d0 : 0 < d
⊢ a / b < c / d ↔ a * d < c * b
[PROOFSTEP]
rw [lt_div_iff d0, div_mul_eq_mul_div, div_lt_iff b0]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
b0 : 0 < b
d0 : 0 < d
⊢ a / b ≤ c / d ↔ a * d ≤ c * b
[PROOFSTEP]
rw [le_div_iff d0, div_mul_eq_mul_div, div_le_iff b0]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
hc : 0 ≤ c
hac : a ≤ c
hd : 0 < d
hbd : d ≤ b
⊢ a / b ≤ c / d
[PROOFSTEP]
rw [div_le_div_iff (hd.trans_le hbd) hd]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
hc : 0 ≤ c
hac : a ≤ c
hd : 0 < d
hbd : d ≤ b
⊢ a * d ≤ c * b
[PROOFSTEP]
exact mul_le_mul hac hbd hd.le hc
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 ≤ a
hb : 1 ≤ b
⊢ a / b ≤ a
[PROOFSTEP]
simpa only [div_one] using div_le_div_of_le_left ha zero_lt_one hb
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 < a
hb : 1 < b
⊢ a / b < a
[PROOFSTEP]
simpa only [div_one] using div_lt_div_of_lt_left ha zero_lt_one hb
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 ≤ a
hb₀ : 0 < b
hb₁ : b ≤ 1
⊢ a ≤ a / b
[PROOFSTEP]
simpa only [div_one] using div_le_div_of_le_left ha hb₀ hb₁
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
hb : 0 < b
⊢ 1 ≤ a / b ↔ b ≤ a
[PROOFSTEP]
rw [le_div_iff hb, one_mul]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
hb : 0 < b
⊢ a / b ≤ 1 ↔ a ≤ b
[PROOFSTEP]
rw [div_le_iff hb, one_mul]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
hb : 0 < b
⊢ 1 < a / b ↔ b < a
[PROOFSTEP]
rw [lt_div_iff hb, one_mul]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
hb : 0 < b
⊢ a / b < 1 ↔ a < b
[PROOFSTEP]
rw [div_lt_iff hb, one_mul]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 < a
hb : 0 < b
⊢ 1 / a ≤ b ↔ 1 / b ≤ a
[PROOFSTEP]
simpa using inv_le ha hb
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 < a
hb : 0 < b
⊢ 1 / a < b ↔ 1 / b < a
[PROOFSTEP]
simpa using inv_lt ha hb
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 < a
hb : 0 < b
⊢ a ≤ 1 / b ↔ b ≤ 1 / a
[PROOFSTEP]
simpa using le_inv ha hb
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 < a
hb : 0 < b
⊢ a < 1 / b ↔ b < 1 / a
[PROOFSTEP]
simpa using lt_inv ha hb
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 < a
h : a ≤ b
⊢ 1 / b ≤ 1 / a
[PROOFSTEP]
simpa using inv_le_inv_of_le ha h
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 < a
h : a < b
⊢ 1 / b < 1 / a
[PROOFSTEP]
rwa [lt_div_iff' ha, ← div_eq_mul_one_div, div_lt_one (ha.trans h)]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
h1 : 0 < a
h2 : a < 1
⊢ 1 < 1 / a
[PROOFSTEP]
rwa [lt_one_div (@zero_lt_one α _ _ _ _ _) h1, one_div_one]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
h1 : 0 < a
h2 : a ≤ 1
⊢ 1 ≤ 1 / a
[PROOFSTEP]
rwa [le_one_div (@zero_lt_one α _ _ _ _ _) h1, one_div_one]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a✝ b c d e : α
m n : ℤ
a : α
⊢ a / 2 + a / 2 = a
[PROOFSTEP]
rw [div_add_div_same, ← two_mul, mul_div_cancel_left a two_ne_zero]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a✝ b c d e : α
m n : ℤ
a : α
⊢ (a + a) / 2 = a
[PROOFSTEP]
rw [← mul_two, mul_div_cancel a two_ne_zero]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
⊢ a / 2 ≤ a ↔ 0 ≤ a
[PROOFSTEP]
rw [div_le_iff (zero_lt_two' α), mul_two, le_add_iff_nonneg_left]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
⊢ a / 2 < a ↔ 0 < a
[PROOFSTEP]
rw [div_lt_iff (zero_lt_two' α), mul_two, lt_add_iff_pos_left]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
⊢ a < (a + b) / 2 ↔ a < b
[PROOFSTEP]
simp [lt_div_iff, mul_two]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
⊢ (a + b) / 2 < b ↔ a < b
[PROOFSTEP]
simp [div_lt_iff, mul_two]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a✝ b c d e : α
m n : ℤ
a : α
⊢ a / 3 + a / 3 + a / 3 = a
[PROOFSTEP]
rw [div_add_div_same, div_add_div_same, ← two_mul, ← add_one_mul 2 a, two_add_one_eq_three,
  mul_div_cancel_left a three_ne_zero]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
h : a * (b / c) ≤ d
hc : 0 < c
⊢ b * a ≤ d * c
[PROOFSTEP]
rw [← mul_div_assoc] at h
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
h : a * b / c ≤ d
hc : 0 < c
⊢ b * a ≤ d * c
[PROOFSTEP]
rwa [mul_comm b, ← div_le_iff hc]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
h : a / b ≤ c / d
he : 0 ≤ e
⊢ a / (b * e) ≤ c / (d * e)
[PROOFSTEP]
rw [div_mul_eq_div_mul_one_div, div_mul_eq_div_mul_one_div]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
h : a / b ≤ c / d
he : 0 ≤ e
⊢ a / b * (1 / e) ≤ c / d * (1 / e)
[PROOFSTEP]
exact mul_le_mul_of_nonneg_right h (one_div_nonneg.2 he)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a✝ b✝ c d e : α
m n : ℤ
a : α
h : 0 < a
b : α
⊢ ∃ c, 0 < c ∧ b * c < a
[PROOFSTEP]
have : 0 < a / max (b + 1) 1 := div_pos h (lt_max_iff.2 (Or.inr zero_lt_one))
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a✝ b✝ c d e : α
m n : ℤ
a : α
h : 0 < a
b : α
this : 0 < a / max (b + 1) 1
⊢ ∃ c, 0 < c ∧ b * c < a
[PROOFSTEP]
refine' ⟨a / max (b + 1) 1, this, _⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a✝ b✝ c d e : α
m n : ℤ
a : α
h : 0 < a
b : α
this : 0 < a / max (b + 1) 1
⊢ b * (a / max (b + 1) 1) < a
[PROOFSTEP]
rw [← lt_div_iff this, div_div_cancel' h.ne']
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a✝ b✝ c d e : α
m n : ℤ
a : α
h : 0 < a
b : α
this : 0 < a / max (b + 1) 1
⊢ b < max (b + 1) 1
[PROOFSTEP]
exact lt_max_iff.2 (Or.inl <| lt_add_one _)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a✝ b✝ c✝ d e : α
m n : ℤ
a : α
h : 0 < a
b c : α
hc₀ : 0 < c
hc : b * c < a
⊢ b < c⁻¹ * a
[PROOFSTEP]
rwa [← div_eq_inv_mul, lt_div_iff hc₀]
[GOAL]
ι : Type u_1
α : Type u_2
β✝ : Type u_3
inst✝¹ : LinearOrderedSemifield α
a b c✝ d e : α
m n : ℤ
β : Type u_4
inst✝ : Preorder β
f : β → α
hf : Monotone f
c : α
hc : 0 ≤ c
⊢ Monotone fun x => f x / c
[PROOFSTEP]
haveI := @LinearOrder.decidableLE α _
[GOAL]
ι : Type u_1
α : Type u_2
β✝ : Type u_3
inst✝¹ : LinearOrderedSemifield α
a b c✝ d e : α
m n : ℤ
β : Type u_4
inst✝ : Preorder β
f : β → α
hf : Monotone f
c : α
hc : 0 ≤ c
this : DecidableRel fun x x_1 => x ≤ x_1
⊢ Monotone fun x => f x / c
[PROOFSTEP]
simpa only [div_eq_mul_inv] using (monotone_mul_right_of_nonneg (inv_nonneg.2 hc)).comp hf
[GOAL]
ι : Type u_1
α : Type u_2
β✝ : Type u_3
inst✝¹ : LinearOrderedSemifield α
a b c✝ d e : α
m n : ℤ
β : Type u_4
inst✝ : Preorder β
f : β → α
hf : StrictMono f
c : α
hc : 0 < c
⊢ StrictMono fun x => f x / c
[PROOFSTEP]
simpa only [div_eq_mul_inv] using hf.mul_const (inv_pos.2 hc)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m✝ n✝ : ℤ
a1 : 1 ≤ a
m n : ℕ
mn : m ≤ n
⊢ 1 / a ^ n ≤ 1 / a ^ m
[PROOFSTEP]
refine' (one_div_le_one_div _ _).mpr (pow_le_pow a1 mn)
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m✝ n✝ : ℤ
a1 : 1 ≤ a
m n : ℕ
mn : m ≤ n
⊢ 0 < a ^ n
[PROOFSTEP]
exact pow_pos (zero_lt_one.trans_le a1) _
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m✝ n✝ : ℤ
a1 : 1 ≤ a
m n : ℕ
mn : m ≤ n
⊢ 0 < a ^ m
[PROOFSTEP]
exact pow_pos (zero_lt_one.trans_le a1) _
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m✝ n✝ : ℤ
a1 : 1 < a
m n : ℕ
mn : m < n
⊢ 1 / a ^ n < 1 / a ^ m
[PROOFSTEP]
refine' (one_div_lt_one_div _ _).mpr (pow_lt_pow a1 mn)
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m✝ n✝ : ℤ
a1 : 1 < a
m n : ℕ
mn : m < n
⊢ 0 < a ^ n
[PROOFSTEP]
exact pow_pos (zero_lt_one.trans a1) _
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m✝ n✝ : ℤ
a1 : 1 < a
m n : ℕ
mn : m < n
⊢ 0 < a ^ m
[PROOFSTEP]
exact pow_pos (zero_lt_one.trans a1) _
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m✝ n✝ : ℤ
a1 : 1 ≤ a
m n : ℕ
mn : m ≤ n
⊢ (a ^ n)⁻¹ ≤ (a ^ m)⁻¹
[PROOFSTEP]
convert one_div_pow_le_one_div_pow_of_le a1 mn using 1
[GOAL]
case h.e'_3
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m✝ n✝ : ℤ
a1 : 1 ≤ a
m n : ℕ
mn : m ≤ n
⊢ (a ^ n)⁻¹ = 1 / a ^ n
[PROOFSTEP]
simp
[GOAL]
case h.e'_4
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m✝ n✝ : ℤ
a1 : 1 ≤ a
m n : ℕ
mn : m ≤ n
⊢ (a ^ m)⁻¹ = 1 / a ^ m
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m✝ n✝ : ℤ
a1 : 1 < a
m n : ℕ
mn : m < n
⊢ (a ^ n)⁻¹ < (a ^ m)⁻¹
[PROOFSTEP]
convert one_div_pow_lt_one_div_pow_of_lt a1 mn using 1
[GOAL]
case h.e'_3
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m✝ n✝ : ℤ
a1 : 1 < a
m n : ℕ
mn : m < n
⊢ (a ^ n)⁻¹ = 1 / a ^ n
[PROOFSTEP]
simp
[GOAL]
case h.e'_4
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m✝ n✝ : ℤ
a1 : 1 < a
m n : ℕ
mn : m < n
⊢ (a ^ m)⁻¹ = 1 / a ^ m
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
s : Set α
ha : 0 ≤ a
hs : IsGLB s b
⊢ IsGLB ((fun b => a * b) '' s) (a * b)
[PROOFSTEP]
rcases lt_or_eq_of_le ha with (ha | rfl)
[GOAL]
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
s : Set α
ha✝ : 0 ≤ a
hs : IsGLB s b
ha : 0 < a
⊢ IsGLB ((fun b => a * b) '' s) (a * b)
[PROOFSTEP]
exact (OrderIso.mulLeft₀ _ ha).isGLB_image'.2 hs
[GOAL]
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
b c d e : α
m n : ℤ
s : Set α
hs : IsGLB s b
ha : 0 ≤ 0
⊢ IsGLB ((fun b => 0 * b) '' s) (0 * b)
[PROOFSTEP]
simp_rw [zero_mul]
[GOAL]
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
b c d e : α
m n : ℤ
s : Set α
hs : IsGLB s b
ha : 0 ≤ 0
⊢ IsGLB ((fun a => 0) '' s) 0
[PROOFSTEP]
rw [hs.nonempty.image_const]
[GOAL]
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
b c d e : α
m n : ℤ
s : Set α
hs : IsGLB s b
ha : 0 ≤ 0
⊢ IsGLB {0} 0
[PROOFSTEP]
exact isGLB_singleton
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
s : Set α
ha : 0 ≤ a
hs : IsGLB s b
⊢ IsGLB ((fun b => b * a) '' s) (b * a)
[PROOFSTEP]
simpa [mul_comm] using hs.mul_left ha
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
⊢ 0 < a / b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
[PROOFSTEP]
simp only [division_def, mul_pos_iff, inv_pos, inv_lt_zero]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
⊢ a / b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
[PROOFSTEP]
simp [division_def, mul_neg_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
⊢ 0 ≤ a / b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
[PROOFSTEP]
simp [division_def, mul_nonneg_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
⊢ a / b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
[PROOFSTEP]
simp [division_def, mul_nonpos_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hc : c < 0
⊢ b / c ≤ a ↔ c * a ≤ b
[PROOFSTEP]
rw [mul_comm, div_le_iff_of_neg hc]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hc : c < 0
⊢ a ≤ b / c ↔ b ≤ a * c
[PROOFSTEP]
rw [← neg_neg c, mul_neg, div_neg, le_neg, div_le_iff (neg_pos.2 hc), neg_mul]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hc : c < 0
⊢ a ≤ b / c ↔ b ≤ c * a
[PROOFSTEP]
rw [mul_comm, le_div_iff_of_neg hc]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hc : c < 0
⊢ b / c < a ↔ c * a < b
[PROOFSTEP]
rw [mul_comm, div_lt_iff_of_neg hc]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hc : c < 0
⊢ a < b / c ↔ b < c * a
[PROOFSTEP]
rw [mul_comm, lt_div_iff_of_neg hc]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
h : b ≤ a
hb : b ≤ 0
⊢ a / b ≤ 1
[PROOFSTEP]
simpa only [neg_div_neg_eq] using div_le_one_of_le (neg_le_neg h) (neg_nonneg_of_nonpos hb)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
ha : a < 0
hb : b < 0
⊢ a⁻¹ ≤ b⁻¹ ↔ b ≤ a
[PROOFSTEP]
rw [← one_div, div_le_iff_of_neg ha, ← div_eq_inv_mul, div_le_iff_of_neg hb, one_mul]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
ha : a < 0
hb : b < 0
⊢ a⁻¹ ≤ b ↔ b⁻¹ ≤ a
[PROOFSTEP]
rw [← inv_le_inv_of_neg hb (inv_lt_zero.2 ha), inv_inv]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
ha : a < 0
hb : b < 0
⊢ a ≤ b⁻¹ ↔ b ≤ a⁻¹
[PROOFSTEP]
rw [← inv_le_inv_of_neg (inv_lt_zero.2 hb) ha, inv_inv]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hc : c ≤ 0
h : b ≤ a
⊢ a / c ≤ b / c
[PROOFSTEP]
rw [div_eq_mul_one_div a c, div_eq_mul_one_div b c]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hc : c ≤ 0
h : b ≤ a
⊢ a * (1 / c) ≤ b * (1 / c)
[PROOFSTEP]
exact mul_le_mul_of_nonpos_right h (one_div_nonpos.2 hc)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hc : c < 0
h : b < a
⊢ a / c < b / c
[PROOFSTEP]
rw [div_eq_mul_one_div a c, div_eq_mul_one_div b c]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hc : c < 0
h : b < a
⊢ a * (1 / c) < b * (1 / c)
[PROOFSTEP]
exact mul_lt_mul_of_neg_right h (one_div_neg.2 hc)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hb : b < 0
⊢ 1 ≤ a / b ↔ a ≤ b
[PROOFSTEP]
rw [le_div_iff_of_neg hb, one_mul]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hb : b < 0
⊢ a / b ≤ 1 ↔ b ≤ a
[PROOFSTEP]
rw [div_le_iff_of_neg hb, one_mul]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hb : b < 0
⊢ 1 < a / b ↔ a < b
[PROOFSTEP]
rw [lt_div_iff_of_neg hb, one_mul]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hb : b < 0
⊢ a / b < 1 ↔ b < a
[PROOFSTEP]
rw [div_lt_iff_of_neg hb, one_mul]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
ha : a < 0
hb : b < 0
⊢ 1 / a ≤ b ↔ 1 / b ≤ a
[PROOFSTEP]
simpa using inv_le_of_neg ha hb
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
ha : a < 0
hb : b < 0
⊢ 1 / a < b ↔ 1 / b < a
[PROOFSTEP]
simpa using inv_lt_of_neg ha hb
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
ha : a < 0
hb : b < 0
⊢ a ≤ 1 / b ↔ b ≤ 1 / a
[PROOFSTEP]
simpa using le_inv_of_neg ha hb
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
ha : a < 0
hb : b < 0
⊢ a < 1 / b ↔ b < 1 / a
[PROOFSTEP]
simpa using lt_inv_of_neg ha hb
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
⊢ 1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b
[PROOFSTEP]
rcases lt_trichotomy b 0 with (hb | rfl | hb)
[GOAL]
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hb : b < 0
⊢ 1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b
[PROOFSTEP]
simp [hb, hb.not_lt, one_lt_div_of_neg]
[GOAL]
case inr.inl
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a c d : α
n : ℤ
⊢ 1 < a / 0 ↔ 0 < 0 ∧ 0 < a ∨ 0 < 0 ∧ a < 0
[PROOFSTEP]
simp [lt_irrefl, zero_le_one]
[GOAL]
case inr.inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hb : 0 < b
⊢ 1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b
[PROOFSTEP]
simp [hb, hb.not_lt, one_lt_div]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
⊢ 1 ≤ a / b ↔ 0 < b ∧ b ≤ a ∨ b < 0 ∧ a ≤ b
[PROOFSTEP]
rcases lt_trichotomy b 0 with (hb | rfl | hb)
[GOAL]
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hb : b < 0
⊢ 1 ≤ a / b ↔ 0 < b ∧ b ≤ a ∨ b < 0 ∧ a ≤ b
[PROOFSTEP]
simp [hb, hb.not_lt, one_le_div_of_neg]
[GOAL]
case inr.inl
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a c d : α
n : ℤ
⊢ 1 ≤ a / 0 ↔ 0 < 0 ∧ 0 ≤ a ∨ 0 < 0 ∧ a ≤ 0
[PROOFSTEP]
simp [lt_irrefl, zero_lt_one.not_le, zero_lt_one]
[GOAL]
case inr.inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hb : 0 < b
⊢ 1 ≤ a / b ↔ 0 < b ∧ b ≤ a ∨ b < 0 ∧ a ≤ b
[PROOFSTEP]
simp [hb, hb.not_lt, one_le_div]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
⊢ a / b < 1 ↔ 0 < b ∧ a < b ∨ b = 0 ∨ b < 0 ∧ b < a
[PROOFSTEP]
rcases lt_trichotomy b 0 with (hb | rfl | hb)
[GOAL]
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hb : b < 0
⊢ a / b < 1 ↔ 0 < b ∧ a < b ∨ b = 0 ∨ b < 0 ∧ b < a
[PROOFSTEP]
simp [hb, hb.not_lt, hb.ne, div_lt_one_of_neg]
[GOAL]
case inr.inl
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a c d : α
n : ℤ
⊢ a / 0 < 1 ↔ 0 < 0 ∧ a < 0 ∨ 0 = 0 ∨ 0 < 0 ∧ 0 < a
[PROOFSTEP]
simp [zero_lt_one]
[GOAL]
case inr.inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hb : 0 < b
⊢ a / b < 1 ↔ 0 < b ∧ a < b ∨ b = 0 ∨ b < 0 ∧ b < a
[PROOFSTEP]
simp [hb, hb.not_lt, div_lt_one, hb.ne.symm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
⊢ a / b ≤ 1 ↔ 0 < b ∧ a ≤ b ∨ b = 0 ∨ b < 0 ∧ b ≤ a
[PROOFSTEP]
rcases lt_trichotomy b 0 with (hb | rfl | hb)
[GOAL]
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hb : b < 0
⊢ a / b ≤ 1 ↔ 0 < b ∧ a ≤ b ∨ b = 0 ∨ b < 0 ∧ b ≤ a
[PROOFSTEP]
simp [hb, hb.not_lt, hb.ne, div_le_one_of_neg]
[GOAL]
case inr.inl
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a c d : α
n : ℤ
⊢ a / 0 ≤ 1 ↔ 0 < 0 ∧ a ≤ 0 ∨ 0 = 0 ∨ 0 < 0 ∧ 0 ≤ a
[PROOFSTEP]
simp [zero_le_one]
[GOAL]
case inr.inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hb : 0 < b
⊢ a / b ≤ 1 ↔ 0 < b ∧ a ≤ b ∨ b = 0 ∨ b < 0 ∧ b ≤ a
[PROOFSTEP]
simp [hb, hb.not_lt, div_le_one, hb.ne.symm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hb : b < 0
h : a ≤ b
⊢ 1 / b ≤ 1 / a
[PROOFSTEP]
rwa [div_le_iff_of_neg' hb, ← div_eq_mul_one_div, div_le_one_of_neg (h.trans_lt hb)]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hb : b < 0
h : a < b
⊢ 1 / b < 1 / a
[PROOFSTEP]
rwa [div_lt_iff_of_neg' hb, ← div_eq_mul_one_div, div_lt_one_of_neg (h.trans hb)]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
ha : a < 0
hb : b < 0
⊢ 1 / a ≤ 1 / b ↔ b ≤ a
[PROOFSTEP]
simpa [one_div] using inv_le_inv_of_neg ha hb
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
h1 : a < 0
h2 : -1 < a
this : 1 / a < 1 / -1
⊢ 1 / a < -1
[PROOFSTEP]
rwa [one_div_neg_one_eq_neg_one] at this
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
h1 : a < 0
h2 : -1 ≤ a
this : 1 / a ≤ 1 / -1
⊢ 1 / a ≤ -1
[PROOFSTEP]
rwa [one_div_neg_one_eq_neg_one] at this
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a✝ b c d : α
n : ℤ
a : α
⊢ a - a / 2 = a / 2
[PROOFSTEP]
suffices a / 2 + a / 2 - a / 2 = a / 2 by rwa [add_halves] at this
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a✝ b c d : α
n : ℤ
a : α
this : a / 2 + a / 2 - a / 2 = a / 2
⊢ a - a / 2 = a / 2
[PROOFSTEP]
rwa [add_halves] at this
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a✝ b c d : α
n : ℤ
a : α
⊢ a / 2 + a / 2 - a / 2 = a / 2
[PROOFSTEP]
rw [add_sub_cancel]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a✝ b c d : α
n : ℤ
a : α
⊢ a / 2 - a = -(a / 2)
[PROOFSTEP]
suffices a / 2 - (a / 2 + a / 2) = -(a / 2) by rwa [add_halves] at this
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a✝ b c d : α
n : ℤ
a : α
this : a / 2 - (a / 2 + a / 2) = -(a / 2)
⊢ a / 2 - a = -(a / 2)
[PROOFSTEP]
rwa [add_halves] at this
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a✝ b c d : α
n : ℤ
a : α
⊢ a / 2 - (a / 2 + a / 2) = -(a / 2)
[PROOFSTEP]
rw [sub_add_eq_sub_sub, sub_self, zero_sub]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
h : a < b
⊢ a + (b - a) / 2 < b
[PROOFSTEP]
rwa [← div_sub_div_same, sub_eq_add_neg, add_comm (b / 2), ← add_assoc, ← sub_eq_add_neg, ← lt_sub_iff_add_lt,
  sub_self_div_two, sub_self_div_two, div_lt_div_right (zero_lt_two' α)]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
a2 : 2 ≤ a
⊢ (1 - 1 / a)⁻¹ ≤ 2
[PROOFSTEP]
refine'
  (inv_le_inv_of_le (inv_pos.2 <| zero_lt_two' α) _).trans_eq
    (inv_inv (2 : α))
      -- move `1 / a` to the left and `2⁻¹` to the right.
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
a2 : 2 ≤ a
⊢ 2⁻¹ ≤ 1 - 1 / a
[PROOFSTEP]
rw [le_sub_iff_add_le, add_comm, ← le_sub_iff_add_le]
  -- take inverses on both sides and use the assumption `2 ≤ a`.
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
a2 : 2 ≤ a
⊢ 1 / a ≤ 1 - 2⁻¹
[PROOFSTEP]
convert (one_div a).le.trans (inv_le_inv_of_le zero_lt_two a2) using 1
  -- show `1 - 1 / 2 = 1 / 2`.
[GOAL]
case h.e'_4
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
a2 : 2 ≤ a
⊢ 1 - 2⁻¹ = 2⁻¹
[PROOFSTEP]
rw [sub_eq_iff_eq_add, ← two_mul, mul_inv_cancel two_ne_zero]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
s : Set α
ha : 0 ≤ a
hs : IsLUB s b
⊢ IsLUB ((fun b => a * b) '' s) (a * b)
[PROOFSTEP]
rcases lt_or_eq_of_le ha with (ha | rfl)
[GOAL]
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
s : Set α
ha✝ : 0 ≤ a
hs : IsLUB s b
ha : 0 < a
⊢ IsLUB ((fun b => a * b) '' s) (a * b)
[PROOFSTEP]
exact (OrderIso.mulLeft₀ _ ha).isLUB_image'.2 hs
[GOAL]
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
b c d : α
n : ℤ
s : Set α
hs : IsLUB s b
ha : 0 ≤ 0
⊢ IsLUB ((fun b => 0 * b) '' s) (0 * b)
[PROOFSTEP]
simp_rw [zero_mul]
[GOAL]
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
b c d : α
n : ℤ
s : Set α
hs : IsLUB s b
ha : 0 ≤ 0
⊢ IsLUB ((fun a => 0) '' s) 0
[PROOFSTEP]
rw [hs.nonempty.image_const]
[GOAL]
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
b c d : α
n : ℤ
s : Set α
hs : IsLUB s b
ha : 0 ≤ 0
⊢ IsLUB {0} 0
[PROOFSTEP]
exact isLUB_singleton
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
s : Set α
ha : 0 ≤ a
hs : IsLUB s b
⊢ IsLUB ((fun b => b * a) '' s) (b * a)
[PROOFSTEP]
simpa [mul_comm] using hs.mul_left ha
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hc : c ≠ 0
hd : d ≠ 0
⊢ (a * d - b * c) / (c * d) < 0 ↔ a / c < b / d
[PROOFSTEP]
rw [mul_comm b c, ← div_sub_div _ _ hc hd, sub_lt_zero]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hc : c ≠ 0
hd : d ≠ 0
⊢ (a * d - b * c) / (c * d) ≤ 0 ↔ a / c ≤ b / d
[PROOFSTEP]
rw [mul_comm b c, ← div_sub_div _ _ hc hd, sub_nonpos]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
h : ∀ (ε : α), ε > 0 → b - ε ≤ a
⊢ b ≤ a
[PROOFSTEP]
contrapose! h
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
h : a < b
⊢ ∃ ε, ε > 0 ∧ a < b - ε
[PROOFSTEP]
simpa only [@and_comm ((0 : α) < _), lt_sub_iff_add_lt, gt_iff_lt] using exists_add_lt_and_pos_of_lt h
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
a0 : 0 ≤ a
b0 : 0 ≤ b
h : a = -b
⊢ a = b
[PROOFSTEP]
subst a
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
b c d : α
n : ℤ
b0 : 0 ≤ b
a0 : 0 ≤ -b
⊢ -b = b
[PROOFSTEP]
have : b = 0 := le_antisymm (neg_nonneg.1 a0) b0
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
b c d : α
n : ℤ
b0 : 0 ≤ b
a0 : 0 ≤ -b
this : b = 0
⊢ -b = b
[PROOFSTEP]
rw [this, neg_zero]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
a✝ b c d : α
n : ℤ
a : α
⊢ |1 / a| = 1 / |a|
[PROOFSTEP]
rw [abs_div, abs_one]


[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : Preorder α
inst✝⁵ : NonAssocSemiring β
inst✝⁴ : Preorder β
inst✝³ : NonAssocSemiring γ
inst✝² : Preorder γ
inst✝¹ : NonAssocSemiring δ
inst✝ : Preorder δ
f g : α →+*o β
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := f
[GOAL]
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : Preorder α
inst✝⁵ : NonAssocSemiring β
inst✝⁴ : Preorder β
inst✝³ : NonAssocSemiring γ
inst✝² : Preorder γ
inst✝¹ : NonAssocSemiring δ
inst✝ : Preorder δ
g : α →+*o β
toMonoidHom✝ : α →* β
map_zero'✝ : OneHom.toFun (↑toMonoidHom✝) 0 = 0
map_add'✝ :
  ∀ (x y : α), OneHom.toFun (↑toMonoidHom✝) (x + y) = OneHom.toFun (↑toMonoidHom✝) x + OneHom.toFun (↑toMonoidHom✝) y
monotone'✝ : Monotone (↑↑{ toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }).toFun
h :
  (fun f => f.toFun)
      { toRingHom := { toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ },
        monotone' := monotone'✝ } =
    (fun f => f.toFun) g
⊢ { toRingHom := { toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ },
      monotone' := monotone'✝ } =
    g
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := g
[GOAL]
case mk.mk.mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : Preorder α
inst✝⁵ : NonAssocSemiring β
inst✝⁴ : Preorder β
inst✝³ : NonAssocSemiring γ
inst✝² : Preorder γ
inst✝¹ : NonAssocSemiring δ
inst✝ : Preorder δ
toMonoidHom✝¹ : α →* β
map_zero'✝¹ : OneHom.toFun (↑toMonoidHom✝¹) 0 = 0
map_add'✝¹ :
  ∀ (x y : α), OneHom.toFun (↑toMonoidHom✝¹) (x + y) = OneHom.toFun (↑toMonoidHom✝¹) x + OneHom.toFun (↑toMonoidHom✝¹) y
monotone'✝¹ : Monotone (↑↑{ toMonoidHom := toMonoidHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ }).toFun
toMonoidHom✝ : α →* β
map_zero'✝ : OneHom.toFun (↑toMonoidHom✝) 0 = 0
map_add'✝ :
  ∀ (x y : α), OneHom.toFun (↑toMonoidHom✝) (x + y) = OneHom.toFun (↑toMonoidHom✝) x + OneHom.toFun (↑toMonoidHom✝) y
monotone'✝ : Monotone (↑↑{ toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }).toFun
h :
  (fun f => f.toFun)
      { toRingHom := { toMonoidHom := toMonoidHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ },
        monotone' := monotone'✝¹ } =
    (fun f => f.toFun)
      { toRingHom := { toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ },
        monotone' := monotone'✝ }
⊢ { toRingHom := { toMonoidHom := toMonoidHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ },
      monotone' := monotone'✝¹ } =
    { toRingHom := { toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ },
      monotone' := monotone'✝ }
[PROOFSTEP]
congr
  -- porting note: needed to add the following line
[GOAL]
case mk.mk.mk.mk.e_toRingHom.e_toMonoidHom
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : Preorder α
inst✝⁵ : NonAssocSemiring β
inst✝⁴ : Preorder β
inst✝³ : NonAssocSemiring γ
inst✝² : Preorder γ
inst✝¹ : NonAssocSemiring δ
inst✝ : Preorder δ
toMonoidHom✝¹ : α →* β
map_zero'✝¹ : OneHom.toFun (↑toMonoidHom✝¹) 0 = 0
map_add'✝¹ :
  ∀ (x y : α), OneHom.toFun (↑toMonoidHom✝¹) (x + y) = OneHom.toFun (↑toMonoidHom✝¹) x + OneHom.toFun (↑toMonoidHom✝¹) y
monotone'✝¹ : Monotone (↑↑{ toMonoidHom := toMonoidHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ }).toFun
toMonoidHom✝ : α →* β
map_zero'✝ : OneHom.toFun (↑toMonoidHom✝) 0 = 0
map_add'✝ :
  ∀ (x y : α), OneHom.toFun (↑toMonoidHom✝) (x + y) = OneHom.toFun (↑toMonoidHom✝) x + OneHom.toFun (↑toMonoidHom✝) y
monotone'✝ : Monotone (↑↑{ toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }).toFun
h :
  (fun f => f.toFun)
      { toRingHom := { toMonoidHom := toMonoidHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ },
        monotone' := monotone'✝¹ } =
    (fun f => f.toFun)
      { toRingHom := { toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ },
        monotone' := monotone'✝ }
⊢ toMonoidHom✝¹ = toMonoidHom✝
[PROOFSTEP]
exact MonoidHom.monoidHomClass.coe_injective' h
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : Preorder α
inst✝⁵ : NonAssocSemiring β
inst✝⁴ : Preorder β
inst✝³ : NonAssocSemiring γ
inst✝² : Preorder γ
inst✝¹ : NonAssocSemiring δ
inst✝ : Preorder δ
f₁ f₂ : β →+*o γ
g : α →+*o β
hg : Surjective ↑g
h : f₁ = f₂
⊢ OrderRingHom.comp f₁ g = OrderRingHom.comp f₂ g
[PROOFSTEP]
rw [h]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : Preorder α
inst✝⁵ : NonAssocSemiring β
inst✝⁴ : Preorder β
inst✝³ : NonAssocSemiring γ
inst✝² : Preorder γ
inst✝¹ : NonAssocSemiring δ
inst✝ : Preorder δ
f : β →+*o γ
g₁ g₂ : α →+*o β
hf : Injective ↑f
h : OrderRingHom.comp f g₁ = OrderRingHom.comp f g₂
a : α
⊢ ↑f (↑g₁ a) = ↑f (↑g₂ a)
[PROOFSTEP]
rw [← comp_apply, h, comp_apply]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹¹ : Mul α
inst✝¹⁰ : Add α
inst✝⁹ : LE α
inst✝⁸ : Mul β
inst✝⁷ : Add β
inst✝⁶ : LE β
inst✝⁵ : Mul γ
inst✝⁴ : Add γ
inst✝³ : LE γ
inst✝² : Mul δ
inst✝¹ : Add δ
inst✝ : LE δ
f g : α ≃+*o β
h₁ : (fun f => f.toFun) f = (fun f => f.toFun) g
h₂ : (fun f => f.invFun) f = (fun f => f.invFun) g
⊢ f = g
[PROOFSTEP]
obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := f
[GOAL]
case mk.mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹¹ : Mul α
inst✝¹⁰ : Add α
inst✝⁹ : LE α
inst✝⁸ : Mul β
inst✝⁷ : Add β
inst✝⁶ : LE β
inst✝⁵ : Mul γ
inst✝⁴ : Add γ
inst✝³ : LE γ
inst✝² : Mul δ
inst✝¹ : Add δ
inst✝ : LE δ
g : α ≃+*o β
toFun✝ : α → β
invFun✝ : β → α
left_inv✝ : LeftInverse invFun✝ toFun✝
right_inv✝ : Function.RightInverse invFun✝ toFun✝
map_mul'✝ :
  ∀ (x y : α),
    Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } (x * y) =
      Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x *
        Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } y
map_add'✝ :
  ∀ (x y : α),
    Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } (x + y) =
      Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x +
        Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } y
map_le_map_iff'✝ :
  ∀ {a b : α},
    Equiv.toFun
          { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
              map_mul' := map_mul'✝, map_add' := map_add'✝ }.toEquiv
          a ≤
        Equiv.toFun
          { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
              map_mul' := map_mul'✝, map_add' := map_add'✝ }.toEquiv
          b ↔
      a ≤ b
h₁ :
  (fun f => f.toFun)
      {
        toRingEquiv :=
          { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
            map_mul' := map_mul'✝, map_add' := map_add'✝ },
        map_le_map_iff' := map_le_map_iff'✝ } =
    (fun f => f.toFun) g
h₂ :
  (fun f => f.invFun)
      {
        toRingEquiv :=
          { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
            map_mul' := map_mul'✝, map_add' := map_add'✝ },
        map_le_map_iff' := map_le_map_iff'✝ } =
    (fun f => f.invFun) g
⊢ {
      toRingEquiv :=
        { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
          map_mul' := map_mul'✝, map_add' := map_add'✝ },
      map_le_map_iff' := map_le_map_iff'✝ } =
    g
[PROOFSTEP]
obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := g
[GOAL]
case mk.mk.mk.mk.mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹¹ : Mul α
inst✝¹⁰ : Add α
inst✝⁹ : LE α
inst✝⁸ : Mul β
inst✝⁷ : Add β
inst✝⁶ : LE β
inst✝⁵ : Mul γ
inst✝⁴ : Add γ
inst✝³ : LE γ
inst✝² : Mul δ
inst✝¹ : Add δ
inst✝ : LE δ
toFun✝¹ : α → β
invFun✝¹ : β → α
left_inv✝¹ : LeftInverse invFun✝¹ toFun✝¹
right_inv✝¹ : Function.RightInverse invFun✝¹ toFun✝¹
map_mul'✝¹ :
  ∀ (x y : α),
    Equiv.toFun { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } (x * y) =
      Equiv.toFun { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } x *
        Equiv.toFun { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } y
map_add'✝¹ :
  ∀ (x y : α),
    Equiv.toFun { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } (x + y) =
      Equiv.toFun { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } x +
        Equiv.toFun { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } y
map_le_map_iff'✝¹ :
  ∀ {a b : α},
    Equiv.toFun
          { toEquiv := { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
              map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ }.toEquiv
          a ≤
        Equiv.toFun
          { toEquiv := { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
              map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ }.toEquiv
          b ↔
      a ≤ b
toFun✝ : α → β
invFun✝ : β → α
left_inv✝ : LeftInverse invFun✝ toFun✝
right_inv✝ : Function.RightInverse invFun✝ toFun✝
map_mul'✝ :
  ∀ (x y : α),
    Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } (x * y) =
      Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x *
        Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } y
map_add'✝ :
  ∀ (x y : α),
    Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } (x + y) =
      Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x +
        Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } y
map_le_map_iff'✝ :
  ∀ {a b : α},
    Equiv.toFun
          { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
              map_mul' := map_mul'✝, map_add' := map_add'✝ }.toEquiv
          a ≤
        Equiv.toFun
          { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
              map_mul' := map_mul'✝, map_add' := map_add'✝ }.toEquiv
          b ↔
      a ≤ b
h₁ :
  (fun f => f.toFun)
      {
        toRingEquiv :=
          { toEquiv := { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
            map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ },
        map_le_map_iff' := map_le_map_iff'✝¹ } =
    (fun f => f.toFun)
      {
        toRingEquiv :=
          { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
            map_mul' := map_mul'✝, map_add' := map_add'✝ },
        map_le_map_iff' := map_le_map_iff'✝ }
h₂ :
  (fun f => f.invFun)
      {
        toRingEquiv :=
          { toEquiv := { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
            map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ },
        map_le_map_iff' := map_le_map_iff'✝¹ } =
    (fun f => f.invFun)
      {
        toRingEquiv :=
          { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
            map_mul' := map_mul'✝, map_add' := map_add'✝ },
        map_le_map_iff' := map_le_map_iff'✝ }
⊢ {
      toRingEquiv :=
        { toEquiv := { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
          map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ },
      map_le_map_iff' := map_le_map_iff'✝¹ } =
    {
      toRingEquiv :=
        { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
          map_mul' := map_mul'✝, map_add' := map_add'✝ },
      map_le_map_iff' := map_le_map_iff'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹¹ : Mul α
inst✝¹⁰ : Add α
inst✝⁹ : LE α
inst✝⁸ : Mul β
inst✝⁷ : Add β
inst✝⁶ : LE β
inst✝⁵ : Mul γ
inst✝⁴ : Add γ
inst✝³ : LE γ
inst✝² : Mul δ
inst✝¹ : Add δ
inst✝ : LE δ
x : α
⊢ ↑(OrderRingIso.refl α) x = x
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹¹ : Mul α
inst✝¹⁰ : Add α
inst✝⁹ : LE α
inst✝⁸ : Mul β
inst✝⁷ : Add β
inst✝⁶ : LE β
inst✝⁵ : Mul γ
inst✝⁴ : Add γ
inst✝³ : LE γ
inst✝² : Mul δ
inst✝¹ : Add δ
inst✝ : LE δ
e : α ≃+*o β
⊢ ∀ {a b : β},
    Equiv.toFun (RingEquiv.symm e.toRingEquiv).toEquiv a ≤ Equiv.toFun (RingEquiv.symm e.toRingEquiv).toEquiv b ↔ a ≤ b
[PROOFSTEP]
intro a b
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹¹ : Mul α
inst✝¹⁰ : Add α
inst✝⁹ : LE α
inst✝⁸ : Mul β
inst✝⁷ : Add β
inst✝⁶ : LE β
inst✝⁵ : Mul γ
inst✝⁴ : Add γ
inst✝³ : LE γ
inst✝² : Mul δ
inst✝¹ : Add δ
inst✝ : LE δ
e : α ≃+*o β
a b : β
⊢ Equiv.toFun (RingEquiv.symm e.toRingEquiv).toEquiv a ≤ Equiv.toFun (RingEquiv.symm e.toRingEquiv).toEquiv b ↔ a ≤ b
[PROOFSTEP]
erw [← map_le_map_iff e, e.1.apply_symm_apply, e.1.apply_symm_apply]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁵ : NonAssocSemiring α
inst✝⁴ : Preorder α
inst✝³ : NonAssocSemiring β
inst✝² : Preorder β
inst✝¹ : NonAssocSemiring γ
inst✝ : Preorder γ
f g : α ≃+*o β
h : toOrderRingHom f = toOrderRingHom g
⊢ (fun f => ↑f) f = (fun f => ↑f) g
[PROOFSTEP]
convert FunLike.ext'_iff.1 h using 0
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
inst✝ : Archimedean β
f g : α →+*o β
⊢ f = g
[PROOFSTEP]
ext x
[GOAL]
case h
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
inst✝ : Archimedean β
f g : α →+*o β
x : α
⊢ ↑f x = ↑g x
[PROOFSTEP]
by_contra' h' : f x ≠ g x
[GOAL]
case h
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
inst✝ : Archimedean β
f g : α →+*o β
x : α
h' : ↑f x ≠ ↑g x
⊢ False
[PROOFSTEP]
wlog h : f x < g x generalizing α β with h₂
[GOAL]
case h.inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
inst✝ : Archimedean β
f g : α →+*o β
x : α
h' : ↑f x ≠ ↑g x
h₂ :
  ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrderedField α] [inst_1 : LinearOrderedField β] [inst_2 : Archimedean β]
    (f g : α →+*o β) (x : α), ↑f x ≠ ↑g x → ↑f x < ↑g x → False
h : ¬↑f x < ↑g x
⊢ False
[PROOFSTEP]
exact h₂ g f x (Ne.symm h') (h'.lt_or_lt.resolve_left h)
[GOAL]
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
inst✝ : Archimedean β
f g : α →+*o β
x : α
h' : ↑f x ≠ ↑g x
h : ↑f x < ↑g x
⊢ False
[PROOFSTEP]
obtain ⟨q, hf, hg⟩ := exists_rat_btwn h
[GOAL]
case intro.intro
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
inst✝ : Archimedean β
f g : α →+*o β
x : α
h' : ↑f x ≠ ↑g x
h : ↑f x < ↑g x
q : ℚ
hf : ↑f x < ↑q
hg : ↑q < ↑g x
⊢ False
[PROOFSTEP]
rw [← map_ratCast f] at hf
[GOAL]
case intro.intro
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
inst✝ : Archimedean β
f g : α →+*o β
x : α
h' : ↑f x ≠ ↑g x
h : ↑f x < ↑g x
q : ℚ
hf : ↑f x < ↑f ↑q
hg : ↑q < ↑g x
⊢ False
[PROOFSTEP]
rw [← map_ratCast g] at hg
[GOAL]
case intro.intro
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
inst✝ : Archimedean β
f g : α →+*o β
x : α
h' : ↑f x ≠ ↑g x
h : ↑f x < ↑g x
q : ℚ
hf : ↑f x < ↑f ↑q
hg : ↑g ↑q < ↑g x
⊢ False
[PROOFSTEP]
exact (lt_asymm ((OrderHomClass.mono g).reflect_lt hg) <| (OrderHomClass.mono f).reflect_lt hf).elim


[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b✝ c a b : α
⊢ |a * b| = |a| * |b|
[PROOFSTEP]
rw [abs_eq (mul_nonneg (abs_nonneg a) (abs_nonneg b))]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b✝ c a b : α
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)
[PROOFSTEP]
cases' le_total a 0 with ha ha
[GOAL]
case inl
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b✝ c a b : α
ha : a ≤ 0
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)
[PROOFSTEP]
cases' le_total b 0 with hb hb
[GOAL]
case inr
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b✝ c a b : α
ha : 0 ≤ a
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)
[PROOFSTEP]
cases' le_total b 0 with hb hb
[GOAL]
case inl.inl
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b✝ c a b : α
ha : a ≤ 0
hb : b ≤ 0
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)
[PROOFSTEP]
simp only [abs_of_nonpos, abs_of_nonneg, true_or_iff, or_true_iff, eq_self_iff_true, neg_mul, mul_neg, neg_neg, *]
[GOAL]
case inl.inr
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b✝ c a b : α
ha : a ≤ 0
hb : 0 ≤ b
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)
[PROOFSTEP]
simp only [abs_of_nonpos, abs_of_nonneg, true_or_iff, or_true_iff, eq_self_iff_true, neg_mul, mul_neg, neg_neg, *]
[GOAL]
case inr.inl
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b✝ c a b : α
ha : 0 ≤ a
hb : b ≤ 0
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)
[PROOFSTEP]
simp only [abs_of_nonpos, abs_of_nonneg, true_or_iff, or_true_iff, eq_self_iff_true, neg_mul, mul_neg, neg_neg, *]
[GOAL]
case inr.inr
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b✝ c a b : α
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)
[PROOFSTEP]
simp only [abs_of_nonpos, abs_of_nonneg, true_or_iff, or_true_iff, eq_self_iff_true, neg_mul, mul_neg, neg_neg, *]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b c a : α
⊢ |a * a| = a * a
[PROOFSTEP]
rw [abs_mul, abs_mul_abs_self]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
a b c : α
⊢ |a| = a ↔ 0 ≤ a
[PROOFSTEP]
simp [abs_eq_max_neg]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
a b c : α
⊢ |a| = -a ↔ a ≤ 0
[PROOFSTEP]
simp [abs_eq_max_neg]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b c a : α
⊢ |a| = a ∧ 0 ≤ a ∨ |a| = -a ∧ a < 0
[PROOFSTEP]
by_cases h : 0 ≤ a
[GOAL]
case pos
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b c a : α
h : 0 ≤ a
⊢ |a| = a ∧ 0 ≤ a ∨ |a| = -a ∧ a < 0
[PROOFSTEP]
left
[GOAL]
case pos.h
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b c a : α
h : 0 ≤ a
⊢ |a| = a ∧ 0 ≤ a
[PROOFSTEP]
exact ⟨abs_eq_self.mpr h, h⟩
[GOAL]
case neg
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b c a : α
h : ¬0 ≤ a
⊢ |a| = a ∧ 0 ≤ a ∨ |a| = -a ∧ a < 0
[PROOFSTEP]
right
[GOAL]
case neg.h
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b c a : α
h : ¬0 ≤ a
⊢ |a| = -a ∧ a < 0
[PROOFSTEP]
push_neg at h
[GOAL]
case neg.h
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b c a : α
h : a < 0
⊢ |a| = -a ∧ a < 0
[PROOFSTEP]
exact ⟨abs_eq_neg_self.mpr (le_of_lt h), h⟩
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b c a : α
⊢ max a 0 + max (-a) 0 = |a|
[PROOFSTEP]
symm
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b c a : α
⊢ |a| = max a 0 + max (-a) 0
[PROOFSTEP]
rcases le_total 0 a with (ha | ha)
[GOAL]
case inl
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b c a : α
ha : 0 ≤ a
⊢ |a| = max a 0 + max (-a) 0
[PROOFSTEP]
simp [ha]
[GOAL]
case inr
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b c a : α
ha : a ≤ 0
⊢ |a| = max a 0 + max (-a) 0
[PROOFSTEP]
simp [ha]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
a b c : α
⊢ |a| = |b| ↔ a * a = b * b
[PROOFSTEP]
rw [← abs_mul_abs_self, ← abs_mul_abs_self b]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
a b c : α
⊢ |a| = |b| ↔ |a| * |a| = |b| * |b|
[PROOFSTEP]
exact (mul_self_inj (abs_nonneg a) (abs_nonneg b)).symm
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
a b c : α
⊢ |a| < |b| ↔ a * a < b * b
[PROOFSTEP]
rw [← abs_mul_abs_self, ← abs_mul_abs_self b]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
a b c : α
⊢ |a| < |b| ↔ |a| * |a| < |b| * |b|
[PROOFSTEP]
exact mul_self_lt_mul_self_iff (abs_nonneg a) (abs_nonneg b)
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
a b c : α
⊢ |a| ≤ |b| ↔ a * a ≤ b * b
[PROOFSTEP]
rw [← abs_mul_abs_self, ← abs_mul_abs_self b]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
a b c : α
⊢ |a| ≤ |b| ↔ |a| * |a| ≤ |b| * |b|
[PROOFSTEP]
exact mul_self_le_mul_self_iff (abs_nonneg a) (abs_nonneg b)
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
a b c : α
⊢ |a| ≤ 1 ↔ a * a ≤ 1
[PROOFSTEP]
simpa only [abs_one, one_mul] using @abs_le_iff_mul_self_le α _ a 1
[GOAL]
α : Type u_1
inst✝ : LinearOrderedCommRing α
a✝ b✝ c d a b : α
⊢ |a - b| * |a - b| = a * a + b * b - (1 + 1) * a * b
[PROOFSTEP]
rw [abs_mul_abs_self]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedCommRing α
a✝ b✝ c d a b : α
⊢ (a - b) * (a - b) = a * a + b * b - (1 + 1) * a * b
[PROOFSTEP]
simp only [mul_add, add_comm, add_left_comm, mul_comm, sub_eq_add_neg, mul_one, mul_neg, neg_add_rev, neg_neg,
  add_assoc]
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : LinearOrder α
a✝ b✝ a b : α
⊢ |a| ∣ b ↔ a ∣ b
[PROOFSTEP]
cases' abs_choice a with h h
[GOAL]
case inl
α : Type u_1
inst✝¹ : Ring α
inst✝ : LinearOrder α
a✝ b✝ a b : α
h : |a| = a
⊢ |a| ∣ b ↔ a ∣ b
[PROOFSTEP]
simp only [h, neg_dvd]
[GOAL]
case inr
α : Type u_1
inst✝¹ : Ring α
inst✝ : LinearOrder α
a✝ b✝ a b : α
h : |a| = -a
⊢ |a| ∣ b ↔ a ∣ b
[PROOFSTEP]
simp only [h, neg_dvd]
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : LinearOrder α
a✝ b✝ a b : α
⊢ a ∣ |b| ↔ a ∣ b
[PROOFSTEP]
cases' abs_choice b with h h
[GOAL]
case inl
α : Type u_1
inst✝¹ : Ring α
inst✝ : LinearOrder α
a✝ b✝ a b : α
h : |b| = b
⊢ a ∣ |b| ↔ a ∣ b
[PROOFSTEP]
simp only [h, dvd_neg]
[GOAL]
case inr
α : Type u_1
inst✝¹ : Ring α
inst✝ : LinearOrder α
a✝ b✝ a b : α
h : |b| = -b
⊢ a ∣ |b| ↔ a ∣ b
[PROOFSTEP]
simp only [h, dvd_neg]


[GOAL]
α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : Preorder α
inst✝¹ : ZeroLEOneClass α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ 0 ≤ 2
[PROOFSTEP]
rw [← one_add_one_eq_two]
[GOAL]
α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : Preorder α
inst✝¹ : ZeroLEOneClass α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ 0 ≤ 1 + 1
[PROOFSTEP]
exact add_nonneg zero_le_one zero_le_one
[GOAL]
α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : Preorder α
inst✝¹ : ZeroLEOneClass α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ 0 ≤ 3
[PROOFSTEP]
rw [← two_add_one_eq_three]
[GOAL]
α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : Preorder α
inst✝¹ : ZeroLEOneClass α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ 0 ≤ 2 + 1
[PROOFSTEP]
exact add_nonneg zero_le_two zero_le_one
[GOAL]
α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : Preorder α
inst✝¹ : ZeroLEOneClass α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ 0 ≤ 4
[PROOFSTEP]
rw [← three_add_one_eq_four]
[GOAL]
α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : Preorder α
inst✝¹ : ZeroLEOneClass α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ 0 ≤ 3 + 1
[PROOFSTEP]
exact add_nonneg zero_le_three zero_le_one
[GOAL]
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : ZeroLEOneClass α
inst✝¹ : NeZero 1
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ 0 < 3
[PROOFSTEP]
rw [← two_add_one_eq_three]
[GOAL]
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : ZeroLEOneClass α
inst✝¹ : NeZero 1
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ 0 < 2 + 1
[PROOFSTEP]
exact lt_add_of_lt_of_nonneg zero_lt_two zero_le_one
[GOAL]
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : ZeroLEOneClass α
inst✝¹ : NeZero 1
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ 0 < 4
[PROOFSTEP]
rw [← three_add_one_eq_four]
[GOAL]
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : ZeroLEOneClass α
inst✝¹ : NeZero 1
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ 0 < 3 + 1
[PROOFSTEP]
exact lt_add_of_lt_of_nonneg zero_lt_three zero_le_one
[GOAL]
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : ZeroLEOneClass α
inst✝¹ : NeZero 1
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
⊢ 1 < 2
[PROOFSTEP]
rw [← one_add_one_eq_two]
[GOAL]
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : ZeroLEOneClass α
inst✝¹ : NeZero 1
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
⊢ 1 < 1 + 1
[PROOFSTEP]
exact lt_add_one _


[GOAL]
α : Type u
β : Type u_1
inst✝¹ : StrictOrderedSemiring α
a b c d : α
inst✝ : ExistsAddOfLE α
hab : a ≤ b
hcd : c ≤ d
⊢ a * d + b * c ≤ a * c + b * d
[PROOFSTEP]
obtain ⟨b, rfl⟩ := exists_add_of_le hab
[GOAL]
case intro
α : Type u
β : Type u_1
inst✝¹ : StrictOrderedSemiring α
a c d : α
inst✝ : ExistsAddOfLE α
hcd : c ≤ d
b : α
hab : a ≤ a + b
⊢ a * d + (a + b) * c ≤ a * c + (a + b) * d
[PROOFSTEP]
obtain ⟨d, rfl⟩ := exists_add_of_le hcd
[GOAL]
case intro.intro
α : Type u
β : Type u_1
inst✝¹ : StrictOrderedSemiring α
a c : α
inst✝ : ExistsAddOfLE α
b : α
hab : a ≤ a + b
d : α
hcd : c ≤ c + d
⊢ a * (c + d) + (a + b) * c ≤ a * c + (a + b) * (c + d)
[PROOFSTEP]
rw [mul_add, add_right_comm, mul_add, ← add_assoc]
[GOAL]
case intro.intro
α : Type u
β : Type u_1
inst✝¹ : StrictOrderedSemiring α
a c : α
inst✝ : ExistsAddOfLE α
b : α
hab : a ≤ a + b
d : α
hcd : c ≤ c + d
⊢ a * c + (a + b) * c + a * d ≤ a * c + (a + b) * c + (a + b) * d
[PROOFSTEP]
exact add_le_add_left (mul_le_mul_of_nonneg_right hab <| (le_add_iff_nonneg_right _).1 hcd) _
[GOAL]
α : Type u
β : Type u_1
inst✝¹ : StrictOrderedSemiring α
a b c d : α
inst✝ : ExistsAddOfLE α
hba : b ≤ a
hdc : d ≤ c
⊢ a • d + b • c ≤ a • c + b • d
[PROOFSTEP]
rw [add_comm (a • d), add_comm (a • c)]
[GOAL]
α : Type u
β : Type u_1
inst✝¹ : StrictOrderedSemiring α
a b c d : α
inst✝ : ExistsAddOfLE α
hba : b ≤ a
hdc : d ≤ c
⊢ b • c + a • d ≤ b • d + a • c
[PROOFSTEP]
exact mul_add_mul_le_mul_add_mul hba hdc
[GOAL]
α : Type u
β : Type u_1
inst✝¹ : StrictOrderedSemiring α
a b c d : α
inst✝ : ExistsAddOfLE α
hab : a < b
hcd : c < d
⊢ a * d + b * c < a * c + b * d
[PROOFSTEP]
obtain ⟨b, rfl⟩ := exists_add_of_le hab.le
[GOAL]
case intro
α : Type u
β : Type u_1
inst✝¹ : StrictOrderedSemiring α
a c d : α
inst✝ : ExistsAddOfLE α
hcd : c < d
b : α
hab : a < a + b
⊢ a * d + (a + b) * c < a * c + (a + b) * d
[PROOFSTEP]
obtain ⟨d, rfl⟩ := exists_add_of_le hcd.le
[GOAL]
case intro.intro
α : Type u
β : Type u_1
inst✝¹ : StrictOrderedSemiring α
a c : α
inst✝ : ExistsAddOfLE α
b : α
hab : a < a + b
d : α
hcd : c < c + d
⊢ a * (c + d) + (a + b) * c < a * c + (a + b) * (c + d)
[PROOFSTEP]
rw [mul_add, add_right_comm, mul_add, ← add_assoc]
[GOAL]
case intro.intro
α : Type u
β : Type u_1
inst✝¹ : StrictOrderedSemiring α
a c : α
inst✝ : ExistsAddOfLE α
b : α
hab : a < a + b
d : α
hcd : c < c + d
⊢ a * c + (a + b) * c + a * d < a * c + (a + b) * c + (a + b) * d
[PROOFSTEP]
exact add_lt_add_left (mul_lt_mul_of_pos_right hab <| (lt_add_iff_pos_right _).1 hcd) _
[GOAL]
α : Type u
β : Type u_1
inst✝¹ : StrictOrderedSemiring α
a b c d : α
inst✝ : ExistsAddOfLE α
hba : b < a
hdc : d < c
⊢ a • d + b • c < a • c + b • d
[PROOFSTEP]
rw [add_comm (a • d), add_comm (a • c)]
[GOAL]
α : Type u
β : Type u_1
inst✝¹ : StrictOrderedSemiring α
a b c d : α
inst✝ : ExistsAddOfLE α
hba : b < a
hdc : d < c
⊢ b • c + a • d < b • d + a • c
[PROOFSTEP]
exact mul_add_mul_lt_mul_add_mul hba hdc
[GOAL]
α : Type u
β : Type u_1
inst✝ : CanonicallyOrderedCommSemiring α
a b : α
⊢ CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
[PROOFSTEP]
refine' ⟨fun a b c h => _⟩
[GOAL]
α : Type u
β : Type u_1
inst✝ : CanonicallyOrderedCommSemiring α
a✝ b✝ a b c : α
h : b ≤ c
⊢ a * b ≤ a * c
[PROOFSTEP]
rcases exists_add_of_le h with ⟨c, rfl⟩
[GOAL]
case intro
α : Type u
β : Type u_1
inst✝ : CanonicallyOrderedCommSemiring α
a✝ b✝ a b c : α
h : b ≤ b + c
⊢ a * b ≤ a * (b + c)
[PROOFSTEP]
rw [mul_add]
[GOAL]
case intro
α : Type u
β : Type u_1
inst✝ : CanonicallyOrderedCommSemiring α
a✝ b✝ a b c : α
h : b ≤ b + c
⊢ a * b ≤ a * b + a * c
[PROOFSTEP]
apply self_le_add_right
[GOAL]
α : Type u
β : Type u_1
inst✝ : CanonicallyOrderedCommSemiring α
a b : α
⊢ 0 < a * b ↔ 0 < a ∧ 0 < b
[PROOFSTEP]
simp only [pos_iff_ne_zero, ne_eq, mul_eq_zero, not_or]
[GOAL]
α : Type u
β : Type u_1
inst✝³ : CanonicallyOrderedCommSemiring α
a b c : α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : IsTotal α fun x x_1 => x ≤ x_1
h : AddLECancellable (a * c)
⊢ a * (b - c) = a * b - a * c
[PROOFSTEP]
cases' total_of (· ≤ ·) b c with hbc hcb
[GOAL]
case inl
α : Type u
β : Type u_1
inst✝³ : CanonicallyOrderedCommSemiring α
a b c : α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : IsTotal α fun x x_1 => x ≤ x_1
h : AddLECancellable (a * c)
hbc : b ≤ c
⊢ a * (b - c) = a * b - a * c
[PROOFSTEP]
rw [tsub_eq_zero_iff_le.2 hbc, mul_zero, tsub_eq_zero_iff_le.2 (mul_le_mul_left' hbc a)]
[GOAL]
case inr
α : Type u
β : Type u_1
inst✝³ : CanonicallyOrderedCommSemiring α
a b c : α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : IsTotal α fun x x_1 => x ≤ x_1
h : AddLECancellable (a * c)
hcb : c ≤ b
⊢ a * (b - c) = a * b - a * c
[PROOFSTEP]
apply h.eq_tsub_of_add_eq
[GOAL]
case inr
α : Type u
β : Type u_1
inst✝³ : CanonicallyOrderedCommSemiring α
a b c : α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : IsTotal α fun x x_1 => x ≤ x_1
h : AddLECancellable (a * c)
hcb : c ≤ b
⊢ a * (b - c) + a * c = a * b
[PROOFSTEP]
rw [← mul_add, tsub_add_cancel_of_le hcb]
[GOAL]
α : Type u
β : Type u_1
inst✝³ : CanonicallyOrderedCommSemiring α
a b c : α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : IsTotal α fun x x_1 => x ≤ x_1
h : AddLECancellable (b * c)
⊢ (a - b) * c = a * c - b * c
[PROOFSTEP]
simp only [mul_comm _ c] at *
[GOAL]
α : Type u
β : Type u_1
inst✝³ : CanonicallyOrderedCommSemiring α
a b c : α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : IsTotal α fun x x_1 => x ≤ x_1
h : AddLECancellable (c * b)
⊢ c * (a - b) = c * a - c * b
[PROOFSTEP]
exact h.mul_tsub