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
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
⊢ 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
have rw₃ : Eq.{u_1 + 1} (α := 𝕜) 0 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 _ _)]
-- 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
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.{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)
have 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)
Tactic: rw [eq_comm]
-- 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
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.{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)
have this : (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
-- 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
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₂
⊢ Eq (α := AffineSubspace 𝕜 P) (affineSpan 𝕜 (Set.range s₁.points)) (affineSpan 𝕜 (Set.range s₂.points))
have rw : Eq (α := AffineSubspace 𝕜 P) (affineSpan 𝕜 (Set.range s₂.points)) (affineSpan 𝕜 (Set.range s₂.points))
Tactic: rw [h]
-- 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 : Simplex 𝕜 P 0
p : P
⊢ (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan 𝕜 (Set.range s.points))) p) : P) = s.points 0
have rw : (↑((orthogonalProjection (affineSpan 𝕜 (Set.range s.points)) : (a : P) → ↥(affineSpan 𝕜 (Set.range s.points))) p) : P) =
  s.points 0
Tactic: rw [orthogonalProjectionSpan]
-- 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 : Simplex 𝕜 P 0
p : P
⊢ (↑((orthogonalProjection (affineSpan 𝕜 (Set.range s.points)) : (a : P) → ↥(affineSpan 𝕜 (Set.range s.points))) p) :
      P) =
    s.points 0
have h : Set.range s.points = {s.points 0}
Tactic: convert! orthogonalProjection_affineSpan_singleton _ _
-- 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
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₂)
    ((↑(((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₂)
have simp_rw : Eq.{u_5 + 1} (α := P₂)
  ((↑((orthogonalProjection (affineSpan 𝕜 (Set.range (s.map f.toAffineMap sorry).points)) :
            (a : P₂) → ↥(affineSpan 𝕜 (Set.range (s.map f.toAffineMap sorry).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: simp_rw [orthogonalProjectionSpan]
-- 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
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 (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₂)
have h : affineSpan 𝕜 (Set.range (s.map f.toAffineMap sorry).points) =
  AffineSubspace.map f.toAffineMap (affineSpan 𝕜 (Set.range s.points))
Tactic: convert! orthogonalProjection_map (affineSpan 𝕜 (Set.range s.points)) f 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
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)
have rw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: rw [eq_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.SignedDist (goal)
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
⊢ 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⟫)
have 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 :
      ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.SignedDist (goal)
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
⊢ ContinuousAffineMap.const ℝ P ⟪-NormedSpace.normalize v, r • x⟫ =
    HSMul.hSMul (α := ℝ) (β := P →ᴬ[ℝ] ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ)
      (ContinuousAffineMap.const ℝ P ⟪-NormedSpace.normalize v, x⟫)
have 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 :
      ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.SignedDist (goal)
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
⊢ 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)))
have 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' := sorry,
                    map_smul' := sorry : 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: ext q
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.SignedDist (goal)
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 →ₗ[ℝ] ℝ)
    (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))
have 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))
Tactic: change (innerₗ V (normalize v)).comp (LinearMap.id - 0) = _
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.SignedDist (goal)
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 : ℝ
⊢ (((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 : ℝ)
have simp : ⟪NormedSpace.normalize (r • v), q -ᵥ p⟫ =
  (↑((SignType.sign : (a : ℝ) → SignType) r) : ℝ) * ⟪NormedSpace.normalize v, q -ᵥ p⟫
Tactic: simp only [signedDist_apply_apply]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.SignedDist (goal)
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 : ℝ
⊢ ⟪NormedSpace.normalize (r • v), q -ᵥ p⟫ =
    (↑((SignType.sign : (a : ℝ) → SignType) r) : ℝ) * ⟪NormedSpace.normalize v, q -ᵥ p⟫
have rw : ⟪HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) r) : ℝ) (NormedSpace.normalize v), q -ᵥ p⟫ =
  (↑((SignType.sign : (a : ℝ) → SignType) r) : ℝ) * ⟪NormedSpace.normalize v, q -ᵥ p⟫
Tactic: rw [normalize_smul, real_inner_smul_left]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.SignedDist (goal)
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⟫
⊢ ⟪NormedSpace.normalize (r • v), q -ᵥ p⟫ =
    (↑((SignType.sign : (a : ℝ) → SignType) r) : ℝ) * ⟪NormedSpace.normalize v, q -ᵥ p⟫
have rw₁ : (↑((SignType.sign : (a : ℝ) → SignType) r) : ℝ) * ⟪NormedSpace.normalize v, q -ᵥ p⟫ =
  (↑((SignType.sign : (a : ℝ) → SignType) r) : ℝ) * ⟪NormedSpace.normalize v, q -ᵥ p⟫
Tactic: rw [normalize_smul, real_inner_smul_left]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.SignedDist (goal)
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
⊢ Eq (α := P →ᵃ[ℝ] P →ᴬ[ℝ] ℝ) (signedDist v) (signedDist w)
have obtain : ∀ r > 0, r • v = w → Eq (α := P →ᵃ[ℝ] P →ᴬ[ℝ] ℝ) (signedDist v) (signedDist w)
Tactic: obtain ⟨r, _, _⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.SignedDist (goal)
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
⊢ Eq (α := P →ᵃ[ℝ] P →ᴬ[ℝ] ℝ) (signedDist v) (signedDist w)
have 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 : ℝ)
Tactic: ext p q
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.SignedDist (goal)
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
⊢ 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
have simp : ⟪NormedSpace.normalize v, q -ᵥ p⟫ + ⟪NormedSpace.normalize v, r -ᵥ q⟫ = ⟪NormedSpace.normalize v, r -ᵥ p⟫
Tactic: simp only [signedDist_apply_apply]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.SignedDist (goal)
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
⊢ ⟪NormedSpace.normalize v, q -ᵥ p⟫ + ⟪NormedSpace.normalize v, r -ᵥ q⟫ = ⟪NormedSpace.normalize v, r -ᵥ p⟫
have rw : ⟪NormedSpace.normalize v, r -ᵥ q⟫ + ⟪NormedSpace.normalize v, q -ᵥ p⟫ = ⟪NormedSpace.normalize v, r -ᵥ p⟫
Tactic: rw [add_comm, ← inner_add_right, vsub_add_vsub_cancel]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.SignedDist (goal)
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⟫
⊢ ⟪NormedSpace.normalize v, q -ᵥ p⟫ + ⟪NormedSpace.normalize v, r -ᵥ q⟫ = ⟪NormedSpace.normalize v, r -ᵥ p⟫
have rw₁ : ⟪NormedSpace.normalize v, r -ᵥ q + (q -ᵥ p)⟫ = ⟪NormedSpace.normalize v, r -ᵥ p⟫
Tactic: rw [add_comm, ← inner_add_right, vsub_add_vsub_cancel]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.SignedDist (goal)
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⟫
⊢ ⟪NormedSpace.normalize v, q -ᵥ p⟫ + ⟪NormedSpace.normalize v, r -ᵥ q⟫ = ⟪NormedSpace.normalize v, r -ᵥ p⟫
have rw₂ : ⟪NormedSpace.normalize v, r -ᵥ p⟫ = ⟪NormedSpace.normalize v, r -ᵥ p⟫
Tactic: rw [add_comm, ← inner_add_right, vsub_add_vsub_cancel]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.SignedDist (goal)
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
⊢ 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
have 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 : ℝ)
Tactic: rw [sub_eq_iff_eq_add', signedDist_triangle]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.SignedDist (goal)
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 : ℝ)
⊢ 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
have rw₁ : Eq (α := ℝ) ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)
  ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)
Tactic: rw [sub_eq_iff_eq_add', signedDist_triangle]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.SignedDist (goal)
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
⊢ 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
have 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 : ℝ)
Tactic: rw [sub_eq_iff_eq_add, signedDist_triangle]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.SignedDist (goal)
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 : ℝ)
⊢ 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
have rw₁ : Eq (α := ℝ) ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) r : ℝ)
  ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) r : ℝ)
Tactic: rw [sub_eq_iff_eq_add, signedDist_triangle]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.SignedDist (goal)
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
⊢ Eq (α := ℝ) ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) (w +ᵥ p) : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)
    ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) (-w +ᵥ q) : ℝ)
have 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)
Tactic: rw [signedDist_vadd_left, signedDist_vadd_right, inner_neg_right]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.SignedDist (goal)
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)
⊢ Eq (α := ℝ) ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) (w +ᵥ p) : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)
    ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) (-w +ᵥ q) : ℝ)
have 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 : ℝ)
Tactic: rw [signedDist_vadd_left, signedDist_vadd_right, inner_neg_right]