awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace ℝ F
K : Submodule 𝕜 E
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
V : ι → Submodule 𝕜 E
inst_7 : ∀ (i : ι), CompleteSpace.{u_2} ↥(V i)
hV : OrthogonalFamily.{u_1, u_2, u_4, u_2} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
h : iSup V = ⊤
x : E
this : (i : ι) → DecidableEq ↥(V i) := fun (i : ι) ↦ Classical.decEq ↥(V i)
⊢ ∑ x_1 : ι, (↑(((V x_1).orthogonalProjection : (a : E) → ↥(V x_1)) x) : E) = x

Tactic:
hV.sum_projection_of_mem_iSup _ ((h.ge :) Submodule.mem_top)

Premises used: Submodule.orthogonalProjectionFn, Eq.ge, Set.Mem, OrthogonalFamily.sum_projection_of_mem_iSup, Classical.choose, Submodule.mem_top
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace ℝ F
K : Submodule 𝕜 E
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
V : ι → Submodule 𝕜 E
inst_7 : ∀ (i : ι), CompleteSpace.{u_2} ↥(V i)
hV : OrthogonalFamily.{u_1, u_2, u_4, u_2} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
h : iSup V = ⊤
x : E
this : (i : ι) → DecidableEq ↥(V i) := fun (i : ι) ↦ Classical.decEq ↥(V i)
⊢ ∑ x_1 : ι, (↑(((V x_1).orthogonalProjection : (a : E) → ↥(V x_1)) x) : E) = x

Tactic:
exact hV.sum_projection_of_mem_iSup _ ((h.ge :) Submodule.mem_top)

Premises used: Eq.ge, OrthogonalFamily.sum_projection_of_mem_iSup, Submodule.mem_top
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace ℝ F
K : Submodule 𝕜 E
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
V : ι → Submodule 𝕜 E
inst_7 : ∀ (i : ι), CompleteSpace.{u_2} ↥(V i)
hV : OrthogonalFamily.{u_1, u_2, u_4, u_2} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
h : iSup V = ⊤
x : E
this : (i : ι) → DecidableEq ↥(V i) := fun (i : ι) ↦ Classical.decEq ↥(V i)
i : ι
⊢ Eq (α := E) (((AddSubmonoidClass.subtype (V i) : ↥(V i) →+ E) : (a : ↥(V i)) → E) 0 : E) (0 : E)

Tactic:
map_zero _

Premises used: map_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace ℝ F
K : Submodule 𝕜 E
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
V : ι → Submodule 𝕜 E
inst_7 : ∀ (i : ι), CompleteSpace.{u_2} ↥(V i)
hV : OrthogonalFamily.{u_1, u_2, u_4, u_2} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
h : iSup V = ⊤
x : E
this : (i : ι) → DecidableEq ↥(V i) := fun (i : ι) ↦ Classical.decEq ↥(V i)
i : ι
⊢ Eq (α := E) (((AddSubmonoidClass.subtype (V i) : ↥(V i) →+ E) : (a : ↥(V i)) → E) 0 : E) (0 : E)

Tactic:
exact map_zero _

Premises used: map_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace ℝ F
K : Submodule 𝕜 E
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
V : ι → Submodule 𝕜 E
inst_7 : ∀ (i : ι), CompleteSpace.{u_2} ↥(V i)
hV : OrthogonalFamily.{u_1, u_2, u_4, u_2} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
h : iSup V = ⊤
x : ⨁ (i : ι), ↥(V i)
simp_rw :
  ((Equiv.symm (DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦ ↥(V i))) : (a : (i : ι) → ↥(V i)) → Π₀ (i : ι), ↥(V i))
      fun (i : ι) ↦ (x : (a : ι) → ↥(V a)) i) =
    x
⊢ ((Equiv.symm (DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦ ↥(V i))) : (a : (i : ι) → ↥(V i)) → Π₀ (i : ι), ↥(V i))
      fun (i : ι) ↦
      ((V i).orthogonalProjection : (a : E) → ↥(V i)) ((DirectSum.coeAddMonoidHom V : (a : ⨁ (i : ι), ↥(V i)) → E) x)) =
    x

Tactic:
simp_rw [hV.projection_directSum_coeAddHom, DFinsupp.equivFunOnFintype_symm_coe]

Premises used: DFinsupp.equivFunOnFintype_symm_coe, OrthogonalFamily.projection_directSum_coeAddHom
-- 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))
rw :
  (∀ 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) ↔
    ∀ (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) ↔
    Eq (α := Submodule 𝕜 E) (span 𝕜 v)ᗮ ⊥

Tactic:
rw [Submodule.eq_bot_iff]

Premises used: Submodule.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
hv : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
mp :
  (∀ 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) →
    ∀ (x : E), Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ x → x = 0
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
⊢ (∀ 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) ↔
    ∀ (x : E), Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ x → x = 0

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
hv : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
mp :
  (∃ (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
⊢ (∀ 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) →
    ∀ (x : E), Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ x → x = 0

Tactic:
contrapose!
-- 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
⊢ ‖e‖ = 1

Tactic:
simp [e, norm_smul_inv_norm hx]

Premises used: norm_smul_inv_norm
-- 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
⊢ ‖e‖ = 1

Tactic:
have he : ‖e‖ = 1 := by simp [e, norm_smul_inv_norm hx]
-- 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
⊢ Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ e

Tactic:
have he' : e ∈ (span 𝕜 v)ᗮ := smul_mem' _ _ hx'
-- 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
hev : e ∈ v
⊢ Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v ⊓ (span 𝕜 v)ᗮ) e

Tactic:
have : e ∈ span 𝕜 v ⊓ (span 𝕜 v)ᗮ := ⟨subset_span hev, he'⟩
-- 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
hev : e ∈ v
this : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v ⊓ (span 𝕜 v)ᗮ) e
⊢ e = 0

Tactic:
simpa [(span 𝕜 v).inf_orthogonal_eq_bot] using this

Premises used: Submodule.span, Submodule.inf_orthogonal_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
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
hev : e ∈ v
⊢ e = 0

Tactic:
have : e = 0 := by
        have : e ∈ span 𝕜 v ⊓ (span 𝕜 v)ᗮ := ⟨subset_span hev, he'⟩
        simpa [(span 𝕜 v).inf_orthogonal_eq_bot] using this
-- 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
hev : e ∈ v
this : e = 0
⊢ e ≠ 0

Tactic:
have : e ≠ 0 := hv.ne_zero ⟨e, hev⟩
-- 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
hev : e ∈ v
this_1 : e = 0
this : e ≠ 0
⊢ False

Tactic:
contradiction
-- 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
⊢ e ∉ v

Tactic:
have he'' : e ∉ v := by
      intro hev
      have : e = 0 := by
        have : e ∈ span 𝕜 v ⊓ (span 𝕜 v)ᗮ := ⟨subset_span hev, he'⟩
        simpa [(span 𝕜 v).inf_orthogonal_eq_bot] using this
      have : e ≠ 0 := hv.ne_zero ⟨e, hev⟩
      contradiction
-- 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
⊢ ∃ 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:
⟨insert e v, v.subset_insert e, ⟨?_, ?_⟩, (ne_insert_of_notMem v he'').symm⟩

Premises used: Insert.insert, Ne.symm, And.intro, Set.ne_insert_of_notMem, Exists.intro, Set.subset_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
mp : ∀ (i : { x : E // x ∈ insert e v }), ‖(↑i : E)‖ = 1
mp₁ : Pairwise fun (i j : { x : E // x ∈ insert e v }) ↦ ⟪(↑i : E), (↑j : E)⟫_𝕜 = 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:
refine ⟨insert e v, v.subset_insert e, ⟨?_, ?_⟩, (ne_insert_of_notMem v he'').symm⟩
-- 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
a : E
ha' : a ∈ insert e v
mp : ∀ (ha : a = e), ‖(↑(Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) a ha') : E)‖ = 1
mp₁ : ∀ (ha : a ∈ v), ‖(↑(Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) a ha') : E)‖ = 1
⊢ ‖(↑(Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) a ha') : E)‖ = 1

Tactic:
rcases eq_or_mem_of_mem_insert ha' with ha | ha

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
a : E
ha' : a ∈ insert e v
ha : a = e
⊢ ‖(↑(Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) a ha') : E)‖ = 1

Tactic:
simp [ha, he]
-- 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
a : E
ha' : a ∈ insert e v
ha : a ∈ v
⊢ ‖(↑(Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) a ha') : E)‖ = 1

Tactic:
hv.1 ⟨a, ha⟩

Premises used: Subtype.mk, And.left
-- 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
a : E
ha' : a ∈ insert e v
ha : a ∈ v
⊢ ‖(↑(Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) a ha') : E)‖ = 1

Tactic:
exact hv.1 ⟨a, ha⟩

Premises used: Subtype.mk, And.left
-- 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
a : E
ha : a ∈ v
⊢ ⟪a, e⟫_𝕜 = 0

Tactic:
he' a (Submodule.subset_span ha)

Premises used: Submodule.subset_span
-- 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
a : E
ha : a ∈ v
⊢ ⟪a, e⟫_𝕜 = 0

Tactic:
exact he' a (Submodule.subset_span ha)

Premises used: Submodule.subset_span
-- 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
⊢ ∀ a ∈ v, ⟪a, e⟫_𝕜 = 0

Tactic:
have h_end : ∀ a ∈ v, ⟪a, e⟫ = 0 := by
        intro a ha
        exact he' a (Submodule.subset_span 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
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
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
⊢ ∀ ⦃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

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 = 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'
⊢ b ∈ v

Tactic:
grind
-- 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 = 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'
⊢ b ∈ v

Tactic:
have hb : b ∈ v := by grind
-- 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 = 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
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
⊢ ⟪(↑(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:
rw [inner_eq_zero_symm]

Premises used: inner_eq_zero_symm
-- 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 = 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) b hb') : E),
      (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) a ha') : E)⟫_𝕜 =
    0

Tactic:
simpa [ha] using h_end b hb