-- Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
theorem nonneg_and_nonneg_or_nonpos_and_nonpos_of_mul_nonneg
    [MulPosStrictMono α] [PosMulStrictMono α]
    (hab : 0 ≤ a * b) : 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

Proof state:
α : Type u
inst✝³ : Semiring α
inst✝² : LinearOrder α
a b : α
inst✝¹ : MulPosStrictMono α
inst✝ : PosMulStrictMono α
hab : 0 ≤ a * b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
⊢ a * b < 0

Tactic:
rcases lt_trichotomy 0 a with (ha | rfl | ha)

Result:
case inl
α : Type u
inst✝³ : Semiring α
inst✝² : LinearOrder α
a b : α
inst✝¹ : MulPosStrictMono α
inst✝ : PosMulStrictMono α
hab : 0 ≤ a * b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
ha : 0 < a
⊢ a * b < 0

case inr.inl
α : Type u
inst✝³ : Semiring α
inst✝² : LinearOrder α
b : α
inst✝¹ : MulPosStrictMono α
inst✝ : PosMulStrictMono α
hab : 0 ≤ 0 * b
ab : 0 ≤ 0 → b < 0
nab : 0 ≤ 0 → 0 < b
⊢ 0 * b < 0

case inr.inr
α : Type u
inst✝³ : Semiring α
inst✝² : LinearOrder α
a b : α
inst✝¹ : MulPosStrictMono α
inst✝ : PosMulStrictMono α
hab : 0 ≤ a * b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
ha : a < 0
⊢ a * b < 0

Proof state:
case inr.inl
α : Type u
inst✝³ : Semiring α
inst✝² : LinearOrder α
b : α
inst✝¹ : MulPosStrictMono α
inst✝ : PosMulStrictMono α
hab : 0 ≤ 0 * b
ab : 0 ≤ 0 → b < 0
nab : 0 ≤ 0 → 0 < b
⊢ 0 * b < 0

Tactic:
exact ((ab le_rfl).asymm (nab le_rfl)).elim

Result:
no goals

Proof state:
α : Type u
inst✝³ : Semiring α
inst✝² : LinearOrder α
a b : α
inst✝¹ : MulPosStrictMono α
inst✝ : PosMulStrictMono α
hab : 0 ≤ a * b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
⊢ False

Tactic:
apply not_lt_of_le hab _

Result:
α : Type u
inst✝³ : Semiring α
inst✝² : LinearOrder α
a b : α
inst✝¹ : MulPosStrictMono α
inst✝ : PosMulStrictMono α
hab : 0 ≤ a * b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
⊢ a * b < 0

Proof state:
case inl
α : Type u
inst✝³ : Semiring α
inst✝² : LinearOrder α
a b : α
inst✝¹ : MulPosStrictMono α
inst✝ : PosMulStrictMono α
hab : 0 ≤ a * b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
ha : 0 < a
⊢ a * b < 0

Tactic:
exact mul_neg_of_pos_of_neg ha (ab ha.le)

Result:
no goals

Proof state:
α : Type u
inst✝³ : Semiring α
inst✝² : LinearOrder α
a b : α
inst✝¹ : MulPosStrictMono α
inst✝ : PosMulStrictMono α
hab : 0 ≤ a * b
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

Tactic:
refine Decidable.or_iff_not_and_not.2 ?_

Result:
α : Type u
inst✝³ : Semiring α
inst✝² : LinearOrder α
a b : α
inst✝¹ : MulPosStrictMono α
inst✝ : PosMulStrictMono α
hab : 0 ≤ a * b
⊢ ¬(¬(0 ≤ a ∧ 0 ≤ b) ∧ ¬(a ≤ 0 ∧ b ≤ 0))

Proof state:
α : Type u
inst✝³ : Semiring α
inst✝² : LinearOrder α
a b : α
inst✝¹ : MulPosStrictMono α
inst✝ : PosMulStrictMono α
hab : 0 ≤ a * b
⊢ ¬(¬(0 ≤ a ∧ 0 ≤ b) ∧ ¬(a ≤ 0 ∧ b ≤ 0))

Tactic:
simp only [not_and, not_le]

Result:
α : Type u
inst✝³ : Semiring α
inst✝² : LinearOrder α
a b : α
inst✝¹ : MulPosStrictMono α
inst✝ : PosMulStrictMono α
hab : 0 ≤ a * b
⊢ (0 ≤ a → b < 0) → ¬(a ≤ 0 → 0 < b)

Proof state:
case inr.inr
α : Type u
inst✝³ : Semiring α
inst✝² : LinearOrder α
a b : α
inst✝¹ : MulPosStrictMono α
inst✝ : PosMulStrictMono α
hab : 0 ≤ a * b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
ha : a < 0
⊢ a * b < 0

Tactic:
exact mul_neg_of_neg_of_pos ha (nab ha.le)

Result:
no goals

Proof state:
α : Type u
inst✝³ : Semiring α
inst✝² : LinearOrder α
a b : α
inst✝¹ : MulPosStrictMono α
inst✝ : PosMulStrictMono α
hab : 0 ≤ a * b
⊢ (0 ≤ a → b < 0) → ¬(a ≤ 0 → 0 < b)

Tactic:
intro ab nab

Result:
α : Type u
inst✝³ : Semiring α
inst✝² : LinearOrder α
a b : α
inst✝¹ : MulPosStrictMono α
inst✝ : PosMulStrictMono α
hab : 0 ≤ a * b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
⊢ False