awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h_1 : ‖u - v‖ = ⨅ (w : (↑(↑K : Set F) : Type u_3)), ‖u - (↑w : F)‖
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : F
hw : w ∈ K
w' : F := w + v
this : w' ∈ K
h₁ : ⟪u - v, w' - v⟫_ℝ ≤ 0
⊢ w' - v = w

Tactic:
have h₂ : w' - v = w := by
          simp only [w', add_neg_cancel_right, sub_eq_add_neg]
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h_1 : ‖u - v‖ = ⨅ (w : (↑(↑K : Set F) : Type u_3)), ‖u - (↑w : F)‖
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : F
hw : w ∈ K
w' : F := w + v
this : w' ∈ K
h₁ : ⟪u - v, w' - v⟫_ℝ ≤ 0
h₂ : w' - v = w
⊢ ⟪u - v, w⟫_ℝ ≤ 0

Tactic:
rw [h₂] at h₁
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h_1 : ‖u - v‖ = ⨅ (w : (↑(↑K : Set F) : Type u_3)), ‖u - (↑w : F)‖
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : F
hw : w ∈ K
w' : F := w + v
this : w' ∈ K
h₁ : ⟪u - v, w' - v⟫_ℝ ≤ 0
h₂ : w' - v = w
h₃ : ⟪u - v, w⟫_ℝ ≤ 0
⊢ w' - v = w

Tactic:
rw [h₂] at h₁
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h_1 : ‖u - v‖ = ⨅ (w : (↑(↑K : Set F) : Type u_3)), ‖u - (↑w : F)‖
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : F
hw : w ∈ K
w' : F := w + v
this : w' ∈ K
h₁ : ⟪u - v, w⟫_ℝ ≤ 0
h₂ : w' - v = w
⊢ ⟪u - v, w⟫_ℝ ≤ 0

Tactic:
h₁
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h_1 : ‖u - v‖ = ⨅ (w : (↑(↑K : Set F) : Type u_3)), ‖u - (↑w : F)‖
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : F
hw : w ∈ K
w' : F := w + v
this : w' ∈ K
h₁ : ⟪u - v, w⟫_ℝ ≤ 0
h₂ : w' - v = w
⊢ ⟪u - v, w⟫_ℝ ≤ 0

Tactic:
exact h₁
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h_1 : ‖u - v‖ = ⨅ (w : (↑(↑K : Set F) : Type u_3)), ‖u - (↑w : F)‖
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : F
hw : w ∈ K
⊢ ⟪u - v, w⟫_ℝ ≤ 0

Tactic:
have le : ⟪u - v, w⟫_ℝ ≤ 0 := by
        let w' := w + v
        have : w' ∈ K := Submodule.add_mem _ hw hv
        have h₁ := h w' this
        have h₂ : w' - v = w := by
          simp only [w', add_neg_cancel_right, sub_eq_add_neg]
        rw [h₂] at h₁
        exact h₁
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h_1 : ‖u - v‖ = ⨅ (w : (↑(↑K : Set F) : Type u_3)), ‖u - (↑w : F)‖
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : F
hw : w ∈ K
le : ⟪u - v, w⟫_ℝ ≤ 0
w'' : F := -w + v
⊢ w'' ∈ K

Tactic:
have : w'' ∈ K := Submodule.add_mem _ (Submodule.neg_mem _ hw) hv
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h_1 : ‖u - v‖ = ⨅ (w : (↑(↑K : Set F) : Type u_3)), ‖u - (↑w : F)‖
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : F
hw : w ∈ K
le : ⟪u - v, w⟫_ℝ ≤ 0
w'' : F := -w + v
this : w'' ∈ K
⊢ ⟪u - v, w'' - v⟫_ℝ ≤ 0

Tactic:
have h₁ := h w'' this
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h_1 : ‖u - v‖ = ⨅ (w : (↑(↑K : Set F) : Type u_3)), ‖u - (↑w : F)‖
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : F
hw : w ∈ K
le : ⟪u - v, w⟫_ℝ ≤ 0
w'' : F := -w + v
this : w'' ∈ K
h₁ : ⟪u - v, w'' - v⟫_ℝ ≤ 0
⊢ w'' - v = -w

Tactic:
simp only [w'', add_neg_cancel_right, sub_eq_add_neg]

Premises used: add_neg_cancel_right, sub_eq_add_neg
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h_1 : ‖u - v‖ = ⨅ (w : (↑(↑K : Set F) : Type u_3)), ‖u - (↑w : F)‖
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : F
hw : w ∈ K
le : ⟪u - v, w⟫_ℝ ≤ 0
w'' : F := -w + v
this : w'' ∈ K
h₁ : ⟪u - v, w'' - v⟫_ℝ ≤ 0
⊢ w'' - v = -w

Tactic:
have h₂ : w'' - v = -w := by
          simp only [w'', add_neg_cancel_right, sub_eq_add_neg]
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h_1 : ‖u - v‖ = ⨅ (w : (↑(↑K : Set F) : Type u_3)), ‖u - (↑w : F)‖
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : F
hw : w ∈ K
le : ⟪u - v, w⟫_ℝ ≤ 0
w'' : F := -w + v
this : w'' ∈ K
h₁ : ⟪u - v, w'' - v⟫_ℝ ≤ 0
h₂ : w'' - v = -w
⊢ -⟪u - v, w⟫_ℝ ≤ 0

Tactic:
rw [h₂, inner_neg_right] at h₁

Premises used: inner_neg_right
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h_1 : ‖u - v‖ = ⨅ (w : (↑(↑K : Set F) : Type u_3)), ‖u - (↑w : F)‖
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : F
hw : w ∈ K
le : ⟪u - v, w⟫_ℝ ≤ 0
w'' : F := -w + v
this : w'' ∈ K
h₁ : ⟪u - v, w'' - v⟫_ℝ ≤ 0
h₂ : w'' - v = -w
h₃ : -⟪u - v, w⟫_ℝ ≤ 0
⊢ w'' - v = -w

Tactic:
rw [h₂, inner_neg_right] at h₁

Premises used: inner_neg_right
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h_1 : ‖u - v‖ = ⨅ (w : (↑(↑K : Set F) : Type u_3)), ‖u - (↑w : F)‖
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : F
hw : w ∈ K
le : ⟪u - v, w⟫_ℝ ≤ 0
w'' : F := -w + v
this : w'' ∈ K
h₁ : -⟪u - v, w⟫_ℝ ≤ 0
h₂ : w'' - v = -w
linarith : ⟪u - v, w⟫_ℝ < 0 → -⟪u - v, w⟫_ℝ - 0 + (⟪u - v, w⟫_ℝ - 0) = 0
⊢ ⟪u - v, w⟫_ℝ ≥ 0

Tactic:
linarith
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h_1 : ‖u - v‖ = ⨅ (w : (↑(↑K : Set F) : Type u_3)), ‖u - (↑w : F)‖
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : F
hw : w ∈ K
le : ⟪u - v, w⟫_ℝ ≤ 0
⊢ ⟪u - v, w⟫_ℝ ≥ 0

Tactic:
have ge : ⟪u - v, w⟫_ℝ ≥ 0 := by
        let w'' := -w + v
        have : w'' ∈ K := Submodule.add_mem _ (Submodule.neg_mem _ hw) hv
        have h₁ := h w'' this
        have h₂ : w'' - v = -w := by
          simp only [w'', add_neg_cancel_right, sub_eq_add_neg]
        rw [h₂, inner_neg_right] at h₁
        linarith
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h_1 : ‖u - v‖ = ⨅ (w : (↑(↑K : Set F) : Type u_3)), ‖u - (↑w : F)‖
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : F
hw : w ∈ K
le : ⟪u - v, w⟫_ℝ ≤ 0
ge : ⟪u - v, w⟫_ℝ ≥ 0
⊢ ⟪u - v, w⟫_ℝ = 0

Tactic:
le_antisymm le ge

Premises used: le_antisymm
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h_1 : ‖u - v‖ = ⨅ (w : (↑(↑K : Set F) : Type u_3)), ‖u - (↑w : F)‖
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : F
hw : w ∈ K
le : ⟪u - v, w⟫_ℝ ≤ 0
ge : ⟪u - v, w⟫_ℝ ≥ 0
⊢ ⟪u - v, w⟫_ℝ = 0

Tactic:
exact le_antisymm le ge

Premises used: le_antisymm
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h : ∀ w ∈ K, ⟪u - v, w⟫_ℝ = 0
w : F
hw : w ∈ K
w' : F := w - v
⊢ w' ∈ K

Tactic:
have : w' ∈ K := Submodule.sub_mem _ hw hv
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h : ∀ w ∈ K, ⟪u - v, w⟫_ℝ = 0
w : F
hw : w ∈ K
w' : F := w - v
this : w' ∈ K
⊢ ⟪u - v, w'⟫_ℝ = 0

Tactic:
have h₁ := h w' this
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h : ∀ w ∈ K, ⟪u - v, w⟫_ℝ = 0
w : F
hw : w ∈ K
w' : F := w - v
this : w' ∈ K
h₁ : ⟪u - v, w'⟫_ℝ = 0
⊢ ⟪u - v, w - v⟫_ℝ ≤ 0

Tactic:
le_of_eq h₁

Premises used: le_of_eq
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h : ∀ w ∈ K, ⟪u - v, w⟫_ℝ = 0
w : F
hw : w ∈ K
w' : F := w - v
this : w' ∈ K
h₁ : ⟪u - v, w'⟫_ℝ = 0
⊢ ⟪u - v, w - v⟫_ℝ ≤ 0

Tactic:
exact le_of_eq h₁

Premises used: le_of_eq
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h : ∀ w ∈ K, ⟪u - v, w⟫_ℝ = 0
⊢ ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0

Tactic:
have : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0 := by
        intro w hw
        let w' := w - v
        have : w' ∈ K := Submodule.sub_mem _ hw hv
        have h₁ := h w' this
        exact le_of_eq h₁
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h : ∀ w ∈ K, ⟪u - v, w⟫_ℝ = 0
this : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
h₁ : Convex ℝ (↑K : Set F)
hv₁ : v ∈ (↑K : Set F)
⊢ ‖u - v‖ = ⨅ (w : (↑(↑K : Set F) : Type u_3)), ‖u - (↑w : F)‖

Tactic:
rwa [norm_eq_iInf_iff_real_inner_le_zero]

Premises used: norm_eq_iInf_iff_real_inner_le_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h : ∀ w ∈ K, ⟪u - v, w⟫_ℝ = 0
this : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
⊢ Convex ℝ (↑K : Set F)

Tactic:
Submodule.convex _

Premises used: Submodule.convex
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h : ∀ w ∈ K, ⟪u - v, w⟫_ℝ = 0
this : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
⊢ v ∈ (↑K : Set F)

Tactic:
hv
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h : ∀ w ∈ K, ⟪u - v, w⟫_ℝ = 0
this : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
⊢ Convex ℝ (↑K : Set F)

Tactic:
exacts [Submodule.convex _, hv]

Premises used: Submodule.convex
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
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
mp : ‖u - v‖ = ⨅ (w : ↥K), ‖u - (↑w : E)‖ → ∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0
mpr : (∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0) → ‖u - v‖ = ⨅ (w : ↥K), ‖u - (↑w : E)‖
⊢ ‖u - v‖ = ⨅ (w : ↥K), ‖u - (↑w : E)‖ ↔ ∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0

Tactic:
constructor
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
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)‖
⊢ ∀ w ∈ K, Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪u - v, w⟫_𝕜 : ℝ) (0 : ℝ)

Tactic:
have A : ∀ w ∈ K, re ⟪u - v, w⟫ = 0 := (K'.norm_eq_iInf_iff_real_inner_eq_zero hv).1 H
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
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 : ℝ)
mp₁ : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) ⟪u - v, w⟫_𝕜 : ℝ) ((im : (a : 𝕜) → ℝ) 0 : ℝ)
⊢ ⟪u - v, w⟫_𝕜 = 0

Tactic:
apply RCLike.ext

Premises used: RCLike.ext
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
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, w⟫_𝕜 : ℝ) ((re : (a : 𝕜) → ℝ) 0 : ℝ)

Tactic:
simp [A w hw]
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
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 (α := ℝ) ((im : (a : 𝕜) → ℝ) 0 : ℝ) ((im : (a : 𝕜) → ℝ) ⟪u - v, w⟫_𝕜 : ℝ)
⊢ Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) ⟪u - v, w⟫_𝕜 : ℝ) ((im : (a : 𝕜) → ℝ) 0 : ℝ)

Tactic:
symm
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
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 : ℝ) (0 : ℝ)

Tactic:
im.map_zero

Premises used: AddMonoidHom.map_zero, RCLike.im
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
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 (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪u - v, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (-I) w⟫_𝕜 : ℝ)

Tactic:
(A _ (K.smul_mem (-I) hw)).symm

Premises used: RCLike.I, Eq.symm, Neg.neg, Submodule.smul_mem
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
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
rw rw₁ : Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) (-I * ⟪u - v, w⟫_𝕜) : ℝ) ((re : (a : 𝕜) → ℝ) (-I * ⟪u - v, w⟫_𝕜) : ℝ)
⊢ Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪u - v, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (-I) w⟫_𝕜 : ℝ)
    ((re : (a : 𝕜) → ℝ) (-I * ⟪u - v, w⟫_𝕜) : ℝ)

Tactic:
rw [inner_smul_right]

Premises used: inner_smul_right
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
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 : 𝕜) → ℝ) (-I * ⟪u - v, w⟫_𝕜) : ℝ) ((im : (a : 𝕜) → ℝ) ⟪u - v, w⟫_𝕜 : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
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⟫_𝕜) : ℝ)
im₁ : Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) (-I * ⟪u - v, w⟫_𝕜) : ℝ) ((RCLike.im : (a : 𝕜) → ℝ) ⟪u - v, w⟫_𝕜 : ℝ)
⊢ Eq (α := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) 0 : ℝ) ((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

Premises used: AddMonoidHom.map_zero, RCLike.im, RCLike.I, OfNat.ofNat, Eq.symm, DFunLike.coe, Neg.neg, Submodule.smul_mem
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
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'
rw : Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) 0 : ℝ) (0 : ℝ)
⊢ ⟪u - v, w⟫_ℝ = 0

Tactic:
rw [real_inner_eq_re_inner, H w hw]

Premises used: real_inner_eq_re_inner
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
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'
⊢ Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) 0 : ℝ) (0 : ℝ)

Tactic:
zero_re

Premises used: RCLike.zero_re
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
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'
⊢ Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) 0 : ℝ) (0 : ℝ)

Tactic:
exact zero_re

Premises used: RCLike.zero_re
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
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 ∈ 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
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
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_1 : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
K' : Submodule ℝ E := restrictScalars ℝ K
H : ∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0
this : ∀ w ∈ K', ⟪u - v, w⟫_ℝ = 0
⊢ ‖u - v‖ = ⨅ (w : ↥K), ‖u - (↑w : E)‖

Tactic:
(K'.norm_eq_iInf_iff_real_inner_eq_zero hv).2 this

Premises used: Iff.mpr, Set.Mem, Submodule.norm_eq_iInf_iff_real_inner_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
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_1 : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
K' : Submodule ℝ E := restrictScalars ℝ K
H : ∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0
this : ∀ w ∈ K', ⟪u - v, w⟫_ℝ = 0
⊢ ‖u - v‖ = ⨅ (w : ↥K), ‖u - (↑w : E)‖

Tactic:
exact (K'.norm_eq_iInf_iff_real_inner_eq_zero hv).2 this

Premises used: Iff.mpr, Submodule.norm_eq_iInf_iff_real_inner_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
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
⊢ (HSMul.hSMul (α := ℕ) 2 (↑K.starProjection : E →ₗ[𝕜] E) - LinearMap.id : (a : E) → E)
      ((HSMul.hSMul (α := ℕ) 2 (↑K.starProjection : E →ₗ[𝕜] E) - LinearMap.id : (a : E) → E) x : E) =
    x

Tactic:
simp [two_smul, starProjection_eq_self_iff.mpr]

Premises used: Iff.mpr, two_smul, Submodule.starProjection_eq_self_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
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)
⊢ ⟪v, (↑w : E)⟫ = 0

Tactic:
have : ⟪v, w⟫ = 0 := starProjection_inner_eq_zero x w w.2
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
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
⊢ ‖(↑w : E) - v‖ = ‖(↑w : E) + v‖

Tactic:
norm_sub_eq_norm_add this

Premises used: norm_sub_eq_norm_add
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
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
h₁ : x = (↑w : E) + v
⊢ norm (E := E) ((K.reflectionLinearEquiv : (a : E) → E) x : E) = ‖x‖

Tactic:
convert! norm_sub_eq_norm_add this using 2

Premises used: norm_sub_eq_norm_add
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
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 :
  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))
⊢ (K.reflectionLinearEquiv : (a : E) → E) x = (↑w : E) - v

Tactic:
dsimp [reflectionLinearEquiv, v, w]

Premises used: Submodule.reflectionLinearEquiv
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
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
⊢ 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:
abel
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
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
⊢ x = (↑w : E) + v

Tactic:
simp only [v, add_sub_cancel]

Premises used: add_sub_cancel