awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
⊢ 1 - z * I ≠ 0

Tactic:
have z₂ : 1 - z * I ≠ 0 := by
    contrapose h₂
    rw [sub_eq_zero, ← div_eq_iff I_ne_zero, div_I, one_mul] at h₂
    exact h₂.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
z₂ : 1 - z * I ≠ 0
⊢ 2 * (I * (-I / 2)) = 1

Tactic:
simp [field]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
z₂ : 1 - z * I ≠ 0
rw : (1 + z * I) / (1 - z * I) ≠ 0
⊢ cexp (2 * (z.arctan * I)) = (1 + z * I) / (1 - z * I)

Tactic:
rw [arctan, ← mul_rotate, ← mul_assoc,
      show 2 * (I * (-I / 2)) = 1 by simp [field], one_mul, exp_log]

Premises used: mul_assoc, Complex.arctan, Complex.exp_log, one_mul, mul_rotate
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
z₂ : 1 - z * I ≠ 0
⊢ (1 + z * I) / (1 - z * I) ≠ 0

Tactic:
div_ne_zero z₁ z₂

Premises used: div_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
z₂ : 1 - z * I ≠ 0
⊢ (1 + z * I) / (1 - z * I) ≠ 0

Tactic:
exact div_ne_zero z₁ z₂

Premises used: div_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
z₂ : 1 - z * I ≠ 0
⊢ cexp (2 * (z.arctan * I)) = (1 + z * I) / (1 - z * I)

Tactic:
have key : exp (2 * (arctan z * I)) = (1 + z * I) / (1 - z * I) := by
    rw [arctan, ← mul_rotate, ← mul_assoc,
      show 2 * (I * (-I / 2)) = 1 by simp [field], one_mul, exp_log]
    · exact div_ne_zero z₁ z₂
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
z₂ : 1 - z * I ≠ 0
key : cexp (2 * (z.arctan * I)) = (1 + z * I) / (1 - z * I)
⊢ (1 - z * I - (1 + z * I)) / (1 + z * I + (1 - z * I)) * I = -(I * I) * z

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
z₂ : 1 - z * I ≠ 0
key : cexp (2 * (z.arctan * I)) = (1 + z * I) / (1 - z * I)
rw : (1 - (1 + z * I) / (1 - z * I)) / ((1 + z * I) / (1 - z * I) + 1) * I = z
rw₁ : (1 - (1 + z * I) / (1 - z * I)) * (1 - z * I) / (((1 + z * I) / (1 - z * I) + 1) * (1 - z * I)) * I = z
rw₂ :
  (1 * (1 - z * I) - (1 + z * I) / (1 - z * I) * (1 - z * I)) / (((1 + z * I) / (1 - z * I) + 1) * (1 - z * I)) * I = z
rw₃ :
  (1 * (1 - z * I) - (1 + z * I) / (1 - z * I) * (1 - z * I)) /
        ((1 + z * I) / (1 - z * I) * (1 - z * I) + 1 * (1 - z * I)) *
      I =
    z
rw₄ : (1 * (1 - z * I) - (1 + z * I)) / (1 + z * I + 1 * (1 - z * I)) * I = z
rw₅ : (1 - z * I - (1 + z * I)) / (1 + z * I + (1 - z * I)) * I = z
rw₆ : -(I * I) * z = z
rw₇ : - -1 * z = z
rw₈ : 1 * z = z
rw₉ rw₁₀ : z = z
⊢ (1 - cexp (2 * (z.arctan * I))) / (cexp (2 * (z.arctan * I)) + 1) * I = z

Tactic:
rw [key, ← mul_div_mul_right _ _ z₂, sub_mul, add_mul, div_mul_cancel₀ _ z₂, one_mul,
    show _ / _ * I = -(I * I) * z by ring, I_mul_I, neg_neg, one_mul]

Premises used: add_mul, mul_div_mul_right, div_mul_cancel₀, neg_neg, sub_mul, Complex.I_mul_I, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₀ : z ≠ (↑π : ℂ) / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
⊢ cos z ≠ 0

Tactic:
cos_ne_zero_iff.mpr (fun k ↦ ?_)

Premises used: Iff.mpr, Complex.cos_ne_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₀ : z ≠ (↑π : ℂ) / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
refine : ∀ (k : ℤ), z ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2
⊢ cos z ≠ 0

Tactic:
refine cos_ne_zero_iff.mpr (fun k ↦ ?_)

Premises used: Iff.mpr, Complex.cos_ne_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₀ : z ≠ (↑π : ℂ) / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
k : ℤ
rw :
  ∀ (h₀ : ¬z.re = ((↑π : ℂ) / 2).re ∨ ¬z.im = ((↑π : ℂ) / 2).im) (h₁ : -(π / 2) < z.re) (h₂ : z.re ≤ π / 2) (k : ℤ),
    ¬z.re = ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2).re ∨
      ¬z.im = ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2).im
⊢ z ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2

Tactic:
rw [ne_eq, Complex.ext_iff, not_and_or] at h₀ ⊢

Premises used: Complex.ext_iff, ne_eq, not_and_or
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₀ : ¬z.re = ((↑π : ℂ) / 2).re ∨ ¬z.im = ((↑π : ℂ) / 2).im
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
k : ℤ
norm_cast : ∀ (h₀ : ¬z.re = π / 2 ∨ ¬z.im = 0), ¬z.re = (↑(2 * k + 1) : ℝ) * π / 2 ∨ ¬z.im = 0
⊢ ¬z.re = ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2).re ∨
    ¬z.im = ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2).im

Tactic:
norm_cast at h₀ ⊢
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
k : ℤ
h₀ : ¬z.re = π / 2 ∨ ¬z.im = 0
inl : ∀ (nr : ¬z.re = π / 2), ¬z.re = (↑(2 * k + 1) : ℝ) * π / 2 ∨ ¬z.im = 0
inr : ∀ (ni : ¬z.im = 0), ¬z.re = (↑(2 * k + 1) : ℝ) * π / 2 ∨ ¬z.im = 0
⊢ ¬z.re = (↑(2 * k + 1) : ℝ) * π / 2 ∨ ¬z.im = 0

Tactic:
rcases h₀ with nr | ni
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
k : ℤ
nr : ¬z.re = π / 2
inl : ¬z.re = (↑(2 * k + 1) : ℝ) * π / 2
⊢ ¬z.re = (↑(2 * k + 1) : ℝ) * π / 2 ∨ ¬z.im = 0

Tactic:
left
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
k : ℤ
nr : ¬z.re = π / 2
inl : ∀ (nr : z.re = (↑(2 * k + 1) : ℝ) * π / 2), z.re = π / 2
⊢ ¬z.re = (↑(2 * k + 1) : ℝ) * π / 2

Tactic:
contrapose nr
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₂ : z.re ≤ π / 2
k : ℤ
h₁ : -1 * (π / 2) < (↑(2 * k + 1) : ℝ) * (π / 2)
nr : z.re = (↑(2 * k + 1) : ℝ) * π / 2
⊢ 0 < π / 2

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
k : ℤ
nr : z.re = (↑(2 * k + 1) : ℝ) * π / 2
⊢ LT.lt (α := ℝ) (-1) (↑(2 * k + 1) : ℝ)

Tactic:
rw [nr, mul_div_assoc, neg_eq_neg_one_mul, mul_lt_mul_iff_of_pos_right (by positivity)] at h₁

Premises used: mul_div_assoc, mul_lt_mul_iff_of_pos_right, neg_eq_neg_one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
k : ℤ
nr : z.re = (↑(2 * k + 1) : ℝ) * π / 2
h₃ : LT.lt (α := ℝ) (-1) (↑(2 * k + 1) : ℝ)
⊢ z.re = (↑(2 * k + 1) : ℝ) * π / 2

Tactic:
rw [nr, mul_div_assoc, neg_eq_neg_one_mul, mul_lt_mul_iff_of_pos_right (by positivity)] at h₁

Premises used: mul_div_assoc, mul_lt_mul_iff_of_pos_right, neg_eq_neg_one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
k : ℤ
h₂ : (↑(2 * k + 1) : ℝ) * (π / 2) ≤ 1 * (π / 2)
h₁ : LT.lt (α := ℝ) (-1) (↑(2 * k + 1) : ℝ)
nr : z.re = (↑(2 * k + 1) : ℝ) * π / 2
⊢ 0 < π / 2

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₂ : z.re ≤ π / 2
k : ℤ
h₁ : LT.lt (α := ℝ) (-1) (↑(2 * k + 1) : ℝ)
nr : z.re = (↑(2 * k + 1) : ℝ) * π / 2
⊢ LE.le (α := ℝ) (↑(2 * k + 1) : ℝ) 1

Tactic:
rw [nr, ← one_mul (π / 2), mul_div_assoc, mul_le_mul_iff_of_pos_right (by positivity)] at h₂

Premises used: Real.pi, mul_le_mul_iff_of_pos_right, mul_div_assoc, HDiv.hDiv, OfNat.ofNat, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₂ : z.re ≤ π / 2
k : ℤ
h₁ : LT.lt (α := ℝ) (-1) (↑(2 * k + 1) : ℝ)
nr : z.re = (↑(2 * k + 1) : ℝ) * π / 2
h₃ : LE.le (α := ℝ) (↑(2 * k + 1) : ℝ) 1
⊢ LT.lt (α := ℝ) (-1) (↑(2 * k + 1) : ℝ)

Tactic:
rw [nr, ← one_mul (π / 2), mul_div_assoc, mul_le_mul_iff_of_pos_right (by positivity)] at h₂

Premises used: Real.pi, mul_le_mul_iff_of_pos_right, mul_div_assoc, HDiv.hDiv, OfNat.ofNat, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₂ : z.re ≤ π / 2
k : ℤ
h₁ : LT.lt (α := ℝ) (-1) (↑(2 * k + 1) : ℝ)
nr : z.re = (↑(2 * k + 1) : ℝ) * π / 2
h₃ : LE.le (α := ℝ) (↑(2 * k + 1) : ℝ) 1
h₄ : LT.lt (α := ℝ) (-1) (↑(2 * k + 1) : ℝ)
⊢ z.re = (↑(2 * k + 1) : ℝ) * π / 2

Tactic:
rw [nr, ← one_mul (π / 2), mul_div_assoc, mul_le_mul_iff_of_pos_right (by positivity)] at h₂

Premises used: Real.pi, mul_le_mul_iff_of_pos_right, mul_div_assoc, HDiv.hDiv, OfNat.ofNat, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
k : ℤ
h₂ : LE.le (α := ℝ) (↑(2 * k + 1) : ℝ) 1
h₁ : LT.lt (α := ℝ) (-1) (↑(2 * k + 1) : ℝ)
nr : z.re = (↑(2 * k + 1) : ℝ) * π / 2
⊢ Int.negSucc 0 < 2 * k + 1

Tactic:
norm_cast at h₁ h₂
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
k : ℤ
h₂ : LE.le (α := ℝ) (↑(2 * k + 1) : ℝ) 1
h₁ : LT.lt (α := ℝ) (-1) (↑(2 * k + 1) : ℝ)
nr : z.re = (↑(2 * k + 1) : ℝ) * π / 2
h₃ : Int.negSucc 0 < 2 * k + 1
⊢ 2 * k + 1 ≤ 1

Tactic:
norm_cast at h₁ h₂
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
k : ℤ
nr : z.re = (↑(2 * k + 1) : ℝ) * π / 2
h₁ : Int.negSucc 0 < 2 * k + 1
h₂ : 2 * k + 1 ≤ 1
⊢ -1 < 2 * k + 1

Tactic:
change -1 < _ at h₁
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
k : ℤ
nr : z.re = (↑(2 * k + 1) : ℝ) * π / 2
h₂ : 2 * k + 1 ≤ 1
h₁ : -1 < 2 * k + 1
⊢ 2 * k + 1 = 1

Tactic:
lia
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
k : ℤ
nr : z.re = (↑(2 * k + 1) : ℝ) * π / 2
h₂ : 2 * k + 1 ≤ 1
h₁ : -1 < 2 * k + 1
inl : ∀ (nr : z.re = (↑1 : ℝ) * π / 2) (h₂ : 2 * k + 1 ≤ 1) (h₁ : -1 < 2 * k + 1), z.re = π / 2
inl₁ : ∀ (nr : z.re = 1 * π / 2) (h₂ : 2 * k + 1 ≤ 1) (h₁ : -1 < 2 * k + 1), z.re = π / 2
inl₂ inl₃ inl₄ inl₅ : ∀ (nr : z.re = π / 2) (h₂ : 2 * k + 1 ≤ 1) (h₁ : -1 < 2 * k + 1), z.re = π / 2
⊢ z.re = π / 2

Tactic:
rwa [show 2 * k + 1 = 1 by lia, Int.cast_one, one_mul] at nr

Premises used: one_mul, Int.cast_one
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
k : ℤ
ni : ¬z.im = 0
⊢ ¬z.re = (↑(2 * k + 1) : ℝ) * π / 2 ∨ ¬z.im = 0

Tactic:
Or.inr ni

Premises used: Or.inr
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
k : ℤ
ni : ¬z.im = 0
⊢ ¬z.re = (↑(2 * k + 1) : ℝ) * π / 2 ∨ ¬z.im = 0

Tactic:
exact Or.inr ni

Premises used: Or.inr
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₀ : z ≠ (↑π : ℂ) / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
⊢ cos z ≠ 0

Tactic:
have h := cos_ne_zero_of_arctan_bounds h₀ h₁ h₂
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₀ : z ≠ (↑π : ℂ) / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
rw : -I / 2 * log ((cos z + sin z * I) / (cos z - sin z * I)) = z
⊢ -I / 2 * log ((1 + sin z / cos z * I) / (1 - sin z / cos z * I)) = z

Tactic:
rw [← mul_div_mul_right (1 + _) _ h, add_mul, sub_mul, one_mul, ← mul_rotate, mul_div_cancel₀ _ h]

Premises used: add_mul, mul_div_mul_right, mul_div_cancel₀, sub_mul, HAdd.hAdd, OfNat.ofNat, one_mul, mul_rotate
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₀ : z ≠ (↑π : ℂ) / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
enter : cos z - sin z * I
| -I / 2 * log ((cos z + sin z * I) / (cos z - sin z * I))

Tactic:
enter [2, 1, 2]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₀ : z ≠ (↑π : ℂ) / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
rw : cos (-z) + sin (-z) * I
| cos z - sin z * I

Tactic:
rw [sub_eq_add_neg, ← neg_mul, ← sin_neg, ← cos_neg]

Premises used: sub_eq_add_neg, Complex.cos_neg, Complex.sin_neg, neg_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₀ : z ≠ (↑π : ℂ) / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
enter : cos (-z) + sin (-z) * I
| -I / 2 * log ((cos z + sin z * I) / (cos z - sin z * I))

Tactic:
enter [2, 1, 2]
    rw [sub_eq_add_neg, ← neg_mul, ← sin_neg, ← cos_neg]

Premises used: sub_eq_add_neg, Complex.cos_neg, Complex.sin_neg, neg_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₀ : z ≠ (↑π : ℂ) / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
conv_lhs : -I / 2 * log ((cos z + sin z * I) / (cos (-z) + sin (-z) * I)) = z
⊢ -I / 2 * log ((cos z + sin z * I) / (cos z - sin z * I)) = z

Tactic:
conv_lhs =>
    enter [2, 1, 2]
    rw [sub_eq_add_neg, ← neg_mul, ← sin_neg, ← cos_neg]

Premises used: sub_eq_add_neg, Complex.cos_neg, Complex.sin_neg, neg_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₀ : z ≠ (↑π : ℂ) / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ z * I - -z * I = 2 * (I * z)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₀ : z ≠ (↑π : ℂ) / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ -I / 2 * (2 * (I * z)) = -(I * I) * z

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₀ : z ≠ (↑π : ℂ) / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
hx₁ : -π < (2 * (I * z)).im
hx₂ : (2 * (I * z)).im ≤ π
⊢ -I / 2 * log ((cos z + sin z * I) / (cos (-z) + sin (-z) * I)) = z

Tactic:
rw [← exp_mul_I, ← exp_mul_I, ← exp_sub, show z * I - -z * I = 2 * (I * z) by ring, log_exp,
    show -I / 2 * (2 * (I * z)) = -(I * I) * z by ring, I_mul_I, neg_neg, one_mul]

Premises used: neg_neg, Complex.log_exp, Complex.I_mul_I, Complex.exp_sub, Complex.exp_mul_I, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₀ : z ≠ (↑π : ℂ) / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
hx₁ : -π < 2 * z.re
⊢ -π < (2 * (I * z)).im

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₀ : z ≠ (↑π : ℂ) / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
hx₂ : 2 * z.re ≤ π
⊢ (2 * (I * z)).im ≤ π

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₀ : z ≠ (↑π : ℂ) / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
hx₁ : -π / 2 < z.re
hx₂ hx₃ hx₄ hx₅ : -(π / 2) < z.re
⊢ -π < 2 * z.re

Tactic:
rwa [← div_lt_iff₀' two_pos, neg_div]

Premises used: neg_div, div_lt_iff₀'
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₀ : z ≠ (↑π : ℂ) / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
hx₂ hx₃ hx₄ hx₅ : z.re ≤ π / 2
⊢ 2 * z.re ≤ π

Tactic:
rwa [← le_div_iff₀' two_pos]

Premises used: le_div_iff₀'
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
x : ℝ
rw : (↑(Real.tan (Real.arctan x)) : ℂ).arctan
| (↑x : ℂ).arctan

Tactic:
rw [← Real.tan_arctan x]

Premises used: Real.tan_arctan
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
x : ℝ
conv_rhs : (↑(Real.arctan x) : ℂ) = (↑(Real.tan (Real.arctan x)) : ℂ).arctan
⊢ (↑(Real.arctan x) : ℂ) = (↑x : ℂ).arctan

Tactic:
conv_rhs => rw [← Real.tan_arctan x]

Premises used: Real.tan_arctan
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
x : ℝ
h₀ : (↑(Real.arctan x) : ℂ) ≠ (↑π : ℂ) / 2
h₁ : -(π / 2) < (↑(Real.arctan x) : ℂ).re
h₂ : (↑(Real.arctan x) : ℂ).re ≤ π / 2
⊢ (↑(Real.arctan x) : ℂ) = (↑(Real.tan (Real.arctan x)) : ℂ).arctan

Tactic:
rw [ofReal_tan, arctan_tan]

Premises used: Complex.arctan_tan, Complex.ofReal_tan
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
x : ℝ
h₀ : ¬Real.arctan x = π / 2
⊢ (↑(Real.arctan x) : ℂ) ≠ (↑π : ℂ) / 2

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
x : ℝ
⊢ Real.arctan x ≠ π / 2

Tactic:
(Real.arctan_lt_pi_div_two _).ne

Premises used: Real.arctan_lt_pi_div_two, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
x : ℝ
⊢ Real.arctan x ≠ π / 2

Tactic:
exact (Real.arctan_lt_pi_div_two _).ne

Premises used: Real.arctan_lt_pi_div_two, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
x : ℝ
⊢ -(π / 2) < Real.arctan x

Tactic:
Real.neg_pi_div_two_lt_arctan _

Premises used: Real.neg_pi_div_two_lt_arctan
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
x : ℝ
⊢ -(π / 2) < Real.arctan x

Tactic:
exact Real.neg_pi_div_two_lt_arctan _

Premises used: Real.neg_pi_div_two_lt_arctan
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
x : ℝ
⊢ Real.arctan x ≤ π / 2

Tactic:
(Real.arctan_lt_pi_div_two _).le

Premises used: LT.lt.le, Real.arctan_lt_pi_div_two
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
x : ℝ
⊢ Real.arctan x ≤ π / 2

Tactic:
exact (Real.arctan_lt_pi_div_two _).le

Premises used: LT.lt.le, Real.arctan_lt_pi_div_two
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
hz : ‖z‖ < 1
rw : -1 < z.re ∨ 1 + z = 0
⊢ (1 + z).arg ∈ Set.Ioo (-(π / 2)) (π / 2)

Tactic:
rw [Set.mem_Ioo, ← abs_lt, abs_arg_lt_pi_div_two_iff, add_re, one_re, ← neg_lt_iff_pos_add']

Premises used: Set.mem_Ioo, Complex.add_re, neg_lt_iff_pos_add', Complex.abs_arg_lt_pi_div_two_iff, abs_lt, Complex.one_re
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
hz : ‖z‖ < 1
⊢ -1 < z.re ∨ 1 + z = 0

Tactic:
Or.inl (abs_lt.mp ((abs_re_le_norm z).trans_lt hz)).1

Premises used: Complex.abs_re_le_norm, And.left, Iff.mp, abs_lt, Or.inl, LE.le.trans_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
hz : ‖z‖ < 1
⊢ -1 < z.re ∨ 1 + z = 0

Tactic:
exact Or.inl (abs_lt.mp ((abs_re_le_norm z).trans_lt hz)).1

Premises used: Complex.abs_re_le_norm, And.left, Iff.mp, abs_lt, Or.inl, LE.le.trans_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
hz : ‖z‖ < 1
⊢ ‖z * I‖ < 1

Tactic:
simpa
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
hz : ‖z‖ < 1
⊢ (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0

Tactic:
have z₁ := mem_slitPlane_iff_arg.mp (mem_slitPlane_of_norm_lt_one (z := z * I) (by simpa))
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
hz : ‖z‖ < 1
z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0
⊢ ‖-(z * I)‖ < 1

Tactic:
simpa
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
hz : ‖z‖ < 1
z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0
⊢ (1 + -(z * I)).arg ≠ π ∧ 1 + -(z * I) ≠ 0

Tactic:
have z₂ := mem_slitPlane_iff_arg.mp (mem_slitPlane_of_norm_lt_one (z := -(z * I)) (by simpa))
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
hz : ‖z‖ < 1
z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0
z₂ : (1 + -(z * I)).arg ≠ π ∧ 1 + -(z * I) ≠ 0
⊢ (1 - z * I).arg ≠ π ∧ 1 - z * I ≠ 0

Tactic:
rw [← sub_eq_add_neg] at z₂

Premises used: sub_eq_add_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
hz : ‖z‖ < 1
z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0
z₂ : (1 - z * I).arg ≠ π ∧ 1 - z * I ≠ 0
rw : (1 + z * I).arg + (1 - z * I)⁻¹.arg ∈ Set.Ioc (-π) π
⊢ log (1 + z * I) + -log (1 - z * I) = log ((1 + z * I) / (1 - z * I))

Tactic:
rw [← log_inv _ z₂.1, ← (log_mul_eq_add_log_iff z₁.2 (inv_eq_zero.ne.mpr z₂.2)).mpr,
    div_eq_mul_inv]

Premises used: Iff.mpr, inv_eq_zero, Complex.log_inv, Complex.log_mul_eq_add_log_iff, div_eq_mul_inv, And.right, And.left, Iff.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
hz : ‖z‖ < 1
z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0
z₂ : (1 - z * I).arg ≠ π ∧ 1 - z * I ≠ 0
⊢ ‖z * I‖ < 1

Tactic:
simpa
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
hz : ‖z‖ < 1
z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0
z₂ : (1 - z * I).arg ≠ π ∧ 1 - z * I ≠ 0
⊢ (1 + z * I).arg ∈ Set.Ioo (-(π / 2)) (π / 2)

Tactic:
have b₁ := arg_one_add_mem_Ioo (z := z * I) (by simpa)
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
hz : ‖z‖ < 1
z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0
z₂ : (1 - z * I).arg ≠ π ∧ 1 - z * I ≠ 0
b₁ : (1 + z * I).arg ∈ Set.Ioo (-(π / 2)) (π / 2)
simp_rw : (1 + -(z * I)).arg ∈ Set.Ioo (-(π / 2)) (π / 2)
⊢ (1 - z * I)⁻¹.arg ∈ Set.Ioo (-(π / 2)) (π / 2)

Tactic:
simp_rw [arg_inv, z₂.1, ite_false, Set.neg_mem_Ioo_iff, neg_neg, sub_eq_add_neg]

Premises used: ite_false, sub_eq_add_neg, Set.neg_mem_Ioo_iff, neg_neg, And.left, Complex.arg_inv
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
hz : ‖z‖ < 1
z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0
z₂ : (1 - z * I).arg ≠ π ∧ 1 - z * I ≠ 0
b₁ : (1 + z * I).arg ∈ Set.Ioo (-(π / 2)) (π / 2)
⊢ ‖-(z * I)‖ < 1

Tactic:
simpa
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
hz : ‖z‖ < 1
z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0
z₂ : (1 - z * I).arg ≠ π ∧ 1 - z * I ≠ 0
b₁ : (1 + z * I).arg ∈ Set.Ioo (-(π / 2)) (π / 2)
⊢ (1 + -(z * I)).arg ∈ Set.Ioo (-(π / 2)) (π / 2)

Tactic:
exact arg_one_add_mem_Ioo (by simpa)

Premises used: Complex.arg_one_add_mem_Ioo
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
hz : ‖z‖ < 1
z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0
z₂ : (1 - z * I).arg ≠ π ∧ 1 - z * I ≠ 0
b₁ : (1 + z * I).arg ∈ Set.Ioo (-(π / 2)) (π / 2)
⊢ (1 - z * I)⁻¹.arg ∈ Set.Ioo (-(π / 2)) (π / 2)

Tactic:
have b₂ : arg (1 - z * I)⁻¹ ∈ Set.Ioo (-(π / 2)) (π / 2) := by
    simp_rw [arg_inv, z₂.1, ite_false, Set.neg_mem_Ioo_iff, neg_neg, sub_eq_add_neg]
    exact arg_one_add_mem_Ioo (by simpa)
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
hz : ‖z‖ < 1
z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0
z₂ : (1 - z * I).arg ≠ π ∧ 1 - z * I ≠ 0
b₁ : (1 + z * I).arg ∈ Set.Ioo (-(π / 2)) (π / 2)
b₂ : (1 - z * I)⁻¹.arg ∈ Set.Ioo (-(π / 2)) (π / 2)
⊢ -(π / 2) + -(π / 2) < (1 + z * I).arg + (1 - z * I)⁻¹.arg

Tactic:
have c₁ := add_lt_add b₁.1 b₂.1
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
hz : ‖z‖ < 1
z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0
z₂ : (1 - z * I).arg ≠ π ∧ 1 - z * I ≠ 0
b₁ : (1 + z * I).arg ∈ Set.Ioo (-(π / 2)) (π / 2)
b₂ : (1 - z * I)⁻¹.arg ∈ Set.Ioo (-(π / 2)) (π / 2)
c₁ : -(π / 2) + -(π / 2) < (1 + z * I).arg + (1 - z * I)⁻¹.arg
⊢ (1 + z * I).arg + (1 - z * I)⁻¹.arg < π / 2 + π / 2

Tactic:
have c₂ := add_lt_add b₁.2 b₂.2
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
hz : ‖z‖ < 1
z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0
z₂ : (1 - z * I).arg ≠ π ∧ 1 - z * I ≠ 0
b₁ : (1 + z * I).arg ∈ Set.Ioo (-(π / 2)) (π / 2)
b₂ : (1 - z * I)⁻¹.arg ∈ Set.Ioo (-(π / 2)) (π / 2)
c₁ : -(π / 2) + -(π / 2) < (1 + z * I).arg + (1 - z * I)⁻¹.arg
c₂ : (1 + z * I).arg + (1 - z * I)⁻¹.arg < π / 2 + π / 2
⊢ -(π / 2) + -(π / 2) = -π

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
hz : ‖z‖ < 1
z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0
z₂ : (1 - z * I).arg ≠ π ∧ 1 - z * I ≠ 0
b₁ : (1 + z * I).arg ∈ Set.Ioo (-(π / 2)) (π / 2)
b₂ : (1 - z * I)⁻¹.arg ∈ Set.Ioo (-(π / 2)) (π / 2)
c₁ : -(π / 2) + -(π / 2) < (1 + z * I).arg + (1 - z * I)⁻¹.arg
c₂ : (1 + z * I).arg + (1 - z * I)⁻¹.arg < π / 2 + π / 2
⊢ -π < (1 + z * I).arg + (1 - z * I)⁻¹.arg

Tactic:
rw [show -(π / 2) + -(π / 2) = -π by ring] at c₁
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
hz : ‖z‖ < 1
z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0
z₂ : (1 - z * I).arg ≠ π ∧ 1 - z * I ≠ 0
b₁ : (1 + z * I).arg ∈ Set.Ioo (-(π / 2)) (π / 2)
b₂ : (1 - z * I)⁻¹.arg ∈ Set.Ioo (-(π / 2)) (π / 2)
c₁ : -(π / 2) + -(π / 2) < (1 + z * I).arg + (1 - z * I)⁻¹.arg
c₂ : (1 + z * I).arg + (1 - z * I)⁻¹.arg < π / 2 + π / 2
c₃ : -π < (1 + z * I).arg + (1 - z * I)⁻¹.arg
⊢ (1 + z * I).arg + (1 - z * I)⁻¹.arg < π / 2 + π / 2

Tactic:
rw [show -(π / 2) + -(π / 2) = -π by ring] at c₁
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
hz : ‖z‖ < 1
z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0
z₂ : (1 - z * I).arg ≠ π ∧ 1 - z * I ≠ 0
b₁ : (1 + z * I).arg ∈ Set.Ioo (-(π / 2)) (π / 2)
b₂ : (1 - z * I)⁻¹.arg ∈ Set.Ioo (-(π / 2)) (π / 2)
c₁ : -π < (1 + z * I).arg + (1 - z * I)⁻¹.arg
c₂ : (1 + z * I).arg + (1 - z * I)⁻¹.arg < π / 2 + π / 2
⊢ π / 2 + π / 2 = π

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
hz : ‖z‖ < 1
z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0
z₂ : (1 - z * I).arg ≠ π ∧ 1 - z * I ≠ 0
b₁ : (1 + z * I).arg ∈ Set.Ioo (-(π / 2)) (π / 2)
b₂ : (1 - z * I)⁻¹.arg ∈ Set.Ioo (-(π / 2)) (π / 2)
c₁ : -π < (1 + z * I).arg + (1 - z * I)⁻¹.arg
c₂ : (1 + z * I).arg + (1 - z * I)⁻¹.arg < π / 2 + π / 2
⊢ (1 + z * I).arg + (1 - z * I)⁻¹.arg < π

Tactic:
rw [show π / 2 + π / 2 = π by ring] at c₂