awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
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‖
⊢ dist (r₁ • v +ᵥ p₁) (r₂ • v +ᵥ p₂) * dist (r₁ • v +ᵥ p₁) (r₂ • v +ᵥ p₂) =
    ‖p₁ -ᵥ p₂ + (r₁ - r₂) • v‖ * ‖p₁ -ᵥ p₂ + (r₁ - r₂) • v‖
have rw₁ : ‖(r₁ • v +ᵥ p₁) -ᵥ p₂ - r₂ • v‖ * ‖(r₁ • v +ᵥ p₁) -ᵥ p₂ - r₂ • v‖ =
  ‖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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
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‖
⊢ dist (r₁ • v +ᵥ p₁) (r₂ • v +ᵥ p₂) * dist (r₁ • v +ᵥ p₁) (r₂ • v +ᵥ p₂) =
    ‖p₁ -ᵥ p₂ + (r₁ - r₂) • v‖ * ‖p₁ -ᵥ p₂ + (r₁ - r₂) • v‖
have rw₂ : ‖r₁ • v + (p₁ -ᵥ p₂) - r₂ • v‖ * ‖r₁ • v + (p₁ -ᵥ p₂) - r₂ • v‖ =
  ‖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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
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‖
⊢ dist (r₁ • v +ᵥ p₁) (r₂ • v +ᵥ p₂) * dist (r₁ • v +ᵥ p₁) (r₂ • v +ᵥ p₂) =
    ‖p₁ -ᵥ p₂ + (r₁ - r₂) • v‖ * ‖p₁ -ᵥ p₂ + (r₁ - r₂) • v‖
have 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)‖
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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
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)‖
⊢ dist (r₁ • v +ᵥ p₁) (r₂ • v +ᵥ p₂) * dist (r₁ • v +ᵥ p₁) (r₂ • v +ᵥ p₂) =
    ‖p₁ -ᵥ p₂ + (r₁ - r₂) • v‖ * ‖p₁ -ᵥ p₂ + (r₁ - r₂) • v‖
have 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)‖
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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
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)‖
⊢ dist (r₁ • v +ᵥ p₁) (r₂ • v +ᵥ p₂) * dist (r₁ • v +ᵥ p₁) (r₂ • v +ᵥ p₂) =
    ‖p₁ -ᵥ p₂ + (r₁ - r₂) • v‖ * ‖p₁ -ᵥ p₂ + (r₁ - r₂) • v‖
have 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)‖
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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
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‖ =
    dist p₁ p₂ * dist p₁ p₂ + ‖r₁ - r₂‖ * ‖r₁ - r₂‖ * (‖v‖ * ‖v‖)
have rw : ‖p₁ -ᵥ p₂‖ * ‖p₁ -ᵥ p₂‖ + ‖r₁ - r₂‖ * ‖v‖ * (‖r₁ - r₂‖ * ‖v‖) =
  ‖p₁ -ᵥ p₂‖ * ‖p₁ -ᵥ p₂‖ + ‖r₁ - r₂‖ * ‖r₁ - r₂‖ * (‖v‖ * ‖v‖)
Tactic: rw [norm_smul, dist_eq_norm_vsub V p₁]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
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₁ p₃ = dist p₂ p₃ ↔
    dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₃) : P) =
      dist p₂ (↑((orthogonalProjection s : (a : P) → ↥s) p₃) : P)
have 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)
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₂]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (hypothesis)
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
⊢ (∃ (r : ℝ), ∀ p₁ ∈ ps, dist p₁ p = r) ↔
    ∃ (r : ℝ), ∀ p₁ ∈ ps, dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) = r
have 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)
Tactic: have h := dist_set_eq_iff_dist_orthogonalProjection_eq hps p
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
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
⊢ (reflection s : (a : P) → P) p = HVAdd.hVAdd (α := V) ((s.direction.reflection : (a : V) → V) (p -ᵥ x) : V) x
have rw : (↑(Classical.arbitrary ↥s) : P) -ᵥ x ∈ s.direction
Tactic: rw [reflection_apply, vadd_eq_vadd_iff_sub_eq_vsub, ← map_sub,
    vsub_sub_vsub_cancel_left, s.direction.reflection_eq_self_iff]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
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 (β := P) ((↑((orthogonalProjection s : (a : P) → ↥s) p) : P) -ᵥ p)
      (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
have 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)
Tactic: rw [reflection_apply, orthogonalProjection_apply', Submodule.coe_orthogonalProjection_apply]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
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)
⊢ HVAdd.hVAdd (α := V) ((s.direction.reflection : (a : V) → V) (p -ᵥ x) : V) x = ((v +ᵥ x) -ᵥ p) +ᵥ v +ᵥ x
have rw : (HSMul.hSMul (α := ℕ) (β := V) 2 ((s.direction.starProjection : (a : V) → V) (p -ᵥ x) : V) - (p -ᵥ x)) +ᵥ 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
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
⊢ HVAdd.hVAdd (α := V) ((s.direction.reflection : (a : V) → V) (p -ᵥ x) : V) x = ((v +ᵥ x) -ᵥ p) +ᵥ v +ᵥ x
have 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
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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
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
⊢ HVAdd.hVAdd (α := V) ((s.direction.reflection : (a : V) → V) (p -ᵥ x) : V) x = ((v +ᵥ x) -ᵥ p) +ᵥ v +ᵥ x
have 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
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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
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
⊢ HVAdd.hVAdd (α := V) ((s.direction.reflection : (a : V) → V) (p -ᵥ x) : V) x = ((v +ᵥ x) -ᵥ p) +ᵥ v +ᵥ x
have 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
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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
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
⊢ HVAdd.hVAdd (α := V) ((s.direction.reflection : (a : V) → V) (p -ᵥ x) : V) x = ((v +ᵥ x) -ᵥ p) +ᵥ v +ᵥ x
have 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
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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
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
⊢ HVAdd.hVAdd (α := V) ((s.direction.reflection : (a : V) → V) (p -ᵥ x) : V) x = ((v +ᵥ x) -ᵥ p) +ᵥ v +ᵥ x
have rw₅ : (HAdd.hAdd (α := V) ((s.direction.starProjection : (a : V) → V) (p -ᵥ x) : V) (x -ᵥ p) + 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
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
⊢ HVAdd.hVAdd (α := V) ((s.direction.reflection : (a : V) → V) (p -ᵥ x) : V) x = ((v +ᵥ x) -ᵥ p) +ᵥ v +ᵥ x
have rw₆ : HAdd.hAdd (α := V) ((s.direction.starProjection : (a : V) → V) (p -ᵥ x) : V) (x -ᵥ p) +ᵥ 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
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
⊢ HVAdd.hVAdd (α := V) ((s.direction.reflection : (a : V) → V) (p -ᵥ x) : V) x = ((v +ᵥ x) -ᵥ p) +ᵥ v +ᵥ x
have rw₇ : HAdd.hAdd (α := V) ((s.direction.starProjection : (a : V) → V) (p -ᵥ x) : V) (x -ᵥ p) +ᵥ 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
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
⊢ Eq (α := P) ((reflection s : (a : P) → P) p : P) ((reflection s' : (a : P) → P) p : P)
have 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)
Tactic: subst h
Cleared hypotheses: s', inst_6, inst_8, h