case h
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.241525
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.242488
inst✝² : Semiring S
M : Type ?u.242494
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
χ : E →ₗ[R] F
hφ : ∀ (u : { x // x ∈ p }), ↑φ u = ↑χ ↑u
hψ : ∀ (u : { x // x ∈ q }), ↑ψ u = ↑χ ↑u
x : E
⊢ ↑(ofIsCompl h φ ψ) x = ↑χ x
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.241525
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.242488
inst✝² : Semiring S
M : Type ?u.242494
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
χ : E →ₗ[R] F
hφ : ∀ (u : { x // x ∈ p }), ↑φ u = ↑χ ↑u
hψ : ∀ (u : { x // x ∈ q }), ↑ψ u = ↑χ ↑u
⊢ ofIsCompl h φ ψ = χ
ext x
case h.intro.intro.intro
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.241525
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.242488
inst✝² : Semiring S
M : Type ?u.242494
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
χ : E →ₗ[R] F
hφ : ∀ (u : { x // x ∈ p }), ↑φ u = ↑χ ↑u
hψ : ∀ (u : { x // x ∈ q }), ↑ψ u = ↑χ ↑u
w✝¹ : { x // x ∈ p }
w✝ : { x // x ∈ q }
right✝ : ∀ (r : { x // x ∈ p }) (s : { x // x ∈ q }), ↑r + ↑s = ↑w✝¹ + ↑w✝ → r = w✝¹ ∧ s = w✝
⊢ ↑(ofIsCompl h φ ψ) (↑w✝¹ + ↑w✝) = ↑χ (↑w✝¹ + ↑w✝)
case h
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.241525
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.242488
inst✝² : Semiring S
M : Type ?u.242494
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
χ : E →ₗ[R] F
hφ : ∀ (u : { x // x ∈ p }), ↑φ u = ↑χ ↑u
hψ : ∀ (u : { x // x ∈ q }), ↑ψ u = ↑χ ↑u
x : E
⊢ ↑(ofIsCompl h φ ψ) x = ↑χ x
obtain ⟨_, _, rfl, _⟩ := existsUnique_add_of_isCompl h x
no goals
case h.intro.intro.intro
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.241525
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.242488
inst✝² : Semiring S
M : Type ?u.242494
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
χ : E →ₗ[R] F
hφ : ∀ (u : { x // x ∈ p }), ↑φ u = ↑χ ↑u
hψ : ∀ (u : { x // x ∈ q }), ↑ψ u = ↑χ ↑u
w✝¹ : { x // x ∈ p }
w✝ : { x // x ∈ q }
right✝ : ∀ (r : { x // x ∈ p }) (s : { x // x ∈ q }), ↑r + ↑s = ↑w✝¹ + ↑w✝ → r = w✝¹ ∧ s = w✝
⊢ ↑(ofIsCompl h φ ψ) (↑w✝¹ + ↑w✝) = ↑χ (↑w✝¹ + ↑w✝)
simp [ofIsCompl, hφ, hψ]