awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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) : ℝ)
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]
-- 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 →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) (w +ᵥ q) : ℝ)
    ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) (-w +ᵥ p) : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)
have rw : Eq (α := ℝ) ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) (w +ᵥ q) : ℝ)
  ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) (- -w +ᵥ q) : ℝ)
Tactic: rw [signedDist_vadd_left_swap, neg_neg]
-- 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 :
  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 : ℝ)
have rw₁ : Eq (α := ℝ) ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) (w +ᵥ q) : ℝ)
  ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) (w +ᵥ q) : ℝ)
Tactic: rw [signedDist_vadd_left_swap, neg_neg]
-- 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) → ℝ) (w +ᵥ q) : ℝ)
    ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)
have rw : Eq (α := ℝ) ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) (-w +ᵥ w +ᵥ q) : ℝ)
  ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)
Tactic: rw [signedDist_vadd_left_swap, neg_vadd_vadd]
-- 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 :
  Eq (α := ℝ) ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) (-w +ᵥ w +ᵥ 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 : ℝ)
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 [signedDist_vadd_left_swap, neg_vadd_vadd]
-- 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
h : ⟪v, p -ᵥ q⟫ = 0
⊢ Eq (α := P →ᴬ[ℝ] ℝ) ((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ)
    ((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) q : P →ᴬ[ℝ] ℝ)
have h₁ : ∀ (r : P),
  Eq (α := ℝ) ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) r : ℝ)
    ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) q : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) r : ℝ)
Tactic: ext r
-- 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
⊢ |(((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q| ≤ dist p q
have rw : |⟪NormedSpace.normalize v, q -ᵥ p⟫| ≤ dist p q
Tactic: rw [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
⊢ |⟪NormedSpace.normalize v, q -ᵥ p⟫| ≤ dist p q
have pos : ∀ (h : v = 0), |⟪NormedSpace.normalize v, q -ᵥ p⟫| ≤ dist p q
Tactic: by_cases h : v = 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
pos : ∀ (h : v = 0), |⟪NormedSpace.normalize v, q -ᵥ p⟫| ≤ dist p q
⊢ |⟪NormedSpace.normalize v, q -ᵥ p⟫| ≤ dist p q
have neg : ∀ (h : ¬v = 0), |⟪NormedSpace.normalize v, q -ᵥ p⟫| ≤ dist p q
Tactic: by_cases h : v = 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
h : ¬v = 0
⊢ |⟪NormedSpace.normalize v, q -ᵥ p⟫| ≤ dist p q
have neg : ‖NormedSpace.normalize v‖ * ‖q -ᵥ p‖ ≤ dist p q
Tactic: grw [abs_real_inner_le_norm]
-- 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
⊢ |(((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q| = dist p q ↔
    Membership.mem (γ := Submodule ℝ V) (ℝ ∙ v) (q -ᵥ p)
have rw : |(((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q| = dist p q ↔ ∃ (a : ℝ), a • v = q -ᵥ p
Tactic: rw [Submodule.mem_span_singleton]
-- 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
⊢ |(((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q| = dist p q ↔ ∃ (a : ℝ), a • v = q -ᵥ p
have rw : ‖v‖⁻¹ * |⟪v, q -ᵥ p⟫| = ‖q -ᵥ p‖ ↔ ∃ (a : ℝ), a • v = q -ᵥ p
Tactic: rw [signedDist_apply_apply, dist_eq_norm_vsub', NormedSpace.normalize, real_inner_smul_left,
    abs_mul, abs_inv, abs_norm]
-- 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
⊢ ‖v‖⁻¹ * |⟪v, q -ᵥ p⟫| = ‖q -ᵥ p‖ ↔ ∃ (a : ℝ), a • v = q -ᵥ p
have pos : ∀ (h : v = 0), ‖v‖⁻¹ * |⟪v, q -ᵥ p⟫| = ‖q -ᵥ p‖ ↔ ∃ (a : ℝ), a • v = q -ᵥ p
Tactic: by_cases h : v = 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
pos : ∀ (h : v = 0), ‖v‖⁻¹ * |⟪v, q -ᵥ p⟫| = ‖q -ᵥ p‖ ↔ ∃ (a : ℝ), a • v = q -ᵥ p
⊢ ‖v‖⁻¹ * |⟪v, q -ᵥ p⟫| = ‖q -ᵥ p‖ ↔ ∃ (a : ℝ), a • v = q -ᵥ p
have neg : ∀ (h : ¬v = 0), ‖v‖⁻¹ * |⟪v, q -ᵥ p⟫| = ‖q -ᵥ p‖ ↔ ∃ (a : ℝ), a • v = q -ᵥ p
Tactic: by_cases h : v = 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
h : ¬v = 0
⊢ ‖v‖⁻¹ * |⟪v, q -ᵥ p⟫| = ‖q -ᵥ p‖ ↔ ∃ (a : ℝ), a • v = q -ᵥ p
have neg : |⟪v, q -ᵥ p⟫| = ‖v‖ * ‖q -ᵥ p‖ ↔ ∃ (a : ℝ), a • v = q -ᵥ p
Tactic: rw [inv_mul_eq_iff_eq_mul₀ (by positivity)]
-- 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
h : ¬v = 0
⊢ |⟪v, q -ᵥ p⟫| = ‖v‖ * ‖q -ᵥ p‖ ↔ ∃ (a : ℝ), a • v = q -ᵥ p
have neg : (v = 0 ∨ ∃ (r : ℝ), q -ᵥ p = r • v) ↔ ∃ (a : ℝ), a • v = q -ᵥ p
Tactic: rw [← Real.norm_eq_abs, ((norm_inner_eq_norm_tfae ℝ v (q -ᵥ p)).out 0 2 :)]
-- 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
⊢ (((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q = dist p q ↔
    Membership.mem (γ := Submodule ℝ≥0 V) (ℝ≥0 ∙ v) (q -ᵥ p)
have rw : (((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q = dist p q ↔ ∃ (a : ℝ≥0), a • v = q -ᵥ p
Tactic: rw [Submodule.mem_span_singleton]
-- 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
⊢ (((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q = dist p q ↔ ∃ (a : ℝ≥0), a • v = q -ᵥ p
have rw : ‖v‖⁻¹ * ⟪v, q -ᵥ p⟫ = ‖q -ᵥ p‖ ↔ ∃ (a : ℝ≥0), a • v = q -ᵥ p
Tactic: rw [signedDist_apply_apply, dist_eq_norm_vsub', NormedSpace.normalize, 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
⊢ ‖v‖⁻¹ * ⟪v, q -ᵥ p⟫ = ‖q -ᵥ p‖ ↔ ∃ (a : ℝ≥0), a • v = q -ᵥ p
have pos : ∀ (h : v = 0), ‖v‖⁻¹ * ⟪v, q -ᵥ p⟫ = ‖q -ᵥ p‖ ↔ ∃ (a : ℝ≥0), a • v = q -ᵥ p
Tactic: by_cases h : v = 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
pos : ∀ (h : v = 0), ‖v‖⁻¹ * ⟪v, q -ᵥ p⟫ = ‖q -ᵥ p‖ ↔ ∃ (a : ℝ≥0), a • v = q -ᵥ p
⊢ ‖v‖⁻¹ * ⟪v, q -ᵥ p⟫ = ‖q -ᵥ p‖ ↔ ∃ (a : ℝ≥0), a • v = q -ᵥ p
have neg : ∀ (h : ¬v = 0), ‖v‖⁻¹ * ⟪v, q -ᵥ p⟫ = ‖q -ᵥ p‖ ↔ ∃ (a : ℝ≥0), a • v = q -ᵥ p
Tactic: by_cases h : v = 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
h : ¬v = 0
⊢ ‖v‖⁻¹ * ⟪v, q -ᵥ p⟫ = ‖q -ᵥ p‖ ↔ ∃ (a : ℝ≥0), a • v = q -ᵥ p
have neg : ⟪v, q -ᵥ p⟫ = ‖v‖ * ‖q -ᵥ p‖ ↔ ∃ (a : ℝ≥0), a • v = q -ᵥ p
Tactic: rw [inv_mul_eq_iff_eq_mul₀ (by positivity)]
-- 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
h : ¬v = 0
⊢ ⟪v, q -ᵥ p⟫ = ‖v‖ * ‖q -ᵥ p‖ ↔ ∃ (a : ℝ≥0), a • v = q -ᵥ p
have neg : ‖q -ᵥ p‖ • v = ‖v‖ • (q -ᵥ p) ↔ ∃ (a : ℝ≥0), a • v = q -ᵥ p
Tactic: rw [inner_eq_norm_mul_iff_real]
-- 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
h : ¬v = 0
⊢ ‖q -ᵥ p‖ • v = ‖v‖ • (q -ᵥ p) ↔ ∃ (a : ℝ≥0), a • v = q -ᵥ p
have neg : ‖q -ᵥ p‖ • v = ‖v‖ • (q -ᵥ p) ↔ ∃ (a : ℝ≥0), (↑a : ℝ) • v = q -ᵥ p
Tactic: simp only [smul_def]
-- 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
h : ¬v = 0
⊢ ‖q -ᵥ p‖ • v = ‖v‖ • (q -ᵥ p) ↔ ∃ (a : ℝ≥0), (↑a : ℝ) • v = q -ᵥ p
have neg : ∀ (h : ‖q -ᵥ p‖ • v = ‖v‖ • (q -ᵥ p)), ∃ (a : ℝ≥0), (↑a : ℝ) • v = q -ᵥ p
Tactic: refine ⟨fun h => ?_, fun ⟨c, 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 : V
p q : P
h : ¬v = 0
neg : ∀ (h : ‖q -ᵥ p‖ • v = ‖v‖ • (q -ᵥ p)), ∃ (a : ℝ≥0), (↑a : ℝ) • v = q -ᵥ p
⊢ ‖q -ᵥ p‖ • v = ‖v‖ • (q -ᵥ p) ↔ ∃ (a : ℝ≥0), (↑a : ℝ) • v = q -ᵥ p
have neg₁ : (∃ (a : ℝ≥0), (↑a : ℝ) • v = q -ᵥ p) → ∀ (c : ℝ≥0) (h : (↑c : ℝ) • v = q -ᵥ p), ‖q -ᵥ p‖ • v = ‖v‖ • (q -ᵥ p)
Tactic: refine ⟨fun h => ?_, fun ⟨c, 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 : V
p q : P
h_1 : ¬v = 0
h : ‖q -ᵥ p‖ • v = ‖v‖ • (q -ᵥ p)
⊢ ∃ (a : ℝ≥0), (↑a : ℝ) • v = q -ᵥ p
have neg : ∃ (x : ℝ), 0 ≤ x ∧ x • v = q -ᵥ p
Tactic: simp only [NNReal.exists, coe_mk, exists_prop]
-- 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
h_1 : ¬v = 0
h : ‖q -ᵥ p‖ • v = ‖v‖ • (q -ᵥ p)
⊢ ∃ (x : ℝ), 0 ≤ x ∧ x • v = q -ᵥ p
have h₁ : 0 ≤ ‖v‖⁻¹ * ‖q -ᵥ p‖ ∧ (‖v‖⁻¹ * ‖q -ᵥ p‖) • v = q -ᵥ p
Tactic: use ‖v‖⁻¹ * ‖q -ᵥ p‖
-- 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
h_1 : ¬v = 0
h : ‖q -ᵥ p‖ • v = ‖v‖ • (q -ᵥ p)
⊢ 0 ≤ ‖v‖⁻¹ * ‖q -ᵥ p‖ ∧ (‖v‖⁻¹ * ‖q -ᵥ p‖) • v = q -ᵥ p
have h₁ : 0 ≤ ‖v‖⁻¹ * ‖q -ᵥ p‖
Tactic: constructor
-- 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
h_1 : ¬v = 0
h : ‖q -ᵥ p‖ • v = ‖v‖ • (q -ᵥ p)
h₁ : 0 ≤ ‖v‖⁻¹ * ‖q -ᵥ p‖
⊢ 0 ≤ ‖v‖⁻¹ * ‖q -ᵥ p‖ ∧ (‖v‖⁻¹ * ‖q -ᵥ p‖) • v = q -ᵥ p
have h₂ : (‖v‖⁻¹ * ‖q -ᵥ p‖) • v = q -ᵥ p
Tactic: constructor
-- 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
h_1 : ¬v = 0
h : ‖q -ᵥ p‖ • v = ‖v‖ • (q -ᵥ p)
⊢ (‖v‖⁻¹ * ‖q -ᵥ p‖) • v = q -ᵥ p
have h₁ : ‖v‖⁻¹ • ‖q -ᵥ p‖ • v = q -ᵥ p
Tactic: rw [← smul_smul, h, smul_smul, inv_mul_cancel₀ (by positivity), one_smul]
-- 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
h_1 : ¬v = 0
h : ‖q -ᵥ p‖ • v = ‖v‖ • (q -ᵥ p)
h₁ : ‖v‖⁻¹ • ‖q -ᵥ p‖ • v = q -ᵥ p
⊢ (‖v‖⁻¹ * ‖q -ᵥ p‖) • v = q -ᵥ p
have h₂ : ‖v‖⁻¹ • ‖v‖ • (q -ᵥ p) = q -ᵥ p
Tactic: rw [← smul_smul, h, smul_smul, inv_mul_cancel₀ (by positivity), one_smul]
-- 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
h_1 : ¬v = 0
h : ‖q -ᵥ p‖ • v = ‖v‖ • (q -ᵥ p)
h₁ : ‖v‖⁻¹ • ‖q -ᵥ p‖ • v = q -ᵥ p
h₂ : ‖v‖⁻¹ • ‖v‖ • (q -ᵥ p) = q -ᵥ p
⊢ (‖v‖⁻¹ * ‖q -ᵥ p‖) • v = q -ᵥ p
have h₃ : (‖v‖⁻¹ * ‖v‖) • (q -ᵥ p) = q -ᵥ p
Tactic: rw [← smul_smul, h, smul_smul, inv_mul_cancel₀ (by positivity), one_smul]
-- 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
h_1 : ¬v = 0
h : ‖q -ᵥ p‖ • v = ‖v‖ • (q -ᵥ p)
h₁ : ‖v‖⁻¹ • ‖q -ᵥ p‖ • v = q -ᵥ p
h₂ : ‖v‖⁻¹ • ‖v‖ • (q -ᵥ p) = q -ᵥ p
h₃ : (‖v‖⁻¹ * ‖v‖) • (q -ᵥ p) = q -ᵥ p
⊢ (‖v‖⁻¹ * ‖q -ᵥ p‖) • v = q -ᵥ p
have h₄ : HSMul.hSMul (α := ℝ) 1 (q -ᵥ p) = q -ᵥ p
Tactic: rw [← smul_smul, h, smul_smul, inv_mul_cancel₀ (by positivity), one_smul]
-- 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
h_1 : ¬v = 0
h : ‖q -ᵥ p‖ • v = ‖v‖ • (q -ᵥ p)
h₁ : ‖v‖⁻¹ • ‖q -ᵥ p‖ • v = q -ᵥ p
h₂ : ‖v‖⁻¹ • ‖v‖ • (q -ᵥ p) = q -ᵥ p
h₃ : (‖v‖⁻¹ * ‖v‖) • (q -ᵥ p) = q -ᵥ p
h₄ : HSMul.hSMul (α := ℝ) 1 (q -ᵥ p) = q -ᵥ p
⊢ (‖v‖⁻¹ * ‖q -ᵥ p‖) • v = q -ᵥ p
have h₅ : q -ᵥ p = q -ᵥ p
Tactic: rw [← smul_smul, h, smul_smul, inv_mul_cancel₀ (by positivity), one_smul]
-- 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
h_1 : ¬v = 0
h_2 : ∃ (a : ℝ≥0), (↑a : ℝ) • v = q -ᵥ p
c : ℝ≥0
h : (↑c : ℝ) • v = q -ᵥ p
⊢ ‖q -ᵥ p‖ • v = ‖v‖ • (q -ᵥ p)
have neg : (‖v‖ * ‖(↑c : ℝ)‖) • v = (‖v‖ * (↑c : ℝ)) • v
Tactic: rw [← h, norm_smul, smul_smul, mul_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
p q : P
⊢ (((signedDist (q -ᵥ p) : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q = dist p q
have rw : Membership.mem (γ := Submodule NNReal V) (NNReal ∙ (q -ᵥ p)) (q -ᵥ p)
Tactic: rw [signedDist_eq_dist_iff_vsub_mem_span]
-- 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
p q : P
⊢ (((signedDist (p -ᵥ q) : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q = -dist p q
have rw : (((signedDist (q -ᵥ p) : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q = dist p q
Tactic: rw [← neg_eq_iff_eq_neg, ← signedDist_neg, neg_vsub_eq_vsub_rev]
-- 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
c₁ c₂ : ℝ
⊢ (((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) ((AffineMap.lineMap p q : (a : ℝ) → P) c₁) : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ)
      ((AffineMap.lineMap p q : (a : ℝ) → P) c₂ : P) =
    HMul.hMul (β := ℝ) (c₂ - c₁) ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)
have trans : (((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) ((AffineMap.lineMap p q : (a : ℝ) → P) c₁) : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ)
    ((AffineMap.lineMap p q : (a : ℝ) → P) c₂ : P) =
  HMul.hMul (β := ℝ) c₂ ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ) +
    HMul.hMul (β := ℝ) c₁ ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) q : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) p : ℝ)
Tactic: trans c₂ * signedDist v p q + c₁ * signedDist v q p
-- 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
c₁ c₂ : ℝ
trans :
  (((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) ((AffineMap.lineMap p q : (a : ℝ) → P) c₁) : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ)
      ((AffineMap.lineMap p q : (a : ℝ) → P) c₂ : P) =
    HMul.hMul (β := ℝ) c₂ ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ) +
      HMul.hMul (β := ℝ) c₁ ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) q : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) p : ℝ)
⊢ (((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) ((AffineMap.lineMap p q : (a : ℝ) → P) c₁) : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ)
      ((AffineMap.lineMap p q : (a : ℝ) → P) c₂ : P) =
    HMul.hMul (β := ℝ) (c₂ - c₁) ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)
have trans₁ : HMul.hMul (β := ℝ) c₂ ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ) +
    HMul.hMul (β := ℝ) c₁ ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) q : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) p : ℝ) =
  HMul.hMul (β := ℝ) (c₂ - c₁) ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)
Tactic: trans c₂ * signedDist v p q + c₁ * signedDist v q p
-- 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
c₁ c₂ : ℝ
⊢ HMul.hMul (β := ℝ) c₂ ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ) +
      HMul.hMul (β := ℝ) c₁ ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) q : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) p : ℝ) =
    HMul.hMul (β := ℝ) (c₂ - c₁) ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)
have rw : HMul.hMul (β := ℝ) c₂ ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ) +
    HMul.hMul (β := ℝ) c₁ ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) q : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) p : ℝ) =
  HMul.hMul (β := ℝ) c₂ ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ) -
    HMul.hMul (β := ℝ) c₁ ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)
Tactic: rw [sub_mul, ← signedDist_anticomm v p, mul_neg, sub_eq_add_neg]
-- 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
c₁ c₂ : ℝ
rw :
  HMul.hMul (β := ℝ) c₂ ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ) +
      HMul.hMul (β := ℝ) c₁ ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) q : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) p : ℝ) =
    HMul.hMul (β := ℝ) c₂ ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ) -
      HMul.hMul (β := ℝ) c₁ ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)
⊢ HMul.hMul (β := ℝ) c₂ ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ) +
      HMul.hMul (β := ℝ) c₁ ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) q : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) p : ℝ) =
    HMul.hMul (β := ℝ) (c₂ - c₁) ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)
have rw₁ : HMul.hMul (β := ℝ) c₂ ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ) +
    HMul.hMul (β := ℝ) c₁ (-(((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ) =
  HMul.hMul (β := ℝ) c₂ ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ) -
    HMul.hMul (β := ℝ) c₁ ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)
Tactic: rw [sub_mul, ← signedDist_anticomm v p, mul_neg, sub_eq_add_neg]