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

State before:
⊢ ∀ (d : ℕ) (l r : ℝ), ContDiffOn ℝ (↑d) Real.exp (Set.Icc l r)
Tactic:
intros d l r
State after:
d : ℕ
l r : ℝ
⊢ ContDiffOn ℝ (↑d) Real.exp (Set.Icc l r)

State before:
d : ℕ
l r : ℝ
⊢ ContDiffOn ℝ (↑d) Real.exp (Set.Icc l r)
Tactic:
apply ContDiff.contDiffOn
State after:
case h
d : ℕ
l r : ℝ
⊢ ContDiff ℝ (↑d) Real.exp

State before:
case h
d : ℕ
l r : ℝ
⊢ ContDiff ℝ (↑d) Real.exp
Tactic:
exact Real.contDiff_exp
State after:
no goals