Theorem: Smt.Reconstruct.Arith.arithTransSineTangentPi (Smt/Reconstruct/Arith/TransFns/ArithTransSineTangentPi.lean)

State before:
pi : ℝ
⊢ ∀ (t : ℝ), (t > -pi → t.sin > -pi - t) ∧ (t < pi → t.sin < pi - t)
Tactic:
intro t
State after:
pi t : ℝ
⊢ (t > -pi → t.sin > -pi - t) ∧ (t < pi → t.sin < pi - t)

State before:
pi t : ℝ
⊢ (t > -pi → t.sin > -pi - t) ∧ (t < pi → t.sin < pi - t)
Tactic:
apply And.intro
State after:
case left
pi t : ℝ
⊢ t > -pi → t.sin > -pi - t

case right
pi t : ℝ
⊢ t < pi → t.sin < pi - t

State before:
case left
pi t : ℝ
⊢ t > -pi → t.sin > -pi - t
Tactic:
intro ht
State after:
case left
pi t : ℝ
ht : t > -pi
⊢ t.sin > -pi - t

State before:
case left
pi t : ℝ
ht : t > -pi
⊢ t.sin > -pi - t
Tactic:
admit
State after:
no goals

State before:
case right
pi t : ℝ
⊢ t < pi → t.sin < pi - t
Tactic:
intro ht
State after:
case right
pi t : ℝ
ht : t < pi
⊢ t.sin < pi - t

State before:
case right
pi t : ℝ
ht : t < pi
⊢ t.sin < pi - t
Tactic:
admit
State after:
no goals