case h.a
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.361842
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.362358
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.363321
inst✝² : Semiring S
M : Type ?u.363327
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] { x // x ∈ p }
hf : ∀ (x : { x // x ∈ p }), ↑f ↑x = x
x : E
⊢ ↑(↑(linearProjOfIsCompl p (ker f) (_ : IsCompl p (ker f))) x) = ↑(↑f x)
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.361842
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.362358
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.363321
inst✝² : Semiring S
M : Type ?u.363327
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] { x // x ∈ p }
hf : ∀ (x : { x // x ∈ p }), ↑f ↑x = x
⊢ linearProjOfIsCompl p (ker f) (_ : IsCompl p (ker f)) = f
ext x
case h.a
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.361842
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.362358
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.363321
inst✝² : Semiring S
M : Type ?u.363327
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] { x // x ∈ p }
hf : ∀ (x : { x // x ∈ p }), ↑f ↑x = x
x : E
this : x ∈ p ⊔ ker f
⊢ ↑(↑(linearProjOfIsCompl p (ker f) (_ : IsCompl p (ker f))) x) = ↑(↑f x)
case h.a
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.361842
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.362358
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.363321
inst✝² : Semiring S
M : Type ?u.363327
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] { x // x ∈ p }
hf : ∀ (x : { x // x ∈ p }), ↑f ↑x = x
x : E
⊢ ↑(↑(linearProjOfIsCompl p (ker f) (_ : IsCompl p (ker f))) x) = ↑(↑f x)
have : x ∈ p ⊔ (ker f) := by simp only [(isCompl_of_proj hf).sup_eq_top, mem_top]
case h.a.intro.intro
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.361842
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.362358
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.363321
inst✝² : Semiring S
M : Type ?u.363327
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] { x // x ∈ p }
hf : ∀ (x : { x // x ∈ p }), ↑f ↑x = x
x : { x // x ∈ p }
y : { x // x ∈ ker f }
this : ↑x + ↑y ∈ p ⊔ ker f
⊢ ↑(↑(linearProjOfIsCompl p (ker f) (_ : IsCompl p (ker f))) (↑x + ↑y)) = ↑(↑f (↑x + ↑y))
case h.a
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.361842
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.362358
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.363321
inst✝² : Semiring S
M : Type ?u.363327
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] { x // x ∈ p }
hf : ∀ (x : { x // x ∈ p }), ↑f ↑x = x
x : E
this : x ∈ p ⊔ ker f
⊢ ↑(↑(linearProjOfIsCompl p (ker f) (_ : IsCompl p (ker f))) x) = ↑(↑f x)
rcases mem_sup'.1 this with ⟨x, y, rfl⟩
no goals
case h.a.intro.intro
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.361842
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.362358
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.363321
inst✝² : Semiring S
M : Type ?u.363327
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] { x // x ∈ p }
hf : ∀ (x : { x // x ∈ p }), ↑f ↑x = x
x : { x // x ∈ p }
y : { x // x ∈ ker f }
this : ↑x + ↑y ∈ p ⊔ ker f
⊢ ↑(↑(linearProjOfIsCompl p (ker f) (_ : IsCompl p (ker f))) (↑x + ↑y)) = ↑(↑f (↑x + ↑y))
simp [hf]
no goals
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.361842
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.362358
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.363321
inst✝² : Semiring S
M : Type ?u.363327
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] { x // x ∈ p }
hf : ∀ (x : { x // x ∈ p }), ↑f ↑x = x
x : E
⊢ x ∈ p ⊔ ker f
simp only [(isCompl_of_proj hf).sup_eq_top, mem_top]