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 q : P
⊢ (((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q ≤ dist p q

Tactic:
le_trans (le_abs_self _) (abs_signedDist_le_dist _ _ _)

Premises used: le_abs_self, abs_signedDist_le_dist, le_trans
-- 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 : |(((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q| = dist p q ↔ ∃ (a : ℝ), a • v = q -ᵥ p
⊢ |(((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q| = dist p q ↔
    Membership.mem (γ := Submodule ℝ V) (ℝ ∙ v) (q -ᵥ p)

Tactic:
rw [Submodule.mem_span_singleton]

Premises used: Submodule.mem_span_singleton
-- 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 : ‖v‖⁻¹ * |⟪v, q -ᵥ p⟫| = ‖q -ᵥ p‖ ↔ ∃ (a : ℝ), a • v = q -ᵥ p
⊢ |(((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q| = dist p q ↔ ∃ (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]

Premises used: signedDist_apply_apply, abs_inv, abs_mul, dist_eq_norm_vsub', real_inner_smul_left, abs_norm, 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
pos : ∀ (h : v = 0), ‖v‖⁻¹ * |⟪v, q -ᵥ p⟫| = ‖q -ᵥ p‖ ↔ ∃ (a : ℝ), a • v = q -ᵥ p
neg : ∀ (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

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
⊢ ‖v‖⁻¹ * |⟪v, q -ᵥ p⟫| = ‖q -ᵥ p‖ ↔ ∃ (a : ℝ), a • v = q -ᵥ p

Tactic:
simp [h, eq_comm (a := (0 : ℝ)), eq_comm (a := (0 : V))]

Premises used: eq_comm
-- 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
⊢ ‖v‖ ≠ 0

Tactic:
positivity
-- 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 : |⟪v, q -ᵥ p⟫| = ‖v‖ * ‖q -ᵥ p‖ ↔ ∃ (a : ℝ), a • v = q -ᵥ p
⊢ ‖v‖⁻¹ * |⟪v, q -ᵥ p⟫| = ‖q -ᵥ p‖ ↔ ∃ (a : ℝ), a • v = q -ᵥ p

Tactic:
rw [inv_mul_eq_iff_eq_mul₀ (by positivity)]

Premises used: inv_mul_eq_iff_eq_mul₀
-- 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 : (v = 0 ∨ ∃ (r : ℝ), q -ᵥ p = r • v) ↔ ∃ (a : ℝ), a • v = q -ᵥ p
⊢ |⟪v, q -ᵥ p⟫| = ‖v‖ * ‖q -ᵥ p‖ ↔ ∃ (a : ℝ), a • v = q -ᵥ p

Tactic:
rw [← Real.norm_eq_abs, ((norm_inner_eq_norm_tfae ℝ v (q -ᵥ p)).out 0 2 :)]

Premises used: Real, norm_inner_eq_norm_tfae, VSub.vsub, List.TFAE.out, OfNat.ofNat, Real.norm_eq_abs
-- 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
⊢ (v = 0 ∨ ∃ (r : ℝ), q -ᵥ p = r • v) ↔ ∃ (a : ℝ), a • v = q -ᵥ p

Tactic:
simp [h, eq_comm]

Premises used: eq_comm
-- 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 : (((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q = dist p q ↔ ∃ (a : ℝ≥0), a • v = q -ᵥ p
⊢ (((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q = dist p q ↔
    Membership.mem (γ := Submodule ℝ≥0 V) (ℝ≥0 ∙ v) (q -ᵥ p)

Tactic:
rw [Submodule.mem_span_singleton]

Premises used: Submodule.mem_span_singleton
-- 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 : ‖v‖⁻¹ * ⟪v, q -ᵥ p⟫ = ‖q -ᵥ p‖ ↔ ∃ (a : ℝ≥0), a • v = q -ᵥ p
⊢ (((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q = dist p q ↔ ∃ (a : ℝ≥0), a • v = q -ᵥ p

Tactic:
rw [signedDist_apply_apply, dist_eq_norm_vsub', NormedSpace.normalize, real_inner_smul_left]

Premises used: signedDist_apply_apply, dist_eq_norm_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
pos : ∀ (h : v = 0), ‖v‖⁻¹ * ⟪v, q -ᵥ p⟫ = ‖q -ᵥ p‖ ↔ ∃ (a : ℝ≥0), a • v = q -ᵥ p
neg : ∀ (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

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
⊢ ‖v‖⁻¹ * ⟪v, q -ᵥ p⟫ = ‖q -ᵥ p‖ ↔ ∃ (a : ℝ≥0), a • v = q -ᵥ p

Tactic:
simp [h, eq_comm (a := (0 : ℝ)), eq_comm (a := (0 : V))]

Premises used: eq_comm
-- 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 : ⟪v, q -ᵥ p⟫ = ‖v‖ * ‖q -ᵥ p‖ ↔ ∃ (a : ℝ≥0), a • v = q -ᵥ p
⊢ ‖v‖⁻¹ * ⟪v, q -ᵥ p⟫ = ‖q -ᵥ p‖ ↔ ∃ (a : ℝ≥0), a • v = q -ᵥ p

Tactic:
rw [inv_mul_eq_iff_eq_mul₀ (by positivity)]

Premises used: inv_mul_eq_iff_eq_mul₀
-- 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 : ‖q -ᵥ p‖ • v = ‖v‖ • (q -ᵥ p) ↔ ∃ (a : ℝ≥0), a • v = q -ᵥ p
⊢ ⟪v, q -ᵥ p⟫ = ‖v‖ * ‖q -ᵥ p‖ ↔ ∃ (a : ℝ≥0), a • v = q -ᵥ p

Tactic:
rw [inner_eq_norm_mul_iff_real]

Premises used: inner_eq_norm_mul_iff_real
-- 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 : ‖q -ᵥ p‖ • v = ‖v‖ • (q -ᵥ p) ↔ ∃ (a : ℝ≥0), (↑a : ℝ) • v = q -ᵥ p
⊢ ‖q -ᵥ p‖ • v = ‖v‖ • (q -ᵥ p) ↔ ∃ (a : ℝ≥0), a • v = q -ᵥ p

Tactic:
simp only [smul_def]

Premises used: NNReal.smul_def
-- 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
⊢ ‖q -ᵥ p‖ • v = ‖v‖ • (q -ᵥ p) ↔ ∃ (a : ℝ≥0), (↑a : ℝ) • v = q -ᵥ p

Tactic:
⟨fun h => ?_, fun ⟨c, h⟩ => ?_⟩

Premises used: Norm.norm, _private.0.signedDist_eq_dist_iff_vsub_mem_span.match_1, VSub.vsub, Iff.intro, HSMul.hSMul, Eq
-- 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 : ∀ (h : ‖q -ᵥ p‖ • v = ‖v‖ • (q -ᵥ p)), ∃ (a : ℝ≥0), (↑a : ℝ) • v = q -ᵥ p
neg₁ : (∃ (a : ℝ≥0), (↑a : ℝ) • v = q -ᵥ p) → ∀ (c : ℝ≥0) (h : (↑c : ℝ) • v = q -ᵥ p), ‖q -ᵥ p‖ • v = ‖v‖ • (q -ᵥ p)
⊢ ‖q -ᵥ p‖ • v = ‖v‖ • (q -ᵥ p) ↔ ∃ (a : ℝ≥0), (↑a : ℝ) • v = q -ᵥ p

Tactic:
refine ⟨fun h => ?_, fun ⟨c, 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_1 : ¬v = 0
h : ‖q -ᵥ p‖ • v = ‖v‖ • (q -ᵥ p)
neg : ∃ (x : ℝ), 0 ≤ x ∧ x • v = q -ᵥ p
⊢ ∃ (a : ℝ≥0), (↑a : ℝ) • v = q -ᵥ p

Tactic:
simp only [NNReal.exists, coe_mk, exists_prop]

Premises used: NNReal.coe_mk, exists_prop, NNReal.exists
-- 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_1 : ¬v = 0
h : ‖q -ᵥ p‖ • v = ‖v‖ • (q -ᵥ p)
h₁ : 0 ≤ ‖v‖⁻¹ * ‖q -ᵥ p‖ ∧ (‖v‖⁻¹ * ‖q -ᵥ p‖) • v = q -ᵥ p
⊢ ∃ (x : ℝ), 0 ≤ x ∧ x • v = q -ᵥ p

Tactic:
use ‖v‖⁻¹ * ‖q -ᵥ p‖
-- Module: Mathlib.Geometry.Euclidean.SignedDist
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
v : V
p q : P
h_1 : ¬v = 0
h : ‖q -ᵥ p‖ • v = ‖v‖ • (q -ᵥ p)
h₁ : 0 ≤ ‖v‖⁻¹ * ‖q -ᵥ p‖
h₂ : (‖v‖⁻¹ * ‖q -ᵥ p‖) • v = q -ᵥ p
⊢ 0 ≤ ‖v‖⁻¹ * ‖q -ᵥ p‖ ∧ (‖v‖⁻¹ * ‖q -ᵥ p‖) • v = q -ᵥ p

Tactic:
constructor
-- 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_1 : ¬v = 0
h : ‖q -ᵥ p‖ • v = ‖v‖ • (q -ᵥ p)
⊢ 0 ≤ ‖v‖⁻¹ * ‖q -ᵥ p‖

Tactic:
positivity
-- 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_1 : ¬v = 0
h : ‖q -ᵥ p‖ • v = ‖v‖ • (q -ᵥ p)
⊢ ‖v‖ ≠ 0

Tactic:
positivity
-- 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_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
h₅ h₆ : q -ᵥ p = q -ᵥ p
⊢ (‖v‖⁻¹ * ‖q -ᵥ p‖) • v = q -ᵥ p

Tactic:
rw [← smul_smul, h, smul_smul, inv_mul_cancel₀ (by positivity), one_smul]

Premises used: smul_smul, one_smul, inv_mul_cancel₀
-- 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_1 : ¬v = 0
h_2 : ∃ (a : ℝ≥0), (↑a : ℝ) • v = q -ᵥ p
c : ℝ≥0
h : (↑c : ℝ) • v = q -ᵥ p
neg : (‖v‖ * ‖(↑c : ℝ)‖) • v = (‖v‖ * (↑c : ℝ)) • v
⊢ ‖q -ᵥ p‖ • v = ‖v‖ • (q -ᵥ p)

Tactic:
rw [← h, norm_smul, smul_smul, mul_comm]

Premises used: norm_smul, smul_smul, mul_comm
-- 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_1 : ¬v = 0
h_2 : ∃ (a : ℝ≥0), (↑a : ℝ) • v = q -ᵥ p
c : ℝ≥0
h : (↑c : ℝ) • v = q -ᵥ p
⊢ (‖v‖ * ‖(↑c : ℝ)‖) • v = (‖v‖ * (↑c : ℝ)) • 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
p q : P
rw : Membership.mem (γ := Submodule NNReal V) (NNReal ∙ (q -ᵥ p)) (q -ᵥ p)
⊢ (((signedDist (q -ᵥ p) : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q = dist p q

Tactic:
rw [signedDist_eq_dist_iff_vsub_mem_span]

Premises used: signedDist_eq_dist_iff_vsub_mem_span
-- 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
⊢ Membership.mem (γ := Submodule NNReal V) (NNReal ∙ (q -ᵥ p)) (q -ᵥ p)

Tactic:
apply Submodule.mem_span_singleton_self

Premises used: Submodule.mem_span_singleton_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
p q : P
rw : (((signedDist (q -ᵥ p) : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q = dist p q
⊢ (((signedDist (p -ᵥ q) : (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]

Premises used: neg_eq_iff_eq_neg, signedDist_neg, neg_vsub_eq_vsub_rev
-- 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
⊢ (((signedDist (q -ᵥ p) : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q = dist p q

Tactic:
apply signedDist_vsub_self

Premises used: 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
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 : ℝ)
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 : ℝ)
⊢ (((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 : ℝ)

Tactic:
trans c₂ * signedDist v p q + c₁ * signedDist v q p

Premises used: signedDist, 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
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₂ ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ) +
      HMul.hMul (β := ℝ) c₁ ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) q : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) p : ℝ)

Tactic:
simp [AffineMap.lineMap_apply_ring']

Premises used: AffineMap.lineMap_apply_ring'
-- 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
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 : ℝ)
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 : ℝ)
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 : ℝ)
rw₃ 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 : ℝ)
⊢ 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:
rw [sub_mul, ← signedDist_anticomm v p, mul_neg, sub_eq_add_neg]

Premises used: sub_eq_add_neg, signedDist_anticomm, sub_mul, mul_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 : V
p q : P
c : ℝ
⊢ (((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) ((AffineMap.lineMap p q : (a : ℝ) → P) c) : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) p =
    HMul.hMul (β := ℝ) (-c) ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)

Tactic:
simpa using signedDist_lineMap_lineMap v p q c 0

Premises used: signedDist_lineMap_lineMap, 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
c : ℝ
⊢ (((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) ((AffineMap.lineMap p q : (a : ℝ) → P) c : P) =
    HMul.hMul (β := ℝ) c ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)

Tactic:
simpa using signedDist_lineMap_lineMap v p q 0 c

Premises used: signedDist_lineMap_lineMap, 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
c : ℝ
⊢ (((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) ((AffineMap.lineMap p q : (a : ℝ) → P) c) : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q =
    HMul.hMul (β := ℝ) (1 - c) ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)

Tactic:
simpa using signedDist_lineMap_lineMap v p q c 1

Premises used: signedDist_lineMap_lineMap, 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
c : ℝ
⊢ (((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) q : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) ((AffineMap.lineMap p q : (a : ℝ) → P) c : P) =
    HMul.hMul (β := ℝ) (c - 1) ((((signedDist v : (a : P) → P →ᴬ[ℝ] ℝ) p : P →ᴬ[ℝ] ℝ) : (a : P) → ℝ) q : ℝ)

Tactic:
simpa using signedDist_lineMap_lineMap v p q 1 c

Premises used: signedDist_lineMap_lineMap, 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
s : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥s
inst_5 : s.direction.HasOrthogonalProjection
p : P
⊢ s.signedInfDist p =
    (signedDist (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) : (a : P) → P →ᴬ[ℝ] ℝ)
      (↑Classical.ofNonempty : P)

Tactic:
rfl

Premises used: AffineSubspace.signedInfDist, 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 q : P
h : q ∈ s
h₁ : ⟪p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P), (↑Classical.ofNonempty : P) -ᵥ q⟫ = 0
⊢ s.signedInfDist p = (signedDist (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) : (a : P) → P →ᴬ[ℝ] ℝ) q

Tactic:
apply signedDist_left_congr

Premises used: signedDist_left_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
s : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥s
inst_5 : s.direction.HasOrthogonalProjection
p q : P
h : q ∈ s
h₁ : (↑Classical.ofNonempty : P) -ᵥ q ∈ s.direction
h₂ : p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) ∈ s.directionᗮ
⊢ ⟪p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P), (↑Classical.ofNonempty : P) -ᵥ q⟫ = 0

Tactic:
apply s.direction.inner_left_of_mem_orthogonal

Premises used: Submodule.inner_left_of_mem_orthogonal
-- 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 q : P
h : q ∈ s
⊢ (↑Classical.ofNonempty : P) -ᵥ q ∈ s.direction

Tactic:
vsub_mem_direction (SetLike.coe_mem _) h

Premises used: SetLike.coe_mem, Set.Mem, AffineSubspace.vsub_mem_direction
-- 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 q : P
h : q ∈ s
⊢ (↑Classical.ofNonempty : P) -ᵥ q ∈ s.direction

Tactic:
exact vsub_mem_direction (SetLike.coe_mem _) h

Premises used: SetLike.coe_mem, AffineSubspace.vsub_mem_direction
-- 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 q : P
h : q ∈ s
⊢ p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) ∈ s.directionᗮ

Tactic:
vsub_orthogonalProjection_mem_direction_orthogonal s p

Premises used: EuclideanGeometry.vsub_orthogonalProjection_mem_direction_orthogonal, Set.Mem, setOf
-- 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 q : P
h : q ∈ s
⊢ p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) ∈ s.directionᗮ

Tactic:
exact vsub_orthogonalProjection_mem_direction_orthogonal s p

Premises used: EuclideanGeometry.vsub_orthogonalProjection_mem_direction_orthogonal