awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
rw :
  Eq (α := Set ℝ)
    (Set.range (ι := ℝ)
      (comp (β := (↑(Set.Ioi 0) : Type)) (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x))
        (⇑expOrderIso : (a : ℝ) → (↑(Set.Ioi 0) : Type))))
    (Set.Ioi 0)
rw₁ :
  Eq (α := Set ℝ)
    (Set.image (α := (↑(Set.Ioi 0) : Type)) (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x))
      (Set.range (ι := ℝ) (⇑expOrderIso : (a : ℝ) → (↑(Set.Ioi 0) : Type))))
    (Set.Ioi 0)
rw₂ :
  Eq (α := Set ℝ)
    (Set.image (α := (↑(Set.Ioi 0) : Type)) (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x))
      Set.univ)
    (Set.Ioi 0)
rw₃ :
  Eq (α := Set ℝ)
    (Set.range (ι := (↑(Set.Ioi 0) : Type))
      (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x)))
    (Set.Ioi 0)
rw₄ rw₅ : Eq (α := Set ℝ) (Set.Ioi 0) (Set.Ioi 0)
⊢ Set.range rexp = Set.Ioi 0

Tactic:
rw [← coe_comp_expOrderIso, range_comp, expOrderIso.range_eq, image_univ, Subtype.range_coe]

Premises used: Set.range_comp, Set.image_univ, OrderIso.range_eq, Subtype.range_coe, Real.coe_comp_expOrderIso, Real.expOrderIso
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
rw :
  Eq (α := Filter ℝ)
    (Filter.map (α := ℝ)
      (comp (β := (↑(Set.Ioi 0) : Type)) (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x))
        (⇑expOrderIso : (a : ℝ) → (↑(Set.Ioi 0) : Type)))
      atTop)
    atTop
rw₁ :
  Eq (α := Filter ℝ)
    (Filter.map (α := (↑(Set.Ioi 0) : Type))
      (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x))
      (Filter.map (α := ℝ) (⇑expOrderIso : (a : ℝ) → (↑(Set.Ioi 0) : Type)) atTop))
    atTop
rw₂ :
  Eq (α := Filter ℝ)
    (Filter.map (α := (↑(Set.Ioi 0) : Type))
      (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x)) atTop)
    atTop
rw₃ rw₄ : Eq (α := Filter ℝ) atTop atTop
⊢ Filter.map rexp atTop = atTop

Tactic:
rw [← coe_comp_expOrderIso, ← Filter.map_map, OrderIso.map_atTop, map_val_Ioi_atTop]

Premises used: Filter.map_map, Real.coe_comp_expOrderIso, Filter.map_val_Ioi_atTop, OrderIso.map_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
rw : comap rexp (Filter.map rexp atTop) = Filter.map rexp atTop
rw₁ : atTop = Filter.map rexp atTop
rw₂ rw₃ : Eq (α := Filter ℝ) atTop atTop
⊢ comap rexp atTop = atTop

Tactic:
rw [← map_exp_atTop, comap_map exp_injective, map_exp_atTop]

Premises used: Filter.comap_map, Real.exp_injective, Real.map_exp_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
α : Type u_1
l : Filter α
f : α → ℝ
simp_rw : Tendsto (β := ℝ) (fun (x : α) ↦ (rexp ∘ f) x) l atTop ↔ Tendsto f l atTop
simp_rw₁ : Tendsto f l (comap rexp atTop) ↔ Tendsto f l atTop
⊢ Tendsto (β := ℝ) (fun (x : α) ↦ rexp (f x)) l atTop ↔ Tendsto f l atTop

Tactic:
simp_rw [← comp_apply (f := exp), ← tendsto_comap_iff, comap_exp_atTop]

Premises used: Filter.tendsto_comap_iff, Real.comap_exp_atTop, Function.comp_apply
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
α : Type u_1
l : Filter α
f : ℝ → α
simp_rw : Tendsto (fun (x : ℝ) ↦ (f ∘ rexp) x) atTop l ↔ Tendsto f atTop l
simp_rw₁ : Tendsto f (Filter.map rexp atTop) l ↔ Tendsto f atTop l
⊢ Tendsto (fun (x : ℝ) ↦ f (rexp x)) atTop l ↔ Tendsto f atTop l

Tactic:
simp_rw [← comp_apply (g := exp), ← tendsto_map'_iff, map_exp_atTop]

Premises used: Filter.tendsto_map'_iff, Function.comp_apply, Real.map_exp_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
rw :
  Eq (α := Filter ℝ)
    (Filter.map (α := ℝ)
      (comp (β := (↑(Set.Ioi 0) : Type)) (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x))
        (⇑expOrderIso : (a : ℝ) → (↑(Set.Ioi 0) : Type)))
      atBot)
    (𝓝[>] 0)
rw₁ :
  Eq (α := Filter ℝ)
    (Filter.map (α := (↑(Set.Ioi 0) : Type))
      (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x))
      (Filter.map (α := ℝ) (⇑expOrderIso : (a : ℝ) → (↑(Set.Ioi 0) : Type)) atBot))
    (𝓝[>] 0)
rw₂ :
  Eq (α := Filter ℝ)
    (Filter.map (α := (↑(Set.Ioi 0) : Type))
      (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x)) atBot)
    (𝓝[>] 0)
rw₃ rw₄ :
  Eq (α := Filter ℝ)
    (Filter.map (α := (↑(Set.Ioi 0) : Type))
      (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x)) atBot)
    (Filter.map (α := { x : ℝ // Membership.mem (γ := Set ℝ) (Set.Ioi 0) x })
      (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x)) atBot)
⊢ Filter.map rexp atBot = 𝓝[>] 0

Tactic:
rw [← coe_comp_expOrderIso, ← Filter.map_map, expOrderIso.map_atBot, ← map_coe_Ioi_atBot]

Premises used: OrderIso.map_atBot, Filter.map_map, map_coe_Ioi_atBot, Real.coe_comp_expOrderIso, Real.expOrderIso
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
rw : comap rexp (Filter.map rexp atBot) = atBot
rw₁ rw₂ : Eq (α := Filter ℝ) atBot atBot
⊢ comap rexp (𝓝[>] 0) = atBot

Tactic:
rw [← map_exp_atBot, comap_map exp_injective]

Premises used: Filter.comap_map, Real.map_exp_atBot, Real.exp_injective
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
α : Type u_1
l : Filter α
f : ℝ → α
rw : Tendsto (fun (x : ℝ) ↦ f (rexp x)) atBot l ↔ Tendsto (f ∘ rexp) atBot l
⊢ Tendsto (fun (x : ℝ) ↦ f (rexp x)) atBot l ↔ Tendsto f (𝓝[>] 0) l

Tactic:
rw [← map_exp_atBot, tendsto_map'_iff]

Premises used: Filter.tendsto_map'_iff, Real.map_exp_atBot
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
α : Type u_1
l : Filter α
f : ℝ → α
⊢ Tendsto (fun (x : ℝ) ↦ f (rexp x)) atBot l ↔ Tendsto (f ∘ rexp) atBot l

Tactic:
rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
⊢ comap rexp (𝓝[Set.range rexp] 0) = atBot

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
α : Type u_1
l : Filter α
f : α → ℝ
simp_rw : Tendsto (β := ℝ) (fun (x : α) ↦ (rexp ∘ f) x) l (𝓝 0) ↔ Tendsto f l atBot
simp_rw₁ : Tendsto f l (comap rexp (𝓝 0)) ↔ Tendsto f l atBot
⊢ Tendsto (β := ℝ) (fun (x : α) ↦ rexp (f x)) l (𝓝 0) ↔ Tendsto f l atBot

Tactic:
simp_rw [← comp_apply (f := exp), ← tendsto_comap_iff, comap_exp_nhds_zero]

Premises used: Real.comap_exp_nhds_zero, Filter.tendsto_comap_iff, Function.comp_apply
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
⊢ IsOpenEmbedding rexp

Tactic:
isOpen_Ioi.isOpenEmbedding_subtypeVal.comp expOrderIso.toHomeomorph.isOpenEmbedding

Premises used: IsOpen.isOpenEmbedding_subtypeVal, Real.exp, OrderIso.toHomeomorph, isOpen_Ioi, Homeomorph.isOpenEmbedding, Real.expOrderIso, Topology.IsOpenEmbedding.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
x : ℝ
⊢ Filter.map rexp (𝓝 x) = 𝓝 (rexp x)

Tactic:
isOpenEmbedding_exp.map_nhds_eq x

Premises used: Topology.IsOpenEmbedding.map_nhds_eq, Real.isOpenEmbedding_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
x : ℝ
⊢ comap rexp (𝓝 (rexp x)) = 𝓝 x

Tactic:
(isOpenEmbedding_exp.nhds_eq_comap x).symm

Premises used: Topology.IsInducing.nhds_eq_comap, Topology.IsOpenEmbedding.toIsEmbedding, Real.isOpenEmbedding_exp, Topology.IsEmbedding.toIsInducing, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
n : ℕ
⊢ IsLittleO (E := ℝ) atTop (fun (x : ℝ) ↦ x ^ n) rexp

Tactic:
simpa [isLittleO_iff_tendsto fun x hx => ((exp_pos x).ne' hx).elim] using
    tendsto_div_pow_mul_exp_add_atTop 1 0 n zero_ne_one

Premises used: False.elim, zero_ne_one, LT.lt.ne', Real.tendsto_div_pow_mul_exp_add_atTop, Asymptotics.isLittleO_iff_tendsto, OfNat.ofNat, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
α : Type u_1
l : Filter α
f g : α → ℝ
⊢ (IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖rexp (f x)‖ / ‖rexp (g x)‖) ↔
    IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l (f - g)

Tactic:
simp only [norm_eq_abs, abs_exp, ← exp_sub, isBoundedUnder_le_exp_comp, Pi.sub_def]

Premises used: Real.isBoundedUnder_le_exp_comp, Pi.sub_def, Real.exp_sub, Real.norm_eq_abs, Real.abs_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
α : Type u_1
l : Filter α
f g : α → ℝ
⊢ (IsTheta (E := ℝ) (F := ℝ) l (fun (x : α) ↦ rexp (f x)) fun (x : α) ↦ rexp (g x)) ↔
    IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ |f x - g x|

Tactic:
simp only [isBoundedUnder_le_abs, ← isBoundedUnder_le_neg, neg_sub, IsTheta,
    isBigO_exp_comp_exp_comp, Pi.sub_def]

Premises used: neg_sub, Asymptotics.IsTheta, Pi.sub_def, Filter.isBoundedUnder_le_neg, Real.isBigO_exp_comp_exp_comp, Filter.isBoundedUnder_le_abs
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
α : Type u_1
l : Filter α
f g : α → ℝ
⊢ (IsLittleO (E := ℝ) (F := ℝ) l (fun (x : α) ↦ rexp (f x)) fun (x : α) ↦ rexp (g x)) ↔
    Tendsto (β := ℝ) (fun (x : α) ↦ g x - f x) l atTop

Tactic:
simp only [isLittleO_iff_tendsto, exp_ne_zero, ← exp_sub, ← tendsto_neg_atTop_iff, false_imp_iff,
    imp_true_iff, tendsto_exp_comp_nhds_zero, neg_sub]

Premises used: neg_sub, Real.tendsto_exp_comp_nhds_zero, imp_true_iff, false_imp_iff, Asymptotics.isLittleO_iff_tendsto, Real.exp_sub, Filter.tendsto_neg_atTop_iff, Real.exp_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
α : Type u_1
l : Filter α
f : α → ℝ
⊢ (IsLittleO (E := ℝ) (F := ℝ) l (fun (x : α) ↦ 1) fun (x : α) ↦ rexp (f x)) ↔ Tendsto f l atTop

Tactic:
simp only [← exp_zero, isLittleO_exp_comp_exp_comp, sub_zero]

Premises used: sub_zero, Real.isLittleO_exp_comp_exp_comp, Real.exp_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
α : Type u_1
l : Filter α
f : α → ℝ
⊢ (IsBigO (E := ℝ) (F := ℝ) l (fun (x : α) ↦ 1) fun (x : α) ↦ rexp (f x)) ↔
    IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) l f

Tactic:
simp only [← exp_zero, isBigO_exp_comp_exp_comp, Pi.sub_def, zero_sub, isBoundedUnder_le_neg]

Premises used: Pi.sub_def, Filter.isBoundedUnder_le_neg, Real.isBigO_exp_comp_exp_comp, Real.exp_zero, zero_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
α : Type u_1
l : Filter α
f : α → ℝ
⊢ (IsBigO (E := ℝ) (F := ℝ) l (fun (x : α) ↦ rexp (f x)) fun (x : α) ↦ 1) ↔
    IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l f

Tactic:
simp only [isBigO_one_iff, norm_eq_abs, abs_exp, isBoundedUnder_le_exp_comp]

Premises used: Real.isBoundedUnder_le_exp_comp, Asymptotics.isBigO_one_iff, Real.norm_eq_abs, Real.abs_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
α : Type u_1
l : Filter α
f : α → ℝ
⊢ (IsTheta (E := ℝ) (F := ℝ) l (fun (x : α) ↦ rexp (f x)) fun (x : α) ↦ 1) ↔
    IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ |f x|

Tactic:
simp only [← exp_zero, isTheta_exp_comp_exp_comp, sub_zero]

Premises used: sub_zero, Real.isTheta_exp_comp_exp_comp, Real.exp_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
a : ℝ
⊢ (Summable (α := ℝ) fun (n : ℕ) ↦ rexp ((↑n : ℝ) * a)) ↔ a < 0

Tactic:
simp only [exp_nat_mul, summable_geometric_iff_norm_lt_one, norm_of_nonneg (exp_nonneg _),
    exp_lt_one_iff]

Premises used: Real.exp_lt_one_iff, summable_geometric_iff_norm_lt_one, Real.exp_nonneg, Real.exp_nat_mul, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ rexp (-(↑n : ℝ))

Tactic:
simpa only [mul_neg_one] using summable_exp_nat_mul_iff.mpr neg_one_lt_zero

Premises used: Iff.mpr, neg_one_lt_zero, mul_neg_one, Real.summable_exp_nat_mul_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
c : ℝ
hc : c < 0
f : ℕ → ℝ
hf : ∀ (i : ℕ), (↑i : ℝ) ≤ f i
x : ℕ
⊢ 0 ≤ rexp (c * f x)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
c : ℝ
hc : c < 0
f : ℕ → ℝ
hf : ∀ (i : ℕ), (↑i : ℝ) ≤ f i
refine : ∀ (i : ℕ), rexp (c * f i) ≤ rexp ((↑i : ℝ) * c)
⊢ Summable (α := ℝ) fun (i : ℕ) ↦ rexp (c * f i)

Tactic:
refine (Real.summable_exp_nat_mul_iff.mpr hc).of_nonneg_of_le (fun _ ↦ by positivity) fun i ↦ ?_

Premises used: Iff.mpr, Summable.of_nonneg_of_le, Real.summable_exp_nat_mul_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
c : ℝ
hc : c < 0
f : ℕ → ℝ
hf : ∀ (i : ℕ), (↑i : ℝ) ≤ f i
i : ℕ
⊢ rexp (c * f i) ≤ rexp ((↑i : ℝ) * c)

Tactic:
Real.exp_monotone ?_

Premises used: Real.exp_monotone
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
c : ℝ
hc : c < 0
f : ℕ → ℝ
hf : ∀ (i : ℕ), (↑i : ℝ) ≤ f i
i : ℕ
refine : c * f i ≤ (↑i : ℝ) * c
⊢ rexp (c * f i) ≤ rexp ((↑i : ℝ) * c)

Tactic:
refine Real.exp_monotone ?_

Premises used: Real.exp_monotone
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
c : ℝ
hc : c < 0
f : ℕ → ℝ
hf : ∀ (i : ℕ), (↑i : ℝ) ≤ f i
i : ℕ
rw : c * (↑i : ℝ)
| (↑i : ℝ) * c

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
c : ℝ
hc : c < 0
f : ℕ → ℝ
hf : ∀ (i : ℕ), (↑i : ℝ) ≤ f i
i : ℕ
conv_rhs : c * f i ≤ c * (↑i : ℝ)
⊢ c * f i ≤ (↑i : ℝ) * c

Tactic:
conv_rhs => rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
c : ℝ
hc : c < 0
f : ℕ → ℝ
hf : ∀ (i : ℕ), (↑i : ℝ) ≤ f i
i : ℕ
⊢ c * f i ≤ c * (↑i : ℝ)

Tactic:
mul_le_mul_of_nonpos_left (hf i) hc.le

Premises used: mul_le_mul_of_nonpos_left, LT.lt.le
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
c : ℝ
hc : c < 0
f : ℕ → ℝ
hf : ∀ (i : ℕ), (↑i : ℝ) ≤ f i
i : ℕ
⊢ c * f i ≤ c * (↑i : ℝ)

Tactic:
exact mul_le_mul_of_nonpos_left (hf i) hc.le

Premises used: mul_le_mul_of_nonpos_left, LT.lt.le
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
k : ℕ
r : ℝ
hr : 0 < r
simp_rw : Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k * rexp (-r) ^ n
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k * rexp (-r * (↑n : ℝ))

Tactic:
simp_rw [mul_comm (-r), exp_nat_mul]

Premises used: mul_comm, Real.exp_nat_mul, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
k : ℕ
r : ℝ
hr : 0 < r
hr₁ : ‖rexp (-r)‖ < 1
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k * rexp (-r) ^ n

Tactic:
apply summable_pow_mul_geometric_of_norm_lt_one

Premises used: summable_pow_mul_geometric_of_norm_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
k : ℕ
r : ℝ
hr : 0 < r
hr₁ : rexp (-r) < 1
hr₂ : -r < 0
hr₃ hr₄ hr₅ hr₆ : 0 < r
⊢ ‖rexp (-r)‖ < 1

Tactic:
rwa [norm_of_nonneg (exp_nonneg _), exp_lt_one_iff, neg_lt_zero]

Premises used: neg_lt_zero, Real.exp_lt_one_iff, Real.exp_nonneg, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
ι : Type u_1
f : ι → ℝ
a : ℝ
h : HasSum f a
⊢ HasProd (rexp ∘ f) (rexp a)

Tactic:
Tendsto.congr (fun s ↦ exp_sum s f) <| Tendsto.rexp h

Premises used: HasProd, Filter.Tendsto.rexp, Filter.Tendsto.congr, Real.exp_sum
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
⊢ comap cexp (cobounded ℂ) = comap re (comap Real.exp atTop)

Tactic:
simp only [← comap_norm_atTop, comap_comap, comp_def, norm_exp]

Premises used: comap_norm_atTop, Function.comp_def, Filter.comap_comap, Complex.norm_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
rw rw₁ : comap re atTop = comap re atTop
⊢ comap re (comap Real.exp atTop) = comap re atTop

Tactic:
rw [Real.comap_exp_atTop]

Premises used: Real.comap_exp_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
rw : comap (β := ℝ) (fun (x : ℂ) ↦ ‖cexp x‖) (𝓝 0) = comap re (comap Real.exp (𝓝 0))
⊢ comap cexp (𝓝 0) = comap re (comap Real.exp (𝓝 0))

Tactic:
rw [← comap_norm_nhds_zero, comap_comap, Function.comp_def]

Premises used: comap_norm_nhds_zero, Function.comp_def, Filter.comap_comap
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
simp_rw : comap (β := ℝ) (fun (x : ℂ) ↦ Real.exp x.re) (𝓝 0) = comap re (comap Real.exp (𝓝 0))
simp_rw₁ : comap (β := ℝ) (fun (x : ℂ) ↦ Real.exp x.re) (𝓝 0) = comap (Real.exp ∘ re) (𝓝 0)
⊢ comap (β := ℝ) (fun (x : ℂ) ↦ ‖cexp x‖) (𝓝 0) = comap re (comap Real.exp (𝓝 0))

Tactic:
simp_rw [norm_exp, comap_comap, Function.comp_def]

Premises used: Function.comp_def, Filter.comap_comap, Complex.norm_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
rw rw₁ : comap re atBot = comap re atBot
⊢ comap re (comap Real.exp (𝓝 0)) = comap re atBot

Tactic:
rw [Real.comap_exp_nhds_zero]

Premises used: Real.comap_exp_nhds_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
⊢ (cexp ⁻¹' {0})ᶜ = Set.univ

Tactic:
have : (exp ⁻¹' {0})ᶜ = Set.univ := eq_univ_of_forall exp_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
this : (cexp ⁻¹' {0})ᶜ = Set.univ
⊢ comap cexp (𝓝[≠] 0) = comap re atBot

Tactic:
simp [nhdsWithin, comap_exp_nhds_zero, this]

Premises used: nhdsWithin, Complex.comap_exp_nhds_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
α : Type u_1
l : Filter α
f : α → ℂ
simp_rw : Tendsto (re ∘ f) l atBot ↔ Tendsto (β := ℝ) (fun (x : α) ↦ (f x).re) l atBot
⊢ Tendsto (β := ℂ) (fun (x : α) ↦ cexp (f x)) l (𝓝 0) ↔ Tendsto (β := ℝ) (fun (x : α) ↦ (f x).re) l atBot

Tactic:
simp_rw [← comp_apply (f := exp), ← tendsto_comap_iff, comap_exp_nhds_zero, tendsto_comap_iff]

Premises used: Complex.comap_exp_nhds_zero, Filter.tendsto_comap_iff, Function.comp_apply
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
α : Type u_1
l : Filter α
f : α → ℂ
⊢ Tendsto (re ∘ f) l atBot ↔ Tendsto (β := ℝ) (fun (x : α) ↦ (f x).re) l atBot

Tactic:
rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
⊢ Tendsto cexp (comap re atTop) (cobounded ℂ)

Tactic:
comap_exp_cobounded ▸ tendsto_comap

Premises used: Complex.comap_exp_cobounded, Eq.rec, Filter.tendsto_comap
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
⊢ Tendsto cexp (comap re atBot) (𝓝 0)

Tactic:
comap_exp_nhds_zero ▸ tendsto_comap

Premises used: Complex.comap_exp_nhds_zero, Eq.rec, Filter.tendsto_comap
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
⊢ Tendsto cexp (comap re atBot) (𝓝[≠] 0)

Tactic:
comap_exp_nhdsNE ▸ tendsto_comap

Premises used: Eq.rec, Complex.comap_exp_nhdsNE, Filter.tendsto_comap
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
ι : Type u_1
f : ι → ℂ
a : ℂ
h : HasSum f a
⊢ HasProd (cexp ∘ f) (cexp a)

Tactic:
Filter.Tendsto.congr (fun s ↦ exp_sum s f) <| Filter.Tendsto.cexp h

Premises used: HasProd, Filter.Tendsto.cexp, Filter.Tendsto.congr, Complex.exp_sum
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
rw : AnalyticOnNhd ℂ (E := ℂ) NormedSpace.exp univ
⊢ AnalyticOnNhd ℂ cexp univ

Tactic:
rw [Complex.exp_eq_exp_ℂ]

Premises used: Complex.exp_eq_exp_ℂ
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
⊢ AnalyticOnNhd ℂ (E := ℂ) NormedSpace.exp univ

Tactic:
fun x _ ↦ NormedSpace.exp_analytic x

Premises used: AnalyticOnNhd, NormedSpace.exp_analytic
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
⊢ AnalyticOnNhd ℂ (E := ℂ) NormedSpace.exp univ

Tactic:
exact fun x _ ↦ NormedSpace.exp_analytic x

Premises used: NormedSpace.exp_analytic
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
⊢ AnalyticOn ℂ cexp univ

Tactic:
analyticOnNhd_cexp.analyticOn

Premises used: analyticOnNhd_cexp, AnalyticOnNhd.analyticOn
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
z : ℂ
⊢ AnalyticAt ℂ cexp z

Tactic:
analyticOnNhd_cexp z (mem_univ _)

Premises used: analyticOnNhd_cexp, Set.mem_univ
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
s : Set ℂ
x : ℂ
⊢ AnalyticWithinAt ℂ cexp s x

Tactic:
analyticAt_cexp.analyticWithinAt

Premises used: AnalyticAt.analyticWithinAt, analyticAt_cexp
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
s : Set ℂ
x : ℂ
⊢ AnalyticWithinAt ℂ cexp s x

Tactic:
exact analyticAt_cexp.analyticWithinAt

Premises used: AnalyticAt.analyticWithinAt, analyticAt_cexp
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
x : E
fa : AnalyticAt ℂ f x
⊢ AnalyticAt ℂ (cexp ∘ f) x

Tactic:
analyticAt_cexp.comp fa

Premises used: AnalyticAt.comp, analyticAt_cexp
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
x : E
fa : AnalyticAt ℂ f x
⊢ AnalyticAt ℂ (F := ℂ) (fun (z : E) ↦ cexp (f z)) x

Tactic:
fa.cexp

Premises used: AnalyticAt.cexp
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
x : E
s : Set E
fa : AnalyticWithinAt ℂ f s x
⊢ AnalyticWithinAt ℂ (F := ℂ) (fun (z : E) ↦ cexp (f z)) s x

Tactic:
analyticAt_cexp.comp_analyticWithinAt fa

Premises used: AnalyticAt.comp_analyticWithinAt, analyticAt_cexp
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
s : Set E
fs : AnalyticOnNhd ℂ f s
⊢ AnalyticOnNhd ℂ (F := ℂ) (fun (z : E) ↦ cexp (f z)) s

Tactic:
fun z n ↦ analyticAt_cexp.comp (fs z n)

Premises used: AnalyticOnNhd, AnalyticAt.comp, analyticAt_cexp
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
s : Set E
fs : AnalyticOn ℂ f s
⊢ AnalyticOn ℂ (F := ℂ) (fun (z : E) ↦ cexp (f z)) s

Tactic:
analyticOnNhd_cexp.comp_analyticOn fs (mapsTo_univ _ _)

Premises used: Set.mapsTo_univ, analyticOnNhd_cexp, AnalyticOnNhd.comp_analyticOn
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
x : ℂ
rw : IsLittleO (E := ℂ) (F := ℂ) (𝓝 0) (fun (h : ℂ) ↦ cexp (x + h) - cexp x - h • cexp x) fun (h : ℂ) ↦ h
⊢ HasDerivAt cexp (cexp x) x

Tactic:
rw [hasDerivAt_iff_isLittleO_nhds_zero]

Premises used: hasDerivAt_iff_isLittleO_nhds_zero
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
x : ℂ
⊢ LT.lt (α := ℕ) 1 2

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
x : ℂ
⊢ LT.lt (α := ℕ) 1 2

Tactic:
have : (1 : ℕ) < 2 := by simp
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
x : ℂ
this : LT.lt (α := ℕ) 1 2
⊢ IsLittleO (E := ℂ) (F := ℂ) (𝓝 0) (fun (h : ℂ) ↦ cexp (x + h) - cexp x - h • cexp x) fun (h : ℂ) ↦ h

Tactic:
(IsBigO.of_bound ‖exp x‖ ?_).trans_isLittleO (isLittleO_pow_id this)

Premises used: Norm.norm, Asymptotics.isLittleO_pow_id, Complex.exp, Asymptotics.IsBigO.trans_isLittleO, Asymptotics.IsBigO.of_bound
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
x : ℂ
this : LT.lt (α := ℕ) 1 2
refine : ∀ᶠ (x_1 : ℂ) in 𝓝 0, ‖cexp (x + x_1) - cexp x - x_1 • cexp x‖ ≤ ‖cexp x‖ * ‖HPow.hPow (β := ℕ) x_1 2‖
⊢ IsLittleO (E := ℂ) (F := ℂ) (𝓝 0) (fun (h : ℂ) ↦ cexp (x + h) - cexp x - h • cexp x) fun (h : ℂ) ↦ h

Tactic:
refine (IsBigO.of_bound ‖exp x‖ ?_).trans_isLittleO (isLittleO_pow_id this)

Premises used: Norm.norm, Complex.exp, Asymptotics.IsBigO.trans_isLittleO, Asymptotics.IsBigO.of_bound
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
x : ℂ
this : LT.lt (α := ℕ) 1 2
h :
  ∀ (a : ℂ),
    Membership.mem (γ := Set ℂ) (Metric.ball 0 1) a →
      ‖cexp (x + a) - cexp x - a • cexp x‖ ≤ ‖cexp x‖ * ‖HPow.hPow (β := ℕ) a 2‖
⊢ ∀ᶠ (x_1 : ℂ) in 𝓝 0, ‖cexp (x + x_1) - cexp x - x_1 • cexp x‖ ≤ ‖cexp x‖ * ‖HPow.hPow (β := ℕ) x_1 2‖

Tactic:
filter_upwards [Metric.ball_mem_nhds (0 : ℂ) zero_lt_one]

Premises used: Metric.ball_mem_nhds, zero_lt_one, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
x : ℂ
this : LT.lt (α := ℕ) 1 2
h : ∀ (a : ℂ), ‖a‖ < 1 → ‖cexp (x + a) - cexp x - a • cexp x‖ ≤ ‖cexp x‖ * HPow.hPow (β := ℕ) ‖a‖ 2
⊢ ∀ (a : ℂ),
    Membership.mem (γ := Set ℂ) (Metric.ball 0 1) a →
      ‖cexp (x + a) - cexp x - a • cexp x‖ ≤ ‖cexp x‖ * ‖HPow.hPow (β := ℕ) a 2‖

Tactic:
simp only [Metric.mem_ball, dist_zero_right, norm_pow]

Premises used: norm_pow, Metric.mem_ball, dist_zero_right
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
x : ℂ
this : LT.lt (α := ℕ) 1 2
⊢ ∀ (a : ℂ), ‖a‖ < 1 → ‖cexp (x + a) - cexp x - a • cexp x‖ ≤ ‖cexp x‖ * HPow.hPow (β := ℕ) ‖a‖ 2

Tactic:
fun z hz => exp_bound_sq x z hz.le

Premises used: LT.lt.le, Complex.exp_bound_sq
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
x : ℂ
this : LT.lt (α := ℕ) 1 2
⊢ ∀ (a : ℂ), ‖a‖ < 1 → ‖cexp (x + a) - cexp x - a • cexp x‖ ≤ ‖cexp x‖ * HPow.hPow (β := ℕ) ‖a‖ 2

Tactic:
exact fun z hz => exp_bound_sq x z hz.le

Premises used: Complex.exp_bound_sq
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAlgebra 𝕜 ℂ
⊢ Differentiable 𝕜 cexp

Tactic:
fun x =>
  (hasDerivAt_exp x).differentiableAt.restrictScalars 𝕜

Premises used: Differentiable, HasDerivAt.differentiableAt, DifferentiableAt.restrictScalars, Complex.hasDerivAt_exp