awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hv : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = -v i
hj : w j = -v j
⊢ ⟪v i, v j⟫ = if i = j then 1 else 0

Tactic:
replace hv := hv i j
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = v i
hj : w j = v j
hv : ⟪v i, v j⟫ = if i = j then 1 else 0
pos : ∀ (h : i = j) (hv : ⟪v i, v j⟫ = 1), ⟪w i, w j⟫ = 1
neg : ∀ (h : ¬i = j) (hv : ⟪v i, v j⟫ = 0), ⟪w i, w j⟫ = 0
⊢ ⟪w i, w j⟫ = if i = j then 1 else 0

Tactic:
split_ifs at hv ⊢ with h
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = v i
hj : w j = -v j
hv : ⟪v i, v j⟫ = if i = j then 1 else 0
pos : ∀ (h : i = j) (hv : ⟪v i, v j⟫ = 1), ⟪w i, w j⟫ = 1
neg : ∀ (h : ¬i = j) (hv : ⟪v i, v j⟫ = 0), ⟪w i, w j⟫ = 0
⊢ ⟪w i, w j⟫ = if i = j then 1 else 0

Tactic:
split_ifs at hv ⊢ with h
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = -v i
hj : w j = v j
hv : ⟪v i, v j⟫ = if i = j then 1 else 0
pos : ∀ (h : i = j) (hv : ⟪v i, v j⟫ = 1), ⟪w i, w j⟫ = 1
neg : ∀ (h : ¬i = j) (hv : ⟪v i, v j⟫ = 0), ⟪w i, w j⟫ = 0
⊢ ⟪w i, w j⟫ = if i = j then 1 else 0

Tactic:
split_ifs at hv ⊢ with h
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = -v i
hj : w j = -v j
hv : ⟪v i, v j⟫ = if i = j then 1 else 0
pos : ∀ (h : i = j) (hv : ⟪v i, v j⟫ = 1), ⟪w i, w j⟫ = 1
neg : ∀ (h : ¬i = j) (hv : ⟪v i, v j⟫ = 0), ⟪w i, w j⟫ = 0
⊢ ⟪w i, w j⟫ = if i = j then 1 else 0

Tactic:
split_ifs at hv ⊢ with h
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = v i
hj : w j = v j
h : i = j
hv : ⟪v i, v j⟫ = 1
⊢ ⟪w i, w j⟫ = 1

Tactic:
simpa only [hi, hj, h, inner_neg_right, inner_neg_left, neg_neg, eq_self_iff_true,
      neg_eq_zero] using hv

Premises used: inner_neg_right, neg_eq_zero, neg_neg, eq_self_iff_true, inner_neg_left
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = v i
hj : w j = v j
h : ¬i = j
hv : ⟪v i, v j⟫ = 0
⊢ ⟪w i, w j⟫ = 0

Tactic:
simpa only [hi, hj, h, inner_neg_right, inner_neg_left, neg_neg, eq_self_iff_true,
      neg_eq_zero] using hv

Premises used: inner_neg_right, neg_eq_zero, neg_neg, eq_self_iff_true, inner_neg_left
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = v i
hj : w j = -v j
h : i = j
hv : ⟪v i, v j⟫ = 1
⊢ ⟪w i, w j⟫ = 1

Tactic:
simpa only [hi, hj, h, inner_neg_right, inner_neg_left, neg_neg, eq_self_iff_true,
      neg_eq_zero] using hv

Premises used: inner_neg_right, neg_eq_zero, neg_neg, eq_self_iff_true, inner_neg_left
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = v i
hj : w j = -v j
h : ¬i = j
hv : ⟪v i, v j⟫ = 0
⊢ ⟪w i, w j⟫ = 0

Tactic:
simpa only [hi, hj, h, inner_neg_right, inner_neg_left, neg_neg, eq_self_iff_true,
      neg_eq_zero] using hv

Premises used: inner_neg_right, neg_eq_zero, neg_neg, eq_self_iff_true, inner_neg_left
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = -v i
hj : w j = v j
h : i = j
hv : ⟪v i, v j⟫ = 1
⊢ ⟪w i, w j⟫ = 1

Tactic:
simpa only [hi, hj, h, inner_neg_right, inner_neg_left, neg_neg, eq_self_iff_true,
      neg_eq_zero] using hv

Premises used: inner_neg_right, neg_eq_zero, neg_neg, eq_self_iff_true, inner_neg_left
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = -v i
hj : w j = v j
h : ¬i = j
hv : ⟪v i, v j⟫ = 0
⊢ ⟪w i, w j⟫ = 0

Tactic:
simpa only [hi, hj, h, inner_neg_right, inner_neg_left, neg_neg, eq_self_iff_true,
      neg_eq_zero] using hv

Premises used: inner_neg_right, neg_eq_zero, neg_neg, eq_self_iff_true, inner_neg_left
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = -v i
hj : w j = -v j
h : i = j
hv : ⟪v i, v j⟫ = 1
⊢ ⟪w i, w j⟫ = 1

Tactic:
simpa only [hi, hj, h, inner_neg_right, inner_neg_left, neg_neg, eq_self_iff_true,
      neg_eq_zero] using hv

Premises used: inner_neg_right, neg_eq_zero, neg_neg, eq_self_iff_true, inner_neg_left
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = -v i
hj : w j = -v j
h : ¬i = j
hv : ⟪v i, v j⟫ = 0
⊢ ⟪w i, w j⟫ = 0

Tactic:
simpa only [hi, hj, h, inner_neg_right, inner_neg_left, neg_neg, eq_self_iff_true,
      neg_eq_zero] using hv

Premises used: inner_neg_right, neg_eq_zero, neg_neg, eq_self_iff_true, inner_neg_left
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hv : Orthonormal 𝕜 v
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
rw rw₁ rw₂ rw₃ :
  ∀ (hv : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0) (hw : ∀ (i : ι), w i = v i ∨ w i = -v i) (i j : ι),
    ⟪w i, w j⟫ = if i = j then 1 else 0
⊢ Orthonormal 𝕜 w

Tactic:
classical
  rw [orthonormal_iff_ite] at *
  intro i j
  rcases hw i with hi | hi <;> rcases hw j with hj | hj <;>
    replace hv := hv i j <;> split_ifs at hv ⊢ with h <;>
    simpa only [hi, hj, h, inner_neg_right, inner_neg_left, neg_neg, eq_self_iff_true,
      neg_eq_zero] using hv

Premises used: inner_neg_right, neg_eq_zero, neg_neg, orthonormal_iff_ite, eq_self_iff_true, inner_neg_left
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
⊢ Orthonormal 𝕜 (E := E) fun (x : (↑∅ : Type u_2)) ↦ (↑x : E)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
⊢ Orthonormal 𝕜 (E := E) fun (x : (↑∅ : Type u_2)) ↦ (↑x : E)

Tactic:
classical
  simp
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
η : Type u_5
s : η → Set E
hs : Directed (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) s
h : ∀ (i : η), Orthonormal 𝕜 (E := E) fun (x : (↑(s i) : Type u_2)) ↦ (↑x : E)
rw :
  ∀ (v : E),
    Membership.mem (γ := Set E) (⋃ (i : η), s i) v →
      ∀ (w : E), Membership.mem (γ := Set E) (⋃ (i : η), s i) w → ⟪v, w⟫ = if v = w then 1 else 0
⊢ Orthonormal 𝕜 (E := E) fun (x : (↑(⋃ (i : η), s i) : Type u_2)) ↦ (↑x : E)

Tactic:
rw [orthonormal_subtype_iff_ite]

Premises used: orthonormal_subtype_iff_ite
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
η : Type u_5
s : η → Set E
hs : Directed (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) s
h : ∀ (i : η), Orthonormal 𝕜 (E := E) fun (x : (↑(s i) : Type u_2)) ↦ (↑x : E)
x : E
i : η
hxi : Membership.mem (γ := Set E) ((fun (i : η) ↦ s i) i) x
y : E
j : η
hyj : Membership.mem (γ := Set E) ((fun (i : η) ↦ s i) j) y
obtain : ∀ (k : η) (hik : s i ⊆ s k) (hjk : s j ⊆ s k), ⟪x, y⟫ = if x = y then 1 else 0
⊢ ⟪x, y⟫ = if x = y then 1 else 0

Tactic:
obtain ⟨k, hik, hjk⟩ := hs i j
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
η : Type u_5
s : η → Set E
hs : Directed (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) s
h : ∀ (i : η), Orthonormal 𝕜 (E := E) fun (x : (↑(s i) : Type u_2)) ↦ (↑x : E)
x : E
i : η
hxi : Membership.mem (γ := Set E) ((fun (i : η) ↦ s i) i) x
y : E
j : η
hyj : Membership.mem (γ := Set E) ((fun (i : η) ↦ s i) j) y
k : η
hik : s i ⊆ s k
hjk : s j ⊆ s k
⊢ Orthonormal 𝕜 (E := E) fun (x : (↑(s k) : Type u_2)) ↦ (↑x : E)

Tactic:
have h_orth : Orthonormal 𝕜 (fun x => x : s k → E) := h k
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
η : Type u_5
s : η → Set E
hs : Directed (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) s
h : ∀ (i : η), Orthonormal 𝕜 (E := E) fun (x : (↑(s i) : Type u_2)) ↦ (↑x : E)
x : E
i : η
hxi : Membership.mem (γ := Set E) ((fun (i : η) ↦ s i) i) x
y : E
j : η
hyj : Membership.mem (γ := Set E) ((fun (i : η) ↦ s i) j) y
k : η
hik : s i ⊆ s k
hjk : s j ⊆ s k
h_orth : Orthonormal 𝕜 (E := E) fun (x : (↑(s k) : Type u_2)) ↦ (↑x : E)
⊢ ∀ v ∈ s k, ∀ w ∈ s k, ⟪v, w⟫ = if v = w then 1 else 0

Tactic:
rw [orthonormal_subtype_iff_ite] at h_orth

Premises used: orthonormal_subtype_iff_ite
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
η : Type u_5
s : η → Set E
hs : Directed (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) s
h : ∀ (i : η), Orthonormal 𝕜 (E := E) fun (x : (↑(s i) : Type u_2)) ↦ (↑x : E)
x : E
i : η
hxi : Membership.mem (γ := Set E) ((fun (i : η) ↦ s i) i) x
y : E
j : η
hyj : Membership.mem (γ := Set E) ((fun (i : η) ↦ s i) j) y
k : η
hik : s i ⊆ s k
hjk : s j ⊆ s k
h_orth : ∀ v ∈ s k, ∀ w ∈ s k, ⟪v, w⟫ = if v = w then 1 else 0
⊢ ⟪x, y⟫ = if x = y then 1 else 0

Tactic:
h_orth x (hik hxi) y (hjk hyj)
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
η : Type u_5
s : η → Set E
hs : Directed (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) s
h : ∀ (i : η), Orthonormal 𝕜 (E := E) fun (x : (↑(s i) : Type u_2)) ↦ (↑x : E)
x : E
i : η
hxi : Membership.mem (γ := Set E) ((fun (i : η) ↦ s i) i) x
y : E
j : η
hyj : Membership.mem (γ := Set E) ((fun (i : η) ↦ s i) j) y
k : η
hik : s i ⊆ s k
hjk : s j ⊆ s k
h_orth : ∀ v ∈ s k, ∀ w ∈ s k, ⟪v, w⟫ = if v = w then 1 else 0
⊢ ⟪x, y⟫ = if x = y then 1 else 0

Tactic:
exact h_orth x (hik hxi) y (hjk hyj)
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
η : Type u_5
s : η → Set E
hs : Directed (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) s
h : ∀ (i : η), Orthonormal 𝕜 (E := E) fun (x : (↑(s i) : Type u_2)) ↦ (↑x : E)
rw rw₁ rw₂ :
  ∀ (v : E),
    Membership.mem (γ := Set E) (⋃ (i : η), s i) v →
      ∀ (w : E), Membership.mem (γ := Set E) (⋃ (i : η), s i) w → ⟪v, w⟫ = if v = w then 1 else 0
rw₃ :
  ∀ (x : E) (i : η) (hxi : Membership.mem (γ := Set E) ((fun (i : η) ↦ s i) i) x) (y : E) (j : η)
    (hyj : Membership.mem (γ := Set E) ((fun (i : η) ↦ s i) j) y), ⟪x, y⟫ = if x = y then 1 else 0
rw₄ :
  ∀ (x : E) (i : η) (hxi : Membership.mem (γ := Set E) ((fun (i : η) ↦ s i) i) x) (y : E) (j : η)
    (hyj : Membership.mem (γ := Set E) ((fun (i : η) ↦ s i) j) y) (k : η) (hik : s i ⊆ s k) (hjk : s j ⊆ s k),
    ⟪x, y⟫ = if x = y then 1 else 0
rw₅ :
  ∀ (x : E) (i : η) (hxi : Membership.mem (γ := Set E) ((fun (i : η) ↦ s i) i) x) (y : E) (j : η)
    (hyj : Membership.mem (γ := Set E) ((fun (i : η) ↦ s i) j) y) (k : η) (hik : s i ⊆ s k) (hjk : s j ⊆ s k)
    (h_orth : Orthonormal 𝕜 (E := E) fun (x : (↑(s k) : Type u_2)) ↦ (↑x : E)), ⟪x, y⟫ = if x = y then 1 else 0
rw₆ :
  ∀ (x : E) (i : η) (hxi : Membership.mem (γ := Set E) ((fun (i : η) ↦ s i) i) x) (y : E) (j : η)
    (hyj : Membership.mem (γ := Set E) ((fun (i : η) ↦ s i) j) y) (k : η) (hik : s i ⊆ s k) (hjk : s j ⊆ s k)
    (h_orth : ∀ v ∈ s k, ∀ w ∈ s k, ⟪v, w⟫ = if v = w then 1 else 0), ⟪x, y⟫ = if x = y then 1 else 0
⊢ Orthonormal 𝕜 (E := E) fun (x : (↑(⋃ (i : η), s i) : Type u_2)) ↦ (↑x : E)

Tactic:
classical
  rw [orthonormal_subtype_iff_ite]
  rintro x ⟨_, ⟨i, rfl⟩, hxi⟩ y ⟨_, ⟨j, rfl⟩, hyj⟩
  obtain ⟨k, hik, hjk⟩ := hs i j
  have h_orth : Orthonormal 𝕜 (fun x => x : s k → E) := h k
  rw [orthonormal_subtype_iff_ite] at h_orth
  exact h_orth x (hik hxi) y (hjk hyj)

Premises used: orthonormal_subtype_iff_ite, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
s : Set (Set E)
hs : DirectedOn (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, Orthonormal 𝕜 (E := E) fun (x : (↑a : Type u_2)) ↦ (↑x : E)
rw : Orthonormal 𝕜 (E := E) fun (x : (↑(⋃ (i : (↑s : Type u_2)), (↑i : Set E)) : Type u_2)) ↦ (↑x : E)
⊢ Orthonormal 𝕜 (E := E) fun (x : (↑(⋃₀ s) : Type u_2)) ↦ (↑x : E)

Tactic:
rw [Set.sUnion_eq_iUnion]

Premises used: Set.sUnion_eq_iUnion
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
s : Set (Set E)
hs : DirectedOn (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, Orthonormal 𝕜 (E := E) fun (x : (↑a : Type u_2)) ↦ (↑x : E)
⊢ ∀ (i : (↑s : Type u_2)), Orthonormal 𝕜 (E := E) fun (x : (↑(↑i : Set E) : Type u_2)) ↦ (↑x : E)

Tactic:
simpa using h
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
s : Set (Set E)
hs : DirectedOn (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, Orthonormal 𝕜 (E := E) fun (x : (↑a : Type u_2)) ↦ (↑x : E)
⊢ Orthonormal 𝕜 (E := E) fun (x : (↑(⋃ (i : (↑s : Type u_2)), (↑i : Set E)) : Type u_2)) ↦ (↑x : E)

Tactic:
exact orthonormal_iUnion_of_directed hs.directed_val (by simpa using h)

Premises used: orthonormal_iUnion_of_directed, DirectedOn.directed_val
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
s : Set E
hs : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ s }) (Subtype.val (p := fun (x : E) ↦ x ∈ s))
refine_2 :
  ∀
    (this :
      ∃ (m : Set E),
        s ⊆ m ∧
          Maximal
            (fun (x : Set E) ↦
              Membership.mem (γ := Set (Set E))
                {b : Set E |
                  Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ b })
                    (Subtype.val (p := fun (x : E) ↦ x ∈ b))}
                x)
            m),
    ∃ w ⊇ s,
      Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ w }) (Subtype.val (p := fun (x : E) ↦ x ∈ w)) ∧
        ∀ u ⊇ w,
          Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ u }) (Subtype.val (p := fun (x : E) ↦ x ∈ u)) →
            u = w
refine_1 :
  ∀
    c ⊆
      {b : Set E |
        Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ b }) (Subtype.val (p := fun (x : E) ↦ x ∈ b))},
    IsChain (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) c →
      c.Nonempty →
        ∃ (ub : Set E),
          Membership.mem (γ := Set (Set E))
              {b : Set E |
                Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ b })
                  (Subtype.val (p := fun (x : E) ↦ x ∈ b))}
              ub ∧
            ∀ s ∈ c, s ⊆ ub
⊢ ∃ w ⊇ s,
    Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ w }) (Subtype.val (p := fun (x : E) ↦ x ∈ w)) ∧
      ∀ u ⊇ w,
        Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ u }) (Subtype.val (p := fun (x : E) ↦ x ∈ u)) →
          u = w

Tactic:
have := zorn_subset_nonempty { b | Orthonormal 𝕜 (Subtype.val : b → E) } ?_ _ hs
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
s : Set E
hs : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ s }) (Subtype.val (p := fun (x : E) ↦ x ∈ s))
this :
  ∃ (m : Set E),
    s ⊆ m ∧
      Maximal
        (fun (x : Set E) ↦
          Membership.mem (γ := Set (Set E))
            {b : Set E |
              Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ b }) (Subtype.val (p := fun (x : E) ↦ x ∈ b))}
            x)
        m
refine_2 :
  ∀ (b : Set E)
    (hb :
      s ⊆ b ∧
        Maximal
          (fun (x : Set E) ↦
            Membership.mem (γ := Set (Set E))
              {b : Set E |
                Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ b })
                  (Subtype.val (p := fun (x : E) ↦ x ∈ b))}
              x)
          b),
    ∃ w ⊇ s,
      Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ w }) (Subtype.val (p := fun (x : E) ↦ x ∈ w)) ∧
        ∀ u ⊇ w,
          Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ u }) (Subtype.val (p := fun (x : E) ↦ x ∈ u)) →
            u = w
⊢ ∃ w ⊇ s,
    Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ w }) (Subtype.val (p := fun (x : E) ↦ x ∈ w)) ∧
      ∀ u ⊇ w,
        Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ u }) (Subtype.val (p := fun (x : E) ↦ x ∈ u)) →
          u = w

Tactic:
obtain ⟨b, hb⟩ := this
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
s : Set E
hs : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ s }) (Subtype.val (p := fun (x : E) ↦ x ∈ s))
b : Set E
hb :
  s ⊆ b ∧
    Maximal
      (fun (x : Set E) ↦
        Membership.mem (γ := Set (Set E))
          {b : Set E |
            Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ b }) (Subtype.val (p := fun (x : E) ↦ x ∈ b))}
          x)
      b
⊢ ∃ w ⊇ s,
    Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ w }) (Subtype.val (p := fun (x : E) ↦ x ∈ w)) ∧
      ∀ u ⊇ w,
        Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ u }) (Subtype.val (p := fun (x : E) ↦ x ∈ u)) →
          u = w

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

Premises used: Maximal.eq_of_ge, And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
s : Set E
hs : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ s }) (Subtype.val (p := fun (x : E) ↦ x ∈ s))
b : Set E
hb :
  s ⊆ b ∧
    Maximal
      (fun (x : Set E) ↦
        Membership.mem (γ := Set (Set E))
          {b : Set E |
            Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ b }) (Subtype.val (p := fun (x : E) ↦ x ∈ b))}
          x)
      b
⊢ ∃ w ⊇ s,
    Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ w }) (Subtype.val (p := fun (x : E) ↦ x ∈ w)) ∧
      ∀ u ⊇ w,
        Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ u }) (Subtype.val (p := fun (x : E) ↦ x ∈ u)) →
          u = w

Tactic:
exact ⟨b, hb.1, hb.2.1, fun u hus hu => hb.2.eq_of_ge hu hus⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
s : Set E
hs : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ s }) (Subtype.val (p := fun (x : E) ↦ x ∈ s))
⊢ ∀
    c ⊆
      {b : Set E |
        Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ b }) (Subtype.val (p := fun (x : E) ↦ x ∈ b))},
    IsChain (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) c →
      c.Nonempty →
        ∃ (ub : Set E),
          Membership.mem (γ := Set (Set E))
              {b : Set E |
                Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ b })
                  (Subtype.val (p := fun (x : E) ↦ x ∈ b))}
              ub ∧
            ∀ s ∈ c, s ⊆ ub

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

Premises used: Set.sUnion, And.intro, Exists.intro
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
s : Set E
hs : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ s }) (Subtype.val (p := fun (x : E) ↦ x ∈ s))
refine_1 :
  ∀ (c : Set (Set E))
    (hc :
      c ⊆
        {b : Set E |
          Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ b }) (Subtype.val (p := fun (x : E) ↦ x ∈ b))})
    (cc : IsChain (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) c) (_c0 : c.Nonempty),
    Membership.mem (γ := Set (Set E))
      {b : Set E |
        Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ b }) (Subtype.val (p := fun (x : E) ↦ x ∈ b))}
      (⋃₀ c)
refine_1₁ :
  ∀ (c : Set (Set E))
    (hc :
      c ⊆
        {b : Set E |
          Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ b }) (Subtype.val (p := fun (x : E) ↦ x ∈ b))})
    (cc : IsChain (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) c) (_c0 : c.Nonempty), ∀ s ∈ c, s ⊆ ⋃₀ c
⊢ ∀
    c ⊆
      {b : Set E |
        Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ b }) (Subtype.val (p := fun (x : E) ↦ x ∈ b))},
    IsChain (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) c →
      c.Nonempty →
        ∃ (ub : Set E),
          Membership.mem (γ := Set (Set E))
              {b : Set E |
                Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ b })
                  (Subtype.val (p := fun (x : E) ↦ x ∈ b))}
              ub ∧
            ∀ s ∈ c, s ⊆ ub

Tactic:
refine fun c hc cc _c0 => ⟨⋃₀ c, ?_, ?_⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
s : Set E
hs : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ s }) (Subtype.val (p := fun (x : E) ↦ x ∈ s))
c : Set (Set E)
hc :
  c ⊆
    {b : Set E |
      Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ b }) (Subtype.val (p := fun (x : E) ↦ x ∈ b))}
cc : IsChain (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) c
_c0 : c.Nonempty
⊢ Membership.mem (γ := Set (Set E))
    {b : Set E |
      Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ b }) (Subtype.val (p := fun (x : E) ↦ x ∈ b))}
    (⋃₀ c)

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

Premises used: Orthonormal, Set.Mem, setOf, IsChain.directedOn, orthonormal_sUnion_of_directed