-- Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
theorem mul_nonneg_of_three [ExistsAddOfLE α] [MulPosStrictMono α] [PosMulStrictMono α]
    [AddLeftMono α] [AddLeftReflectLE α]
    (a b c : α) : 0 ≤ a * b ∨ 0 ≤ b * c ∨ 0 ≤ c * a

Proof state:
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : MulPosStrictMono α
inst✝² : PosMulStrictMono α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
a b c : α
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c ∧ 0 ≤ a ∨ c ≤ 0 ∧ a ≤ 0

Tactic:
have or_a := le_total 0 a

Result:
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : MulPosStrictMono α
inst✝² : PosMulStrictMono α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
a b c : α
or_a : 0 ≤ a ∨ a ≤ 0
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c ∧ 0 ≤ a ∨ c ≤ 0 ∧ a ≤ 0

Proof state:
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : MulPosStrictMono α
inst✝² : PosMulStrictMono α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
a b c : α
⊢ 0 ≤ a * b ∨ 0 ≤ b * c ∨ 0 ≤ c * a

Tactic:
iterate 3 rw [mul_nonneg_iff]

Result:
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : MulPosStrictMono α
inst✝² : PosMulStrictMono α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
a b c : α
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c ∧ 0 ≤ a ∨ c ≤ 0 ∧ a ≤ 0

Proof state:
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : MulPosStrictMono α
inst✝² : PosMulStrictMono α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
a b c : α
or_a : 0 ≤ a ∨ a ≤ 0
or_b : 0 ≤ b ∨ b ≤ 0
or_c : 0 ≤ c ∨ c ≤ 0
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c ∧ 0 ≤ a ∨ c ≤ 0 ∧ a ≤ 0

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : MulPosStrictMono α
inst✝² : PosMulStrictMono α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
a b c : α
or_a : 0 ≤ a ∨ a ≤ 0
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c ∧ 0 ≤ a ∨ c ≤ 0 ∧ a ≤ 0

Tactic:
have or_b := le_total 0 b

Result:
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : MulPosStrictMono α
inst✝² : PosMulStrictMono α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
a b c : α
or_a : 0 ≤ a ∨ a ≤ 0
or_b : 0 ≤ b ∨ b ≤ 0
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c ∧ 0 ≤ a ∨ c ≤ 0 ∧ a ≤ 0

Proof state:
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : MulPosStrictMono α
inst✝² : PosMulStrictMono α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
a b c : α
or_a : 0 ≤ a ∨ a ≤ 0
or_b : 0 ≤ b ∨ b ≤ 0
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c ∧ 0 ≤ a ∨ c ≤ 0 ∧ a ≤ 0

Tactic:
have or_c := le_total 0 c

Result:
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : MulPosStrictMono α
inst✝² : PosMulStrictMono α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
a b c : α
or_a : 0 ≤ a ∨ a ≤ 0
or_b : 0 ≤ b ∨ b ≤ 0
or_c : 0 ≤ c ∨ c ≤ 0
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c ∧ 0 ≤ a ∨ c ≤ 0 ∧ a ≤ 0

Proof state:
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : MulPosStrictMono α
inst✝² : PosMulStrictMono α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
a b c : α
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c * a

Tactic:
rw [mul_nonneg_iff]

Result:
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : MulPosStrictMono α
inst✝² : PosMulStrictMono α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
a b c : α
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c ∧ 0 ≤ a ∨ c ≤ 0 ∧ a ≤ 0