awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z w : ℂ
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ)
        ((normSq : (a : ℂ) → ℝ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) : ℝ) +
      2 * (HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ)).re ≤
    HAdd.hAdd (α := ℝ) (β := ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ)
        ((normSq : (a : ℂ) → ℝ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) : ℝ) +
      2 * √((normSq : (a : ℂ) → ℝ) (HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ)))
have bc : (HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ)).re ≤
  √((normSq : (a : ℂ) → ℝ) (HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ)))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
⊢ ‖-z‖ = ‖z‖
have rw : √((normSq : (a : ℂ) → ℝ) (-z)) = ‖z‖
Tactic: rw [Complex.norm_def, norm_def, normSq_neg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
rw : √((normSq : (a : ℂ) → ℝ) (-z)) = ‖z‖
⊢ ‖-z‖ = ‖z‖
have rw₁ : √((normSq : (a : ℂ) → ℝ) (-z)) = √((normSq : (a : ℂ) → ℝ) z)
Tactic: rw [Complex.norm_def, norm_def, normSq_neg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
rw : √((normSq : (a : ℂ) → ℝ) (-z)) = ‖z‖
rw₁ : √((normSq : (a : ℂ) → ℝ) (-z)) = √((normSq : (a : ℂ) → ℝ) z)
⊢ ‖-z‖ = ‖z‖
have rw₂ : √((normSq : (a : ℂ) → ℝ) z) = √((normSq : (a : ℂ) → ℝ) z)
Tactic: rw [Complex.norm_def, norm_def, normSq_neg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z w : ℂ
⊢ ‖z * w‖ = ‖z‖ * ‖w‖
have rw : √((normSq : (a : ℂ) → ℝ) (z * w)) = ‖z‖ * ‖w‖
Tactic: rw [norm_def, norm_def, norm_def, normSq_mul, Real.sqrt_mul (normSq_nonneg _)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z w : ℂ
rw : √((normSq : (a : ℂ) → ℝ) (z * w)) = ‖z‖ * ‖w‖
⊢ ‖z * w‖ = ‖z‖ * ‖w‖
have rw₁ : √((normSq : (a : ℂ) → ℝ) (z * w)) = √((normSq : (a : ℂ) → ℝ) z) * ‖w‖
Tactic: rw [norm_def, norm_def, norm_def, normSq_mul, Real.sqrt_mul (normSq_nonneg _)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z w : ℂ
rw : √((normSq : (a : ℂ) → ℝ) (z * w)) = ‖z‖ * ‖w‖
rw₁ : √((normSq : (a : ℂ) → ℝ) (z * w)) = √((normSq : (a : ℂ) → ℝ) z) * ‖w‖
⊢ ‖z * w‖ = ‖z‖ * ‖w‖
have rw₂ : √((normSq : (a : ℂ) → ℝ) (z * w)) = √((normSq : (a : ℂ) → ℝ) z) * √((normSq : (a : ℂ) → ℝ) w)
Tactic: rw [norm_def, norm_def, norm_def, normSq_mul, Real.sqrt_mul (normSq_nonneg _)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z w : ℂ
rw : √((normSq : (a : ℂ) → ℝ) (z * w)) = ‖z‖ * ‖w‖
rw₁ : √((normSq : (a : ℂ) → ℝ) (z * w)) = √((normSq : (a : ℂ) → ℝ) z) * ‖w‖
rw₂ : √((normSq : (a : ℂ) → ℝ) (z * w)) = √((normSq : (a : ℂ) → ℝ) z) * √((normSq : (a : ℂ) → ℝ) w)
⊢ ‖z * w‖ = ‖z‖ * ‖w‖
have rw₃ : √(HMul.hMul (α := ℝ) (β := ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ) ((normSq : (a : ℂ) → ℝ) w : ℝ)) =
  √((normSq : (a : ℂ) → ℝ) z) * √((normSq : (a : ℂ) → ℝ) w)
Tactic: rw [norm_def, norm_def, norm_def, normSq_mul, Real.sqrt_mul (normSq_nonneg _)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z w : ℂ
rw : √((normSq : (a : ℂ) → ℝ) (z * w)) = ‖z‖ * ‖w‖
rw₁ : √((normSq : (a : ℂ) → ℝ) (z * w)) = √((normSq : (a : ℂ) → ℝ) z) * ‖w‖
rw₂ : √((normSq : (a : ℂ) → ℝ) (z * w)) = √((normSq : (a : ℂ) → ℝ) z) * √((normSq : (a : ℂ) → ℝ) w)
rw₃ :
  √(HMul.hMul (α := ℝ) (β := ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ) ((normSq : (a : ℂ) → ℝ) w : ℝ)) =
    √((normSq : (a : ℂ) → ℝ) z) * √((normSq : (a : ℂ) → ℝ) w)
⊢ ‖z * w‖ = ‖z‖ * ‖w‖
have rw₄ : √((normSq : (a : ℂ) → ℝ) z) * √((normSq : (a : ℂ) → ℝ) w) = √((normSq : (a : ℂ) → ℝ) z) * √((normSq : (a : ℂ) → ℝ) w)
Tactic: rw [norm_def, norm_def, norm_def, normSq_mul, Real.sqrt_mul (normSq_nonneg _)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z w : ℂ
⊢ ‖z / w‖ = ‖z‖ / ‖w‖
have rw : √((normSq : (a : ℂ) → ℝ) (z / w)) = ‖z‖ / ‖w‖
Tactic: rw [norm_def, norm_def, norm_def, normSq_div, Real.sqrt_div (normSq_nonneg _)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z w : ℂ
rw : √((normSq : (a : ℂ) → ℝ) (z / w)) = ‖z‖ / ‖w‖
⊢ ‖z / w‖ = ‖z‖ / ‖w‖
have rw₁ : √((normSq : (a : ℂ) → ℝ) (z / w)) = √((normSq : (a : ℂ) → ℝ) z) / ‖w‖
Tactic: rw [norm_def, norm_def, norm_def, normSq_div, Real.sqrt_div (normSq_nonneg _)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z w : ℂ
rw : √((normSq : (a : ℂ) → ℝ) (z / w)) = ‖z‖ / ‖w‖
rw₁ : √((normSq : (a : ℂ) → ℝ) (z / w)) = √((normSq : (a : ℂ) → ℝ) z) / ‖w‖
⊢ ‖z / w‖ = ‖z‖ / ‖w‖
have rw₂ : √((normSq : (a : ℂ) → ℝ) (z / w)) = √((normSq : (a : ℂ) → ℝ) z) / √((normSq : (a : ℂ) → ℝ) w)
Tactic: rw [norm_def, norm_def, norm_def, normSq_div, Real.sqrt_div (normSq_nonneg _)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z w : ℂ
rw : √((normSq : (a : ℂ) → ℝ) (z / w)) = ‖z‖ / ‖w‖
rw₁ : √((normSq : (a : ℂ) → ℝ) (z / w)) = √((normSq : (a : ℂ) → ℝ) z) / ‖w‖
rw₂ : √((normSq : (a : ℂ) → ℝ) (z / w)) = √((normSq : (a : ℂ) → ℝ) z) / √((normSq : (a : ℂ) → ℝ) w)
⊢ ‖z / w‖ = ‖z‖ / ‖w‖
have rw₃ : √(HDiv.hDiv (α := ℝ) (β := ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ) ((normSq : (a : ℂ) → ℝ) w : ℝ)) =
  √((normSq : (a : ℂ) → ℝ) z) / √((normSq : (a : ℂ) → ℝ) w)
Tactic: rw [norm_def, norm_def, norm_def, normSq_div, Real.sqrt_div (normSq_nonneg _)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z w : ℂ
rw : √((normSq : (a : ℂ) → ℝ) (z / w)) = ‖z‖ / ‖w‖
rw₁ : √((normSq : (a : ℂ) → ℝ) (z / w)) = √((normSq : (a : ℂ) → ℝ) z) / ‖w‖
rw₂ : √((normSq : (a : ℂ) → ℝ) (z / w)) = √((normSq : (a : ℂ) → ℝ) z) / √((normSq : (a : ℂ) → ℝ) w)
rw₃ :
  √(HDiv.hDiv (α := ℝ) (β := ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ) ((normSq : (a : ℂ) → ℝ) w : ℝ)) =
    √((normSq : (a : ℂ) → ℝ) z) / √((normSq : (a : ℂ) → ℝ) w)
⊢ ‖z / w‖ = ‖z‖ / ‖w‖
have rw₄ : √((normSq : (a : ℂ) → ℝ) z) / √((normSq : (a : ℂ) → ℝ) w) = √((normSq : (a : ℂ) → ℝ) z) / √((normSq : (a : ℂ) → ℝ) w)
Tactic: rw [norm_def, norm_def, norm_def, normSq_div, Real.sqrt_div (normSq_nonneg _)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
r : ℝ
⊢ ‖(↑r : ℂ)‖₊ = ‖r‖₊
have a : (↑‖(↑r : ℂ)‖₊ : ℝ) = (↑‖r‖₊ : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
n : ℤ
⊢ norm (E := ℂ) (↑n : ℂ) = |(↑n : ℝ)|
have rw : ‖(↑(↑n : ℝ) : ℂ)‖ = |(↑n : ℝ)|
Tactic: rw [← ofReal_intCast, norm_real, Real.norm_eq_abs]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
n : ℤ
rw : ‖(↑(↑n : ℝ) : ℂ)‖ = |(↑n : ℝ)|
⊢ norm (E := ℂ) (↑n : ℂ) = |(↑n : ℝ)|
have rw₁ : norm (E := ℝ) (↑n : ℝ) = |(↑n : ℝ)|
Tactic: rw [← ofReal_intCast, norm_real, Real.norm_eq_abs]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
n : ℤ
rw : ‖(↑(↑n : ℝ) : ℂ)‖ = |(↑n : ℝ)|
rw₁ : norm (E := ℝ) (↑n : ℝ) = |(↑n : ℝ)|
⊢ norm (E := ℂ) (↑n : ℂ) = |(↑n : ℝ)|
have rw₂ : Eq (α := ℝ) |(↑n : ℝ)| |(↑n : ℝ)|
Tactic: rw [← ofReal_intCast, norm_real, Real.norm_eq_abs]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
n : ℤ
hn : 0 ≤ n
⊢ norm (E := ℂ) (↑n : ℂ) = (↑n : ℝ)
have rw : Eq (α := ℝ) |(↑n : ℝ)| (↑n : ℝ)
Tactic: rw [norm_intCast, ← Int.cast_abs, abs_of_nonneg hn]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
n : ℤ
hn : 0 ≤ n
rw : Eq (α := ℝ) |(↑n : ℝ)| (↑n : ℝ)
⊢ norm (E := ℂ) (↑n : ℂ) = (↑n : ℝ)
have rw₁ : Eq (α := ℝ) (↑|n| : ℝ) (↑n : ℝ)
Tactic: rw [norm_intCast, ← Int.cast_abs, abs_of_nonneg hn]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
n : ℤ
hn : 0 ≤ n
rw : Eq (α := ℝ) |(↑n : ℝ)| (↑n : ℝ)
rw₁ : Eq (α := ℝ) (↑|n| : ℝ) (↑n : ℝ)
⊢ norm (E := ℂ) (↑n : ℂ) = (↑n : ℝ)
have rw₂ : Eq (α := ℝ) (↑n : ℝ) (↑n : ℝ)
Tactic: rw [norm_intCast, ← Int.cast_abs, abs_of_nonneg hn]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
q : ℚ≥0
⊢ nnnorm (E := ℂ) (↑q : ℂ) = (↑q : NNReal)
have simp : NNReal.mk (↑q : ℝ) sorry = (↑q : NNReal)
Tactic: simp [nnnorm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
x : ℂ
⊢ LT.lt (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) x : ℝ) ↔ 1 < ‖x‖
have rw : LT.lt (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) x : ℝ) ↔ 1 < HPow.hPow (β := ℕ) ‖x‖ 2
Tactic: rw [← one_lt_sq_iff₀ (norm_nonneg _), normSq_eq_norm_sq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
x : ℂ
rw : LT.lt (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) x : ℝ) ↔ 1 < HPow.hPow (β := ℕ) ‖x‖ 2
⊢ LT.lt (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) x : ℝ) ↔ 1 < ‖x‖
have rw₁ : 1 < HPow.hPow (β := ℕ) ‖x‖ 2 ↔ 1 < HPow.hPow (β := ℕ) ‖x‖ 2
Tactic: rw [← one_lt_sq_iff₀ (norm_nonneg _), normSq_eq_norm_sq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
x : ℂ
⊢ LE.le (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) x : ℝ) ↔ 1 ≤ ‖x‖
have rw : LE.le (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) x : ℝ) ↔ 1 ≤ HPow.hPow (β := ℕ) ‖x‖ 2
Tactic: rw [← one_le_sq_iff₀ (norm_nonneg _), normSq_eq_norm_sq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
x : ℂ
rw : LE.le (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) x : ℝ) ↔ 1 ≤ HPow.hPow (β := ℕ) ‖x‖ 2
⊢ LE.le (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) x : ℝ) ↔ 1 ≤ ‖x‖
have rw₁ : 1 ≤ HPow.hPow (β := ℕ) ‖x‖ 2 ↔ 1 ≤ HPow.hPow (β := ℕ) ‖x‖ 2
Tactic: rw [← one_le_sq_iff₀ (norm_nonneg _), normSq_eq_norm_sq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
⊢ HPow.hPow (β := ℕ) ‖z‖ 2 - HPow.hPow (β := ℕ) z.re 2 = HPow.hPow (β := ℕ) z.im 2
have rw : HSub.hSub (α := ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ) (HPow.hPow (β := ℕ) z.re 2) = HPow.hPow (β := ℕ) z.im 2
Tactic: rw [Complex.sq_norm, normSq_apply, ← sq, ← sq, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
rw : HSub.hSub (α := ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ) (HPow.hPow (β := ℕ) z.re 2) = HPow.hPow (β := ℕ) z.im 2
⊢ HPow.hPow (β := ℕ) ‖z‖ 2 - HPow.hPow (β := ℕ) z.re 2 = HPow.hPow (β := ℕ) z.im 2
have rw₁ : z.re * z.re + z.im * z.im - HPow.hPow (β := ℕ) z.re 2 = HPow.hPow (β := ℕ) z.im 2
Tactic: rw [Complex.sq_norm, normSq_apply, ← sq, ← sq, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
rw : HSub.hSub (α := ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ) (HPow.hPow (β := ℕ) z.re 2) = HPow.hPow (β := ℕ) z.im 2
rw₁ : z.re * z.re + z.im * z.im - HPow.hPow (β := ℕ) z.re 2 = HPow.hPow (β := ℕ) z.im 2
⊢ HPow.hPow (β := ℕ) ‖z‖ 2 - HPow.hPow (β := ℕ) z.re 2 = HPow.hPow (β := ℕ) z.im 2
have rw₂ : HPow.hPow (β := ℕ) z.re 2 + z.im * z.im - HPow.hPow (β := ℕ) z.re 2 = HPow.hPow (β := ℕ) z.im 2
Tactic: rw [Complex.sq_norm, normSq_apply, ← sq, ← sq, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
rw : HSub.hSub (α := ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ) (HPow.hPow (β := ℕ) z.re 2) = HPow.hPow (β := ℕ) z.im 2
rw₁ : z.re * z.re + z.im * z.im - HPow.hPow (β := ℕ) z.re 2 = HPow.hPow (β := ℕ) z.im 2
rw₂ : HPow.hPow (β := ℕ) z.re 2 + z.im * z.im - HPow.hPow (β := ℕ) z.re 2 = HPow.hPow (β := ℕ) z.im 2
⊢ HPow.hPow (β := ℕ) ‖z‖ 2 - HPow.hPow (β := ℕ) z.re 2 = HPow.hPow (β := ℕ) z.im 2
have rw₃ : HPow.hPow (β := ℕ) z.re 2 + HPow.hPow (β := ℕ) z.im 2 - HPow.hPow (β := ℕ) z.re 2 = HPow.hPow (β := ℕ) z.im 2
Tactic: rw [Complex.sq_norm, normSq_apply, ← sq, ← sq, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
rw : HSub.hSub (α := ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ) (HPow.hPow (β := ℕ) z.re 2) = HPow.hPow (β := ℕ) z.im 2
rw₁ : z.re * z.re + z.im * z.im - HPow.hPow (β := ℕ) z.re 2 = HPow.hPow (β := ℕ) z.im 2
rw₂ : HPow.hPow (β := ℕ) z.re 2 + z.im * z.im - HPow.hPow (β := ℕ) z.re 2 = HPow.hPow (β := ℕ) z.im 2
rw₃ : HPow.hPow (β := ℕ) z.re 2 + HPow.hPow (β := ℕ) z.im 2 - HPow.hPow (β := ℕ) z.re 2 = HPow.hPow (β := ℕ) z.im 2
⊢ HPow.hPow (β := ℕ) ‖z‖ 2 - HPow.hPow (β := ℕ) z.re 2 = HPow.hPow (β := ℕ) z.im 2
have rw₄ : HPow.hPow (β := ℕ) z.im 2 = HPow.hPow (β := ℕ) z.im 2
Tactic: rw [Complex.sq_norm, normSq_apply, ← sq, ← sq, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
⊢ HPow.hPow (β := ℕ) ‖z‖ 2 - HPow.hPow (β := ℕ) z.im 2 = HPow.hPow (β := ℕ) z.re 2
have rw : HPow.hPow (β := ℕ) ‖z‖ 2 - (HPow.hPow (β := ℕ) ‖z‖ 2 - HPow.hPow (β := ℕ) z.re 2) = HPow.hPow (β := ℕ) z.re 2
Tactic: rw [← sq_norm_sub_sq_re, sub_sub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
rw : HPow.hPow (β := ℕ) ‖z‖ 2 - (HPow.hPow (β := ℕ) ‖z‖ 2 - HPow.hPow (β := ℕ) z.re 2) = HPow.hPow (β := ℕ) z.re 2
⊢ HPow.hPow (β := ℕ) ‖z‖ 2 - HPow.hPow (β := ℕ) z.im 2 = HPow.hPow (β := ℕ) z.re 2
have rw₁ : HPow.hPow (β := ℕ) z.re 2 = HPow.hPow (β := ℕ) z.re 2
Tactic: rw [← sq_norm_sub_sq_re, sub_sub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
x y : ℝ
⊢ ‖(↑x : ℂ) + (↑y : ℂ) * I‖ = √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2)
have rw : ‖(↑x : ℂ) + (↑y : ℂ) * I‖ = √((normSq : (a : ℂ) → ℝ) ((↑x : ℂ) + (↑y : ℂ) * I))
Tactic: rw [← normSq_add_mul_I]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
⊢ ‖z‖ = √(HPow.hPow (β := ℕ) z.re 2 + HPow.hPow (β := ℕ) z.im 2)
have rw : √((normSq : (a : ℂ) → ℝ) z) = √(HPow.hPow (β := ℕ) z.re 2 + HPow.hPow (β := ℕ) z.im 2)
Tactic: rw [norm_def, normSq_apply, sq, sq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
rw : √((normSq : (a : ℂ) → ℝ) z) = √(HPow.hPow (β := ℕ) z.re 2 + HPow.hPow (β := ℕ) z.im 2)
⊢ ‖z‖ = √(HPow.hPow (β := ℕ) z.re 2 + HPow.hPow (β := ℕ) z.im 2)
have rw₁ : √(z.re * z.re + z.im * z.im) = √(HPow.hPow (β := ℕ) z.re 2 + HPow.hPow (β := ℕ) z.im 2)
Tactic: rw [norm_def, normSq_apply, sq, sq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
rw : √((normSq : (a : ℂ) → ℝ) z) = √(HPow.hPow (β := ℕ) z.re 2 + HPow.hPow (β := ℕ) z.im 2)
rw₁ : √(z.re * z.re + z.im * z.im) = √(HPow.hPow (β := ℕ) z.re 2 + HPow.hPow (β := ℕ) z.im 2)
⊢ ‖z‖ = √(HPow.hPow (β := ℕ) z.re 2 + HPow.hPow (β := ℕ) z.im 2)
have rw₂ : √(z.re * z.re + z.im * z.im) = √(z.re * z.re + HPow.hPow (β := ℕ) z.im 2)
Tactic: rw [norm_def, normSq_apply, sq, sq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
rw : √((normSq : (a : ℂ) → ℝ) z) = √(HPow.hPow (β := ℕ) z.re 2 + HPow.hPow (β := ℕ) z.im 2)
rw₁ : √(z.re * z.re + z.im * z.im) = √(HPow.hPow (β := ℕ) z.re 2 + HPow.hPow (β := ℕ) z.im 2)
rw₂ : √(z.re * z.re + z.im * z.im) = √(z.re * z.re + HPow.hPow (β := ℕ) z.im 2)
⊢ ‖z‖ = √(HPow.hPow (β := ℕ) z.re 2 + HPow.hPow (β := ℕ) z.im 2)
have rw₃ : √(z.re * z.re + z.im * z.im) = √(z.re * z.re + z.im * z.im)
Tactic: rw [norm_def, normSq_apply, sq, sq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
⊢ (normSq : (a : ℂ) → ℝ) (↑√x : ℂ) = x
have rw : √x * √x = x
Tactic: rw [normSq_ofReal, Real.mul_self_sqrt hx]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
rw : √x * √x = x
⊢ (normSq : (a : ℂ) → ℝ) (↑√x : ℂ) = x
have rw₁ : x = x
Tactic: rw [normSq_ofReal, Real.mul_self_sqrt hx]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
⊢ HPow.hPow (β := ℕ) z.im 2 ≤ (normSq : (a : ℂ) → ℝ) z
have rw : HPow.hPow (β := ℕ) z.im 2 ≤ HPow.hPow (β := ℕ) z.re 2 + HPow.hPow (β := ℕ) z.im 2
Tactic: rw [normSq_apply, ← sq, ← sq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
⊢ |z.re| < ‖z‖ ↔ z.im ≠ 0
have rw : |z.re| < √((normSq : (a : ℂ) → ℝ) z) ↔ z.im ≠ 0
Tactic: rw [norm_def, Real.lt_sqrt (abs_nonneg _), normSq_apply, sq_abs, ← sq, lt_add_iff_pos_right,
    mul_self_pos]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
rw : |z.re| < √((normSq : (a : ℂ) → ℝ) z) ↔ z.im ≠ 0
⊢ |z.re| < ‖z‖ ↔ z.im ≠ 0
have rw₁ : HPow.hPow (β := ℕ) |z.re| 2 < (normSq : (a : ℂ) → ℝ) z ↔ z.im ≠ 0
Tactic: rw [norm_def, Real.lt_sqrt (abs_nonneg _), normSq_apply, sq_abs, ← sq, lt_add_iff_pos_right,
    mul_self_pos]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
rw : |z.re| < √((normSq : (a : ℂ) → ℝ) z) ↔ z.im ≠ 0
rw₁ : HPow.hPow (β := ℕ) |z.re| 2 < (normSq : (a : ℂ) → ℝ) z ↔ z.im ≠ 0
⊢ |z.re| < ‖z‖ ↔ z.im ≠ 0
have rw₂ : HPow.hPow (β := ℕ) |z.re| 2 < z.re * z.re + z.im * z.im ↔ z.im ≠ 0
Tactic: rw [norm_def, Real.lt_sqrt (abs_nonneg _), normSq_apply, sq_abs, ← sq, lt_add_iff_pos_right,
    mul_self_pos]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
rw : |z.re| < √((normSq : (a : ℂ) → ℝ) z) ↔ z.im ≠ 0
rw₁ : HPow.hPow (β := ℕ) |z.re| 2 < (normSq : (a : ℂ) → ℝ) z ↔ z.im ≠ 0
rw₂ : HPow.hPow (β := ℕ) |z.re| 2 < z.re * z.re + z.im * z.im ↔ z.im ≠ 0
⊢ |z.re| < ‖z‖ ↔ z.im ≠ 0
have rw₃ : HPow.hPow (β := ℕ) z.re 2 < z.re * z.re + z.im * z.im ↔ z.im ≠ 0
Tactic: rw [norm_def, Real.lt_sqrt (abs_nonneg _), normSq_apply, sq_abs, ← sq, lt_add_iff_pos_right,
    mul_self_pos]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
rw : |z.re| < √((normSq : (a : ℂ) → ℝ) z) ↔ z.im ≠ 0
rw₁ : HPow.hPow (β := ℕ) |z.re| 2 < (normSq : (a : ℂ) → ℝ) z ↔ z.im ≠ 0
rw₂ : HPow.hPow (β := ℕ) |z.re| 2 < z.re * z.re + z.im * z.im ↔ z.im ≠ 0
rw₃ : HPow.hPow (β := ℕ) z.re 2 < z.re * z.re + z.im * z.im ↔ z.im ≠ 0
⊢ |z.re| < ‖z‖ ↔ z.im ≠ 0
have rw₄ : HPow.hPow (β := ℕ) z.re 2 < HPow.hPow (β := ℕ) z.re 2 + z.im * z.im ↔ z.im ≠ 0
Tactic: rw [norm_def, Real.lt_sqrt (abs_nonneg _), normSq_apply, sq_abs, ← sq, lt_add_iff_pos_right,
    mul_self_pos]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
rw : |z.re| < √((normSq : (a : ℂ) → ℝ) z) ↔ z.im ≠ 0
rw₁ : HPow.hPow (β := ℕ) |z.re| 2 < (normSq : (a : ℂ) → ℝ) z ↔ z.im ≠ 0
rw₂ : HPow.hPow (β := ℕ) |z.re| 2 < z.re * z.re + z.im * z.im ↔ z.im ≠ 0
rw₃ : HPow.hPow (β := ℕ) z.re 2 < z.re * z.re + z.im * z.im ↔ z.im ≠ 0
rw₄ : HPow.hPow (β := ℕ) z.re 2 < HPow.hPow (β := ℕ) z.re 2 + z.im * z.im ↔ z.im ≠ 0
⊢ |z.re| < ‖z‖ ↔ z.im ≠ 0
have rw₅ : 0 < z.im * z.im ↔ z.im ≠ 0
Tactic: rw [norm_def, Real.lt_sqrt (abs_nonneg _), normSq_apply, sq_abs, ← sq, lt_add_iff_pos_right,
    mul_self_pos]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
rw : |z.re| < √((normSq : (a : ℂ) → ℝ) z) ↔ z.im ≠ 0
rw₁ : HPow.hPow (β := ℕ) |z.re| 2 < (normSq : (a : ℂ) → ℝ) z ↔ z.im ≠ 0
rw₂ : HPow.hPow (β := ℕ) |z.re| 2 < z.re * z.re + z.im * z.im ↔ z.im ≠ 0
rw₃ : HPow.hPow (β := ℕ) z.re 2 < z.re * z.re + z.im * z.im ↔ z.im ≠ 0
rw₄ : HPow.hPow (β := ℕ) z.re 2 < HPow.hPow (β := ℕ) z.re 2 + z.im * z.im ↔ z.im ≠ 0
rw₅ : 0 < z.im * z.im ↔ z.im ≠ 0
⊢ |z.re| < ‖z‖ ↔ z.im ≠ 0
have rw₆ : z.im ≠ 0 ↔ z.im ≠ 0
Tactic: rw [norm_def, Real.lt_sqrt (abs_nonneg _), normSq_apply, sq_abs, ← sq, lt_add_iff_pos_right,
    mul_self_pos]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
⊢ ‖z‖ ≤ √2 * max |z.re| |z.im|
have obtain : ∀ (x y : ℝ), ‖{ re := x, im := y : ℂ }‖ ≤ √2 * max |{ re := x, im := y : ℂ }.re| |{ re := x, im := y : ℂ }.im|
Tactic: obtain ⟨x, y⟩ := z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
x y : ℝ
⊢ ‖{ re := x, im := y : ℂ }‖ ≤ √2 * max |{ re := x, im := y : ℂ }.re| |{ re := x, im := y : ℂ }.im|
have simp : √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) ≤ √2 * max |x| |y|
Tactic: simp only [norm_def, normSq_mk, norm_def, ← sq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (hypothesis)
Goal:
x y : ℝ
m : ℝ := max |x| |y|
⊢ √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) ≤ √2 * m
have hm₀ : 0 ≤ m
Tactic: have hm₀ : 0 ≤ m := by positivity
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
x y : ℝ
m : ℝ := max |x| |y|
hm₀ : 0 ≤ m
⊢ √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) ≤ √(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) m 2)
have a : HPow.hPow (β := ℕ) x 2 ≤ HPow.hPow (β := ℕ) m 2
Tactic: gcongr √(?_ + ?_)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
x y : ℝ
m : ℝ := max |x| |y|
hm₀ : 0 ≤ m
a : HPow.hPow (β := ℕ) x 2 ≤ HPow.hPow (β := ℕ) m 2
⊢ √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) ≤ √(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) m 2)
have a₁ : HPow.hPow (β := ℕ) y 2 ≤ HPow.hPow (β := ℕ) m 2
Tactic: gcongr √(?_ + ?_)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
x y : ℝ
m : ℝ := max |x| |y|
hm₀ : 0 ≤ m
⊢ HPow.hPow (β := ℕ) x 2 ≤ HPow.hPow (β := ℕ) m 2
have a : |x| ≤ m
Tactic: rw [sq_le_sq, abs_of_nonneg hm₀]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
x y : ℝ
m : ℝ := max |x| |y|
hm₀ : 0 ≤ m
⊢ HPow.hPow (β := ℕ) y 2 ≤ HPow.hPow (β := ℕ) m 2
have a : |y| ≤ m
Tactic: rw [sq_le_sq, abs_of_nonneg hm₀]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
x y : ℝ
m : ℝ := max |x| |y|
hm₀ rw : 0 ≤ m
⊢ √(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) m 2) = √2 * m
have hx : LE.le (α := ℝ) 0 2
Tactic: rw [← two_mul, Real.sqrt_mul, Real.sqrt_sq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
x y : ℝ
m : ℝ := max |x| |y|
hm₀ : 0 ≤ m
⊢ √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) ≤ √2 * m
have y₁ : √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) ≤ √(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) m 2)
Tactic: calc
    √(x ^ 2 + y ^ 2) ≤ √(m ^ 2 + m ^ 2) := by
      gcongr √(?_ + ?_) <;> rw [sq_le_sq, abs_of_nonneg hm₀]
      exacts [le_max_left _ _, le_max_right _ _]
    _ = √2 * m := by
      rw [← two_mul, Real.sqrt_mul, Real.sqrt_sq] <;> positivity
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
x y : ℝ
m : ℝ := max |x| |y|
hm₀ : 0 ≤ m
y₁ : √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) ≤ √(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) m 2)
⊢ √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) ≤ √2 * m
have y₂ : √(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) m 2) = √2 * m
Tactic: calc
    √(x ^ 2 + y ^ 2) ≤ √(m ^ 2 + m ^ 2) := by
      gcongr √(?_ + ?_) <;> rw [sq_le_sq, abs_of_nonneg hm₀]
      exacts [le_max_left _ _, le_max_right _ _]
    _ = √2 * m := by
      rw [← two_mul, Real.sqrt_mul, Real.sqrt_sq] <;> positivity
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
hz : ¬z = 0
⊢ |z.re / ‖z‖| ≤ 1
have simp_rw : |z.re| / |‖z‖| ≤ 1
Tactic: simp_rw [abs_div, abs_norm, div_le_iff₀ (norm_pos_iff.mpr hz), one_mul, abs_re_le_norm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
hz : ¬z = 0
simp_rw : |z.re| / |‖z‖| ≤ 1
⊢ |z.re / ‖z‖| ≤ 1
have simp_rw₁ : |z.re| / ‖z‖ ≤ 1
Tactic: simp_rw [abs_div, abs_norm, div_le_iff₀ (norm_pos_iff.mpr hz), one_mul, abs_re_le_norm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
hz : ¬z = 0
simp_rw : |z.re| / |‖z‖| ≤ 1
simp_rw₁ : |z.re| / ‖z‖ ≤ 1
⊢ |z.re / ‖z‖| ≤ 1
have simp_rw₂ : |z.re| ≤ 1 * ‖z‖
Tactic: simp_rw [abs_div, abs_norm, div_le_iff₀ (norm_pos_iff.mpr hz), one_mul, abs_re_le_norm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
hz : ¬z = 0
simp_rw : |z.re| / |‖z‖| ≤ 1
simp_rw₁ : |z.re| / ‖z‖ ≤ 1
simp_rw₂ : |z.re| ≤ 1 * ‖z‖
⊢ |z.re / ‖z‖| ≤ 1
have simp_rw₃ : |z.re| ≤ ‖z‖
Tactic: simp_rw [abs_div, abs_norm, div_le_iff₀ (norm_pos_iff.mpr hz), one_mul, abs_re_le_norm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
hz : ¬z = 0
⊢ |z.im / ‖z‖| ≤ 1
have simp_rw : |z.im| / |‖z‖| ≤ 1
Tactic: simp_rw [_root_.abs_div, abs_norm, div_le_iff₀ (norm_pos_iff.mpr hz), one_mul, abs_im_le_norm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
hz : ¬z = 0
simp_rw : |z.im| / |‖z‖| ≤ 1
⊢ |z.im / ‖z‖| ≤ 1
have simp_rw₁ : |z.im| / ‖z‖ ≤ 1
Tactic: simp_rw [_root_.abs_div, abs_norm, div_le_iff₀ (norm_pos_iff.mpr hz), one_mul, abs_im_le_norm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
hz : ¬z = 0
simp_rw : |z.im| / |‖z‖| ≤ 1
simp_rw₁ : |z.im| / ‖z‖ ≤ 1
⊢ |z.im / ‖z‖| ≤ 1
have simp_rw₂ : |z.im| ≤ 1 * ‖z‖
Tactic: simp_rw [_root_.abs_div, abs_norm, div_le_iff₀ (norm_pos_iff.mpr hz), one_mul, abs_im_le_norm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
hz : ¬z = 0
simp_rw : |z.im| / |‖z‖| ≤ 1
simp_rw₁ : |z.im| / ‖z‖ ≤ 1
simp_rw₂ : |z.im| ≤ 1 * ‖z‖
⊢ |z.im / ‖z‖| ≤ 1
have simp_rw₃ : |z.im| ≤ ‖z‖
Tactic: simp_rw [_root_.abs_div, abs_norm, div_le_iff₀ (norm_pos_iff.mpr hz), one_mul, abs_im_le_norm]