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
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
v : V
hv : v ∈ s.direction
rw :
  inner.{u_1, u_4} 𝕜 (E := V₂) ((f.linearIsometry.toLinearMap : (a : V) → V₂) v : V₂)
      ((f.linearIsometry.toLinearMap : (a : V) → V₂) (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) : V₂) =
    0
rw₁ :
  inner.{u_1, u_4} 𝕜 (E := V₂) ((f.linearIsometry : (a : V) → V₂) v : V₂)
      ((f.linearIsometry : (a : V) → V₂) (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) : V₂) =
    0
rw₂ : inner 𝕜 v (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) = 0
rw₃ rw₄ : Eq.{u_1 + 1} (α := 𝕜) 0 0
⊢ 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

Tactic:
rw [AffineIsometry.linear_eq_linearIsometry, LinearIsometry.coe_toLinearMap,
    LinearIsometry.inner_map_map, Submodule.inner_right_of_mem_orthogonal hv
      (vsub_orthogonalProjection_mem_direction_orthogonal _ _)]

Premises used: LinearIsometry.coe_toLinearMap, EuclideanGeometry.vsub_orthogonalProjection_mem_direction_orthogonal, LinearIsometry.inner_map_map, AffineIsometry.linear_eq_linearIsometry, Submodule.inner_right_of_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
s' : AffineSubspace 𝕜 ↥s
inst_6 : Nonempty.{u_3 + 1} ↥s'
inst_7 : Submodule.HasOrthogonalProjection.{u_1, u_2} (𝕜 := 𝕜) (E := ↥s.direction) s'.direction
inst_8 : (map s.subtype s').direction.HasOrthogonalProjection
p : ↥s
rw :
  Eq.{u_3 + 1} (α := P) (↑((orthogonalProjection (map s.subtype s') : (a : P) → ↥(map s.subtype s')) (↑p : P)) : P)
    (↑(↑(((orthogonalProjection.{u_1, u_2, u_3} (𝕜 := 𝕜) (P := ↥s) s' :
                  ContinuousAffineMap.{u_1, u_2, u_2, u_3, u_3} 𝕜 ↥s ↥s') :
                (a : ↥s) → ↥s')
              p) :
          ↥s) :
      P)
⊢ Eq.{u_3 + 1} (α := P)
    (↑(↑(((orthogonalProjection.{u_1, u_2, u_3} (𝕜 := 𝕜) (P := ↥s) s' :
                  ContinuousAffineMap.{u_1, u_2, u_2, u_3, u_3} 𝕜 ↥s ↥s') :
                (a : ↥s) → ↥s')
              p) :
          ↥s) :
      P)
    (↑((orthogonalProjection (map s.subtype s') : (a : P) → ↥(map s.subtype s')) (↑p : P)) : P)

Tactic:
rw [eq_comm]

Premises used: eq_comm
-- 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
s' : AffineSubspace 𝕜 ↥s
inst_6 : Nonempty.{u_3 + 1} ↥s'
inst_7 : Submodule.HasOrthogonalProjection.{u_1, u_2} (𝕜 := 𝕜) (E := ↥s.direction) s'.direction
inst_8 : (map s.subtype s').direction.HasOrthogonalProjection
p : ↥s
⊢ (map s.subtype s').direction.HasOrthogonalProjection

Tactic:
infer_instance
-- 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
s' : AffineSubspace 𝕜 ↥s
inst_6 : Nonempty.{u_3 + 1} ↥s'
inst_7 : Submodule.HasOrthogonalProjection.{u_1, u_2} (𝕜 := 𝕜) (E := ↥s.direction) s'.direction
inst_8 : (map s.subtype s').direction.HasOrthogonalProjection
p : ↥s
⊢ (map (AffineIsometry.toAffineMap (subtypeₐᵢ.{u_1, u_2, u_3} (𝕜 := 𝕜) (P := P) s))
        s').direction.HasOrthogonalProjection

Tactic:
have : (s'.map s.subtypeₐᵢ.toAffineMap).direction.HasOrthogonalProjection := by
    rw [subtypeₐᵢ_toAffineMap]
    infer_instance
-- 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
s' : AffineSubspace 𝕜 ↥s
inst_6 : Nonempty.{u_3 + 1} ↥s'
inst_7 : Submodule.HasOrthogonalProjection.{u_1, u_2} (𝕜 := 𝕜) (E := ↥s.direction) s'.direction
inst_8 : (map s.subtype s').direction.HasOrthogonalProjection
p : ↥s
this :
  (map (AffineIsometry.toAffineMap (subtypeₐᵢ.{u_1, u_2, u_3} (𝕜 := 𝕜) (P := P) s))
        s').direction.HasOrthogonalProjection
⊢ Eq.{u_3 + 1} (α := P)
    ((↑((orthogonalProjection (map (AffineIsometry.toAffineMap (subtypeₐᵢ.{u_1, u_2, u_3} (𝕜 := 𝕜) (P := P) s)) s') :
              (a : P) → ↥(map s.subtypeₐᵢ.toAffineMap s'))
            (((subtypeₐᵢ.{u_1, u_2, u_3} (𝕜 := 𝕜) (P := P) s : ↥s →ᵃⁱ[𝕜] P) : (a : ↥s) → P) p)) :
        P) :
      P)
    (((subtypeₐᵢ.{u_1, u_2, u_3} (𝕜 := 𝕜) (P := P) s : ↥s →ᵃⁱ[𝕜] P) : (a : ↥s) → P)
        (↑(((orthogonalProjection.{u_1, u_2, u_3} (𝕜 := 𝕜) (P := ↥s) s' :
                  ContinuousAffineMap.{u_1, u_2, u_2, u_3, u_3} 𝕜 ↥s ↥s') :
                (a : ↥s) → ↥s')
              p) :
          ↥s) :
      P)

Tactic:
orthogonalProjection_map s' s.subtypeₐᵢ p

Premises used: EuclideanGeometry.orthogonalProjection_map, AffineSubspace.subtypeₐᵢ
-- 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
s' : AffineSubspace 𝕜 ↥s
inst_6 : Nonempty.{u_3 + 1} ↥s'
inst_7 : Submodule.HasOrthogonalProjection.{u_1, u_2} (𝕜 := 𝕜) (E := ↥s.direction) s'.direction
inst_8 : (map s.subtype s').direction.HasOrthogonalProjection
p : ↥s
this :
  (map (AffineIsometry.toAffineMap (subtypeₐᵢ.{u_1, u_2, u_3} (𝕜 := 𝕜) (P := P) s))
        s').direction.HasOrthogonalProjection
⊢ Eq.{u_3 + 1} (α := P) (↑((orthogonalProjection (map s.subtype s') : (a : P) → ↥(map s.subtype s')) (↑p : P)) : P)
    (↑(↑(((orthogonalProjection.{u_1, u_2, u_3} (𝕜 := 𝕜) (P := ↥s) s' :
                  ContinuousAffineMap.{u_1, u_2, u_2, u_3, u_3} 𝕜 ↥s ↥s') :
                (a : ↥s) → ↥s')
              p) :
          ↥s) :
      P)

Tactic:
convert! orthogonalProjection_map s' s.subtypeₐᵢ p

Premises used: EuclideanGeometry.orthogonalProjection_map, AffineSubspace.subtypeₐᵢ
-- 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
⊢ Eq (α := P₂) ((reflection (map f.toAffineMap s) : (a : P₂) → P₂) ((f : (a : P) → P₂) p : P₂) : P₂)
    ((f : (a : P) → P₂) ((reflection s : (a : P) → P) p : P) : P₂)

Tactic:
simp [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 : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
s' : AffineSubspace 𝕜 ↥s
inst_6 : Nonempty.{u_3 + 1} ↥s'
inst_7 : Submodule.HasOrthogonalProjection.{u_1, u_2} (𝕜 := 𝕜) (E := ↥s.direction) s'.direction
inst_8 : (map s.subtype s').direction.HasOrthogonalProjection
p : ↥s
⊢ Eq (α := P)
    ((↑(((reflection.{u_1, u_2, u_3} (𝕜 := 𝕜) (P := ↥s) s' : AffineIsometryEquiv.{u_1, u_2, u_2, u_3, u_3} 𝕜 ↥s ↥s) :
              (a : ↥s) → ↥s)
            p) :
        P) :
      P)
    ((reflection (map s.subtype s') : (a : P) → P) (↑p : P) : P)

Tactic:
simp [reflection_apply', orthogonalProjection_subtype]

Premises used: EuclideanGeometry.orthogonalProjection_subtype, 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
m n : ℕ
s₁ : Simplex 𝕜 P m
s₂ : Simplex 𝕜 P n
p₁ p₂ : P
h : Set.range s₁.points = Set.range s₂.points
hp : p₁ = p₂
rw rw₁ : Eq (α := AffineSubspace 𝕜 P) (affineSpan 𝕜 (Set.range s₂.points)) (affineSpan 𝕜 (Set.range s₂.points))
⊢ Eq (α := AffineSubspace 𝕜 P) (affineSpan 𝕜 (Set.range s₁.points)) (affineSpan 𝕜 (Set.range s₂.points))

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
m n : ℕ
s : Simplex 𝕜 P m
e : Fin (m + 1) ≃ Fin (n + 1)
p : P
⊢ Eq.{u_3 + 1} (α := P)
    (↑(((s.reindex e).orthogonalProjectionSpan : (a : P) → ↥(affineSpan 𝕜 (Set.range (s.reindex e).points))) p) : P)
    (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan 𝕜 (Set.range s.points))) p) : P)

Tactic:
orthogonalProjectionSpan_congr (s.reindex_range_points e) rfl

Premises used: Affine.Simplex.orthogonalProjectionSpan_congr, Affine.Simplex.reindex_range_points, 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
n : ℕ
s : Simplex 𝕜 P n
p₁ p₂ : P
r : 𝕜
hp : Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 (Set.range s.points)) p₁
⊢ (s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan 𝕜 (Set.range s.points)))
      (r • (p₂ -ᵥ (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan 𝕜 (Set.range s.points))) p₂) : P)) +ᵥ p₁) =
    Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 (Set.range s.points)) x) p₁ hp

Tactic:
EuclideanGeometry.orthogonalProjection_vadd_smul_vsub_orthogonalProjection _ _ _

Premises used: EuclideanGeometry.orthogonalProjection_vadd_smul_vsub_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
n : ℕ
r₁ : 𝕜
s : Simplex 𝕜 P n
p p₁o : P
hp₁o : Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 (Set.range s.points)) p₁o
⊢ (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan 𝕜 (Set.range s.points)))
          (r₁ • (p -ᵥ (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan 𝕜 (Set.range s.points))) p) : P)) +ᵥ
            p₁o)) :
      P) =
    p₁o

Tactic:
congrArg ((↑) : _ → P) (orthogonalProjection_vadd_smul_vsub_orthogonalProjection _ _ _ hp₁o)

Premises used: Affine.Simplex.orthogonalProjection_vadd_smul_vsub_orthogonalProjection, congrArg
-- 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
n : ℕ
s : Simplex 𝕜 P n
p₁ p₂ : P
hp₁ : Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 (Set.range s.points)) p₁
⊢ dist p₁ p₂ * dist p₁ p₂ =
    dist p₁ (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan 𝕜 (Set.range s.points))) p₂) : P) *
        dist p₁ (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan 𝕜 (Set.range s.points))) p₂) : P) +
      dist p₂ (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan 𝕜 (Set.range s.points))) p₂) : P) *
        dist p₂ (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan 𝕜 (Set.range s.points))) p₂) : P)

Tactic:
EuclideanGeometry.dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq _ hp₁

Premises used: 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 : Simplex 𝕜 P 0
p : P
rw :
  (↑((orthogonalProjection (affineSpan 𝕜 (Set.range s.points)) : (a : P) → ↥(affineSpan 𝕜 (Set.range s.points))) p) :
      P) =
    s.points 0
⊢ (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan 𝕜 (Set.range s.points))) p) : P) = s.points 0

Tactic:
rw [orthogonalProjectionSpan]

Premises used: Affine.Simplex.orthogonalProjectionSpan
-- 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 : Simplex 𝕜 P 0
p : P
⊢ (↑((orthogonalProjection (affineSpan 𝕜 {s.points 0}) : (a : P) → ↥(affineSpan 𝕜 {s.points 0})) p) : P) = s.points 0

Tactic:
orthogonalProjection_affineSpan_singleton _ _

Premises used: EuclideanGeometry.orthogonalProjection_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 : Simplex 𝕜 P 0
p : P
h : Set.range s.points = {s.points 0}
⊢ (↑((orthogonalProjection (affineSpan 𝕜 (Set.range s.points)) : (a : P) → ↥(affineSpan 𝕜 (Set.range s.points))) p) :
      P) =
    s.points 0

Tactic:
convert! orthogonalProjection_affineSpan_singleton _ _

Premises used: EuclideanGeometry.orthogonalProjection_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 : Simplex 𝕜 P 0
p : P
⊢ Set.range s.points = {s.points 0}

Tactic:
simp [Fin.fin_one_eq_zero]

Premises used: Fin.fin_one_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 : Simplex 𝕜 P 1
i : Fin 2
p : P
⊢ (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan 𝕜 (Set.range (s.faceOpposite i).points)))
          p) :
      P) =
    s.points i.rev

Tactic:
simp [faceOpposite_point_eq_point_rev]

Premises used: Affine.Simplex.faceOpposite_point_eq_point_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
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₂
n : ℕ
s : Simplex 𝕜 P n
f : P →ᵃⁱ[𝕜] P₂
p : P
simp_rw :
  Eq.{u_5 + 1} (α := P₂)
    ((↑((orthogonalProjection (affineSpan 𝕜 (Set.range (s.map f.toAffineMap ⋯).points)) :
              (a : P₂) → ↥(affineSpan 𝕜 (Set.range (s.map f.toAffineMap ⋯).points)))
            ((f : (a : P) → P₂) p)) :
        P₂) :
      P₂)
    ((f : (a : P) → P₂)
        (↑((orthogonalProjection (affineSpan 𝕜 (Set.range s.points)) : (a : P) → ↥(affineSpan 𝕜 (Set.range s.points)))
              p) :
          P) :
      P₂)
⊢ Eq.{u_5 + 1} (α := P₂)
    ((↑(((s.map f.toAffineMap ⋯).orthogonalProjectionSpan :
              (a : P₂) → ↥(affineSpan 𝕜 (Set.range (s.map f.toAffineMap ⋯).points)))
            ((f : (a : P) → P₂) p)) :
        P₂) :
      P₂)
    ((f : (a : P) → P₂) (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan 𝕜 (Set.range s.points))) p) : P) : P₂)

Tactic:
simp_rw [orthogonalProjectionSpan]

Premises used: Affine.Simplex.orthogonalProjectionSpan
-- 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₂
n : ℕ
s : Simplex 𝕜 P n
f : P →ᵃⁱ[𝕜] P₂
p : P
⊢ Eq.{u_5 + 1} (α := P₂)
    ((↑((orthogonalProjection (AffineSubspace.map f.toAffineMap (affineSpan 𝕜 (Set.range s.points))) :
              (a : P₂) → ↥(AffineSubspace.map f.toAffineMap (affineSpan 𝕜 (Set.range s.points))))
            ((f : (a : P) → P₂) p)) :
        P₂) :
      P₂)
    ((f : (a : P) → P₂)
        (↑((orthogonalProjection (affineSpan 𝕜 (Set.range s.points)) : (a : P) → ↥(affineSpan 𝕜 (Set.range s.points)))
              p) :
          P) :
      P₂)

Tactic:
orthogonalProjection_map (affineSpan 𝕜 (Set.range s.points)) f p

Premises used: Affine.Simplex.points, EuclideanGeometry.orthogonalProjection_map, affineSpan, Set.range
-- 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₂
n : ℕ
s : Simplex 𝕜 P n
f : P →ᵃⁱ[𝕜] P₂
p : P
h :
  affineSpan 𝕜 (Set.range (s.map f.toAffineMap ⋯).points) =
    AffineSubspace.map f.toAffineMap (affineSpan 𝕜 (Set.range s.points))
⊢ Eq.{u_5 + 1} (α := P₂)
    ((↑((orthogonalProjection (affineSpan 𝕜 (Set.range (s.map f.toAffineMap ⋯).points)) :
              (a : P₂) → ↥(affineSpan 𝕜 (Set.range (s.map f.toAffineMap ⋯).points)))
            ((f : (a : P) → P₂) p)) :
        P₂) :
      P₂)
    ((f : (a : P) → P₂)
        (↑((orthogonalProjection (affineSpan 𝕜 (Set.range s.points)) : (a : P) → ↥(affineSpan 𝕜 (Set.range s.points)))
              p) :
          P) :
      P₂)

Tactic:
convert! orthogonalProjection_map (affineSpan 𝕜 (Set.range s.points)) f p

Premises used: Affine.Simplex.points, EuclideanGeometry.orthogonalProjection_map, affineSpan, Set.range
-- 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₂
n : ℕ
s : Simplex 𝕜 P n
f : P →ᵃⁱ[𝕜] P₂
p : P
⊢ affineSpan 𝕜 (Set.range (s.map f.toAffineMap ⋯).points) =
    AffineSubspace.map f.toAffineMap (affineSpan 𝕜 (Set.range s.points))

Tactic:
simp [AffineSubspace.map_span, Set.range_comp]

Premises used: Set.range_comp, AffineSubspace.map_span
-- 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
n : ℕ
s : Simplex 𝕜 P n
S : AffineSubspace 𝕜 P
hS : affineSpan 𝕜 (Set.range s.points) ≤ S
p : ↥S
rw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [eq_comm]

Premises used: eq_comm
-- 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
n : ℕ
s : Simplex 𝕜 P n
S : AffineSubspace 𝕜 P
hS : affineSpan 𝕜 (Set.range s.points) ≤ S
p : ↥S
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
(s.restrict S hS).orthogonalProjectionSpan_map S.subtypeₐᵢ p

Premises used: Affine.Simplex.orthogonalProjectionSpan_map, AffineSubspace.subtypeₐᵢ
-- 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
n : ℕ
s : Simplex 𝕜 P n
S : AffineSubspace 𝕜 P
hS : affineSpan 𝕜 (Set.range s.points) ≤ S
p : ↥S
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
convert! (s.restrict S hS).orthogonalProjectionSpan_map S.subtypeₐᵢ p
-- Module: Mathlib.Geometry.Euclidean.SignedDist
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
v x y : V
h :
  ∀ (x_1 : P),
    Eq (α := ℝ) ((ContinuousAffineMap.const ℝ P ⟪-NormedSpace.normalize v, x + y⟫ : (a : P) → ℝ) x_1 : ℝ)
      ((HAdd.hAdd (α := P →ᴬ[ℝ] ℝ) (ContinuousAffineMap.const ℝ P ⟪-NormedSpace.normalize v, x⟫)
              (ContinuousAffineMap.const ℝ P ⟪-NormedSpace.normalize v, y⟫) :
            (a : P) → ℝ)
          x_1 :
        ℝ)
⊢ ContinuousAffineMap.const ℝ P ⟪-NormedSpace.normalize v, x + y⟫ =
    HAdd.hAdd (α := P →ᴬ[ℝ] ℝ) (ContinuousAffineMap.const ℝ P ⟪-NormedSpace.normalize v, x⟫)
      (ContinuousAffineMap.const ℝ P ⟪-NormedSpace.normalize v, y⟫)

Tactic:
ext
-- Module: Mathlib.Geometry.Euclidean.SignedDist
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
v x y : V
x_1 : P
⊢ Eq (α := ℝ) ((ContinuousAffineMap.const ℝ P ⟪-NormedSpace.normalize v, x + y⟫ : (a : P) → ℝ) x_1 : ℝ)
    ((HAdd.hAdd (α := P →ᴬ[ℝ] ℝ) (ContinuousAffineMap.const ℝ P ⟪-NormedSpace.normalize v, x⟫)
            (ContinuousAffineMap.const ℝ P ⟪-NormedSpace.normalize v, y⟫) :
          (a : P) → ℝ)
        x_1 :
      ℝ)

Tactic:
simp [inner_add_right]

Premises used: inner_add_right
-- Module: Mathlib.Geometry.Euclidean.SignedDist
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
v : V
r : ℝ
x : V
h :
  ∀ (x_1 : P),
    Eq (α := ℝ) ((ContinuousAffineMap.const ℝ P ⟪-NormedSpace.normalize v, r • x⟫ : (a : P) → ℝ) x_1 : ℝ)
      ((HSMul.hSMul (α := ℝ) (β := P →ᴬ[ℝ] ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ)
              (ContinuousAffineMap.const ℝ P ⟪-NormedSpace.normalize v, x⟫) :
            (a : P) → ℝ)
          x_1 :
        ℝ)
⊢ ContinuousAffineMap.const ℝ P ⟪-NormedSpace.normalize v, r • x⟫ =
    HSMul.hSMul (α := ℝ) (β := P →ᴬ[ℝ] ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ)
      (ContinuousAffineMap.const ℝ P ⟪-NormedSpace.normalize v, x⟫)

Tactic:
ext
-- Module: Mathlib.Geometry.Euclidean.SignedDist
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
v : V
r : ℝ
x : V
x_1 : P
⊢ Eq (α := ℝ) ((ContinuousAffineMap.const ℝ P ⟪-NormedSpace.normalize v, r • x⟫ : (a : P) → ℝ) x_1 : ℝ)
    ((HSMul.hSMul (α := ℝ) (β := P →ᴬ[ℝ] ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ)
            (ContinuousAffineMap.const ℝ P ⟪-NormedSpace.normalize v, x⟫) :
          (a : P) → ℝ)
        x_1 :
      ℝ)

Tactic:
simp [inner_smul_right]

Premises used: inner_smul_right