awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
x : ℂ
y : ℝ
hx : IsSelfAdjoint x
rw : y = (RCLike.re : (a : ℂ) → ℝ) x ↔ (↑y : ℂ) = x
⊢ y = x.re ↔ (↑y : ℂ) = x

Tactic:
rw [← RCLike.re_eq_complex_re]

Premises used: RCLike.re_eq_complex_re
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
x : ℂ
y : ℝ
hx : IsSelfAdjoint x
⊢ y = (RCLike.re : (a : ℂ) → ℝ) x ↔ (↑y : ℂ) = x

Tactic:
RCLike.ofReal_eq_re_of_isSelfAdjoint hx

Premises used: RCLike.ofReal_eq_re_of_isSelfAdjoint
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
x : ℂ
y : ℝ
hx : IsSelfAdjoint x
⊢ y = (RCLike.re : (a : ℂ) → ℝ) x ↔ (↑y : ℂ) = x

Tactic:
exact RCLike.ofReal_eq_re_of_isSelfAdjoint hx

Premises used: RCLike.ofReal_eq_re_of_isSelfAdjoint
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℂ E
𝕜 : Type u_2
inst_2 : RCLike 𝕜
h : Eq (α := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) RCLike.I : ℝ) (1 : ℝ)
x : 𝕜
⊢ (fun (x : ℂ) ↦ (↑x.re : 𝕜) + HMul.hMul (α := 𝕜) (↑x.im : 𝕜) RCLike.I)
      ((fun (x : 𝕜) ↦ (↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) + (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * I) x) =
    x

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℂ E
𝕜 : Type u_2
inst_2 : RCLike 𝕜
h : Eq (α := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) RCLike.I : ℝ) (1 : ℝ)
x : ℂ
⊢ (fun (x : 𝕜) ↦ (↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) + (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * I)
      ((fun (x : ℂ) ↦ (↑x.re : 𝕜) + HMul.hMul (α := 𝕜) (↑x.im : 𝕜) RCLike.I) x) =
    x

Tactic:
simp [h]
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℂ E
𝕜 : Type u_2
inst_2 : RCLike 𝕜
h : Eq (α := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) RCLike.I : ℝ) (1 : ℝ)
x y : 𝕜
simp :
  (↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) -
        (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) +
      ((↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) +
          (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ)) *
        I =
    ((↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) + (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * I) *
      ((↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) + (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) * I)
⊢ (↑((RCLike.re : (a : 𝕜) → ℝ) (x * y)) : ℂ) + (↑((RCLike.im : (a : 𝕜) → ℝ) (x * y)) : ℂ) * I =
    ((↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) + (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * I) *
      ((↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) + (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) * I)

Tactic:
simp only [RCLike.mul_re, ofReal_sub, ofReal_mul, RCLike.mul_im, ofReal_add]

Premises used: Complex.ofReal_add, RCLike.mul_im, Complex.ofReal_sub, RCLike.mul_re, Complex.ofReal_mul
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℂ E
𝕜 : Type u_2
inst_2 : RCLike 𝕜
h : Eq (α := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) RCLike.I : ℝ) (1 : ℝ)
x y : 𝕜
ring_nf :
  (↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) +
          (↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) * I +
        (↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * I -
      (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) =
    (↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) +
          (↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) * I +
        (↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * I +
      (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) * HPow.hPow (β := ℕ) I 2
⊢ (↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) -
        (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) +
      ((↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) +
          (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ)) *
        I =
    ((↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) + (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * I) *
      ((↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) + (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) * I)

Tactic:
ring_nf
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℂ E
𝕜 : Type u_2
inst_2 : RCLike 𝕜
h : Eq (α := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) RCLike.I : ℝ) (1 : ℝ)
x y : 𝕜
rw :
  (↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) +
          (↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) * I +
        (↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * I -
      (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) =
    (↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) +
          (↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) * I +
        (↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * I +
      (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) * -1
⊢ (↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) +
          (↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) * I +
        (↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * I -
      (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) =
    (↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) +
          (↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) * I +
        (↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * I +
      (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) * HPow.hPow (β := ℕ) I 2

Tactic:
rw [I_sq]

Premises used: Complex.I_sq
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℂ E
𝕜 : Type u_2
inst_2 : RCLike 𝕜
h : Eq (α := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) RCLike.I : ℝ) (1 : ℝ)
x y : 𝕜
⊢ (↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) +
          (↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) * I +
        (↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * I -
      (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) =
    (↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) +
          (↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) * I +
        (↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * I +
      (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) * -1

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℂ E
𝕜 : Type u_2
inst_2 : RCLike 𝕜
h : Eq (α := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) RCLike.I : ℝ) (1 : ℝ)
x y : 𝕜
simp :
  (↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) + (↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) +
      ((↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) + (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ)) * I =
    (↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) + (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * I +
      ((↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) + (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) * I)
⊢ (↑((RCLike.re : (a : 𝕜) → ℝ) (x + y)) : ℂ) + (↑((RCLike.im : (a : 𝕜) → ℝ) (x + y)) : ℂ) * I =
    (↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) + (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * I +
      ((↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) + (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) * I)

Tactic:
simp only [map_add, ofReal_add]

Premises used: Complex.ofReal_add, map_add
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℂ E
𝕜 : Type u_2
inst_2 : RCLike 𝕜
h : Eq (α := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) RCLike.I : ℝ) (1 : ℝ)
x y : 𝕜
⊢ (↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) + (↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) +
      ((↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) + (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ)) * I =
    (↑((RCLike.re : (a : 𝕜) → ℝ) x) : ℂ) + (↑((RCLike.im : (a : 𝕜) → ℝ) x) : ℂ) * I +
      ((↑((RCLike.re : (a : 𝕜) → ℝ) y) : ℂ) + (↑((RCLike.im : (a : 𝕜) → ℝ) y) : ℂ) * I)

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
𝕜 : Type u_2
𝕜' : Type u_3
inst : RCLike 𝕜
inst_1 : RCLike 𝕜'
h : Eq (α := ℝ) ((RCLike.im : (a : 𝕜') → ℝ) RCLike.I : ℝ) (1 : ℝ)
a : 𝕜
rw :
  LE.le (α := ℝ) (0 : ℝ) ((RCLike.re : (a : 𝕜') → ℝ) ((RCLike.map 𝕜 𝕜' : (a : 𝕜) → 𝕜') a : 𝕜') : ℝ) ∧
      Eq (α := ℝ) ((RCLike.im : (a : 𝕜') → ℝ) ((RCLike.map 𝕜 𝕜' : (a : 𝕜) → 𝕜') a : 𝕜') : ℝ) (0 : ℝ) ↔
    LE.le (α := ℝ) (0 : ℝ) ((RCLike.re : (a : 𝕜) → ℝ) a : ℝ) ∧ Eq (α := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) a : ℝ) (0 : ℝ)
⊢ LE.le.{u_3} (α := 𝕜') (0 : 𝕜') ((RCLike.map 𝕜 𝕜' : (a : 𝕜) → 𝕜') a : 𝕜') ↔ 0 ≤ a

Tactic:
rw [RCLike.nonneg_iff, RCLike.nonneg_iff (K := 𝕜)]

Premises used: RCLike.nonneg_iff
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
𝕜 : Type u_2
𝕜' : Type u_3
inst : RCLike 𝕜
inst_1 : RCLike 𝕜'
h : Eq (α := ℝ) ((RCLike.im : (a : 𝕜') → ℝ) RCLike.I : ℝ) (1 : ℝ)
a : 𝕜
⊢ LE.le (α := ℝ) (0 : ℝ) ((RCLike.re : (a : 𝕜') → ℝ) ((RCLike.map 𝕜 𝕜' : (a : 𝕜) → 𝕜') a : 𝕜') : ℝ) ∧
      Eq (α := ℝ) ((RCLike.im : (a : 𝕜') → ℝ) ((RCLike.map 𝕜 𝕜' : (a : 𝕜) → 𝕜') a : 𝕜') : ℝ) (0 : ℝ) ↔
    LE.le (α := ℝ) (0 : ℝ) ((RCLike.re : (a : 𝕜) → ℝ) a : ℝ) ∧ Eq (α := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) a : ℝ) (0 : ℝ)

Tactic:
simp [h]
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
a : 𝕜
⊢ 0 ≤ (↑((RCLike.re : (a : 𝕜) → ℝ) a) : ℂ) + (↑((RCLike.im : (a : 𝕜) → ℝ) a) : ℂ) * I ↔ 0 ≤ a

Tactic:
RCLike.map_nonneg_iff I_im

Premises used: RCLike.map_nonneg_iff
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℂ E
𝕜 : Type u_2
inst_2 : RCLike 𝕜
h : Eq (α := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) RCLike.I : ℝ) (1 : ℝ)
x : ℝ
x_1 : 𝕜
simp : (↑x : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) x_1) : ℂ) * I = (↑x : ℂ) * ((↑((RCLike.im : (a : 𝕜) → ℝ) x_1) : ℂ) * I)
⊢ (RCLike.complexRingEquiv h).toFun (x • x_1) =
    HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) x : ℝ) ((RCLike.complexRingEquiv h).toFun x_1)

Tactic:
simp [RCLike.smul_re, RCLike.smul_im, ofReal_mul]

Premises used: RCLike.smul_re, RCLike.smul_im, Complex.ofReal_mul
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℂ E
𝕜 : Type u_2
inst_2 : RCLike 𝕜
h : Eq (α := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) RCLike.I : ℝ) (1 : ℝ)
x : ℝ
x_1 : 𝕜
⊢ (↑x : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) x_1) : ℂ) * I = (↑x : ℂ) * ((↑((RCLike.im : (a : 𝕜) → ℝ) x_1) : ℂ) * I)

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℂ E
𝕜 : Type u_2
inst_2 : RCLike 𝕜
h : Eq (α := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) RCLike.I : ℝ) (1 : ℝ)
x : 𝕜
⊢ 0 ≤
    norm (E := ℂ)
      (({ toFun := (RCLike.complexRingEquiv h).toFun, map_add' := ⋯, map_smul' := ⋯,
              invFun := (RCLike.complexRingEquiv h).invFun, left_inv := ⋯, right_inv := ⋯ : 𝕜 ≃ₗ[ℝ] ℂ } :
            (a : 𝕜) → ℂ)
          x :
        ℂ)

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℂ E
𝕜 : Type u_2
inst_2 : RCLike 𝕜
h : Eq (α := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) RCLike.I : ℝ) (1 : ℝ)
x : 𝕜
⊢ 0 ≤ ‖x‖

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℂ E
𝕜 : Type u_2
inst_2 : RCLike 𝕜
h : Eq (α := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) RCLike.I : ℝ) (1 : ℝ)
x : 𝕜
rw :
  (normSq : (a : ℂ) → ℝ)
      (({ toFun := (RCLike.complexRingEquiv h).toFun, map_add' := ⋯, map_smul' := ⋯,
              invFun := (RCLike.complexRingEquiv h).invFun, left_inv := ⋯, right_inv := ⋯ } :
            (a : 𝕜) → ℂ)
          x :
        ℂ) =
    HMul.hMul (α := ℝ) (β := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) x : ℝ) ((RCLike.re : (a : 𝕜) → ℝ) x : ℝ) +
      HMul.hMul (α := ℝ) (β := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) x : ℝ) ((RCLike.im : (a : 𝕜) → ℝ) x : ℝ)
⊢ norm (E := ℂ)
      (({ toFun := (RCLike.complexRingEquiv h).toFun, map_add' := ⋯, map_smul' := ⋯,
              invFun := (RCLike.complexRingEquiv h).invFun, left_inv := ⋯, right_inv := ⋯ : 𝕜 ≃ₗ[ℝ] ℂ } :
            (a : 𝕜) → ℂ)
          x :
        ℂ) =
    ‖x‖

Tactic:
rw [← sq_eq_sq₀ (by positivity) (by positivity), ← normSq_eq_norm_sq, ← RCLike.normSq_eq_def',
      RCLike.normSq_apply]

Premises used: Complex.normSq_eq_norm_sq, RCLike.normSq_eq_def', sq_eq_sq₀, RCLike.normSq_apply
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℂ E
𝕜 : Type u_2
inst_2 : RCLike 𝕜
h : Eq (α := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) RCLike.I : ℝ) (1 : ℝ)
x : 𝕜
⊢ (normSq : (a : ℂ) → ℝ)
      (({ toFun := (RCLike.complexRingEquiv h).toFun, map_add' := ⋯, map_smul' := ⋯,
              invFun := (RCLike.complexRingEquiv h).invFun, left_inv := ⋯, right_inv := ⋯ } :
            (a : 𝕜) → ℂ)
          x :
        ℂ) =
    HMul.hMul (α := ℝ) (β := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) x : ℝ) ((RCLike.re : (a : 𝕜) → ℝ) x : ℝ) +
      HMul.hMul (α := ℝ) (β := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) x : ℝ) ((RCLike.im : (a : 𝕜) → ℝ) x : ℝ)

Tactic:
simp [normSq_add]

Premises used: Complex.normSq_add
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
h : Eq (α := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) RCLike.I : ℝ) (1 : ℝ)
⊢ (↑(↑(RCLike.complexLinearIsometryEquiv h) : 𝕜 ≃L[ℝ] ℂ) : 𝕜 →L[ℝ] ℂ) = RCLike.map 𝕜 ℂ

Tactic:
rfl

Premises used: RCLike.map, rfl, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
a : 𝕜
inl :
  ∀ (h : Eq.{u_2 + 1} (α := 𝕜) RCLike.I 0),
    ‖(↑((RCLike.re : (a : 𝕜) → ℝ) a) : ℂ) + (↑((RCLike.im : (a : 𝕜) → ℝ) a) : ℂ) * I‖ = ‖a‖
inr :
  ∀ (h : Eq (α := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) RCLike.I : ℝ) (1 : ℝ)),
    ‖(↑((RCLike.re : (a : 𝕜) → ℝ) a) : ℂ) + (↑((RCLike.im : (a : 𝕜) → ℝ) a) : ℂ) * I‖ = ‖a‖
⊢ ‖(↑((RCLike.re : (a : 𝕜) → ℝ) a) : ℂ) + (↑((RCLike.im : (a : 𝕜) → ℝ) a) : ℂ) * I‖ = ‖a‖

Tactic:
obtain (h | h) := RCLike.I_eq_zero_or_im_I_eq_one (K := 𝕜)

Premises used: RCLike.I_eq_zero_or_im_I_eq_one
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
a : 𝕜
h : Eq.{u_2 + 1} (α := 𝕜) RCLike.I 0
inl :
  ‖(↑((RCLike.re : (a : 𝕜) → ℝ) ((↑((RCLike.re : (a : 𝕜) → ℝ) a) : 𝕜) + HMul.hMul (α := 𝕜) (↑0 : 𝕜) RCLike.I)) : ℂ) +
        (↑((RCLike.im : (a : 𝕜) → ℝ) ((↑((RCLike.re : (a : 𝕜) → ℝ) a) : 𝕜) + HMul.hMul (α := 𝕜) (↑0 : 𝕜) RCLike.I)) :
            ℂ) *
          I‖ =
    ‖(↑((RCLike.re : (a : 𝕜) → ℝ) a) : 𝕜) + HMul.hMul (α := 𝕜) (↑0 : 𝕜) RCLike.I‖
⊢ ‖(↑((RCLike.re : (a : 𝕜) → ℝ) a) : ℂ) + (↑((RCLike.im : (a : 𝕜) → ℝ) a) : ℂ) * I‖ = ‖a‖

Tactic:
rw [← RCLike.re_add_im a, RCLike.im_eq_zero h]

Premises used: RCLike.re_add_im, RCLike.im_eq_zero
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
a : 𝕜
h : Eq.{u_2 + 1} (α := 𝕜) RCLike.I 0
⊢ ‖(↑((RCLike.re : (a : 𝕜) → ℝ) ((↑((RCLike.re : (a : 𝕜) → ℝ) a) : 𝕜) + HMul.hMul (α := 𝕜) (↑0 : 𝕜) RCLike.I)) : ℂ) +
        (↑((RCLike.im : (a : 𝕜) → ℝ) ((↑((RCLike.re : (a : 𝕜) → ℝ) a) : 𝕜) + HMul.hMul (α := 𝕜) (↑0 : 𝕜) RCLike.I)) :
            ℂ) *
          I‖ =
    ‖(↑((RCLike.re : (a : 𝕜) → ℝ) a) : 𝕜) + HMul.hMul (α := 𝕜) (↑0 : 𝕜) RCLike.I‖

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
a : 𝕜
h : Eq (α := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) RCLike.I : ℝ) (1 : ℝ)
⊢ ‖(↑((RCLike.re : (a : 𝕜) → ℝ) a) : ℂ) + (↑((RCLike.im : (a : 𝕜) → ℝ) a) : ℂ) * I‖ = ‖a‖

Tactic:
(RCLike.complexLinearIsometryEquiv h).norm_map a

Premises used: LinearIsometryEquiv.norm_map, RCLike.complexLinearIsometryEquiv
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
a : 𝕜
h : Eq (α := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) RCLike.I : ℝ) (1 : ℝ)
⊢ ‖(↑((RCLike.re : (a : 𝕜) → ℝ) a) : ℂ) + (↑((RCLike.im : (a : 𝕜) → ℝ) a) : ℂ) * I‖ = ‖a‖

Tactic:
exact (RCLike.complexLinearIsometryEquiv h).norm_map a

Premises used: LinearIsometryEquiv.norm_map, RCLike.complexLinearIsometryEquiv
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
simp_rw : ∀ (x y : ℤ), dist (↑(↑x : ℝ) : ℂ) (↑(↑y : ℝ) : ℂ) = dist x y
simp_rw₁ : ∀ (x y : ℤ), dist (α := ℝ) (↑x : ℝ) (↑y : ℝ) = dist x y
simp_rw₂ : ∀ (x y : ℤ), True
⊢ ∀ (x y : ℤ), dist (α := ℂ) (↑x : ℂ) (↑y : ℂ) = dist x y

Tactic:
simp_rw [← Complex.ofReal_intCast,
    Complex.isometry_ofReal.dist_eq, Int.dist_cast_real, implies_true]

Premises used: Complex.isometry_ofReal, Complex.ofReal_intCast, Int.dist_cast_real, Isometry.dist_eq, implies_true
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
⊢ IsClosedEmbedding (Y := ℂ) Int.cast

Tactic:
isometry_intCast.isClosedEmbedding

Premises used: Isometry.isClosedEmbedding, Complex.isometry_intCast
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
⊢ IsClosed (X := ℂ) (Set.range Int.cast)

Tactic:
Complex.isClosedEmbedding_intCast.isClosed_range

Premises used: Complex.isClosedEmbedding_intCast, Topology.IsClosedEmbedding.isClosed_range
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
⊢ IsOpen (X := ℂ) (Set.range Int.cast)ᶜ

Tactic:
Complex.isClosed_range_intCast.isOpen_compl

Premises used: IsClosed.isOpen_compl
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
hz : 0 ≤ z
⊢ z.im = 0

Tactic:
hz.2.symm

Premises used: And.right, Eq.symm
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
hz : 0 ≤ z
lift : ∀ (z : ℝ) (hz : 0 ≤ (↑z : ℂ)), (↑z : ℂ) = (↑‖(↑z : ℂ)‖ : ℂ)
⊢ z = (↑‖z‖ : ℂ)

Tactic:
lift z to ℝ using hz.2.symm

Premises used: And.right, Eq.symm
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℝ
hz : 0 ≤ (↑z : ℂ)
rw : (↑z : ℂ) = (↑‖z‖ : ℂ)
rw₁ rw₂ : (↑z : ℂ) = (↑z : ℂ)
⊢ (↑z : ℂ) = (↑‖(↑z : ℂ)‖ : ℂ)

Tactic:
rw [norm_real, Real.norm_of_nonneg (id hz.1 : 0 ≤ z)]

Premises used: id, Complex.norm_real, And.left, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
⊢ OrderClosedTopology ℂ

Tactic:
RCLike.instOrderClosedTopology

Premises used: RCLike.instOrderClosedTopology
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
x : ℂ
hx : 0 ≤ x
⊢ (↑‖x‖ : ℂ) = x

Tactic:
RCLike.norm_of_nonneg' hx

Premises used: RCLike.norm_of_nonneg'
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
x : ℂ
hx : 0 ≤ x
⊢ (↑‖x‖ : ℂ) = x

Tactic:
exact RCLike.norm_of_nonneg' hx

Premises used: RCLike.norm_of_nonneg'
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
x : ℂ
hx : IsSelfAdjoint x
rw : LE.le (α := ℝ) (0 : ℝ) ((RCLike.re : (a : ℂ) → ℝ) x : ℝ) ↔ 0 ≤ x
⊢ 0 ≤ x.re ↔ 0 ≤ x

Tactic:
rw [← RCLike.re_eq_complex_re]

Premises used: RCLike.re_eq_complex_re
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
x : ℂ
hx : IsSelfAdjoint x
⊢ LE.le (α := ℝ) (0 : ℝ) ((RCLike.re : (a : ℂ) → ℝ) x : ℝ) ↔ 0 ≤ x

Tactic:
RCLike.re_nonneg_of_nonneg hx

Premises used: RCLike.re_nonneg_of_nonneg
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
x : ℂ
hx : IsSelfAdjoint x
⊢ LE.le (α := ℝ) (0 : ℝ) ((RCLike.re : (a : ℂ) → ℝ) x : ℝ) ↔ 0 ≤ x

Tactic:
exact RCLike.re_nonneg_of_nonneg hx

Premises used: RCLike.re_nonneg_of_nonneg
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
x y : ℂ
h : x ≤ y
⊢ LE.le (α := ℝ) ((RCLike.re : (a : ℂ) → ℝ) x : ℝ) ((RCLike.re : (a : ℂ) → ℝ) y : ℝ) ∧
    Eq (α := ℝ) ((RCLike.im : (a : ℂ) → ℝ) x : ℝ) ((RCLike.im : (a : ℂ) → ℝ) y : ℝ)

Tactic:
rw [RCLike.le_iff_re_im] at h

Premises used: RCLike.le_iff_re_im
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
x y : ℂ
h :
  LE.le (α := ℝ) ((RCLike.re : (a : ℂ) → ℝ) x : ℝ) ((RCLike.re : (a : ℂ) → ℝ) y : ℝ) ∧
    Eq (α := ℝ) ((RCLike.im : (a : ℂ) → ℝ) x : ℝ) ((RCLike.im : (a : ℂ) → ℝ) y : ℝ)
⊢ x.re ≤ y.re

Tactic:
h.1

Premises used: And.left
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
x y : ℂ
h :
  LE.le (α := ℝ) ((RCLike.re : (a : ℂ) → ℝ) x : ℝ) ((RCLike.re : (a : ℂ) → ℝ) y : ℝ) ∧
    Eq (α := ℝ) ((RCLike.im : (a : ℂ) → ℝ) x : ℝ) ((RCLike.im : (a : ℂ) → ℝ) y : ℝ)
⊢ x.re ≤ y.re

Tactic:
exact h.1

Premises used: And.left
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
x : ℂ
⊢ (re : (a : ℂ) → ℝ) x = x.re

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
⊢ I = Complex.I

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
x : ℂ
⊢ Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) x : ℝ) ((Complex.normSq : (a : ℂ) → ℝ) x : ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
α : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
L : SummationFilter α
f : α → 𝕜
x : 𝕜
⊢ HasSum (fun (x : α) ↦ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (f x)) x L ↔ HasSum f ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x) L

Tactic:
conjCLE.hasSum

Premises used: ContinuousLinearEquiv.hasSum, RCLike.conjCLE
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
α : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
L : SummationFilter α
f : α → 𝕜
x : 𝕜
⊢ HasSum (α := 𝕜) (fun (x : α) ↦ ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (f x) : 𝕜)) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜) L ↔
    HasSum f x L

Tactic:
conjCLE.hasSum'

Premises used: ContinuousLinearEquiv.hasSum', RCLike.conjCLE
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
α : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
L : SummationFilter α
f : α → 𝕜
⊢ Summable.{u_2, u_1} (α := 𝕜) (fun (x : α) ↦ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (f x)) L ↔ Summable f L

Tactic:
summable_star_iff

Premises used: summable_star_iff
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
α : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
L : SummationFilter α
f : α → 𝕜
⊢ Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (∑'[L] (a : α), f a) : 𝕜)
    (∑'[L] (a : α), (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (f a) : 𝕜)

Tactic:
tsum_star

Premises used: tsum_star
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
α : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
L : SummationFilter α
f : α → ℝ
x : ℝ
h : HasSum.{u_2, u_1} (α := 𝕜) (fun (x : α) ↦ (↑(f x) : 𝕜)) (↑x : 𝕜) L
⊢ HasSum f x L

Tactic:
simpa only [RCLike.reCLM_apply, RCLike.ofReal_re] using reCLM.hasSum h

Premises used: RCLike.reCLM_apply, RCLike.ofReal_re, RCLike.reCLM, ContinuousLinearMap.hasSum
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
α : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
L : SummationFilter α
f : α → ℝ
h : Summable.{u_2, u_1} (α := 𝕜) (fun (x : α) ↦ (↑(f x) : 𝕜)) L
⊢ Summable f L

Tactic:
simpa only [RCLike.reCLM_apply, RCLike.ofReal_re] using reCLM.summable h

Premises used: RCLike.reCLM_apply, RCLike.ofReal_re, ContinuousLinearMap.summable, RCLike.reCLM
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
α : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
L : SummationFilter α
f : α → ℝ
x : ℝ
⊢ (re : (a : 𝕜) → ℝ) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) x : 𝕜) = x

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
α : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
L : SummationFilter α
f : α → 𝕜
x : 𝕜
h : HasSum f x L
⊢ HasSum (α := ℝ) (fun (x : α) ↦ ((re : (a : 𝕜) → ℝ) (f x) : ℝ)) ((re : (a : 𝕜) → ℝ) x : ℝ) L

Tactic:
reCLM.hasSum h

Premises used: RCLike.reCLM, ContinuousLinearMap.hasSum
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
α : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
L : SummationFilter α
f : α → 𝕜
x : 𝕜
h : HasSum f x L
⊢ HasSum (α := ℝ) (fun (x : α) ↦ ((im : (a : 𝕜) → ℝ) (f x) : ℝ)) ((im : (a : 𝕜) → ℝ) x : ℝ) L

Tactic:
imCLM.hasSum h

Premises used: ContinuousLinearMap.hasSum, RCLike.imCLM
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
α : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
L : SummationFilter α
inst_1 : L.NeBot
f : α → 𝕜
h : Summable f L
⊢ Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) (∑'[L] (a : α), f a) : ℝ) (∑'[L] (a : α), (re : (a : 𝕜) → ℝ) (f a) : ℝ)

Tactic:
reCLM.map_tsum h

Premises used: RCLike.reCLM, ContinuousLinearMap.map_tsum
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
α : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
L : SummationFilter α
inst_1 : L.NeBot
f : α → 𝕜
h : Summable f L
⊢ Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) (∑'[L] (a : α), f a) : ℝ) (∑'[L] (a : α), (im : (a : 𝕜) → ℝ) (f a) : ℝ)

Tactic:
imCLM.map_tsum h

Premises used: ContinuousLinearMap.map_tsum, RCLike.imCLM