English
In a parallelogram, the angle at the vertex splits into the sum of two adjacent angles with the opposite vertex and the angle at the other side.
Русский
В параллелограмме угол вершины раскладывается на сумму двух соседних углов напротив вершины и угла другой стороны.
LaTeX
$$$\angle x y = \angle x (x+y) + \angle y (x+y)$$$
Lean4
/-- In a paralellogram, the two parts of the inner angle add to the inner angle,
vector angle form. -/
theorem angle_eq_angle_add_add_angle_add (x : V) {y : V} (hy : y ≠ 0) : angle x y = angle x (x + y) + angle y (x + y) :=
by
rcases eq_or_ne x 0 with (rfl | hx)
· simp [hy]
have h :=
Real.Angle.cos_sin_inj (cos_angle_eq_cos_angle_add_add_angle_add hx hy)
(sin_angle_eq_sin_angle_add_add_angle_add hx hy)
rw [add_comm y x] at h
obtain ⟨_, ⟨n, rfl⟩, h⟩ := (QuotientAddGroup.mk'_eq_mk' _).mp h
simp only at h
have : -1 < n := by
replace h := h.ge
contrapose! h
grw [h, neg_smul, one_smul, angle_le_pi, ← angle_nonneg, ← angle_nonneg]
linear_combination Real.pi_pos
have : n < 1 := by
replace h := h.le
by_contra! hn
grw [← hn, one_smul, ← angle_nonneg x y, zero_add, two_mul] at h
have h' := h.trans_eq (add_comm _ _)
grw [angle_le_pi] at h' h
rw [add_le_add_iff_left, (angle_le_pi _ _).ge_iff_eq, angle_comm, angle_eq_pi_iff] at h' h
obtain ⟨hxy, r₁, r₁_pos, hr₁⟩ := h'
obtain ⟨-, r₂, r₂_pos, hr₂⟩ := h
have : (r₁ + r₂ - 1) • (x + y) = 0 := by rw [sub_smul, add_smul, one_smul, ← hr₁, ← hr₂, sub_eq_zero]
cases eq_zero_or_eq_zero_of_smul_eq_zero this
· linarith
· contradiction
obtain rfl : n = 0 := by cutsat
simpa using h
