awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.Arg
Goal:
x y : ℂ
⊢ ‖x - y‖ = |‖x‖ - ‖y‖| ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg

Tactic:
sameRay_iff_norm_sub.symm.trans sameRay_iff

Premises used: sameRay_iff_norm_sub, Iff.trans, Complex.sameRay_iff, Iff.symm
-- Module: Mathlib.Analysis.Complex.Arg
Goal:
x y : ℂ
h : x.arg = y.arg
⊢ SameRay ℝ x y

Tactic:
sameRay_iff.mpr <| Or.inr <| Or.inr h

Premises used: Iff.mpr, Complex.sameRay_iff, Or.inr
-- Module: Mathlib.Analysis.Complex.Arg
Goal:
x y : ℂ
h : x.arg = y.arg
⊢ ‖x + y‖ = ‖x‖ + ‖y‖

Tactic:
(sameRay_of_arg_eq h).norm_add

Premises used: Complex.sameRay_of_arg_eq, SameRay.norm_add
-- Module: Mathlib.Analysis.Complex.Arg
Goal:
x y : ℂ
h : x.arg = y.arg
⊢ ‖x - y‖ = ‖‖x‖ - ‖y‖‖

Tactic:
(sameRay_of_arg_eq h).norm_sub

Premises used: SameRay.norm_sub, Complex.sameRay_of_arg_eq
-- Module: Mathlib.Analysis.Complex.Asymptotics
Goal:
α : Type u_1
f : α → ℝ
l : Filter α
⊢ Asymptotics.IsTheta (E := ℝ) l (fun (x : α) ↦ ‖(↑(f x) : ℂ)‖) f

Tactic:
simpa using (Asymptotics.isTheta_rfl (f := f)).norm_left

Premises used: Asymptotics.IsTheta.norm_left, Asymptotics.isTheta_rfl
-- Module: Mathlib.Analysis.Complex.Asymptotics
Goal:
α : Type u_1
E : Type u_2
inst : Norm E
l : Filter α
f : α → ℝ
g : α → E
⊢ Asymptotics.IsLittleO (E := ℂ) l (fun (x : α) ↦ (↑(f x) : ℂ)) g ↔ f =o[l] g

Tactic:
(isTheta_ofReal f l).isLittleO_congr_left

Premises used: Asymptotics.IsTheta.isLittleO_congr_left, Complex.isTheta_ofReal
-- Module: Mathlib.Analysis.Complex.Asymptotics
Goal:
α : Type u_1
E : Type u_2
inst : Norm E
l : Filter α
f : α → E
g : α → ℝ
⊢ (Asymptotics.IsLittleO (F := ℂ) l f fun (x : α) ↦ (↑(g x) : ℂ)) ↔ f =o[l] g

Tactic:
(isTheta_ofReal g l).isLittleO_congr_right

Premises used: Complex.isTheta_ofReal, Asymptotics.IsTheta.isLittleO_congr_right
-- Module: Mathlib.Analysis.Complex.Asymptotics
Goal:
α : Type u_1
E : Type u_2
inst : Norm E
l : Filter α
f : α → ℝ
g : α → E
⊢ Asymptotics.IsBigO (E := ℂ) l (fun (x : α) ↦ (↑(f x) : ℂ)) g ↔ f =O[l] g

Tactic:
(isTheta_ofReal f l).isBigO_congr_left

Premises used: Asymptotics.IsTheta.isBigO_congr_left, Complex.isTheta_ofReal
-- Module: Mathlib.Analysis.Complex.Asymptotics
Goal:
α : Type u_1
E : Type u_2
inst : Norm E
l : Filter α
f : α → E
g : α → ℝ
⊢ (Asymptotics.IsBigO (F := ℂ) l f fun (x : α) ↦ (↑(g x) : ℂ)) ↔ f =O[l] g

Tactic:
(isTheta_ofReal g l).isBigO_congr_right

Premises used: Complex.isTheta_ofReal, Asymptotics.IsTheta.isBigO_congr_right
-- Module: Mathlib.Analysis.Complex.Asymptotics
Goal:
α : Type u_1
E : Type u_2
inst : Norm E
l : Filter α
f : α → ℝ
g : α → E
⊢ Asymptotics.IsTheta (E := ℂ) l (fun (x : α) ↦ (↑(f x) : ℂ)) g ↔ f =Θ[l] g

Tactic:
(isTheta_ofReal f l).isTheta_congr_left

Premises used: Asymptotics.IsTheta.isTheta_congr_left, Complex.isTheta_ofReal
-- Module: Mathlib.Analysis.Complex.Asymptotics
Goal:
α : Type u_1
E : Type u_2
inst : Norm E
l : Filter α
f : α → E
g : α → ℝ
⊢ (Asymptotics.IsTheta (F := ℂ) l f fun (x : α) ↦ (↑(g x) : ℂ)) ↔ f =Θ[l] g

Tactic:
(isTheta_ofReal g l).isTheta_congr_right

Premises used: Complex.isTheta_ofReal, Asymptotics.IsTheta.isTheta_congr_right
-- Module: Mathlib.Analysis.Complex.Asymptotics
Goal:
f g : ℂ → ℂ
x : ℝ
h : f =O[𝓝 (↑x : ℂ)] g
⊢ Asymptotics.IsBigO (E := ℂ) (F := ℂ) (𝓝 x) (fun (y : ℝ) ↦ f (↑y : ℂ)) fun (y : ℝ) ↦ g (↑y : ℂ)

Tactic:
h.comp_tendsto <| continuous_ofReal.tendsto x

Premises used: Continuous.tendsto, Complex.continuous_ofReal, Asymptotics.IsBigO.comp_tendsto
-- Module: Mathlib.Analysis.Complex.Asymptotics
Goal:
f g : ℂ → ℂ
x : ℝ
h : f =O[𝓝[≠] (↑x : ℂ)] g
x_1 : ℝ
h_1 : Membership.mem (γ := Set ℝ) {x}ᶜ x_1
⊢ Membership.mem (γ := Set ℂ) {(↑x : ℂ)}ᶜ (↑x_1 : ℂ)

Tactic:
simp_all
-- Module: Mathlib.Analysis.Complex.Asymptotics
Goal:
z : ℂ
⊢ Asymptotics.IsBigO (E := ℝ) (F := ℂ) (𝓝 z) (fun (w : ℂ) ↦ w.re - z.re) fun (w : ℂ) ↦ w - z

Tactic:
Asymptotics.isBigO_of_le _ fun w ↦ abs_re_le_norm (w - z)

Premises used: HSub.hSub, Complex.abs_re_le_norm, Asymptotics.isBigO_of_le
-- Module: Mathlib.Analysis.Complex.Asymptotics
Goal:
z : ℂ
⊢ Asymptotics.IsBigO (E := ℝ) (F := ℂ) (𝓝 z) (fun (w : ℂ) ↦ w.im - z.im) fun (w : ℂ) ↦ w - z

Tactic:
Asymptotics.isBigO_of_le _ fun w ↦ abs_im_le_norm (w - z)

Premises used: HSub.hSub, Complex.abs_im_le_norm, Asymptotics.isBigO_of_le
-- Module: Mathlib.Analysis.Complex.Asymptotics
Goal:
h : EventuallyEq (β := ℝ) cofinite (fun (x : ℤ) ↦ norm (E := ℂ) (↑x : ℂ)) fun (x : ℤ) ↦ norm (E := ℝ) (↑x : ℝ)
⊢ Asymptotics.IsTheta (E := ℂ) (F := ℝ) cofinite Int.cast Int.cast

Tactic:
apply Asymptotics.IsTheta.of_norm_eventuallyEq_norm

Premises used: Asymptotics.IsTheta.of_norm_eventuallyEq_norm
-- Module: Mathlib.Analysis.Complex.Asymptotics
Goal:
n : ℤ
⊢ norm (E := ℂ) (↑n : ℂ) = norm (E := ℝ) (↑n : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Asymptotics
Goal:
h :
  ∀ (a : ℤ),
    Membership.mem (γ := Set ℤ)
      {x : ℤ |
        (fun (x : ℤ) ↦
            Eq (α := ℝ) ((fun (x : ℤ) ↦ norm (E := ℂ) (↑x : ℂ)) x) ((fun (x : ℤ) ↦ norm (E := ℝ) (↑x : ℝ)) x))
          x}
      a
h₁ h₂ : ∀ (n : ℤ), norm (E := ℂ) (↑n : ℂ) = norm (E := ℝ) (↑n : ℝ)
⊢ EventuallyEq (β := ℝ) cofinite (fun (x : ℤ) ↦ norm (E := ℂ) (↑x : ℂ)) fun (x : ℤ) ↦ norm (E := ℝ) (↑x : ℝ)

Tactic:
filter_upwards with n using by simp
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
r₁ r₂ : ℝ
h₀ : 0 ≤ r₁
hr : r₁ < r₂
x : ℝ
h : r₁ < x ∧ x < r₂
rwa : r₁ < ‖x‖ ∧ ‖x‖ < r₂
rwa₁ rwa₂ rwa₃ rwa₄ : r₁ < x ∧ x < r₂
⊢ r₁ < ‖(↑x : ℂ)‖ ∧ ‖(↑x : ℂ)‖ < r₂

Tactic:
rwa [norm_real, Real.norm_of_nonneg (h₀.trans_lt h.1).le]

Premises used: LT.lt.le, Complex.norm_real, And.left, LE.le.trans_lt, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
R : Type u_1
inst : NormedField R
inst_1 : NormedAlgebra R ℝ
r : R
x : ℂ
rw : ‖HSMul.hSMul (α := ℝ) ((algebraMap R ℝ : (a : R) → ℝ) r : ℝ) x‖ ≤ ‖r‖ * ‖x‖
rw₁ : ‖(↑((algebraMap R ℝ : (a : R) → ℝ) r) : ℂ) * x‖ ≤ ‖r‖ * ‖x‖
rw₂ : ‖(↑((algebraMap R ℝ : (a : R) → ℝ) r) : ℂ)‖ * ‖x‖ ≤ ‖r‖ * ‖x‖
rw₃ : norm (E := ℝ) ((algebraMap R ℝ : (a : R) → ℝ) r : ℝ) * ‖x‖ ≤ ‖r‖ * ‖x‖
rw₄ rw₅ : ‖r‖ * ‖x‖ ≤ ‖r‖ * ‖x‖
⊢ ‖r • x‖ ≤ ‖r‖ * ‖x‖

Tactic:
rw [← algebraMap_smul ℝ r x, real_smul, norm_mul, norm_real, norm_algebraMap']

Premises used: Complex.real_smul, Real, algebraMap_smul, norm_mul, Complex.norm_real, norm_algebraMap'
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
n : ℤ
a : (↑(nnnorm (E := ℂ) (↑n : ℂ)) : ℝ) = (↑‖n‖₊ : ℝ)
⊢ nnnorm (E := ℂ) (↑n : ℂ) = ‖n‖₊

Tactic:
ext
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
n : ℤ
⊢ (↑(nnnorm (E := ℂ) (↑n : ℂ)) : ℝ) = (↑‖n‖₊ : ℝ)

Tactic:
norm_intCast n

Premises used: abs, Complex.norm_intCast, NNReal.toReal
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
n : ℤ
⊢ (↑(nnnorm (E := ℂ) (↑n : ℂ)) : ℝ) = (↑‖n‖₊ : ℝ)

Tactic:
exact norm_intCast n

Premises used: Complex.norm_intCast
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
⊢ Continuous (X := ℂ) (Y := ℝ) (⇑normSq : (a : ℂ) → ℝ)

Tactic:
simpa [← Complex.normSq_eq_norm_sq] using continuous_norm (E := ℂ).pow 2

Premises used: Continuous.pow, Complex.normSq_eq_norm_sq, OfNat.ofNat, continuous_norm
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
ζ : ℂ
n : ℕ
h : ζ ^ n = 1
hn : n ≠ 0
rw : ‖ζ ^ n‖₊ = HPow.hPow (α := NNReal) 1 n
rw₁ : nnnorm (E := ℂ) 1 = HPow.hPow (α := NNReal) 1 n
rw₂ : 1 = HPow.hPow (α := NNReal) 1 n
rw₃ rw₄ : Eq (α := NNReal) 1 1
⊢ ‖ζ‖₊ ^ n = HPow.hPow (α := NNReal) 1 n

Tactic:
rw [← nnnorm_pow, h, nnnorm_one, one_pow]

Premises used: one_pow, nnnorm_one, nnnorm_pow
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
ζ : ℂ
n : ℕ
h : ζ ^ n = 1
hn : n ≠ 0
⊢ ‖ζ‖ = 1

Tactic:
congr_arg Subtype.val (nnnorm_eq_one_of_pow_eq_one h hn)

Premises used: congr_arg, Subtype.val, Complex.nnnorm_eq_one_of_pow_eq_one
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
ι : Type u_2
a b : ℝ
f : ι → ℂ
s : Finset ι
ha₀ : 0 ≤ a
ha : (↑a : ℂ) = ∑ i ∈ s, f i
hb : (↑b : ℂ) = ∑ i ∈ s, (↑‖f i‖ : ℂ)
⊢ b = ∑ i ∈ s, ‖f i‖

Tactic:
norm_cast at hb
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
ι : Type u_2
a b : ℝ
f : ι → ℂ
s : Finset ι
ha₀ : 0 ≤ a
ha : (↑a : ℂ) = ∑ i ∈ s, f i
hb : b = ∑ i ∈ s, ‖f i‖
rw : norm (E := ℂ) (∑ i ∈ s, f i) ≤ ∑ i ∈ s, ‖f i‖
⊢ a ≤ b

Tactic:
rw [← Complex.norm_of_nonneg ha₀, ha, hb]

Premises used: Complex.norm_of_nonneg
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
ι : Type u_2
a b : ℝ
f : ι → ℂ
s : Finset ι
ha₀ : 0 ≤ a
ha : (↑a : ℂ) = ∑ i ∈ s, f i
hb : b = ∑ i ∈ s, ‖f i‖
⊢ norm (E := ℂ) (∑ i ∈ s, f i) ≤ ∑ i ∈ s, ‖f i‖

Tactic:
norm_sum_le s f

Premises used: norm_sum_le
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
ι : Type u_2
a b : ℝ
f : ι → ℂ
s : Finset ι
ha₀ : 0 ≤ a
ha : (↑a : ℂ) = ∑ i ∈ s, f i
hb : b = ∑ i ∈ s, ‖f i‖
⊢ norm (E := ℂ) (∑ i ∈ s, f i) ≤ ∑ i ∈ s, ‖f i‖

Tactic:
exact norm_sum_le s f

Premises used: norm_sum_le
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
⊢ norm (E := ℝ × ℝ) ((equivRealProd : (a : ℂ) → ℝ × ℝ) z : ℝ × ℝ) ≤ ‖z‖

Tactic:
simp [Prod.norm_def, abs_re_le_norm, abs_im_le_norm]

Premises used: Complex.abs_im_le_norm, Prod.norm_def, Complex.abs_re_le_norm
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
⊢ norm (E := ℝ × ℝ) ((equivRealProd : (a : ℂ) → ℝ × ℝ) z : ℝ × ℝ) ≤ 1 * ‖z‖

Tactic:
simpa using equivRealProd_apply_le z

Premises used: Complex.equivRealProd_apply_le
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
⊢ ‖z‖ ≤
    (↑((NNReal.sqrt : (a : NNReal) → NNReal) 2) : ℝ) * norm (E := ℝ × ℝ) ((equivRealProdLm : (a : ℂ) → ℝ × ℝ) z : ℝ × ℝ)

Tactic:
simpa only [Real.coe_sqrt, NNReal.coe_ofNat] using norm_le_sqrt_two_mul_max z

Premises used: NNReal.coe_ofNat, Real.coe_sqrt, Complex.norm_le_sqrt_two_mul_max
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
⊢ IsUniformEmbedding (α := ℂ) (β := ℝ × ℝ) (⇑equivRealProd : (a : ℂ) → ℝ × ℝ)

Tactic:
antilipschitz_equivRealProd.isUniformEmbedding lipschitz_equivRealProd.uniformContinuous

Premises used: Complex.lipschitz_equivRealProd, AntilipschitzWith.isUniformEmbedding, Set.Mem, setOf, Complex.antilipschitz_equivRealProd, LipschitzWith.uniformContinuous
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℂ E
⊢ CompleteSpace ℂ

Tactic:
(completeSpace_congr isUniformEmbedding_equivRealProd).mpr inferInstance

Premises used: Iff.mpr, completeSpace_congr, inferInstance, Complex.isUniformEmbedding_equivRealProd
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℂ E
⊢ T2Space ℂ

Tactic:
TopologicalSpace.t2Space_of_metrizableSpace

Premises used: TopologicalSpace.t2Space_of_metrizableSpace
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
p : ℝ × ℝ
⊢ (equivRealProdCLM.symm : (a : ℝ × ℝ) → ℂ) p = (↑p.1 : ℂ) + (↑p.2 : ℂ) * I

Tactic:
Complex.equivRealProd_symm_apply p

Premises used: Complex.equivRealProd_symm_apply
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℂ E
⊢ ProperSpace ℂ

Tactic:
lipschitz_equivRealProd.properSpace
  equivRealProdCLM.toHomeomorph.isProperMap

Premises used: Complex.lipschitz_equivRealProd, LipschitzWith.properSpace, Homeomorph.isProperMap, Complex.equivRealProdCLM, ContinuousLinearEquiv.toHomeomorph
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
⊢ Tendsto (β := ℝ) (⇑normSq : (a : ℂ) → ℝ) (cocompact ℂ) atTop

Tactic:
simpa [norm_mul_self_eq_normSq]
    using tendsto_norm_cocompact_atTop.atTop_mul_atTop₀ (tendsto_norm_cocompact_atTop (E := ℂ))

Premises used: Complex.norm_mul_self_eq_normSq, Filter.Tendsto.atTop_mul_atTop₀, tendsto_norm_cocompact_atTop
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℂ E
x : ℂ
⊢ norm (E := ℝ) ((reLm : (a : ℂ) → ℝ) x : ℝ) ≤ 1 * ‖x‖

Tactic:
simp [abs_re_le_norm]

Premises used: Complex.abs_re_le_norm
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
⊢ Continuous re

Tactic:
reCLM.continuous

Premises used: ContinuousLinearMap.continuous, Complex.reCLM
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
⊢ UniformContinuous re

Tactic:
reCLM.uniformContinuous

Premises used: ContinuousLinearMap.uniformContinuous, Complex.reCLM
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
⊢ (↑reCLM : ℂ →ₗ[ℝ] ℝ) = reLm

Tactic:
rfl

Premises used: Complex.reLm, rfl
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
⊢ (reCLM : (a : ℂ) → ℝ) z = z.re

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℂ E
x : ℂ
⊢ norm (E := ℝ) ((imLm : (a : ℂ) → ℝ) x : ℝ) ≤ 1 * ‖x‖

Tactic:
simp [abs_im_le_norm]

Premises used: Complex.abs_im_le_norm
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
⊢ Continuous im

Tactic:
imCLM.continuous

Premises used: ContinuousLinearMap.continuous, Complex.imCLM
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
⊢ UniformContinuous im

Tactic:
imCLM.uniformContinuous

Premises used: ContinuousLinearMap.uniformContinuous, Complex.imCLM
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
⊢ (↑imCLM : ℂ →ₗ[ℝ] ℝ) = imLm

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℂ E
x : E
h :
  ∀ (a b : ℝ),
    Eq (α := E) ((restrictScalars ℝ (toSpanSingleton ℂ x) : (a : ℂ) → E) { re := a, im := b : ℂ } : E)
      ((reCLM.smulRight x + HSMul.hSMul (β := ℂ →L[ℝ] E) I (imCLM.smulRight x) : (a : ℂ) → E) { re := a, im := b : ℂ } :
        E)
⊢ restrictScalars ℝ (toSpanSingleton ℂ x) = reCLM.smulRight x + HSMul.hSMul (β := ℂ →L[ℝ] E) I (imCLM.smulRight x)

Tactic:
ext ⟨a, b⟩
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℂ E
x : E
a b : ℝ
⊢ Eq (α := E) ((restrictScalars ℝ (toSpanSingleton ℂ x) : (a : ℂ) → E) { re := a, im := b : ℂ } : E)
    ((reCLM.smulRight x + HSMul.hSMul (β := ℂ →L[ℝ] E) I (imCLM.smulRight x) : (a : ℂ) → E) { re := a, im := b : ℂ } :
      E)

Tactic:
simp [map_add, mk_eq_add_mul_I, mul_smul, smul_comm I b x]

Premises used: Complex.mk_eq_add_mul_I, map_add, SMulCommClass.smul_comm, SemigroupAction.mul_smul, Complex.I
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
x : ℂ
h :
  ∀ (z : ℂ),
    Eq (α := ℂ) ((restrictScalars ℝ (toSpanSingleton ℂ x) : (a : ℂ) → ℂ) z : ℂ)
      ((HSMul.hSMul (β := ℂ →L[ℝ] ℂ) x 1 : (a : ℂ) → ℂ) z : ℂ)
⊢ restrictScalars ℝ (toSpanSingleton ℂ x) = HSMul.hSMul (β := ℂ →L[ℝ] ℂ) x 1

Tactic:
ext1 z
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
x z : ℂ
h : z * x = x * z
⊢ Eq (α := ℂ) ((restrictScalars ℝ (toSpanSingleton ℂ x) : (a : ℂ) → ℂ) z : ℂ)
    ((HSMul.hSMul (β := ℂ →L[ℝ] ℂ) x 1 : (a : ℂ) → ℂ) z : ℂ)

Tactic:
dsimp
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
x z : ℂ
⊢ z * x = x * z

Tactic:
apply mul_comm

Premises used: mul_comm
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
⊢ Eq (α := ℂ) ((conjLIE : (a : ℂ) → ℂ) z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ)

Tactic:
rfl

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

Tactic:
rfl

Premises used: LinearEquiv.symm, LinearIsometryEquiv.symm, Complex.conjLIE, AlgEquiv.toLinearEquiv, rfl
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
⊢ Isometry (α := ℂ) (β := ℂ) (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ)

Tactic:
conjLIE.isometry

Premises used: LinearIsometryEquiv.isometry, Complex.conjLIE
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z w : ℂ
⊢ dist (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) = dist z w

Tactic:
isometry_conj.dist_eq z w

Premises used: Complex.isometry_conj, Isometry.dist_eq
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z w : ℂ
⊢ nndist (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) = nndist z w

Tactic:
isometry_conj.nndist_eq z w

Premises used: Complex.isometry_conj, Isometry.nndist_eq
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z w : ℂ
rw :
  dist (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) : ℂ)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) =
    dist z ((starRingEnd ℂ : (a : ℂ) → ℂ) w)
rw₁ rw₂ : dist z ((starRingEnd ℂ : (a : ℂ) → ℂ) w) = dist z ((starRingEnd ℂ : (a : ℂ) → ℂ) w)
⊢ dist ((starRingEnd ℂ : (a : ℂ) → ℂ) z) w = dist z ((starRingEnd ℂ : (a : ℂ) → ℂ) w)

Tactic:
rw [← dist_conj_conj, conj_conj]

Premises used: Complex.dist_conj_conj, Complex.conj_conj
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z w : ℂ
⊢ nndist ((starRingEnd ℂ : (a : ℂ) → ℂ) z) w = nndist z ((starRingEnd ℂ : (a : ℂ) → ℂ) w)

Tactic:
Subtype.ext <| dist_conj_comm _ _

Premises used: NNReal, Complex.dist_conj_comm, Subtype.ext
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℂ E
⊢ ContinuousStar ℂ

Tactic:
⟨conjLIE.continuous⟩

Premises used: ContinuousStar.mk, Complex.conjLIE, LinearIsometryEquiv.continuous
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
⊢ Continuous (X := ℂ) (Y := ℂ) (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ)

Tactic:
continuous_star

Premises used: ContinuousStar.continuous_star
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
f : ℂ →+* ℂ
hf : Continuous (X := ℂ) (Y := ℂ) (⇑f : (a : ℂ) → ℂ)
⊢ f = RingHom.id ℂ ∨ f = starRingEnd ℂ

Tactic:
simpa only [DFunLike.ext_iff] using real_algHom_eq_id_or_conj (AlgHom.mk' f (map_real_smul f hf))

Premises used: Complex.real_algHom_eq_id_or_conj, DFunLike.ext_iff, map_real_smul, AlgHom.mk'
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
⊢ (↑conjLIE : ℂ ≃L[ℝ] ℂ) = conjCLE

Tactic:
rfl

Premises used: ContinuousAlgEquiv.toContinuousLinearEquiv, LinearIsometryEquiv.toContinuousLinearEquiv, rfl
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
⊢ conjCAE.toAlgEquiv = conjAe

Tactic:
rfl

Premises used: Complex.conjAe, rfl
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
⊢ (↑conjCLE : ℂ ≃ₗ[ℝ] ℂ) = (↑conjAe : ℂ ≃ₗ[ℝ] ℂ)

Tactic:
rfl

Premises used: AlgEquiv.toLinearEquiv, rfl
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
⊢ (↑(↑conjCLE : ℂ ≃ₗ[ℝ] ℂ) : ℂ →ₗ[ℝ] ℂ) = conjAe.toLinearMap

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
⊢ Eq (α := ℂ) ((conjCAE : (a : ℂ) → ℂ) z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
⊢ Eq (α := ℂ) ((conjCLE : (a : ℂ) → ℂ) z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
⊢ conjCAE.toLinearMap = conjAe.toLinearMap

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
⊢ Isometry ofReal

Tactic:
ofRealLI.isometry

Premises used: LinearIsometry.isometry, Complex.ofRealLI
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
⊢ Continuous ofReal

Tactic:
ofRealLI.continuous

Premises used: LinearIsometry.continuous, Complex.ofRealLI
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
⊢ IsUniformEmbedding ofReal

Tactic:
ofRealLI.isometry.isUniformEmbedding

Premises used: LinearIsometry.isometry, Complex.ofRealLI, Isometry.isUniformEmbedding
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
⊢ IsUniformEmbedding.{0, u_2} (β := 𝕜) RCLike.ofReal

Tactic:
RCLike.ofRealLI.isometry.isUniformEmbedding

Premises used: RCLike.ofRealLI, LinearIsometry.isometry, Isometry.isUniformEmbedding
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
α : Type u_2
l : Filter α
f : α → ℝ
x : ℝ
⊢ Tendsto (fun (x : α) ↦ (↑(f x) : ℂ)) l (𝓝 (↑x : ℂ)) ↔ Tendsto f l (𝓝 x)

Tactic:
isUniformEmbedding_ofReal.isClosedEmbedding.tendsto_nhds_iff.symm

Premises used: Complex.isUniformEmbedding_ofReal, IsUniformEmbedding.isClosedEmbedding, Topology.IsClosedEmbedding.tendsto_nhds_iff, Iff.symm
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
α : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
l : Filter α
f : α → ℝ
x : ℝ
⊢ Tendsto.{u_2, u_3} (β := 𝕜) (fun (x : α) ↦ (↑(f x) : 𝕜)) l (𝓝 (↑x : 𝕜)) ↔ Tendsto f l (𝓝 x)

Tactic:
RCLike.isUniformEmbedding_ofReal.isClosedEmbedding.tendsto_nhds_iff.symm

Premises used: RCLike.isUniformEmbedding_ofReal, IsUniformEmbedding.isClosedEmbedding, Topology.IsClosedEmbedding.tendsto_nhds_iff, Iff.symm
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
α : Type u_2
l : Filter α
f : α → ℝ
x : ℝ
hf : Tendsto f l (𝓝 x)
⊢ Tendsto (fun (x : α) ↦ (↑(f x) : ℂ)) l (𝓝 (↑x : ℂ))

Tactic:
tendsto_ofReal_iff.mpr hf

Premises used: Iff.mpr, Filter.tendsto_ofReal_iff
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
f : ℝ →+* ℂ
h : Continuous (X := ℝ) (Y := ℂ) (⇑f : (a : ℝ) → ℂ)
⊢ (AlgHom.mk' f ⋯).toRingHom = AlgHom.toRingHom (Algebra.ofId ℝ ℂ)

Tactic:
congr_arg AlgHom.toRingHom <|
      Subsingleton.elim (AlgHom.mk' f <| map_real_smul f h) (Algebra.ofId ℝ ℂ)

Premises used: Real, map_real_smul, congr_arg, Algebra.ofId, AlgHom.toRingHom, AlgHom.mk', Complex, Subsingleton.elim
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
f : ℝ →+* ℂ
h : Continuous (X := ℝ) (Y := ℂ) (⇑f : (a : ℝ) → ℂ)
⊢ f = ofRealHom

Tactic:
convert!
    congr_arg AlgHom.toRingHom <|
      Subsingleton.elim (AlgHom.mk' f <| map_real_smul f h) (Algebra.ofId ℝ ℂ)

Premises used: Real, map_real_smul, congr_arg, Algebra.ofId, AlgHom.toRingHom, AlgHom.mk', Complex, Subsingleton.elim
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
⊢ (↑ofRealCLM : ℝ →ₗ[ℝ] ℂ) = ofRealAm.toLinearMap

Tactic:
rfl

Premises used: AlgHom.toLinearMap, rfl
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
x : ℝ
⊢ (ofRealCLM : (a : ℝ) → ℂ) x = (↑x : ℂ)

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
⊢ HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) = HPow.hPow (β := ℕ) (↑‖z‖ : ℂ) 2

Tactic:
RCLike.mul_conj z

Premises used: RCLike.mul_conj
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
⊢ HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) z = HPow.hPow (β := ℕ) (↑‖z‖ : ℂ) 2

Tactic:
RCLike.conj_mul z

Premises used: RCLike.conj_mul
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
hz : ‖z‖ = 1
⊢ z⁻¹ = (starRingEnd ℂ : (a : ℂ) → ℂ) z

Tactic:
RCLike.inv_eq_conj hz

Premises used: RCLike.inv_eq_conj
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
⊢ ∃ (c : ℂ), ‖c‖ = 1 ∧ (↑‖z‖ : ℂ) = c * z

Tactic:
RCLike.exists_norm_eq_mul_self _

Premises used: RCLike.exists_norm_eq_mul_self
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
⊢ ∃ (c : ℂ), ‖c‖ = 1 ∧ c * (↑‖z‖ : ℂ) = z

Tactic:
RCLike.exists_norm_mul_eq_self _

Premises used: RCLike.exists_norm_mul_eq_self
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
x : ℂ
rw : Eq (α := ℝ) ((RCLike.im : (a : ℂ) → ℝ) x : ℝ) (0 : ℝ) ↔ IsSelfAdjoint x
⊢ x.im = 0 ↔ IsSelfAdjoint x

Tactic:
rw [← RCLike.im_eq_complex_im]

Premises used: RCLike.im_eq_complex_im
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
x : ℂ
⊢ Eq (α := ℝ) ((RCLike.im : (a : ℂ) → ℝ) x : ℝ) (0 : ℝ) ↔ IsSelfAdjoint x

Tactic:
RCLike.im_eq_zero_iff_isSelfAdjoint

Premises used: RCLike.im_eq_zero_iff_isSelfAdjoint
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
x : ℂ
⊢ Eq (α := ℝ) ((RCLike.im : (a : ℂ) → ℝ) x : ℝ) (0 : ℝ) ↔ IsSelfAdjoint x

Tactic:
exact RCLike.im_eq_zero_iff_isSelfAdjoint

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

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
⊢ (RCLike.re : (a : ℂ) → ℝ) x = y ↔ x = (↑y : ℂ)

Tactic:
RCLike.re_eq_ofReal_of_isSelfAdjoint hx

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

Tactic:
exact RCLike.re_eq_ofReal_of_isSelfAdjoint hx

Premises used: RCLike.re_eq_ofReal_of_isSelfAdjoint