awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
h : 0 < a
h' : b < 0
inr : (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₁ : (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂ : 0 < b → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₃ : a < 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₄ : a = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₅ : b = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₆ : 0 < b → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₇ : a < 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₈ : a = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₉ : b = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₁₀ : 0 < b → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₁ : a < 0 → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₂ : a = 0 → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₃ : b = 0 → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₄ : 0 < b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₅ : 0 = b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₆ : a < 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₇ : a = 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₈ : 0 < b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₉ : 0 = b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂₀ : a < 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂₁ : a = 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂₂ : 0 < b → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₃ : 0 = b → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₄ : a < 0 → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₅ : a = 0 → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
⊢ (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0 ↔ (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
have inr₂₆ : 0 < b → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
h : 0 < a
h' : b < 0
inr : (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₁ : (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂ : 0 < b → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₃ : a < 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₄ : a = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₅ : b = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₆ : 0 < b → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₇ : a < 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₈ : a = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₉ : b = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₁₀ : 0 < b → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₁ : a < 0 → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₂ : a = 0 → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₃ : b = 0 → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₄ : 0 < b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₅ : 0 = b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₆ : a < 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₇ : a = 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₈ : 0 < b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₉ : 0 = b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂₀ : a < 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂₁ : a = 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂₂ : 0 < b → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₃ : 0 = b → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₄ : a < 0 → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₅ : a = 0 → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₆ : 0 < b → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
⊢ (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0 ↔ (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
have inr₂₇ : a < 0 → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
h : 0 < a
h' : b < 0
inr : (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₁ : (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂ : 0 < b → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₃ : a < 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₄ : a = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₅ : b = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₆ : 0 < b → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₇ : a < 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₈ : a = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₉ : b = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₁₀ : 0 < b → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₁ : a < 0 → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₂ : a = 0 → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₃ : b = 0 → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₄ : 0 < b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₅ : 0 = b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₆ : a < 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₇ : a = 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₈ : 0 < b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₉ : 0 = b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂₀ : a < 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂₁ : a = 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂₂ : 0 < b → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₃ : 0 = b → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₄ : a < 0 → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₅ : a = 0 → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₆ : 0 < b → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
inr₂₇ inr₂₈ : a < 0 → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
⊢ (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0 ↔ (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
have inr₂₉ : a < 0 → ¬0 < b → ¬0 = b → ¬a < 0 → a = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
h : 0 < a
h' : b < 0
inr : (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₁ : (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂ : 0 < b → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₃ : a < 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₄ : a = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₅ : b = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₆ : 0 < b → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₇ : a < 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₈ : a = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₉ : b = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₁₀ : 0 < b → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₁ : a < 0 → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₂ : a = 0 → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₃ : b = 0 → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₄ : 0 < b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₅ : 0 = b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₆ : a < 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₇ : a = 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₈ : 0 < b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₉ : 0 = b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂₀ : a < 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂₁ : a = 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂₂ : 0 < b → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₃ : 0 = b → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₄ : a < 0 → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₅ : a = 0 → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₆ : 0 < b → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
inr₂₇ inr₂₈ : a < 0 → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
inr₂₉ : a < 0 → ¬0 < b → ¬0 = b → ¬a < 0 → a = 0
⊢ (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0 ↔ (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
have inr₃₀ : a = 0 → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
h : 0 < a
h' : b < 0
inr : (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₁ : (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂ : 0 < b → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₃ : a < 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₄ : a = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₅ : b = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₆ : 0 < b → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₇ : a < 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₈ : a = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₉ : b = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₁₀ : 0 < b → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₁ : a < 0 → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₂ : a = 0 → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₃ : b = 0 → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₄ : 0 < b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₅ : 0 = b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₆ : a < 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₇ : a = 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₈ : 0 < b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₉ : 0 = b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂₀ : a < 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂₁ : a = 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂₂ : 0 < b → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₃ : 0 = b → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₄ : a < 0 → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₅ : a = 0 → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₆ : 0 < b → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
inr₂₇ inr₂₈ : a < 0 → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
inr₂₉ : a < 0 → ¬0 < b → ¬0 = b → ¬a < 0 → a = 0
inr₃₀ inr₃₁ : a = 0 → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
⊢ (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0 ↔ (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
have inr₃₂ : a = 0 → ¬0 < b → ¬0 = b → ¬a < 0 → a = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
h : 0 < a
h' : b < 0
inr : (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₁ : (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂ : 0 < b → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₃ : a < 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₄ : a = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₅ : b = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₆ : 0 < b → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₇ : a < 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₈ : a = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₉ : b = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₁₀ : 0 < b → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₁ : a < 0 → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₂ : a = 0 → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₃ : b = 0 → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₄ : 0 < b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₅ : 0 = b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₆ : a < 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₇ : a = 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₈ : 0 < b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₉ : 0 = b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂₀ : a < 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂₁ : a = 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂₂ : 0 < b → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₃ : 0 = b → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₄ : a < 0 → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₅ : a = 0 → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₆ : 0 < b → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
inr₂₇ inr₂₈ : a < 0 → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
inr₂₉ : a < 0 → ¬0 < b → ¬0 = b → ¬a < 0 → a = 0
inr₃₀ inr₃₁ : a = 0 → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
inr₃₂ : a = 0 → ¬0 < b → ¬0 = b → ¬a < 0 → a = 0
⊢ (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0 ↔ (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
have inr₃₃ : b = 0 → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
h : 0 < a
h' : b < 0
inr : (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₁ : (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂ : 0 < b → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₃ : a < 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₄ : a = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₅ : b = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₆ : 0 < b → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₇ : a < 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₈ : a = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₉ : b = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₁₀ : 0 < b → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₁ : a < 0 → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₂ : a = 0 → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₃ : b = 0 → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₄ : 0 < b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₅ : 0 = b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₆ : a < 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₇ : a = 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₈ : 0 < b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₉ : 0 = b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂₀ : a < 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂₁ : a = 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂₂ : 0 < b → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₃ : 0 = b → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₄ : a < 0 → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₅ : a = 0 → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₆ : 0 < b → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
inr₂₇ inr₂₈ : a < 0 → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
inr₂₉ : a < 0 → ¬0 < b → ¬0 = b → ¬a < 0 → a = 0
inr₃₀ inr₃₁ : a = 0 → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
inr₃₂ : a = 0 → ¬0 < b → ¬0 = b → ¬a < 0 → a = 0
inr₃₃ inr₃₄ : b = 0 → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
⊢ (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0 ↔ (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
have inr₃₅ : b = 0 → ¬0 < b → ¬0 = b → ¬a < 0 → a = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
h : 0 < a
h' : b < 0
inr : (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₁ : (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂ : 0 < b → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₃ : a < 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₄ : a = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₅ : b = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₆ : 0 < b → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₇ : a < 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₈ : a = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₉ : b = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₁₀ : 0 < b → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₁ : a < 0 → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₂ : a = 0 → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₃ : b = 0 → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₄ : 0 < b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₅ : 0 = b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₆ : a < 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₇ : a = 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₈ : 0 < b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₉ : 0 = b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂₀ : a < 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂₁ : a = 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂₂ : 0 < b → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₃ : 0 = b → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₄ : a < 0 → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₅ : a = 0 → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₆ : 0 < b → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
inr₂₇ inr₂₈ : a < 0 → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
inr₂₉ : a < 0 → ¬0 < b → ¬0 = b → ¬a < 0 → a = 0
inr₃₀ inr₃₁ : a = 0 → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
inr₃₂ : a = 0 → ¬0 < b → ¬0 = b → ¬a < 0 → a = 0
inr₃₃ inr₃₄ : b = 0 → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
inr₃₅ : b = 0 → ¬0 < b → ¬0 = b → ¬a < 0 → a = 0
⊢ (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0 ↔ (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
have inr₃₆ : 0 < b → ¬0 < b → ¬a < 0 → a = 0 ∨ b = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
h : 0 < a
h' : b < 0
inr : (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₁ : (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂ : 0 < b → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₃ : a < 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₄ : a = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₅ : b = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₆ : 0 < b → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₇ : a < 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₈ : a = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₉ : b = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₁₀ : 0 < b → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₁ : a < 0 → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₂ : a = 0 → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₃ : b = 0 → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₄ : 0 < b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₅ : 0 = b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₆ : a < 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₇ : a = 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₈ : 0 < b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₉ : 0 = b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂₀ : a < 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂₁ : a = 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂₂ : 0 < b → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₃ : 0 = b → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₄ : a < 0 → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₅ : a = 0 → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₆ : 0 < b → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
inr₂₇ inr₂₈ : a < 0 → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
inr₂₉ : a < 0 → ¬0 < b → ¬0 = b → ¬a < 0 → a = 0
inr₃₀ inr₃₁ : a = 0 → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
inr₃₂ : a = 0 → ¬0 < b → ¬0 = b → ¬a < 0 → a = 0
inr₃₃ inr₃₄ : b = 0 → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
inr₃₅ : b = 0 → ¬0 < b → ¬0 = b → ¬a < 0 → a = 0
inr₃₆ : 0 < b → ¬0 < b → ¬a < 0 → a = 0 ∨ b = 0
⊢ (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0 ↔ (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
have inr₃₇ : 0 = b → ¬0 < b → ¬a < 0 → a = 0 ∨ b = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
h : 0 < a
h' : b < 0
inr : (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₁ : (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂ : 0 < b → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₃ : a < 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₄ : a = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₅ : b = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₆ : 0 < b → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₇ : a < 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₈ : a = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₉ : b = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₁₀ : 0 < b → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₁ : a < 0 → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₂ : a = 0 → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₃ : b = 0 → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₄ : 0 < b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₅ : 0 = b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₆ : a < 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₇ : a = 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₈ : 0 < b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₉ : 0 = b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂₀ : a < 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂₁ : a = 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂₂ : 0 < b → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₃ : 0 = b → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₄ : a < 0 → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₅ : a = 0 → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₆ : 0 < b → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
inr₂₇ inr₂₈ : a < 0 → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
inr₂₉ : a < 0 → ¬0 < b → ¬0 = b → ¬a < 0 → a = 0
inr₃₀ inr₃₁ : a = 0 → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
inr₃₂ : a = 0 → ¬0 < b → ¬0 = b → ¬a < 0 → a = 0
inr₃₃ inr₃₄ : b = 0 → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
inr₃₅ : b = 0 → ¬0 < b → ¬0 = b → ¬a < 0 → a = 0
inr₃₆ : 0 < b → ¬0 < b → ¬a < 0 → a = 0 ∨ b = 0
inr₃₇ inr₃₈ : 0 = b → ¬0 < b → ¬a < 0 → a = 0 ∨ b = 0
⊢ (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0 ↔ (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
have inr₃₉ : 0 = b → ¬0 < b → ¬a < 0 → ¬a = 0 → b = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
h : 0 < a
h' : b < 0
inr : (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₁ : (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂ : 0 < b → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₃ : a < 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₄ : a = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₅ : b = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₆ : 0 < b → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₇ : a < 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₈ : a = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₉ : b = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₁₀ : 0 < b → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₁ : a < 0 → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₂ : a = 0 → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₃ : b = 0 → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₄ : 0 < b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₅ : 0 = b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₆ : a < 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₇ : a = 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₈ : 0 < b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₉ : 0 = b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂₀ : a < 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂₁ : a = 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂₂ : 0 < b → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₃ : 0 = b → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₄ : a < 0 → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₅ : a = 0 → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₆ : 0 < b → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
inr₂₇ inr₂₈ : a < 0 → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
inr₂₉ : a < 0 → ¬0 < b → ¬0 = b → ¬a < 0 → a = 0
inr₃₀ inr₃₁ : a = 0 → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
inr₃₂ : a = 0 → ¬0 < b → ¬0 = b → ¬a < 0 → a = 0
inr₃₃ inr₃₄ : b = 0 → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
inr₃₅ : b = 0 → ¬0 < b → ¬0 = b → ¬a < 0 → a = 0
inr₃₆ : 0 < b → ¬0 < b → ¬a < 0 → a = 0 ∨ b = 0
inr₃₇ inr₃₈ : 0 = b → ¬0 < b → ¬a < 0 → a = 0 ∨ b = 0
inr₃₉ : 0 = b → ¬0 < b → ¬a < 0 → ¬a = 0 → b = 0
⊢ (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0 ↔ (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
have inr₄₀ : a < 0 → ¬0 < b → ¬a < 0 → a = 0 ∨ b = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
h : 0 < a
h' : b < 0
inr : (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₁ : (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂ : 0 < b → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₃ : a < 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₄ : a = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₅ : b = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₆ : 0 < b → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₇ : a < 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₈ : a = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₉ : b = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₁₀ : 0 < b → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₁ : a < 0 → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₂ : a = 0 → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₃ : b = 0 → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₄ : 0 < b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₅ : 0 = b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₆ : a < 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₇ : a = 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₈ : 0 < b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₉ : 0 = b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂₀ : a < 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂₁ : a = 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂₂ : 0 < b → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₃ : 0 = b → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₄ : a < 0 → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₅ : a = 0 → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₆ : 0 < b → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
inr₂₇ inr₂₈ : a < 0 → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
inr₂₉ : a < 0 → ¬0 < b → ¬0 = b → ¬a < 0 → a = 0
inr₃₀ inr₃₁ : a = 0 → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
inr₃₂ : a = 0 → ¬0 < b → ¬0 = b → ¬a < 0 → a = 0
inr₃₃ inr₃₄ : b = 0 → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
inr₃₅ : b = 0 → ¬0 < b → ¬0 = b → ¬a < 0 → a = 0
inr₃₆ : 0 < b → ¬0 < b → ¬a < 0 → a = 0 ∨ b = 0
inr₃₇ inr₃₈ : 0 = b → ¬0 < b → ¬a < 0 → a = 0 ∨ b = 0
inr₃₉ : 0 = b → ¬0 < b → ¬a < 0 → ¬a = 0 → b = 0
inr₄₀ : a < 0 → ¬0 < b → ¬a < 0 → a = 0 ∨ b = 0
⊢ (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0 ↔ (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
have inr₄₁ : a = 0 → ¬0 < b → ¬a < 0 → a = 0 ∨ b = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
h : 0 < a
h' : b < 0
inr : (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₁ : (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂ : 0 < b → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₃ : a < 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₄ : a = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₅ : b = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₆ : 0 < b → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₇ : a < 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₈ : a = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₉ : b = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₁₀ : 0 < b → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₁ : a < 0 → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₂ : a = 0 → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₃ : b = 0 → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₄ : 0 < b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₅ : 0 = b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₆ : a < 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₇ : a = 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₈ : 0 < b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₉ : 0 = b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂₀ : a < 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂₁ : a = 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂₂ : 0 < b → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₃ : 0 = b → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₄ : a < 0 → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₅ : a = 0 → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₆ : 0 < b → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
inr₂₇ inr₂₈ : a < 0 → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
inr₂₉ : a < 0 → ¬0 < b → ¬0 = b → ¬a < 0 → a = 0
inr₃₀ inr₃₁ : a = 0 → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
inr₃₂ : a = 0 → ¬0 < b → ¬0 = b → ¬a < 0 → a = 0
inr₃₃ inr₃₄ : b = 0 → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
inr₃₅ : b = 0 → ¬0 < b → ¬0 = b → ¬a < 0 → a = 0
inr₃₆ : 0 < b → ¬0 < b → ¬a < 0 → a = 0 ∨ b = 0
inr₃₇ inr₃₈ : 0 = b → ¬0 < b → ¬a < 0 → a = 0 ∨ b = 0
inr₃₉ : 0 = b → ¬0 < b → ¬a < 0 → ¬a = 0 → b = 0
inr₄₀ : a < 0 → ¬0 < b → ¬a < 0 → a = 0 ∨ b = 0
inr₄₁ inr₄₂ : a = 0 → ¬0 < b → ¬a < 0 → a = 0 ∨ b = 0
⊢ (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0 ↔ (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
have inr₄₃ : a = 0 → ¬0 < b → ¬a < 0 → ¬a = 0 → b = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
h : -x * y = -(x * y)
⊢ - -x * y = -(-x * y)
have neg_left : - -x * y = - -(x * y)
Tactic: rw [h, neg_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
h : -x * y = -(x * y)
neg_left : - -x * y = - -(x * y)
⊢ - -x * y = -(-x * y)
have neg_left₁ : x * y = - -(x * y)
Tactic: rw [h, neg_neg, neg_neg]