awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
s : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥s
inst_5 : s.direction.HasOrthogonalProjection
p x : P
rw rw₁ :
  Eq (α := ℝ)
    (((signedDist (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) : (a : P) → P →ᴬ[ℝ] ℝ)
            (↑((orthogonalProjection s : (a : P) → ↥s) x) : P) :
          (a : P) → ℝ)
        x :
      ℝ)
    (((signedDist (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) : (a : P) → P →ᴬ[ℝ] ℝ)
            (↑((orthogonalProjection s : (a : P) → ↥s) x) : P) :
          (a : P) → ℝ)
        x :
      ℝ)
⊢ Eq (α := ℝ) ((s.signedInfDist p : (a : P) → ℝ) x : ℝ)
    (((signedDist (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) : (a : P) → P →ᴬ[ℝ] ℝ)
            (↑((orthogonalProjection s : (a : P) → ↥s) x) : P) :
          (a : P) → ℝ)
        x :
      ℝ)

Tactic:
rw [signedInfDist_eq_signedDist_of_mem (orthogonalProjection_mem x)]

Premises used: AffineSubspace.signedInfDist_eq_signedDist_of_mem, EuclideanGeometry.orthogonalProjection_mem
-- 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
s : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥s
inst_5 : s.direction.HasOrthogonalProjection
p : P
rw :
  ((signedDist (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) : (a : P) → P →ᴬ[ℝ] ℝ)
          (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) :
        (a : P) → ℝ)
      p =
    ‖p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)‖
rw₁ :
  dist (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p = ‖p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)‖
rw₂ rw₃ :
  ‖p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)‖ = ‖p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)‖
⊢ (s.signedInfDist p : (a : P) → ℝ) p = ‖p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)‖

Tactic:
rw [signedInfDist_eq_signedDist_orthogonalProjection, signedDist_vsub_self, dist_eq_norm_vsub']

Premises used: AffineSubspace.signedInfDist_eq_signedDist_orthogonalProjection, dist_eq_norm_vsub', signedDist_vsub_self
-- 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
s : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥s
inst_5 : s.direction.HasOrthogonalProjection
p x : P
hx : x ∈ s
⊢ Eq (α := ℝ) ((s.signedInfDist p : (a : P) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
simp [signedInfDist_eq_signedDist_orthogonalProjection, orthogonalProjection_eq_self_iff.2 hx]

Premises used: Iff.mpr, AffineSubspace.signedInfDist_eq_signedDist_orthogonalProjection, EuclideanGeometry.orthogonalProjection_eq_self_iff
-- 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
s : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥s
inst_5 : s.direction.HasOrthogonalProjection
p : P
h : p ∈ s
h₁ :
  ∀ (x : P),
    Eq (α := ℝ) (((↑(s.signedInfDist p) : P →ᵃ[ℝ] ℝ) : (a : P) → ℝ) x : ℝ) ((AffineMap.const ℝ P 0 : (a : P) → ℝ) x : ℝ)
⊢ (↑(s.signedInfDist p) : P →ᵃ[ℝ] ℝ) = AffineMap.const ℝ P 0

Tactic:
ext x
-- 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
s : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥s
inst_5 : s.direction.HasOrthogonalProjection
p : P
h : p ∈ s
x : P
⊢ Eq (α := ℝ) (((↑(s.signedInfDist p) : P →ᵃ[ℝ] ℝ) : (a : P) → ℝ) x : ℝ) ((AffineMap.const ℝ P 0 : (a : P) → ℝ) x : ℝ)

Tactic:
simp [signedInfDist_def, orthogonalProjection_eq_self_iff.2 h]

Premises used: Iff.mpr, AffineSubspace.signedInfDist_def, EuclideanGeometry.orthogonalProjection_eq_self_iff
-- 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
s : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥s
inst_5 : s.direction.HasOrthogonalProjection
p x : P
h : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (insert p (↑s : Set P))) x
⊢ ∃ (r : ℝ), ∃ p0 ∈ s, x = r • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) +ᵥ p0

Tactic:
rw [mem_affineSpan_insert_iff (orthogonalProjection s p).property] at h

Premises used: AffineSubspace.mem_affineSpan_insert_iff, EuclideanGeometry.orthogonalProjection, DFunLike.coe, Subtype.property
-- 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
s : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥s
inst_5 : s.direction.HasOrthogonalProjection
p x : P
h : ∃ (r : ℝ), ∃ p0 ∈ s, x = r • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) +ᵥ p0
rcases :
  ∀ (r : ℝ) (p₀ : P) (hp₀ : p₀ ∈ s),
    |(s.signedInfDist p : (a : P) → ℝ) (r • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) +ᵥ p₀)| =
      dist (r • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) +ᵥ p₀)
        (↑((orthogonalProjection s : (a : P) → ↥s)
              (r • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) +ᵥ p₀)) :
          P)
⊢ |(s.signedInfDist p : (a : P) → ℝ) x| = dist x (↑((orthogonalProjection s : (a : P) → ↥s) x) : P)

Tactic:
rcases h with ⟨r, p₀, hp₀, rfl⟩

Premises used: rfl
-- 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
s : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥s
inst_5 : s.direction.HasOrthogonalProjection
p : P
r : ℝ
p₀ : P
hp₀ : p₀ ∈ s
⊢ |(s.signedInfDist p : (a : P) → ℝ) (r • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) +ᵥ p₀)| =
    dist (r • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) +ᵥ p₀)
      (↑((orthogonalProjection s : (a : P) → ↥s)
            (r • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) +ᵥ p₀)) :
        P)

Tactic:
simp [hp₀, dist_eq_norm_vsub, orthogonalProjection_eq_self_iff.2 hp₀,
    orthogonalProjection_vsub_orthogonalProjection, norm_smul, abs_mul]

Premises used: Iff.mpr, norm_smul, abs_mul, dist_eq_norm_vsub, EuclideanGeometry.orthogonalProjection_eq_self_iff, EuclideanGeometry.orthogonalProjection_vsub_orthogonalProjection
-- 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
p q : P
⊢ Eq (α := P →ᴬ[ℝ] ℝ) (signedInfDist (affineSpan ℝ {q}) p) ((signedDist (p -ᵥ q) : (a : P) → P →ᴬ[ℝ] ℝ) q)

Tactic:
simpa using signedInfDist_eq_signedDist_of_mem (mem_affineSpan ℝ (Set.mem_singleton q))

Premises used: Set.mem_singleton, Real, AffineSubspace.signedInfDist_eq_signedDist_of_mem, mem_affineSpan
-- 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
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
m : ℕ
inst_5 : NeZero m
e : Fin (n + 1) ≃ Fin (m + 1)
j : Fin (m + 1)
simp_rw :
  Eq (α := P →ᴬ[ℝ] ℝ)
    (AffineSubspace.signedInfDist (affineSpan ℝ ((s.reindex e).points '' {j}ᶜ)) ((s.reindex e).points j))
    (AffineSubspace.signedInfDist
      (affineSpan ℝ
        (s.points '' (singleton (α := Fin (n + 1)) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j : Fin (n + 1)))ᶜ))
      (s.points ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j)))
simp_rw₁ :
  Eq (α := P →ᴬ[ℝ] ℝ)
    (AffineSubspace.signedInfDist
      (affineSpan ℝ ((fun (a : Fin (m + 1)) ↦ (s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) a) '' {j}ᶜ))
      ((s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) j))
    (AffineSubspace.signedInfDist
      (affineSpan ℝ
        (s.points '' (singleton (α := Fin (n + 1)) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j : Fin (n + 1)))ᶜ))
      (s.points ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j)))
simp_rw₂ :
  Eq (α := P →ᴬ[ℝ] ℝ)
    (AffineSubspace.signedInfDist
      (affineSpan ℝ (s.points '' Set.image (α := Fin (m + 1)) (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1)) {j}ᶜ))
      ((s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) j))
    (AffineSubspace.signedInfDist
      (affineSpan ℝ
        (s.points '' (singleton (α := Fin (n + 1)) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j : Fin (n + 1)))ᶜ))
      (s.points ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j)))
simp_rw₃ :
  Eq (α := P →ᴬ[ℝ] ℝ)
    (AffineSubspace.signedInfDist
      (affineSpan ℝ (s.points '' (Set.image (α := Fin (m + 1)) (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1)) {j})ᶜ))
      ((s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) j))
    (AffineSubspace.signedInfDist
      (affineSpan ℝ
        (s.points '' (singleton (α := Fin (n + 1)) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j : Fin (n + 1)))ᶜ))
      (s.points ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j)))
simp_rw₄ :
  Eq (α := P →ᴬ[ℝ] ℝ)
    (AffineSubspace.signedInfDist
      (affineSpan ℝ
        (s.points '' (singleton (α := Fin (n + 1)) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j : Fin (n + 1)))ᶜ))
      ((s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) j))
    (AffineSubspace.signedInfDist
      (affineSpan ℝ
        (s.points '' (singleton (α := Fin (n + 1)) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j : Fin (n + 1)))ᶜ))
      (s.points ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j)))
⊢ (s.reindex e).signedInfDist j = s.signedInfDist ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j)

Tactic:
simp_rw [signedInfDist, reindex_points, Set.image_comp, Set.image_compl_eq e.symm.bijective,
    Set.image_singleton, Function.comp_apply]

Premises used: Set.image_singleton, Equiv.bijective, Set.image_compl_eq, Affine.Simplex.signedInfDist, Affine.Simplex.reindex_points, Set.image_comp, Function.comp_apply, Equiv.symm
-- 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
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
⊢ ‖s.points i -ᵥ
        (↑((orthogonalProjection (affineSpan ℝ (s.points '' {i}ᶜ)) : (a : P) → ↥(affineSpan ℝ (s.points '' {i}ᶜ)))
              (s.points i)) :
          P)‖ =
    ‖s.points i -ᵥ
        (↑(((s.faceOpposite i).orthogonalProjectionSpan :
                (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
              (s.points i)) :
          P)‖

Tactic:
simp [orthogonalProjectionSpan]

Premises used: Affine.Simplex.orthogonalProjectionSpan
-- 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
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
i j : Fin (n + 1)
h : j ≠ i
⊢ Eq (α := ℝ) ((s.signedInfDist i : (a : P) → ℝ) (s.points j) : ℝ) (0 : ℝ)

Tactic:
AffineSubspace.signedInfDist_apply_of_mem _ (s.mem_affineSpan_image_iff.2 h)

Premises used: Iff.mpr, Affine.Simplex.mem_affineSpan_image_iff, AffineSubspace.signedInfDist_apply_of_mem
-- 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
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
w : Fin (n + 1) → ℝ
h : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
rw :
  (AffineMap.lineMap 0
          ‖s.points i -ᵥ
              (↑(((s.faceOpposite i).orthogonalProjectionSpan :
                      (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
                    (s.points i)) :
                P)‖ :
        (a : ℝ) → ℝ)
      (∑ i ∈ Finset.univ ∩ {i}, w i) =
    w i *
      ‖s.points i -ᵥ
          (↑(((s.faceOpposite i).orthogonalProjectionSpan :
                  (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
                (s.points i)) :
            P)‖
hp₂ :
  ∀ (i_1 : Fin (n + 1)),
    Membership.mem (γ := Finset (Fin (n + 1))) (Finset.univ ∩ {i}) i_1 →
      ((⇑(↑(s.signedInfDist i) : P →ᵃ[ℝ] ℝ) : (a : P) → ℝ) ∘ s.points) i_1 =
        ‖s.points i -ᵥ
            (↑(((s.faceOpposite i).orthogonalProjectionSpan :
                    (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
                  (s.points i)) :
              P)‖
hp₁ :
  ∀ (i_1 : Fin (n + 1)),
    Membership.mem (γ := Finset (Fin (n + 1))) (Finset.univ \ {i}) i_1 →
      Eq (α := ℝ) (((⇑(↑(s.signedInfDist i) : P →ᵃ[ℝ] ℝ) : (a : P) → ℝ) ∘ s.points) i_1) 0
⊢ (s.signedInfDist i : (a : P) → ℝ)
      ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P) =
    w i *
      ‖s.points i -ᵥ
          (↑(((s.faceOpposite i).orthogonalProjectionSpan :
                  (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
                (s.points i)) :
            P)‖

Tactic:
rw [← ContinuousAffineMap.coe_toAffineMap, Finset.map_affineCombination _ _ _ h,
    Finset.univ.affineCombination_apply_eq_lineMap_sum w
      ((s.signedInfDist i).toAffineMap ∘ s.points) 0
      ‖s.points i -ᵥ (s.faceOpposite i).orthogonalProjectionSpan (s.points i)‖
      {i} h]

Premises used: Norm.norm, Finset.affineCombination_apply_eq_lineMap_sum, Affine.Simplex.points, Finset.univ, Affine.Simplex.orthogonalProjectionSpan, ContinuousAffineMap.coe_toAffineMap, Function.comp, Finset.map_affineCombination, VSub.vsub, Affine.Simplex.signedInfDist, ContinuousAffineMap.toAffineMap, Affine.Simplex.faceOpposite, Singleton.singleton, OfNat.ofNat, Subtype.val, DFunLike.coe
-- 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
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
w : Fin (n + 1) → ℝ
h : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
⊢ (AffineMap.lineMap 0
          ‖s.points i -ᵥ
              (↑(((s.faceOpposite i).orthogonalProjectionSpan :
                      (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
                    (s.points i)) :
                P)‖ :
        (a : ℝ) → ℝ)
      (∑ i ∈ Finset.univ ∩ {i}, w i) =
    w i *
      ‖s.points i -ᵥ
          (↑(((s.faceOpposite i).orthogonalProjectionSpan :
                  (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
                (s.points i)) :
            P)‖

Tactic:
simp [AffineMap.lineMap_apply]

Premises used: AffineMap.lineMap_apply
-- 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
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
w : Fin (n + 1) → ℝ
h : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
⊢ ∀ (i_1 : Fin (n + 1)),
    Membership.mem (γ := Finset (Fin (n + 1))) (Finset.univ ∩ {i}) i_1 →
      ((⇑(↑(s.signedInfDist i) : P →ᵃ[ℝ] ℝ) : (a : P) → ℝ) ∘ s.points) i_1 =
        ‖s.points i -ᵥ
            (↑(((s.faceOpposite i).orthogonalProjectionSpan :
                    (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
                  (s.points i)) :
              P)‖

Tactic:
simp [signedInfDist_apply_self]

Premises used: Affine.Simplex.signedInfDist_apply_self
-- 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
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
w : Fin (n + 1) → ℝ
h : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hp₁ :
  ∀ (i_1 : Fin (n + 1)),
    ¬i_1 = i → Eq (α := ℝ) (((↑(s.signedInfDist i) : P →ᵃ[ℝ] ℝ) : (a : P) → ℝ) (s.points i_1) : ℝ) (0 : ℝ)
⊢ ∀ (i_1 : Fin (n + 1)),
    Membership.mem (γ := Finset (Fin (n + 1))) (Finset.univ \ {i}) i_1 →
      Eq (α := ℝ) (((⇑(↑(s.signedInfDist i) : P →ᵃ[ℝ] ℝ) : (a : P) → ℝ) ∘ s.points) i_1) 0

Tactic:
simp only [Finset.mem_sdiff, Finset.mem_univ, Finset.mem_singleton, true_and,
      Function.comp_apply]

Premises used: Finset.mem_univ, Finset.mem_singleton, Finset.mem_sdiff, Function.comp_apply, true_and
-- 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
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
w : Fin (n + 1) → ℝ
h : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
j : Fin (n + 1)
hj : ¬j = i
⊢ Eq (α := ℝ) (((↑(s.signedInfDist i) : P →ᵃ[ℝ] ℝ) : (a : P) → ℝ) (s.points j) : ℝ) (0 : ℝ)

Tactic:
s.signedInfDist_apply_of_ne hj

Premises used: Affine.Simplex.signedInfDist_apply_of_ne
-- 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
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
w : Fin (n + 1) → ℝ
h : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
j : Fin (n + 1)
hj : ¬j = i
⊢ Eq (α := ℝ) (((↑(s.signedInfDist i) : P →ᵃ[ℝ] ℝ) : (a : P) → ℝ) (s.points j) : ℝ) (0 : ℝ)

Tactic:
exact s.signedInfDist_apply_of_ne hj

Premises used: Affine.Simplex.signedInfDist_apply_of_ne
-- 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
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
p : P
h : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p
rw :
  dist p
      (↑((orthogonalProjection (affineSpan ℝ (s.points '' {i}ᶜ)) : (a : P) → ↥(affineSpan ℝ (s.points '' {i}ᶜ))) p) :
        P) =
    dist p
      (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
              (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
            p) :
        P)
rw₁ :
  Membership.mem (γ := AffineSubspace ℝ P)
    (affineSpan ℝ (insert (s.points i) (↑(affineSpan ℝ (s.points '' {i}ᶜ)) : Set P))) p
⊢ |(s.signedInfDist i : (a : P) → ℝ) p| =
    dist p
      (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
            p) :
        P)

Tactic:
rw [signedInfDist, AffineSubspace.abs_signedInfDist_eq_dist_of_mem_affineSpan_insert,
    orthogonalProjectionSpan]

Premises used: Affine.Simplex.orthogonalProjectionSpan, AffineSubspace.abs_signedInfDist_eq_dist_of_mem_affineSpan_insert, Affine.Simplex.signedInfDist
-- 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
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
p : P
h : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p
⊢ dist p
      (↑((orthogonalProjection (affineSpan ℝ (s.points '' {i}ᶜ)) : (a : P) → ↥(affineSpan ℝ (s.points '' {i}ᶜ))) p) :
        P) =
    dist p
      (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
              (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
            p) :
        P)

Tactic:
simp_rw [range_faceOpposite_points]

Premises used: Affine.Simplex.range_faceOpposite_points
-- 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
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
p : P
h : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p
rw : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (insert (s.points i) (s.points '' {i}ᶜ))) p
⊢ Membership.mem (γ := AffineSubspace ℝ P)
    (affineSpan ℝ (insert (s.points i) (↑(affineSpan ℝ (s.points '' {i}ᶜ)) : Set P))) p

Tactic:
rw [affineSpan_insert_affineSpan]

Premises used: affineSpan_insert_affineSpan
-- 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
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
p : P
h : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p

Tactic:
h
-- 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
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
p : P
h : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p
h₁ : insert (s.points i) (s.points '' {i}ᶜ) = Set.range s.points
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (insert (s.points i) (s.points '' {i}ᶜ))) p

Tactic:
convert! h
-- 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
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
p : P
h : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p
⊢ insert (s.points i) (s.points '' {i}ᶜ) = Set.range s.points

Tactic:
Set.insert_image_compl_eq_range s.points i

Premises used: Affine.Simplex.points, Set.insert_image_compl_eq_range
-- 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
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
p : P
h : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p
⊢ insert (s.points i) (s.points '' {i}ᶜ) = Set.range s.points

Tactic:
exact Set.insert_image_compl_eq_range s.points i

Premises used: Affine.Simplex.points, Set.insert_image_compl_eq_range
-- Module: Mathlib.Geometry.Euclidean.Similarity
Goal:
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst : NormedAddCommGroup V₁
inst_1 : NormedAddCommGroup V₂
inst_2 : InnerProductSpace ℝ V₁
inst_3 : InnerProductSpace ℝ V₂
inst_4 : MetricSpace P₁
inst_5 : MetricSpace P₂
inst_6 : NormedAddTorsor V₁ P₁
inst_7 : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
h_not_col : ¬Collinear ℝ (P := P₁) {a, b, c}
h₁ : ∠ a b c = ∠ a' b' c'
h₂ : ∠ b c a = ∠ b' c' a'
by_contra! : ∀ (hq : ∠ a b c = Real.pi / 2 ∧ ∠ b c a = Real.pi / 2), False
⊢ ∠ a b c ≠ Real.pi / 2 ∨ ∠ b c a ≠ Real.pi / 2

Tactic:
by_contra! hq
-- Module: Mathlib.Geometry.Euclidean.Similarity
Goal:
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst : NormedAddCommGroup V₁
inst_1 : NormedAddCommGroup V₂
inst_2 : InnerProductSpace ℝ V₁
inst_3 : InnerProductSpace ℝ V₂
inst_4 : MetricSpace P₁
inst_5 : MetricSpace P₂
inst_6 : NormedAddTorsor V₁ P₁
inst_7 : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
h_not_col : ¬Collinear ℝ (P := P₁) {a, b, c}
h₁ : ∠ a b c = ∠ a' b' c'
h₂ : ∠ b c a = ∠ b' c' a'
hq : ∠ a b c = Real.pi / 2 ∧ ∠ b c a = Real.pi / 2
⊢ ∠ b c a < Real.pi / 2

Tactic:
have := angle_lt_pi_div_two_of_angle_eq_pi_div_two hq.1 (ne₂₃_of_not_collinear h_not_col).symm
-- Module: Mathlib.Geometry.Euclidean.Similarity
Goal:
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst : NormedAddCommGroup V₁
inst_1 : NormedAddCommGroup V₂
inst_2 : InnerProductSpace ℝ V₁
inst_3 : InnerProductSpace ℝ V₂
inst_4 : MetricSpace P₁
inst_5 : MetricSpace P₂
inst_6 : NormedAddTorsor V₁ P₁
inst_7 : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
h_not_col : ¬Collinear ℝ (P := P₁) {a, b, c}
h₁ : ∠ a b c = ∠ a' b' c'
h₂ : ∠ b c a = ∠ b' c' a'
hq : ∠ a b c = Real.pi / 2 ∧ ∠ b c a = Real.pi / 2
this : ∠ b c a < Real.pi / 2
⊢ False

Tactic:
grind