awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
hb₀ : 0 < b
hb : b ≠ 1
h : ContinuousAt (logb b) 0
hb₁ : 1 < b
⊢ False

Tactic:
exact not_tendsto_nhds_of_tendsto_atBot (tendsto_logb_nhdsNE_zero hb₁)
        _ (h.tendsto.mono_left inf_le_left)

Premises used: not_tendsto_nhds_of_tendsto_atBot, ContinuousAt.tendsto, Filter.Tendsto.mono_left, inf_le_left, Real.tendsto_logb_nhdsNE_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
hb₀ : 0 < b
hb : b ≠ 1
h : ContinuousAt (logb b) 0
⊢ b < 1 ∨ 1 < b

Tactic:
cases lt_or_gt_of_ne hb with
  | inl hb₁ =>
      exact not_tendsto_nhds_of_tendsto_atTop (tendsto_logb_nhdsNE_zero_of_base_lt_one hb₀ hb₁)
        _ (h.tendsto.mono_left inf_le_left)
  | inr hb₁ =>
      exact not_tendsto_nhds_of_tendsto_atBot (tendsto_logb_nhdsNE_zero hb₁)
        _ (h.tendsto.mono_left inf_le_left)

Premises used: lt_or_gt_of_ne
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
α : Type u_1
f : α → ℝ
hf : ∀ (x : α), Membership.mem (γ := Finset α) ∅ x → f x ≠ 0
⊢ logb b (∏ i ∈ ∅, f i) = ∑ i ∈ ∅, logb b (f i)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
α : Type u_1
f : α → ℝ
a : α
s : Finset α
h : a ∉ s
h_1 : ∀ (hf : ∀ x ∈ s, f x ≠ 0), logb b (∏ i ∈ s, f i) = ∑ i ∈ s, logb b (f i)
hf : ∀ x ∈ Finset.cons a s h, f x ≠ 0
⊢ logb b (∏ i ∈ Finset.cons a s h, f i) = ∑ i ∈ Finset.cons a s h, logb b (f i)

Tactic:
simp_all [logb_mul, Finset.prod_ne_zero_iff]

Premises used: Real.logb_mul, Finset.prod_ne_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ x ∈ s, f x ≠ 0
empty : ∀ (hf : ∀ (x : α), Membership.mem (γ := Finset α) ∅ x → f x ≠ 0), logb b (∏ i ∈ ∅, f i) = ∑ i ∈ ∅, logb b (f i)
cons :
  ∀ (a : α) (s : Finset α) (h : a ∉ s),
    (∀ (hf : ∀ x ∈ s, f x ≠ 0), logb b (∏ i ∈ s, f i) = ∑ i ∈ s, logb b (f i)) →
      ∀ (hf : ∀ x ∈ Finset.cons a s h, f x ≠ 0),
        logb b (∏ i ∈ Finset.cons a s h, f i) = ∑ i ∈ Finset.cons a s h, logb b (f i)
⊢ logb b (∏ i ∈ s, f i) = ∑ i ∈ s, logb b (f i)

Tactic:
induction s using Finset.cons_induction_on with
  | empty => simp
  | cons => simp_all [logb_mul, Finset.prod_ne_zero_iff]

Premises used: Real.logb_mul, Finset.prod_ne_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
α : Type u_1
β : Type u_2
inst : Zero β
f : α →₀ β
g : α → β → ℝ
hg : ∀ (a : α), g a ((f : (a : α) → β) a) = 0 → Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a : β) (0 : β)
⊢ logb b (f.prod g) = f.sum fun (a : α) (c : β) ↦ logb b (g a c)

Tactic:
logb_prod _ _ fun _x hx h₀ ↦ Finsupp.mem_support_iff.1 hx <| hg _ h₀

Premises used: Finsupp.mem_support_iff, Real.logb_prod, Finsupp.sum, Iff.mp, Finsupp.prod
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
n : ℕ
⊢ logb b (↑n : ℝ) = n.factorization.sum fun (p t : ℕ) ↦ (↑t : ℝ) * logb b (↑p : ℝ)

Tactic:
simp only [logb, mul_div_assoc', log_nat_eq_sum_factorization n, Finsupp.sum, Finset.sum_div]

Premises used: Finsupp.sum, Real.log_nat_eq_sum_factorization, mul_div_assoc', Finset.sum_div, Real.logb
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b a c : ℝ
n : ℕ
ha : a ≠ 0
h : log b = 0
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ logb b x ^ n / (a * x + c)) atTop (𝓝 0)

Tactic:
simpa [logb, h] using ((tendsto_mul_add_inv_atTop_nhds_zero _ _ ha).const_mul _)

Premises used: Filter.Tendsto.const_mul, Real.logb, tendsto_mul_add_inv_atTop_nhds_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b a c : ℝ
n : ℕ
ha : a ≠ 0
h : log b ≠ 0
⊢ a * log b ^ n ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b a c : ℝ
n : ℕ
ha : a ≠ 0
h : log b ≠ 0
x : ℝ
⊢ log x ^ n / (a * log b ^ n * x + c * log b ^ n) = logb b x ^ n / (a * x + c)

Tactic:
simp [field, div_pow, logb]

Premises used: Real.logb, div_pow
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b a c : ℝ
n : ℕ
ha : a ≠ 0
h : log b ≠ 0
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ logb b x ^ n / (a * x + c)) atTop (𝓝 0)

Tactic:
apply (tendsto_pow_log_div_mul_add_atTop (a * (log b) ^ n) (c * (log b) ^ n) n
                (by positivity)).congr fun x ↦ by simp [field, div_pow, logb]

Premises used: HMul.hMul, Real.log, HPow.hPow, Filter.Tendsto.congr, Real.tendsto_pow_log_div_mul_add_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b a c : ℝ
n : ℕ
ha : a ≠ 0
⊢ log b = 0 ∨ log b ≠ 0

Tactic:
cases eq_or_ne (log b) 0 with
  | inl h => simpa [logb, h] using ((tendsto_mul_add_inv_atTop_nhds_zero _ _ ha).const_mul _)
  | inr h => apply (tendsto_pow_log_div_mul_add_atTop (a * (log b) ^ n) (c * (log b) ^ n) n
                (by positivity)).congr fun x ↦ by simp [field, div_pow, logb]

Premises used: HMul.hMul, Real.log, Filter.Tendsto.const_mul, Real.logb, HPow.hPow, tendsto_mul_add_inv_atTop_nhds_zero, eq_or_ne, Filter.Tendsto.congr, OfNat.ofNat, Real.tendsto_pow_log_div_mul_add_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
n : ℕ
rw : Tendsto (β := ℝ) (fun (x : ℝ) ↦ logb b x ^ n / id x) atTop (𝓝 0)
rw₁ : ∀ᶠ (x : ℝ) in atTop, id x = 0 → logb b x ^ n = 0
⊢ Asymptotics.IsLittleO (E := ℝ) atTop (fun (x : ℝ) ↦ logb b x ^ n) id

Tactic:
rw [Asymptotics.isLittleO_iff_tendsto']

Premises used: Asymptotics.isLittleO_iff_tendsto'
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
n : ℕ
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ logb b x ^ n / id x) atTop (𝓝 0)

Tactic:
simpa using tendsto_pow_logb_div_mul_add_atTop 1 0 n one_ne_zero

Premises used: Real.tendsto_pow_logb_div_mul_add_atTop, one_ne_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
n : ℕ
x : ℝ
h₁ : x ≠ 0
h₂ : id x = 0
⊢ logb b x ^ n = 0

Tactic:
(h₁ h₂).elim

Premises used: False.elim
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
n : ℕ
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ x ≠ 0) x} x →
          Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ id x = 0 → logb b x ^ n = 0) x} x}
      a
h₁ h₂ : ∀ (x : ℝ) (h₁ : x ≠ 0) (h₂ : id x = 0), logb b x ^ n = 0
⊢ ∀ᶠ (x : ℝ) in atTop, id x = 0 → logb b x ^ n = 0

Tactic:
filter_upwards [eventually_ne_atTop (0 : ℝ)] with x h₁ h₂ using (h₁ h₂).elim

Premises used: Filter.eventually_ne_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
⊢ logb b =o[atTop] id

Tactic:
isLittleO_pow_logb_id_atTop.congr_left fun _ => pow_one _

Premises used: Asymptotics.IsLittleO.congr_left, Real.logb, pow_one, Real.isLittleO_pow_logb_id_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b c : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
rw : ¬c = 0 → Tendsto (Norm.norm ∘ logb b) atTop atTop
⊢ Asymptotics.IsLittleO (E := ℝ) atTop (fun (x : ℝ) ↦ c) (logb b)

Tactic:
rw [Asymptotics.isLittleO_const_left, or_iff_not_imp_left]

Premises used: Asymptotics.isLittleO_const_left, Classical.or_iff_not_imp_left
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b c : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hc : ¬c = 0
⊢ Tendsto (Norm.norm ∘ logb b) atTop atTop

Tactic:
tendsto_abs_logb_atTop hb

Premises used: abs, Real.tendsto_abs_logb_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b c : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hc : ¬c = 0
⊢ Tendsto (Norm.norm ∘ logb b) atTop atTop

Tactic:
exact tendsto_abs_logb_atTop hb

Premises used: Real.tendsto_abs_logb_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
pos : ∀ (h : b = -1 ∨ b = 0 ∨ b = 1), logb b =O[⊤] log
neg : ∀ (h : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1), logb b =O[⊤] log
⊢ logb b =O[⊤] log

Tactic:
by_cases! h : b = -1 ∨ b = 0 ∨ b = 1
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
h : b = -1 ∨ b = 0 ∨ b = 1
pos : logb (-1) =O[⊤] log
pos₁ : logb 0 =O[⊤] log
pos₂ : logb 1 =O[⊤] log
⊢ logb b =O[⊤] log

Tactic:
obtain rfl | rfl | rfl := h

Premises used: rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
⊢ logb (-1) =O[⊤] log

Tactic:
simpa [-Asymptotics.isBigO_top] using Asymptotics.isBigO_zero log ⊤

Premises used: Asymptotics.isBigO_zero, Asymptotics.isBigO_top, Real.log, Top.top
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
⊢ logb 0 =O[⊤] log

Tactic:
simpa [-Asymptotics.isBigO_top] using Asymptotics.isBigO_zero log ⊤

Premises used: Asymptotics.isBigO_zero, Asymptotics.isBigO_top, Real.log, Top.top
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
⊢ logb 1 =O[⊤] log

Tactic:
simpa [-Asymptotics.isBigO_top] using Asymptotics.isBigO_zero log ⊤

Premises used: Asymptotics.isBigO_zero, Asymptotics.isBigO_top, Real.log, Top.top
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
h : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
⊢ logb b =O[⊤] log

Tactic:
simpa [logb, div_eq_mul_inv, mul_comm]
      using (Asymptotics.isBigO_refl log ⊤).const_mul_left (log b)⁻¹

Premises used: Asymptotics.IsBigO.const_mul_left, div_eq_mul_inv, Real.log, Real.logb, Inv.inv, mul_comm, Top.top, Asymptotics.isBigO_refl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
c : ℝ
inl : Asymptotics.IsBigO (E := ℝ) atTop (fun (x : ℝ) ↦ log (0 * x)) log
inr : ∀ (hc : c ≠ 0), Asymptotics.IsBigO (E := ℝ) atTop (fun (x : ℝ) ↦ log (c * x)) log
⊢ Asymptotics.IsBigO (E := ℝ) atTop (fun (x : ℝ) ↦ log (c * x)) log

Tactic:
obtain rfl | hc := eq_or_ne c 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
⊢ Asymptotics.IsBigO (E := ℝ) atTop (fun (x : ℝ) ↦ log (0 * x)) log

Tactic:
simpa using isLittleO_const_log_atTop.isBigO

Premises used: Real.isLittleO_const_log_atTop, Asymptotics.IsLittleO.isBigO
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
c : ℝ
hc : c ≠ 0
a : ℝ
ha : 0 < a
⊢ log (c * a) = log c + log a

Tactic:
log_mul hc ha.ne'

Premises used: LT.lt.ne', Real.log_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
c : ℝ
hc : c ≠ 0
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ 0 < x) x} x →
          Membership.mem (γ := Set ℝ)
            {x : ℝ | (fun (x : ℝ) ↦ Eq (α := ℝ) ((fun (x : ℝ) ↦ log (c * x)) x) ((fun (x : ℝ) ↦ log c + log x) x)) x} x}
      a
h₁ h₂ : ∀ (a : ℝ) (ha : 0 < a), log (c * a) = log c + log a
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ log (c * x)) fun (x : ℝ) ↦ log c + log x

Tactic:
filter_upwards [eventually_gt_atTop 0] with a ha using log_mul hc ha.ne'

Premises used: OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
c : ℝ
hc : c ≠ 0
⊢ Asymptotics.IsBigO (E := ℝ) atTop (fun (x : ℝ) ↦ log c + log x) log

Tactic:
isLittleO_const_log_atTop.isBigO.add (Asymptotics.isBigO_refl ..)

Premises used: Asymptotics.IsBigO.add, Real.isLittleO_const_log_atTop, Asymptotics.IsLittleO.isBigO, Asymptotics.isBigO_refl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
c : ℝ
hc : c ≠ 0
calc : EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ log (c * x)) fun (x : ℝ) ↦ log c + log x
⊢ Asymptotics.IsBigO (E := ℝ) atTop (fun (x : ℝ) ↦ log (c * x)) log

Tactic:
calc (fun x ↦ log (c * x))
      =ᶠ[atTop] (fun x => log c + log x) := by
          filter_upwards [eventually_gt_atTop 0] with a ha using log_mul hc ha.ne'
      _ =O[atTop] log :=
          isLittleO_const_log_atTop.isBigO.add (Asymptotics.isBigO_refl ..)

Premises used: HMul.hMul, Real.log, Asymptotics.IsBigO.add, Real.isLittleO_const_log_atTop, Filter.atTop, Asymptotics.IsLittleO.isBigO, HAdd.hAdd, Asymptotics.isBigO_refl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
c : ℝ
⊢ Asymptotics.IsBigO (E := ℝ) atTop (fun (x : ℝ) ↦ log (x * c)) log

Tactic:
simpa [mul_comm] using isBigO_log_const_mul_log_atTop c

Premises used: Real.isBigO_log_const_mul_log_atTop, mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b c : ℝ
⊢ Asymptotics.IsBigO (E := ℝ) atTop (fun (x : ℝ) ↦ logb b (c * x)) log

Tactic:
simpa [logb, div_eq_mul_inv, mul_comm]
    using (isBigO_log_const_mul_log_atTop c).const_mul_left (log b)⁻¹

Premises used: Asymptotics.IsBigO.const_mul_left, Real.isBigO_log_const_mul_log_atTop, div_eq_mul_inv, Real.log, Real.logb, Inv.inv, mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b c : ℝ
⊢ Asymptotics.IsBigO (E := ℝ) atTop (fun (x : ℝ) ↦ logb b (x * c)) log

Tactic:
simpa [mul_comm] using isBigO_logb_const_mul_log_atTop c

Premises used: mul_comm, Real.isBigO_logb_const_mul_log_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
α : Type u_1
b : ℝ
f : α → ℝ
l : Filter α
x : ℝ
h : Tendsto f l (𝓝 x)
hx : x ≠ 0
⊢ Tendsto (fun (y : α) ↦ Real.logb b (f y)) l (𝓝 (Real.logb b x))

Tactic:
(continuousAt_logb hx).tendsto.comp h

Premises used: Real.logb, ContinuousAt.tendsto, Real.continuousAt_logb, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
α : Type u_1
b : ℝ
inst : TopologicalSpace α
f : α → ℝ
hf : Continuous[inst, _] f
h₀ : ∀ (x : α), f x ≠ 0
⊢ Continuous[inst, _] fun (x : α) ↦ Real.logb b (f x)

Tactic:
continuousOn_logb.comp_continuous hf h₀

Premises used: ContinuousOn.comp_continuous, Real.continuousOn_logb, Real.logb
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
α : Type u_1
b : ℝ
inst : TopologicalSpace α
f : α → ℝ
a : α
hf : ContinuousAt f a
h₀ : f a ≠ 0
⊢ ContinuousAt (Y := ℝ) (fun (x : α) ↦ Real.logb b (f x)) a

Tactic:
hf.logb h₀

Premises used: Filter.Tendsto.logb, ContinuousAt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
α : Type u_1
b : ℝ
inst : TopologicalSpace α
f : α → ℝ
s : Set α
a : α
hf : ContinuousWithinAt f s a
h₀ : f a ≠ 0
⊢ ContinuousWithinAt (Y := ℝ) (fun (x : α) ↦ Real.logb b (f x)) s a

Tactic:
hf.logb h₀

Premises used: Filter.Tendsto.logb, ContinuousWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
α : Type u_1
b : ℝ
inst : TopologicalSpace α
f : α → ℝ
s : Set α
hf : ContinuousOn f s
h₀ : ∀ x ∈ s, f x ≠ 0
⊢ ContinuousOn (Y := ℝ) (fun (x : α) ↦ Real.logb b (f x)) s

Tactic:
fun x hx => (hf x hx).logb (h₀ x hx)

Premises used: ContinuousWithinAt.logb, ContinuousOn
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b y : ℝ
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ logb b (x + y) - logb b x) atTop (𝓝 0)

Tactic:
simpa [sub_div] using (tendsto_log_comp_add_sub_log y).div_const (log b)

Premises used: sub_div, Real.log, Filter.Tendsto.div_const, Real.tendsto_log_comp_add_sub_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
b : ℝ
⊢ Tendsto (β := ℝ) (fun (k : ℕ) ↦ logb b (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1) - logb b (↑k : ℝ)) atTop (𝓝 0)

Tactic:
(tendsto_logb_comp_add_sub_logb 1).comp tendsto_natCast_atTop_atTop

Premises used: tendsto_natCast_atTop_atTop, Real.tendsto_logb_comp_add_sub_logb, Filter.Tendsto.comp, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
P : ℝ → Prop
x₀ r : ℝ
hr : 1 < r
hx₀ : 0 < x₀
base : ∀ x ∈ Ico x₀ (r * x₀), P x
step : ∀ n ≥ 1, (∀ z ∈ Ico x₀ (r ^ n * x₀), P z) → ∀ z ∈ Ico (r ^ n * x₀) (r ^ (n + 1) * x₀), P z
this : ∀ (n : ℕ), ∀ x ∈ Ico x₀ (r ^ (n + 1) * x₀), P x
x : ℝ
hx : x ≥ x₀
have : ∀ (hx' : 0 < x / x₀), P x
⊢ P x

Tactic:
have hx' : 0 < x / x₀ := div_pos (hx₀.trans_le hx) hx₀
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
P : ℝ → Prop
x₀ r : ℝ
hr : 1 < r
hx₀ : 0 < x₀
base : ∀ x ∈ Ico x₀ (r * x₀), P x
step : ∀ n ≥ 1, (∀ z ∈ Ico x₀ (r ^ n * x₀), P z) → ∀ z ∈ Ico (r ^ n * x₀) (r ^ (n + 1) * x₀), P z
this : ∀ (n : ℕ), ∀ x ∈ Ico x₀ (r ^ (n + 1) * x₀), P x
x : ℝ
hx : x ≥ x₀
hx' : 0 < x / x₀
⊢ P x

Tactic:
this ⌊logb r (x / x₀)⌋₊ x ?_

Premises used: HDiv.hDiv, Real.logb, Nat.floor
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
P : ℝ → Prop
x₀ r : ℝ
hr : 1 < r
hx₀ : 0 < x₀
base : ∀ x ∈ Ico x₀ (r * x₀), P x
step : ∀ n ≥ 1, (∀ z ∈ Ico x₀ (r ^ n * x₀), P z) → ∀ z ∈ Ico (r ^ n * x₀) (r ^ (n + 1) * x₀), P z
this : ∀ (n : ℕ), ∀ x ∈ Ico x₀ (r ^ (n + 1) * x₀), P x
x : ℝ
hx : x ≥ x₀
hx' : 0 < x / x₀
refine : x ∈ Ico x₀ (r ^ (⌊logb r (x / x₀)⌋₊ + 1) * x₀)
⊢ P x

Tactic:
refine this ⌊logb r (x / x₀)⌋₊ x ?_

Premises used: HDiv.hDiv, Real.logb, Nat.floor
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
P : ℝ → Prop
x₀ r : ℝ
hr : 1 < r
hx₀ : 0 < x₀
base : ∀ x ∈ Ico x₀ (r * x₀), P x
step : ∀ n ≥ 1, (∀ z ∈ Ico x₀ (r ^ n * x₀), P z) → ∀ z ∈ Ico (r ^ n * x₀) (r ^ (n + 1) * x₀), P z
this : ∀ (n : ℕ), ∀ x ∈ Ico x₀ (r ^ (n + 1) * x₀), P x
x : ℝ
hx : x ≥ x₀
hx' : 0 < x / x₀
rw : x₀ ≤ x ∧ logb r (x / x₀) < HAdd.hAdd (α := ℝ) (↑⌊logb r (x / x₀)⌋₊ : ℝ) 1
⊢ x ∈ Ico x₀ (r ^ (⌊logb r (x / x₀)⌋₊ + 1) * x₀)

Tactic:
rw [mem_Ico, ← div_lt_iff₀ hx₀, ← rpow_natCast, ← logb_lt_iff_lt_rpow hr hx', Nat.cast_add,
      Nat.cast_one]

Premises used: Real.logb_lt_iff_lt_rpow, Set.mem_Ico, div_lt_iff₀, Nat.cast_add, Nat.cast_one, Real.rpow_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
P : ℝ → Prop
x₀ r : ℝ
hr : 1 < r
hx₀ : 0 < x₀
base : ∀ x ∈ Ico x₀ (r * x₀), P x
step : ∀ n ≥ 1, (∀ z ∈ Ico x₀ (r ^ n * x₀), P z) → ∀ z ∈ Ico (r ^ n * x₀) (r ^ (n + 1) * x₀), P z
this : ∀ (n : ℕ), ∀ x ∈ Ico x₀ (r ^ (n + 1) * x₀), P x
x : ℝ
hx : x ≥ x₀
hx' : 0 < x / x₀
⊢ x₀ ≤ x ∧ logb r (x / x₀) < HAdd.hAdd (α := ℝ) (↑⌊logb r (x / x₀)⌋₊ : ℝ) 1

Tactic:
⟨hx, Nat.lt_floor_add_one _⟩

Premises used: And.intro, Nat.lt_floor_add_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
P : ℝ → Prop
x₀ r : ℝ
hr : 1 < r
hx₀ : 0 < x₀
base : ∀ x ∈ Ico x₀ (r * x₀), P x
step : ∀ n ≥ 1, (∀ z ∈ Ico x₀ (r ^ n * x₀), P z) → ∀ z ∈ Ico (r ^ n * x₀) (r ^ (n + 1) * x₀), P z
this : ∀ (n : ℕ), ∀ x ∈ Ico x₀ (r ^ (n + 1) * x₀), P x
x : ℝ
hx : x ≥ x₀
hx' : 0 < x / x₀
⊢ x₀ ≤ x ∧ logb r (x / x₀) < HAdd.hAdd (α := ℝ) (↑⌊logb r (x / x₀)⌋₊ : ℝ) 1

Tactic:
exact ⟨hx, Nat.lt_floor_add_one _⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
P : ℝ → Prop
x₀ r : ℝ
hr : 1 < r
hx₀ : 0 < x₀
base : ∀ x ∈ Ico x₀ (r * x₀), P x
step : ∀ n ≥ 1, (∀ z ∈ Ico x₀ (r ^ n * x₀), P z) → ∀ z ∈ Ico (r ^ n * x₀) (r ^ (n + 1) * x₀), P z
suffices : ∀ (n : ℕ), ∀ x ∈ Ico x₀ (r ^ (n + 1) * x₀), P x
⊢ ∀ x ≥ x₀, P x

Tactic:
suffices ∀ n : ℕ, ∀ x ∈ Set.Ico x₀ (r ^ (n + 1) * x₀), P x by
    intro x hx
    have hx' : 0 < x / x₀ := div_pos (hx₀.trans_le hx) hx₀
    refine this ⌊logb r (x / x₀)⌋₊ x ?_
    rw [mem_Ico, ← div_lt_iff₀ hx₀, ← rpow_natCast, ← logb_lt_iff_lt_rpow hr hx', Nat.cast_add,
      Nat.cast_one]
    exact ⟨hx, Nat.lt_floor_add_one _⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
P : ℝ → Prop
x₀ r : ℝ
hr : 1 < r
hx₀ : 0 < x₀
base : ∀ x ∈ Ico x₀ (r * x₀), P x
step : ∀ n ≥ 1, (∀ z ∈ Ico x₀ (r ^ n * x₀), P z) → ∀ z ∈ Ico (r ^ n * x₀) (r ^ (n + 1) * x₀), P z
⊢ ∀ x ∈ Ico x₀ (r ^ HAdd.hAdd (α := ℕ) 0 1 * x₀), P x

Tactic:
simpa using base
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
P : ℝ → Prop
x₀ r : ℝ
hr : 1 < r
hx₀ : 0 < x₀
base : ∀ x ∈ Ico x₀ (r * x₀), P x
step : ∀ n ≥ 1, (∀ z ∈ Ico x₀ (r ^ n * x₀), P z) → ∀ z ∈ Ico (r ^ n * x₀) (r ^ (n + 1) * x₀), P z
n : ℕ
ih : ∀ x ∈ Ico x₀ (r ^ (n + 1) * x₀), P x
x : ℝ
hx : x ∈ Ico x₀ (r ^ (n + 1 + 1) * x₀)
⊢ n + 1 ≥ 1

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
P : ℝ → Prop
x₀ r : ℝ
hr : 1 < r
hx₀ : 0 < x₀
base : ∀ x ∈ Ico x₀ (r * x₀), P x
step : ∀ n ≥ 1, (∀ z ∈ Ico x₀ (r ^ n * x₀), P z) → ∀ z ∈ Ico (r ^ n * x₀) (r ^ (n + 1) * x₀), P z
n : ℕ
ih : ∀ x ∈ Ico x₀ (r ^ (n + 1) * x₀), P x
⊢ ∀ x ∈ Ico x₀ (r ^ (n + 1 + 1) * x₀), P x

Tactic:
exact fun x hx => (Ico_subset_Ico_union_Ico hx).elim (ih x) (step (n + 1) (by simp) ih _)

Premises used: Set.Ico_subset_Ico_union_Ico, HAdd.hAdd, Or.elim, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Base
Goal:
P : ℝ → Prop
x₀ r : ℝ
hr : 1 < r
hx₀ : 0 < x₀
base : ∀ x ∈ Ico x₀ (r * x₀), P x
step : ∀ n ≥ 1, (∀ z ∈ Ico x₀ (r ^ n * x₀), P z) → ∀ z ∈ Ico (r ^ n * x₀) (r ^ (n + 1) * x₀), P z
n : ℕ
zero : ∀ x ∈ Ico x₀ (r ^ HAdd.hAdd (α := ℕ) 0 1 * x₀), P x
succ : ∀ (n : ℕ) (ih : ∀ x ∈ Ico x₀ (r ^ (n + 1) * x₀), P x), ∀ x ∈ Ico x₀ (r ^ (n + 1 + 1) * x₀), P x
⊢ ∀ x ∈ Ico x₀ (r ^ (n + 1) * x₀), P x

Tactic:
induction n with
  | zero => simpa using base
  | succ n ih =>
    exact fun x hx => (Ico_subset_Ico_union_Ico hx).elim (ih x) (step (n + 1) (by simp) ih _)
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx : x ≠ 0
⊢ log x =
    (expOrderIso.symm : (a : (↑(Ioi 0) : Type)) → ℝ)
      (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) |x| ⋯)

Tactic:
dif_neg hx

Premises used: dif_neg, Real.log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx : 0 < x
rw :
  Eq (α := ℝ)
    ((expOrderIso.symm : (a : (↑(Ioi 0) : Type)) → ℝ)
        (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) |x| ⋯) :
      ℝ)
    ((expOrderIso.symm : (a : (↑(Ioi 0) : Type)) → ℝ)
        (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) x hx) :
      ℝ)
⊢ log x =
    (expOrderIso.symm : (a : (↑(Ioi 0) : Type)) → ℝ)
      (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) x hx)

Tactic:
rw [log_of_ne_zero hx.ne']

Premises used: LT.lt.ne', Real.log_of_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx : 0 < x
h : |x| = x
⊢ Eq (α := ℝ)
    ((expOrderIso.symm : (a : (↑(Ioi 0) : Type)) → ℝ)
        (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) |x| ⋯) :
      ℝ)
    ((expOrderIso.symm : (a : (↑(Ioi 0) : Type)) → ℝ)
        (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) x hx) :
      ℝ)

Tactic:
congr
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx : 0 < x
⊢ |x| = x

Tactic:
abs_of_pos hx

Premises used: abs_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx : 0 < x
⊢ |x| = x

Tactic:
exact abs_of_pos hx

Premises used: abs_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx : x ≠ 0
rw :
  rexp
      ((expOrderIso.symm : (a : (↑(Ioi 0) : Type)) → ℝ)
        (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) |x| ⋯)) =
    |x|
rw₁ :
  (↑((expOrderIso : (a : ℝ) → (↑(Ioi 0) : Type))
          ((expOrderIso.symm : (a : (↑(Ioi 0) : Type)) → ℝ)
            (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) |x| ⋯))) :
      ℝ) =
    |x|
rw₂ : (↑(Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) |x| ⋯) : ℝ) = |x|
rw₃ rw₄ : |x| = |x|
⊢ rexp (log x) = |x|

Tactic:
rw [log_of_ne_zero hx, ← coe_expOrderIso_apply, OrderIso.apply_symm_apply, Subtype.coe_mk]

Premises used: Subtype.coe_mk, OrderIso.apply_symm_apply, Real.coe_expOrderIso_apply, Real.log_of_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx : 0 < x
rw : |x| = x
⊢ rexp (log x) = x

Tactic:
rw [exp_log_eq_abs hx.ne']

Premises used: LT.lt.ne', Real.exp_log_eq_abs
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx : x < 0
rw : |x| = -x
⊢ rexp (log x) = -x

Tactic:
rw [exp_log_eq_abs (ne_of_lt hx)]

Premises used: ne_of_lt, Real.exp_log_eq_abs
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx : x < 0
⊢ |x| = -x

Tactic:
abs_of_neg hx

Premises used: abs_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
hx : x < 0
⊢ |x| = -x

Tactic:
exact abs_of_neg hx

Premises used: abs_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
pos : ∀ (h_zero : x = 0), x ≤ rexp (log x)
neg : ∀ (h_zero : ¬x = 0), x ≤ rexp (log x)
⊢ x ≤ rexp (log x)

Tactic:
by_cases h_zero : x = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h_zero : x = 0
pos : LE.le (α := ℝ) 0 1
⊢ x ≤ rexp (log x)

Tactic:
rw [h_zero, log, dif_pos rfl, exp_zero]

Premises used: dif_pos, Real.log, Real.exp_zero, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h_zero : x = 0
⊢ LE.le (α := ℝ) 0 1

Tactic:
zero_le_one

Premises used: zero_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h_zero : x = 0
⊢ LE.le (α := ℝ) 0 1

Tactic:
exact zero_le_one

Premises used: zero_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h_zero : ¬x = 0
neg : x ≤ |x|
⊢ x ≤ rexp (log x)

Tactic:
rw [exp_log_eq_abs h_zero]

Premises used: Real.exp_log_eq_abs
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x : ℝ
h_zero : ¬x = 0
⊢ x ≤ |x|

Tactic:
le_abs_self _

Premises used: le_abs_self