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

State before:
⊢ ∀ (l r : ℝ), l < r → UniqueDiffOn ℝ (Set.Icc l r)
Tactic:
intros l r h
State after:
l r : ℝ
h : l < r
⊢ UniqueDiffOn ℝ (Set.Icc l r)

State before:
l r : ℝ
h : l < r
⊢ UniqueDiffOn ℝ (Set.Icc l r)
Tactic:
refine uniqueDiffOn_Icc ?hab
State after:
case hab
l r : ℝ
h : l < r
⊢ l < r

State before:
case hab
l r : ℝ
h : l < r
⊢ l < r
Tactic:
exact h
State after:
no goals