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
⊢ ContinuousAffineMap.contLinear (orthogonalProjection s) = s.direction.orthogonalProjection

Tactic:
rfl

Premises used: ContinuousAffineMap.contLinear, Set.Mem, Submodule.orthogonalProjection, LinearMap.mkContinuous, rfl
-- 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
⊢ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) ∈ s

Tactic:
(orthogonalProjection s p).2

Premises used: EuclideanGeometry.orthogonalProjection, DFunLike.coe, Subtype.property
-- 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 :
  p -ᵥ (↑(Classical.arbitrary ↥s) : P) -
      (↑((s.direction.orthogonalProjection : (a : V) → ↥s.direction) (p -ᵥ (↑(Classical.arbitrary ↥s) : P))) : V) ∈
    s.directionᗮ
⊢ Membership.mem (γ := AffineSubspace 𝕜 P) (mk' p s.directionᗮ) (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)

Tactic:
rw [mem_mk', orthogonalProjection_apply, coe_vadd, vadd_vsub_eq_sub_vsub,
    ← Submodule.neg_mem_iff, neg_sub]

Premises used: neg_sub, vadd_vsub_eq_sub_vsub, Submodule.neg_mem_iff, AffineSubspace.coe_vadd, AffineSubspace.mem_mk', EuclideanGeometry.orthogonalProjection_apply
-- 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 -ᵥ (↑(Classical.arbitrary ↥s) : P) -
      (↑((s.direction.orthogonalProjection : (a : V) → ↥s.direction) (p -ᵥ (↑(Classical.arbitrary ↥s) : P))) : V) ∈
    s.directionᗮ

Tactic:
apply Submodule.sub_starProjection_mem_orthogonal

Premises used: Submodule.sub_starProjection_mem_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
rw : IsCompl s.direction s.directionᗮ
⊢ IsCompl s.direction (direction (mk' p s.directionᗮ))

Tactic:
rw [direction_mk' p s.directionᗮ]

Premises used: Submodule.orthogonal, AffineSubspace.direction_mk', AffineSubspace.direction
-- 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
⊢ IsCompl s.direction s.directionᗮ

Tactic:
Submodule.isCompl_orthogonal_of_hasOrthogonalProjection

Premises used: Submodule.isCompl_orthogonal_of_hasOrthogonalProjection
-- 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
⊢ IsCompl s.direction s.directionᗮ

Tactic:
exact Submodule.isCompl_orthogonal_of_hasOrthogonalProjection

Premises used: Submodule.isCompl_orthogonal_of_hasOrthogonalProjection
-- 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
obtain :
  ∀ (q : P) (hq : (↑s : Set P) ∩ (↑(mk' p s.directionᗮ) : Set P) = {q}),
    (↑s : Set P) ∩ (↑(mk' p s.directionᗮ) : Set P) = {(↑((orthogonalProjection s : (a : P) → ↥s) p) : P)}
⊢ (↑s : Set P) ∩ (↑(mk' p s.directionᗮ) : Set P) = {(↑((orthogonalProjection s : (a : P) → ↥s) p) : P)}

Tactic:
obtain ⟨q, hq⟩ := inter_eq_singleton_of_nonempty_of_isCompl (nonempty_subtype.mp ‹_›)
    (mk'_nonempty p s.directionᗮ)
    (by
      rw [direction_mk' p s.directionᗮ]
      exact Submodule.isCompl_orthogonal_of_hasOrthogonalProjection)

Premises used: AffineSubspace.inter_eq_singleton_of_nonempty_of_isCompl, Submodule.orthogonal, AffineSubspace.mk'_nonempty, nonempty_subtype, Iff.mp, AffineSubspace.direction
-- 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
hq : (↑s : Set P) ∩ (↑(mk' p s.directionᗮ) : Set P) = {q}
rwa rwa₁ rwa₂ rwa₃ : (↑s : Set P) ∩ (↑(mk' p s.directionᗮ) : Set P) = {q}
⊢ (↑s : Set P) ∩ (↑(mk' p s.directionᗮ) : Set P) = {(↑((orthogonalProjection s : (a : P) → ↥s) p) : P)}

Tactic:
rwa [Set.eq_singleton_iff_nonempty_unique_mem.1 hq |>.2 _
    ⟨orthogonalProjection_mem _, orthogonalProjection_mem_orthogonal _ _⟩]

Premises used: Set.eq_singleton_iff_nonempty_unique_mem, And.right, EuclideanGeometry.orthogonalProjection_mem, And.intro, Iff.mp, EuclideanGeometry.orthogonalProjection_mem_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
⊢ (↑((orthogonalProjection s : (a : P) → ↥s) p₂ -ᵥ Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁) : V) ∈ s.direction

Tactic:
(orthogonalProjection s p₂ -ᵥ ⟨p₁, hp₁⟩ : s.direction).2

Premises used: VSub.vsub, Subtype.mk, EuclideanGeometry.orthogonalProjection, DFunLike.coe, Subtype.property
-- 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
⊢ (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁ -ᵥ (orthogonalProjection s : (a : P) → ↥s) p₂) : V) ∈ s.direction

Tactic:
((⟨p₁, hp₁⟩ : s) -ᵥ orthogonalProjection s p₂ : s.direction).2

Premises used: VSub.vsub, Subtype.mk, EuclideanGeometry.orthogonalProjection, DFunLike.coe, Subtype.property
-- 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
mp : (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) = p → p ∈ s
mpr : p ∈ s → (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) = p
⊢ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) = p ↔ p ∈ s

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 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p : P
⊢ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) = p → p ∈ s

Tactic:
fun h => h ▸ orthogonalProjection_mem p

Premises used: Eq.rec, 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
⊢ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) = p → p ∈ s

Tactic:
exact fun h => h ▸ orthogonalProjection_mem p
-- 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
h : p ∈ s
⊢ p ∈ (↑s : Set P) ∩ (↑(mk' p s.directionᗮ) : Set P)

Tactic:
have hp : p ∈ (s : Set P) ∩ mk' p s.directionᗮ := ⟨h, self_mem_mk' p _⟩
-- 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
h : p ∈ s
hp : p ∈ (↑s : Set P) ∩ (↑(mk' p s.directionᗮ) : Set P)
⊢ Membership.mem (γ := Set P) {(↑((orthogonalProjection s : (a : P) → ↥s) p) : P)} p

Tactic:
rw [inter_eq_singleton_orthogonalProjection p] at hp

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 : P
h : p ∈ s
hp : Membership.mem (γ := Set P) {(↑((orthogonalProjection s : (a : P) → ↥s) p) : P)} p
mpr : p = (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
⊢ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) = p

Tactic:
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 : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p : P
h : p ∈ s
hp : Membership.mem (γ := Set P) {(↑((orthogonalProjection s : (a : P) → ↥s) p) : P)} p
⊢ p = (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)

Tactic:
hp

Premises used: Set.Mem, setOf, Set.singleton
-- 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
h : p ∈ s
hp : Membership.mem (γ := Set P) {(↑((orthogonalProjection s : (a : P) → ↥s) p) : P)} p
⊢ p = (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)

Tactic:
exact 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 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p : ↥s
a : (↑((orthogonalProjection s : (a : P) → ↥s) (↑p : P)) : P) = (↑p : P)
⊢ (orthogonalProjection s : (a : P) → ↥s) (↑p : P) = p

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 : ↥s
a : (↑p : P) ∈ s
⊢ (↑((orthogonalProjection s : (a : P) → ↥s) (↑p : P)) : P) = (↑p : P)

Tactic:
rw [orthogonalProjection_eq_self_iff]

Premises used: EuclideanGeometry.orthogonalProjection_eq_self_iff
-- 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 : ↥s
⊢ (↑p : P) ∈ s

Tactic:
p.2

Premises used: Subtype.property
-- 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 : ↥s
⊢ (↑p : P) ∈ s

Tactic:
exact p.2

Premises used: Subtype.property
-- 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
⊢ Eq (α := ↥s) ((orthogonalProjection s : (a : P) → ↥s) (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) : ↥s)
    ((orthogonalProjection s : (a : P) → ↥s) p : ↥s)

Tactic:
orthogonalProjection_mem_subspace_eq_self ((orthogonalProjection s) p)

Premises used: EuclideanGeometry.orthogonalProjection, DFunLike.coe, EuclideanGeometry.orthogonalProjection_mem_subspace_eq_self
-- 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
subst :
  ∀ [inst_9 : Nonempty.{u_3 + 1} ↥s] [inst_10 : s.direction.HasOrthogonalProjection],
    Eq.{u_3 + 1} (α := P) (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
      (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
⊢ Eq.{u_3 + 1} (α := P) (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
    (↑((orthogonalProjection s' : (a : P) → ↥s') p) : P)

Tactic:
subst 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
inst_7 : Nonempty.{u_3 + 1} ↥s
inst_8 : s.direction.HasOrthogonalProjection
⊢ Eq.{u_3 + 1} (α := P) (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
    (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)

Tactic:
rfl
-- 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
p₁ p₂ : P
⊢ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 {p₁})
    (↑((orthogonalProjection (affineSpan 𝕜 {p₁}) : (a : P) → ↥(affineSpan 𝕜 {p₁})) p₂) : P)

Tactic:
have h := SetLike.coe_mem (orthogonalProjection (affineSpan 𝕜 {p₁}) p₂)
-- 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
p₁ p₂ : P
h :
  Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 {p₁})
    (↑((orthogonalProjection (affineSpan 𝕜 {p₁}) : (a : P) → ↥(affineSpan 𝕜 {p₁})) p₂) : P)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (h : (↑((orthogonalProjection (affineSpan 𝕜 {p₁}) : (a : P) → ↥(affineSpan 𝕜 {p₁})) p₂) : P) = p₁),
    (↑((orthogonalProjection (affineSpan 𝕜 {p₁}) : (a : P) → ↥(affineSpan 𝕜 {p₁})) p₂) : P) = p₁
⊢ (↑((orthogonalProjection (affineSpan 𝕜 {p₁}) : (a : P) → ↥(affineSpan 𝕜 {p₁})) p₂) : P) = p₁

Tactic:
rwa [mem_affineSpan_singleton] at h

Premises used: AffineSubspace.mem_affineSpan_singleton
-- 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 (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p = 0 ↔ p ∈ s
rw₁ : (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) = p ↔ p ∈ s
rw₂ rw₃ : p ∈ s ↔ p ∈ s
⊢ dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) = 0 ↔ p ∈ s

Tactic:
rw [dist_comm, dist_eq_zero, orthogonalProjection_eq_self_iff]

Premises used: dist_comm, dist_eq_zero, EuclideanGeometry.orthogonalProjection_eq_self_iff
-- 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
⊢ dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) ≠ 0

Tactic:
mt dist_orthogonalProjection_eq_zero_iff.mp hp

Premises used: mt, EuclideanGeometry.dist_orthogonalProjection_eq_zero_iff, 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 : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p : P
rw : Membership.mem (γ := AffineSubspace 𝕜 P) (mk' p s.directionᗮ) (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
⊢ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) -ᵥ p ∈ s.directionᗮ

Tactic:
rw [← mem_mk']

Premises used: AffineSubspace.mem_mk'
-- 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
⊢ Membership.mem (γ := AffineSubspace 𝕜 P) (mk' p s.directionᗮ) (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)

Tactic:
apply orthogonalProjection_mem_orthogonal

Premises used: EuclideanGeometry.orthogonalProjection_mem_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 -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) ∈ s.directionᗮ

Tactic:
direction_mk' p s.directionᗮ ▸
    vsub_mem_direction (self_mem_mk' _ _) (orthogonalProjection_mem_orthogonal s p)

Premises used: AffineSubspace.self_mem_mk', AffineSubspace.vsub_mem_direction, Eq.rec, Submodule.orthogonal, AffineSubspace.direction_mk', EuclideanGeometry.orthogonalProjection_mem_orthogonal, AffineSubspace.direction
-- 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
⊢ Eq (α := ↥s.direction)
    ((s.direction.orthogonalProjection : (a : V) → ↥s.direction)
        (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) :
      ↥s.direction)
    (0 : ↥s.direction)

Tactic:
simpa using vsub_orthogonalProjection_mem_direction_orthogonal _ _

Premises used: EuclideanGeometry.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 q : P
mp : (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) = q → q ∈ s ∧ p -ᵥ q ∈ s.directionᗮ
mpr : q ∈ s ∧ p -ᵥ q ∈ s.directionᗮ → (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) = q
⊢ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) = q ↔ q ∈ s ∧ p -ᵥ q ∈ s.directionᗮ

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 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p : P
⊢ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) ∈ s ∧
    p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) ∈ s.directionᗮ

Tactic:
⟨orthogonalProjection_mem _, vsub_orthogonalProjection_mem_direction_orthogonal _ _⟩

Premises used: EuclideanGeometry.vsub_orthogonalProjection_mem_direction_orthogonal, EuclideanGeometry.orthogonalProjection_mem, 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 : P
⊢ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) ∈ s ∧
    p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) ∈ s.directionᗮ

Tactic:
exact ⟨orthogonalProjection_mem _, 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 q : P
hqs : q ∈ s
hpq : p -ᵥ q ∈ s.directionᗮ
rwa : q -ᵥ p ∈ s.directionᗮ
rwa₁ : -(q -ᵥ p) ∈ s.directionᗮ
rwa₂ rwa₃ rwa₄ rwa₅ : p -ᵥ q ∈ s.directionᗮ
⊢ Membership.mem (γ := AffineSubspace 𝕜 P) (mk' p s.directionᗮ) q

Tactic:
rwa [mem_mk', ← neg_mem_iff, neg_vsub_eq_vsub_rev]

Premises used: neg_mem_iff, neg_vsub_eq_vsub_rev, AffineSubspace.mem_mk'
-- 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ᗮ
⊢ Membership.mem (γ := AffineSubspace 𝕜 P) (mk' p s.directionᗮ) q

Tactic:
have hq : q ∈ mk' p s.directionᗮ := by
      rwa [mem_mk', ← neg_mem_iff, neg_vsub_eq_vsub_rev]
-- 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
this : Membership.mem (γ := Set P) {(↑((orthogonalProjection s : (a : P) → ↥s) p) : P)} q
⊢ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) = q

Tactic:
simpa [eq_comm] using this

Premises used: eq_comm