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
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
⊢ (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
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
⊢ (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
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
⊢ (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
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
⊢ (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
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
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
⊢ (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
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
⊢ (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
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
⊢ (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 : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop
have inr : ∀
  (this :
    ∀ {b : ℝ} (hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1) (hb₀ : 0 < b), Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop)
  (hb₀ : ¬0 < b), Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop
Tactic: wlog hb₀ : 0 < b generalizing b
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
inr :
  ∀
    (this :
      ∀ {b : ℝ} (hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1) (hb₀ : 0 < b), Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop)
    (hb₀ : ¬0 < b), Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop
have wlog : ∀ {b : ℝ} (hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1) (hb₀ : 0 < b), Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop
Tactic: wlog hb₀ : 0 < b generalizing b
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
this : ∀ {b : ℝ} (hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1) (hb₀ : 0 < b), Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop
hb₀ : ¬0 < b
⊢ 0 < -b
have linarith : -b ≤ 0 → b < -1 → b < 0 → b < 1 → -1 + (b - -1) + (-b - 0) = 0
Tactic: linarith +splitNe
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
this : ∀ {b : ℝ} (hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1) (hb₀ : 0 < b), Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop
hb₀ : ¬0 < b
linarith : -b ≤ 0 → b < -1 → b < 0 → b < 1 → -1 + (b - -1) + (-b - 0) = 0
⊢ 0 < -b
have linarith₁ : -b ≤ 0 → b < -1 → b < 0 → 1 < b → HMul.hMul (α := ℝ) 2 (-1) + (b - -1) + (1 - b) = 0
Tactic: linarith +splitNe