Module: Mathlib.Algebra.Star.Module

Goal state before:
pp: case hl.fst
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : ↥(selfAdjoint A)
⊢ ↑((((selfAdjointPart R).prod (skewAdjointPart R) ∘ₗ
              (selfAdjoint.submodule R A).subtype.coprod (skewAdjoint.submodule R A).subtype) ∘ₗ
            LinearMap.inl R ↥(selfAdjoint A) ↥(skewAdjoint A))
          x).1 =
    ↑((LinearMap.id ∘ₗ LinearMap.inl R ↥(selfAdjoint A) ↥(skewAdjoint A)) x).1

pp: case hl.snd
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : ↥(selfAdjoint A)
⊢ ↑((((selfAdjointPart R).prod (skewAdjointPart R) ∘ₗ
              (selfAdjoint.submodule R A).subtype.coprod (skewAdjoint.submodule R A).subtype) ∘ₗ
            LinearMap.inl R ↥(selfAdjoint A) ↥(skewAdjoint A))
          x).2 =
    ↑((LinearMap.id ∘ₗ LinearMap.inl R ↥(selfAdjoint A) ↥(skewAdjoint A)) x).2

pp: case hr.fst
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : ↥(skewAdjoint A)
⊢ ↑((((selfAdjointPart R).prod (skewAdjointPart R) ∘ₗ
              (selfAdjoint.submodule R A).subtype.coprod (skewAdjoint.submodule R A).subtype) ∘ₗ
            LinearMap.inr R ↥(selfAdjoint A) ↥(skewAdjoint A))
          x).1 =
    ↑((LinearMap.id ∘ₗ LinearMap.inr R ↥(selfAdjoint A) ↥(skewAdjoint A)) x).1

pp: case hr.snd
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : ↥(skewAdjoint A)
⊢ ↑((((selfAdjointPart R).prod (skewAdjointPart R) ∘ₗ
              (selfAdjoint.submodule R A).subtype.coprod (skewAdjoint.submodule R A).subtype) ∘ₗ
            LinearMap.inr R ↥(selfAdjoint A) ↥(skewAdjoint A))
          x).2 =
    ↑((LinearMap.id ∘ₗ LinearMap.inr R ↥(selfAdjoint A) ↥(skewAdjoint A)) x).2

Tactic:
<;>

Goal state after:
case hl.fst
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : ↥(selfAdjoint A)
⊢ ↑((((selfAdjointPart R).prod (skewAdjointPart R) ∘ₗ
              (selfAdjoint.submodule R A).subtype.coprod (skewAdjoint.submodule R A).subtype) ∘ₗ
            LinearMap.inl R ↥(selfAdjoint A) ↥(skewAdjoint A))
          x).1 =
    ↑((LinearMap.id ∘ₗ LinearMap.inl R ↥(selfAdjoint A) ↥(skewAdjoint A)) x).1

case hl.snd
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : ↥(selfAdjoint A)
⊢ ↑((((selfAdjointPart R).prod (skewAdjointPart R) ∘ₗ
              (selfAdjoint.submodule R A).subtype.coprod (skewAdjoint.submodule R A).subtype) ∘ₗ
            LinearMap.inl R ↥(selfAdjoint A) ↥(skewAdjoint A))
          x).2 =
    ↑((LinearMap.id ∘ₗ LinearMap.inl R ↥(selfAdjoint A) ↥(skewAdjoint A)) x).2

case hr.fst
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : ↥(skewAdjoint A)
⊢ ↑((((selfAdjointPart R).prod (skewAdjointPart R) ∘ₗ
              (selfAdjoint.submodule R A).subtype.coprod (skewAdjoint.submodule R A).subtype) ∘ₗ
            LinearMap.inr R ↥(selfAdjoint A) ↥(skewAdjoint A))
          x).1 =
    ↑((LinearMap.id ∘ₗ LinearMap.inr R ↥(selfAdjoint A) ↥(skewAdjoint A)) x).1

case hr.snd
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : ↥(skewAdjoint A)
⊢ ↑((((selfAdjointPart R).prod (skewAdjointPart R) ∘ₗ
              (selfAdjoint.submodule R A).subtype.coprod (skewAdjoint.submodule R A).subtype) ∘ₗ
            LinearMap.inr R ↥(selfAdjoint A) ↥(skewAdjoint A))
          x).2 =
    ↑((LinearMap.id ∘ₗ LinearMap.inr R ↥(selfAdjoint A) ↥(skewAdjoint A)) x).2