-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem Submodule.sup_orthogonal_inf_of_completeSpace {K₁ K₂ : Submodule 𝕜 E} (h : K₁ ≤ K₂)
    [HasOrthogonalProjection K₁] : K₁ ⊔ K₁ᗮ ⊓ K₂ = K₂

Proof state:
case h.mp.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst✝ : HasOrthogonalProjection K₁
y : E
hy : y ∈ K₁
z : E
hz : z ∈ K₁ᗮ ⊓ K₂
v : ↥K₁ := (orthogonalProjection K₁) (y + z)
hvm : y + z - ↑v ∈ K₁ᗮ
⊢ y + z ∈ K₂

Tactic:
exact K₂.add_mem (h hy) hz.2

Result:
no goals

Proof state:
case h.mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst✝ : HasOrthogonalProjection K₁
x : E
v : ↥K₁ := (orthogonalProjection K₁) x
hvm : x - ↑v ∈ K₁ᗮ
⊢ (∃ y ∈ K₁, ∃ z ∈ K₁ᗮ ⊓ K₂, y + z = x) → x ∈ K₂

Tactic:
rintro ⟨y, hy, z, hz, rfl⟩

Result:
case h.mp.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst✝ : HasOrthogonalProjection K₁
y : E
hy : y ∈ K₁
z : E
hz : z ∈ K₁ᗮ ⊓ K₂
v : ↥K₁ := (orthogonalProjection K₁) (y + z)
hvm : y + z - ↑v ∈ K₁ᗮ
⊢ y + z ∈ K₂

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst✝ : HasOrthogonalProjection K₁
x : E
⊢ x ∈ K₁ ⊔ K₁ᗮ ⊓ K₂ ↔ x ∈ K₂

Tactic:
rw [Submodule.mem_sup]

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst✝ : HasOrthogonalProjection K₁
x : E
⊢ (∃ y ∈ K₁, ∃ z ∈ K₁ᗮ ⊓ K₂, y + z = x) ↔ x ∈ K₂

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst✝ : HasOrthogonalProjection K₁
⊢ K₁ ⊔ K₁ᗮ ⊓ K₂ = K₂

Tactic:
ext x

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst✝ : HasOrthogonalProjection K₁
x : E
⊢ x ∈ K₁ ⊔ K₁ᗮ ⊓ K₂ ↔ x ∈ K₂

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst✝ : HasOrthogonalProjection K₁
x : E
⊢ (∃ y ∈ K₁, ∃ z ∈ K₁ᗮ ⊓ K₂, y + z = x) ↔ x ∈ K₂

Tactic:
let v : K₁ := orthogonalProjection K₁ x

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst✝ : HasOrthogonalProjection K₁
x : E
v : ↥K₁ := (orthogonalProjection K₁) x
⊢ (∃ y ∈ K₁, ∃ z ∈ K₁ᗮ ⊓ K₂, y + z = x) ↔ x ∈ K₂

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst✝ : HasOrthogonalProjection K₁
x : E
v : ↥K₁ := (orthogonalProjection K₁) x
hvm : x - ↑v ∈ K₁ᗮ
⊢ (∃ y ∈ K₁, ∃ z ∈ K₁ᗮ ⊓ K₂, y + z = x) ↔ x ∈ K₂

Tactic:
constructor

Result:
case h.mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst✝ : HasOrthogonalProjection K₁
x : E
v : ↥K₁ := (orthogonalProjection K₁) x
hvm : x - ↑v ∈ K₁ᗮ
⊢ (∃ y ∈ K₁, ∃ z ∈ K₁ᗮ ⊓ K₂, y + z = x) → x ∈ K₂

case h.mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst✝ : HasOrthogonalProjection K₁
x : E
v : ↥K₁ := (orthogonalProjection K₁) x
hvm : x - ↑v ∈ K₁ᗮ
⊢ x ∈ K₂ → ∃ y ∈ K₁, ∃ z ∈ K₁ᗮ ⊓ K₂, y + z = x

Proof state:
case h.mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst✝ : HasOrthogonalProjection K₁
x : E
v : ↥K₁ := (orthogonalProjection K₁) x
hvm : x - ↑v ∈ K₁ᗮ
⊢ x ∈ K₂ → ∃ y ∈ K₁, ∃ z ∈ K₁ᗮ ⊓ K₂, y + z = x

Tactic:
exact fun hx => ⟨v, v.prop, x - v, ⟨hvm, K₂.sub_mem hx (h v.prop)⟩, add_sub_cancel _ _⟩

Result:
no goals

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst✝ : HasOrthogonalProjection K₁
x : E
v : ↥K₁ := (orthogonalProjection K₁) x
⊢ (∃ y ∈ K₁, ∃ z ∈ K₁ᗮ ⊓ K₂, y + z = x) ↔ x ∈ K₂

Tactic:
have hvm : x - v ∈ K₁ᗮ := sub_orthogonalProjection_mem_orthogonal x

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst✝ : HasOrthogonalProjection K₁
x : E
v : ↥K₁ := (orthogonalProjection K₁) x
hvm : x - ↑v ∈ K₁ᗮ
⊢ (∃ y ∈ K₁, ∃ z ∈ K₁ᗮ ⊓ K₂, y + z = x) ↔ x ∈ K₂