awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
hr : 0 < r
h_meas : Measurable (β := ℝ) fun (ω : E) ↦ (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int :
  ∀ (t : ℝ),
    0 < t →
      Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {a : E | t ≤ (1 + ‖a‖) ^ (-r)} : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall 0 (t ^ (-r⁻¹) - 1)) : ℝ≥0∞)
f : (t : ℝ) → ℝ≥0∞ := fun (t : ℝ) ↦ (μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
mB : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) (Metric.ball 0 1)
h_int'' : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 1) t → f t = 0
calc_2 : LT.lt (α := ℝ≥0∞) 0 ∞
⊢ ∫⁻ (t : ℝ) in Ioi 1, f t < ∞

Tactic:
rw [setLIntegral_congr_fun measurableSet_Ioi h_int'', lintegral_const 0,
      zero_mul]

Premises used: MeasureTheory.lintegral_const, MulZeroClass.zero_mul, MeasureTheory.setLIntegral_congr_fun, measurableSet_Ioi, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
hr : 0 < r
h_meas : Measurable (β := ℝ) fun (ω : E) ↦ (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int :
  ∀ (t : ℝ),
    0 < t →
      Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {a : E | t ≤ (1 + ‖a‖) ^ (-r)} : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall 0 (t ^ (-r⁻¹) - 1)) : ℝ≥0∞)
f : (t : ℝ) → ℝ≥0∞ := fun (t : ℝ) ↦ (μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
mB : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) (Metric.ball 0 1)
h_int'' : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 1) t → f t = 0
⊢ LT.lt (α := ℝ≥0∞) 0 ∞

Tactic:
WithTop.top_pos

Premises used: ENNReal.ofNNReal, WithTop.top_pos
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
hr : 0 < r
h_meas : Measurable (β := ℝ) fun (ω : E) ↦ (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int :
  ∀ (t : ℝ),
    0 < t →
      Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {a : E | t ≤ (1 + ‖a‖) ^ (-r)} : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall 0 (t ^ (-r⁻¹) - 1)) : ℝ≥0∞)
f : (t : ℝ) → ℝ≥0∞ := fun (t : ℝ) ↦ (μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
mB : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) (Metric.ball 0 1)
h_int'' : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 1) t → f t = 0
⊢ LT.lt (α := ℝ≥0∞) 0 ∞

Tactic:
exact WithTop.top_pos

Premises used: WithTop.top_pos
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
left : AEStronglyMeasurable (β := ℝ) (fun (x : E) ↦ (1 + ‖x‖) ^ (-r)) μ
right : HasFiniteIntegral (ε := ℝ) (fun (x : E) ↦ (1 + ‖x‖) ^ (-r)) μ
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ (1 + ‖x‖) ^ (-r)) μ

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
⊢ Measurable (β := ℝ) fun (x : E) ↦ (1 + ‖x‖) ^ (-r)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : E) ↦ (1 + ‖x‖) ^ (-r)) μ

Tactic:
apply Measurable.aestronglyMeasurable (by fun_prop)

Premises used: Measurable.aestronglyMeasurable
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
x : E
⊢ 0 ≤ 1 + ‖x‖

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
⊢ ∫⁻ (a : E), ‖(1 + ‖a‖) ^ (-r)‖ₑ ∂μ = ∫⁻ (a : E), ENNReal.ofReal ((1 + ‖a‖) ^ (-r)) ∂μ

Tactic:
have : (∫⁻ a : E, ‖(1 + ‖a‖) ^ (-r)‖ₑ ∂μ) = ∫⁻ a : E, ENNReal.ofReal ((1 + ‖a‖) ^ (-r)) ∂μ :=
    lintegral_enorm_of_nonneg fun _ => rpow_nonneg (by positivity) _
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
this : ∫⁻ (a : E), ‖(1 + ‖a‖) ^ (-r)‖ₑ ∂μ = ∫⁻ (a : E), ENNReal.ofReal ((1 + ‖a‖) ^ (-r)) ∂μ
right : ∫⁻ (a : E), ENNReal.ofReal ((1 + ‖a‖) ^ (-r)) ∂μ < ∞
⊢ HasFiniteIntegral (ε := ℝ) (fun (x : E) ↦ (1 + ‖x‖) ^ (-r)) μ

Tactic:
rw [hasFiniteIntegral_iff_enorm, this]

Premises used: MeasureTheory.hasFiniteIntegral_iff_enorm
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
this : ∫⁻ (a : E), ‖(1 + ‖a‖) ^ (-r)‖ₑ ∂μ = ∫⁻ (a : E), ENNReal.ofReal ((1 + ‖a‖) ^ (-r)) ∂μ
⊢ ∫⁻ (a : E), ENNReal.ofReal ((1 + ‖a‖) ^ (-r)) ∂μ < ∞

Tactic:
finite_integral_one_add_norm hnr

Premises used: finite_integral_one_add_norm
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
this : ∫⁻ (a : E), ‖(1 + ‖a‖) ^ (-r)‖ₑ ∂μ = ∫⁻ (a : E), ENNReal.ofReal ((1 + ‖a‖) ^ (-r)) ∂μ
⊢ ∫⁻ (a : E), ENNReal.ofReal ((1 + ‖a‖) ^ (-r)) ∂μ < ∞

Tactic:
exact finite_integral_one_add_norm hnr

Premises used: finite_integral_one_add_norm
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
hr : 0 < r
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-r / 2)) μ

Tactic:
((integrable_one_add_norm hnr).const_mul <| (2 : ℝ) ^ (r / 2)).mono'
    ?_ (Eventually.of_forall fun x => ?_)

Premises used: integrable_one_add_norm, MeasureTheory.Integrable.const_mul, MeasureTheory.Integrable.mono', HDiv.hDiv, Filter.Eventually.of_forall, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
hr : 0 < r
refine_1 : AEStronglyMeasurable (β := ℝ) (fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-r / 2)) μ
refine_2 : ∀ (x : E), ‖(1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-r / 2)‖ ≤ HPow.hPow (α := ℝ) 2 (r / 2) * (1 + ‖x‖) ^ (-r)
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-r / 2)) μ

Tactic:
refine ((integrable_one_add_norm hnr).const_mul <| (2 : ℝ) ^ (r / 2)).mono'
    ?_ (Eventually.of_forall fun x => ?_)

Premises used: integrable_one_add_norm, MeasureTheory.Integrable.const_mul, MeasureTheory.Integrable.mono', HDiv.hDiv, Filter.Eventually.of_forall, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
hr : 0 < r
⊢ Measurable (β := ℝ) fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-r / 2)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
hr : 0 < r
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-r / 2)) μ

Tactic:
apply Measurable.aestronglyMeasurable (by fun_prop)

Premises used: Measurable.aestronglyMeasurable
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
hr : 0 < r
x : E
⊢ ‖(1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-r / 2)‖ ≤ HPow.hPow (α := ℝ) 2 (r / 2) * (1 + ‖x‖) ^ (-r)

Tactic:
(abs_of_pos ?_).trans_le (rpow_neg_one_add_norm_sq_le x hr)

Premises used: Eq.trans_le, rpow_neg_one_add_norm_sq_le, abs_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
hr : 0 < r
x : E
refine_2 : 0 < (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-r / 2)
⊢ ‖(1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-r / 2)‖ ≤ HPow.hPow (α := ℝ) 2 (r / 2) * (1 + ‖x‖) ^ (-r)

Tactic:
refine (abs_of_pos ?_).trans_le (rpow_neg_one_add_norm_sq_le x hr)

Premises used: Eq.trans_le, rpow_neg_one_add_norm_sq_le, abs_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
hr : 0 < r
x : E
⊢ 0 < (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-r / 2)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
⊢ log x / log b = logb b x

Tactic:
rfl

Premises used: Real.logb, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
⊢ logb b 0 = 0

Tactic:
simp [logb]

Premises used: Real.logb
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
⊢ logb b 1 = 0

Tactic:
simp [logb]

Premises used: Real.logb
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
x : ℝ
⊢ logb 0 x = 0

Tactic:
simp only [← log_div_log, log_zero, div_zero]

Premises used: Real.log_div_log, Real.log_zero, div_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
h : ∀ (x : ℝ), logb 0 x = 0 x
⊢ logb 0 = 0

Tactic:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
x : ℝ
h : Eq (α := ℝ) 0 (0 x)
h₁ h₂ : Eq (α := ℝ) 0 0
⊢ logb 0 x = 0 x

Tactic:
rw [logb_zero_left, Pi.zero_apply]

Premises used: Real.logb_zero_left, Pi.zero_apply
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
x : ℝ
⊢ logb 1 x = 0

Tactic:
simp only [← log_div_log, log_one, div_zero]

Premises used: Real.log_div_log, Real.log_one, div_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
h : ∀ (x : ℝ), logb 1 x = 0 x
⊢ logb 1 = 0

Tactic:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
x : ℝ
h : Eq (α := ℝ) 0 (0 x)
h₁ h₂ : Eq (α := ℝ) 0 0
⊢ logb 1 x = 0 x

Tactic:
rw [logb_one_left, Pi.zero_apply]

Premises used: Pi.zero_apply, Real.logb_one_left
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
hb : 1 < b
⊢ logb b b = 1

Tactic:
div_self (log_pos hb).ne'

Premises used: Real.log_pos, LT.lt.ne', Real.logb, div_self
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
h : logb b b = 1
h' : log b = 0
⊢ False

Tactic:
simp [logb, h'] at h

Premises used: Real.logb
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
rw : log x / log |b| = logb b x
rw₁ : log x / log |b| = log x / log b
rw₂ rw₃ : log x / log b = log x / log b
⊢ logb |b| x = logb b x

Tactic:
rw [logb, logb, log_abs]

Premises used: Real.log_abs, Real.logb
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
rw : log |x| / log b = logb b x
rw₁ : log |x| / log b = log x / log b
rw₂ rw₃ : log x / log b = log x / log b
⊢ logb b |x| = logb b x

Tactic:
rw [logb, logb, log_abs]

Premises used: Real.log_abs, Real.logb
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
h : ∀ (x : ℝ), logb (-b) x = logb b x
⊢ logb (-b) = logb b

Tactic:
ext x
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
h : logb (-b) x = logb |b| x
h₁ : logb |(-b)| x = logb |b| x
h₂ h₃ : logb |b| x = logb |b| x
⊢ logb (-b) x = logb b x

Tactic:
rw [← logb_abs_base b x, ← logb_abs_base (-b) x, abs_neg]

Premises used: abs_neg, Real.logb_abs_base, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
rw : logb b (-x) = logb b |x|
rw₁ : logb b |(-x)| = logb b |x|
rw₂ rw₃ : logb b |x| = logb b |x|
⊢ logb b (-x) = logb b x

Tactic:
rw [← logb_abs b x, ← logb_abs b (-x), abs_neg]

Premises used: abs_neg, Real.logb_abs, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
simp_rw : log (x * y) / log b = log x / log b + log y / log b
simp_rw₁ : (log x + log y) / log b = log x / log b + log y / log b
⊢ logb b (x * y) = logb b x + logb b y

Tactic:
simp_rw [logb, log_mul hx hy, add_div]

Premises used: Real.logb, Real.log_mul, add_div
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
simp_rw : log (x / y) / log b = log x / log b - log y / log b
simp_rw₁ : (log x - log y) / log b = log x / log b - log y / log b
⊢ logb b (x / y) = logb b x - logb b y

Tactic:
simp_rw [logb, log_div hx hy, sub_div]

Premises used: sub_div, Real.log_div, Real.logb
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
⊢ logb b x⁻¹ = -logb b x

Tactic:
simp [logb, neg_div]

Premises used: neg_div, Real.logb
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
⊢ logb b⁻¹ x = -logb b x

Tactic:
simp [logb, div_neg]

Premises used: Real.logb, div_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
a b : ℝ
h₁ : a ≠ 0
h₂ : b ≠ 0
c : ℝ
simp_rw : logb c (a * b) = logb c a + logb c b
⊢ (logb (a * b) c)⁻¹ = (logb a c)⁻¹ + (logb b c)⁻¹

Tactic:
simp_rw [inv_logb]

Premises used: Real.inv_logb
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
a b : ℝ
h₁ : a ≠ 0
h₂ : b ≠ 0
c : ℝ
⊢ logb c (a * b) = logb c a + logb c b

Tactic:
logb_mul h₁ h₂

Premises used: Real.logb_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
a b : ℝ
h₁ : a ≠ 0
h₂ : b ≠ 0
c : ℝ
⊢ logb c (a * b) = logb c a + logb c b

Tactic:
exact logb_mul h₁ h₂

Premises used: Real.logb_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
a b : ℝ
h₁ : a ≠ 0
h₂ : b ≠ 0
c : ℝ
simp_rw : logb c (a / b) = logb c a - logb c b
⊢ (logb (a / b) c)⁻¹ = (logb a c)⁻¹ - (logb b c)⁻¹

Tactic:
simp_rw [inv_logb]

Premises used: Real.inv_logb
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
a b : ℝ
h₁ : a ≠ 0
h₂ : b ≠ 0
c : ℝ
⊢ logb c (a / b) = logb c a - logb c b

Tactic:
logb_div h₁ h₂

Premises used: Real.logb_div
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
a b : ℝ
h₁ : a ≠ 0
h₂ : b ≠ 0
c : ℝ
⊢ logb c (a / b) = logb c a - logb c b

Tactic:
exact logb_div h₁ h₂

Premises used: Real.logb_div
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
a b : ℝ
h₁ : a ≠ 0
h₂ : b ≠ 0
c : ℝ
rw : logb (a * b) c = (logb (a * b) c)⁻¹⁻¹
rw₁ rw₂ : logb (a * b) c = logb (a * b) c
⊢ logb (a * b) c = ((logb a c)⁻¹ + (logb b c)⁻¹)⁻¹

Tactic:
rw [← inv_logb_mul_base h₁ h₂ c, inv_inv]

Premises used: Real.inv_logb_mul_base, inv_inv
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
a b : ℝ
h₁ : a ≠ 0
h₂ : b ≠ 0
c : ℝ
rw : logb (a / b) c = (logb (a / b) c)⁻¹⁻¹
rw₁ rw₂ : logb (a / b) c = logb (a / b) c
⊢ logb (a / b) c = ((logb a c)⁻¹ - (logb b c)⁻¹)⁻¹

Tactic:
rw [← inv_logb_div_base h₁ h₂ c, inv_inv]

Premises used: Real.inv_logb_div_base, inv_inv
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
a b c : ℝ
h₁ : b ≠ 0
h₂ : b ≠ 1
h₃ : b ≠ -1
rw : log c / log b * (log b / log a) = log c / log a
rw₁ rw₂ : log c / log a = log c / log a
⊢ log b / log a * (log c / log b) = log c / log a

Tactic:
rw [mul_comm, div_mul_div_cancel₀ (log_ne_zero.mpr ⟨h₁, h₂, h₃⟩)]

Premises used: Iff.mpr, And.intro, mul_comm, div_mul_div_cancel₀, Real.log_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
a b c : ℝ
h₁ : c ≠ 0
h₂ : c ≠ 1
h₃ : c ≠ -1
⊢ logb a c / logb b c = logb a b

Tactic:
div_div_div_cancel_left' _ _ <| log_ne_zero.mpr ⟨h₁, h₂, h₃⟩

Premises used: Iff.mpr, Real.logb, div_div_div_cancel_left', And.intro, Real.log_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x y : ℝ
hx : 0 < x
rw : log (x ^ y) / log b = y * logb b x
rw₁ : y * log x / log b = y * logb b x
rw₂ : y * log x / log b = y * (log x / log b)
rw₃ rw₄ : y * (log x / log b) = y * (log x / log b)
⊢ logb b (x ^ y) = y * logb b x

Tactic:
rw [logb, log_rpow hx, logb, mul_div_assoc]

Premises used: Real.log_rpow, mul_div_assoc, Real.logb
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
k : ℕ
rw : log (x ^ k) / log b = (↑k : ℝ) * logb b x
rw₁ : log (x ^ k) / log b = (↑k : ℝ) * (log x / log b)
rw₂ : (↑k : ℝ) * log x / log b = (↑k : ℝ) * (log x / log b)
rw₃ rw₄ : (↑k : ℝ) * (log x / log b) = (↑k : ℝ) * (log x / log b)
⊢ logb b (x ^ k) = (↑k : ℝ) * logb b x

Tactic:
rw [logb, logb, log_pow, mul_div_assoc]

Premises used: mul_div_assoc, Real.logb, Real.log_pow
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
rw : log b ≠ 0
⊢ logb b (b ^ x) = x

Tactic:
rw [logb, div_eq_iff, log_rpow b_pos]

Premises used: Real.log_rpow, Real.logb, div_eq_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
⊢ log b ≠ 0

Tactic:
log_ne_zero_of_pos_of_ne_one b_pos b_ne_one

Premises used: Real.log_ne_zero_of_pos_of_ne_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
⊢ log b ≠ 0

Tactic:
exact log_ne_zero_of_pos_of_ne_one b_pos b_ne_one

Premises used: Real.log_ne_zero_of_pos_of_ne_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
a : Membership.mem (γ := Set ℝ) (Ioi 0) (b ^ logb b x)
a₁ : Membership.mem (γ := Set ℝ) (Ioi 0) |x|
a₂ : log (b ^ logb b x) = log |x|
⊢ b ^ logb b x = |x|

Tactic:
apply log_injOn_pos

Premises used: Real.log_injOn_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
⊢ 0 < b ^ logb b x

Tactic:
apply rpow_pos_of_pos b_pos

Premises used: Real.rpow_pos_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) |x|

Tactic:
simp only [abs_pos, mem_Ioi, Ne, hx, not_false_iff]

Premises used: Set.mem_Ioi, Ne, abs_pos, not_false_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
a : log x / log b * log b = log x
⊢ log (b ^ logb b x) = log |x|

Tactic:
rw [log_rpow b_pos, logb, log_abs]

Premises used: Real.log_abs, Real.log_rpow, Real.logb
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
⊢ log x / log b * log b = log x

Tactic:
field [log_ne_zero_of_pos_of_ne_one b_pos b_ne_one]

Premises used: Real.log_ne_zero_of_pos_of_ne_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : 0 < x
rw : |x| = x
⊢ b ^ logb b x = x

Tactic:
rw [rpow_logb_eq_abs b_pos b_ne_one hx.ne']

Premises used: Real.rpow_logb_eq_abs, LT.lt.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : 0 < x
⊢ |x| = x

Tactic:
abs_of_pos hx

Premises used: abs_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : 0 < x
⊢ |x| = x

Tactic:
exact abs_of_pos hx

Premises used: abs_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x < 0
rw : |x| = -x
⊢ b ^ logb b x = -x

Tactic:
rw [rpow_logb_eq_abs b_pos b_ne_one (ne_of_lt hx)]

Premises used: Real.rpow_logb_eq_abs, ne_of_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x < 0
⊢ |x| = -x

Tactic:
abs_of_neg hx

Premises used: abs_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x < 0
⊢ |x| = -x

Tactic:
exact abs_of_neg hx

Premises used: abs_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hy : 0 < y
mp : logb b y = x → b ^ x = y
mpr : b ^ x = y → logb b y = x
⊢ logb b y = x ↔ b ^ x = y

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hy : 0 < y
⊢ b ^ logb b y = y

Tactic:
rpow_logb b_pos b_ne_one hy

Premises used: Real.rpow_logb
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hy : 0 < y
⊢ b ^ logb b y = y

Tactic:
exact rpow_logb b_pos b_ne_one hy

Premises used: Real.rpow_logb
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hy : 0 < b ^ x
⊢ logb b (b ^ x) = x

Tactic:
logb_rpow b_pos b_ne_one

Premises used: Real.logb_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hy : 0 < b ^ x
⊢ logb b (b ^ x) = x

Tactic:
exact logb_rpow b_pos b_ne_one

Premises used: Real.logb_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
⊢ SurjOn (logb b) (Ioi 0) univ

Tactic:
fun x _ =>
  ⟨b ^ x, rpow_pos_of_pos b_pos x, logb_rpow b_pos b_ne_one⟩

Premises used: Real.rpow_pos_of_pos, Set.Mem, setOf, Set.SurjOn, Set.Subset, HPow.hPow, And.intro, Exists.intro, Set.image, Real.logb_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
⊢ Surjective (logb b)

Tactic:
fun x => ⟨b ^ x, logb_rpow b_pos b_ne_one⟩

Premises used: HPow.hPow, Exists.intro, Real.logb_rpow, Function.Surjective
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
⊢ range (logb b) = univ

Tactic:
(logb_surjective b_pos b_ne_one).range_eq

Premises used: Real.logb_surjective, Function.Surjective.range_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
x : ℝ
_ : Membership.mem (γ := Set ℝ) univ x → x ∈ logb b '' Iio 0
⊢ Membership.mem (γ := Set ℝ) univ x → x ∈ logb b '' Iio 0

Tactic:
_
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
x : ℝ
h_1 : Membership.mem (γ := Set ℝ) univ x
h : Membership.mem (γ := Set ℝ) (Iio 0) (-b ^ x) ∧ logb b (-b ^ x) = x
⊢ x ∈ logb b '' Iio 0

Tactic:
use -b ^ x
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
x : ℝ
h_1 : Membership.mem (γ := Set ℝ) univ x
h : Membership.mem (γ := Set ℝ) (Iio 0) (-b ^ x)
h₁ : logb b (-b ^ x) = x
⊢ Membership.mem (γ := Set ℝ) (Iio 0) (-b ^ x) ∧ logb b (-b ^ x) = x

Tactic:
constructor