awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (goal)
Goal:
x y : ℂ
hy : norm (E := ℂ) 1 = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ √(HPow.hPow (β := ℕ) (Real.cos θ - 1) 2 + HPow.hPow (β := ℕ) (Real.sin θ) 2) ∈ Icc (2 / π * |θ|) |θ|
have refine_1 : HPow.hPow (β := ℕ) (2 / π * |θ|) 2 ≤ HPow.hPow (β := ℕ) (Real.cos θ - 1) 2 + HPow.hPow (β := ℕ) (Real.sin θ) 2
Tactic: refine ⟨Real.le_sqrt_of_sq_le ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (goal)
Goal:
x y : ℂ
hy : norm (E := ℂ) 1 = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
refine_1 :
  HPow.hPow (β := ℕ) (2 / π * |θ|) 2 ≤ HPow.hPow (β := ℕ) (Real.cos θ - 1) 2 + HPow.hPow (β := ℕ) (Real.sin θ) 2
⊢ √(HPow.hPow (β := ℕ) (Real.cos θ - 1) 2 + HPow.hPow (β := ℕ) (Real.sin θ) 2) ∈ Icc (2 / π * |θ|) |θ|
have refine_2 : √(HPow.hPow (β := ℕ) (Real.cos θ - 1) 2 + HPow.hPow (β := ℕ) (Real.sin θ) 2) ≤ |θ|
Tactic: refine ⟨Real.le_sqrt_of_sq_le ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (goal)
Goal:
x y : ℂ
hy : norm (E := ℂ) 1 = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ HPow.hPow (β := ℕ) (2 / π * |θ|) 2 ≤ HPow.hPow (β := ℕ) (Real.cos θ - 1) 2 + HPow.hPow (β := ℕ) (Real.sin θ) 2
have refine_1 : HPow.hPow (β := ℕ) (2 / π) 2 * HPow.hPow (β := ℕ) θ 2 ≤
  HPow.hPow (β := ℕ) (Real.cos θ - 1) 2 + HPow.hPow (β := ℕ) (Real.sin θ) 2
Tactic: rw [mul_pow, ← abs_pow, abs_sq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (goal)
Goal:
x y : ℂ
hy : norm (E := ℂ) 1 = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ 2 * (1 - (1 - 2 / HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) θ 2)) ≤ 2 * (1 - Real.cos θ)
have hbc : Real.cos θ ≤ 1 - 2 / HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) θ 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (goal)
Goal:
x y : ℂ
hy : norm (E := ℂ) 1 = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ HPow.hPow (β := ℕ) (2 / π) 2 * HPow.hPow (β := ℕ) θ 2 ≤
    HPow.hPow (β := ℕ) (Real.cos θ - 1) 2 + HPow.hPow (β := ℕ) (Real.sin θ) 2
have _ : HPow.hPow (β := ℕ) (2 / π) 2 * HPow.hPow (β := ℕ) θ 2 =
  2 * (1 - (1 - 2 / HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) θ 2))
Tactic: calc
        _ = 2 * (1 - (1 - 2 / π ^ 2 * θ ^ 2)) := by ring
        _ ≤ 2 * (1 - θ.cos) := by
            gcongr; exact Real.cos_le_one_sub_mul_cos_sq <| abs_le.2 <| Ioc_subset_Icc_self hθ
        _ = _ := by linear_combination -θ.cos_sq_add_sin_sq
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (goal)
Goal:
x y : ℂ
hy : norm (E := ℂ) 1 = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
_ :
  HPow.hPow (β := ℕ) (2 / π) 2 * HPow.hPow (β := ℕ) θ 2 =
    2 * (1 - (1 - 2 / HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) θ 2))
⊢ HPow.hPow (β := ℕ) (2 / π) 2 * HPow.hPow (β := ℕ) θ 2 ≤
    HPow.hPow (β := ℕ) (Real.cos θ - 1) 2 + HPow.hPow (β := ℕ) (Real.sin θ) 2
have _₁ : 2 * (1 - (1 - 2 / HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) θ 2)) ≤ 2 * (1 - Real.cos θ)
Tactic: calc
        _ = 2 * (1 - (1 - 2 / π ^ 2 * θ ^ 2)) := by ring
        _ ≤ 2 * (1 - θ.cos) := by
            gcongr; exact Real.cos_le_one_sub_mul_cos_sq <| abs_le.2 <| Ioc_subset_Icc_self hθ
        _ = _ := by linear_combination -θ.cos_sq_add_sin_sq
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (goal)
Goal:
x y : ℂ
hy : norm (E := ℂ) 1 = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
_ :
  HPow.hPow (β := ℕ) (2 / π) 2 * HPow.hPow (β := ℕ) θ 2 =
    2 * (1 - (1 - 2 / HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) θ 2))
_₁ : 2 * (1 - (1 - 2 / HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) θ 2)) ≤ 2 * (1 - Real.cos θ)
⊢ HPow.hPow (β := ℕ) (2 / π) 2 * HPow.hPow (β := ℕ) θ 2 ≤
    HPow.hPow (β := ℕ) (Real.cos θ - 1) 2 + HPow.hPow (β := ℕ) (Real.sin θ) 2
have _₂ : 2 * (1 - Real.cos θ) = HPow.hPow (β := ℕ) (Real.cos θ - 1) 2 + HPow.hPow (β := ℕ) (Real.sin θ) 2
Tactic: calc
        _ = 2 * (1 - (1 - 2 / π ^ 2 * θ ^ 2)) := by ring
        _ ≤ 2 * (1 - θ.cos) := by
            gcongr; exact Real.cos_le_one_sub_mul_cos_sq <| abs_le.2 <| Ioc_subset_Icc_self hθ
        _ = _ := by linear_combination -θ.cos_sq_add_sin_sq
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (goal)
Goal:
x y : ℂ
hy : norm (E := ℂ) 1 = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ √(HPow.hPow (β := ℕ) (Real.cos θ - 1) 2 + HPow.hPow (β := ℕ) (Real.sin θ) 2) ≤ |θ|
have refine_2 : HPow.hPow (β := ℕ) (Real.cos θ - 1) 2 + HPow.hPow (β := ℕ) (Real.sin θ) 2 ≤ HPow.hPow (β := ℕ) θ 2
Tactic: rw [Real.sqrt_le_left (by positivity), ← abs_pow, abs_sq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (goal)
Goal:
x y : ℂ
hy : norm (E := ℂ) 1 = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ 2 * (1 - Real.cos θ) ≤ 2 * (1 - (1 - HPow.hPow (β := ℕ) θ 2 / 2))
have hbc : 1 - HPow.hPow (β := ℕ) θ 2 / 2 ≤ Real.cos θ
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (goal)
Goal:
x y : ℂ
hy : norm (E := ℂ) 1 = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ HPow.hPow (β := ℕ) (Real.cos θ - 1) 2 + HPow.hPow (β := ℕ) (Real.sin θ) 2 ≤ HPow.hPow (β := ℕ) θ 2
have _ : HPow.hPow (β := ℕ) (Real.cos θ - 1) 2 + HPow.hPow (β := ℕ) (Real.sin θ) 2 = 2 * (1 - Real.cos θ)
Tactic: calc
        _ = 2 * (1 - θ.cos) := by linear_combination θ.cos_sq_add_sin_sq
        _ ≤ 2 * (1 - (1 - θ ^ 2 / 2)) := by gcongr; exact Real.one_sub_sq_div_two_le_cos
        _ = _ := by ring
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (goal)
Goal:
x y : ℂ
hy : norm (E := ℂ) 1 = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
_ : HPow.hPow (β := ℕ) (Real.cos θ - 1) 2 + HPow.hPow (β := ℕ) (Real.sin θ) 2 = 2 * (1 - Real.cos θ)
⊢ HPow.hPow (β := ℕ) (Real.cos θ - 1) 2 + HPow.hPow (β := ℕ) (Real.sin θ) 2 ≤ HPow.hPow (β := ℕ) θ 2
have _₁ : 2 * (1 - Real.cos θ) ≤ 2 * (1 - (1 - HPow.hPow (β := ℕ) θ 2 / 2))
Tactic: calc
        _ = 2 * (1 - θ.cos) := by linear_combination θ.cos_sq_add_sin_sq
        _ ≤ 2 * (1 - (1 - θ ^ 2 / 2)) := by gcongr; exact Real.one_sub_sq_div_two_le_cos
        _ = _ := by ring
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (goal)
Goal:
x y : ℂ
hy : norm (E := ℂ) 1 = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
_ : HPow.hPow (β := ℕ) (Real.cos θ - 1) 2 + HPow.hPow (β := ℕ) (Real.sin θ) 2 = 2 * (1 - Real.cos θ)
_₁ : 2 * (1 - Real.cos θ) ≤ 2 * (1 - (1 - HPow.hPow (β := ℕ) θ 2 / 2))
⊢ HPow.hPow (β := ℕ) (Real.cos θ - 1) 2 + HPow.hPow (β := ℕ) (Real.sin θ) 2 ≤ HPow.hPow (β := ℕ) θ 2
have _₂ : 2 * (1 - (1 - HPow.hPow (β := ℕ) θ 2 / 2)) = HPow.hPow (β := ℕ) θ 2
Tactic: calc
        _ = 2 * (1 - θ.cos) := by linear_combination θ.cos_sq_add_sin_sq
        _ ≤ 2 * (1 - (1 - θ ^ 2 / 2)) := by gcongr; exact Real.one_sub_sq_div_two_le_cos
        _ = _ := by ring
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (goal)
Goal:
x y : ℂ
hy : norm (E := ℂ) 1 = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ θ ∈ Ioc (-π) (-π + 2 * π)
have h : -π + 2 * π = π
Tactic: convert! hθ
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (goal)
Goal:
x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ angle x y ≤ π / 2 * ‖x - y‖
have rw : 2 / π * angle x y ≤ ‖x - y‖
Tactic: rw [← div_le_iff₀' <| by positivity, div_eq_inv_mul, inv_div]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Arg (goal)
Goal:
x y : ℂ
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg
have inl : SameRay ℝ 0 y ↔ Eq (α := ℂ) 0 0 ∨ y = 0 ∨ arg 0 = y.arg
Tactic: rcases eq_or_ne x 0 with (rfl | hx)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.Complex.Arg (goal)
Goal:
x y : ℂ
inl : SameRay ℝ 0 y ↔ Eq (α := ℂ) 0 0 ∨ y = 0 ∨ arg 0 = y.arg
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg
have inr : ∀ (hx : x ≠ 0), SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg
Tactic: rcases eq_or_ne x 0 with (rfl | hx)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Arg (goal)
Goal:
x y : ℂ
hx : x ≠ 0
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg
have inr : SameRay ℝ x 0 ↔ x = 0 ∨ Eq (α := ℂ) 0 0 ∨ x.arg = arg 0
Tactic: rcases eq_or_ne y 0 with (rfl | hy)
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Analysis.Complex.Arg (goal)
Goal:
x y : ℂ
hx : x ≠ 0
inr : SameRay ℝ x 0 ↔ x = 0 ∨ Eq (α := ℂ) 0 0 ∨ x.arg = arg 0
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg
have inr₁ : ∀ (hy : y ≠ 0), SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg
Tactic: rcases eq_or_ne y 0 with (rfl | hy)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Arg (goal)
Goal:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg
have inr : ‖x‖ • y = ‖y‖ • x ↔ False ∨ False ∨ (↑‖y‖ : ℂ) / (↑‖x‖ : ℂ) * x = y
Tactic: simp only [hx, hy, sameRay_iff_norm_smul_eq, arg_eq_arg_iff hx hy]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Arg (goal)
Goal:
x y : ℂ
⊢ SameRay ℝ x y ↔ (x / y).arg = 0
have rw : x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ (↑(x / y).arg : Real.Angle) = 0
Tactic: rw [← Real.Angle.toReal_zero, ← arg_coe_angle_eq_iff_eq_toReal, sameRay_iff]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Arg (goal)
Goal:
x y : ℂ
⊢ x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ (↑(x / y).arg : Real.Angle) = 0
have pos : ∀ (hx : x = 0), x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ (↑(x / y).arg : Real.Angle) = 0
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.Arg (goal)
Goal:
x y : ℂ
pos : ∀ (hx : x = 0), x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ (↑(x / y).arg : Real.Angle) = 0
⊢ x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ (↑(x / y).arg : Real.Angle) = 0
have neg : ∀ (hx : ¬x = 0), x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ (↑(x / y).arg : Real.Angle) = 0
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.Arg (goal)
Goal:
x y : ℂ
hx : ¬x = 0
⊢ x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ (↑(x / y).arg : Real.Angle) = 0
have pos : ∀ (hy : y = 0), x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ (↑(x / y).arg : Real.Angle) = 0
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.Arg (goal)
Goal:
x y : ℂ
hx : ¬x = 0
pos : ∀ (hy : y = 0), x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ (↑(x / y).arg : Real.Angle) = 0
⊢ x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ (↑(x / y).arg : Real.Angle) = 0
have neg : ∀ (hy : ¬y = 0), x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ (↑(x / y).arg : Real.Angle) = 0
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.Asymptotics (goal)
Goal:
⊢ Asymptotics.IsTheta (E := ℂ) (F := ℝ) cofinite Int.cast Int.cast
have h : EventuallyEq (β := ℝ) cofinite (fun (x : ℤ) ↦ norm (E := ℂ) (↑x : ℂ)) fun (x : ℤ) ↦ norm (E := ℝ) (↑x : ℝ)
Tactic: apply Asymptotics.IsTheta.of_norm_eventuallyEq_norm
-- Lean 4 proof step from Mathlib.Analysis.Complex.Asymptotics (goal)
Goal:
⊢ EventuallyEq (β := ℝ) cofinite (fun (x : ℤ) ↦ norm (E := ℂ) (↑x : ℂ)) fun (x : ℤ) ↦ norm (E := ℝ) (↑x : ℝ)
have h : ∀ (a : ℤ),
  Membership.mem (γ := Set ℤ)
    {x : ℤ |
      (fun (x : ℤ) ↦ Eq (α := ℝ) ((fun (x : ℤ) ↦ norm (E := ℂ) (↑x : ℂ)) x) ((fun (x : ℤ) ↦ norm (E := ℝ) (↑x : ℝ)) x))
        x}
    a
Tactic: filter_upwards with n using by simp
-- Lean 4 proof step from Mathlib.Analysis.Complex.Asymptotics (goal)
Goal:
h :
  ∀ (a : ℤ),
    Membership.mem (γ := Set ℤ)
      {x : ℤ |
        (fun (x : ℤ) ↦
            Eq (α := ℝ) ((fun (x : ℤ) ↦ norm (E := ℂ) (↑x : ℂ)) x) ((fun (x : ℤ) ↦ norm (E := ℝ) (↑x : ℝ)) x))
          x}
      a
⊢ EventuallyEq (β := ℝ) cofinite (fun (x : ℤ) ↦ norm (E := ℂ) (↑x : ℂ)) fun (x : ℤ) ↦ norm (E := ℝ) (↑x : ℝ)
have h₁ : ∀ (a : ℤ), norm (E := ℂ) (↑a : ℂ) = norm (E := ℝ) (↑a : ℝ)
Tactic: filter_upwards with n using by simp
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
z : ℂ
r₁ r₂ : ℝ
h₀ : 0 ≤ r₁
hr : r₁ < r₂
x : ℝ
h : r₁ < x ∧ x < r₂
⊢ r₁ < ‖(↑x : ℂ)‖ ∧ ‖(↑x : ℂ)‖ < r₂
have rwa : r₁ < ‖x‖ ∧ ‖x‖ < r₂
Tactic: rwa [norm_real, Real.norm_of_nonneg (h₀.trans_lt h.1).le]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
z : ℂ
R : Type u_1
inst : NormedField R
inst_1 : NormedAlgebra R ℝ
r : R
x : ℂ
⊢ ‖r • x‖ ≤ ‖r‖ * ‖x‖
have rw : ‖HSMul.hSMul (α := ℝ) ((algebraMap R ℝ : (a : R) → ℝ) r : ℝ) x‖ ≤ ‖r‖ * ‖x‖
Tactic: rw [← algebraMap_smul ℝ r x, real_smul, norm_mul, norm_real, norm_algebraMap']
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
z : ℂ
R : Type u_1
inst : NormedField R
inst_1 : NormedAlgebra R ℝ
r : R
x : ℂ
rw : ‖HSMul.hSMul (α := ℝ) ((algebraMap R ℝ : (a : R) → ℝ) r : ℝ) x‖ ≤ ‖r‖ * ‖x‖
⊢ ‖r • x‖ ≤ ‖r‖ * ‖x‖
have rw₁ : ‖(↑((algebraMap R ℝ : (a : R) → ℝ) r) : ℂ) * x‖ ≤ ‖r‖ * ‖x‖
Tactic: rw [← algebraMap_smul ℝ r x, real_smul, norm_mul, norm_real, norm_algebraMap']
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
z : ℂ
R : Type u_1
inst : NormedField R
inst_1 : NormedAlgebra R ℝ
r : R
x : ℂ
rw : ‖HSMul.hSMul (α := ℝ) ((algebraMap R ℝ : (a : R) → ℝ) r : ℝ) x‖ ≤ ‖r‖ * ‖x‖
rw₁ : ‖(↑((algebraMap R ℝ : (a : R) → ℝ) r) : ℂ) * x‖ ≤ ‖r‖ * ‖x‖
⊢ ‖r • x‖ ≤ ‖r‖ * ‖x‖
have rw₂ : ‖(↑((algebraMap R ℝ : (a : R) → ℝ) r) : ℂ)‖ * ‖x‖ ≤ ‖r‖ * ‖x‖
Tactic: rw [← algebraMap_smul ℝ r x, real_smul, norm_mul, norm_real, norm_algebraMap']
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
z : ℂ
R : Type u_1
inst : NormedField R
inst_1 : NormedAlgebra R ℝ
r : R
x : ℂ
rw : ‖HSMul.hSMul (α := ℝ) ((algebraMap R ℝ : (a : R) → ℝ) r : ℝ) x‖ ≤ ‖r‖ * ‖x‖
rw₁ : ‖(↑((algebraMap R ℝ : (a : R) → ℝ) r) : ℂ) * x‖ ≤ ‖r‖ * ‖x‖
rw₂ : ‖(↑((algebraMap R ℝ : (a : R) → ℝ) r) : ℂ)‖ * ‖x‖ ≤ ‖r‖ * ‖x‖
⊢ ‖r • x‖ ≤ ‖r‖ * ‖x‖
have rw₃ : norm (E := ℝ) ((algebraMap R ℝ : (a : R) → ℝ) r : ℝ) * ‖x‖ ≤ ‖r‖ * ‖x‖
Tactic: rw [← algebraMap_smul ℝ r x, real_smul, norm_mul, norm_real, norm_algebraMap']
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
z : ℂ
R : Type u_1
inst : NormedField R
inst_1 : NormedAlgebra R ℝ
r : R
x : ℂ
rw : ‖HSMul.hSMul (α := ℝ) ((algebraMap R ℝ : (a : R) → ℝ) r : ℝ) x‖ ≤ ‖r‖ * ‖x‖
rw₁ : ‖(↑((algebraMap R ℝ : (a : R) → ℝ) r) : ℂ) * x‖ ≤ ‖r‖ * ‖x‖
rw₂ : ‖(↑((algebraMap R ℝ : (a : R) → ℝ) r) : ℂ)‖ * ‖x‖ ≤ ‖r‖ * ‖x‖
rw₃ : norm (E := ℝ) ((algebraMap R ℝ : (a : R) → ℝ) r : ℝ) * ‖x‖ ≤ ‖r‖ * ‖x‖
⊢ ‖r • x‖ ≤ ‖r‖ * ‖x‖
have rw₄ : ‖r‖ * ‖x‖ ≤ ‖r‖ * ‖x‖
Tactic: rw [← algebraMap_smul ℝ r x, real_smul, norm_mul, norm_real, norm_algebraMap']
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
n : ℤ
⊢ nnnorm (E := ℂ) (↑n : ℂ) = ‖n‖₊
have a : (↑(nnnorm (E := ℂ) (↑n : ℂ)) : ℝ) = (↑‖n‖₊ : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
ζ : ℂ
n : ℕ
h : ζ ^ n = 1
hn : n ≠ 0
⊢ ‖ζ‖₊ ^ n = HPow.hPow (α := NNReal) 1 n
have rw : ‖ζ ^ n‖₊ = HPow.hPow (α := NNReal) 1 n
Tactic: rw [← nnnorm_pow, h, nnnorm_one, one_pow]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
ζ : ℂ
n : ℕ
h : ζ ^ n = 1
hn : n ≠ 0
rw : ‖ζ ^ n‖₊ = HPow.hPow (α := NNReal) 1 n
⊢ ‖ζ‖₊ ^ n = HPow.hPow (α := NNReal) 1 n
have rw₁ : nnnorm (E := ℂ) 1 = HPow.hPow (α := NNReal) 1 n
Tactic: rw [← nnnorm_pow, h, nnnorm_one, one_pow]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
ζ : ℂ
n : ℕ
h : ζ ^ n = 1
hn : n ≠ 0
rw : ‖ζ ^ n‖₊ = HPow.hPow (α := NNReal) 1 n
rw₁ : nnnorm (E := ℂ) 1 = HPow.hPow (α := NNReal) 1 n
⊢ ‖ζ‖₊ ^ n = HPow.hPow (α := NNReal) 1 n
have rw₂ : 1 = HPow.hPow (α := NNReal) 1 n
Tactic: rw [← nnnorm_pow, h, nnnorm_one, one_pow]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
ζ : ℂ
n : ℕ
h : ζ ^ n = 1
hn : n ≠ 0
rw : ‖ζ ^ n‖₊ = HPow.hPow (α := NNReal) 1 n
rw₁ : nnnorm (E := ℂ) 1 = HPow.hPow (α := NNReal) 1 n
rw₂ : 1 = HPow.hPow (α := NNReal) 1 n
⊢ ‖ζ‖₊ ^ n = HPow.hPow (α := NNReal) 1 n
have rw₃ : Eq (α := NNReal) 1 1
Tactic: rw [← nnnorm_pow, h, nnnorm_one, one_pow]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (hypothesis)
Goal:
ι : Type u_2
a b : ℝ
f : ι → ℂ
s : Finset ι
ha₀ : 0 ≤ a
ha : (↑a : ℂ) = ∑ i ∈ s, f i
hb : (↑b : ℂ) = ∑ i ∈ s, (↑‖f i‖ : ℂ)
⊢ a ≤ b
have hb₁ : b = ∑ i ∈ s, ‖f i‖
Tactic: norm_cast at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
ι : Type u_2
a b : ℝ
f : ι → ℂ
s : Finset ι
ha₀ : 0 ≤ a
ha : (↑a : ℂ) = ∑ i ∈ s, f i
hb : b = ∑ i ∈ s, ‖f i‖
⊢ a ≤ b
have rw : norm (E := ℂ) (∑ i ∈ s, f i) ≤ ∑ i ∈ s, ‖f i‖
Tactic: rw [← Complex.norm_of_nonneg ha₀, ha, hb]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℂ E
x : E
⊢ restrictScalars ℝ (toSpanSingleton ℂ x) = reCLM.smulRight x + HSMul.hSMul (β := ℂ →L[ℝ] E) I (imCLM.smulRight x)
have h : ∀ (a b : ℝ),
  Eq (α := E) ((restrictScalars ℝ (toSpanSingleton ℂ x) : (a : ℂ) → E) { re := a, im := b : ℂ } : E)
    ((reCLM.smulRight x + HSMul.hSMul (β := ℂ →L[ℝ] E) I (imCLM.smulRight x) : (a : ℂ) → E) { re := a, im := b : ℂ } :
      E)
Tactic: ext ⟨a, b⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
x : ℂ
⊢ restrictScalars ℝ (toSpanSingleton ℂ x) = HSMul.hSMul (β := ℂ →L[ℝ] ℂ) x 1
have h : ∀ (z : ℂ),
  Eq (α := ℂ) ((restrictScalars ℝ (toSpanSingleton ℂ x) : (a : ℂ) → ℂ) z : ℂ)
    ((HSMul.hSMul (β := ℂ →L[ℝ] ℂ) x 1 : (a : ℂ) → ℂ) z : ℂ)
Tactic: ext1 z
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
x z : ℂ
⊢ Eq (α := ℂ) ((restrictScalars ℝ (toSpanSingleton ℂ x) : (a : ℂ) → ℂ) z : ℂ)
    ((HSMul.hSMul (β := ℂ →L[ℝ] ℂ) x 1 : (a : ℂ) → ℂ) z : ℂ)
have h : z * x = x * z
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
z w : ℂ
⊢ dist ((starRingEnd ℂ : (a : ℂ) → ℂ) z) w = dist z ((starRingEnd ℂ : (a : ℂ) → ℂ) w)
have rw : dist (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) =
  dist z ((starRingEnd ℂ : (a : ℂ) → ℂ) w)
Tactic: rw [← dist_conj_conj, conj_conj]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
z w : ℂ
rw :
  dist (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) : ℂ)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) =
    dist z ((starRingEnd ℂ : (a : ℂ) → ℂ) w)
⊢ dist ((starRingEnd ℂ : (a : ℂ) → ℂ) z) w = dist z ((starRingEnd ℂ : (a : ℂ) → ℂ) w)
have rw₁ : dist z ((starRingEnd ℂ : (a : ℂ) → ℂ) w) = dist z ((starRingEnd ℂ : (a : ℂ) → ℂ) w)
Tactic: rw [← dist_conj_conj, conj_conj]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
x : ℂ
⊢ x.im = 0 ↔ IsSelfAdjoint x
have rw : Eq (α := ℝ) ((RCLike.im : (a : ℂ) → ℝ) x : ℝ) (0 : ℝ) ↔ IsSelfAdjoint x
Tactic: rw [← RCLike.im_eq_complex_im]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
x : ℂ
y : ℝ
hx : IsSelfAdjoint x
⊢ x.re = y ↔ x = (↑y : ℂ)
have rw : (RCLike.re : (a : ℂ) → ℝ) x = y ↔ x = (↑y : ℂ)
Tactic: rw [← RCLike.re_eq_complex_re]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
x : ℂ
y : ℝ
hx : IsSelfAdjoint x
⊢ y = x.re ↔ (↑y : ℂ) = x
have rw : y = (RCLike.re : (a : ℂ) → ℝ) x ↔ (↑y : ℂ) = x
Tactic: rw [← RCLike.re_eq_complex_re]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
z : ℂ
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℂ E
𝕜 : Type u_2
inst_2 : RCLike 𝕜
h : Eq (α := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) RCLike.I : ℝ) (1 : ℝ)
x y : 𝕜
⊢ (↑((RCLike.re : (a : 𝕜) → ℝ) (x * y)) : ℂ) + (↑((RCLike.im : (a : 𝕜) → ℝ) (x * y)) : ℂ) * I =
    ((↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) + (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * I) *
      ((↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) + (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) * I)
have simp : (↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) -
      (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) +
    ((↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) +
        (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ)) *
      I =
  ((↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) + (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * I) *
    ((↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) + (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) * I)
Tactic: simp only [RCLike.mul_re, ofReal_sub, ofReal_mul, RCLike.mul_im, ofReal_add]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
z : ℂ
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℂ E
𝕜 : Type u_2
inst_2 : RCLike 𝕜
h : Eq (α := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) RCLike.I : ℝ) (1 : ℝ)
x y : 𝕜
⊢ (↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) -
        (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) +
      ((↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) +
          (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ)) *
        I =
    ((↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) + (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * I) *
      ((↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) + (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) * I)
have ring_nf : (↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) +
        (↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) * I +
      (↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * I -
    (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) =
  (↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) +
        (↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) * I +
      (↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * I +
    (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) * HPow.hPow (β := ℕ) I 2
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
z : ℂ
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℂ E
𝕜 : Type u_2
inst_2 : RCLike 𝕜
h : Eq (α := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) RCLike.I : ℝ) (1 : ℝ)
x y : 𝕜
⊢ (↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) +
          (↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) * I +
        (↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * I -
      (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) =
    (↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) +
          (↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) * I +
        (↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * I +
      (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) * HPow.hPow (β := ℕ) I 2
have rw : (↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) +
        (↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) * I +
      (↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * I -
    (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) =
  (↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) +
        (↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) * I +
      (↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * I +
    (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) * -1
Tactic: rw [I_sq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
z : ℂ
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℂ E
𝕜 : Type u_2
inst_2 : RCLike 𝕜
h : Eq (α := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) RCLike.I : ℝ) (1 : ℝ)
x y : 𝕜
⊢ (↑((RCLike.re : (a : 𝕜) → ℝ) (x + y)) : ℂ) + (↑((RCLike.im : (a : 𝕜) → ℝ) (x + y)) : ℂ) * I =
    (↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) + (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * I +
      ((↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) + (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) * I)
have simp : (↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) + (↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) +
    ((↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) + (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ)) * I =
  (↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) + (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * I +
    ((↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) + (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) * I)
Tactic: simp only [map_add, ofReal_add]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
𝕜 : Type u_2
𝕜' : Type u_3
inst : RCLike 𝕜
inst_1 : RCLike 𝕜'
h : Eq (α := ℝ) ((RCLike.im : (a : 𝕜') → ℝ) RCLike.I : ℝ) (1 : ℝ)
a : 𝕜
⊢ LE.le.{u_3} (α := 𝕜') (0 : 𝕜') ((RCLike.map 𝕜 𝕜' : (a : 𝕜) → 𝕜') a : 𝕜') ↔ 0 ≤ a
have rw : LE.le (α := ℝ) (0 : ℝ) ((RCLike.re : (a : 𝕜') → ℝ) ((RCLike.map 𝕜 𝕜' : (a : 𝕜) → 𝕜') a : 𝕜') : ℝ) ∧
    Eq (α := ℝ) ((RCLike.im : (a : 𝕜') → ℝ) ((RCLike.map 𝕜 𝕜' : (a : 𝕜) → 𝕜') a : 𝕜') : ℝ) (0 : ℝ) ↔
  LE.le (α := ℝ) (0 : ℝ) ((RCLike.re : (a : 𝕜) → ℝ) a : ℝ) ∧ Eq (α := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) a : ℝ) (0 : ℝ)
Tactic: rw [RCLike.nonneg_iff, RCLike.nonneg_iff (K := 𝕜)]