From 3396ec6130e854fec8a0343b8f58071bfb4a6929 Mon Sep 17 00:00:00 2001 From: Wang Ying Date: Sun, 10 Aug 2025 16:22:31 +0800 Subject: [PATCH 1/9] add Exterior angle theorem --- Mathlib/Geometry/Euclidean/Triangle.lean | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/Mathlib/Geometry/Euclidean/Triangle.lean b/Mathlib/Geometry/Euclidean/Triangle.lean index 14aa2ee49e5bfe..ee93d57e75d437 100644 --- a/Mathlib/Geometry/Euclidean/Triangle.lean +++ b/Mathlib/Geometry/Euclidean/Triangle.lean @@ -403,4 +403,19 @@ theorem dist_mul_of_eq_angle_of_dist_mul (a b c a' b' c' : P) (r : ℝ) (h : ∠ have h2 : 0 ≤ r := nonneg_of_mul_nonneg_left h1 (dist_pos.mpr hab₁) exact (sq_eq_sq₀ dist_nonneg (mul_nonneg h2 dist_nonneg)).mp h' +/-- **Exterior angle theorem**. -/ +theorem exterior_angle_eq_angle_add_angle {p₁ p₂ p₃ : P} (p : P) (h_Sbtw : Sbtw ℝ p p₁ p₂) : + ∠ p₃ p₁ p = ∠ p₁ p₃ p₂ + ∠ p₃ p₂ p₁ := by + have h_pi : ∠ p p₁ p₂ = π := by + rw[Sbtw.angle₁₂₃_eq_pi] + assumption + have h1 : ∠ p₃ p₁ p + ∠ p₃ p₁ p₂ = π := by + rw [← EuclideanGeometry.angle_add_angle_eq_pi_of_angle_eq_pi p₃ h_pi] + have h₁₂ : p₁ ≠ p₂ := by + exact Ne.symm (Sbtw.right_ne h_Sbtw) + have h2 := angle_add_angle_add_angle_eq_pi p₃ h₁₂ + rw[show ∠ p₃ p₁ p₂ = ∠ p₂ p₁ p₃ by rw[angle_comm], add_comm, ← h2, add_assoc] at h1 + simp at h1 + rw [h1] + end EuclideanGeometry From 3e979e3a19a0b3865362c6669e2c337ccd450ba3 Mon Sep 17 00:00:00 2001 From: Wang Ying Date: Sat, 6 Sep 2025 12:28:53 +0800 Subject: [PATCH 2/9] conflict solved --- Mathlib/Geometry/Euclidean/Triangle.lean | 28 ++++++++++-------------- 1 file changed, 11 insertions(+), 17 deletions(-) diff --git a/Mathlib/Geometry/Euclidean/Triangle.lean b/Mathlib/Geometry/Euclidean/Triangle.lean index a51a3390014b99..64e5f4dd7cee94 100644 --- a/Mathlib/Geometry/Euclidean/Triangle.lean +++ b/Mathlib/Geometry/Euclidean/Triangle.lean @@ -343,22 +343,6 @@ theorem dist_mul_of_eq_angle_of_dist_mul (a b c a' b' c' : P) (r : ℝ) (h : ∠ have h2 : 0 ≤ r := nonneg_of_mul_nonneg_left h1 (dist_pos.mpr hab₁) exact (sq_eq_sq₀ dist_nonneg (mul_nonneg h2 dist_nonneg)).mp h' -<<<<<<< HEAD -/-- **Exterior angle theorem**. -/ -theorem exterior_angle_eq_angle_add_angle {p₁ p₂ p₃ : P} (p : P) (h_Sbtw : Sbtw ℝ p p₁ p₂) : - ∠ p₃ p₁ p = ∠ p₁ p₃ p₂ + ∠ p₃ p₂ p₁ := by - have h_pi : ∠ p p₁ p₂ = π := by - rw[Sbtw.angle₁₂₃_eq_pi] - assumption - have h1 : ∠ p₃ p₁ p + ∠ p₃ p₁ p₂ = π := by - rw [← EuclideanGeometry.angle_add_angle_eq_pi_of_angle_eq_pi p₃ h_pi] - have h₁₂ : p₁ ≠ p₂ := by - exact Ne.symm (Sbtw.right_ne h_Sbtw) - have h2 := angle_add_angle_add_angle_eq_pi p₃ h₁₂ - rw[show ∠ p₃ p₁ p₂ = ∠ p₂ p₁ p₃ by rw[angle_comm], add_comm, ← h2, add_assoc] at h1 - simp at h1 - rw [h1] -======= /-- In a triangle, the smaller angle is opposite the smaller side. -/ theorem dist_lt_of_angle_lt {a b c : P} (h : ¬Collinear ℝ ({a, b, c} : Set P)) : ∠ a c b < ∠ a b c → dist a b < dist a c := by @@ -421,6 +405,16 @@ theorem angle_le_iff_dist_le {a b c : P} (h : ¬Collinear ℝ ({a, b, c} : Set P have h1 := (angle_lt_iff_dist_lt h).not simp at h1 exact h1 ->>>>>>> upstream/master + +/-- **Exterior angle theorem**. -/ +theorem exterior_angle_eq_angle_add_angle {p₁ p₂ p₃ : P} (p : P) (h : Sbtw ℝ p p₁ p₂) : + ∠ p₃ p₁ p = ∠ p₁ p₃ p₂ + ∠ p₃ p₂ p₁ := by + have H := (EuclideanGeometry.angle_add_angle_eq_pi_of_angle_eq_pi p₃ (Sbtw.angle₁₂₃_eq_pi h)).symm + rw [show ∠ p₃ p₁ p₂ = ∠ p₂ p₁ p₃ by simp only [angle_comm], + add_comm, + ← angle_add_angle_add_angle_eq_pi p₃ ((Sbtw.right_ne h).symm), + add_assoc] at H + simp only [add_right_inj] at H + rw [H] end EuclideanGeometry From ddec112e6b8bf3ba622dfc6c649a1b8a02cda92d Mon Sep 17 00:00:00 2001 From: yulia Date: Mon, 29 Dec 2025 19:56:07 +0800 Subject: [PATCH 3/9] add some angle theorem about Wbtw and Sbtw --- .../Euclidean/Angle/Unoriented/Affine.lean | 41 +++++++++++++++++++ Mathlib/Geometry/Euclidean/Triangle.lean | 11 ----- 2 files changed, 41 insertions(+), 11 deletions(-) diff --git a/Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean b/Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean index 301de95fd6dc1e..aa259ea2f3aa59 100644 --- a/Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean +++ b/Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean @@ -373,6 +373,47 @@ theorem angle_eq_zero_iff_eq_and_ne_or_sbtw {p₁ p₂ p₃ : P} : by_cases hp₃p₂ : p₃ = p₂; · simp [hp₃p₂] simp [hp₁p₂, hp₁p₃, Ne.symm hp₁p₃, Sbtw, hp₃p₂] +/-- An Unoriented angle is unchanged by replacing the third point by one strictly further away on +the same ray. -/ +theorem _root_.Sbtw.angle_eq_right {p₁ p₂ p₃ p₃' : P} (h : Sbtw ℝ p₂ p₃ p₃') : + ∠ p₁ p₂ p₃ = ∠ p₁ p₂ p₃' := by + rw [angle, angle] + have h : ∃ r : ℝ, 0 < r ∧ (p₃ -ᵥ p₂) = r • (p₃' -ᵥ p₂) := by + have hr := sbtw_iff_mem_image_Ioo_and_ne.mp h + obtain ⟨hr1, hr2⟩ := hr + simp only [Set.mem_image, Set.mem_Ioo] at hr1 + obtain ⟨r, hr1, hr2⟩ := hr1 + rw [AffineMap.lineMap_apply] at hr2 + use r; repeat aesop + obtain ⟨r, hr1,hr2⟩ := h + rw [hr2] + apply InnerProductGeometry.angle_smul_right_of_pos + exact hr1 + +/-- An Unoriented angle is unchanged by replacing the first point by one strictly further away on +the same ray. -/ +theorem _root_.Sbtw.angle_eq_left {p₁ p₁' p₂ p₃ : P} (h : Sbtw ℝ p₂ p₁ p₁') : + ∠ p₁ p₂ p₃ = ∠ p₁' p₂ p₃ := by + rw [angle_comm] + nth_rw 2 [angle_comm] + exact Sbtw.angle_eq_right h + +/-- An Unoriented angle is unchanged by replacing the third point by one weakly further away on the +same ray. -/ +theorem _root_.Wbtw.angle_eq_right {p₁ p₂ p₃ p₃' : P} (h : Wbtw ℝ p₂ p₃ p₃') (hp₃p₂ : p₃ ≠ p₂) : + ∠ p₁ p₂ p₃ = ∠ p₁ p₂ p₃' := by + by_cases hp₃p₃' : p₃ = p₃'; · simp [hp₃p₃'] + apply Sbtw.angle_eq_right + exact ⟨h, hp₃p₂, hp₃p₃'⟩ + +/-- An Unoriented angle is unchanged by replacing the first point by one weakly further away on the +same ray. -/ +theorem _root_.Wbtw.angle_eq_left {p₁ p₁' p₂ p₃ : P} (h : Wbtw ℝ p₂ p₁ p₁') (hp₁p₂ : p₁ ≠ p₂) : + ∠ p₁ p₂ p₃ = ∠ p₁' p₂ p₃ := by + rw [angle_comm] + nth_rw 2 [angle_comm] + exact Wbtw.angle_eq_right h hp₁p₂ + /-- Three points are collinear if and only if the first or third point equals the second or the angle between them is 0 or π. -/ theorem collinear_iff_eq_or_eq_or_angle_eq_zero_or_angle_eq_pi {p₁ p₂ p₃ : P} : diff --git a/Mathlib/Geometry/Euclidean/Triangle.lean b/Mathlib/Geometry/Euclidean/Triangle.lean index 16c4983f963dff..9b68961d9a33c9 100644 --- a/Mathlib/Geometry/Euclidean/Triangle.lean +++ b/Mathlib/Geometry/Euclidean/Triangle.lean @@ -508,15 +508,4 @@ lemma angle_lt_pi_div_three_of_le_of_le_of_ne {p₁ p₂ p₃ : P} (h₂₃₁ : rcases hne.lt_or_gt with hne | hne <;> linarith [angle_add_angle_add_angle_eq_pi p₃ h] -/-- **Exterior angle theorem**. -/ -theorem exterior_angle_eq_angle_add_angle {p₁ p₂ p₃ : P} (p : P) (h : Sbtw ℝ p p₁ p₂) : - ∠ p₃ p₁ p = ∠ p₁ p₃ p₂ + ∠ p₃ p₂ p₁ := by - have H := (EuclideanGeometry.angle_add_angle_eq_pi_of_angle_eq_pi p₃ (Sbtw.angle₁₂₃_eq_pi h)).symm - rw [show ∠ p₃ p₁ p₂ = ∠ p₂ p₁ p₃ by simp only [angle_comm], - add_comm, - ← angle_add_angle_add_angle_eq_pi p₃ ((Sbtw.right_ne h).symm), - add_assoc] at H - simp only [add_right_inj] at H - rw [H] - end EuclideanGeometry From 102f1fefd26b9f9c1dc8b70071bf4df47ebc60b3 Mon Sep 17 00:00:00 2001 From: yulia Date: Tue, 30 Dec 2025 00:27:17 +0800 Subject: [PATCH 4/9] change p' to p --- .../Euclidean/Angle/Unoriented/Affine.lean | 22 +++++++++---------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean b/Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean index aa259ea2f3aa59..bee7a930dc57d2 100644 --- a/Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean +++ b/Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean @@ -375,10 +375,10 @@ theorem angle_eq_zero_iff_eq_and_ne_or_sbtw {p₁ p₂ p₃ : P} : /-- An Unoriented angle is unchanged by replacing the third point by one strictly further away on the same ray. -/ -theorem _root_.Sbtw.angle_eq_right {p₁ p₂ p₃ p₃' : P} (h : Sbtw ℝ p₂ p₃ p₃') : - ∠ p₁ p₂ p₃ = ∠ p₁ p₂ p₃' := by +theorem _root_.Sbtw.angle_eq_right {p₁ p₂ p₃ p : P} (h : Sbtw ℝ p₂ p₃ p) : + ∠ p₁ p₂ p₃ = ∠ p₁ p₂ p := by rw [angle, angle] - have h : ∃ r : ℝ, 0 < r ∧ (p₃ -ᵥ p₂) = r • (p₃' -ᵥ p₂) := by + have h : ∃ r : ℝ, 0 < r ∧ (p₃ -ᵥ p₂) = r • (p -ᵥ p₂) := by have hr := sbtw_iff_mem_image_Ioo_and_ne.mp h obtain ⟨hr1, hr2⟩ := hr simp only [Set.mem_image, Set.mem_Ioo] at hr1 @@ -392,24 +392,24 @@ theorem _root_.Sbtw.angle_eq_right {p₁ p₂ p₃ p₃' : P} (h : Sbtw ℝ p₂ /-- An Unoriented angle is unchanged by replacing the first point by one strictly further away on the same ray. -/ -theorem _root_.Sbtw.angle_eq_left {p₁ p₁' p₂ p₃ : P} (h : Sbtw ℝ p₂ p₁ p₁') : - ∠ p₁ p₂ p₃ = ∠ p₁' p₂ p₃ := by +theorem _root_.Sbtw.angle_eq_left {p₁ p p₂ p₃ : P} (h : Sbtw ℝ p₂ p₁ p) : + ∠ p₁ p₂ p₃ = ∠ p p₂ p₃ := by rw [angle_comm] nth_rw 2 [angle_comm] exact Sbtw.angle_eq_right h /-- An Unoriented angle is unchanged by replacing the third point by one weakly further away on the same ray. -/ -theorem _root_.Wbtw.angle_eq_right {p₁ p₂ p₃ p₃' : P} (h : Wbtw ℝ p₂ p₃ p₃') (hp₃p₂ : p₃ ≠ p₂) : - ∠ p₁ p₂ p₃ = ∠ p₁ p₂ p₃' := by - by_cases hp₃p₃' : p₃ = p₃'; · simp [hp₃p₃'] +theorem _root_.Wbtw.angle_eq_right {p₁ p₂ p₃ p : P} (h : Wbtw ℝ p₂ p₃ p) (hp₃p₂ : p₃ ≠ p₂) : + ∠ p₁ p₂ p₃ = ∠ p₁ p₂ p := by + by_cases hp₃p : p₃ = p; · simp [hp₃p] apply Sbtw.angle_eq_right - exact ⟨h, hp₃p₂, hp₃p₃'⟩ + exact ⟨h, hp₃p₂, hp₃p⟩ /-- An Unoriented angle is unchanged by replacing the first point by one weakly further away on the same ray. -/ -theorem _root_.Wbtw.angle_eq_left {p₁ p₁' p₂ p₃ : P} (h : Wbtw ℝ p₂ p₁ p₁') (hp₁p₂ : p₁ ≠ p₂) : - ∠ p₁ p₂ p₃ = ∠ p₁' p₂ p₃ := by +theorem _root_.Wbtw.angle_eq_left {p₁ p p₂ p₃ : P} (h : Wbtw ℝ p₂ p₁ p) (hp₁p₂ : p₁ ≠ p₂) : + ∠ p₁ p₂ p₃ = ∠ p p₂ p₃ := by rw [angle_comm] nth_rw 2 [angle_comm] exact Wbtw.angle_eq_right h hp₁p₂ From 621e5734c84fc0f61b4a2f9d28a4ede0b5ca53fc Mon Sep 17 00:00:00 2001 From: wangying11123 <134686157+wangying11123@users.noreply.github.com> Date: Tue, 30 Dec 2025 22:30:42 +0800 Subject: [PATCH 5/9] Update Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean Modify the proof process with jsm28's help Co-authored-by: Joseph Myers --- .../Euclidean/Angle/Unoriented/Affine.lean | 15 ++------------- 1 file changed, 2 insertions(+), 13 deletions(-) diff --git a/Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean b/Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean index bee7a930dc57d2..65540110d1a046 100644 --- a/Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean +++ b/Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean @@ -376,19 +376,8 @@ theorem angle_eq_zero_iff_eq_and_ne_or_sbtw {p₁ p₂ p₃ : P} : /-- An Unoriented angle is unchanged by replacing the third point by one strictly further away on the same ray. -/ theorem _root_.Sbtw.angle_eq_right {p₁ p₂ p₃ p : P} (h : Sbtw ℝ p₂ p₃ p) : - ∠ p₁ p₂ p₃ = ∠ p₁ p₂ p := by - rw [angle, angle] - have h : ∃ r : ℝ, 0 < r ∧ (p₃ -ᵥ p₂) = r • (p -ᵥ p₂) := by - have hr := sbtw_iff_mem_image_Ioo_and_ne.mp h - obtain ⟨hr1, hr2⟩ := hr - simp only [Set.mem_image, Set.mem_Ioo] at hr1 - obtain ⟨r, hr1, hr2⟩ := hr1 - rw [AffineMap.lineMap_apply] at hr2 - use r; repeat aesop - obtain ⟨r, hr1,hr2⟩ := h - rw [hr2] - apply InnerProductGeometry.angle_smul_right_of_pos - exact hr1 + ∠ p₁ p₂ p₃ = ∠ p₁ p₂ p := + angle_eq_angle_of_angle_eq_pi _ h.angle₁₂₃_eq_pi /-- An Unoriented angle is unchanged by replacing the first point by one strictly further away on the same ray. -/ From d096180a831fc5cc4d730449879cabbd32e59ff9 Mon Sep 17 00:00:00 2001 From: yulia Date: Wed, 31 Dec 2025 12:16:24 +0800 Subject: [PATCH 6/9] change some points to explicit points --- .../Geometry/Euclidean/Angle/Unoriented/Affine.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean b/Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean index 65540110d1a046..9e7a4f3ed35d6a 100644 --- a/Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean +++ b/Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean @@ -375,21 +375,21 @@ theorem angle_eq_zero_iff_eq_and_ne_or_sbtw {p₁ p₂ p₃ : P} : /-- An Unoriented angle is unchanged by replacing the third point by one strictly further away on the same ray. -/ -theorem _root_.Sbtw.angle_eq_right {p₁ p₂ p₃ p : P} (h : Sbtw ℝ p₂ p₃ p) : +theorem _root_.Sbtw.angle_eq_right {p₂ p₃ p : P} (p₁ : P) (h : Sbtw ℝ p₂ p₃ p) : ∠ p₁ p₂ p₃ = ∠ p₁ p₂ p := angle_eq_angle_of_angle_eq_pi _ h.angle₁₂₃_eq_pi /-- An Unoriented angle is unchanged by replacing the first point by one strictly further away on the same ray. -/ -theorem _root_.Sbtw.angle_eq_left {p₁ p p₂ p₃ : P} (h : Sbtw ℝ p₂ p₁ p) : +theorem _root_.Sbtw.angle_eq_left {p₁ p p₂ : P} (p₃ : P) (h : Sbtw ℝ p₂ p₁ p) : ∠ p₁ p₂ p₃ = ∠ p p₂ p₃ := by rw [angle_comm] nth_rw 2 [angle_comm] - exact Sbtw.angle_eq_right h + exact Sbtw.angle_eq_right p₃ h /-- An Unoriented angle is unchanged by replacing the third point by one weakly further away on the same ray. -/ -theorem _root_.Wbtw.angle_eq_right {p₁ p₂ p₃ p : P} (h : Wbtw ℝ p₂ p₃ p) (hp₃p₂ : p₃ ≠ p₂) : +theorem _root_.Wbtw.angle_eq_right {p₂ p₃ p : P} (p₁ : P) (h : Wbtw ℝ p₂ p₃ p) (hp₃p₂ : p₃ ≠ p₂) : ∠ p₁ p₂ p₃ = ∠ p₁ p₂ p := by by_cases hp₃p : p₃ = p; · simp [hp₃p] apply Sbtw.angle_eq_right @@ -397,11 +397,11 @@ theorem _root_.Wbtw.angle_eq_right {p₁ p₂ p₃ p : P} (h : Wbtw ℝ p₂ p /-- An Unoriented angle is unchanged by replacing the first point by one weakly further away on the same ray. -/ -theorem _root_.Wbtw.angle_eq_left {p₁ p p₂ p₃ : P} (h : Wbtw ℝ p₂ p₁ p) (hp₁p₂ : p₁ ≠ p₂) : +theorem _root_.Wbtw.angle_eq_left {p₁ p p₂ : P} (p₃ : P) (h : Wbtw ℝ p₂ p₁ p) (hp₁p₂ : p₁ ≠ p₂) : ∠ p₁ p₂ p₃ = ∠ p p₂ p₃ := by rw [angle_comm] nth_rw 2 [angle_comm] - exact Wbtw.angle_eq_right h hp₁p₂ + exact Wbtw.angle_eq_right p₃ h hp₁p₂ /-- Three points are collinear if and only if the first or third point equals the second or the angle between them is 0 or π. -/ From 662177e22dd7c576b08994703b20a6e27fca98e5 Mon Sep 17 00:00:00 2001 From: wangying11123 <134686157+wangying11123@users.noreply.github.com> Date: Mon, 5 Jan 2026 20:16:51 +0800 Subject: [PATCH 7/9] Update Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean Co-authored-by: Johan Commelin --- Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean b/Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean index 9e7a4f3ed35d6a..6d9ab2dc39c02b 100644 --- a/Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean +++ b/Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean @@ -383,9 +383,7 @@ theorem _root_.Sbtw.angle_eq_right {p₂ p₃ p : P} (p₁ : P) (h : Sbtw ℝ p the same ray. -/ theorem _root_.Sbtw.angle_eq_left {p₁ p p₂ : P} (p₃ : P) (h : Sbtw ℝ p₂ p₁ p) : ∠ p₁ p₂ p₃ = ∠ p p₂ p₃ := by - rw [angle_comm] - nth_rw 2 [angle_comm] - exact Sbtw.angle_eq_right p₃ h + simpa only [angle_comm] using h.angle_eq_right p₃ /-- An Unoriented angle is unchanged by replacing the third point by one weakly further away on the same ray. -/ From 95cf30bb9c6cf91417c3993c1d99e1a8b2994a4a Mon Sep 17 00:00:00 2001 From: wangying11123 <134686157+wangying11123@users.noreply.github.com> Date: Mon, 5 Jan 2026 20:17:01 +0800 Subject: [PATCH 8/9] Update Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean Co-authored-by: Johan Commelin --- Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean b/Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean index 6d9ab2dc39c02b..a443c31c5f6f80 100644 --- a/Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean +++ b/Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean @@ -390,8 +390,7 @@ same ray. -/ theorem _root_.Wbtw.angle_eq_right {p₂ p₃ p : P} (p₁ : P) (h : Wbtw ℝ p₂ p₃ p) (hp₃p₂ : p₃ ≠ p₂) : ∠ p₁ p₂ p₃ = ∠ p₁ p₂ p := by by_cases hp₃p : p₃ = p; · simp [hp₃p] - apply Sbtw.angle_eq_right - exact ⟨h, hp₃p₂, hp₃p⟩ + exact Sbtw.angle_eq_right _ ⟨h, hp₃p₂, hp₃p⟩ /-- An Unoriented angle is unchanged by replacing the first point by one weakly further away on the same ray. -/ From 192b2244e605cca326fe84d60430956b10d25413 Mon Sep 17 00:00:00 2001 From: wangying11123 <134686157+wangying11123@users.noreply.github.com> Date: Mon, 5 Jan 2026 20:17:15 +0800 Subject: [PATCH 9/9] Update Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean Co-authored-by: Johan Commelin --- Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean b/Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean index a443c31c5f6f80..7a82a0432f0d56 100644 --- a/Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean +++ b/Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean @@ -396,9 +396,7 @@ theorem _root_.Wbtw.angle_eq_right {p₂ p₃ p : P} (p₁ : P) (h : Wbtw ℝ p same ray. -/ theorem _root_.Wbtw.angle_eq_left {p₁ p p₂ : P} (p₃ : P) (h : Wbtw ℝ p₂ p₁ p) (hp₁p₂ : p₁ ≠ p₂) : ∠ p₁ p₂ p₃ = ∠ p p₂ p₃ := by - rw [angle_comm] - nth_rw 2 [angle_comm] - exact Wbtw.angle_eq_right p₃ h hp₁p₂ + simpa only [angle_comm] using h.angle_eq_right p₃ hp₁p₂ /-- Three points are collinear if and only if the first or third point equals the second or the angle between them is 0 or π. -/