awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
φ : E ≃ₗᵢ[ℝ] E
hφ : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑φ.toLinearEquiv : E →ₗ[ℝ] E) : ℝ)
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
x : Fin (n + 1) → E
this : FiniteDimensional ℝ E
⊢ Eq (α := ℝ)
    ((volumeForm
            ((map (Fin (n + 1)) φ.toLinearEquiv : (a : Orientation ℝ E (Fin (n + 1))) → Orientation ℝ E (Fin (n + 1)))
              o) :
          (a : Fin (n + 1) → E) → ℝ)
        ((⇑φ : (a : E) → E) ∘ x) :
      ℝ)
    ((o.volumeForm : (a : Fin (n + 1) → E) → ℝ)
        (Function.comp (β := E) (⇑φ.symm : (a : E) → E) ((⇑φ : (a : E) → E) ∘ x)) :
      ℝ)

Tactic:
o.volumeForm_map φ (φ ∘ x)

Premises used: Orientation.volumeForm_map, Function.comp, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
φ : E ≃ₗᵢ[ℝ] E
hφ : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑φ.toLinearEquiv : E →ₗ[ℝ] E) : ℝ)
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
x : Fin (n + 1) → E
this : FiniteDimensional ℝ E
h : o = (map (Fin (n + 1)) φ.toLinearEquiv : (a : Orientation ℝ E (Fin (n + 1))) → Orientation ℝ E (Fin (n + 1))) o
h₁ : x = Function.comp (β := E) (⇑φ.symm : (a : E) → E) ((⇑φ : (a : E) → E) ∘ x)
⊢ Eq (α := ℝ) ((o.volumeForm : (a : Fin (n + 1) → E) → ℝ) ((⇑φ : (a : E) → E) ∘ x) : ℝ)
    ((o.volumeForm : (a : Fin (n + 1) → E) → ℝ) x : ℝ)

Tactic:
convert! o.volumeForm_map φ (φ ∘ x)

Premises used: Orientation.volumeForm_map, Function.comp, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
φ : E ≃ₗᵢ[ℝ] E
hφ : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑φ.toLinearEquiv : E →ₗ[ℝ] E) : ℝ)
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
x : Fin (n + 1) → E
this : FiniteDimensional ℝ E
h : (map (Fin (n + 1)) φ.toLinearEquiv : (a : Orientation ℝ E (Fin (n + 1))) → Orientation ℝ E (Fin (n + 1))) o = o
⊢ o = (map (Fin (n + 1)) φ.toLinearEquiv : (a : Orientation ℝ E (Fin (n + 1))) → Orientation ℝ E (Fin (n + 1))) o

Tactic:
symm
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
φ : E ≃ₗᵢ[ℝ] E
hφ : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑φ.toLinearEquiv : E →ₗ[ℝ] E) : ℝ)
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
x : Fin (n + 1) → E
this : FiniteDimensional ℝ E
h : Fintype.card (Fin (n + 1)) = finrank ℝ E
⊢ (map (Fin (n + 1)) φ.toLinearEquiv : (a : Orientation ℝ E (Fin (n + 1))) → Orientation ℝ E (Fin (n + 1))) o = o

Tactic:
rwa [← o.map_eq_iff_det_pos φ.toLinearEquiv] at hφ

Premises used: LinearIsometryEquiv.toLinearEquiv, Orientation.map_eq_iff_det_pos
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
φ : E ≃ₗᵢ[ℝ] E
hφ : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑φ.toLinearEquiv : E →ₗ[ℝ] E) : ℝ)
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
x : Fin (n + 1) → E
this : FiniteDimensional ℝ E
h : Fintype.card (Fin (n + 1)) = n + 1
h₁ h₂ : n + 1 = n + 1
⊢ Fintype.card (Fin (n + 1)) = finrank ℝ E

Tactic:
rw [_i.out, Fintype.card_fin]

Premises used: Fintype.card_fin, Fact.out
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
φ : E ≃ₗᵢ[ℝ] E
hφ : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑φ.toLinearEquiv : E →ₗ[ℝ] E) : ℝ)
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
x : Fin (n + 1) → E
this : FiniteDimensional ℝ E
h : ∀ (x_1 : Fin (n + 1)), x x_1 = Function.comp (β := E) (⇑φ.symm : (a : E) → E) ((⇑φ : (a : E) → E) ∘ x) x_1
⊢ x = Function.comp (β := E) (⇑φ.symm : (a : E) → E) ((⇑φ : (a : E) → E) ∘ x)

Tactic:
ext
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
φ : E ≃ₗᵢ[ℝ] E
hφ : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑φ.toLinearEquiv : E →ₗ[ℝ] E) : ℝ)
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
x : Fin (n + 1) → E
this : FiniteDimensional ℝ E
x_1 : Fin (n + 1)
⊢ x x_1 = Function.comp (β := E) (⇑φ.symm : (a : E) → E) ((⇑φ : (a : E) → E) ∘ x) x_1

Tactic:
simp
-- 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
K : Submodule 𝕜 E
a b : E
hx : Membership.mem (γ := Set E) {v : E | ∀ u ∈ K, ⟪u, v⟫ = 0} a
hy : Membership.mem (γ := Set E) {v : E | ∀ u ∈ K, ⟪u, v⟫ = 0} b
u : E
hu : u ∈ K
rw : ⟪u, a⟫ + ⟪u, b⟫ = 0
rw₁ : 0 + ⟪u, b⟫ = 0
rw₂ : HAdd.hAdd (α := 𝕜) 0 0 = 0
rw₃ rw₄ : Eq.{u_1 + 1} (α := 𝕜) 0 0
⊢ ⟪u, a + b⟫ = 0

Tactic:
rw [inner_add_right, hx u hu, hy u hu, add_zero]

Premises used: inner_add_right, add_zero
-- 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
K : Submodule 𝕜 E
c : 𝕜
x : E
hx : Membership.mem (γ := Set E) {v : E | ∀ u ∈ K, ⟪u, v⟫ = 0} x
u : E
hu : u ∈ K
rw : c * ⟪u, x⟫ = 0
rw₁ : c * 0 = 0
rw₂ rw₃ : Eq.{u_1 + 1} (α := 𝕜) 0 0
⊢ ⟪u, c • x⟫ = 0

Tactic:
rw [inner_smul_right, hx u hu, mul_zero]

Premises used: MulZeroClass.mul_zero, inner_smul_right
-- 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
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_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
u v : E
hu : u ∈ K
hv : v ∈ Kᗮ
⊢ ⟪u, v⟫ = 0

Tactic:
(K.mem_orthogonal v).1 hv u hu

Premises used: Submodule.mem_orthogonal, Iff.mp
-- 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
u v : E
hu : u ∈ K
hv : v ∈ Kᗮ
rw : ⟪u, v⟫ = 0
⊢ ⟪v, u⟫ = 0

Tactic:
rw [inner_eq_zero_symm]

Premises used: 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
K : Submodule 𝕜 E
u v : E
hu : u ∈ K
hv : v ∈ Kᗮ
⊢ ⟪u, v⟫ = 0

Tactic:
inner_right_of_mem_orthogonal hu hv

Premises used: Submodule.inner_right_of_mem_orthogonal
-- 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
u v : E
hu : u ∈ K
hv : v ∈ Kᗮ
⊢ ⟪u, v⟫ = 0

Tactic:
exact inner_right_of_mem_orthogonal hu hv

Premises used: Submodule.inner_right_of_mem_orthogonal
-- 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 : E
⊢ Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ u)ᗮ v ↔ ⟪u, v⟫ = 0

Tactic:
⟨inner_right_of_mem_orthogonal (mem_span_singleton_self u), ?_⟩

Premises used: Submodule.mem_span_singleton_self, Submodule.inner_right_of_mem_orthogonal, 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
u v : E
refine : ⟪u, v⟫ = 0 → Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ u)ᗮ v
⊢ Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ u)ᗮ v ↔ ⟪u, v⟫ = 0

Tactic:
refine ⟨inner_right_of_mem_orthogonal (mem_span_singleton_self u), ?_⟩
-- 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 : E
hv : ⟪u, v⟫ = 0
w : E
hw : Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ u) w
⊢ ∃ (a : 𝕜), a • u = w

Tactic:
rw [mem_span_singleton] at hw

Premises used: Submodule.mem_span_singleton
-- 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 : E
hv : ⟪u, v⟫ = 0
w : E
hw : ∃ (a : 𝕜), a • u = w
obtain : ∀ (c : 𝕜), ⟪c • u, v⟫ = 0
⊢ ⟪w, v⟫ = 0

Tactic:
obtain ⟨c, rfl⟩ := hw

Premises used: 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 : E
hv : ⟪u, v⟫ = 0
c : 𝕜
⊢ ⟪c • u, v⟫ = 0

Tactic:
simp [inner_smul_left, hv]

Premises used: inner_smul_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 : E
rw : ⟪u, v⟫ = 0 ↔ ⟪v, u⟫ = 0
rw₁ rw₂ : ⟪v, u⟫ = 0 ↔ ⟪v, u⟫ = 0
⊢ Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ u)ᗮ v ↔ ⟪v, u⟫ = 0

Tactic:
rw [mem_orthogonal_singleton_iff_inner_right, inner_eq_zero_symm]

Premises used: Submodule.mem_orthogonal_singleton_iff_inner_right, 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
K : Submodule 𝕜 E
x y : E
h : ∀ (v : ↥K), ⟪x, (↑v : E)⟫ = ⟪y, (↑v : E)⟫
rw : ∀ u ∈ K, ⟪x - y, u⟫ = 0
⊢ x - y ∈ Kᗮ

Tactic:
rw [mem_orthogonal']

Premises used: Submodule.mem_orthogonal'
-- 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 y : E
h : ∀ (v : ↥K), ⟪x, (↑v : E)⟫ = ⟪y, (↑v : E)⟫
u : E
hu : u ∈ K
rw : ⟪x, u⟫ = ⟪y, u⟫
⊢ ⟪x - y, u⟫ = 0

Tactic:
rw [inner_sub_left, sub_eq_zero]

Premises used: sub_eq_zero, inner_sub_left
-- 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 y : E
h : ∀ (v : ↥K), ⟪x, (↑v : E)⟫ = ⟪y, (↑v : E)⟫
u : E
hu : u ∈ K
⊢ ⟪x, u⟫ = ⟪y, u⟫

Tactic:
h ⟨u, hu⟩

Premises used: Subtype.mk
-- 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 y : E
h : ∀ (v : ↥K), ⟪x, (↑v : E)⟫ = ⟪y, (↑v : E)⟫
u : E
hu : u ∈ K
⊢ ⟪x, u⟫ = ⟪y, u⟫

Tactic:
exact h ⟨u, hu⟩

Premises used: Subtype.mk
-- 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 y : E
h : ∀ (v : ↥K), ⟪(↑v : E), x⟫ = ⟪(↑v : E), y⟫
u : E
hu : u ∈ K
rw : ⟪u, x⟫ = ⟪u, y⟫
⊢ ⟪u, x - y⟫ = 0

Tactic:
rw [inner_sub_right, sub_eq_zero]

Premises used: sub_eq_zero, inner_sub_right
-- 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 y : E
h : ∀ (v : ↥K), ⟪(↑v : E), x⟫ = ⟪(↑v : E), y⟫
u : E
hu : u ∈ K
⊢ ⟪u, x⟫ = ⟪u, y⟫

Tactic:
h ⟨u, hu⟩

Premises used: Subtype.mk
-- 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 y : E
h : ∀ (v : ↥K), ⟪(↑v : E), x⟫ = ⟪(↑v : E), y⟫
u : E
hu : u ∈ K
⊢ ⟪u, x⟫ = ⟪u, y⟫

Tactic:
exact h ⟨u, hu⟩

Premises used: Subtype.mk
-- 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
rw : K ⊓ Kᗮ ≤ ⊥
⊢ K ⊓ Kᗮ = ⊥

Tactic:
rw [eq_bot_iff]

Premises used: eq_bot_iff
-- 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
⊢ x ∈ K ∧ x ∈ Kᗮ → Membership.mem (γ := Submodule 𝕜 E) ⊥ x

Tactic:
fun ⟨hx, ho⟩ => inner_self_eq_zero.1 (ho x hx)

Premises used: _private.0.Submodule.inf_orthogonal_eq_bot.match_1, Membership.mem, Bot.bot, inner_self_eq_zero, Iff.mp
-- 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
⊢ x ∈ K ∧ x ∈ Kᗮ → Membership.mem (γ := Submodule 𝕜 E) ⊥ x

Tactic:
exact fun ⟨hx, ho⟩ => inner_self_eq_zero.1 (ho x hx)
-- 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
⊢ Disjoint K Kᗮ

Tactic:
simp [disjoint_iff, K.inf_orthogonal_eq_bot]

Premises used: disjoint_iff, Submodule.inf_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
K : Submodule 𝕜 E
h :
  ∀ (x : E),
    x ∈ Kᗮ ↔
      Membership.mem (γ := Submodule 𝕜 E)
        (⨅ (v : ↥K),
          LinearMap.ker (R₂ := 𝕜) (M₂ := 𝕜) (τ₁₂ := RingHom.id 𝕜)
            (↑((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) (↑v : E)) : E →ₗ[𝕜] 𝕜))
        x
⊢ Kᗮ =
    ⨅ (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_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
x : E
⊢ x ∈ Kᗮ ↔
    Membership.mem (γ := Submodule 𝕜 E)
      (⨅ (v : ↥K),
        LinearMap.ker (R₂ := 𝕜) (M₂ := 𝕜) (τ₁₂ := RingHom.id 𝕜)
          (↑((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) (↑v : E)) : E →ₗ[𝕜] 𝕜))
      x

Tactic:
simpa using mem_orthogonal _ _

Premises used: Submodule.mem_orthogonal
-- 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
rw :
  IsClosed
    (↑(⨅ (v : ↥K),
          LinearMap.ker (R₂ := 𝕜) (M₂ := 𝕜) (τ₁₂ := RingHom.id 𝕜)
            (↑((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) (↑v : E)) : E →ₗ[𝕜] 𝕜)) :
      Set E)
⊢ IsClosed (↑Kᗮ : Set E)

Tactic:
rw [orthogonal_eq_inter K]

Premises used: Submodule.orthogonal_eq_inter
-- 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
⊢ IsClosed.{u_2} (X := E)
    (⋂ (i : ↥K),
      (↑(LinearMap.ker (R₂ := 𝕜) (M₂ := 𝕜) (τ₁₂ := RingHom.id 𝕜)
            (↑((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) (↑i : E)) : E →ₗ[𝕜] 𝕜)) :
        Set E))

Tactic:
isClosed_iInter <| fun v : K => ContinuousLinearMap.isClosed_ker (innerSL 𝕜 (v : E))

Premises used: innerSL, ContinuousLinearMap.isClosed_ker, Subtype.val, DFunLike.coe, isClosed_iInter
-- 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 :
  (↑(⨅ (v : ↥K),
          LinearMap.ker (R₂ := 𝕜) (M₂ := 𝕜) (τ₁₂ := RingHom.id 𝕜)
            (↑((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) (↑v : E)) : E →ₗ[𝕜] 𝕜)) :
      Set E) =
    ⋂ (i : ↥K),
      (↑(LinearMap.ker (R₂ := 𝕜) (M₂ := 𝕜) (τ₁₂ := RingHom.id 𝕜)
            (↑((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) (↑i : E)) : E →ₗ[𝕜] 𝕜)) :
        Set E)
⊢ IsClosed
    (↑(⨅ (v : ↥K),
          LinearMap.ker (R₂ := 𝕜) (M₂ := 𝕜) (τ₁₂ := RingHom.id 𝕜)
            (↑((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) (↑v : E)) : E →ₗ[𝕜] 𝕜)) :
      Set E)

Tactic:
convert! isClosed_iInter <| fun v : K => ContinuousLinearMap.isClosed_ker (innerSL 𝕜 (v : E))

Premises used: innerSL, ContinuousLinearMap.isClosed_ker, Subtype.val, DFunLike.coe, isClosed_iInter
-- 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
⊢ (↑(⨅ (v : ↥K),
          LinearMap.ker (R₂ := 𝕜) (M₂ := 𝕜) (τ₁₂ := RingHom.id 𝕜)
            (↑((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) (↑v : E)) : E →ₗ[𝕜] 𝕜)) :
      Set E) =
    ⋂ (i : ↥K),
      (↑(LinearMap.ker (R₂ := 𝕜) (M₂ := 𝕜) (τ₁₂ := RingHom.id 𝕜)
            (↑((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) (↑i : E)) : E →ₗ[𝕜] 𝕜)) :
        Set E)

Tactic:
simp
-- 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
K : Submodule 𝕜 E
inst_5 : CompleteSpace E
⊢ CompleteSpace.{u_2} ↥Kᗮ

Tactic:
K.isClosed_orthogonal.completeSpace_coe

Premises used: IsClosed.completeSpace_coe
-- 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
K : Submodule 𝕜 E
f : E →ₗᵢ[𝕜] F
simp :
  ∀ (x : F),
    (∃ (y : E), (∀ u ∈ K, ⟪u, y⟫ = 0) ∧ (f : (a : E) → F) y = x) ↔
      (∀ a ∈ K, ⟪(f : (a : E) → F) a, x⟫ = 0) ∧ ∃ (y : E), (f : (a : E) → F) y = x
⊢ map f.toLinearMap Kᗮ = (map f.toLinearMap K)ᗮ ⊓ f.range

Tactic:
simp only [Submodule.ext_iff, mem_map, mem_orthogonal, forall_exists_index, and_imp,
    forall_apply_eq_imp_iff₂, mem_inf, mem_map, LinearMap.mem_range,
    LinearIsometry.coe_toLinearMap]

Premises used: LinearIsometry.coe_toLinearMap, Submodule.mem_map, and_imp, Submodule.ext_iff, forall_exists_index, Submodule.mem_inf, Submodule.mem_orthogonal, LinearMap.mem_range, forall_apply_eq_imp_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
K : Submodule 𝕜 E
f : E →ₗᵢ[𝕜] F
⊢ ∀ (x : F),
    (∃ (y : E), (∀ u ∈ K, ⟪u, y⟫ = 0) ∧ (f : (a : E) → F) y = x) ↔
      (∀ a ∈ K, ⟪(f : (a : E) → F) a, x⟫ = 0) ∧ ∃ (y : E), (f : (a : E) → F) y = x

Tactic:
grind [LinearIsometry.inner_map_map]

Premises used: 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
K : Submodule 𝕜 E
f : E ≃ₗᵢ[𝕜] F
⊢ map (↑f.toLinearEquiv : E →ₗ[𝕜] F) Kᗮ = (map (↑f.toLinearEquiv : E →ₗ[𝕜] F) K)ᗮ

Tactic:
(map_orthogonal K f.toLinearIsometry).trans ?_

Premises used: LinearIsometryEquiv.toLinearIsometry, Submodule.map_orthogonal, Eq.trans
-- 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
K : Submodule 𝕜 E
f : E ≃ₗᵢ[𝕜] F
refine : (map f.toLinearIsometry.toLinearMap K)ᗮ ⊓ f.toLinearIsometry.range = (map (↑f.toLinearEquiv : E →ₗ[𝕜] F) K)ᗮ
⊢ map (↑f.toLinearEquiv : E →ₗ[𝕜] F) Kᗮ = (map (↑f.toLinearEquiv : E →ₗ[𝕜] F) K)ᗮ

Tactic:
refine (map_orthogonal K f.toLinearIsometry).trans ?_

Premises used: LinearIsometryEquiv.toLinearIsometry, Submodule.map_orthogonal, Eq.trans
-- 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
K : Submodule 𝕜 E
f : E ≃ₗᵢ[𝕜] F
⊢ f.toLinearIsometry.range = ⊤

Tactic:
have : f.toLinearIsometry.range = ⊤ := f.range
-- 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
K : Submodule 𝕜 E
f : E ≃ₗᵢ[𝕜] F
this : f.toLinearIsometry.range = ⊤
rw : (map f.toLinearIsometry.toLinearMap K)ᗮ = (map (↑f.toLinearEquiv : E →ₗ[𝕜] F) K)ᗮ
⊢ (map f.toLinearIsometry.toLinearMap K)ᗮ ⊓ f.toLinearIsometry.range = (map (↑f.toLinearEquiv : E →ₗ[𝕜] F) K)ᗮ

Tactic:
rw [this, inf_top_eq]

Premises used: inf_top_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
K : Submodule 𝕜 E
f : E ≃ₗᵢ[𝕜] F
this : f.toLinearIsometry.range = ⊤
⊢ (map f.toLinearIsometry.toLinearMap K)ᗮ = (map (↑f.toLinearEquiv : E →ₗ[𝕜] F) K)ᗮ

Tactic:
rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
⊢ GaloisConnection.{u_2, u_2} (α := Submodule 𝕜 E) orthogonal orthogonal

Tactic:
fun _K₁ _K₂ =>
  ⟨fun h _v hv _u hu => inner_left_of_mem_orthogonal hv (h hu), fun h _v hv _u hu =>
    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_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
⊢ K₂ᗮ ≤ K₁ᗮ

Tactic:
(orthogonal_gc 𝕜 E).monotone_l h

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

Tactic:
orthogonal_le (orthogonal_le h)

Premises used: Submodule.orthogonal_le
-- 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
⊢ K ≤ Kᗮᗮ

Tactic:
(orthogonal_gc 𝕜 E).le_u_l _

Premises used: Submodule.orthogonal_gc, GaloisConnection.le_u_l
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
⊢ K₁ᗮ ⊓ K₂ᗮ = (K₁ ⊔ K₂)ᗮ

Tactic:
(orthogonal_gc 𝕜 E).l_sup.symm

Premises used: Submodule.orthogonal_gc, OrderDual, GaloisConnection.l_sup, Eq.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
K : ι → Submodule 𝕜 E
⊢ ⨅ (i : ι), (K i)ᗮ = (iSup K)ᗮ

Tactic:
(orthogonal_gc 𝕜 E).l_iSup.symm

Premises used: iInf, Set.Mem, Submodule.orthogonal_gc, GaloisConnection.l_iSup, OrderDual, Eq.symm
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
s : Set (Submodule 𝕜 E)
⊢ ⨅ K ∈ s, Kᗮ = (sSup s)ᗮ

Tactic:
(orthogonal_gc 𝕜 E).l_sSup.symm

Premises used: iInf, Set.Mem, GaloisConnection.l_sSup, Submodule.orthogonal_gc, OrderDual, Eq.symm
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
h : ∀ (x : E), Membership.mem (γ := Submodule 𝕜 E) ⊤ᗮ x ↔ Membership.mem (γ := Submodule 𝕜 E) ⊥ x
⊢ Eq.{u_2 + 1} (α := Submodule 𝕜 E) ⊤ᗮ ⊥

Tactic:
ext x
-- Module: Mathlib.Analysis.InnerProductSpace.Orthogonal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
⊢ ∀ (u : E), Membership.mem (γ := Submodule 𝕜 E) ⊤ u → ⟪u, 0⟫ = 0

Tactic:
simp