b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : 0 < x
⊢ abs x = x
b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : 0 < x
⊢ b ^ logb b x = x
rw [rpow_logb_eq_abs b_pos b_ne_one hx.ne']
no goals
b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : 0 < x
⊢ abs x = x
exact abs_of_pos hx