awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_1
inst : AddCommGroup A
inst_1 : Module ℂ A
inst_2 : StarAddMonoid A
inst_3 : StarModule ℂ A
x y : A
h₁ :
  Eq (α := ↥(selfAdjoint A)) (((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x : ↥(selfAdjoint A))
    (((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) y : ↥(selfAdjoint A))
h₂ :
  Eq (α := ↥(selfAdjoint A)) (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x : ↥(selfAdjoint A))
    (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) y : ↥(selfAdjoint A))
rw :
  (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
      HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) =
    y
rw₁ :
  (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
      HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) =
    (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) y) : A) +
      HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) y) : A)
rw₂ :
  (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) y) : A) +
      HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) =
    (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) y) : A) +
      HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) y) : A)
rw₃ rw₄ :
  (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) y) : A) +
      HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) y) : A) =
    (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) y) : A) +
      HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) y) : A)
⊢ x = y

Tactic:
rw [← realPart_add_I_smul_imaginaryPart x, ← realPart_add_I_smul_imaginaryPart y, h₁, h₂]

Premises used: realPart_add_I_smul_imaginaryPart
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_1
inst : AddCommGroup A
inst_1 : Module ℂ A
inst_2 : StarAddMonoid A
inst_3 : StarModule ℂ A
x y : A
⊢ x = y →
    Eq (α := ↥(selfAdjoint A)) (((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x : ↥(selfAdjoint A))
        (((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) y : ↥(selfAdjoint A)) ∧
      Eq (α := ↥(selfAdjoint A)) (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x : ↥(selfAdjoint A))
        (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) y : ↥(selfAdjoint A))

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_1
inst : AddCommGroup A
inst_1 : Module ℂ A
inst_2 : StarAddMonoid A
inst_3 : StarModule ℂ A
h :
  ∀ (x : A),
    Membership.mem (γ := Submodule ℝ A) (LinearMap.ker (M₂ := ↥(selfAdjoint A)) (ℑ : A →ₗ[ℝ] ↥(selfAdjoint A))) x ↔
      Membership.mem (γ := Submodule ℝ A) (selfAdjoint.submodule ℝ A) x
⊢ Eq (α := Submodule ℝ A) (LinearMap.ker (M₂ := ↥(selfAdjoint A)) (ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)))
    (selfAdjoint.submodule ℝ A)

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_1
inst : AddCommGroup A
inst_1 : Module ℂ A
inst_2 : StarAddMonoid A
inst_3 : StarModule ℂ A
x : A
h : x - star x = 0 ↔ star x = x
⊢ Membership.mem (γ := Submodule ℝ A) (LinearMap.ker (M₂ := ↥(selfAdjoint A)) (ℑ : A →ₗ[ℝ] ↥(selfAdjoint A))) x ↔
    Membership.mem (γ := Submodule ℝ A) (selfAdjoint.submodule ℝ A) x

Tactic:
simp [selfAdjoint.submodule, selfAdjoint.mem_iff, imaginaryPart, Subtype.ext_iff]

Premises used: imaginaryPart, Subtype.ext_iff, selfAdjoint.submodule, selfAdjoint.mem_iff
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_1
inst : AddCommGroup A
inst_1 : Module ℂ A
inst_2 : StarAddMonoid A
inst_3 : StarModule ℂ A
x : A
⊢ x - star x = 0 ↔ star x = x

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_1
inst : AddCommGroup A
inst_1 : Module ℂ A
inst_2 : StarAddMonoid A
inst_3 : StarModule ℂ A
x : A
⊢ Eq (α := ↥(selfAdjoint A)) (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x : ↥(selfAdjoint A))
      (0 : ↥(selfAdjoint A)) ↔
    IsSelfAdjoint x

Tactic:
simpa [-ker_imaginaryPart] using SetLike.ext_iff.mp ker_imaginaryPart x

Premises used: SetLike.ext_iff, ker_imaginaryPart, Iff.mp
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_1
inst : AddCommGroup A
inst_1 : Module ℂ A
inst_2 : StarAddMonoid A
inst_3 : StarModule ℂ A
⊢ Eq (α := Submodule ℂ A) (span ℂ (↑(selfAdjoint A) : Set A)) ⊤

Tactic:
eq_top_iff'.mpr fun x ↦ ?_

Premises used: Iff.mpr, Submodule.eq_top_iff'
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_1
inst : AddCommGroup A
inst_1 : Module ℂ A
inst_2 : StarAddMonoid A
inst_3 : StarModule ℂ A
refine : ∀ (x : A), Membership.mem (γ := Submodule ℂ A) (span ℂ (↑(selfAdjoint A) : Set A)) x
⊢ Eq (α := Submodule ℂ A) (span ℂ (↑(selfAdjoint A) : Set A)) ⊤

Tactic:
refine eq_top_iff'.mpr fun x ↦ ?_

Premises used: Iff.mpr, Submodule.eq_top_iff'
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_1
inst : AddCommGroup A
inst_1 : Module ℂ A
inst_2 : StarAddMonoid A
inst_3 : StarModule ℂ A
x : A
rw :
  Membership.mem (γ := Submodule ℂ A) (span ℂ (↑(selfAdjoint A) : Set A))
    ((↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
      HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A))
⊢ Membership.mem (γ := Submodule ℂ A) (span ℂ (↑(selfAdjoint A) : Set A)) x

Tactic:
rw [← realPart_add_I_smul_imaginaryPart x]

Premises used: realPart_add_I_smul_imaginaryPart
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_1
inst : AddCommGroup A
inst_1 : Module ℂ A
inst_2 : StarAddMonoid A
inst_3 : StarModule ℂ A
x : A
⊢ Membership.mem (γ := Submodule ℂ A) (span ℂ (↑(selfAdjoint A) : Set A))
    ((↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
      HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A))

Tactic:
add_mem (subset_span (ℜ x).property) <|
    SMulMemClass.smul_mem _ <| subset_span (ℑ x).property

Premises used: SMulMemClass.smul_mem, imaginaryPart, AddMemClass.add_mem, Submodule.subset_span, realPart, DFunLike.coe, Subtype.property
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_1
inst : AddCommGroup A
inst_1 : Module ℂ A
inst_2 : StarAddMonoid A
inst_3 : StarModule ℂ A
x : A
⊢ Membership.mem (γ := Submodule ℂ A) (span ℂ (↑(selfAdjoint A) : Set A))
    ((↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
      HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A))

Tactic:
exact add_mem (subset_span (ℜ x).property) <|
    SMulMemClass.smul_mem _ <| subset_span (ℑ x).property

Premises used: SMulMemClass.smul_mem, imaginaryPart, AddMemClass.add_mem, Submodule.subset_span, realPart, DFunLike.coe, Subtype.property
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_1
⊢ ∀ (x y : ↥(selfAdjoint ℂ)), (↑(x + y) : ℂ).re = (↑x : ℂ).re + (↑y : ℂ).re

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_1
⊢ ∀ (m : ℝ) (x : ↥(selfAdjoint ℂ)),
    (↑(m • x) : ℂ).re = HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) m : ℝ) (↑x : ℂ).re

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
z : ↥(selfAdjoint ℂ)
⊢ (↑((selfAdjointEquiv : (a : ↥(selfAdjoint ℂ)) → ℝ) z) : ℂ) = (↑z : ℂ)

Tactic:
simpa [selfAdjointEquiv_symm_apply]
    using (congr_arg Subtype.val <| Complex.selfAdjointEquiv.left_inv z)

Premises used: LinearEquiv.left_inv, congr_arg, Complex.selfAdjointEquiv, Complex.selfAdjointEquiv_symm_apply, Subtype.val
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
r : ℝ
rw : HSMul.hSMul (α := ℝ) 2⁻¹ (HSMul.hSMul (α := ℝ) 2 (↑r : ℂ)) = (↑r : ℂ)
⊢ (↑(((ℜ : ℂ →ₗ[ℝ] ↥(selfAdjoint ℂ)) : (a : ℂ) → ↥(selfAdjoint ℂ)) (↑r : ℂ)) : ℂ) = (↑r : ℂ)

Tactic:
rw [realPart_apply_coe, star_def, conj_ofReal, ← two_smul ℝ (r : ℂ)]

Premises used: Real, Complex.star_def, two_smul, Complex.ofReal, realPart_apply_coe, Complex.conj_ofReal
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
r : ℝ
⊢ HSMul.hSMul (α := ℝ) 2⁻¹ (HSMul.hSMul (α := ℝ) 2 (↑r : ℂ)) = (↑r : ℂ)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
r : ℝ
a : Eq (α := ℂ) (↑(((ℑ : ℂ →ₗ[ℝ] ↥(selfAdjoint ℂ)) : (a : ℂ) → ↥(selfAdjoint ℂ)) (↑r : ℂ)) : ℂ) (↑0 : ℂ)
⊢ Eq (α := ↥(selfAdjoint ℂ)) (((ℑ : ℂ →ₗ[ℝ] ↥(selfAdjoint ℂ)) : (a : ℂ) → ↥(selfAdjoint ℂ)) (↑r : ℂ) : ↥(selfAdjoint ℂ))
    (0 : ↥(selfAdjoint ℂ))

Tactic:
ext1
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
r : ℝ
⊢ Eq (α := ℂ) (↑(((ℑ : ℂ →ₗ[ℝ] ↥(selfAdjoint ℂ)) : (a : ℂ) → ↥(selfAdjoint ℂ)) (↑r : ℂ)) : ℂ) (↑0 : ℂ)

Tactic:
simp [imaginaryPart_apply_coe, conj_ofReal]

Premises used: imaginaryPart_apply_coe, Complex.conj_ofReal
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
z : ℂ
⊢ Eq (α := ℂ) (↑(((ℜ : ℂ →ₗ[ℝ] ↥(selfAdjoint ℂ)) : (a : ℂ) → ↥(selfAdjoint ℂ)) z) : ℂ)
    (↑(((ℜ : ℂ →ₗ[ℝ] ↥(selfAdjoint ℂ)) : (a : ℂ) → ↥(selfAdjoint ℂ)) ((↑z.re : ℂ) + (↑z.im : ℂ) * I)) : ℂ)

Tactic:
congrm (ℜ $((re_add_im z).symm))
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
z : ℂ
rw :
  HAdd.hAdd (α := ℂ) (↑(((ℜ : ℂ →ₗ[ℝ] ↥(selfAdjoint ℂ)) : (a : ℂ) → ↥(selfAdjoint ℂ)) (↑z.re : ℂ)) : ℂ)
      (↑(-((ℑ : ℂ →ₗ[ℝ] ↥(selfAdjoint ℂ)) : (a : ℂ) → ↥(selfAdjoint ℂ)) (↑z.im : ℂ)) : ℂ) =
    (↑z.re : ℂ)
⊢ (↑(((ℜ : ℂ →ₗ[ℝ] ↥(selfAdjoint ℂ)) : (a : ℂ) → ↥(selfAdjoint ℂ)) ((↑z.re : ℂ) + (↑z.im : ℂ) * I)) : ℂ) = (↑z.re : ℂ)

Tactic:
rw [map_add, AddSubmonoid.coe_add, mul_comm, ← smul_eq_mul, realPart_I_smul]

Premises used: AddSubmonoid.coe_add, map_add, realPart_I_smul, mul_comm, smul_eq_mul
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
z : ℂ
⊢ HAdd.hAdd (α := ℂ) (↑(((ℜ : ℂ →ₗ[ℝ] ↥(selfAdjoint ℂ)) : (a : ℂ) → ↥(selfAdjoint ℂ)) (↑z.re : ℂ)) : ℂ)
      (↑(-((ℑ : ℂ →ₗ[ℝ] ↥(selfAdjoint ℂ)) : (a : ℂ) → ↥(selfAdjoint ℂ)) (↑z.im : ℂ)) : ℂ) =
    (↑z.re : ℂ)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_1
inst : NonUnitalNonAssocRing A
inst_1 : StarRing A
inst_2 : Module ℂ A
inst_3 : IsScalarTower ℂ A A
inst_4 : SMulCommClass ℂ A A
inst_5 : StarModule ℂ A
a : A
a_eq :
  a =
    (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) +
      HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
⊢ HMul.hMul (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
            (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) +
          -(I •
              HMul.hMul (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
                (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)) +
        (I •
            HMul.hMul (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
              (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) +
          HMul.hMul (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
            (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)) +
      (HMul.hMul (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
            (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) +
          I •
            HMul.hMul (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
              (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) +
        (HMul.hMul (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
            (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) +
          -(I •
              HMul.hMul (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
                (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)))) =
    HSMul.hSMul (α := ℕ) 2
        (HMul.hMul (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
          (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)) +
      HSMul.hSMul (α := ℕ) 2
        (HMul.hMul (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
          (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A))

Tactic:
abel
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_1
inst : NonUnitalNonAssocRing A
inst_1 : StarRing A
inst_2 : Module ℂ A
inst_3 : IsScalarTower ℂ A A
inst_4 : SMulCommClass ℂ A A
inst_5 : StarModule ℂ A
a : A
a_eq :
  a =
    (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) +
      HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
⊢ HMul.hMul (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
            (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) +
          -(I •
              HMul.hMul (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
                (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)) +
        (I •
            HMul.hMul (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
              (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) +
          HMul.hMul (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
            (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)) -
      (HMul.hMul (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
            (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) +
          I •
            HMul.hMul (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
              (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) +
        (HMul.hMul (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
            (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) +
          -(I •
              HMul.hMul (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
                (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)))) =
    HSMul.hSMul (α := ℕ) 2
      (I •
        (HMul.hMul (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
            (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) -
          HMul.hMul (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
            (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)))

Tactic:
module
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_1
inst : NonUnitalNonAssocRing A
inst_1 : StarRing A
inst_2 : Module ℂ A
inst_3 : IsScalarTower ℂ A A
inst_4 : SMulCommClass ℂ A A
inst_5 : StarModule ℂ A
x : A
inst_6 : IsStarNormal x
⊢ Commute.{u_1} (S := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
    (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)

Tactic:
isStarNormal_iff_commute_realPart_imaginaryPart.mp inferInstance

Premises used: inferInstance, Iff.mp, isStarNormal_iff_commute_realPart_imaginaryPart
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_1
inst : NonUnitalNonAssocRing A
inst_1 : StarRing A
inst_2 : Module ℂ A
inst_3 : IsScalarTower ℂ A A
inst_4 : SMulCommClass ℂ A A
inst_5 : StarModule ℂ A
x : A
hx : IsStarNormal x
rw :
  star
      ((↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
        HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)) *
    ((↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
      HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A))
| star x * x

Tactic:
rw [← realPart_add_I_smul_imaginaryPart x]

Premises used: realPart_add_I_smul_imaginaryPart
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_1
inst : NonUnitalNonAssocRing A
inst_1 : StarRing A
inst_2 : Module ℂ A
inst_3 : IsScalarTower ℂ A A
inst_4 : SMulCommClass ℂ A A
inst_5 : StarModule ℂ A
x : A
hx : IsStarNormal x
conv_lhs :
  star
        ((↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
          HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)) *
      ((↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
        HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)) =
    HMul.hMul (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
          (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
        HMul.hMul (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
          (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
      I •
        (HMul.hMul (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
            (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) -
          HMul.hMul (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
            (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A))
⊢ star x * x =
    HMul.hMul (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
          (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
        HMul.hMul (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
          (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
      I •
        (HMul.hMul (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
            (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) -
          HMul.hMul (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
            (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A))

Tactic:
conv_lhs => rw [← realPart_add_I_smul_imaginaryPart x]

Premises used: realPart_add_I_smul_imaginaryPart
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_1
inst : NonUnitalNonAssocRing A
inst_1 : StarRing A
inst_2 : Module ℂ A
inst_3 : IsScalarTower ℂ A A
inst_4 : SMulCommClass ℂ A A
inst_5 : StarModule ℂ A
x : A
hx : IsStarNormal x
simp :
  HMul.hMul (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
          (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
        -(I •
            HMul.hMul (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
              (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)) +
      (I •
          HMul.hMul (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
            (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
        HMul.hMul (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
          (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)) =
    HMul.hMul (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
          (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
        HMul.hMul (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
          (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
      (I •
          HMul.hMul (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
            (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) -
        I •
          HMul.hMul (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
            (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A))
⊢ star
        ((↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
          HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)) *
      ((↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
        HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)) =
    HMul.hMul (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
          (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
        HMul.hMul (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
          (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
      I •
        (HMul.hMul (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
            (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) -
          HMul.hMul (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
            (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A))

Tactic:
simp [add_mul, mul_add, smul_mul_assoc, mul_smul_comm, smul_smul, smul_sub]

Premises used: add_mul, smul_smul, smul_mul_assoc, smul_sub, mul_smul_comm, mul_add
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_1
inst : NonUnitalNonAssocRing A
inst_1 : StarRing A
inst_2 : Module ℂ A
inst_3 : IsScalarTower ℂ A A
inst_4 : SMulCommClass ℂ A A
inst_5 : StarModule ℂ A
x : A
hx : IsStarNormal x
⊢ HMul.hMul (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
          (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
        -(I •
            HMul.hMul (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
              (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)) +
      (I •
          HMul.hMul (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
            (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
        HMul.hMul (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
          (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)) =
    HMul.hMul (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
          (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
        HMul.hMul (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
          (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
      (I •
          HMul.hMul (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
            (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) -
        I •
          HMul.hMul (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
            (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A))

Tactic:
grind