awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
mp : (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mpr : b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
mp₁ : x = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₂ : x = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₃ : x = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₄ : b = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₅ : b = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
⊢ (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 ↔ b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
have mp₆ : b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
mp : (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mpr : b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
mp₁ : x = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₂ : x = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₃ : x = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₄ : b = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₅ : b = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₆ : b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₇ : x = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₈ : x = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₉ : x = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₀ : b = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₁ : b = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₂ : b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
⊢ (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 ↔ b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
have mp₁₃ : x = 0 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
mp : (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mpr : b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
mp₁ : x = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₂ : x = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₃ : x = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₄ : b = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₅ : b = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₆ : b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₇ : x = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₈ : x = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₉ : x = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₀ : b = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₁ : b = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₂ : b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₃ : x = 0 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
⊢ (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 ↔ b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
have mp₁₄ : x = 1 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
mp : (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mpr : b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
mp₁ : x = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₂ : x = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₃ : x = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₄ : b = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₅ : b = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₆ : b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₇ : x = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₈ : x = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₉ : x = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₀ : b = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₁ : b = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₂ : b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₃ : x = 0 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₄ : x = 1 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
⊢ (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 ↔ b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
have mp₁₅ : x = -1 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
mp : (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mpr : b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
mp₁ : x = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₂ : x = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₃ : x = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₄ : b = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₅ : b = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₆ : b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₇ : x = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₈ : x = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₉ : x = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₀ : b = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₁ : b = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₂ : b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₃ : x = 0 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₄ : x = 1 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₅ : x = -1 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
⊢ (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 ↔ b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
have mp₁₆ : b = 0 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
mp : (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mpr : b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
mp₁ : x = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₂ : x = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₃ : x = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₄ : b = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₅ : b = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₆ : b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₇ : x = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₈ : x = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₉ : x = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₀ : b = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₁ : b = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₂ : b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₃ : x = 0 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₄ : x = 1 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₅ : x = -1 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₆ : b = 0 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
⊢ (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 ↔ b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
have mp₁₇ : b = 1 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
mp : (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mpr : b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
mp₁ : x = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₂ : x = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₃ : x = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₄ : b = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₅ : b = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₆ : b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₇ : x = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₈ : x = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₉ : x = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₀ : b = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₁ : b = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₂ : b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₃ : x = 0 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₄ : x = 1 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₅ : x = -1 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₆ : b = 0 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₇ : b = 1 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
⊢ (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 ↔ b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
have mp₁₈ : b = -1 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
mp : (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mpr : b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
mp₁ : x = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₂ : x = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₃ : x = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₄ : b = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₅ : b = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₆ : b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₇ : x = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₈ : x = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₉ : x = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₀ : b = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₁ : b = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₂ : b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₃ : x = 0 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₄ : x = 1 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₅ : x = -1 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₆ : b = 0 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₇ : b = 1 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₈ : b = -1 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
⊢ (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 ↔ b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
have mpr₁ : b = 0 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
mp : (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mpr : b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
mp₁ : x = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₂ : x = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₃ : x = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₄ : b = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₅ : b = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₆ : b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₇ : x = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₈ : x = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₉ : x = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₀ : b = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₁ : b = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₂ : b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₃ : x = 0 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₄ : x = 1 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₅ : x = -1 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₆ : b = 0 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₇ : b = 1 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₈ : b = -1 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mpr₁ : b = 0 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
⊢ (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 ↔ b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
have mpr₂ : b = 1 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
mp : (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mpr : b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
mp₁ : x = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₂ : x = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₃ : x = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₄ : b = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₅ : b = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₆ : b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₇ : x = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₈ : x = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₉ : x = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₀ : b = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₁ : b = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₂ : b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₃ : x = 0 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₄ : x = 1 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₅ : x = -1 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₆ : b = 0 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₇ : b = 1 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₈ : b = -1 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mpr₁ : b = 0 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
mpr₂ : b = 1 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
⊢ (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 ↔ b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
have mpr₃ : b = -1 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
mp : (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mpr : b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
mp₁ : x = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₂ : x = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₃ : x = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₄ : b = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₅ : b = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₆ : b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₇ : x = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₈ : x = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₉ : x = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₀ : b = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₁ : b = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₂ : b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₃ : x = 0 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₄ : x = 1 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₅ : x = -1 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₆ : b = 0 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₇ : b = 1 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₈ : b = -1 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mpr₁ : b = 0 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
mpr₂ : b = 1 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
mpr₃ : b = -1 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
⊢ (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 ↔ b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
have mpr₄ : x = 0 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
mp : (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mpr : b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
mp₁ : x = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₂ : x = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₃ : x = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₄ : b = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₅ : b = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₆ : b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₇ : x = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₈ : x = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₉ : x = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₀ : b = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₁ : b = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₂ : b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₃ : x = 0 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₄ : x = 1 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₅ : x = -1 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₆ : b = 0 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₇ : b = 1 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₈ : b = -1 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mpr₁ : b = 0 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
mpr₂ : b = 1 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
mpr₃ : b = -1 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
mpr₄ : x = 0 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
⊢ (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 ↔ b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
have mpr₅ : x = 1 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
mp : (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mpr : b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
mp₁ : x = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₂ : x = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₃ : x = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₄ : b = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₅ : b = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₆ : b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₇ : x = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₈ : x = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₉ : x = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₀ : b = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₁ : b = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₂ : b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₃ : x = 0 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₄ : x = 1 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₅ : x = -1 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₆ : b = 0 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₇ : b = 1 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₈ : b = -1 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mpr₁ : b = 0 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
mpr₂ : b = 1 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
mpr₃ : b = -1 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
mpr₄ : x = 0 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
mpr₅ : x = 1 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
⊢ (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 ↔ b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
have mpr₆ : x = -1 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
mp : (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mpr : b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
mp₁ : x = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₂ : x = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₃ : x = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₄ : b = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₅ : b = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₆ : b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₇ : x = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₈ : x = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₉ : x = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₀ : b = 0 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₁ : b = 1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₂ : b = -1 → b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₃ : x = 0 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₄ : x = 1 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₅ : x = -1 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₆ : b = 0 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₇ : b = 1 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₁₈ : b = -1 → ¬b = 0 → b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mpr₁ : b = 0 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
mpr₂ : b = 1 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
mpr₃ : b = -1 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
mpr₄ : x = 0 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
mpr₅ : x = 1 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
mpr₆ : x = -1 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
mpr₇ : b = 0 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
mpr₈ : b = 1 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
mpr₉ : b = -1 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
mpr₁₀ : x = 0 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
mpr₁₁ : x = 1 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
mpr₁₂ : x = -1 → (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1
⊢ (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 ↔ b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
have mpr₁₃ : b = 0 → ¬(x = 0 ∨ x = 1 ∨ x = -1) → b = 0 ∨ b = 1 ∨ b = -1
Tactic: tauto