awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exponential (hypothesis)
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)
this_1 : Tendsto.{u_2, u_3} (β := 𝔸) (fun (h : 𝕊) ↦ h • x) (𝓝 0) (𝓝 0)
this :
  ∀ᶠ (h : 𝕊) in 𝓝 0,
    Membership.mem (γ := Set 𝔸)
      (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_3, u_3} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸)))
      (h • x)
h : 𝕊
hh :
  Membership.mem (γ := Set 𝔸)
    (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_3, u_3} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) (h • x)
⊢ exp (t • x) *
      HSub.hSub (β := 𝔸) (exp ((0 + h) • x) - exp (HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕊) 0 x))
        ((ContinuousLinearMap.smulRight (S := 𝕊) 1 x : (a : 𝕊) → 𝔸) h : 𝔸) =
    HSub.hSub (β := 𝔸) (exp ((t + h) • x) - exp (t • x))
      ((HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) : (a : 𝕊) → 𝔸) h : 𝔸)
have this₁ : Commute (t • x) (h • x)
Tactic: have : Commute (t • x) (h • x) := ((Commute.refl x).smul_left t).smul_right h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exponential (goal)
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)
this_1 : Tendsto.{u_2, u_3} (β := 𝔸) (fun (h : 𝕊) ↦ h • x) (𝓝 0) (𝓝 0)
this_2 :
  ∀ᶠ (h : 𝕊) in 𝓝 0,
    Membership.mem (γ := Set 𝔸)
      (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_3, u_3} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸)))
      (h • x)
h : 𝕊
hh :
  Membership.mem (γ := Set 𝔸)
    (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_3, u_3} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) (h • x)
this : Commute (t • x) (h • x)
⊢ exp (t • x) *
      HSub.hSub (β := 𝔸) (exp ((0 + h) • x) - exp (HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕊) 0 x))
        ((ContinuousLinearMap.smulRight (S := 𝕊) 1 x : (a : 𝕊) → 𝔸) h : 𝔸) =
    HSub.hSub (β := 𝔸) (exp ((t + h) • x) - exp (t • x))
      ((HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) : (a : 𝕊) → 𝔸) h : 𝔸)
have h₁ : exp (t • x) *
    HSub.hSub (β := 𝔸) (exp ((0 + h) • x) - exp (HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕊) 0 x))
      ((ContinuousLinearMap.smulRight (S := 𝕊) 1 x : (a : 𝕊) → 𝔸) h : 𝔸) =
  HSub.hSub (β := 𝔸) (exp (t • x + h • x) - exp (t • x))
    ((HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) : (a : 𝕊) → 𝔸) h : 𝔸)
Tactic: rw [add_smul t h, exp_add_of_commute_of_mem_ball this htx hh, zero_add, zero_smul, exp_zero,
    ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply,
    ContinuousLinearMap.smul_apply, ContinuousLinearMap.smulRight_apply,
    ContinuousLinearMap.one_apply, smul_eq_mul, mul_sub_left_distrib, mul_sub_left_distrib, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exponential (goal)
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)
this_1 : Tendsto.{u_2, u_3} (β := 𝔸) (fun (h : 𝕊) ↦ h • x) (𝓝 0) (𝓝 0)
this_2 :
  ∀ᶠ (h : 𝕊) in 𝓝 0,
    Membership.mem (γ := Set 𝔸)
      (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_3, u_3} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸)))
      (h • x)
h : 𝕊
hh :
  Membership.mem (γ := Set 𝔸)
    (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_3, u_3} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) (h • x)
this : Commute (t • x) (h • x)
h₁ :
  exp (t • x) *
      HSub.hSub (β := 𝔸) (exp ((0 + h) • x) - exp (HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕊) 0 x))
        ((ContinuousLinearMap.smulRight (S := 𝕊) 1 x : (a : 𝕊) → 𝔸) h : 𝔸) =
    HSub.hSub (β := 𝔸) (exp (t • x + h • x) - exp (t • x))
      ((HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) : (a : 𝕊) → 𝔸) h : 𝔸)
⊢ exp (t • x) *
      HSub.hSub (β := 𝔸) (exp ((0 + h) • x) - exp (HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕊) 0 x))
        ((ContinuousLinearMap.smulRight (S := 𝕊) 1 x : (a : 𝕊) → 𝔸) h : 𝔸) =
    HSub.hSub (β := 𝔸) (exp ((t + h) • x) - exp (t • x))
      ((HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) : (a : 𝕊) → 𝔸) h : 𝔸)
have h₂ : exp (t • x) *
    HSub.hSub (β := 𝔸) (exp ((0 + h) • x) - exp (HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕊) 0 x))
      ((ContinuousLinearMap.smulRight (S := 𝕊) 1 x : (a : 𝕊) → 𝔸) h : 𝔸) =
  HSub.hSub (β := 𝔸) (exp (t • x) * exp (h • x) - exp (t • x))
    ((HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) : (a : 𝕊) → 𝔸) h : 𝔸)
Tactic: rw [add_smul t h, exp_add_of_commute_of_mem_ball this htx hh, zero_add, zero_smul, exp_zero,
    ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply,
    ContinuousLinearMap.smul_apply, ContinuousLinearMap.smulRight_apply,
    ContinuousLinearMap.one_apply, smul_eq_mul, mul_sub_left_distrib, mul_sub_left_distrib, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exponential (goal)
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)
this_1 : Tendsto.{u_2, u_3} (β := 𝔸) (fun (h : 𝕊) ↦ h • x) (𝓝 0) (𝓝 0)
this_2 :
  ∀ᶠ (h : 𝕊) in 𝓝 0,
    Membership.mem (γ := Set 𝔸)
      (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_3, u_3} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸)))
      (h • x)
h : 𝕊
hh :
  Membership.mem (γ := Set 𝔸)
    (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_3, u_3} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) (h • x)
this : Commute (t • x) (h • x)
h₁ :
  exp (t • x) *
      HSub.hSub (β := 𝔸) (exp ((0 + h) • x) - exp (HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕊) 0 x))
        ((ContinuousLinearMap.smulRight (S := 𝕊) 1 x : (a : 𝕊) → 𝔸) h : 𝔸) =
    HSub.hSub (β := 𝔸) (exp (t • x + h • x) - exp (t • x))
      ((HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) : (a : 𝕊) → 𝔸) h : 𝔸)
h₂ :
  exp (t • x) *
      HSub.hSub (β := 𝔸) (exp ((0 + h) • x) - exp (HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕊) 0 x))
        ((ContinuousLinearMap.smulRight (S := 𝕊) 1 x : (a : 𝕊) → 𝔸) h : 𝔸) =
    HSub.hSub (β := 𝔸) (exp (t • x) * exp (h • x) - exp (t • x))
      ((HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) : (a : 𝕊) → 𝔸) h : 𝔸)
⊢ exp (t • x) *
      HSub.hSub (β := 𝔸) (exp ((0 + h) • x) - exp (HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕊) 0 x))
        ((ContinuousLinearMap.smulRight (S := 𝕊) 1 x : (a : 𝕊) → 𝔸) h : 𝔸) =
    HSub.hSub (β := 𝔸) (exp ((t + h) • x) - exp (t • x))
      ((HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) : (a : 𝕊) → 𝔸) h : 𝔸)
have h₃ : exp (t • x) *
    HSub.hSub (β := 𝔸) (exp (h • x) - exp (HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕊) 0 x))
      ((ContinuousLinearMap.smulRight (S := 𝕊) 1 x : (a : 𝕊) → 𝔸) h : 𝔸) =
  HSub.hSub (β := 𝔸) (exp (t • x) * exp (h • x) - exp (t • x))
    ((HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) : (a : 𝕊) → 𝔸) h : 𝔸)
Tactic: rw [add_smul t h, exp_add_of_commute_of_mem_ball this htx hh, zero_add, zero_smul, exp_zero,
    ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply,
    ContinuousLinearMap.smul_apply, ContinuousLinearMap.smulRight_apply,
    ContinuousLinearMap.one_apply, smul_eq_mul, mul_sub_left_distrib, mul_sub_left_distrib, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exponential (goal)
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)
this_1 : Tendsto.{u_2, u_3} (β := 𝔸) (fun (h : 𝕊) ↦ h • x) (𝓝 0) (𝓝 0)
this_2 :
  ∀ᶠ (h : 𝕊) in 𝓝 0,
    Membership.mem (γ := Set 𝔸)
      (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_3, u_3} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸)))
      (h • x)
h : 𝕊
hh :
  Membership.mem (γ := Set 𝔸)
    (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_3, u_3} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) (h • x)
this : Commute (t • x) (h • x)
h₁ :
  exp (t • x) *
      HSub.hSub (β := 𝔸) (exp ((0 + h) • x) - exp (HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕊) 0 x))
        ((ContinuousLinearMap.smulRight (S := 𝕊) 1 x : (a : 𝕊) → 𝔸) h : 𝔸) =
    HSub.hSub (β := 𝔸) (exp (t • x + h • x) - exp (t • x))
      ((HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) : (a : 𝕊) → 𝔸) h : 𝔸)
h₂ :
  exp (t • x) *
      HSub.hSub (β := 𝔸) (exp ((0 + h) • x) - exp (HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕊) 0 x))
        ((ContinuousLinearMap.smulRight (S := 𝕊) 1 x : (a : 𝕊) → 𝔸) h : 𝔸) =
    HSub.hSub (β := 𝔸) (exp (t • x) * exp (h • x) - exp (t • x))
      ((HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) : (a : 𝕊) → 𝔸) h : 𝔸)
h₃ :
  exp (t • x) *
      HSub.hSub (β := 𝔸) (exp (h • x) - exp (HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕊) 0 x))
        ((ContinuousLinearMap.smulRight (S := 𝕊) 1 x : (a : 𝕊) → 𝔸) h : 𝔸) =
    HSub.hSub (β := 𝔸) (exp (t • x) * exp (h • x) - exp (t • x))
      ((HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) : (a : 𝕊) → 𝔸) h : 𝔸)
⊢ exp (t • x) *
      HSub.hSub (β := 𝔸) (exp ((0 + h) • x) - exp (HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕊) 0 x))
        ((ContinuousLinearMap.smulRight (S := 𝕊) 1 x : (a : 𝕊) → 𝔸) h : 𝔸) =
    HSub.hSub (β := 𝔸) (exp ((t + h) • x) - exp (t • x))
      ((HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) : (a : 𝕊) → 𝔸) h : 𝔸)
have h₄ : exp (t • x) *
    HSub.hSub (β := 𝔸) (exp (h • x) - exp 0) ((ContinuousLinearMap.smulRight (S := 𝕊) 1 x : (a : 𝕊) → 𝔸) h : 𝔸) =
  HSub.hSub (β := 𝔸) (exp (t • x) * exp (h • x) - exp (t • x))
    ((HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) : (a : 𝕊) → 𝔸) h : 𝔸)
Tactic: rw [add_smul t h, exp_add_of_commute_of_mem_ball this htx hh, zero_add, zero_smul, exp_zero,
    ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply,
    ContinuousLinearMap.smul_apply, ContinuousLinearMap.smulRight_apply,
    ContinuousLinearMap.one_apply, smul_eq_mul, mul_sub_left_distrib, mul_sub_left_distrib, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exponential (goal)
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)
⊢ HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕂) (fun (u : 𝕊) ↦ exp (u • x))
    (ContinuousLinearMap.smulRight (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) (exp (t • x))) t
have h : ContinuousLinearMap.smulRight (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) (exp (t • x)) =
  HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x)
Tactic: convert! hasFDerivAt_exp_smul_const_of_mem_ball 𝕂 _ _ htx using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exponential (goal)
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)
⊢ ContinuousLinearMap.smulRight (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) (exp (t • x)) =
    HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x)
have 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' : 𝔸)
Tactic: ext t'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exponential (goal)
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)
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' : 𝔸)
have h : Commute (t' • x) (exp (t • x))
Tactic: change Commute (t' • x) (exp (t • x))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exponential (goal)
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.{u_1, u_2, u_3} (𝕜 := 𝕂) (fun (u : 𝕊) ↦ exp (u • x))
    (ContinuousLinearMap.smulRight (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) (exp (t • x))) t
have 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
Tactic: let ⟨_, _⟩ := analyticAt_exp_of_mem_ball (t • x) htx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exponential (goal)
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.{u_1, u_2, u_3} (𝕜 := 𝕂) (fun (u : 𝕊) ↦ exp (u • x))
    (ContinuousLinearMap.smulRight (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) (exp (t • x))) t
have h : ContinuousLinearMap.smulRight (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) (exp (t • x)) =
  HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x)
Tactic: convert! hasStrictFDerivAt_exp_smul_const_of_mem_ball 𝕂 _ _ htx using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exponential (goal)
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)
⊢ ContinuousLinearMap.smulRight (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) (exp (t • x)) =
    HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x)
have 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' : 𝔸)
Tactic: ext t'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exponential (goal)
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' : 𝕊
⊢ 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' : 𝔸)
have h : Commute (t' • x) (exp (t • x))
Tactic: change Commute (t' • x) (exp (t • x))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℝ
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (-x) * x ^ s) fun (x : ℝ) ↦ rexp (-(1 / 2) * x)
have refine_1 : ∀ (x : ℝ) (hx : rexp (-(1 / 2) * x) = 0), rexp (-x) * x ^ s = 0
Tactic: refine isLittleO_of_tendsto (fun x hx => ?_) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℝ
refine_1 : ∀ (x : ℝ) (hx : rexp (-(1 / 2) * x) = 0), rexp (-x) * x ^ s = 0
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (-x) * x ^ s) fun (x : ℝ) ↦ rexp (-(1 / 2) * x)
have refine_2 : Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (-x) * x ^ s / rexp (-(1 / 2) * x)) atTop (𝓝 0)
Tactic: refine isLittleO_of_tendsto (fun x hx => ?_) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s x : ℝ
hx : rexp (-(1 / 2) * x) = 0
⊢ rexp (-x) * x ^ s = 0
have refine_1 : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℝ
⊢ Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ rexp (-x) * x ^ s / rexp (-(1 / 2) * x))
    (fun (x : ℝ) ↦ rexp (1 / 2 * x) / x ^ s)⁻¹
have h : ∀ (x : ℝ), rexp (-x) * x ^ s / rexp (-(1 / 2) * x) = (fun (x : ℝ) ↦ rexp (1 / 2 * x) / x ^ s)⁻¹ x
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (hypothesis)
Goal:
s : ℝ
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (-x) * x ^ s / rexp (-(1 / 2) * x)) atTop (𝓝 0)
have this : 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
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 (-x) * x ^ s / rexp (-(1 / 2) * x)) atTop (𝓝 0)
have refine_2 : Tendsto (α := ℝ) (β := ℝ) (fun (x : ℝ) ↦ rexp (1 / 2 * x) / x ^ s)⁻¹ atTop (𝓝 0)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℝ
h : 0 < s
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) (Ioi 0) volume
have 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
Tactic: rw [← Ioc_union_Ioi_eq_Ioi (@zero_le_one ℝ _ _ _ _), integrableOn_union]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℝ
h : 0 < s
⊢ 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
have left : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) (Ioc 0 1) volume
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℝ
h : 0 < s
left :
  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)) (Ioc 0 1)
      volume ∧
    IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) (Ioi 1) volume
have right : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) (Ioi 1) volume
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℝ
h : 0 < s
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) (Ioc 0 1) volume
have left : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) (Icc 0 1) volume
Tactic: rw [← integrableOn_Icc_iff_integrableOn_Ioc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℝ
h : 0 < s
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) (Icc 0 1) volume
have left : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ (s - 1)) (Icc 0 1) volume
Tactic: refine IntegrableOn.continuousOn_mul continuousOn_id.neg.rexp ?_ isCompact_Icc
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℝ
h : 0 < s
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ (s - 1)) (Icc 0 1) volume
have left : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ (s - 1)) volume 0 1
Tactic: refine (intervalIntegrable_iff_integrableOn_Icc_of_le zero_le_one).mp ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℝ
h : 0 < s
⊢ -1 < s - 1
have linarith : s - 1 ≤ -1 → 0 - s + (s - 1 - -1) = 0
Tactic: linarith