Lean4
/-- Given two pairs of distinct points on the same line, such that the vectors between those
pairs of points are on the same ray (oriented in the same direction on that line), and a fifth
point, the angles at the fifth point between each of those two pairs of points have the same
sign. -/
theorem _root_.Collinear.oangle_sign_of_sameRay_vsub {p₁ p₂ p₃ p₄ : P} (p₅ : P) (hp₁p₂ : p₁ ≠ p₂) (hp₃p₄ : p₃ ≠ p₄)
(hc : Collinear ℝ ({ p₁, p₂, p₃, p₄ } : Set P)) (hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)) :
(∡ p₁ p₅ p₂).sign = (∡ p₃ p₅ p₄).sign :=
by
by_cases hc₅₁₂ : Collinear ℝ ({ p₅, p₁, p₂ } : Set P)
· have hc₅₁₂₃₄ : Collinear ℝ ({ p₅, p₁, p₂, p₃, p₄ } : Set P) :=
(hc.collinear_insert_iff_of_ne (Set.mem_insert _ _) (Set.mem_insert_of_mem _ (Set.mem_insert _ _)) hp₁p₂).2 hc₅₁₂
have hc₅₃₄ : Collinear ℝ ({ p₅, p₃, p₄ } : Set P) :=
(hc.collinear_insert_iff_of_ne (Set.mem_insert_of_mem _ (Set.mem_insert_of_mem _ (Set.mem_insert _ _)))
(Set.mem_insert_of_mem _ (Set.mem_insert_of_mem _ (Set.mem_insert_of_mem _ (Set.mem_singleton _)))) hp₃p₄).1
hc₅₁₂₃₄
rw [Set.insert_comm] at hc₅₁₂ hc₅₃₄
have hs₁₅₂ := oangle_eq_zero_or_eq_pi_iff_collinear.2 hc₅₁₂
have hs₃₅₄ := oangle_eq_zero_or_eq_pi_iff_collinear.2 hc₅₃₄
rw [← Real.Angle.sign_eq_zero_iff] at hs₁₅₂ hs₃₅₄
rw [hs₁₅₂, hs₃₅₄]
· let s : Set (P × P × P) :=
(fun x : line[ℝ, p₁, p₂] × V => (x.1, p₅, x.2 +ᵥ (x.1 : P))) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
have hco : IsConnected s :=
haveI : ConnectedSpace line[ℝ, p₁, p₂] := AddTorsor.connectedSpace _ _
(isConnected_univ.prod (isConnected_setOf_sameRay_and_ne_zero (vsub_ne_zero.2 hp₁p₂.symm))).image _ (by fun_prop)
have hf : ContinuousOn (fun p : P × P × P => ∡ p.1 p.2.1 p.2.2) s :=
by
refine continuousOn_of_forall_continuousAt fun p hp => continuousAt_oangle ?_ ?_
all_goals
simp_rw [s, Set.mem_image, Set.mem_prod, Set.mem_univ, true_and, Prod.ext_iff] at hp
obtain ⟨q₁, q₅, q₂⟩ := p
dsimp only at hp ⊢
obtain ⟨⟨⟨q, hq⟩, v⟩, hv, rfl, rfl, rfl⟩ := hp
dsimp only [Subtype.coe_mk, Set.mem_setOf] at hv ⊢
obtain ⟨hvr, -⟩ := hv
rintro rfl
refine hc₅₁₂ ((collinear_insert_iff_of_mem_affineSpan ?_).2 (collinear_pair _ _ _))
· exact hq
· refine vadd_mem_of_mem_direction ?_ hq
rw [← exists_nonneg_left_iff_sameRay (vsub_ne_zero.2 hp₁p₂.symm)] at hvr
obtain ⟨r, -, rfl⟩ := hvr
rw [direction_affineSpan]
exact smul_vsub_rev_mem_vectorSpan_pair _ _ _
have hsp : ∀ p : P × P × P, p ∈ s → ∡ p.1 p.2.1 p.2.2 ≠ 0 ∧ ∡ p.1 p.2.1 p.2.2 ≠ π :=
by
intro p hp
simp_rw [s, Set.mem_image, Set.mem_prod, Set.mem_setOf, Set.mem_univ, true_and, Prod.ext_iff] at hp
obtain ⟨q₁, q₅, q₂⟩ := p
dsimp only at hp ⊢
obtain ⟨⟨⟨q, hq⟩, v⟩, hv, rfl, rfl, rfl⟩ := hp
dsimp only [Subtype.coe_mk, Set.mem_setOf] at hv ⊢
obtain ⟨hvr, hv0⟩ := hv
rw [← exists_nonneg_left_iff_sameRay (vsub_ne_zero.2 hp₁p₂.symm)] at hvr
obtain ⟨r, -, rfl⟩ := hvr
change q ∈ line[ℝ, p₁, p₂] at hq
rw [oangle_ne_zero_and_ne_pi_iff_affineIndependent]
refine
affineIndependent_of_ne_of_mem_of_notMem_of_mem ?_ hq
(fun h => hc₅₁₂ ((collinear_insert_iff_of_mem_affineSpan h).2 (collinear_pair _ _ _))) ?_
· rwa [← @vsub_ne_zero V, vsub_vadd_eq_vsub_sub, vsub_self, zero_sub, neg_ne_zero]
· refine vadd_mem_of_mem_direction ?_ hq
rw [direction_affineSpan]
exact smul_vsub_rev_mem_vectorSpan_pair _ _ _
have hp₁p₂s : (p₁, p₅, p₂) ∈ s :=
by
simp_rw [s, Set.mem_image, Set.mem_prod, Set.mem_setOf, Set.mem_univ, true_and, Prod.ext_iff]
refine ⟨⟨⟨p₁, left_mem_affineSpan_pair ℝ _ _⟩, p₂ -ᵥ p₁⟩, ⟨SameRay.rfl, vsub_ne_zero.2 hp₁p₂.symm⟩, ?_⟩
simp
have hp₃p₄s : (p₃, p₅, p₄) ∈ s :=
by
simp_rw [s, Set.mem_image, Set.mem_prod, Set.mem_setOf, Set.mem_univ, true_and, Prod.ext_iff]
refine
⟨⟨⟨p₃,
hc.mem_affineSpan_of_mem_of_ne (Set.mem_insert _ _) (Set.mem_insert_of_mem _ (Set.mem_insert _ _))
(Set.mem_insert_of_mem _ (Set.mem_insert_of_mem _ (Set.mem_insert _ _))) hp₁p₂⟩,
p₄ -ᵥ p₃⟩,
⟨hr, vsub_ne_zero.2 hp₃p₄.symm⟩, ?_⟩
simp
convert Real.Angle.sign_eq_of_continuousOn hco hf hsp hp₃p₄s hp₁p₂s
