awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
x : ℂ
rw : LT.lt (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) x : ℝ) ↔ 1 < HPow.hPow (β := ℕ) ‖x‖ 2
rw₁ rw₂ : 1 < HPow.hPow (β := ℕ) ‖x‖ 2 ↔ 1 < HPow.hPow (β := ℕ) ‖x‖ 2
⊢ LT.lt (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) x : ℝ) ↔ 1 < ‖x‖

Tactic:
rw [← one_lt_sq_iff₀ (norm_nonneg _), normSq_eq_norm_sq]

Premises used: one_lt_sq_iff₀, Complex.normSq_eq_norm_sq, norm_nonneg
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
x : ℂ
rw : LE.le (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) x : ℝ) ↔ 1 ≤ HPow.hPow (β := ℕ) ‖x‖ 2
rw₁ rw₂ : 1 ≤ HPow.hPow (β := ℕ) ‖x‖ 2 ↔ 1 ≤ HPow.hPow (β := ℕ) ‖x‖ 2
⊢ LE.le (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) x : ℝ) ↔ 1 ≤ ‖x‖

Tactic:
rw [← one_le_sq_iff₀ (norm_nonneg _), normSq_eq_norm_sq]

Premises used: Complex.normSq_eq_norm_sq, one_le_sq_iff₀, norm_nonneg
-- Module: Mathlib.Analysis.Complex.Norm
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
rw₄ rw₅ : HPow.hPow (β := ℕ) z.im 2 = HPow.hPow (β := ℕ) z.im 2
⊢ HPow.hPow (β := ℕ) ‖z‖ 2 - HPow.hPow (β := ℕ) z.re 2 = HPow.hPow (β := ℕ) z.im 2

Tactic:
rw [Complex.sq_norm, normSq_apply, ← sq, ← sq, add_sub_cancel_left]

Premises used: add_sub_cancel_left, Complex.sq_norm, sq, Complex.normSq_apply
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z : ℂ
rw : HPow.hPow (β := ℕ) ‖z‖ 2 - (HPow.hPow (β := ℕ) ‖z‖ 2 - HPow.hPow (β := ℕ) z.re 2) = HPow.hPow (β := ℕ) z.re 2
rw₁ rw₂ : HPow.hPow (β := ℕ) z.re 2 = HPow.hPow (β := ℕ) z.re 2
⊢ HPow.hPow (β := ℕ) ‖z‖ 2 - HPow.hPow (β := ℕ) z.im 2 = HPow.hPow (β := ℕ) z.re 2

Tactic:
rw [← sq_norm_sub_sq_re, sub_sub_cancel]

Premises used: Complex.sq_norm_sub_sq_re, sub_sub_cancel
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
x y : ℝ
rw : ‖(↑x : ℂ) + (↑y : ℂ) * I‖ = √((normSq : (a : ℂ) → ℝ) ((↑x : ℂ) + (↑y : ℂ) * I))
⊢ ‖(↑x : ℂ) + (↑y : ℂ) * I‖ = √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2)

Tactic:
rw [← normSq_add_mul_I]

Premises used: Complex.normSq_add_mul_I
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
x y : ℝ
⊢ ‖(↑x : ℂ) + (↑y : ℂ) * I‖ = √((normSq : (a : ℂ) → ℝ) ((↑x : ℂ) + (↑y : ℂ) * I))

Tactic:
rfl
-- Module: Mathlib.Analysis.Complex.Norm
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)
rw₃ rw₄ : √(z.re * z.re + z.im * z.im) = √(z.re * z.re + z.im * z.im)
⊢ ‖z‖ = √(HPow.hPow (β := ℕ) z.re 2 + HPow.hPow (β := ℕ) z.im 2)

Tactic:
rw [norm_def, normSq_apply, sq, sq]

Premises used: sq, Complex.norm_def, Complex.normSq_apply
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
⊢ Eq (α := Set ℝ) (range fun (x : ℂ) ↦ ‖x‖) (Ici 0)

Tactic:
Subset.antisymm (range_subset_iff.2 norm_nonneg) fun x hx ↦ ⟨x, Complex.norm_of_nonneg hx⟩

Premises used: Set.Subset.antisymm, Iff.mpr, Complex.ofReal, Complex.norm_of_nonneg, Exists.intro, Set.range_subset_iff, norm_nonneg
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
rw : √x * √x = x
rw₁ rw₂ : x = x
⊢ (normSq : (a : ℂ) → ℝ) (↑√x : ℂ) = x

Tactic:
rw [normSq_ofReal, Real.mul_self_sqrt hx]

Premises used: Real.mul_self_sqrt, Complex.normSq_ofReal
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z : ℂ
⊢ ‖z‖ ≤ |z.re| + |z.im|

Tactic:
simpa [re_add_im] using norm_add_le (z.re : ℂ) (z.im * I)

Premises used: HMul.hMul, Complex.im, norm_add_le, Complex.ofReal, Complex.re, Complex.re_add_im, Complex.I
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z : ℂ
rw : HPow.hPow (β := ℕ) z.im 2 ≤ HPow.hPow (β := ℕ) z.re 2 + HPow.hPow (β := ℕ) z.im 2
⊢ HPow.hPow (β := ℕ) z.im 2 ≤ (normSq : (a : ℂ) → ℝ) z

Tactic:
rw [normSq_apply, ← sq, ← sq]

Premises used: sq, Complex.normSq_apply
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z : ℂ
⊢ HPow.hPow (β := ℕ) z.im 2 ≤ HPow.hPow (β := ℕ) z.re 2 + HPow.hPow (β := ℕ) z.im 2

Tactic:
le_add_of_nonneg_left (sq_nonneg _)

Premises used: sq_nonneg, le_add_of_nonneg_left
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z : ℂ
⊢ HPow.hPow (β := ℕ) z.im 2 ≤ HPow.hPow (β := ℕ) z.re 2 + HPow.hPow (β := ℕ) z.im 2

Tactic:
exact le_add_of_nonneg_left (sq_nonneg _)

Premises used: le_add_of_nonneg_left
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z : ℂ
⊢ z.im ≤ ‖z‖

Tactic:
(abs_le.1 (abs_im_le_norm _)).2

Premises used: abs_le, Complex.abs_im_le_norm, And.right, Iff.mp
-- Module: Mathlib.Analysis.Complex.Norm
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
rw₆ rw₇ : z.im ≠ 0 ↔ z.im ≠ 0
⊢ |z.re| < ‖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]

Premises used: lt_add_iff_pos_right, sq, mul_self_pos, Complex.norm_def, Real.lt_sqrt, sq_abs, Complex.normSq_apply, abs_nonneg
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z : ℂ
⊢ |z.im| < ‖z‖ ↔ z.re ≠ 0

Tactic:
simpa using @abs_re_lt_norm (z * I)

Premises used: Complex.abs_re_lt_norm
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z : ℂ
⊢ |z.re| = ‖z‖ ↔ z.im = 0

Tactic:
not_iff_not.1 <| (abs_re_le_norm z).lt_iff_ne.symm.trans abs_re_lt_norm

Premises used: not_iff_not, Complex.abs_re_le_norm, LE.le.lt_iff_ne, Iff.mp, Iff.trans, Complex.abs_re_lt_norm, Iff.symm
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z : ℂ
⊢ |z.im| = ‖z‖ ↔ z.re = 0

Tactic:
not_iff_not.1 <| (abs_im_le_norm z).lt_iff_ne.symm.trans abs_im_lt_norm

Premises used: not_iff_not, Complex.abs_im_le_norm, Complex.abs_im_lt_norm, LE.le.lt_iff_ne, Iff.mp, Iff.trans, Iff.symm
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z : ℂ
obtain : ∀ (x y : ℝ), ‖{ re := x, im := y : ℂ }‖ ≤ √2 * max |{ re := x, im := y : ℂ }.re| |{ re := x, im := y : ℂ }.im|
⊢ ‖z‖ ≤ √2 * max |z.re| |z.im|

Tactic:
obtain ⟨x, y⟩ := z
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
x y : ℝ
simp : √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) ≤ √2 * max |x| |y|
⊢ ‖{ re := x, im := y : ℂ }‖ ≤ √2 * max |{ re := x, im := y : ℂ }.re| |{ re := x, im := y : ℂ }.im|

Tactic:
simp only [norm_def, normSq_mk, norm_def, ← sq]

Premises used: Complex.normSq_mk, sq, Complex.norm_def
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
x y : ℝ
set :
  let m := max |x| |y|;
  √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) ≤ √2 * m
⊢ √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) ≤ √2 * max |x| |y|

Tactic:
set m := max |x| |y|

Premises used: abs, Max.max
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
x y : ℝ
m : ℝ := max |x| |y|
⊢ 0 ≤ m

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
x y : ℝ
m : ℝ := max |x| |y|
⊢ 0 ≤ m

Tactic:
have hm₀ : 0 ≤ m := by positivity
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
x y : ℝ
m : ℝ := max |x| |y|
hm₀ : 0 ≤ m
a : HPow.hPow (β := ℕ) x 2 ≤ HPow.hPow (β := ℕ) m 2
a₁ : HPow.hPow (β := ℕ) y 2 ≤ HPow.hPow (β := ℕ) m 2
⊢ √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) ≤ √(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) m 2)

Tactic:
gcongr √(?_ + ?_)

Premises used: HAdd.hAdd
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
x y : ℝ
m : ℝ := max |x| |y|
hm₀ : 0 ≤ m
a : |x| ≤ m
⊢ HPow.hPow (β := ℕ) x 2 ≤ HPow.hPow (β := ℕ) m 2

Tactic:
rw [sq_le_sq, abs_of_nonneg hm₀]

Premises used: sq_le_sq, abs_of_nonneg
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
x y : ℝ
m : ℝ := max |x| |y|
hm₀ : 0 ≤ m
a : |y| ≤ m
⊢ HPow.hPow (β := ℕ) y 2 ≤ HPow.hPow (β := ℕ) m 2

Tactic:
rw [sq_le_sq, abs_of_nonneg hm₀]

Premises used: sq_le_sq, abs_of_nonneg
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
x y : ℝ
m : ℝ := max |x| |y|
hm₀ : 0 ≤ m
⊢ |x| ≤ m

Tactic:
le_max_left _ _

Premises used: le_max_left
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
x y : ℝ
m : ℝ := max |x| |y|
hm₀ : 0 ≤ m
⊢ |y| ≤ m

Tactic:
le_max_right _ _

Premises used: le_max_right
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
x y : ℝ
m : ℝ := max |x| |y|
hm₀ : 0 ≤ m
⊢ |x| ≤ m

Tactic:
exacts [le_max_left _ _, le_max_right _ _]

Premises used: le_max_right, le_max_left
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
x y : ℝ
m : ℝ := max |x| |y|
hm₀ rw : 0 ≤ m
hx : LE.le (α := ℝ) 0 2
⊢ √(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) m 2) = √2 * m

Tactic:
rw [← two_mul, Real.sqrt_mul, Real.sqrt_sq]

Premises used: two_mul, Real.sqrt_mul, Real.sqrt_sq
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
x y : ℝ
m : ℝ := max |x| |y|
hm₀ : 0 ≤ m
⊢ 0 ≤ m

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
x y : ℝ
m : ℝ := max |x| |y|
hm₀ : 0 ≤ m
⊢ LE.le (α := ℝ) 0 2

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.Norm
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)
y₂ : √(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) m 2) = √2 * m
⊢ √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 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

Premises used: HPow.hPow, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z : ℂ
hz : z = 0
⊢ |z.re / ‖z‖| ≤ 1

Tactic:
simp [hz, zero_le_one]

Premises used: zero_le_one
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z : ℂ
hz : ¬z = 0
simp_rw : |z.re| / |‖z‖| ≤ 1
simp_rw₁ : |z.re| / ‖z‖ ≤ 1
simp_rw₂ : |z.re| ≤ 1 * ‖z‖
simp_rw₃ : |z.re| ≤ ‖z‖
⊢ |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]

Premises used: Iff.mpr, div_le_iff₀, norm_pos_iff, abs_div, Complex.abs_re_le_norm, abs_norm, one_mul
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z : ℂ
hz : z = 0
⊢ |z.im / ‖z‖| ≤ 1

Tactic:
simp [hz, zero_le_one]

Premises used: zero_le_one
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z : ℂ
hz : ¬z = 0
simp_rw : |z.im| / |‖z‖| ≤ 1
simp_rw₁ : |z.im| / ‖z‖ ≤ 1
simp_rw₂ : |z.im| ≤ 1 * ‖z‖
simp_rw₃ : |z.im| ≤ ‖z‖
⊢ |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]

Premises used: Iff.mpr, div_le_iff₀, norm_pos_iff, abs_div, Complex.abs_im_le_norm, abs_norm, one_mul
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z w : ℂ
⊢ dist z w = ‖z - w‖

Tactic:
dist_eq_norm _ _

Premises used: dist_eq_norm, NNReal.toReal
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z w : ℂ
rw : ‖z - w‖ = √((z.re - w.re) * (z.re - w.re) + (z.im - w.im) * (z.im - w.im))
⊢ dist z w = √(HPow.hPow (β := ℕ) (z.re - w.re) 2 + HPow.hPow (β := ℕ) (z.im - w.im) 2)

Tactic:
rw [sq, sq, dist_eq]

Premises used: sq, Complex.dist_eq
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z w : ℂ
⊢ ‖z - w‖ = √((z.re - w.re) * (z.re - w.re) + (z.im - w.im) * (z.im - w.im))

Tactic:
rfl
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
x₁ y₁ x₂ y₂ : ℝ
⊢ dist { re := x₁, im := y₁ : ℂ } { re := x₂, im := y₂ : ℂ } =
    √(HPow.hPow (β := ℕ) (x₁ - x₂) 2 + HPow.hPow (β := ℕ) (y₁ - y₂) 2)

Tactic:
dist_eq_re_im _ _

Premises used: Complex.dist_eq_re_im
-- Module: Mathlib.Analysis.Complex.Norm
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
rw₆ rw₇ : |z.im - w.im| = |z.im - w.im|
⊢ dist z w = 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]

Premises used: sub_self, Real.sqrt_sq_eq_abs, zero_add, two_ne_zero, Real.dist_eq, zero_pow, Complex.dist_eq_re_im
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z w : ℂ
h : z.re = w.re
⊢ nndist z w = nndist z.im w.im

Tactic:
NNReal.eq <| dist_of_re_eq h

Premises used: NNReal.eq, Complex.dist_of_re_eq
-- Module: Mathlib.Analysis.Complex.Norm
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)
rw₂ rw₃ : (↑(nndist z.im w.im) : ENNReal) = (↑(nndist z.im w.im) : ENNReal)
⊢ edist z w = edist z.im w.im

Tactic:
rw [edist_nndist, edist_nndist, nndist_of_re_eq h]

Premises used: Complex.nndist_of_re_eq, edist_nndist
-- Module: Mathlib.Analysis.Complex.Norm
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
rw₆ rw₇ : |z.re - w.re| = |z.re - w.re|
⊢ dist z w = 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]

Premises used: sub_self, Real.sqrt_sq_eq_abs, two_ne_zero, Real.dist_eq, add_zero, zero_pow, Complex.dist_eq_re_im
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z w : ℂ
h : z.im = w.im
⊢ nndist z w = nndist z.re w.re

Tactic:
NNReal.eq <| dist_of_im_eq h

Premises used: NNReal.eq, Complex.dist_of_im_eq
-- Module: Mathlib.Analysis.Complex.Norm
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)
rw₂ rw₃ : (↑(nndist z.re w.re) : ENNReal) = (↑(nndist z.re w.re) : ENNReal)
⊢ edist z w = edist z.re w.re

Tactic:
rw [edist_nndist, edist_nndist, nndist_of_im_eq h]

Premises used: Complex.nndist_of_im_eq, edist_nndist
-- Module: Mathlib.Analysis.Complex.Norm
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|
rw₇ rw₈ : 2 * |z.im| = 2 * |z.im|
⊢ dist ((starRingEnd ℂ : (a : ℂ) → ℂ) z) z = 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' ℝ)]

Premises used: Real, abs_mul, two_mul, Complex.conj_im, dist_comm, Real.dist_eq, zero_lt_two', Complex.conj_re, abs_of_pos, Complex.dist_of_re_eq, sub_neg_eq_add
-- Module: Mathlib.Analysis.Complex.Norm
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|
rw₄ rw₅ : 2 * |z.im| = 2 * |z.im|
⊢ (↑(nndist ((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]

Premises used: Real.coe_nnabs, dist_nndist, NNReal.coe_two, NNReal.coe_mul, Complex.dist_conj_self
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z : ℂ
rw : dist ((starRingEnd ℂ : (a : ℂ) → ℂ) z) z = 2 * |z.im|
rw₁ rw₂ : 2 * |z.im| = 2 * |z.im|
⊢ dist z ((starRingEnd ℂ : (a : ℂ) → ℂ) z) = 2 * |z.im|

Tactic:
rw [dist_comm, dist_conj_self]

Premises used: dist_comm, Complex.dist_conj_self
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z : ℂ
rw :
  nndist ((starRingEnd ℂ : (a : ℂ) → ℂ) z) z =
    HMul.hMul (α := NNReal) (β := NNReal) (2 : NNReal) ((Real.nnabs : (a : ℝ) → NNReal) z.im : NNReal)
rw₁ 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)
⊢ nndist z ((starRingEnd ℂ : (a : ℂ) → ℂ) z) =
    HMul.hMul (α := NNReal) (β := NNReal) (2 : NNReal) ((Real.nnabs : (a : ℝ) → NNReal) z.im : NNReal)

Tactic:
rw [nndist_comm, nndist_conj_self]

Premises used: nndist_comm, Complex.nndist_conj_self
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
f : CauSeq (α := ℝ) ℂ fun (x : ℂ) ↦ ‖x‖
x : ℝ
ε0 : x > 0
i : ℕ
H : ∀ j ≥ i, ‖(↑f : ℕ → ℂ) j - (↑f : ℕ → ℂ) i‖ < x
j : ℕ
ij : j ≥ i
⊢ |HSub.hSub (α := ℝ) ((fun (n : ℕ) ↦ ((↑f : ℕ → ℂ) n).re) j) ((fun (n : ℕ) ↦ ((↑f : ℕ → ℂ) n).re) i)| ≤
    ‖(↑f : ℕ → ℂ) j - (↑f : ℕ → ℂ) i‖

Tactic:
simpa using abs_re_le_norm (f j - f i)

Premises used: HSub.hSub, Complex.abs_re_le_norm, Subtype.val
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
f : CauSeq (α := ℝ) ℂ fun (x : ℂ) ↦ ‖x‖
ε : ℝ
ε0 : ε > 0
i : ℕ
H : ∀ j ≥ i, ‖(↑f : ℕ → ℂ) j - (↑f : ℕ → ℂ) i‖ < ε
j : ℕ
ij : j ≥ i
⊢ |HSub.hSub (α := ℝ) ((fun (n : ℕ) ↦ ((↑f : ℕ → ℂ) n).im) j) ((fun (n : ℕ) ↦ ((↑f : ℕ → ℂ) n).im) i)| < ε

Tactic:
simpa only [← ofReal_sub, norm_real, sub_re, sub_im] using (abs_im_le_norm _).trans_lt <| H _ ij

Premises used: Complex.sub_im, Complex.sub_re, Complex.abs_im_le_norm, Complex.norm_real, Complex.ofReal_sub, LE.le.trans_lt
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
f : ℕ → ℂ
hf : IsCauSeq (α := ℝ) (fun (x : ℂ) ↦ ‖x‖) f
⊢ IsCauSeq (α := ℝ) abs ((fun (x : ℂ) ↦ ‖x‖) ∘ f)

Tactic:
fun ε ε0 ↦
  let ⟨i, hi⟩ := hf ε ε0
  ⟨i, fun j hj ↦ lt_of_le_of_lt (abs_norm_sub_norm_le _ _) (hi j hj)⟩

Premises used: lt_of_le_of_lt, Exists, abs_norm_sub_norm_le, _private.0.Complex.isCauSeq_norm.match_1, Exists.intro, IsCauSeq
-- Module: Mathlib.Analysis.Complex.Norm
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
⊢ |(↑(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

Tactic:
obtain ⟨H₁, H₂⟩ := H _ ij
-- Module: Mathlib.Analysis.Complex.Norm
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
⊢ |(↑(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

Tactic:
obtain ⟨H₁, H₂⟩ := H _ ij
-- Module: Mathlib.Analysis.Complex.Norm
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
apply :
  |((↑(f - CauSeq.const (fun (x : ℂ) ↦ ‖x‖) (limAux f)) : ℕ → ℂ) j).re| +
      |((↑(f - CauSeq.const (fun (x : ℂ) ↦ ‖x‖) (limAux f)) : ℕ → ℂ) j).im| <
    ε
⊢ (fun (x : ℂ) ↦ ‖x‖) ((↑(f - CauSeq.const (fun (x : ℂ) ↦ ‖x‖) (limAux f)) : ℕ → ℂ) j) < ε

Tactic:
apply lt_of_le_of_lt (norm_le_abs_re_add_abs_im _)

Premises used: Complex.norm_le_abs_re_add_abs_im, lt_of_le_of_lt