awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthogonal (goal)
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
⊢ span 𝕜 s ⟂ span 𝕜 t ↔ ∀ ⦃u : E⦄, u ∈ s → ∀ ⦃v : E⦄, v ∈ t → ⟪u, v⟫ = 0
have 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
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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthogonal (goal)
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
⊢ span 𝕜 s ⟂ span 𝕜 t ↔ ∀ ⦃u : E⦄, u ∈ s → ∀ ⦃v : E⦄, v ∈ t → ⟪u, v⟫ = 0
have 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
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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthogonal (goal)
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
⊢ span 𝕜 s ⟂ span 𝕜 t ↔ ∀ ⦃u : E⦄, u ∈ s → ∀ ⦃v : E⦄, v ∈ t → ⟪u, v⟫ = 0
have 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
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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthogonal (goal)
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
⊢ span 𝕜 s ⟂ span 𝕜 t ↔ ∀ ⦃u : E⦄, u ∈ s → ∀ ⦃v : E⦄, v ∈ t → ⟪u, v⟫ = 0
have 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
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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthogonal (goal)
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
⊢ span 𝕜 s ⟂ span 𝕜 t ↔ ∀ ⦃u : E⦄, u ∈ s → ∀ ⦃v : E⦄, v ∈ t → ⟪u, v⟫ = 0
have 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
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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthogonal (goal)
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
⊢ span 𝕜 s ⟂ span 𝕜 t ↔ ∀ ⦃u : E⦄, u ∈ s → ∀ ⦃v : E⦄, v ∈ t → ⟪u, v⟫ = 0
have 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
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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthogonal (goal)
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
⊢ span 𝕜 s ⟂ span 𝕜 t ↔ ∀ ⦃u : E⦄, u ∈ s → ∀ ⦃v : E⦄, v ∈ t → ⟪u, v⟫ = 0
have 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
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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthogonal (goal)
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
⊢ 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
have 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
Tactic: rw [isOrtho_iff_inner_eq] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthogonal (goal)
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),
    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
have 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
Tactic: simp_rw [mem_comap, ← f.inner_map_map]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthogonal (goal)
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
have 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
Tactic: refine ⟨fun h ↦ ?_, IsOrtho.map f.toLinearIsometry⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthogonal (hypothesis)
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
⊢ U ⟂ V
have 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
Tactic: have hf : ∀ p : Submodule 𝕜 E,
      (p.map (f : E →ₗ[𝕜] F)).comap (f.toLinearIsometry : E →ₗ[𝕜] F) = p :=
    comap_map_eq_of_injective f.injective
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthogonal (goal)
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.comap (↑(↑(↑f : E ≃L[𝕜] F) : E ≃ₗ[𝕜] F) : E →ₗ[𝕜] F) V ↔
    U ⟂ V
have h : Submodule.comap (↑(↑(↑f : E ≃L[𝕜] F) : E ≃ₗ[𝕜] F) : E →ₗ[𝕜] F) U =
  Submodule.map (↑(↑(↑f.symm : F ≃L[𝕜] E) : F ≃ₗ[𝕜] E) : F →ₗ[𝕜] E) U
Tactic: convert! IsOrtho.map_iff f.symm using 2
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthogonal (goal)
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
⊢ Submodule.comap (↑(↑(↑f : E ≃L[𝕜] F) : E ≃ₗ[𝕜] F) : E →ₗ[𝕜] F) U ⟂
      Submodule.comap (↑(↑(↑f : E ≃L[𝕜] F) : E ≃ₗ[𝕜] F) : E →ₗ[𝕜] F) V ↔
    U ⟂ V
have h₁ : Submodule.comap (↑(↑(↑f : E ≃L[𝕜] F) : E ≃ₗ[𝕜] F) : E →ₗ[𝕜] F) V =
  Submodule.map (↑(↑(↑f.symm : F ≃L[𝕜] E) : F ≃ₗ[𝕜] E) : F →ₗ[𝕜] E) V
Tactic: convert! IsOrtho.map_iff f.symm using 2
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthogonal (goal)
Goal:
𝕜 : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : ClosedSubmodule 𝕜 E
⊢ K ⊓ Kᗮ = ⊥
have rw : K ⊓ Kᗮ ≤ ⊥
Tactic: rw [eq_bot_iff]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthogonal (goal)
Goal:
𝕜 : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : ClosedSubmodule 𝕜 E
⊢ (↑Kᗮ : Submodule 𝕜 E) =
    ⨅ (v : ↥K),
      LinearMap.ker (R₂ := 𝕜) (M₂ := 𝕜) (τ₁₂ := RingHom.id 𝕜)
        (↑((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) (↑v : E)) : E →ₗ[𝕜] 𝕜)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthogonal (goal)
Goal:
𝕜 : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
⊢ Eq.{u_5 + 1} (α := ClosedSubmodule 𝕜 E) ⊤ᗮ ⊥
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthogonal (goal)
Goal:
𝕜 : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
⊢ Eq.{u_5 + 1} (α := ClosedSubmodule 𝕜 E) ⊥ᗮ ⊤
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthogonal (goal)
Goal:
𝕜 : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : ClosedSubmodule 𝕜 E
⊢ Kᗮ = ⊤ ↔ K = ⊥
have by : Kᗮ = ⊤ → K = ⊥
Tactic: refine
    ⟨?_, by rintro rfl; exact bot_orthogonal_eq_top⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthogonal (hypothesis)
Goal:
𝕜 : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : ClosedSubmodule 𝕜 E
h : Kᗮ = ⊤
⊢ K = ⊥
have this : K ⊓ Kᗮ = ⊥
Tactic: have : K ⊓ Kᗮ = ⊥ := K.orthogonal_disjoint.eq_bot
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthogonal (goal)
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ᗮ = ⊥
⊢ K = ⊥
have rwa : ∀ (this : K ⊓ ⊤ = ⊥), K = ⊥
Tactic: rwa [h, inf_comm, top_inf_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthogonal (goal)
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 = ⊥
⊢ K = ⊥
have rwa₁ : ∀ (this : ⊤ ⊓ K = ⊥), K = ⊥
Tactic: rwa [h, inf_comm, top_inf_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthogonal (goal)
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 = ⊥
⊢ K = ⊥
have rwa₂ : ∀ (this : K = ⊥), K = ⊥
Tactic: rwa [h, inf_comm, top_inf_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthogonal (goal)
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ᗮ
have rw : (↑K.closure : Submodule 𝕜 E)ᗮ = K.topologicalClosureᗮ
Tactic: rw [← Submodule.orthogonal_closure K]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthogonal (goal)
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' := ⋯ }
have carrier : ∀ (x : E),
  x ∈ (↑K.closureᗮ : Submodule 𝕜 E).carrier ↔
    x ∈ (↑{ toSubmodule := Kᗮ, isClosed' := sorry : ClosedSubmodule 𝕜 E } : Submodule 𝕜 E).carrier
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthogonal (goal)
Goal:
𝕜 : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
⊢ K.closureᗮ = Kᗮ.closure
have rw : K.closureᗮ = { toSubmodule := Kᗮ, isClosed' := sorry }
Tactic: rw [Submodule.closure_eq' K.isClosed_orthogonal]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
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
⊢ Orthonormal 𝕜 (Matrix.vecCons v vs) ↔ ‖v‖ = 1 ∧ (∀ (i : Fin n), ⟪v, vs i⟫ = 0) ∧ Orthonormal 𝕜 vs
have 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
Tactic: simp_rw [Orthonormal, pairwise_fin_succ_iff_of_isSymm, Fin.forall_fin_succ]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
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
⊢ ((‖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
have mp : ((‖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
Tactic: tauto