ι : Type ?u.670433
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.670584
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
K : Submodule 𝕜 E
hK : CompleteSpace { x // x ∈ K }
this : ∀ (b : Bool), CompleteSpace { x // x ∈ bif b then K else Kᗮ }
⊢ IsHilbertSum 𝕜 (fun b => { x // x ∈ bif b then K else Kᗮ }) fun b => subtypeₗᵢ (bif b then K else Kᗮ)
ι : Type ?u.670433
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.670584
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
K : Submodule 𝕜 E
hK : CompleteSpace { x // x ∈ K }
⊢ IsHilbertSum 𝕜 (fun b => { x // x ∈ bif b then K else Kᗮ }) fun b => subtypeₗᵢ (bif b then K else Kᗮ)
have : ∀ b, CompleteSpace (↥(cond b K Kᗮ)) := by
  intro b
  cases b <;> first | exact instOrthogonalCompleteSpace K | assumption
ι : Type ?u.670433
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.670584
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
K : Submodule 𝕜 E
hK : CompleteSpace { x // x ∈ K }
this : ∀ (b : Bool), CompleteSpace { x // x ∈ bif b then K else Kᗮ }
⊢ ⊤ ≤ topologicalClosure (⨆ (i : Bool), bif i then K else Kᗮ)
ι : Type ?u.670433
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.670584
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
K : Submodule 𝕜 E
hK : CompleteSpace { x // x ∈ K }
this : ∀ (b : Bool), CompleteSpace { x // x ∈ bif b then K else Kᗮ }
⊢ IsHilbertSum 𝕜 (fun b => { x // x ∈ bif b then K else Kᗮ }) fun b => subtypeₗᵢ (bif b then K else Kᗮ)
refine' IsHilbertSum.mkInternal _ K.orthogonalFamily_self _
ι : Type ?u.670433
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.670584
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
K : Submodule 𝕜 E
hK : CompleteSpace { x // x ∈ K }
this : ∀ (b : Bool), CompleteSpace { x // x ∈ bif b then K else Kᗮ }
⊢ ⊤ ≤ ⨆ (i : Bool), bif i then K else Kᗮ
ι : Type ?u.670433
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.670584
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
K : Submodule 𝕜 E
hK : CompleteSpace { x // x ∈ K }
this : ∀ (b : Bool), CompleteSpace { x // x ∈ bif b then K else Kᗮ }
⊢ ⊤ ≤ topologicalClosure (⨆ (i : Bool), bif i then K else Kᗮ)
refine' le_trans _ (Submodule.le_topologicalClosure _)
ι : Type ?u.670433
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.670584
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
K : Submodule 𝕜 E
hK : CompleteSpace { x // x ∈ K }
this : ∀ (b : Bool), CompleteSpace { x // x ∈ bif b then K else Kᗮ }
⊢ ⊤ ≤
    (match true with
      | true => K
      | false => Kᗮ) ⊔
      match false with
      | true => K
      | false => Kᗮ
ι : Type ?u.670433
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.670584
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
K : Submodule 𝕜 E
hK : CompleteSpace { x // x ∈ K }
this : ∀ (b : Bool), CompleteSpace { x // x ∈ bif b then K else Kᗮ }
⊢ ⊤ ≤ ⨆ (i : Bool), bif i then K else Kᗮ
rw [iSup_bool_eq, cond, cond]
ι : Type ?u.670433
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.670584
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
K : Submodule 𝕜 E
hK : CompleteSpace { x // x ∈ K }
this : ∀ (b : Bool), CompleteSpace { x // x ∈ bif b then K else Kᗮ }
⊢ Codisjoint
    (match true with
    | true => K
    | false => Kᗮ)
    (match false with
    | true => K
    | false => Kᗮ)
ι : Type ?u.670433
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.670584
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
K : Submodule 𝕜 E
hK : CompleteSpace { x // x ∈ K }
this : ∀ (b : Bool), CompleteSpace { x // x ∈ bif b then K else Kᗮ }
⊢ ⊤ ≤
    (match true with
      | true => K
      | false => Kᗮ) ⊔
      match false with
      | true => K
      | false => Kᗮ
refine' Codisjoint.top_le _
no goals
ι : Type ?u.670433
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.670584
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
K : Submodule 𝕜 E
hK : CompleteSpace { x // x ∈ K }
this : ∀ (b : Bool), CompleteSpace { x // x ∈ bif b then K else Kᗮ }
⊢ Codisjoint
    (match true with
    | true => K
    | false => Kᗮ)
    (match false with
    | true => K
    | false => Kᗮ)
exact Submodule.isCompl_orthogonal_of_completeSpace.codisjoint
ι : Type ?u.670433
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.670584
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
K : Submodule 𝕜 E
hK : CompleteSpace { x // x ∈ K }
b : Bool
⊢ CompleteSpace { x // x ∈ bif b then K else Kᗮ }
ι : Type ?u.670433
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.670584
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
K : Submodule 𝕜 E
hK : CompleteSpace { x // x ∈ K }
⊢ ∀ (b : Bool), CompleteSpace { x // x ∈ bif b then K else Kᗮ }
intro b
no goals
ι : Type ?u.670433
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.670584
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
K : Submodule 𝕜 E
hK : CompleteSpace { x // x ∈ K }
b : Bool
⊢ CompleteSpace { x // x ∈ bif b then K else Kᗮ }
cases b <;> first | exact instOrthogonalCompleteSpace K | assumption
case true
ι : Type ?u.670433
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.670584
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
K : Submodule 𝕜 E
hK : CompleteSpace { x // x ∈ K }
⊢ CompleteSpace { x // x ∈ bif true then K else Kᗮ }
case true
ι : Type ?u.670433
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.670584
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
K : Submodule 𝕜 E
hK : CompleteSpace { x // x ∈ K }
⊢ CompleteSpace { x // x ∈ bif true then K else Kᗮ }
exact instOrthogonalCompleteSpace K
no goals
case true
ι : Type ?u.670433
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.670584
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
K : Submodule 𝕜 E
hK : CompleteSpace { x // x ∈ K }
⊢ CompleteSpace { x // x ∈ bif true then K else Kᗮ }
assumption