-- 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
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
mp₁₉ mp₂₀ : x = 0 → ¬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₂₂ 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₂₅ 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₂₉ 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₃₂ 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₁₉ mpr₂₀ : b = 0 → ¬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₂₂ 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₂₅ 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₂₉ 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₃₂ 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
mp₃₅ mp₃₆ : x = 0 → ¬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₃₈ 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₄₁ 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 = 1 → ¬b = 0 → ¬b = 1 → b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
mp₄₅ 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 → ¬b = 0 → ¬x = 1 → ¬x = -1 → b = 1 ∨ b = -1
mpr₃₆ mpr₃₇ : b = 1 → ¬x = 0 → ¬b = 0 → ¬x = 1 → ¬x = -1 → b = 1 ∨ b = -1
mpr₃₈ : b = 1 → ¬x = 0 → ¬b = 0 → ¬x = 1 → ¬x = -1 → ¬b = 1 → b = -1
mpr₃₉ mpr₄₀ : b = -1 → ¬x = 0 → ¬b = 0 → ¬x = 1 → ¬x = -1 → b = 1 ∨ b = -1
mpr₄₁ : b = -1 → ¬x = 0 → ¬b = 0 → ¬x = 1 → ¬x = -1 → ¬b = 1 → b = -1
mpr₄₂ : x = 1 → ¬x = 0 → ¬b = 0 → ¬x = 1 → ¬x = -1 → b = 1 ∨ b = -1
mpr₄₃ : x = -1 → ¬x = 0 → ¬b = 0 → ¬x = 1 → ¬x = -1 → b = 1 ∨ b = -1
mp₄₈ mp₄₉ : x = 0 → ¬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₅₁ 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₅₄ 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