English
If the two lines determined by corresponding point pairs in two angles are parallel, then the doubled angles are equal.
Русский
Если прямые, соответствующие пары точек в двух углах, параллельны, то удвоенные углы равны.
LaTeX
$$$ (affineSpan Real (Set.insert p_1 (Set.singleton p_2))).Parallel (affineSpan Real (Set.insert p_4 (Set.singleton p_5))) \rightarrow\ (affineSpan Real (Set.insert p_3 (Set.singleton p_2))).Parallel (affineSpan Real (Set.insert p_6 (Set.singleton p_5))) \rightarrow\ (2 : \mathbb{Z}) \!\cdot \angle p_1 p_2 p_3 = (2 : \mathbb{Z}) \!\cdot \angle p_4 p_5 p_6$$
Lean4
/-- If the lines determined by corresponding pairs of points in two angles are parallel, twice
those angles are equal. -/
theorem two_zsmul_oangle_of_parallel {p₁ p₂ p₃ p₄ p₅ p₆ : P} (h₁₂₄₅ : line[ℝ, p₁, p₂] ∥ line[ℝ, p₄, p₅])
(h₃₂₆₅ : line[ℝ, p₃, p₂] ∥ line[ℝ, p₆, p₅]) : (2 : ℤ) • ∡ p₁ p₂ p₃ = (2 : ℤ) • ∡ p₄ p₅ p₆ :=
by
rw [AffineSubspace.affineSpan_pair_parallel_iff_vectorSpan_eq] at h₁₂₄₅ h₃₂₆₅
exact two_zsmul_oangle_of_vectorSpan_eq h₁₂₄₅ h₃₂₆₅
