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

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

State before:
n : ℕ
l r : ℝ
⊢ ContDiffOn ℝ (↑n) Real.exp (Set.Icc l r)
Tactic:
exact exp_contDiffOn n l r
State after:
no goals