awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ affineSpan ℝ {p₁, p₃}
h₄ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₃}) p₄
h₆ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₃}) p₆
h₁₂₄₅ : AffineSubspace.Parallel (P := P) (affineSpan ℝ {p₁, p₂}) (affineSpan ℝ {p₄, p₅})
h₃₂₆₅ : AffineSubspace.Parallel (P := P) (affineSpan ℝ {p₃, p₂}) (affineSpan ℝ {p₆, p₅})
hd :
  LE.le (α := Submodule ℝ V) (AffineSubspace.direction (P := P) (affineSpan ℝ {p₆, p₄}))
    (AffineSubspace.direction (P := P) (affineSpan ℝ {p₃, p₁}))
r : ℝ
hr : r ≠ 0
h₅₄ : p₄ -ᵥ p₅ = r • (p₁ -ᵥ p₂)
h₆₅ : p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂)
inl :
  ∀ (hlt : r < 0), Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = Orientation.oangle o (r • (p₁ -ᵥ p₂)) (r • (p₃ -ᵥ p₂))
⊢ Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = Orientation.oangle o (r • (p₁ -ᵥ p₂)) (r • (p₃ -ᵥ p₂))
have inr : ∀ (hlt : 0 < r), Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = Orientation.oangle o (r • (p₁ -ᵥ p₂)) (r • (p₃ -ᵥ p₂))
Tactic: rcases hr.lt_or_gt with hlt | hlt
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : dist p₁ p₂ = dist p₁ p₃
⊢ ∡ p₁ p₂ p₃ = ∡ p₂ p₃ p₁
have h₁ : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
Tactic: simp_rw [dist_eq_norm_vsub V] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ ∡ p₁ p₂ p₃ = ∡ p₂ p₃ p₁
have rw : Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = ∡ p₂ p₃ p₁
Tactic: rw [oangle, oangle, ← vsub_sub_vsub_cancel_left p₃ p₂ p₁, ← vsub_sub_vsub_cancel_left p₂ p₃ p₁,
    o.oangle_sub_eq_oangle_sub_rev_of_norm_eq h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
rw : Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = ∡ p₂ p₃ p₁
⊢ ∡ p₁ p₂ p₃ = ∡ p₂ p₃ p₁
have rw₁ : Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = Orientation.oangle o (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)
Tactic: rw [oangle, oangle, ← vsub_sub_vsub_cancel_left p₃ p₂ p₁, ← vsub_sub_vsub_cancel_left p₂ p₃ p₁,
    o.oangle_sub_eq_oangle_sub_rev_of_norm_eq h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
rw : Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = ∡ p₂ p₃ p₁
rw₁ : Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = Orientation.oangle o (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)
⊢ ∡ p₁ p₂ p₃ = ∡ p₂ p₃ p₁
have rw₂ : Orientation.oangle o (p₁ -ᵥ p₂) (p₁ -ᵥ p₂ - (p₁ -ᵥ p₃)) = Orientation.oangle o (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)
Tactic: rw [oangle, oangle, ← vsub_sub_vsub_cancel_left p₃ p₂ p₁, ← vsub_sub_vsub_cancel_left p₂ p₃ p₁,
    o.oangle_sub_eq_oangle_sub_rev_of_norm_eq h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
rw : Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = ∡ p₂ p₃ p₁
rw₁ : Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = Orientation.oangle o (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)
rw₂ : Orientation.oangle o (p₁ -ᵥ p₂) (p₁ -ᵥ p₂ - (p₁ -ᵥ p₃)) = Orientation.oangle o (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)
⊢ ∡ p₁ p₂ p₃ = ∡ p₂ p₃ p₁
have rw₃ : Orientation.oangle o (p₁ -ᵥ p₂) (p₁ -ᵥ p₂ - (p₁ -ᵥ p₃)) = Orientation.oangle o (p₁ -ᵥ p₃ - (p₁ -ᵥ p₂)) (p₁ -ᵥ p₃)
Tactic: rw [oangle, oangle, ← vsub_sub_vsub_cancel_left p₃ p₂ p₁, ← vsub_sub_vsub_cancel_left p₂ p₃ p₁,
    o.oangle_sub_eq_oangle_sub_rev_of_norm_eq h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
rw : Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = ∡ p₂ p₃ p₁
rw₁ : Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = Orientation.oangle o (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)
rw₂ : Orientation.oangle o (p₁ -ᵥ p₂) (p₁ -ᵥ p₂ - (p₁ -ᵥ p₃)) = Orientation.oangle o (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)
rw₃ : Orientation.oangle o (p₁ -ᵥ p₂) (p₁ -ᵥ p₂ - (p₁ -ᵥ p₃)) = Orientation.oangle o (p₁ -ᵥ p₃ - (p₁ -ᵥ p₂)) (p₁ -ᵥ p₃)
⊢ ∡ p₁ p₂ p₃ = ∡ p₂ p₃ p₁
have rw₄ : Orientation.oangle o (p₁ -ᵥ p₃ - (p₁ -ᵥ p₂)) (p₁ -ᵥ p₃) = Orientation.oangle o (p₁ -ᵥ p₃ - (p₁ -ᵥ p₂)) (p₁ -ᵥ p₃)
Tactic: rw [oangle, oangle, ← vsub_sub_vsub_cancel_left p₃ p₂ p₁, ← vsub_sub_vsub_cancel_left p₂ p₃ p₁,
    o.oangle_sub_eq_oangle_sub_rev_of_norm_eq h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
hn : p₂ ≠ p₃
h : dist p₁ p₂ = dist p₁ p₃
⊢ ∡ p₃ p₁ p₂ = (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃)
have h₁ : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
Tactic: simp_rw [dist_eq_norm_vsub V] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
hn : p₂ ≠ p₃
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ Orientation.oangle o (p₃ -ᵥ p₁) (p₂ -ᵥ p₁) =
    (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂))
have h₁ : Orientation.oangle o (p₃ -ᵥ p₁) (p₂ -ᵥ p₁) = Orientation.oangle o (p₁ -ᵥ p₃) (p₁ -ᵥ p₂)
Tactic: convert! o.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq _ h using 1
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
hn : p₂ ≠ p₃
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
h₁ : Orientation.oangle o (p₃ -ᵥ p₁) (p₂ -ᵥ p₁) = Orientation.oangle o (p₁ -ᵥ p₃) (p₁ -ᵥ p₂)
⊢ Orientation.oangle o (p₃ -ᵥ p₁) (p₂ -ᵥ p₁) =
    (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂))
have h₂ : (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)) =
  (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₁ -ᵥ p₃ - (p₁ -ᵥ p₂)) (p₁ -ᵥ p₃))
Tactic: convert! o.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq _ h using 1
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
hn : p₂ ≠ p₃
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
h₁ : Orientation.oangle o (p₃ -ᵥ p₁) (p₂ -ᵥ p₁) = Orientation.oangle o (p₁ -ᵥ p₃) (p₁ -ᵥ p₂)
h₂ :
  (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)) =
    (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₁ -ᵥ p₃ - (p₁ -ᵥ p₂)) (p₁ -ᵥ p₃))
⊢ Orientation.oangle o (p₃ -ᵥ p₁) (p₂ -ᵥ p₁) =
    (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂))
have convert! : p₁ -ᵥ p₂ ≠ p₁ -ᵥ p₃
Tactic: convert! o.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq _ h using 1
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
hn : p₂ ≠ p₃
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ Orientation.oangle o (p₃ -ᵥ p₁) (p₂ -ᵥ p₁) = Orientation.oangle o (p₁ -ᵥ p₃) (p₁ -ᵥ p₂)
have h₁ : Orientation.oangle o (-(p₁ -ᵥ p₃)) (p₂ -ᵥ p₁) = Orientation.oangle o (p₁ -ᵥ p₃) (p₁ -ᵥ p₂)
Tactic: rw [← neg_vsub_eq_vsub_rev p₁ p₃, ← neg_vsub_eq_vsub_rev p₁ p₂, o.oangle_neg_neg]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
hn : p₂ ≠ p₃
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
h₁ : Orientation.oangle o (-(p₁ -ᵥ p₃)) (p₂ -ᵥ p₁) = Orientation.oangle o (p₁ -ᵥ p₃) (p₁ -ᵥ p₂)
⊢ Orientation.oangle o (p₃ -ᵥ p₁) (p₂ -ᵥ p₁) = Orientation.oangle o (p₁ -ᵥ p₃) (p₁ -ᵥ p₂)
have h₂ : Orientation.oangle o (-(p₁ -ᵥ p₃)) (-(p₁ -ᵥ p₂)) = Orientation.oangle o (p₁ -ᵥ p₃) (p₁ -ᵥ p₂)
Tactic: rw [← neg_vsub_eq_vsub_rev p₁ p₃, ← neg_vsub_eq_vsub_rev p₁ p₂, o.oangle_neg_neg]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
hn : p₂ ≠ p₃
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
h₁ : Orientation.oangle o (-(p₁ -ᵥ p₃)) (p₂ -ᵥ p₁) = Orientation.oangle o (p₁ -ᵥ p₃) (p₁ -ᵥ p₂)
h₂ : Orientation.oangle o (-(p₁ -ᵥ p₃)) (-(p₁ -ᵥ p₂)) = Orientation.oangle o (p₁ -ᵥ p₃) (p₁ -ᵥ p₂)
⊢ Orientation.oangle o (p₃ -ᵥ p₁) (p₂ -ᵥ p₁) = Orientation.oangle o (p₁ -ᵥ p₃) (p₁ -ᵥ p₂)
have h₃ : Orientation.oangle o (p₁ -ᵥ p₃) (p₁ -ᵥ p₂) = Orientation.oangle o (p₁ -ᵥ p₃) (p₁ -ᵥ p₂)
Tactic: rw [← neg_vsub_eq_vsub_rev p₁ p₃, ← neg_vsub_eq_vsub_rev p₁ p₂, o.oangle_neg_neg]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
hn : p₂ ≠ p₃
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)) =
    (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₁ -ᵥ p₃ - (p₁ -ᵥ p₂)) (p₁ -ᵥ p₃))
have h₁ : (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)) =
  (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₁ -ᵥ p₂) (p₁ -ᵥ p₂ - (p₁ -ᵥ p₃)))
Tactic: rw [← o.oangle_sub_eq_oangle_sub_rev_of_norm_eq h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : dist p₁ p₂ = dist p₁ p₃
⊢ |(∡ p₁ p₂ p₃).toReal| < π / 2
have h₁ : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
Tactic: simp_rw [dist_eq_norm_vsub V] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ |(∡ p₁ p₂ p₃).toReal| < π / 2
have rw : |(Orientation.oangle o (p₁ -ᵥ p₂) (p₁ -ᵥ p₂ - (p₁ -ᵥ p₃))).toReal| < π / 2
Tactic: rw [oangle, ← vsub_sub_vsub_cancel_left p₃ p₂ p₁]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p p₁ p₂ : P
h : (∡ p₁ p p₂).sign = 0
⊢ p₁ = p ∨ p₂ = p ∨ ∠ p₁ p p₂ = 0 ∨ ∠ p₁ p p₂ = π
have h₁ : p₁ = p ↔ p₁ -ᵥ p = 0
Tactic: convert! o.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p p₁ p₂ : P
h : (∡ p₁ p p₂).sign = 0
h₁ : p₁ = p ↔ p₁ -ᵥ p = 0
⊢ p₁ = p ∨ p₂ = p ∨ ∠ p₁ p p₂ = 0 ∨ ∠ p₁ p p₂ = π
have h₂ : p₂ = p ↔ p₂ -ᵥ p = 0
Tactic: convert! o.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
⊢ ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ ∨ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆
have h_1 : ∡ p₁ p₂ p₃ = (↑(∠ p₁ p₂ p₃) : Real.Angle) ∨ ∡ p₁ p₂ p₃ = -(↑(∠ p₁ p₂ p₃) : Real.Angle)
Tactic: have h_1 := EuclideanGeometry.oangle_eq_angle_or_eq_neg_angle h1.symm h2.symm
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
h_1 : ∡ p₁ p₂ p₃ = (↑(∠ p₁ p₂ p₃) : Real.Angle) ∨ ∡ p₁ p₂ p₃ = -(↑(∠ p₁ p₂ p₃) : Real.Angle)
⊢ ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ ∨ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆
have h_2 : ∡ p₄ p₅ p₆ = (↑(∠ p₄ p₅ p₆) : Real.Angle) ∨ ∡ p₄ p₅ p₆ = -(↑(∠ p₄ p₅ p₆) : Real.Angle)
Tactic: have h_2 := EuclideanGeometry.oangle_eq_angle_or_eq_neg_angle h3.symm h4.symm
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
h_1 : ∡ p₁ p₂ p₃ = (↑(∠ p₁ p₂ p₃) : Real.Angle) ∨ ∡ p₁ p₂ p₃ = -(↑(∠ p₁ p₂ p₃) : Real.Angle)
h_2 : ∡ p₄ p₅ p₆ = (↑(∠ p₄ p₅ p₆) : Real.Angle) ∨ ∡ p₄ p₅ p₆ = -(↑(∠ p₄ p₅ p₆) : Real.Angle)
⊢ ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ ∨ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆
have inl : ∀ (h₁ : ∡ p₁ p₂ p₃ = (↑(∠ p₁ p₂ p₃) : Real.Angle)), ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ ∨ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆
Tactic: rcases h_1 with h₁ | h₁
Cleared hypotheses: h_1
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
h_1 : ∡ p₁ p₂ p₃ = (↑(∠ p₁ p₂ p₃) : Real.Angle) ∨ ∡ p₁ p₂ p₃ = -(↑(∠ p₁ p₂ p₃) : Real.Angle)
h_2 : ∡ p₄ p₅ p₆ = (↑(∠ p₄ p₅ p₆) : Real.Angle) ∨ ∡ p₄ p₅ p₆ = -(↑(∠ p₄ p₅ p₆) : Real.Angle)
inl : ∀ (h₁ : ∡ p₁ p₂ p₃ = (↑(∠ p₁ p₂ p₃) : Real.Angle)), ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ ∨ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆
⊢ ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ ∨ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆
have inr : ∀ (h₁ : ∡ p₁ p₂ p₃ = -(↑(∠ p₁ p₂ p₃) : Real.Angle)), ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ ∨ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆
Tactic: rcases h_1 with h₁ | h₁
Cleared hypotheses: h_1
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
h_2 : ∡ p₄ p₅ p₆ = (↑(∠ p₄ p₅ p₆) : Real.Angle) ∨ ∡ p₄ p₅ p₆ = -(↑(∠ p₄ p₅ p₆) : Real.Angle)
h₁ : ∡ p₁ p₂ p₃ = (↑(∠ p₁ p₂ p₃) : Real.Angle)
⊢ ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ ∨ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆
have inl : ∀ (h₂ : ∡ p₄ p₅ p₆ = (↑(∠ p₄ p₅ p₆) : Real.Angle)), ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ ∨ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆
Tactic: rcases h_2 with h₂ | h₂
Cleared hypotheses: h_2
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
h_2 : ∡ p₄ p₅ p₆ = (↑(∠ p₄ p₅ p₆) : Real.Angle) ∨ ∡ p₄ p₅ p₆ = -(↑(∠ p₄ p₅ p₆) : Real.Angle)
h₁ : ∡ p₁ p₂ p₃ = (↑(∠ p₁ p₂ p₃) : Real.Angle)
inl : ∀ (h₂ : ∡ p₄ p₅ p₆ = (↑(∠ p₄ p₅ p₆) : Real.Angle)), ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ ∨ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆
⊢ ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ ∨ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆
have inl₁ : ∀ (h₂ : ∡ p₄ p₅ p₆ = -(↑(∠ p₄ p₅ p₆) : Real.Angle)), ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ ∨ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆
Tactic: rcases h_2 with h₂ | h₂
Cleared hypotheses: h_2
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
h_2 : ∡ p₄ p₅ p₆ = (↑(∠ p₄ p₅ p₆) : Real.Angle) ∨ ∡ p₄ p₅ p₆ = -(↑(∠ p₄ p₅ p₆) : Real.Angle)
h₁ : ∡ p₁ p₂ p₃ = -(↑(∠ p₁ p₂ p₃) : Real.Angle)
⊢ ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ ∨ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆
have inr : ∀ (h₂ : ∡ p₄ p₅ p₆ = (↑(∠ p₄ p₅ p₆) : Real.Angle)), ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ ∨ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆
Tactic: rcases h_2 with h₂ | h₂
Cleared hypotheses: h_2
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
h_2 : ∡ p₄ p₅ p₆ = (↑(∠ p₄ p₅ p₆) : Real.Angle) ∨ ∡ p₄ p₅ p₆ = -(↑(∠ p₄ p₅ p₆) : Real.Angle)
h₁ : ∡ p₁ p₂ p₃ = -(↑(∠ p₁ p₂ p₃) : Real.Angle)
inr : ∀ (h₂ : ∡ p₄ p₅ p₆ = (↑(∠ p₄ p₅ p₆) : Real.Angle)), ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ ∨ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆
⊢ ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ ∨ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆
have inr₁ : ∀ (h₂ : ∡ p₄ p₅ p₆ = -(↑(∠ p₄ p₅ p₆) : Real.Angle)), ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ ∨ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆
Tactic: rcases h_2 with h₂ | h₂
Cleared hypotheses: h_2
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
h₁ : ∡ p₁ p₂ p₃ = (↑(∠ p₁ p₂ p₃) : Real.Angle)
h₂ : ∡ p₄ p₅ p₆ = (↑(∠ p₄ p₅ p₆) : Real.Angle)
⊢ ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ ∨ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆
have inl : ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆
Tactic: left
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
h₁ : ∡ p₁ p₂ p₃ = (↑(∠ p₁ p₂ p₃) : Real.Angle)
h₂ : ∡ p₄ p₅ p₆ = (↑(∠ p₄ p₅ p₆) : Real.Angle)
⊢ ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆
have inl : (↑(∠ p₁ p₂ p₃) : Real.Angle) = ∡ p₄ p₅ p₆
Tactic: rw [h₁, h₂, h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
h₁ : ∡ p₁ p₂ p₃ = (↑(∠ p₁ p₂ p₃) : Real.Angle)
h₂ : ∡ p₄ p₅ p₆ = (↑(∠ p₄ p₅ p₆) : Real.Angle)
inl : (↑(∠ p₁ p₂ p₃) : Real.Angle) = ∡ p₄ p₅ p₆
⊢ ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆
have inl₁ : (↑(∠ p₁ p₂ p₃) : Real.Angle) = (↑(∠ p₄ p₅ p₆) : Real.Angle)
Tactic: rw [h₁, h₂, h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
h₁ : ∡ p₁ p₂ p₃ = (↑(∠ p₁ p₂ p₃) : Real.Angle)
h₂ : ∡ p₄ p₅ p₆ = (↑(∠ p₄ p₅ p₆) : Real.Angle)
inl : (↑(∠ p₁ p₂ p₃) : Real.Angle) = ∡ p₄ p₅ p₆
inl₁ : (↑(∠ p₁ p₂ p₃) : Real.Angle) = (↑(∠ p₄ p₅ p₆) : Real.Angle)
⊢ ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆
have inl₂ : (↑(∠ p₄ p₅ p₆) : Real.Angle) = (↑(∠ p₄ p₅ p₆) : Real.Angle)
Tactic: rw [h₁, h₂, h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
h₁ : ∡ p₁ p₂ p₃ = (↑(∠ p₁ p₂ p₃) : Real.Angle)
h₂ : ∡ p₄ p₅ p₆ = -(↑(∠ p₄ p₅ p₆) : Real.Angle)
⊢ ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ ∨ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆
have inl : ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆
Tactic: right
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
h₁ : ∡ p₁ p₂ p₃ = (↑(∠ p₁ p₂ p₃) : Real.Angle)
h₂ : ∡ p₄ p₅ p₆ = -(↑(∠ p₄ p₅ p₆) : Real.Angle)
⊢ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆
have inl : (↑(∠ p₁ p₂ p₃) : Real.Angle) = -∡ p₄ p₅ p₆
Tactic: rw [h₁, h₂, h, neg_neg]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
h₁ : ∡ p₁ p₂ p₃ = (↑(∠ p₁ p₂ p₃) : Real.Angle)
h₂ : ∡ p₄ p₅ p₆ = -(↑(∠ p₄ p₅ p₆) : Real.Angle)
inl : (↑(∠ p₁ p₂ p₃) : Real.Angle) = -∡ p₄ p₅ p₆
⊢ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆
have inl₁ : (↑(∠ p₁ p₂ p₃) : Real.Angle) = - -(↑(∠ p₄ p₅ p₆) : Real.Angle)
Tactic: rw [h₁, h₂, h, neg_neg]