Theorem: Smt.Reconstruct.Arith.arithTransExpSuperLin (Smt/Reconstruct/Arith/TransFns/ArithTransExpSuperLin.lean)

State before:
t : ℝ
⊢ t ≤ 0 ∨ t.exp > t + 1
Tactic:
apply orImplies
State after:
case a
t : ℝ
⊢ ¬t ≤ 0 → t.exp > t + 1

State before:
case a
t : ℝ
⊢ ¬t ≤ 0 → t.exp > t + 1
Tactic:
intro h
State after:
case a
t : ℝ
h : ¬t ≤ 0
⊢ t.exp > t + 1

State before:
case a
t : ℝ
h : ¬t ≤ 0
⊢ t.exp > t + 1
Tactic:
simp at h
State after:
case a
t : ℝ
h : 0 < t
⊢ t.exp > t + 1

State before:
case a
t : ℝ
h : 0 < t
⊢ t.exp > t + 1
Tactic:
exact arithTransExpSuperLin' t h
State after:
no goals