awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z w : ℂ
⊢ dist z w = √(HPow.hPow (β := ℕ) (z.re - w.re) 2 + HPow.hPow (β := ℕ) (z.im - w.im) 2)
have rw : ‖z - w‖ = √((z.re - w.re) * (z.re - w.re) + (z.im - w.im) * (z.im - w.im))
Tactic: rw [sq, sq, dist_eq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z w : ℂ
h : z.re = w.re
⊢ dist z w = dist z.im w.im
have rw : √(HPow.hPow (β := ℕ) (z.re - w.re) 2 + HPow.hPow (β := ℕ) (z.im - w.im) 2) = dist z.im w.im
Tactic: rw [dist_eq_re_im, h, sub_self, zero_pow two_ne_zero, zero_add, Real.sqrt_sq_eq_abs, Real.dist_eq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z w : ℂ
h : z.re = w.re
rw : √(HPow.hPow (β := ℕ) (z.re - w.re) 2 + HPow.hPow (β := ℕ) (z.im - w.im) 2) = dist z.im w.im
⊢ dist z w = dist z.im w.im
have rw₁ : √(HPow.hPow (β := ℕ) (w.re - w.re) 2 + HPow.hPow (β := ℕ) (z.im - w.im) 2) = dist z.im w.im
Tactic: rw [dist_eq_re_im, h, sub_self, zero_pow two_ne_zero, zero_add, Real.sqrt_sq_eq_abs, Real.dist_eq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z w : ℂ
h : z.re = w.re
rw : √(HPow.hPow (β := ℕ) (z.re - w.re) 2 + HPow.hPow (β := ℕ) (z.im - w.im) 2) = dist z.im w.im
rw₁ : √(HPow.hPow (β := ℕ) (w.re - w.re) 2 + HPow.hPow (β := ℕ) (z.im - w.im) 2) = dist z.im w.im
⊢ dist z w = dist z.im w.im
have rw₂ : √(HPow.hPow (α := ℝ) (β := ℕ) 0 2 + HPow.hPow (β := ℕ) (z.im - w.im) 2) = dist z.im w.im
Tactic: rw [dist_eq_re_im, h, sub_self, zero_pow two_ne_zero, zero_add, Real.sqrt_sq_eq_abs, Real.dist_eq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z w : ℂ
h : z.re = w.re
rw : √(HPow.hPow (β := ℕ) (z.re - w.re) 2 + HPow.hPow (β := ℕ) (z.im - w.im) 2) = dist z.im w.im
rw₁ : √(HPow.hPow (β := ℕ) (w.re - w.re) 2 + HPow.hPow (β := ℕ) (z.im - w.im) 2) = dist z.im w.im
rw₂ : √(HPow.hPow (α := ℝ) (β := ℕ) 0 2 + HPow.hPow (β := ℕ) (z.im - w.im) 2) = dist z.im w.im
⊢ dist z w = dist z.im w.im
have rw₃ : √(0 + HPow.hPow (β := ℕ) (z.im - w.im) 2) = dist z.im w.im
Tactic: rw [dist_eq_re_im, h, sub_self, zero_pow two_ne_zero, zero_add, Real.sqrt_sq_eq_abs, Real.dist_eq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z w : ℂ
h : z.re = w.re
rw : √(HPow.hPow (β := ℕ) (z.re - w.re) 2 + HPow.hPow (β := ℕ) (z.im - w.im) 2) = dist z.im w.im
rw₁ : √(HPow.hPow (β := ℕ) (w.re - w.re) 2 + HPow.hPow (β := ℕ) (z.im - w.im) 2) = dist z.im w.im
rw₂ : √(HPow.hPow (α := ℝ) (β := ℕ) 0 2 + HPow.hPow (β := ℕ) (z.im - w.im) 2) = dist z.im w.im
rw₃ : √(0 + HPow.hPow (β := ℕ) (z.im - w.im) 2) = dist z.im w.im
⊢ dist z w = dist z.im w.im
have rw₄ : √(HPow.hPow (β := ℕ) (z.im - w.im) 2) = dist z.im w.im
Tactic: rw [dist_eq_re_im, h, sub_self, zero_pow two_ne_zero, zero_add, Real.sqrt_sq_eq_abs, Real.dist_eq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z w : ℂ
h : z.re = w.re
rw : √(HPow.hPow (β := ℕ) (z.re - w.re) 2 + HPow.hPow (β := ℕ) (z.im - w.im) 2) = dist z.im w.im
rw₁ : √(HPow.hPow (β := ℕ) (w.re - w.re) 2 + HPow.hPow (β := ℕ) (z.im - w.im) 2) = dist z.im w.im
rw₂ : √(HPow.hPow (α := ℝ) (β := ℕ) 0 2 + HPow.hPow (β := ℕ) (z.im - w.im) 2) = dist z.im w.im
rw₃ : √(0 + HPow.hPow (β := ℕ) (z.im - w.im) 2) = dist z.im w.im
rw₄ : √(HPow.hPow (β := ℕ) (z.im - w.im) 2) = dist z.im w.im
⊢ dist z w = dist z.im w.im
have rw₅ : |z.im - w.im| = dist z.im w.im
Tactic: rw [dist_eq_re_im, h, sub_self, zero_pow two_ne_zero, zero_add, Real.sqrt_sq_eq_abs, Real.dist_eq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z w : ℂ
h : z.re = w.re
rw : √(HPow.hPow (β := ℕ) (z.re - w.re) 2 + HPow.hPow (β := ℕ) (z.im - w.im) 2) = dist z.im w.im
rw₁ : √(HPow.hPow (β := ℕ) (w.re - w.re) 2 + HPow.hPow (β := ℕ) (z.im - w.im) 2) = dist z.im w.im
rw₂ : √(HPow.hPow (α := ℝ) (β := ℕ) 0 2 + HPow.hPow (β := ℕ) (z.im - w.im) 2) = dist z.im w.im
rw₃ : √(0 + HPow.hPow (β := ℕ) (z.im - w.im) 2) = dist z.im w.im
rw₄ : √(HPow.hPow (β := ℕ) (z.im - w.im) 2) = dist z.im w.im
rw₅ : |z.im - w.im| = dist z.im w.im
⊢ dist z w = dist z.im w.im
have rw₆ : |z.im - w.im| = |z.im - w.im|
Tactic: rw [dist_eq_re_im, h, sub_self, zero_pow two_ne_zero, zero_add, Real.sqrt_sq_eq_abs, Real.dist_eq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z w : ℂ
h : z.re = w.re
⊢ edist z w = edist z.im w.im
have rw : (↑(nndist z w) : ENNReal) = edist z.im w.im
Tactic: rw [edist_nndist, edist_nndist, nndist_of_re_eq h]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z w : ℂ
h : z.re = w.re
rw : (↑(nndist z w) : ENNReal) = edist z.im w.im
⊢ edist z w = edist z.im w.im
have rw₁ : (↑(nndist z w) : ENNReal) = (↑(nndist z.im w.im) : ENNReal)
Tactic: rw [edist_nndist, edist_nndist, nndist_of_re_eq h]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z w : ℂ
h : z.re = w.re
rw : (↑(nndist z w) : ENNReal) = edist z.im w.im
rw₁ : (↑(nndist z w) : ENNReal) = (↑(nndist z.im w.im) : ENNReal)
⊢ edist z w = edist z.im w.im
have rw₂ : (↑(nndist z.im w.im) : ENNReal) = (↑(nndist z.im w.im) : ENNReal)
Tactic: rw [edist_nndist, edist_nndist, nndist_of_re_eq h]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z w : ℂ
h : z.im = w.im
⊢ dist z w = dist z.re w.re
have rw : √(HPow.hPow (β := ℕ) (z.re - w.re) 2 + HPow.hPow (β := ℕ) (z.im - w.im) 2) = dist z.re w.re
Tactic: rw [dist_eq_re_im, h, sub_self, zero_pow two_ne_zero, add_zero, Real.sqrt_sq_eq_abs, Real.dist_eq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z w : ℂ
h : z.im = w.im
rw : √(HPow.hPow (β := ℕ) (z.re - w.re) 2 + HPow.hPow (β := ℕ) (z.im - w.im) 2) = dist z.re w.re
⊢ dist z w = dist z.re w.re
have rw₁ : √(HPow.hPow (β := ℕ) (z.re - w.re) 2 + HPow.hPow (β := ℕ) (w.im - w.im) 2) = dist z.re w.re
Tactic: rw [dist_eq_re_im, h, sub_self, zero_pow two_ne_zero, add_zero, Real.sqrt_sq_eq_abs, Real.dist_eq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z w : ℂ
h : z.im = w.im
rw : √(HPow.hPow (β := ℕ) (z.re - w.re) 2 + HPow.hPow (β := ℕ) (z.im - w.im) 2) = dist z.re w.re
rw₁ : √(HPow.hPow (β := ℕ) (z.re - w.re) 2 + HPow.hPow (β := ℕ) (w.im - w.im) 2) = dist z.re w.re
⊢ dist z w = dist z.re w.re
have rw₂ : √(HPow.hPow (β := ℕ) (z.re - w.re) 2 + HPow.hPow (α := ℝ) (β := ℕ) 0 2) = dist z.re w.re
Tactic: rw [dist_eq_re_im, h, sub_self, zero_pow two_ne_zero, add_zero, Real.sqrt_sq_eq_abs, Real.dist_eq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z w : ℂ
h : z.im = w.im
rw : √(HPow.hPow (β := ℕ) (z.re - w.re) 2 + HPow.hPow (β := ℕ) (z.im - w.im) 2) = dist z.re w.re
rw₁ : √(HPow.hPow (β := ℕ) (z.re - w.re) 2 + HPow.hPow (β := ℕ) (w.im - w.im) 2) = dist z.re w.re
rw₂ : √(HPow.hPow (β := ℕ) (z.re - w.re) 2 + HPow.hPow (α := ℝ) (β := ℕ) 0 2) = dist z.re w.re
⊢ dist z w = dist z.re w.re
have rw₃ : √(HPow.hPow (β := ℕ) (z.re - w.re) 2 + 0) = dist z.re w.re
Tactic: rw [dist_eq_re_im, h, sub_self, zero_pow two_ne_zero, add_zero, Real.sqrt_sq_eq_abs, Real.dist_eq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z w : ℂ
h : z.im = w.im
rw : √(HPow.hPow (β := ℕ) (z.re - w.re) 2 + HPow.hPow (β := ℕ) (z.im - w.im) 2) = dist z.re w.re
rw₁ : √(HPow.hPow (β := ℕ) (z.re - w.re) 2 + HPow.hPow (β := ℕ) (w.im - w.im) 2) = dist z.re w.re
rw₂ : √(HPow.hPow (β := ℕ) (z.re - w.re) 2 + HPow.hPow (α := ℝ) (β := ℕ) 0 2) = dist z.re w.re
rw₃ : √(HPow.hPow (β := ℕ) (z.re - w.re) 2 + 0) = dist z.re w.re
⊢ dist z w = dist z.re w.re
have rw₄ : √(HPow.hPow (β := ℕ) (z.re - w.re) 2) = dist z.re w.re
Tactic: rw [dist_eq_re_im, h, sub_self, zero_pow two_ne_zero, add_zero, Real.sqrt_sq_eq_abs, Real.dist_eq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z w : ℂ
h : z.im = w.im
rw : √(HPow.hPow (β := ℕ) (z.re - w.re) 2 + HPow.hPow (β := ℕ) (z.im - w.im) 2) = dist z.re w.re
rw₁ : √(HPow.hPow (β := ℕ) (z.re - w.re) 2 + HPow.hPow (β := ℕ) (w.im - w.im) 2) = dist z.re w.re
rw₂ : √(HPow.hPow (β := ℕ) (z.re - w.re) 2 + HPow.hPow (α := ℝ) (β := ℕ) 0 2) = dist z.re w.re
rw₃ : √(HPow.hPow (β := ℕ) (z.re - w.re) 2 + 0) = dist z.re w.re
rw₄ : √(HPow.hPow (β := ℕ) (z.re - w.re) 2) = dist z.re w.re
⊢ dist z w = dist z.re w.re
have rw₅ : |z.re - w.re| = dist z.re w.re
Tactic: rw [dist_eq_re_im, h, sub_self, zero_pow two_ne_zero, add_zero, Real.sqrt_sq_eq_abs, Real.dist_eq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z w : ℂ
h : z.im = w.im
rw : √(HPow.hPow (β := ℕ) (z.re - w.re) 2 + HPow.hPow (β := ℕ) (z.im - w.im) 2) = dist z.re w.re
rw₁ : √(HPow.hPow (β := ℕ) (z.re - w.re) 2 + HPow.hPow (β := ℕ) (w.im - w.im) 2) = dist z.re w.re
rw₂ : √(HPow.hPow (β := ℕ) (z.re - w.re) 2 + HPow.hPow (α := ℝ) (β := ℕ) 0 2) = dist z.re w.re
rw₃ : √(HPow.hPow (β := ℕ) (z.re - w.re) 2 + 0) = dist z.re w.re
rw₄ : √(HPow.hPow (β := ℕ) (z.re - w.re) 2) = dist z.re w.re
rw₅ : |z.re - w.re| = dist z.re w.re
⊢ dist z w = dist z.re w.re
have rw₆ : |z.re - w.re| = |z.re - w.re|
Tactic: rw [dist_eq_re_im, h, sub_self, zero_pow two_ne_zero, add_zero, Real.sqrt_sq_eq_abs, Real.dist_eq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z w : ℂ
h : z.im = w.im
⊢ edist z w = edist z.re w.re
have rw : (↑(nndist z w) : ENNReal) = edist z.re w.re
Tactic: rw [edist_nndist, edist_nndist, nndist_of_im_eq h]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z w : ℂ
h : z.im = w.im
rw : (↑(nndist z w) : ENNReal) = edist z.re w.re
⊢ edist z w = edist z.re w.re
have rw₁ : (↑(nndist z w) : ENNReal) = (↑(nndist z.re w.re) : ENNReal)
Tactic: rw [edist_nndist, edist_nndist, nndist_of_im_eq h]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z w : ℂ
h : z.im = w.im
rw : (↑(nndist z w) : ENNReal) = edist z.re w.re
rw₁ : (↑(nndist z w) : ENNReal) = (↑(nndist z.re w.re) : ENNReal)
⊢ edist z w = edist z.re w.re
have rw₂ : (↑(nndist z.re w.re) : ENNReal) = (↑(nndist z.re w.re) : ENNReal)
Tactic: rw [edist_nndist, edist_nndist, nndist_of_im_eq h]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
⊢ dist ((starRingEnd ℂ : (a : ℂ) → ℂ) z) z = 2 * |z.im|
have rw : dist (im ((starRingEnd ℂ : (a : ℂ) → ℂ) z)) z.im = 2 * |z.im|
Tactic: rw [dist_of_re_eq (conj_re z), conj_im, dist_comm, Real.dist_eq, sub_neg_eq_add, ← two_mul,
    _root_.abs_mul, abs_of_pos (zero_lt_two' ℝ)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
rw : dist (im ((starRingEnd ℂ : (a : ℂ) → ℂ) z)) z.im = 2 * |z.im|
⊢ dist ((starRingEnd ℂ : (a : ℂ) → ℂ) z) z = 2 * |z.im|
have rw₁ : dist (-z.im) z.im = 2 * |z.im|
Tactic: rw [dist_of_re_eq (conj_re z), conj_im, dist_comm, Real.dist_eq, sub_neg_eq_add, ← two_mul,
    _root_.abs_mul, abs_of_pos (zero_lt_two' ℝ)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
rw : dist (im ((starRingEnd ℂ : (a : ℂ) → ℂ) z)) z.im = 2 * |z.im|
rw₁ : dist (-z.im) z.im = 2 * |z.im|
⊢ dist ((starRingEnd ℂ : (a : ℂ) → ℂ) z) z = 2 * |z.im|
have rw₂ : dist z.im (-z.im) = 2 * |z.im|
Tactic: rw [dist_of_re_eq (conj_re z), conj_im, dist_comm, Real.dist_eq, sub_neg_eq_add, ← two_mul,
    _root_.abs_mul, abs_of_pos (zero_lt_two' ℝ)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
rw : dist (im ((starRingEnd ℂ : (a : ℂ) → ℂ) z)) z.im = 2 * |z.im|
rw₁ : dist (-z.im) z.im = 2 * |z.im|
rw₂ : dist z.im (-z.im) = 2 * |z.im|
⊢ dist ((starRingEnd ℂ : (a : ℂ) → ℂ) z) z = 2 * |z.im|
have rw₃ : |z.im - -z.im| = 2 * |z.im|
Tactic: rw [dist_of_re_eq (conj_re z), conj_im, dist_comm, Real.dist_eq, sub_neg_eq_add, ← two_mul,
    _root_.abs_mul, abs_of_pos (zero_lt_two' ℝ)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
rw : dist (im ((starRingEnd ℂ : (a : ℂ) → ℂ) z)) z.im = 2 * |z.im|
rw₁ : dist (-z.im) z.im = 2 * |z.im|
rw₂ : dist z.im (-z.im) = 2 * |z.im|
rw₃ : |z.im - -z.im| = 2 * |z.im|
⊢ dist ((starRingEnd ℂ : (a : ℂ) → ℂ) z) z = 2 * |z.im|
have rw₄ : |z.im + z.im| = 2 * |z.im|
Tactic: rw [dist_of_re_eq (conj_re z), conj_im, dist_comm, Real.dist_eq, sub_neg_eq_add, ← two_mul,
    _root_.abs_mul, abs_of_pos (zero_lt_two' ℝ)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
rw : dist (im ((starRingEnd ℂ : (a : ℂ) → ℂ) z)) z.im = 2 * |z.im|
rw₁ : dist (-z.im) z.im = 2 * |z.im|
rw₂ : dist z.im (-z.im) = 2 * |z.im|
rw₃ : |z.im - -z.im| = 2 * |z.im|
rw₄ : |z.im + z.im| = 2 * |z.im|
⊢ dist ((starRingEnd ℂ : (a : ℂ) → ℂ) z) z = 2 * |z.im|
have rw₅ : |2 * z.im| = 2 * |z.im|
Tactic: rw [dist_of_re_eq (conj_re z), conj_im, dist_comm, Real.dist_eq, sub_neg_eq_add, ← two_mul,
    _root_.abs_mul, abs_of_pos (zero_lt_two' ℝ)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
rw : dist (im ((starRingEnd ℂ : (a : ℂ) → ℂ) z)) z.im = 2 * |z.im|
rw₁ : dist (-z.im) z.im = 2 * |z.im|
rw₂ : dist z.im (-z.im) = 2 * |z.im|
rw₃ : |z.im - -z.im| = 2 * |z.im|
rw₄ : |z.im + z.im| = 2 * |z.im|
rw₅ : |2 * z.im| = 2 * |z.im|
⊢ dist ((starRingEnd ℂ : (a : ℂ) → ℂ) z) z = 2 * |z.im|
have rw₆ : |2| * |z.im| = 2 * |z.im|
Tactic: rw [dist_of_re_eq (conj_re z), conj_im, dist_comm, Real.dist_eq, sub_neg_eq_add, ← two_mul,
    _root_.abs_mul, abs_of_pos (zero_lt_two' ℝ)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
rw : dist (im ((starRingEnd ℂ : (a : ℂ) → ℂ) z)) z.im = 2 * |z.im|
rw₁ : dist (-z.im) z.im = 2 * |z.im|
rw₂ : dist z.im (-z.im) = 2 * |z.im|
rw₃ : |z.im - -z.im| = 2 * |z.im|
rw₄ : |z.im + z.im| = 2 * |z.im|
rw₅ : |2 * z.im| = 2 * |z.im|
rw₆ : |2| * |z.im| = 2 * |z.im|
⊢ dist ((starRingEnd ℂ : (a : ℂ) → ℂ) z) z = 2 * |z.im|
have rw₇ : 2 * |z.im| = 2 * |z.im|
Tactic: rw [dist_of_re_eq (conj_re z), conj_im, dist_comm, Real.dist_eq, sub_neg_eq_add, ← two_mul,
    _root_.abs_mul, abs_of_pos (zero_lt_two' ℝ)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
⊢ (↑(nndist ((starRingEnd ℂ : (a : ℂ) → ℂ) z) z) : ℝ) =
    (↑(HMul.hMul (α := NNReal) (β := NNReal) (2 : NNReal) ((Real.nnabs : (a : ℝ) → NNReal) z.im : NNReal)) : ℝ)
have rw : dist ((starRingEnd ℂ : (a : ℂ) → ℂ) z) z =
  (↑(HMul.hMul (α := NNReal) (β := NNReal) (2 : NNReal) ((Real.nnabs : (a : ℝ) → NNReal) z.im : NNReal)) : ℝ)
Tactic: rw [← dist_nndist, NNReal.coe_mul, NNReal.coe_two, Real.coe_nnabs, dist_conj_self]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
rw :
  dist ((starRingEnd ℂ : (a : ℂ) → ℂ) z) z =
    (↑(HMul.hMul (α := NNReal) (β := NNReal) (2 : NNReal) ((Real.nnabs : (a : ℝ) → NNReal) z.im : NNReal)) : ℝ)
⊢ (↑(nndist ((starRingEnd ℂ : (a : ℂ) → ℂ) z) z) : ℝ) =
    (↑(HMul.hMul (α := NNReal) (β := NNReal) (2 : NNReal) ((Real.nnabs : (a : ℝ) → NNReal) z.im : NNReal)) : ℝ)
have rw₁ : dist ((starRingEnd ℂ : (a : ℂ) → ℂ) z) z = (↑2 : ℝ) * (↑((Real.nnabs : (a : ℝ) → NNReal) z.im) : ℝ)
Tactic: rw [← dist_nndist, NNReal.coe_mul, NNReal.coe_two, Real.coe_nnabs, dist_conj_self]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
rw :
  dist ((starRingEnd ℂ : (a : ℂ) → ℂ) z) z =
    (↑(HMul.hMul (α := NNReal) (β := NNReal) (2 : NNReal) ((Real.nnabs : (a : ℝ) → NNReal) z.im : NNReal)) : ℝ)
rw₁ : dist ((starRingEnd ℂ : (a : ℂ) → ℂ) z) z = (↑2 : ℝ) * (↑((Real.nnabs : (a : ℝ) → NNReal) z.im) : ℝ)
⊢ (↑(nndist ((starRingEnd ℂ : (a : ℂ) → ℂ) z) z) : ℝ) =
    (↑(HMul.hMul (α := NNReal) (β := NNReal) (2 : NNReal) ((Real.nnabs : (a : ℝ) → NNReal) z.im : NNReal)) : ℝ)
have rw₂ : dist ((starRingEnd ℂ : (a : ℂ) → ℂ) z) z = 2 * (↑((Real.nnabs : (a : ℝ) → NNReal) z.im) : ℝ)
Tactic: rw [← dist_nndist, NNReal.coe_mul, NNReal.coe_two, Real.coe_nnabs, dist_conj_self]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
rw :
  dist ((starRingEnd ℂ : (a : ℂ) → ℂ) z) z =
    (↑(HMul.hMul (α := NNReal) (β := NNReal) (2 : NNReal) ((Real.nnabs : (a : ℝ) → NNReal) z.im : NNReal)) : ℝ)
rw₁ : dist ((starRingEnd ℂ : (a : ℂ) → ℂ) z) z = (↑2 : ℝ) * (↑((Real.nnabs : (a : ℝ) → NNReal) z.im) : ℝ)
rw₂ : dist ((starRingEnd ℂ : (a : ℂ) → ℂ) z) z = 2 * (↑((Real.nnabs : (a : ℝ) → NNReal) z.im) : ℝ)
⊢ (↑(nndist ((starRingEnd ℂ : (a : ℂ) → ℂ) z) z) : ℝ) =
    (↑(HMul.hMul (α := NNReal) (β := NNReal) (2 : NNReal) ((Real.nnabs : (a : ℝ) → NNReal) z.im : NNReal)) : ℝ)
have rw₃ : dist ((starRingEnd ℂ : (a : ℂ) → ℂ) z) z = 2 * |z.im|
Tactic: rw [← dist_nndist, NNReal.coe_mul, NNReal.coe_two, Real.coe_nnabs, dist_conj_self]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
rw :
  dist ((starRingEnd ℂ : (a : ℂ) → ℂ) z) z =
    (↑(HMul.hMul (α := NNReal) (β := NNReal) (2 : NNReal) ((Real.nnabs : (a : ℝ) → NNReal) z.im : NNReal)) : ℝ)
rw₁ : dist ((starRingEnd ℂ : (a : ℂ) → ℂ) z) z = (↑2 : ℝ) * (↑((Real.nnabs : (a : ℝ) → NNReal) z.im) : ℝ)
rw₂ : dist ((starRingEnd ℂ : (a : ℂ) → ℂ) z) z = 2 * (↑((Real.nnabs : (a : ℝ) → NNReal) z.im) : ℝ)
rw₃ : dist ((starRingEnd ℂ : (a : ℂ) → ℂ) z) z = 2 * |z.im|
⊢ (↑(nndist ((starRingEnd ℂ : (a : ℂ) → ℂ) z) z) : ℝ) =
    (↑(HMul.hMul (α := NNReal) (β := NNReal) (2 : NNReal) ((Real.nnabs : (a : ℝ) → NNReal) z.im : NNReal)) : ℝ)
have rw₄ : 2 * |z.im| = 2 * |z.im|
Tactic: rw [← dist_nndist, NNReal.coe_mul, NNReal.coe_two, Real.coe_nnabs, dist_conj_self]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
⊢ dist z ((starRingEnd ℂ : (a : ℂ) → ℂ) z) = 2 * |z.im|
have rw : dist ((starRingEnd ℂ : (a : ℂ) → ℂ) z) z = 2 * |z.im|
Tactic: rw [dist_comm, dist_conj_self]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
rw : dist ((starRingEnd ℂ : (a : ℂ) → ℂ) z) z = 2 * |z.im|
⊢ dist z ((starRingEnd ℂ : (a : ℂ) → ℂ) z) = 2 * |z.im|
have rw₁ : 2 * |z.im| = 2 * |z.im|
Tactic: rw [dist_comm, dist_conj_self]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
⊢ nndist z ((starRingEnd ℂ : (a : ℂ) → ℂ) z) =
    HMul.hMul (α := NNReal) (β := NNReal) (2 : NNReal) ((Real.nnabs : (a : ℝ) → NNReal) z.im : NNReal)
have rw : nndist ((starRingEnd ℂ : (a : ℂ) → ℂ) z) z =
  HMul.hMul (α := NNReal) (β := NNReal) (2 : NNReal) ((Real.nnabs : (a : ℝ) → NNReal) z.im : NNReal)
Tactic: rw [nndist_comm, nndist_conj_self]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
rw :
  nndist ((starRingEnd ℂ : (a : ℂ) → ℂ) z) z =
    HMul.hMul (α := NNReal) (β := NNReal) (2 : NNReal) ((Real.nnabs : (a : ℝ) → NNReal) z.im : NNReal)
⊢ nndist z ((starRingEnd ℂ : (a : ℂ) → ℂ) z) =
    HMul.hMul (α := NNReal) (β := NNReal) (2 : NNReal) ((Real.nnabs : (a : ℝ) → NNReal) z.im : NNReal)
have rw₁ : HMul.hMul (α := NNReal) (β := NNReal) (2 : NNReal) ((Real.nnabs : (a : ℝ) → NNReal) z.im : NNReal) =
  HMul.hMul (α := NNReal) (β := NNReal) (2 : NNReal) ((Real.nnabs : (a : ℝ) → NNReal) z.im : NNReal)
Tactic: rw [nndist_comm, nndist_conj_self]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (hypothesis)
Goal:
f : CauSeq (α := ℝ) ℂ fun (x : ℂ) ↦ ‖x‖
ε : ℝ
ε0 : ε > 0
x : ℕ
H :
  ∀ j ≥ x,
    |(↑(Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑f : ℕ → ℂ) n).re) ⋯ -
                  CauSeq.const abs
                    (CauSeq.lim
                      (Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑f : ℕ → ℂ) n).re) ⋯))) :
              ℕ → ℝ)
            j| <
        ε / 2 ∧
      |(↑(Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑f : ℕ → ℂ) n).im) ⋯ -
                  CauSeq.const abs
                    (CauSeq.lim
                      (Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑f : ℕ → ℂ) n).im) ⋯))) :
              ℕ → ℝ)
            j| <
        ε / 2
j : ℕ
ij : j ≥ x
⊢ (fun (x : ℂ) ↦ ‖x‖) ((↑(f - CauSeq.const (fun (x : ℂ) ↦ ‖x‖) (limAux f)) : ℕ → ℂ) j) < ε
have H₁ : |(↑(Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑f : ℕ → ℂ) n).re) sorry -
            CauSeq.const abs
              (CauSeq.lim (Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑f : ℕ → ℂ) n).re) sorry))) :
        ℕ → ℝ)
      j| <
  ε / 2
Tactic: obtain ⟨H₁, H₂⟩ := H _ ij
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (hypothesis)
Goal:
f : CauSeq (α := ℝ) ℂ fun (x : ℂ) ↦ ‖x‖
ε : ℝ
ε0 : ε > 0
x : ℕ
H :
  ∀ j ≥ x,
    |(↑(Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑f : ℕ → ℂ) n).re) ⋯ -
                  CauSeq.const abs
                    (CauSeq.lim
                      (Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑f : ℕ → ℂ) n).re) ⋯))) :
              ℕ → ℝ)
            j| <
        ε / 2 ∧
      |(↑(Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑f : ℕ → ℂ) n).im) ⋯ -
                  CauSeq.const abs
                    (CauSeq.lim
                      (Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑f : ℕ → ℂ) n).im) ⋯))) :
              ℕ → ℝ)
            j| <
        ε / 2
j : ℕ
ij : j ≥ x
H₁ :
  |(↑(Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑f : ℕ → ℂ) n).re) ⋯ -
              CauSeq.const abs
                (CauSeq.lim
                  (Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑f : ℕ → ℂ) n).re) ⋯))) :
          ℕ → ℝ)
        j| <
    ε / 2
⊢ (fun (x : ℂ) ↦ ‖x‖) ((↑(f - CauSeq.const (fun (x : ℂ) ↦ ‖x‖) (limAux f)) : ℕ → ℂ) j) < ε
have H₂ : |(↑(Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑f : ℕ → ℂ) n).im) sorry -
            CauSeq.const abs
              (CauSeq.lim (Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑f : ℕ → ℂ) n).im) sorry))) :
        ℕ → ℝ)
      j| <
  ε / 2
Tactic: obtain ⟨H₁, H₂⟩ := H _ ij
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
f : CauSeq (α := ℝ) ℂ fun (x : ℂ) ↦ ‖x‖
ε : ℝ
ε0 : ε > 0
x : ℕ
H :
  ∀ j ≥ x,
    |(↑(Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑f : ℕ → ℂ) n).re) ⋯ -
                  CauSeq.const abs
                    (CauSeq.lim
                      (Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑f : ℕ → ℂ) n).re) ⋯))) :
              ℕ → ℝ)
            j| <
        ε / 2 ∧
      |(↑(Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑f : ℕ → ℂ) n).im) ⋯ -
                  CauSeq.const abs
                    (CauSeq.lim
                      (Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑f : ℕ → ℂ) n).im) ⋯))) :
              ℕ → ℝ)
            j| <
        ε / 2
j : ℕ
ij : j ≥ x
H₁ :
  |(↑(Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑f : ℕ → ℂ) n).re) ⋯ -
              CauSeq.const abs
                (CauSeq.lim
                  (Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑f : ℕ → ℂ) n).re) ⋯))) :
          ℕ → ℝ)
        j| <
    ε / 2
H₂ :
  |(↑(Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑f : ℕ → ℂ) n).im) ⋯ -
              CauSeq.const abs
                (CauSeq.lim
                  (Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑f : ℕ → ℂ) n).im) ⋯))) :
          ℕ → ℝ)
        j| <
    ε / 2
⊢ (fun (x : ℂ) ↦ ‖x‖) ((↑(f - CauSeq.const (fun (x : ℂ) ↦ ‖x‖) (limAux f)) : ℕ → ℂ) j) < ε
have apply : |((↑(f - CauSeq.const (fun (x : ℂ) ↦ ‖x‖) (limAux f)) : ℕ → ℂ) j).re| +
    |((↑(f - CauSeq.const (fun (x : ℂ) ↦ ‖x‖) (limAux f)) : ℕ → ℂ) j).im| <
  ε
Tactic: apply lt_of_le_of_lt (norm_le_abs_re_add_abs_im _)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
f : CauSeq (α := ℝ) ℂ fun (x : ℂ) ↦ ‖x‖
⊢ (cauSeqRe f).lim = f.lim.re
have rw : (cauSeqRe f).lim = ((↑(cauSeqRe f).lim : ℂ) + (↑(cauSeqIm f).lim : ℂ) * I).re
Tactic: rw [lim_eq_lim_im_add_lim_re]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
f : CauSeq (α := ℝ) ℂ fun (x : ℂ) ↦ ‖x‖
⊢ (cauSeqIm f).lim = f.lim.im
have rw : (cauSeqIm f).lim = ((↑(cauSeqRe f).lim : ℂ) + (↑(cauSeqIm f).lim : ℂ) * I).im
Tactic: rw [lim_eq_lim_im_add_lim_re]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
f : CauSeq (α := ℝ) ℂ fun (x : ℂ) ↦ ‖x‖
ε : ℝ
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, (fun (x : ℂ) ↦ ‖x‖) ((↑f : ℕ → ℂ) j - (↑f : ℕ → ℂ) i) < ε
j : ℕ
hj : j ≥ i
⊢ (fun (x : ℂ) ↦ ‖x‖)
      (HSub.hSub (α := ℂ) ((fun (n : ℕ) ↦ ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑f : ℕ → ℂ) n) : ℂ)) j)
        ((fun (n : ℕ) ↦ ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑f : ℕ → ℂ) n) : ℂ)) i)) <
    ε
have simp_rw : ‖(↑f : ℕ → ℂ) j - (↑f : ℕ → ℂ) i‖ < ε
Tactic: simp_rw [← map_sub, norm_conj]