a b c : ℝ
hb : 0 ≠ b
⊢ (exp ∘ fun x => a * (x / (b * exp x + c))) ∘ log =ᶠ[atTop] fun x => x ^ (a / (b * x + c))
a b c : ℝ
hb : 0 ≠ b
⊢ Tendsto (fun x => x ^ (a / (b * x + c))) atTop (𝓝 1)
refine'
  Tendsto.congr' _
    ((tendsto_exp_nhds_0_nhds_1.comp
          (by
            simpa only [MulZeroClass.mul_zero, pow_one] using
              (@tendsto_const_nhds _ _ _ a _).mul
                (tendsto_div_pow_mul_exp_add_atTop b c 1 hb))).comp
      tendsto_log_atTop)
a b c : ℝ
hb : 0 ≠ b
⊢ EqOn ((exp ∘ fun x => a * (x / (b * exp x + c))) ∘ log) (fun x => x ^ (a / (b * x + c))) (Set.Ioi 0)
a b c : ℝ
hb : 0 ≠ b
⊢ (exp ∘ fun x => a * (x / (b * exp x + c))) ∘ log =ᶠ[atTop] fun x => x ^ (a / (b * x + c))
apply eventuallyEq_of_mem (Ioi_mem_atTop (0 : ℝ))
a b c : ℝ
hb : 0 ≠ b
x : ℝ
hx : x ∈ Set.Ioi 0
⊢ ((exp ∘ fun x => a * (x / (b * exp x + c))) ∘ log) x = (fun x => x ^ (a / (b * x + c))) x
a b c : ℝ
hb : 0 ≠ b
⊢ EqOn ((exp ∘ fun x => a * (x / (b * exp x + c))) ∘ log) (fun x => x ^ (a / (b * x + c))) (Set.Ioi 0)
intro x hx
a b c : ℝ
hb : 0 ≠ b
x : ℝ
hx : 0 < x
⊢ exp (a * (log x / (b * exp (log x) + c))) = x ^ (a / (b * x + c))
a b c : ℝ
hb : 0 ≠ b
x : ℝ
hx : x ∈ Set.Ioi 0
⊢ ((exp ∘ fun x => a * (x / (b * exp x + c))) ∘ log) x = (fun x => x ^ (a / (b * x + c))) x
simp only [Set.mem_Ioi, Function.comp_apply] at hx⊢
a b c : ℝ
hb : 0 ≠ b
x : ℝ
hx : 0 < x
⊢ exp (a * (log x / (b * x + c))) = exp (a / (b * x + c) * log x)
a b c : ℝ
hb : 0 ≠ b
x : ℝ
hx : 0 < x
⊢ exp (a * (log x / (b * exp (log x) + c))) = x ^ (a / (b * x + c))
rw [exp_log hx, ← exp_log (rpow_pos_of_pos hx (a / (b * x + c))), log_rpow hx (a / (b * x + c))]
no goals
a b c : ℝ
hb : 0 ≠ b
x : ℝ
hx : 0 < x
⊢ exp (a * (log x / (b * x + c))) = exp (a / (b * x + c) * log x)
field_simp
no goals
a b c : ℝ
hb : 0 ≠ b
⊢ Tendsto ?m.9221 atTop (𝓝 0)
simpa only [MulZeroClass.mul_zero, pow_one] using
  (@tendsto_const_nhds _ _ _ a _).mul
    (tendsto_div_pow_mul_exp_add_atTop b c 1 hb)