awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
n : ℕ
x : ℂ
a : ((n + 1) • x).re = (n • x + x).re
⊢ (n + 1) • x = n • x + x
have a₁ : ((n + 1) • x).im = (n • x + x).im
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
n : ℕ
x : ℂ
⊢ ((n + 1) • x).re = (n • x + x).re
have a : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x.re = (↑n : ℝ) * x.re + x.re
Tactic: simp [smul_re, smul_im]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
n : ℕ
x : ℂ
⊢ ((n + 1) • x).im = (n • x + x).im
have a : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x.im = (↑n : ℝ) * x.im + x.im
Tactic: simp [smul_re, smul_im]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
a : ℂ
⊢ HSMul.hSMul (α := ℤ) 0 a = 0
have a : (HSMul.hSMul (α := ℤ) 0 a).re = re 0
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
a_1 : ℂ
a : (HSMul.hSMul (α := ℤ) 0 a_1).re = re 0
⊢ HSMul.hSMul (α := ℤ) 0 a_1 = 0
have a₁ : (HSMul.hSMul (α := ℤ) 0 a_1).im = im 0
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
n : ℕ
a : ℂ
⊢ HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) a = HSMul.hSMul (α := ℤ) (↑n : ℤ) a + a
have a : (HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) a).re = (HSMul.hSMul (α := ℤ) (↑n : ℤ) a + a).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
n : ℕ
a_1 : ℂ
a : (HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) a_1).re = (HSMul.hSMul (α := ℤ) (↑n : ℤ) a_1 + a_1).re
⊢ HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) a_1 = HSMul.hSMul (α := ℤ) (↑n : ℤ) a_1 + a_1
have a₁ : (HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) a_1).im = (HSMul.hSMul (α := ℤ) (↑n : ℤ) a_1 + a_1).im
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
n : ℕ
a : ℂ
⊢ (HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) a).re = (HSMul.hSMul (α := ℤ) (↑n : ℤ) a + a).re
have a : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * a.re = (↑n : ℝ) * a.re + a.re
Tactic: simp [smul_re, smul_im]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
n : ℕ
a : ℂ
⊢ (HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) a).im = (HSMul.hSMul (α := ℤ) (↑n : ℤ) a + a).im
have a : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * a.im = (↑n : ℝ) * a.im + a.im
Tactic: simp [smul_re, smul_im]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
n : ℕ
a : ℂ
⊢ Int.negSucc n • a = -HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) a
have a : (Int.negSucc n • a).re = (-HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) a).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
n : ℕ
a_1 : ℂ
a : (Int.negSucc n • a_1).re = (-HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) a_1).re
⊢ Int.negSucc n • a_1 = -HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) a_1
have a₁ : (Int.negSucc n • a_1).im = (-HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) a_1).im
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
n : ℕ
a : ℂ
⊢ (Int.negSucc n • a).re = (-HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) a).re
have a : HAdd.hAdd (α := ℝ) (-1) (-(↑n : ℝ)) * a.re = -(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * a.re)
Tactic: simp [smul_re, smul_im]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
n : ℕ
a : ℂ
⊢ (Int.negSucc n • a).im = (-HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) a).im
have a : HAdd.hAdd (α := ℝ) (-1) (-(↑n : ℝ)) * a.im = -(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * a.im)
Tactic: simp [smul_re, smul_im]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
a : ℂ
⊢ -a + a = 0
have a : (-a + a).re = re 0
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
a_1 : ℂ
a : (-a_1 + a_1).re = re 0
⊢ -a_1 + a_1 = 0
have a₁ : (-a_1 + a_1).im = im 0
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
a b : ℂ
⊢ a + b = b + a
have a : (a + b).re = (b + a).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
a_1 b : ℂ
a : (a_1 + b).re = (b + a_1).re
⊢ a_1 + b = b + a_1
have a₁ : (a_1 + b).im = (b + a_1).im
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
⊢ Eq (α := ℂ) (↑0) 0
have a : re ↑0 = re 0
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
a : re ↑0 = re 0
⊢ Eq (α := ℂ) (↑0) 0
have a₁ : im ↑0 = im 0
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
x : ℕ
⊢ ↑(x + 1) = HAdd.hAdd (α := ℂ) (↑x) 1
have a : re ↑(x + 1) = (HAdd.hAdd (α := ℂ) (↑x) 1).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
x : ℕ
a : re ↑(x + 1) = (HAdd.hAdd (α := ℂ) (↑x) 1).re
⊢ ↑(x + 1) = HAdd.hAdd (α := ℂ) (↑x) 1
have a₁ : im ↑(x + 1) = (HAdd.hAdd (α := ℂ) (↑x) 1).im
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
x : ℕ
⊢ Eq (α := ℂ) (IntCast.intCast (↑x : ℤ)) (↑x : ℂ)
have a : re (IntCast.intCast (↑x : ℤ)) = re (↑x : ℂ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
x : ℕ
a : re (IntCast.intCast (↑x : ℤ)) = re (↑x : ℂ)
⊢ Eq (α := ℂ) (IntCast.intCast (↑x : ℤ)) (↑x : ℂ)
have a₁ : im (IntCast.intCast (↑x : ℤ)) = im (↑x : ℂ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
x : ℕ
⊢ Eq (α := ℂ) (IntCast.intCast (Int.negSucc x)) (-(↑(x + 1) : ℂ))
have a : re (IntCast.intCast (Int.negSucc x)) = re (-(↑(x + 1) : ℂ))
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
x : ℕ
a : re (IntCast.intCast (Int.negSucc x)) = re (-(↑(x + 1) : ℂ))
⊢ Eq (α := ℂ) (IntCast.intCast (Int.negSucc x)) (-(↑(x + 1) : ℂ))
have a₁ : im (IntCast.intCast (Int.negSucc x)) = im (-(↑(x + 1) : ℂ))
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
a b c : ℂ
⊢ a * b * c = a * (b * c)
have a : (a * b * c).re = (a * (b * c)).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
a_1 b c : ℂ
a : (a_1 * b * c).re = (a_1 * (b * c)).re
⊢ a_1 * b * c = a_1 * (b * c)
have a₁ : (a_1 * b * c).im = (a_1 * (b * c)).im
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
a : ℂ
⊢ 1 * a = a
have a : (1 * a).re = a.re
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
a_1 : ℂ
a : (1 * a_1).re = a_1.re
⊢ 1 * a_1 = a_1
have a₁ : (1 * a_1).im = a_1.im
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
a : ℂ
⊢ a * 1 = a
have a : (a * 1).re = a.re
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
a_1 : ℂ
a : (a_1 * 1).re = a_1.re
⊢ a_1 * 1 = a_1
have a₁ : (a_1 * 1).im = a_1.im
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
a : ℂ
⊢ 0 * a = 0
have a : (0 * a).re = re 0
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
a_1 : ℂ
a : (0 * a_1).re = re 0
⊢ 0 * a_1 = 0
have a₁ : (0 * a_1).im = im 0
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
a : ℂ
⊢ a * 0 = 0
have a : (a * 0).re = re 0
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
a_1 : ℂ
a : (a_1 * 0).re = re 0
⊢ a_1 * 0 = 0
have a₁ : (a_1 * 0).im = im 0
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
a b c : ℂ
⊢ a * (b + c) = a * b + a * c
have a : (a * (b + c)).re = (a * b + a * c).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
a_1 b c : ℂ
a : (a_1 * (b + c)).re = (a_1 * b + a_1 * c).re
⊢ a_1 * (b + c) = a_1 * b + a_1 * c
have a₁ : (a_1 * (b + c)).im = (a_1 * b + a_1 * c).im
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
a b c : ℂ
⊢ (a + b) * c = a * c + b * c
have a : ((a + b) * c).re = (a * c + b * c).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
a_1 b c : ℂ
a : ((a_1 + b) * c).re = (a_1 * c + b * c).re
⊢ (a_1 + b) * c = a_1 * c + b * c
have a₁ : ((a_1 + b) * c).im = (a_1 * c + b * c).im
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
a b : ℂ
⊢ a * b = b * a
have a : (a * b).re = (b * a).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
a_1 b : ℂ
a : (a_1 * b).re = (b * a_1).re
⊢ a_1 * b = b * a_1
have a₁ : (a_1 * b).im = (b * a_1).im
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
a b : ℂ
⊢ { re := (a * b).re, im := -(a * b).im : ℂ } = { re := b.re, im := -b.im : ℂ } * { re := a.re, im := -a.im : ℂ }
have a₁ : { re := (a * b).re, im := -(a * b).im : ℂ }.re = ({ re := b.re, im := -b.im : ℂ } * { re := a.re, im := -a.im : ℂ }).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
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
⊢ { re := (a * b).re, im := -(a * b).im : ℂ } = { re := b.re, im := -b.im : ℂ } * { re := a.re, im := -a.im : ℂ }
have a₂ : { re := (a * b).re, im := -(a * b).im : ℂ }.im = ({ re := b.re, im := -b.im : ℂ } * { re := a.re, im := -a.im : ℂ }).im
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
a b : ℂ
⊢ { re := (a * b).re, im := -(a * b).im : ℂ }.re =
    ({ re := b.re, im := -b.im : ℂ } * { re := a.re, im := -a.im : ℂ }).re
have a₁ : a.re * b.re - a.im * b.im = b.re * a.re - b.im * a.im
Tactic: simp [add_comm]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
a b : ℂ
⊢ { re := (a * b).re, im := -(a * b).im : ℂ }.im =
    ({ re := b.re, im := -b.im : ℂ } * { re := a.re, im := -a.im : ℂ }).im
have a₁ : -(a.re * b.im) + -(a.im * b.re) = -(b.re * a.im) + -(b.im * a.re)
Tactic: simp [add_comm]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
a b : ℂ
⊢ { re := (a + b).re, im := -(a + b).im : ℂ } = { re := a.re, im := -a.im : ℂ } + { re := b.re, im := -b.im : ℂ }
have a₁ : { re := (a + b).re, im := -(a + b).im : ℂ }.re = ({ re := a.re, im := -a.im : ℂ } + { re := b.re, im := -b.im : ℂ }).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
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
⊢ { re := (a + b).re, im := -(a + b).im : ℂ } = { re := a.re, im := -a.im : ℂ } + { re := b.re, im := -b.im : ℂ }
have a₂ : { re := (a + b).re, im := -(a + b).im : ℂ }.im = ({ re := a.re, im := -a.im : ℂ } + { re := b.re, im := -b.im : ℂ }).im
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
z : ℂ
h_1 : ∃ (r : ℝ), z = (↑r : ℂ)
h : ℝ
e : z = (↑h : ℂ)
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) z = z
have rw : (starRingEnd ℂ : (a : ℂ) → ℂ) (↑h : ℂ) = (↑h : ℂ)
Tactic: rw [e, conj_ofReal]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
z : ℂ
h_1 : ∃ (r : ℝ), z = (↑r : ℂ)
h : ℝ
e : z = (↑h : ℂ)
rw : (starRingEnd ℂ : (a : ℂ) → ℂ) (↑h : ℂ) = (↑h : ℂ)
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) z = z
have rw₁ : (↑h : ℂ) = (↑h : ℂ)
Tactic: rw [e, conj_ofReal]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
x y : ℝ
⊢ (normSq : (a : ℂ) → ℝ) ((↑x : ℂ) + (↑y : ℂ) * I) = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
have rw : (normSq : (a : ℂ) → ℝ) { re := x, im := y : ℂ } = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
Tactic: rw [← mk_eq_add_mul_I, normSq_mk, sq, sq]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
x y : ℝ
rw : (normSq : (a : ℂ) → ℝ) { re := x, im := y : ℂ } = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
⊢ (normSq : (a : ℂ) → ℝ) ((↑x : ℂ) + (↑y : ℂ) * I) = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
have rw₁ : x * x + y * y = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
Tactic: rw [← mk_eq_add_mul_I, normSq_mk, sq, sq]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
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
⊢ (normSq : (a : ℂ) → ℝ) ((↑x : ℂ) + (↑y : ℂ) * I) = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
have rw₂ : x * x + y * y = x * x + HPow.hPow (β := ℕ) y 2
Tactic: rw [← mk_eq_add_mul_I, normSq_mk, sq, sq]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
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
⊢ (normSq : (a : ℂ) → ℝ) ((↑x : ℂ) + (↑y : ℂ) * I) = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
have rw₃ : x * x + y * y = x * x + y * y
Tactic: rw [← mk_eq_add_mul_I, normSq_mk, sq, sq]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
z : ℂ
⊢ (↑((normSq : (a : ℂ) → ℝ) z) : ℂ) = HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) z
have a : (↑((normSq : (a : ℂ) → ℝ) z) : ℂ).re = (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) z).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
z : ℂ
a : (↑((normSq : (a : ℂ) → ℝ) z) : ℂ).re = (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) z).re
⊢ (↑((normSq : (a : ℂ) → ℝ) z) : ℂ) = HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) z
have a₁ : (↑((normSq : (a : ℂ) → ℝ) z) : ℂ).im = (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) z).im
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
z w : ℂ
⊢ (normSq : (a : ℂ) → ℝ) (z + w) =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ) ((normSq : (a : ℂ) → ℝ) w : ℝ) +
      2 * (HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ)).re
have 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)
Tactic: simp [normSq]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
⊢ HPow.hPow (β := ℕ) I 2 = -1
have rw : I * I = -1
Tactic: rw [sq, I_mul_I]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
rw : I * I = -1
⊢ HPow.hPow (β := ℕ) I 2 = -1
have rw₁ : Eq (α := ℂ) (-1) (-1)
Tactic: rw [sq, I_mul_I]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
⊢ HPow.hPow (β := ℕ) I 3 = -I
have rw : HPow.hPow (β := ℕ) I 2 * I = -I
Tactic: rw [pow_succ, I_sq, neg_one_mul]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
rw : HPow.hPow (β := ℕ) I 2 * I = -I
⊢ HPow.hPow (β := ℕ) I 3 = -I
have rw₁ : -1 * I = -I
Tactic: rw [pow_succ, I_sq, neg_one_mul]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
rw : HPow.hPow (β := ℕ) I 2 * I = -I
rw₁ : -1 * I = -I
⊢ HPow.hPow (β := ℕ) I 3 = -I
have rw₂ : -I = -I
Tactic: rw [pow_succ, I_sq, neg_one_mul]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
⊢ HPow.hPow (β := ℕ) I 4 = 1
have rw : 4 = HMul.hMul (α := ℕ) 2 2
Tactic: rw [(by simp : 4 = 2 * 2), pow_mul, I_sq, neg_one_sq]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
rw : 4 = HMul.hMul (α := ℕ) 2 2
rw₁ : I ^ HMul.hMul (α := ℕ) 2 2 = 1
⊢ HPow.hPow (β := ℕ) I 4 = 1
have rw₂ : HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) I 2) 2 = 1
Tactic: rw [(by simp : 4 = 2 * 2), pow_mul, I_sq, neg_one_sq]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
rw : 4 = HMul.hMul (α := ℕ) 2 2
rw₁ : I ^ HMul.hMul (α := ℕ) 2 2 = 1
rw₂ : HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) I 2) 2 = 1
⊢ HPow.hPow (β := ℕ) I 4 = 1
have rw₃ : HPow.hPow (α := ℂ) (β := ℕ) (-1) 2 = 1
Tactic: rw [(by simp : 4 = 2 * 2), pow_mul, I_sq, neg_one_sq]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
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
⊢ HPow.hPow (β := ℕ) I 4 = 1
have rw₄ : Eq (α := ℂ) 1 1
Tactic: rw [(by simp : 4 = 2 * 2), pow_mul, I_sq, neg_one_sq]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
n : ℕ
| I ^ n
have rw : I ^ (4 * (n / 4) + n % 4)
Tactic: rw [← Nat.div_add_mod n 4]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
n : ℕ
⊢ I ^ n = I ^ (n % 4)
have conv_lhs : I ^ (4 * (n / 4) + n % 4) = I ^ (n % 4)
Tactic: conv_lhs => rw [← Nat.div_add_mod n 4]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
r : ℝ
n : ℕ
⊢ (↑(r ^ n) : ℂ) = (↑r : ℂ) ^ n
have zero : (↑(HPow.hPow (β := ℕ) r 0) : ℂ) = HPow.hPow (β := ℕ) (↑r : ℂ) 0
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
r : ℝ
n : ℕ
zero : (↑(HPow.hPow (β := ℕ) r 0) : ℂ) = HPow.hPow (β := ℕ) (↑r : ℂ) 0
⊢ (↑(r ^ n) : ℂ) = (↑r : ℂ) ^ n
have succ : ∀ (n : ℕ), (↑(r ^ n) : ℂ) = (↑r : ℂ) ^ n → (↑(r ^ (n + 1)) : ℂ) = (↑r : ℂ) ^ (n + 1)
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
z w : ℂ
⊢ (normSq : (a : ℂ) → ℝ) (z - w) =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ) ((normSq : (a : ℂ) → ℝ) w : ℝ) -
      2 * (HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ)).re
have 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
Tactic: rw [sub_eq_add_neg, normSq_add]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
z w : ℂ
⊢ 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
have 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
Tactic: simp only [map_neg, mul_neg, neg_re, normSq_neg]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
⊢ Eq (α := ℂ) 0⁻¹ 0
have rw : (↑0 : ℂ)⁻¹ = (↑0 : ℂ)
Tactic: rw [← ofReal_zero, ← ofReal_inv, inv_zero]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
rw : (↑0 : ℂ)⁻¹ = (↑0 : ℂ)
⊢ Eq (α := ℂ) 0⁻¹ 0
have rw₁ : (↑0⁻¹ : ℂ) = (↑0 : ℂ)
Tactic: rw [← ofReal_zero, ← ofReal_inv, inv_zero]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
rw : (↑0 : ℂ)⁻¹ = (↑0 : ℂ)
rw₁ : (↑0⁻¹ : ℂ) = (↑0 : ℂ)
⊢ Eq (α := ℂ) 0⁻¹ 0
have rw₂ : (↑0 : ℂ) = (↑0 : ℂ)
Tactic: rw [← ofReal_zero, ← ofReal_inv, inv_zero]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
z : ℂ
h : z ≠ 0
⊢ z * z⁻¹ = 1
have rw : z * HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) (↑((normSq : (a : ℂ) → ℝ) z)⁻¹ : ℂ) = 1
Tactic: rw [inv_def, ← mul_assoc, mul_conj, ← ofReal_mul, mul_inv_cancel₀ (mt normSq_eq_zero.1 h),
    ofReal_one]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
z : ℂ
h : z ≠ 0
rw : z * HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) (↑((normSq : (a : ℂ) → ℝ) z)⁻¹ : ℂ) = 1
⊢ z * z⁻¹ = 1
have rw₁ : HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) * (↑((normSq : (a : ℂ) → ℝ) z)⁻¹ : ℂ) = 1
Tactic: rw [inv_def, ← mul_assoc, mul_conj, ← ofReal_mul, mul_inv_cancel₀ (mt normSq_eq_zero.1 h),
    ofReal_one]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
z : ℂ
h : z ≠ 0
rw : z * HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) (↑((normSq : (a : ℂ) → ℝ) z)⁻¹ : ℂ) = 1
rw₁ : HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) * (↑((normSq : (a : ℂ) → ℝ) z)⁻¹ : ℂ) = 1
⊢ z * z⁻¹ = 1
have rw₂ : (↑((normSq : (a : ℂ) → ℝ) z) : ℂ) * (↑((normSq : (a : ℂ) → ℝ) z)⁻¹ : ℂ) = 1
Tactic: rw [inv_def, ← mul_assoc, mul_conj, ← ofReal_mul, mul_inv_cancel₀ (mt normSq_eq_zero.1 h),
    ofReal_one]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
z : ℂ
h : z ≠ 0
rw : z * HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) (↑((normSq : (a : ℂ) → ℝ) z)⁻¹ : ℂ) = 1
rw₁ : HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) * (↑((normSq : (a : ℂ) → ℝ) z)⁻¹ : ℂ) = 1
rw₂ : (↑((normSq : (a : ℂ) → ℝ) z) : ℂ) * (↑((normSq : (a : ℂ) → ℝ) z)⁻¹ : ℂ) = 1
⊢ z * z⁻¹ = 1
have rw₃ : (↑(HMul.hMul (α := ℝ) (β := ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ) (((normSq : (a : ℂ) → ℝ) z)⁻¹ : ℝ)) : ℂ) = 1
Tactic: rw [inv_def, ← mul_assoc, mul_conj, ← ofReal_mul, mul_inv_cancel₀ (mt normSq_eq_zero.1 h),
    ofReal_one]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
z : ℂ
h : z ≠ 0
rw : z * HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) (↑((normSq : (a : ℂ) → ℝ) z)⁻¹ : ℂ) = 1
rw₁ : HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) * (↑((normSq : (a : ℂ) → ℝ) z)⁻¹ : ℂ) = 1
rw₂ : (↑((normSq : (a : ℂ) → ℝ) z) : ℂ) * (↑((normSq : (a : ℂ) → ℝ) z)⁻¹ : ℂ) = 1
rw₃ : (↑(HMul.hMul (α := ℝ) (β := ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ) (((normSq : (a : ℂ) → ℝ) z)⁻¹ : ℝ)) : ℂ) = 1
⊢ z * z⁻¹ = 1
have rw₄ : (↑1 : ℂ) = 1
Tactic: rw [inv_def, ← mul_assoc, mul_conj, ← ofReal_mul, mul_inv_cancel₀ (mt normSq_eq_zero.1 h),
    ofReal_one]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
z : ℂ
h : z ≠ 0
rw : z * HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) (↑((normSq : (a : ℂ) → ℝ) z)⁻¹ : ℂ) = 1
rw₁ : HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) * (↑((normSq : (a : ℂ) → ℝ) z)⁻¹ : ℂ) = 1
rw₂ : (↑((normSq : (a : ℂ) → ℝ) z) : ℂ) * (↑((normSq : (a : ℂ) → ℝ) z)⁻¹ : ℂ) = 1
rw₃ : (↑(HMul.hMul (α := ℝ) (β := ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ) (((normSq : (a : ℂ) → ℝ) z)⁻¹ : ℝ)) : ℂ) = 1
rw₄ : (↑1 : ℂ) = 1
⊢ z * z⁻¹ = 1
have rw₅ : Eq (α := ℂ) 1 1
Tactic: rw [inv_def, ← mul_assoc, mul_conj, ← ofReal_mul, mul_inv_cancel₀ (mt normSq_eq_zero.1 h),
    ofReal_one]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
α : Type u_1
q : ℚ≥0
⊢ (↑q : ℂ) = HDiv.hDiv (α := ℂ) (↑q.num : ℂ) (↑q.den : ℂ)
have a : re (↑q : ℂ) = (HDiv.hDiv (α := ℂ) (↑q.num : ℂ) (↑q.den : ℂ)).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
α : Type u_1
q : ℚ≥0
a : re (↑q : ℂ) = (HDiv.hDiv (α := ℂ) (↑q.num : ℂ) (↑q.den : ℂ)).re
⊢ (↑q : ℂ) = HDiv.hDiv (α := ℂ) (↑q.num : ℂ) (↑q.den : ℂ)
have a₁ : im (↑q : ℂ) = (HDiv.hDiv (α := ℂ) (↑q.num : ℂ) (↑q.den : ℂ)).im
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
α : Type u_1
q : ℚ
⊢ (↑q : ℂ) = HDiv.hDiv (α := ℂ) (↑q.num : ℂ) (↑q.den : ℂ)
have a : re (↑q : ℂ) = (HDiv.hDiv (α := ℂ) (↑q.num : ℂ) (↑q.den : ℂ)).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
α : Type u_1
q : ℚ
a : re (↑q : ℂ) = (HDiv.hDiv (α := ℂ) (↑q.num : ℂ) (↑q.den : ℂ)).re
⊢ (↑q : ℂ) = HDiv.hDiv (α := ℂ) (↑q.num : ℂ) (↑q.den : ℂ)
have a₁ : im (↑q : ℂ) = (HDiv.hDiv (α := ℂ) (↑q.num : ℂ) (↑q.den : ℂ)).im
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
⊢ I⁻¹ = -I
have rw : 1 / I = -I
Tactic: rw [inv_eq_one_div, div_I, one_mul]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
rw : 1 / I = -I
⊢ I⁻¹ = -I
have rw₁ : -(1 * I) = -I
Tactic: rw [inv_eq_one_div, div_I, one_mul]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
rw : 1 / I = -I
rw₁ : -(1 * I) = -I
⊢ I⁻¹ = -I
have rw₂ : -I = -I
Tactic: rw [inv_eq_one_div, div_I, one_mul]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
z : ℂ
x : ℝ
⊢ z / (↑x : ℂ) = { re := z.re / x, im := z.im / x }
have simp_rw : (↑x : ℂ)⁻¹ * z = { re := x⁻¹ * z.re, im := x⁻¹ * z.im }
Tactic: simp_rw [div_eq_inv_mul, ← ofReal_inv, ofReal_mul']
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
z : ℂ
x : ℝ
simp_rw : (↑x : ℂ)⁻¹ * z = { re := x⁻¹ * z.re, im := x⁻¹ * z.im }
⊢ z / (↑x : ℂ) = { re := z.re / x, im := z.im / x }
have simp_rw₁ : (↑x⁻¹ : ℂ) * z = { re := x⁻¹ * z.re, im := x⁻¹ * z.im }
Tactic: simp_rw [div_eq_inv_mul, ← ofReal_inv, ofReal_mul']
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
z : ℂ
x : ℝ
⊢ (z / (↑x : ℂ)).re = z.re / x
have rw : { re := z.re / x, im := z.im / x : ℂ }.re = z.re / x
Tactic: rw [div_ofReal]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
z : ℂ
x : ℝ
⊢ (z / (↑x : ℂ)).im = z.im / x
have rw : { re := z.re / x, im := z.im / x : ℂ }.im = z.im / x
Tactic: rw [div_ofReal]