awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx₀ : 0 < x
hx₁ : x ≠ 1
H : y = z
⊢ x ^ y = x ^ z
have rw : x ^ z = x ^ z
Tactic: rw [H]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx₀ : 0 < x
hx₁ : x ≠ 1
⊢ x ^ y = x ^ z ↔ y = z
have refine : ∀ (H : x ^ y = x ^ z), y = z
Tactic: refine ⟨fun H ↦ ?_, fun H ↦ by rw [H]⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx₀ : 0 < x
hx₁ : x ≠ 1
H : x ^ y = x ^ z
⊢ y = z
have inl : ∀ (h : x < 1), y = z
Tactic: rcases hx₁.lt_or_gt with h | h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx₀ : 0 < x
hx₁ : x ≠ 1
H : x ^ y = x ^ z
inl : ∀ (h : x < 1), y = z
⊢ y = z
have inr : ∀ (h : 1 < x), y = z
Tactic: rcases hx₁.lt_or_gt with h | h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
h : 1 ≤ x ∧ y ≤ z ∨ 0 < x ∧ x ≤ 1 ∧ z ≤ y
⊢ x ^ y ≤ x ^ z
have inl : ∀ (x1 : 1 ≤ x) (yz : y ≤ z), x ^ y ≤ x ^ z
Tactic: rcases h with ⟨x1, yz⟩ | ⟨x0, x1, zy⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
h : 1 ≤ x ∧ y ≤ z ∨ 0 < x ∧ x ≤ 1 ∧ z ≤ y
inl : ∀ (x1 : 1 ≤ x) (yz : y ≤ z), x ^ y ≤ x ^ z
⊢ x ^ y ≤ x ^ z
have inr : ∀ (x0 : 0 < x) (x1 : x ≤ 1) (zy : z ≤ y), x ^ y ≤ x ^ z
Tactic: rcases h with ⟨x1, yz⟩ | ⟨x0, x1, zy⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
p : Nat.Primes
s : ℂ
hs : 1 < s.re
⊢ -s.re ≠ 0
have linarith : -s.re = 0 → -1 + -(-s.re - 0) + (1 - s.re) = 0
Tactic: linarith only [hs]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
p : Nat.Primes
s : ℂ
hs : 1 < s.re
⊢ ‖HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-s)‖ ≤ 1 / 2
have rw : HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) (-s).re ≤ 1 / 2
Tactic: rw [norm_natCast_cpow_of_re_ne_zero p <| by rw [neg_re]; linarith only [hs]]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
p : Nat.Primes
s : ℂ
hs : 1 < s.re
⊢ -s.re ≤ 0
have linarith : 0 < -s.re → -1 + (0 - -s.re) + (1 - s.re) = 0
Tactic: linarith only [hs]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
p : Nat.Primes
s : ℂ
hs : 1 < s.re
⊢ HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) (-s).re ≤ 1 / 2
have refine : HPow.hPow (α := ℝ) 2 (-s).re ≤ 1 / 2
Tactic: refine (Real.rpow_le_rpow_of_nonpos zero_lt_two (Nat.cast_le.mpr p.prop.two_le) <|
    by rw [neg_re]; linarith only [hs]).trans ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
p : Nat.Primes
s : ℂ
hs : 1 < s.re
⊢ HPow.hPow (α := ℝ) 2 (-s).re ≤ 1 / 2
have rw : HPow.hPow (α := ℝ) 2 (-s).re ≤ HPow.hPow (α := ℝ) (β := ℝ) 2 (-1)
Tactic: rw [one_div, ← Real.rpow_neg_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
p : ℕ
hp : Nat.Prime p
s : ℂ
hs : 1 < s.re
⊢ 1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s) ≠ 0
have refine : ∀ (H : 1 = HPow.hPow (α := ℂ) (↑p : ℂ) (-s)), False
Tactic: refine sub_ne_zero_of_ne fun H ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (hypothesis)
Goal:
p : ℕ
hp : Nat.Prime p
s : ℂ
hs : 1 < s.re
H : 1 = HPow.hPow (α := ℂ) (↑p : ℂ) (-s)
⊢ False
have this : ‖HPow.hPow (α := ℂ) (↑(↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) p hp) : ℕ) : ℂ) (-s)‖ ≤ 1 / 2
Tactic: have := norm_prime_cpow_le_one_half ⟨p, hp⟩ hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (hypothesis)
Goal:
p : ℕ
hp : Nat.Prime p
s : ℂ
hs : 1 < s.re
H : 1 = HPow.hPow (α := ℂ) (↑p : ℂ) (-s)
this : ‖HPow.hPow (α := ℂ) (↑p : ℂ) (-s)‖ ≤ 1 / 2
⊢ False
have this₁ : 1 ≤ 1 / 2
Tactic: rw [← H, norm_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
n : ℕ
hn : 0 < n
w z : ℂ
h : w.re ≤ z.re
⊢ ‖HPow.hPow (α := ℂ) (↑n : ℂ) w‖ ≤ ‖HPow.hPow (α := ℂ) (↑n : ℂ) z‖
have simp_rw : HPow.hPow (α := ℝ) (↑n : ℝ) w.re ≤ HPow.hPow (α := ℝ) (↑n : ℝ) z.re
Tactic: simp_rw [norm_natCast_cpow_of_pos hn]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
n : ℕ
hn : 1 < n
w z : ℂ
⊢ ‖HPow.hPow (α := ℂ) (↑n : ℂ) w‖ ≤ ‖HPow.hPow (α := ℂ) (↑n : ℂ) z‖ ↔ w.re ≤ z.re
have simp_rw : HPow.hPow (α := ℝ) (↑n : ℝ) w.re ≤ HPow.hPow (α := ℝ) (↑n : ℝ) z.re ↔ w.re ≤ z.re
Tactic: simp_rw [norm_natCast_cpow_of_pos (Nat.zero_lt_of_lt hn),
    Real.rpow_le_rpow_left_iff (Nat.one_lt_cast.mpr hn)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
⊢ ‖log (↑n : ℂ)‖ ≤ HPow.hPow (α := ℝ) (↑n : ℝ) ε / ε
have inl : ‖log (↑0 : ℂ)‖ ≤ HPow.hPow (α := ℝ) (↑0 : ℝ) ε / ε
Tactic: rcases n.eq_zero_or_pos with rfl | h
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
inl : ‖log (↑0 : ℂ)‖ ≤ HPow.hPow (α := ℝ) (↑0 : ℝ) ε / ε
⊢ ‖log (↑n : ℂ)‖ ≤ HPow.hPow (α := ℝ) (↑n : ℝ) ε / ε
have inr : ∀ (h : n > 0), ‖log (↑n : ℂ)‖ ≤ HPow.hPow (α := ℝ) (↑n : ℝ) ε / ε
Tactic: rcases n.eq_zero_or_pos with rfl | h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
ε : ℝ
hε : 0 < ε
⊢ ‖log (↑0 : ℂ)‖ ≤ HPow.hPow (α := ℝ) (↑0 : ℝ) ε / ε
have inl : ‖log 0‖ ≤ HPow.hPow (α := ℝ) (↑0 : ℝ) ε / ε
Tactic: rw [Nat.cast_zero, Nat.cast_zero, log_zero, norm_zero, Real.zero_rpow hε.ne', zero_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
ε : ℝ
hε : 0 < ε
inl : ‖log 0‖ ≤ HPow.hPow (α := ℝ) (↑0 : ℝ) ε / ε
⊢ ‖log (↑0 : ℂ)‖ ≤ HPow.hPow (α := ℝ) (↑0 : ℝ) ε / ε
have inl₁ : ‖log 0‖ ≤ HPow.hPow (α := ℝ) 0 ε / ε
Tactic: rw [Nat.cast_zero, Nat.cast_zero, log_zero, norm_zero, Real.zero_rpow hε.ne', zero_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
ε : ℝ
hε : 0 < ε
inl : ‖log 0‖ ≤ HPow.hPow (α := ℝ) (↑0 : ℝ) ε / ε
inl₁ : ‖log 0‖ ≤ HPow.hPow (α := ℝ) 0 ε / ε
⊢ ‖log (↑0 : ℂ)‖ ≤ HPow.hPow (α := ℝ) (↑0 : ℝ) ε / ε
have inl₂ : Norm.norm (E := ℂ) 0 ≤ HPow.hPow (α := ℝ) 0 ε / ε
Tactic: rw [Nat.cast_zero, Nat.cast_zero, log_zero, norm_zero, Real.zero_rpow hε.ne', zero_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
ε : ℝ
hε : 0 < ε
inl : ‖log 0‖ ≤ HPow.hPow (α := ℝ) (↑0 : ℝ) ε / ε
inl₁ : ‖log 0‖ ≤ HPow.hPow (α := ℝ) 0 ε / ε
inl₂ : Norm.norm (E := ℂ) 0 ≤ HPow.hPow (α := ℝ) 0 ε / ε
⊢ ‖log (↑0 : ℂ)‖ ≤ HPow.hPow (α := ℝ) (↑0 : ℝ) ε / ε
have inl₃ : 0 ≤ HPow.hPow (α := ℝ) 0 ε / ε
Tactic: rw [Nat.cast_zero, Nat.cast_zero, log_zero, norm_zero, Real.zero_rpow hε.ne', zero_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
ε : ℝ
hε : 0 < ε
inl : ‖log 0‖ ≤ HPow.hPow (α := ℝ) (↑0 : ℝ) ε / ε
inl₁ : ‖log 0‖ ≤ HPow.hPow (α := ℝ) 0 ε / ε
inl₂ : Norm.norm (E := ℂ) 0 ≤ HPow.hPow (α := ℝ) 0 ε / ε
inl₃ : 0 ≤ HPow.hPow (α := ℝ) 0 ε / ε
⊢ ‖log (↑0 : ℂ)‖ ≤ HPow.hPow (α := ℝ) (↑0 : ℝ) ε / ε
have inl₄ : 0 ≤ 0 / ε
Tactic: rw [Nat.cast_zero, Nat.cast_zero, log_zero, norm_zero, Real.zero_rpow hε.ne', zero_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
ε : ℝ
hε : 0 < ε
inl : ‖log 0‖ ≤ HPow.hPow (α := ℝ) (↑0 : ℝ) ε / ε
inl₁ : ‖log 0‖ ≤ HPow.hPow (α := ℝ) 0 ε / ε
inl₂ : Norm.norm (E := ℂ) 0 ≤ HPow.hPow (α := ℝ) 0 ε / ε
inl₃ : 0 ≤ HPow.hPow (α := ℝ) 0 ε / ε
inl₄ : 0 ≤ 0 / ε
⊢ ‖log (↑0 : ℂ)‖ ≤ HPow.hPow (α := ℝ) (↑0 : ℝ) ε / ε
have inl₅ : LE.le (α := ℝ) 0 0
Tactic: rw [Nat.cast_zero, Nat.cast_zero, log_zero, norm_zero, Real.zero_rpow hε.ne', zero_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
h : n > 0
⊢ ‖log (↑n : ℂ)‖ ≤ HPow.hPow (α := ℝ) (↑n : ℝ) ε / ε
have inr : Real.log (↑n : ℝ) ≤ HPow.hPow (α := ℝ) (↑n : ℝ) ε / ε
Tactic: rw [← natCast_log, norm_real, norm_of_nonneg <| Real.log_nonneg <| by
    exact_mod_cast Nat.one_le_of_lt h.lt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
⊢ √x = x ^ (1 / 2)
have inl : ∀ (h : 0 ≤ x), √x = x ^ (1 / 2)
Tactic: obtain h | h := le_or_gt 0 x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
inl : ∀ (h : 0 ≤ x), √x = x ^ (1 / 2)
⊢ √x = x ^ (1 / 2)
have inr : ∀ (h : x < 0), √x = x ^ (1 / 2)
Tactic: obtain h | h := le_or_gt 0 x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
h : 0 ≤ x
⊢ √x = x ^ (1 / 2)
have inl : x = x ^ (1 / 2 * (↑2 : ℝ))
Tactic: rw [← mul_self_inj_of_nonneg (sqrt_nonneg _) (rpow_nonneg h _), mul_self_sqrt h, ← sq,
      ← rpow_natCast, ← rpow_mul h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (hypothesis)
Goal:
x : ℝ
h : x < 0
⊢ √x = x ^ (1 / 2)
have this : 1 / 2 * π = π / 2
Tactic: have : 1 / (2 : ℝ) * π = π / (2 : ℝ) := by ring
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
h : x < 0
this : 1 / 2 * π = π / 2
⊢ √x = x ^ (1 / 2)
have inr : 0 = x ^ (1 / 2)
Tactic: rw [sqrt_eq_zero_of_nonpos h.le, rpow_def_of_neg h, this, cos_pi_div_two, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
h : x < 0
this : 1 / 2 * π = π / 2
inr : 0 = x ^ (1 / 2)
⊢ √x = x ^ (1 / 2)
have inr₁ : 0 = rexp (log x * (1 / 2)) * cos (1 / 2 * π)
Tactic: rw [sqrt_eq_zero_of_nonpos h.le, rpow_def_of_neg h, this, cos_pi_div_two, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
h : x < 0
this : 1 / 2 * π = π / 2
inr : 0 = x ^ (1 / 2)
inr₁ : 0 = rexp (log x * (1 / 2)) * cos (1 / 2 * π)
⊢ √x = x ^ (1 / 2)
have inr₂ : 0 = rexp (log x * (1 / 2)) * cos (π / 2)
Tactic: rw [sqrt_eq_zero_of_nonpos h.le, rpow_def_of_neg h, this, cos_pi_div_two, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
h : x < 0
this : 1 / 2 * π = π / 2
inr : 0 = x ^ (1 / 2)
inr₁ : 0 = rexp (log x * (1 / 2)) * cos (1 / 2 * π)
inr₂ : 0 = rexp (log x * (1 / 2)) * cos (π / 2)
⊢ √x = x ^ (1 / 2)
have inr₃ : 0 = rexp (log x * (1 / 2)) * 0
Tactic: rw [sqrt_eq_zero_of_nonpos h.le, rpow_def_of_neg h, this, cos_pi_div_two, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
h : x < 0
this : 1 / 2 * π = π / 2
inr : 0 = x ^ (1 / 2)
inr₁ : 0 = rexp (log x * (1 / 2)) * cos (1 / 2 * π)
inr₂ : 0 = rexp (log x * (1 / 2)) * cos (π / 2)
inr₃ : 0 = rexp (log x * (1 / 2)) * 0
⊢ √x = x ^ (1 / 2)
have inr₄ : Eq (α := ℝ) 0 0
Tactic: rw [sqrt_eq_zero_of_nonpos h.le, rpow_def_of_neg h, this, cos_pi_div_two, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x r : ℝ
hx : 0 ≤ x
⊢ x ^ (r / 2) = √x ^ r
have rw : x ^ (r / 2) = x ^ (1 / 2 * r)
Tactic: rw [sqrt_eq_rpow, ← rpow_mul hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x r : ℝ
hx : 0 ≤ x
⊢ x ^ (r / 2) = x ^ (1 / 2 * r)
have e_a : r / 2 = 1 / 2 * r
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℂ
⊢ (HPow.hPow (β := ℂ) x 2⁻¹).re = √((‖x‖ + x.re) / 2)
have hx : 0 ≤ ‖x‖
Tactic: rw [← ofReal_ofNat, ← ofReal_inv, cpow_ofReal_re, ← div_eq_mul_inv, ← one_div,
    ← Real.sqrt_eq_rpow, cos_half, ← sqrt_mul, ← mul_div_assoc, mul_add, mul_one, norm_mul_cos_arg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℂ
hx : 0 ≤ ‖x‖
⊢ (HPow.hPow (β := ℂ) x 2⁻¹).re = √((‖x‖ + x.re) / 2)
have hl : -π ≤ x.arg
Tactic: rw [← ofReal_ofNat, ← ofReal_inv, cpow_ofReal_re, ← div_eq_mul_inv, ← one_div,
    ← Real.sqrt_eq_rpow, cos_half, ← sqrt_mul, ← mul_div_assoc, mul_add, mul_one, norm_mul_cos_arg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℂ
hx : 0 ≤ ‖x‖
hl : -π ≤ x.arg
⊢ (HPow.hPow (β := ℂ) x 2⁻¹).re = √((‖x‖ + x.re) / 2)
have hr : x.arg ≤ π
Tactic: rw [← ofReal_ofNat, ← ofReal_inv, cpow_ofReal_re, ← div_eq_mul_inv, ← one_div,
    ← Real.sqrt_eq_rpow, cos_half, ← sqrt_mul, ← mul_div_assoc, mul_add, mul_one, norm_mul_cos_arg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℂ
hx : 0 ≤ x.im
⊢ (HPow.hPow (β := ℂ) x 2⁻¹).im = √((‖x‖ - x.re) / 2)
have hl : 0 ≤ x.arg
Tactic: rw [← ofReal_ofNat, ← ofReal_inv, cpow_ofReal_im, ← div_eq_mul_inv, ← one_div,
    ← Real.sqrt_eq_rpow, sin_half_eq_sqrt, ← sqrt_mul (norm_nonneg _), ← mul_div_assoc, mul_sub,
    mul_one, norm_mul_cos_arg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℂ
hx : 0 ≤ x.im
hl : 0 ≤ x.arg
⊢ (HPow.hPow (β := ℂ) x 2⁻¹).im = √((‖x‖ - x.re) / 2)
have hr : x.arg ≤ 2 * π
Tactic: rw [← ofReal_ofNat, ← ofReal_inv, cpow_ofReal_im, ← div_eq_mul_inv, ← one_div,
    ← Real.sqrt_eq_rpow, sin_half_eq_sqrt, ← sqrt_mul (norm_nonneg _), ← mul_div_assoc, mul_sub,
    mul_one, norm_mul_cos_arg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℂ
hx : 0 ≤ x.im
⊢ x.arg ≤ 2 * π
have linarith : 2 * π < x.arg → 2 * π - x.arg + (0 - π) + (x.arg - π) = 0
Tactic: linarith [pi_pos, arg_le_pi x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℂ
hx : x.im < 0
⊢ (HPow.hPow (β := ℂ) x 2⁻¹).im = -√((‖x‖ - x.re) / 2)
have hl : -(2 * π) ≤ x.arg
Tactic: rw [← ofReal_ofNat, ← ofReal_inv, cpow_ofReal_im, ← div_eq_mul_inv, ← one_div,
    ← Real.sqrt_eq_rpow, sin_half_eq_neg_sqrt, mul_neg, ← sqrt_mul (norm_nonneg _),
    ← mul_div_assoc, mul_sub, mul_one, norm_mul_cos_arg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℂ
hx : x.im < 0
hl : -(2 * π) ≤ x.arg
⊢ (HPow.hPow (β := ℂ) x 2⁻¹).im = -√((‖x‖ - x.re) / 2)
have hr : x.arg ≤ 0
Tactic: rw [← ofReal_ofNat, ← ofReal_inv, cpow_ofReal_im, ← div_eq_mul_inv, ← one_div,
    ← Real.sqrt_eq_rpow, sin_half_eq_neg_sqrt, mul_neg, ← sqrt_mul (norm_nonneg _),
    ← mul_div_assoc, mul_sub, mul_one, norm_mul_cos_arg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℂ
hx : x.im < 0
⊢ -(2 * π) ≤ x.arg
have linarith : x.arg < -(2 * π) → x.arg - -(2 * π) + (0 - π) + (-π - x.arg) = 0
Tactic: linarith [pi_pos, neg_pi_lt_arg x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℂ
⊢ |(HPow.hPow (β := ℂ) x 2⁻¹).im| = √((‖x‖ - x.re) / 2)
have rw : |(x ^ (↑2 : ℂ)⁻¹).im| = √((‖x‖ - x.re) / 2)
Tactic: rw [← ofReal_ofNat, ← ofReal_inv, cpow_ofReal_im, ← div_eq_mul_inv, ← one_div,
    ← Real.sqrt_eq_rpow, abs_mul, abs_of_nonneg (sqrt_nonneg _), abs_sin_half,
    ← sqrt_mul (norm_nonneg _), ← mul_div_assoc, mul_sub, mul_one, norm_mul_cos_arg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℂ
rw : |(x ^ (↑2 : ℂ)⁻¹).im| = √((‖x‖ - x.re) / 2)
⊢ |(HPow.hPow (β := ℂ) x 2⁻¹).im| = √((‖x‖ - x.re) / 2)
have rw₁ : |(x ^ (↑2⁻¹ : ℂ)).im| = √((‖x‖ - x.re) / 2)
Tactic: rw [← ofReal_ofNat, ← ofReal_inv, cpow_ofReal_im, ← div_eq_mul_inv, ← one_div,
    ← Real.sqrt_eq_rpow, abs_mul, abs_of_nonneg (sqrt_nonneg _), abs_sin_half,
    ← sqrt_mul (norm_nonneg _), ← mul_div_assoc, mul_sub, mul_one, norm_mul_cos_arg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℂ
rw : |(x ^ (↑2 : ℂ)⁻¹).im| = √((‖x‖ - x.re) / 2)
rw₁ : |(x ^ (↑2⁻¹ : ℂ)).im| = √((‖x‖ - x.re) / 2)
⊢ |(HPow.hPow (β := ℂ) x 2⁻¹).im| = √((‖x‖ - x.re) / 2)
have rw₂ : |HPow.hPow (β := ℝ) ‖x‖ 2⁻¹ * Real.sin (x.arg * 2⁻¹)| = √((‖x‖ - x.re) / 2)
Tactic: rw [← ofReal_ofNat, ← ofReal_inv, cpow_ofReal_im, ← div_eq_mul_inv, ← one_div,
    ← Real.sqrt_eq_rpow, abs_mul, abs_of_nonneg (sqrt_nonneg _), abs_sin_half,
    ← sqrt_mul (norm_nonneg _), ← mul_div_assoc, mul_sub, mul_one, norm_mul_cos_arg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℂ
rw : |(x ^ (↑2 : ℂ)⁻¹).im| = √((‖x‖ - x.re) / 2)
rw₁ : |(x ^ (↑2⁻¹ : ℂ)).im| = √((‖x‖ - x.re) / 2)
rw₂ : |HPow.hPow (β := ℝ) ‖x‖ 2⁻¹ * Real.sin (x.arg * 2⁻¹)| = √((‖x‖ - x.re) / 2)
⊢ |(HPow.hPow (β := ℂ) x 2⁻¹).im| = √((‖x‖ - x.re) / 2)
have rw₃ : |HPow.hPow (β := ℝ) ‖x‖ 2⁻¹ * Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
Tactic: rw [← ofReal_ofNat, ← ofReal_inv, cpow_ofReal_im, ← div_eq_mul_inv, ← one_div,
    ← Real.sqrt_eq_rpow, abs_mul, abs_of_nonneg (sqrt_nonneg _), abs_sin_half,
    ← sqrt_mul (norm_nonneg _), ← mul_div_assoc, mul_sub, mul_one, norm_mul_cos_arg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℂ
rw : |(x ^ (↑2 : ℂ)⁻¹).im| = √((‖x‖ - x.re) / 2)
rw₁ : |(x ^ (↑2⁻¹ : ℂ)).im| = √((‖x‖ - x.re) / 2)
rw₂ : |HPow.hPow (β := ℝ) ‖x‖ 2⁻¹ * Real.sin (x.arg * 2⁻¹)| = √((‖x‖ - x.re) / 2)
rw₃ : |HPow.hPow (β := ℝ) ‖x‖ 2⁻¹ * Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
⊢ |(HPow.hPow (β := ℂ) x 2⁻¹).im| = √((‖x‖ - x.re) / 2)
have rw₄ : |‖x‖ ^ HDiv.hDiv (α := ℝ) 1 2 * Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
Tactic: rw [← ofReal_ofNat, ← ofReal_inv, cpow_ofReal_im, ← div_eq_mul_inv, ← one_div,
    ← Real.sqrt_eq_rpow, abs_mul, abs_of_nonneg (sqrt_nonneg _), abs_sin_half,
    ← sqrt_mul (norm_nonneg _), ← mul_div_assoc, mul_sub, mul_one, norm_mul_cos_arg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℂ
rw : |(x ^ (↑2 : ℂ)⁻¹).im| = √((‖x‖ - x.re) / 2)
rw₁ : |(x ^ (↑2⁻¹ : ℂ)).im| = √((‖x‖ - x.re) / 2)
rw₂ : |HPow.hPow (β := ℝ) ‖x‖ 2⁻¹ * Real.sin (x.arg * 2⁻¹)| = √((‖x‖ - x.re) / 2)
rw₃ : |HPow.hPow (β := ℝ) ‖x‖ 2⁻¹ * Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
rw₄ : |‖x‖ ^ HDiv.hDiv (α := ℝ) 1 2 * Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
⊢ |(HPow.hPow (β := ℂ) x 2⁻¹).im| = √((‖x‖ - x.re) / 2)
have rw₅ : |√‖x‖ * Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
Tactic: rw [← ofReal_ofNat, ← ofReal_inv, cpow_ofReal_im, ← div_eq_mul_inv, ← one_div,
    ← Real.sqrt_eq_rpow, abs_mul, abs_of_nonneg (sqrt_nonneg _), abs_sin_half,
    ← sqrt_mul (norm_nonneg _), ← mul_div_assoc, mul_sub, mul_one, norm_mul_cos_arg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℂ
rw : |(x ^ (↑2 : ℂ)⁻¹).im| = √((‖x‖ - x.re) / 2)
rw₁ : |(x ^ (↑2⁻¹ : ℂ)).im| = √((‖x‖ - x.re) / 2)
rw₂ : |HPow.hPow (β := ℝ) ‖x‖ 2⁻¹ * Real.sin (x.arg * 2⁻¹)| = √((‖x‖ - x.re) / 2)
rw₃ : |HPow.hPow (β := ℝ) ‖x‖ 2⁻¹ * Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
rw₄ : |‖x‖ ^ HDiv.hDiv (α := ℝ) 1 2 * Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
rw₅ : |√‖x‖ * Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
⊢ |(HPow.hPow (β := ℂ) x 2⁻¹).im| = √((‖x‖ - x.re) / 2)
have rw₆ : |√‖x‖| * |Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
Tactic: rw [← ofReal_ofNat, ← ofReal_inv, cpow_ofReal_im, ← div_eq_mul_inv, ← one_div,
    ← Real.sqrt_eq_rpow, abs_mul, abs_of_nonneg (sqrt_nonneg _), abs_sin_half,
    ← sqrt_mul (norm_nonneg _), ← mul_div_assoc, mul_sub, mul_one, norm_mul_cos_arg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℂ
rw : |(x ^ (↑2 : ℂ)⁻¹).im| = √((‖x‖ - x.re) / 2)
rw₁ : |(x ^ (↑2⁻¹ : ℂ)).im| = √((‖x‖ - x.re) / 2)
rw₂ : |HPow.hPow (β := ℝ) ‖x‖ 2⁻¹ * Real.sin (x.arg * 2⁻¹)| = √((‖x‖ - x.re) / 2)
rw₃ : |HPow.hPow (β := ℝ) ‖x‖ 2⁻¹ * Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
rw₄ : |‖x‖ ^ HDiv.hDiv (α := ℝ) 1 2 * Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
rw₅ : |√‖x‖ * Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
rw₆ : |√‖x‖| * |Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
⊢ |(HPow.hPow (β := ℂ) x 2⁻¹).im| = √((‖x‖ - x.re) / 2)
have rw₇ : √‖x‖ * |Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
Tactic: rw [← ofReal_ofNat, ← ofReal_inv, cpow_ofReal_im, ← div_eq_mul_inv, ← one_div,
    ← Real.sqrt_eq_rpow, abs_mul, abs_of_nonneg (sqrt_nonneg _), abs_sin_half,
    ← sqrt_mul (norm_nonneg _), ← mul_div_assoc, mul_sub, mul_one, norm_mul_cos_arg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℂ
rw : |(x ^ (↑2 : ℂ)⁻¹).im| = √((‖x‖ - x.re) / 2)
rw₁ : |(x ^ (↑2⁻¹ : ℂ)).im| = √((‖x‖ - x.re) / 2)
rw₂ : |HPow.hPow (β := ℝ) ‖x‖ 2⁻¹ * Real.sin (x.arg * 2⁻¹)| = √((‖x‖ - x.re) / 2)
rw₃ : |HPow.hPow (β := ℝ) ‖x‖ 2⁻¹ * Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
rw₄ : |‖x‖ ^ HDiv.hDiv (α := ℝ) 1 2 * Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
rw₅ : |√‖x‖ * Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
rw₆ : |√‖x‖| * |Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
rw₇ : √‖x‖ * |Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
⊢ |(HPow.hPow (β := ℂ) x 2⁻¹).im| = √((‖x‖ - x.re) / 2)
have rw₈ : √‖x‖ * √((1 - Real.cos x.arg) / 2) = √((‖x‖ - x.re) / 2)
Tactic: rw [← ofReal_ofNat, ← ofReal_inv, cpow_ofReal_im, ← div_eq_mul_inv, ← one_div,
    ← Real.sqrt_eq_rpow, abs_mul, abs_of_nonneg (sqrt_nonneg _), abs_sin_half,
    ← sqrt_mul (norm_nonneg _), ← mul_div_assoc, mul_sub, mul_one, norm_mul_cos_arg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℂ
rw : |(x ^ (↑2 : ℂ)⁻¹).im| = √((‖x‖ - x.re) / 2)
rw₁ : |(x ^ (↑2⁻¹ : ℂ)).im| = √((‖x‖ - x.re) / 2)
rw₂ : |HPow.hPow (β := ℝ) ‖x‖ 2⁻¹ * Real.sin (x.arg * 2⁻¹)| = √((‖x‖ - x.re) / 2)
rw₃ : |HPow.hPow (β := ℝ) ‖x‖ 2⁻¹ * Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
rw₄ : |‖x‖ ^ HDiv.hDiv (α := ℝ) 1 2 * Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
rw₅ : |√‖x‖ * Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
rw₆ : |√‖x‖| * |Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
rw₇ : √‖x‖ * |Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
rw₈ : √‖x‖ * √((1 - Real.cos x.arg) / 2) = √((‖x‖ - x.re) / 2)
⊢ |(HPow.hPow (β := ℂ) x 2⁻¹).im| = √((‖x‖ - x.re) / 2)
have rw₉ : √(‖x‖ * ((1 - Real.cos x.arg) / 2)) = √((‖x‖ - x.re) / 2)
Tactic: rw [← ofReal_ofNat, ← ofReal_inv, cpow_ofReal_im, ← div_eq_mul_inv, ← one_div,
    ← Real.sqrt_eq_rpow, abs_mul, abs_of_nonneg (sqrt_nonneg _), abs_sin_half,
    ← sqrt_mul (norm_nonneg _), ← mul_div_assoc, mul_sub, mul_one, norm_mul_cos_arg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℂ
rw : |(x ^ (↑2 : ℂ)⁻¹).im| = √((‖x‖ - x.re) / 2)
rw₁ : |(x ^ (↑2⁻¹ : ℂ)).im| = √((‖x‖ - x.re) / 2)
rw₂ : |HPow.hPow (β := ℝ) ‖x‖ 2⁻¹ * Real.sin (x.arg * 2⁻¹)| = √((‖x‖ - x.re) / 2)
rw₃ : |HPow.hPow (β := ℝ) ‖x‖ 2⁻¹ * Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
rw₄ : |‖x‖ ^ HDiv.hDiv (α := ℝ) 1 2 * Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
rw₅ : |√‖x‖ * Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
rw₆ : |√‖x‖| * |Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
rw₇ : √‖x‖ * |Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
rw₈ : √‖x‖ * √((1 - Real.cos x.arg) / 2) = √((‖x‖ - x.re) / 2)
rw₉ : √(‖x‖ * ((1 - Real.cos x.arg) / 2)) = √((‖x‖ - x.re) / 2)
⊢ |(HPow.hPow (β := ℂ) x 2⁻¹).im| = √((‖x‖ - x.re) / 2)
have rw₁₀ : √(‖x‖ * (1 - Real.cos x.arg) / 2) = √((‖x‖ - x.re) / 2)
Tactic: rw [← ofReal_ofNat, ← ofReal_inv, cpow_ofReal_im, ← div_eq_mul_inv, ← one_div,
    ← Real.sqrt_eq_rpow, abs_mul, abs_of_nonneg (sqrt_nonneg _), abs_sin_half,
    ← sqrt_mul (norm_nonneg _), ← mul_div_assoc, mul_sub, mul_one, norm_mul_cos_arg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℂ
rw : |(x ^ (↑2 : ℂ)⁻¹).im| = √((‖x‖ - x.re) / 2)
rw₁ : |(x ^ (↑2⁻¹ : ℂ)).im| = √((‖x‖ - x.re) / 2)
rw₂ : |HPow.hPow (β := ℝ) ‖x‖ 2⁻¹ * Real.sin (x.arg * 2⁻¹)| = √((‖x‖ - x.re) / 2)
rw₃ : |HPow.hPow (β := ℝ) ‖x‖ 2⁻¹ * Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
rw₄ : |‖x‖ ^ HDiv.hDiv (α := ℝ) 1 2 * Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
rw₅ : |√‖x‖ * Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
rw₆ : |√‖x‖| * |Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
rw₇ : √‖x‖ * |Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
rw₈ : √‖x‖ * √((1 - Real.cos x.arg) / 2) = √((‖x‖ - x.re) / 2)
rw₉ : √(‖x‖ * ((1 - Real.cos x.arg) / 2)) = √((‖x‖ - x.re) / 2)
rw₁₀ : √(‖x‖ * (1 - Real.cos x.arg) / 2) = √((‖x‖ - x.re) / 2)
⊢ |(HPow.hPow (β := ℂ) x 2⁻¹).im| = √((‖x‖ - x.re) / 2)
have rw₁₁ : √((‖x‖ * 1 - ‖x‖ * Real.cos x.arg) / 2) = √((‖x‖ - x.re) / 2)
Tactic: rw [← ofReal_ofNat, ← ofReal_inv, cpow_ofReal_im, ← div_eq_mul_inv, ← one_div,
    ← Real.sqrt_eq_rpow, abs_mul, abs_of_nonneg (sqrt_nonneg _), abs_sin_half,
    ← sqrt_mul (norm_nonneg _), ← mul_div_assoc, mul_sub, mul_one, norm_mul_cos_arg]