awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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 :
  Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₁ -ᵥ p₂)) =
    Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₂ -ᵥ p₁))
⊢ Real.sin (InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₁)) =
    Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₂ -ᵥ p₁))
have h₁ : Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₁ -ᵥ p₂)) =
  Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (-(p₁ -ᵥ p₂)))
Tactic: rw [InnerProductGeometry.angle_comm, ← neg_vsub_eq_vsub_rev p₁ p₂, angle_neg_right,
    Real.sin_pi_sub]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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 :
  Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₁ -ᵥ p₂)) =
    Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₂ -ᵥ p₁))
h₁ :
  Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₁ -ᵥ p₂)) =
    Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (-(p₁ -ᵥ p₂)))
⊢ Real.sin (InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₁)) =
    Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₂ -ᵥ p₁))
have h₂ : Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₁ -ᵥ p₂)) =
  Real.sin (π - InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₁ -ᵥ p₂))
Tactic: rw [InnerProductGeometry.angle_comm, ← neg_vsub_eq_vsub_rev p₁ p₂, angle_neg_right,
    Real.sin_pi_sub]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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 :
  Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₁ -ᵥ p₂)) =
    Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₂ -ᵥ p₁))
h₁ :
  Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₁ -ᵥ p₂)) =
    Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (-(p₁ -ᵥ p₂)))
h₂ :
  Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₁ -ᵥ p₂)) =
    Real.sin (π - InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₁ -ᵥ p₂))
⊢ Real.sin (InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₁)) =
    Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₂ -ᵥ p₁))
have h₃ : Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₁ -ᵥ p₂)) =
  Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₁ -ᵥ p₂))
Tactic: rw [InnerProductGeometry.angle_comm, ← neg_vsub_eq_vsub_rev p₁ p₂, angle_neg_right,
    Real.sin_pi_sub]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
h23 : p₂ ≠ p₃
h31 : p₃ ≠ p₁
⊢ Real.sin (∠ p₁ p₂ p₃) / dist p₃ p₁ = Real.sin (∠ p₃ p₁ p₂) / dist p₂ p₃
have simp : Real.sin (∠ p₁ p₂ p₃) * dist p₂ p₃ = Real.sin (∠ p₃ p₁ p₂) * dist p₃ p₁
Tactic: simp [field, dist_ne_zero.mpr h23, dist_ne_zero.mpr h31, mul_comm (dist ..)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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 : ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
⊢ dist p₁ p₂ = dist p₃ p₁ * Real.sin (∠ p₂ p₃ p₁) / Real.sin (∠ p₁ p₂ p₃)
have sin_gt_zero : 0 < Real.sin (∠ p₁ p₂ p₃)
Tactic: have sin_gt_zero : 0 < Real.sin (∠ p₁ p₂ p₃) := sin_pos_of_not_collinear h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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 : ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
sin_gt_zero : 0 < Real.sin (∠ p₁ p₂ p₃)
⊢ dist p₁ p₂ = dist p₃ p₁ * Real.sin (∠ p₂ p₃ p₁) / Real.sin (∠ p₁ p₂ p₃)
have field_simp : dist p₁ p₂ * Real.sin (∠ p₁ p₂ p₃) = dist p₃ p₁ * Real.sin (∠ p₂ p₃ p₁)
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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 : ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
sin_gt_zero : 0 < Real.sin (∠ p₁ p₂ p₃)
⊢ dist p₁ p₂ * Real.sin (∠ p₁ p₂ p₃) = dist p₃ p₁ * Real.sin (∠ p₂ p₃ p₁)
have rw : Real.sin (∠ p₁ p₂ p₃) * dist p₁ p₂ = dist p₃ p₁ * Real.sin (∠ p₂ p₃ p₁)
Tactic: rw [mul_comm, mul_comm (dist p₃ p₁), law_sin]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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 : ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
sin_gt_zero : 0 < Real.sin (∠ p₁ p₂ p₃)
rw : Real.sin (∠ p₁ p₂ p₃) * dist p₁ p₂ = dist p₃ p₁ * Real.sin (∠ p₂ p₃ p₁)
⊢ dist p₁ p₂ * Real.sin (∠ p₁ p₂ p₃) = dist p₃ p₁ * Real.sin (∠ p₂ p₃ p₁)
have rw₁ : Real.sin (∠ p₁ p₂ p₃) * dist p₁ p₂ = Real.sin (∠ p₂ p₃ p₁) * dist p₃ p₁
Tactic: rw [mul_comm, mul_comm (dist p₃ p₁), law_sin]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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 : ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
sin_gt_zero : 0 < Real.sin (∠ p₁ p₂ p₃)
rw : Real.sin (∠ p₁ p₂ p₃) * dist p₁ p₂ = dist p₃ p₁ * Real.sin (∠ p₂ p₃ p₁)
rw₁ : Real.sin (∠ p₁ p₂ p₃) * dist p₁ p₂ = Real.sin (∠ p₂ p₃ p₁) * dist p₃ p₁
⊢ dist p₁ p₂ * Real.sin (∠ p₁ p₂ p₃) = dist p₃ p₁ * Real.sin (∠ p₂ p₃ p₁)
have rw₂ : Real.sin (∠ p₁ p₂ p₃) * dist p₁ p₂ = Real.sin (∠ p₁ p₂ p₃) * dist p₁ p₂
Tactic: rw [mul_comm, mul_comm (dist p₃ p₁), law_sin]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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₃
⊢ ∠ p₁ p₂ p₃ = ∠ p₁ p₃ p₂
have h₁ : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
Tactic: rw [dist_eq_norm_vsub V p₁ p₂, dist_eq_norm_vsub V p₁ p₃] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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₁ -ᵥ p₃‖
⊢ InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = InnerProductGeometry.angle (p₁ -ᵥ p₃) (p₂ -ᵥ p₃)
have h₁ : p₃ -ᵥ p₂ = p₁ -ᵥ p₂ - (p₁ -ᵥ p₃)
Tactic: convert! angle_sub_eq_angle_sub_rev_of_norm_eq h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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₁ -ᵥ p₃‖
h₁ : p₃ -ᵥ p₂ = p₁ -ᵥ p₂ - (p₁ -ᵥ p₃)
⊢ InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = InnerProductGeometry.angle (p₁ -ᵥ p₃) (p₂ -ᵥ p₃)
have h₂ : p₂ -ᵥ p₃ = p₁ -ᵥ p₃ - (p₁ -ᵥ p₂)
Tactic: convert! angle_sub_eq_angle_sub_rev_of_norm_eq h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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 : InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = InnerProductGeometry.angle (p₁ -ᵥ p₃) (p₂ -ᵥ p₃)
hpi : InnerProductGeometry.angle (p₂ -ᵥ p₁) (p₃ -ᵥ p₁) ≠ π
⊢ dist p₁ p₂ = dist p₁ p₃
have rw : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
Tactic: rw [dist_eq_norm_vsub V p₁ p₂, dist_eq_norm_vsub V p₁ p₃]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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 : InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = InnerProductGeometry.angle (p₁ -ᵥ p₃) (p₂ -ᵥ p₃)
hpi : InnerProductGeometry.angle (p₂ -ᵥ p₁) (p₃ -ᵥ p₁) ≠ π
⊢ ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
have hpi₁ : InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₁ -ᵥ p₃) ≠ π
Tactic: rw [← angle_neg_neg, neg_vsub_eq_vsub_rev, neg_vsub_eq_vsub_rev] at hpi
Cleared hypotheses: hpi
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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 : InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = InnerProductGeometry.angle (p₁ -ᵥ p₃) (p₂ -ᵥ p₃)
hpi : InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₁ -ᵥ p₃) ≠ π
⊢ ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
have h₁ : InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₁ -ᵥ p₂ - (p₁ -ᵥ p₃)) =
  InnerProductGeometry.angle (p₁ -ᵥ p₃) (p₁ -ᵥ p₃ - (p₁ -ᵥ p₂))
Tactic: rw [← vsub_sub_vsub_cancel_left p₃ p₂ p₁, ← vsub_sub_vsub_cancel_left p₂ p₃ p₁] at h
Cleared hypotheses: h, hpi
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
inst_4 : Module.Oriented ℝ V (Fin 2)
inst_5 : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₃ p₁)
h0 : ∡ p₃ p₁ p₂ ≠ 0
hpi : ∡ p₃ p₁ p₂ ≠ (↑π : Real.Angle)
⊢ dist p₁ p₂ = ‖p₂ -ᵥ p₁‖
have h₁ : ‖p₂ -ᵥ p₁‖ = ‖p₂ -ᵥ p₁‖
Tactic: rw [dist_eq_norm_vsub']
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
inst_4 : Module.Oriented ℝ V (Fin 2)
inst_5 : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₃ p₁)
h0 : ∡ p₃ p₁ p₂ ≠ 0
hpi : ∡ p₃ p₁ p₂ ≠ (↑π : Real.Angle)
⊢ dist p₁ p₃ = ‖p₃ -ᵥ p₁‖
have h₁ : ‖p₃ -ᵥ p₁‖ = ‖p₃ -ᵥ p₁‖
Tactic: rw [dist_eq_norm_vsub']
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
inst_4 : Module.Oriented ℝ V (Fin 2)
inst_5 : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₃ p₁)
h0 : ∡ p₃ p₁ p₂ ≠ 0
hpi : ∡ p₃ p₁ p₂ ≠ (↑π : Real.Angle)
⊢ HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₃ -ᵥ p₁) (p₃ -ᵥ p₁ - (p₂ -ᵥ p₁))) =
    HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₂ -ᵥ p₁ - (p₃ -ᵥ p₁)) (p₂ -ᵥ p₁))
have rw : HSMul.hSMul (α := ℤ) 2 (-Orientation.oangle o (-(p₂ -ᵥ p₁)) (-(p₂ -ᵥ p₁ - (p₃ -ᵥ p₁)))) =
  HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₃ -ᵥ p₁) (p₃ -ᵥ p₁ - (p₂ -ᵥ p₁)))
Tactic: rw [eq_comm, o.oangle_rev, ← o.oangle_neg_neg]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
inst_4 : Module.Oriented ℝ V (Fin 2)
inst_5 : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₃ p₁)
h0 : ∡ p₃ p₁ p₂ ≠ 0
hpi : ∡ p₃ p₁ p₂ ≠ (↑π : Real.Angle)
⊢ HSMul.hSMul (α := ℤ) 2 (-Orientation.oangle o (-(p₂ -ᵥ p₁)) (-(p₂ -ᵥ p₁ - (p₃ -ᵥ p₁)))) =
    HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₃ -ᵥ p₁) (p₃ -ᵥ p₁ - (p₂ -ᵥ p₁)))
have nth_rw : HSMul.hSMul (α := ℤ) 2 (-Orientation.oangle o (-(p₂ -ᵥ p₁)) (-(p₂ -ᵥ p₁ - (p₃ -ᵥ p₁)))) =
  HSMul.hSMul (α := ℤ) 2 (-Orientation.oangle o (-(p₃ -ᵥ p₁ - (p₂ -ᵥ p₁))) (-(p₃ -ᵥ p₁)))
Tactic: nth_rw 2 [o.oangle_rev, ← o.oangle_neg_neg]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
inst_4 : Module.Oriented ℝ V (Fin 2)
inst_5 : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₃ p₁)
h0 : ∡ p₃ p₁ p₂ ≠ 0
hpi : ∡ p₃ p₁ p₂ ≠ (↑π : Real.Angle)
⊢ HSMul.hSMul (α := ℤ) 2 (-Orientation.oangle o (-(p₂ -ᵥ p₁)) (-(p₂ -ᵥ p₁ - (p₃ -ᵥ p₁)))) =
    HSMul.hSMul (α := ℤ) 2 (-Orientation.oangle o (-(p₃ -ᵥ p₁ - (p₂ -ᵥ p₁))) (-(p₃ -ᵥ p₁)))
have simp_rw : HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (-(p₂ -ᵥ p₁)) (-(p₂ -ᵥ p₁ - (p₃ -ᵥ p₁)))) =
  HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (-(p₃ -ᵥ p₁ - (p₂ -ᵥ p₁))) (-(p₃ -ᵥ p₁)))
Tactic: simp_rw [smul_neg, neg_inj]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
inst_4 : Module.Oriented ℝ V (Fin 2)
inst_5 : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h :
  HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)) =
    HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₂ -ᵥ p₃) (p₁ -ᵥ p₃))
h0 : ∡ p₃ p₁ p₂ ≠ 0
hpi : ∡ p₃ p₁ p₂ ≠ (↑π : Real.Angle)
⊢ HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (-(p₂ -ᵥ p₁)) (-(p₂ -ᵥ p₁ - (p₃ -ᵥ p₁)))) =
    HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (-(p₃ -ᵥ p₁ - (p₂ -ᵥ p₁))) (-(p₃ -ᵥ p₁)))
have h₁ : -(p₂ -ᵥ p₁) = p₁ -ᵥ p₂
Tactic: convert! h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
inst_4 : Module.Oriented ℝ V (Fin 2)
inst_5 : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h :
  HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)) =
    HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₂ -ᵥ p₃) (p₁ -ᵥ p₃))
h0 : ∡ p₃ p₁ p₂ ≠ 0
hpi : ∡ p₃ p₁ p₂ ≠ (↑π : Real.Angle)
h₁ : -(p₂ -ᵥ p₁) = p₁ -ᵥ p₂
⊢ HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (-(p₂ -ᵥ p₁)) (-(p₂ -ᵥ p₁ - (p₃ -ᵥ p₁)))) =
    HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (-(p₃ -ᵥ p₁ - (p₂ -ᵥ p₁))) (-(p₃ -ᵥ p₁)))
have h₂ : -(p₂ -ᵥ p₁ - (p₃ -ᵥ p₁)) = p₃ -ᵥ p₂
Tactic: convert! h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
inst_4 : Module.Oriented ℝ V (Fin 2)
inst_5 : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h :
  HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)) =
    HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₂ -ᵥ p₃) (p₁ -ᵥ p₃))
h0 : ∡ p₃ p₁ p₂ ≠ 0
hpi : ∡ p₃ p₁ p₂ ≠ (↑π : Real.Angle)
h₁ : -(p₂ -ᵥ p₁) = p₁ -ᵥ p₂
h₂ : -(p₂ -ᵥ p₁ - (p₃ -ᵥ p₁)) = p₃ -ᵥ p₂
⊢ HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (-(p₂ -ᵥ p₁)) (-(p₂ -ᵥ p₁ - (p₃ -ᵥ p₁)))) =
    HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (-(p₃ -ᵥ p₁ - (p₂ -ᵥ p₁))) (-(p₃ -ᵥ p₁)))
have h₃ : -(p₃ -ᵥ p₁ - (p₂ -ᵥ p₁)) = p₂ -ᵥ p₃
Tactic: convert! h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
inst_4 : Module.Oriented ℝ V (Fin 2)
inst_5 : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h :
  HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)) =
    HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₂ -ᵥ p₃) (p₁ -ᵥ p₃))
h0 : ∡ p₃ p₁ p₂ ≠ 0
hpi : ∡ p₃ p₁ p₂ ≠ (↑π : Real.Angle)
h₁ : -(p₂ -ᵥ p₁) = p₁ -ᵥ p₂
h₂ : -(p₂ -ᵥ p₁ - (p₃ -ᵥ p₁)) = p₃ -ᵥ p₂
h₃ : -(p₃ -ᵥ p₁ - (p₂ -ᵥ p₁)) = p₂ -ᵥ p₃
⊢ HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (-(p₂ -ᵥ p₁)) (-(p₂ -ᵥ p₁ - (p₃ -ᵥ p₁)))) =
    HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (-(p₃ -ᵥ p₁ - (p₂ -ᵥ p₁))) (-(p₃ -ᵥ p₁)))
have h₄ : -(p₃ -ᵥ p₁) = p₁ -ᵥ p₃
Tactic: convert! h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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₁ p₂ p₃ + ∠ p₂ p₃ p₁ + ∠ p₃ p₁ p₂ = π
have rw : ∠ p₃ p₁ p₂ + ∠ p₁ p₃ p₂ + ∠ p₁ p₂ p₃ = π
Tactic: rw [add_assoc, add_comm, add_comm (∠ p₂ p₃ p₁), angle_comm p₂ p₃ p₁]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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₁
⊢ InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₂ -ᵥ p₁) + InnerProductGeometry.angle (p₁ -ᵥ p₃) (p₂ -ᵥ p₃) +
      InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) =
    π
have rw : InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₂ -ᵥ p₁) + InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₃ -ᵥ p₁ - (p₂ -ᵥ p₁)) +
    InnerProductGeometry.angle (p₂ -ᵥ p₁) (p₂ -ᵥ p₁ - (p₃ -ᵥ p₁)) =
  π
Tactic: rw [← angle_neg_neg (p₁ -ᵥ p₃), ← angle_neg_neg (p₁ -ᵥ p₂), neg_vsub_eq_vsub_rev,
    neg_vsub_eq_vsub_rev, neg_vsub_eq_vsub_rev, neg_vsub_eq_vsub_rev, ←
    vsub_sub_vsub_cancel_right p₃ p₂ p₁, ← vsub_sub_vsub_cancel_right p₂ p₃ p₁]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
h : Sbtw ℝ p p₁ p₂
⊢ ∠ p₃ p₁ p = ∠ 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₂ - ∠ p₂ p₁ p₃) =
    0
Tactic: linarith [angle_add_angle_eq_pi_of_angle_eq_pi p₃ h.angle₁₂₃_eq_pi,
    angle_add_angle_add_angle_eq_pi p₃ h.right_ne.symm, angle_comm p₃ p₁ p₂]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
h : Sbtw ℝ 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₂ - ∠ p₂ p₁ p₃) =
      0
⊢ ∠ p₃ p₁ p = ∠ 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₂ - ∠ p₂ p₁ p₃) =
    0
Tactic: linarith [angle_add_angle_eq_pi_of_angle_eq_pi p₃ h.angle₁₂₃_eq_pi,
    angle_add_angle_add_angle_eq_pi p₃ h.right_ne.symm, angle_comm p₃ p₁ p₂]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
a b c p : P
hb : a ≠ b
hc : a ≠ c
hp : Wbtw ℝ b p c
⊢ ∠ b a p + ∠ p a c = ∠ b a c
have pos : ∀ (pb : p = b), ∠ b a p + ∠ p a c = ∠ b a c
Tactic: by_cases pb : p = b
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
a b c p : P
hb : a ≠ b
hc : a ≠ c
hp : Wbtw ℝ b p c
pos : ∀ (pb : p = b), ∠ b a p + ∠ p a c = ∠ b a c
⊢ ∠ b a p + ∠ p a c = ∠ b a c
have neg : ∀ (pb : ¬p = b), ∠ b a p + ∠ p a c = ∠ b a c
Tactic: by_cases pb : p = b
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
a b c p : P
hb : a ≠ b
hc : a ≠ c
hp : Wbtw ℝ b p c
pb : ¬p = b
⊢ ∠ b a p + ∠ p a c = ∠ b a c
have pos : ∀ (pc : p = c), ∠ b a p + ∠ p a c = ∠ b a c
Tactic: by_cases pc : p = c
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
a b c p : P
hb : a ≠ b
hc : a ≠ c
hp : Wbtw ℝ b p c
pb : ¬p = b
pos : ∀ (pc : p = c), ∠ b a p + ∠ p a c = ∠ b a c
⊢ ∠ b a p + ∠ p a c = ∠ b a c
have neg : ∀ (pc : ¬p = c), ∠ b a p + ∠ p a c = ∠ b a c
Tactic: by_cases pc : p = c
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
a b c p : P
hb : a ≠ b
hc : a ≠ c
hp : Wbtw ℝ b p c
pb : ¬p = b
pc : ¬p = c
⊢ ∠ b a p + ∠ p a c = ∠ b a c
have ea : ∠ b a c + ∠ a c b + ∠ c b a = π
Tactic: have ea := angle_add_angle_add_angle_eq_pi c hb
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
a b c p : P
hb : a ≠ b
hc : a ≠ c
hp : Wbtw ℝ b p c
pb : ¬p = b
pc : ¬p = c
ea : ∠ b a c + ∠ a c b + ∠ c b a = π
⊢ ∠ b a p + ∠ p a c = ∠ b a c
have eb : ∠ b a p + ∠ a p b + ∠ p b a = π
Tactic: have eb := angle_add_angle_add_angle_eq_pi p hb
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
a b c p : P
hb : a ≠ b
hc : a ≠ c
hp : Wbtw ℝ b p c
pb : ¬p = b
pc : ¬p = c
ea : ∠ b a c + ∠ a c b + ∠ c b a = π
eb : ∠ b a p + ∠ a p b + ∠ p b a = π
ec : ∠ a c p + ∠ c p a + ∠ p a c = π
⊢ ∠ b a p + ∠ p a c = ∠ b a c
have hp₁ : ∠ b p c = π
Tactic: replace hp : ∠ b p c = π := angle_eq_pi_iff_sbtw.mpr ⟨hp, pb, pc⟩
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
a b c p : P
hb : a ≠ b
hc : a ≠ c
pb : ¬p = b
pc : ¬p = c
ea : ∠ b a c + ∠ a c b + ∠ c b a = π
eb : ∠ b a p + ∠ a p b + ∠ p b a = π
ec : ∠ a c p + ∠ c p a + ∠ p a c = π
hp : ∠ b p c = π
⊢ ∠ c p b = π
have rwa : ∀ (hp : ∠ c p b = π), ∠ c p b = π
Tactic: rwa [angle_comm] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
a b c p : P
hb : a ≠ b
hc : a ≠ c
pb : ¬p = b
pc : ¬p = c
ea : ∠ b a c + ∠ a c b + ∠ c b a = π
eb : ∠ b a p + ∠ a p b + ∠ p b a = π
ec : ∠ a c p + ∠ c p a + ∠ p a c = π
hp : ∠ b p c = π
⊢ ∠ b a p + ∠ p a c = ∠ b a c
have hp' : ∠ c p b = π
Tactic: have hp' : ∠ c p b = π := by rwa [angle_comm] at hp
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
a b c p : P
hb : a ≠ b
hc : a ≠ c
pb : ¬p = b
pc : ¬p = c
ea : ∠ b a c + ∠ a c b + ∠ c b a = π
eb : ∠ b a p + ∠ a p b + ∠ p b a = π
ec : ∠ a c p + ∠ c p a + ∠ p a c = π
hp : ∠ b p c = π
hp' : ∠ c p b = π
⊢ ∠ b a p + ∠ p a c = ∠ b a c
have eb₁ : ∠ b a p + ∠ a p b + ∠ c b a = π
Tactic: rw [angle_comm p b a, angle_eq_angle_of_angle_eq_pi a hp, angle_comm a b c] at eb
Cleared hypotheses: eb, ec, hp, hp'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
a b c p : P
hb : a ≠ b
hc : a ≠ c
pb : ¬p = b
pc : ¬p = c
ea : ∠ b a c + ∠ a c b + ∠ c b a = π
eb : ∠ b a p + ∠ a p b + ∠ c b a = π
ec : ∠ a c p + ∠ c p a + ∠ p a c = π
hp : ∠ b p c = π
hp' : ∠ c p b = π
⊢ ∠ b a p + ∠ p a c = ∠ b a c
have ec₁ : ∠ a c b + ∠ a p c + ∠ p a c = π
Tactic: rw [angle_eq_angle_of_angle_eq_pi a hp', angle_comm c p a] at ec
Cleared hypotheses: ec, hp, hp'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
a b c p : P
hb : a ≠ b
hc : a ≠ c
pb : ¬p = b
pc : ¬p = c
ea : ∠ b a c + ∠ a c b + ∠ c b a = π
eb : ∠ b a p + ∠ a p b + ∠ c b a = π
ec : ∠ a c b + ∠ a p c + ∠ p a c = π
hp : ∠ b p c = π
hp' : ∠ c p b = π
⊢ ∠ b a p + ∠ p a c = ∠ b a c
have ep : ∠ a p b + ∠ a p c = π
Tactic: have ep := angle_add_angle_eq_pi_of_angle_eq_pi a hp