sorry ex

jjdishere · Nov 24, 2023 · 24f014e · 24f014e
1 parent 55e6239
commit 24f014e
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 5 deletions.
diff --git a/EuclideanGeometry/Example/ArefWernick/Chap1.lean b/EuclideanGeometry/Example/ArefWernick/Chap1.lean
@@ -67,7 +67,7 @@ lemma b_ne_f : B ≠ F := by
 lemma d_ne_f : D ≠ F := sorry
 
 -- Theorem : $\angle BFD = \pi / 2 - \angle CAB$
-theorem Aref_Wernick_Exercise_1_2 : ∠ B F D (b_ne_f (hnd := hnd) (hd := hd) (hf := hf)) d_ne_f = π / 2 - ∠ C A B (c_ne_a (hnd := hnd)) (b_ne_a (hnd := hnd)) := sorry
+theorem Aref_Wernick_Exercise_1_2 : ∠ B F D (b_ne_f (hnd := hnd) (hd := hd) (hf := hf)) d_ne_f = ↑(π / 2) - ∠ C A B (c_ne_a (hnd := hnd)) (b_ne_a (hnd := hnd)) := sorry
 
 end Aref_Wernick_Exercise_1_2
 

diff --git a/EuclideanGeometry/Example/ExerciseXT8.lean b/EuclideanGeometry/Example/ExerciseXT8.lean
@@ -13,7 +13,7 @@ namespace Exercise_XT_8_1_11
 /- Let $\triangle ABC$ be a triangle. Let $X_1$, $Y_1$, and $Z_1$ be points on the extensions of $BC$, $CA$, $AB$, respectively. Let $X_2$, $Y_2$, and $Z_2$ be points on the extensions of $CB$, $AC$, $BA$, respectively.
 
 Prove that $\angle AY_1Z_2 + \angle BZ_1X_2 + \angle CX_1Y_2 + \angle Y_1Z_2A + \angle Z_1X_2B + \angle X_1Y_2C = 2 \cdot \pi$.
--/ 
+-/
 
 -- Let $\triangle ABC$ be a nondegenerate triangle.
 variable {A B C : P} {hnd : ¬ colinear A B C}
@@ -36,8 +36,7 @@ lemma x1_ne_y2 : X₁ ≠ Y₂ := sorry
 lemma y1_ne_z2 : Y₁ ≠ Z₂ := sorry
 lemma z1_ne_x2 : Z₁ ≠ X₂ := sorry
 
-theorem XT_8_1_11 : ∠ A Y₁ Z₂ a_ne_y1 y1_ne_z2.symm + ∠ B Z₁ X₂ b_ne_z1 z1_ne_x2.symm + ∠ C X₁ Y₂ c_ne_x1 x1_ne_y2.symm + ∠ Y₁ Z₂ A y1_ne_z2 a_ne_z2 + ∠ Z₁ X₂ B z1_ne_x2 b_ne_x2 + ∠ X₁ Y₂ C x1_ne_y2 c_ne_y2  = 2 * π := sorry
+theorem XT_8_1_11 : ∠ A Y₁ Z₂ a_ne_y1 y1_ne_z2.symm + ∠ B Z₁ X₂ b_ne_z1 z1_ne_x2.symm + ∠ C X₁ Y₂ c_ne_x1 x1_ne_y2.symm + ∠ Y₁ Z₂ A y1_ne_z2 a_ne_z2 + ∠ Z₁ X₂ B z1_ne_x2 b_ne_x2 + ∠ X₁ Y₂ C x1_ne_y2 c_ne_y2  = ↑(2 * π) := sorry
 
 end Exercise_XT_8_1_11
 end EuclidGeom
-
diff --git a/EuclideanGeometry/Example/ShanZun/Ex1.lean b/EuclideanGeometry/Example/ShanZun/Ex1.lean
@@ -27,6 +27,8 @@ lemma d_ne_a : D ≠ A := sorry
 lemma e_ne_a : E ≠ A := sorry
 
 -- Theorem : $\angle DAE = (\angle CBA - \angle ACB) / 2$
+--`This need to reformulate`
+/-
 theorem Shan_Problem_1_1 : ∠ D A E d_ne_a e_ne_A = (1 / 2) * (∠ C B A b_ne_c.symm a_ne_b - ∠ A C B c_ne_a.symm b_ne_c) := by
   -- $\angle BAE - \angle DAE = \angle BAD$
   have ang₁ : ∠ B A E a_ne_b.symm e_ne_a - ∠ D A E d_ne_a e_ne_a = ∠ B A D a_ne_b d_ne_a := sorry
@@ -38,7 +40,7 @@ theorem Shan_Problem_1_1 : ∠ D A E d_ne_a e_ne_A = (1 / 2) * (∠ C B A b_ne_c
   have ang₄ : ∠ D A C d_ne_a c_ne_a - ∠ B A D a_ne_b d_ne_a = ∠ C B A b_ne_c.symm a_ne_b - ∠ A C B c_ne_a.symm b_ne_c := sorry
   rw[← ang₄, ← ang₂, ← ang₁, ← ang₃]
   ring
-
+-/
 end Shan_Problem_1_1
 
 namespace Shan_Problem_1_2