awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℝ A
F : ℂ →ₐ[ℝ] A
rw : Eq (α := A) ((F : (a : ℂ) → A) (I * I) : A) (-1 : A)
rw₁ : Eq (α := A) ((F : (a : ℂ) → A) (-1) : A) (-1 : A)
rw₂ : Eq (α := A) (-(F : (a : ℂ) → A) 1 : A) (-1 : A)
rw₃ rw₄ : Eq.{u_1 + 1} (α := A) (-1) (-1)
⊢ HMul.hMul (α := A) (β := A) ((F : (a : ℂ) → A) I : A) ((F : (a : ℂ) → A) I : A) = -1

Tactic:
rw [← map_mul, I_mul_I, map_neg, map_one]

Premises used: map_neg, map_mul, map_one, Complex.I_mul_I
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
⊢ liftAux I I_mul_I = AlgHom.id ℝ ℂ

Tactic:
algHom_ext <| liftAux_apply_I _ _

Premises used: Complex.liftAux_apply_I, Complex.algHom_ext
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
⊢ liftAux (-I) ⋯ = (↑conjAe : ℂ →ₐ[ℝ] ℂ)

Tactic:
algHom_ext <| (liftAux_apply_I _ _).trans conj_I.symm

Premises used: Complex.liftAux_apply_I, Complex.algHom_ext, Eq.symm, Complex.conj_I, Eq.trans
-- 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
a : ↥(skewAdjoint A)
⊢ Membership.mem (γ := AddSubgroup A) (selfAdjoint A) (-I • (↑a : A))

Tactic:
simp only [neg_smul, neg_mem_iff, selfAdjoint.mem_iff, star_smul, star_def, conj_I,
        star_val_eq, smul_neg, neg_neg]

Premises used: neg_mem_iff, neg_smul, Complex.star_def, StarModule.star_smul, neg_neg, smul_neg, skewAdjoint.star_val_eq, selfAdjoint.mem_iff, Complex.conj_I
-- 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
a b : ↥(skewAdjoint A)
a₁ :
  (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (selfAdjoint A) x) (-I • (↑(a + b) : A)) ⋯) :
      A) =
    (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (selfAdjoint A) x) (-I • (↑a : A)) ⋯ +
          Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (selfAdjoint A) x) (-I • (↑b : A)) ⋯) :
      A)
⊢ Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (selfAdjoint A) x) (-I • (↑(a + b) : A)) ⋯ =
    Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (selfAdjoint A) x) (-I • (↑a : A)) ⋯ +
      Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (selfAdjoint A) x) (-I • (↑b : A)) ⋯

Tactic:
ext
-- 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
a b : ↥(skewAdjoint A)
⊢ (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (selfAdjoint A) x) (-I • (↑(a + b) : A)) ⋯) :
      A) =
    (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (selfAdjoint A) x) (-I • (↑a : A)) ⋯ +
          Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (selfAdjoint A) x) (-I • (↑b : A)) ⋯) :
      A)

Tactic:
simp only [AddSubgroup.coe_add, smul_add, AddMemClass.mk_add_mk]

Premises used: AddSubgroup.coe_add, AddMemClass.mk_add_mk, smul_add
-- 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
a : ℝ
b : ↥(skewAdjoint A)
a₁ :
  (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (selfAdjoint A) x) (-I • (↑(a • b) : A)) ⋯) :
      A) =
    (↑(HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) a : ℝ)
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (selfAdjoint A) x) (-I • (↑b : A)) ⋯)) :
      A)
⊢ Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (selfAdjoint A) x) (-I • (↑(a • b) : A)) ⋯ =
    HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) a : ℝ)
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (selfAdjoint A) x) (-I • (↑b : A)) ⋯)

Tactic:
ext
-- 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
a : ℝ
b : ↥(skewAdjoint A)
a₁ : I • a • (↑b : A) = a • I • (↑b : A)
⊢ (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (selfAdjoint A) x) (-I • (↑(a • b) : A)) ⋯) :
      A) =
    (↑(HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) a : ℝ)
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (selfAdjoint A) x) (-I • (↑b : A)) ⋯)) :
      A)

Tactic:
simp only [neg_smul, skewAdjoint.val_smul, RingHom.id_apply,
      selfAdjoint.val_smul, smul_neg, neg_inj]

Premises used: neg_smul, RingHom.id_apply, skewAdjoint.val_smul, smul_neg, selfAdjoint.val_smul, neg_inj
-- 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
a : ℝ
b : ↥(skewAdjoint A)
a₁ a₂ : a • I • (↑b : A) = a • I • (↑b : A)
⊢ I • a • (↑b : A) = a • I • (↑b : A)

Tactic:
rw [smul_comm]

Premises used: SMulCommClass.smul_comm
-- 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
a : ↥(skewAdjoint A)
⊢ HSMul.hSMul (β := A) I
      (↑(((negISMul : ↥(skewAdjoint A) →ₗ[ℝ] ↥(selfAdjoint A)) : (a : ↥(skewAdjoint A)) → ↥(selfAdjoint A)) a) : A) =
    (↑a : A)

Tactic:
simp only [smul_smul, skewAdjoint.negISMul_apply_coe, neg_smul, smul_neg, I_mul_I, one_smul,
    neg_neg]

Premises used: neg_smul, smul_smul, neg_neg, smul_neg, skewAdjoint.negISMul_apply_coe, one_smul, Complex.I_mul_I
-- 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
a : A
unfold : (↑((selfAdjointPart ℝ : (a : A) → ↥(selfAdjoint A)) a) : A) = HSMul.hSMul (α := ℝ) 2⁻¹ (a + star a)
⊢ (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) = HSMul.hSMul (α := ℝ) 2⁻¹ (a + star a)

Tactic:
unfold realPart

Premises used: realPart
-- 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
a : A
⊢ (↑((selfAdjointPart ℝ : (a : A) → ↥(selfAdjoint A)) a) : A) = HSMul.hSMul (α := ℝ) 2⁻¹ (a + star a)

Tactic:
simp only [selfAdjointPart_apply_coe, invOf_eq_inv]

Premises used: selfAdjointPart_apply_coe, invOf_eq_inv
-- 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
a : A
unfold :
  (↑((((skewAdjoint.negISMul : ↥(skewAdjoint A) →ₗ[ℝ] ↥(selfAdjoint A)) ∘ₗ
                (skewAdjointPart ℝ : A →ₗ[ℝ] ↥(skewAdjoint A)) :
              A →ₗ[ℝ] ↥(selfAdjoint A)) :
            (a : A) → ↥(selfAdjoint A))
          a) :
      A) =
    -I • HSMul.hSMul (α := ℝ) 2⁻¹ (a - star a)
⊢ (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) = -I • HSMul.hSMul (α := ℝ) 2⁻¹ (a - star a)

Tactic:
unfold imaginaryPart

Premises used: 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
a : A
⊢ (↑((((skewAdjoint.negISMul : ↥(skewAdjoint A) →ₗ[ℝ] ↥(selfAdjoint A)) ∘ₗ
                (skewAdjointPart ℝ : A →ₗ[ℝ] ↥(skewAdjoint A)) :
              A →ₗ[ℝ] ↥(selfAdjoint A)) :
            (a : A) → ↥(selfAdjoint A))
          a) :
      A) =
    -I • HSMul.hSMul (α := ℝ) 2⁻¹ (a - star a)

Tactic:
simp only [LinearMap.coe_comp, Function.comp_apply, skewAdjoint.negISMul_apply_coe,
    skewAdjointPart_apply_coe, invOf_eq_inv, neg_smul]

Premises used: neg_smul, skewAdjoint.negISMul_apply_coe, skewAdjointPart_apply_coe, LinearMap.coe_comp, Function.comp_apply, invOf_eq_inv
-- 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
a : A
⊢ (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) +
      HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) =
    a

Tactic:
simpa only [smul_smul, realPart_apply_coe, imaginaryPart_apply_coe, neg_smul, I_mul_I, one_smul,
    neg_sub, add_add_sub_cancel, smul_sub, smul_add, neg_sub_neg, invOf_eq_inv] using
    invOf_two_smul_add_invOf_two_smul ℝ a

Premises used: neg_smul, Real, neg_sub, smul_smul, add_add_sub_cancel, invOf_two_smul_add_invOf_two_smul, one_smul, imaginaryPart_apply_coe, smul_sub, Complex.I_mul_I, neg_sub_neg, invOf_eq_inv, realPart_apply_coe, smul_add
-- 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
a : A
a₁ :
  Eq.{u_1 + 1} (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (I • a)) : A)
    (↑(-((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
⊢ Eq (α := ↥(selfAdjoint A)) (((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (I • a) : ↥(selfAdjoint A))
    (-((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a : ↥(selfAdjoint A))

Tactic:
ext
-- 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
a : A
⊢ Eq.{u_1 + 1} (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (I • a)) : A)
    (↑(-((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)

Tactic:
simp [realPart_apply_coe, imaginaryPart_apply_coe, smul_comm I, sub_eq_add_neg, add_comm]

Premises used: sub_eq_add_neg, add_comm, imaginaryPart_apply_coe, realPart_apply_coe, SMulCommClass.smul_comm, Complex.I
-- 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
a : A
a₁ :
  Eq.{u_1 + 1} (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (I • a)) : A)
    (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
⊢ Eq (α := ↥(selfAdjoint A)) (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (I • a) : ↥(selfAdjoint A))
    (((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a : ↥(selfAdjoint A))

Tactic:
ext
-- 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
a : A
⊢ Eq.{u_1 + 1} (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (I • a)) : A)
    (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)

Tactic:
simp [realPart_apply_coe, imaginaryPart_apply_coe, smul_comm I (2⁻¹ : ℝ), smul_smul I]

Premises used: smul_smul, imaginaryPart_apply_coe, Inv.inv, realPart_apply_coe, SMulCommClass.smul_comm, OfNat.ofNat, Complex.I
-- 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
z : ℂ
a : A
⊢ Eq (α := ↥(selfAdjoint A)) (((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (z • a) : ↥(selfAdjoint A))
    (((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (((↑z.re : ℂ) + (↑z.im : ℂ) * I) • a) :
      ↥(selfAdjoint A))

Tactic:
congrm (ℜ ($((re_add_im z).symm) • a))
-- 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
z : ℂ
a : A
⊢ Eq (α := ↥(selfAdjoint A)) (((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (z • a) : ↥(selfAdjoint A))
    (((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (((↑z.re : ℂ) + (↑z.im : ℂ) * I) • a) :
      ↥(selfAdjoint A))

Tactic:
have := by congrm (ℜ ($((re_add_im z).symm) • a))
-- 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
z : ℂ
a : A
this :
  Eq (α := ↥(selfAdjoint A)) (((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (z • a) : ↥(selfAdjoint A))
    (((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (((↑z.re : ℂ) + (↑z.im : ℂ) * I) • a) :
      ↥(selfAdjoint A))
⊢ ((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (z • a) =
    HSMul.hSMul (β := ↥(selfAdjoint A)) z.re
        (((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a : ↥(selfAdjoint A)) -
      HSMul.hSMul (β := ↥(selfAdjoint A)) z.im
        (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a : ↥(selfAdjoint A))

Tactic:
simpa [-re_add_im, add_smul, ← smul_smul, sub_eq_add_neg]

Premises used: sub_eq_add_neg, smul_smul, add_smul, Complex.re_add_im
-- 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
z : ℂ
a : A
⊢ Eq (α := ↥(selfAdjoint A)) (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (z • a) : ↥(selfAdjoint A))
    (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (((↑z.re : ℂ) + (↑z.im : ℂ) * I) • a) :
      ↥(selfAdjoint A))

Tactic:
congrm (ℑ ($((re_add_im z).symm) • a))
-- 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
z : ℂ
a : A
⊢ Eq (α := ↥(selfAdjoint A)) (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (z • a) : ↥(selfAdjoint A))
    (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (((↑z.re : ℂ) + (↑z.im : ℂ) * I) • a) :
      ↥(selfAdjoint A))

Tactic:
have := by congrm (ℑ ($((re_add_im z).symm) • a))
-- 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
z : ℂ
a : A
this :
  Eq (α := ↥(selfAdjoint A)) (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (z • a) : ↥(selfAdjoint A))
    (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (((↑z.re : ℂ) + (↑z.im : ℂ) * I) • a) :
      ↥(selfAdjoint A))
⊢ ((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (z • a) =
    HSMul.hSMul (β := ↥(selfAdjoint A)) z.re
        (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a : ↥(selfAdjoint A)) +
      HSMul.hSMul (β := ↥(selfAdjoint A)) z.im
        (((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a : ↥(selfAdjoint A))

Tactic:
simpa [-re_add_im, add_smul, ← smul_smul]

Premises used: smul_smul, add_smul, Complex.re_add_im
-- 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
⊢ (↑((skewAdjointPart ℝ : (a : A) → ↥(skewAdjoint A)) x) : A) =
    HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)

Tactic:
simp [imaginaryPart_apply_coe, smul_smul]

Premises used: smul_smul, imaginaryPart_apply_coe
-- 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
⊢ (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) =
    HSMul.hSMul (β := A) (-I) (↑((skewAdjointPart ℝ : (a : A) → ↥(skewAdjoint A)) x) : A)

Tactic:
rfl

Premises used: rfl
-- 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
hx : IsSelfAdjoint x
⊢ (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) = x

Tactic:
hx.coe_selfAdjointPart_apply ℝ

Premises used: Real, IsSelfAdjoint.coe_selfAdjointPart_apply
-- 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
hx : IsSelfAdjoint x
rw :
  Eq (α := ↥(selfAdjoint A))
    ((((skewAdjoint.negISMul : ↥(skewAdjoint A) →ₗ[ℝ] ↥(selfAdjoint A)) ∘ₗ
              (skewAdjointPart ℝ : A →ₗ[ℝ] ↥(skewAdjoint A)) :
            A →ₗ[ℝ] ↥(selfAdjoint A)) :
          (a : A) → ↥(selfAdjoint A))
        x :
      ↥(selfAdjoint A))
    (0 : ↥(selfAdjoint A))
rw₁ :
  Eq (α := ↥(selfAdjoint A))
    (((skewAdjoint.negISMul : ↥(skewAdjoint A) →ₗ[ℝ] ↥(selfAdjoint A)) : (a : ↥(skewAdjoint A)) → ↥(selfAdjoint A))
        ((skewAdjointPart ℝ : (a : A) → ↥(skewAdjoint A)) x) :
      ↥(selfAdjoint A))
    (0 : ↥(selfAdjoint A))
rw₂ :
  Eq.{u_1 + 1} (α := ↥(selfAdjoint A))
    (((skewAdjoint.negISMul : ↥(skewAdjoint A) →ₗ[ℝ] ↥(selfAdjoint A)) : (a : ↥(skewAdjoint A)) → ↥(selfAdjoint A)) 0) 0
rw₃ rw₄ : Eq.{u_1 + 1} (α := ↥(selfAdjoint A)) 0 0
⊢ Eq (α := ↥(selfAdjoint A)) (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x : ↥(selfAdjoint A))
    (0 : ↥(selfAdjoint A))

Tactic:
rw [imaginaryPart, LinearMap.comp_apply, hx.skewAdjointPart_apply _, map_zero]

Premises used: LinearMap.comp_apply, IsSelfAdjoint.skewAdjointPart_apply, map_zero, IsSelfAdjoint.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
⊢ Eq (α := ↥(selfAdjoint.submodule ℝ A) →ₗ[ℝ] ↥(selfAdjoint A))
    (ℜ ∘ₗ Submodule.subtype (selfAdjoint.submodule ℝ A) : ↥(selfAdjoint.submodule ℝ A) →ₗ[ℝ] ↥(selfAdjoint A))
    (LinearMap.id : ↥(selfAdjoint.submodule ℝ A) →ₗ[ℝ] ↥(selfAdjoint.submodule ℝ A))

Tactic:
selfAdjointPart_comp_subtype_selfAdjoint ℝ

Premises used: Real, Set.Mem, selfAdjointPart_comp_subtype_selfAdjoint, realPart
-- 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
rw :
  Eq (α := ↥(selfAdjoint.submodule ℝ A) →ₗ[ℝ] ↥(selfAdjoint A))
    (((skewAdjoint.negISMul : ↥(skewAdjoint A) →ₗ[ℝ] ↥(selfAdjoint A)) ∘ₗ
          (skewAdjointPart ℝ : A →ₗ[ℝ] ↥(skewAdjoint A))) ∘ₗ
        Submodule.subtype (selfAdjoint.submodule ℝ A) :
      ↥(selfAdjoint.submodule ℝ A) →ₗ[ℝ] ↥(selfAdjoint A))
    (0 : ↥(selfAdjoint.submodule ℝ A) →ₗ[ℝ] ↥(selfAdjoint A))
rw₁ :
  Eq (α := ↥(selfAdjoint.submodule ℝ A) →ₗ[ℝ] ↥(selfAdjoint A))
    ((skewAdjoint.negISMul : ↥(skewAdjoint A) →ₗ[ℝ] ↥(selfAdjoint A)) ∘ₗ
        (skewAdjointPart ℝ ∘ₗ Submodule.subtype (selfAdjoint.submodule ℝ A) :
          ↥(selfAdjoint.submodule ℝ A) →ₗ[ℝ] ↥(skewAdjoint A)) :
      ↥(selfAdjoint.submodule ℝ A) →ₗ[ℝ] ↥(selfAdjoint A))
    (0 : ↥(selfAdjoint.submodule ℝ A) →ₗ[ℝ] ↥(selfAdjoint A))
rw₂ :
  Eq.{u_1 + 1} (α := ↥(selfAdjoint.submodule ℝ A) →ₗ[ℝ] ↥(selfAdjoint A))
    ((skewAdjoint.negISMul : ↥(skewAdjoint A) →ₗ[ℝ] ↥(selfAdjoint A)) ∘ₗ
        (0 : ↥(selfAdjoint.submodule ℝ A) →ₗ[ℝ] ↥(skewAdjoint A)) :
      ↥(selfAdjoint.submodule ℝ A) →ₗ[ℝ] ↥(selfAdjoint A))
    (0 : ↥(selfAdjoint.submodule ℝ A) →ₗ[ℝ] ↥(selfAdjoint A))
rw₃ rw₄ : Eq.{u_1 + 1} (α := ↥(selfAdjoint.submodule ℝ A) →ₗ[ℝ] ↥(selfAdjoint A)) 0 0
⊢ Eq (α := ↥(selfAdjoint.submodule ℝ A) →ₗ[ℝ] ↥(selfAdjoint A))
    (ℑ ∘ₗ Submodule.subtype (selfAdjoint.submodule ℝ A) : ↥(selfAdjoint.submodule ℝ A) →ₗ[ℝ] ↥(selfAdjoint A))
    (0 : ↥(selfAdjoint.submodule ℝ A) →ₗ[ℝ] ↥(selfAdjoint A))

Tactic:
rw [imaginaryPart, LinearMap.comp_assoc, skewAdjointPart_comp_subtype_selfAdjoint,
    LinearMap.comp_zero]

Premises used: LinearMap.comp_assoc, LinearMap.comp_zero, imaginaryPart, skewAdjointPart_comp_subtype_selfAdjoint
-- 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 : ↥(selfAdjoint A)
⊢ ((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (↑x : A) = x

Tactic:
Subtype.ext x.property.coe_realPart

Premises used: IsSelfAdjoint.coe_realPart, Subtype.property, Subtype.ext
-- 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 : ↥(selfAdjoint A)
⊢ Eq (α := ↥(selfAdjoint A)) (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (↑x : A) : ↥(selfAdjoint A))
    (0 : ↥(selfAdjoint A))

Tactic:
x.property.imaginaryPart

Premises used: IsSelfAdjoint.imaginaryPart, 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
⊢ Eq.{u_1 + 1} (α := ↥(selfAdjoint A))
    (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A))
      (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A))
    0

Tactic:
(ℜ x).property.imaginaryPart

Premises used: realPart, DFunLike.coe, IsSelfAdjoint.imaginaryPart, 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
⊢ Eq.{u_1 + 1} (α := ↥(selfAdjoint A))
    (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A))
      (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A))
    0

Tactic:
(ℑ x).property.imaginaryPart

Premises used: imaginaryPart, DFunLike.coe, IsSelfAdjoint.imaginaryPart, 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
⊢ Eq (α := ↥(selfAdjoint A))
    (((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A))
        (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) :
      ↥(selfAdjoint A))
    (((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x : ↥(selfAdjoint A))

Tactic:
Subtype.ext <| (ℜ x).property.coe_realPart

Premises used: IsSelfAdjoint.coe_realPart, realPart, DFunLike.coe, Subtype.property, Subtype.ext
-- 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))
        (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) :
      ↥(selfAdjoint A))
    (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x : ↥(selfAdjoint A))

Tactic:
Subtype.ext <| (ℑ x).property.coe_realPart

Premises used: imaginaryPart, IsSelfAdjoint.coe_realPart, DFunLike.coe, Subtype.property, Subtype.ext
-- 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
⊢ Function.Surjective.{u_1 + 1, u_1 + 1} (α := A) (β := ↥(selfAdjoint A))
    (⇑(ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A))

Tactic:
fun x ↦ ⟨(x : A), Subtype.ext x.property.coe_realPart⟩

Premises used: Exists.intro, IsSelfAdjoint.coe_realPart, Subtype.val, Function.Surjective, Subtype.property, Subtype.ext
-- 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 : ↥(selfAdjoint A)
⊢ (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (I • (↑x : A))) : A) = (↑x : A)

Tactic:
simp only [imaginaryPart_I_smul, x.property.coe_realPart]

Premises used: imaginaryPart_I_smul, IsSelfAdjoint.coe_realPart, Subtype.property