x : ℝ
⊢ x ∈ Ioo (-(π / 2)) (π / 2) → x ∈ {x | cos x ≠ 0}
⊢ ContinuousOn tan (Ioo (-(π / 2)) (π / 2))
refine' ContinuousOn.mono continuousOn_tan fun x => _
x : ℝ
⊢ -(π / 2) < x → x < π / 2 → ¬cos x = 0
x : ℝ
⊢ x ∈ Ioo (-(π / 2)) (π / 2) → x ∈ {x | cos x ≠ 0}
simp only [and_imp, mem_Ioo, mem_setOf_eq, Ne.def]
x : ℝ
⊢ -(π / 2) < x → x < π / 2 → ¬∃ k, x = (2 * ↑k + 1) * π / 2
x : ℝ
⊢ -(π / 2) < x → x < π / 2 → ¬cos x = 0
rw [cos_eq_zero_iff]
case intro
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
⊢ False
x : ℝ
⊢ -(π / 2) < x → x < π / 2 → ¬∃ k, x = (2 * ↑k + 1) * π / 2
rintro hx_gt hx_lt ⟨r, hxr_eq⟩
case intro.inl
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : 0 ≤ r
⊢ False

case intro.inr
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
⊢ False
case intro
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
⊢ False
cases' le_or_lt 0 r with h h
case intro.inl
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : ¬x ≥ π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : 0 ≤ r
⊢ False
case intro.inl
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : 0 ≤ r
⊢ False
rw [lt_iff_not_ge] at hx_lt
case intro.inl
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : ¬x ≥ π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : 0 ≤ r
⊢ x ≥ π / 2
case intro.inl
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : ¬x ≥ π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : 0 ≤ r
⊢ False
refine' hx_lt _
case intro.inl
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : ¬x ≥ π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : 0 ≤ r
⊢ 1 ≤ 2 * ↑r + 1
case intro.inl
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : ¬x ≥ π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : 0 ≤ r
⊢ x ≥ π / 2
rw [hxr_eq, ← one_mul (π / 2), mul_div_assoc, ge_iff_le, mul_le_mul_right (half_pos pi_pos)]
no goals
case intro.inl
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : ¬x ≥ π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : 0 ≤ r
⊢ 1 ≤ 2 * ↑r + 1
simp [h]
case intro.inr
x : ℝ
hx_gt : ¬-(π / 2) ≥ x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
⊢ False
case intro.inr
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
⊢ False
rw [lt_iff_not_ge] at hx_gt
case intro.inr
x : ℝ
hx_gt : ¬-(π / 2) ≥ x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
⊢ -(π / 2) ≥ x
case intro.inr
x : ℝ
hx_gt : ¬-(π / 2) ≥ x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
⊢ False
refine' hx_gt _
case intro.inr
x : ℝ
hx_gt : ¬-(π / 2) ≥ x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
⊢ 2 * ↑r + 1 ≤ -1
case intro.inr
x : ℝ
hx_gt : ¬-(π / 2) ≥ x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
⊢ -(π / 2) ≥ x
rw [hxr_eq, ← one_mul (π / 2), mul_div_assoc, ge_iff_le, neg_mul_eq_neg_mul,
  mul_le_mul_right (half_pos pi_pos)]
case intro.inr
x : ℝ
hx_gt : ¬-(π / 2) ≥ x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
hr_le : r ≤ -1
⊢ 2 * ↑r + 1 ≤ -1
case intro.inr
x : ℝ
hx_gt : ¬-(π / 2) ≥ x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
⊢ 2 * ↑r + 1 ≤ -1
have hr_le : r ≤ -1 := by rwa [Int.lt_iff_add_one_le, ← le_neg_iff_add_nonpos_right] at h
case intro.inr
x : ℝ
hx_gt : ¬-(π / 2) ≥ x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
hr_le : r ≤ -1
⊢ ↑r ≤ (-1 - 1) / 2

case intro.inr
x : ℝ
hx_gt : ¬-(π / 2) ≥ x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
hr_le : r ≤ -1
⊢ 0 < 2
case intro.inr
x : ℝ
hx_gt : ¬-(π / 2) ≥ x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
hr_le : r ≤ -1
⊢ 2 * ↑r + 1 ≤ -1
rw [← le_sub_iff_add_le, mul_comm, ← le_div_iff]
no goals
x : ℝ
hx_gt : ¬-(π / 2) ≥ x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
⊢ r ≤ -1
rwa [Int.lt_iff_add_one_le, ← le_neg_iff_add_nonpos_right] at h
case intro.inr
x : ℝ
hx_gt : ¬-(π / 2) ≥ x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
hr_le : r ≤ -1
⊢ ↑r ≤ -1
case intro.inr
x : ℝ
hx_gt : ¬-(π / 2) ≥ x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
hr_le : r ≤ -1
⊢ ↑r ≤ (-1 - 1) / 2
norm_num
case intro.inr
x : ℝ
hx_gt : ¬-(π / 2) ≥ x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
hr_le : r ≤ -1
⊢ ↑r ≤ ↑(-1)
case intro.inr
x : ℝ
hx_gt : ¬-(π / 2) ≥ x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
hr_le : r ≤ -1
⊢ ↑r ≤ -1
rw [← Int.cast_one, ← Int.cast_neg]
no goals
case intro.inr
x : ℝ
hx_gt : ¬-(π / 2) ≥ x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
hr_le : r ≤ -1
⊢ ↑r ≤ ↑(-1)
norm_cast
no goals
case intro.inr
x : ℝ
hx_gt : ¬-(π / 2) ≥ x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
hr_le : r ≤ -1
⊢ 0 < 2
exact zero_lt_two