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₄ p₅ : P
hapc : ∠ p₁ p₅ p₃ = π
hbpd : ∠ p₂ p₅ p₄ = π
linarith :
  ∠ p₁ p₅ p₂ < ∠ p₃ p₅ p₄ →
    ∠ p₁ p₅ p₂ - ∠ p₃ p₅ p₄ + -(∠ p₁ p₅ p₂ + ∠ p₁ p₅ p₄ - π) + -(∠ p₄ p₅ p₁ - ∠ p₁ p₅ p₄) +
          (∠ p₄ p₅ p₁ + ∠ p₄ p₅ p₃ - π) +
        -(∠ p₄ p₅ p₃ - ∠ p₃ p₅ p₄) =
      0
⊢ ∠ p₁ p₅ p₂ = ∠ p₃ p₅ p₄
have linarith₁ : ∠ p₃ p₅ p₄ < ∠ p₁ p₅ p₂ →
  ∠ p₃ p₅ p₄ - ∠ p₁ p₅ p₂ + (∠ p₁ p₅ p₂ + ∠ p₁ p₅ p₄ - π) + (∠ p₄ p₅ p₁ - ∠ p₁ p₅ p₄) + -(∠ p₄ p₅ p₁ + ∠ p₄ p₅ p₃ - π) +
      (∠ p₄ p₅ p₃ - ∠ p₃ p₅ p₄) =
    0
Tactic: linarith [angle_add_angle_eq_pi_of_angle_eq_pi p₁ hbpd, angle_comm p₄ p₅ p₁,
    angle_add_angle_eq_pi_of_angle_eq_pi p₄ hapc, angle_comm p₄ p₅ 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₃ : P
h : ∠ p₁ p₂ p₃ = π
heq : dist p₁ p₂ = 0
⊢ False
have heq₁ : p₁ = p₂
Tactic: rw [dist_eq_zero] at heq
Cleared hypotheses: heq
-- 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
h : ∠ p₁ p₂ p₃ = π
heq : p₁ = p₂
⊢ False
have h₁ : π / 2 = π
Tactic: rw [heq, angle_self_left] at h
Cleared hypotheses: h, heq
-- 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 : π / 2 = π
heq : p₁ = p₂
⊢ π = 0
have linarith : π < 0 → 2 / 2 = 1
Tactic: linarith
-- 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 : π / 2 = π
heq : p₁ = p₂
linarith : π < 0 → 2 / 2 = 1
⊢ π = 0
have linarith₁ : π < 0 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- 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 : π / 2 = π
heq : p₁ = p₂
linarith : π < 0 → 2 / 2 = 1
linarith₁ : π < 0 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ π = 0
have linarith₂ : π < 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- 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 : π / 2 = π
heq : p₁ = p₂
linarith : π < 0 → 2 / 2 = 1
linarith₁ : π < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π < 0 → GT.gt (α := ℝ) 2 0
⊢ π = 0
have linarith₃ : π < 0 → 1 * π - 2 * π + (π - 0) = 0
Tactic: linarith
-- 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 : π / 2 = π
heq : p₁ = p₂
linarith : π < 0 → 2 / 2 = 1
linarith₁ : π < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π < 0 → GT.gt (α := ℝ) 2 0
linarith₃ : π < 0 → 1 * π - 2 * π + (π - 0) = 0
⊢ π = 0
have linarith₄ : 0 < π → 2 / 2 = 1
Tactic: linarith
-- 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 : π / 2 = π
heq : p₁ = p₂
linarith : π < 0 → 2 / 2 = 1
linarith₁ : π < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π < 0 → GT.gt (α := ℝ) 2 0
linarith₃ : π < 0 → 1 * π - 2 * π + (π - 0) = 0
linarith₄ : 0 < π → 2 / 2 = 1
⊢ π = 0
have linarith₅ : 0 < π → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- 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 : π / 2 = π
heq : p₁ = p₂
linarith : π < 0 → 2 / 2 = 1
linarith₁ : π < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π < 0 → GT.gt (α := ℝ) 2 0
linarith₃ : π < 0 → 1 * π - 2 * π + (π - 0) = 0
linarith₄ : 0 < π → 2 / 2 = 1
linarith₅ : 0 < π → HMul.hMul (α := ℝ) 1 2 = 2
⊢ π = 0
have linarith₆ : 0 < π → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- 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 : π / 2 = π
heq : p₁ = p₂
linarith : π < 0 → 2 / 2 = 1
linarith₁ : π < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π < 0 → GT.gt (α := ℝ) 2 0
linarith₃ : π < 0 → 1 * π - 2 * π + (π - 0) = 0
linarith₄ : 0 < π → 2 / 2 = 1
linarith₅ : 0 < π → HMul.hMul (α := ℝ) 1 2 = 2
linarith₆ : 0 < π → GT.gt (α := ℝ) 2 0
⊢ π = 0
have linarith₇ : 0 < π → -(1 * π - 2 * π) + (0 - π) = 0
Tactic: linarith
-- 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 : ∠ p₁ p₂ p₃ = π
⊢ dist p₁ p₃ = dist p₁ p₂ + dist p₃ p₂
have rw : ‖p₁ -ᵥ p₂ - (p₃ -ᵥ p₂)‖ = ‖p₁ -ᵥ p₂‖ + ‖p₃ -ᵥ p₂‖
Tactic: rw [dist_eq_norm_vsub V, dist_eq_norm_vsub V, dist_eq_norm_vsub V, ← vsub_sub_vsub_cancel_right]
-- 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₂
hp₃p₂ : p₃ ≠ p₂
⊢ dist p₁ p₃ = dist p₁ p₂ + dist p₃ p₂ ↔ ∠ p₁ p₂ p₃ = π
have rw : ‖p₁ -ᵥ p₂ - (p₃ -ᵥ p₂)‖ = ‖p₁ -ᵥ p₂‖ + ‖p₃ -ᵥ p₂‖ ↔ ∠ p₁ p₂ p₃ = π
Tactic: rw [dist_eq_norm_vsub V, dist_eq_norm_vsub V, dist_eq_norm_vsub V, ← vsub_sub_vsub_cancel_right]
-- 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 : ∠ p₁ p₂ p₃ = 0
⊢ dist p₁ p₃ = |dist p₁ p₂ - dist p₃ p₂|
have rw : ‖p₁ -ᵥ p₂ - (p₃ -ᵥ p₂)‖ = |‖p₁ -ᵥ p₂‖ - ‖p₃ -ᵥ p₂‖|
Tactic: rw [dist_eq_norm_vsub V, dist_eq_norm_vsub V, dist_eq_norm_vsub V, ← vsub_sub_vsub_cancel_right]
-- 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₂
hp₃p₂ : p₃ ≠ p₂
⊢ dist p₁ p₃ = |dist p₁ p₂ - dist p₃ p₂| ↔ ∠ p₁ p₂ p₃ = 0
have rw : ‖p₁ -ᵥ p₂ - (p₃ -ᵥ p₂)‖ = |‖p₁ -ᵥ p₂‖ - ‖p₃ -ᵥ p₂‖| ↔ ∠ p₁ p₂ p₃ = 0
Tactic: rw [dist_eq_norm_vsub V, dist_eq_norm_vsub V, dist_eq_norm_vsub V, ← vsub_sub_vsub_cancel_right]
-- 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
hp₁p₂ : p₁ ≠ p₂
⊢ ∠ p₁ (midpoint ℝ p₁ p₂) p₂ = π
have simp : InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₂ -ᵥ p₁) = π
Tactic: simp only [angle, left_vsub_midpoint, invOf_eq_inv, right_vsub_midpoint, inv_pos, zero_lt_two,
    angle_smul_right_of_pos, angle_smul_left_of_pos]
-- 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
hp₁p₂ : p₁ ≠ p₂
⊢ InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₂ -ᵥ p₁) = π
have rw : InnerProductGeometry.angle (p₁ -ᵥ p₂) (-(p₁ -ᵥ p₂)) = π
Tactic: rw [← neg_vsub_eq_vsub_rev p₁ 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
hp₁p₂ : p₁ ≠ p₂
⊢ InnerProductGeometry.angle (p₁ -ᵥ p₂) (-(p₁ -ᵥ p₂)) = π
have hx : p₁ -ᵥ p₂ ≠ 0
Tactic: apply angle_self_neg_of_nonzero
-- 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
h : dist p₃ p₁ = dist p₃ p₂
m : P := midpoint ℝ p₁ p₂
⊢ ∠ p₃ (midpoint ℝ p₁ p₂) p₁ = π / 2
have h1 : p₃ -ᵥ p₁ = p₃ -ᵥ m - (p₁ -ᵥ m)
Tactic: have h1 : p₃ -ᵥ p₁ = p₃ -ᵥ m - (p₁ -ᵥ m) := (vsub_sub_vsub_cancel_right p₃ p₁ m).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
h : dist p₃ p₁ = dist p₃ p₂
m : P := midpoint ℝ p₁ p₂
h1 : p₃ -ᵥ p₁ = p₃ -ᵥ m - (p₁ -ᵥ m)
⊢ p₃ -ᵥ p₂ = p₃ -ᵥ m + (p₁ -ᵥ m)
have rw : p₃ -ᵥ p₂ = p₃ -ᵥ m + HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₂)
Tactic: rw [left_vsub_midpoint, ← midpoint_vsub_right, vsub_add_vsub_cancel]
-- 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 : dist p₃ p₁ = dist p₃ p₂
m : P := midpoint ℝ p₁ p₂
h1 : p₃ -ᵥ p₁ = p₃ -ᵥ m - (p₁ -ᵥ m)
rw : p₃ -ᵥ p₂ = p₃ -ᵥ m + HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₂)
⊢ p₃ -ᵥ p₂ = p₃ -ᵥ m + (p₁ -ᵥ m)
have rw₁ : p₃ -ᵥ p₂ = p₃ -ᵥ m + (midpoint ℝ p₁ p₂ -ᵥ p₂)
Tactic: rw [left_vsub_midpoint, ← midpoint_vsub_right, vsub_add_vsub_cancel]
-- 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 : dist p₃ p₁ = dist p₃ p₂
m : P := midpoint ℝ p₁ p₂
h1 : p₃ -ᵥ p₁ = p₃ -ᵥ m - (p₁ -ᵥ m)
rw : p₃ -ᵥ p₂ = p₃ -ᵥ m + HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₂)
rw₁ : p₃ -ᵥ p₂ = p₃ -ᵥ m + (midpoint ℝ p₁ p₂ -ᵥ p₂)
⊢ p₃ -ᵥ p₂ = p₃ -ᵥ m + (p₁ -ᵥ m)
have rw₂ : p₃ -ᵥ p₂ = p₃ -ᵥ p₂
Tactic: rw [left_vsub_midpoint, ← midpoint_vsub_right, vsub_add_vsub_cancel]
-- 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
h : dist p₃ p₁ = dist p₃ p₂
m : P := midpoint ℝ p₁ p₂
h1 : p₃ -ᵥ p₁ = p₃ -ᵥ m - (p₁ -ᵥ m)
⊢ ∠ p₃ (midpoint ℝ p₁ p₂) p₁ = π / 2
have h2 : p₃ -ᵥ p₂ = p₃ -ᵥ m + (p₁ -ᵥ m)
Tactic: have h2 : p₃ -ᵥ p₂ = p₃ -ᵥ m + (p₁ -ᵥ m) := by
    rw [left_vsub_midpoint, ← midpoint_vsub_right, vsub_add_vsub_cancel]
-- 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
h : dist p₃ p₁ = dist p₃ p₂
m : P := midpoint ℝ p₁ p₂
h1 : p₃ -ᵥ p₁ = p₃ -ᵥ m - (p₁ -ᵥ m)
h2 : p₃ -ᵥ p₂ = p₃ -ᵥ m + (p₁ -ᵥ m)
⊢ ∠ p₃ (midpoint ℝ p₁ p₂) p₁ = π / 2
have h₁ : let m := midpoint ℝ p₁ p₂;
‖p₃ -ᵥ m - (p₁ -ᵥ m)‖ = ‖p₃ -ᵥ m + (p₁ -ᵥ m)‖
Tactic: rw [dist_eq_norm_vsub V p₃ p₁, dist_eq_norm_vsub V p₃ p₂, h1, h2] at h
Cleared hypotheses: h, m, h1, h2
-- 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 : dist p₃ p₁ = dist p₃ p₂
⊢ ∠ p₃ (midpoint ℝ p₁ p₂) p₂ = π / 2
have rw : ∠ p₃ (midpoint ℝ p₂ p₁) p₂ = π / 2
Tactic: rw [midpoint_comm p₁ p₂, angle_left_midpoint_eq_pi_div_two_of_dist_eq h.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
h : dist p₃ p₁ = dist p₃ p₂
rw : ∠ p₃ (midpoint ℝ p₂ p₁) p₂ = π / 2
⊢ ∠ p₃ (midpoint ℝ p₁ p₂) p₂ = π / 2
have rw₁ : π / 2 = π / 2
Tactic: rw [midpoint_comm p₁ p₂, angle_left_midpoint_eq_pi_div_two_of_dist_eq h.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
h : Sbtw ℝ p₁ p₂ p₃
⊢ ∠ p₁ p₂ p₃ = π
have rw : p₁ -ᵥ p₂ ≠ 0 ∧ ∃ r < 0, p₃ -ᵥ p₂ = r • (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
h : Sbtw ℝ p₁ p₂ p₃
⊢ p₁ -ᵥ p₂ ≠ 0 ∧ ∃ r < 0, p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
have rcases : ∀ (r : ℝ) (hp₂ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r = p₂) (hr0 : 0 ≤ r) (hr1 : r ≤ 1) (hp₂p₁ : p₂ ≠ p₁)
  (hp₂p₃ : p₂ ≠ p₃), p₁ -ᵥ p₂ ≠ 0 ∧ ∃ r < 0, p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
Tactic: rcases h with ⟨⟨r, ⟨hr0, hr1⟩, hp₂⟩, hp₂p₁, hp₂p₃⟩
Cleared hypotheses: h
-- 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₂
hr0 : 0 ≤ r
hr1 : r ≤ 1
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ p₁ -ᵥ p₂ ≠ 0 ∧ ∃ r < 0, p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
have refine : -(1 - r) / r < 0 ∧ p₃ -ᵥ p₂ = (-(1 - r) / r) • (p₁ -ᵥ p₂)
Tactic: refine ⟨vsub_ne_zero.2 hp₂p₁.symm, -(1 - r) / r, ?_⟩
-- 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₁
hp₂p₃ : p₂ ≠ p₃
hp₂ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) 0 = p₂
hr0 : LE.le (α := ℝ) 0 0
hr1 : LE.le (α := ℝ) 0 1
⊢ False
have hp₂p₂ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) 0 ≠ p₁
Tactic: rw [← hp₂] at hp₂p₁
Cleared hypotheses: hp₂p₁, hp₂p₃, hp₂, hr0, hr1
-- 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
r : ℝ
hp₂ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r = p₂
hr0 : 0 ≤ r
hr1 : r ≤ 1
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ -(1 - r) / r < 0 ∧ p₃ -ᵥ p₂ = (-(1 - r) / r) • (p₁ -ᵥ p₂)
have hr0' : r ≠ 0
Tactic: have hr0' : r ≠ 0 := by
    rintro rfl
    rw [← hp₂] at hp₂p₁
    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₃ : P
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hp₂ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) 1 = p₂
hr0 : LE.le (α := ℝ) 0 1
hr1 : LE.le (α := ℝ) 1 1
hr0' : Ne (α := ℝ) 1 0
⊢ False
have hp₂p₄ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) 1 ≠ p₃
Tactic: rw [← hp₂] at hp₂p₃
Cleared hypotheses: hp₂p₃, hp₂, hr0, hr1, hr0'
-- 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
r : ℝ
hp₂ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r = p₂
hr0 : 0 ≤ r
hr1 : r ≤ 1
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hr0' : r ≠ 0
⊢ -(1 - r) / r < 0 ∧ p₃ -ᵥ p₂ = (-(1 - r) / r) • (p₁ -ᵥ p₂)
have hr1' : r ≠ 1
Tactic: have hr1' : r ≠ 1 := by
    rintro rfl
    rw [← hp₂] at hp₂p₃
    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₃ : P
r : ℝ
hp₂ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r = p₂
hr0 : 0 ≤ r
hr1 : r ≤ 1
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hr0' : r ≠ 0
hr1' : r ≠ 1
⊢ -(1 - r) / r < 0 ∧ p₃ -ᵥ p₂ = (-(1 - r) / r) • (p₁ -ᵥ 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 (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
r : ℝ
hp₂ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r = p₂
hr1 : r ≤ 1
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hr0' : r ≠ 0
hr1' : r ≠ 1
hr0 : 0 < r
⊢ -(1 - r) / r < 0 ∧ p₃ -ᵥ p₂ = (-(1 - r) / r) • (p₁ -ᵥ p₂)
have hr1₁ : r < 1
Tactic: replace hr1 := hr1.lt_of_ne hr1'
Cleared hypotheses: hr1
-- 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
⊢ -(1 - r) / r < 0 ∧ p₃ -ᵥ p₂ = (-(1 - r) / r) • (p₁ -ᵥ p₂)
have refine : p₃ -ᵥ p₂ = (-(1 - r) / r) • (p₁ -ᵥ p₂)
Tactic: refine ⟨div_neg_of_neg_of_pos (Left.neg_neg_iff.2 (sub_pos.2 hr1)) 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₃ : 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
⊢ p₃ -ᵥ p₂ = (-(1 - r) / r) • (p₁ -ᵥ p₂)
have rw : p₃ -ᵥ (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r = (-(1 - r) / r) • (p₁ -ᵥ (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r)
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)
⊢ p₃ -ᵥ p₂ = (-(1 - r) / r) • (p₁ -ᵥ p₂)
have rw₁ : p₃ -ᵥ (r • (p₃ -ᵥ p₁) +ᵥ p₁) = (-(1 - r) / r) • (p₁ -ᵥ (r • (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
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₁))
⊢ p₃ -ᵥ p₂ = (-(1 - r) / r) • (p₁ -ᵥ p₂)
have rw₂ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • (p₁ -ᵥ (r • (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
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₁))
⊢ p₃ -ᵥ p₂ = (-(1 - r) / r) • (p₁ -ᵥ p₂)
have rw₃ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / 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₁))
⊢ p₃ -ᵥ p₂ = (-(1 - r) / r) • (p₁ -ᵥ p₂)
have rw₄ : p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • (0 - 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₁))
⊢ 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]