[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
