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

State before:
⊢ ∀ (t : ℝ), t.sin ≤ 1 ∧ t.sin ≥ -1
Tactic:
intro t
State after:
t : ℝ
⊢ t.sin ≤ 1 ∧ t.sin ≥ -1

State before:
t : ℝ
⊢ t.sin ≤ 1 ∧ t.sin ≥ -1
Tactic:
apply And.intro
State after:
case left
t : ℝ
⊢ t.sin ≤ 1

case right
t : ℝ
⊢ t.sin ≥ -1

State before:
case left
t : ℝ
⊢ t.sin ≤ 1
Tactic:
exact sin_le_one t
State after:
no goals

State before:
case right
t : ℝ
⊢ t.sin ≥ -1
Tactic:
exact neg_one_le_sin t
State after:
no goals