awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ x ∈ s, f x ≠ 0
⊢ ∀ (x : ℝ), Membership.mem (γ := List ℝ) (List.map (fun (i : α) ↦ f i) s.toList) x → x ≠ 0

Tactic:
simp_all
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ x ∈ s, f x ≠ 0
rw :
  Eq (α := ℝ) (List.sum (List.map (fun (x : ℝ) ↦ log x) (List.map (fun (i : α) ↦ f i) s.toList))) (∑ i ∈ s, log (f i))
⊢ log (∏ i ∈ s, f i) = ∑ i ∈ s, log (f i)

Tactic:
rw [← prod_map_toList, log_list_prod (by simp_all)]

Premises used: Finset.prod_map_toList, Real.log_list_prod
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ x ∈ s, f x ≠ 0
⊢ Eq (α := ℝ) (List.sum (List.map (fun (x : ℝ) ↦ log x) (List.map (fun (i : α) ↦ f i) s.toList))) (∑ i ∈ s, log (f i))

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
α : 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 : β)
⊢ log (f.prod g) = f.sum fun (a : α) (b : β) ↦ log (g a b)

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

Premises used: Finsupp.mem_support_iff, Real.log_prod, Finsupp.sum, Iff.mp, Finsupp.prod
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
α : Type u_1
f : α → ℝ
h : ∀ (a : α), 0 < f a
⊢ (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f

Tactic:
grind [mem_mulSupport, mem_support, log_eq_zero]

Premises used: Function.mem_mulSupport, Real.log_eq_zero, Function.mem_support
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
α : Type u_1
f : α → ℝ
h : ∀ (a : α), 0 < f a
⊢ (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f

Tactic:
have H : (fun i ↦ log (f i)).support = f.mulSupport := by
    grind [mem_mulSupport, mem_support, log_eq_zero]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
α : Type u_1
f : α → ℝ
h : ∀ (a : α), 0 < f a
H : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f
⊢ HasFiniteMulSupport f ↔ HasFiniteSupport (M := ℝ) fun (a : α) ↦ log (f a)

Tactic:
simp [HasFiniteMulSupport, HasFiniteSupport, H]

Premises used: Function.HasFiniteSupport, Function.HasFiniteMulSupport
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
α : Type u_1
f : α → ℝ
h : ∀ (a : α), 0 < f a
H : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f
⊢ HasFiniteMulSupport f ↔ HasFiniteSupport (M := ℝ) fun (a : α) ↦ log (f a)

Tactic:
have H' : HasFiniteMulSupport f ↔ HasFiniteSupport fun a ↦ log (f a) := by
    simp [HasFiniteMulSupport, HasFiniteSupport, H]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
α : Type u_1
f : α → ℝ
h : ∀ (a : α), 0 < f a
H : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f
H' : HasFiniteMulSupport f ↔ HasFiniteSupport (M := ℝ) fun (a : α) ↦ log (f a)
simp :
  log (if h : HasFiniteMulSupport f then ∏ i ∈ Finite.toFinset (s := mulSupport f) h, f i else 1) =
    if h : HasFiniteSupport (M := ℝ) fun (i : α) ↦ log (f i) then
      ∑ i ∈ Finite.toFinset (s := support (M := ℝ) fun (i : α) ↦ log (f i)) h, log (f i)
    else 0
⊢ log (∏ᶠ (a : α), f a) = ∑ᶠ (a : α), log (f a)

Tactic:
simp only [finprod_def, finsum_def]

Premises used: finsum_def, finprod_def
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
α : Type u_1
f : α → ℝ
h : ∀ (a : α), 0 < f a
H : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f
H' : HasFiniteMulSupport f ↔ HasFiniteSupport (M := ℝ) fun (a : α) ↦ log (f a)
pos :
  ∀ (h' : HasFiniteMulSupport f),
    log (if h : HasFiniteMulSupport f then ∏ i ∈ Finite.toFinset (s := mulSupport f) h, f i else 1) =
      if h : HasFiniteSupport (M := ℝ) fun (i : α) ↦ log (f i) then
        ∑ i ∈ Finite.toFinset (s := support (M := ℝ) fun (i : α) ↦ log (f i)) h, log (f i)
      else 0
neg :
  ∀ (h' : ¬HasFiniteMulSupport f),
    log (if h : HasFiniteMulSupport f then ∏ i ∈ Finite.toFinset (s := mulSupport f) h, f i else 1) =
      if h : HasFiniteSupport (M := ℝ) fun (i : α) ↦ log (f i) then
        ∑ i ∈ Finite.toFinset (s := support (M := ℝ) fun (i : α) ↦ log (f i)) h, log (f i)
      else 0
⊢ log (if h : HasFiniteMulSupport f then ∏ i ∈ Finite.toFinset (s := mulSupport f) h, f i else 1) =
    if h : HasFiniteSupport (M := ℝ) fun (i : α) ↦ log (f i) then
      ∑ i ∈ Finite.toFinset (s := support (M := ℝ) fun (i : α) ↦ log (f i)) h, log (f i)
    else 0

Tactic:
by_cases h' : HasFiniteMulSupport f

Premises used: Function.HasFiniteMulSupport
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
α : Type u_1
f : α → ℝ
h : ∀ (a : α), 0 < f a
H : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f
H' : HasFiniteMulSupport f ↔ HasFiniteSupport (M := ℝ) fun (a : α) ↦ log (f a)
h' : HasFiniteMulSupport f
⊢ log (if h : HasFiniteMulSupport f then ∏ i ∈ Finite.toFinset (s := mulSupport f) h, f i else 1) =
    if h : HasFiniteSupport (M := ℝ) fun (i : α) ↦ log (f i) then
      ∑ i ∈ Finite.toFinset (s := support (M := ℝ) fun (i : α) ↦ log (f i)) h, log (f i)
    else 0

Tactic:
simp [h', log_prod (fun a _ ↦ (h a).ne'), H'.mp h', H]

Premises used: Real.log_prod, LT.lt.ne', Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
α : Type u_1
f : α → ℝ
h : ∀ (a : α), 0 < f a
H : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f
H' : HasFiniteMulSupport f ↔ HasFiniteSupport (M := ℝ) fun (a : α) ↦ log (f a)
h' : ¬HasFiniteMulSupport f
⊢ log (if h : HasFiniteMulSupport f then ∏ i ∈ Finite.toFinset (s := mulSupport f) h, f i else 1) =
    if h : HasFiniteSupport (M := ℝ) fun (i : α) ↦ log (f i) then
      ∑ i ∈ Finite.toFinset (s := support (M := ℝ) fun (i : α) ↦ log (f i)) h, log (f i)
    else 0

Tactic:
simp [h', mt H'.mpr h']

Premises used: Iff.mpr, mt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
α : Type u_1
f : α → ℝ
h : ∀ (a : α), 0 < f a
have : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f
have₁ : ∀ (H : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f), log (∏ᶠ (a : α), f a) = ∑ᶠ (a : α), log (f a)
have₂ : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f
have₃ have₄ :
  ∀ (H : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f), log (∏ᶠ (a : α), f a) = ∑ᶠ (a : α), log (f a)
have₅ :
  ∀ (H : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f)
    (H' : HasFiniteMulSupport f ↔ HasFiniteSupport (M := ℝ) fun (a : α) ↦ log (f a)),
    log (∏ᶠ (a : α), f a) = ∑ᶠ (a : α), log (f a)
have₆ :
  ∀ (H : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f)
    (H' : HasFiniteMulSupport f ↔ HasFiniteSupport (M := ℝ) fun (a : α) ↦ log (f a)),
    log (if h : HasFiniteMulSupport f then ∏ i ∈ Finite.toFinset (s := mulSupport f) h, f i else 1) =
      if h : HasFiniteSupport (M := ℝ) fun (i : α) ↦ log (f i) then
        ∑ i ∈ Finite.toFinset (s := support (M := ℝ) fun (i : α) ↦ log (f i)) h, log (f i)
      else 0
pos :
  ∀ (H : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f)
    (H' : HasFiniteMulSupport f ↔ HasFiniteSupport (M := ℝ) fun (a : α) ↦ log (f a)) (h' : HasFiniteMulSupport f),
    log (if h : HasFiniteMulSupport f then ∏ i ∈ Finite.toFinset (s := mulSupport f) h, f i else 1) =
      if h : HasFiniteSupport (M := ℝ) fun (i : α) ↦ log (f i) then
        ∑ i ∈ Finite.toFinset (s := support (M := ℝ) fun (i : α) ↦ log (f i)) h, log (f i)
      else 0
neg neg₁ :
  ∀ (H : (support (M := ℝ) fun (i : α) ↦ log (f i)) = mulSupport f)
    (H' : HasFiniteMulSupport f ↔ HasFiniteSupport (M := ℝ) fun (a : α) ↦ log (f a)) (h' : ¬HasFiniteMulSupport f),
    log (if h : HasFiniteMulSupport f then ∏ i ∈ Finite.toFinset (s := mulSupport f) h, f i else 1) =
      if h : HasFiniteSupport (M := ℝ) fun (i : α) ↦ log (f i) then
        ∑ i ∈ Finite.toFinset (s := support (M := ℝ) fun (i : α) ↦ log (f i)) h, log (f i)
      else 0
⊢ log (∏ᶠ (a : α), f a) = ∑ᶠ (a : α), log (f a)

Tactic:
classical
  have H : (fun i ↦ log (f i)).support = f.mulSupport := by
    grind [mem_mulSupport, mem_support, log_eq_zero]
  have H' : HasFiniteMulSupport f ↔ HasFiniteSupport fun a ↦ log (f a) := by
    simp [HasFiniteMulSupport, HasFiniteSupport, H]
  simp only [finprod_def, finsum_def]
  by_cases h' : HasFiniteMulSupport f
  · simp [h', log_prod (fun a _ ↦ (h a).ne'), H'.mp h', H]
  · simp [h', mt H'.mpr h']

Premises used: Real.log_prod, finsum_def, LT.lt.ne', Function.HasFiniteMulSupport, finprod_def
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
n : ℕ
inl : log (↑0 : ℝ) = (Nat.factorization 0).sum fun (p t : ℕ) ↦ (↑t : ℝ) * log (↑p : ℝ)
inr : ∀ (hn : n ≠ 0), log (↑n : ℝ) = n.factorization.sum fun (p t : ℕ) ↦ (↑t : ℝ) * log (↑p : ℝ)
⊢ log (↑n : ℝ) = n.factorization.sum fun (p t : ℕ) ↦ (↑t : ℝ) * log (↑p : ℝ)

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
⊢ log (↑0 : ℝ) = (Nat.factorization 0).sum fun (p t : ℕ) ↦ (↑t : ℝ) * log (↑p : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
n : ℕ
hn : n ≠ 0
inr : log (↑n : ℝ) = n.factorization.sum fun (p t : ℕ) ↦ log (↑(p ^ t) : ℝ)
⊢ log (↑n : ℝ) = n.factorization.sum fun (p t : ℕ) ↦ (↑t : ℝ) * log (↑p : ℝ)

Tactic:
simp only [← log_pow, ← Nat.cast_pow]

Premises used: Real.log_pow, Nat.cast_pow
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
n : ℕ
hn : n ≠ 0
inr :
  ∀ (a : ℕ),
    Eq (α := ℝ) (↑(HPow.hPow (β := ℕ) a ((n.factorization : (a : ℕ) → ℕ) a : ℕ)) : ℝ) 0 →
      Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) a : ℕ) (0 : ℕ)
⊢ log (↑n : ℝ) = n.factorization.sum fun (p t : ℕ) ↦ log (↑(p ^ t) : ℝ)

Tactic:
rw [← Finsupp.log_prod, ← Nat.cast_finsuppProd, Nat.prod_factorization_pow_eq_self hn]

Premises used: Nat.cast_finsuppProd, Nat.prod_factorization_pow_eq_self, Finsupp.log_prod
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
n : ℕ
hn : n ≠ 0
p : ℕ
hp : Eq (α := ℝ) (↑(HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)) : ℝ) 0
inr : Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) 0 : ℕ) (0 : ℕ)
inr₁ inr₂ : Eq (α := ℕ) 0 0
⊢ Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)

Tactic:
rw [eq_zero_of_pow_eq_zero (Nat.cast_eq_zero.1 hp), Nat.factorization_zero_right]

Premises used: Nat.cast_eq_zero, Iff.mp, eq_zero_of_pow_eq_zero, Nat.factorization_zero_right
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
a b : ℝ
n : ℕ
ha : a ≠ 0
x : ℝ
hx : 0 < x
⊢ ((fun (x : ℝ) ↦ x ^ n / (a * rexp x + b)) ∘ log) x = log x ^ n / (a * x + b)

Tactic:
simp [exp_log hx]

Premises used: Real.exp_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
a b : ℝ
n : ℕ
ha : a ≠ 0
h :
  ∀ (a_1 : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ 0 < x) x} x →
          Membership.mem (γ := Set ℝ)
            {x : ℝ |
              (fun (x : ℝ) ↦
                  Eq (α := ℝ) (((fun (x : ℝ) ↦ x ^ n / (a * rexp x + b)) ∘ log) x)
                    ((fun (x : ℝ) ↦ log x ^ n / (a * x + b)) x))
                x}
            x}
      a_1
h₁ h₂ : ∀ (x : ℝ) (hx : 0 < x), ((fun (x : ℝ) ↦ x ^ n / (a * rexp x + b)) ∘ log) x = log x ^ n / (a * x + b)
⊢ EventuallyEq (β := ℝ) atTop ((fun (x : ℝ) ↦ x ^ n / (a * rexp x + b)) ∘ log) fun (x : ℝ) ↦ log x ^ n / (a * x + b)

Tactic:
filter_upwards [eventually_gt_atTop (0 : ℝ)] with x hx using by simp [exp_log hx]

Premises used: OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
n : ℕ
rw : Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x ^ n / id x) atTop (𝓝 0)
rw₁ : ∀ᶠ (x : ℝ) in atTop, id x = 0 → log x ^ n = 0
⊢ Asymptotics.IsLittleO (E := ℝ) atTop (fun (x : ℝ) ↦ log x ^ n) id

Tactic:
rw [Asymptotics.isLittleO_iff_tendsto']

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

Tactic:
simpa using tendsto_pow_log_div_mul_add_atTop 1 0 n one_ne_zero

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

Tactic:
(h₁ h₂).elim

Premises used: False.elim
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
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 → log x ^ n = 0) x} x}
      a
h₁ h₂ : ∀ (x : ℝ) (h₁ : x ≠ 0) (h₂ : id x = 0), log x ^ n = 0
⊢ ∀ᶠ (x : ℝ) in atTop, id x = 0 → log 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.Basic
Goal:
⊢ log =o[atTop] id

Tactic:
isLittleO_pow_log_id_atTop.congr_left fun _ => pow_one _

Premises used: Asymptotics.IsLittleO.congr_left, Real.log, pow_one, Real.isLittleO_pow_log_id_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
c : ℝ
⊢ Tendsto (fun (x : ℝ) ↦ c) atTop (𝓝 c)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
c : ℝ
refine : ∀ᶠ (x : ℝ) in atTop, log x = 0 → c = 0
⊢ Asymptotics.IsLittleO (E := ℝ) atTop (fun (x : ℝ) ↦ c) log

Tactic:
refine Asymptotics.isLittleO_of_tendsto' ?_
    <| Tendsto.div_atTop (a := c) (by simp) tendsto_log_atTop

Premises used: Filter.Tendsto.div_atTop, Asymptotics.isLittleO_of_tendsto', Real.tendsto_log_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
c : ℝ
h : ∀ (x : ℝ) (hx : 1 < x), log x = 0 → c = 0
⊢ ∀ᶠ (x : ℝ) in atTop, log x = 0 → c = 0

Tactic:
filter_upwards [eventually_gt_atTop 1] with x hx

Premises used: OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
c x : ℝ
hx : 1 < x
⊢ log x = 0 → c = 0

Tactic:
aesop (add safe forward log_pos)

Premises used: Real.log_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
x y x_1 : ℝ
h : Membership.mem (γ := Set ℝ) univ x_1
⊢ log (rexp x_1) = x_1

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
p : ℕ
hp : Prime p
⊢ 0 < Real.log (↑p : ℝ)

Tactic:
Real.log_pos <| mod_cast hp.one_lt

Premises used: Nat.Prime.one_lt, congrArg, Nat.cast_lt._simp_1, cast, Real.log_pos, Nat.cast, LT.lt, congrFun', Eq.symm, Nat.cast_one, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
p : ℕ
hp : Prime p
⊢ Real.log (↑p : ℝ) ≠ 0

Tactic:
hp.log_pos.ne'

Premises used: Nat.Prime.log_pos, LT.lt.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
α : Type u_1
f : α → ℝ
l : Filter α
x : ℝ
h : Tendsto f l (𝓝 x)
hx : x ≠ 0
⊢ Tendsto (fun (x : α) ↦ Real.log (f x)) l (𝓝 (Real.log x))

Tactic:
(continuousAt_log hx).tendsto.comp h

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

Tactic:
continuousOn_log.comp_continuous hf h₀

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

Tactic:
hf.log h₀

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

Tactic:
hf.log h₀

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

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

Premises used: ContinuousWithinAt.log, ContinuousOn
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
y : ℝ
⊢ Tendsto (fun (x : ℝ) ↦ 1 + y / x) atTop (𝓝 (HAdd.hAdd (α := ℝ) 1 0))

Tactic:
have : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0)) :=
    tendsto_const_nhds.add (tendsto_const_nhds.div_atTop tendsto_id)
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
y : ℝ
this : Tendsto (fun (x : ℝ) ↦ 1 + y / x) atTop (𝓝 (HAdd.hAdd (α := ℝ) 1 0))
rw : Tendsto (α := ℝ) (rexp ∘ fun (x : ℝ) ↦ log (x + y) - log x) atTop (𝓝 (HAdd.hAdd (α := ℝ) 1 0))
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ log (x + y) - log x) atTop (𝓝 0)

Tactic:
rw [← comap_exp_nhds_exp, exp_zero, tendsto_comap_iff, ← add_zero (1 : ℝ)]

Premises used: Real.comap_exp_nhds_exp, Filter.tendsto_comap_iff, Real.exp_zero, add_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
y : ℝ
this : Tendsto (fun (x : ℝ) ↦ 1 + y / x) atTop (𝓝 (HAdd.hAdd (α := ℝ) 1 0))
⊢ Tendsto (α := ℝ) (rexp ∘ fun (x : ℝ) ↦ log (x + y) - log x) atTop (𝓝 (HAdd.hAdd (α := ℝ) 1 0))

Tactic:
this.congr' ?_

Premises used: Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
y : ℝ
this : Tendsto (fun (x : ℝ) ↦ 1 + y / x) atTop (𝓝 (HAdd.hAdd (α := ℝ) 1 0))
refine : (fun (x : ℝ) ↦ 1 + y / x) =ᶠ[atTop] rexp ∘ fun (x : ℝ) ↦ log (x + y) - log x
⊢ Tendsto (α := ℝ) (rexp ∘ fun (x : ℝ) ↦ log (x + y) - log x) atTop (𝓝 (HAdd.hAdd (α := ℝ) 1 0))

Tactic:
refine this.congr' ?_

Premises used: Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
y : ℝ
this : Tendsto (fun (x : ℝ) ↦ 1 + y / x) atTop (𝓝 (HAdd.hAdd (α := ℝ) 1 0))
h : ∀ (x : ℝ) (hx₀ : 0 < x) (hxy : -y < x), 1 + y / x = (rexp ∘ fun (x : ℝ) ↦ log (x + y) - log x) x
⊢ (fun (x : ℝ) ↦ 1 + y / x) =ᶠ[atTop] rexp ∘ fun (x : ℝ) ↦ log (x + y) - log x

Tactic:
filter_upwards [eventually_gt_atTop (0 : ℝ), eventually_gt_atTop (-y)] with x hx₀ hxy

Premises used: OfNat.ofNat, Neg.neg, Filter.eventually_gt_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
y : ℝ
this : Tendsto (fun (x : ℝ) ↦ 1 + y / x) atTop (𝓝 (HAdd.hAdd (α := ℝ) 1 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
h : x ≠ 0
h₁ : 0 < x
h₂ : 0 < x + y
⊢ 1 + y / x = (rexp ∘ fun (x : ℝ) ↦ log (x + y) - log x) x

Tactic:
rw [comp_apply, exp_sub, exp_log, exp_log, one_add_div]

Premises used: Real.exp_log, Function.comp_apply, one_add_div, Real.exp_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
y : ℝ
this : Tendsto (fun (x : ℝ) ↦ 1 + y / x) atTop (𝓝 (HAdd.hAdd (α := ℝ) 1 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
linarith : x = 0 → 0 - x + (x - 0) = 0
⊢ x ≠ 0

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
y : ℝ
this : Tendsto (fun (x : ℝ) ↦ 1 + y / x) atTop (𝓝 (HAdd.hAdd (α := ℝ) 1 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
linarith : x ≤ 0 → 0 - x + (x - 0) = 0
⊢ 0 < x

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
y : ℝ
this : Tendsto (fun (x : ℝ) ↦ 1 + y / x) atTop (𝓝 (HAdd.hAdd (α := ℝ) 1 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
linarith : x + y ≤ 0 → -y - x + (x + y - 0) = 0
⊢ 0 < x + y

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
⊢ Tendsto (β := ℝ) (fun (k : ℕ) ↦ log (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1) - log (↑k : ℝ)) atTop (𝓝 0)

Tactic:
(tendsto_log_comp_add_sub_log 1).comp tendsto_natCast_atTop_atTop

Premises used: Real.tendsto_log_comp_add_sub_log, tendsto_natCast_atTop_atTop, Filter.Tendsto.comp, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
e : ℝ
n : ℕ
h : NormNum.IsNat e n
rw : 0 ≤ Real.log (↑n : ℝ)
⊢ 0 ≤ Real.log e

Tactic:
rw [NormNum.IsNat.to_eq h rfl]

Premises used: Mathlib.Meta.NormNum.IsNat.to_eq, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
e : ℝ
n : ℕ
h : NormNum.IsNat e n
⊢ 0 ≤ Real.log (↑n : ℝ)

Tactic:
Real.log_natCast_nonneg _

Premises used: Real.log_natCast_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
e : ℝ
n : ℕ
h : NormNum.IsNat e n
⊢ 0 ≤ Real.log (↑n : ℝ)

Tactic:
exact Real.log_natCast_nonneg _

Premises used: Real.log_natCast_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
e : ℝ
n : ℕ
h : NormNum.IsNat e n
w : Nat.blt 1 n = true
rw : 0 < Real.log (↑n : ℝ)
⊢ 0 < Real.log e

Tactic:
rw [NormNum.IsNat.to_eq h rfl]

Premises used: Mathlib.Meta.NormNum.IsNat.to_eq, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
e : ℝ
n : ℕ
h : NormNum.IsNat e n
w : Nat.blt 1 n = true
hx : LT.lt (α := ℝ) 1 (↑n : ℝ)
⊢ 0 < Real.log (↑n : ℝ)

Tactic:
apply Real.log_pos

Premises used: Real.log_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
e : ℝ
n : ℕ
h : NormNum.IsNat e n
w : Nat.blt 1 n = true
⊢ LT.lt (α := ℝ) 1 (↑n : ℝ)

Tactic:
simpa using w
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
rw : 0 ≤ Real.log (-(↑n : ℝ))
⊢ 0 ≤ Real.log e

Tactic:
rw [NormNum.IsInt.neg_to_eq h rfl]

Premises used: Mathlib.Meta.NormNum.IsInt.neg_to_eq, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
⊢ 0 ≤ Real.log (-(↑n : ℝ))

Tactic:
Real.log_neg_natCast_nonneg _

Premises used: Real.log_neg_natCast_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
⊢ 0 ≤ Real.log (-(↑n : ℝ))

Tactic:
exact Real.log_neg_natCast_nonneg _

Premises used: Real.log_neg_natCast_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.blt 1 n = true
rw : 0 < Real.log (-(↑n : ℝ))
⊢ 0 < Real.log e

Tactic:
rw [NormNum.IsInt.neg_to_eq h rfl]

Premises used: Mathlib.Meta.NormNum.IsInt.neg_to_eq, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.blt 1 n = true
rw : 0 < Real.log (↑n : ℝ)
⊢ 0 < Real.log (-(↑n : ℝ))

Tactic:
rw [Real.log_neg_eq_log]

Premises used: Real.log_neg_eq_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.blt 1 n = true
hx : LT.lt (α := ℝ) 1 (↑n : ℝ)
⊢ 0 < Real.log (↑n : ℝ)

Tactic:
apply Real.log_pos

Premises used: Real.log_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.blt 1 n = true
⊢ LT.lt (α := ℝ) 1 (↑n : ℝ)

Tactic:
simpa using w
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
e : ℝ
d n : ℕ
inv : Invertible (α := ℝ) (↑d : ℝ)
eq : e = HMul.hMul (α := ℝ) (↑n : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℝ) _)
h : decide (1 < HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)) = true
rw : 0 < Real.log (HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ))
⊢ 0 < Real.log e

Tactic:
rw [eq, invOf_eq_inv, ← div_eq_mul_inv]

Premises used: div_eq_mul_inv, invOf_eq_inv
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
e : ℝ
d n : ℕ
inv : Invertible (α := ℝ) (↑d : ℝ)
eq : e = HMul.hMul (α := ℝ) (↑n : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℝ) _)
h : decide (1 < HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)) = true
⊢ 1 < HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ)

Tactic:
simpa using (Rat.cast_lt (K := ℝ)).2 (of_decide_eq_true h)

Premises used: Iff.mpr, of_decide_eq_true, Rat.cast_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
e : ℝ
d n : ℕ
inv : Invertible (α := ℝ) (↑d : ℝ)
eq : e = HMul.hMul (α := ℝ) (↑n : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℝ) _)
h : decide (1 < HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)) = true
⊢ 1 < HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ)

Tactic:
have : 1 < (n : ℝ) / d := by
      simpa using (Rat.cast_lt (K := ℝ)).2 (of_decide_eq_true h)
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
e : ℝ
d n : ℕ
inv : Invertible (α := ℝ) (↑d : ℝ)
eq : e = HMul.hMul (α := ℝ) (↑n : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℝ) _)
h : decide (1 < HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)) = true
this : 1 < HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ)
⊢ 0 < Real.log (HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ))

Tactic:
Real.log_pos this

Premises used: Real.log_pos