[GOAL]
z w : ℂ
H : z = w
⊢ z.re = w.re ∧ z.im = w.im
[PROOFSTEP]
simp [H]
[GOAL]
z w : ℝ
⊢ z = w → ↑z = ↑w
[PROOFSTEP]
apply congrArg
[GOAL]
r s : ℝ
⊢ (↑(r + s)).re = (↑r + ↑s).re ∧ (↑(r + s)).im = (↑r + ↑s).im
[PROOFSTEP]
simp [ofReal']
[GOAL]
r : ℝ
⊢ (↑(bit0 r)).re = (bit0 ↑r).re ∧ (↑(bit0 r)).im = (bit0 ↑r).im
[PROOFSTEP]
simp [bit0]
[GOAL]
r : ℝ
⊢ (↑(bit1 r)).re = (bit1 ↑r).re ∧ (↑(bit1 r)).im = (bit1 ↑r).im
[PROOFSTEP]
simp [bit1]
[GOAL]
r : ℝ
⊢ (↑(-r)).re = (-↑r).re ∧ (↑(-r)).im = (-↑r).im
[PROOFSTEP]
simp [ofReal']
[GOAL]
r s : ℝ
⊢ (↑(r * s)).re = (↑r * ↑s).re ∧ (↑(r * s)).im = (↑r * ↑s).im
[PROOFSTEP]
simp [ofReal']
[GOAL]
r : ℝ
z : ℂ
⊢ (↑r * z).re = r * z.re
[PROOFSTEP]
simp [ofReal']
[GOAL]
r : ℝ
z : ℂ
⊢ (↑r * z).im = r * z.im
[PROOFSTEP]
simp [ofReal']
[GOAL]
⊢ (I * I).re = (-1).re ∧ (I * I).im = (-1).im
[PROOFSTEP]
simp
[GOAL]
z : ℂ
⊢ (I * z).re = { re := -z.im, im := z.re }.re ∧ (I * z).im = { re := -z.im, im := z.re }.im
[PROOFSTEP]
simp
[GOAL]
a b : ℝ
⊢ { re := a, im := b }.re = (↑a + ↑b * I).re ∧ { re := a, im := b }.im = (↑a + ↑b * I).im
[PROOFSTEP]
simp [ofReal']
[GOAL]
z : ℂ
⊢ (↑z.re + ↑z.im * I).re = z.re ∧ (↑z.re + ↑z.im * I).im = z.im
[PROOFSTEP]
simp [ofReal']
[GOAL]
z : ℂ
⊢ (z * I).re = -z.im
[PROOFSTEP]
simp
[GOAL]
z : ℂ
⊢ (z * I).im = z.re
[PROOFSTEP]
simp
[GOAL]
z : ℂ
⊢ (I * z).re = -z.im
[PROOFSTEP]
simp
[GOAL]
z : ℂ
⊢ (I * z).im = z.re
[PROOFSTEP]
simp
[GOAL]
p : ℝ × ℝ
⊢ ↑equivRealProd.symm p = ↑p.fst + ↑p.snd * I
[PROOFSTEP]
ext
[GOAL]
case a
p : ℝ × ℝ
⊢ (↑equivRealProd.symm p).re = (↑p.fst + ↑p.snd * I).re
[PROOFSTEP]
simp [Complex.equivRealProd, ofReal']
[GOAL]
case a
p : ℝ × ℝ
⊢ (↑equivRealProd.symm p).im = (↑p.fst + ↑p.snd * I).im
[PROOFSTEP]
simp [Complex.equivRealProd, ofReal']
[GOAL]
R : Type u_1
inst✝ : SMul R ℝ
r : R
z : ℂ
⊢ (r • z).re = r • z.re
[PROOFSTEP]
simp [(· • ·), SMul.smul]
[GOAL]
R : Type u_1
inst✝ : SMul R ℝ
r : R
z : ℂ
⊢ (r • z).im = r • z.im
[PROOFSTEP]
simp [(· • ·), SMul.smul]
[GOAL]
⊢ ∀ (a b c : ℂ), a + b + c = a + (b + c)
[PROOFSTEP]
intros
[GOAL]
a✝ b✝ c✝ : ℂ
⊢ a✝ + b✝ + c✝ = a✝ + (b✝ + c✝)
[PROOFSTEP]
ext
[GOAL]
case a
a✝ b✝ c✝ : ℂ
⊢ (a✝ + b✝ + c✝).re = (a✝ + (b✝ + c✝)).re
[PROOFSTEP]
simp [add_assoc]
[GOAL]
case a
a✝ b✝ c✝ : ℂ
⊢ (a✝ + b✝ + c✝).im = (a✝ + (b✝ + c✝)).im
[PROOFSTEP]
simp [add_assoc]
[GOAL]
⊢ ∀ (a : ℂ), 0 + a = a
[PROOFSTEP]
intros
[GOAL]
a✝ : ℂ
⊢ 0 + a✝ = a✝
[PROOFSTEP]
ext
[GOAL]
case a
a✝ : ℂ
⊢ (0 + a✝).re = a✝.re
[PROOFSTEP]
simp
[GOAL]
case a
a✝ : ℂ
⊢ (0 + a✝).im = a✝.im
[PROOFSTEP]
simp
[GOAL]
⊢ ∀ (a : ℂ), a + 0 = a
[PROOFSTEP]
intros
[GOAL]
a✝ : ℂ
⊢ a✝ + 0 = a✝
[PROOFSTEP]
ext
[GOAL]
case a
a✝ : ℂ
⊢ (a✝ + 0).re = a✝.re
[PROOFSTEP]
simp
[GOAL]
case a
a✝ : ℂ
⊢ (a✝ + 0).im = a✝.im
[PROOFSTEP]
simp
[GOAL]
⊢ ∀ (x : ℂ), (fun n z => n • z) 0 x = 0
[PROOFSTEP]
intros
[GOAL]
x✝ : ℂ
⊢ (fun n z => n • z) 0 x✝ = 0
[PROOFSTEP]
ext
[GOAL]
case a
x✝ : ℂ
⊢ ((fun n z => n • z) 0 x✝).re = 0.re
[PROOFSTEP]
simp [smul_re, smul_im]
[GOAL]
case a
x✝ : ℂ
⊢ ((fun n z => n • z) 0 x✝).im = 0.im
[PROOFSTEP]
simp [smul_re, smul_im]
[GOAL]
⊢ ∀ (n : ℕ) (x : ℂ), (fun n z => n • z) (n + 1) x = x + (fun n z => n • z) n x
[PROOFSTEP]
intros
[GOAL]
n✝ : ℕ
x✝ : ℂ
⊢ (fun n z => n • z) (n✝ + 1) x✝ = x✝ + (fun n z => n • z) n✝ x✝
[PROOFSTEP]
ext
[GOAL]
case a
n✝ : ℕ
x✝ : ℂ
⊢ ((fun n z => n • z) (n✝ + 1) x✝).re = (x✝ + (fun n z => n • z) n✝ x✝).re
[PROOFSTEP]
simp [AddMonoid.nsmul_succ, add_mul, add_comm, smul_re, smul_im]
[GOAL]
case a
n✝ : ℕ
x✝ : ℂ
⊢ ((fun n z => n • z) (n✝ + 1) x✝).im = (x✝ + (fun n z => n • z) n✝ x✝).im
[PROOFSTEP]
simp [AddMonoid.nsmul_succ, add_mul, add_comm, smul_re, smul_im]
[GOAL]
⊢ ∀ (a : ℂ), (fun n z => n • z) 0 a = 0
[PROOFSTEP]
intros
[GOAL]
a✝ : ℂ
⊢ (fun n z => n • z) 0 a✝ = 0
[PROOFSTEP]
ext
[GOAL]
case a
a✝ : ℂ
⊢ ((fun n z => n • z) 0 a✝).re = 0.re
[PROOFSTEP]
simp [smul_re, smul_im]
[GOAL]
case a
a✝ : ℂ
⊢ ((fun n z => n • z) 0 a✝).im = 0.im
[PROOFSTEP]
simp [smul_re, smul_im]
[GOAL]
⊢ ∀ (n : ℕ) (a : ℂ), (fun n z => n • z) (Int.ofNat (Nat.succ n)) a = a + (fun n z => n • z) (Int.ofNat n) a
[PROOFSTEP]
intros
[GOAL]
n✝ : ℕ
a✝ : ℂ
⊢ (fun n z => n • z) (Int.ofNat (Nat.succ n✝)) a✝ = a✝ + (fun n z => n • z) (Int.ofNat n✝) a✝
[PROOFSTEP]
ext
[GOAL]
case a
n✝ : ℕ
a✝ : ℂ
⊢ ((fun n z => n • z) (Int.ofNat (Nat.succ n✝)) a✝).re = (a✝ + (fun n z => n • z) (Int.ofNat n✝) a✝).re
[PROOFSTEP]
simp [SubNegMonoid.zsmul_succ', add_mul, add_comm, smul_re, smul_im]
[GOAL]
case a
n✝ : ℕ
a✝ : ℂ
⊢ ((fun n z => n • z) (Int.ofNat (Nat.succ n✝)) a✝).im = (a✝ + (fun n z => n • z) (Int.ofNat n✝) a✝).im
[PROOFSTEP]
simp [SubNegMonoid.zsmul_succ', add_mul, add_comm, smul_re, smul_im]
[GOAL]
⊢ ∀ (n : ℕ) (a : ℂ), (fun n z => n • z) (Int.negSucc n) a = -(fun n z => n • z) (↑(Nat.succ n)) a
[PROOFSTEP]
intros
[GOAL]
n✝ : ℕ
a✝ : ℂ
⊢ (fun n z => n • z) (Int.negSucc n✝) a✝ = -(fun n z => n • z) (↑(Nat.succ n✝)) a✝
[PROOFSTEP]
ext
[GOAL]
case a
n✝ : ℕ
a✝ : ℂ
⊢ ((fun n z => n • z) (Int.negSucc n✝) a✝).re = (-(fun n z => n • z) (↑(Nat.succ n✝)) a✝).re
[PROOFSTEP]
simp [zsmul_neg', add_mul, smul_re, smul_im]
[GOAL]
case a
n✝ : ℕ
a✝ : ℂ
⊢ ((fun n z => n • z) (Int.negSucc n✝) a✝).im = (-(fun n z => n • z) (↑(Nat.succ n✝)) a✝).im
[PROOFSTEP]
simp [zsmul_neg', add_mul, smul_re, smul_im]
[GOAL]
⊢ ∀ (a : ℂ), -a + a = 0
[PROOFSTEP]
intros
[GOAL]
a✝ : ℂ
⊢ -a✝ + a✝ = 0
[PROOFSTEP]
ext
[GOAL]
case a
a✝ : ℂ
⊢ (-a✝ + a✝).re = 0.re
[PROOFSTEP]
simp
[GOAL]
case a
a✝ : ℂ
⊢ (-a✝ + a✝).im = 0.im
[PROOFSTEP]
simp
[GOAL]
⊢ ∀ (a b : ℂ), a + b = b + a
[PROOFSTEP]
intros
[GOAL]
a✝ b✝ : ℂ
⊢ a✝ + b✝ = b✝ + a✝
[PROOFSTEP]
ext
[GOAL]
case a
a✝ b✝ : ℂ
⊢ (a✝ + b✝).re = (b✝ + a✝).re
[PROOFSTEP]
simp [add_comm]
[GOAL]
case a
a✝ b✝ : ℂ
⊢ (a✝ + b✝).im = (b✝ + a✝).im
[PROOFSTEP]
simp [add_comm]
[GOAL]
src✝ : AddCommGroup ℂ := addCommGroup
⊢ NatCast.natCast 0 = 0
[PROOFSTEP]
ext
[GOAL]
case a
src✝ : AddCommGroup ℂ := addCommGroup
⊢ (NatCast.natCast 0).re = 0.re
[PROOFSTEP]
simp [Nat.cast, AddMonoidWithOne.natCast_zero]
[GOAL]
case a
src✝ : AddCommGroup ℂ := addCommGroup
⊢ (NatCast.natCast 0).im = 0.im
[PROOFSTEP]
simp [Nat.cast, AddMonoidWithOne.natCast_zero]
[GOAL]
src✝ : AddCommGroup ℂ := addCommGroup
x✝ : ℕ
⊢ NatCast.natCast (x✝ + 1) = NatCast.natCast x✝ + 1
[PROOFSTEP]
ext
[GOAL]
case a
src✝ : AddCommGroup ℂ := addCommGroup
x✝ : ℕ
⊢ (NatCast.natCast (x✝ + 1)).re = (NatCast.natCast x✝ + 1).re
[PROOFSTEP]
simp [Nat.cast, AddMonoidWithOne.natCast_succ]
[GOAL]
case a
src✝ : AddCommGroup ℂ := addCommGroup
x✝ : ℕ
⊢ (NatCast.natCast (x✝ + 1)).im = (NatCast.natCast x✝ + 1).im
[PROOFSTEP]
simp [Nat.cast, AddMonoidWithOne.natCast_succ]
[GOAL]
src✝ : AddCommGroup ℂ := addCommGroup
x✝ : ℕ
⊢ IntCast.intCast ↑x✝ = ↑x✝
[PROOFSTEP]
ext
[GOAL]
case a
src✝ : AddCommGroup ℂ := addCommGroup
x✝ : ℕ
⊢ (IntCast.intCast ↑x✝).re = (↑x✝).re
[PROOFSTEP]
rfl
[GOAL]
case a
src✝ : AddCommGroup ℂ := addCommGroup
x✝ : ℕ
⊢ (IntCast.intCast ↑x✝).im = (↑x✝).im
[PROOFSTEP]
rfl
[GOAL]
src✝ : AddCommGroup ℂ := addCommGroup
n : ℕ
⊢ IntCast.intCast (Int.negSucc n) = -↑(n + 1)
[PROOFSTEP]
ext
[GOAL]
case a
src✝ : AddCommGroup ℂ := addCommGroup
n : ℕ
⊢ (IntCast.intCast (Int.negSucc n)).re = (-↑(n + 1)).re
[PROOFSTEP]
simp [AddGroupWithOne.intCast_negSucc]
[GOAL]
case a
src✝ : AddCommGroup ℂ := addCommGroup
n : ℕ
⊢ -1 + -↑n = -(↑(n + 1)).re
[PROOFSTEP]
show -(1 : ℝ) + (-n) = -(↑(n + 1))
[GOAL]
case a
src✝ : AddCommGroup ℂ := addCommGroup
n : ℕ
⊢ -1 + -↑n = -↑(n + 1)
[PROOFSTEP]
simp [Nat.cast_add, add_comm]
[GOAL]
case a
src✝ : AddCommGroup ℂ := addCommGroup
n : ℕ
⊢ (IntCast.intCast (Int.negSucc n)).im = (-↑(n + 1)).im
[PROOFSTEP]
simp [AddGroupWithOne.intCast_negSucc]
[GOAL]
case a
src✝ : AddCommGroup ℂ := addCommGroup
n : ℕ
⊢ (↑(n + 1)).im = 0
[PROOFSTEP]
show im ⟨n, 0⟩ = 0
[GOAL]
case a
src✝ : AddCommGroup ℂ := addCommGroup
n : ℕ
⊢ { re := ↑n, im := 0 }.im = 0
[PROOFSTEP]
rfl
[GOAL]
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
⊢ ∀ (a b : ℂ), a + b = b + a
[PROOFSTEP]
intros
[GOAL]
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ b✝ : ℂ
⊢ a✝ + b✝ = b✝ + a✝
[PROOFSTEP]
ext
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ b✝ : ℂ
⊢ (a✝ + b✝).re = (b✝ + a✝).re
[PROOFSTEP]
simp [add_comm]
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ b✝ : ℂ
⊢ (a✝ + b✝).im = (b✝ + a✝).im
[PROOFSTEP]
simp [add_comm]
[GOAL]
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
⊢ ∀ (a b c : ℂ), a * (b + c) = a * b + a * c
[PROOFSTEP]
intros
[GOAL]
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ b✝ c✝ : ℂ
⊢ a✝ * (b✝ + c✝) = a✝ * b✝ + a✝ * c✝
[PROOFSTEP]
ext
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ b✝ c✝ : ℂ
⊢ (a✝ * (b✝ + c✝)).re = (a✝ * b✝ + a✝ * c✝).re
[PROOFSTEP]
simp [mul_re, mul_im]
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ b✝ c✝ : ℂ
⊢ (a✝ * (b✝ + c✝)).im = (a✝ * b✝ + a✝ * c✝).im
[PROOFSTEP]
simp [mul_re, mul_im]
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ b✝ c✝ : ℂ
⊢ a✝.re * (b✝.re + c✝.re) - a✝.im * (b✝.im + c✝.im) = a✝.re * b✝.re - a✝.im * b✝.im + (a✝.re * c✝.re - a✝.im * c✝.im)
[PROOFSTEP]
ring
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ b✝ c✝ : ℂ
⊢ a✝.re * (b✝.im + c✝.im) + a✝.im * (b✝.re + c✝.re) = a✝.re * b✝.im + a✝.im * b✝.re + (a✝.re * c✝.im + a✝.im * c✝.re)
[PROOFSTEP]
ring
[GOAL]
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
⊢ ∀ (a b c : ℂ), (a + b) * c = a * c + b * c
[PROOFSTEP]
intros
[GOAL]
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ b✝ c✝ : ℂ
⊢ (a✝ + b✝) * c✝ = a✝ * c✝ + b✝ * c✝
[PROOFSTEP]
ext
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ b✝ c✝ : ℂ
⊢ ((a✝ + b✝) * c✝).re = (a✝ * c✝ + b✝ * c✝).re
[PROOFSTEP]
simp [mul_re, mul_im]
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ b✝ c✝ : ℂ
⊢ ((a✝ + b✝) * c✝).im = (a✝ * c✝ + b✝ * c✝).im
[PROOFSTEP]
simp [mul_re, mul_im]
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ b✝ c✝ : ℂ
⊢ (a✝.re + b✝.re) * c✝.re - (a✝.im + b✝.im) * c✝.im = a✝.re * c✝.re - a✝.im * c✝.im + (b✝.re * c✝.re - b✝.im * c✝.im)
[PROOFSTEP]
ring
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ b✝ c✝ : ℂ
⊢ (a✝.re + b✝.re) * c✝.im + (a✝.im + b✝.im) * c✝.re = a✝.re * c✝.im + a✝.im * c✝.re + (b✝.re * c✝.im + b✝.im * c✝.re)
[PROOFSTEP]
ring
[GOAL]
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
⊢ ∀ (a : ℂ), 0 * a = 0
[PROOFSTEP]
intros
[GOAL]
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ : ℂ
⊢ 0 * a✝ = 0
[PROOFSTEP]
ext
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ : ℂ
⊢ (0 * a✝).re = 0.re
[PROOFSTEP]
simp [zero_mul]
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ : ℂ
⊢ (0 * a✝).im = 0.im
[PROOFSTEP]
simp [zero_mul]
[GOAL]
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
⊢ ∀ (a : ℂ), a * 0 = 0
[PROOFSTEP]
intros
[GOAL]
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ : ℂ
⊢ a✝ * 0 = 0
[PROOFSTEP]
ext
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ : ℂ
⊢ (a✝ * 0).re = 0.re
[PROOFSTEP]
simp [mul_zero]
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ : ℂ
⊢ (a✝ * 0).im = 0.im
[PROOFSTEP]
simp [mul_zero]
[GOAL]
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
⊢ ∀ (a b c : ℂ), a * b * c = a * (b * c)
[PROOFSTEP]
intros
[GOAL]
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ b✝ c✝ : ℂ
⊢ a✝ * b✝ * c✝ = a✝ * (b✝ * c✝)
[PROOFSTEP]
ext
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ b✝ c✝ : ℂ
⊢ (a✝ * b✝ * c✝).re = (a✝ * (b✝ * c✝)).re
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ b✝ c✝ : ℂ
⊢ (a✝ * b✝ * c✝).im = (a✝ * (b✝ * c✝)).im
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ b✝ c✝ : ℂ
⊢ (a✝.re * b✝.re - a✝.im * b✝.im) * c✝.re - (a✝.re * b✝.im + a✝.im * b✝.re) * c✝.im =
    a✝.re * (b✝.re * c✝.re - b✝.im * c✝.im) - a✝.im * (b✝.re * c✝.im + b✝.im * c✝.re)
[PROOFSTEP]
ring
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ b✝ c✝ : ℂ
⊢ (a✝.re * b✝.re - a✝.im * b✝.im) * c✝.im + (a✝.re * b✝.im + a✝.im * b✝.re) * c✝.re =
    a✝.re * (b✝.re * c✝.im + b✝.im * c✝.re) + a✝.im * (b✝.re * c✝.re - b✝.im * c✝.im)
[PROOFSTEP]
ring
[GOAL]
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
⊢ ∀ (a : ℂ), 1 * a = a
[PROOFSTEP]
intros
[GOAL]
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ : ℂ
⊢ 1 * a✝ = a✝
[PROOFSTEP]
ext
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ : ℂ
⊢ (1 * a✝).re = a✝.re
[PROOFSTEP]
simp [one_mul]
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ : ℂ
⊢ (1 * a✝).im = a✝.im
[PROOFSTEP]
simp [one_mul]
[GOAL]
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
⊢ ∀ (a : ℂ), a * 1 = a
[PROOFSTEP]
intros
[GOAL]
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ : ℂ
⊢ a✝ * 1 = a✝
[PROOFSTEP]
ext
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ : ℂ
⊢ (a✝ * 1).re = a✝.re
[PROOFSTEP]
simp [mul_one]
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ : ℂ
⊢ (a✝ * 1).im = a✝.im
[PROOFSTEP]
simp [mul_one]
[GOAL]
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
⊢ ∀ (a b : ℂ), a * b = b * a
[PROOFSTEP]
intros
[GOAL]
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ b✝ : ℂ
⊢ a✝ * b✝ = b✝ * a✝
[PROOFSTEP]
ext
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ b✝ : ℂ
⊢ (a✝ * b✝).re = (b✝ * a✝).re
[PROOFSTEP]
simp [mul_comm]
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ b✝ : ℂ
⊢ (a✝ * b✝).im = (b✝ * a✝).im
[PROOFSTEP]
simp [mul_comm]
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ b✝ : ℂ
⊢ a✝.re * b✝.im + b✝.re * a✝.im = b✝.re * a✝.im + a✝.re * b✝.im
[PROOFSTEP]
ring
[GOAL]
⊢ Ring ℂ
[PROOFSTEP]
infer_instance
[GOAL]
n : ℕ
⊢ I ^ bit0 n = (-1) ^ n
[PROOFSTEP]
rw [pow_bit0', Complex.I_mul_I]
[GOAL]
n : ℕ
⊢ I ^ bit1 n = (-1) ^ n * I
[PROOFSTEP]
rw [pow_bit1', Complex.I_mul_I]
[GOAL]
x : ℂ
⊢ star (star x) = x
[PROOFSTEP]
simp only [eta, neg_neg]
[GOAL]
a b : ℂ
⊢ star (a * b) = star b * star a
[PROOFSTEP]
ext
[GOAL]
case a
a b : ℂ
⊢ (star (a * b)).re = (star b * star a).re
[PROOFSTEP]
simp [add_comm]
[GOAL]
case a
a b : ℂ
⊢ (star (a * b)).im = (star b * star a).im
[PROOFSTEP]
simp [add_comm]
[GOAL]
case a
a b : ℂ
⊢ a.re * b.re - a.im * b.im = b.re * a.re - b.im * a.im
[PROOFSTEP]
ring
[GOAL]
case a
a b : ℂ
⊢ -(a.re * b.im) + -(a.im * b.re) = -(b.re * a.im) + -(b.im * a.re)
[PROOFSTEP]
ring
[GOAL]
a b : ℂ
⊢ star (a + b) = star a + star b
[PROOFSTEP]
ext
[GOAL]
case a
a b : ℂ
⊢ (star (a + b)).re = (star a + star b).re
[PROOFSTEP]
simp [add_comm]
[GOAL]
case a
a b : ℂ
⊢ (star (a + b)).im = (star a + star b).im
[PROOFSTEP]
simp [add_comm]
[GOAL]
r : ℝ
⊢ (↑(starRingEnd ℂ) ↑r).re = (↑r).re ∧ (↑(starRingEnd ℂ) ↑r).im = (↑r).im
[PROOFSTEP]
simp [star]
[GOAL]
⊢ (↑(starRingEnd ℂ) I).re = (-I).re ∧ (↑(starRingEnd ℂ) I).im = (-I).im
[PROOFSTEP]
simp
[GOAL]
z : ℂ
⊢ (↑(starRingEnd ℂ) (bit0 z)).re = (bit0 (↑(starRingEnd ℂ) z)).re ∧
    (↑(starRingEnd ℂ) (bit0 z)).im = (bit0 (↑(starRingEnd ℂ) z)).im
[PROOFSTEP]
simp [bit0]
[GOAL]
z : ℂ
⊢ (↑(starRingEnd ℂ) (bit1 z)).re = (bit1 (↑(starRingEnd ℂ) z)).re ∧
    (↑(starRingEnd ℂ) (bit1 z)).im = (bit1 (↑(starRingEnd ℂ) z)).im
[PROOFSTEP]
simp [bit0]
[GOAL]
⊢ (↑(starRingEnd ℂ) (-I)).re = I.re ∧ (↑(starRingEnd ℂ) (-I)).im = I.im
[PROOFSTEP]
simp
[GOAL]
z : ℂ
x✝ : ∃ r, z = ↑r
h : ℝ
e : z = ↑h
⊢ ↑(starRingEnd ℂ) z = z
[PROOFSTEP]
rw [e, conj_ofReal]
[GOAL]
z : ℂ
⊢ (∃ r, z = ↑r) → ↑z.re = z
[PROOFSTEP]
rintro ⟨r, rfl⟩
[GOAL]
case intro
r : ℝ
⊢ ↑(↑r).re = ↑r
[PROOFSTEP]
simp [ofReal']
[GOAL]
⊢ (fun z => z.re * z.re + z.im * z.im) 0 = 0
[PROOFSTEP]
simp
[GOAL]
⊢ ZeroHom.toFun { toFun := fun z => z.re * z.re + z.im * z.im, map_zero' := (_ : 0 * 0 + 0 * 0 = 0) } 1 = 1
[PROOFSTEP]
simp
[GOAL]
z w : ℂ
⊢ ZeroHom.toFun { toFun := fun z => z.re * z.re + z.im * z.im, map_zero' := (_ : 0 * 0 + 0 * 0 = 0) } (z * w) =
    ZeroHom.toFun { toFun := fun z => z.re * z.re + z.im * z.im, map_zero' := (_ : 0 * 0 + 0 * 0 = 0) } z *
      ZeroHom.toFun { toFun := fun z => z.re * z.re + z.im * z.im, map_zero' := (_ : 0 * 0 + 0 * 0 = 0) } w
[PROOFSTEP]
dsimp
[GOAL]
z w : ℂ
⊢ (z.re * w.re - z.im * w.im) * (z.re * w.re - z.im * w.im) +
      (z.re * w.im + z.im * w.re) * (z.re * w.im + z.im * w.re) =
    (z.re * z.re + z.im * z.im) * (w.re * w.re + w.im * w.im)
[PROOFSTEP]
ring
[GOAL]
r : ℝ
⊢ ↑normSq ↑r = r * r
[PROOFSTEP]
simp [normSq, ofReal']
[GOAL]
x y : ℝ
⊢ ↑normSq (↑x + ↑y * I) = x ^ 2 + y ^ 2
[PROOFSTEP]
rw [← mk_eq_add_mul_I, normSq_mk, sq, sq]
[GOAL]
z : ℂ
⊢ ↑(↑normSq z) = ↑(starRingEnd ℂ) z * z
[PROOFSTEP]
ext
[GOAL]
case a
z : ℂ
⊢ (↑(↑normSq z)).re = (↑(starRingEnd ℂ) z * z).re
[PROOFSTEP]
simp [normSq, mul_comm, ofReal']
[GOAL]
case a
z : ℂ
⊢ (↑(↑normSq z)).im = (↑(starRingEnd ℂ) z * z).im
[PROOFSTEP]
simp [normSq, mul_comm, ofReal']
[GOAL]
⊢ ↑normSq I = 1
[PROOFSTEP]
simp [normSq]
[GOAL]
x : ℝ
hx : x ∈ Ici 0
⊢ ↑normSq ↑(Real.sqrt x) = x
[PROOFSTEP]
rw [normSq_ofReal, Real.mul_self_sqrt hx]
[GOAL]
z : ℂ
⊢ ↑normSq (-z) = ↑normSq z
[PROOFSTEP]
simp [normSq]
[GOAL]
z : ℂ
⊢ ↑normSq (↑(starRingEnd ℂ) z) = ↑normSq z
[PROOFSTEP]
simp [normSq]
[GOAL]
z w : ℂ
⊢ ↑normSq (z + w) = ↑normSq z + ↑normSq w + 2 * (z * ↑(starRingEnd ℂ) w).re
[PROOFSTEP]
dsimp [normSq]
[GOAL]
z w : ℂ
⊢ (z.re + w.re) * (z.re + w.re) + (z.im + w.im) * (z.im + w.im) =
    z.re * z.re + z.im * z.im + (w.re * w.re + w.im * w.im) + 2 * (z.re * w.re - z.im * -w.im)
[PROOFSTEP]
ring
[GOAL]
z : ℂ
⊢ (z * ↑(starRingEnd ℂ) z).re = (↑(↑normSq z)).re ∧ (z * ↑(starRingEnd ℂ) z).im = (↑(↑normSq z)).im
[PROOFSTEP]
simp [normSq, mul_comm, sub_eq_neg_add, add_comm, ofReal']
[GOAL]
z : ℂ
⊢ (z + ↑(starRingEnd ℂ) z).re = (↑(2 * z.re)).re ∧ (z + ↑(starRingEnd ℂ) z).im = (↑(2 * z.re)).im
[PROOFSTEP]
simp [two_mul, ofReal']
[GOAL]
⊢ I ^ 2 = -1
[PROOFSTEP]
rw [sq, I_mul_I]
[GOAL]
r s : ℝ
⊢ (↑(r - s)).re = (↑r - ↑s).re ∧ (↑(r - s)).im = (↑r - ↑s).im
[PROOFSTEP]
simp [ofReal']
[GOAL]
r : ℝ
n : ℕ
⊢ ↑(r ^ n) = ↑r ^ n
[PROOFSTEP]
induction n
[GOAL]
case zero
r : ℝ
⊢ ↑(r ^ Nat.zero) = ↑r ^ Nat.zero
[PROOFSTEP]
simp [*, ofReal_mul, pow_succ]
[GOAL]
case succ
r : ℝ
n✝ : ℕ
n_ih✝ : ↑(r ^ n✝) = ↑r ^ n✝
⊢ ↑(r ^ Nat.succ n✝) = ↑r ^ Nat.succ n✝
[PROOFSTEP]
simp [*, ofReal_mul, pow_succ]
[GOAL]
z : ℂ
⊢ (z - ↑(starRingEnd ℂ) z).re = (↑(2 * z.im) * I).re ∧ (z - ↑(starRingEnd ℂ) z).im = (↑(2 * z.im) * I).im
[PROOFSTEP]
simp [two_mul, sub_eq_add_neg, ofReal']
[GOAL]
z w : ℂ
⊢ ↑normSq (z - w) = ↑normSq z + ↑normSq w - 2 * (z * ↑(starRingEnd ℂ) w).re
[PROOFSTEP]
rw [sub_eq_add_neg, normSq_add]
[GOAL]
z w : ℂ
⊢ ↑normSq z + ↑normSq (-w) + 2 * (z * ↑(starRingEnd ℂ) (-w)).re =
    ↑normSq z + ↑normSq w - 2 * (z * ↑(starRingEnd ℂ) w).re
[PROOFSTEP]
simp only [RingHom.map_neg, mul_neg, neg_re, normSq_neg]
[GOAL]
z w : ℂ
⊢ ↑normSq z + ↑normSq w + -(2 * (z * ↑(starRingEnd ℂ) w).re) = ↑normSq z + ↑normSq w - 2 * (z * ↑(starRingEnd ℂ) w).re
[PROOFSTEP]
ring
[GOAL]
z : ℂ
⊢ z⁻¹.re = z.re / ↑normSq z
[PROOFSTEP]
simp [inv_def, division_def, ofReal']
[GOAL]
z : ℂ
⊢ z⁻¹.im = -z.im / ↑normSq z
[PROOFSTEP]
simp [inv_def, division_def, ofReal']
[GOAL]
r : ℝ
⊢ (↑r⁻¹).re = (↑r)⁻¹.re ∧ (↑r⁻¹).im = (↑r)⁻¹.im
[PROOFSTEP]
simp [ofReal']
[GOAL]
⊢ 0⁻¹ = 0
[PROOFSTEP]
rw [← ofReal_zero, ← ofReal_inv, inv_zero]
[GOAL]
z : ℂ
h : z ≠ 0
⊢ z * z⁻¹ = 1
[PROOFSTEP]
rw [inv_def, ← mul_assoc, mul_conj, ← ofReal_mul, mul_inv_cancel (mt normSq_eq_zero.1 h), ofReal_one]
[GOAL]
n : ℕ
⊢ (↑n).re = ↑n
[PROOFSTEP]
rw [← ofReal_nat_cast, ofReal_re]
[GOAL]
n : ℕ
⊢ (↑n).im = 0
[PROOFSTEP]
rw [← ofReal_nat_cast, ofReal_im]
[GOAL]
n : ℤ
⊢ (↑n).re = ↑n
[PROOFSTEP]
rw [← ofReal_int_cast, ofReal_re]
[GOAL]
n : ℤ
⊢ (↑n).im = 0
[PROOFSTEP]
rw [← ofReal_int_cast, ofReal_im]
[GOAL]
q : ℚ
⊢ (↑q).im = 0
[PROOFSTEP]
show (Rat.castRec q : ℂ).im = 0
[GOAL]
q : ℚ
⊢ (Rat.castRec q).im = 0
[PROOFSTEP]
cases q
[GOAL]
case mk'
num✝ : ℤ
den✝ : ℕ
den_nz✝ : den✝ ≠ 0
reduced✝ : Nat.coprime (Int.natAbs num✝) den✝
⊢ (Rat.castRec (Rat.mk' num✝ den✝)).im = 0
[PROOFSTEP]
simp [Rat.castRec]
[GOAL]
q : ℚ
⊢ (↑q).re = ↑q
[PROOFSTEP]
show (Rat.castRec q : ℂ).re = _
[GOAL]
q : ℚ
⊢ (Rat.castRec q).re = ↑q
[PROOFSTEP]
cases q
[GOAL]
case mk'
num✝ : ℤ
den✝ : ℕ
den_nz✝ : den✝ ≠ 0
reduced✝ : Nat.coprime (Int.natAbs num✝) den✝
⊢ (Rat.castRec (Rat.mk' num✝ den✝)).re = ↑(Rat.mk' num✝ den✝)
[PROOFSTEP]
simp [Rat.castRec, normSq, Rat.mk_eq_divInt, Rat.mkRat_eq_div, div_eq_mul_inv, *]
[GOAL]
n : ℚ
z : ℂ
⊢ ((fun n z => n • z) n z).re = (↑n * z).re ∧ ((fun n z => n • z) n z).im = (↑n * z).im
[PROOFSTEP]
simp [Rat.smul_def, smul_re, smul_im]
[GOAL]
n : ℤ
⊢ I ^ bit0 n = (-1) ^ n
[PROOFSTEP]
rw [zpow_bit0', I_mul_I]
[GOAL]
n : ℤ
⊢ I ^ bit1 n = (-1) ^ n * I
[PROOFSTEP]
rw [zpow_bit1', I_mul_I]
[GOAL]
z w : ℂ
⊢ (z / w).re = z.re * w.re / ↑normSq w + z.im * w.im / ↑normSq w
[PROOFSTEP]
simp [div_eq_mul_inv, mul_assoc, sub_eq_add_neg]
[GOAL]
z w : ℂ
⊢ (z / w).im = z.im * w.re / ↑normSq w - z.re * w.im / ↑normSq w
[PROOFSTEP]
simp [div_eq_mul_inv, mul_assoc, sub_eq_add_neg, add_comm]
[GOAL]
z : ℂ
⊢ -(z * I) * I = z
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
⊢ I⁻¹ = -I
[PROOFSTEP]
rw [inv_eq_one_div, div_I, one_mul]
[GOAL]
n : ℕ
h : ↑n = 0
⊢ n = 0
[PROOFSTEP]
rwa [← ofReal_nat_cast, ofReal_eq_zero, Nat.cast_eq_zero] at h 
[GOAL]
z : ℂ
⊢ ↑z.re = (z + ↑(starRingEnd ℂ) z) / 2
[PROOFSTEP]
have : (↑(↑2 : ℝ) : ℂ) = (2 : ℂ) := by rfl
[GOAL]
z : ℂ
⊢ ↑2 = 2
[PROOFSTEP]
rfl
[GOAL]
z : ℂ
this : ↑2 = 2
⊢ ↑z.re = (z + ↑(starRingEnd ℂ) z) / 2
[PROOFSTEP]
simp only [add_conj, ofReal_mul, ofReal_one, ofReal_bit0, this, mul_div_cancel_left (z.re : ℂ) two_ne_zero]
[GOAL]
z : ℂ
⊢ ↑z.im = (z - ↑(starRingEnd ℂ) z) / (2 * I)
[PROOFSTEP]
have : (↑2 : ℝ) * I = 2 * I := by rfl
[GOAL]
z : ℂ
⊢ ↑2 * I = 2 * I
[PROOFSTEP]
rfl
[GOAL]
z : ℂ
this : ↑2 * I = 2 * I
⊢ ↑z.im = (z - ↑(starRingEnd ℂ) z) / (2 * I)
[PROOFSTEP]
simp only [sub_conj, ofReal_mul, ofReal_one, ofReal_bit0, mul_right_comm, this,
  mul_div_cancel_left _ (mul_ne_zero two_ne_zero I_ne_zero : 2 * I ≠ 0)]
[GOAL]
z : ℂ
⊢ Real.sqrt (↑normSq (↑(starRingEnd ℂ) z)) = Real.sqrt (↑normSq z)
[PROOFSTEP]
simp
[GOAL]
z : ℂ
⊢ |z.re| ≤ Real.sqrt (↑normSq z)
[PROOFSTEP]
rw [mul_self_le_mul_self_iff (abs_nonneg z.re) (abs_nonneg' _), abs_mul_abs_self, mul_self_abs]
[GOAL]
z : ℂ
⊢ z.re * z.re ≤ ↑normSq z
[PROOFSTEP]
apply re_sq_le_normSq
[GOAL]
z w : ℂ
⊢ Real.sqrt (↑normSq (z * w)) = Real.sqrt (↑normSq z) * Real.sqrt (↑normSq w)
[PROOFSTEP]
rw [normSq_mul, Real.sqrt_mul (normSq_nonneg _)]
[GOAL]
z w : ℂ
⊢ Real.sqrt (↑normSq (z + w)) * Real.sqrt (↑normSq (z + w)) ≤
    (Real.sqrt (↑normSq z) + Real.sqrt (↑normSq w)) * (Real.sqrt (↑normSq z) + Real.sqrt (↑normSq w))
[PROOFSTEP]
rw [mul_self_abs, add_mul_self_eq, mul_self_abs, mul_self_abs, add_right_comm, normSq_add, add_le_add_iff_left,
  mul_assoc, mul_le_mul_left (zero_lt_two' ℝ), ← Real.sqrt_mul <| normSq_nonneg z, ← normSq_conj w, ← map_mul]
[GOAL]
z w : ℂ
⊢ (z * ↑(starRingEnd ℂ) w).re ≤ Real.sqrt (↑normSq (z * ↑(starRingEnd ℂ) w))
[PROOFSTEP]
exact re_le_abs (z * conj w)
[GOAL]
r : ℝ
⊢ ↑abs ↑r = |r|
[PROOFSTEP]
simp [Complex.abs, normSq_ofReal, Real.sqrt_mul_self_eq_abs]
[GOAL]
n : ℕ
⊢ ↑abs ↑n = ↑abs ↑↑n
[PROOFSTEP]
rw [ofReal_nat_cast]
[GOAL]
z : ℂ
⊢ ↑abs z ^ 2 - z.re ^ 2 = z.im ^ 2
[PROOFSTEP]
rw [sq_abs, normSq_apply, ← sq, ← sq, add_sub_cancel']
[GOAL]
z : ℂ
⊢ ↑abs z ^ 2 - z.im ^ 2 = z.re ^ 2
[PROOFSTEP]
rw [← sq_abs_sub_sq_re, sub_sub_cancel]
[GOAL]
⊢ ↑abs I = 1
[PROOFSTEP]
simp [Complex.abs]
[GOAL]
⊢ ↑abs 2 = ↑abs ↑2
[PROOFSTEP]
rfl
[GOAL]
⊢ 0 ≤ 2
[PROOFSTEP]
norm_num
[GOAL]
⊢ range ↑abs ⊆ Ici 0
[PROOFSTEP]
simp only [range_subset_iff, Ici, mem_setOf_eq, map_nonneg, forall_const]
[GOAL]
z : ℂ
⊢ z.re ^ 2 ≤ ↑normSq z
[PROOFSTEP]
rw [normSq_apply, ← sq]
[GOAL]
z : ℂ
⊢ z.re ^ 2 ≤ z.re ^ 2 + z.im * z.im
[PROOFSTEP]
exact le_add_of_nonneg_right (mul_self_nonneg _)
[GOAL]
z : ℂ
⊢ z.im ^ 2 ≤ ↑normSq z
[PROOFSTEP]
rw [normSq_apply, ← sq, ← sq]
[GOAL]
z : ℂ
⊢ z.im ^ 2 ≤ z.re ^ 2 + z.im ^ 2
[PROOFSTEP]
exact le_add_of_nonneg_left (sq_nonneg _)
[GOAL]
z : ℂ
⊢ |z.re| < ↑abs z ↔ z.im ≠ 0
[PROOFSTEP]
rw [Complex.abs, AbsoluteValue.coe_mk, MulHom.coe_mk, Real.lt_sqrt (abs_nonneg _), normSq_apply, _root_.sq_abs, ← sq,
  lt_add_iff_pos_right, mul_self_pos]
[GOAL]
z : ℂ
⊢ |z.im| < ↑abs z ↔ z.re ≠ 0
[PROOFSTEP]
simpa using @abs_re_lt_abs (z * I)
[GOAL]
z : ℂ
⊢ ↑abs z ≤ |z.re| + |z.im|
[PROOFSTEP]
simpa [re_add_im] using Complex.abs.add_le z.re (z.im * I)
[GOAL]
⊢ 1 ≠ 0
[PROOFSTEP]
apply one_ne_zero
[GOAL]
z : ℂ
⊢ ↑abs z ≤ Real.sqrt 2 * max |z.re| |z.im|
[PROOFSTEP]
cases' z with x y
[GOAL]
case mk
x y : ℝ
⊢ ↑abs { re := x, im := y } ≤ Real.sqrt 2 * max |{ re := x, im := y }.re| |{ re := x, im := y }.im|
[PROOFSTEP]
simp only [abs_apply, normSq_mk, ← sq]
[GOAL]
case mk
x y : ℝ
⊢ Real.sqrt (x ^ 2 + y ^ 2) ≤ Real.sqrt 2 * max |x| |y|
[PROOFSTEP]
by_cases hle : |x| ≤ |y|
[GOAL]
case pos
x y : ℝ
hle : |x| ≤ |y|
⊢ Real.sqrt (x ^ 2 + y ^ 2) ≤ Real.sqrt 2 * max |x| |y|
[PROOFSTEP]
calc
  Real.sqrt (x ^ 2 + y ^ 2) ≤ Real.sqrt (y ^ 2 + y ^ 2) := Real.sqrt_le_sqrt (add_le_add_right (sq_le_sq.2 hle) _)
  _ = Real.sqrt 2 * max |x| |y| := by rw [max_eq_right hle, ← two_mul, Real.sqrt_mul two_pos.le, Real.sqrt_sq_eq_abs]
[GOAL]
x y : ℝ
hle : |x| ≤ |y|
⊢ Real.sqrt (y ^ 2 + y ^ 2) = Real.sqrt 2 * max |x| |y|
[PROOFSTEP]
rw [max_eq_right hle, ← two_mul, Real.sqrt_mul two_pos.le, Real.sqrt_sq_eq_abs]
[GOAL]
case neg
x y : ℝ
hle : ¬|x| ≤ |y|
⊢ Real.sqrt (x ^ 2 + y ^ 2) ≤ Real.sqrt 2 * max |x| |y|
[PROOFSTEP]
have hle' := le_of_not_le hle
[GOAL]
case neg
x y : ℝ
hle : ¬|x| ≤ |y|
hle' : |y| ≤ |x|
⊢ Real.sqrt (x ^ 2 + y ^ 2) ≤ Real.sqrt 2 * max |x| |y|
[PROOFSTEP]
rw [add_comm]
[GOAL]
case neg
x y : ℝ
hle : ¬|x| ≤ |y|
hle' : |y| ≤ |x|
⊢ Real.sqrt (y ^ 2 + x ^ 2) ≤ Real.sqrt 2 * max |x| |y|
[PROOFSTEP]
calc
  Real.sqrt (y ^ 2 + x ^ 2) ≤ Real.sqrt (x ^ 2 + x ^ 2) := Real.sqrt_le_sqrt (add_le_add_right (sq_le_sq.2 hle') _)
  _ = Real.sqrt 2 * max |x| |y| := by rw [max_eq_left hle', ← two_mul, Real.sqrt_mul two_pos.le, Real.sqrt_sq_eq_abs]
[GOAL]
x y : ℝ
hle : ¬|x| ≤ |y|
hle' : |y| ≤ |x|
⊢ Real.sqrt (x ^ 2 + x ^ 2) = Real.sqrt 2 * max |x| |y|
[PROOFSTEP]
rw [max_eq_left hle', ← two_mul, Real.sqrt_mul two_pos.le, Real.sqrt_sq_eq_abs]
[GOAL]
z : ℂ
hz : z = 0
⊢ |z.re / ↑abs z| ≤ 1
[PROOFSTEP]
simp [hz, zero_le_one]
[GOAL]
z : ℂ
hz : ¬z = 0
⊢ |z.re / ↑abs z| ≤ 1
[PROOFSTEP]
simp_rw [_root_.abs_div, abs_abs, div_le_iff (AbsoluteValue.pos Complex.abs hz), one_mul, abs_re_le_abs]
[GOAL]
z : ℂ
hz : z = 0
⊢ |z.im / ↑abs z| ≤ 1
[PROOFSTEP]
simp [hz, zero_le_one]
[GOAL]
z : ℂ
hz : ¬z = 0
⊢ |z.im / ↑abs z| ≤ 1
[PROOFSTEP]
simp_rw [_root_.abs_div, abs_abs, div_le_iff (AbsoluteValue.pos Complex.abs hz), one_mul, abs_im_le_abs]
[GOAL]
n : ℕ
⊢ ↑abs ↑n = ↑n
[PROOFSTEP]
rw [← ofReal_nat_cast, abs_of_nonneg (Nat.cast_nonneg n)]
[GOAL]
n : ℤ
⊢ |↑n| = ↑abs ↑n
[PROOFSTEP]
rw [← ofReal_int_cast, abs_ofReal]
[GOAL]
x : ℂ
⊢ ↑normSq x = ↑abs x ^ 2
[PROOFSTEP]
simp [abs, sq, abs_def, Real.mul_self_sqrt (normSq_nonneg _)]
[GOAL]
f : CauSeq ℂ ↑abs
ε : ℝ
ε0 : ε > 0
i : ℕ
H : ∀ (j : ℕ), j ≥ i → ↑abs (↑f j - ↑f i) < ε
j : ℕ
ij : j ≥ i
⊢ abs' ((fun n => (↑f n).re) j - (fun n => (↑f n).re) i) ≤ ↑abs (↑f j - ↑f i)
[PROOFSTEP]
simpa using abs_re_le_abs (f j - f i)
[GOAL]
f : CauSeq ℂ ↑abs
ε : ℝ
ε0 : ε > 0
i : ℕ
H : ∀ (j : ℕ), j ≥ i → ↑abs (↑f j - ↑f i) < ε
j : ℕ
ij : j ≥ i
⊢ abs' ((fun n => (↑f n).im) j - (fun n => (↑f n).im) i) ≤ ↑abs (↑f j - ↑f i)
[PROOFSTEP]
simpa using abs_im_le_abs (f j - f i)
[GOAL]
f : CauSeq ℂ ↑abs
ε : ℝ
ε0 : ε > 0
i : ℕ
H :
  ∀ (j : ℕ),
    j ≥ i →
      abs'
            (↑({ val := fun n => (↑f n).re, property := (_ : IsCauSeq abs' fun n => (↑f n).re) } -
                  CauSeq.const abs'
                    (CauSeq.lim { val := fun n => (↑f n).re, property := (_ : IsCauSeq abs' fun n => (↑f n).re) }))
              j) <
          ε / 2 ∧
        abs'
            (↑({ val := fun n => (↑f n).im, property := (_ : IsCauSeq abs' fun n => (↑f n).im) } -
                  CauSeq.const abs'
                    (CauSeq.lim { val := fun n => (↑f n).im, property := (_ : IsCauSeq abs' fun n => (↑f n).im) }))
              j) <
          ε / 2
j : ℕ
ij : j ≥ i
⊢ ↑abs (↑(f - CauSeq.const (↑abs) (limAux f)) j) < ε
[PROOFSTEP]
cases' H _ ij with H₁ H₂
[GOAL]
case intro
f : CauSeq ℂ ↑abs
ε : ℝ
ε0 : ε > 0
i : ℕ
H :
  ∀ (j : ℕ),
    j ≥ i →
      abs'
            (↑({ val := fun n => (↑f n).re, property := (_ : IsCauSeq abs' fun n => (↑f n).re) } -
                  CauSeq.const abs'
                    (CauSeq.lim { val := fun n => (↑f n).re, property := (_ : IsCauSeq abs' fun n => (↑f n).re) }))
              j) <
          ε / 2 ∧
        abs'
            (↑({ val := fun n => (↑f n).im, property := (_ : IsCauSeq abs' fun n => (↑f n).im) } -
                  CauSeq.const abs'
                    (CauSeq.lim { val := fun n => (↑f n).im, property := (_ : IsCauSeq abs' fun n => (↑f n).im) }))
              j) <
          ε / 2
j : ℕ
ij : j ≥ i
H₁ :
  abs'
      (↑({ val := fun n => (↑f n).re, property := (_ : IsCauSeq abs' fun n => (↑f n).re) } -
            CauSeq.const abs'
              (CauSeq.lim { val := fun n => (↑f n).re, property := (_ : IsCauSeq abs' fun n => (↑f n).re) }))
        j) <
    ε / 2
H₂ :
  abs'
      (↑({ val := fun n => (↑f n).im, property := (_ : IsCauSeq abs' fun n => (↑f n).im) } -
            CauSeq.const abs'
              (CauSeq.lim { val := fun n => (↑f n).im, property := (_ : IsCauSeq abs' fun n => (↑f n).im) }))
        j) <
    ε / 2
⊢ ↑abs (↑(f - CauSeq.const (↑abs) (limAux f)) j) < ε
[PROOFSTEP]
apply lt_of_le_of_lt (abs_le_abs_re_add_abs_im _)
[GOAL]
case intro
f : CauSeq ℂ ↑abs
ε : ℝ
ε0 : ε > 0
i : ℕ
H :
  ∀ (j : ℕ),
    j ≥ i →
      abs'
            (↑({ val := fun n => (↑f n).re, property := (_ : IsCauSeq abs' fun n => (↑f n).re) } -
                  CauSeq.const abs'
                    (CauSeq.lim { val := fun n => (↑f n).re, property := (_ : IsCauSeq abs' fun n => (↑f n).re) }))
              j) <
          ε / 2 ∧
        abs'
            (↑({ val := fun n => (↑f n).im, property := (_ : IsCauSeq abs' fun n => (↑f n).im) } -
                  CauSeq.const abs'
                    (CauSeq.lim { val := fun n => (↑f n).im, property := (_ : IsCauSeq abs' fun n => (↑f n).im) }))
              j) <
          ε / 2
j : ℕ
ij : j ≥ i
H₁ :
  abs'
      (↑({ val := fun n => (↑f n).re, property := (_ : IsCauSeq abs' fun n => (↑f n).re) } -
            CauSeq.const abs'
              (CauSeq.lim { val := fun n => (↑f n).re, property := (_ : IsCauSeq abs' fun n => (↑f n).re) }))
        j) <
    ε / 2
H₂ :
  abs'
      (↑({ val := fun n => (↑f n).im, property := (_ : IsCauSeq abs' fun n => (↑f n).im) } -
            CauSeq.const abs'
              (CauSeq.lim { val := fun n => (↑f n).im, property := (_ : IsCauSeq abs' fun n => (↑f n).im) }))
        j) <
    ε / 2
⊢ abs' (↑(f - CauSeq.const (↑abs) (limAux f)) j).re + abs' (↑(f - CauSeq.const (↑abs) (limAux f)) j).im < ε
[PROOFSTEP]
dsimp [limAux] at *
[GOAL]
case intro
f : CauSeq ℂ ↑abs
ε : ℝ
ε0 : ε > 0
i : ℕ
H :
  ∀ (j : ℕ),
    j ≥ i →
      abs' ((↑f j).re - CauSeq.lim { val := fun n => (↑f n).re, property := (_ : IsCauSeq abs' fun n => (↑f n).re) }) <
          ε / 2 ∧
        abs'
            ((↑f j).im - CauSeq.lim { val := fun n => (↑f n).im, property := (_ : IsCauSeq abs' fun n => (↑f n).im) }) <
          ε / 2
j : ℕ
ij : j ≥ i
H₁ :
  abs' ((↑f j).re - CauSeq.lim { val := fun n => (↑f n).re, property := (_ : IsCauSeq abs' fun n => (↑f n).re) }) <
    ε / 2
H₂ :
  abs' ((↑f j).im - CauSeq.lim { val := fun n => (↑f n).im, property := (_ : IsCauSeq abs' fun n => (↑f n).im) }) <
    ε / 2
⊢ abs' ((↑f j).re - CauSeq.lim (cauSeqRe f)) + abs' ((↑f j).im - CauSeq.lim (cauSeqIm f)) < ε
[PROOFSTEP]
have := add_lt_add H₁ H₂
[GOAL]
case intro
f : CauSeq ℂ ↑abs
ε : ℝ
ε0 : ε > 0
i : ℕ
H :
  ∀ (j : ℕ),
    j ≥ i →
      abs' ((↑f j).re - CauSeq.lim { val := fun n => (↑f n).re, property := (_ : IsCauSeq abs' fun n => (↑f n).re) }) <
          ε / 2 ∧
        abs'
            ((↑f j).im - CauSeq.lim { val := fun n => (↑f n).im, property := (_ : IsCauSeq abs' fun n => (↑f n).im) }) <
          ε / 2
j : ℕ
ij : j ≥ i
H₁ :
  abs' ((↑f j).re - CauSeq.lim { val := fun n => (↑f n).re, property := (_ : IsCauSeq abs' fun n => (↑f n).re) }) <
    ε / 2
H₂ :
  abs' ((↑f j).im - CauSeq.lim { val := fun n => (↑f n).im, property := (_ : IsCauSeq abs' fun n => (↑f n).im) }) <
    ε / 2
this :
  abs' ((↑f j).re - CauSeq.lim { val := fun n => (↑f n).re, property := (_ : IsCauSeq abs' fun n => (↑f n).re) }) +
      abs' ((↑f j).im - CauSeq.lim { val := fun n => (↑f n).im, property := (_ : IsCauSeq abs' fun n => (↑f n).im) }) <
    ε / 2 + ε / 2
⊢ abs' ((↑f j).re - CauSeq.lim (cauSeqRe f)) + abs' ((↑f j).im - CauSeq.lim (cauSeqIm f)) < ε
[PROOFSTEP]
rwa [add_halves] at this 
[GOAL]
f : CauSeq ℂ ↑abs
x✝ : ℕ
⊢ (↑(CauSeq.const (↑abs) (limAux f)) x✝).re =
    (↑(CauSeq.const (↑abs) (↑(CauSeq.lim (cauSeqRe f)) + ↑(CauSeq.lim (cauSeqIm f)) * I)) x✝).re
[PROOFSTEP]
simp [limAux, cauSeqRe, ofReal']
[GOAL]
f : CauSeq ℂ ↑abs
x✝ : ℕ
⊢ (↑(CauSeq.const (↑abs) (limAux f)) x✝).im =
    (↑(CauSeq.const (↑abs) (↑(CauSeq.lim (cauSeqRe f)) + ↑(CauSeq.lim (cauSeqIm f)) * I)) x✝).im
[PROOFSTEP]
simp [limAux, cauSeqIm, ofReal']
[GOAL]
f : CauSeq ℂ ↑abs
⊢ CauSeq.lim (cauSeqRe f) = (CauSeq.lim f).re
[PROOFSTEP]
rw [lim_eq_lim_im_add_lim_re]
[GOAL]
f : CauSeq ℂ ↑abs
⊢ CauSeq.lim (cauSeqRe f) = (↑(CauSeq.lim (cauSeqRe f)) + ↑(CauSeq.lim (cauSeqIm f)) * I).re
[PROOFSTEP]
simp [ofReal']
[GOAL]
f : CauSeq ℂ ↑abs
⊢ CauSeq.lim (cauSeqIm f) = (CauSeq.lim f).im
[PROOFSTEP]
rw [lim_eq_lim_im_add_lim_re]
[GOAL]
f : CauSeq ℂ ↑abs
⊢ CauSeq.lim (cauSeqIm f) = (↑(CauSeq.lim (cauSeqRe f)) + ↑(CauSeq.lim (cauSeqIm f)) * I).im
[PROOFSTEP]
simp [ofReal']
[GOAL]
f : CauSeq ℂ ↑abs
ε : ℝ
ε0 : ε > 0
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → ↑abs (↑f j - ↑f i) < ε
j : ℕ
hj : j ≥ i
⊢ ↑abs ((fun n => ↑(starRingEnd ℂ) (↑f n)) j - (fun n => ↑(starRingEnd ℂ) (↑f n)) i) < ε
[PROOFSTEP]
rw [← RingHom.map_sub, abs_conj]
[GOAL]
f : CauSeq ℂ ↑abs
ε : ℝ
ε0 : ε > 0
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → ↑abs (↑f j - ↑f i) < ε
j : ℕ
hj : j ≥ i
⊢ ↑abs (↑f j - ↑f i) < ε
[PROOFSTEP]
exact hi j hj
[GOAL]
f : CauSeq ℂ ↑abs
⊢ (CauSeq.lim (cauSeqConj f)).re = (↑(starRingEnd ℂ) (CauSeq.lim f)).re
[PROOFSTEP]
simp [cauSeqConj, (lim_re _).symm, cauSeqRe]
[GOAL]
f : CauSeq ℂ ↑abs
⊢ (CauSeq.lim (cauSeqConj f)).im = (↑(starRingEnd ℂ) (CauSeq.lim f)).im
[PROOFSTEP]
simp [cauSeqConj, (lim_im _).symm, cauSeqIm, (lim_neg _).symm]
[GOAL]
f : CauSeq ℂ ↑abs
⊢ CauSeq.lim { val := fun n => -(↑f n).im, property := (_ : (fun f => IsCauSeq abs' f) fun n => -(↑f n).im) } =
    CauSeq.lim (-{ val := fun n => (↑f n).im, property := (_ : IsCauSeq abs' fun n => (↑f n).im) })
[PROOFSTEP]
rfl
