awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
f : E ≃ₗᵢ[𝕜] F
U V : Submodule 𝕜 F
⊢ Submodule.comap (↑(↑(↑f : E ≃L[𝕜] F) : E ≃ₗ[𝕜] F) : E →ₗ[𝕜] F) U =
    Submodule.map (↑(↑(↑f.symm : F ≃L[𝕜] E) : F ≃ₗ[𝕜] E) : F →ₗ[𝕜] E) U

Tactic:
Submodule.comap_equiv_eq_map_symm (f : E ≃ₗ[𝕜] F) _

Premises used: Submodule.comap_equiv_eq_map_symm, ContinuousLinearEquiv.toLinearEquiv, LinearIsometryEquiv.toContinuousLinearEquiv
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
f : E ≃ₗᵢ[𝕜] F
U V : Submodule 𝕜 F
⊢ Submodule.comap (↑(↑(↑f : E ≃L[𝕜] F) : E ≃ₗ[𝕜] F) : E →ₗ[𝕜] F) U =
    Submodule.map (↑(↑(↑f.symm : F ≃L[𝕜] E) : F ≃ₗ[𝕜] E) : F →ₗ[𝕜] E) U

Tactic:
exact Submodule.comap_equiv_eq_map_symm (f : E ≃ₗ[𝕜] F) _

Premises used: Submodule.comap_equiv_eq_map_symm, ContinuousLinearEquiv.toLinearEquiv, LinearIsometryEquiv.toContinuousLinearEquiv
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
f : E ≃ₗᵢ[𝕜] F
U V : Submodule 𝕜 F
⊢ Submodule.comap (↑(↑(↑f : E ≃L[𝕜] F) : E ≃ₗ[𝕜] F) : E →ₗ[𝕜] F) V =
    Submodule.map (↑(↑(↑f.symm : F ≃L[𝕜] E) : F ≃ₗ[𝕜] E) : F →ₗ[𝕜] E) V

Tactic:
Submodule.comap_equiv_eq_map_symm (f : E ≃ₗ[𝕜] F) _

Premises used: Submodule.comap_equiv_eq_map_symm, ContinuousLinearEquiv.toLinearEquiv, LinearIsometryEquiv.toContinuousLinearEquiv
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
f : E ≃ₗᵢ[𝕜] F
U V : Submodule 𝕜 F
⊢ Submodule.comap (↑(↑(↑f : E ≃L[𝕜] F) : E ≃ₗ[𝕜] F) : E →ₗ[𝕜] F) V =
    Submodule.map (↑(↑(↑f.symm : F ≃L[𝕜] E) : F ≃ₗ[𝕜] E) : F →ₗ[𝕜] E) V

Tactic:
exact Submodule.comap_equiv_eq_map_symm (f : E ≃ₗ[𝕜] F) _

Premises used: Submodule.comap_equiv_eq_map_symm, ContinuousLinearEquiv.toLinearEquiv, LinearIsometryEquiv.toContinuousLinearEquiv
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
V : ι → Submodule 𝕜 E
⊢ (OrthogonalFamily.{u_1, u_2, u_4, u_2} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ) ↔
    Pairwise ((fun (x1 x2 : Submodule 𝕜 E) ↦ x1 ⟂ x2) on V)

Tactic:
forall₃_congr fun _i _j _hij =>
    Subtype.forall.trans <|
      forall₂_congr fun _x _hx => Subtype.forall.trans <|
        forall₂_congr fun _y _hy => inner_eq_zero_symm

Premises used: forall₃_congr, OrthogonalFamily, Subtype.forall, forall₂_congr, Pairwise, Iff.trans, inner_eq_zero_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily.{u_1, u_2, u_4, u_2} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
i j : ι
hij : i ≠ j
⊢ V i ⟂ V j

Tactic:
hV.pairwise hij

Premises used: OrthogonalFamily.pairwise
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : ClosedSubmodule 𝕜 E
⊢ (↑Kᗮ : Submodule 𝕜 E) = (↑K : Submodule 𝕜 E)ᗮ

Tactic:
rfl

Premises used: Submodule.orthogonal, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : ClosedSubmodule 𝕜 E
v : E
⊢ v ∈ (↑K : Submodule 𝕜 E)ᗮ ↔ v ∈ Kᗮ

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : ClosedSubmodule 𝕜 E
v : E
⊢ v ∈ Kᗮ ↔ ∀ u ∈ K, ⟪u, v⟫ = 0

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : ClosedSubmodule 𝕜 E
v : E
⊢ v ∈ Kᗮ ↔ ∀ u ∈ K, ⟪v, u⟫ = 0

Tactic:
Submodule.mem_orthogonal' K.toSubmodule v

Premises used: Set.Mem, ClosedSubmodule.toSubmodule, Submodule.mem_orthogonal'
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : ClosedSubmodule 𝕜 E
x y : E
h : ∀ (v : ↥K), ⟪x, (↑v : E)⟫ = ⟪y, (↑v : E)⟫
⊢ x - y ∈ Kᗮ

Tactic:
Submodule.sub_mem_orthogonal_of_inner_left h

Premises used: Submodule.sub_mem_orthogonal_of_inner_left, Set.Mem
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : ClosedSubmodule 𝕜 E
x y : E
h : ∀ (v : ↥K), ⟪(↑v : E), x⟫ = ⟪(↑v : E), y⟫
⊢ x - y ∈ Kᗮ

Tactic:
Submodule.sub_mem_orthogonal_of_inner_right h

Premises used: Set.Mem, Submodule.sub_mem_orthogonal_of_inner_right
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : ClosedSubmodule 𝕜 E
rw : K ⊓ Kᗮ ≤ ⊥
⊢ K ⊓ Kᗮ = ⊥

Tactic:
rw [eq_bot_iff]

Premises used: eq_bot_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : ClosedSubmodule 𝕜 E
x : E
⊢ x ∈ K ⊓ Kᗮ → Membership.mem (γ := ClosedSubmodule 𝕜 E) ⊥ x

Tactic:
simpa using fun hx ho => inner_self_eq_zero.1 (ho x hx)

Premises used: inner_self_eq_zero, Iff.mp
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : ClosedSubmodule 𝕜 E
⊢ Disjoint K Kᗮ

Tactic:
simp [disjoint_iff, K.inf_orthogonal_eq_bot]

Premises used: disjoint_iff, ClosedSubmodule.inf_orthogonal_eq_bot
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : ClosedSubmodule 𝕜 E
h :
  ∀ (x : E),
    x ∈ (↑Kᗮ : Submodule 𝕜 E) ↔
      Membership.mem (γ := Submodule 𝕜 E)
        (⨅ (v : ↥K),
          LinearMap.ker (R₂ := 𝕜) (M₂ := 𝕜) (τ₁₂ := RingHom.id 𝕜)
            (↑((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) (↑v : E)) : E →ₗ[𝕜] 𝕜))
        x
⊢ (↑Kᗮ : Submodule 𝕜 E) =
    ⨅ (v : ↥K),
      LinearMap.ker (R₂ := 𝕜) (M₂ := 𝕜) (τ₁₂ := RingHom.id 𝕜)
        (↑((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) (↑v : E)) : E →ₗ[𝕜] 𝕜)

Tactic:
ext
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : ClosedSubmodule 𝕜 E
x : E
⊢ x ∈ (↑Kᗮ : Submodule 𝕜 E) ↔
    Membership.mem (γ := Submodule 𝕜 E)
      (⨅ (v : ↥K),
        LinearMap.ker (R₂ := 𝕜) (M₂ := 𝕜) (τ₁₂ := RingHom.id 𝕜)
          (↑((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) (↑v : E)) : E →ₗ[𝕜] 𝕜))
      x

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
⊢ GaloisConnection.{u_5, u_5} (α := ClosedSubmodule 𝕜 E) orthogonal orthogonal

Tactic:
fun _K₁ _K₂ =>
  ⟨fun h _v hv _u hu => Submodule.inner_left_of_mem_orthogonal hv (h hu), fun h _v hv _u hu =>
    Submodule.inner_left_of_mem_orthogonal hv (h hu)⟩

Premises used: Submodule.inner_left_of_mem_orthogonal, Iff.intro, GaloisConnection
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K₁ K₂ : ClosedSubmodule 𝕜 E
h : K₁ ≤ K₂
⊢ K₂ᗮ ≤ K₁ᗮ

Tactic:
(orthogonal_gc 𝕜 E).monotone_l h

Premises used: ClosedSubmodule.orthogonal_gc, GaloisConnection.monotone_l
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K₁ K₂ : ClosedSubmodule 𝕜 E
h : K₁ ≤ K₂
⊢ K₁ᗮᗮ ≤ K₂ᗮᗮ

Tactic:
orthogonal_le (orthogonal_le h)

Premises used: ClosedSubmodule.orthogonal_le
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K₁ K₂ : ClosedSubmodule 𝕜 E
⊢ K₁ᗮ ⊓ K₂ᗮ = (K₁ ⊔ K₂)ᗮ

Tactic:
(orthogonal_gc 𝕜 E).l_sup.symm

Premises used: ClosedSubmodule.orthogonal_gc, OrderDual, GaloisConnection.l_sup, Eq.symm
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_7
K : ι → ClosedSubmodule 𝕜 E
⊢ ⨅ (i : ι), (K i)ᗮ = (iSup K)ᗮ

Tactic:
(orthogonal_gc 𝕜 E).l_iSup.symm

Premises used: ClosedSubmodule.orthogonal_gc, iInf, Set.Mem, GaloisConnection.l_iSup, OrderDual, Eq.symm
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
carrier :
  ∀ (x : E),
    Membership.mem (γ := Set E)
        (AddSubsemigroup.carrier
          (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid.{u_4, u_5} (R := 𝕜) (↑⊤ᗮ : Submodule 𝕜 E))))
        x ↔
      Membership.mem (γ := Set E)
        (AddSubsemigroup.carrier
          (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid.{u_4, u_5} (R := 𝕜) (↑⊥ : Submodule 𝕜 E))))
        x
⊢ Eq.{u_5 + 1} (α := ClosedSubmodule 𝕜 E) ⊤ᗮ ⊥

Tactic:
ext x
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
⊢ Membership.mem (γ := Set E)
      (AddSubsemigroup.carrier
        (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid.{u_4, u_5} (R := 𝕜) (↑⊤ᗮ : Submodule 𝕜 E))))
      x ↔
    Membership.mem (γ := Set E)
      (AddSubsemigroup.carrier
        (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid.{u_4, u_5} (R := 𝕜) (↑⊥ : Submodule 𝕜 E))))
      x

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
carrier :
  ∀ (x : E),
    Membership.mem (γ := Set E)
        (AddSubsemigroup.carrier
          (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid.{u_4, u_5} (R := 𝕜) (↑⊥ᗮ : Submodule 𝕜 E))))
        x ↔
      Membership.mem (γ := Set E)
        (AddSubsemigroup.carrier
          (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid.{u_4, u_5} (R := 𝕜) (↑⊤ : Submodule 𝕜 E))))
        x
⊢ Eq.{u_5 + 1} (α := ClosedSubmodule 𝕜 E) ⊥ᗮ ⊤

Tactic:
ext x
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
⊢ Membership.mem (γ := Set E)
      (AddSubsemigroup.carrier
        (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid.{u_4, u_5} (R := 𝕜) (↑⊥ᗮ : Submodule 𝕜 E))))
      x ↔
    Membership.mem (γ := Set E)
      (AddSubsemigroup.carrier
        (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid.{u_4, u_5} (R := 𝕜) (↑⊤ : Submodule 𝕜 E))))
      x

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
⊢ Eq.{u_5 + 1} (α := ClosedSubmodule 𝕜 E) ⊥ᗮ ⊤

Tactic:
bot_orthogonal_eq_top

Premises used: ClosedSubmodule.bot_orthogonal_eq_top
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
⊢ Eq.{u_5 + 1} (α := ClosedSubmodule 𝕜 E) ⊥ᗮ ⊤

Tactic:
exact bot_orthogonal_eq_top

Premises used: ClosedSubmodule.bot_orthogonal_eq_top
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : ClosedSubmodule 𝕜 E
by : Kᗮ = ⊤ → K = ⊥
⊢ Kᗮ = ⊤ ↔ K = ⊥

Tactic:
refine
    ⟨?_, by rintro rfl; exact bot_orthogonal_eq_top⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : ClosedSubmodule 𝕜 E
h : Kᗮ = ⊤
⊢ K ⊓ Kᗮ = ⊥

Tactic:
have : K ⊓ Kᗮ = ⊥ := K.orthogonal_disjoint.eq_bot
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : ClosedSubmodule 𝕜 E
h : Kᗮ = ⊤
this : K ⊓ Kᗮ = ⊥
rwa : ∀ (this : K ⊓ ⊤ = ⊥), K = ⊥
rwa₁ : ∀ (this : ⊤ ⊓ K = ⊥), K = ⊥
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (this : K = ⊥), K = ⊥
⊢ K = ⊥

Tactic:
rwa [h, inf_comm, top_inf_eq] at this

Premises used: top_inf_eq, inf_comm
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
rw : (↑K.closure : Submodule 𝕜 E)ᗮ = K.topologicalClosureᗮ
⊢ (↑K.closure : Submodule 𝕜 E)ᗮ = Kᗮ

Tactic:
rw [← Submodule.orthogonal_closure K]

Premises used: Submodule.orthogonal_closure
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
⊢ (↑K.closure : Submodule 𝕜 E)ᗮ = K.topologicalClosureᗮ

Tactic:
congr
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
carrier :
  ∀ (x : E),
    x ∈ (↑K.closureᗮ : Submodule 𝕜 E).carrier ↔
      x ∈ (↑{ toSubmodule := Kᗮ, isClosed' := ⋯ : ClosedSubmodule 𝕜 E } : Submodule 𝕜 E).carrier
⊢ K.closureᗮ = { toSubmodule := Kᗮ, isClosed' := ⋯ }

Tactic:
ext x
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
x : E
⊢ x ∈ (↑K.closureᗮ : Submodule 𝕜 E).carrier ↔
    x ∈ (↑{ toSubmodule := Kᗮ, isClosed' := ⋯ : ClosedSubmodule 𝕜 E } : Submodule 𝕜 E).carrier

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
rw : K.closureᗮ = { toSubmodule := Kᗮ, isClosed' := ⋯ }
⊢ K.closureᗮ = Kᗮ.closure

Tactic:
rw [Submodule.closure_eq' K.isClosed_orthogonal]

Premises used: Submodule.closure_eq', Submodule.isClosed_orthogonal
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
⊢ K.closureᗮ = { toSubmodule := Kᗮ, isClosed' := ⋯ }

Tactic:
orthogonal_closure' K

Premises used: ClosedSubmodule.orthogonal_closure'
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
⊢ K.closureᗮ = { toSubmodule := Kᗮ, isClosed' := ⋯ }

Tactic:
exact orthogonal_closure' K

Premises used: ClosedSubmodule.orthogonal_closure'
-- 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
inst_3 : IsEmpty ι
v : ι → E
⊢ Orthonormal 𝕜 v

Tactic:
⟨IsEmpty.elim ‹_›, Subsingleton.pairwise⟩

Premises used: Orthonormal, IsEmpty.elim, And.intro, Subsingleton.pairwise
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
n : ℕ
v : E
vs : Fin n → E
simp_rw :
  ((‖Matrix.vecCons v vs 0‖ = 1 ∧ ∀ (i : Fin n), ‖Matrix.vecCons v vs i.succ‖ = 1) ∧
      (∀ (j : Fin n), ⟪Matrix.vecCons v vs 0, Matrix.vecCons v vs j.succ⟫ = 0) ∧
        Pairwise fun (i j : Fin n) ↦ ⟪Matrix.vecCons v vs i.succ, Matrix.vecCons v vs j.succ⟫ = 0) ↔
    ‖v‖ = 1 ∧
      (∀ (i : Fin n), ⟪v, vs i⟫ = 0) ∧ (∀ (i : Fin n), ‖vs i‖ = 1) ∧ Pairwise fun (i j : Fin n) ↦ ⟪vs i, vs j⟫ = 0
⊢ Orthonormal 𝕜 (Matrix.vecCons v vs) ↔ ‖v‖ = 1 ∧ (∀ (i : Fin n), ⟪v, vs i⟫ = 0) ∧ Orthonormal 𝕜 vs

Tactic:
simp_rw [Orthonormal, pairwise_fin_succ_iff_of_isSymm, Fin.forall_fin_succ]

Premises used: Orthonormal, Fin.forall_fin_succ, pairwise_fin_succ_iff_of_isSymm
-- 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 : ι → E
h : Orthonormal 𝕜 v
i : ι
⊢ ‖v i‖ = 1

Tactic:
h.1 i

Premises used: And.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 : ι → E
h : Orthonormal 𝕜 v
i : ι
this : (↑‖v i‖₊ : ℝ) = 1
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : ∀ (this : ‖v i‖₊ = 1), ‖v i‖₊ = 1
⊢ ‖v i‖₊ = 1

Tactic:
norm_cast at this
-- 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 : ι → E
h : Orthonormal 𝕜 v
i : ι
suffices : (↑‖v i‖₊ : ℝ) = 1
⊢ ‖v i‖₊ = 1

Tactic:
suffices (‖v i‖₊ : ℝ) = 1 by norm_cast at this
-- 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 : ι → E
h : Orthonormal 𝕜 v
i : ι
⊢ (↑‖v i‖₊ : ℝ) = 1

Tactic:
simp [h.norm_eq_one]

Premises used: Orthonormal.norm_eq_one
-- 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 : ι → E
h : Orthonormal 𝕜 v
i : ι
rw : ENNReal.ofReal ‖v i‖ = 1
⊢ ‖v i‖ₑ = 1

Tactic:
rw [← ofReal_norm]

Premises used: ofReal_norm
-- 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 : ι → E
h : Orthonormal 𝕜 v
i : ι
⊢ ENNReal.ofReal ‖v i‖ = 1

Tactic:
simp [h.norm_eq_one]

Premises used: Orthonormal.norm_eq_one
-- 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 : ι → E
i j : ι
h : Orthonormal 𝕜 v
hij : i ≠ j
⊢ ⟪v i, v j⟫ = 0

Tactic:
h.2 hij

Premises used: And.right
-- 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
inst_3 : DecidableEq ι
v : ι → E
mp : Orthonormal 𝕜 v → ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
mpr : (∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0) → Orthonormal 𝕜 v
⊢ Orthonormal 𝕜 v ↔ ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0

Tactic:
constructor
-- 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
inst_3 : DecidableEq ι
v : ι → E
hv : Orthonormal 𝕜 v
i j : ι
pos : ∀ (h : i = j), ⟪v i, v j⟫ = 1
neg : ∀ (h : ¬i = j), ⟪v i, v j⟫ = 0
⊢ ⟪v i, v j⟫ = if i = j then 1 else 0

Tactic:
split_ifs 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
inst_3 : DecidableEq ι
v : ι → E
hv : Orthonormal 𝕜 v
i j : ι
h : i = j
⊢ ⟪v i, v j⟫ = 1

Tactic:
simp [h, inner_self_eq_norm_sq_to_K, hv.norm_eq_one]

Premises used: Orthonormal.norm_eq_one, inner_self_eq_norm_sq_to_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_4
inst_3 : DecidableEq ι
v : ι → E
hv : Orthonormal 𝕜 v
i j : ι
h : ¬i = j
⊢ ⟪v i, v j⟫ = 0

Tactic:
hv.inner_eq_zero h

Premises used: Orthonormal.inner_eq_zero
-- 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
inst_3 : DecidableEq ι
v : ι → E
hv : Orthonormal 𝕜 v
i j : ι
h : ¬i = j
⊢ ⟪v i, v j⟫ = 0

Tactic:
exact hv.inner_eq_zero h

Premises used: Orthonormal.inner_eq_zero
-- 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
inst_3 : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
mpr : ∀ (i : ι), ‖v i‖ = 1
mpr₁ : Pairwise fun (i j : ι) ↦ ⟪v i, v j⟫ = 0
⊢ Orthonormal 𝕜 v

Tactic:
constructor
-- 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
inst_3 : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
i : ι
rw : (re : (a : 𝕜) → ℝ) (if i = i then 1 else 0) = HPow.hPow (α := ℝ) (β := ℕ) 1 2
⊢ HPow.hPow (β := ℕ) ‖v i‖ 2 = HPow.hPow (α := ℝ) (β := ℕ) 1 2

Tactic:
rw [@norm_sq_eq_re_inner 𝕜, h i i]

Premises used: InnerProductSpace.norm_sq_eq_re_inner
-- 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
inst_3 : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
i : ι
⊢ (re : (a : 𝕜) → ℝ) (if i = i then 1 else 0) = HPow.hPow (α := ℝ) (β := ℕ) 1 2

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
ι : Type u_4
inst_3 : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
i : ι
⊢ HPow.hPow (β := ℕ) ‖v i‖ 2 = HPow.hPow (α := ℝ) (β := ℕ) 1 2

Tactic:
have h' : ‖v i‖ ^ 2 = 1 ^ 2 := by
        rw [@norm_sq_eq_re_inner 𝕜, h i i]; 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_4
inst_3 : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
i : ι
h' : HPow.hPow (β := ℕ) ‖v i‖ 2 = HPow.hPow (α := ℝ) (β := ℕ) 1 2
⊢ 0 ≤ ‖v i‖

Tactic:
have h₁ : 0 ≤ ‖v i‖ := norm_nonneg _
-- 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
inst_3 : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
i : ι
h' : HPow.hPow (β := ℕ) ‖v i‖ 2 = HPow.hPow (α := ℝ) (β := ℕ) 1 2
h₁ : 0 ≤ ‖v i‖
⊢ LE.le (α := ℝ) 0 1

Tactic:
have h₂ : (0 : ℝ) ≤ 1 := zero_le_one
-- 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
inst_3 : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
i : ι
h' : HPow.hPow (β := ℕ) ‖v i‖ 2 = HPow.hPow (α := ℝ) (β := ℕ) 1 2
h₁ : 0 ≤ ‖v i‖
h₂ : LE.le (α := ℝ) 0 1
mpr mpr₁ mpr₂ mpr₃ : ∀ (h' : ‖v i‖ = 1) (h₁ : 0 ≤ ‖v i‖) (h₂ : LE.le (α := ℝ) 0 1), ‖v i‖ = 1
⊢ ‖v i‖ = 1

Tactic:
rwa [sq_eq_sq₀ h₁ h₂] at h'

Premises used: sq_eq_sq₀