awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Star.Module (goal)
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
⊢ (↑((selfAdjointPart R : (a : A) → ↥(selfAdjoint A)) x) : A) = x
have 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
Tactic: rw [selfAdjointPart_apply_coe, hx.star_eq, smul_add, invOf_two_smul_add_invOf_two_smul]
-- Lean 4 proof step from Mathlib.Algebra.Star.Module (goal)
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
⊢ (↑((selfAdjointPart R : (a : A) → ↥(selfAdjoint A)) x) : A) = x
have rw₃ : x = x
Tactic: rw [selfAdjointPart_apply_coe, hx.star_eq, smul_add, invOf_two_smul_add_invOf_two_smul]
-- Lean 4 proof step from Mathlib.Algebra.Star.Module (goal)
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
⊢ Eq.{u_2 + 1} (α := A) (↑((skewAdjointPart R : (a : A) → ↥(skewAdjoint A)) x) : A) (↑0 : A)
have rw : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x - star x) =
  (↑0 : A)
Tactic: rw [skewAdjointPart_apply_coe, hx.star_eq, sub_self, smul_zero, ZeroMemClass.coe_zero]
-- Lean 4 proof step from Mathlib.Algebra.Star.Module (goal)
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)
⊢ Eq.{u_2 + 1} (α := A) (↑((skewAdjointPart R : (a : A) → ↥(skewAdjoint A)) x) : A) (↑0 : A)
have rw₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x - x) = (↑0 : A)
Tactic: rw [skewAdjointPart_apply_coe, hx.star_eq, sub_self, smul_zero, ZeroMemClass.coe_zero]
-- Lean 4 proof step from Mathlib.Algebra.Star.Module (goal)
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)
⊢ Eq.{u_2 + 1} (α := A) (↑((skewAdjointPart R : (a : A) → ↥(skewAdjoint A)) x) : A) (↑0 : A)
have rw₂ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) 0 =
  (↑0 : A)
Tactic: rw [skewAdjointPart_apply_coe, hx.star_eq, sub_self, smul_zero, ZeroMemClass.coe_zero]
-- Lean 4 proof step from Mathlib.Algebra.Star.Module (goal)
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)
⊢ Eq.{u_2 + 1} (α := A) (↑((skewAdjointPart R : (a : A) → ↥(skewAdjoint A)) x) : A) (↑0 : A)
have rw₃ : Eq.{u_2 + 1} (α := A) 0 (↑0 : A)
Tactic: rw [skewAdjointPart_apply_coe, hx.star_eq, sub_self, smul_zero, ZeroMemClass.coe_zero]
-- Lean 4 proof step from Mathlib.Algebra.Star.Module (goal)
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)
⊢ Eq.{u_2 + 1} (α := A) (↑((skewAdjointPart R : (a : A) → ↥(skewAdjoint A)) x) : A) (↑0 : A)
have rw₄ : Eq.{u_2 + 1} (α := A) 0 0
Tactic: rw [skewAdjointPart_apply_coe, hx.star_eq, sub_self, smul_zero, ZeroMemClass.coe_zero]
-- Lean 4 proof step from Mathlib.Algebra.Star.Module (goal)
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)
    (↑((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)
have 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)
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]
-- Lean 4 proof step from Mathlib.Algebra.Star.Module (goal)
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
⊢ A ≃ₗ[R] ↥(selfAdjoint A) × ↥(skewAdjoint A)
have 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))
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)
-- Lean 4 proof step from Mathlib.Algebra.Star.Module (goal)
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 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))
have hl : ∀ (x : ↥(selfAdjoint 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: ext x
-- Lean 4 proof step from Mathlib.Algebra.Star.Module (goal)
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
hl :
  ∀ (x : ↥(selfAdjoint 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)
⊢ 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))
have hl₁ : ∀ (x : ↥(selfAdjoint 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).2 :
      A)
    (↑((LinearMap.id ∘ₗ LinearMap.inl R ↥(selfAdjoint A) ↥(skewAdjoint A) :
              (a : ↥(selfAdjoint A)) → ↥(selfAdjoint A) × ↥(skewAdjoint A))
            x).2 :
      A)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Star.Module (goal)
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)
⊢ 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)
have 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)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Star.Module (goal)
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)
⊢ 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)
have 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
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Star.Module (goal)
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)
⊢ 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)
have 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
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Star.Module (goal)
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)
⊢ 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).2 :
      A)
    (↑((LinearMap.id ∘ₗ LinearMap.inr R ↥(selfAdjoint A) ↥(skewAdjoint A) :
              (a : ↥(skewAdjoint A)) → ↥(selfAdjoint A) × ↥(skewAdjoint A))
            x).2 :
      A)
have 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))) =
  (↑x : A)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Star.Module (goal)
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)
⊢ 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)
have hl : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
    ((↑x : A) + (↑0 : A) + star ((↑x : A) + (↑0 : A))) =
  (↑x : A)
Tactic: erw [Submodule.coe_subtype, Submodule.coe_subtype]
-- Lean 4 proof step from Mathlib.Algebra.Star.Module (goal)
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)
⊢ 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
have hl : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
    ((↑x : A) + (↑0 : A) - star ((↑x : A) + (↑0 : A))) =
  0
Tactic: erw [Submodule.coe_subtype, Submodule.coe_subtype]