R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.451177
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.451693
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.452656
inst✝² : Semiring S
M : Type ?u.452662
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] E
h : IsProj p f
⊢ comp f ↑(prodEquivOfIsCompl p (ker f) (_ : IsCompl p (ker f))) =
    comp (↑(prodEquivOfIsCompl p (ker f) (_ : IsCompl p (ker f)))) (prodMap id 0)
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.451177
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.451693
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.452656
inst✝² : Semiring S
M : Type ?u.452662
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] E
h : IsProj p f
⊢ f =
    comp (↑(prodEquivOfIsCompl p (ker f) (_ : IsCompl p (ker f))))
      (comp (prodMap id 0) ↑(LinearEquiv.symm (prodEquivOfIsCompl p (ker f) (_ : IsCompl p (ker f)))))
rw [← LinearMap.comp_assoc, LinearEquiv.eq_comp_toLinearMap_symm]
case hl.h
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.451177
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.451693
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.452656
inst✝² : Semiring S
M : Type ?u.452662
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] E
h : IsProj p f
x : { x // x ∈ p }
⊢ ↑(comp (comp f ↑(prodEquivOfIsCompl p (ker f) (_ : IsCompl p (ker f)))) (inl R { x // x ∈ p } { x // x ∈ ker f })) x =
    ↑(comp (comp (↑(prodEquivOfIsCompl p (ker f) (_ : IsCompl p (ker f)))) (prodMap id 0))
          (inl R { x // x ∈ p } { x // x ∈ ker f }))
      x

case hr.h
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.451177
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.451693
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.452656
inst✝² : Semiring S
M : Type ?u.452662
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] E
h : IsProj p f
x : { x // x ∈ ker f }
⊢ ↑(comp (comp f ↑(prodEquivOfIsCompl p (ker f) (_ : IsCompl p (ker f)))) (inr R { x // x ∈ p } { x // x ∈ ker f })) x =
    ↑(comp (comp (↑(prodEquivOfIsCompl p (ker f) (_ : IsCompl p (ker f)))) (prodMap id 0))
          (inr R { x // x ∈ p } { x // x ∈ ker f }))
      x
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.451177
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.451693
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.452656
inst✝² : Semiring S
M : Type ?u.452662
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] E
h : IsProj p f
⊢ comp f ↑(prodEquivOfIsCompl p (ker f) (_ : IsCompl p (ker f))) =
    comp (↑(prodEquivOfIsCompl p (ker f) (_ : IsCompl p (ker f)))) (prodMap id 0)
ext x
no goals
case hl.h
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.451177
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.451693
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.452656
inst✝² : Semiring S
M : Type ?u.452662
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] E
h : IsProj p f
x : { x // x ∈ p }
⊢ ↑(comp (comp f ↑(prodEquivOfIsCompl p (ker f) (_ : IsCompl p (ker f)))) (inl R { x // x ∈ p } { x // x ∈ ker f })) x =
    ↑(comp (comp (↑(prodEquivOfIsCompl p (ker f) (_ : IsCompl p (ker f)))) (prodMap id 0))
          (inl R { x // x ∈ p } { x // x ∈ ker f }))
      x
simp only [coe_prodEquivOfIsCompl, comp_apply, coe_inl, coprod_apply, coeSubtype,
  _root_.map_zero, add_zero, h.map_id x x.2, prodMap_apply, id_apply]
no goals
case hr.h
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.451177
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.451693
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.452656
inst✝² : Semiring S
M : Type ?u.452662
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] E
h : IsProj p f
x : { x // x ∈ ker f }
⊢ ↑(comp (comp f ↑(prodEquivOfIsCompl p (ker f) (_ : IsCompl p (ker f)))) (inr R { x // x ∈ p } { x // x ∈ ker f })) x =
    ↑(comp (comp (↑(prodEquivOfIsCompl p (ker f) (_ : IsCompl p (ker f)))) (prodMap id 0))
          (inr R { x // x ∈ p } { x // x ∈ ker f }))
      x
simp only [coe_prodEquivOfIsCompl, comp_apply, coe_inr, coprod_apply, _root_.map_zero,
  coeSubtype, zero_add, map_coe_ker, prodMap_apply, zero_apply, add_zero]