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 : 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 : ℝ)
⊢ 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]
-- 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 : ℝ)
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 : ℝ)
⊢ 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]
-- 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
s : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥s
inst_5 : s.direction.HasOrthogonalProjection
p q : P
h : q ∈ s
⊢ s.signedInfDist p = (signedDist (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) : (a : P) → P →ᴬ[ℝ] ℝ) q
have h₁ : ⟪p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P), (↑Classical.ofNonempty : P) -ᵥ q⟫ = 0
Tactic: apply signedDist_left_congr
-- 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
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), (↑Classical.ofNonempty : P) -ᵥ q⟫ = 0
have h₁ : (↑Classical.ofNonempty : P) -ᵥ q ∈ s.direction
Tactic: apply s.direction.inner_left_of_mem_orthogonal
-- 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
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
⊢ ⟪p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P), (↑Classical.ofNonempty : P) -ᵥ q⟫ = 0
have h₂ : p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) ∈ s.directionᗮ
Tactic: apply s.direction.inner_left_of_mem_orthogonal
-- 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
s : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥s
inst_5 : s.direction.HasOrthogonalProjection
p x : P
⊢ Eq (α := ℝ) ((s.signedInfDist p : (a : P) → ℝ) x : ℝ)
    (((signedDist (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) : (a : P) → P →ᴬ[ℝ] ℝ)
            (↑((orthogonalProjection s : (a : P) → ↥s) x) : P) :
          (a : P) → ℝ)
        x :
      ℝ)
have rw : Eq (α := ℝ)
  (((signedDist (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) : (a : P) → P →ᴬ[ℝ] ℝ)
          (↑((orthogonalProjection s : (a : P) → ↥s) x) : P) :
        (a : P) → ℝ)
      x :
    ℝ)
  (((signedDist (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) : (a : P) → P →ᴬ[ℝ] ℝ)
          (↑((orthogonalProjection s : (a : P) → ↥s) x) : P) :
        (a : P) → ℝ)
      x :
    ℝ)
Tactic: rw [signedInfDist_eq_signedDist_of_mem (orthogonalProjection_mem x)]
-- 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
s : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥s
inst_5 : s.direction.HasOrthogonalProjection
p : P
⊢ (s.signedInfDist p : (a : P) → ℝ) p = ‖p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)‖
have rw : ((signedDist (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) : (a : P) → P →ᴬ[ℝ] ℝ)
        (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) :
      (a : P) → ℝ)
    p =
  ‖p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)‖
Tactic: rw [signedInfDist_eq_signedDist_orthogonalProjection, signedDist_vsub_self, dist_eq_norm_vsub']
-- 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
s : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥s
inst_5 : s.direction.HasOrthogonalProjection
p : P
rw :
  ((signedDist (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) : (a : P) → P →ᴬ[ℝ] ℝ)
          (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) :
        (a : P) → ℝ)
      p =
    ‖p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)‖
⊢ (s.signedInfDist p : (a : P) → ℝ) p = ‖p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)‖
have rw₁ : dist (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p = ‖p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)‖
Tactic: rw [signedInfDist_eq_signedDist_orthogonalProjection, signedDist_vsub_self, dist_eq_norm_vsub']
-- 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
s : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥s
inst_5 : s.direction.HasOrthogonalProjection
p : P
rw :
  ((signedDist (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) : (a : P) → P →ᴬ[ℝ] ℝ)
          (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) :
        (a : P) → ℝ)
      p =
    ‖p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)‖
rw₁ :
  dist (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p = ‖p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)‖
⊢ (s.signedInfDist p : (a : P) → ℝ) p = ‖p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)‖
have rw₂ : ‖p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)‖ = ‖p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)‖
Tactic: rw [signedInfDist_eq_signedDist_orthogonalProjection, signedDist_vsub_self, dist_eq_norm_vsub']
-- 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
s : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥s
inst_5 : s.direction.HasOrthogonalProjection
p : P
h : p ∈ s
⊢ (↑(s.signedInfDist p) : P →ᵃ[ℝ] ℝ) = AffineMap.const ℝ P 0
have h₁ : ∀ (x : P),
  Eq (α := ℝ) (((↑(s.signedInfDist p) : P →ᵃ[ℝ] ℝ) : (a : P) → ℝ) x : ℝ) ((AffineMap.const ℝ P 0 : (a : P) → ℝ) x : ℝ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.SignedDist (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥s
inst_5 : s.direction.HasOrthogonalProjection
p x : P
h : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (insert p (↑s : Set P))) x
⊢ |(s.signedInfDist p : (a : P) → ℝ) x| = dist x (↑((orthogonalProjection s : (a : P) → ↥s) x) : P)
have h₁ : ∃ (r : ℝ), ∃ p0 ∈ s, x = r • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) +ᵥ p0
Tactic: rw [mem_affineSpan_insert_iff (orthogonalProjection s p).property] at h
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
s : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥s
inst_5 : s.direction.HasOrthogonalProjection
p x : P
h : ∃ (r : ℝ), ∃ p0 ∈ s, x = r • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) +ᵥ p0
⊢ |(s.signedInfDist p : (a : P) → ℝ) x| = dist x (↑((orthogonalProjection s : (a : P) → ↥s) x) : P)
have rcases : ∀ (r : ℝ) (p₀ : P) (hp₀ : p₀ ∈ s),
  |(s.signedInfDist p : (a : P) → ℝ) (r • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) +ᵥ p₀)| =
    dist (r • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) +ᵥ p₀)
      (↑((orthogonalProjection s : (a : P) → ↥s)
            (r • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) +ᵥ p₀)) :
        P)
Tactic: rcases h with ⟨r, p₀, hp₀, rfl⟩
Cleared hypotheses: x, 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
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
m : ℕ
inst_5 : NeZero m
e : Fin (n + 1) ≃ Fin (m + 1)
j : Fin (m + 1)
⊢ (s.reindex e).signedInfDist j = s.signedInfDist ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j)
have simp_rw : Eq (α := P →ᴬ[ℝ] ℝ)
  (AffineSubspace.signedInfDist (affineSpan ℝ ((s.reindex e).points '' {j}ᶜ)) ((s.reindex e).points j))
  (AffineSubspace.signedInfDist
    (affineSpan ℝ
      (s.points '' (singleton (α := Fin (n + 1)) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j : Fin (n + 1)))ᶜ))
    (s.points ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j)))
Tactic: simp_rw [signedInfDist, reindex_points, Set.image_comp, Set.image_compl_eq e.symm.bijective,
    Set.image_singleton, Function.comp_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
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
m : ℕ
inst_5 : NeZero m
e : Fin (n + 1) ≃ Fin (m + 1)
j : Fin (m + 1)
simp_rw :
  Eq (α := P →ᴬ[ℝ] ℝ)
    (AffineSubspace.signedInfDist (affineSpan ℝ ((s.reindex e).points '' {j}ᶜ)) ((s.reindex e).points j))
    (AffineSubspace.signedInfDist
      (affineSpan ℝ
        (s.points '' (singleton (α := Fin (n + 1)) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j : Fin (n + 1)))ᶜ))
      (s.points ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j)))
⊢ (s.reindex e).signedInfDist j = s.signedInfDist ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j)
have simp_rw₁ : Eq (α := P →ᴬ[ℝ] ℝ)
  (AffineSubspace.signedInfDist
    (affineSpan ℝ ((fun (a : Fin (m + 1)) ↦ (s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) a) '' {j}ᶜ))
    ((s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) j))
  (AffineSubspace.signedInfDist
    (affineSpan ℝ
      (s.points '' (singleton (α := Fin (n + 1)) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j : Fin (n + 1)))ᶜ))
    (s.points ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j)))
Tactic: simp_rw [signedInfDist, reindex_points, Set.image_comp, Set.image_compl_eq e.symm.bijective,
    Set.image_singleton, Function.comp_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
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
m : ℕ
inst_5 : NeZero m
e : Fin (n + 1) ≃ Fin (m + 1)
j : Fin (m + 1)
simp_rw :
  Eq (α := P →ᴬ[ℝ] ℝ)
    (AffineSubspace.signedInfDist (affineSpan ℝ ((s.reindex e).points '' {j}ᶜ)) ((s.reindex e).points j))
    (AffineSubspace.signedInfDist
      (affineSpan ℝ
        (s.points '' (singleton (α := Fin (n + 1)) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j : Fin (n + 1)))ᶜ))
      (s.points ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j)))
simp_rw₁ :
  Eq (α := P →ᴬ[ℝ] ℝ)
    (AffineSubspace.signedInfDist
      (affineSpan ℝ ((fun (a : Fin (m + 1)) ↦ (s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) a) '' {j}ᶜ))
      ((s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) j))
    (AffineSubspace.signedInfDist
      (affineSpan ℝ
        (s.points '' (singleton (α := Fin (n + 1)) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j : Fin (n + 1)))ᶜ))
      (s.points ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j)))
⊢ (s.reindex e).signedInfDist j = s.signedInfDist ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j)
have simp_rw₂ : Eq (α := P →ᴬ[ℝ] ℝ)
  (AffineSubspace.signedInfDist
    (affineSpan ℝ (s.points '' Set.image (α := Fin (m + 1)) (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1)) {j}ᶜ))
    ((s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) j))
  (AffineSubspace.signedInfDist
    (affineSpan ℝ
      (s.points '' (singleton (α := Fin (n + 1)) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j : Fin (n + 1)))ᶜ))
    (s.points ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j)))
Tactic: simp_rw [signedInfDist, reindex_points, Set.image_comp, Set.image_compl_eq e.symm.bijective,
    Set.image_singleton, Function.comp_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
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
m : ℕ
inst_5 : NeZero m
e : Fin (n + 1) ≃ Fin (m + 1)
j : Fin (m + 1)
simp_rw :
  Eq (α := P →ᴬ[ℝ] ℝ)
    (AffineSubspace.signedInfDist (affineSpan ℝ ((s.reindex e).points '' {j}ᶜ)) ((s.reindex e).points j))
    (AffineSubspace.signedInfDist
      (affineSpan ℝ
        (s.points '' (singleton (α := Fin (n + 1)) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j : Fin (n + 1)))ᶜ))
      (s.points ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j)))
simp_rw₁ :
  Eq (α := P →ᴬ[ℝ] ℝ)
    (AffineSubspace.signedInfDist
      (affineSpan ℝ ((fun (a : Fin (m + 1)) ↦ (s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) a) '' {j}ᶜ))
      ((s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) j))
    (AffineSubspace.signedInfDist
      (affineSpan ℝ
        (s.points '' (singleton (α := Fin (n + 1)) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j : Fin (n + 1)))ᶜ))
      (s.points ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j)))
simp_rw₂ :
  Eq (α := P →ᴬ[ℝ] ℝ)
    (AffineSubspace.signedInfDist
      (affineSpan ℝ (s.points '' Set.image (α := Fin (m + 1)) (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1)) {j}ᶜ))
      ((s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) j))
    (AffineSubspace.signedInfDist
      (affineSpan ℝ
        (s.points '' (singleton (α := Fin (n + 1)) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j : Fin (n + 1)))ᶜ))
      (s.points ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j)))
⊢ (s.reindex e).signedInfDist j = s.signedInfDist ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j)
have simp_rw₃ : Eq (α := P →ᴬ[ℝ] ℝ)
  (AffineSubspace.signedInfDist
    (affineSpan ℝ (s.points '' (Set.image (α := Fin (m + 1)) (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1)) {j})ᶜ))
    ((s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) j))
  (AffineSubspace.signedInfDist
    (affineSpan ℝ
      (s.points '' (singleton (α := Fin (n + 1)) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j : Fin (n + 1)))ᶜ))
    (s.points ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j)))
Tactic: simp_rw [signedInfDist, reindex_points, Set.image_comp, Set.image_compl_eq e.symm.bijective,
    Set.image_singleton, Function.comp_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
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
m : ℕ
inst_5 : NeZero m
e : Fin (n + 1) ≃ Fin (m + 1)
j : Fin (m + 1)
simp_rw :
  Eq (α := P →ᴬ[ℝ] ℝ)
    (AffineSubspace.signedInfDist (affineSpan ℝ ((s.reindex e).points '' {j}ᶜ)) ((s.reindex e).points j))
    (AffineSubspace.signedInfDist
      (affineSpan ℝ
        (s.points '' (singleton (α := Fin (n + 1)) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j : Fin (n + 1)))ᶜ))
      (s.points ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j)))
simp_rw₁ :
  Eq (α := P →ᴬ[ℝ] ℝ)
    (AffineSubspace.signedInfDist
      (affineSpan ℝ ((fun (a : Fin (m + 1)) ↦ (s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) a) '' {j}ᶜ))
      ((s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) j))
    (AffineSubspace.signedInfDist
      (affineSpan ℝ
        (s.points '' (singleton (α := Fin (n + 1)) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j : Fin (n + 1)))ᶜ))
      (s.points ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j)))
simp_rw₂ :
  Eq (α := P →ᴬ[ℝ] ℝ)
    (AffineSubspace.signedInfDist
      (affineSpan ℝ (s.points '' Set.image (α := Fin (m + 1)) (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1)) {j}ᶜ))
      ((s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) j))
    (AffineSubspace.signedInfDist
      (affineSpan ℝ
        (s.points '' (singleton (α := Fin (n + 1)) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j : Fin (n + 1)))ᶜ))
      (s.points ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j)))
simp_rw₃ :
  Eq (α := P →ᴬ[ℝ] ℝ)
    (AffineSubspace.signedInfDist
      (affineSpan ℝ (s.points '' (Set.image (α := Fin (m + 1)) (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1)) {j})ᶜ))
      ((s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) j))
    (AffineSubspace.signedInfDist
      (affineSpan ℝ
        (s.points '' (singleton (α := Fin (n + 1)) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j : Fin (n + 1)))ᶜ))
      (s.points ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j)))
⊢ (s.reindex e).signedInfDist j = s.signedInfDist ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j)
have simp_rw₄ : Eq (α := P →ᴬ[ℝ] ℝ)
  (AffineSubspace.signedInfDist
    (affineSpan ℝ
      (s.points '' (singleton (α := Fin (n + 1)) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j : Fin (n + 1)))ᶜ))
    ((s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) j))
  (AffineSubspace.signedInfDist
    (affineSpan ℝ
      (s.points '' (singleton (α := Fin (n + 1)) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j : Fin (n + 1)))ᶜ))
    (s.points ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) j)))
Tactic: simp_rw [signedInfDist, reindex_points, Set.image_comp, Set.image_compl_eq e.symm.bijective,
    Set.image_singleton, Function.comp_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
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
w : Fin (n + 1) → ℝ
h : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
⊢ (s.signedInfDist i : (a : P) → ℝ)
      ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P) =
    w i *
      ‖s.points i -ᵥ
          (↑(((s.faceOpposite i).orthogonalProjectionSpan :
                  (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
                (s.points i)) :
            P)‖
have rw : (AffineMap.lineMap 0
        ‖s.points i -ᵥ
            (↑(((s.faceOpposite i).orthogonalProjectionSpan :
                    (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
                  (s.points i)) :
              P)‖ :
      (a : ℝ) → ℝ)
    (∑ i ∈ Finset.univ ∩ {i}, w i) =
  w i *
    ‖s.points i -ᵥ
        (↑(((s.faceOpposite i).orthogonalProjectionSpan :
                (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
              (s.points i)) :
          P)‖
Tactic: rw [← ContinuousAffineMap.coe_toAffineMap, Finset.map_affineCombination _ _ _ h,
    Finset.univ.affineCombination_apply_eq_lineMap_sum w
      ((s.signedInfDist i).toAffineMap ∘ s.points) 0
      ‖s.points i -ᵥ (s.faceOpposite i).orthogonalProjectionSpan (s.points i)‖
      {i} h]