awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (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
hv : v ∈ K
this : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
K' : Submodule ℝ E := restrictScalars ℝ K
H : ‖u - v‖ = ⨅ (w : ↥K), ‖u - (↑w : E)‖
A : ∀ w ∈ K, Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪u - v, w⟫_𝕜 : ℝ) (0 : ℝ)
w : E
hw : w ∈ K
⊢ ⟪u - v, w⟫_𝕜 = 0
have mp : Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪u - v, w⟫_𝕜 : ℝ) ((re : (a : 𝕜) → ℝ) 0 : ℝ)
Tactic: apply RCLike.ext
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (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
hv : v ∈ K
this : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
K' : Submodule ℝ E := restrictScalars ℝ K
H : ‖u - v‖ = ⨅ (w : ↥K), ‖u - (↑w : E)‖
A : ∀ w ∈ K, Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪u - v, w⟫_𝕜 : ℝ) (0 : ℝ)
w : E
hw : w ∈ K
mp : Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪u - v, w⟫_𝕜 : ℝ) ((re : (a : 𝕜) → ℝ) 0 : ℝ)
⊢ ⟪u - v, w⟫_𝕜 = 0
have mp₁ : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) ⟪u - v, w⟫_𝕜 : ℝ) ((im : (a : 𝕜) → ℝ) 0 : ℝ)
Tactic: apply RCLike.ext
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (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
hv : v ∈ K
this : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
K' : Submodule ℝ E := restrictScalars ℝ K
H : ‖u - v‖ = ⨅ (w : ↥K), ‖u - (↑w : E)‖
A : ∀ w ∈ K, Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪u - v, w⟫_𝕜 : ℝ) (0 : ℝ)
w : E
hw : w ∈ K
⊢ Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) ⟪u - v, w⟫_𝕜 : ℝ) ((im : (a : 𝕜) → ℝ) 0 : ℝ)
have mp : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) 0 : ℝ) ((im : (a : 𝕜) → ℝ) ⟪u - v, w⟫_𝕜 : ℝ)
Tactic: symm
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (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
hv : v ∈ K
this : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
K' : Submodule ℝ E := restrictScalars ℝ K
H : ‖u - v‖ = ⨅ (w : ↥K), ‖u - (↑w : E)‖
A : ∀ w ∈ K, Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪u - v, w⟫_𝕜 : ℝ) (0 : ℝ)
w : E
hw : w ∈ K
⊢ Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪u - v, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (-I) w⟫_𝕜 : ℝ)
    ((re : (a : 𝕜) → ℝ) (-I * ⟪u - v, w⟫_𝕜) : ℝ)
have rw : Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) (-I * ⟪u - v, w⟫_𝕜) : ℝ) ((re : (a : 𝕜) → ℝ) (-I * ⟪u - v, w⟫_𝕜) : ℝ)
Tactic: rw [inner_smul_right]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (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
hv : v ∈ K
this : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
K' : Submodule ℝ E := restrictScalars ℝ K
H : ‖u - v‖ = ⨅ (w : ↥K), ‖u - (↑w : E)‖
A : ∀ w ∈ K, Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪u - v, w⟫_𝕜 : ℝ) (0 : ℝ)
w : E
hw : w ∈ K
⊢ Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) 0 : ℝ) ((im : (a : 𝕜) → ℝ) ⟪u - v, w⟫_𝕜 : ℝ)
have im : Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪u - v, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (-I) w⟫_𝕜 : ℝ)
  ((re : (a : 𝕜) → ℝ) (-I * ⟪u - v, w⟫_𝕜) : ℝ)
Tactic: calc
        im (0 : 𝕜) = 0 := im.map_zero
        _ = re ⟪u - v, (-I : 𝕜) • w⟫ := (A _ (K.smul_mem (-I) hw)).symm
        _ = re (-I * ⟪u - v, w⟫) := by rw [inner_smul_right]
        _ = im ⟪u - v, w⟫ := by simp
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (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
hv : v ∈ K
this : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
K' : Submodule ℝ E := restrictScalars ℝ K
H : ‖u - v‖ = ⨅ (w : ↥K), ‖u - (↑w : E)‖
A : ∀ w ∈ K, Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪u - v, w⟫_𝕜 : ℝ) (0 : ℝ)
w : E
hw : w ∈ K
im :
  Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪u - v, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (-I) w⟫_𝕜 : ℝ)
    ((re : (a : 𝕜) → ℝ) (-I * ⟪u - v, w⟫_𝕜) : ℝ)
⊢ Eq (α := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) 0 : ℝ) ((RCLike.im : (a : 𝕜) → ℝ) ⟪u - v, w⟫_𝕜 : ℝ)
have im₁ : Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) (-I * ⟪u - v, w⟫_𝕜) : ℝ) ((RCLike.im : (a : 𝕜) → ℝ) ⟪u - v, w⟫_𝕜 : ℝ)
Tactic: calc
        im (0 : 𝕜) = 0 := im.map_zero
        _ = re ⟪u - v, (-I : 𝕜) • w⟫ := (A _ (K.smul_mem (-I) hw)).symm
        _ = re (-I * ⟪u - v, w⟫) := by rw [inner_smul_right]
        _ = im ⟪u - v, w⟫ := by simp
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (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
hv : v ∈ K
this : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
K' : Submodule ℝ E := restrictScalars ℝ K
H : ∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0
w : E
hw : w ∈ K'
⊢ ⟪u - v, w⟫_ℝ = 0
have rw : Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) 0 : ℝ) (0 : ℝ)
Tactic: rw [real_inner_eq_re_inner, H w hw]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
K' : Submodule ℝ E := restrictScalars ℝ K
H : ∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0
⊢ ‖u - v‖ = ⨅ (w : ↥K), ‖u - (↑w : E)‖
have this₁ : ∀ w ∈ K', ⟪u - v, w⟫_ℝ = 0
Tactic: have : ∀ w ∈ K', ⟪u - v, w⟫_ℝ = 0 := by
      intro w hw
      rw [real_inner_eq_re_inner, H w hw]
      exact zero_re
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Reflection (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst_5 : K.HasOrthogonalProjection
x : E
w : ↥K := (K.orthogonalProjection : (a : E) → ↥K) x
v : E := x - (↑w : E)
⊢ norm (E := E) ((K.reflectionLinearEquiv : (a : E) → E) x : E) = ‖x‖
have this : ⟪v, (↑w : E)⟫ = 0
Tactic: have : ⟪v, w⟫ = 0 := starProjection_inner_eq_zero x w w.2
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Reflection (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst_5 : K.HasOrthogonalProjection
x : E
w : ↥K := (K.orthogonalProjection : (a : E) → ↥K) x
v : E := x - (↑w : E)
this : ⟪v, (↑w : E)⟫ = 0
⊢ norm (E := E) ((K.reflectionLinearEquiv : (a : E) → E) x : E) = ‖x‖
have h : (K.reflectionLinearEquiv : (a : E) → E) x = (↑w : E) - v
Tactic: convert! norm_sub_eq_norm_add this using 2
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Reflection (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst_5 : K.HasOrthogonalProjection
x : E
w : ↥K := (K.orthogonalProjection : (a : E) → ↥K) x
v : E := x - (↑w : E)
this : ⟪v, (↑w : E)⟫ = 0
h : (K.reflectionLinearEquiv : (a : E) → E) x = (↑w : E) - v
⊢ norm (E := E) ((K.reflectionLinearEquiv : (a : E) → E) x : E) = ‖x‖
have h₁ : x = (↑w : E) + v
Tactic: convert! norm_sub_eq_norm_add this using 2
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Reflection (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst_5 : K.HasOrthogonalProjection
x : E
w : ↥K := (K.orthogonalProjection : (a : E) → ↥K) x
v : E := x - (↑w : E)
this : ⟪v, (↑w : E)⟫ = 0
⊢ (K.reflectionLinearEquiv : (a : E) → E) x = (↑w : E) - v
have h : HSMul.hSMul (α := ℕ) (β := E) 2 ((K.starProjection : (a : E) → E) x : E) - x =
  HSub.hSub (α := E) ((K.starProjection : (a : E) → E) x : E)
    (HSub.hSub (β := E) x ((K.starProjection : (a : E) → E) x : E))
Tactic: dsimp [reflectionLinearEquiv, v, w]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Reflection (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
v : E
⊢ Eq (α := E) ((Kᗮ.reflection : (a : E) → E) v : E) (-(K.reflection : (a : E) → E) v : E)
have simp : HSMul.hSMul (α := ℕ) 2 (HSub.hSub (β := E) v ((K.starProjection : (a : E) → E) v : E)) - v =
  v - HSMul.hSMul (α := ℕ) (β := E) 2 ((K.starProjection : (a : E) → E) v : E)
Tactic: simp [reflection_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Reflection (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
⊢ Kᗮ.reflection = K.reflection.trans (LinearIsometryEquiv.neg 𝕜)
have h : ∀ (x : E),
  Eq (α := E) ((Kᗮ.reflection : (a : E) → E) x : E)
    ((K.reflection.trans (LinearIsometryEquiv.neg 𝕜) : (a : E) → E) x : E)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Reflection (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
u v : E
⊢ (reflection (𝕜 ∙ u) : (a : E) → E) v =
    HSMul.hSMul (α := ℕ) 2 ((⟪u, v⟫ / HPow.hPow (α := 𝕜) (β := ℕ) (↑‖u‖ : 𝕜) 2) • u) - v
have rw : HSMul.hSMul (α := ℕ) (β := E) 2 ((starProjection (𝕜 ∙ u) : (a : E) → E) v : E) - v =
  HSMul.hSMul (α := ℕ) 2 ((⟪u, v⟫ / HPow.hPow (α := 𝕜) (β := ℕ) (↑‖u‖ : 𝕜) 2) • u) - v
Tactic: rw [reflection_apply, starProjection_singleton, ofReal_pow]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Reflection (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
u v : E
rw :
  HSMul.hSMul (α := ℕ) (β := E) 2 ((starProjection (𝕜 ∙ u) : (a : E) → E) v : E) - v =
    HSMul.hSMul (α := ℕ) 2 ((⟪u, v⟫ / HPow.hPow (α := 𝕜) (β := ℕ) (↑‖u‖ : 𝕜) 2) • u) - v
⊢ (reflection (𝕜 ∙ u) : (a : E) → E) v =
    HSMul.hSMul (α := ℕ) 2 ((⟪u, v⟫ / HPow.hPow (α := 𝕜) (β := ℕ) (↑‖u‖ : 𝕜) 2) • u) - v
have rw₁ : HSMul.hSMul (α := ℕ) 2 ((⟪u, v⟫ / (↑(HPow.hPow (β := ℕ) ‖u‖ 2) : 𝕜)) • u) - v =
  HSMul.hSMul (α := ℕ) 2 ((⟪u, v⟫ / HPow.hPow (α := 𝕜) (β := ℕ) (↑‖u‖ : 𝕜) 2) • u) - v
Tactic: rw [reflection_apply, starProjection_singleton, ofReal_pow]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Reflection (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
u v : E
rw :
  HSMul.hSMul (α := ℕ) (β := E) 2 ((starProjection (𝕜 ∙ u) : (a : E) → E) v : E) - v =
    HSMul.hSMul (α := ℕ) 2 ((⟪u, v⟫ / HPow.hPow (α := 𝕜) (β := ℕ) (↑‖u‖ : 𝕜) 2) • u) - v
rw₁ :
  HSMul.hSMul (α := ℕ) 2 ((⟪u, v⟫ / (↑(HPow.hPow (β := ℕ) ‖u‖ 2) : 𝕜)) • u) - v =
    HSMul.hSMul (α := ℕ) 2 ((⟪u, v⟫ / HPow.hPow (α := 𝕜) (β := ℕ) (↑‖u‖ : 𝕜) 2) • u) - v
⊢ (reflection (𝕜 ∙ u) : (a : E) → E) v =
    HSMul.hSMul (α := ℕ) 2 ((⟪u, v⟫ / HPow.hPow (α := 𝕜) (β := ℕ) (↑‖u‖ : 𝕜) 2) • u) - v
have rw₂ : HSMul.hSMul (α := ℕ) 2 ((⟪u, v⟫ / HPow.hPow (α := 𝕜) (β := ℕ) (↑‖u‖ : 𝕜) 2) • u) - v =
  HSMul.hSMul (α := ℕ) 2 ((⟪u, v⟫ / HPow.hPow (α := 𝕜) (β := ℕ) (↑‖u‖ : 𝕜) 2) • u) - v
Tactic: rw [reflection_apply, starProjection_singleton, ofReal_pow]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Reflection (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
x : E
⊢ (K.reflection : (a : E) → E) x = x ↔ x ∈ K
have rw : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) 2 ((K.starProjection : (a : E) → E) x : E) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2 x ↔
  (K.starProjection : (a : E) → E) x = x
Tactic: rw [← starProjection_eq_self_iff, reflection_apply, sub_eq_iff_eq_add', ← two_smul 𝕜,
    two_smul ℕ, ← two_smul 𝕜]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Reflection (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
x : E
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) 2 ((K.starProjection : (a : E) → E) x : E) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2 x ↔
    (K.starProjection : (a : E) → E) x = x
have refine : Ne.{u_1 + 1} (α := 𝕜) 2 0
Tactic: refine (smul_right_injective E ?_).eq_iff
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Reflection (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
⊢ Eq.{u_2 + 1} (α := E ≃ₗᵢ[𝕜] E) (reflection ⊥) (LinearIsometryEquiv.neg 𝕜)
have h : ∀ (x : E), Eq (α := E) ((reflection ⊥ : (a : E) → E) x : E) ((LinearIsometryEquiv.neg 𝕜 : (a : E) → E) x : E)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Reflection (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (ℝ ∙ (v - w))ᗮ
this : HAdd.hAdd (α := F) (β := F) ((R : (a : F) → F) v : F) ((R : (a : F) → F) v : F) = w + w
⊢ (R : (a : F) → F) v = w
have a : Eq.{u_3 + 1} (α := F) ((fun (x : F) ↦ HSMul.hSMul (α := ℝ) 2 x) ((R : (a : F) → F) v))
  ((fun (x : F) ↦ HSMul.hSMul (α := ℝ) 2 x) w)
Tactic: apply smul_right_injective F (by simp : (2 : ℝ) ≠ 0)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Reflection (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (ℝ ∙ (v - w))ᗮ
⊢ (R : (a : F) → F) v = w
have suffices : HAdd.hAdd (α := F) (β := F) ((R : (a : F) → F) v : F) ((R : (a : F) → F) v : F) = w + w
Tactic: suffices R v + R v = w + w by
    apply smul_right_injective F (by simp : (2 : ℝ) ≠ 0)
    simpa [two_smul] using this
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Reflection (hypothesis)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (ℝ ∙ (v - w))ᗮ
⊢ HAdd.hAdd (α := F) (β := F) ((R : (a : F) → F) v : F) ((R : (a : F) → F) v : F) = w + w
have h₁ : (R : (a : F) → F) (v - w) = -(v - w)
Tactic: have h₁ : R (v - w) = -(v - w) := reflection_orthogonalComplement_singleton_eq_neg (v - w)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Reflection (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (ℝ ∙ (v - w))ᗮ
h₁ : (R : (a : F) → F) (v - w) = -(v - w)
⊢ (R : (a : F) → F) (v + w) = v + w
have hx : Membership.mem (γ := Submodule ℝ F) (ℝ ∙ (v - w))ᗮ (v + w)
Tactic: apply reflection_mem_subspace_eq_self
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Reflection (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (ℝ ∙ (v - w))ᗮ
h₁ : (R : (a : F) → F) (v - w) = -(v - w)
⊢ Membership.mem (γ := Submodule ℝ F) (ℝ ∙ (v - w))ᗮ (v + w)
have hx : inner ℝ (v + w) (v - w) = 0
Tactic: rw [Submodule.mem_orthogonal_singleton_iff_inner_left]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Reflection (hypothesis)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (ℝ ∙ (v - w))ᗮ
h₁ : (R : (a : F) → F) (v - w) = -(v - w)
⊢ HAdd.hAdd (α := F) (β := F) ((R : (a : F) → F) v : F) ((R : (a : F) → F) v : F) = w + w
have h₂ : (R : (a : F) → F) (v + w) = v + w
Tactic: have h₂ : R (v + w) = v + w := by
    apply reflection_mem_subspace_eq_self
    rw [Submodule.mem_orthogonal_singleton_iff_inner_left]
    rw [real_inner_add_sub_eq_zero_iff]
    exact h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Reflection (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (ℝ ∙ (v - w))ᗮ
h₁ : (R : (a : F) → F) (v - w) = -(v - w)
h₂ : (R : (a : F) → F) (v + w) = v + w
⊢ HAdd.hAdd (α := F) (β := F) ((R : (a : F) → F) v : F) ((R : (a : F) → F) v : F) = w + w
have h₃ : HAdd.hAdd (α := F) (β := F) ((R : (a : F) → F) v : F) ((R : (a : F) → F) v : F) =
  HAdd.hAdd (α := F) (β := F) ((R : (a : F) → F) (v + w) : F) ((R : (a : F) → F) (v - w) : F)
Tactic: convert! congr_arg₂ (· + ·) h₂ h₁ using 1
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Reflection (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (ℝ ∙ (v - w))ᗮ
h₁ : (R : (a : F) → F) (v - w) = -(v - w)
h₂ : (R : (a : F) → F) (v + w) = v + w
h₃ :
  HAdd.hAdd (α := F) (β := F) ((R : (a : F) → F) v : F) ((R : (a : F) → F) v : F) =
    HAdd.hAdd (α := F) (β := F) ((R : (a : F) → F) (v + w) : F) ((R : (a : F) → F) (v - w) : F)
⊢ HAdd.hAdd (α := F) (β := F) ((R : (a : F) → F) v : F) ((R : (a : F) → F) v : F) = w + w
have h₄ : w + w = v + w + -(v - w)
Tactic: convert! congr_arg₂ (· + ·) h₂ h₁ using 1
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
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₂
inst_3 : K₁.HasOrthogonalProjection
⊢ K₁ ⊔ K₁ᗮ ⊓ K₂ = K₂
have h₁ : ∀ (x : E), x ∈ K₁ ⊔ K₁ᗮ ⊓ K₂ ↔ x ∈ K₂
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
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₂
inst_3 : K₁.HasOrthogonalProjection
x : E
⊢ x ∈ K₁ ⊔ K₁ᗮ ⊓ K₂ ↔ x ∈ K₂
have h₁ : (∃ y ∈ K₁, ∃ z ∈ K₁ᗮ ⊓ K₂, y + z = x) ↔ x ∈ K₂
Tactic: rw [Submodule.mem_sup]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (hypothesis)
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₂
inst_3 : K₁.HasOrthogonalProjection
x : E
v : ↥K₁ := (K₁.orthogonalProjection : (a : E) → ↥K₁) x
⊢ (∃ y ∈ K₁, ∃ z ∈ K₁ᗮ ⊓ K₂, y + z = x) ↔ x ∈ K₂
have hvm : x - (↑v : E) ∈ K₁ᗮ
Tactic: have hvm : x - v ∈ K₁ᗮ := sub_starProjection_mem_orthogonal x
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
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₂
inst_3 : K₁.HasOrthogonalProjection
x : E
v : ↥K₁ := (K₁.orthogonalProjection : (a : E) → ↥K₁) x
hvm : x - (↑v : E) ∈ K₁ᗮ
⊢ (∃ y ∈ K₁, ∃ z ∈ K₁ᗮ ⊓ K₂, y + z = x) ↔ x ∈ K₂
have h₁ : (∃ y ∈ K₁, ∃ z ∈ K₁ᗮ ⊓ K₂, y + z = x) → x ∈ K₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
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₂
inst_3 : K₁.HasOrthogonalProjection
x : E
v : ↥K₁ := (K₁.orthogonalProjection : (a : E) → ↥K₁) x
hvm : x - (↑v : E) ∈ K₁ᗮ
h₁ : (∃ y ∈ K₁, ∃ z ∈ K₁ᗮ ⊓ K₂, y + z = x) → x ∈ K₂
⊢ (∃ y ∈ K₁, ∃ z ∈ K₁ᗮ ⊓ K₂, y + z = x) ↔ x ∈ K₂
have h₂ : x ∈ K₂ → ∃ y ∈ K₁, ∃ z ∈ K₁ᗮ ⊓ K₂, y + z = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
⊢ K ⊔ Kᗮ = ⊤
have h : Kᗮ = Kᗮ ⊓ ⊤
Tactic: convert! Submodule.sup_orthogonal_inf_of_hasOrthogonalProjection (le_top : K ≤ ⊤) using 2
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
⊢ Kᗮᗮ = K
have h : ∀ (v : E), v ∈ Kᗮᗮ ↔ v ∈ K
Tactic: ext v
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
v : E
⊢ v ∈ Kᗮᗮ ↔ v ∈ K
have h : v ∈ Kᗮᗮ → v ∈ K
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
v : E
h : v ∈ Kᗮᗮ → v ∈ K
⊢ v ∈ Kᗮᗮ ↔ v ∈ K
have h₁ : v ∈ K → v ∈ Kᗮᗮ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
v : E
⊢ v ∈ Kᗮᗮ → v ∈ K
have h : ∀ (y : E) (hy : y ∈ K) (z : E) (hz : z ∈ Kᗮ), y + z ∈ Kᗮᗮ → y + z ∈ K
Tactic: obtain ⟨y, hy, z, hz, rfl⟩ := K.exists_add_mem_mem_orthogonal v
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
y : E
hy : y ∈ K
z : E
hz : z ∈ Kᗮ
hv : y + z ∈ Kᗮᗮ
⊢ z = 0
have hyz : ⟪z, y⟫ = 0
Tactic: have hyz : ⟪z, y⟫ = 0 := by simp [hz y hy, inner_eq_zero_symm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
y : E
hy : y ∈ K
z : E
hz : z ∈ Kᗮ
hv : y + z ∈ Kᗮᗮ
⊢ y + z ∈ K
have hz' : z = 0
Tactic: have hz' : z = 0 := by
      have hyz : ⟪z, y⟫ = 0 := by simp [hz y hy, inner_eq_zero_symm]
      simpa [inner_add_right, hyz] using hv z hz
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
v : E
hv : v ∈ K
w : E
hw : w ∈ Kᗮ
⊢ ⟪w, v⟫ = 0
have h : ⟪v, w⟫ = 0
Tactic: rw [inner_eq_zero_symm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K₀ K₁ : Submodule 𝕜 E
inst_3 : K₀.HasOrthogonalProjection
inst_4 : K₁.HasOrthogonalProjection
⊢ K₀ᗮ ≤ K₁ ↔ K₁ᗮ ≤ K₀
have rw : K₁ᗮ ≤ K₀ᗮᗮ ↔ K₁ᗮ ≤ K₀
Tactic: rw [← orthogonal_le_orthogonal_iff, orthogonal_orthogonal]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K₀ K₁ : Submodule 𝕜 E
inst_3 : K₀.HasOrthogonalProjection
inst_4 : K₁.HasOrthogonalProjection
rw : K₁ᗮ ≤ K₀ᗮᗮ ↔ K₁ᗮ ≤ K₀
⊢ K₀ᗮ ≤ K₁ ↔ K₁ᗮ ≤ K₀
have rw₁ : K₁ᗮ ≤ K₀ ↔ K₁ᗮ ≤ K₀
Tactic: rw [← orthogonal_le_orthogonal_iff, orthogonal_orthogonal]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K₀ K₁ : Submodule 𝕜 E
inst_3 : K₀.HasOrthogonalProjection
inst_4 : K₁.HasOrthogonalProjection
⊢ K₀ ≤ K₁ᗮ ↔ K₁ ≤ K₀ᗮ
have rw : K₁ᗮᗮ ≤ K₀ᗮ ↔ K₁ ≤ K₀ᗮ
Tactic: rw [← orthogonal_le_orthogonal_iff, orthogonal_orthogonal]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K₀ K₁ : Submodule 𝕜 E
inst_3 : K₀.HasOrthogonalProjection
inst_4 : K₁.HasOrthogonalProjection
rw : K₁ᗮᗮ ≤ K₀ᗮ ↔ K₁ ≤ K₀ᗮ
⊢ K₀ ≤ K₁ᗮ ↔ K₁ ≤ K₀ᗮ
have rw₁ : K₁ ≤ K₀ᗮ ↔ K₁ ≤ K₀ᗮ
Tactic: rw [← orthogonal_le_orthogonal_iff, orthogonal_orthogonal]