awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Star.Module
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : TrivialStar R
inst_3 : AddCommGroup A
inst_4 : Module R A
inst_5 : StarAddMonoid A
inst_6 : StarModule R A
inst_7 : Invertible (α := R) 2
x y : A
⊢ (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (selfAdjoint A) x)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
            (x + y + star (x + y)))
          ⋯) :
      A) =
    (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (selfAdjoint A) x)
            (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
              (x + star x))
            ⋯ +
          Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (selfAdjoint A) x)
            (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
              (y + star y))
            ⋯) :
      A)

Tactic:
simp [add_add_add_comm]

Premises used: add_add_add_comm
-- Module: Mathlib.Algebra.Star.Module
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : TrivialStar R
inst_3 : AddCommGroup A
inst_4 : Module R A
inst_5 : StarAddMonoid A
inst_6 : StarModule R A
inst_7 : Invertible (α := R) 2
r : R
x : A
a :
  (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (selfAdjoint A) x)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
            (r • x + star (r • x)))
          ⋯) :
      A) =
    (↑(HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R)
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (selfAdjoint A) x)
            (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
              (x + star x))
            ⋯)) :
      A)
⊢ Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (selfAdjoint A) x)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        (r • x + star (r • x)))
      ⋯ =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R)
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (selfAdjoint A) x)
        (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
          (x + star x))
        ⋯)

Tactic:
ext
-- Module: Mathlib.Algebra.Star.Module
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : TrivialStar R
inst_3 : AddCommGroup A
inst_4 : Module R A
inst_5 : StarAddMonoid A
inst_6 : StarModule R A
inst_7 : Invertible (α := R) 2
r : R
x : A
⊢ (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (selfAdjoint A) x)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
            (r • x + star (r • x)))
          ⋯) :
      A) =
    (↑(HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R)
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (selfAdjoint A) x)
            (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
              (x + star x))
            ⋯)) :
      A)

Tactic:
simp [← mul_smul, show ⅟2 * r = r * ⅟2 from Commute.invOf_left <| (2 : ℕ).cast_commute r]

Premises used: Commute.invOf_left, OfNat.ofNat, SemigroupAction.mul_smul, Nat.cast_commute
-- Module: Mathlib.Algebra.Star.Module
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : TrivialStar R
inst_3 : AddCommGroup A
inst_4 : Module R A
inst_5 : StarAddMonoid A
inst_6 : StarModule R A
inst_7 : Invertible (α := R) 2
x : A
⊢ Membership.mem (γ := AddSubgroup A) (skewAdjoint A)
    (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x - star x))

Tactic:
simp only [skewAdjoint.mem_iff, star_smul, star_sub, star_star, star_trivial, ← smul_neg,
        neg_sub]

Premises used: neg_sub, star_star, skewAdjoint.mem_iff, StarModule.star_smul, TrivialStar.star_trivial, smul_neg, star_sub
-- Module: Mathlib.Algebra.Star.Module
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : TrivialStar R
inst_3 : AddCommGroup A
inst_4 : Module R A
inst_5 : StarAddMonoid A
inst_6 : StarModule R A
inst_7 : Invertible (α := R) 2
x y : A
a :
  (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (skewAdjoint A) x)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
            (x + y - star (x + y)))
          ⋯) :
      A) =
    (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (skewAdjoint A) x)
            (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
              (x - star x))
            ⋯ +
          Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (skewAdjoint A) x)
            (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
              (y - star y))
            ⋯) :
      A)
⊢ Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (skewAdjoint A) x)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        (x + y - star (x + y)))
      ⋯ =
    Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (skewAdjoint A) x)
        (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
          (x - star x))
        ⋯ +
      Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (skewAdjoint A) x)
        (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
          (y - star y))
        ⋯

Tactic:
ext
-- Module: Mathlib.Algebra.Star.Module
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : TrivialStar R
inst_3 : AddCommGroup A
inst_4 : Module R A
inst_5 : StarAddMonoid A
inst_6 : StarModule R A
inst_7 : Invertible (α := R) 2
x y : A
⊢ (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (skewAdjoint A) x)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
            (x + y - star (x + y)))
          ⋯) :
      A) =
    (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (skewAdjoint A) x)
            (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
              (x - star x))
            ⋯ +
          Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (skewAdjoint A) x)
            (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
              (y - star y))
            ⋯) :
      A)

Tactic:
simp only [sub_add, ← smul_add, sub_sub_eq_add_sub, star_add, AddSubgroup.coe_add]

Premises used: sub_add, StarAddMonoid.star_add, sub_sub_eq_add_sub, AddSubgroup.coe_add, smul_add
-- Module: Mathlib.Algebra.Star.Module
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : TrivialStar R
inst_3 : AddCommGroup A
inst_4 : Module R A
inst_5 : StarAddMonoid A
inst_6 : StarModule R A
inst_7 : Invertible (α := R) 2
r : R
x : A
a :
  (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (skewAdjoint A) x)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
            (r • x - star (r • x)))
          ⋯) :
      A) =
    (↑(HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R)
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (skewAdjoint A) x)
            (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
              (x - star x))
            ⋯)) :
      A)
⊢ Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (skewAdjoint A) x)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        (r • x - star (r • x)))
      ⋯ =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R)
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (skewAdjoint A) x)
        (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
          (x - star x))
        ⋯)

Tactic:
ext
-- Module: Mathlib.Algebra.Star.Module
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : TrivialStar R
inst_3 : AddCommGroup A
inst_4 : Module R A
inst_5 : StarAddMonoid A
inst_6 : StarModule R A
inst_7 : Invertible (α := R) 2
r : R
x : A
⊢ (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (skewAdjoint A) x)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
            (r • x - star (r • x)))
          ⋯) :
      A) =
    (↑(HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R)
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (skewAdjoint A) x)
            (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
              (x - star x))
            ⋯)) :
      A)

Tactic:
simp [← mul_smul, ← smul_sub,
      show r * ⅟2 = ⅟2 * r from Commute.invOf_right <| (2 : ℕ).commute_cast r]

Premises used: Nat.commute_cast, Commute.invOf_right, smul_sub, OfNat.ofNat, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Star.Module
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : TrivialStar R
inst_3 : AddCommGroup A
inst_4 : Module R A
inst_5 : StarAddMonoid A
inst_6 : StarModule R A
inst_7 : Invertible (α := R) 2
x : A
⊢ HAdd.hAdd (α := A) (↑((selfAdjointPart R : (a : A) → ↥(selfAdjoint A)) x) : A)
      (↑((skewAdjointPart R : (a : A) → ↥(skewAdjoint A)) x) : A) =
    x

Tactic:
simp only [smul_sub, selfAdjointPart_apply_coe, smul_add, skewAdjointPart_apply_coe,
    add_add_sub_cancel, invOf_two_smul_add_invOf_two_smul]

Premises used: add_add_sub_cancel, invOf_two_smul_add_invOf_two_smul, smul_sub, skewAdjointPart_apply_coe, selfAdjointPart_apply_coe, smul_add
-- Module: Mathlib.Algebra.Star.Module
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : TrivialStar R
inst_3 : AddCommGroup A
inst_4 : Module R A
inst_5 : StarAddMonoid A
inst_6 : StarModule R A
inst_7 : Invertible (α := R) 2
x : A
hx : IsSelfAdjoint x
rw :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + star x) = x
rw₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + x) = x
rw₂ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) x +
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) x =
    x
rw₃ rw₄ : x = x
⊢ (↑((selfAdjointPart R : (a : A) → ↥(selfAdjoint A)) x) : A) = x

Tactic:
rw [selfAdjointPart_apply_coe, hx.star_eq, smul_add, invOf_two_smul_add_invOf_two_smul]

Premises used: invOf_two_smul_add_invOf_two_smul, selfAdjointPart_apply_coe, IsSelfAdjoint.star_eq, smul_add
-- Module: Mathlib.Algebra.Star.Module
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : TrivialStar R
inst_3 : AddCommGroup A
inst_4 : Module R A
inst_5 : StarAddMonoid A
inst_6 : StarModule R A
inst_7 : Invertible (α := R) 2
x : A
hx : IsSelfAdjoint x
⊢ (selfAdjointPart R : (a : A) → ↥(selfAdjoint A)) x =
    Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (selfAdjoint A) x) x hx

Tactic:
Subtype.ext (hx.coe_selfAdjointPart_apply R)

Premises used: IsSelfAdjoint.coe_selfAdjointPart_apply, Subtype.ext
-- Module: Mathlib.Algebra.Star.Module
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : TrivialStar R
inst_3 : AddCommGroup A
inst_4 : Module R A
inst_5 : StarAddMonoid A
inst_6 : StarModule R A
inst_7 : Invertible (α := R) 2
⊢ Eq (α := ↥(selfAdjoint.submodule R A) →ₗ[R] ↥(selfAdjoint A))
    (selfAdjointPart R ∘ₗ Submodule.subtype (selfAdjoint.submodule R A)) LinearMap.id

Tactic:
LinearMap.ext fun x ↦ x.2.selfAdjointPart_apply R

Premises used: IsSelfAdjoint.selfAdjointPart_apply, LinearMap.ext, Subtype.property
-- Module: Mathlib.Algebra.Star.Module
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : TrivialStar R
inst_3 : AddCommGroup A
inst_4 : Module R A
inst_5 : StarAddMonoid A
inst_6 : StarModule R A
inst_7 : Invertible (α := R) 2
x : A
hx : IsSelfAdjoint x
rw :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x - star x) =
    (↑0 : A)
rw₁ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x - x) = (↑0 : A)
rw₂ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) 0 =
    (↑0 : A)
rw₃ : Eq.{u_2 + 1} (α := A) 0 (↑0 : A)
rw₄ rw₅ : Eq.{u_2 + 1} (α := A) 0 0
⊢ Eq.{u_2 + 1} (α := A) (↑((skewAdjointPart R : (a : A) → ↥(skewAdjoint A)) x) : A) (↑0 : A)

Tactic:
rw [skewAdjointPart_apply_coe, hx.star_eq, sub_self, smul_zero, ZeroMemClass.coe_zero]

Premises used: sub_self, smul_zero, ZeroMemClass.coe_zero, skewAdjointPart_apply_coe, IsSelfAdjoint.star_eq
-- Module: Mathlib.Algebra.Star.Module
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : TrivialStar R
inst_3 : AddCommGroup A
inst_4 : Module R A
inst_5 : StarAddMonoid A
inst_6 : StarModule R A
inst_7 : Invertible (α := R) 2
⊢ Eq (α := ↥(selfAdjoint.submodule R A) →ₗ[R] ↥(skewAdjoint A))
    (skewAdjointPart R ∘ₗ Submodule.subtype (selfAdjoint.submodule R A)) 0

Tactic:
LinearMap.ext fun x ↦ x.2.skewAdjointPart_apply R

Premises used: LinearMap.ext, IsSelfAdjoint.skewAdjointPart_apply, Subtype.property
-- Module: Mathlib.Algebra.Star.Module
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : TrivialStar R
inst_3 : AddCommGroup A
inst_4 : Module R A
inst_5 : StarAddMonoid A
inst_6 : StarModule R A
inst_7 : Invertible (α := R) 2
x_1 : ↥(skewAdjoint.submodule R A)
x : A
hx : star x = -x
⊢ Eq.{u_2 + 1} (α := A)
    (↑((selfAdjointPart R ∘ₗ Submodule.subtype (skewAdjoint.submodule R A) :
            (a : ↥(skewAdjoint.submodule R A)) → ↥(selfAdjoint A))
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submodule R A) (skewAdjoint.submodule R A) x) x hx)) :
      A)
    (↑((0 : (a : ↥(skewAdjoint.submodule R A)) → ↥(selfAdjoint A))
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submodule R A) (skewAdjoint.submodule R A) x) x hx)) :
      A)

Tactic:
simp [hx]
-- Module: Mathlib.Algebra.Star.Module
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : TrivialStar R
inst_3 : AddCommGroup A
inst_4 : Module R A
inst_5 : StarAddMonoid A
inst_6 : StarModule R A
inst_7 : Invertible (α := R) 2
x_1 : ↥(skewAdjoint.submodule R A)
x : A
hx : star x = -x
simp :
  x =
    (↑((LinearMap.id : (a : ↥(skewAdjoint.submodule R A)) → ↥(skewAdjoint A))
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submodule R A) (skewAdjoint.submodule R A) x) x hx)) :
      A)
⊢ Eq.{u_2 + 1} (α := A)
    (↑((skewAdjointPart R ∘ₗ Submodule.subtype (skewAdjoint.submodule R A) :
            (a : ↥(skewAdjoint.submodule R A)) → ↥(skewAdjoint A))
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submodule R A) (skewAdjoint.submodule R A) x) x hx)) :
      A)
    (↑((LinearMap.id : (a : ↥(skewAdjoint.submodule R A)) → ↥(skewAdjoint A))
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submodule R A) (skewAdjoint.submodule R A) x) x hx)) :
      A)

Tactic:
simp only [LinearMap.comp_apply, Submodule.subtype_apply, skewAdjointPart_apply_coe, hx,
      sub_neg_eq_add, smul_add, invOf_two_smul_add_invOf_two_smul]

Premises used: Submodule.subtype_apply, LinearMap.comp_apply, invOf_two_smul_add_invOf_two_smul, skewAdjointPart_apply_coe, smul_add, sub_neg_eq_add
-- Module: Mathlib.Algebra.Star.Module
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : TrivialStar R
inst_3 : AddCommGroup A
inst_4 : Module R A
inst_5 : StarAddMonoid A
inst_6 : StarModule R A
inst_7 : Invertible (α := R) 2
x_1 : ↥(skewAdjoint.submodule R A)
x : A
hx : star x = -x
⊢ x =
    (↑((LinearMap.id : (a : ↥(skewAdjoint.submodule R A)) → ↥(skewAdjoint A))
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submodule R A) (skewAdjoint.submodule R A) x) x hx)) :
      A)

Tactic:
rfl
-- Module: Mathlib.Algebra.Star.Module
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : TrivialStar R
inst_3 : AddCommGroup A
inst_4 : Module R A
inst_5 : StarAddMonoid A
inst_6 : StarModule R A
inst_7 : Invertible (α := R) 2
refine :
  Eq (α := ↥(selfAdjoint A) × ↥(skewAdjoint A) →ₗ[R] ↥(selfAdjoint A) × ↥(skewAdjoint A))
    (LinearMap.prod (selfAdjointPart R) (skewAdjointPart R) ∘ₗ
        LinearMap.coprod (Submodule.subtype (selfAdjoint.submodule R A))
          (Submodule.subtype (skewAdjoint.submodule R A)) :
      ↥(selfAdjoint A) × ↥(skewAdjoint A) →ₗ[R] ↥(selfAdjoint A) × ↥(skewAdjoint A))
    (LinearMap.id : ↥(selfAdjoint A) × ↥(skewAdjoint A) →ₗ[R] ↥(selfAdjoint A) × ↥(skewAdjoint A))
⊢ A ≃ₗ[R] ↥(selfAdjoint A) × ↥(skewAdjoint A)

Tactic:
refine LinearEquiv.ofLinear ((selfAdjointPart R).prod (skewAdjointPart R))
    (LinearMap.coprod ((selfAdjoint.submodule R A).subtype) (skewAdjoint.submodule R A).subtype)
    ?_ (LinearMap.ext <| StarModule.selfAdjointPart_add_skewAdjointPart R)

Premises used: StarModule.selfAdjointPart_add_skewAdjointPart, LinearMap.coprod, LinearMap.ext, LinearEquiv.ofLinear, selfAdjointPart, selfAdjoint.submodule, Submodule.subtype, LinearMap.prod, skewAdjoint.submodule, skewAdjointPart
-- Module: Mathlib.Algebra.Star.Module
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : TrivialStar R
inst_3 : AddCommGroup A
inst_4 : Module R A
inst_5 : StarAddMonoid A
inst_6 : StarModule R A
inst_7 : Invertible (α := R) 2
x : ↥(selfAdjoint A)
hl :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HAdd.hAdd (α := A) (β := A)
          (((Submodule.subtype (selfAdjoint.submodule R A) : ↥(selfAdjoint.submodule R A) →ₗ[R] A) :
                (a : ↥(selfAdjoint A)) → A)
              x :
            A)
          (((Submodule.subtype (skewAdjoint.submodule R A) : ↥(skewAdjoint.submodule R A) →ₗ[R] A) :
                (a : ↥(skewAdjoint A)) → A)
              0 :
            A) +
        star
          (HAdd.hAdd (α := A) (β := A)
            (((Submodule.subtype (selfAdjoint.submodule R A) : ↥(selfAdjoint.submodule R A) →ₗ[R] A) :
                  (a : ↥(selfAdjoint A)) → A)
                x :
              A)
            (((Submodule.subtype (skewAdjoint.submodule R A) : ↥(skewAdjoint.submodule R A) →ₗ[R] A) :
                  (a : ↥(skewAdjoint A)) → A)
                0 :
              A))) =
    (↑x : A)
⊢ Eq.{u_2 + 1} (α := A)
    (↑((((LinearMap.prod (selfAdjointPart R) (skewAdjointPart R) ∘ₗ
                      LinearMap.coprod (Submodule.subtype (selfAdjoint.submodule R A))
                        (Submodule.subtype (skewAdjoint.submodule R A)) :
                    ↥(selfAdjoint A) × ↥(skewAdjoint A) →ₗ[R] ↥(selfAdjoint A) × ↥(skewAdjoint A)) ∘ₗ
                  (LinearMap.inl R ↥(selfAdjoint A) ↥(skewAdjoint A) :
                    ↥(selfAdjoint A) →ₗ[R] ↥(selfAdjoint A) × ↥(skewAdjoint A)) :
                ↥(selfAdjoint A) →ₗ[R] ↥(selfAdjoint A) × ↥(skewAdjoint A)) :
              (a : ↥(selfAdjoint A)) → ↥(selfAdjoint A) × ↥(skewAdjoint A))
            x).1 :
      A)
    (↑((LinearMap.id ∘ₗ LinearMap.inl R ↥(selfAdjoint A) ↥(skewAdjoint A) :
              (a : ↥(selfAdjoint A)) → ↥(selfAdjoint A) × ↥(skewAdjoint A))
            x).1 :
      A)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Star.Module
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : TrivialStar R
inst_3 : AddCommGroup A
inst_4 : Module R A
inst_5 : StarAddMonoid A
inst_6 : StarModule R A
inst_7 : Invertible (α := R) 2
x : ↥(selfAdjoint A)
hl :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HAdd.hAdd (α := A) (β := A)
          (((Submodule.subtype (selfAdjoint.submodule R A) : ↥(selfAdjoint.submodule R A) →ₗ[R] A) :
                (a : ↥(selfAdjoint A)) → A)
              x :
            A)
          (((Submodule.subtype (skewAdjoint.submodule R A) : ↥(skewAdjoint.submodule R A) →ₗ[R] A) :
                (a : ↥(skewAdjoint A)) → A)
              0 :
            A) -
        star
          (HAdd.hAdd (α := A) (β := A)
            (((Submodule.subtype (selfAdjoint.submodule R A) : ↥(selfAdjoint.submodule R A) →ₗ[R] A) :
                  (a : ↥(selfAdjoint A)) → A)
                x :
              A)
            (((Submodule.subtype (skewAdjoint.submodule R A) : ↥(skewAdjoint.submodule R A) →ₗ[R] A) :
                  (a : ↥(skewAdjoint A)) → A)
                0 :
              A))) =
    0
⊢ Eq.{u_2 + 1} (α := A)
    (↑((((LinearMap.prod (selfAdjointPart R) (skewAdjointPart R) ∘ₗ
                      LinearMap.coprod (Submodule.subtype (selfAdjoint.submodule R A))
                        (Submodule.subtype (skewAdjoint.submodule R A)) :
                    ↥(selfAdjoint A) × ↥(skewAdjoint A) →ₗ[R] ↥(selfAdjoint A) × ↥(skewAdjoint A)) ∘ₗ
                  (LinearMap.inl R ↥(selfAdjoint A) ↥(skewAdjoint A) :
                    ↥(selfAdjoint A) →ₗ[R] ↥(selfAdjoint A) × ↥(skewAdjoint A)) :
                ↥(selfAdjoint A) →ₗ[R] ↥(selfAdjoint A) × ↥(skewAdjoint A)) :
              (a : ↥(selfAdjoint A)) → ↥(selfAdjoint A) × ↥(skewAdjoint A))
            x).2 :
      A)
    (↑((LinearMap.id ∘ₗ LinearMap.inl R ↥(selfAdjoint A) ↥(skewAdjoint A) :
              (a : ↥(selfAdjoint A)) → ↥(selfAdjoint A) × ↥(skewAdjoint A))
            x).2 :
      A)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Star.Module
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : TrivialStar R
inst_3 : AddCommGroup A
inst_4 : Module R A
inst_5 : StarAddMonoid A
inst_6 : StarModule R A
inst_7 : Invertible (α := R) 2
x : ↥(skewAdjoint A)
hr :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HAdd.hAdd (α := A) (β := A)
          (((Submodule.subtype (selfAdjoint.submodule R A) : ↥(selfAdjoint.submodule R A) →ₗ[R] A) :
                (a : ↥(selfAdjoint A)) → A)
              0 :
            A)
          (((Submodule.subtype (skewAdjoint.submodule R A) : ↥(skewAdjoint.submodule R A) →ₗ[R] A) :
                (a : ↥(skewAdjoint A)) → A)
              x :
            A) +
        star
          (HAdd.hAdd (α := A) (β := A)
            (((Submodule.subtype (selfAdjoint.submodule R A) : ↥(selfAdjoint.submodule R A) →ₗ[R] A) :
                  (a : ↥(selfAdjoint A)) → A)
                0 :
              A)
            (((Submodule.subtype (skewAdjoint.submodule R A) : ↥(skewAdjoint.submodule R A) →ₗ[R] A) :
                  (a : ↥(skewAdjoint A)) → A)
                x :
              A))) =
    0
⊢ Eq.{u_2 + 1} (α := A)
    (↑((((LinearMap.prod (selfAdjointPart R) (skewAdjointPart R) ∘ₗ
                      LinearMap.coprod (Submodule.subtype (selfAdjoint.submodule R A))
                        (Submodule.subtype (skewAdjoint.submodule R A)) :
                    ↥(selfAdjoint A) × ↥(skewAdjoint A) →ₗ[R] ↥(selfAdjoint A) × ↥(skewAdjoint A)) ∘ₗ
                  (LinearMap.inr R ↥(selfAdjoint A) ↥(skewAdjoint A) :
                    ↥(skewAdjoint A) →ₗ[R] ↥(selfAdjoint A) × ↥(skewAdjoint A)) :
                ↥(skewAdjoint A) →ₗ[R] ↥(selfAdjoint A) × ↥(skewAdjoint A)) :
              (a : ↥(skewAdjoint A)) → ↥(selfAdjoint A) × ↥(skewAdjoint A))
            x).1 :
      A)
    (↑((LinearMap.id ∘ₗ LinearMap.inr R ↥(selfAdjoint A) ↥(skewAdjoint A) :
              (a : ↥(skewAdjoint A)) → ↥(selfAdjoint A) × ↥(skewAdjoint A))
            x).1 :
      A)

Tactic:
dsimp