Theorem: Smt.Reconstruct.Arith.arithTransSineBounds (Smt/Reconstruct/Arith/TransFns/ArithTransSineTangentZero.lean)

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

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

case right
t : ℝ
⊢ t < 0 → t.sin > t

State before:
case left
t : ℝ
⊢ t > 0 → t.sin < t
Tactic:
exact sin_lt
State after:
no goals

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

State before:
case right
t : ℝ
ht : t < 0
⊢ t.sin > t
Tactic:
rw [sin_neg']
State after:
case right
t : ℝ
ht : t < 0
⊢ -(-t).sin > t

State before:
case right
t : ℝ
ht : t < 0
⊢ -(-t).sin > t
Tactic:
apply lt_neg.mpr
State after:
case right
t : ℝ
ht : t < 0
⊢ (-t).sin < -t

State before:
case right
t : ℝ
ht : t < 0
⊢ (-t).sin < -t
Tactic:
apply sin_lt
State after:
case right.h
t : ℝ
ht : t < 0
⊢ 0 < -t

State before:
case right.h
t : ℝ
ht : t < 0
⊢ 0 < -t
Tactic:
linarith
State after:
no goals