awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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
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
⊢ ⟪(↑(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

Premises used: Set.eq_or_mem_of_mem_insert
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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 = 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:
simpa [hb] using h_end a ha
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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
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'
⊢ False

Tactic:
apply hab'
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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
⊢ 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:
simpa using hab''
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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 ∈ 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''
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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
this : Subtype.mk (p := fun (x : E) ↦ x ∈ v) a ha ≠ Subtype.mk (p := fun (x : E) ↦ x ∈ 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

Tactic:
hv.2 this

Premises used: And.right
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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
this : Subtype.mk (p := fun (x : E) ↦ x ∈ v) a ha ≠ Subtype.mk (p := fun (x : E) ↦ x ∈ 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

Tactic:
exact hv.2 this

Premises used: And.right
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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))
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
⊢ (∀ (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

Tactic:
simp only [Subset.antisymm_iff]

Premises used: Set.Subset.antisymm_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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

Tactic:
⟨?_, huv⟩

Premises used: And.intro
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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))
mpr : u ⊆ v
⊢ u ⊆ v ∧ v ⊆ u

Tactic:
refine ⟨?_, huv⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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

Tactic:
((mt (h x)) (hu.ne_zero ⟨x, hxu⟩)).imp_symm ?_

Premises used: Orthonormal.ne_zero, mt, Not.imp_symm, Subtype.mk
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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
mpr : x ∉ v → Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ x
⊢ x ∈ v

Tactic:
refine ((mt (h x)) (hu.ne_zero ⟨x, hxu⟩)).imp_symm ?_

Premises used: Orthonormal.ne_zero, mt, Not.imp_symm, Subtype.mk
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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
⊢ Subtype.mk (p := fun (x : E) ↦ x ∈ u) x hxu ∉ Subtype.val (p := fun (x : E) ↦ x ∈ u) ⁻¹' v

Tactic:
simp [hxv]
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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
⊢ 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]
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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
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
⊢ ∃ (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

Tactic:
rw [← Finsupp.mem_span_image_iff_linearCombination]

Premises used: Finsupp.mem_span_image_iff_linearCombination
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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
⊢ 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:
simp [huv, inter_eq_self_of_subset_right, hy]

Premises used: Set.inter_eq_self_of_subset_right
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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
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
⊢ ⟪y, 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]

Premises used: Finsupp.supported, Set.preimage, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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
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) 𝕜
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:
hu.inner_finsupp_eq_zero hxv' hl

Premises used: Orthonormal.inner_finsupp_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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
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) 𝕜
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:
exact hu.inner_finsupp_eq_zero hxv' hl

Premises used: Orthonormal.inner_finsupp_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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))
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))
⊢ (∀ 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))

Tactic:
rw [maximal_orthonormal_iff_orthogonalComplement_eq_bot hv]

Premises used: maximal_orthonormal_iff_orthogonalComplement_eq_bot
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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))
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))
⊢ 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]

Premises used: Submodule.orthogonal_eq_bot_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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))
⊢ Set.range (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v)) = v

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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))
⊢ 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
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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))
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) ⊤
⊢ 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
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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))

Tactic:
fun h => ⟨Basis.mk hv.linearIndependent _, Basis.coe_mk _ ?_⟩

Premises used: Orthonormal.linearIndependent, Module.Basis.mk, Module.Basis.coe_mk, Exists.intro
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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 :
  ∀ (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))))
⊢ 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:
refine fun h => ⟨Basis.mk hv.linearIndependent _, Basis.coe_mk _ ?_⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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 : Eq (α := Submodule 𝕜 E) (span 𝕜 v) ⊤
⊢ LE.le (α := Submodule 𝕜 E) ⊤ (span 𝕜 v)

Tactic:
h.ge

Premises used: Eq.ge