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
v : V
p : P
v' : V
h :
  ∀ (q : P),
    Eq (α := ℝ)
      ((ContinuousAffineMap.comp
              (ContinuousLinearMap.toContinuousAffineMap ((innerSL ℝ : (a : V) → V →L[ℝ] ℝ) (NormedSpace.normalize v)))
              (VSub.vsub (P := P →ᴬ[ℝ] P) (ContinuousAffineMap.id ℝ P) (ContinuousAffineMap.const ℝ P (v' +ᵥ p))) :
            (a : P) → ℝ)
          q :
        ℝ)
      ((HVAdd.hVAdd (α := P →ᴬ[ℝ] ℝ) (β := P →ᴬ[ℝ] ℝ)
              (({ toFun := fun (w : V) ↦ ContinuousAffineMap.const ℝ P ⟪-NormedSpace.normalize v, w⟫, map_add' := ⋯,
                      map_smul' := ⋯ : V →ₗ[ℝ] P →ᴬ[ℝ] ℝ } :
                    (a : V) → P →ᴬ[ℝ] ℝ)
                  v' :
                P →ᴬ[ℝ] ℝ)
              (ContinuousAffineMap.comp
                (ContinuousLinearMap.toContinuousAffineMap
                  ((innerSL ℝ : (a : V) → V →L[ℝ] ℝ) (NormedSpace.normalize v)))
                (VSub.vsub (P := P →ᴬ[ℝ] P) (ContinuousAffineMap.id ℝ P) (ContinuousAffineMap.const ℝ P p))) :
            (a : P) → ℝ)
          q :
        ℝ)
⊢ ContinuousAffineMap.comp
      (ContinuousLinearMap.toContinuousAffineMap ((innerSL ℝ : (a : V) → V →L[ℝ] ℝ) (NormedSpace.normalize v)))
      (VSub.vsub (P := P →ᴬ[ℝ] P) (ContinuousAffineMap.id ℝ P) (ContinuousAffineMap.const ℝ P (v' +ᵥ p))) =
    HVAdd.hVAdd (α := P →ᴬ[ℝ] ℝ) (β := P →ᴬ[ℝ] ℝ)
      (({ toFun := fun (w : V) ↦ ContinuousAffineMap.const ℝ P ⟪-NormedSpace.normalize v, w⟫, map_add' := ⋯,
              map_smul' := ⋯ : V →ₗ[ℝ] P →ᴬ[ℝ] ℝ } :
            (a : V) → P →ᴬ[ℝ] ℝ)
          v' :
        P →ᴬ[ℝ] ℝ)
      (ContinuousAffineMap.comp
        (ContinuousLinearMap.toContinuousAffineMap ((innerSL ℝ : (a : V) → V →L[ℝ] ℝ) (NormedSpace.normalize v)))
        (VSub.vsub (P := P →ᴬ[ℝ] P) (ContinuousAffineMap.id ℝ P) (ContinuousAffineMap.const ℝ P p)))

Tactic:
ext q
-- 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
p : P
v' : V
q : P
⊢ Eq (α := ℝ)
    ((ContinuousAffineMap.comp
            (ContinuousLinearMap.toContinuousAffineMap ((innerSL ℝ : (a : V) → V →L[ℝ] ℝ) (NormedSpace.normalize v)))
            (VSub.vsub (P := P →ᴬ[ℝ] P) (ContinuousAffineMap.id ℝ P) (ContinuousAffineMap.const ℝ P (v' +ᵥ p))) :
          (a : P) → ℝ)
        q :
      ℝ)
    ((HVAdd.hVAdd (α := P →ᴬ[ℝ] ℝ) (β := P →ᴬ[ℝ] ℝ)
            (({ toFun := fun (w : V) ↦ ContinuousAffineMap.const ℝ P ⟪-NormedSpace.normalize v, w⟫, map_add' := ⋯,
                    map_smul' := ⋯ : V →ₗ[ℝ] P →ᴬ[ℝ] ℝ } :
                  (a : V) → P →ᴬ[ℝ] ℝ)
                v' :
              P →ᴬ[ℝ] ℝ)
            (ContinuousAffineMap.comp
              (ContinuousLinearMap.toContinuousAffineMap ((innerSL ℝ : (a : V) → V →L[ℝ] ℝ) (NormedSpace.normalize v)))
              (VSub.vsub (P := P →ᴬ[ℝ] P) (ContinuousAffineMap.id ℝ P) (ContinuousAffineMap.const ℝ P p))) :
          (a : P) → ℝ)
        q :
      ℝ)

Tactic:
simp [vsub_vadd_eq_vsub_sub, inner_sub_right, ← sub_eq_neg_add]

Premises used: vsub_vadd_eq_vsub_sub, sub_eq_neg_add, inner_sub_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
p : P
⊢ Eq (α := P →ᴬ[ℝ] ℝ) ((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ)
    (ContinuousAffineMap.comp
        (ContinuousLinearMap.toContinuousAffineMap ((innerSL ℝ : (a : V) → V →L[ℝ] ℝ) (NormedSpace.normalize v)))
        (VSub.vsub (P := P →ᴬ[ℝ] P) (ContinuousAffineMap.id ℝ P) (ContinuousAffineMap.const ℝ P p)) :
      P →ᴬ[ℝ] ℝ)

Tactic:
rfl

Premises used: ContinuousAffineMap.comp, 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
v : V
p q : P
⊢ (((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q = ⟪NormedSpace.normalize v, q -ᵥ p⟫

Tactic:
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
v : V
p : P
change :
  Eq (α := V →ₗ[ℝ] ℝ)
    ((innerₗ V : (a : V) → V →ₗ[ℝ] ℝ) (NormedSpace.normalize v) ∘ₗ HSub.hSub (α := V →ₗ[ℝ] V) LinearMap.id 0)
    ((innerₗ V : (a : V) → V →ₗ[ℝ] ℝ) (NormedSpace.normalize v))
⊢ Eq (α := V →ₗ[ℝ] ℝ)
    (AffineMap.linear.{0, u_1, u_2, 0, 0} (P1 := P) (P2 := ℝ) (↑((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p) : P →ᵃ[ℝ] ℝ))
    ((innerₗ V : (a : V) → V →ₗ[ℝ] ℝ) (NormedSpace.normalize v))

Tactic:
change (innerₗ V (normalize v)).comp (LinearMap.id - 0) = _

Premises used: LinearMap.id, HSub.hSub, LinearMap.comp, OfNat.ofNat, NormedSpace.normalize, DFunLike.coe, innerₗ
-- 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
p : P
⊢ Eq (α := V →ₗ[ℝ] ℝ)
    ((innerₗ V : (a : V) → V →ₗ[ℝ] ℝ) (NormedSpace.normalize v) ∘ₗ HSub.hSub (α := V →ₗ[ℝ] V) LinearMap.id 0)
    ((innerₗ V : (a : V) → V →ₗ[ℝ] ℝ) (NormedSpace.normalize v))

Tactic:
simp
-- 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 w : V
p : P
⊢ (AffineMap.linear.{0, u_1, u_2, 0, 0} (P1 := P) (P2 := ℝ) (↑((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p) : P →ᵃ[ℝ] ℝ) :
        (a : V) → ℝ)
      w =
    ⟪NormedSpace.normalize v, w⟫

Tactic:
simp [signedDist_apply_linear]

Premises used: signedDist_apply_linear
-- 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 w : V
⊢ Eq (α := P →ᴬ[ℝ] ℝ) ((AffineMap.linear (signedDist v) : (a : V) → P →ᴬ[ℝ] ℝ) w : P →ᴬ[ℝ] ℝ)
    (ContinuousAffineMap.const ℝ P ⟪-NormedSpace.normalize v, w⟫ : P →ᴬ[ℝ] ℝ)

Tactic:
rfl

Premises used: ContinuousAffineMap.const, 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
v w : V
p : P
⊢ (((AffineMap.linear (signedDist v) : (a : V) → P →ᴬ[ℝ] ℝ) w : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) p =
    ⟪-NormedSpace.normalize v, w⟫

Tactic:
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
v : V
p q : P
r : ℝ
simp :
  ⟪NormedSpace.normalize (r • v), q -ᵥ p⟫ =
    (↑((SignType.sign : (a : ℝ) → SignType) r) : ℝ) * ⟪NormedSpace.normalize v, q -ᵥ p⟫
⊢ (((signedDist (r • v) : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q =
    HMul.hMul (α := ℝ) (β := ℝ) ((↑((SignType.sign : (a : ℝ) → SignType) r) : ℝ) : ℝ)
      ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)

Tactic:
simp only [signedDist_apply_apply]

Premises used: signedDist_apply_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
v : V
p q : P
r : ℝ
rw :
  ⟪HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) r) : ℝ) (NormedSpace.normalize v), q -ᵥ p⟫ =
    (↑((SignType.sign : (a : ℝ) → SignType) r) : ℝ) * ⟪NormedSpace.normalize v, q -ᵥ p⟫
rw₁ rw₂ :
  (↑((SignType.sign : (a : ℝ) → SignType) r) : ℝ) * ⟪NormedSpace.normalize v, q -ᵥ p⟫ =
    (↑((SignType.sign : (a : ℝ) → SignType) r) : ℝ) * ⟪NormedSpace.normalize v, q -ᵥ p⟫
⊢ ⟪NormedSpace.normalize (r • v), q -ᵥ p⟫ =
    (↑((SignType.sign : (a : ℝ) → SignType) r) : ℝ) * ⟪NormedSpace.normalize v, q -ᵥ p⟫

Tactic:
rw [normalize_smul, real_inner_smul_left]

Premises used: NormedSpace.normalize_smul, real_inner_smul_left
-- 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
p q : P
r : ℝ
h : 0 < r
⊢ Eq (α := ℝ) ((((signedDist (r • v) : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)
    ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)

Tactic:
simp [signedDist_smul, h]

Premises used: signedDist_smul
-- 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
p q : P
r : ℝ
h : r < 0
⊢ Eq (α := ℝ) ((((signedDist (r • v) : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)
    (-(((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)

Tactic:
simp [signedDist_smul, h]

Premises used: signedDist_smul
-- 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 (α := ℝ) ((((signedDist 0 : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ) (0 : ℝ)

Tactic:
simpa using signedDist_smul 0 p q 0

Premises used: signedDist_smul, OfNat.ofNat
-- 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
p q : P
⊢ Eq (α := ℝ) ((((signedDist (-v) : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)
    (-(((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)

Tactic:
simpa using signedDist_smul v p q (-1)

Premises used: signedDist_smul, OfNat.ofNat, Neg.neg
-- 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 w : V
h : ∃ r > 0, r • v = w
obtain : ∀ r > 0, r • v = w → Eq (α := P →ᵃ[ℝ] P →ᴬ[ℝ] ℝ) (signedDist v) (signedDist w)
⊢ Eq (α := P →ᵃ[ℝ] P →ᴬ[ℝ] ℝ) (signedDist v) (signedDist w)

Tactic:
obtain ⟨r, _, _⟩ := 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
v w : V
r : ℝ
left : r > 0
right : r • v = w
h :
  ∀ (p q : P),
    Eq (α := ℝ) ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)
      ((((signedDist w : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)
⊢ Eq (α := P →ᵃ[ℝ] P →ᴬ[ℝ] ℝ) (signedDist v) (signedDist w)

Tactic:
ext p q
-- 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 w : V
r : ℝ
left : r > 0
right : r • v = w
p q : P
⊢ Eq (α := ℝ) ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)
    ((((signedDist w : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)

Tactic:
simpa [*] using (signedDist_smul v p q r).symm

Premises used: signedDist_smul, Eq.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
v : V
p : P
⊢ Eq (α := ℝ) ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) p : ℝ) (0 : ℝ)

Tactic:
simp [signedDist_apply_apply]

Premises used: signedDist_apply_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
v : V
p q : P
⊢ Eq (α := ℝ) (-(((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)
    ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) q : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) p : ℝ)

Tactic:
simp [signedDist_apply_apply, ← inner_neg_right]

Premises used: signedDist_apply_apply, inner_neg_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
p q r : P
simp : ⟪NormedSpace.normalize v, q -ᵥ p⟫ + ⟪NormedSpace.normalize v, r -ᵥ q⟫ = ⟪NormedSpace.normalize v, r -ᵥ p⟫
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)
      ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) q : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) r : ℝ) =
    (((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) r

Tactic:
simp only [signedDist_apply_apply]

Premises used: signedDist_apply_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
v : V
p q r : P
rw : ⟪NormedSpace.normalize v, r -ᵥ q⟫ + ⟪NormedSpace.normalize v, q -ᵥ p⟫ = ⟪NormedSpace.normalize v, r -ᵥ p⟫
rw₁ : ⟪NormedSpace.normalize v, r -ᵥ q + (q -ᵥ p)⟫ = ⟪NormedSpace.normalize v, r -ᵥ p⟫
rw₂ rw₃ : ⟪NormedSpace.normalize v, r -ᵥ p⟫ = ⟪NormedSpace.normalize v, r -ᵥ p⟫
⊢ ⟪NormedSpace.normalize v, q -ᵥ p⟫ + ⟪NormedSpace.normalize v, r -ᵥ q⟫ = ⟪NormedSpace.normalize v, r -ᵥ p⟫

Tactic:
rw [add_comm, ← inner_add_right, vsub_add_vsub_cancel]

Premises used: vsub_add_vsub_cancel, add_comm, 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
p q r : P
rw :
  (((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) r : ℝ)
      ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) r : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)
rw₁ rw₂ :
  Eq (α := ℝ) ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)
    ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)
⊢ HSub.hSub (α := ℝ) (β := ℝ) ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)
      ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) r : ℝ) =
    (((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) r : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q

Tactic:
rw [sub_eq_iff_eq_add', signedDist_triangle]

Premises used: signedDist_triangle, sub_eq_iff_eq_add'
-- 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
p q r : P
rw :
  (((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) r =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)
      ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) q : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) r : ℝ)
rw₁ rw₂ :
  Eq (α := ℝ) ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) r : ℝ)
    ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) r : ℝ)
⊢ HSub.hSub (α := ℝ) (β := ℝ) ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) r : ℝ)
      ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) q : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) r : ℝ) =
    (((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q

Tactic:
rw [sub_eq_iff_eq_add, signedDist_triangle]

Premises used: signedDist_triangle, sub_eq_iff_eq_add
-- 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 w : V
p q : P
⊢ (((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) (w +ᵥ p) : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q =
    HAdd.hAdd (β := ℝ) (-⟪NormedSpace.normalize v, w⟫)
      ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)

Tactic:
simp [signedDist_linear_apply_apply]

Premises used: signedDist_linear_apply_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
v w : V
p q : P
⊢ (((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) (w +ᵥ q) =
    HAdd.hAdd (β := ℝ) ⟪NormedSpace.normalize v, w⟫
      ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)

Tactic:
simp [signedDist_apply_linear_apply]

Premises used: signedDist_apply_linear_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
v w : V
p q : P
rw :
  HAdd.hAdd (β := ℝ) (-⟪NormedSpace.normalize v, w⟫)
      ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ) =
    (((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) (-w +ᵥ q)
rw₁ :
  HAdd.hAdd (β := ℝ) (-⟪NormedSpace.normalize v, w⟫)
      ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ) =
    HAdd.hAdd (β := ℝ) ⟪NormedSpace.normalize v, -w⟫
      ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)
rw₂ rw₃ :
  HAdd.hAdd (β := ℝ) (-⟪NormedSpace.normalize v, w⟫)
      ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ) =
    HAdd.hAdd (β := ℝ) (-⟪NormedSpace.normalize v, w⟫)
      ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)
⊢ Eq (α := ℝ) ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) (w +ᵥ p) : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)
    ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) (-w +ᵥ q) : ℝ)

Tactic:
rw [signedDist_vadd_left, signedDist_vadd_right, inner_neg_right]

Premises used: inner_neg_right, signedDist_vadd_right, signedDist_vadd_left
-- 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 w : V
p q : P
rw :
  Eq (α := ℝ) ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) (w +ᵥ q) : ℝ)
    ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) (- -w +ᵥ q) : ℝ)
rw₁ rw₂ :
  Eq (α := ℝ) ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) (w +ᵥ q) : ℝ)
    ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) (w +ᵥ q) : ℝ)
⊢ Eq (α := ℝ) ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) (w +ᵥ q) : ℝ)
    ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) (-w +ᵥ p) : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)

Tactic:
rw [signedDist_vadd_left_swap, neg_neg]

Premises used: neg_neg, signedDist_vadd_left_swap
-- 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 w : V
p q : P
rw :
  Eq (α := ℝ) ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) (-w +ᵥ w +ᵥ q) : ℝ)
    ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)
rw₁ rw₂ :
  Eq (α := ℝ) ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)
    ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)
⊢ Eq (α := ℝ) ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) (w +ᵥ p) : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) (w +ᵥ q) : ℝ)
    ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)

Tactic:
rw [signedDist_vadd_left_swap, neg_vadd_vadd]

Premises used: signedDist_vadd_left_swap, neg_vadd_vadd
-- 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
p q : P
h : ⟪v, p -ᵥ q⟫ = 0
h₁ :
  ∀ (r : P),
    Eq (α := ℝ) ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) r : ℝ)
      ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) q : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) r : ℝ)
⊢ Eq (α := P →ᴬ[ℝ] ℝ) ((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ)
    ((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) q : P →ᴬ[ℝ] ℝ)

Tactic:
ext r
-- 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
p q : P
h : ⟪v, p -ᵥ q⟫ = 0
r : P
⊢ Eq (α := ℝ) ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) r : ℝ)
    ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) q : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) r : ℝ)

Tactic:
simpa [NormedSpace.normalize, real_inner_smul_left, h] using signedDist_vadd_left v (p -ᵥ q) q r

Premises used: VSub.vsub, signedDist_vadd_left, real_inner_smul_left, NormedSpace.normalize
-- 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
p q r : P
h : ⟪v, q -ᵥ r⟫ = 0
⊢ Eq (α := ℝ) ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)
    ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) r : ℝ)

Tactic:
simpa [NormedSpace.normalize, real_inner_smul_left, h] using signedDist_vadd_right v (q -ᵥ r) p r

Premises used: signedDist_vadd_right, VSub.vsub, real_inner_smul_left, NormedSpace.normalize
-- 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
p q : P
h : ⟪v, q -ᵥ p⟫ = 0
⊢ Eq (α := ℝ) ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ) (0 : ℝ)

Tactic:
simpa using signedDist_right_congr p h

Premises used: signedDist_right_congr
-- 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
p q : P
rw : |⟪NormedSpace.normalize v, q -ᵥ p⟫| ≤ dist p q
⊢ |(((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q| ≤ dist p q

Tactic:
rw [signedDist_apply_apply]

Premises used: signedDist_apply_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
v : V
p q : P
pos : ∀ (h : v = 0), |⟪NormedSpace.normalize v, q -ᵥ p⟫| ≤ dist p q
neg : ∀ (h : ¬v = 0), |⟪NormedSpace.normalize v, q -ᵥ p⟫| ≤ dist p q
⊢ |⟪NormedSpace.normalize v, q -ᵥ p⟫| ≤ dist p q

Tactic:
by_cases h : v = 0
-- 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
p q : P
h : v = 0
⊢ |⟪NormedSpace.normalize v, q -ᵥ p⟫| ≤ dist p q

Tactic:
simp [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
v : V
p q : P
h : ¬v = 0
neg : ‖NormedSpace.normalize v‖ * ‖q -ᵥ p‖ ≤ dist p q
⊢ |⟪NormedSpace.normalize v, q -ᵥ p⟫| ≤ dist p q

Tactic:
grw [abs_real_inner_le_norm]

Premises used: abs_real_inner_le_norm
-- 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
p q : P
h : ¬v = 0
⊢ ‖NormedSpace.normalize v‖ * ‖q -ᵥ p‖ ≤ dist p q

Tactic:
simp [norm_normalize h, dist_eq_norm_vsub']

Premises used: dist_eq_norm_vsub', NormedSpace.norm_normalize