awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Complex.Basic
Goal:
q : ℚ≥0
⊢ im (↑q : ℂ) = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
q : ℚ
⊢ re (↑q : ℂ) = (↑q : ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
q : ℚ
⊢ im (↑q : ℂ) = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
m : ℕ
s : Bool
e : ℕ
⊢ re (OfScientific.ofScientific m s e) = OfScientific.ofScientific m s e

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
m : ℕ
s : Bool
e : ℕ
⊢ im (OfScientific.ofScientific m s e) = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
a : re ↑0 = re 0
a₁ : im ↑0 = im 0
⊢ Eq (α := ℂ) (↑0) 0

Tactic:
ext
-- Module: Mathlib.Data.Complex.Basic
Goal:
⊢ re ↑0 = re 0

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
Goal:
⊢ im ↑0 = im 0

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
Goal:
x : ℕ
a : re ↑(x + 1) = (HAdd.hAdd (α := ℂ) (↑x) 1).re
a₁ : im ↑(x + 1) = (HAdd.hAdd (α := ℂ) (↑x) 1).im
⊢ ↑(x + 1) = HAdd.hAdd (α := ℂ) (↑x) 1

Tactic:
ext
-- Module: Mathlib.Data.Complex.Basic
Goal:
x : ℕ
⊢ re ↑(x + 1) = (HAdd.hAdd (α := ℂ) (↑x) 1).re

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
Goal:
x : ℕ
⊢ im ↑(x + 1) = (HAdd.hAdd (α := ℂ) (↑x) 1).im

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
Goal:
x : ℕ
a : re (IntCast.intCast (↑x : ℤ)) = re (↑x : ℂ)
a₁ : im (IntCast.intCast (↑x : ℤ)) = im (↑x : ℂ)
⊢ Eq (α := ℂ) (IntCast.intCast (↑x : ℤ)) (↑x : ℂ)

Tactic:
ext
-- Module: Mathlib.Data.Complex.Basic
Goal:
x : ℕ
⊢ re (IntCast.intCast (↑x : ℤ)) = re (↑x : ℂ)

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
Goal:
x : ℕ
⊢ im (IntCast.intCast (↑x : ℤ)) = im (↑x : ℂ)

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
Goal:
x : ℕ
a : re (IntCast.intCast (Int.negSucc x)) = re (-(↑(x + 1) : ℂ))
a₁ : im (IntCast.intCast (Int.negSucc x)) = im (-(↑(x + 1) : ℂ))
⊢ Eq (α := ℂ) (IntCast.intCast (Int.negSucc x)) (-(↑(x + 1) : ℂ))

Tactic:
ext
-- Module: Mathlib.Data.Complex.Basic
Goal:
x : ℕ
⊢ re (IntCast.intCast (Int.negSucc x)) = re (-(↑(x + 1) : ℂ))

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
Goal:
x : ℕ
⊢ im (IntCast.intCast (Int.negSucc x)) = im (-(↑(x + 1) : ℂ))

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
Goal:
a_1 b c : ℂ
a : (a_1 * b * c).re = (a_1 * (b * c)).re
a₁ : (a_1 * b * c).im = (a_1 * (b * c)).im
⊢ a_1 * b * c = a_1 * (b * c)

Tactic:
ext
-- Module: Mathlib.Data.Complex.Basic
Goal:
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)

Tactic:
ring
-- Module: Mathlib.Data.Complex.Basic
Goal:
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)

Tactic:
ring
-- Module: Mathlib.Data.Complex.Basic
Goal:
a_1 : ℂ
a : (1 * a_1).re = a_1.re
a₁ : (1 * a_1).im = a_1.im
⊢ 1 * a_1 = a_1

Tactic:
ext
-- Module: Mathlib.Data.Complex.Basic
Goal:
a : ℂ
⊢ (1 * a).re = a.re

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
Goal:
a : ℂ
⊢ (1 * a).im = a.im

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
Goal:
a_1 : ℂ
a : (a_1 * 1).re = a_1.re
a₁ : (a_1 * 1).im = a_1.im
⊢ a_1 * 1 = a_1

Tactic:
ext
-- Module: Mathlib.Data.Complex.Basic
Goal:
a : ℂ
⊢ (a * 1).re = a.re

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
Goal:
a : ℂ
⊢ (a * 1).im = a.im

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
Goal:
a_1 : ℂ
a : (0 * a_1).re = re 0
a₁ : (0 * a_1).im = im 0
⊢ 0 * a_1 = 0

Tactic:
ext
-- Module: Mathlib.Data.Complex.Basic
Goal:
a : ℂ
⊢ (0 * a).re = re 0

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
Goal:
a : ℂ
⊢ (0 * a).im = im 0

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
Goal:
a_1 : ℂ
a : (a_1 * 0).re = re 0
a₁ : (a_1 * 0).im = im 0
⊢ a_1 * 0 = 0

Tactic:
ext
-- Module: Mathlib.Data.Complex.Basic
Goal:
a : ℂ
⊢ (a * 0).re = re 0

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
Goal:
a : ℂ
⊢ (a * 0).im = im 0

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
Goal:
a_1 b c : ℂ
a : (a_1 * (b + c)).re = (a_1 * b + a_1 * c).re
a₁ : (a_1 * (b + c)).im = (a_1 * b + a_1 * c).im
⊢ a_1 * (b + c) = a_1 * b + a_1 * c

Tactic:
ext
-- Module: Mathlib.Data.Complex.Basic
Goal:
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)

Tactic:
ring
-- Module: Mathlib.Data.Complex.Basic
Goal:
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)

Tactic:
ring
-- Module: Mathlib.Data.Complex.Basic
Goal:
a_1 b c : ℂ
a : ((a_1 + b) * c).re = (a_1 * c + b * c).re
a₁ : ((a_1 + b) * c).im = (a_1 * c + b * c).im
⊢ (a_1 + b) * c = a_1 * c + b * c

Tactic:
ext
-- Module: Mathlib.Data.Complex.Basic
Goal:
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)

Tactic:
ring
-- Module: Mathlib.Data.Complex.Basic
Goal:
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)

Tactic:
ring
-- Module: Mathlib.Data.Complex.Basic
Goal:
a_1 b : ℂ
a : (a_1 * b).re = (b * a_1).re
a₁ : (a_1 * b).im = (b * a_1).im
⊢ a_1 * b = b * a_1

Tactic:
ext
-- Module: Mathlib.Data.Complex.Basic
Goal:
a b : ℂ
⊢ a.re * b.re - a.im * b.im = b.re * a.re - b.im * a.im

Tactic:
ring
-- Module: Mathlib.Data.Complex.Basic
Goal:
a b : ℂ
⊢ a.re * b.im + a.im * b.re = b.re * a.im + b.im * a.re

Tactic:
ring
-- Module: Mathlib.Data.Complex.Basic
Goal:
⊢ Ring ℂ

Tactic:
infer_instance
-- Module: Mathlib.Data.Complex.Basic
Goal:
⊢ (⇑reAddGroupHom : (a : ℂ) → ℝ) = re

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
⊢ (⇑imAddGroupHom : (a : ℂ) → ℝ) = im

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
n : ℕ
z : ℂ
⊢ (n • z).re = n • z.re

Tactic:
smul_re ..

Premises used: Complex.smul_re
-- Module: Mathlib.Data.Complex.Basic
Goal:
n : ℕ
z : ℂ
⊢ (n • z).im = n • z.im

Tactic:
smul_im ..

Premises used: Complex.smul_im
-- Module: Mathlib.Data.Complex.Basic
Goal:
n : ℤ
z : ℂ
⊢ (n • z).re = n • z.re

Tactic:
smul_re ..

Premises used: Complex.smul_re
-- Module: Mathlib.Data.Complex.Basic
Goal:
n : ℤ
z : ℂ
⊢ (n • z).im = n • z.im

Tactic:
smul_im ..

Premises used: Complex.smul_im
-- Module: Mathlib.Data.Complex.Basic
Goal:
q : ℚ≥0
z : ℂ
⊢ (q • z).re = q • z.re

Tactic:
smul_re ..

Premises used: Complex.smul_re
-- Module: Mathlib.Data.Complex.Basic
Goal:
q : ℚ≥0
z : ℂ
⊢ (q • z).im = q • z.im

Tactic:
smul_im ..

Premises used: Complex.smul_im
-- Module: Mathlib.Data.Complex.Basic
Goal:
q : ℚ
z : ℂ
⊢ (q • z).re = q • z.re

Tactic:
smul_re ..

Premises used: Complex.smul_re
-- Module: Mathlib.Data.Complex.Basic
Goal:
q : ℚ
z : ℂ
⊢ (q • z).im = q • z.im

Tactic:
smul_im ..

Premises used: Complex.smul_im
-- Module: Mathlib.Data.Complex.Basic
Goal:
n : ℕ
r : ℝ
⊢ (↑(n • r) : ℂ) = n • (↑r : ℂ)

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
Goal:
n : ℤ
r : ℝ
⊢ (↑(n • r) : ℂ) = n • (↑r : ℂ)

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
Goal:
x : ℂ
⊢ (fun (z : ℂ) ↦ { re := z.re, im := -z.im : ℂ }) ((fun (z : ℂ) ↦ { re := z.re, im := -z.im : ℂ }) x) = x

Tactic:
simp only [eta, neg_neg]

Premises used: Complex.eta, neg_neg
-- Module: Mathlib.Data.Complex.Basic
Goal:
a b : ℂ
a₁ :
  { re := (a * b).re, im := -(a * b).im : ℂ }.re =
    ({ re := b.re, im := -b.im : ℂ } * { re := a.re, im := -a.im : ℂ }).re
a₂ :
  { re := (a * b).re, im := -(a * b).im : ℂ }.im =
    ({ re := b.re, im := -b.im : ℂ } * { re := a.re, im := -a.im : ℂ }).im
⊢ { re := (a * b).re, im := -(a * b).im : ℂ } = { re := b.re, im := -b.im : ℂ } * { re := a.re, im := -a.im : ℂ }

Tactic:
ext
-- Module: Mathlib.Data.Complex.Basic
Goal:
a b : ℂ
a₁ : a.re * b.re - a.im * b.im = b.re * a.re - b.im * a.im
⊢ { re := (a * b).re, im := -(a * b).im : ℂ }.re =
    ({ re := b.re, im := -b.im : ℂ } * { re := a.re, im := -a.im : ℂ }).re

Tactic:
simp [add_comm]

Premises used: add_comm
-- Module: Mathlib.Data.Complex.Basic
Goal:
a b : ℂ
a₁ : -(a.re * b.im) + -(a.im * b.re) = -(b.re * a.im) + -(b.im * a.re)
⊢ { re := (a * b).re, im := -(a * b).im : ℂ }.im =
    ({ re := b.re, im := -b.im : ℂ } * { re := a.re, im := -a.im : ℂ }).im

Tactic:
simp [add_comm]

Premises used: add_comm
-- Module: Mathlib.Data.Complex.Basic
Goal:
a b : ℂ
⊢ -(a.re * b.im) + -(a.im * b.re) = -(b.re * a.im) + -(b.im * a.re)

Tactic:
ring
-- Module: Mathlib.Data.Complex.Basic
Goal:
a b : ℂ
a₁ :
  { re := (a + b).re, im := -(a + b).im : ℂ }.re =
    ({ re := a.re, im := -a.im : ℂ } + { re := b.re, im := -b.im : ℂ }).re
a₂ :
  { re := (a + b).re, im := -(a + b).im : ℂ }.im =
    ({ re := a.re, im := -a.im : ℂ } + { re := b.re, im := -b.im : ℂ }).im
⊢ { re := (a + b).re, im := -(a + b).im : ℂ } = { re := a.re, im := -a.im : ℂ } + { re := b.re, im := -b.im : ℂ }

Tactic:
ext
-- Module: Mathlib.Data.Complex.Basic
Goal:
a b : ℂ
⊢ { re := (a + b).re, im := -(a + b).im : ℂ }.re =
    ({ re := a.re, im := -a.im : ℂ } + { re := b.re, im := -b.im : ℂ }).re

Tactic:
simp [add_comm]

Premises used: add_comm
-- Module: Mathlib.Data.Complex.Basic
Goal:
a b : ℂ
⊢ { re := (a + b).re, im := -(a + b).im : ℂ }.im =
    ({ re := a.re, im := -a.im : ℂ } + { re := b.re, im := -b.im : ℂ }).im

Tactic:
simp [add_comm]

Premises used: add_comm
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
⊢ re ((starRingEnd ℂ : (a : ℂ) → ℂ) z) = z.re

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
⊢ im ((starRingEnd ℂ : (a : ℂ) → ℂ) z) = -z.im

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
r : ℝ
⊢ re ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑r : ℂ)) = (↑r : ℂ).re ∧ im ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑r : ℂ)) = (↑r : ℂ).im

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
Goal:
⊢ re ((starRingEnd ℂ : (a : ℂ) → ℂ) I) = (-I).re ∧ im ((starRingEnd ℂ : (a : ℂ) → ℂ) I) = (-I).im

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
Goal:
n : ℕ
⊢ Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑n : ℂ) : ℂ) ((↑n : ℂ) : ℂ)

Tactic:
map_natCast _ _

Premises used: map_natCast
-- Module: Mathlib.Data.Complex.Basic
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (OfNat.ofNat n) : ℂ) (OfNat.ofNat n : ℂ)

Tactic:
map_ofNat _ _

Premises used: map_ofNat
-- Module: Mathlib.Data.Complex.Basic
Goal:
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) (-I) = I

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
h_1 : ∃ (r : ℝ), z = (↑r : ℂ)
h : ℝ
e : z = (↑h : ℂ)
rw : (starRingEnd ℂ : (a : ℂ) → ℂ) (↑h : ℂ) = (↑h : ℂ)
rw₁ rw₂ : (↑h : ℂ) = (↑h : ℂ)
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) z = z

Tactic:
rw [e, conj_ofReal]

Premises used: Complex.conj_ofReal
-- Module: Mathlib.Data.Complex.Basic
Goal:
r : ℝ
⊢ (↑(↑r : ℂ).re : ℂ) = (↑r : ℂ)

Tactic:
simp [ofReal]

Premises used: Complex.ofReal
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) z = z ↔ z.im = 0

Tactic:
⟨fun h => add_self_eq_zero.mp (neg_eq_iff_add_eq_zero.mp (congr_arg im h)), fun h =>
    ext rfl (neg_eq_iff_add_eq_zero.mpr (add_self_eq_zero.mpr h))⟩

Premises used: Iff.mpr, neg_eq_iff_add_eq_zero, Complex.im, add_self_eq_zero, congr_arg, Iff.intro, Iff.mp, Complex.ext, rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
⊢ Eq (α := ℂ → ℂ) star (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
⊢ re 0 * re 0 + im 0 * im 0 = 0

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
Goal:
⊢ re 1 * re 1 + im 1 * im 1 = 1

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
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)

Tactic:
ring
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
⊢ (normSq : (a : ℂ) → ℝ) z = z.re * z.re + z.im * z.im

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
r : ℝ
⊢ (normSq : (a : ℂ) → ℝ) (↑r : ℂ) = r * r

Tactic:
simp [normSq, ofReal]

Premises used: Complex.normSq, Complex.ofReal
-- Module: Mathlib.Data.Complex.Basic
Goal:
n : ℕ
⊢ (normSq : (a : ℂ) → ℝ) (↑n : ℂ) = HMul.hMul (α := ℝ) (↑n : ℝ) (↑n : ℝ)

Tactic:
normSq_ofReal _

Premises used: Complex.normSq_ofReal
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℤ
⊢ (normSq : (a : ℂ) → ℝ) (↑z : ℂ) = HMul.hMul (α := ℝ) (↑z : ℝ) (↑z : ℝ)

Tactic:
normSq_ofReal _

Premises used: Complex.normSq_ofReal
-- Module: Mathlib.Data.Complex.Basic
Goal:
q : ℚ
⊢ (normSq : (a : ℂ) → ℝ) (↑q : ℂ) = HMul.hMul (α := ℝ) (↑q : ℝ) (↑q : ℝ)

Tactic:
normSq_ofReal _

Premises used: Complex.normSq_ofReal
-- Module: Mathlib.Data.Complex.Basic
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ (normSq : (a : ℂ) → ℝ) (OfNat.ofNat n) = HMul.hMul (α := ℝ) (OfNat.ofNat n) (OfNat.ofNat n)

Tactic:
normSq_natCast _

Premises used: Complex.normSq_natCast
-- Module: Mathlib.Data.Complex.Basic
Goal:
x y : ℝ
⊢ (normSq : (a : ℂ) → ℝ) { re := x, im := y : ℂ } = x * x + y * y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
x y : ℝ
rw : (normSq : (a : ℂ) → ℝ) { re := x, im := y : ℂ } = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
rw₁ : x * x + y * y = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
rw₂ : x * x + y * y = x * x + HPow.hPow (β := ℕ) y 2
rw₃ rw₄ : x * x + y * y = x * x + y * y
⊢ (normSq : (a : ℂ) → ℝ) ((↑x : ℂ) + (↑y : ℂ) * I) = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2

Tactic:
rw [← mk_eq_add_mul_I, normSq_mk, sq, sq]

Premises used: Complex.mk_eq_add_mul_I, Complex.normSq_mk, sq
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
a : (↑((normSq : (a : ℂ) → ℝ) z) : ℂ).re = (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) z).re
a₁ : (↑((normSq : (a : ℂ) → ℝ) z) : ℂ).im = (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) z).im
⊢ (↑((normSq : (a : ℂ) → ℝ) z) : ℂ) = HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) z

Tactic:
ext
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
⊢ (↑((normSq : (a : ℂ) → ℝ) z) : ℂ).re = (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) z).re

Tactic:
simp [normSq, mul_comm, ofReal]

Premises used: Complex.normSq, Complex.ofReal, mul_comm
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
⊢ (↑((normSq : (a : ℂ) → ℝ) z) : ℂ).im = (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) z).im

Tactic:
simp [normSq, mul_comm, ofReal]

Premises used: Complex.normSq, Complex.ofReal, mul_comm
-- Module: Mathlib.Data.Complex.Basic
Goal:
⊢ Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) 0 : ℝ) (0 : ℝ)

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
Goal:
⊢ Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) 1 : ℝ) (1 : ℝ)

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
Goal:
⊢ Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) I : ℝ) (1 : ℝ)

Tactic:
simp [normSq]

Premises used: Complex.normSq
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
⊢ LE.le (α := ℝ) (0 : ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ)

Tactic:
add_nonneg (mul_self_nonneg _) (mul_self_nonneg _)

Premises used: mul_self_nonneg, add_nonneg
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
⊢ Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ) (0 : ℝ) ↔ z = 0

Tactic:
⟨fun h =>
    ext (eq_zero_of_mul_self_add_mul_self_eq_zero h)
      (eq_zero_of_mul_self_add_mul_self_eq_zero <| (add_comm _ _).trans h),
    fun h => h.symm ▸ normSq_zero⟩

Premises used: HMul.hMul, Complex.im, Eq.rec, Complex.normSq_zero, add_comm, Complex.re, Iff.intro, Complex.ext, eq_zero_of_mul_self_add_mul_self_eq_zero, Eq.symm, Eq.trans
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
⊢ LT.lt (α := ℝ) (0 : ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ) ↔ z ≠ 0

Tactic:
(normSq_nonneg z).lt_iff_ne.trans <| not_congr (eq_comm.trans normSq_eq_zero)

Premises used: eq_comm, Complex.normSq_nonneg, LE.le.lt_iff_ne, Iff.trans, not_congr, Complex.normSq_eq_zero
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
⊢ Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (-z) : ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ)

Tactic:
simp [normSq]

Premises used: Complex.normSq
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
⊢ Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) : ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ)

Tactic:
simp [normSq]

Premises used: Complex.normSq
-- Module: Mathlib.Data.Complex.Basic
Goal:
z w : ℂ
⊢ (normSq : (a : ℂ) → ℝ) (z * w) =
    HMul.hMul (α := ℝ) (β := ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ) ((normSq : (a : ℂ) → ℝ) w : ℝ)

Tactic:
normSq.map_mul z w

Premises used: Complex.normSq, MonoidWithZeroHom.map_mul
-- Module: Mathlib.Data.Complex.Basic
Goal:
z w : ℂ
simp :
  (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)
⊢ (normSq : (a : ℂ) → ℝ) (z + w) =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ) ((normSq : (a : ℂ) → ℝ) w : ℝ) +
      2 * (HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ)).re

Tactic:
simp [normSq]

Premises used: Complex.normSq
-- Module: Mathlib.Data.Complex.Basic
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)

Tactic:
ring
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
⊢ z.re * z.re ≤ (normSq : (a : ℂ) → ℝ) z

Tactic:
le_add_of_nonneg_right (mul_self_nonneg _)

Premises used: mul_self_nonneg, le_add_of_nonneg_right
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
⊢ z.im * z.im ≤ (normSq : (a : ℂ) → ℝ) z

Tactic:
le_add_of_nonneg_left (mul_self_nonneg _)

Premises used: mul_self_nonneg, le_add_of_nonneg_left
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
⊢ (HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ)).re = (↑((normSq : (a : ℂ) → ℝ) z) : ℂ).re ∧
    (HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ)).im = (↑((normSq : (a : ℂ) → ℝ) z) : ℂ).im

Tactic:
simp [normSq, mul_comm, sub_eq_neg_add, add_comm, ofReal]

Premises used: sub_eq_neg_add, Complex.normSq, Complex.ofReal, add_comm, mul_comm
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
⊢ (HAdd.hAdd (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ)).re = (↑(2 * z.re) : ℂ).re ∧
    (HAdd.hAdd (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ)).im = (↑(2 * z.re) : ℂ).im

Tactic:
simp [two_mul, ofReal]

Premises used: two_mul, Complex.ofReal
-- Module: Mathlib.Data.Complex.Basic
Goal:
r : ℝ
⊢ (ofRealHom : (a : ℝ) → ℂ) r = (↑r : ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
α : Type u_1
f g : α → ℝ
⊢ ofReal ∘ (f + g) = ofReal ∘ f + ofReal ∘ g

Tactic:
map_comp_add ofRealHom ..

Premises used: map_comp_add, Complex.ofRealHom
-- Module: Mathlib.Data.Complex.Basic
Goal:
α : Type u_1
f g : α → ℝ
⊢ ofReal ∘ (f - g) = ofReal ∘ f - ofReal ∘ g

Tactic:
map_comp_sub ofRealHom ..

Premises used: map_comp_sub, Complex.ofRealHom
-- Module: Mathlib.Data.Complex.Basic
Goal:
α : Type u_1
f : α → ℝ
⊢ ofReal ∘ (-f) = -ofReal ∘ f

Tactic:
map_comp_neg ofRealHom _

Premises used: Complex.ofRealHom, map_comp_neg
-- Module: Mathlib.Data.Complex.Basic
Goal:
α : Type u_1
n : ℕ
f : α → ℝ
⊢ ofReal ∘ (n • f) = n • ofReal ∘ f

Tactic:
map_comp_nsmul ofRealHom ..

Premises used: map_comp_nsmul, Complex.ofRealHom
-- Module: Mathlib.Data.Complex.Basic
Goal:
α : Type u_1
n : ℤ
f : α → ℝ
⊢ ofReal ∘ (n • f) = n • ofReal ∘ f

Tactic:
map_comp_zsmul ofRealHom ..

Premises used: Complex.ofRealHom, map_comp_zsmul
-- Module: Mathlib.Data.Complex.Basic
Goal:
α : Type u_1
f g : α → ℝ
⊢ ofReal ∘ (f * g) = ofReal ∘ f * ofReal ∘ g

Tactic:
map_comp_mul ofRealHom ..

Premises used: Complex.ofRealHom, map_comp_mul
-- Module: Mathlib.Data.Complex.Basic
Goal:
α : Type u_1
f : α → ℝ
n : ℕ
⊢ ofReal ∘ (f ^ n) = ofReal ∘ f ^ n

Tactic:
map_comp_pow ofRealHom ..

Premises used: map_comp_pow, Complex.ofRealHom
-- Module: Mathlib.Data.Complex.Basic
Goal:
rw : I * I = -1
rw₁ rw₂ : Eq (α := ℂ) (-1) (-1)
⊢ HPow.hPow (β := ℕ) I 2 = -1

Tactic:
rw [sq, I_mul_I]

Premises used: sq, Complex.I_mul_I
-- Module: Mathlib.Data.Complex.Basic
Goal:
rw : HPow.hPow (β := ℕ) I 2 * I = -I
rw₁ : -1 * I = -I
rw₂ rw₃ : -I = -I
⊢ HPow.hPow (β := ℕ) I 3 = -I

Tactic:
rw [pow_succ, I_sq, neg_one_mul]

Premises used: pow_succ, neg_one_mul, Complex.I_sq
-- Module: Mathlib.Data.Complex.Basic
Goal:
⊢ 4 = HMul.hMul (α := ℕ) 2 2

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
Goal:
rw : 4 = HMul.hMul (α := ℕ) 2 2
rw₁ : I ^ HMul.hMul (α := ℕ) 2 2 = 1
rw₂ : HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) I 2) 2 = 1
rw₃ : HPow.hPow (α := ℂ) (β := ℕ) (-1) 2 = 1
rw₄ rw₅ : Eq (α := ℂ) 1 1
⊢ HPow.hPow (β := ℕ) I 4 = 1

Tactic:
rw [(by simp : 4 = 2 * 2), pow_mul, I_sq, neg_one_sq]

Premises used: neg_one_sq, pow_mul, Complex.I_sq
-- Module: Mathlib.Data.Complex.Basic
Goal:
n : ℕ
rw : I ^ (4 * (n / 4) + n % 4)
| I ^ n

Tactic:
rw [← Nat.div_add_mod n 4]

Premises used: Nat.div_add_mod, OfNat.ofNat
-- Module: Mathlib.Data.Complex.Basic
Goal:
n : ℕ
conv_lhs : I ^ (4 * (n / 4) + n % 4) = I ^ (n % 4)
⊢ I ^ n = I ^ (n % 4)

Tactic:
conv_lhs => rw [← Nat.div_add_mod n 4]

Premises used: Nat.div_add_mod, OfNat.ofNat
-- Module: Mathlib.Data.Complex.Basic
Goal:
n : ℕ
⊢ I ^ (4 * (n / 4) + n % 4) = I ^ (n % 4)

Tactic:
simp [pow_add, pow_mul, I_pow_four]

Premises used: pow_add, Complex.I_pow_four, pow_mul
-- Module: Mathlib.Data.Complex.Basic
Goal:
z w : ℂ
⊢ (z - w).re = z.re - w.re

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
z w : ℂ
⊢ (z - w).im = z.im - w.im

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
r s : ℝ
⊢ (↑(r - s) : ℂ).re = ((↑r : ℂ) - (↑s : ℂ)).re ∧ (↑(r - s) : ℂ).im = ((↑r : ℂ) - (↑s : ℂ)).im

Tactic:
simp [ofReal]

Premises used: Complex.ofReal
-- Module: Mathlib.Data.Complex.Basic
Goal:
r : ℝ
n : ℕ
zero : (↑(HPow.hPow (β := ℕ) r 0) : ℂ) = HPow.hPow (β := ℕ) (↑r : ℂ) 0
succ : ∀ (n : ℕ), (↑(r ^ n) : ℂ) = (↑r : ℂ) ^ n → (↑(r ^ (n + 1)) : ℂ) = (↑r : ℂ) ^ (n + 1)
⊢ (↑(r ^ n) : ℂ) = (↑r : ℂ) ^ n

Tactic:
induction n
-- Module: Mathlib.Data.Complex.Basic
Goal:
r : ℝ
⊢ (↑(HPow.hPow (β := ℕ) r 0) : ℂ) = HPow.hPow (β := ℕ) (↑r : ℂ) 0

Tactic:
simp [*, ofReal_mul, pow_succ]

Premises used: pow_succ, Complex.ofReal_mul
-- Module: Mathlib.Data.Complex.Basic
Goal:
r : ℝ
n : ℕ
h : (↑(r ^ n) : ℂ) = (↑r : ℂ) ^ n
⊢ (↑(r ^ (n + 1)) : ℂ) = (↑r : ℂ) ^ (n + 1)

Tactic:
simp [*, ofReal_mul, pow_succ]

Premises used: pow_succ, Complex.ofReal_mul
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
⊢ (HSub.hSub (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ)).re = ((↑(2 * z.im) : ℂ) * I).re ∧
    (HSub.hSub (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ)).im = ((↑(2 * z.im) : ℂ) * I).im

Tactic:
simp [two_mul, sub_eq_add_neg, ofReal]

Premises used: sub_eq_add_neg, two_mul, Complex.ofReal
-- Module: Mathlib.Data.Complex.Basic
Goal:
z w : ℂ
rw :
  HAdd.hAdd (α := ℝ) (β := ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ) ((normSq : (a : ℂ) → ℝ) (-w) : ℝ) +
      2 * (HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) (-w) : ℂ)).re =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ) ((normSq : (a : ℂ) → ℝ) w : ℝ) -
      2 * (HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ)).re
⊢ (normSq : (a : ℂ) → ℝ) (z - w) =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ) ((normSq : (a : ℂ) → ℝ) w : ℝ) -
      2 * (HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ)).re

Tactic:
rw [sub_eq_add_neg, normSq_add]

Premises used: sub_eq_add_neg, Complex.normSq_add
-- Module: Mathlib.Data.Complex.Basic
Goal:
z w : ℂ
simp :
  HAdd.hAdd (α := ℝ) (β := ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ) ((normSq : (a : ℂ) → ℝ) w : ℝ) +
      -(2 * (HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ)).re) =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ) ((normSq : (a : ℂ) → ℝ) w : ℝ) -
      2 * (HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ)).re
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ) ((normSq : (a : ℂ) → ℝ) (-w) : ℝ) +
      2 * (HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) (-w) : ℂ)).re =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ) ((normSq : (a : ℂ) → ℝ) w : ℝ) -
      2 * (HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ)).re

Tactic:
simp only [map_neg, mul_neg, neg_re, normSq_neg]

Premises used: map_neg, Complex.neg_re, Complex.normSq_neg, mul_neg