Team_F_Changed_Ray_ex.lean

[mathzhuonichi]

Modified most proofs, 60 lines shorter now.
The last theorem is still too long. I think we can prove this by prove that it lies on seg_nd.toRay and (SEG A source).toRay. And the proof should be much shorter. But I met some problem, for example, to unify pt LiesOn seg with Seg.IsOn pt seg, and also i don't know how to define (SEG target A).toSeg_nd and some other stuff without lemmas and calculations.

[jjdishere]

But I met some problem, for example, to unify pt LiesOn seg with Seg.IsOn pt seg,

1. Here, pt LiesOn seg and Seg.IsOn pt seg are definitionally equal. They are equal by rfl you may directly substitute one with another. e. g.

variable {P : Type _} [EuclideanPlane P]
theorem test_is_on (A : P) (seg : Seg P) : (p LiesOn seg) = (Seg.IsOn p seg) := rfl

and also i don't know how to define (SEG target A).toSeg_nd and some other stuff without lemmas and calculations.

2. To define a Seg_nd, you can use constructor ⟨ ⟩. One can use ⟨ SEG target A, h ⟩ : Seg_nd to create a Seg_nd, where h : A ≠ target

Would you like to further modify some of the proof? The already modified proofs are good!

[mathzhuonichi]

But I met some problem, for example, to unify pt LiesOn seg with Seg.IsOn pt seg,

1. Here, pt LiesOn seg and Seg.IsOn pt seg are definitionally equal. They are equal by rfl you may directly substitute one with another. e. g.

variable {P : Type _} [EuclideanPlane P]
theorem test_is_on (A : P) (seg : Seg P) : (p LiesOn seg) = (Seg.IsOn p seg) := rfl

and also i don't know how to define (SEG target A).toSeg_nd and some other stuff without lemmas and calculations.

2. To define a Seg_nd, you can use constructor ⟨ ⟩. One can use ⟨ SEG target A, h ⟩ : Seg_nd to create a Seg_nd, where h : A ≠ target

Would you like to further modify some of the proof? The already modified proofs are good!

I’d say not so soon as I have other stuff to deal with.

[jjdishere]

I’d say not so soon as I have other stuff to deal with.

That is fine. I shall merge your current PR. If you further modified your code, you can always open a new PR.