-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean
theorem continuousOn_tan_Ioo : ContinuousOn tan (Ioo (-(π / 2)) (π / 2))

Proof state:
case intro
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
⊢ False

Tactic:
rcases le_or_lt 0 r with h | h

Result:
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

Proof state:
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

Tactic:
norm_num

Result:
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

Proof state:
case intro.inr
x : ℝ
hx_gt : ¬-(π / 2) ≥ x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
⊢ False

Tactic:
refine hx_gt ?_

Result:
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

Proof state:
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

Tactic:
exact zero_lt_two

Result:
no goals

Proof state:
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

Tactic:
rw [hxr_eq, ← one_mul (π / 2), mul_div_assoc, ge_iff_le, mul_le_mul_right (half_pos pi_pos)]

Result:
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

Proof state:
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)

Tactic:
norm_cast

Result:
no goals

Proof state:
case intro.inl
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : 0 ≤ r
⊢ False

Tactic:
rw [lt_iff_not_ge] at hx_lt

Result:
case intro.inl
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : ¬x ≥ π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : 0 ≤ r
⊢ False

Proof state:
x : ℝ
hx_gt : ¬-(π / 2) ≥ x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
⊢ r ≤ -1

Tactic:
rwa [Int.lt_iff_add_one_le, ← le_neg_iff_add_nonpos_right] at h

Result:
no goals

Proof state:
⊢ ContinuousOn tan (Ioo (-(π / 2)) (π / 2))

Tactic:
refine ContinuousOn.mono continuousOn_tan fun x => ?_

Result:
x : ℝ
⊢ x ∈ Ioo (-(π / 2)) (π / 2) → x ∈ {x | cos x ≠ 0}

Proof state:
x : ℝ
⊢ -(π / 2) < x → x < π / 2 → ¬∃ k, x = (2 * ↑k + 1) * π / 2

Tactic:
rintro hx_gt hx_lt ⟨r, hxr_eq⟩

Result:
case intro
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
⊢ False

Proof state:
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

Tactic:
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)]

Result:
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

Proof state:
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

Tactic:
rw [← Int.cast_one, ← Int.cast_neg]

Result:
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)

Proof state:
case intro.inr
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
⊢ False

Tactic:
rw [lt_iff_not_ge] at hx_gt

Result:
case intro.inr
x : ℝ
hx_gt : ¬-(π / 2) ≥ x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
⊢ False

Proof state:
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

Tactic:
rw [← le_sub_iff_add_le, mul_comm, ← le_div_iff₀]

Result:
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

Proof state:
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

Tactic:
simp [h]

Result:
no goals

Proof state:
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

Tactic:
have hr_le : r ≤ -1 := by rwa [Int.lt_iff_add_one_le, ← le_neg_iff_add_nonpos_right] at h

Result:
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

Proof state:
x : ℝ
⊢ -(π / 2) < x → x < π / 2 → ¬cos x = 0

Tactic:
rw [cos_eq_zero_iff]

Result:
x : ℝ
⊢ -(π / 2) < x → x < π / 2 → ¬∃ k, x = (2 * ↑k + 1) * π / 2

Proof state:
case intro.inl
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : ¬x ≥ π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : 0 ≤ r
⊢ False

Tactic:
refine hx_lt ?_

Result:
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

Proof state:
x : ℝ
⊢ x ∈ Ioo (-(π / 2)) (π / 2) → x ∈ {x | cos x ≠ 0}

Tactic:
simp only [and_imp, mem_Ioo, mem_setOf_eq, Ne]

Result:
x : ℝ
⊢ -(π / 2) < x → x < π / 2 → ¬cos x = 0