awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine (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₁ p₂ p₃ : P
r : ℝ
hp₂ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r = p₂
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hr0' : r ≠ 0
hr1' : r ≠ 1
hr0 : 0 < r
hr1 : r < 1
rw :
  p₃ -ᵥ (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r = (-(1 - r) / r) • (p₁ -ᵥ (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r)
rw₁ : p₃ -ᵥ (r • (p₃ -ᵥ p₁) +ᵥ p₁) = (-(1 - r) / r) • (p₁ -ᵥ (r • (p₃ -ᵥ p₁) +ᵥ p₁))
rw₂ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • (p₁ -ᵥ (r • (p₃ -ᵥ p₁) +ᵥ p₁))
rw₃ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • (p₁ -ᵥ p₁ - r • (p₃ -ᵥ p₁))
rw₄ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • (0 - r • (p₃ -ᵥ p₁))
rw₅ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • -(r • (p₃ -ᵥ p₁))
⊢ p₃ -ᵥ p₂ = (-(1 - r) / r) • (p₁ -ᵥ p₂)
have rw₆ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = -((-(1 - r) / r) • r • (p₃ -ᵥ p₁))
Tactic: rw [← hp₂, AffineMap.lineMap_apply, vsub_vadd_eq_vsub_sub, vsub_vadd_eq_vsub_sub, vsub_self,
    zero_sub, smul_neg, smul_smul, div_mul_cancel₀ _ hr0', neg_smul, neg_neg, sub_eq_iff_eq_add, ←
    add_smul, sub_add_cancel, one_smul]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine (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₁ p₂ p₃ : P
r : ℝ
hp₂ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r = p₂
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hr0' : r ≠ 0
hr1' : r ≠ 1
hr0 : 0 < r
hr1 : r < 1
rw :
  p₃ -ᵥ (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r = (-(1 - r) / r) • (p₁ -ᵥ (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r)
rw₁ : p₃ -ᵥ (r • (p₃ -ᵥ p₁) +ᵥ p₁) = (-(1 - r) / r) • (p₁ -ᵥ (r • (p₃ -ᵥ p₁) +ᵥ p₁))
rw₂ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • (p₁ -ᵥ (r • (p₃ -ᵥ p₁) +ᵥ p₁))
rw₃ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • (p₁ -ᵥ p₁ - r • (p₃ -ᵥ p₁))
rw₄ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • (0 - r • (p₃ -ᵥ p₁))
rw₅ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • -(r • (p₃ -ᵥ p₁))
rw₆ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = -((-(1 - r) / r) • r • (p₃ -ᵥ p₁))
⊢ p₃ -ᵥ p₂ = (-(1 - r) / r) • (p₁ -ᵥ p₂)
have rw₇ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = -((-(1 - r) / r * r) • (p₃ -ᵥ p₁))
Tactic: rw [← hp₂, AffineMap.lineMap_apply, vsub_vadd_eq_vsub_sub, vsub_vadd_eq_vsub_sub, vsub_self,
    zero_sub, smul_neg, smul_smul, div_mul_cancel₀ _ hr0', neg_smul, neg_neg, sub_eq_iff_eq_add, ←
    add_smul, sub_add_cancel, one_smul]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine (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₁ p₂ p₃ : P
r : ℝ
hp₂ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r = p₂
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hr0' : r ≠ 0
hr1' : r ≠ 1
hr0 : 0 < r
hr1 : r < 1
rw :
  p₃ -ᵥ (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r = (-(1 - r) / r) • (p₁ -ᵥ (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r)
rw₁ : p₃ -ᵥ (r • (p₃ -ᵥ p₁) +ᵥ p₁) = (-(1 - r) / r) • (p₁ -ᵥ (r • (p₃ -ᵥ p₁) +ᵥ p₁))
rw₂ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • (p₁ -ᵥ (r • (p₃ -ᵥ p₁) +ᵥ p₁))
rw₃ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • (p₁ -ᵥ p₁ - r • (p₃ -ᵥ p₁))
rw₄ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • (0 - r • (p₃ -ᵥ p₁))
rw₅ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • -(r • (p₃ -ᵥ p₁))
rw₆ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = -((-(1 - r) / r) • r • (p₃ -ᵥ p₁))
rw₇ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = -((-(1 - r) / r * r) • (p₃ -ᵥ p₁))
⊢ p₃ -ᵥ p₂ = (-(1 - r) / r) • (p₁ -ᵥ p₂)
have rw₈ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = -(-(1 - r) • (p₃ -ᵥ p₁))
Tactic: rw [← hp₂, AffineMap.lineMap_apply, vsub_vadd_eq_vsub_sub, vsub_vadd_eq_vsub_sub, vsub_self,
    zero_sub, smul_neg, smul_smul, div_mul_cancel₀ _ hr0', neg_smul, neg_neg, sub_eq_iff_eq_add, ←
    add_smul, sub_add_cancel, one_smul]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine (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₁ p₂ p₃ : P
r : ℝ
hp₂ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r = p₂
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hr0' : r ≠ 0
hr1' : r ≠ 1
hr0 : 0 < r
hr1 : r < 1
rw :
  p₃ -ᵥ (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r = (-(1 - r) / r) • (p₁ -ᵥ (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r)
rw₁ : p₃ -ᵥ (r • (p₃ -ᵥ p₁) +ᵥ p₁) = (-(1 - r) / r) • (p₁ -ᵥ (r • (p₃ -ᵥ p₁) +ᵥ p₁))
rw₂ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • (p₁ -ᵥ (r • (p₃ -ᵥ p₁) +ᵥ p₁))
rw₃ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • (p₁ -ᵥ p₁ - r • (p₃ -ᵥ p₁))
rw₄ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • (0 - r • (p₃ -ᵥ p₁))
rw₅ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • -(r • (p₃ -ᵥ p₁))
rw₆ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = -((-(1 - r) / r) • r • (p₃ -ᵥ p₁))
rw₇ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = -((-(1 - r) / r * r) • (p₃ -ᵥ p₁))
rw₈ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = -(-(1 - r) • (p₃ -ᵥ p₁))
⊢ p₃ -ᵥ p₂ = (-(1 - r) / r) • (p₁ -ᵥ p₂)
have rw₉ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = - -((1 - r) • (p₃ -ᵥ p₁))
Tactic: rw [← hp₂, AffineMap.lineMap_apply, vsub_vadd_eq_vsub_sub, vsub_vadd_eq_vsub_sub, vsub_self,
    zero_sub, smul_neg, smul_smul, div_mul_cancel₀ _ hr0', neg_smul, neg_neg, sub_eq_iff_eq_add, ←
    add_smul, sub_add_cancel, one_smul]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine (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₁ p₂ p₃ : P
r : ℝ
hp₂ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r = p₂
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hr0' : r ≠ 0
hr1' : r ≠ 1
hr0 : 0 < r
hr1 : r < 1
rw :
  p₃ -ᵥ (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r = (-(1 - r) / r) • (p₁ -ᵥ (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r)
rw₁ : p₃ -ᵥ (r • (p₃ -ᵥ p₁) +ᵥ p₁) = (-(1 - r) / r) • (p₁ -ᵥ (r • (p₃ -ᵥ p₁) +ᵥ p₁))
rw₂ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • (p₁ -ᵥ (r • (p₃ -ᵥ p₁) +ᵥ p₁))
rw₃ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • (p₁ -ᵥ p₁ - r • (p₃ -ᵥ p₁))
rw₄ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • (0 - r • (p₃ -ᵥ p₁))
rw₅ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • -(r • (p₃ -ᵥ p₁))
rw₆ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = -((-(1 - r) / r) • r • (p₃ -ᵥ p₁))
rw₇ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = -((-(1 - r) / r * r) • (p₃ -ᵥ p₁))
rw₈ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = -(-(1 - r) • (p₃ -ᵥ p₁))
rw₉ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = - -((1 - r) • (p₃ -ᵥ p₁))
⊢ p₃ -ᵥ p₂ = (-(1 - r) / r) • (p₁ -ᵥ p₂)
have rw₁₀ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (1 - r) • (p₃ -ᵥ p₁)
Tactic: rw [← hp₂, AffineMap.lineMap_apply, vsub_vadd_eq_vsub_sub, vsub_vadd_eq_vsub_sub, vsub_self,
    zero_sub, smul_neg, smul_smul, div_mul_cancel₀ _ hr0', neg_smul, neg_neg, sub_eq_iff_eq_add, ←
    add_smul, sub_add_cancel, one_smul]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine (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₁ p₂ p₃ : P
r : ℝ
hp₂ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r = p₂
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hr0' : r ≠ 0
hr1' : r ≠ 1
hr0 : 0 < r
hr1 : r < 1
rw :
  p₃ -ᵥ (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r = (-(1 - r) / r) • (p₁ -ᵥ (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r)
rw₁ : p₃ -ᵥ (r • (p₃ -ᵥ p₁) +ᵥ p₁) = (-(1 - r) / r) • (p₁ -ᵥ (r • (p₃ -ᵥ p₁) +ᵥ p₁))
rw₂ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • (p₁ -ᵥ (r • (p₃ -ᵥ p₁) +ᵥ p₁))
rw₃ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • (p₁ -ᵥ p₁ - r • (p₃ -ᵥ p₁))
rw₄ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • (0 - r • (p₃ -ᵥ p₁))
rw₅ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • -(r • (p₃ -ᵥ p₁))
rw₆ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = -((-(1 - r) / r) • r • (p₃ -ᵥ p₁))
rw₇ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = -((-(1 - r) / r * r) • (p₃ -ᵥ p₁))
rw₈ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = -(-(1 - r) • (p₃ -ᵥ p₁))
rw₉ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = - -((1 - r) • (p₃ -ᵥ p₁))
rw₁₀ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (1 - r) • (p₃ -ᵥ p₁)
⊢ p₃ -ᵥ p₂ = (-(1 - r) / r) • (p₁ -ᵥ p₂)
have rw₁₁ : p₃ -ᵥ p₁ = (1 - r) • (p₃ -ᵥ p₁) + r • (p₃ -ᵥ p₁)
Tactic: rw [← hp₂, AffineMap.lineMap_apply, vsub_vadd_eq_vsub_sub, vsub_vadd_eq_vsub_sub, vsub_self,
    zero_sub, smul_neg, smul_smul, div_mul_cancel₀ _ hr0', neg_smul, neg_neg, sub_eq_iff_eq_add, ←
    add_smul, sub_add_cancel, one_smul]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine (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₁ p₂ p₃ : P
r : ℝ
hp₂ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r = p₂
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hr0' : r ≠ 0
hr1' : r ≠ 1
hr0 : 0 < r
hr1 : r < 1
rw :
  p₃ -ᵥ (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r = (-(1 - r) / r) • (p₁ -ᵥ (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r)
rw₁ : p₃ -ᵥ (r • (p₃ -ᵥ p₁) +ᵥ p₁) = (-(1 - r) / r) • (p₁ -ᵥ (r • (p₃ -ᵥ p₁) +ᵥ p₁))
rw₂ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • (p₁ -ᵥ (r • (p₃ -ᵥ p₁) +ᵥ p₁))
rw₃ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • (p₁ -ᵥ p₁ - r • (p₃ -ᵥ p₁))
rw₄ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • (0 - r • (p₃ -ᵥ p₁))
rw₅ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • -(r • (p₃ -ᵥ p₁))
rw₆ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = -((-(1 - r) / r) • r • (p₃ -ᵥ p₁))
rw₇ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = -((-(1 - r) / r * r) • (p₃ -ᵥ p₁))
rw₈ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = -(-(1 - r) • (p₃ -ᵥ p₁))
rw₉ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = - -((1 - r) • (p₃ -ᵥ p₁))
rw₁₀ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (1 - r) • (p₃ -ᵥ p₁)
rw₁₁ : p₃ -ᵥ p₁ = (1 - r) • (p₃ -ᵥ p₁) + r • (p₃ -ᵥ p₁)
⊢ p₃ -ᵥ p₂ = (-(1 - r) / r) • (p₁ -ᵥ p₂)
have rw₁₂ : p₃ -ᵥ p₁ = (1 - r + r) • (p₃ -ᵥ p₁)
Tactic: rw [← hp₂, AffineMap.lineMap_apply, vsub_vadd_eq_vsub_sub, vsub_vadd_eq_vsub_sub, vsub_self,
    zero_sub, smul_neg, smul_smul, div_mul_cancel₀ _ hr0', neg_smul, neg_neg, sub_eq_iff_eq_add, ←
    add_smul, sub_add_cancel, one_smul]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine (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₁ p₂ p₃ : P
r : ℝ
hp₂ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r = p₂
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hr0' : r ≠ 0
hr1' : r ≠ 1
hr0 : 0 < r
hr1 : r < 1
rw :
  p₃ -ᵥ (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r = (-(1 - r) / r) • (p₁ -ᵥ (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r)
rw₁ : p₃ -ᵥ (r • (p₃ -ᵥ p₁) +ᵥ p₁) = (-(1 - r) / r) • (p₁ -ᵥ (r • (p₃ -ᵥ p₁) +ᵥ p₁))
rw₂ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • (p₁ -ᵥ (r • (p₃ -ᵥ p₁) +ᵥ p₁))
rw₃ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • (p₁ -ᵥ p₁ - r • (p₃ -ᵥ p₁))
rw₄ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • (0 - r • (p₃ -ᵥ p₁))
rw₅ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • -(r • (p₃ -ᵥ p₁))
rw₆ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = -((-(1 - r) / r) • r • (p₃ -ᵥ p₁))
rw₇ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = -((-(1 - r) / r * r) • (p₃ -ᵥ p₁))
rw₈ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = -(-(1 - r) • (p₃ -ᵥ p₁))
rw₉ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = - -((1 - r) • (p₃ -ᵥ p₁))
rw₁₀ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (1 - r) • (p₃ -ᵥ p₁)
rw₁₁ : p₃ -ᵥ p₁ = (1 - r) • (p₃ -ᵥ p₁) + r • (p₃ -ᵥ p₁)
rw₁₂ : p₃ -ᵥ p₁ = (1 - r + r) • (p₃ -ᵥ p₁)
⊢ p₃ -ᵥ p₂ = (-(1 - r) / r) • (p₁ -ᵥ p₂)
have rw₁₃ : p₃ -ᵥ p₁ = HSMul.hSMul (α := ℝ) 1 (p₃ -ᵥ p₁)
Tactic: rw [← hp₂, AffineMap.lineMap_apply, vsub_vadd_eq_vsub_sub, vsub_vadd_eq_vsub_sub, vsub_self,
    zero_sub, smul_neg, smul_smul, div_mul_cancel₀ _ hr0', neg_smul, neg_neg, sub_eq_iff_eq_add, ←
    add_smul, sub_add_cancel, one_smul]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine (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₁ p₂ p₃ : P
r : ℝ
hp₂ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r = p₂
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hr0' : r ≠ 0
hr1' : r ≠ 1
hr0 : 0 < r
hr1 : r < 1
rw :
  p₃ -ᵥ (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r = (-(1 - r) / r) • (p₁ -ᵥ (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r)
rw₁ : p₃ -ᵥ (r • (p₃ -ᵥ p₁) +ᵥ p₁) = (-(1 - r) / r) • (p₁ -ᵥ (r • (p₃ -ᵥ p₁) +ᵥ p₁))
rw₂ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • (p₁ -ᵥ (r • (p₃ -ᵥ p₁) +ᵥ p₁))
rw₃ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • (p₁ -ᵥ p₁ - r • (p₃ -ᵥ p₁))
rw₄ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • (0 - r • (p₃ -ᵥ p₁))
rw₅ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • -(r • (p₃ -ᵥ p₁))
rw₆ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = -((-(1 - r) / r) • r • (p₃ -ᵥ p₁))
rw₇ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = -((-(1 - r) / r * r) • (p₃ -ᵥ p₁))
rw₈ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = -(-(1 - r) • (p₃ -ᵥ p₁))
rw₉ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = - -((1 - r) • (p₃ -ᵥ p₁))
rw₁₀ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (1 - r) • (p₃ -ᵥ p₁)
rw₁₁ : p₃ -ᵥ p₁ = (1 - r) • (p₃ -ᵥ p₁) + r • (p₃ -ᵥ p₁)
rw₁₂ : p₃ -ᵥ p₁ = (1 - r + r) • (p₃ -ᵥ p₁)
rw₁₃ : p₃ -ᵥ p₁ = HSMul.hSMul (α := ℝ) 1 (p₃ -ᵥ p₁)
⊢ p₃ -ᵥ p₂ = (-(1 - r) / r) • (p₁ -ᵥ p₂)
have rw₁₄ : p₃ -ᵥ p₁ = p₃ -ᵥ p₁
Tactic: rw [← hp₂, AffineMap.lineMap_apply, vsub_vadd_eq_vsub_sub, vsub_vadd_eq_vsub_sub, vsub_self,
    zero_sub, smul_neg, smul_smul, div_mul_cancel₀ _ hr0', neg_smul, neg_neg, sub_eq_iff_eq_add, ←
    add_smul, sub_add_cancel, one_smul]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine (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₁ p₂ p₃ : P
h : Sbtw ℝ p₁ p₂ p₃
⊢ ∠ p₃ p₂ p₁ = π
have rw : ∠ p₃ p₂ p₁ = ∠ p₁ p₂ p₃
Tactic: rw [← h.angle₁₂₃_eq_pi, angle_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine (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₁ p₂ p₃ : P
h : Sbtw ℝ p₁ p₂ p₃
rw : ∠ p₃ p₂ p₁ = ∠ p₁ p₂ p₃
⊢ ∠ p₃ p₂ p₁ = π
have rw₁ : ∠ p₁ p₂ p₃ = ∠ p₁ p₂ p₃
Tactic: rw [← h.angle₁₂₃_eq_pi, angle_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine (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₁ p₂ p₃ : P
⊢ ∠ p₁ p₂ p₃ = π ↔ Sbtw ℝ p₁ p₂ p₃
have refine : ∠ p₁ p₂ p₃ = π → Sbtw ℝ p₁ p₂ p₃
Tactic: refine ⟨?_, fun h => h.angle₁₂₃_eq_pi⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine (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₁ p₂ p₃ : P
⊢ ∠ p₁ p₂ p₃ = π → Sbtw ℝ p₁ p₂ p₃
have rw : (p₁ -ᵥ p₂ ≠ 0 ∧ ∃ r < 0, p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)) → Sbtw ℝ p₁ p₂ p₃
Tactic: rw [angle, angle_eq_pi_iff]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine (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₁ p₂ p₃ : P
hp₁p₂ : p₁ -ᵥ p₂ ≠ 0
r : ℝ
hr : r < 0
hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
⊢ Sbtw ℝ p₁ p₂ p₃
have refine_1 : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) (1 / (1 - r)) = p₂
Tactic: refine ⟨⟨1 / (1 - r), ⟨div_nonneg zero_le_one (sub_nonneg.2 (hr.le.trans zero_le_one)),
    (div_le_one (sub_pos.2 (hr.trans zero_lt_one))).2 ((le_sub_self_iff 1).2 hr.le)⟩, ?_⟩,
    (vsub_ne_zero.1 hp₁p₂).symm, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine (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₁ p₂ p₃ : P
hp₁p₂ : p₁ -ᵥ p₂ ≠ 0
r : ℝ
hr : r < 0
hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
refine_1 : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) (1 / (1 - r)) = p₂
⊢ Sbtw ℝ p₁ p₂ p₃
have refine_2 : p₂ ≠ p₃
Tactic: refine ⟨⟨1 / (1 - r), ⟨div_nonneg zero_le_one (sub_nonneg.2 (hr.le.trans zero_le_one)),
    (div_le_one (sub_pos.2 (hr.trans zero_lt_one))).2 ((le_sub_self_iff 1).2 hr.le)⟩, ?_⟩,
    (vsub_ne_zero.1 hp₁p₂).symm, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine (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
p₁ p₂ p₃ : P
hp₁p₂ : p₁ -ᵥ p₂ ≠ 0
r : ℝ
hr : r < 0
hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
⊢ (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) (1 / (1 - r)) = p₂
have hp₃p₃ : p₃ = r • (p₁ -ᵥ p₂) +ᵥ p₂
Tactic: rw [← eq_vadd_iff_vsub_eq] at hp₃p₂
Cleared hypotheses: hp₃p₂
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine (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₁ p₂ p₃ : P
hp₁p₂ : p₁ -ᵥ p₂ ≠ 0
r : ℝ
hr : r < 0
hp₃p₂ : p₃ = r • (p₁ -ᵥ p₂) +ᵥ p₂
⊢ (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) (1 / (1 - r)) = p₂
have refine_1 : p₂ -ᵥ p₁ = (1 / (1 - r) * -r + 1 / (1 - r)) • (p₂ -ᵥ p₁)
Tactic: rw [AffineMap.lineMap_apply, hp₃p₂, vadd_vsub_assoc, ← neg_vsub_eq_vsub_rev p₂ p₁, smul_neg, ←
      neg_smul, smul_add, smul_smul, ← add_smul, eq_comm, eq_vadd_iff_vsub_eq]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine (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₁ p₂ p₃ : P
hp₁p₂ : p₁ -ᵥ p₂ ≠ 0
r : ℝ
hr : r < 0
hp₃p₂ : p₃ = r • (p₁ -ᵥ p₂) +ᵥ p₂
⊢ p₂ -ᵥ p₁ = (1 / (1 - r) * -r + 1 / (1 - r)) • (p₂ -ᵥ p₁)
have h : 1 / (1 - r) * -r + 1 / (1 - r) = 1
Tactic: convert! (one_smul ℝ (p₂ -ᵥ p₁)).symm
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine (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₁ p₂ p₃ : P
hp₁p₂ : p₁ -ᵥ p₂ ≠ 0
r : ℝ
hr : r < 0
hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
⊢ p₂ ≠ p₃
have refine_2 : r ≠ 0 ∧ p₁ -ᵥ p₂ ≠ 0
Tactic: rw [ne_comm, ← @vsub_ne_zero V, hp₃p₂, smul_ne_zero_iff]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine (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₁ p₂ p₃ : P
h : Wbtw ℝ p₁ p₂ p₃
hp₂p₁ : p₂ ≠ p₁
⊢ ∠ p₂ p₁ p₃ = 0
have rw : p₂ -ᵥ p₁ ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ p₃ -ᵥ p₁ = r • (p₂ -ᵥ p₁)
Tactic: rw [angle, angle_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine (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₁ p₂ p₃ : P
h : Wbtw ℝ p₁ p₂ p₃
hp₂p₁ : p₂ ≠ p₁
⊢ p₂ -ᵥ p₁ ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ p₃ -ᵥ p₁ = r • (p₂ -ᵥ p₁)
have rcases : ∀ (r : ℝ) (hr0 : 0 ≤ r) (hr1 : r ≤ 1) (hp₂p₁ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r ≠ p₁),
  (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r -ᵥ p₁ ≠ 0 ∧
    ∃ (r_1 : ℝ), 0 < r_1 ∧ p₃ -ᵥ p₁ = r_1 • ((AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r -ᵥ p₁)
Tactic: rcases h with ⟨r, ⟨hr0, hr1⟩, rfl⟩
Cleared hypotheses: p₂, h, hp₂p₁
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine (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
p₁ p₃ : P
r : ℝ
hr0 : 0 ≤ r
hr1 : r ≤ 1
hp₂p₁ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r ≠ p₁
⊢ (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r -ᵥ p₁ ≠ 0 ∧
    ∃ (r_1 : ℝ), 0 < r_1 ∧ p₃ -ᵥ p₁ = r_1 • ((AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r -ᵥ p₁)
have hr0' : r ≠ 0
Tactic: have hr0' : r ≠ 0 := by
    rintro rfl
    simp at hp₂p₁
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine (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
p₁ p₃ : P
r : ℝ
hr0 : 0 ≤ r
hr1 : r ≤ 1
hp₂p₁ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r ≠ p₁
hr0' : r ≠ 0
⊢ (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r -ᵥ p₁ ≠ 0 ∧
    ∃ (r_1 : ℝ), 0 < r_1 ∧ p₃ -ᵥ p₁ = r_1 • ((AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r -ᵥ p₁)
have hr0₁ : 0 < r
Tactic: replace hr0 := hr0.lt_of_ne hr0'.symm
Cleared hypotheses: hr0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine (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₁ p₃ : P
r : ℝ
hr1 : r ≤ 1
hp₂p₁ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r ≠ p₁
hr0' : r ≠ 0
hr0 : 0 < r
⊢ (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r -ᵥ p₁ ≠ 0 ∧
    ∃ (r_1 : ℝ), 0 < r_1 ∧ p₃ -ᵥ p₁ = r_1 • ((AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r -ᵥ p₁)
have refine : p₃ -ᵥ p₁ = r⁻¹ • ((AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r -ᵥ p₁)
Tactic: refine ⟨vsub_ne_zero.2 hp₂p₁, r⁻¹, inv_pos.2 hr0, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine (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₁ p₃ : P
r : ℝ
hr1 : r ≤ 1
hp₂p₁ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r ≠ p₁
hr0' : r ≠ 0
hr0 : 0 < r
⊢ p₃ -ᵥ p₁ = r⁻¹ • ((AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r -ᵥ p₁)
have rw : p₃ -ᵥ p₁ = r⁻¹ • ((r • (p₃ -ᵥ p₁) +ᵥ p₁) -ᵥ p₁)
Tactic: rw [AffineMap.lineMap_apply, vadd_vsub_assoc, vsub_self, add_zero, smul_smul,
    inv_mul_cancel₀ hr0', one_smul]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine (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₁ p₃ : P
r : ℝ
hr1 : r ≤ 1
hp₂p₁ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r ≠ p₁
hr0' : r ≠ 0
hr0 : 0 < r
rw : p₃ -ᵥ p₁ = r⁻¹ • ((r • (p₃ -ᵥ p₁) +ᵥ p₁) -ᵥ p₁)
⊢ p₃ -ᵥ p₁ = r⁻¹ • ((AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r -ᵥ p₁)
have rw₁ : p₃ -ᵥ p₁ = r⁻¹ • (r • (p₃ -ᵥ p₁) + (p₁ -ᵥ p₁))
Tactic: rw [AffineMap.lineMap_apply, vadd_vsub_assoc, vsub_self, add_zero, smul_smul,
    inv_mul_cancel₀ hr0', one_smul]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine (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₁ p₃ : P
r : ℝ
hr1 : r ≤ 1
hp₂p₁ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r ≠ p₁
hr0' : r ≠ 0
hr0 : 0 < r
rw : p₃ -ᵥ p₁ = r⁻¹ • ((r • (p₃ -ᵥ p₁) +ᵥ p₁) -ᵥ p₁)
rw₁ : p₃ -ᵥ p₁ = r⁻¹ • (r • (p₃ -ᵥ p₁) + (p₁ -ᵥ p₁))
⊢ p₃ -ᵥ p₁ = r⁻¹ • ((AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r -ᵥ p₁)
have rw₂ : p₃ -ᵥ p₁ = r⁻¹ • (r • (p₃ -ᵥ p₁) + 0)
Tactic: rw [AffineMap.lineMap_apply, vadd_vsub_assoc, vsub_self, add_zero, smul_smul,
    inv_mul_cancel₀ hr0', one_smul]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine (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₁ p₃ : P
r : ℝ
hr1 : r ≤ 1
hp₂p₁ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r ≠ p₁
hr0' : r ≠ 0
hr0 : 0 < r
rw : p₃ -ᵥ p₁ = r⁻¹ • ((r • (p₃ -ᵥ p₁) +ᵥ p₁) -ᵥ p₁)
rw₁ : p₃ -ᵥ p₁ = r⁻¹ • (r • (p₃ -ᵥ p₁) + (p₁ -ᵥ p₁))
rw₂ : p₃ -ᵥ p₁ = r⁻¹ • (r • (p₃ -ᵥ p₁) + 0)
⊢ p₃ -ᵥ p₁ = r⁻¹ • ((AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r -ᵥ p₁)
have rw₃ : p₃ -ᵥ p₁ = r⁻¹ • r • (p₃ -ᵥ p₁)
Tactic: rw [AffineMap.lineMap_apply, vadd_vsub_assoc, vsub_self, add_zero, smul_smul,
    inv_mul_cancel₀ hr0', one_smul]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine (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₁ p₃ : P
r : ℝ
hr1 : r ≤ 1
hp₂p₁ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r ≠ p₁
hr0' : r ≠ 0
hr0 : 0 < r
rw : p₃ -ᵥ p₁ = r⁻¹ • ((r • (p₃ -ᵥ p₁) +ᵥ p₁) -ᵥ p₁)
rw₁ : p₃ -ᵥ p₁ = r⁻¹ • (r • (p₃ -ᵥ p₁) + (p₁ -ᵥ p₁))
rw₂ : p₃ -ᵥ p₁ = r⁻¹ • (r • (p₃ -ᵥ p₁) + 0)
rw₃ : p₃ -ᵥ p₁ = r⁻¹ • r • (p₃ -ᵥ p₁)
⊢ p₃ -ᵥ p₁ = r⁻¹ • ((AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r -ᵥ p₁)
have rw₄ : p₃ -ᵥ p₁ = (r⁻¹ * r) • (p₃ -ᵥ p₁)
Tactic: rw [AffineMap.lineMap_apply, vadd_vsub_assoc, vsub_self, add_zero, smul_smul,
    inv_mul_cancel₀ hr0', one_smul]