awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
⊢ (∀ (u : E), Membership.mem (γ := Submodule 𝕜 E) ⊤ u → ⟪u, x⟫ = 0) ↔ x = 0

Tactic:
exact
    ⟨fun h => inner_self_eq_zero.mp (h x mem_top), by
      rintro rfl
      simp⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
rw : LE.le.{u_2} (α := Submodule 𝕜 E) ⊤ ⊤ᗮᗮ
⊢ Eq.{u_2 + 1} (α := Submodule 𝕜 E) ⊥ᗮ ⊤

Tactic:
rw [← top_orthogonal_eq_bot, eq_top_iff]

Premises used: eq_top_iff, Submodule.top_orthogonal_eq_bot
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
⊢ LE.le.{u_2} (α := Submodule 𝕜 E) ⊤ ⊤ᗮᗮ

Tactic:
le_orthogonal_orthogonal ⊤

Premises used: Set.Mem, Submodule.le_orthogonal_orthogonal, Top.top
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
⊢ LE.le.{u_2} (α := Submodule 𝕜 E) ⊤ ⊤ᗮᗮ

Tactic:
exact le_orthogonal_orthogonal ⊤

Premises used: Submodule.le_orthogonal_orthogonal, Top.top
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
⊢ Eq.{u_2 + 1} (α := Submodule 𝕜 E) ⊥ᗮ ⊤

Tactic:
bot_orthogonal_eq_top

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

Tactic:
exact bot_orthogonal_eq_top

Premises used: Submodule.bot_orthogonal_eq_top
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
rintro : Kᗮ = ⊤ → K = ⊥
⊢ Kᗮ = ⊤ ↔ K = ⊥

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

Tactic:
have : K ⊓ Kᗮ = ⊥ := K.orthogonal_disjoint.eq_bot
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 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_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
x : E
hx : x ∈ Kᗮ
y : E
hy : y ∈ K.topologicalClosure
⊢ Continuous.{u_2, u_1} (Y := 𝕜) fun (a : E) ↦ ⟪a, x⟫

Tactic:
fun_prop
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
x : E
hx : x ∈ Kᗮ
y : E
hy : y ∈ K.topologicalClosure
⊢ Continuous.{u_2, u_1} (Y := 𝕜) fun (a : E) ↦ 0

Tactic:
fun_prop
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
x : E
simp_rw : x ∈ Kᗮ ↔ x ∈ K.topologicalClosureᗮ
⊢ (∀ y ∈ K, ⟪y, x⟫ = 0) ↔ ∀ y ∈ K.topologicalClosure, ⟪y, x⟫ = 0

Tactic:
simp_rw [← mem_orthogonal, orthogonal_closure]

Premises used: Submodule.orthogonal_closure, Submodule.mem_orthogonal
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
K : Submodule ℝ E
⊢ Submodule.orthogonalBilin (innerₗ E) K = Kᗮ

Tactic:
rfl

Premises used: Set.Mem, setOf, LinearMap.IsOrtho, Submodule.orthogonal, Submodule.orthogonalBilin, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U V : Submodule 𝕜 E
⊢ U ⟂ V ↔ U ≤ Vᗮ

Tactic:
Iff.rfl

Premises used: Iff.rfl, Submodule.IsOrtho
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U V : Submodule 𝕜 E
h : U ⟂ V
⊢ V ⟂ U

Tactic:
(le_orthogonal_orthogonal _).trans (orthogonal_le h)

Premises used: Submodule.le_orthogonal_orthogonal, Submodule.IsOrtho, Submodule.orthogonal_le, LE.le.trans
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U V : Submodule 𝕜 E
⊢ U ⟂ V ↔ V ⟂ U

Tactic:
⟨IsOrtho.symm, IsOrtho.symm⟩

Premises used: Submodule.IsOrtho.symm, Iff.intro
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
⊢ Symmetric.{u_2 + 1} (α := Submodule 𝕜 E) IsOrtho

Tactic:
fun _ _ =>
  IsOrtho.symm

Premises used: Symmetric, Submodule.IsOrtho.symm
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U V : Submodule 𝕜 E
h : U ⟂ V
u v : E
hu : u ∈ U
hv : v ∈ V
⊢ ⟪u, v⟫ = 0

Tactic:
h.symm hv _ hu

Premises used: Submodule.IsOrtho.symm
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U V : Submodule 𝕜 E
⊢ U ⟂ V ↔ ∀ u ∈ U, ∀ v ∈ V, ⟪u, v⟫ = 0

Tactic:
forall₄_congr fun _u _hu _v _hv => inner_eq_zero_symm

Premises used: Set.Mem, setOf, Submodule.IsOrtho, inner_eq_zero_symm, forall₄_congr
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
V : Submodule 𝕜 E
⊢ ⊥ ⟂ V

Tactic:
bot_le

Premises used: Set.Mem, Submodule.IsOrtho, bot_le
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U : Submodule 𝕜 E
⊢ U ⟂ ⊥

Tactic:
isOrtho_bot_left.symm

Premises used: Submodule.IsOrtho.symm, Submodule.isOrtho_bot_left
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U₁ U₂ V : Submodule 𝕜 E
hU : U₂ ≤ U₁
h : U₁ ⟂ V
⊢ U₂ ⟂ V

Tactic:
hU.trans h

Premises used: Submodule.IsOrtho, LE.le.trans
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U V₁ V₂ : Submodule 𝕜 E
hV : V₂ ≤ V₁
h : U ⟂ V₁
⊢ U ⟂ V₂

Tactic:
(h.symm.mono_left hV).symm

Premises used: Submodule.IsOrtho.symm, Submodule.IsOrtho.mono_left
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U₁ V₁ U₂ V₂ : Submodule 𝕜 E
hU : U₂ ≤ U₁
hV : V₂ ≤ V₁
h : U₁ ⟂ V₁
⊢ U₂ ⟂ V₂

Tactic:
(h.mono_right hV).mono_left hU

Premises used: Submodule.IsOrtho.mono_left, Submodule.IsOrtho.mono_right
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U : Submodule 𝕜 E
⊢ U ⟂ U ↔ U = ⊥

Tactic:
⟨fun h => eq_bot_iff.mpr fun x hx => inner_self_eq_zero.mp (h hx x hx), fun h =>
    h.symm ▸ isOrtho_bot_left⟩

Premises used: Iff.mpr, Eq.rec, inner_self_eq_zero, Iff.intro, Iff.mp, eq_bot_iff, Eq.symm, Submodule.isOrtho_bot_left
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U : Submodule 𝕜 E
⊢ U ⟂ Uᗮ

Tactic:
le_orthogonal_orthogonal _

Premises used: Submodule.le_orthogonal_orthogonal, Submodule.IsOrtho
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U : Submodule 𝕜 E
⊢ Uᗮ ⟂ U

Tactic:
(isOrtho_orthogonal_right U).symm

Premises used: Submodule.isOrtho_orthogonal_right, Submodule.IsOrtho.symm
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U V : Submodule 𝕜 E
h : U ⟂ V
⊢ U ≤ Vᗮ

Tactic:
h

Premises used: Submodule.IsOrtho
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U V : Submodule 𝕜 E
h : U ⟂ V
⊢ V ≤ Uᗮ

Tactic:
h.symm

Premises used: Submodule.IsOrtho.symm, Submodule.IsOrtho
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U : Submodule 𝕜 E
⊢ U ⟂ ⊤ ↔ U = ⊥

Tactic:
⟨fun h => eq_bot_iff.mpr fun _x hx => inner_self_eq_zero.mp (h hx _ mem_top), fun h =>
    h.symm ▸ isOrtho_bot_left⟩

Premises used: Iff.mpr, Eq.rec, inner_self_eq_zero, Iff.intro, Iff.mp, eq_bot_iff, Eq.symm, Submodule.mem_top, Submodule.isOrtho_bot_left
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
V : Submodule 𝕜 E
⊢ ⊤ ⟂ V ↔ V = ⊥

Tactic:
isOrtho_comm.trans isOrtho_top_right

Premises used: Submodule.isOrtho_top_right, Submodule.isOrtho_comm, Iff.trans
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U V : Submodule 𝕜 E
h : U ⟂ V
⊢ Disjoint U V

Tactic:
(Submodule.orthogonal_disjoint _).mono_right h.symm

Premises used: Submodule.orthogonal_disjoint, Submodule.IsOrtho.symm, Disjoint.mono_right
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U₁ U₂ V : Submodule 𝕜 E
⊢ U₁ ⊔ U₂ ⟂ V ↔ U₁ ⟂ V ∧ U₂ ⟂ V

Tactic:
sup_le_iff

Premises used: Submodule.IsOrtho, sup_le_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U V₁ V₂ : Submodule 𝕜 E
⊢ U ⟂ V₁ ⊔ V₂ ↔ U ⟂ V₁ ∧ U ⟂ V₂

Tactic:
isOrtho_comm.trans <| isOrtho_sup_left.trans <| isOrtho_comm.and isOrtho_comm

Premises used: Iff.and, Submodule.isOrtho_comm, Iff.trans, Submodule.isOrtho_sup_left
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U : Set (Submodule 𝕜 E)
V : Submodule 𝕜 E
⊢ sSup U ⟂ V ↔ ∀ Uᵢ ∈ U, Uᵢ ⟂ V

Tactic:
sSup_le_iff

Premises used: Set.Mem, Submodule.IsOrtho, sSup_le_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U : Submodule 𝕜 E
V : Set (Submodule 𝕜 E)
⊢ (∀ Uᵢ ∈ V, Uᵢ ⟂ U) ↔ ∀ Vᵢ ∈ V, U ⟂ Vᵢ

Tactic:
simp_rw [isOrtho_comm]

Premises used: Submodule.isOrtho_comm
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Sort u_4
U : ι → Submodule 𝕜 E
V : Submodule 𝕜 E
⊢ iSup U ⟂ V ↔ ∀ (i : ι), U i ⟂ V

Tactic:
iSup_le_iff

Premises used: Set.Mem, Submodule.IsOrtho, iSup_le_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Sort u_4
U : Submodule 𝕜 E
V : ι → Submodule 𝕜 E
⊢ (∀ (i : ι), V i ⟂ U) ↔ ∀ (i : ι), U ⟂ V i

Tactic:
simp_rw [isOrtho_comm]

Premises used: Submodule.isOrtho_comm
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
s t : Set E
simp_rw : ⨆ x ∈ s, 𝕜 ∙ x ⟂ span 𝕜 t ↔ ∀ ⦃u : E⦄, u ∈ s → ∀ ⦃v : E⦄, v ∈ t → ⟪u, v⟫ = 0
simp_rw₁ :
  IsOrtho.{u_1, u_2} (𝕜 := 𝕜) (E := E) (⨆ x ∈ s, 𝕜 ∙ x) (⨆ x ∈ t, 𝕜 ∙ x) ↔
    ∀ ⦃u : E⦄, u ∈ s → ∀ ⦃v : E⦄, v ∈ t → ⟪u, v⟫ = 0
simp_rw₂ :
  (∀ (i : E) (i_1 : i ∈ s), IsOrtho (E := E) (𝕜 ∙ i) (⨆ x ∈ t, 𝕜 ∙ x)) ↔
    ∀ ⦃u : E⦄, u ∈ s → ∀ ⦃v : E⦄, v ∈ t → ⟪u, v⟫ = 0
simp_rw₃ :
  (∀ (i : E) (i_1 : i ∈ s) (i_2 : E) (i_3 : i_2 ∈ t), IsOrtho (E := E) (𝕜 ∙ i) (𝕜 ∙ i_2)) ↔
    ∀ ⦃u : E⦄, u ∈ s → ∀ ⦃v : E⦄, v ∈ t → ⟪u, v⟫ = 0
simp_rw₄ :
  (∀ (i : E) (i_1 : i ∈ s) (i_2 : E) (i_3 : i_2 ∈ t), LE.le (α := Submodule 𝕜 E) (𝕜 ∙ i) (𝕜 ∙ i_2)ᗮ) ↔
    ∀ ⦃u : E⦄, u ∈ s → ∀ ⦃v : E⦄, v ∈ t → ⟪u, v⟫ = 0
simp_rw₅ :
  (∀ (i : E) (i_1 : i ∈ s) (i_2 : E) (i_3 : i_2 ∈ t), {i} ⊆ (↑(𝕜 ∙ i_2)ᗮ : Set E)) ↔
    ∀ ⦃u : E⦄, u ∈ s → ∀ ⦃v : E⦄, v ∈ t → ⟪u, v⟫ = 0
simp_rw₆ :
  (∀ (i : E) (i_1 : i ∈ s) (i_2 : E) (i_3 : i_2 ∈ t) (x : E),
      Membership.mem (γ := Set E) {i} x → x ∈ (↑(𝕜 ∙ i_2)ᗮ : Set E)) ↔
    ∀ ⦃u : E⦄, u ∈ s → ∀ ⦃v : E⦄, v ∈ t → ⟪u, v⟫ = 0
simp_rw₇ :
  (∀ (i : E) (i_1 : i ∈ s) (i_2 : E) (i_3 : i_2 ∈ t) (x : E),
      Membership.mem (γ := Set E) {i} x → Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ i_2)ᗮ x) ↔
    ∀ ⦃u : E⦄, u ∈ s → ∀ ⦃v : E⦄, v ∈ t → ⟪u, v⟫ = 0
simp_rw₈ :
  (∀ (i : E) (i_1 : i ∈ s) (i_2 : E) (i_3 : i_2 ∈ t) (x : E), Membership.mem (γ := Set E) {i} x → ⟪x, i_2⟫ = 0) ↔
    ∀ ⦃u : E⦄, u ∈ s → ∀ ⦃v : E⦄, v ∈ t → ⟪u, v⟫ = 0
simp_rw₉ :
  (∀ (i : E) (i_1 : i ∈ s) (i_2 : E) (i_3 : i_2 ∈ t) (x : E), x = i → ⟪x, i_2⟫ = 0) ↔
    ∀ ⦃u : E⦄, u ∈ s → ∀ ⦃v : E⦄, v ∈ t → ⟪u, v⟫ = 0
⊢ span 𝕜 s ⟂ span 𝕜 t ↔ ∀ ⦃u : E⦄, u ∈ s → ∀ ⦃v : E⦄, v ∈ t → ⟪u, v⟫ = 0

Tactic:
simp_rw [span_eq_iSup_of_singleton_spans s, span_eq_iSup_of_singleton_spans t, isOrtho_iSup_left,
    isOrtho_iSup_right, isOrtho_iff_le, span_le, Set.subset_def, SetLike.mem_coe,
    mem_orthogonal_singleton_iff_inner_left, Set.mem_singleton_iff, forall_eq]

Premises used: Set.subset_def, forall_eq, Submodule.isOrtho_iSup_left, Submodule.isOrtho_iff_le, Set.mem_singleton_iff, SetLike.mem_coe, Submodule.isOrtho_iSup_right, Submodule.mem_orthogonal_singleton_iff_inner_left, Submodule.span_le, Submodule.span_eq_iSup_of_singleton_spans
-- 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 𝕜 E
h : U ⟂ V
⊢ Submodule.map
      (↑f : [inst_5 : FunLike (E →ₗᵢ[𝕜] F) E F] → [SemilinearMapClass (E →ₗᵢ[𝕜] F) (RingHom.id 𝕜) E F] → E →ₗ[𝕜] F) U ⟂
    Submodule.map
      (↑f : [inst_5 : FunLike (E →ₗᵢ[𝕜] F) E F] → [SemilinearMapClass (E →ₗᵢ[𝕜] F) (RingHom.id 𝕜) E F] → E →ₗ[𝕜] F) V

Tactic:
aesop (add simp [isOrtho_iff_inner_eq])

Premises used: Submodule.isOrtho_iff_inner_eq
-- 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
h : U ⟂ V
rw :
  ∀ (h : ∀ u ∈ U, ∀ v ∈ V, ⟪u, v⟫ = 0) (u : E),
    Membership.mem (γ := Submodule 𝕜 E)
        (Submodule.comap
          (↑f : [inst_5 : FunLike (E →ₗᵢ[𝕜] F) E F] → [SemilinearMapClass (E →ₗᵢ[𝕜] F) (RingHom.id 𝕜) E F] → E →ₗ[𝕜] F)
          U)
        u →
      ∀ (v : E),
        Membership.mem (γ := Submodule 𝕜 E)
            (Submodule.comap
              (↑f :
                [inst_5 : FunLike (E →ₗᵢ[𝕜] F) E F] → [SemilinearMapClass (E →ₗᵢ[𝕜] F) (RingHom.id 𝕜) E F] → E →ₗ[𝕜] F)
              V)
            v →
          ⟪u, v⟫ = 0
⊢ Submodule.comap
      (↑f : [inst_5 : FunLike (E →ₗᵢ[𝕜] F) E F] → [SemilinearMapClass (E →ₗᵢ[𝕜] F) (RingHom.id 𝕜) E F] → E →ₗ[𝕜] F) U ⟂
    Submodule.comap
      (↑f : [inst_5 : FunLike (E →ₗᵢ[𝕜] F) E F] → [SemilinearMapClass (E →ₗᵢ[𝕜] F) (RingHom.id 𝕜) E F] → E →ₗ[𝕜] F) V

Tactic:
rw [isOrtho_iff_inner_eq] at *

Premises used: Submodule.isOrtho_iff_inner_eq
-- 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
h : ∀ u ∈ U, ∀ v ∈ V, ⟪u, v⟫ = 0
simp_rw :
  ∀ (u : E),
    Membership.mem (α := F) U
        (((↑f :
                [inst_5 : FunLike (E →ₗᵢ[𝕜] F) E F] →
                  [SemilinearMapClass (E →ₗᵢ[𝕜] F) (RingHom.id 𝕜) E F] → E →ₗ[𝕜] F) :
              (a : E) → F)
            u :
          F) →
      ∀ (v : E),
        Membership.mem (α := F) V
            (((↑f :
                    [inst_5 : FunLike (E →ₗᵢ[𝕜] F) E F] →
                      [SemilinearMapClass (E →ₗᵢ[𝕜] F) (RingHom.id 𝕜) E F] → E →ₗ[𝕜] F) :
                  (a : E) → F)
                v :
              F) →
          inner.{u_1, u_3} 𝕜 (E := F) ((f : (a : E) → F) u : F) ((f : (a : E) → F) v : F) = 0
⊢ ∀ (u : E),
    Membership.mem (γ := Submodule 𝕜 E)
        (Submodule.comap
          (↑f : [inst_5 : FunLike (E →ₗᵢ[𝕜] F) E F] → [SemilinearMapClass (E →ₗᵢ[𝕜] F) (RingHom.id 𝕜) E F] → E →ₗ[𝕜] F)
          U)
        u →
      ∀ (v : E),
        Membership.mem (γ := Submodule 𝕜 E)
            (Submodule.comap
              (↑f :
                [inst_5 : FunLike (E →ₗᵢ[𝕜] F) E F] → [SemilinearMapClass (E →ₗᵢ[𝕜] F) (RingHom.id 𝕜) E F] → E →ₗ[𝕜] F)
              V)
            v →
          ⟪u, v⟫ = 0

Tactic:
simp_rw [mem_comap, ← f.inner_map_map]

Premises used: Submodule.mem_comap, LinearIsometry.inner_map_map
-- 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
h : ∀ u ∈ U, ∀ v ∈ V, ⟪u, v⟫ = 0
u : E
hu :
  Membership.mem (α := F) U
    (((↑f : [inst_5 : FunLike (E →ₗᵢ[𝕜] F) E F] → [SemilinearMapClass (E →ₗᵢ[𝕜] F) (RingHom.id 𝕜) E F] → E →ₗ[𝕜] F) :
          (a : E) → F)
        u :
      F)
v : E
hv :
  Membership.mem (α := F) V
    (((↑f : [inst_5 : FunLike (E →ₗᵢ[𝕜] F) E F] → [SemilinearMapClass (E →ₗᵢ[𝕜] F) (RingHom.id 𝕜) E F] → E →ₗ[𝕜] F) :
          (a : E) → F)
        v :
      F)
⊢ inner.{u_1, u_3} 𝕜 (E := F) ((f : (a : E) → F) u : F) ((f : (a : E) → F) v : F) = 0

Tactic:
h _ hu _ hv
-- 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
h : ∀ u ∈ U, ∀ v ∈ V, ⟪u, v⟫ = 0
u : E
hu :
  Membership.mem (α := F) U
    (((↑f : [inst_5 : FunLike (E →ₗᵢ[𝕜] F) E F] → [SemilinearMapClass (E →ₗᵢ[𝕜] F) (RingHom.id 𝕜) E F] → E →ₗ[𝕜] F) :
          (a : E) → F)
        u :
      F)
v : E
hv :
  Membership.mem (α := F) V
    (((↑f : [inst_5 : FunLike (E →ₗᵢ[𝕜] F) E F] → [SemilinearMapClass (E →ₗᵢ[𝕜] F) (RingHom.id 𝕜) E F] → E →ₗ[𝕜] F) :
          (a : E) → F)
        v :
      F)
⊢ inner.{u_1, u_3} 𝕜 (E := F) ((f : (a : E) → F) u : F) ((f : (a : E) → F) v : F) = 0

Tactic:
exact h _ hu _ hv
-- 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 𝕜 E
⊢ Submodule.map (↑(↑(↑f : E ≃L[𝕜] F) : E ≃ₗ[𝕜] F) : E →ₗ[𝕜] F) U ⟂
      Submodule.map (↑(↑(↑f : E ≃L[𝕜] F) : E ≃ₗ[𝕜] F) : E →ₗ[𝕜] F) V ↔
    U ⟂ V

Tactic:
⟨fun h ↦ ?_, IsOrtho.map f.toLinearIsometry⟩

Premises used: LinearIsometryEquiv.toLinearIsometry, Submodule.IsOrtho.map, Iff.intro
-- 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 𝕜 E
refine :
  ∀
    (h :
      Submodule.map (↑(↑(↑f : E ≃L[𝕜] F) : E ≃ₗ[𝕜] F) : E →ₗ[𝕜] F) U ⟂
        Submodule.map (↑(↑(↑f : E ≃L[𝕜] F) : E ≃ₗ[𝕜] F) : E →ₗ[𝕜] F) V),
    U ⟂ V
⊢ Submodule.map (↑(↑(↑f : E ≃L[𝕜] F) : E ≃ₗ[𝕜] F) : E →ₗ[𝕜] F) U ⟂
      Submodule.map (↑(↑(↑f : E ≃L[𝕜] F) : E ≃ₗ[𝕜] F) : E →ₗ[𝕜] F) V ↔
    U ⟂ V

Tactic:
refine ⟨fun h ↦ ?_, IsOrtho.map f.toLinearIsometry⟩
-- 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 𝕜 E
h :
  Submodule.map (↑(↑(↑f : E ≃L[𝕜] F) : E ≃ₗ[𝕜] F) : E →ₗ[𝕜] F) U ⟂
    Submodule.map (↑(↑(↑f : E ≃L[𝕜] F) : E ≃ₗ[𝕜] F) : E →ₗ[𝕜] F) V
⊢ ∀ (p : Submodule 𝕜 E),
    Submodule.comap
        (↑f.toLinearIsometry :
          [inst_5 : FunLike (E →ₗᵢ[𝕜] F) E F] → [SemilinearMapClass (E →ₗᵢ[𝕜] F) (RingHom.id 𝕜) E F] → E →ₗ[𝕜] F)
        (Submodule.map (↑(↑(↑f : E ≃L[𝕜] F) : E ≃ₗ[𝕜] F) : E →ₗ[𝕜] F) p) =
      p

Tactic:
have hf : ∀ p : Submodule 𝕜 E,
      (p.map (f : E →ₗ[𝕜] F)).comap (f.toLinearIsometry : E →ₗ[𝕜] F) = p :=
    comap_map_eq_of_injective f.injective
-- 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 𝕜 E
h :
  Submodule.map (↑(↑(↑f : E ≃L[𝕜] F) : E ≃ₗ[𝕜] F) : E →ₗ[𝕜] F) U ⟂
    Submodule.map (↑(↑(↑f : E ≃L[𝕜] F) : E ≃ₗ[𝕜] F) : E →ₗ[𝕜] F) V
hf :
  ∀ (p : Submodule 𝕜 E),
    Submodule.comap
        (↑f.toLinearIsometry :
          [inst_5 : FunLike (E →ₗᵢ[𝕜] F) E F] → [SemilinearMapClass (E →ₗᵢ[𝕜] F) (RingHom.id 𝕜) E F] → E →ₗ[𝕜] F)
        (Submodule.map (↑(↑(↑f : E ≃L[𝕜] F) : E ≃ₗ[𝕜] F) : E →ₗ[𝕜] F) p) =
      p
⊢ U ⟂ V

Tactic:
simpa only [hf] using h.comap f.toLinearIsometry

Premises used: LinearIsometryEquiv.toLinearIsometry, Submodule.IsOrtho.comap
-- 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.map (↑(↑(↑f.symm : F ≃L[𝕜] E) : F ≃ₗ[𝕜] E) : F →ₗ[𝕜] E) U ⟂
      Submodule.map (↑(↑(↑f.symm : F ≃L[𝕜] E) : F ≃ₗ[𝕜] E) : F →ₗ[𝕜] E) V ↔
    U ⟂ V

Tactic:
IsOrtho.map_iff f.symm

Premises used: LinearIsometryEquiv.symm, Submodule.IsOrtho.map_iff
-- 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
h :
  Submodule.comap (↑(↑(↑f : E ≃L[𝕜] F) : E ≃ₗ[𝕜] F) : E →ₗ[𝕜] F) U =
    Submodule.map (↑(↑(↑f.symm : F ≃L[𝕜] E) : F ≃ₗ[𝕜] E) : F →ₗ[𝕜] E) U
h₁ :
  Submodule.comap (↑(↑(↑f : E ≃L[𝕜] F) : E ≃ₗ[𝕜] F) : E →ₗ[𝕜] F) V =
    Submodule.map (↑(↑(↑f.symm : F ≃L[𝕜] E) : F ≃ₗ[𝕜] E) : F →ₗ[𝕜] E) V
⊢ Submodule.comap (↑(↑(↑f : E ≃L[𝕜] F) : E ≃ₗ[𝕜] F) : E →ₗ[𝕜] F) U ⟂
      Submodule.comap (↑(↑(↑f : E ≃L[𝕜] F) : E ≃ₗ[𝕜] F) : E →ₗ[𝕜] F) V ↔
    U ⟂ V

Tactic:
convert! IsOrtho.map_iff f.symm using 2

Premises used: LinearIsometryEquiv.symm, Submodule.IsOrtho.map_iff