Theorem: verus_lemma_mul_ordering (VerusLeanStd/MulInternalsNonlinear.lean)

State before:
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
⊢ x * y ≥ x ∧ x * y ≥ y
Tactic:
have h' : ∀ x y : Int, x ≠ 0 → y ≠ 0 → 0 ≤ x * y → x * y ≥ x := by
  intros x y h1 h2 h3
  by_cases h4 : x > 0
  . apply le_mul_of_one_le_right (Int.nonneg_of_pos h4)
    have h5 : y < 0 ∨ 1 ≤ y := by
      rw [← Int.zero_add 1, Int.add_one_le_iff]
      exact Int.lt_or_gt_of_ne h2
    rcases h5 with h5 | h5
    . have := Int.mul_neg_of_pos_of_neg h4 h5
      linarith
    . exact h5
  . have h5 : x < 0 := by
      simp only [gt_iff_lt, not_lt] at h4
      exact lt_of_le_of_ne h4 h1
    linarith
State after:
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h' : ∀ (x y : ℤ), x ≠ 0 → y ≠ 0 → 0 ≤ x * y → x * y ≥ x
⊢ x * y ≥ x ∧ x * y ≥ y

State before:
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h' : ∀ (x y : ℤ), x ≠ 0 → y ≠ 0 → 0 ≤ x * y → x * y ≥ x
⊢ x * y ≥ x ∧ x * y ≥ y
Tactic:
constructor
State after:
case left
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h' : ∀ (x y : ℤ), x ≠ 0 → y ≠ 0 → 0 ≤ x * y → x * y ≥ x
⊢ x * y ≥ x

case right
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h' : ∀ (x y : ℤ), x ≠ 0 → y ≠ 0 → 0 ≤ x * y → x * y ≥ x
⊢ x * y ≥ y

State before:
case left
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h' : ∀ (x y : ℤ), x ≠ 0 → y ≠ 0 → 0 ≤ x * y → x * y ≥ x
⊢ x * y ≥ x

case right
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h' : ∀ (x y : ℤ), x ≠ 0 → y ≠ 0 → 0 ≤ x * y → x * y ≥ x
⊢ x * y ≥ y
Tactic:
. exact h' x y h1 h2 h3
State after:
case right
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h' : ∀ (x y : ℤ), x ≠ 0 → y ≠ 0 → 0 ≤ x * y → x * y ≥ x
⊢ x * y ≥ y

State before:
case right
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h' : ∀ (x y : ℤ), x ≠ 0 → y ≠ 0 → 0 ≤ x * y → x * y ≥ x
⊢ x * y ≥ y
Tactic:
. rw [mul_comm] at h3
  rw [mul_comm]
  exact h' y x h2 h1 h3
State after:
no goals

State before:
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
⊢ ∀ (x y : ℤ), x ≠ 0 → y ≠ 0 → 0 ≤ x * y → x * y ≥ x
Tactic:
intros x y h1 h2 h3
State after:
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
⊢ x * y ≥ x

State before:
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
⊢ x * y ≥ x
Tactic:
by_cases h4 : x > 0
State after:
case pos
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : x > 0
⊢ x * y ≥ x

case neg
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : ¬x > 0
⊢ x * y ≥ x

State before:
case pos
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : x > 0
⊢ x * y ≥ x

case neg
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : ¬x > 0
⊢ x * y ≥ x
Tactic:
. apply le_mul_of_one_le_right (Int.nonneg_of_pos h4)
  have h5 : y < 0 ∨ 1 ≤ y := by
    rw [← Int.zero_add 1, Int.add_one_le_iff]
    exact Int.lt_or_gt_of_ne h2
  rcases h5 with h5 | h5
  . have := Int.mul_neg_of_pos_of_neg h4 h5
    linarith
  . exact h5
State after:
case neg
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : ¬x > 0
⊢ x * y ≥ x

State before:
case neg
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : ¬x > 0
⊢ x * y ≥ x
Tactic:
. have h5 : x < 0 := by
    simp only [gt_iff_lt, not_lt] at h4
    exact lt_of_le_of_ne h4 h1
  linarith
State after:
no goals

State before:
case pos
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : x > 0
⊢ x * y ≥ x
Tactic:
apply le_mul_of_one_le_right (Int.nonneg_of_pos h4)
State after:
case pos
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : x > 0
⊢ 1 ≤ y

State before:
case pos
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : x > 0
⊢ 1 ≤ y
Tactic:
have h5 : y < 0 ∨ 1 ≤ y := by
  rw [← Int.zero_add 1, Int.add_one_le_iff]
  exact Int.lt_or_gt_of_ne h2
State after:
case pos
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : x > 0
h5 : y < 0 ∨ 1 ≤ y
⊢ 1 ≤ y

State before:
case pos
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : x > 0
h5 : y < 0 ∨ 1 ≤ y
⊢ 1 ≤ y
Tactic:
rcases h5 with h5 | h5
State after:
case pos.inl
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : x > 0
h5 : y < 0
⊢ 1 ≤ y

case pos.inr
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : x > 0
h5 : 1 ≤ y
⊢ 1 ≤ y

State before:
case pos.inl
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : x > 0
h5 : y < 0
⊢ 1 ≤ y

case pos.inr
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : x > 0
h5 : 1 ≤ y
⊢ 1 ≤ y
Tactic:
. have := Int.mul_neg_of_pos_of_neg h4 h5
  linarith
State after:
case pos.inr
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : x > 0
h5 : 1 ≤ y
⊢ 1 ≤ y

State before:
case pos.inr
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : x > 0
h5 : 1 ≤ y
⊢ 1 ≤ y
Tactic:
. exact h5
State after:
no goals

State before:
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : x > 0
⊢ y < 0 ∨ 1 ≤ y
Tactic:
rw [← Int.zero_add 1, Int.add_one_le_iff]
State after:
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : x > 0
⊢ y < 0 ∨ 0 < y

State before:
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : x > 0
⊢ y < 0 ∨ 0 < y
Tactic:
exact Int.lt_or_gt_of_ne h2
State after:
no goals

State before:
case pos.inl
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : x > 0
h5 : y < 0
⊢ 1 ≤ y
Tactic:
have := Int.mul_neg_of_pos_of_neg h4 h5
State after:
case pos.inl
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : x > 0
h5 : y < 0
this : x * y < 0
⊢ 1 ≤ y

State before:
case pos.inl
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : x > 0
h5 : y < 0
this : x * y < 0
⊢ 1 ≤ y
Tactic:
linarith
State after:
no goals

State before:
case pos.inr
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : x > 0
h5 : 1 ≤ y
⊢ 1 ≤ y
Tactic:
exact h5
State after:
no goals

State before:
case neg
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : ¬x > 0
⊢ x * y ≥ x
Tactic:
have h5 : x < 0 := by
  simp only [gt_iff_lt, not_lt] at h4
  exact lt_of_le_of_ne h4 h1
State after:
case neg
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : ¬x > 0
h5 : x < 0
⊢ x * y ≥ x

State before:
case neg
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : ¬x > 0
h5 : x < 0
⊢ x * y ≥ x
Tactic:
linarith
State after:
no goals

State before:
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : ¬x > 0
⊢ x < 0
Tactic:
simp only [gt_iff_lt, not_lt] at h4
State after:
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : x ≤ 0
⊢ x < 0

State before:
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : x ≤ 0
⊢ x < 0
Tactic:
exact lt_of_le_of_ne h4 h1
State after:
no goals

State before:
case left
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h' : ∀ (x y : ℤ), x ≠ 0 → y ≠ 0 → 0 ≤ x * y → x * y ≥ x
⊢ x * y ≥ x
Tactic:
exact h' x y h1 h2 h3
State after:
no goals

State before:
case right
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h' : ∀ (x y : ℤ), x ≠ 0 → y ≠ 0 → 0 ≤ x * y → x * y ≥ x
⊢ x * y ≥ y
Tactic:
rw [mul_comm] at h3
State after:
case right
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ y * x
h' : ∀ (x y : ℤ), x ≠ 0 → y ≠ 0 → 0 ≤ x * y → x * y ≥ x
⊢ x * y ≥ y

State before:
case right
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ y * x
h' : ∀ (x y : ℤ), x ≠ 0 → y ≠ 0 → 0 ≤ x * y → x * y ≥ x
⊢ x * y ≥ y
Tactic:
rw [mul_comm]
State after:
case right
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ y * x
h' : ∀ (x y : ℤ), x ≠ 0 → y ≠ 0 → 0 ≤ x * y → x * y ≥ x
⊢ y * x ≥ y

State before:
case right
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ y * x
h' : ∀ (x y : ℤ), x ≠ 0 → y ≠ 0 → 0 ≤ x * y → x * y ≥ x
⊢ y * x ≥ y
Tactic:
exact h' y x h2 h1 h3
State after:
no goals