awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
φ : E ≃ₗᵢ[ℝ] E
hφ : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑φ.toLinearEquiv : E →ₗ[ℝ] E) : ℝ)
x : Fin n → E
zero :
  ∀ [_i : Fact (finrank ℝ E = 0)] (o : Orientation ℝ E (Fin 0)) (x : Fin 0 → E),
    Eq (α := ℝ) ((o.volumeForm : (a : Fin 0 → E) → ℝ) ((⇑φ : (a : E) → E) ∘ x) : ℝ)
      ((o.volumeForm : (a : Fin 0 → E) → ℝ) x : ℝ)
⊢ Eq (α := ℝ) ((o.volumeForm : (a : Fin n → E) → ℝ) ((⇑φ : (a : E) → E) ∘ x) : ℝ)
    ((o.volumeForm : (a : Fin n → E) → ℝ) x : ℝ)
have succ : ∀ (n : ℕ) [_i : Fact (finrank ℝ E = n + 1)] (o : Orientation ℝ E (Fin (n + 1))) (x : Fin (n + 1) → E),
  Eq (α := ℝ) ((o.volumeForm : (a : Fin (n + 1) → E) → ℝ) ((⇑φ : (a : E) → E) ∘ x) : ℝ)
    ((o.volumeForm : (a : Fin (n + 1) → E) → ℝ) x : ℝ)
Tactic: rcases n with - | n
Cleared hypotheses: n, _i, o, x
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
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) : ℝ)
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
x : Fin 0 → E
⊢ Eq (α := ℝ) ((o.volumeForm : (a : Fin 0 → E) → ℝ) ((⇑φ : (a : E) → E) ∘ x) : ℝ)
    ((o.volumeForm : (a : Fin 0 → E) → ℝ) x : ℝ)
have zero : o = positiveOrientation →
  Eq (α := ℝ) ((o.volumeForm : (a : Fin 0 → E) → ℝ) ((⇑φ : (a : E) → E) ∘ x) : ℝ)
    ((o.volumeForm : (a : Fin 0 → E) → ℝ) x : ℝ)
Tactic: refine o.eq_or_eq_neg_of_isEmpty.elim ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
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) : ℝ)
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
x : Fin 0 → E
zero :
  o = positiveOrientation →
    Eq (α := ℝ) ((o.volumeForm : (a : Fin 0 → E) → ℝ) ((⇑φ : (a : E) → E) ∘ x) : ℝ)
      ((o.volumeForm : (a : Fin 0 → E) → ℝ) x : ℝ)
⊢ Eq (α := ℝ) ((o.volumeForm : (a : Fin 0 → E) → ℝ) ((⇑φ : (a : E) → E) ∘ x) : ℝ)
    ((o.volumeForm : (a : Fin 0 → E) → ℝ) x : ℝ)
have zero₁ : o = -positiveOrientation →
  Eq (α := ℝ) ((o.volumeForm : (a : Fin 0 → E) → ℝ) ((⇑φ : (a : E) → E) ∘ x) : ℝ)
    ((o.volumeForm : (a : Fin 0 → E) → ℝ) x : ℝ)
Tactic: refine o.eq_or_eq_neg_of_isEmpty.elim ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (hypothesis)
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
⊢ Eq (α := ℝ) ((o.volumeForm : (a : Fin (n + 1) → E) → ℝ) ((⇑φ : (a : E) → E) ∘ x) : ℝ)
    ((o.volumeForm : (a : Fin (n + 1) → E) → ℝ) x : ℝ)
have this : FiniteDimensional ℝ E
Tactic: have : FiniteDimensional ℝ E := .of_fact_finrank_eq_succ n
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
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 (α := ℝ) ((o.volumeForm : (a : Fin (n + 1) → E) → ℝ) ((⇑φ : (a : E) → E) ∘ x) : ℝ)
    ((o.volumeForm : (a : Fin (n + 1) → E) → ℝ) x : ℝ)
have h : o = (map (Fin (n + 1)) φ.toLinearEquiv : (a : Orientation ℝ E (Fin (n + 1))) → Orientation ℝ E (Fin (n + 1))) o
Tactic: convert! o.volumeForm_map φ (φ ∘ x)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
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
⊢ Eq (α := ℝ) ((o.volumeForm : (a : Fin (n + 1) → E) → ℝ) ((⇑φ : (a : E) → E) ∘ x) : ℝ)
    ((o.volumeForm : (a : Fin (n + 1) → E) → ℝ) x : ℝ)
have h₁ : x = Function.comp (β := E) (⇑φ.symm : (a : E) → E) ((⇑φ : (a : E) → E) ∘ x)
Tactic: convert! o.volumeForm_map φ (φ ∘ x)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
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
⊢ o = (map (Fin (n + 1)) φ.toLinearEquiv : (a : Orientation ℝ E (Fin (n + 1))) → Orientation ℝ E (Fin (n + 1))) o
have h : (map (Fin (n + 1)) φ.toLinearEquiv : (a : Orientation ℝ E (Fin (n + 1))) → Orientation ℝ E (Fin (n + 1))) o = o
Tactic: symm
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
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
⊢ (map (Fin (n + 1)) φ.toLinearEquiv : (a : Orientation ℝ E (Fin (n + 1))) → Orientation ℝ E (Fin (n + 1))) o = o
have h : Fintype.card (Fin (n + 1)) = finrank ℝ E
Tactic: rwa [← o.map_eq_iff_det_pos φ.toLinearEquiv] at hφ
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
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
⊢ Fintype.card (Fin (n + 1)) = finrank ℝ E
have h : Fintype.card (Fin (n + 1)) = n + 1
Tactic: rw [_i.out, Fintype.card_fin]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
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
⊢ Fintype.card (Fin (n + 1)) = finrank ℝ E
have h₁ : n + 1 = n + 1
Tactic: rw [_i.out, Fintype.card_fin]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
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 = Function.comp (β := E) (⇑φ.symm : (a : E) → E) ((⇑φ : (a : E) → E) ∘ x)
have h : ∀ (x_1 : Fin (n + 1)), x x_1 = Function.comp (β := E) (⇑φ.symm : (a : E) → E) ((⇑φ : (a : E) → E) ∘ x) x_1
Tactic: ext
-- 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
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
⊢ ⟪u, a + b⟫ = 0
have rw : ⟪u, a⟫ + ⟪u, b⟫ = 0
Tactic: rw [inner_add_right, hx u hu, hy u hu, add_zero]
-- 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
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
⊢ ⟪u, a + b⟫ = 0
have rw₁ : 0 + ⟪u, b⟫ = 0
Tactic: rw [inner_add_right, hx u hu, hy u hu, add_zero]
-- 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
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
⊢ ⟪u, a + b⟫ = 0
have rw₂ : HAdd.hAdd (α := 𝕜) 0 0 = 0
Tactic: rw [inner_add_right, hx u hu, hy u hu, add_zero]
-- 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
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
⊢ ⟪u, a + b⟫ = 0
have rw₃ : Eq.{u_1 + 1} (α := 𝕜) 0 0
Tactic: rw [inner_add_right, hx u hu, hy u hu, add_zero]
-- 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
K : Submodule 𝕜 E
c : 𝕜
x : E
hx : Membership.mem (γ := Set E) {v : E | ∀ u ∈ K, ⟪u, v⟫ = 0} x
u : E
hu : u ∈ K
⊢ ⟪u, c • x⟫ = 0
have rw : c * ⟪u, x⟫ = 0
Tactic: rw [inner_smul_right, hx u hu, mul_zero]
-- 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
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
⊢ ⟪u, c • x⟫ = 0
have rw₁ : c * 0 = 0
Tactic: rw [inner_smul_right, hx u hu, mul_zero]
-- 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
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
⊢ ⟪u, c • x⟫ = 0
have rw₂ : Eq.{u_1 + 1} (α := 𝕜) 0 0
Tactic: rw [inner_smul_right, hx u hu, mul_zero]
-- 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
K : Submodule 𝕜 E
u v : E
hu : u ∈ K
hv : v ∈ Kᗮ
⊢ ⟪v, u⟫ = 0
have rw : ⟪u, v⟫ = 0
Tactic: rw [inner_eq_zero_symm]
-- 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
u v : E
⊢ Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ u)ᗮ v ↔ ⟪u, v⟫ = 0
have refine : ⟪u, v⟫ = 0 → Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ u)ᗮ v
Tactic: refine ⟨inner_right_of_mem_orthogonal (mem_span_singleton_self u), ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthogonal (hypothesis)
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
⊢ ⟪w, v⟫ = 0
have hw₁ : ∃ (a : 𝕜), a • u = w
Tactic: rw [mem_span_singleton] at hw
Cleared hypotheses: hw
-- 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
u v : E
hv : ⟪u, v⟫ = 0
w : E
hw : ∃ (a : 𝕜), a • u = w
⊢ ⟪w, v⟫ = 0
have obtain : ∀ (c : 𝕜), ⟪c • u, v⟫ = 0
Tactic: obtain ⟨c, rfl⟩ := hw
Cleared hypotheses: w, hw
-- 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
u v : E
⊢ Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ u)ᗮ v ↔ ⟪v, u⟫ = 0
have rw : ⟪u, v⟫ = 0 ↔ ⟪v, u⟫ = 0
Tactic: rw [mem_orthogonal_singleton_iff_inner_right, inner_eq_zero_symm]
-- 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
u v : E
rw : ⟪u, v⟫ = 0 ↔ ⟪v, u⟫ = 0
⊢ Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ u)ᗮ v ↔ ⟪v, u⟫ = 0
have rw₁ : ⟪v, u⟫ = 0 ↔ ⟪v, u⟫ = 0
Tactic: rw [mem_orthogonal_singleton_iff_inner_right, inner_eq_zero_symm]
-- 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
K : Submodule 𝕜 E
x y : E
h : ∀ (v : ↥K), ⟪x, (↑v : E)⟫ = ⟪y, (↑v : E)⟫
⊢ x - y ∈ Kᗮ
have rw : ∀ u ∈ K, ⟪x - y, u⟫ = 0
Tactic: rw [mem_orthogonal']
-- 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
K : Submodule 𝕜 E
x y : E
h : ∀ (v : ↥K), ⟪x, (↑v : E)⟫ = ⟪y, (↑v : E)⟫
u : E
hu : u ∈ K
⊢ ⟪x - y, u⟫ = 0
have rw : ⟪x, u⟫ = ⟪y, u⟫
Tactic: rw [inner_sub_left, sub_eq_zero]
-- 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
K : Submodule 𝕜 E
x y : E
h : ∀ (v : ↥K), ⟪(↑v : E), x⟫ = ⟪(↑v : E), y⟫
u : E
hu : u ∈ K
⊢ ⟪u, x - y⟫ = 0
have rw : ⟪u, x⟫ = ⟪u, y⟫
Tactic: rw [inner_sub_right, sub_eq_zero]
-- 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
K : Submodule 𝕜 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_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
⊢ Kᗮ =
    ⨅ (v : ↥K),
      LinearMap.ker (R₂ := 𝕜) (M₂ := 𝕜) (τ₁₂ := RingHom.id 𝕜)
        (↑((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) (↑v : E)) : E →ₗ[𝕜] 𝕜)
have 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
Tactic: ext
-- 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
K : Submodule 𝕜 E
⊢ IsClosed (↑Kᗮ : Set E)
have rw : IsClosed
  (↑(⨅ (v : ↥K),
        LinearMap.ker (R₂ := 𝕜) (M₂ := 𝕜) (τ₁₂ := RingHom.id 𝕜)
          (↑((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) (↑v : E)) : E →ₗ[𝕜] 𝕜)) :
    Set E)
Tactic: rw [orthogonal_eq_inter K]
-- 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
K : Submodule 𝕜 E
⊢ IsClosed
    (↑(⨅ (v : ↥K),
          LinearMap.ker (R₂ := 𝕜) (M₂ := 𝕜) (τ₁₂ := RingHom.id 𝕜)
            (↑((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) (↑v : E)) : E →ₗ[𝕜] 𝕜)) :
      Set E)
have 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)
Tactic: convert! isClosed_iInter <| fun v : K => ContinuousLinearMap.isClosed_ker (innerSL 𝕜 (v : E))
-- 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
K : Submodule 𝕜 E
f : E →ₗᵢ[𝕜] F
⊢ map f.toLinearMap Kᗮ = (map f.toLinearMap K)ᗮ ⊓ f.range
have 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
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]
-- 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
K : Submodule 𝕜 E
f : E ≃ₗᵢ[𝕜] F
⊢ map (↑f.toLinearEquiv : E →ₗ[𝕜] F) Kᗮ = (map (↑f.toLinearEquiv : E →ₗ[𝕜] F) K)ᗮ
have refine : (map f.toLinearIsometry.toLinearMap K)ᗮ ⊓ f.toLinearIsometry.range = (map (↑f.toLinearEquiv : E →ₗ[𝕜] F) K)ᗮ
Tactic: refine (map_orthogonal K f.toLinearIsometry).trans ?_
-- 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
K : Submodule 𝕜 E
f : E ≃ₗᵢ[𝕜] F
⊢ (map f.toLinearIsometry.toLinearMap K)ᗮ ⊓ f.toLinearIsometry.range = (map (↑f.toLinearEquiv : E →ₗ[𝕜] F) K)ᗮ
have this : f.toLinearIsometry.range = ⊤
Tactic: have : f.toLinearIsometry.range = ⊤ := f.range
-- 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
K : Submodule 𝕜 E
f : E ≃ₗᵢ[𝕜] F
this : f.toLinearIsometry.range = ⊤
⊢ (map f.toLinearIsometry.toLinearMap K)ᗮ ⊓ f.toLinearIsometry.range = (map (↑f.toLinearEquiv : E →ₗ[𝕜] F) K)ᗮ
have rw : (map f.toLinearIsometry.toLinearMap K)ᗮ = (map (↑f.toLinearEquiv : E →ₗ[𝕜] F) K)ᗮ
Tactic: rw [this, inf_top_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
⊢ Eq.{u_2 + 1} (α := Submodule 𝕜 E) ⊤ᗮ ⊥
have h : ∀ (x : E), Membership.mem (γ := Submodule 𝕜 E) ⊤ᗮ x ↔ Membership.mem (γ := Submodule 𝕜 E) ⊥ x
Tactic: ext x
-- 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
⊢ Eq.{u_2 + 1} (α := Submodule 𝕜 E) ⊥ᗮ ⊤
have rw : LE.le.{u_2} (α := Submodule 𝕜 E) ⊤ ⊤ᗮᗮ
Tactic: rw [← top_orthogonal_eq_bot, eq_top_iff]
-- 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
K : Submodule 𝕜 E
⊢ Kᗮ = ⊤ ↔ K = ⊥
have rintro : 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_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 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_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 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_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 = ⊥
⊢ 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_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 = ⊥
⊢ 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_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
x : E
⊢ (∀ y ∈ K, ⟪y, x⟫ = 0) ↔ ∀ y ∈ K.topologicalClosure, ⟪y, x⟫ = 0
have simp_rw : x ∈ Kᗮ ↔ x ∈ K.topologicalClosureᗮ
Tactic: simp_rw [← mem_orthogonal, orthogonal_closure]
-- 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
⊢ span 𝕜 s ⟂ span 𝕜 t ↔ ∀ ⦃u : E⦄, u ∈ s → ∀ ⦃v : E⦄, v ∈ t → ⟪u, v⟫ = 0
have simp_rw : ⨆ x ∈ s, 𝕜 ∙ x ⟂ 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]
-- 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
⊢ span 𝕜 s ⟂ span 𝕜 t ↔ ∀ ⦃u : E⦄, u ∈ s → ∀ ⦃v : E⦄, v ∈ t → ⟪u, v⟫ = 0
have 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
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
⊢ span 𝕜 s ⟂ span 𝕜 t ↔ ∀ ⦃u : E⦄, u ∈ s → ∀ ⦃v : E⦄, v ∈ t → ⟪u, v⟫ = 0
have 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
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]