[GOAL]
K : Type u_1
E : Type u_2
inst✝⁴ : IsROrC K
inst✝³ : AddCommGroup E
inst✝² : Module K E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ K E
r : ℝ
x : E
⊢ r • x = ↑r • x
[PROOFSTEP]
rw [IsROrC.ofReal_alg, smul_one_smul]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
⊢ ↑re 1 = 1
[PROOFSTEP]
rw [← ofReal_one, ofReal_re]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
⊢ ↑im 1 = 0
[PROOFSTEP]
rw [← ofReal_one, ofReal_im]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
⊢ ↑re (bit1 z) = bit1 (↑re z)
[PROOFSTEP]
simp only [bit1, map_add, bit0_re, one_re]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
⊢ ↑im (bit1 z) = bit0 (↑im z)
[PROOFSTEP]
simp only [bit1, map_add, bit0_im, one_im, add_zero]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
r : ℝ
z : K
⊢ ↑re (↑r * z) = r * ↑re z
[PROOFSTEP]
simp only [mul_re, ofReal_im, zero_mul, ofReal_re, sub_zero]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
r : ℝ
z : K
⊢ ↑im (↑r * z) = r * ↑im z
[PROOFSTEP]
simp only [add_zero, ofReal_im, zero_mul, ofReal_re, mul_im]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
r : ℝ
z : K
⊢ ↑re (r • z) = r * ↑re z
[PROOFSTEP]
rw [real_smul_eq_coe_mul, ofReal_mul_re]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
r : ℝ
z : K
⊢ ↑im (r • z) = r * ↑im z
[PROOFSTEP]
rw [real_smul_eq_coe_mul, ofReal_mul_im]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
⊢ ↑im I * ↑im z = ↑im z
[PROOFSTEP]
rw [mul_comm, I_im]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
⊢ ↑re (I * z) = -↑im z
[PROOFSTEP]
simp only [I_re, zero_sub, I_im', zero_mul, mul_re]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
r : ℝ
⊢ ↑(starRingEnd K) ↑r = ↑r
[PROOFSTEP]
rw [ext_iff]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
r : ℝ
⊢ ↑re (↑(starRingEnd K) ↑r) = ↑re ↑r ∧ ↑im (↑(starRingEnd K) ↑r) = ↑im ↑r
[PROOFSTEP]
simp only [ofReal_im, conj_im, eq_self_iff_true, conj_re, and_self_iff, neg_zero]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
⊢ ↑(starRingEnd K) (-I) = I
[PROOFSTEP]
rw [map_neg, conj_I, neg_neg]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
⊢ ↑(starRingEnd K) (↑(↑re z) + ↑(↑im z) * I) = ↑(↑re z) - ↑(↑im z) * I
[PROOFSTEP]
rw [map_add, map_mul, conj_I, conj_ofReal, conj_ofReal, mul_neg, sub_eq_add_neg]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
⊢ z - ↑(starRingEnd K) z = ↑(↑re z) + ↑(↑im z) * I - (↑(↑re z) - ↑(↑im z) * I)
[PROOFSTEP]
rw [re_add_im, ← conj_eq_re_sub_im]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
⊢ ↑(↑re z) + ↑(↑im z) * I - (↑(↑re z) - ↑(↑im z) * I) = 2 * ↑(↑im z) * I
[PROOFSTEP]
rw [add_sub_sub_cancel, ← two_mul, mul_assoc]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
r : ℝ
z : K
⊢ ↑(starRingEnd K) (r • z) = r • ↑(starRingEnd K) z
[PROOFSTEP]
rw [conj_eq_re_sub_im, conj_eq_re_sub_im, smul_re, smul_im, ofReal_mul, ofReal_mul, real_smul_eq_coe_mul r (_ - _),
  mul_sub, mul_assoc]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
⊢ z + ↑(starRingEnd K) z = ↑(↑re z) + ↑(↑im z) * I + (↑(↑re z) - ↑(↑im z) * I)
[PROOFSTEP]
rw [re_add_im, conj_eq_re_sub_im]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
⊢ ↑(↑re z) + ↑(↑im z) * I + (↑(↑re z) - ↑(↑im z) * I) = 2 * ↑(↑re z)
[PROOFSTEP]
rw [add_add_sub_cancel, two_mul]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
⊢ ↑(↑re z) = (z + ↑(starRingEnd K) z) / 2
[PROOFSTEP]
rw [add_conj, mul_div_cancel_left (re z : K) two_ne_zero]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
⊢ ↑(↑im z) = I * (↑(starRingEnd K) z - z) / 2
[PROOFSTEP]
rw [← neg_inj, ← ofReal_neg, ← I_mul_re, re_eq_add_conj, map_mul, conj_I, ← neg_div, ← mul_neg, neg_sub, mul_sub,
  neg_mul, sub_eq_add_neg]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
⊢ TFAE [↑(starRingEnd K) z = z, ∃ r, ↑r = z, ↑(↑re z) = z, ↑im z = 0]
[PROOFSTEP]
tfae_have 1 → 4
[GOAL]
case tfae_1_to_4
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
⊢ ↑(starRingEnd K) z = z → ↑im z = 0
[PROOFSTEP]
intro h
[GOAL]
case tfae_1_to_4
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
h : ↑(starRingEnd K) z = z
⊢ ↑im z = 0
[PROOFSTEP]
rw [← @ofReal_inj K, im_eq_conj_sub, h, sub_self, mul_zero, zero_div, ofReal_zero]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
tfae_1_to_4 : ↑(starRingEnd K) z = z → ↑im z = 0
⊢ TFAE [↑(starRingEnd K) z = z, ∃ r, ↑r = z, ↑(↑re z) = z, ↑im z = 0]
[PROOFSTEP]
tfae_have 4 → 3
[GOAL]
case tfae_4_to_3
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
tfae_1_to_4 : ↑(starRingEnd K) z = z → ↑im z = 0
⊢ ↑im z = 0 → ↑(↑re z) = z
[PROOFSTEP]
intro h
[GOAL]
case tfae_4_to_3
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
tfae_1_to_4 : ↑(starRingEnd K) z = z → ↑im z = 0
h : ↑im z = 0
⊢ ↑(↑re z) = z
[PROOFSTEP]
conv_rhs => rw [← re_add_im z, h, ofReal_zero, zero_mul, add_zero]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
tfae_1_to_4 : ↑(starRingEnd K) z = z → ↑im z = 0
h : ↑im z = 0
| z
[PROOFSTEP]
rw [← re_add_im z, h, ofReal_zero, zero_mul, add_zero]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
tfae_1_to_4 : ↑(starRingEnd K) z = z → ↑im z = 0
h : ↑im z = 0
| z
[PROOFSTEP]
rw [← re_add_im z, h, ofReal_zero, zero_mul, add_zero]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
tfae_1_to_4 : ↑(starRingEnd K) z = z → ↑im z = 0
h : ↑im z = 0
| z
[PROOFSTEP]
rw [← re_add_im z, h, ofReal_zero, zero_mul, add_zero]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
tfae_1_to_4 : ↑(starRingEnd K) z = z → ↑im z = 0
tfae_4_to_3 : ↑im z = 0 → ↑(↑re z) = z
⊢ TFAE [↑(starRingEnd K) z = z, ∃ r, ↑r = z, ↑(↑re z) = z, ↑im z = 0]
[PROOFSTEP]
tfae_have 3 → 2
[GOAL]
case tfae_3_to_2
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
tfae_1_to_4 : ↑(starRingEnd K) z = z → ↑im z = 0
tfae_4_to_3 : ↑im z = 0 → ↑(↑re z) = z
⊢ ↑(↑re z) = z → ∃ r, ↑r = z
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
tfae_1_to_4 : ↑(starRingEnd K) z = z → ↑im z = 0
tfae_4_to_3 : ↑im z = 0 → ↑(↑re z) = z
tfae_3_to_2 : ↑(↑re z) = z → ∃ r, ↑r = z
⊢ TFAE [↑(starRingEnd K) z = z, ∃ r, ↑r = z, ↑(↑re z) = z, ↑im z = 0]
[PROOFSTEP]
exact fun h => ⟨_, h⟩
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
tfae_1_to_4 : ↑(starRingEnd K) z = z → ↑im z = 0
tfae_4_to_3 : ↑im z = 0 → ↑(↑re z) = z
tfae_3_to_2 : ↑(↑re z) = z → ∃ r, ↑r = z
⊢ TFAE [↑(starRingEnd K) z = z, ∃ r, ↑r = z, ↑(↑re z) = z, ↑im z = 0]
[PROOFSTEP]
tfae_have 2 → 1
[GOAL]
case tfae_2_to_1
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
tfae_1_to_4 : ↑(starRingEnd K) z = z → ↑im z = 0
tfae_4_to_3 : ↑im z = 0 → ↑(↑re z) = z
tfae_3_to_2 : ↑(↑re z) = z → ∃ r, ↑r = z
⊢ (∃ r, ↑r = z) → ↑(starRingEnd K) z = z
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
tfae_1_to_4 : ↑(starRingEnd K) z = z → ↑im z = 0
tfae_4_to_3 : ↑im z = 0 → ↑(↑re z) = z
tfae_3_to_2 : ↑(↑re z) = z → ∃ r, ↑r = z
tfae_2_to_1 : (∃ r, ↑r = z) → ↑(starRingEnd K) z = z
⊢ TFAE [↑(starRingEnd K) z = z, ∃ r, ↑r = z, ↑(↑re z) = z, ↑im z = 0]
[PROOFSTEP]
exact fun ⟨r, hr⟩ => hr ▸ conj_ofReal _
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
tfae_1_to_4 : ↑(starRingEnd K) z = z → ↑im z = 0
tfae_4_to_3 : ↑im z = 0 → ↑(↑re z) = z
tfae_3_to_2 : ↑(↑re z) = z → ∃ r, ↑r = z
tfae_2_to_1 : (∃ r, ↑r = z) → ↑(starRingEnd K) z = z
⊢ TFAE [↑(starRingEnd K) z = z, ∃ r, ↑r = z, ↑(↑re z) = z, ↑im z = 0]
[PROOFSTEP]
tfae_finish
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
⊢ (∃ r, ↑r = z) ↔ ∃ r, z = ↑r
[PROOFSTEP]
simp only [eq_comm]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
⊢ (fun z => ↑re z * ↑re z + ↑im z * ↑im z) 0 = 0
[PROOFSTEP]
simp only [add_zero, mul_zero, map_zero]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
⊢ ZeroHom.toFun
      { toFun := fun z => ↑re z * ↑re z + ↑im z * ↑im z, map_zero' := (_ : ↑re 0 * ↑re 0 + ↑im 0 * ↑im 0 = 0) } 1 =
    1
[PROOFSTEP]
simp only [one_im, add_zero, mul_one, one_re, mul_zero]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z w : K
⊢ ZeroHom.toFun
      { toFun := fun z => ↑re z * ↑re z + ↑im z * ↑im z, map_zero' := (_ : ↑re 0 * ↑re 0 + ↑im 0 * ↑im 0 = 0) }
      (z * w) =
    ZeroHom.toFun
        { toFun := fun z => ↑re z * ↑re z + ↑im z * ↑im z, map_zero' := (_ : ↑re 0 * ↑re 0 + ↑im 0 * ↑im 0 = 0) } z *
      ZeroHom.toFun
        { toFun := fun z => ↑re z * ↑re z + ↑im z * ↑im z, map_zero' := (_ : ↑re 0 * ↑re 0 + ↑im 0 * ↑im 0 = 0) } w
[PROOFSTEP]
simp only [mul_im, mul_re]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z w : K
⊢ (↑re z * ↑re w - ↑im z * ↑im w) * (↑re z * ↑re w - ↑im z * ↑im w) +
      (↑re z * ↑im w + ↑im z * ↑re w) * (↑re z * ↑im w + ↑im z * ↑re w) =
    (↑re z * ↑re z + ↑im z * ↑im z) * (↑re w * ↑re w + ↑im w * ↑im w)
[PROOFSTEP]
ring
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
⊢ 0 < ↑normSq z ↔ z ≠ 0
[PROOFSTEP]
rw [lt_iff_le_and_ne, Ne, eq_comm]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
⊢ 0 ≤ ↑normSq z ∧ ¬↑normSq z = 0 ↔ z ≠ 0
[PROOFSTEP]
simp [normSq_nonneg]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
⊢ ↑normSq (-z) = ↑normSq z
[PROOFSTEP]
simp only [normSq_eq_def', norm_neg]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
⊢ ↑normSq (↑(starRingEnd K) z) = ↑normSq z
[PROOFSTEP]
simp only [normSq_apply, neg_mul, mul_neg, neg_neg, isROrC_simps]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z w : K
⊢ ↑normSq (z + w) = ↑normSq z + ↑normSq w + 2 * ↑re (z * ↑(starRingEnd K) w)
[PROOFSTEP]
simp only [normSq_apply, map_add, isROrC_simps]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z w : K
⊢ (↑re z + ↑re w) * (↑re z + ↑re w) + (↑im z + ↑im w) * (↑im z + ↑im w) =
    ↑re z * ↑re z + ↑im z * ↑im z + (↑re w * ↑re w + ↑im w * ↑im w) + 2 * (↑re z * ↑re w - ↑im z * -↑im w)
[PROOFSTEP]
ring
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
⊢ z * ↑(starRingEnd K) z = ↑(↑normSq z)
[PROOFSTEP]
apply ext
[GOAL]
case hre
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
⊢ ↑re (z * ↑(starRingEnd K) z) = ↑re ↑(↑normSq z)
[PROOFSTEP]
simp only [normSq_apply, isROrC_simps, map_add, mul_zero]
[GOAL]
case him
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
⊢ ↑im (z * ↑(starRingEnd K) z) = ↑im ↑(↑normSq z)
[PROOFSTEP]
simp only [normSq_apply, isROrC_simps, map_add, mul_zero]
[GOAL]
case hre
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
⊢ ↑re z * ↑re z - ↑im z * -↑im z = ↑re z * ↑re z - 0 + (↑im z * ↑im z - 0)
[PROOFSTEP]
ring
[GOAL]
case him
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
⊢ ↑re z * -↑im z + ↑im z * ↑re z = 0 + 0 * ↑re z + (0 + 0 * ↑im z)
[PROOFSTEP]
ring
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
x : K
⊢ ↑(starRingEnd K) x * x = ↑(↑normSq x)
[PROOFSTEP]
rw [mul_comm, mul_conj]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z w : K
⊢ ↑normSq (z - w) = ↑normSq z + ↑normSq w - 2 * ↑re (z * ↑(starRingEnd K) w)
[PROOFSTEP]
simp only [normSq_add, sub_eq_add_neg, map_neg, mul_neg, normSq_neg, map_neg]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
⊢ Real.sqrt (↑normSq z) = ‖z‖
[PROOFSTEP]
rw [normSq_eq_def', Real.sqrt_sq (norm_nonneg _)]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
⊢ z⁻¹ = ↑(starRingEnd K) z * ↑(‖z‖ ^ 2)⁻¹
[PROOFSTEP]
rcases eq_or_ne z 0 with (rfl | h₀)
[GOAL]
case inl
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
⊢ 0⁻¹ = ↑(starRingEnd K) 0 * ↑(‖0‖ ^ 2)⁻¹
[PROOFSTEP]
simp
[GOAL]
case inr
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
h₀ : z ≠ 0
⊢ z⁻¹ = ↑(starRingEnd K) z * ↑(‖z‖ ^ 2)⁻¹
[PROOFSTEP]
apply inv_eq_of_mul_eq_one_right
[GOAL]
case inr.a
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
h₀ : z ≠ 0
⊢ z * (↑(starRingEnd K) z * ↑(‖z‖ ^ 2)⁻¹) = 1
[PROOFSTEP]
rw [← mul_assoc, mul_conj, ofReal_inv, ← normSq_eq_def', mul_inv_cancel]
[GOAL]
case inr.a
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
h₀ : z ≠ 0
⊢ ↑(↑normSq z) ≠ 0
[PROOFSTEP]
rwa [ofReal_ne_zero, Ne.def, normSq_eq_zero]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
⊢ ↑re z⁻¹ = ↑re z / ↑normSq z
[PROOFSTEP]
rw [inv_def, normSq_eq_def', mul_comm, ofReal_mul_re, conj_re, div_eq_inv_mul]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
⊢ ↑im z⁻¹ = -↑im z / ↑normSq z
[PROOFSTEP]
rw [inv_def, normSq_eq_def', mul_comm, ofReal_mul_im, conj_im, div_eq_inv_mul]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z w : K
⊢ ↑re (z / w) = ↑re z * ↑re w / ↑normSq w + ↑im z * ↑im w / ↑normSq w
[PROOFSTEP]
simp only [div_eq_mul_inv, mul_assoc, sub_eq_add_neg, neg_mul, mul_neg, neg_neg, map_neg, isROrC_simps]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z w : K
⊢ ↑im (z / w) = ↑im z * ↑re w / ↑normSq w - ↑re z * ↑im w / ↑normSq w
[PROOFSTEP]
simp only [div_eq_mul_inv, mul_assoc, sub_eq_add_neg, add_comm, neg_mul, mul_neg, map_neg, isROrC_simps]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
r : ℝ
⊢ ↑re (z / ↑r) = ↑re z / r
[PROOFSTEP]
rw [div_eq_inv_mul, div_eq_inv_mul, ← ofReal_inv, ofReal_mul_re]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
⊢ I⁻¹ = -I
[PROOFSTEP]
by_cases h : (I : K) = 0
[GOAL]
case pos
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
h : I = 0
⊢ I⁻¹ = -I
[PROOFSTEP]
simp [h]
[GOAL]
case neg
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
h : ¬I = 0
⊢ I⁻¹ = -I
[PROOFSTEP]
field_simp [I_mul_I_of_nonzero h]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
⊢ z / I = -(z * I)
[PROOFSTEP]
rw [div_eq_mul_inv, inv_I, mul_neg]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
⊢ ‖↑(starRingEnd K) z‖ = ‖z‖
[PROOFSTEP]
simp only [← sqrt_normSq_eq_norm, normSq_conj]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
n : ℕ
⊢ ↑re ↑n = ↑n
[PROOFSTEP]
rw [← ofReal_natCast, ofReal_re]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
n : ℕ
⊢ ↑im ↑n = 0
[PROOFSTEP]
rw [← ofReal_natCast, ofReal_im]
[GOAL]
K : Type u_1
E : Type u_2
inst✝¹ : IsROrC K
n : ℕ
inst✝ : Nat.AtLeastTwo n
z : K
⊢ ↑re (OfNat.ofNat n * z) = OfNat.ofNat n * ↑re z
[PROOFSTEP]
rw [← ofReal_ofNat, ofReal_mul_re]
[GOAL]
K : Type u_1
E : Type u_2
inst✝¹ : IsROrC K
n : ℕ
inst✝ : Nat.AtLeastTwo n
z : K
⊢ ↑im (OfNat.ofNat n * z) = OfNat.ofNat n * ↑im z
[PROOFSTEP]
rw [← ofReal_ofNat, ofReal_mul_im]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
n : ℤ
⊢ ↑re ↑n = ↑n
[PROOFSTEP]
rw [← ofReal_intCast, ofReal_re]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
n : ℤ
⊢ ↑im ↑n = 0
[PROOFSTEP]
rw [← ofReal_intCast, ofReal_im]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
q : ℚ
⊢ ↑re ↑q = ↑q
[PROOFSTEP]
rw [← ofReal_ratCast, ofReal_re]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
q : ℚ
⊢ ↑im ↑q = 0
[PROOFSTEP]
rw [← ofReal_ratCast, ofReal_im]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
n : ℕ
⊢ ‖↑n‖ = ↑n
[PROOFSTEP]
rw [← ofReal_natCast]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
n : ℕ
⊢ ‖↑↑n‖ = ↑n
[PROOFSTEP]
exact norm_of_nonneg (Nat.cast_nonneg n)
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
⊢ ‖z‖ * ‖z‖ = ↑normSq z
[PROOFSTEP]
rw [normSq_eq_def', sq]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
⊢ |↑re z| ≤ ‖z‖
[PROOFSTEP]
rw [mul_self_le_mul_self_iff (abs_nonneg _) (norm_nonneg _), abs_mul_abs_self, mul_self_norm]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
⊢ ↑re z * ↑re z ≤ ↑normSq z
[PROOFSTEP]
apply re_sq_le_normSq
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
⊢ |↑im z| ≤ ‖z‖
[PROOFSTEP]
rw [mul_self_le_mul_self_iff (abs_nonneg _) (norm_nonneg _), abs_mul_abs_self, mul_self_norm]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
⊢ ↑im z * ↑im z ≤ ↑normSq z
[PROOFSTEP]
apply im_sq_le_normSq
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
a : K
h : ‖a‖ ≤ ↑re a
⊢ ↑im a = 0
[PROOFSTEP]
simpa only [mul_self_norm a, normSq_apply, self_eq_add_right, mul_self_eq_zero] using
  congr_arg (fun z => z * z) ((re_le_norm a).antisymm h)
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
a : K
h : ‖a‖ ≤ ↑re a
⊢ ↑(↑re a) = a
[PROOFSTEP]
rw [← conj_eq_iff_re, conj_eq_iff_im, im_eq_zero_of_le h]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
⊢ |↑re z / ‖z‖| ≤ 1
[PROOFSTEP]
rw [abs_div, abs_norm]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
⊢ |↑re z| / ‖z‖ ≤ 1
[PROOFSTEP]
exact div_le_one_of_le (abs_re_le_norm _) (norm_nonneg _)
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
⊢ |↑im z / ‖z‖| ≤ 1
[PROOFSTEP]
rw [abs_div, abs_norm]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
⊢ |↑im z| / ‖z‖ ≤ 1
[PROOFSTEP]
exact div_le_one_of_le (abs_im_le_norm _) (norm_nonneg _)
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
hI : I ≠ 0
⊢ ‖I‖ = 1
[PROOFSTEP]
rw [← mul_self_inj_of_nonneg (norm_nonneg I) zero_le_one, one_mul, ← norm_mul, I_mul_I_of_nonzero hI, norm_neg,
  norm_one]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
x : K
⊢ ↑re (x * ↑(starRingEnd K) x) = ‖x * ↑(starRingEnd K) x‖
[PROOFSTEP]
rw [mul_conj, ofReal_re, norm_ofReal, abs_of_nonneg (normSq_nonneg _)]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
x : K
⊢ ‖x + ↑(starRingEnd K) x‖ ^ 2 = ↑re (x + ↑(starRingEnd K) x) ^ 2
[PROOFSTEP]
rw [add_conj, ← ofReal_ofNat, ← ofReal_mul, norm_ofReal, sq_abs, ofReal_re]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
x : K
⊢ ‖↑(starRingEnd K) x + x‖ ^ 2 = ↑re (↑(starRingEnd K) x + x) ^ 2
[PROOFSTEP]
rw [add_comm, norm_sq_re_add_conj]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
f : CauSeq K norm
ε : ℝ
ε0 : ε > 0
i : ℕ
H : ∀ (j : ℕ), j ≥ i → ‖↑f j - ↑f i‖ < ε
j : ℕ
ij : j ≥ i
⊢ |(fun n => ↑re (↑f n)) j - (fun n => ↑re (↑f n)) i| ≤ ‖↑f j - ↑f i‖
[PROOFSTEP]
simpa only [map_sub] using abs_re_le_norm (f j - f i)
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
f : CauSeq K norm
ε : ℝ
ε0 : ε > 0
i : ℕ
H : ∀ (j : ℕ), j ≥ i → ‖↑f j - ↑f i‖ < ε
j : ℕ
ij : j ≥ i
⊢ |(fun n => ↑im (↑f n)) j - (fun n => ↑im (↑f n)) i| ≤ ‖↑f j - ↑f i‖
[PROOFSTEP]
simpa only [map_sub] using abs_im_le_norm (f j - f i)
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
⊢ ↑(AddMonoidHom.id ℝ) 0 = 0
[PROOFSTEP]
simp only [AddMonoidHom.map_zero]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : ℝ
⊢ ↑(algebraMap ℝ ℝ) (↑(AddMonoidHom.id ℝ) z) + ↑(algebraMap ℝ ℝ) (↑0 z) * 0 = z
[PROOFSTEP]
simp only [add_zero, mul_zero, Algebra.id.map_eq_id, RingHom.id_apply, AddMonoidHom.id_apply]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z w : ℝ
⊢ ↑(AddMonoidHom.id ℝ) (z * w) = ↑(AddMonoidHom.id ℝ) z * ↑(AddMonoidHom.id ℝ) w - ↑0 z * ↑0 w
[PROOFSTEP]
simp only [sub_zero, mul_zero, AddMonoidHom.zero_apply, AddMonoidHom.id_apply]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z w : ℝ
⊢ ↑0 (z * w) = ↑(AddMonoidHom.id ℝ) z * ↑0 w + ↑0 z * ↑(AddMonoidHom.id ℝ) w
[PROOFSTEP]
simp only [add_zero, zero_mul, mul_zero, AddMonoidHom.zero_apply]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : ℝ
⊢ ↑(AddMonoidHom.id ℝ) (↑(starRingEnd ℝ) z) = ↑(AddMonoidHom.id ℝ) z
[PROOFSTEP]
simp only [starRingEnd_apply, star_id_of_comm]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : ℝ
⊢ ↑0 (↑(starRingEnd ℝ) z) = -↑0 z
[PROOFSTEP]
simp only [neg_zero, AddMonoidHom.zero_apply]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
⊢ ↑(starRingEnd ℝ) 0 = -0
[PROOFSTEP]
simp only [RingHom.map_zero, neg_zero]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : ℝ
⊢ ‖z‖ ^ 2 = ↑(AddMonoidHom.id ℝ) z * ↑(AddMonoidHom.id ℝ) z + ↑0 z * ↑0 z
[PROOFSTEP]
simp only [sq, Real.norm_eq_abs, ← abs_mul, abs_mul_self z, add_zero, mul_zero, AddMonoidHom.zero_apply,
  AddMonoidHom.id_apply]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : ℝ
⊢ ↑0 z * ↑0 0 = ↑0 z
[PROOFSTEP]
simp only [mul_zero, AddMonoidHom.zero_apply]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z w : K
⊢ z < w ↔ ↑re z < ↑re w ∧ ↑im z = ↑im w
[PROOFSTEP]
simp_rw [lt_iff_le_and_ne, @IsROrC.le_iff_re_im K]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z w : K
⊢ (↑re z ≤ ↑re w ∧ ↑im z = ↑im w) ∧ z ≠ w ↔ (↑re z ≤ ↑re w ∧ ↑re z ≠ ↑re w) ∧ ↑im z = ↑im w
[PROOFSTEP]
constructor
[GOAL]
case mp
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z w : K
⊢ (↑re z ≤ ↑re w ∧ ↑im z = ↑im w) ∧ z ≠ w → (↑re z ≤ ↑re w ∧ ↑re z ≠ ↑re w) ∧ ↑im z = ↑im w
[PROOFSTEP]
rintro ⟨⟨hr, hi⟩, heq⟩
[GOAL]
case mp.intro.intro
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z w : K
heq : z ≠ w
hr : ↑re z ≤ ↑re w
hi : ↑im z = ↑im w
⊢ (↑re z ≤ ↑re w ∧ ↑re z ≠ ↑re w) ∧ ↑im z = ↑im w
[PROOFSTEP]
exact ⟨⟨hr, mt (fun hreq => ext hreq hi) heq⟩, hi⟩
[GOAL]
case mpr
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z w : K
⊢ (↑re z ≤ ↑re w ∧ ↑re z ≠ ↑re w) ∧ ↑im z = ↑im w → (↑re z ≤ ↑re w ∧ ↑im z = ↑im w) ∧ z ≠ w
[PROOFSTEP]
rintro ⟨⟨hr, hrn⟩, hi⟩
[GOAL]
case mpr.intro.intro
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z w : K
hi : ↑im z = ↑im w
hr : ↑re z ≤ ↑re w
hrn : ↑re z ≠ ↑re w
⊢ (↑re z ≤ ↑re w ∧ ↑im z = ↑im w) ∧ z ≠ w
[PROOFSTEP]
exact ⟨⟨hr, hi⟩, ne_of_apply_ne _ hrn⟩
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
⊢ 0 ≤ z ↔ 0 ≤ ↑re z ∧ ↑im z = 0
[PROOFSTEP]
simpa only [map_zero, eq_comm] using le_iff_re_im (z := 0) (w := z)
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
⊢ 0 < z ↔ 0 < ↑re z ∧ ↑im z = 0
[PROOFSTEP]
simpa only [map_zero, eq_comm] using lt_iff_re_im (z := 0) (w := z)
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
⊢ z ≤ 0 ↔ ↑re z ≤ 0 ∧ ↑im z = 0
[PROOFSTEP]
simpa only [map_zero] using le_iff_re_im (z := z) (w := 0)
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z : K
⊢ z < 0 ↔ ↑re z < 0 ∧ ↑im z = 0
[PROOFSTEP]
simpa only [map_zero] using lt_iff_re_im (z := z) (w := 0)
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
x y : K
hxy : x ≤ y
z : K
⊢ z + x ≤ z + y
[PROOFSTEP]
rw [IsROrC.le_iff_re_im] at *
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
x y : K
hxy : ↑re x ≤ ↑re y ∧ ↑im x = ↑im y
z : K
⊢ ↑re (z + x) ≤ ↑re (z + y) ∧ ↑im (z + x) = ↑im (z + y)
[PROOFSTEP]
simpa [map_add, add_le_add_iff_left, add_right_inj] using hxy
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
x : K
⊢ 0 ≤ x ↔ ∃ s, x = star s * s
[PROOFSTEP]
rw [IsROrC.le_iff_re_im, map_zero, map_zero, IsROrC.star_def, eq_comm]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
x : K
⊢ 0 ≤ ↑re x ∧ ↑im x = 0 ↔ ∃ s, x = ↑(starRingEnd K) s * s
[PROOFSTEP]
constructor
[GOAL]
case mp
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
x : K
⊢ 0 ≤ ↑re x ∧ ↑im x = 0 → ∃ s, x = ↑(starRingEnd K) s * s
[PROOFSTEP]
rintro ⟨hr, hi⟩
[GOAL]
case mp.intro
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
x : K
hr : 0 ≤ ↑re x
hi : ↑im x = 0
⊢ ∃ s, x = ↑(starRingEnd K) s * s
[PROOFSTEP]
refine ⟨Real.sqrt (IsROrC.re x), ?_⟩
[GOAL]
case mp.intro
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
x : K
hr : 0 ≤ ↑re x
hi : ↑im x = 0
⊢ x = ↑(starRingEnd K) ↑(Real.sqrt (↑re x)) * ↑(Real.sqrt (↑re x))
[PROOFSTEP]
have := (IsROrC.is_real_TFAE x).out 2 3
[GOAL]
case mp.intro
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
x : K
hr : 0 ≤ ↑re x
hi : ↑im x = 0
this : ↑(↑re x) = x ↔ ↑im x = 0
⊢ x = ↑(starRingEnd K) ↑(Real.sqrt (↑re x)) * ↑(Real.sqrt (↑re x))
[PROOFSTEP]
rw [IsROrC.conj_ofReal, ← IsROrC.ofReal_mul, Real.mul_self_sqrt hr, eq_comm, this, hi]
[GOAL]
case mpr
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
x : K
⊢ (∃ s, x = ↑(starRingEnd K) s * s) → 0 ≤ ↑re x ∧ ↑im x = 0
[PROOFSTEP]
rintro ⟨s, rfl⟩
[GOAL]
case mpr.intro
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
s : K
⊢ 0 ≤ ↑re (↑(starRingEnd K) s * s) ∧ ↑im (↑(starRingEnd K) s * s) = 0
[PROOFSTEP]
simp only [IsROrC.star_def, IsROrC.conj_mul]
[GOAL]
case mpr.intro
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
s : K
⊢ 0 ≤ ↑re ↑(↑normSq s) ∧ ↑im ↑(↑normSq s) = 0
[PROOFSTEP]
rw [IsROrC.ofReal_re, IsROrC.ofReal_im, eq_self, and_true]
[GOAL]
case mpr.intro
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
s : K
⊢ 0 ≤ ↑normSq s
[PROOFSTEP]
apply IsROrC.normSq_nonneg
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
⊢ 0 ≤ 1
[PROOFSTEP]
simp [@IsROrC.le_iff_re_im K]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z w : K
hz : 0 < z
hw : 0 < w
⊢ 0 < z * w
[PROOFSTEP]
rw [lt_iff_re_im, map_zero] at hz hw ⊢
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
z w : K
hz : 0 < ↑re z ∧ ↑im 0 = ↑im z
hw : 0 < ↑re w ∧ ↑im 0 = ↑im w
⊢ 0 < ↑re (z * w) ∧ ↑im 0 = ↑im (z * w)
[PROOFSTEP]
simp [mul_re, mul_im, ← hz.2, ← hw.2, mul_pos hz.1 hw.1]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
⊢ ∀ (a b : K), a * b = b * a
[PROOFSTEP]
intros
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
a✝ b✝ : K
⊢ a✝ * b✝ = b✝ * a✝
[PROOFSTEP]
apply ext
[GOAL]
case hre
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
a✝ b✝ : K
⊢ ↑re (a✝ * b✝) = ↑re (b✝ * a✝)
[PROOFSTEP]
ring_nf
[GOAL]
case him
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
a✝ b✝ : K
⊢ ↑im (a✝ * b✝) = ↑im (b✝ * a✝)
[PROOFSTEP]
ring_nf
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
a b : K
r : ℝ
hab : a < b
hr : 0 < r
⊢ r • a ≤ r • b
[PROOFSTEP]
replace hab := hab.le
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
a b : K
r : ℝ
hr : 0 < r
hab : a ≤ b
⊢ r • a ≤ r • b
[PROOFSTEP]
rw [IsROrC.le_iff_re_im] at hab 
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
a b : K
r : ℝ
hr : 0 < r
hab : ↑re a ≤ ↑re b ∧ ↑im a = ↑im b
⊢ r • a ≤ r • b
[PROOFSTEP]
rw [IsROrC.le_iff_re_im, smul_re, smul_re, smul_im, smul_im]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
a b : K
r : ℝ
hr : 0 < r
hab : ↑re a ≤ ↑re b ∧ ↑im a = ↑im b
⊢ r * ↑re a ≤ r * ↑re b ∧ r * ↑im a = r * ↑im b
[PROOFSTEP]
exact hab.imp (fun h => mul_le_mul_of_nonneg_left h hr.le) (congr_arg _)
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
x : ℝ
⊢ ↑normSq x = x * x
[PROOFSTEP]
simp [IsROrC.normSq]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
x : K
⊢ ‖↑reLm x‖ ≤ 1 * ‖x‖
[PROOFSTEP]
rw [one_mul]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
x : K
⊢ ‖↑reLm x‖ ≤ ‖x‖
[PROOFSTEP]
exact abs_re_le_norm x
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
x : K
⊢ ‖↑imLm x‖ ≤ 1 * ‖x‖
[PROOFSTEP]
rw [one_mul]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
x : K
⊢ ‖↑imLm x‖ ≤ ‖x‖
[PROOFSTEP]
exact abs_im_le_norm x
