no goals
a b c : Int
h₁ : a ≤ b
h₂ : 0 ≤ c
⊢ c * a ≤ c * b
if hba : b ≤ a then rw [Int.le_antisymm hba h₁]; apply Int.le_refl else
if hc0 : c ≤ 0 then simp [Int.le_antisymm hc0 h₂, Int.zero_mul] else
exact Int.le_of_lt <| Int.mul_lt_mul_of_pos_left
  (Int.lt_iff_le_not_le.2 ⟨h₁, hba⟩) (Int.lt_iff_le_not_le.2 ⟨h₂, hc0⟩)
a b c : Int
h₁ : a ≤ b
h₂ : 0 ≤ c
hba : b ≤ a
⊢ c * a ≤ c * a
a b c : Int
h₁ : a ≤ b
h₂ : 0 ≤ c
hba : b ≤ a
⊢ c * a ≤ c * b
rw [Int.le_antisymm hba h₁]
no goals
a b c : Int
h₁ : a ≤ b
h₂ : 0 ≤ c
hba : b ≤ a
⊢ c * a ≤ c * a
apply Int.le_refl
no goals
a b c : Int
h₁ : a ≤ b
h₂ : 0 ≤ c
hba : ¬b ≤ a
⊢ c * a ≤ c * b
if hc0 : c ≤ 0 then simp [Int.le_antisymm hc0 h₂, Int.zero_mul] else
exact Int.le_of_lt <| Int.mul_lt_mul_of_pos_left
  (Int.lt_iff_le_not_le.2 ⟨h₁, hba⟩) (Int.lt_iff_le_not_le.2 ⟨h₂, hc0⟩)
no goals
a b c : Int
h₁ : a ≤ b
h₂ : 0 ≤ c
hba : ¬b ≤ a
hc0 : c ≤ 0
⊢ c * a ≤ c * b
simp [Int.le_antisymm hc0 h₂, Int.zero_mul]
no goals
a b c : Int
h₁ : a ≤ b
h₂ : 0 ≤ c
hba : ¬b ≤ a
hc0 : ¬c ≤ 0
⊢ c * a ≤ c * b
exact Int.le_of_lt <| Int.mul_lt_mul_of_pos_left
  (Int.lt_iff_le_not_le.2 ⟨h₁, hba⟩) (Int.lt_iff_le_not_le.2 ⟨h₂, hc0⟩)