R : Type u_2
inst✝⁹ : Ring R
E : Type u_1
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.186731
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.187247
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.188210
inst✝² : Semiring S
M : Type ?u.188216
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
hpq : IsCompl p q
x : E
⊢ ↑(↑(comp (LinearMap.fst R { x // x ∈ p } { x // x ∈ q }) ↑(LinearEquiv.symm (prodEquivOfIsCompl p q hpq))) x) +
      ↑(↑(comp (LinearMap.fst R { x // x ∈ q } { x // x ∈ p })
              ↑(LinearEquiv.symm (prodEquivOfIsCompl q p (_ : IsCompl q p))))
          x) =
    x
R : Type u_2
inst✝⁹ : Ring R
E : Type u_1
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.186731
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.187247
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.188210
inst✝² : Semiring S
M : Type ?u.188216
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
hpq : IsCompl p q
x : E
⊢ ↑(↑(linearProjOfIsCompl p q hpq) x) + ↑(↑(linearProjOfIsCompl q p (_ : IsCompl q p)) x) = x
dsimp only [linearProjOfIsCompl]
R : Type u_2
inst✝⁹ : Ring R
E : Type u_1
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.186731
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.187247
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.188210
inst✝² : Semiring S
M : Type ?u.188216
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
hpq : IsCompl p q
x : E
⊢ ↑(↑(comp (LinearMap.fst R { x // x ∈ p } { x // x ∈ q }) ↑(LinearEquiv.symm (prodEquivOfIsCompl p q hpq))) x) +
      ↑(↑(comp (LinearMap.fst R { x // x ∈ q } { x // x ∈ p })
              ↑(LinearEquiv.symm
                  (LinearEquiv.trans (LinearEquiv.prodComm R { x // x ∈ q } { x // x ∈ p })
                    (prodEquivOfIsCompl p q hpq))))
          x) =
    x
R : Type u_2
inst✝⁹ : Ring R
E : Type u_1
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.186731
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.187247
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.188210
inst✝² : Semiring S
M : Type ?u.188216
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
hpq : IsCompl p q
x : E
⊢ ↑(↑(comp (LinearMap.fst R { x // x ∈ p } { x // x ∈ q }) ↑(LinearEquiv.symm (prodEquivOfIsCompl p q hpq))) x) +
      ↑(↑(comp (LinearMap.fst R { x // x ∈ q } { x // x ∈ p })
              ↑(LinearEquiv.symm (prodEquivOfIsCompl q p (_ : IsCompl q p))))
          x) =
    x
rw [← prodComm_trans_prodEquivOfIsCompl _ _ hpq]
no goals
R : Type u_2
inst✝⁹ : Ring R
E : Type u_1
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.186731
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.187247
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.188210
inst✝² : Semiring S
M : Type ?u.188216
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
hpq : IsCompl p q
x : E
⊢ ↑(↑(comp (LinearMap.fst R { x // x ∈ p } { x // x ∈ q }) ↑(LinearEquiv.symm (prodEquivOfIsCompl p q hpq))) x) +
      ↑(↑(comp (LinearMap.fst R { x // x ∈ q } { x // x ∈ p })
              ↑(LinearEquiv.symm
                  (LinearEquiv.trans (LinearEquiv.prodComm R { x // x ∈ q } { x // x ∈ p })
                    (prodEquivOfIsCompl p q hpq))))
          x) =
    x
exact (prodEquivOfIsCompl _ _ hpq).apply_symm_apply x