Theorem: Usa1998P3.lemma0 (Compfiles/Usa1998P3.lean)

State before:
⊢ Set.Icc (-Real.pi / 4) (Real.pi / 4) ⊆ Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)
Tactic:
intro a ha
State after:
a : ℝ
ha : a ∈ Set.Icc (-Real.pi / 4) (Real.pi / 4)
⊢ a ∈ Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)

State before:
a : ℝ
ha : a ∈ Set.Icc (-Real.pi / 4) (Real.pi / 4)
⊢ a ∈ Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)
Tactic:
exact ⟨by linarith[ha.1, Real.pi_pos], by linarith[ha.2, Real.pi_pos]⟩
State after:
no goals

State before:
a : ℝ
ha : a ∈ Set.Icc (-Real.pi / 4) (Real.pi / 4)
⊢ -(Real.pi / 2) < a
Tactic:
linarith[ha.1, Real.pi_pos]
State after:
no goals

State before:
a : ℝ
ha : a ∈ Set.Icc (-Real.pi / 4) (Real.pi / 4)
⊢ a < Real.pi / 2
Tactic:
linarith[ha.2, Real.pi_pos]
State after:
no goals