case b_ne_zero
b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
⊢ b ≠ 0

b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
b_ne_zero : b ≠ 0
⊢ log b ≠ 0
b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
⊢ log b ≠ 0
have b_ne_zero : b ≠ 0
b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
b_ne_zero : b ≠ 0
⊢ log b ≠ 0
case b_ne_zero
b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
⊢ b ≠ 0

b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
b_ne_zero : b ≠ 0
⊢ log b ≠ 0
linarith
case b_ne_minus_one
b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
b_ne_zero : b ≠ 0
⊢ b ≠ -1

b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
b_ne_zero : b ≠ 0
b_ne_minus_one : b ≠ -1
⊢ log b ≠ 0
b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
b_ne_zero : b ≠ 0
⊢ log b ≠ 0
have b_ne_minus_one : b ≠ -1
b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
b_ne_zero : b ≠ 0
b_ne_minus_one : b ≠ -1
⊢ log b ≠ 0
case b_ne_minus_one
b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
b_ne_zero : b ≠ 0
⊢ b ≠ -1

b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
b_ne_zero : b ≠ 0
b_ne_minus_one : b ≠ -1
⊢ log b ≠ 0
linarith
no goals
b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
b_ne_zero : b ≠ 0
b_ne_minus_one : b ≠ -1
⊢ log b ≠ 0
simp [b_ne_one, b_ne_zero, b_ne_minus_one]