case refine_2
𝕜 : Type u_2
E : Type u_1
F : Type ?u.2163317
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.2163366
dec_ι : DecidableEq ι
s : Set E
hs : Orthonormal 𝕜 Subtype.val
this :
  ∃ m, m ∈ {b | Orthonormal 𝕜 Subtype.val} ∧ s ⊆ m ∧ ∀ (a : Set E), a ∈ {b | Orthonormal 𝕜 Subtype.val} → m ⊆ a → a = m
⊢ ∃ w _hw, Orthonormal 𝕜 Subtype.val ∧ ∀ (u : Set E), u ⊇ w → Orthonormal 𝕜 Subtype.val → u = w

case refine_1
𝕜 : Type u_2
E : Type u_1
F : Type ?u.2163317
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.2163366
dec_ι : DecidableEq ι
s : Set E
hs : Orthonormal 𝕜 Subtype.val
⊢ ∀ (c : Set (Set E)),
    c ⊆ {b | Orthonormal 𝕜 Subtype.val} →
      IsChain (fun x x_1 => x ⊆ x_1) c →
        Set.Nonempty c → ∃ ub, ub ∈ {b | Orthonormal 𝕜 Subtype.val} ∧ ∀ (s : Set E), s ∈ c → s ⊆ ub
𝕜 : Type u_2
E : Type u_1
F : Type ?u.2163317
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.2163366
dec_ι : DecidableEq ι
s : Set E
hs : Orthonormal 𝕜 Subtype.val
⊢ ∃ w _hw, Orthonormal 𝕜 Subtype.val ∧ ∀ (u : Set E), u ⊇ w → Orthonormal 𝕜 Subtype.val → u = w
have := zorn_subset_nonempty { b | Orthonormal 𝕜 (Subtype.val : b → E) } ?_ _ hs
case refine_2.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.2163317
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.2163366
dec_ι : DecidableEq ι
s : Set E
hs : Orthonormal 𝕜 Subtype.val
b : Set E
bi : b ∈ {b | Orthonormal 𝕜 Subtype.val}
sb : s ⊆ b
h : ∀ (a : Set E), a ∈ {b | Orthonormal 𝕜 Subtype.val} → b ⊆ a → a = b
⊢ ∃ w _hw, Orthonormal 𝕜 Subtype.val ∧ ∀ (u : Set E), u ⊇ w → Orthonormal 𝕜 Subtype.val → u = w

case refine_1
𝕜 : Type u_2
E : Type u_1
F : Type ?u.2163317
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.2163366
dec_ι : DecidableEq ι
s : Set E
hs : Orthonormal 𝕜 Subtype.val
⊢ ∀ (c : Set (Set E)),
    c ⊆ {b | Orthonormal 𝕜 Subtype.val} →
      IsChain (fun x x_1 => x ⊆ x_1) c →
        Set.Nonempty c → ∃ ub, ub ∈ {b | Orthonormal 𝕜 Subtype.val} ∧ ∀ (s : Set E), s ∈ c → s ⊆ ub
case refine_2
𝕜 : Type u_2
E : Type u_1
F : Type ?u.2163317
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.2163366
dec_ι : DecidableEq ι
s : Set E
hs : Orthonormal 𝕜 Subtype.val
this :
  ∃ m, m ∈ {b | Orthonormal 𝕜 Subtype.val} ∧ s ⊆ m ∧ ∀ (a : Set E), a ∈ {b | Orthonormal 𝕜 Subtype.val} → m ⊆ a → a = m
⊢ ∃ w _hw, Orthonormal 𝕜 Subtype.val ∧ ∀ (u : Set E), u ⊇ w → Orthonormal 𝕜 Subtype.val → u = w

case refine_1
𝕜 : Type u_2
E : Type u_1
F : Type ?u.2163317
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.2163366
dec_ι : DecidableEq ι
s : Set E
hs : Orthonormal 𝕜 Subtype.val
⊢ ∀ (c : Set (Set E)),
    c ⊆ {b | Orthonormal 𝕜 Subtype.val} →
      IsChain (fun x x_1 => x ⊆ x_1) c →
        Set.Nonempty c → ∃ ub, ub ∈ {b | Orthonormal 𝕜 Subtype.val} ∧ ∀ (s : Set E), s ∈ c → s ⊆ ub
obtain ⟨b, bi, sb, h⟩ := this
case refine_2.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.2163317
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.2163366
dec_ι : DecidableEq ι
s : Set E
hs : Orthonormal 𝕜 Subtype.val
b : Set E
bi : b ∈ {b | Orthonormal 𝕜 Subtype.val}
sb : s ⊆ b
h : ∀ (a : Set E), a ∈ {b | Orthonormal 𝕜 Subtype.val} → b ⊆ a → a = b
⊢ ∀ (u : Set E), u ⊇ b → Orthonormal 𝕜 Subtype.val → u = b
case refine_2.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.2163317
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.2163366
dec_ι : DecidableEq ι
s : Set E
hs : Orthonormal 𝕜 Subtype.val
b : Set E
bi : b ∈ {b | Orthonormal 𝕜 Subtype.val}
sb : s ⊆ b
h : ∀ (a : Set E), a ∈ {b | Orthonormal 𝕜 Subtype.val} → b ⊆ a → a = b
⊢ ∃ w _hw, Orthonormal 𝕜 Subtype.val ∧ ∀ (u : Set E), u ⊇ w → Orthonormal 𝕜 Subtype.val → u = w
refine' ⟨b, sb, bi, _⟩
no goals
case refine_2.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.2163317
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.2163366
dec_ι : DecidableEq ι
s : Set E
hs : Orthonormal 𝕜 Subtype.val
b : Set E
bi : b ∈ {b | Orthonormal 𝕜 Subtype.val}
sb : s ⊆ b
h : ∀ (a : Set E), a ∈ {b | Orthonormal 𝕜 Subtype.val} → b ⊆ a → a = b
⊢ ∀ (u : Set E), u ⊇ b → Orthonormal 𝕜 Subtype.val → u = b
exact fun u hus hu => h u hu hus
case refine_1.refine'_1
𝕜 : Type u_2
E : Type u_1
F : Type ?u.2163317
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.2163366
dec_ι : DecidableEq ι
s : Set E
hs : Orthonormal 𝕜 Subtype.val
c : Set (Set E)
hc : c ⊆ {b | Orthonormal 𝕜 Subtype.val}
cc : IsChain (fun x x_1 => x ⊆ x_1) c
_c0 : Set.Nonempty c
⊢ ⋃₀ c ∈ {b | Orthonormal 𝕜 Subtype.val}

case refine_1.refine'_2
𝕜 : Type u_2
E : Type u_1
F : Type ?u.2163317
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.2163366
dec_ι : DecidableEq ι
s : Set E
hs : Orthonormal 𝕜 Subtype.val
c : Set (Set E)
hc : c ⊆ {b | Orthonormal 𝕜 Subtype.val}
cc : IsChain (fun x x_1 => x ⊆ x_1) c
_c0 : Set.Nonempty c
⊢ ∀ (s : Set E), s ∈ c → s ⊆ ⋃₀ c
case refine_1
𝕜 : Type u_2
E : Type u_1
F : Type ?u.2163317
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.2163366
dec_ι : DecidableEq ι
s : Set E
hs : Orthonormal 𝕜 Subtype.val
⊢ ∀ (c : Set (Set E)),
    c ⊆ {b | Orthonormal 𝕜 Subtype.val} →
      IsChain (fun x x_1 => x ⊆ x_1) c →
        Set.Nonempty c → ∃ ub, ub ∈ {b | Orthonormal 𝕜 Subtype.val} ∧ ∀ (s : Set E), s ∈ c → s ⊆ ub
refine' fun c hc cc _c0 => ⟨⋃₀ c, _, _⟩
no goals
case refine_1.refine'_1
𝕜 : Type u_2
E : Type u_1
F : Type ?u.2163317
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.2163366
dec_ι : DecidableEq ι
s : Set E
hs : Orthonormal 𝕜 Subtype.val
c : Set (Set E)
hc : c ⊆ {b | Orthonormal 𝕜 Subtype.val}
cc : IsChain (fun x x_1 => x ⊆ x_1) c
_c0 : Set.Nonempty c
⊢ ⋃₀ c ∈ {b | Orthonormal 𝕜 Subtype.val}
exact orthonormal_sUnion_of_directed cc.directedOn fun x xc => hc xc
no goals
case refine_1.refine'_2
𝕜 : Type u_2
E : Type u_1
F : Type ?u.2163317
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.2163366
dec_ι : DecidableEq ι
s : Set E
hs : Orthonormal 𝕜 Subtype.val
c : Set (Set E)
hc : c ⊆ {b | Orthonormal 𝕜 Subtype.val}
cc : IsChain (fun x x_1 => x ⊆ x_1) c
_c0 : Set.Nonempty c
⊢ ∀ (s : Set E), s ∈ c → s ⊆ ⋃₀ c
exact fun _ => Set.subset_sUnion_of_mem