α : Type u
β : Type ?u.180652
inst✝ : LinearOrderedRing α
a✝ b✝ c✝ 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
α : Type u
β : Type ?u.180652
inst✝ : LinearOrderedRing α
a✝ b✝ c✝ a b c : α
⊢ 0 ≤ a * b ∨ 0 ≤ b * c ∨ 0 ≤ c * a
iterate 3 rw [mul_nonneg_iff]
α : Type u
β : Type ?u.180652
inst✝ : LinearOrderedRing α
a✝ b✝ c✝ 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
α : Type u
β : Type ?u.180652
inst✝ : LinearOrderedRing α
a✝ b✝ c✝ 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
have or_a := le_total 0 a
α : Type u
β : Type ?u.180652
inst✝ : LinearOrderedRing α
a✝ b✝ c✝ 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
α : Type u
β : Type ?u.180652
inst✝ : LinearOrderedRing α
a✝ b✝ c✝ 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
have or_b := le_total 0 b
α : Type u
β : Type ?u.180652
inst✝ : LinearOrderedRing α
a✝ b✝ c✝ 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
α : Type u
β : Type ?u.180652
inst✝ : LinearOrderedRing α
a✝ b✝ c✝ 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
have or_c := le_total 0 c
no goals
α : Type u
β : Type ?u.180652
inst✝ : LinearOrderedRing α
a✝ b✝ c✝ 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
exact Or.elim or_c
  (fun (h0 : 0 ≤ c) =>
    Or.elim or_b
      (fun (h1 : 0 ≤ b) =>
          Or.elim or_a (fun (h2 : 0 ≤ a) => Or.inl (Or.inl ⟨h2, h1⟩))
            (fun (_ : a ≤ 0) => Or.inr (Or.inl (Or.inl ⟨h1, h0⟩))))
      (fun (h1 : b ≤ 0) =>
          Or.elim or_a (fun (h3 : 0 ≤ a) => Or.inr (Or.inr (Or.inl ⟨h0, h3⟩)))
            (fun (h3 : a ≤ 0) => Or.inl (Or.inr ⟨h3, h1⟩))))
  (fun (h0 : c ≤ 0) =>
    Or.elim or_b
      (fun (h4 : 0 ≤ b) =>
          Or.elim or_a (fun (h5 : 0 ≤ a) => Or.inl (Or.inl ⟨h5, h4⟩))
            (fun (h5 : a ≤ 0) => Or.inr (Or.inr (Or.inr ⟨h0, h5⟩))))
      (fun (h4 : b ≤ 0) =>
          Or.elim or_a (fun (_ : 0 ≤ a) => Or.inr (Or.inl (Or.inr ⟨h4, h0⟩)))
            (fun (h6 : a ≤ 0) => Or.inl (Or.inr ⟨h6, h4⟩))))
α : Type u
β : Type ?u.180652
inst✝ : LinearOrderedRing α
a✝ b✝ c✝ 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
α : Type u
β : Type ?u.180652
inst✝ : LinearOrderedRing α
a✝ b✝ c✝ a b c : α
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c * a
rw [mul_nonneg_iff]