awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
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)
⊢ Set.range rexp = Set.Ioi 0
have rw₃ : Eq (α := Set ℝ)
  (Set.range (ι := (↑(Set.Ioi 0) : Type)) (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x)))
  (Set.Ioi 0)
Tactic: rw [← coe_comp_expOrderIso, range_comp, expOrderIso.range_eq, image_univ, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
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)
⊢ Set.range rexp = Set.Ioi 0
have rw₄ : Eq (α := Set ℝ) (Set.Ioi 0) (Set.Ioi 0)
Tactic: rw [← coe_comp_expOrderIso, range_comp, expOrderIso.range_eq, image_univ, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
⊢ Filter.map rexp atTop = atTop
have 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
Tactic: rw [← coe_comp_expOrderIso, ← Filter.map_map, OrderIso.map_atTop, map_val_Ioi_atTop]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
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
⊢ Filter.map rexp atTop = atTop
have 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
Tactic: rw [← coe_comp_expOrderIso, ← Filter.map_map, OrderIso.map_atTop, map_val_Ioi_atTop]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
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
⊢ Filter.map rexp atTop = atTop
have rw₂ : Eq (α := Filter ℝ)
  (Filter.map (α := (↑(Set.Ioi 0) : Type)) (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x))
    atTop)
  atTop
Tactic: rw [← coe_comp_expOrderIso, ← Filter.map_map, OrderIso.map_atTop, map_val_Ioi_atTop]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
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
⊢ Filter.map rexp atTop = atTop
have rw₃ : Eq (α := Filter ℝ) atTop atTop
Tactic: rw [← coe_comp_expOrderIso, ← Filter.map_map, OrderIso.map_atTop, map_val_Ioi_atTop]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
⊢ comap rexp atTop = atTop
have rw : comap rexp (Filter.map rexp atTop) = Filter.map rexp atTop
Tactic: rw [← map_exp_atTop, comap_map exp_injective, map_exp_atTop]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
rw : comap rexp (Filter.map rexp atTop) = Filter.map rexp atTop
⊢ comap rexp atTop = atTop
have rw₁ : atTop = Filter.map rexp atTop
Tactic: rw [← map_exp_atTop, comap_map exp_injective, map_exp_atTop]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
rw : comap rexp (Filter.map rexp atTop) = Filter.map rexp atTop
rw₁ : atTop = Filter.map rexp atTop
⊢ comap rexp atTop = atTop
have rw₂ : Eq (α := Filter ℝ) atTop atTop
Tactic: rw [← map_exp_atTop, comap_map exp_injective, map_exp_atTop]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
α : Type u_1
l : Filter α
f : α → ℝ
⊢ Tendsto (β := ℝ) (fun (x : α) ↦ rexp (f x)) l atTop ↔ Tendsto f l atTop
have simp_rw : 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
α : Type u_1
l : Filter α
f : α → ℝ
simp_rw : Tendsto (β := ℝ) (fun (x : α) ↦ (rexp ∘ f) x) l atTop ↔ Tendsto f l atTop
⊢ Tendsto (β := ℝ) (fun (x : α) ↦ rexp (f x)) l atTop ↔ Tendsto f l atTop
have simp_rw₁ : Tendsto f l (comap rexp atTop) ↔ Tendsto f l atTop
Tactic: simp_rw [← comp_apply (f := exp), ← tendsto_comap_iff, comap_exp_atTop]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
α : Type u_1
l : Filter α
f : ℝ → α
⊢ Tendsto (fun (x : ℝ) ↦ f (rexp x)) atTop l ↔ Tendsto f atTop l
have simp_rw : 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
α : Type u_1
l : Filter α
f : ℝ → α
simp_rw : Tendsto (fun (x : ℝ) ↦ (f ∘ rexp) x) atTop l ↔ Tendsto f atTop l
⊢ Tendsto (fun (x : ℝ) ↦ f (rexp x)) atTop l ↔ Tendsto f atTop l
have simp_rw₁ : Tendsto f (Filter.map rexp atTop) l ↔ Tendsto f atTop l
Tactic: simp_rw [← comp_apply (g := exp), ← tendsto_map'_iff, map_exp_atTop]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
⊢ Filter.map rexp atBot = 𝓝[>] 0
have 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)
Tactic: rw [← coe_comp_expOrderIso, ← Filter.map_map, expOrderIso.map_atBot, ← map_coe_Ioi_atBot]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
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)
⊢ Filter.map rexp atBot = 𝓝[>] 0
have 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)
Tactic: rw [← coe_comp_expOrderIso, ← Filter.map_map, expOrderIso.map_atBot, ← map_coe_Ioi_atBot]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
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)
⊢ Filter.map rexp atBot = 𝓝[>] 0
have rw₂ : Eq (α := Filter ℝ)
  (Filter.map (α := (↑(Set.Ioi 0) : Type)) (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x))
    atBot)
  (𝓝[>] 0)
Tactic: rw [← coe_comp_expOrderIso, ← Filter.map_map, expOrderIso.map_atBot, ← map_coe_Ioi_atBot]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
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)
⊢ Filter.map rexp atBot = 𝓝[>] 0
have 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)
Tactic: rw [← coe_comp_expOrderIso, ← Filter.map_map, expOrderIso.map_atBot, ← map_coe_Ioi_atBot]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
⊢ comap rexp (𝓝[>] 0) = atBot
have rw : comap rexp (Filter.map rexp atBot) = atBot
Tactic: rw [← map_exp_atBot, comap_map exp_injective]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
rw : comap rexp (Filter.map rexp atBot) = atBot
⊢ comap rexp (𝓝[>] 0) = atBot
have rw₁ : Eq (α := Filter ℝ) atBot atBot
Tactic: rw [← map_exp_atBot, comap_map exp_injective]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
α : Type u_1
l : Filter α
f : ℝ → α
⊢ Tendsto (fun (x : ℝ) ↦ f (rexp x)) atBot l ↔ Tendsto f (𝓝[>] 0) l
have rw : Tendsto (fun (x : ℝ) ↦ f (rexp x)) atBot l ↔ Tendsto (f ∘ rexp) atBot l
Tactic: rw [← map_exp_atBot, tendsto_map'_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
α : Type u_1
l : Filter α
f : α → ℝ
⊢ Tendsto (β := ℝ) (fun (x : α) ↦ rexp (f x)) l (𝓝 0) ↔ Tendsto f l atBot
have simp_rw : 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
α : Type u_1
l : Filter α
f : α → ℝ
simp_rw : Tendsto (β := ℝ) (fun (x : α) ↦ (rexp ∘ f) x) l (𝓝 0) ↔ Tendsto f l atBot
⊢ Tendsto (β := ℝ) (fun (x : α) ↦ rexp (f x)) l (𝓝 0) ↔ Tendsto f l atBot
have simp_rw₁ : Tendsto f l (comap rexp (𝓝 0)) ↔ Tendsto f l atBot
Tactic: simp_rw [← comp_apply (f := exp), ← tendsto_comap_iff, comap_exp_nhds_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
c : ℝ
hc : c < 0
f : ℕ → ℝ
hf : ∀ (i : ℕ), (↑i : ℝ) ≤ f i
⊢ Summable (α := ℝ) fun (i : ℕ) ↦ rexp (c * f i)
have refine : ∀ (i : ℕ), rexp (c * f i) ≤ rexp ((↑i : ℝ) * c)
Tactic: refine (Real.summable_exp_nat_mul_iff.mpr hc).of_nonneg_of_le (fun _ ↦ by positivity) fun i ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
c : ℝ
hc : c < 0
f : ℕ → ℝ
hf : ∀ (i : ℕ), (↑i : ℝ) ≤ f i
i : ℕ
⊢ rexp (c * f i) ≤ rexp ((↑i : ℝ) * c)
have refine : c * f i ≤ (↑i : ℝ) * c
Tactic: refine Real.exp_monotone ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
c : ℝ
hc : c < 0
f : ℕ → ℝ
hf : ∀ (i : ℕ), (↑i : ℝ) ≤ f i
i : ℕ
| (↑i : ℝ) * c
have rw : c * (↑i : ℝ)
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
c : ℝ
hc : c < 0
f : ℕ → ℝ
hf : ∀ (i : ℕ), (↑i : ℝ) ≤ f i
i : ℕ
⊢ c * f i ≤ (↑i : ℝ) * c
have conv_rhs : c * f i ≤ c * (↑i : ℝ)
Tactic: conv_rhs => rw [mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
k : ℕ
r : ℝ
hr : 0 < r
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k * rexp (-r * (↑n : ℝ))
have simp_rw : Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k * rexp (-r) ^ n
Tactic: simp_rw [mul_comm (-r), exp_nat_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
k : ℕ
r : ℝ
hr : 0 < r
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k * rexp (-r) ^ n
have hr₁ : ‖rexp (-r)‖ < 1
Tactic: apply summable_pow_mul_geometric_of_norm_lt_one
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
k : ℕ
r : ℝ
hr : 0 < r
⊢ ‖rexp (-r)‖ < 1
have hr₁ : rexp (-r) < 1
Tactic: rwa [norm_of_nonneg (exp_nonneg _), exp_lt_one_iff, neg_lt_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
k : ℕ
r : ℝ
hr : 0 < r
hr₁ : rexp (-r) < 1
⊢ ‖rexp (-r)‖ < 1
have hr₂ : -r < 0
Tactic: rwa [norm_of_nonneg (exp_nonneg _), exp_lt_one_iff, neg_lt_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
⊢ comap re (comap Real.exp atTop) = comap re atTop
have rw : comap re atTop = comap re atTop
Tactic: rw [Real.comap_exp_atTop]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
⊢ comap cexp (𝓝 0) = comap re (comap Real.exp (𝓝 0))
have rw : comap (β := ℝ) (fun (x : ℂ) ↦ ‖cexp x‖) (𝓝 0) = comap re (comap Real.exp (𝓝 0))
Tactic: rw [← comap_norm_nhds_zero, comap_comap, Function.comp_def]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
⊢ comap (β := ℝ) (fun (x : ℂ) ↦ ‖cexp x‖) (𝓝 0) = comap re (comap Real.exp (𝓝 0))
have simp_rw : comap (β := ℝ) (fun (x : ℂ) ↦ Real.exp x.re) (𝓝 0) = comap re (comap Real.exp (𝓝 0))
Tactic: simp_rw [norm_exp, comap_comap, Function.comp_def]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
simp_rw : comap (β := ℝ) (fun (x : ℂ) ↦ Real.exp x.re) (𝓝 0) = comap re (comap Real.exp (𝓝 0))
⊢ comap (β := ℝ) (fun (x : ℂ) ↦ ‖cexp x‖) (𝓝 0) = comap re (comap Real.exp (𝓝 0))
have simp_rw₁ : comap (β := ℝ) (fun (x : ℂ) ↦ Real.exp x.re) (𝓝 0) = comap (Real.exp ∘ re) (𝓝 0)
Tactic: simp_rw [norm_exp, comap_comap, Function.comp_def]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
⊢ comap re (comap Real.exp (𝓝 0)) = comap re atBot
have rw : comap re atBot = comap re atBot
Tactic: rw [Real.comap_exp_nhds_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (hypothesis)
Goal:
⊢ comap cexp (𝓝[≠] 0) = comap re atBot
have this : (cexp ⁻¹' {0})ᶜ = Set.univ
Tactic: have : (exp ⁻¹' {0})ᶜ = Set.univ := eq_univ_of_forall exp_ne_zero
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
α : Type u_1
l : Filter α
f : α → ℂ
⊢ Tendsto (β := ℂ) (fun (x : α) ↦ cexp (f x)) l (𝓝 0) ↔ Tendsto (β := ℝ) (fun (x : α) ↦ (f x).re) l atBot
have simp_rw : Tendsto (re ∘ f) l atBot ↔ 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ExpDeriv (goal)
Goal:
⊢ AnalyticOnNhd ℂ cexp univ
have rw : AnalyticOnNhd ℂ (E := ℂ) NormedSpace.exp univ
Tactic: rw [Complex.exp_eq_exp_ℂ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ExpDeriv (goal)
Goal:
x : ℂ
⊢ HasDerivAt cexp (cexp x) x
have rw : IsLittleO (E := ℂ) (F := ℂ) (𝓝 0) (fun (h : ℂ) ↦ cexp (x + h) - cexp x - h • cexp x) fun (h : ℂ) ↦ h
Tactic: rw [hasDerivAt_iff_isLittleO_nhds_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ExpDeriv (hypothesis)
Goal:
x : ℂ
⊢ IsLittleO (E := ℂ) (F := ℂ) (𝓝 0) (fun (h : ℂ) ↦ cexp (x + h) - cexp x - h • cexp x) fun (h : ℂ) ↦ h
have this : LT.lt (α := ℕ) 1 2
Tactic: have : (1 : ℕ) < 2 := by simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ExpDeriv (goal)
Goal:
x : ℂ
this : LT.lt (α := ℕ) 1 2
⊢ IsLittleO (E := ℂ) (F := ℂ) (𝓝 0) (fun (h : ℂ) ↦ cexp (x + h) - cexp x - h • cexp x) fun (h : ℂ) ↦ h
have refine : ∀ᶠ (x_1 : ℂ) in 𝓝 0, ‖cexp (x + x_1) - cexp x - x_1 • cexp x‖ ≤ ‖cexp x‖ * ‖HPow.hPow (β := ℕ) x_1 2‖
Tactic: refine (IsBigO.of_bound ‖exp x‖ ?_).trans_isLittleO (isLittleO_pow_id this)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ExpDeriv (goal)
Goal:
x : ℂ
this : LT.lt (α := ℕ) 1 2
⊢ ∀ᶠ (x_1 : ℂ) in 𝓝 0, ‖cexp (x + x_1) - cexp x - x_1 • cexp x‖ ≤ ‖cexp x‖ * ‖HPow.hPow (β := ℕ) x_1 2‖
have h : ∀ (a : ℂ),
  Membership.mem (γ := Set ℂ) (Metric.ball 0 1) a →
    ‖cexp (x + a) - cexp x - a • cexp x‖ ≤ ‖cexp x‖ * ‖HPow.hPow (β := ℕ) a 2‖
Tactic: filter_upwards [Metric.ball_mem_nhds (0 : ℂ) zero_lt_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ExpDeriv (goal)
Goal:
x : ℂ
this : LT.lt (α := ℕ) 1 2
⊢ ∀ (a : ℂ),
    Membership.mem (γ := Set ℂ) (Metric.ball 0 1) a →
      ‖cexp (x + a) - cexp x - a • cexp x‖ ≤ ‖cexp x‖ * ‖HPow.hPow (β := ℕ) a 2‖
have h : ∀ (a : ℂ), ‖a‖ < 1 → ‖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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ExpDeriv (goal)
Goal:
n : ℕ
⊢ deriv^[n + 1] cexp = cexp
have rw : deriv^[n] (deriv cexp) = cexp
Tactic: rw [iterate_succ_apply, deriv_exp, iter_deriv_exp n]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ExpDeriv (goal)
Goal:
n : ℕ
rw : deriv^[n] (deriv cexp) = cexp
⊢ deriv^[n + 1] cexp = cexp
have rw₁ : deriv^[n] cexp = cexp
Tactic: rw [iterate_succ_apply, deriv_exp, iter_deriv_exp n]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ExpDeriv (goal)
Goal:
n : ℕ
rw : deriv^[n] (deriv cexp) = cexp
rw₁ : deriv^[n] cexp = cexp
⊢ deriv^[n + 1] cexp = cexp
have rw₂ : cexp = cexp
Tactic: rw [iterate_succ_apply, deriv_exp, iter_deriv_exp n]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ExpDeriv (goal)
Goal:
n : ℕ
c : ℂ
⊢ Eq (α := (x : ℂ) → ℂ) (iteratedDeriv n fun (s : ℂ) ↦ cexp (c * s)) fun (s : ℂ) ↦ c ^ n * cexp (c * s)
have rw : Eq (α := (x : ℂ) → ℂ) (fun (x : ℂ) ↦ c ^ n * iteratedDeriv n cexp (c * x)) fun (s : ℂ) ↦ c ^ n * cexp (c * s)
Tactic: rw [iteratedDeriv_comp_const_mul contDiff_exp, iteratedDeriv_eq_iterate, iter_deriv_exp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ExpDeriv (goal)
Goal:
n : ℕ
c : ℂ
rw : Eq (α := (x : ℂ) → ℂ) (fun (x : ℂ) ↦ c ^ n * iteratedDeriv n cexp (c * x)) fun (s : ℂ) ↦ c ^ n * cexp (c * s)
⊢ Eq (α := (x : ℂ) → ℂ) (iteratedDeriv n fun (s : ℂ) ↦ cexp (c * s)) fun (s : ℂ) ↦ c ^ n * cexp (c * s)
have rw₁ : Eq (α := (x : ℂ) → ℂ) (fun (x : ℂ) ↦ c ^ n * deriv^[n] cexp (c * x)) fun (s : ℂ) ↦ c ^ n * cexp (c * s)
Tactic: rw [iteratedDeriv_comp_const_mul contDiff_exp, iteratedDeriv_eq_iterate, iter_deriv_exp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ExpDeriv (goal)
Goal:
n : ℕ
c : ℂ
rw : Eq (α := (x : ℂ) → ℂ) (fun (x : ℂ) ↦ c ^ n * iteratedDeriv n cexp (c * x)) fun (s : ℂ) ↦ c ^ n * cexp (c * s)
rw₁ : Eq (α := (x : ℂ) → ℂ) (fun (x : ℂ) ↦ c ^ n * deriv^[n] cexp (c * x)) fun (s : ℂ) ↦ c ^ n * cexp (c * s)
⊢ Eq (α := (x : ℂ) → ℂ) (iteratedDeriv n fun (s : ℂ) ↦ cexp (c * s)) fun (s : ℂ) ↦ c ^ n * cexp (c * s)
have rw₂ : Eq (α := (x : ℂ) → ℂ) (fun (x : ℂ) ↦ c ^ n * cexp (c * x)) fun (s : ℂ) ↦ c ^ n * cexp (c * s)
Tactic: rw [iteratedDeriv_comp_const_mul contDiff_exp, iteratedDeriv_eq_iterate, iter_deriv_exp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ExpDeriv (goal)
Goal:
⊢ AnalyticOnNhd ℝ rexp univ
have rw : AnalyticOnNhd ℝ (E := ℝ) NormedSpace.exp univ
Tactic: rw [Real.exp_eq_exp_ℝ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ExpDeriv (goal)
Goal:
n : ℕ
⊢ deriv^[n + 1] rexp = rexp
have rw : deriv^[n] (deriv rexp) = rexp
Tactic: rw [iterate_succ_apply, deriv_exp, iter_deriv_exp n]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ExpDeriv (goal)
Goal:
n : ℕ
rw : deriv^[n] (deriv rexp) = rexp
⊢ deriv^[n + 1] rexp = rexp
have rw₁ : deriv^[n] rexp = rexp
Tactic: rw [iterate_succ_apply, deriv_exp, iter_deriv_exp n]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ExpDeriv (goal)
Goal:
n : ℕ
rw : deriv^[n] (deriv rexp) = rexp
rw₁ : deriv^[n] rexp = rexp
⊢ deriv^[n + 1] rexp = rexp
have rw₂ : rexp = rexp
Tactic: rw [iterate_succ_apply, deriv_exp, iter_deriv_exp n]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ExpDeriv (goal)
Goal:
n : ℕ
c : ℝ
⊢ Eq (α := (x : ℝ) → ℝ) (iteratedDeriv n fun (s : ℝ) ↦ rexp (c * s)) fun (s : ℝ) ↦ c ^ n * rexp (c * s)
have rw : Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ c ^ n * iteratedDeriv n rexp (c * x)) fun (s : ℝ) ↦ c ^ n * rexp (c * s)
Tactic: rw [iteratedDeriv_comp_const_mul contDiff_exp, iteratedDeriv_eq_iterate, iter_deriv_exp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ExpDeriv (goal)
Goal:
n : ℕ
c : ℝ
rw : Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ c ^ n * iteratedDeriv n rexp (c * x)) fun (s : ℝ) ↦ c ^ n * rexp (c * s)
⊢ Eq (α := (x : ℝ) → ℝ) (iteratedDeriv n fun (s : ℝ) ↦ rexp (c * s)) fun (s : ℝ) ↦ c ^ n * rexp (c * s)
have rw₁ : Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ c ^ n * deriv^[n] rexp (c * x)) fun (s : ℝ) ↦ c ^ n * rexp (c * s)
Tactic: rw [iteratedDeriv_comp_const_mul contDiff_exp, iteratedDeriv_eq_iterate, iter_deriv_exp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ExpDeriv (goal)
Goal:
n : ℕ
c : ℝ
rw : Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ c ^ n * iteratedDeriv n rexp (c * x)) fun (s : ℝ) ↦ c ^ n * rexp (c * s)
rw₁ : Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ c ^ n * deriv^[n] rexp (c * x)) fun (s : ℝ) ↦ c ^ n * rexp (c * s)
⊢ Eq (α := (x : ℝ) → ℝ) (iteratedDeriv n fun (s : ℝ) ↦ rexp (c * s)) fun (s : ℝ) ↦ c ^ n * rexp (c * s)
have rw₂ : Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ c ^ n * rexp (c * x)) fun (s : ℝ) ↦ c ^ n * rexp (c * s)
Tactic: rw [iteratedDeriv_comp_const_mul contDiff_exp, iteratedDeriv_eq_iterate, iter_deriv_exp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : CharZero 𝕂
inst_3 : NormedAlgebra 𝕂 𝔸
inst_4 : CompleteSpace 𝔸
h : 0 < FormalMultilinearSeries.radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸)
⊢ HasStrictFDerivAt.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) exp 1 0
have h₁ : Eq.{u_2 + 1} (α := AddCommGroup 𝔸) Ring.toAddCommGroup NormedAddCommGroup.toAddCommGroup →
  HEq (α := Module 𝕂 𝔸) (toModule : Module 𝕂 𝔸) (β := Module 𝕂 𝔸) (toModule : Module 𝕂 𝔸) →
    Eq (α := 𝔸 →L[𝕂] 𝔸) (1 : 𝔸 →L[𝕂] 𝔸)
      ((continuousMultilinearCurryFin1 𝕂 𝔸 𝔸 : (a : ContinuousMultilinearMap 𝕂 (fun (i : Fin 1) ↦ 𝔸) 𝔸) → 𝔸 →L[𝕂] 𝔸)
          (expSeries 𝕂 𝔸 1) :
        𝔸 →L[𝕂] 𝔸)
Tactic: convert! (hasFPowerSeriesAt_exp_zero_of_radius_pos h).hasStrictFDerivAt