-- Mathlib/Analysis/InnerProductSpace/l2Space.lean
theorem Submodule.isHilbertSumOrthogonal (K : Submodule 𝕜 E) [hK : CompleteSpace K] :
    IsHilbertSum 𝕜 (fun b => ↥(cond b K Kᗮ)) fun b => (cond b K Kᗮ).subtypeₗᵢ

Proof state:
case true
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
K : Submodule 𝕜 E
hK : CompleteSpace ↥K
⊢ CompleteSpace ↥(bif true then K else Kᗮ)

Tactic:
assumption

Result:
no goals

Proof state:
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
K : Submodule 𝕜 E
hK : CompleteSpace ↥K
this : ∀ (b : Bool), CompleteSpace ↥(bif b then K else Kᗮ)
⊢ ⊤ ≤ (⨆ i, bif i then K else Kᗮ).topologicalClosure

Tactic:
refine le_trans ?_ (Submodule.le_topologicalClosure _)

Result:
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
K : Submodule 𝕜 E
hK : CompleteSpace ↥K
this : ∀ (b : Bool), CompleteSpace ↥(bif b then K else Kᗮ)
⊢ ⊤ ≤ ⨆ i, bif i then K else Kᗮ

Proof state:
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
K : Submodule 𝕜 E
hK : CompleteSpace ↥K
this : ∀ (b : Bool), CompleteSpace ↥(bif b then K else Kᗮ)
⊢ ⊤ ≤ ⨆ i, bif i then K else Kᗮ

Tactic:
rw [iSup_bool_eq, cond, cond]

Result:
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
K : Submodule 𝕜 E
hK : CompleteSpace ↥K
this : ∀ (b : Bool), CompleteSpace ↥(bif b then K else Kᗮ)
⊢ ⊤ ≤ K ⊔ Kᗮ

Proof state:
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
K : Submodule 𝕜 E
hK : CompleteSpace ↥K
this : ∀ (b : Bool), CompleteSpace ↥(bif b then K else Kᗮ)
⊢ ⊤ ≤ K ⊔ Kᗮ

Tactic:
refine Codisjoint.top_le ?_

Result:
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
K : Submodule 𝕜 E
hK : CompleteSpace ↥K
this : ∀ (b : Bool), CompleteSpace ↥(bif b then K else Kᗮ)
⊢ Codisjoint K Kᗮ

Proof state:
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
K : Submodule 𝕜 E
hK : CompleteSpace ↥K
⊢ IsHilbertSum 𝕜 (fun b => ↥(bif b then K else Kᗮ)) fun b => (bif b then K else Kᗮ).subtypeₗᵢ

Tactic:
have : ∀ b, CompleteSpace (↥(cond b K Kᗮ)) := by
  intro b
  cases b <;> first | exact instOrthogonalCompleteSpace K | assumption

Result:
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
K : Submodule 𝕜 E
hK : CompleteSpace ↥K
this : ∀ (b : Bool), CompleteSpace ↥(bif b then K else Kᗮ)
⊢ IsHilbertSum 𝕜 (fun b => ↥(bif b then K else Kᗮ)) fun b => (bif b then K else Kᗮ).subtypeₗᵢ

Proof state:
case false
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
K : Submodule 𝕜 E
hK : CompleteSpace ↥K
⊢ CompleteSpace ↥(bif false then K else Kᗮ)

Tactic:
exact instOrthogonalCompleteSpace K

Result:
no goals

Proof state:
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
K : Submodule 𝕜 E
hK : CompleteSpace ↥K
this : ∀ (b : Bool), CompleteSpace ↥(bif b then K else Kᗮ)
⊢ IsHilbertSum 𝕜 (fun b => ↥(bif b then K else Kᗮ)) fun b => (bif b then K else Kᗮ).subtypeₗᵢ

Tactic:
refine IsHilbertSum.mkInternal _ K.orthogonalFamily_self ?_

Result:
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
K : Submodule 𝕜 E
hK : CompleteSpace ↥K
this : ∀ (b : Bool), CompleteSpace ↥(bif b then K else Kᗮ)
⊢ ⊤ ≤ (⨆ i, bif i then K else Kᗮ).topologicalClosure

Proof state:
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
K : Submodule 𝕜 E
hK : CompleteSpace ↥K
⊢ ∀ (b : Bool), CompleteSpace ↥(bif b then K else Kᗮ)

Tactic:
intro b

Result:
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
K : Submodule 𝕜 E
hK : CompleteSpace ↥K
b : Bool
⊢ CompleteSpace ↥(bif b then K else Kᗮ)

Proof state:
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
K : Submodule 𝕜 E
hK : CompleteSpace ↥K
this : ∀ (b : Bool), CompleteSpace ↥(bif b then K else Kᗮ)
⊢ Codisjoint K Kᗮ

Tactic:
exact Submodule.isCompl_orthogonal_of_completeSpace.codisjoint

Result:
no goals

Proof state:
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
K : Submodule 𝕜 E
hK : CompleteSpace ↥K
b : Bool
⊢ CompleteSpace ↥(bif b then K else Kᗮ)

Tactic:
cases b <;> first | exact instOrthogonalCompleteSpace K | assumption

Result:
no goals