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 : P
rw : (∃ p₂ ∈ s, p -ᵥ (↑(Classical.arbitrary ↥s) : P) = p₂ -ᵥ (↑(Classical.arbitrary ↥s) : P)) ↔ p ∈ s
⊢ (reflection s : (a : P) → P) p = p ↔ p ∈ s

Tactic:
rw [reflection_apply, Eq.comm, eq_vadd_iff_vsub_eq, Eq.comm, s.direction.reflection_eq_self_iff,
    s.mem_direction_iff_eq_vsub_right (SetLike.coe_mem (Classical.arbitrary s))]

Premises used: SetLike.coe_mem, Membership.mem, Subtype, Submodule.reflection_eq_self_iff, Classical.arbitrary, Eq.comm, AffineSubspace.mem_direction_iff_eq_vsub_right, eq_vadd_iff_vsub_eq, EuclideanGeometry.reflection_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₂ ∈ s, p -ᵥ (↑(Classical.arbitrary ↥s) : P) = p₂ -ᵥ (↑(Classical.arbitrary ↥s) : P)) ↔ p ∈ s

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
rw :
  HVAdd.hVAdd (β := P) ((↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) -ᵥ p)
        (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      HVAdd.hVAdd (β := P) ((↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : 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)
⊢ Eq (α := P) ((reflection s₁ : (a : P) → P) p : P) ((reflection s₂ : (a : P) → P) p : P) ↔
    Eq.{u_3 + 1} (α := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
      (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)

Tactic:
rw [reflection_apply', reflection_apply']

Premises used: EuclideanGeometry.reflection_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₁ 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
mp :
  HVAdd.hVAdd (β := P) ((↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) -ᵥ p)
        (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      HVAdd.hVAdd (β := P) ((↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : 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)
mpr :
  Eq.{u_3 + 1} (α := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
      (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) →
    HVAdd.hVAdd (β := P) ((↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) -ᵥ p)
        (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      HVAdd.hVAdd (β := P) ((↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) -ᵥ p)
        (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
⊢ HVAdd.hVAdd (β := P) ((↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) -ᵥ p)
        (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      HVAdd.hVAdd (β := P) ((↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : 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:
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₁ 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 :
  HVAdd.hVAdd (β := P) ((↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) -ᵥ p)
      (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
    HVAdd.hVAdd (β := P) ((↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) -ᵥ p)
      (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
⊢ Eq.{u_1 + 1} (α := 𝕜) 2 0 ∨
    VSub.vsub.{u_2, u_3} (P := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
        (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) =
      0

Tactic:
rw [← @vsub_eq_zero_iff_eq V, vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, add_comm, add_sub_assoc,
      vsub_sub_vsub_cancel_right, ←
      two_smul 𝕜 ((orthogonalProjection s₁ p : P) -ᵥ orthogonalProjection s₂ p), smul_eq_zero] at h

Premises used: add_sub_assoc, vadd_vsub_assoc, vsub_vadd_eq_vsub_sub, vsub_eq_zero_iff_eq, two_smul, add_comm, VSub.vsub, vsub_sub_vsub_cancel_right, EuclideanGeometry.orthogonalProjection, Subtype.val, DFunLike.coe, smul_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₁ 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_1 + 1} (α := 𝕜) 2 0 ∨
    VSub.vsub.{u_2, u_3} (P := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
        (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) =
      0
⊢ Eq.{u_3 + 1} (α := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
    (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)

Tactic:
simpa using 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₁ 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)
mpr mpr₁ :
  HVAdd.hVAdd (β := P) ((↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) -ᵥ p)
      (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) =
    HVAdd.hVAdd (β := P) ((↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) -ᵥ p)
      (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
⊢ HVAdd.hVAdd (β := P) ((↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) -ᵥ p)
      (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
    HVAdd.hVAdd (β := P) ((↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) -ᵥ p)
      (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)

Tactic:
rw [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₂ : P
rw :
  dist (α := P) ((reflection s : (a : P) → P) ((reflection s : (a : P) → P) p₁ : P) : P)
    ((reflection s : (a : P) → P) p₂ : P)
| dist p₁ ((reflection s : (a : P) → P) p₂)

Tactic:
rw [← reflection_reflection s p₁]

Premises used: EuclideanGeometry.reflection_reflection
-- 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
conv_lhs :
  dist (α := P) ((reflection s : (a : P) → P) ((reflection s : (a : P) → P) p₁ : P) : P)
      ((reflection s : (a : P) → P) p₂ : P) =
    dist ((reflection s : (a : P) → P) p₁) p₂
⊢ dist p₁ ((reflection s : (a : P) → P) p₂) = dist ((reflection s : (a : P) → P) p₁) p₂

Tactic:
conv_lhs => rw [← reflection_reflection s p₁]

Premises used: EuclideanGeometry.reflection_reflection
-- 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
⊢ dist (α := P) ((reflection s : (a : P) → P) ((reflection s : (a : P) → P) p₁ : P) : P)
      ((reflection s : (a : P) → P) p₂ : P) =
    dist ((reflection s : (a : P) → P) p₁) p₂

Tactic:
(reflection s).dist_map _ _

Premises used: EuclideanGeometry.reflection, AffineIsometryEquiv.dist_map
-- 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
⊢ dist (α := P) ((reflection s : (a : P) → P) ((reflection s : (a : P) → P) p₁ : P) : P)
      ((reflection s : (a : P) → P) p₂ : P) =
    dist ((reflection s : (a : P) → P) p₁) p₂

Tactic:
exact (reflection s).dist_map _ _

Premises used: EuclideanGeometry.reflection, AffineIsometryEquiv.dist_map
-- 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
p₂ : P
rw : ∀ (hp₁ : (reflection s : (a : P) → P) p₁ = p₁) (p₂ : P), dist p₁ ((reflection s : (a : P) → P) p₂) = dist p₁ p₂
⊢ dist p₁ ((reflection s : (a : P) → P) p₂) = dist p₁ p₂

Tactic:
rw [← reflection_eq_self_iff p₁] at hp₁

Premises used: EuclideanGeometry.reflection_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₁ : (reflection s : (a : P) → P) p₁ = p₁
p₂ : P
⊢ dist (α := P) ((reflection s : (a : P) → P) p₁ : P) ((reflection s : (a : P) → P) p₂ : P) = dist p₁ p₂

Tactic:
(reflection s).dist_map p₁ p₂

Premises used: EuclideanGeometry.reflection, AffineIsometryEquiv.dist_map
-- 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₁ : (reflection s : (a : P) → P) p₁ = p₁
p₂ : P
h : p₁ = (reflection s : (a : P) → P) p₁
⊢ dist p₁ ((reflection s : (a : P) → P) p₂) = dist p₁ p₂

Tactic:
convert! (reflection s).dist_map p₁ p₂

Premises used: EuclideanGeometry.reflection, AffineIsometryEquiv.dist_map
-- 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₁ : (reflection s : (a : P) → P) p₁ = p₁
p₂ : P
h h₁ : p₁ = p₁
⊢ p₁ = (reflection s : (a : P) → P) p₁

Tactic:
rw [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₁ s₂ : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s₁
inst_6 : s₁.direction.HasOrthogonalProjection
hle : s₁ ≤ s₂
p : P
hp : p ∈ s₂
rw :
  HVAdd.hVAdd (β := P) ((↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) -ᵥ p)
      (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ∈
    s₂
⊢ Membership.mem (α := P) s₂ ((reflection s₁ : (a : P) → P) p : P)

Tactic:
rw [reflection_apply']

Premises used: EuclideanGeometry.reflection_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₁ s₂ : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s₁
inst_6 : s₁.direction.HasOrthogonalProjection
hle : s₁ ≤ s₂
p : P
hp : p ∈ s₂
⊢ (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ∈ s₂

Tactic:
have ho : ↑(orthogonalProjection s₁ p) ∈ s₂ := hle (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₁ s₂ : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s₁
inst_6 : s₁.direction.HasOrthogonalProjection
hle : s₁ ≤ s₂
p : P
hp : p ∈ s₂
ho : (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ∈ s₂
⊢ HVAdd.hVAdd (β := P) ((↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) -ᵥ p)
      (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ∈
    s₂

Tactic:
vadd_mem_of_mem_direction (vsub_mem_direction ho hp) ho

Premises used: Set.Mem, AffineSubspace.vsub_mem_direction, AffineSubspace.vadd_mem_of_mem_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₁ s₂ : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s₁
inst_6 : s₁.direction.HasOrthogonalProjection
hle : s₁ ≤ s₂
p : P
hp : p ∈ s₂
ho : (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ∈ s₂
⊢ HVAdd.hVAdd (β := P) ((↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) -ᵥ p)
      (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ∈
    s₂

Tactic:
exact vadd_mem_of_mem_direction (vsub_mem_direction ho hp) ho

Premises used: AffineSubspace.vsub_mem_direction, AffineSubspace.vadd_mem_of_mem_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
hp : p ∈ s
v : V
hv : v ∈ s.directionᗮ
rw :
  ((↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp) : P) -ᵥ p - v) +ᵥ
      (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp) : P) =
    -v +ᵥ p
⊢ (reflection s : (a : P) → P) (v +ᵥ p) = -v +ᵥ p

Tactic:
rw [reflection_apply', orthogonalProjection_vadd_eq_self hp hv, vsub_vadd_eq_vsub_sub]

Premises used: vsub_vadd_eq_vsub_sub, EuclideanGeometry.orthogonalProjection_vadd_eq_self, EuclideanGeometry.reflection_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
hp : p ∈ s
v : V
hv : v ∈ s.directionᗮ
⊢ ((↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp) : P) -ᵥ p - v) +ᵥ
      (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp) : P) =
    -v +ᵥ p

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₂ : P
r : 𝕜
hp₁ : p₁ ∈ s
⊢ (reflection s : (a : P) → P) (r • (p₂ -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p₂) : P)) +ᵥ p₁) =
    -(r • (p₂ -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p₂) : P))) +ᵥ p₁

Tactic:
reflection_orthogonal_vadd hp₁
    (Submodule.smul_mem _ _ (vsub_orthogonalProjection_mem_direction_orthogonal s _))

Premises used: EuclideanGeometry.vsub_orthogonalProjection_mem_direction_orthogonal, EuclideanGeometry.reflection_orthogonal_vadd, 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
V₂ : Type u_4
P₂ : Type u_5
inst_3 : NormedAddCommGroup V₂
inst_4 : InnerProductSpace 𝕜 V₂
inst_5 : MetricSpace P
inst_6 : NormedAddTorsor V P
inst_7 : MetricSpace P₂
inst_8 : NormedAddTorsor V₂ P₂
s : AffineSubspace 𝕜 P
inst_9 : Nonempty.{u_3 + 1} ↥s
inst_10 : s.direction.HasOrthogonalProjection
f : P →ᵃⁱ[𝕜] P₂
inst_11 : (map f.toAffineMap s).direction.HasOrthogonalProjection
p : P
rw :
  Membership.mem (α := P₂) (map f.toAffineMap s)
      ((f : (a : P) → P₂) (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) : P₂) ∧
    VSub.vsub.{u_4, u_5} (P := P₂) ((f : (a : P) → P₂) p : P₂)
        ((f : (a : P) → P₂) (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) : P₂) ∈
      (map f.toAffineMap s).directionᗮ
⊢ Eq.{u_5 + 1} (α := P₂)
    ((↑((orthogonalProjection (map f.toAffineMap s) : (a : P₂) → ↥(map f.toAffineMap s)) ((f : (a : P) → P₂) p)) : P₂) :
      P₂)
    ((f : (a : P) → P₂) (↑((orthogonalProjection s : (a : P) → ↥s) p) : 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
V₂ : Type u_4
P₂ : Type u_5
inst_3 : NormedAddCommGroup V₂
inst_4 : InnerProductSpace 𝕜 V₂
inst_5 : MetricSpace P
inst_6 : NormedAddTorsor V P
inst_7 : MetricSpace P₂
inst_8 : NormedAddTorsor V₂ P₂
s : AffineSubspace 𝕜 P
inst_9 : Nonempty.{u_3 + 1} ↥s
inst_10 : s.direction.HasOrthogonalProjection
f : P →ᵃⁱ[𝕜] P₂
inst_11 : (map f.toAffineMap s).direction.HasOrthogonalProjection
p : P
simp :
  VSub.vsub.{u_4, u_5} (P := P₂) ((f : (a : P) → P₂) p : P₂)
      ((f : (a : P) → P₂) (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) : P₂) ∈
    (Submodule.map f.linearIsometry.toLinearMap s.direction)ᗮ
⊢ Membership.mem (α := P₂) (map f.toAffineMap s)
      ((f : (a : P) → P₂) (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) : P₂) ∧
    VSub.vsub.{u_4, u_5} (P := P₂) ((f : (a : P) → P₂) p : P₂)
        ((f : (a : P) → P₂) (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) : P₂) ∈
      (map f.toAffineMap s).directionᗮ

Tactic:
simp only [mem_map, AffineIsometry.coe_toAffineMap, AffineIsometry.map_eq_iff, exists_eq_right,
    SetLike.coe_mem, map_direction, AffineIsometry.linear_eq_linearIsometry, true_and]

Premises used: SetLike.coe_mem, AffineIsometry.linear_eq_linearIsometry, exists_eq_right, AffineIsometry.coe_toAffineMap, AffineSubspace.mem_map, AffineIsometry.map_eq_iff, AffineSubspace.map_direction, true_and
-- 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
V₂ : Type u_4
P₂ : Type u_5
inst_3 : NormedAddCommGroup V₂
inst_4 : InnerProductSpace 𝕜 V₂
inst_5 : MetricSpace P
inst_6 : NormedAddTorsor V P
inst_7 : MetricSpace P₂
inst_8 : NormedAddTorsor V₂ P₂
s : AffineSubspace 𝕜 P
inst_9 : Nonempty.{u_3 + 1} ↥s
inst_10 : s.direction.HasOrthogonalProjection
f : P →ᵃⁱ[𝕜] P₂
inst_11 : (map f.toAffineMap s).direction.HasOrthogonalProjection
p : P
rw :
  ∀ u ∈ Submodule.map f.linearIsometry.toLinearMap s.direction,
    inner 𝕜 u ((f.linear : (a : V) → V₂) (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P))) = 0
⊢ VSub.vsub.{u_4, u_5} (P := P₂) ((f : (a : P) → P₂) p : P₂)
      ((f : (a : P) → P₂) (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) : P₂) ∈
    (Submodule.map f.linearIsometry.toLinearMap s.direction)ᗮ

Tactic:
rw [← AffineIsometry.coe_toAffineMap, ← AffineMap.linearMap_vsub, Submodule.mem_orthogonal]

Premises used: AffineMap.linearMap_vsub, AffineIsometry.coe_toAffineMap, Submodule.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
V₂ : Type u_4
P₂ : Type u_5
inst_3 : NormedAddCommGroup V₂
inst_4 : InnerProductSpace 𝕜 V₂
inst_5 : MetricSpace P
inst_6 : NormedAddTorsor V P
inst_7 : MetricSpace P₂
inst_8 : NormedAddTorsor V₂ P₂
s : AffineSubspace 𝕜 P
inst_9 : Nonempty.{u_3 + 1} ↥s
inst_10 : s.direction.HasOrthogonalProjection
f : P →ᵃⁱ[𝕜] P₂
inst_11 : (map f.toAffineMap s).direction.HasOrthogonalProjection
p : P
u : V₂
hu : u ∈ Submodule.map f.linearIsometry.toLinearMap s.direction
⊢ ∃ y ∈ s.direction, (f.linearIsometry.toLinearMap : (a : V) → V₂) y = u

Tactic:
rw [Submodule.mem_map] at hu

Premises used: Submodule.mem_map
-- 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
V₂ : Type u_4
P₂ : Type u_5
inst_3 : NormedAddCommGroup V₂
inst_4 : InnerProductSpace 𝕜 V₂
inst_5 : MetricSpace P
inst_6 : NormedAddTorsor V P
inst_7 : MetricSpace P₂
inst_8 : NormedAddTorsor V₂ P₂
s : AffineSubspace 𝕜 P
inst_9 : Nonempty.{u_3 + 1} ↥s
inst_10 : s.direction.HasOrthogonalProjection
f : P →ᵃⁱ[𝕜] P₂
inst_11 : (map f.toAffineMap s).direction.HasOrthogonalProjection
p : P
u : V₂
hu : ∃ y ∈ s.direction, (f.linearIsometry.toLinearMap : (a : V) → V₂) y = u
obtain :
  ∀ (v : V) (hv : v ∈ s.direction),
    inner.{u_1, u_4} 𝕜 (E := V₂) ((f.linearIsometry.toLinearMap : (a : V) → V₂) v : V₂)
        ((f.linear : (a : V) → V₂) (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) : V₂) =
      0
⊢ inner 𝕜 u ((f.linear : (a : V) → V₂) (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P))) = 0

Tactic:
obtain ⟨v, hv, rfl⟩ := hu

Premises used: rfl