awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
x : E
hx' : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ x
hx : x ≠ 0
e : E := HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖x‖ : 𝕜)⁻¹ x
he : ‖e‖ = 1
he' : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ e
he'' : e ∉ v
h_end : ∀ a ∈ v, ⟪a, e⟫_𝕜 = 0
a : E
ha' : a ∈ insert e v
mp :
  ∀ (ha : a = e) ⦃j : { x : E // x ∈ insert e v }⦄,
    Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) a ha' ≠ j →
      (fun (i j : { x : E // x ∈ insert e v }) ↦ ⟪(↑i : E), (↑j : E)⟫_𝕜 = 0)
        (Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) a ha') j
⊢ ∀ ⦃j : { x : E // x ∈ insert e v }⦄,
    Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) a ha' ≠ j →
      (fun (i j : { x : E // x ∈ insert e v }) ↦ ⟪(↑i : E), (↑j : E)⟫_𝕜 = 0)
        (Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) a ha') j
have mp₁ : ∀ (ha : a ∈ v) ⦃j : { x : E // x ∈ insert e v }⦄,
  Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) a ha' ≠ j →
    (fun (i j : { x : E // x ∈ insert e v }) ↦ ⟪(↑i : E), (↑j : E)⟫_𝕜 = 0)
      (Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) a ha') j
Tactic: rcases eq_or_mem_of_mem_insert ha' with ha | ha
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
x : E
hx' : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ x
hx : x ≠ 0
e : E := HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖x‖ : 𝕜)⁻¹ x
he : ‖e‖ = 1
he' : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ e
he'' : e ∉ v
h_end : ∀ a ∈ v, ⟪a, e⟫_𝕜 = 0
a : E
ha' : a ∈ insert e v
ha : a = e
b : E
hb' : b ∈ insert e v
hab' : Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) a ha' ≠ Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) b hb'
⊢ ⟪(↑(Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) a ha') : E),
      (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) b hb') : E)⟫_𝕜 =
    0
have hb : b ∈ v
Tactic: have hb : b ∈ v := by grind
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
x : E
hx' : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ x
hx : x ≠ 0
e : E := HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖x‖ : 𝕜)⁻¹ x
he : ‖e‖ = 1
he' : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ e
he'' : e ∉ v
h_end : ∀ a ∈ v, ⟪a, e⟫_𝕜 = 0
a : E
ha' : a ∈ insert e v
ha : a = e
b : E
hb' : b ∈ insert e v
hab' : Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) a ha' ≠ Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) b hb'
hb : b ∈ v
⊢ ⟪(↑(Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) a ha') : E),
      (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) b hb') : E)⟫_𝕜 =
    0
have mp : ⟪(↑(Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) b hb') : E),
    (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) a ha') : E)⟫_𝕜 =
  0
Tactic: rw [inner_eq_zero_symm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
x : E
hx' : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ x
hx : x ≠ 0
e : E := HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖x‖ : 𝕜)⁻¹ x
he : ‖e‖ = 1
he' : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ e
he'' : e ∉ v
h_end : ∀ a ∈ v, ⟪a, e⟫_𝕜 = 0
a : E
ha' : a ∈ insert e v
ha : a ∈ v
b : E
hb' : b ∈ insert e v
hab' : Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) a ha' ≠ Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) b hb'
⊢ ⟪(↑(Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) a ha') : E),
      (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) b hb') : E)⟫_𝕜 =
    0
have mp : ∀ (hb : b = e),
  ⟪(↑(Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) a ha') : E),
      (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) b hb') : E)⟫_𝕜 =
    0
Tactic: rcases eq_or_mem_of_mem_insert hb' with hb | hb
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
x : E
hx' : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ x
hx : x ≠ 0
e : E := HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖x‖ : 𝕜)⁻¹ x
he : ‖e‖ = 1
he' : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ e
he'' : e ∉ v
h_end : ∀ a ∈ v, ⟪a, e⟫_𝕜 = 0
a : E
ha' : a ∈ insert e v
ha : a ∈ v
b : E
hb' : b ∈ insert e v
hab' : Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) a ha' ≠ Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) b hb'
mp :
  ∀ (hb : b = e),
    ⟪(↑(Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) a ha') : E),
        (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) b hb') : E)⟫_𝕜 =
      0
⊢ ⟪(↑(Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) a ha') : E),
      (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) b hb') : E)⟫_𝕜 =
    0
have mp₁ : ∀ (hb : b ∈ v),
  ⟪(↑(Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) a ha') : E),
      (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) b hb') : E)⟫_𝕜 =
    0
Tactic: rcases eq_or_mem_of_mem_insert hb' with hb | hb
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
x : E
hx' : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ x
hx : x ≠ 0
e : E := HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖x‖ : 𝕜)⁻¹ x
he : ‖e‖ = 1
he' : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ e
he'' : e ∉ v
h_end : ∀ a ∈ v, ⟪a, e⟫_𝕜 = 0
a : E
ha' : a ∈ insert e v
ha : a ∈ v
b : E
hb' : b ∈ insert e v
hab' : Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) a ha' ≠ Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) b hb'
hb : b ∈ v
hab'' : Subtype.mk (p := fun (x : E) ↦ x ∈ v) a ha = Subtype.mk (p := fun (x : E) ↦ x ∈ v) b hb
⊢ False
have apply : Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) a ha' = Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) b hb'
Tactic: apply hab'
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
x : E
hx' : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ x
hx : x ≠ 0
e : E := HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖x‖ : 𝕜)⁻¹ x
he : ‖e‖ = 1
he' : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ e
he'' : e ∉ v
h_end : ∀ a ∈ v, ⟪a, e⟫_𝕜 = 0
a : E
ha' : a ∈ insert e v
ha : a ∈ v
b : E
hb' : b ∈ insert e v
hab' : Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) a ha' ≠ Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) b hb'
hb : b ∈ v
⊢ ⟪(↑(Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) a ha') : E),
      (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) b hb') : E)⟫_𝕜 =
    0
have this : Subtype.mk (p := fun (x : E) ↦ x ∈ v) a ha ≠ Subtype.mk (p := fun (x : E) ↦ x ∈ v) b hb
Tactic: have : (⟨a, ha⟩ : v) ≠ ⟨b, hb⟩ := by
        intro hab''
        apply hab'
        simpa using hab''
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
⊢ (∀ (x : E), Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ x → x = 0) →
    ∀ u ⊇ v,
      Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ u }) (Subtype.val (p := fun (x : E) ↦ x ∈ u)) → u = v
have mpr : (∀ (x : E), Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ x → x = 0) →
  ∀ u ⊇ v,
    Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ u }) (Subtype.val (p := fun (x : E) ↦ x ∈ u)) →
      u ⊆ v ∧ v ⊆ u
Tactic: simp only [Subset.antisymm_iff]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
h : ∀ (x : E), Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ x → x = 0
u : Set E
huv : v ⊆ u
hu : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ u }) (Subtype.val (p := fun (x : E) ↦ x ∈ u))
⊢ u ⊆ v ∧ v ⊆ u
have mpr : u ⊆ v
Tactic: refine ⟨?_, huv⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
h : ∀ (x : E), Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ x → x = 0
u : Set E
huv : v ⊆ u
hu : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ u }) (Subtype.val (p := fun (x : E) ↦ x ∈ u))
x : E
hxu : x ∈ u
⊢ x ∈ v
have mpr : x ∉ v → Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ x
Tactic: refine ((mt (h x)) (hu.ne_zero ⟨x, hxu⟩)).imp_symm ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
h : ∀ (x : E), Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ x → x = 0
u : Set E
huv : v ⊆ u
hu : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ u }) (Subtype.val (p := fun (x : E) ↦ x ∈ u))
x : E
hxu : x ∈ u
hxv : x ∉ v
y : E
hy : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v) y
⊢ ⟪y, x⟫_𝕜 = 0
have hxv' : Subtype.mk (p := fun (x : E) ↦ x ∈ u) x hxu ∉ Subtype.val (p := fun (x : E) ↦ x ∈ u) ⁻¹' v
Tactic: have hxv' : (⟨x, hxu⟩ : u) ∉ ((↑) ⁻¹' v : Set u) := by simp [hxv]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
h : ∀ (x : E), Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ x → x = 0
u : Set E
huv : v ⊆ u
hu : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ u }) (Subtype.val (p := fun (x : E) ↦ x ∈ u))
x : E
hxu : x ∈ u
hxv : x ∉ v
y : E
hy : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v) y
hxv' : Subtype.mk (p := fun (x : E) ↦ x ∈ u) x hxu ∉ Subtype.val (p := fun (x : E) ↦ x ∈ u) ⁻¹' v
⊢ ∃ (l : Finsupp.{u_2, u_1} (↑u : Type u_2) 𝕜),
    Membership.mem (γ := Submodule 𝕜 (Finsupp.{u_2, u_1} (↑u : Type u_2) 𝕜))
        (supported 𝕜 𝕜 (Subtype.val (p := fun (x : E) ↦ x ∈ u) ⁻¹' v)) l ∧
      (linearCombination 𝕜 (Subtype.val (p := fun (x : E) ↦ x ∈ u)) : (a : { x : E // x ∈ u } →₀ 𝕜) → E) l = y
have rw : Membership.mem (γ := Submodule 𝕜 E)
  (span 𝕜
    (image (α := (↑u : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ u))
      (Subtype.val (p := fun (x : E) ↦ x ∈ u) ⁻¹' v)))
  y
Tactic: rw [← Finsupp.mem_span_image_iff_linearCombination]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
h : ∀ (x : E), Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ x → x = 0
u : Set E
huv : v ⊆ u
hu : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ u }) (Subtype.val (p := fun (x : E) ↦ x ∈ u))
x : E
hxu : x ∈ u
hxv : x ∉ v
y : E
hy : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v) y
hxv' : Subtype.mk (p := fun (x : E) ↦ x ∈ u) x hxu ∉ Subtype.val (p := fun (x : E) ↦ x ∈ u) ⁻¹' v
⊢ ⟪y, x⟫_𝕜 = 0
have mpr : ∀ (l : Finsupp.{u_2, u_1} (↑u : Type u_2) 𝕜)
  (hl :
    Membership.mem (γ := Submodule 𝕜 (Finsupp.{u_2, u_1} (↑u : Type u_2) 𝕜))
      (supported 𝕜 𝕜 (Subtype.val (p := fun (x : E) ↦ x ∈ u) ⁻¹' v)) l)
  (hy :
    Membership.mem (α := E) (γ := Submodule 𝕜 E) (span 𝕜 v)
      ((linearCombination 𝕜 (Subtype.val (p := fun (x : E) ↦ x ∈ u)) : (a : { x : E // x ∈ u } →₀ 𝕜) → E) l : E)),
  ⟪(linearCombination 𝕜 (Subtype.val (p := fun (x : E) ↦ x ∈ u)) : (a : { x : E // x ∈ u } →₀ 𝕜) → E) l, x⟫_𝕜 = 0
Tactic: obtain ⟨l, hl, rfl⟩ :
      ∃ l ∈ supported 𝕜 𝕜 ((↑) ⁻¹' v : Set u), (linearCombination 𝕜 ((↑) : u → E)) l = y := by
      rw [← Finsupp.mem_span_image_iff_linearCombination]
      simp [huv, inter_eq_self_of_subset_right, hy]
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
inst_3 : FiniteDimensional 𝕜 E
hv : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
⊢ (∀ u ⊇ v,
      Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ u }) (Subtype.val (p := fun (x : E) ↦ x ∈ u)) →
        u = v) ↔
    ∃ (b : Basis (↑v : Type u_2) 𝕜 E),
      Eq.{u_2 + 1} (α := (a : (↑v : Type u_2)) → E) (⇑b : (a : (↑v : Type u_2)) → E)
        (Subtype.val (p := fun (x : E) ↦ x ∈ v))
have rw : Eq (α := Submodule 𝕜 E) (span 𝕜 v)ᗮ ⊥ ↔
  ∃ (b : Basis (↑v : Type u_2) 𝕜 E),
    Eq.{u_2 + 1} (α := (a : (↑v : Type u_2)) → E) (⇑b : (a : (↑v : Type u_2)) → E)
      (Subtype.val (p := fun (x : E) ↦ x ∈ v))
Tactic: rw [maximal_orthonormal_iff_orthogonalComplement_eq_bot hv]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
inst_3 : FiniteDimensional 𝕜 E
hv : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
⊢ Eq (α := Submodule 𝕜 E) (span 𝕜 v)ᗮ ⊥ ↔
    ∃ (b : Basis (↑v : Type u_2) 𝕜 E),
      Eq.{u_2 + 1} (α := (a : (↑v : Type u_2)) → E) (⇑b : (a : (↑v : Type u_2)) → E)
        (Subtype.val (p := fun (x : E) ↦ x ∈ v))
have rw : Eq (α := Submodule 𝕜 E) (span 𝕜 v) ⊤ ↔
  ∃ (b : Basis (↑v : Type u_2) 𝕜 E),
    Eq.{u_2 + 1} (α := (a : (↑v : Type u_2)) → E) (⇑b : (a : (↑v : Type u_2)) → E)
      (Subtype.val (p := fun (x : E) ↦ x ∈ v))
Tactic: rw [Submodule.orthogonal_eq_bot_iff]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
inst_3 : FiniteDimensional 𝕜 E
hv : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
⊢ Eq (α := Submodule 𝕜 E) (span 𝕜 v) ⊤ ↔
    ∃ (b : Basis (↑v : Type u_2) 𝕜 E),
      Eq.{u_2 + 1} (α := (a : (↑v : Type u_2)) → E) (⇑b : (a : (↑v : Type u_2)) → E)
        (Subtype.val (p := fun (x : E) ↦ x ∈ v))
have hv_coe : Set.range (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v)) = v
Tactic: have hv_coe : range ((↑) : v → E) = v := by simp
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
inst_3 : FiniteDimensional 𝕜 E
hv : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
hv_coe : Set.range (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v)) = v
⊢ Eq (α := Submodule 𝕜 E) (span 𝕜 v) ⊤ ↔
    ∃ (b : Basis (↑v : Type u_2) 𝕜 E),
      Eq.{u_2 + 1} (α := (a : (↑v : Type u_2)) → E) (⇑b : (a : (↑v : Type u_2)) → E)
        (Subtype.val (p := fun (x : E) ↦ x ∈ v))
have mp : Eq (α := Submodule 𝕜 E) (span 𝕜 v) ⊤ →
  ∃ (b : Basis (↑v : Type u_2) 𝕜 E),
    Eq.{u_2 + 1} (α := (a : (↑v : Type u_2)) → E) (⇑b : (a : (↑v : Type u_2)) → E)
      (Subtype.val (p := fun (x : E) ↦ x ∈ v))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
inst_3 : FiniteDimensional 𝕜 E
hv : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
hv_coe : Set.range (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v)) = v
mp :
  Eq (α := Submodule 𝕜 E) (span 𝕜 v) ⊤ →
    ∃ (b : Basis (↑v : Type u_2) 𝕜 E),
      Eq.{u_2 + 1} (α := (a : (↑v : Type u_2)) → E) (⇑b : (a : (↑v : Type u_2)) → E)
        (Subtype.val (p := fun (x : E) ↦ x ∈ v))
⊢ Eq (α := Submodule 𝕜 E) (span 𝕜 v) ⊤ ↔
    ∃ (b : Basis (↑v : Type u_2) 𝕜 E),
      Eq.{u_2 + 1} (α := (a : (↑v : Type u_2)) → E) (⇑b : (a : (↑v : Type u_2)) → E)
        (Subtype.val (p := fun (x : E) ↦ x ∈ v))
have mpr : (∃ (b : Basis (↑v : Type u_2) 𝕜 E),
    Eq.{u_2 + 1} (α := (a : (↑v : Type u_2)) → E) (⇑b : (a : (↑v : Type u_2)) → E)
      (Subtype.val (p := fun (x : E) ↦ x ∈ v))) →
  Eq (α := Submodule 𝕜 E) (span 𝕜 v) ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
inst_3 : FiniteDimensional 𝕜 E
hv : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
hv_coe : Set.range (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v)) = v
⊢ Eq (α := Submodule 𝕜 E) (span 𝕜 v) ⊤ →
    ∃ (b : Basis (↑v : Type u_2) 𝕜 E),
      Eq.{u_2 + 1} (α := (a : (↑v : Type u_2)) → E) (⇑b : (a : (↑v : Type u_2)) → E)
        (Subtype.val (p := fun (x : E) ↦ x ∈ v))
have mp : ∀ (h : Eq (α := Submodule 𝕜 E) (span 𝕜 v) ⊤),
  LE.le.{u_2} (α := Submodule 𝕜 E) ⊤
    (span 𝕜 (Set.range (ι := (↑v : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ v))))
Tactic: refine fun h => ⟨Basis.mk hv.linearIndependent _, Basis.coe_mk _ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
inst_3 : FiniteDimensional 𝕜 E
hv : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
hv_coe : Set.range (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v)) = v
h : Basis (↑v : Type u_2) 𝕜 E
coe_h :
  Eq.{u_2 + 1} (α := (a : (↑v : Type u_2)) → E) (⇑h : (a : (↑v : Type u_2)) → E)
    (Subtype.val (p := fun (x : E) ↦ x ∈ v))
⊢ Eq (α := Submodule 𝕜 E) (span 𝕜 v) ⊤
have mpr : Eq (α := Submodule 𝕜 E) (span 𝕜 v) (span 𝕜 (Set.range (ι := (↑v : Type u_2)) (⇑h : (a : (↑v : Type u_2)) → E)))
Tactic: rw [← h.span_eq, coe_h, hv_coe]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
inst_3 : FiniteDimensional 𝕜 E
hv : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
hv_coe : Set.range (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v)) = v
h : Basis (↑v : Type u_2) 𝕜 E
coe_h :
  Eq.{u_2 + 1} (α := (a : (↑v : Type u_2)) → E) (⇑h : (a : (↑v : Type u_2)) → E)
    (Subtype.val (p := fun (x : E) ↦ x ∈ v))
mpr : Eq (α := Submodule 𝕜 E) (span 𝕜 v) (span 𝕜 (Set.range (ι := (↑v : Type u_2)) (⇑h : (a : (↑v : Type u_2)) → E)))
⊢ Eq (α := Submodule 𝕜 E) (span 𝕜 v) ⊤
have mpr₁ : Eq (α := Submodule 𝕜 E) (span 𝕜 v) (span 𝕜 (Set.range (ι := (↑v : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ v))))
Tactic: rw [← h.span_eq, coe_h, hv_coe]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
inst_3 : FiniteDimensional 𝕜 E
hv : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
hv_coe : Set.range (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v)) = v
h : Basis (↑v : Type u_2) 𝕜 E
coe_h :
  Eq.{u_2 + 1} (α := (a : (↑v : Type u_2)) → E) (⇑h : (a : (↑v : Type u_2)) → E)
    (Subtype.val (p := fun (x : E) ↦ x ∈ v))
mpr : Eq (α := Submodule 𝕜 E) (span 𝕜 v) (span 𝕜 (Set.range (ι := (↑v : Type u_2)) (⇑h : (a : (↑v : Type u_2)) → E)))
mpr₁ :
  Eq (α := Submodule 𝕜 E) (span 𝕜 v)
    (span 𝕜 (Set.range (ι := (↑v : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ v))))
⊢ Eq (α := Submodule 𝕜 E) (span 𝕜 v) ⊤
have mpr₂ : Eq (α := Submodule 𝕜 E) (span 𝕜 v) (span 𝕜 v)
Tactic: rw [← h.span_eq, coe_h, hv_coe]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (hypothesis)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
ne : K.Nonempty
h₁ : IsComplete K
h₂ : Convex ℝ K
u : F
δ : ℝ := ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
this : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
⊢ ∃ v ∈ K, ‖u - v‖ = ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
have zero_le_δ : 0 ≤ δ
Tactic: have zero_le_δ : 0 ≤ δ := le_ciInf fun _ => norm_nonneg _
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (hypothesis)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
ne : K.Nonempty
h₁ : IsComplete K
h₂ : Convex ℝ K
u : F
δ : ℝ := ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
this : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
zero_le_δ : 0 ≤ δ
⊢ ∃ v ∈ K, ‖u - v‖ = ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
have δ_le : ∀ (w : (↑K : Type u_3)), δ ≤ ‖u - (↑w : F)‖
Tactic: have δ_le : ∀ w : K, δ ≤ ‖u - w‖ := ciInf_le ⟨0, Set.forall_mem_range.2 fun _ => norm_nonneg _⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (hypothesis)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
ne : K.Nonempty
h₁ : IsComplete K
h₂ : Convex ℝ K
u : F
δ : ℝ := ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
this : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
zero_le_δ : 0 ≤ δ
δ_le : ∀ (w : (↑K : Type u_3)), δ ≤ ‖u - (↑w : F)‖
⊢ ∃ v ∈ K, ‖u - v‖ = ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
have δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
Tactic: have δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖ := fun w hw => δ_le ⟨w, hw⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (hypothesis)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
ne : K.Nonempty
h₁ : IsComplete K
h₂ : Convex ℝ K
u : F
δ : ℝ := ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
this : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
zero_le_δ : 0 ≤ δ
δ_le : ∀ (w : (↑K : Type u_3)), δ ≤ ‖u - (↑w : F)‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
⊢ ∃ (w : ℕ → (↑K : Type u_3)), ∀ (n : ℕ), ‖u - (↑(w n) : F)‖ < δ + 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have hδ : ∀ (n : ℕ), δ < δ + 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: have hδ : ∀ n : ℕ, δ < δ + 1 / (n + 1) := fun n =>
      lt_add_of_le_of_pos le_rfl Nat.one_div_pos_of_nat