no goals
R : Type u_2
inst✝⁹ : Ring R
E : Type u_1
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.281059
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.282022
inst✝² : Semiring S
M : Type ?u.282028
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
φ₁ φ₂ : { x // x ∈ p } →ₗ[R] F
ψ₁ ψ₂ : { x // x ∈ q } →ₗ[R] F
⊢ ∀ (u : { x // x ∈ p }), ↑(φ₁ + φ₂) u = ↑(ofIsCompl h φ₁ ψ₁ + ofIsCompl h φ₂ ψ₂) ↑u
simp
no goals
R : Type u_2
inst✝⁹ : Ring R
E : Type u_1
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.281059
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.282022
inst✝² : Semiring S
M : Type ?u.282028
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
φ₁ φ₂ : { x // x ∈ p } →ₗ[R] F
ψ₁ ψ₂ : { x // x ∈ q } →ₗ[R] F
⊢ ∀ (u : { x // x ∈ q }), ↑(ψ₁ + ψ₂) u = ↑(ofIsCompl h φ₁ ψ₁ + ofIsCompl h φ₂ ψ₂) ↑u
simp