awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
symm : ∀ {x y : EReal} (h : 0 < x * y ↔ 0 < x ∧ 0 < y ∨ x < 0 ∧ y < 0), 0 < y * x ↔ 0 < y ∧ 0 < x ∨ y < 0 ∧ x < 0
top_top :
  0 < HMul.hMul (α := EReal) ⊤ ⊤ ↔
    LT.lt (α := EReal) 0 ⊤ ∧ LT.lt (α := EReal) 0 ⊤ ∨ LT.lt (α := EReal) ⊤ 0 ∧ LT.lt (α := EReal) ⊤ 0
top_pos :
  ∀ (x : ℝ) (hx : 0 < x),
    0 < ⊤ * (↑x : EReal) ↔ LT.lt (α := EReal) 0 ⊤ ∧ 0 < (↑x : EReal) ∨ LT.lt (α := EReal) ⊤ 0 ∧ (↑x : EReal) < 0
top_zero :
  0 < HMul.hMul (α := EReal) ⊤ 0 ↔
    LT.lt (α := EReal) 0 ⊤ ∧ LT.lt (α := EReal) 0 0 ∨ LT.lt (α := EReal) ⊤ 0 ∧ LT.lt (α := EReal) 0 0
top_neg :
  ∀ (x : ℝ) (hx : x < 0),
    0 < ⊤ * (↑x : EReal) ↔ LT.lt (α := EReal) 0 ⊤ ∧ 0 < (↑x : EReal) ∨ LT.lt (α := EReal) ⊤ 0 ∧ (↑x : EReal) < 0
top_bot :
  0 < HMul.hMul (α := EReal) ⊤ ⊥ ↔
    LT.lt (α := EReal) 0 ⊤ ∧ LT.lt (α := EReal) 0 ⊥ ∨ LT.lt (α := EReal) ⊤ 0 ∧ LT.lt (α := EReal) ⊥ 0
⊢ 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
have pos_bot : ∀ (x : ℝ) (hx : 0 < x),
  0 < (↑x : EReal) * ⊥ ↔ 0 < (↑x : EReal) ∧ LT.lt (α := EReal) 0 ⊥ ∨ (↑x : EReal) < 0 ∧ LT.lt (α := EReal) ⊥ 0
Tactic: induction a, b using EReal.induction₂_symm with
  | symm h => simp [EReal.mul_comm, h, and_comm]
  | top_top => simp
  | top_pos _ hx => simp [EReal.top_mul_coe_of_pos hx, hx]
  | top_zero => simp
  | top_neg _ hx => simp [hx, EReal.top_mul_coe_of_neg hx, le_of_lt]
  | top_bot => simp
  | pos_bot _ hx => simp [hx, EReal.coe_mul_bot_of_pos hx, le_of_lt]
  | coe_coe x y => simp [← coe_mul, _root_.mul_pos_iff]
  | zero_bot => simp
  | neg_bot _ hx => simp [hx, EReal.coe_mul_bot_of_neg hx]
  | bot_bot => simp
Cleared hypotheses: a, b
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
symm : ∀ {x y : EReal} (h : 0 < x * y ↔ 0 < x ∧ 0 < y ∨ x < 0 ∧ y < 0), 0 < y * x ↔ 0 < y ∧ 0 < x ∨ y < 0 ∧ x < 0
top_top :
  0 < HMul.hMul (α := EReal) ⊤ ⊤ ↔
    LT.lt (α := EReal) 0 ⊤ ∧ LT.lt (α := EReal) 0 ⊤ ∨ LT.lt (α := EReal) ⊤ 0 ∧ LT.lt (α := EReal) ⊤ 0
top_pos :
  ∀ (x : ℝ) (hx : 0 < x),
    0 < ⊤ * (↑x : EReal) ↔ LT.lt (α := EReal) 0 ⊤ ∧ 0 < (↑x : EReal) ∨ LT.lt (α := EReal) ⊤ 0 ∧ (↑x : EReal) < 0
top_zero :
  0 < HMul.hMul (α := EReal) ⊤ 0 ↔
    LT.lt (α := EReal) 0 ⊤ ∧ LT.lt (α := EReal) 0 0 ∨ LT.lt (α := EReal) ⊤ 0 ∧ LT.lt (α := EReal) 0 0
top_neg :
  ∀ (x : ℝ) (hx : x < 0),
    0 < ⊤ * (↑x : EReal) ↔ LT.lt (α := EReal) 0 ⊤ ∧ 0 < (↑x : EReal) ∨ LT.lt (α := EReal) ⊤ 0 ∧ (↑x : EReal) < 0
top_bot :
  0 < HMul.hMul (α := EReal) ⊤ ⊥ ↔
    LT.lt (α := EReal) 0 ⊤ ∧ LT.lt (α := EReal) 0 ⊥ ∨ LT.lt (α := EReal) ⊤ 0 ∧ LT.lt (α := EReal) ⊥ 0
pos_bot :
  ∀ (x : ℝ) (hx : 0 < x),
    0 < (↑x : EReal) * ⊥ ↔ 0 < (↑x : EReal) ∧ LT.lt (α := EReal) 0 ⊥ ∨ (↑x : EReal) < 0 ∧ LT.lt (α := EReal) ⊥ 0
⊢ 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
have coe_coe : ∀ (x y : ℝ), 0 < (↑x : EReal) * (↑y : EReal) ↔ 0 < (↑x : EReal) ∧ 0 < (↑y : EReal) ∨ (↑x : EReal) < 0 ∧ (↑y : EReal) < 0
Tactic: induction a, b using EReal.induction₂_symm with
  | symm h => simp [EReal.mul_comm, h, and_comm]
  | top_top => simp
  | top_pos _ hx => simp [EReal.top_mul_coe_of_pos hx, hx]
  | top_zero => simp
  | top_neg _ hx => simp [hx, EReal.top_mul_coe_of_neg hx, le_of_lt]
  | top_bot => simp
  | pos_bot _ hx => simp [hx, EReal.coe_mul_bot_of_pos hx, le_of_lt]
  | coe_coe x y => simp [← coe_mul, _root_.mul_pos_iff]
  | zero_bot => simp
  | neg_bot _ hx => simp [hx, EReal.coe_mul_bot_of_neg hx]
  | bot_bot => simp
Cleared hypotheses: a, b
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
symm : ∀ {x y : EReal} (h : 0 < x * y ↔ 0 < x ∧ 0 < y ∨ x < 0 ∧ y < 0), 0 < y * x ↔ 0 < y ∧ 0 < x ∨ y < 0 ∧ x < 0
top_top :
  0 < HMul.hMul (α := EReal) ⊤ ⊤ ↔
    LT.lt (α := EReal) 0 ⊤ ∧ LT.lt (α := EReal) 0 ⊤ ∨ LT.lt (α := EReal) ⊤ 0 ∧ LT.lt (α := EReal) ⊤ 0
top_pos :
  ∀ (x : ℝ) (hx : 0 < x),
    0 < ⊤ * (↑x : EReal) ↔ LT.lt (α := EReal) 0 ⊤ ∧ 0 < (↑x : EReal) ∨ LT.lt (α := EReal) ⊤ 0 ∧ (↑x : EReal) < 0
top_zero :
  0 < HMul.hMul (α := EReal) ⊤ 0 ↔
    LT.lt (α := EReal) 0 ⊤ ∧ LT.lt (α := EReal) 0 0 ∨ LT.lt (α := EReal) ⊤ 0 ∧ LT.lt (α := EReal) 0 0
top_neg :
  ∀ (x : ℝ) (hx : x < 0),
    0 < ⊤ * (↑x : EReal) ↔ LT.lt (α := EReal) 0 ⊤ ∧ 0 < (↑x : EReal) ∨ LT.lt (α := EReal) ⊤ 0 ∧ (↑x : EReal) < 0
top_bot :
  0 < HMul.hMul (α := EReal) ⊤ ⊥ ↔
    LT.lt (α := EReal) 0 ⊤ ∧ LT.lt (α := EReal) 0 ⊥ ∨ LT.lt (α := EReal) ⊤ 0 ∧ LT.lt (α := EReal) ⊥ 0
pos_bot :
  ∀ (x : ℝ) (hx : 0 < x),
    0 < (↑x : EReal) * ⊥ ↔ 0 < (↑x : EReal) ∧ LT.lt (α := EReal) 0 ⊥ ∨ (↑x : EReal) < 0 ∧ LT.lt (α := EReal) ⊥ 0
coe_coe :
  ∀ (x y : ℝ),
    0 < (↑x : EReal) * (↑y : EReal) ↔ 0 < (↑x : EReal) ∧ 0 < (↑y : EReal) ∨ (↑x : EReal) < 0 ∧ (↑y : EReal) < 0
⊢ 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
have zero_bot : 0 < HMul.hMul (α := EReal) 0 ⊥ ↔
  LT.lt (α := EReal) 0 0 ∧ LT.lt (α := EReal) 0 ⊥ ∨ LT.lt (α := EReal) 0 0 ∧ LT.lt (α := EReal) ⊥ 0
Tactic: induction a, b using EReal.induction₂_symm with
  | symm h => simp [EReal.mul_comm, h, and_comm]
  | top_top => simp
  | top_pos _ hx => simp [EReal.top_mul_coe_of_pos hx, hx]
  | top_zero => simp
  | top_neg _ hx => simp [hx, EReal.top_mul_coe_of_neg hx, le_of_lt]
  | top_bot => simp
  | pos_bot _ hx => simp [hx, EReal.coe_mul_bot_of_pos hx, le_of_lt]
  | coe_coe x y => simp [← coe_mul, _root_.mul_pos_iff]
  | zero_bot => simp
  | neg_bot _ hx => simp [hx, EReal.coe_mul_bot_of_neg hx]
  | bot_bot => simp
Cleared hypotheses: a, b
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
symm : ∀ {x y : EReal} (h : 0 < x * y ↔ 0 < x ∧ 0 < y ∨ x < 0 ∧ y < 0), 0 < y * x ↔ 0 < y ∧ 0 < x ∨ y < 0 ∧ x < 0
top_top :
  0 < HMul.hMul (α := EReal) ⊤ ⊤ ↔
    LT.lt (α := EReal) 0 ⊤ ∧ LT.lt (α := EReal) 0 ⊤ ∨ LT.lt (α := EReal) ⊤ 0 ∧ LT.lt (α := EReal) ⊤ 0
top_pos :
  ∀ (x : ℝ) (hx : 0 < x),
    0 < ⊤ * (↑x : EReal) ↔ LT.lt (α := EReal) 0 ⊤ ∧ 0 < (↑x : EReal) ∨ LT.lt (α := EReal) ⊤ 0 ∧ (↑x : EReal) < 0
top_zero :
  0 < HMul.hMul (α := EReal) ⊤ 0 ↔
    LT.lt (α := EReal) 0 ⊤ ∧ LT.lt (α := EReal) 0 0 ∨ LT.lt (α := EReal) ⊤ 0 ∧ LT.lt (α := EReal) 0 0
top_neg :
  ∀ (x : ℝ) (hx : x < 0),
    0 < ⊤ * (↑x : EReal) ↔ LT.lt (α := EReal) 0 ⊤ ∧ 0 < (↑x : EReal) ∨ LT.lt (α := EReal) ⊤ 0 ∧ (↑x : EReal) < 0
top_bot :
  0 < HMul.hMul (α := EReal) ⊤ ⊥ ↔
    LT.lt (α := EReal) 0 ⊤ ∧ LT.lt (α := EReal) 0 ⊥ ∨ LT.lt (α := EReal) ⊤ 0 ∧ LT.lt (α := EReal) ⊥ 0
pos_bot :
  ∀ (x : ℝ) (hx : 0 < x),
    0 < (↑x : EReal) * ⊥ ↔ 0 < (↑x : EReal) ∧ LT.lt (α := EReal) 0 ⊥ ∨ (↑x : EReal) < 0 ∧ LT.lt (α := EReal) ⊥ 0
coe_coe :
  ∀ (x y : ℝ),
    0 < (↑x : EReal) * (↑y : EReal) ↔ 0 < (↑x : EReal) ∧ 0 < (↑y : EReal) ∨ (↑x : EReal) < 0 ∧ (↑y : EReal) < 0
zero_bot :
  0 < HMul.hMul (α := EReal) 0 ⊥ ↔
    LT.lt (α := EReal) 0 0 ∧ LT.lt (α := EReal) 0 ⊥ ∨ LT.lt (α := EReal) 0 0 ∧ LT.lt (α := EReal) ⊥ 0
⊢ 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
have neg_bot : ∀ (x : ℝ) (hx : x < 0),
  0 < (↑x : EReal) * ⊥ ↔ 0 < (↑x : EReal) ∧ LT.lt (α := EReal) 0 ⊥ ∨ (↑x : EReal) < 0 ∧ LT.lt (α := EReal) ⊥ 0
Tactic: induction a, b using EReal.induction₂_symm with
  | symm h => simp [EReal.mul_comm, h, and_comm]
  | top_top => simp
  | top_pos _ hx => simp [EReal.top_mul_coe_of_pos hx, hx]
  | top_zero => simp
  | top_neg _ hx => simp [hx, EReal.top_mul_coe_of_neg hx, le_of_lt]
  | top_bot => simp
  | pos_bot _ hx => simp [hx, EReal.coe_mul_bot_of_pos hx, le_of_lt]
  | coe_coe x y => simp [← coe_mul, _root_.mul_pos_iff]
  | zero_bot => simp
  | neg_bot _ hx => simp [hx, EReal.coe_mul_bot_of_neg hx]
  | bot_bot => simp
Cleared hypotheses: a, b
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
symm : ∀ {x y : EReal} (h : 0 < x * y ↔ 0 < x ∧ 0 < y ∨ x < 0 ∧ y < 0), 0 < y * x ↔ 0 < y ∧ 0 < x ∨ y < 0 ∧ x < 0
top_top :
  0 < HMul.hMul (α := EReal) ⊤ ⊤ ↔
    LT.lt (α := EReal) 0 ⊤ ∧ LT.lt (α := EReal) 0 ⊤ ∨ LT.lt (α := EReal) ⊤ 0 ∧ LT.lt (α := EReal) ⊤ 0
top_pos :
  ∀ (x : ℝ) (hx : 0 < x),
    0 < ⊤ * (↑x : EReal) ↔ LT.lt (α := EReal) 0 ⊤ ∧ 0 < (↑x : EReal) ∨ LT.lt (α := EReal) ⊤ 0 ∧ (↑x : EReal) < 0
top_zero :
  0 < HMul.hMul (α := EReal) ⊤ 0 ↔
    LT.lt (α := EReal) 0 ⊤ ∧ LT.lt (α := EReal) 0 0 ∨ LT.lt (α := EReal) ⊤ 0 ∧ LT.lt (α := EReal) 0 0
top_neg :
  ∀ (x : ℝ) (hx : x < 0),
    0 < ⊤ * (↑x : EReal) ↔ LT.lt (α := EReal) 0 ⊤ ∧ 0 < (↑x : EReal) ∨ LT.lt (α := EReal) ⊤ 0 ∧ (↑x : EReal) < 0
top_bot :
  0 < HMul.hMul (α := EReal) ⊤ ⊥ ↔
    LT.lt (α := EReal) 0 ⊤ ∧ LT.lt (α := EReal) 0 ⊥ ∨ LT.lt (α := EReal) ⊤ 0 ∧ LT.lt (α := EReal) ⊥ 0
pos_bot :
  ∀ (x : ℝ) (hx : 0 < x),
    0 < (↑x : EReal) * ⊥ ↔ 0 < (↑x : EReal) ∧ LT.lt (α := EReal) 0 ⊥ ∨ (↑x : EReal) < 0 ∧ LT.lt (α := EReal) ⊥ 0
coe_coe :
  ∀ (x y : ℝ),
    0 < (↑x : EReal) * (↑y : EReal) ↔ 0 < (↑x : EReal) ∧ 0 < (↑y : EReal) ∨ (↑x : EReal) < 0 ∧ (↑y : EReal) < 0
zero_bot :
  0 < HMul.hMul (α := EReal) 0 ⊥ ↔
    LT.lt (α := EReal) 0 0 ∧ LT.lt (α := EReal) 0 ⊥ ∨ LT.lt (α := EReal) 0 0 ∧ LT.lt (α := EReal) ⊥ 0
neg_bot :
  ∀ (x : ℝ) (hx : x < 0),
    0 < (↑x : EReal) * ⊥ ↔ 0 < (↑x : EReal) ∧ LT.lt (α := EReal) 0 ⊥ ∨ (↑x : EReal) < 0 ∧ LT.lt (α := EReal) ⊥ 0
⊢ 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
have bot_bot : 0 < HMul.hMul (α := EReal) ⊥ ⊥ ↔
  LT.lt (α := EReal) 0 ⊥ ∧ LT.lt (α := EReal) 0 ⊥ ∨ LT.lt (α := EReal) ⊥ 0 ∧ LT.lt (α := EReal) ⊥ 0
Tactic: induction a, b using EReal.induction₂_symm with
  | symm h => simp [EReal.mul_comm, h, and_comm]
  | top_top => simp
  | top_pos _ hx => simp [EReal.top_mul_coe_of_pos hx, hx]
  | top_zero => simp
  | top_neg _ hx => simp [hx, EReal.top_mul_coe_of_neg hx, le_of_lt]
  | top_bot => simp
  | pos_bot _ hx => simp [hx, EReal.coe_mul_bot_of_pos hx, le_of_lt]
  | coe_coe x y => simp [← coe_mul, _root_.mul_pos_iff]
  | zero_bot => simp
  | neg_bot _ hx => simp [hx, EReal.coe_mul_bot_of_neg hx]
  | bot_bot => simp
Cleared hypotheses: a, b
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
⊢ 0 ≤ a * b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
have simp_rw : (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔ (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
Tactic: simp_rw [le_iff_lt_or_eq, mul_pos_iff, zero_eq_mul (a := a)]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
⊢ (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
have inl : ∀ (h : a < 0),
  (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
Tactic: rcases lt_trichotomy a 0 with (h | h | h)
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
inl :
  ∀ (h : a < 0),
    (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
      (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
⊢ (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
have inr : ∀ (h : a = 0),
  (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
Tactic: rcases lt_trichotomy a 0 with (h | h | h)
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
inl :
  ∀ (h : a < 0),
    (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
      (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
inr :
  ∀ (h : a = 0),
    (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
      (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
⊢ (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
have inr₁ : ∀ (h : 0 < a),
  (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
Tactic: rcases lt_trichotomy a 0 with (h | h | h)
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
h : a < 0
⊢ (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
have inl : ∀ (h' : b < 0),
  (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
Tactic: rcases lt_trichotomy b 0 with (h' | h' | h')
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
h : a < 0
inl :
  ∀ (h' : b < 0),
    (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
      (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
⊢ (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
have inl₁ : ∀ (h' : b = 0),
  (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
Tactic: rcases lt_trichotomy b 0 with (h' | h' | h')
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
h : a < 0
inl :
  ∀ (h' : b < 0),
    (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
      (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
inl₁ :
  ∀ (h' : b = 0),
    (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
      (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
⊢ (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
have inl₂ : ∀ (h' : 0 < b),
  (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
Tactic: rcases lt_trichotomy b 0 with (h' | h' | h')
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
h : a = 0
⊢ (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
have inr : ∀ (h' : b < 0),
  (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
Tactic: rcases lt_trichotomy b 0 with (h' | h' | h')
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
h : a = 0
inr :
  ∀ (h' : b < 0),
    (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
      (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
⊢ (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
have inr₁ : ∀ (h' : b = 0),
  (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
Tactic: rcases lt_trichotomy b 0 with (h' | h' | h')
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
h : a = 0
inr :
  ∀ (h' : b < 0),
    (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
      (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
inr₁ :
  ∀ (h' : b = 0),
    (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
      (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
⊢ (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
have inr₂ : ∀ (h' : 0 < b),
  (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
Tactic: rcases lt_trichotomy b 0 with (h' | h' | h')
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
h : 0 < a
⊢ (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
have inr : ∀ (h' : b < 0),
  (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
Tactic: rcases lt_trichotomy b 0 with (h' | h' | h')
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
h : 0 < a
inr :
  ∀ (h' : b < 0),
    (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
      (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
⊢ (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
have inr₁ : ∀ (h' : b = 0),
  (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
Tactic: rcases lt_trichotomy b 0 with (h' | h' | h')
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
h : 0 < a
inr :
  ∀ (h' : b < 0),
    (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
      (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
inr₁ :
  ∀ (h' : b = 0),
    (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
      (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
⊢ (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
have inr₂ : ∀ (h' : 0 < b),
  (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
Tactic: rcases lt_trichotomy b 0 with (h' | h' | h')
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
h : a < 0
h' : 0 < b
⊢ (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
have inl : (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0 ↔ (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
Tactic: simp only [h, h', true_or, true_and, or_true, and_true]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
h : 0 < a
h' : b < 0
⊢ (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
have inr : (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0 ↔ (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
Tactic: simp only [h, h', true_or, true_and, or_true, and_true]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
h : a < 0
h' : 0 < b
⊢ (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0 ↔ (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
have inl : (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
h : a < 0
h' : 0 < b
inl : (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
⊢ (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0 ↔ (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
have inl₁ : (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0 → (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
h : a < 0
h' : 0 < b
inl : (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₁ : (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0 → (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0
⊢ (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0 ↔ (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
have inl₂ : 0 < a → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
h : a < 0
h' : 0 < b
inl : (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₁ : (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0 → (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0
inl₂ : 0 < a → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
⊢ (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0 ↔ (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
have inl₃ : b < 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
h : a < 0
h' : 0 < b
inl : (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₁ : (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0 → (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0
inl₂ : 0 < a → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₃ : b < 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
⊢ (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0 ↔ (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
have inl₄ : a = 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
h : a < 0
h' : 0 < b
inl : (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₁ : (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0 → (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0
inl₂ : 0 < a → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₃ : b < 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₄ : a = 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
⊢ (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0 ↔ (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
have inl₅ : b = 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
h : a < 0
h' : 0 < b
inl : (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₁ : (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0 → (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0
inl₂ : 0 < a → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₃ : b < 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₄ : a = 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₅ : b = 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₆ : 0 < a → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₇ : b < 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₈ : a = 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₉ : b = 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
⊢ (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0 ↔ (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
have inl₁₀ : 0 < a → ¬(0 < a ∨ 0 = a) → b < 0 ∨ b = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
h : a < 0
h' : 0 < b
inl : (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₁ : (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0 → (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0
inl₂ : 0 < a → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₃ : b < 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₄ : a = 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₅ : b = 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₆ : 0 < a → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₇ : b < 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₈ : a = 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₉ : b = 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₁₀ : 0 < a → ¬(0 < a ∨ 0 = a) → b < 0 ∨ b = 0
⊢ (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0 ↔ (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
have inl₁₁ : b < 0 → ¬(0 < a ∨ 0 = a) → b < 0 ∨ b = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
h : a < 0
h' : 0 < b
inl : (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₁ : (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0 → (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0
inl₂ : 0 < a → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₃ : b < 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₄ : a = 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₅ : b = 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₆ : 0 < a → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₇ : b < 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₈ : a = 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₉ : b = 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₁₀ : 0 < a → ¬(0 < a ∨ 0 = a) → b < 0 ∨ b = 0
inl₁₁ : b < 0 → ¬(0 < a ∨ 0 = a) → b < 0 ∨ b = 0
⊢ (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0 ↔ (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
have inl₁₂ : a = 0 → ¬(0 < a ∨ 0 = a) → b < 0 ∨ b = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
h : a < 0
h' : 0 < b
inl : (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₁ : (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0 → (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0
inl₂ : 0 < a → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₃ : b < 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₄ : a = 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₅ : b = 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₆ : 0 < a → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₇ : b < 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₈ : a = 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₉ : b = 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₁₀ : 0 < a → ¬(0 < a ∨ 0 = a) → b < 0 ∨ b = 0
inl₁₁ : b < 0 → ¬(0 < a ∨ 0 = a) → b < 0 ∨ b = 0
inl₁₂ : a = 0 → ¬(0 < a ∨ 0 = a) → b < 0 ∨ b = 0
⊢ (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0 ↔ (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
have inl₁₃ : b = 0 → ¬(0 < a ∨ 0 = a) → b < 0 ∨ b = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
h : a < 0
h' : 0 < b
inl : (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₁ : (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0 → (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0
inl₂ : 0 < a → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₃ : b < 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₄ : a = 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₅ : b = 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₆ : 0 < a → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₇ : b < 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₈ : a = 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₉ : b = 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₁₀ : 0 < a → ¬(0 < a ∨ 0 = a) → b < 0 ∨ b = 0
inl₁₁ : b < 0 → ¬(0 < a ∨ 0 = a) → b < 0 ∨ b = 0
inl₁₂ : a = 0 → ¬(0 < a ∨ 0 = a) → b < 0 ∨ b = 0
inl₁₃ : b = 0 → ¬(0 < a ∨ 0 = a) → b < 0 ∨ b = 0
⊢ (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0 ↔ (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
have inl₁₄ : 0 < a → (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0
Tactic: tauto