awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
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‖
have pos : 0 ≤ x.re → Real.sin (Real.arcsin (x.im / ‖x‖)) = x.im / ‖x‖
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
pos : 0 ≤ x.re → 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‖
have pos₁ : ¬0 ≤ x.re → 0 ≤ x.im → Real.sin (Real.arcsin ((-x).im / ‖x‖) + π) = x.im / ‖x‖
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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‖
⊢ 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‖
have neg : ¬0 ≤ x.re → ¬0 ≤ x.im → Real.sin (Real.arcsin ((-x).im / ‖x‖) - π) = x.im / ‖x‖
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
hx : x ≠ 0
⊢ 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‖
have pos : ∀ (h₁ : 0 ≤ x.re), Real.cos (Real.arcsin (x.im / ‖x‖)) = x.re / ‖x‖
Tactic: split_ifs with h₁ h₂
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
hx : x ≠ 0
pos : ∀ (h₁ : 0 ≤ x.re), 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‖
have pos₁ : ∀ (h₁ : ¬0 ≤ x.re) (h₂ : 0 ≤ x.im), Real.cos (Real.arcsin ((-x).im / ‖x‖) + π) = x.re / ‖x‖
Tactic: split_ifs with h₁ h₂
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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‖
⊢ 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‖
have neg : ∀ (h₁ : ¬0 ≤ x.re) (h₂ : ¬0 ≤ x.im), Real.cos (Real.arcsin ((-x).im / ‖x‖) - π) = x.re / ‖x‖
Tactic: split_ifs with h₁ h₂
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
hx : x ≠ 0
h₁ : 0 ≤ x.re
⊢ Real.cos (Real.arcsin (x.im / ‖x‖)) = x.re / ‖x‖
have pos : √(1 - HPow.hPow (β := ℕ) (x.im / ‖x‖) 2) = x.re / ‖x‖
Tactic: rw [Real.cos_arcsin]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
hx : x ≠ 0
h₁ : 0 ≤ x.re
⊢ √(1 - HPow.hPow (β := ℕ) (x.im / ‖x‖) 2) = x.re / ‖x‖
have pos : ‖x‖ * √((HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) x.im 2) / HPow.hPow (β := ℕ) ‖x‖ 2) = x.re
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
hx : x ≠ 0
h₁ : 0 ≤ x.re
⊢ ‖x‖ * √((HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) x.im 2) / HPow.hPow (β := ℕ) ‖x‖ 2) = x.re
have pos : ‖x‖ * (x.re / ‖x‖) = x.re
Tactic: simp [Real.sqrt_sq, (norm_pos_iff.mpr hx).le, *]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
hx : x ≠ 0
h₁ : ¬0 ≤ x.re
h₂ : 0 ≤ x.im
⊢ Real.cos (Real.arcsin ((-x).im / ‖x‖) + π) = x.re / ‖x‖
have pos : -√(1 - HPow.hPow (β := ℕ) ((-x).im / ‖x‖) 2) = x.re / ‖x‖
Tactic: rw [Real.cos_add_pi, Real.cos_arcsin]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
hx : x ≠ 0
h₁ : ¬0 ≤ x.re
h₂ : 0 ≤ x.im
⊢ -√(1 - HPow.hPow (β := ℕ) ((-x).im / ‖x‖) 2) = x.re / ‖x‖
have pos : -(‖x‖ * √((HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) (-x).im 2) / HPow.hPow (β := ℕ) ‖x‖ 2)) = x.re
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
hx : x ≠ 0
h₁ : ¬0 ≤ x.re
h₂ : 0 ≤ x.im
⊢ -(‖x‖ * √((HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) (-x).im 2) / HPow.hPow (β := ℕ) ‖x‖ 2)) = x.re
have pos : -(‖x‖ * (-x.re / ‖x‖)) = x.re
Tactic: simp [Real.sqrt_div (sq_nonneg _), Real.sqrt_sq_eq_abs, _root_.abs_of_neg (not_le.1 h₁), *]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
hx : x ≠ 0
h₁ : ¬0 ≤ x.re
h₂ : ¬0 ≤ x.im
⊢ Real.cos (Real.arcsin ((-x).im / ‖x‖) - π) = x.re / ‖x‖
have neg : -√(1 - HPow.hPow (β := ℕ) ((-x).im / ‖x‖) 2) = x.re / ‖x‖
Tactic: rw [Real.cos_sub_pi, Real.cos_arcsin]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
hx : x ≠ 0
h₁ : ¬0 ≤ x.re
h₂ : ¬0 ≤ x.im
⊢ -√(1 - HPow.hPow (β := ℕ) ((-x).im / ‖x‖) 2) = x.re / ‖x‖
have neg : -(‖x‖ * √((HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) (-x).im 2) / HPow.hPow (β := ℕ) ‖x‖ 2)) = x.re
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
hx : x ≠ 0
h₁ : ¬0 ≤ x.re
h₂ : ¬0 ≤ x.im
⊢ -(‖x‖ * √((HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) (-x).im 2) / HPow.hPow (β := ℕ) ‖x‖ 2)) = x.re
have neg : -(‖x‖ * (-x.re / ‖x‖)) = x.re
Tactic: simp [Real.sqrt_div (sq_nonneg _), Real.sqrt_sq_eq_abs, _root_.abs_of_neg (not_le.1 h₁), *]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
⊢ (↑‖x‖ : ℂ) * cexp ((↑x.arg : ℂ) * I) = x
have inl : (↑(norm (E := ℂ) 0) : ℂ) * cexp ((↑(arg 0) : ℂ) * I) = 0
Tactic: rcases eq_or_ne x 0 with (rfl | hx)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
inl : (↑(norm (E := ℂ) 0) : ℂ) * cexp ((↑(arg 0) : ℂ) * I) = 0
⊢ (↑‖x‖ : ℂ) * cexp ((↑x.arg : ℂ) * I) = x
have inr : ∀ (hx : x ≠ 0), (↑‖x‖ : ℂ) * cexp ((↑x.arg : ℂ) * I) = x
Tactic: rcases eq_or_ne x 0 with (rfl | hx)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (hypothesis)
Goal:
x : ℂ
hx : x ≠ 0
⊢ (↑‖x‖ : ℂ) * cexp ((↑x.arg : ℂ) * I) = x
have this : ‖x‖ ≠ 0
Tactic: have : ‖x‖ ≠ 0 := norm_ne_zero_iff.mpr hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
hx : x ≠ 0
this : ‖x‖ ≠ 0
⊢ (↑‖x‖ : ℂ) * cexp ((↑x.arg : ℂ) * I) = x
have inr : ((↑‖x‖ : ℂ) * cexp ((↑x.arg : ℂ) * I)).re = x.re
Tactic: apply Complex.ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
hx : x ≠ 0
this : ‖x‖ ≠ 0
inr : ((↑‖x‖ : ℂ) * cexp ((↑x.arg : ℂ) * I)).re = x.re
⊢ (↑‖x‖ : ℂ) * cexp ((↑x.arg : ℂ) * I) = x
have inr₁ : ((↑‖x‖ : ℂ) * cexp ((↑x.arg : ℂ) * I)).im = x.im
Tactic: apply Complex.ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
⊢ (↑‖x‖ : ℂ) * (cos (↑x.arg : ℂ) + sin (↑x.arg : ℂ) * I) = x
have rw : (↑‖x‖ : ℂ) * cexp ((↑x.arg : ℂ) * I) = x
Tactic: rw [← exp_mul_I, norm_mul_exp_arg_mul_I]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
rw : (↑‖x‖ : ℂ) * cexp ((↑x.arg : ℂ) * I) = x
⊢ (↑‖x‖ : ℂ) * (cos (↑x.arg : ℂ) + sin (↑x.arg : ℂ) * I) = x
have rw₁ : x = x
Tactic: rw [← exp_mul_I, norm_mul_exp_arg_mul_I]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
⊢ ‖z‖ = 1 ↔ ∃ (θ : ℝ), cexp ((↑θ : ℂ) * I) = z
have refine_1 : ∀ (hz : ‖z‖ = 1), cexp ((↑z.arg : ℂ) * I) = z
Tactic: refine ⟨fun hz => ⟨arg z, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
refine_1 : ∀ (hz : ‖z‖ = 1), cexp ((↑z.arg : ℂ) * I) = z
⊢ ‖z‖ = 1 ↔ ∃ (θ : ℝ), cexp ((↑θ : ℂ) * I) = z
have refine_2 : (∃ (θ : ℝ), cexp ((↑θ : ℂ) * I) = z) → ‖z‖ = 1
Tactic: refine ⟨fun hz => ⟨arg z, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
hz : ‖z‖ = 1
⊢ cexp ((↑z.arg : ℂ) * I) = (↑‖z‖ : ℂ) * cexp ((↑z.arg : ℂ) * I)
have rw : cexp ((↑z.arg : ℂ) * I) = (↑1 : ℂ) * cexp ((↑z.arg : ℂ) * I)
Tactic: rw [hz, ofReal_one, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
hz : ‖z‖ = 1
rw : cexp ((↑z.arg : ℂ) * I) = (↑1 : ℂ) * cexp ((↑z.arg : ℂ) * I)
⊢ cexp ((↑z.arg : ℂ) * I) = (↑‖z‖ : ℂ) * cexp ((↑z.arg : ℂ) * I)
have rw₁ : cexp ((↑z.arg : ℂ) * I) = 1 * cexp ((↑z.arg : ℂ) * I)
Tactic: rw [hz, ofReal_one, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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)
⊢ cexp ((↑z.arg : ℂ) * I) = (↑‖z‖ : ℂ) * cexp ((↑z.arg : ℂ) * I)
have rw₂ : cexp ((↑z.arg : ℂ) * I) = cexp ((↑z.arg : ℂ) * I)
Tactic: rw [hz, ofReal_one, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
hz : ‖z‖ = 1
⊢ cexp ((↑z.arg : ℂ) * I) = z
have exp : cexp ((↑z.arg : ℂ) * I) = (↑‖z‖ : ℂ) * cexp ((↑z.arg : ℂ) * I)
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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
⊢ Eq (α := Set ℂ) (range fun (x : ℝ) ↦ cexp ((↑x : ℂ) * I)) (sphere 0 1)
have h : ∀ (x : ℂ),
  Membership.mem (γ := Set ℂ) (range fun (x : ℝ) ↦ cexp ((↑x : ℂ) * I)) x ↔ Membership.mem (γ := Set ℂ) (sphere 0 1) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ ((↑r : ℂ) * (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I)).arg = θ
have 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) - π) =
  θ
Tactic: simp only [arg, norm_mul, norm_cos_add_sin_mul_I, Complex.norm_of_nonneg hr.le, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ (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) - π) =
    θ
have simp : (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
  else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
  θ
Tactic: simp only [re_ofReal_mul, im_ofReal_mul, neg_im, ← ofReal_cos, ← ofReal_sin, ←
    mk_eq_add_mul_I, neg_div, mul_div_cancel_left₀ _ hr.ne', mul_nonneg_iff_right_nonneg_of_pos hr]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
have pos : ∀ (h₁ : θ ∈ Icc (-(π / 2)) (π / 2)),
  (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
Tactic: by_cases h₁ : θ ∈ Set.Icc (-(π / 2)) (π / 2)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
pos :
  ∀ (h₁ : θ ∈ Icc (-(π / 2)) (π / 2)),
    (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
      else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
      θ
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
have neg : ∀ (h₁ : θ ∉ Icc (-(π / 2)) (π / 2)),
  (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
Tactic: by_cases h₁ : θ ∈ Set.Icc (-(π / 2)) (π / 2)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : θ ∈ Icc (-(π / 2)) (π / 2)
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
have pos : Real.arcsin (Real.sin θ) = θ
Tactic: rw [if_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : θ ∈ Icc (-(π / 2)) (π / 2)
pos : Real.arcsin (Real.sin θ) = θ
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
have pos₁ : 0 ≤ Real.cos θ
Tactic: rw [if_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (hypothesis)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : θ ∉ Icc (-(π / 2)) (π / 2)
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
have h₂ : θ < -(π / 2) ∨ π / 2 < θ
Tactic: rw [Set.mem_Icc, not_and_or, not_le, not_le] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : θ < -(π / 2) ∨ π / 2 < θ
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
have neg : ∀ (h₁ : θ < -(π / 2)),
  (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
Tactic: rcases h₁ with h₁ | h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : θ < -(π / 2) ∨ π / 2 < θ
neg :
  ∀ (h₁ : θ < -(π / 2)),
    (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
      else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
      θ
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
have neg₁ : ∀ (h₁ : π / 2 < θ),
  (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
Tactic: rcases h₁ with h₁ | h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (hypothesis)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : θ < -(π / 2)
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
have hθ₁ : -π < θ
Tactic: replace hθ := hθ.1
Cleared hypotheses: hθ
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
⊢ Real.cos θ < 0
have rw : 0 < Real.cos (θ + π)
Tactic: rw [← neg_pos, ← Real.cos_add_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
⊢ 0 < Real.cos (θ + π)
have refine_1 : -(π / 2) < θ + π
Tactic: refine Real.cos_pos_of_mem_Ioo ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
refine_1 : -(π / 2) < θ + π
⊢ 0 < Real.cos (θ + π)
have refine_2 : θ + π < π / 2
Tactic: refine Real.cos_pos_of_mem_Ioo ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
⊢ -(π / 2) < θ + π
have linarith : θ + π ≤ -(π / 2) → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
linarith : θ + π ≤ -(π / 2) → 2 / 2 = 1
⊢ -(π / 2) < θ + π
have linarith₁ : θ + π ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
linarith : θ + π ≤ -(π / 2) → 2 / 2 = 1
linarith₁ : θ + π ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
⊢ -(π / 2) < θ + π
have linarith₂ : θ + π ≤ -(π / 2) → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
linarith : θ + π ≤ -(π / 2) → 2 / 2 = 1
linarith₁ : θ + π ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : θ + π ≤ -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₃ : θ + π ≤ -(π / 2) → 2 / 2 = 1
linarith₄ : θ + π ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : θ + π ≤ -(π / 2) → GT.gt (α := ℝ) 2 0
⊢ -(π / 2) < θ + π
have linarith₆ : θ + π ≤ -(π / 2) → 2 * θ - -(1 * π) + 4 * (-π - θ) + (2 * θ + 2 * π - -(1 * π)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
linarith : θ + π ≤ -(π / 2) → 2 / 2 = 1
linarith₁ : θ + π ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : θ + π ≤ -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₃ : θ + π ≤ -(π / 2) → 2 / 2 = 1
linarith₄ : θ + π ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : θ + π ≤ -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₆ : θ + π ≤ -(π / 2) → 2 * θ - -(1 * π) + 4 * (-π - θ) + (2 * θ + 2 * π - -(1 * π)) = 0
⊢ -(π / 2) < θ + π
have linarith₇ : θ + π ≤ -(π / 2) → GT.gt (α := ℝ) 4 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
⊢ θ + π < π / 2
have linarith : π / 2 ≤ θ + π → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
linarith : π / 2 ≤ θ + π → 2 / 2 = 1
⊢ θ + π < π / 2
have linarith₁ : π / 2 ≤ θ + π → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
linarith : π / 2 ≤ θ + π → 2 / 2 = 1
linarith₁ : π / 2 ≤ θ + π → HMul.hMul (α := ℝ) 1 2 = 2
⊢ θ + π < π / 2
have linarith₂ : π / 2 ≤ θ + π → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
linarith : π / 2 ≤ θ + π → 2 / 2 = 1
linarith₁ : π / 2 ≤ θ + π → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π / 2 ≤ θ + π → GT.gt (α := ℝ) 2 0
linarith₃ : π / 2 ≤ θ + π → 2 / 2 = 1
linarith₄ : π / 2 ≤ θ + π → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : π / 2 ≤ θ + π → GT.gt (α := ℝ) 2 0
⊢ θ + π < π / 2
have linarith₆ : π / 2 ≤ θ + π → 2 * θ - -(1 * π) + (1 * π - (2 * θ + 2 * π)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (hypothesis)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
have hcos : Real.cos θ < 0
Tactic: have hcos : Real.cos θ < 0 := by
        rw [← neg_pos, ← Real.cos_add_pi]
        refine Real.cos_pos_of_mem_Ioo ⟨?_, ?_⟩ <;> linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
⊢ θ < 0
have linarith : 0 ≤ θ → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
linarith : 0 ≤ θ → 2 / 2 = 1
⊢ θ < 0
have linarith₁ : 0 ≤ θ → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
linarith : 0 ≤ θ → 2 / 2 = 1
linarith₁ : 0 ≤ θ → HMul.hMul (α := ℝ) 1 2 = 2
⊢ θ < 0
have linarith₂ : 0 ≤ θ → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
linarith : 0 ≤ θ → 2 / 2 = 1
linarith₁ : 0 ≤ θ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 0 ≤ θ → GT.gt (α := ℝ) 2 0
⊢ θ < 0
have linarith₃ : 0 ≤ θ → 2 * θ - -(1 * π) + (-π - θ) + (0 - θ) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (hypothesis)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
have hsin : Real.sin θ < 0
Tactic: have hsin : Real.sin θ < 0 := Real.sin_neg_of_neg_of_neg_pi_lt (by linarith) hθ
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
have neg : -(π / 2) ≤ θ + π
Tactic: rw [if_neg, if_neg, ← Real.sin_add_pi, Real.arcsin_sin, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
neg : -(π / 2) ≤ θ + π
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
have neg₁ : θ + π ≤ π / 2
Tactic: rw [if_neg, if_neg, ← Real.sin_add_pi, Real.arcsin_sin, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
neg : -(π / 2) ≤ θ + π
neg₁ : θ + π ≤ π / 2
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
have neg₂ : ¬0 ≤ Real.sin θ
Tactic: rw [if_neg, if_neg, ← Real.sin_add_pi, Real.arcsin_sin, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
neg : -(π / 2) ≤ θ + π
neg₁ : θ + π ≤ π / 2
neg₂ : ¬0 ≤ Real.sin θ
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
have neg₃ : ¬0 ≤ Real.cos θ
Tactic: rw [if_neg, if_neg, ← Real.sin_add_pi, Real.arcsin_sin, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
⊢ -(π / 2) ≤ θ + π
have linarith : θ + π < -(π / 2) → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
linarith : θ + π < -(π / 2) → 2 / 2 = 1
⊢ -(π / 2) ≤ θ + π
have linarith₁ : θ + π < -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith