-- Mathlib/Analysis/InnerProductSpace/Orthonormal.lean
theorem exists_maximal_orthonormal {s : Set E} (hs : Orthonormal 𝕜 (Subtype.val : s → E)) :
    ∃ w ⊇ s, Orthonormal 𝕜 (Subtype.val : w → E) ∧
      ∀ u ⊇ w, Orthonormal 𝕜 (Subtype.val : u → E) → u = w

Proof state:
case refine_1.refine_1
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
s : Set E
hs : Orthonormal 𝕜 Subtype.val
c : Set (Set E)
hc : c ⊆ {b | Orthonormal 𝕜 Subtype.val}
cc : IsChain (fun x1 x2 => x1 ⊆ x2) c
_c0 : c.Nonempty
⊢ ⋃₀ c ∈ {b | Orthonormal 𝕜 Subtype.val}

Tactic:
exact orthonormal_sUnion_of_directed cc.directedOn fun x xc => hc xc

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
s : Set E
hs : Orthonormal 𝕜 Subtype.val
⊢ ∃ w ⊇ s, Orthonormal 𝕜 Subtype.val ∧ ∀ u ⊇ w, Orthonormal 𝕜 Subtype.val → u = w

Tactic:
have := zorn_subset_nonempty { b | Orthonormal 𝕜 (Subtype.val : b → E) } ?_ _ hs

Result:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
s : Set E
hs : Orthonormal 𝕜 Subtype.val
this : ∃ m, s ⊆ m ∧ Maximal (fun x => x ∈ {b | Orthonormal 𝕜 Subtype.val}) m
⊢ ∃ w ⊇ s, Orthonormal 𝕜 Subtype.val ∧ ∀ u ⊇ w, Orthonormal 𝕜 Subtype.val → u = w

case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
s : Set E
hs : Orthonormal 𝕜 Subtype.val
⊢ ∀ c ⊆ {b | Orthonormal 𝕜 Subtype.val},
    IsChain (fun x1 x2 => x1 ⊆ x2) c → c.Nonempty → ∃ ub ∈ {b | Orthonormal 𝕜 Subtype.val}, ∀ s ∈ c, s ⊆ ub

Proof state:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
s : Set E
hs : Orthonormal 𝕜 Subtype.val
this : ∃ m, s ⊆ m ∧ Maximal (fun x => x ∈ {b | Orthonormal 𝕜 Subtype.val}) m
⊢ ∃ w ⊇ s, Orthonormal 𝕜 Subtype.val ∧ ∀ u ⊇ w, Orthonormal 𝕜 Subtype.val → u = w

Tactic:
obtain ⟨b, hb⟩ := this

Result:
case refine_2.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
s : Set E
hs : Orthonormal 𝕜 Subtype.val
b : Set E
hb : s ⊆ b ∧ Maximal (fun x => x ∈ {b | Orthonormal 𝕜 Subtype.val}) b
⊢ ∃ w ⊇ s, Orthonormal 𝕜 Subtype.val ∧ ∀ u ⊇ w, Orthonormal 𝕜 Subtype.val → u = w

Proof state:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
s : Set E
hs : Orthonormal 𝕜 Subtype.val
⊢ ∀ c ⊆ {b | Orthonormal 𝕜 Subtype.val},
    IsChain (fun x1 x2 => x1 ⊆ x2) c → c.Nonempty → ∃ ub ∈ {b | Orthonormal 𝕜 Subtype.val}, ∀ s ∈ c, s ⊆ ub

Tactic:
refine fun c hc cc _c0 => ⟨⋃₀ c, ?_, ?_⟩

Result:
case refine_1.refine_1
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
s : Set E
hs : Orthonormal 𝕜 Subtype.val
c : Set (Set E)
hc : c ⊆ {b | Orthonormal 𝕜 Subtype.val}
cc : IsChain (fun x1 x2 => x1 ⊆ x2) c
_c0 : c.Nonempty
⊢ ⋃₀ c ∈ {b | Orthonormal 𝕜 Subtype.val}

case refine_1.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
s : Set E
hs : Orthonormal 𝕜 Subtype.val
c : Set (Set E)
hc : c ⊆ {b | Orthonormal 𝕜 Subtype.val}
cc : IsChain (fun x1 x2 => x1 ⊆ x2) c
_c0 : c.Nonempty
⊢ ∀ s ∈ c, s ⊆ ⋃₀ c

Proof state:
case refine_1.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
s : Set E
hs : Orthonormal 𝕜 Subtype.val
c : Set (Set E)
hc : c ⊆ {b | Orthonormal 𝕜 Subtype.val}
cc : IsChain (fun x1 x2 => x1 ⊆ x2) c
_c0 : c.Nonempty
⊢ ∀ s ∈ c, s ⊆ ⋃₀ c

Tactic:
exact fun _ => Set.subset_sUnion_of_mem

Result:
no goals

Proof state:
case refine_2.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
s : Set E
hs : Orthonormal 𝕜 Subtype.val
b : Set E
hb : s ⊆ b ∧ Maximal (fun x => x ∈ {b | Orthonormal 𝕜 Subtype.val}) b
⊢ ∃ w ⊇ s, Orthonormal 𝕜 Subtype.val ∧ ∀ u ⊇ w, Orthonormal 𝕜 Subtype.val → u = w

Tactic:
exact ⟨b, hb.1, hb.2.1, fun u hus hu => hb.2.eq_of_ge hu hus⟩

Result:
no goals