awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Projection
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p q : P
hqs : q ∈ s
hpq : p -ᵥ q ∈ s.directionᗮ
hq : Membership.mem (γ := AffineSubspace 𝕜 P) (mk' p s.directionᗮ) q
mpr : Membership.mem (γ := Set P) {(↑((orthogonalProjection s : (a : P) → ↥s) p) : P)} q
⊢ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) = q

Tactic:
suffices q ∈ ({(orthogonalProjection s p : P)} : Set P) by
      simpa [eq_comm] using this
-- Module: Mathlib.Geometry.Euclidean.Projection
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p q : P
hqs : q ∈ s
hpq : p -ᵥ q ∈ s.directionᗮ
hq : Membership.mem (γ := AffineSubspace 𝕜 P) (mk' p s.directionᗮ) q
mpr : q ∈ (↑s : Set P) ∩ (↑(mk' p s.directionᗮ) : Set P)
⊢ Membership.mem (γ := Set P) {(↑((orthogonalProjection s : (a : P) → ↥s) p) : P)} q

Tactic:
rw [← inter_eq_singleton_orthogonalProjection]

Premises used: EuclideanGeometry.inter_eq_singleton_orthogonalProjection
-- Module: Mathlib.Geometry.Euclidean.Projection
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p q : P
hqs : q ∈ s
hpq : p -ᵥ q ∈ s.directionᗮ
hq : Membership.mem (γ := AffineSubspace 𝕜 P) (mk' p s.directionᗮ) q
⊢ q ∈ s ∧ Membership.mem (γ := AffineSubspace 𝕜 P) (mk' p s.directionᗮ) q

Tactic:
⟨hqs, hq⟩

Premises used: And.intro
-- Module: Mathlib.Geometry.Euclidean.Projection
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p q : P
hqs : q ∈ s
hpq : p -ᵥ q ∈ s.directionᗮ
hq : Membership.mem (γ := AffineSubspace 𝕜 P) (mk' p s.directionᗮ) q
⊢ q ∈ s ∧ Membership.mem (γ := AffineSubspace 𝕜 P) (mk' p s.directionᗮ) q

Tactic:
exact ⟨hqs, hq⟩
-- Module: Mathlib.Geometry.Euclidean.Projection
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p : P
q : ↥s
⊢ (orthogonalProjection s : (a : P) → ↥s) p = q ↔ p -ᵥ (↑q : P) ∈ s.directionᗮ

Tactic:
simpa using coe_orthogonalProjection_eq_iff_mem (s := s) (p := p) (q := (q : P))

Premises used: EuclideanGeometry.coe_orthogonalProjection_eq_iff_mem
-- Module: Mathlib.Geometry.Euclidean.Projection
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p q : P
rw :
  p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) q) : P) ∈ s.directionᗮ ↔
    p -ᵥ q + (q -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) q) : P)) ∈ s.directionᗮ
⊢ Eq (α := ↥s) ((orthogonalProjection s : (a : P) → ↥s) p : ↥s) ((orthogonalProjection s : (a : P) → ↥s) q : ↥s) ↔
    p -ᵥ q ∈ s.directionᗮ

Tactic:
rw [orthogonalProjection_eq_iff_mem, ← s.directionᗮ.add_mem_iff_left (x := p -ᵥ q)
    (vsub_orthogonalProjection_mem_direction_orthogonal s q)]

Premises used: EuclideanGeometry.vsub_orthogonalProjection_mem_direction_orthogonal, Submodule.orthogonal, Submodule.add_mem_iff_left, AffineSubspace.direction, EuclideanGeometry.orthogonalProjection_eq_iff_mem
-- Module: Mathlib.Geometry.Euclidean.Projection
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p q : P
⊢ p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) q) : P) ∈ s.directionᗮ ↔
    p -ᵥ q + (q -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) q) : P)) ∈ s.directionᗮ

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Projection
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s₁ s₂ : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s₁
inst_6 : Nonempty.{u_3 + 1} ↥s₂
inst_7 : s₁.direction.HasOrthogonalProjection
inst_8 : s₂.direction.HasOrthogonalProjection
p : P
h :
  Eq.{u_3 + 1} (α := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
    (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
inst_9 : (s₁ ⊔ s₂).direction.HasOrthogonalProjection
rw :
  (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ∈ s₁ ⊔ s₂ ∧
    p -ᵥ (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ∈ (s₁ ⊔ s₂).directionᗮ
⊢ Eq.{u_3 + 1} (α := P) (↑((orthogonalProjection (s₁ ⊔ s₂) : (a : P) → ↥(s₁ ⊔ s₂)) p) : P)
    (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)

Tactic:
rw [coe_orthogonalProjection_eq_iff_mem]

Premises used: EuclideanGeometry.coe_orthogonalProjection_eq_iff_mem
-- Module: Mathlib.Geometry.Euclidean.Projection
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s₁ s₂ : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s₁
inst_6 : Nonempty.{u_3 + 1} ↥s₂
inst_7 : s₁.direction.HasOrthogonalProjection
inst_8 : s₂.direction.HasOrthogonalProjection
p : P
h :
  Eq.{u_3 + 1} (α := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
    (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
inst_9 : (s₁ ⊔ s₂).direction.HasOrthogonalProjection
⊢ (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ∈ s₁ ⊔ s₂ ∧
    p -ᵥ (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ∈ (s₁ ⊔ s₂).directionᗮ

Tactic:
⟨SetLike.le_def.1 le_sup_left (orthogonalProjection_mem _), ?_⟩

Premises used: le_sup_left, SetLike.le_def, EuclideanGeometry.orthogonalProjection_mem, And.intro, Iff.mp
-- Module: Mathlib.Geometry.Euclidean.Projection
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s₁ s₂ : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s₁
inst_6 : Nonempty.{u_3 + 1} ↥s₂
inst_7 : s₁.direction.HasOrthogonalProjection
inst_8 : s₂.direction.HasOrthogonalProjection
p : P
h :
  Eq.{u_3 + 1} (α := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
    (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
inst_9 : (s₁ ⊔ s₂).direction.HasOrthogonalProjection
refine : p -ᵥ (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ∈ (s₁ ⊔ s₂).directionᗮ
⊢ (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ∈ s₁ ⊔ s₂ ∧
    p -ᵥ (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ∈ (s₁ ⊔ s₂).directionᗮ

Tactic:
refine ⟨SetLike.le_def.1 le_sup_left (orthogonalProjection_mem _), ?_⟩
-- Module: Mathlib.Geometry.Euclidean.Projection
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s₁ s₂ : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s₁
inst_6 : Nonempty.{u_3 + 1} ↥s₂
inst_7 : s₁.direction.HasOrthogonalProjection
inst_8 : s₂.direction.HasOrthogonalProjection
p : P
h :
  Eq.{u_3 + 1} (α := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
    (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
inst_9 : (s₁ ⊔ s₂).direction.HasOrthogonalProjection
rw : p -ᵥ (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ∈ s₁.directionᗮ ⊓ s₂.directionᗮ
⊢ p -ᵥ (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ∈ (s₁ ⊔ s₂).directionᗮ

Tactic:
rw [direction_sup_eq_sup_direction (orthogonalProjection_mem p) (h ▸ orthogonalProjection_mem p),
    ← Submodule.inf_orthogonal]

Premises used: AffineSubspace.direction_sup_eq_sup_direction, Submodule.inf_orthogonal, EuclideanGeometry.orthogonalProjection_mem
-- Module: Mathlib.Geometry.Euclidean.Projection
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s₁ s₂ : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s₁
inst_6 : Nonempty.{u_3 + 1} ↥s₂
inst_7 : s₁.direction.HasOrthogonalProjection
inst_8 : s₂.direction.HasOrthogonalProjection
p : P
h :
  Eq.{u_3 + 1} (α := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
    (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
inst_9 : (s₁ ⊔ s₂).direction.HasOrthogonalProjection
⊢ p -ᵥ (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ∈ s₁.directionᗮ ⊓ s₂.directionᗮ

Tactic:
⟨vsub_orthogonalProjection_mem_direction_orthogonal _ _,
    h ▸ vsub_orthogonalProjection_mem_direction_orthogonal _ _⟩

Premises used: EuclideanGeometry.vsub_orthogonalProjection_mem_direction_orthogonal, Set.Mem, setOf, Eq.rec, Set.inter, And.intro, Eq.symm
-- Module: Mathlib.Geometry.Euclidean.Projection
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s₁ s₂ : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s₁
inst_6 : Nonempty.{u_3 + 1} ↥s₂
inst_7 : s₁.direction.HasOrthogonalProjection
inst_8 : s₂.direction.HasOrthogonalProjection
p : P
h :
  Eq.{u_3 + 1} (α := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
    (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
inst_9 : (s₁ ⊔ s₂).direction.HasOrthogonalProjection
⊢ p -ᵥ (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ∈ s₁.directionᗮ ⊓ s₂.directionᗮ

Tactic:
exact ⟨vsub_orthogonalProjection_mem_direction_orthogonal _ _,
    h ▸ vsub_orthogonalProjection_mem_direction_orthogonal _ _⟩
-- Module: Mathlib.Geometry.Euclidean.Projection
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p : P
hp : p ∈ s
v : V
hv : v ∈ s.directionᗮ
a : (↑((orthogonalProjection s : (a : P) → ↥s) (v +ᵥ p)) : P) = (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp) : P)
⊢ (orthogonalProjection s : (a : P) → ↥s) (v +ᵥ p) = Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp

Tactic:
ext
-- Module: Mathlib.Geometry.Euclidean.Projection
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p : P
hp : p ∈ s
v : V
hv : v ∈ s.directionᗮ
⊢ (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp) : P) ∈ s ∧
    (v +ᵥ p) -ᵥ (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp) : P) ∈ s.directionᗮ

Tactic:
simp [*]
-- Module: Mathlib.Geometry.Euclidean.Projection
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p : P
hp : p ∈ s
v : V
hv : v ∈ s.directionᗮ
⊢ (↑((orthogonalProjection s : (a : P) → ↥s) (v +ᵥ p)) : P) = (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp) : P)

Tactic:
exact coe_orthogonalProjection_eq_iff_mem.mpr (by simp [*])

Premises used: Iff.mpr, EuclideanGeometry.coe_orthogonalProjection_eq_iff_mem
-- Module: Mathlib.Geometry.Euclidean.Projection
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p₁ p₂ : P
r : 𝕜
hp : p₁ ∈ s
⊢ (orthogonalProjection s : (a : P) → ↥s) (r • (p₂ -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p₂) : P)) +ᵥ p₁) =
    Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp

Tactic:
orthogonalProjection_vadd_eq_self hp
    (Submodule.smul_mem _ _ (vsub_orthogonalProjection_mem_direction_orthogonal s _))

Premises used: EuclideanGeometry.vsub_orthogonalProjection_mem_direction_orthogonal, EuclideanGeometry.orthogonalProjection_vadd_eq_self, Submodule.smul_mem
-- Module: Mathlib.Geometry.Euclidean.Projection
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s₁ s₂ : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s₁
inst_6 : Nonempty.{u_3 + 1} ↥s₂
inst_7 : s₁.direction.HasOrthogonalProjection
inst_8 : s₂.direction.HasOrthogonalProjection
h : s₁ ≤ s₂
p : P
rw : (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) -ᵥ p ∈ s₁.directionᗮ
⊢ Eq (α := ↥s₁) ((orthogonalProjection s₁ : (a : P) → ↥s₁) (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) : ↥s₁)
    ((orthogonalProjection s₁ : (a : P) → ↥s₁) p : ↥s₁)

Tactic:
rw [orthogonalProjection_eq_orthogonalProjection_iff_vsub_mem]

Premises used: EuclideanGeometry.orthogonalProjection_eq_orthogonalProjection_iff_vsub_mem
-- Module: Mathlib.Geometry.Euclidean.Projection
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s₁ s₂ : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s₁
inst_6 : Nonempty.{u_3 + 1} ↥s₂
inst_7 : s₁.direction.HasOrthogonalProjection
inst_8 : s₂.direction.HasOrthogonalProjection
h : s₁ ≤ s₂
p : P
⊢ (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) -ᵥ p ∈ s₁.directionᗮ

Tactic:
SetLike.le_def.1 (Submodule.orthogonal_le (direction_le h))
    (orthogonalProjection_vsub_mem_direction_orthogonal _ _)

Premises used: AffineSubspace.direction_le, Set.Mem, setOf, SetLike.le_def, Iff.mp, Submodule.orthogonal_le, EuclideanGeometry.orthogonalProjection_vsub_mem_direction_orthogonal
-- Module: Mathlib.Geometry.Euclidean.Projection
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s₁ s₂ : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s₁
inst_6 : Nonempty.{u_3 + 1} ↥s₂
inst_7 : s₁.direction.HasOrthogonalProjection
inst_8 : s₂.direction.HasOrthogonalProjection
h : s₁ ≤ s₂
p : P
⊢ (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) -ᵥ p ∈ s₁.directionᗮ

Tactic:
exact SetLike.le_def.1 (Submodule.orthogonal_le (direction_le h))
    (orthogonalProjection_vsub_mem_direction_orthogonal _ _)

Premises used: AffineSubspace.direction_le, SetLike.le_def, Iff.mp, Submodule.orthogonal_le, EuclideanGeometry.orthogonalProjection_vsub_mem_direction_orthogonal
-- Module: Mathlib.Geometry.Euclidean.Projection
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p₁ p₂ : P
hp₁ : p₁ ∈ s
h :
  inner 𝕜 (p₁ -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p₂) : P))
      ((↑((orthogonalProjection s : (a : P) → ↥s) p₂) : P) -ᵥ p₂) =
    0
⊢ dist p₁ p₂ * dist p₁ p₂ =
    dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₂) : P) *
        dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₂) : P) +
      dist p₂ (↑((orthogonalProjection s : (a : P) → ↥s) p₂) : P) *
        dist p₂ (↑((orthogonalProjection s : (a : P) → ↥s) p₂) : P)

Tactic:
rw [dist_comm p₂ _, dist_eq_norm_vsub V p₁ _, dist_eq_norm_vsub V p₁ _, dist_eq_norm_vsub V _ p₂,
    ← vsub_add_vsub_cancel p₁ (orthogonalProjection s p₂) p₂,
    norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero (𝕜 := 𝕜)]

Premises used: vsub_add_vsub_cancel, dist_comm, EuclideanGeometry.orthogonalProjection, dist_eq_norm_vsub, Subtype.val, DFunLike.coe, norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Projection
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p₁ p₂ : P
hp₁ : p₁ ∈ s
⊢ inner 𝕜 (p₁ -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p₂) : P))
      ((↑((orthogonalProjection s : (a : P) → ↥s) p₂) : P) -ᵥ p₂) =
    0

Tactic:
Submodule.inner_right_of_mem_orthogonal (vsub_orthogonalProjection_mem_direction p₂ hp₁)
    (orthogonalProjection_vsub_mem_direction_orthogonal s p₂)

Premises used: Submodule.inner_right_of_mem_orthogonal, EuclideanGeometry.vsub_orthogonalProjection_mem_direction, EuclideanGeometry.orthogonalProjection_vsub_mem_direction_orthogonal
-- Module: Mathlib.Geometry.Euclidean.Projection
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p₁ p₂ : P
hp₁ : p₁ ∈ s
⊢ inner 𝕜 (p₁ -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p₂) : P))
      ((↑((orthogonalProjection s : (a : P) → ↥s) p₂) : P) -ᵥ p₂) =
    0

Tactic:
exact Submodule.inner_right_of_mem_orthogonal (vsub_orthogonalProjection_mem_direction p₂ hp₁)
    (orthogonalProjection_vsub_mem_direction_orthogonal s p₂)

Premises used: Submodule.inner_right_of_mem_orthogonal, EuclideanGeometry.vsub_orthogonalProjection_mem_direction, EuclideanGeometry.orthogonalProjection_vsub_mem_direction_orthogonal
-- Module: Mathlib.Geometry.Euclidean.Projection
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst_5 : s.direction.HasOrthogonalProjection
p₁ p₂ : P
hp₂ : p₂ ∈ s
⊢ Nonempty.{u_3 + 1} ↥s

Tactic:
haveI : Nonempty s := ⟨p₂, hp₂⟩
-- Module: Mathlib.Geometry.Euclidean.Projection
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst_5 : s.direction.HasOrthogonalProjection
p₁ p₂ : P
hp₂ : p₂ ∈ s
this : Nonempty.{u_3 + 1} ↥s
mp :
  dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = dist p₁ p₂ →
    (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = p₂
mpr :
  (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = p₂ →
    dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = dist p₁ p₂
⊢ dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = dist p₁ p₂ ↔
    (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = p₂

Tactic:
constructor
-- Module: Mathlib.Geometry.Euclidean.Projection
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst_5 : s.direction.HasOrthogonalProjection
p₁ p₂ : P
hp₂ : p₂ ∈ s
this : Nonempty.{u_3 + 1} ↥s
h : (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = p₂
mpr mpr₁ :
  dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) =
    dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P)
⊢ dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = dist p₁ p₂

Tactic:
nth_rw 4 [← h]
-- Module: Mathlib.Geometry.Euclidean.Projection
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p : P
⊢ dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) = Metric.infDist p (↑s : Set P)

Tactic:
le_antisymm ?_ (Metric.infDist_le_dist_of_mem (orthogonalProjection_mem _))

Premises used: Metric.infDist_le_dist_of_mem, le_antisymm, EuclideanGeometry.orthogonalProjection_mem
-- Module: Mathlib.Geometry.Euclidean.Projection
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p : P
refine : dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) ≤ Metric.infDist p (↑s : Set P)
⊢ dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) = Metric.infDist p (↑s : Set P)

Tactic:
refine le_antisymm ?_ (Metric.infDist_le_dist_of_mem (orthogonalProjection_mem _))

Premises used: Metric.infDist_le_dist_of_mem, le_antisymm, EuclideanGeometry.orthogonalProjection_mem
-- Module: Mathlib.Geometry.Euclidean.Projection
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p : P
rw : dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) ≤ ⨅ (y : (↑(↑s : Set P) : Type u_3)), dist p (↑y : P)
⊢ dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) ≤ Metric.infDist p (↑s : Set P)

Tactic:
rw [Metric.infDist_eq_iInf]

Premises used: Metric.infDist_eq_iInf
-- Module: Mathlib.Geometry.Euclidean.Projection
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p : P
⊢ dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) ≤ ⨅ (y : (↑(↑s : Set P) : Type u_3)), dist p (↑y : P)

Tactic:
le_ciInf fun x ↦ le_of_sq_le_sq ?_ dist_nonneg

Premises used: dist_nonneg, le_of_sq_le_sq, le_ciInf
-- Module: Mathlib.Geometry.Euclidean.Projection
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p : P
refine :
  ∀ (x : (↑(↑s : Set P) : Type u_3)),
    HPow.hPow (β := ℕ) (dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) 2 ≤
      HPow.hPow (β := ℕ) (dist p (↑x : P)) 2
⊢ dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) ≤ ⨅ (y : (↑(↑s : Set P) : Type u_3)), dist p (↑y : P)

Tactic:
refine le_ciInf fun x ↦ le_of_sq_le_sq ?_ dist_nonneg

Premises used: dist_nonneg, le_of_sq_le_sq, le_ciInf
-- Module: Mathlib.Geometry.Euclidean.Projection
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p : P
x : (↑(↑s : Set P) : Type u_3)
rw :
  HPow.hPow (β := ℕ) (dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) 2 ≤
    HPow.hPow (β := ℕ) (dist (↑x : P) p) 2
⊢ HPow.hPow (β := ℕ) (dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) 2 ≤
    HPow.hPow (β := ℕ) (dist p (↑x : P)) 2

Tactic:
rw [dist_comm _ (x : P)]

Premises used: dist_comm, Subtype.val