awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst : NontriviallyNormedField 𝕂
inst_1 : CharZero 𝕂
inst_2 : NormedCommRing 𝕊
inst_3 : NormedRing 𝔸
inst_4 : NormedSpace 𝕂 𝕊
inst_5 : NormedAlgebra 𝕂 𝔸
inst_6 : Algebra 𝕊 𝔸
inst_7 : ContinuousSMul 𝕊 𝔸
inst_8 : IsScalarTower 𝕂 𝕊 𝔸
inst_9 : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx :
  Membership.mem (γ := Set 𝔸)
    (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_3, u_3} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) (t • x)
⊢ HasStrictFDerivAt (fun (u : 𝕊) ↦ exp (u • x))
    (HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x)) t

Tactic:
let ⟨_, hp⟩ := analyticAt_exp_of_mem_ball (t • x) htx
  have deriv₁ : HasStrictFDerivAt (fun u : 𝕊 => exp (u • x)) _ t :=
    hp.hasStrictFDerivAt.comp t ((ContinuousLinearMap.id 𝕂 𝕊).smulRight x).hasStrictFDerivAt
  have deriv₂ : HasFDerivAt (fun u : 𝕊 => exp (u • x)) _ t :=
    hasFDerivAt_exp_smul_const_of_mem_ball 𝕂 x t htx
  deriv₁.hasFDerivAt.unique deriv₂ ▸ deriv₁

Premises used: ContinuousLinearMap.smulRight, NormedSpace.exp, _private.0.hasStrictFDerivAt_exp_smul_const_of_mem_ball.match_1, NormedSpace.analyticAt_exp_of_mem_ball, Eq.rec, ContinuousLinearMap.id, HasStrictFDerivAt.hasFDerivAt, hasFDerivAt_exp_smul_const_of_mem_ball, ContinuousLinearMap.hasStrictFDerivAt, HasStrictFDerivAt, HSMul.hSMul, HasStrictFDerivAt.comp, HasFDerivAt.unique, OfNat.ofNat, HasFPowerSeriesAt.hasStrictFDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst : NontriviallyNormedField 𝕂
inst_1 : CharZero 𝕂
inst_2 : NormedCommRing 𝕊
inst_3 : NormedRing 𝔸
inst_4 : NormedSpace 𝕂 𝕊
inst_5 : NormedAlgebra 𝕂 𝔸
inst_6 : Algebra 𝕊 𝔸
inst_7 : ContinuousSMul 𝕊 𝔸
inst_8 : IsScalarTower 𝕂 𝕊 𝔸
inst_9 : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx :
  Membership.mem (γ := Set 𝔸)
    (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_3, u_3} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) (t • x)
let :
  ∀ (w : FormalMultilinearSeries 𝕂 𝔸 𝔸),
    HasFPowerSeriesAt exp w (t • x) →
      HasStrictFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕂) (fun (u : 𝕊) ↦ exp (u • x))
        (ContinuousLinearMap.smulRight (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) (exp (t • x))) t
⊢ HasStrictFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕂) (fun (u : 𝕊) ↦ exp (u • x))
    (ContinuousLinearMap.smulRight (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) (exp (t • x))) t

Tactic:
let ⟨_, _⟩ := analyticAt_exp_of_mem_ball (t • x) htx
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst : NontriviallyNormedField 𝕂
inst_1 : CharZero 𝕂
inst_2 : NormedCommRing 𝕊
inst_3 : NormedRing 𝔸
inst_4 : NormedSpace 𝕂 𝕊
inst_5 : NormedAlgebra 𝕂 𝔸
inst_6 : Algebra 𝕊 𝔸
inst_7 : ContinuousSMul 𝕊 𝔸
inst_8 : IsScalarTower 𝕂 𝕊 𝔸
inst_9 : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx :
  Membership.mem (γ := Set 𝔸)
    (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_3, u_3} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) (t • x)
w : FormalMultilinearSeries 𝕂 𝔸 𝔸
h : HasFPowerSeriesAt exp w (t • x)
⊢ HasStrictFDerivAt (fun (u : 𝕊) ↦ exp (u • x))
    (HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x)) t

Tactic:
hasStrictFDerivAt_exp_smul_const_of_mem_ball 𝕂 _ _ htx

Premises used: hasStrictFDerivAt_exp_smul_const_of_mem_ball
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst : NontriviallyNormedField 𝕂
inst_1 : CharZero 𝕂
inst_2 : NormedCommRing 𝕊
inst_3 : NormedRing 𝔸
inst_4 : NormedSpace 𝕂 𝕊
inst_5 : NormedAlgebra 𝕂 𝔸
inst_6 : Algebra 𝕊 𝔸
inst_7 : ContinuousSMul 𝕊 𝔸
inst_8 : IsScalarTower 𝕂 𝕊 𝔸
inst_9 : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx :
  Membership.mem (γ := Set 𝔸)
    (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_3, u_3} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) (t • x)
w : FormalMultilinearSeries 𝕂 𝔸 𝔸
h_1 : HasFPowerSeriesAt exp w (t • x)
h :
  ContinuousLinearMap.smulRight (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) (exp (t • x)) =
    HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x)
⊢ HasStrictFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕂) (fun (u : 𝕊) ↦ exp (u • x))
    (ContinuousLinearMap.smulRight (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) (exp (t • x))) t

Tactic:
convert! hasStrictFDerivAt_exp_smul_const_of_mem_ball 𝕂 _ _ htx using 1

Premises used: hasStrictFDerivAt_exp_smul_const_of_mem_ball
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst : NontriviallyNormedField 𝕂
inst_1 : CharZero 𝕂
inst_2 : NormedCommRing 𝕊
inst_3 : NormedRing 𝔸
inst_4 : NormedSpace 𝕂 𝕊
inst_5 : NormedAlgebra 𝕂 𝔸
inst_6 : Algebra 𝕊 𝔸
inst_7 : ContinuousSMul 𝕊 𝔸
inst_8 : IsScalarTower 𝕂 𝕊 𝔸
inst_9 : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx :
  Membership.mem (γ := Set 𝔸)
    (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_3, u_3} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) (t • x)
w : FormalMultilinearSeries 𝕂 𝔸 𝔸
h_1 : HasFPowerSeriesAt exp w (t • x)
h :
  ∀ (t' : 𝕊),
    Eq.{u_3 + 1} (α := 𝔸)
      ((ContinuousLinearMap.smulRight (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) (exp (t • x)) : (a : 𝕊) → 𝔸) t' : 𝔸)
      ((HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) : (a : 𝕊) → 𝔸) t' : 𝔸)
⊢ ContinuousLinearMap.smulRight (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) (exp (t • x)) =
    HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x)

Tactic:
ext t'
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst : NontriviallyNormedField 𝕂
inst_1 : CharZero 𝕂
inst_2 : NormedCommRing 𝕊
inst_3 : NormedRing 𝔸
inst_4 : NormedSpace 𝕂 𝕊
inst_5 : NormedAlgebra 𝕂 𝔸
inst_6 : Algebra 𝕊 𝔸
inst_7 : ContinuousSMul 𝕊 𝔸
inst_8 : IsScalarTower 𝕂 𝕊 𝔸
inst_9 : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx :
  Membership.mem (γ := Set 𝔸)
    (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_3, u_3} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) (t • x)
w : FormalMultilinearSeries 𝕂 𝔸 𝔸
h_1 : HasFPowerSeriesAt exp w (t • x)
t' : 𝕊
h : Commute (t' • x) (exp (t • x))
⊢ Eq.{u_3 + 1} (α := 𝔸)
    ((ContinuousLinearMap.smulRight (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) (exp (t • x)) : (a : 𝕊) → 𝔸) t' : 𝔸)
    ((HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) : (a : 𝕊) → 𝔸) t' : 𝔸)

Tactic:
change Commute (t' • x) (exp (t • x))

Premises used: NormedSpace.exp, Commute, HSMul.hSMul
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst : NontriviallyNormedField 𝕂
inst_1 : CharZero 𝕂
inst_2 : NormedCommRing 𝕊
inst_3 : NormedRing 𝔸
inst_4 : NormedSpace 𝕂 𝕊
inst_5 : NormedAlgebra 𝕂 𝔸
inst_6 : Algebra 𝕊 𝔸
inst_7 : ContinuousSMul 𝕊 𝔸
inst_8 : IsScalarTower 𝕂 𝕊 𝔸
inst_9 : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx :
  Membership.mem (γ := Set 𝔸)
    (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_3, u_3} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) (t • x)
w : FormalMultilinearSeries 𝕂 𝔸 𝔸
h : HasFPowerSeriesAt exp w (t • x)
t' : 𝕊
⊢ Commute (t' • x) (exp (t • x))

Tactic:
(((Commute.refl x).smul_left t').smul_right t).exp_right

Premises used: Commute.exp_right, Commute.smul_left, Commute.smul_right, Commute.refl
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst : NontriviallyNormedField 𝕂
inst_1 : CharZero 𝕂
inst_2 : NormedCommRing 𝕊
inst_3 : NormedRing 𝔸
inst_4 : NormedSpace 𝕂 𝕊
inst_5 : NormedAlgebra 𝕂 𝔸
inst_6 : Algebra 𝕊 𝔸
inst_7 : ContinuousSMul 𝕊 𝔸
inst_8 : IsScalarTower 𝕂 𝕊 𝔸
inst_9 : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx :
  Membership.mem (γ := Set 𝔸)
    (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_3, u_3} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) (t • x)
w : FormalMultilinearSeries 𝕂 𝔸 𝔸
h : HasFPowerSeriesAt exp w (t • x)
t' : 𝕊
⊢ Commute (t' • x) (exp (t • x))

Tactic:
exact (((Commute.refl x).smul_left t').smul_right t).exp_right

Premises used: Commute.exp_right, Commute.smul_left, Commute.smul_right, Commute.refl
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_3
inst : NontriviallyNormedField 𝕂
inst_1 : CharZero 𝕂
inst_2 : NormedRing 𝔸
inst_3 : NormedAlgebra 𝕂 𝔸
inst_4 : CompleteSpace 𝔸
x : 𝔸
t : 𝕂
htx :
  Membership.mem (γ := Set 𝔸)
    (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_3, u_3} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) (t • x)
⊢ HasStrictDerivAt (fun (u : 𝕂) ↦ exp (u • x)) (exp (t • x) * x) t

Tactic:
simpa using (hasStrictFDerivAt_exp_smul_const_of_mem_ball 𝕂 x t htx).hasStrictDerivAt

Premises used: HasStrictFDerivAt.hasStrictDerivAt, hasStrictFDerivAt_exp_smul_const_of_mem_ball
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_3
inst : NontriviallyNormedField 𝕂
inst_1 : CharZero 𝕂
inst_2 : NormedRing 𝔸
inst_3 : NormedAlgebra 𝕂 𝔸
inst_4 : CompleteSpace 𝔸
x : 𝔸
t : 𝕂
htx :
  Membership.mem (γ := Set 𝔸)
    (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_3, u_3} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) (t • x)
⊢ HasStrictDerivAt (fun (u : 𝕂) ↦ exp (u • x)) (x * exp (t • x)) t

Tactic:
simpa using (hasStrictFDerivAt_exp_smul_const_of_mem_ball' 𝕂 x t htx).hasStrictDerivAt

Premises used: hasStrictFDerivAt_exp_smul_const_of_mem_ball', HasStrictFDerivAt.hasStrictDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_3
inst : NontriviallyNormedField 𝕂
inst_1 : CharZero 𝕂
inst_2 : NormedRing 𝔸
inst_3 : NormedAlgebra 𝕂 𝔸
inst_4 : CompleteSpace 𝔸
x : 𝔸
t : 𝕂
htx :
  Membership.mem (γ := Set 𝔸)
    (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_3, u_3} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) (t • x)
⊢ HasDerivAt (fun (u : 𝕂) ↦ exp (u • x)) (exp (t • x) * x) t

Tactic:
(hasStrictDerivAt_exp_smul_const_of_mem_ball x t htx).hasDerivAt

Premises used: HasStrictDerivAt.hasDerivAt, hasStrictDerivAt_exp_smul_const_of_mem_ball
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_3
inst : NontriviallyNormedField 𝕂
inst_1 : CharZero 𝕂
inst_2 : NormedRing 𝔸
inst_3 : NormedAlgebra 𝕂 𝔸
inst_4 : CompleteSpace 𝔸
x : 𝔸
t : 𝕂
htx :
  Membership.mem (γ := Set 𝔸)
    (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_3, u_3} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) (t • x)
⊢ HasDerivAt (fun (u : 𝕂) ↦ exp (u • x)) (x * exp (t • x)) t

Tactic:
(hasStrictDerivAt_exp_smul_const_of_mem_ball' x t htx).hasDerivAt

Premises used: HasStrictDerivAt.hasDerivAt, hasStrictDerivAt_exp_smul_const_of_mem_ball'
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst : RCLike 𝕂
inst_1 : NormedCommRing 𝕊
inst_2 : NormedRing 𝔸
inst_3 : NormedAlgebra 𝕂 𝕊
inst_4 : NormedAlgebra 𝕂 𝔸
inst_5 : Algebra 𝕊 𝔸
inst_6 : ContinuousSMul 𝕊 𝔸
inst_7 : IsScalarTower 𝕂 𝕊 𝔸
inst_8 : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
⊢ HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕂) (F := 𝔸) (fun (u : 𝕊) ↦ exp (u • x))
    (HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x)) t

Tactic:
hasFDerivAt_exp_smul_const_of_mem_ball 𝕂 _ _ <|
    (expSeries_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _

Premises used: Eq.rec, NormedSpace.expSeries_radius_eq_top, hasFDerivAt_exp_smul_const_of_mem_ball, edist_lt_top, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst : RCLike 𝕂
inst_1 : NormedCommRing 𝕊
inst_2 : NormedRing 𝔸
inst_3 : NormedAlgebra 𝕂 𝕊
inst_4 : NormedAlgebra 𝕂 𝔸
inst_5 : Algebra 𝕊 𝔸
inst_6 : ContinuousSMul 𝕊 𝔸
inst_7 : IsScalarTower 𝕂 𝕊 𝔸
inst_8 : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
⊢ HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕂) (fun (u : 𝕊) ↦ exp (u • x))
    (ContinuousLinearMap.smulRight (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) (exp (t • x))) t

Tactic:
hasFDerivAt_exp_smul_const_of_mem_ball' 𝕂 _ _ <|
    (expSeries_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _

Premises used: Eq.rec, NormedSpace.expSeries_radius_eq_top, edist_lt_top, hasFDerivAt_exp_smul_const_of_mem_ball', Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst : RCLike 𝕂
inst_1 : NormedCommRing 𝕊
inst_2 : NormedRing 𝔸
inst_3 : NormedAlgebra 𝕂 𝕊
inst_4 : NormedAlgebra 𝕂 𝔸
inst_5 : Algebra 𝕊 𝔸
inst_6 : ContinuousSMul 𝕊 𝔸
inst_7 : IsScalarTower 𝕂 𝕊 𝔸
inst_8 : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
⊢ HasStrictFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕂) (F := 𝔸) (fun (u : 𝕊) ↦ exp (u • x))
    (HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x)) t

Tactic:
hasStrictFDerivAt_exp_smul_const_of_mem_ball 𝕂 _ _ <|
    (expSeries_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _

Premises used: Eq.rec, NormedSpace.expSeries_radius_eq_top, edist_lt_top, Eq.symm, hasStrictFDerivAt_exp_smul_const_of_mem_ball
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst : RCLike 𝕂
inst_1 : NormedCommRing 𝕊
inst_2 : NormedRing 𝔸
inst_3 : NormedAlgebra 𝕂 𝕊
inst_4 : NormedAlgebra 𝕂 𝔸
inst_5 : Algebra 𝕊 𝔸
inst_6 : ContinuousSMul 𝕊 𝔸
inst_7 : IsScalarTower 𝕂 𝕊 𝔸
inst_8 : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
⊢ HasStrictFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕂) (fun (u : 𝕊) ↦ exp (u • x))
    (ContinuousLinearMap.smulRight (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) (exp (t • x))) t

Tactic:
hasStrictFDerivAt_exp_smul_const_of_mem_ball' 𝕂 _ _ <|
    (expSeries_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _

Premises used: hasStrictFDerivAt_exp_smul_const_of_mem_ball', Eq.rec, NormedSpace.expSeries_radius_eq_top, edist_lt_top, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_3
inst : RCLike 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
x : 𝔸
t : 𝕂
⊢ HasStrictDerivAt (fun (u : 𝕂) ↦ exp (u • x)) (exp (t • x) * x) t

Tactic:
hasStrictDerivAt_exp_smul_const_of_mem_ball _ _ <|
    (expSeries_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _

Premises used: Eq.rec, NormedSpace.expSeries_radius_eq_top, edist_lt_top, Eq.symm, hasStrictDerivAt_exp_smul_const_of_mem_ball
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_3
inst : RCLike 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
x : 𝔸
t : 𝕂
⊢ HasStrictDerivAt (fun (u : 𝕂) ↦ exp (u • x)) (x * exp (t • x)) t

Tactic:
hasStrictDerivAt_exp_smul_const_of_mem_ball' _ _ <|
    (expSeries_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _

Premises used: Eq.rec, NormedSpace.expSeries_radius_eq_top, edist_lt_top, hasStrictDerivAt_exp_smul_const_of_mem_ball', Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_3
inst : RCLike 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
x : 𝔸
t : 𝕂
⊢ HasDerivAt (fun (u : 𝕂) ↦ exp (u • x)) (exp (t • x) * x) t

Tactic:
hasDerivAt_exp_smul_const_of_mem_ball _ _ <| (expSeries_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _

Premises used: Eq.rec, NormedSpace.expSeries_radius_eq_top, edist_lt_top, Eq.symm, hasDerivAt_exp_smul_const_of_mem_ball
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_3
inst : RCLike 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
x : 𝔸
t : 𝕂
⊢ HasDerivAt (fun (u : 𝕂) ↦ exp (u • x)) (x * exp (t • x)) t

Tactic:
hasDerivAt_exp_smul_const_of_mem_ball' _ _ <|
    (expSeries_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _

Premises used: Eq.rec, NormedSpace.expSeries_radius_eq_top, edist_lt_top, hasDerivAt_exp_smul_const_of_mem_ball', Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_3
inst : RCLike 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
x : 𝔸
⊢ Differentiable.{u_1, u_1, u_3} 𝕂 (F := 𝔸) fun (t : 𝕂) ↦ exp (t • x)

Tactic:
(⟨_, hasDerivAt_exp_smul_const x ·⟩)

Premises used: Differentiable, HMul.hMul, DifferentiableAt, NormedSpace.exp, hasDerivAt_exp_smul_const, ContinuousLinearMap.toSpanSingleton, Exists.intro, HSMul.hSMul
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_3
inst : RCLike 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
x : 𝔸
r : 𝕂
⊢ DifferentiableAt.{u_1, u_1, u_3} 𝕂 (F := 𝔸) (fun (t : 𝕂) ↦ exp (t • x)) r

Tactic:
differentiable_exp_smul_const 𝕂 x |>.differentiableAt

Premises used: Differentiable.differentiableAt, differentiable_exp_smul_const
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝔸 : Type u_1
inst : NormedCommRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
ι : Type u_2
f : ι → 𝔸
a : 𝔸
h : HasSum f a
⊢ HasProd (NormedSpace.exp ∘ f) (NormedSpace.exp a)

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

Premises used: Filter.Tendsto.exp, HasProd, NormedSpace.exp_sum, Filter.Tendsto.congr
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (-x) * x ^ s) fun (x : ℝ) ↦ rexp (-(1 / 2) * x)

Tactic:
isLittleO_of_tendsto (fun x hx => ?_) ?_

Premises used: Asymptotics.isLittleO_of_tendsto
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
refine_1 : ∀ (x : ℝ) (hx : rexp (-(1 / 2) * x) = 0), rexp (-x) * x ^ s = 0
refine_2 : Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (-x) * x ^ s / rexp (-(1 / 2) * x)) atTop (𝓝 0)
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (-x) * x ^ s) fun (x : ℝ) ↦ rexp (-(1 / 2) * x)

Tactic:
refine isLittleO_of_tendsto (fun x hx => ?_) ?_

Premises used: Asymptotics.isLittleO_of_tendsto
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s x : ℝ
hx : rexp (-(1 / 2) * x) = 0
refine_1 : False
⊢ rexp (-x) * x ^ s = 0

Tactic:
exfalso
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s x : ℝ
hx : rexp (-(1 / 2) * x) = 0
⊢ False

Tactic:
(exp_pos (-(1 / 2) * x)).ne' hx

Premises used: HMul.hMul, HDiv.hDiv, LT.lt.ne', OfNat.ofNat, Neg.neg, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s x : ℝ
hx : rexp (-(1 / 2) * x) = 0
⊢ False

Tactic:
exact (exp_pos (-(1 / 2) * x)).ne' hx

Premises used: HMul.hMul, HDiv.hDiv, LT.lt.ne', OfNat.ofNat, Neg.neg, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
h : ∀ (x : ℝ), rexp (-x) * x ^ s / rexp (-(1 / 2) * x) = (fun (x : ℝ) ↦ rexp (1 / 2 * x) / x ^ s)⁻¹ x
⊢ Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ rexp (-x) * x ^ s / rexp (-(1 / 2) * x))
    (fun (x : ℝ) ↦ rexp (1 / 2 * x) / x ^ s)⁻¹

Tactic:
ext1 x
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s x : ℝ
⊢ rexp (-x) * x ^ s / rexp (-(1 / 2) * x) = (fun (x : ℝ) ↦ rexp (1 / 2 * x) / x ^ s)⁻¹ x

Tactic:
simp [field, ← exp_nsmul, exp_neg]

Premises used: Real.exp_nsmul, Real.exp_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
⊢ Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ rexp (-x) * x ^ s / rexp (-(1 / 2) * x))
    (fun (x : ℝ) ↦ rexp (1 / 2 * x) / x ^ s)⁻¹

Tactic:
have : (fun x : ℝ => exp (-x) * x ^ s / exp (-(1 / 2) * x)) =
      (fun x : ℝ => exp (1 / 2 * x) / x ^ s)⁻¹ := by
    ext1 x
    simp [field, ← exp_nsmul, exp_neg]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
this :
  Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ rexp (-x) * x ^ s / rexp (-(1 / 2) * x))
    (fun (x : ℝ) ↦ rexp (1 / 2 * x) / x ^ s)⁻¹
refine_2 : Tendsto (α := ℝ) (β := ℝ) (fun (x : ℝ) ↦ rexp (1 / 2 * x) / x ^ s)⁻¹ atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (-x) * x ^ s / rexp (-(1 / 2) * x)) atTop (𝓝 0)

Tactic:
rw [this]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
this :
  Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ rexp (-x) * x ^ s / rexp (-(1 / 2) * x))
    (fun (x : ℝ) ↦ rexp (1 / 2 * x) / x ^ s)⁻¹
⊢ Tendsto (α := ℝ) (β := ℝ) (fun (x : ℝ) ↦ rexp (1 / 2 * x) / x ^ s)⁻¹ atTop (𝓝 0)

Tactic:
(tendsto_exp_mul_div_rpow_atTop s (1 / 2) one_half_pos).inv_tendsto_atTop

Premises used: HDiv.hDiv, one_half_pos, Filter.Tendsto.inv_tendsto_atTop, OfNat.ofNat, tendsto_exp_mul_div_rpow_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
this :
  Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ rexp (-x) * x ^ s / rexp (-(1 / 2) * x))
    (fun (x : ℝ) ↦ rexp (1 / 2 * x) / x ^ s)⁻¹
⊢ Tendsto (α := ℝ) (β := ℝ) (fun (x : ℝ) ↦ rexp (1 / 2 * x) / x ^ s)⁻¹ atTop (𝓝 0)

Tactic:
exact (tendsto_exp_mul_div_rpow_atTop s (1 / 2) one_half_pos).inv_tendsto_atTop

Premises used: HDiv.hDiv, one_half_pos, Filter.Tendsto.inv_tendsto_atTop, OfNat.ofNat, tendsto_exp_mul_div_rpow_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
h : 0 < s
rw :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) (Ioc 0 1)
      volume ∧
    IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) (Ioi 1) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) (Ioi 0) volume

Tactic:
rw [← Ioc_union_Ioi_eq_Ioi (@zero_le_one ℝ _ _ _ _), integrableOn_union]

Premises used: MeasureTheory.integrableOn_union, Set.Ioc_union_Ioi_eq_Ioi, zero_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
h : 0 < s
left :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) (Ioc 0 1) volume
right :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) (Ioi 1) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) (Ioc 0 1)
      volume ∧
    IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) (Ioi 1) volume

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
h : 0 < s
left :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) (Icc 0 1) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) (Ioc 0 1) volume

Tactic:
rw [← integrableOn_Icc_iff_integrableOn_Ioc]

Premises used: integrableOn_Icc_iff_integrableOn_Ioc
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
h : 0 < s
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) (Icc 0 1) volume

Tactic:
IntegrableOn.continuousOn_mul continuousOn_id.neg.rexp ?_ isCompact_Icc

Premises used: ContinuousOn.neg, CompactIccSpace.isCompact_Icc, MeasureTheory.IntegrableOn.continuousOn_mul, continuousOn_id, ContinuousOn.rexp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
h : 0 < s
left : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ (s - 1)) (Icc 0 1) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) (Icc 0 1) volume

Tactic:
refine IntegrableOn.continuousOn_mul continuousOn_id.neg.rexp ?_ isCompact_Icc

Premises used: ContinuousOn.neg, CompactIccSpace.isCompact_Icc, MeasureTheory.IntegrableOn.continuousOn_mul, continuousOn_id, ContinuousOn.rexp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
h : 0 < s
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ (s - 1)) (Icc 0 1) volume

Tactic:
(intervalIntegrable_iff_integrableOn_Icc_of_le zero_le_one).mp ?_

Premises used: intervalIntegrable_iff_integrableOn_Icc_of_le, zero_le_one, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
h : 0 < s
left : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ (s - 1)) volume 0 1
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ (s - 1)) (Icc 0 1) volume

Tactic:
refine (intervalIntegrable_iff_integrableOn_Icc_of_le zero_le_one).mp ?_

Premises used: intervalIntegrable_iff_integrableOn_Icc_of_le, zero_le_one, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
h : 0 < s
linarith : s - 1 ≤ -1 → 0 - s + (s - 1 - -1) = 0
⊢ -1 < s - 1

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
h : 0 < s
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ (s - 1)) volume 0 1

Tactic:
exact intervalIntegrable_rpow' (by linarith)

Premises used: intervalIntegral.intervalIntegrable_rpow'