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
x : (↑(↑s : Set P) : Type u_3)
simp_rw :
  dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) *
      dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) ≤
    dist (↑x : P) (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) *
        dist (↑x : 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)
⊢ HPow.hPow (β := ℕ) (dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) 2 ≤
    HPow.hPow (β := ℕ) (dist (↑x : P) p) 2

Tactic:
simp_rw [pow_two,
    dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq p x.property]

Premises used: pow_two, EuclideanGeometry.dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq, 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
x : (↑(↑s : Set P) : Type u_3)
⊢ dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) *
      dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) ≤
    dist (↑x : P) (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) *
        dist (↑x : 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:
simp [mul_self_nonneg]

Premises used: mul_self_nonneg
-- 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 : (↑(nndist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) : ℝ) = (↑(Metric.infNndist p (↑s : Set P)) : ℝ)
⊢ nndist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) = Metric.infNndist p (↑s : Set P)

Tactic:
rw [← NNReal.coe_inj]

Premises used: NNReal.coe_inj
-- 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
⊢ (↑(nndist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) : ℝ) = (↑(Metric.infNndist p (↑s : Set P)) : ℝ)

Tactic:
simp [dist_orthogonalProjection_eq_infDist]

Premises used: EuclideanGeometry.dist_orthogonalProjection_eq_infDist
-- 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
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
r₁ r₂ : 𝕜
v : V
hv : v ∈ s.directionᗮ
rw :
  ‖(r₁ • v +ᵥ p₁) -ᵥ (r₂ • v +ᵥ p₂)‖ * ‖(r₁ • v +ᵥ p₁) -ᵥ (r₂ • v +ᵥ p₂)‖ =
    ‖p₁ -ᵥ p₂ + (r₁ - r₂) • v‖ * ‖p₁ -ᵥ p₂ + (r₁ - r₂) • v‖
rw₁ :
  ‖(r₁ • v +ᵥ p₁) -ᵥ p₂ - r₂ • v‖ * ‖(r₁ • v +ᵥ p₁) -ᵥ p₂ - r₂ • v‖ =
    ‖p₁ -ᵥ p₂ + (r₁ - r₂) • v‖ * ‖p₁ -ᵥ p₂ + (r₁ - r₂) • v‖
rw₂ :
  ‖r₁ • v + (p₁ -ᵥ p₂) - r₂ • v‖ * ‖r₁ • v + (p₁ -ᵥ p₂) - r₂ • v‖ =
    ‖p₁ -ᵥ p₂ + (r₁ - r₂) • v‖ * ‖p₁ -ᵥ p₂ + (r₁ - r₂) • v‖
rw₃ :
  ‖r₁ • v + (p₁ -ᵥ p₂) - r₂ • v‖ * ‖r₁ • v + (p₁ -ᵥ p₂) - r₂ • v‖ =
    ‖p₁ -ᵥ p₂ + (r₁ • v - r₂ • v)‖ * ‖p₁ -ᵥ p₂ + (r₁ • v - r₂ • v)‖
rw₄ :
  ‖p₁ -ᵥ p₂ + r₁ • v - r₂ • v‖ * ‖p₁ -ᵥ p₂ + r₁ • v - r₂ • v‖ =
    ‖p₁ -ᵥ p₂ + (r₁ • v - r₂ • v)‖ * ‖p₁ -ᵥ p₂ + (r₁ • v - r₂ • v)‖
rw₅ rw₆ :
  ‖p₁ -ᵥ p₂ + (r₁ • v - r₂ • v)‖ * ‖p₁ -ᵥ p₂ + (r₁ • v - r₂ • v)‖ =
    ‖p₁ -ᵥ p₂ + (r₁ • v - r₂ • v)‖ * ‖p₁ -ᵥ p₂ + (r₁ • v - r₂ • v)‖
⊢ dist (r₁ • v +ᵥ p₁) (r₂ • v +ᵥ p₂) * dist (r₁ • v +ᵥ p₁) (r₂ • v +ᵥ p₂) =
    ‖p₁ -ᵥ p₂ + (r₁ - r₂) • v‖ * ‖p₁ -ᵥ p₂ + (r₁ - r₂) • v‖

Tactic:
rw [dist_eq_norm_vsub V (r₁ • v +ᵥ p₁), vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, sub_smul,
        add_comm, add_sub_assoc]

Premises used: add_sub_assoc, vadd_vsub_assoc, vsub_vadd_eq_vsub_sub, sub_smul, add_comm, HVAdd.hVAdd, HSMul.hSMul, dist_eq_norm_vsub
-- 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
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
r₁ r₂ : 𝕜
v : V
hv : v ∈ s.directionᗮ
rw :
  ‖p₁ -ᵥ p₂‖ * ‖p₁ -ᵥ p₂‖ + ‖r₁ - r₂‖ * ‖v‖ * (‖r₁ - r₂‖ * ‖v‖) =
    ‖p₁ -ᵥ p₂‖ * ‖p₁ -ᵥ p₂‖ + ‖r₁ - r₂‖ * ‖r₁ - r₂‖ * (‖v‖ * ‖v‖)
⊢ ‖p₁ -ᵥ p₂‖ * ‖p₁ -ᵥ p₂‖ + ‖(r₁ - r₂) • v‖ * ‖(r₁ - r₂) • v‖ =
    dist p₁ p₂ * dist p₁ p₂ + ‖r₁ - r₂‖ * ‖r₁ - r₂‖ * (‖v‖ * ‖v‖)

Tactic:
rw [norm_smul, dist_eq_norm_vsub V p₁]

Premises used: norm_smul, dist_eq_norm_vsub
-- 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
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
r₁ r₂ : 𝕜
v : V
hv : v ∈ s.directionᗮ
⊢ ‖p₁ -ᵥ p₂‖ * ‖p₁ -ᵥ p₂‖ + ‖r₁ - r₂‖ * ‖v‖ * (‖r₁ - r₂‖ * ‖v‖) =
    ‖p₁ -ᵥ p₂‖ * ‖p₁ -ᵥ p₂‖ + ‖r₁ - r₂‖ * ‖r₁ - r₂‖ * (‖v‖ * ‖v‖)

Tactic:
ring
-- 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₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
rw :
  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) =
      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) ↔
    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)
⊢ dist p₁ p₃ = dist p₂ p₃ ↔
    dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₃) : P) =
      dist p₂ (↑((orthogonalProjection s : (a : P) → ↥s) p₃) : P)

Tactic:
rw [← mul_self_inj_of_nonneg dist_nonneg dist_nonneg, ←
    mul_self_inj_of_nonneg dist_nonneg dist_nonneg,
    dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq p₃ hp₁,
    dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq p₃ hp₂]

Premises used: mul_self_inj_of_nonneg, dist_nonneg, EuclideanGeometry.dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq
-- 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₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
⊢ 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) =
      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) ↔
    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:
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
ps : Set P
hps : ps ⊆ (↑s : Set P)
p : P
⊢ (ps.Pairwise fun (p₁ p₂ : P) ↦ dist p₁ p = dist p₂ p) ↔
    ps.Pairwise fun (p₁ p₂ : P) ↦
      dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) =
        dist p₂ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)

Tactic:
⟨fun h _ hp₁ _ hp₂ hne =>
    (dist_eq_iff_dist_orthogonalProjection_eq p (hps hp₁) (hps hp₂)).1 (h hp₁ hp₂ hne),
    fun h _ hp₁ _ hp₂ hne =>
    (dist_eq_iff_dist_orthogonalProjection_eq p (hps hp₁) (hps hp₂)).2 (h hp₁ hp₂ hne)⟩

Premises used: Iff.mpr, EuclideanGeometry.dist_eq_iff_dist_orthogonalProjection_eq, Iff.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 : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
ps : Set P
hps : ps ⊆ (↑s : Set P)
p : P
⊢ (ps.Pairwise fun (p₁ p₂ : P) ↦ dist p₁ p = dist p₂ p) ↔
    ps.Pairwise fun (p₁ p₂ : P) ↦
      dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) =
        dist p₂ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)

Tactic:
have h := dist_set_eq_iff_dist_orthogonalProjection_eq hps 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
ps : Set P
hps : ps ⊆ (↑s : Set P)
p : P
h :
  (ps.Pairwise fun (p₁ p₂ : P) ↦ dist p₁ p = dist p₂ p) ↔
    ps.Pairwise fun (p₁ p₂ : P) ↦
      dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) =
        dist p₂ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
⊢ (∃ (z : ℝ), ∀ x ∈ ps, dist x p = z) ↔
    ∃ (z : ℝ), ∀ x ∈ ps, dist x (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) = z

Tactic:
simp_rw [Set.pairwise_eq_iff_exists_eq] at h

Premises used: Set.pairwise_eq_iff_exists_eq
-- 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
ps : Set P
hps : ps ⊆ (↑s : Set P)
p : P
h :
  (∃ (z : ℝ), ∀ x ∈ ps, dist x p = z) ↔
    ∃ (z : ℝ), ∀ x ∈ ps, dist x (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) = z
⊢ (∃ (r : ℝ), ∀ p₁ ∈ ps, dist p₁ p = r) ↔
    ∃ (r : ℝ), ∀ p₁ ∈ ps, dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) = r

Tactic:
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
ps : Set P
hps : ps ⊆ (↑s : Set P)
p : P
h :
  (∃ (z : ℝ), ∀ x ∈ ps, dist x p = z) ↔
    ∃ (z : ℝ), ∀ x ∈ ps, dist x (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) = z
⊢ (∃ (r : ℝ), ∀ p₁ ∈ ps, dist p₁ p = r) ↔
    ∃ (r : ℝ), ∀ p₁ ∈ ps, dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) = r

Tactic:
exact 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
⊢ (reflection s : (a : P) → P) p =
    HVAdd.hVAdd (α := V) (β := P) ((s.direction.reflection : (a : V) → V) (p -ᵥ (↑(Classical.arbitrary ↥s) : P)) : V)
      (↑(Classical.arbitrary ↥s) : P)

Tactic:
rfl

Premises used: 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 x : P
hx : x ∈ s
rw : (↑(Classical.arbitrary ↥s) : P) -ᵥ x ∈ s.direction
⊢ (reflection s : (a : P) → P) p = HVAdd.hVAdd (α := V) ((s.direction.reflection : (a : V) → V) (p -ᵥ x) : V) x

Tactic:
rw [reflection_apply, vadd_eq_vadd_iff_sub_eq_vsub, ← map_sub,
    vsub_sub_vsub_cancel_left, s.direction.reflection_eq_self_iff]

Premises used: map_sub, vadd_eq_vadd_iff_sub_eq_vsub, vsub_sub_vsub_cancel_left, Submodule.reflection_eq_self_iff, 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
rw :
  HVAdd.hVAdd (α := V) (β := P) ((s.direction.reflection : (a : V) → V) (p -ᵥ (↑(Classical.arbitrary ↥s) : P)) : V)
      (↑(Classical.arbitrary ↥s) : P) =
    (HVAdd.hVAdd (α := V) (β := P)
          ((s.direction.starProjection : (a : V) → V) (p -ᵥ (↑(Classical.arbitrary ↥s) : P)) : V)
          (↑(Classical.arbitrary ↥s) : P) -ᵥ
        p) +ᵥ
      HVAdd.hVAdd (α := V) (β := P)
        ((s.direction.starProjection : (a : V) → V) (p -ᵥ (↑(Classical.arbitrary ↥s) : P)) : V)
        (↑(Classical.arbitrary ↥s) : P)
⊢ (reflection s : (a : P) → P) p =
    HVAdd.hVAdd (β := P) ((↑((orthogonalProjection s : (a : P) → ↥s) p) : P) -ᵥ p)
      (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)

Tactic:
rw [reflection_apply, orthogonalProjection_apply', Submodule.coe_orthogonalProjection_apply]

Premises used: EuclideanGeometry.orthogonalProjection_apply', Submodule.coe_orthogonalProjection_apply, 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
set :
  let x : P := (↑(Classical.arbitrary ↥s) : P);
  HVAdd.hVAdd (α := V) ((s.direction.reflection : (a : V) → V) (p -ᵥ x) : V) x =
    (HVAdd.hVAdd (α := V) ((s.direction.starProjection : (a : V) → V) (p -ᵥ x) : V) x -ᵥ p) +ᵥ
      HVAdd.hVAdd (α := V) ((s.direction.starProjection : (a : V) → V) (p -ᵥ x) : V) x
⊢ HVAdd.hVAdd (α := V) (β := P) ((s.direction.reflection : (a : V) → V) (p -ᵥ (↑(Classical.arbitrary ↥s) : P)) : V)
      (↑(Classical.arbitrary ↥s) : P) =
    (HVAdd.hVAdd (α := V) (β := P)
          ((s.direction.starProjection : (a : V) → V) (p -ᵥ (↑(Classical.arbitrary ↥s) : P)) : V)
          (↑(Classical.arbitrary ↥s) : P) -ᵥ
        p) +ᵥ
      HVAdd.hVAdd (α := V) (β := P)
        ((s.direction.starProjection : (a : V) → V) (p -ᵥ (↑(Classical.arbitrary ↥s) : P)) : V)
        (↑(Classical.arbitrary ↥s) : P)

Tactic:
set x : P := ↑(Classical.arbitrary s)

Premises used: Membership.mem, Subtype, Classical.arbitrary
-- 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 : P := (↑(Classical.arbitrary ↥s) : P)
set :
  let v : V := (s.direction.starProjection : (a : V) → V) (p -ᵥ x);
  HVAdd.hVAdd (α := V) ((s.direction.reflection : (a : V) → V) (p -ᵥ x) : V) x = ((v +ᵥ x) -ᵥ p) +ᵥ v +ᵥ x
⊢ HVAdd.hVAdd (α := V) ((s.direction.reflection : (a : V) → V) (p -ᵥ x) : V) x =
    (HVAdd.hVAdd (α := V) ((s.direction.starProjection : (a : V) → V) (p -ᵥ x) : V) x -ᵥ p) +ᵥ
      HVAdd.hVAdd (α := V) ((s.direction.starProjection : (a : V) → V) (p -ᵥ x) : V) x

Tactic:
set v : V := s.direction.starProjection (p -ᵥ x)

Premises used: Submodule.starProjection, VSub.vsub, DFunLike.coe, 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
x : P := (↑(Classical.arbitrary ↥s) : P)
v : V := (s.direction.starProjection : (a : V) → V) (p -ᵥ x)
rw :
  (HSMul.hSMul (α := ℕ) (β := V) 2 ((s.direction.starProjection : (a : V) → V) (p -ᵥ x) : V) - (p -ᵥ x)) +ᵥ x =
    ((v +ᵥ x) -ᵥ p) +ᵥ v +ᵥ x
rw₁ :
  (HAdd.hAdd (α := V) (β := V) ((s.direction.starProjection : (a : V) → V) (p -ᵥ x) : V)
          ((s.direction.starProjection : (a : V) → V) (p -ᵥ x) : V) -
        (p -ᵥ x)) +ᵥ
      x =
    ((v +ᵥ x) -ᵥ p) +ᵥ v +ᵥ x
rw₂ :
  (HAdd.hAdd (α := V) (β := V) ((s.direction.starProjection : (a : V) → V) (p -ᵥ x) : V)
          ((s.direction.starProjection : (a : V) → V) (p -ᵥ x) : V) +
        -(p -ᵥ x)) +ᵥ
      x =
    ((v +ᵥ x) -ᵥ p) +ᵥ v +ᵥ x
rw₃ :
  (HAdd.hAdd (α := V) (β := V) ((s.direction.starProjection : (a : V) → V) (p -ᵥ x) : V)
          ((s.direction.starProjection : (a : V) → V) (p -ᵥ x) : V) +
        (x -ᵥ p)) +ᵥ
      x =
    ((v +ᵥ x) -ᵥ p) +ᵥ v +ᵥ x
rw₄ :
  HAdd.hAdd (α := V) ((s.direction.starProjection : (a : V) → V) (p -ᵥ x) : V)
        (HAdd.hAdd (α := V) ((s.direction.starProjection : (a : V) → V) (p -ᵥ x) : V) (x -ᵥ p)) +ᵥ
      x =
    ((v +ᵥ x) -ᵥ p) +ᵥ v +ᵥ x
rw₅ :
  (HAdd.hAdd (α := V) ((s.direction.starProjection : (a : V) → V) (p -ᵥ x) : V) (x -ᵥ p) + v) +ᵥ x =
    ((v +ᵥ x) -ᵥ p) +ᵥ v +ᵥ x
rw₆ :
  HAdd.hAdd (α := V) ((s.direction.starProjection : (a : V) → V) (p -ᵥ x) : V) (x -ᵥ p) +ᵥ v +ᵥ x =
    ((v +ᵥ x) -ᵥ p) +ᵥ v +ᵥ x
rw₇ rw₈ :
  HAdd.hAdd (α := V) ((s.direction.starProjection : (a : V) → V) (p -ᵥ x) : V) (x -ᵥ p) +ᵥ v +ᵥ x =
    (v + (x -ᵥ p)) +ᵥ v +ᵥ x
⊢ HVAdd.hVAdd (α := V) ((s.direction.reflection : (a : V) → V) (p -ᵥ x) : V) x = ((v +ᵥ x) -ᵥ p) +ᵥ v +ᵥ x

Tactic:
rw [Submodule.reflection_apply, two_smul, sub_eq_add_neg, neg_vsub_eq_vsub_rev, add_assoc,
    add_comm v, add_vadd, vadd_vsub_assoc]

Premises used: vadd_vsub_assoc, Submodule.reflection_apply, add_assoc, AddSemigroupAction.add_vadd, sub_eq_add_neg, two_smul, add_comm, 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 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 (α := P) ((reflection s : (a : P) → P) p : P) ((reflection s : (a : P) → P) p : P)
⊢ Eq (α := P) ((reflection s : (a : P) → P) p : P) ((reflection s' : (a : P) → P) 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 (α := P) ((reflection s : (a : P) → P) p : P) ((reflection s : (a : P) → P) 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
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p : P
⊢ (reflection s : (a : P) → P) ((reflection s : (a : P) → P) p : P) = p

Tactic:
simp [reflection, -AffineIsometryEquiv.map_vadd]

Premises used: EuclideanGeometry.reflection, AffineIsometryEquiv.map_vadd
-- 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
h : ∀ (x : P), Eq (α := P) (((reflection s).symm : (a : P) → P) x : P) ((reflection s : (a : P) → P) x : P)
⊢ (reflection s).symm = reflection s

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
x : P
h :
  Eq (α := P) ((reflection s : (a : P) → P) (((reflection s).symm : (a : P) → P) x : P) : P)
    ((reflection s : (a : P) → P) ((reflection s : (a : P) → P) x : P) : P)
⊢ Eq (α := P) (((reflection s).symm : (a : P) → P) x : P) ((reflection s : (a : P) → P) x : P)

Tactic:
rw [← (reflection s).injective.eq_iff]

Premises used: Function.Injective.eq_iff, EuclideanGeometry.reflection, AffineIsometryEquiv.injective
-- 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
x : P
⊢ Eq (α := P) ((reflection s : (a : P) → P) (((reflection s).symm : (a : P) → P) x : P) : P)
    ((reflection s : (a : P) → P) ((reflection s : (a : P) → P) x : P) : 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
⊢ Function.Involutive.{u_3 + 1} (α := P) (⇑(reflection s) : (a : P) → P)

Tactic:
reflection_reflection s

Premises used: EuclideanGeometry.reflection_reflection, Function.Involutive