Theorem: Smt.Reconstruct.Arith.exp_DiffOn (Smt/Reconstruct/Arith/TransFns/ArithTransExpApproxAboveNeg.lean)

State before:
⊢ ∀ (d : ℕ) (l r : ℝ), l < r → DifferentiableOn ℝ (iteratedDerivWithin d Real.exp (Set.Icc l r)) (Set.Ioo l r)
Tactic:
intros d l r h
State after:
d : ℕ
l r : ℝ
h : l < r
⊢ DifferentiableOn ℝ (iteratedDerivWithin d Real.exp (Set.Icc l r)) (Set.Ioo l r)

State before:
d : ℕ
l r : ℝ
h : l < r
⊢ DifferentiableOn ℝ (iteratedDerivWithin d Real.exp (Set.Icc l r)) (Set.Ioo l r)
Tactic:
have d_lt_succ_d := Nat.lt.base d
State after:
d : ℕ
l r : ℝ
h : l < r
d_lt_succ_d : d < d.succ
⊢ DifferentiableOn ℝ (iteratedDerivWithin d Real.exp (Set.Icc l r)) (Set.Ioo l r)

State before:
d : ℕ
l r : ℝ
h : l < r
d_lt_succ_d : d < d.succ
⊢ DifferentiableOn ℝ (iteratedDerivWithin d Real.exp (Set.Icc l r)) (Set.Ioo l r)
Tactic:
have h' := ContDiffOn.differentiableOn_iteratedDerivWithin (m := d) (n := d + 1) (t1 (d + 1) l r) (StrictMono.imp Nat.strictMono_cast d_lt_succ_d) (t2 l r h)
State after:
d : ℕ
l r : ℝ
h : l < r
d_lt_succ_d : d < d.succ
h' : DifferentiableOn ℝ (iteratedDerivWithin d Real.exp (Set.Icc l r)) (Set.Icc l r)
⊢ DifferentiableOn ℝ (iteratedDerivWithin d Real.exp (Set.Icc l r)) (Set.Ioo l r)

State before:
d : ℕ
l r : ℝ
h : l < r
d_lt_succ_d : d < d.succ
h' : DifferentiableOn ℝ (iteratedDerivWithin d Real.exp (Set.Icc l r)) (Set.Icc l r)
⊢ DifferentiableOn ℝ (iteratedDerivWithin d Real.exp (Set.Icc l r)) (Set.Ioo l r)
Tactic:
have o : Set.Ioo l r ⊆ Set.Icc l r := Set.Ioo_subset_Icc_self
State after:
d : ℕ
l r : ℝ
h : l < r
d_lt_succ_d : d < d.succ
h' : DifferentiableOn ℝ (iteratedDerivWithin d Real.exp (Set.Icc l r)) (Set.Icc l r)
o : Set.Ioo l r ⊆ Set.Icc l r
⊢ DifferentiableOn ℝ (iteratedDerivWithin d Real.exp (Set.Icc l r)) (Set.Ioo l r)

State before:
d : ℕ
l r : ℝ
h : l < r
d_lt_succ_d : d < d.succ
h' : DifferentiableOn ℝ (iteratedDerivWithin d Real.exp (Set.Icc l r)) (Set.Icc l r)
o : Set.Ioo l r ⊆ Set.Icc l r
⊢ DifferentiableOn ℝ (iteratedDerivWithin d Real.exp (Set.Icc l r)) (Set.Ioo l r)
Tactic:
exact DifferentiableOn.mono h' o
State after:
no goals