example #218
example #218
Conversation
Schaum10-14
update Ray
| variable {M : Plane} {hm : M = Quadrilateral_cvx.diag_inx (QDR_cvx A B C D (is_convex_of_is_prg hprg))} | ||
| -- Let $P$ and $Q$ be points on $AM$ and $MC$, respectively, such that $MP = MQ$. | ||
| variable {P Q : Plane} {hp : Seg.IsInt P (SEG A M)} {hq : Seg.IsInt Q (SEG M C)} {hpq : (SEG P M).length = (SEG M Q).length} | ||
| -- State the main goal. |
There was a problem hiding this comment.
Please write out the main goal explicitly.
| variable {P Q : Plane} {hp : Seg.IsInt P (SEG A M)} {hq : Seg.IsInt Q (SEG M C)} {hpq : (SEG P M).length = (SEG M Q).length} | ||
| -- State the main goal. | ||
| theorem SCHAUM_Problem_1_13 : Quadrilateral.IsParallelogram (QDR P B Q D) := by | ||
| have m1 : M = (SEG B D).midpoint := by |
There was a problem hiding this comment.
such a lemma should be equipped with comments.
-- Point $M$ is the midpoint of the segment $BD$.
| · simp | ||
| exact hpq | ||
| apply is_prg_of_diag_inx_eq_mid_eq_mid | ||
| rw [← m1, ← m2] |
There was a problem hiding this comment.
Line 35 36 should have a comment.
| variable {M : P} {median_M_position : M = (SEG B C).midpoint} | ||
| --Prove that $DM = EM$. | ||
| theorem Problem_1_1 : (SEG D M).length = (SEG E M).length := by | ||
| have h₀ : (SEG A B).length = (SEG A C).length := by |
There was a problem hiding this comment.
Although this looks very clear, it still needs a comment.
-- We show that the length of segment $AB$ equals to length of $AC$
| have a_ne_b : A ≠ B := (ne_of_not_colinear hnd).2.2.symm | ||
| have c_ne_b : C ≠ B := (ne_of_not_colinear hnd).1 | ||
| have a_ne_c : A ≠ C := (ne_of_not_colinear hnd).2.1 | ||
| have b_ne_c : B ≠ C := (ne_of_not_colinear hnd).1.symm |
There was a problem hiding this comment.
From Line 31 to Line 41, add a single comment to explain what each line do
-- Point $A$ is not equals to point $B$.
| have c_ne_b : C ≠ B := (ne_of_not_colinear hnd).1 | ||
| have a_ne_c : A ≠ C := (ne_of_not_colinear hnd).2.1 | ||
| have b_ne_c : B ≠ C := (ne_of_not_colinear hnd).1.symm | ||
| --the second edge of congruence |
There was a problem hiding this comment.
the comment should be written as the style of proving in human-readable language, not comment of code.
-- the length of $BD$ equals to length of $CE$.
| _= (SEG E C).length := by | ||
| rw [← eq_sub_of_add_eq'] | ||
| exact (length_eq_length_add_length (SEG A C) E (E_on_seg)).symm | ||
| _= (SEG C E).length := length_eq_length_of_rev (SEG E C) |
There was a problem hiding this comment.
the calc mode needs comments too.
| apply (is_isoceles_tri_iff_ang_eq_ang_of_nd_tri (tri_nd := ⟨▵ A B C, hnd⟩)).mp | ||
| exact hisoc | ||
| rw [h₅₃] | ||
| have h₆ : TRI_nd B D M h₁ ≅ₐ TRI_nd C E M h₂ := by |
There was a problem hiding this comment.
comment here what congruence criterion and what condition you use to show the congruence.
No description provided.