awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 < π
⊢ (1 + z * I).arg + (1 - z * I)⁻¹.arg ∈ Set.Ioc (-π) π

Tactic:
⟨c₁, c₂.le⟩

Premises used: Set.Ioc, Set.Mem, setOf, LT.lt.le, And.intro
-- 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 < π
⊢ (1 + z * I).arg + (1 - z * I)⁻¹.arg ∈ Set.Ioc (-π) π

Tactic:
exact ⟨c₁, c₂.le⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
hz : ‖z‖ < 1
⊢ HasSum (fun (i : ℕ) ↦ -I / 2 * (HPow.hPow (α := ℂ) (-1) (i + 1) * (z * I) ^ i / (↑i : ℂ) + (z * I) ^ i / (↑i : ℂ)))
    (-I / 2 * (log (1 + z * I) + -log (1 - z * I)))

Tactic:
have := ((hasSum_taylorSeries_log (z := z * I) (by simpa)).add
    (hasSum_taylorSeries_neg_log (z := z * I) (by simpa))).mul_left (-I / 2)
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum (fun (i : ℕ) ↦ -I / 2 * (HPow.hPow (α := ℂ) (-1) (i + 1) * (z * I) ^ i / (↑i : ℂ) + (z * I) ^ i / (↑i : ℂ)))
    (-I / 2 * (log (1 + z * I) + -log (1 - z * I)))
⊢ HasSum (fun (i : ℕ) ↦ -I / 2 * ((HPow.hPow (α := ℂ) (-1) (i + 1) + 1) * (z * I) ^ i / (↑i : ℂ)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))

Tactic:
simp_rw [← add_div, ← add_one_mul, hasSum_arctan_aux hz] at this

Premises used: add_one_mul, Complex.hasSum_arctan_aux, add_div
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum (fun (i : ℕ) ↦ -I / 2 * ((HPow.hPow (α := ℂ) (-1) (i + 1) + 1) * (z * I) ^ i / (↑i : ℂ)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
⊢ HasSum (β := ℕ × Fin 2)
    ((fun (i : ℕ) ↦ -I / 2 * ((HPow.hPow (α := ℂ) (-1) (i + 1) + 1) * (z * I) ^ i / (↑i : ℂ))) ∘
      (⇑(Equiv.symm (Nat.divModEquiv 2)) : (a : ℕ × Fin 2) → ℕ))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))

Tactic:
replace := (Nat.divModEquiv 2).symm.hasSum_iff.mpr this
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum
    (fun (x : ℕ × Fin 2) ↦
      -I / 2 *
        ((HPow.hPow (α := ℂ) (-1) (x.1 * 2 + (↑x.2 : ℕ) + 1) + 1) * (z * I) ^ (x.1 * 2 + (↑x.2 : ℕ)) /
          (↑(x.1 * 2 + (↑x.2 : ℕ)) : ℂ)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
⊢ HasSum
    (fun (x : ℕ × Fin 2) ↦
      -I / 2 *
        ((HPow.hPow (α := ℂ) (-1) (2 * x.1 + (↑x.2 : ℕ) + 1) + 1) * (z * I) ^ (2 * x.1 + (↑x.2 : ℕ)) /
          (↑(2 * x.1 + (↑x.2 : ℕ)) : ℂ)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))

Tactic:
simp_rw [← mul_comm 2 _] at this

Premises used: mul_comm, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum
    (fun (x : ℕ × Fin 2) ↦
      -I / 2 *
        ((HPow.hPow (α := ℂ) (-1) (2 * x.1 + (↑x.2 : ℕ) + 1) + 1) * (z * I) ^ (2 * x.1 + (↑x.2 : ℕ)) /
          (↑(2 * x.1 + (↑x.2 : ℕ)) : ℂ)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
⊢ HasSum (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * z ^ (2 * n + 1) / (↑(2 * n + 1) : ℂ)) z.arctan

Tactic:
this.prod_fiberwise fun k => ?_

Premises used: HasSum.prod_fiberwise, Complex.arctan
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum
    (fun (x : ℕ × Fin 2) ↦
      -I / 2 *
        ((HPow.hPow (α := ℂ) (-1) (2 * x.1 + (↑x.2 : ℕ) + 1) + 1) * (z * I) ^ (2 * x.1 + (↑x.2 : ℕ)) /
          (↑(2 * x.1 + (↑x.2 : ℕ)) : ℂ)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
refine :
  ∀ (k : ℕ),
    HasSum
      (fun (c : Fin 2) ↦
        -I / 2 *
          ((HPow.hPow (α := ℂ) (-1) (2 * (k, c).1 + (↑(k, c).2 : ℕ) + 1) + 1) *
              (z * I) ^ (2 * (k, c).1 + (↑(k, c).2 : ℕ)) /
            (↑(2 * (k, c).1 + (↑(k, c).2 : ℕ)) : ℂ)))
      (HPow.hPow (α := ℂ) (-1) k * z ^ (2 * k + 1) / (↑(2 * k + 1) : ℂ))
⊢ HasSum (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * z ^ (2 * n + 1) / (↑(2 * n + 1) : ℂ)) z.arctan

Tactic:
refine this.prod_fiberwise fun k => ?_

Premises used: HasSum.prod_fiberwise
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum
    (fun (x : ℕ × Fin 2) ↦
      -I / 2 *
        ((HPow.hPow (α := ℂ) (-1) (2 * x.1 + (↑x.2 : ℕ) + 1) + 1) * (z * I) ^ (2 * x.1 + (↑x.2 : ℕ)) /
          (↑(2 * x.1 + (↑x.2 : ℕ)) : ℂ)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
k : ℕ
dsimp :
  HasSum
    (fun (c : Fin 2) ↦
      -I / 2 *
        ((HPow.hPow (α := ℂ) (-1) (2 * k + (↑c : ℕ) + 1) + 1) * (z * I) ^ (2 * k + (↑c : ℕ)) /
          (↑(2 * k + (↑c : ℕ)) : ℂ)))
    (HPow.hPow (α := ℂ) (-1) k * z ^ (2 * k + 1) / (↑(2 * k + 1) : ℂ))
⊢ HasSum
    (fun (c : Fin 2) ↦
      -I / 2 *
        ((HPow.hPow (α := ℂ) (-1) (2 * (k, c).1 + (↑(k, c).2 : ℕ) + 1) + 1) *
            (z * I) ^ (2 * (k, c).1 + (↑(k, c).2 : ℕ)) /
          (↑(2 * (k, c).1 + (↑(k, c).2 : ℕ)) : ℂ)))
    (HPow.hPow (α := ℂ) (-1) k * z ^ (2 * k + 1) / (↑(2 * k + 1) : ℂ))

Tactic:
dsimp only
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum
    (fun (x : ℕ × Fin 2) ↦
      -I / 2 *
        ((HPow.hPow (α := ℂ) (-1) (2 * x.1 + (↑x.2 : ℕ) + 1) + 1) * (z * I) ^ (2 * x.1 + (↑x.2 : ℕ)) /
          (↑(2 * x.1 + (↑x.2 : ℕ)) : ℂ)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
k : ℕ
⊢ HasSum (α := ℂ)
    (fun (c : Fin 2) ↦
      -I / 2 *
        ((HPow.hPow (α := ℂ) (-1) (2 * k + (↑c : ℕ) + 1) + 1) * (z * I) ^ (2 * k + (↑c : ℕ)) /
          (↑(2 * k + (↑c : ℕ)) : ℂ)))
    (∑ b : Fin 2,
      -I / 2 *
        ((HPow.hPow (α := ℂ) (-1) (2 * k + (↑b : ℕ) + 1) + 1) * (z * I) ^ (2 * k + (↑b : ℕ)) /
          (↑(2 * k + (↑b : ℕ)) : ℂ)))

Tactic:
hasSum_fintype (_ : Fin 2 → ℂ)

Premises used: hasSum_fintype, SummationFilter.unconditional
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum
    (fun (x : ℕ × Fin 2) ↦
      -I / 2 *
        ((HPow.hPow (α := ℂ) (-1) (2 * x.1 + (↑x.2 : ℕ) + 1) + 1) * (z * I) ^ (2 * x.1 + (↑x.2 : ℕ)) /
          (↑(2 * x.1 + (↑x.2 : ℕ)) : ℂ)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
k : ℕ
h :
  HPow.hPow (α := ℂ) (-1) k * z ^ (2 * k + 1) / (↑(2 * k + 1) : ℂ) =
    ∑ b : Fin 2,
      -I / 2 *
        ((HPow.hPow (α := ℂ) (-1) (2 * k + (↑b : ℕ) + 1) + 1) * (z * I) ^ (2 * k + (↑b : ℕ)) /
          (↑(2 * k + (↑b : ℕ)) : ℂ))
⊢ HasSum
    (fun (c : Fin 2) ↦
      -I / 2 *
        ((HPow.hPow (α := ℂ) (-1) (2 * k + (↑c : ℕ) + 1) + 1) * (z * I) ^ (2 * k + (↑c : ℕ)) /
          (↑(2 * k + (↑c : ℕ)) : ℂ)))
    (HPow.hPow (α := ℂ) (-1) k * z ^ (2 * k + 1) / (↑(2 * k + 1) : ℂ))

Tactic:
convert! hasSum_fintype (_ : Fin 2 → ℂ) using 1

Premises used: hasSum_fintype, SummationFilter.unconditional
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum
    (fun (x : ℕ × Fin 2) ↦
      -I / 2 *
        ((HPow.hPow (α := ℂ) (-1) (2 * x.1 + (↑x.2 : ℕ) + 1) + 1) * (z * I) ^ (2 * x.1 + (↑x.2 : ℕ)) /
          (↑(2 * x.1 + (↑x.2 : ℕ)) : ℂ)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
k : ℕ
⊢ Odd (2 * k + 0 + 1)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum
    (fun (x : ℕ × Fin 2) ↦
      -I / 2 *
        ((HPow.hPow (α := ℂ) (-1) (2 * x.1 + (↑x.2 : ℕ) + 1) + 1) * (z * I) ^ (2 * x.1 + (↑x.2 : ℕ)) /
          (↑(2 * x.1 + (↑x.2 : ℕ)) : ℂ)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
k : ℕ
⊢ 2 * k + 1 + 1 = 2 * (k + 1)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum
    (fun (x : ℕ × Fin 2) ↦
      -I / 2 *
        ((HPow.hPow (α := ℂ) (-1) (2 * x.1 + (↑x.2 : ℕ) + 1) + 1) * (z * I) ^ (2 * x.1 + (↑x.2 : ℕ)) /
          (↑(2 * x.1 + (↑x.2 : ℕ)) : ℂ)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
k : ℕ
⊢ Even (2 * (k + 1))

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum
    (fun (x : ℕ × Fin 2) ↦
      -I / 2 *
        ((HPow.hPow (α := ℂ) (-1) (2 * x.1 + (↑x.2 : ℕ) + 1) + 1) * (z * I) ^ (2 * x.1 + (↑x.2 : ℕ)) /
          (↑(2 * x.1 + (↑x.2 : ℕ)) : ℂ)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
k : ℕ
⊢ -I / 2 * HAdd.hAdd (α := ℂ) 1 1 = -I

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum
    (fun (x : ℕ × Fin 2) ↦
      -I / 2 *
        ((HPow.hPow (α := ℂ) (-1) (2 * x.1 + (↑x.2 : ℕ) + 1) + 1) * (z * I) ^ (2 * x.1 + (↑x.2 : ℕ)) /
          (↑(2 * x.1 + (↑x.2 : ℕ)) : ℂ)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
k : ℕ
h : HPow.hPow (α := ℂ) (-1) k * z ^ (2 * k + 1) / (↑(2 * k + 1) : ℂ) = -I * (z * I) ^ (2 * k + 1) / (↑(2 * k + 1) : ℂ)
⊢ HPow.hPow (α := ℂ) (-1) k * z ^ (2 * k + 1) / (↑(2 * k + 1) : ℂ) =
    ∑ b : Fin 2,
      -I / 2 *
        ((HPow.hPow (α := ℂ) (-1) (2 * k + (↑b : ℕ) + 1) + 1) * (z * I) ^ (2 * k + (↑b : ℕ)) /
          (↑(2 * k + (↑b : ℕ)) : ℂ))

Tactic:
rw [Fin.sum_univ_two, Fin.val_zero, Fin.val_one, Odd.neg_one_pow (n := 2 * k + 0 + 1) (by simp),
    neg_add_cancel, zero_mul, zero_div, mul_zero, zero_add,
    show 2 * k + 1 + 1 = 2 * (k + 1) by ring, Even.neg_one_pow (n := 2 * (k + 1)) (by simp),
    ← mul_div_assoc (_ / _), ← mul_assoc, show -I / 2 * (1 + 1) = -I by ring]

Premises used: MulZeroClass.zero_mul, mul_assoc, mul_div_assoc, zero_div, HDiv.hDiv, Fin.val_one, Even.neg_one_pow, zero_add, MulZeroClass.mul_zero, neg_add_cancel, Fin.sum_univ_two, Fin.val_zero, Odd.neg_one_pow
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum
    (fun (x : ℕ × Fin 2) ↦
      -I / 2 *
        ((HPow.hPow (α := ℂ) (-1) (2 * x.1 + (↑x.2 : ℕ) + 1) + 1) * (z * I) ^ (2 * x.1 + (↑x.2 : ℕ)) /
          (↑(2 * x.1 + (↑x.2 : ℕ)) : ℂ)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
k : ℕ
h : HPow.hPow (α := ℂ) (-1) k * z ^ (2 * k + 1) = -I * (z * I) ^ (2 * k + 1)
⊢ HPow.hPow (α := ℂ) (-1) k * z ^ (2 * k + 1) / (↑(2 * k + 1) : ℂ) = -I * (z * I) ^ (2 * k + 1) / (↑(2 * k + 1) : ℂ)

Tactic:
congr 1
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum
    (fun (x : ℕ × Fin 2) ↦
      -I / 2 *
        ((HPow.hPow (α := ℂ) (-1) (2 * x.1 + (↑x.2 : ℕ) + 1) + 1) * (z * I) ^ (2 * x.1 + (↑x.2 : ℕ)) /
          (↑(2 * x.1 + (↑x.2 : ℕ)) : ℂ)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
k : ℕ
⊢ -I * (z ^ (2 * k + 1) * (I * HPow.hPow (α := ℂ) (-1) k)) = -(I * I) * HPow.hPow (α := ℂ) (-1) k * z ^ (2 * k + 1)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum
    (fun (x : ℕ × Fin 2) ↦
      -I / 2 *
        ((HPow.hPow (α := ℂ) (-1) (2 * x.1 + (↑x.2 : ℕ) + 1) + 1) * (z * I) ^ (2 * x.1 + (↑x.2 : ℕ)) /
          (↑(2 * x.1 + (↑x.2 : ℕ)) : ℂ)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
k : ℕ
h : HPow.hPow (α := ℂ) (-1) k * z ^ (2 * k + 1) = -I * (z ^ (2 * k + 1) * I ^ (2 * k + 1))
h₁ : HPow.hPow (α := ℂ) (-1) k * z ^ (2 * k + 1) = -I * (z ^ (2 * k + 1) * (I * I ^ (2 * k)))
h₂ : HPow.hPow (α := ℂ) (-1) k * z ^ (2 * k + 1) = -I * (z ^ (2 * k + 1) * (I * HPow.hPow (β := ℕ) I 2 ^ k))
h₃ : HPow.hPow (α := ℂ) (-1) k * z ^ (2 * k + 1) = -I * (z ^ (2 * k + 1) * (I * HPow.hPow (α := ℂ) (-1) k))
h₄ : HPow.hPow (α := ℂ) (-1) k * z ^ (2 * k + 1) = -(I * I) * HPow.hPow (α := ℂ) (-1) k * z ^ (2 * k + 1)
h₅ : HPow.hPow (α := ℂ) (-1) k * z ^ (2 * k + 1) = - -1 * HPow.hPow (α := ℂ) (-1) k * z ^ (2 * k + 1)
h₆ : HPow.hPow (α := ℂ) (-1) k * z ^ (2 * k + 1) = 1 * HPow.hPow (α := ℂ) (-1) k * z ^ (2 * k + 1)
h₇ h₈ : HPow.hPow (α := ℂ) (-1) k * z ^ (2 * k + 1) = HPow.hPow (α := ℂ) (-1) k * z ^ (2 * k + 1)
⊢ HPow.hPow (α := ℂ) (-1) k * z ^ (2 * k + 1) = -I * (z * I) ^ (2 * k + 1)

Tactic:
rw [mul_pow, pow_succ' I, pow_mul, I_sq,
    show -I * _ = -(I * I) * (-1) ^ k * z ^ (2 * k + 1) by ring, I_mul_I, neg_neg, one_mul]

Premises used: neg_neg, pow_mul, Complex.I_mul_I, Complex.I_sq, mul_pow, pow_succ', one_mul, Complex.I
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
x : ℝ
hx : ‖x‖ < 1
⊢ ‖(↑x : ℂ)‖ < 1

Tactic:
simpa
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
pos : 0 ≤ x.re → Real.sin (Real.arcsin (x.im / ‖x‖)) = x.im / ‖x‖
pos₁ : ¬0 ≤ x.re → 0 ≤ x.im → Real.sin (Real.arcsin ((-x).im / ‖x‖) + π) = x.im / ‖x‖
neg : ¬0 ≤ x.re → ¬0 ≤ x.im → Real.sin (Real.arcsin ((-x).im / ‖x‖) - π) = x.im / ‖x‖
⊢ Real.sin
      (if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
      else if 0 ≤ x.im then Real.arcsin ((-x).im / ‖x‖) + π else Real.arcsin ((-x).im / ‖x‖) - π) =
    x.im / ‖x‖

Tactic:
split_ifs
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
h : 0 ≤ x.re
⊢ Real.sin (Real.arcsin (x.im / ‖x‖)) = x.im / ‖x‖

Tactic:
simp [sub_eq_add_neg, Real.sin_arcsin (abs_le.1 (abs_im_div_norm_le_one x)).1
      (abs_le.1 (abs_im_div_norm_le_one x)).2, Real.sin_add, neg_div, Real.arcsin_neg, Real.sin_neg]

Premises used: neg_div, Real.sin_arcsin, abs_le, sub_eq_add_neg, Real.sin_add, Real.sin_neg, Real.arcsin_neg, Complex.abs_im_div_norm_le_one, And.right, And.left, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
h : ¬0 ≤ x.re
h_1 : ¬0 ≤ x.im
⊢ Real.sin (Real.arcsin ((-x).im / ‖x‖) - π) = x.im / ‖x‖

Tactic:
simp [sub_eq_add_neg, Real.sin_arcsin (abs_le.1 (abs_im_div_norm_le_one x)).1
      (abs_le.1 (abs_im_div_norm_le_one x)).2, Real.sin_add, neg_div, Real.arcsin_neg, Real.sin_neg]

Premises used: neg_div, Real.sin_arcsin, abs_le, sub_eq_add_neg, Real.sin_add, Real.sin_neg, Real.arcsin_neg, Complex.abs_im_div_norm_le_one, And.right, And.left, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hx : x ≠ 0
pos : ∀ (h₁ : 0 ≤ x.re), Real.cos (Real.arcsin (x.im / ‖x‖)) = x.re / ‖x‖
pos₁ : ∀ (h₁ : ¬0 ≤ x.re) (h₂ : 0 ≤ x.im), Real.cos (Real.arcsin ((-x).im / ‖x‖) + π) = x.re / ‖x‖
neg : ∀ (h₁ : ¬0 ≤ x.re) (h₂ : ¬0 ≤ x.im), Real.cos (Real.arcsin ((-x).im / ‖x‖) - π) = x.re / ‖x‖
⊢ Real.cos
      (if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
      else if 0 ≤ x.im then Real.arcsin ((-x).im / ‖x‖) + π else Real.arcsin ((-x).im / ‖x‖) - π) =
    x.re / ‖x‖

Tactic:
split_ifs with h₁ h₂
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hx : x ≠ 0
h₁ : 0 ≤ x.re
pos : √(1 - HPow.hPow (β := ℕ) (x.im / ‖x‖) 2) = x.re / ‖x‖
⊢ Real.cos (Real.arcsin (x.im / ‖x‖)) = x.re / ‖x‖

Tactic:
rw [Real.cos_arcsin]

Premises used: Real.cos_arcsin
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hx : x ≠ 0
h₁ : 0 ≤ x.re
pos : ‖x‖ * √((HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) x.im 2) / HPow.hPow (β := ℕ) ‖x‖ 2) = x.re
⊢ √(1 - HPow.hPow (β := ℕ) (x.im / ‖x‖) 2) = x.re / ‖x‖

Tactic:
field_simp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hx : x ≠ 0
h₁ : 0 ≤ x.re
pos : ‖x‖ * (x.re / ‖x‖) = x.re
⊢ ‖x‖ * √((HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) x.im 2) / HPow.hPow (β := ℕ) ‖x‖ 2) = x.re

Tactic:
simp [Real.sqrt_sq, (norm_pos_iff.mpr hx).le, *]

Premises used: Iff.mpr, norm_pos_iff, LT.lt.le, Real.sqrt_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hx : x ≠ 0
h₁ : 0 ≤ x.re
⊢ ‖x‖ * (x.re / ‖x‖) = x.re

Tactic:
field
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hx : x ≠ 0
h₁ : ¬0 ≤ x.re
h₂ : 0 ≤ x.im
pos : -√(1 - HPow.hPow (β := ℕ) ((-x).im / ‖x‖) 2) = x.re / ‖x‖
⊢ Real.cos (Real.arcsin ((-x).im / ‖x‖) + π) = x.re / ‖x‖

Tactic:
rw [Real.cos_add_pi, Real.cos_arcsin]

Premises used: Real.cos_add_pi, Real.cos_arcsin
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hx : x ≠ 0
h₁ : ¬0 ≤ x.re
h₂ : 0 ≤ x.im
pos : -(‖x‖ * √((HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) (-x).im 2) / HPow.hPow (β := ℕ) ‖x‖ 2)) = x.re
⊢ -√(1 - HPow.hPow (β := ℕ) ((-x).im / ‖x‖) 2) = x.re / ‖x‖

Tactic:
field_simp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hx : x ≠ 0
h₁ : ¬0 ≤ x.re
h₂ : 0 ≤ x.im
pos : -(‖x‖ * (-x.re / ‖x‖)) = x.re
⊢ -(‖x‖ * √((HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) (-x).im 2) / HPow.hPow (β := ℕ) ‖x‖ 2)) = x.re

Tactic:
simp [Real.sqrt_div (sq_nonneg _), Real.sqrt_sq_eq_abs, _root_.abs_of_neg (not_le.1 h₁), *]

Premises used: not_le, abs_of_neg, Real.sqrt_sq_eq_abs, sq_nonneg, Iff.mp, Real.sqrt_div
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hx : x ≠ 0
h₁ : ¬0 ≤ x.re
h₂ : 0 ≤ x.im
⊢ -(‖x‖ * (-x.re / ‖x‖)) = x.re

Tactic:
field
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hx : x ≠ 0
h₁ : ¬0 ≤ x.re
h₂ : ¬0 ≤ x.im
neg : -√(1 - HPow.hPow (β := ℕ) ((-x).im / ‖x‖) 2) = x.re / ‖x‖
⊢ Real.cos (Real.arcsin ((-x).im / ‖x‖) - π) = x.re / ‖x‖

Tactic:
rw [Real.cos_sub_pi, Real.cos_arcsin]

Premises used: Real.cos_sub_pi, Real.cos_arcsin
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hx : x ≠ 0
h₁ : ¬0 ≤ x.re
h₂ : ¬0 ≤ x.im
neg : -(‖x‖ * √((HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) (-x).im 2) / HPow.hPow (β := ℕ) ‖x‖ 2)) = x.re
⊢ -√(1 - HPow.hPow (β := ℕ) ((-x).im / ‖x‖) 2) = x.re / ‖x‖

Tactic:
field_simp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hx : x ≠ 0
h₁ : ¬0 ≤ x.re
h₂ : ¬0 ≤ x.im
neg : -(‖x‖ * (-x.re / ‖x‖)) = x.re
⊢ -(‖x‖ * √((HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) (-x).im 2) / HPow.hPow (β := ℕ) ‖x‖ 2)) = x.re

Tactic:
simp [Real.sqrt_div (sq_nonneg _), Real.sqrt_sq_eq_abs, _root_.abs_of_neg (not_le.1 h₁), *]

Premises used: not_le, abs_of_neg, Real.sqrt_sq_eq_abs, sq_nonneg, Iff.mp, Real.sqrt_div
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hx : x ≠ 0
h₁ : ¬0 ≤ x.re
h₂ : ¬0 ≤ x.im
⊢ -(‖x‖ * (-x.re / ‖x‖)) = x.re

Tactic:
field
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
inl : (↑(norm (E := ℂ) 0) : ℂ) * cexp ((↑(arg 0) : ℂ) * I) = 0
inr : ∀ (hx : x ≠ 0), (↑‖x‖ : ℂ) * cexp ((↑x.arg : ℂ) * I) = x
⊢ (↑‖x‖ : ℂ) * cexp ((↑x.arg : ℂ) * I) = x

Tactic:
rcases eq_or_ne x 0 with (rfl | hx)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
⊢ (↑(norm (E := ℂ) 0) : ℂ) * cexp ((↑(arg 0) : ℂ) * I) = 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hx : x ≠ 0
⊢ ‖x‖ ≠ 0

Tactic:
have : ‖x‖ ≠ 0 := norm_ne_zero_iff.mpr hx
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hx : x ≠ 0
this : ‖x‖ ≠ 0
inr : ((↑‖x‖ : ℂ) * cexp ((↑x.arg : ℂ) * I)).re = x.re
inr₁ : ((↑‖x‖ : ℂ) * cexp ((↑x.arg : ℂ) * I)).im = x.im
⊢ (↑‖x‖ : ℂ) * cexp ((↑x.arg : ℂ) * I) = x

Tactic:
apply Complex.ext

Premises used: Complex.ext
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hx : x ≠ 0
this : ‖x‖ ≠ 0
⊢ ((↑‖x‖ : ℂ) * cexp ((↑x.arg : ℂ) * I)).re = x.re

Tactic:
simp [sin_arg, cos_arg hx, this, mul_comm ‖x‖]

Premises used: Norm.norm, mul_comm, Complex.sin_arg, Complex.cos_arg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hx : x ≠ 0
this : ‖x‖ ≠ 0
⊢ ((↑‖x‖ : ℂ) * cexp ((↑x.arg : ℂ) * I)).im = x.im

Tactic:
simp [sin_arg, cos_arg hx, this, mul_comm ‖x‖]

Premises used: Norm.norm, mul_comm, Complex.sin_arg, Complex.cos_arg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
rw : (↑‖x‖ : ℂ) * cexp ((↑x.arg : ℂ) * I) = x
rw₁ rw₂ : x = x
⊢ (↑‖x‖ : ℂ) * (cos (↑x.arg : ℂ) + sin (↑x.arg : ℂ) * I) = x

Tactic:
rw [← exp_mul_I, norm_mul_exp_arg_mul_I]

Premises used: Complex.norm_mul_exp_arg_mul_I, Complex.exp_mul_I
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
⊢ ‖x‖ * Real.cos x.arg = x.re

Tactic:
simpa [-norm_mul_cos_add_sin_mul_I] using congr_arg re (norm_mul_cos_add_sin_mul_I x)

Premises used: Complex.norm_mul_cos_add_sin_mul_I, Complex.re, congr_arg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
⊢ ‖x‖ * Real.sin x.arg = x.im

Tactic:
simpa [-norm_mul_cos_add_sin_mul_I] using congr_arg im (norm_mul_cos_add_sin_mul_I x)

Premises used: Complex.im, Complex.norm_mul_cos_add_sin_mul_I, congr_arg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
⊢ ‖z‖ = 1 ↔ ∃ (θ : ℝ), cexp ((↑θ : ℂ) * I) = z

Tactic:
⟨fun hz => ⟨arg z, ?_⟩, ?_⟩

Premises used: Complex.arg, Iff.intro, Exists.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
refine_1 : ∀ (hz : ‖z‖ = 1), cexp ((↑z.arg : ℂ) * I) = z
refine_2 : (∃ (θ : ℝ), cexp ((↑θ : ℂ) * I) = z) → ‖z‖ = 1
⊢ ‖z‖ = 1 ↔ ∃ (θ : ℝ), cexp ((↑θ : ℂ) * I) = z

Tactic:
refine ⟨fun hz => ⟨arg z, ?_⟩, ?_⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hz : ‖z‖ = 1
rw : cexp ((↑z.arg : ℂ) * I) = (↑1 : ℂ) * cexp ((↑z.arg : ℂ) * I)
rw₁ : cexp ((↑z.arg : ℂ) * I) = 1 * cexp ((↑z.arg : ℂ) * I)
rw₂ rw₃ : cexp ((↑z.arg : ℂ) * I) = cexp ((↑z.arg : ℂ) * I)
⊢ cexp ((↑z.arg : ℂ) * I) = (↑‖z‖ : ℂ) * cexp ((↑z.arg : ℂ) * I)

Tactic:
rw [hz, ofReal_one, one_mul]

Premises used: Complex.ofReal_one, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hz : ‖z‖ = 1
⊢ (↑‖z‖ : ℂ) * cexp ((↑z.arg : ℂ) * I) = z

Tactic:
norm_mul_exp_arg_mul_I z

Premises used: Complex.norm_mul_exp_arg_mul_I
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hz : ‖z‖ = 1
exp : cexp ((↑z.arg : ℂ) * I) = (↑‖z‖ : ℂ) * cexp ((↑z.arg : ℂ) * I)
⊢ cexp ((↑z.arg : ℂ) * I) = z

Tactic:
calc
      exp (arg z * I) = ‖z‖ * exp (arg z * I) := by rw [hz, ofReal_one, one_mul]
      _ = z := norm_mul_exp_arg_mul_I z

Premises used: HMul.hMul, Complex.arg, Complex.ofReal, Complex.norm_mul_exp_arg_mul_I, Complex.exp, Complex.I
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
θ : ℝ
⊢ ‖cexp ((↑θ : ℂ) * I)‖ = 1

Tactic:
Complex.norm_exp_ofReal_mul_I θ

Premises used: Complex.norm_exp_ofReal_mul_I
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
θ : ℝ
⊢ ‖cexp ((↑θ : ℂ) * I)‖ = 1

Tactic:
exact Complex.norm_exp_ofReal_mul_I θ

Premises used: Complex.norm_exp_ofReal_mul_I
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
h :
  ∀ (x : ℂ),
    Membership.mem (γ := Set ℂ) (range fun (x : ℝ) ↦ cexp ((↑x : ℂ) * I)) x ↔ Membership.mem (γ := Set ℂ) (sphere 0 1) x
⊢ Eq (α := Set ℂ) (range fun (x : ℝ) ↦ cexp ((↑x : ℂ) * I)) (sphere 0 1)

Tactic:
ext x
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
⊢ Membership.mem (γ := Set ℂ) (range fun (x : ℝ) ↦ cexp ((↑x : ℂ) * I)) x ↔ Membership.mem (γ := Set ℂ) (sphere 0 1) x

Tactic:
simp only [mem_sphere_zero_iff_norm, norm_eq_one_iff, Set.mem_range]

Premises used: Set.mem_range, Complex.norm_eq_one_iff, mem_sphere_zero_iff_norm
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
simp :
  (if 0 ≤ ((↑r : ℂ) * (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I)).re then
      Real.arcsin (((↑r : ℂ) * (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I)).im / r)
    else
      if 0 ≤ ((↑r : ℂ) * (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I)).im then
        Real.arcsin ((-((↑r : ℂ) * (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I))).im / r) + π
      else Real.arcsin ((-((↑r : ℂ) * (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I))).im / r) - π) =
    θ
⊢ ((↑r : ℂ) * (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I)).arg = θ

Tactic:
simp only [arg, norm_mul, norm_cos_add_sin_mul_I, Complex.norm_of_nonneg hr.le, mul_one]

Premises used: Complex.norm_cos_add_sin_mul_I, Complex.arg, LT.lt.le, norm_mul, Complex.norm_of_nonneg, mul_one