Reposted by Elementary Penguin
The fuck do you mean there's a four episode Manos: the Hands of Fate sequel series on Amazon???!!!
Elementary Penguin
@elempeng.bsky.social
504 followers 236 following 5.1K posts
Elementary Penguin is an okapi at the San Diego Zoo. He likes math and hates food.
![A bunch of Lean 4 code for a theorem names Geom.inner_five_sgmt. Above it is the comment "Satz 4.2; this is basically SSS to five_sgmt's SAS".
The code reads as follows:
theorem Geom.inner_five_sgmt {x y z u x' y' z' u' : G.Point} : B x y z → B x' y' z' →
E x y x' y' → E y z y' z' → E x u x' u' → E z u z' u' → E y u y' u' := by
intro hb1 hb'1 he1 he2 he3 he4
by_cases heq : x = z
· subst heq; rw [btwn_id hb1] at he1 he3
rwa [G.E_id he1.symm] at he3
have ⟨w, hw1, hw2⟩ := G.sgmt_const x z x z
have ⟨w', hw'1, hw'2⟩ := G.sgmt_const x' z' x' z'
have he5 : E x z x' z' := G.sgmt_add hb1 hb'1 he1 he2
have he6 : E z w z' w' := G.E_trans (G.E_trans hw2 he5) hw'2.symm
have he7 : E w u w' u' := G.five_sgmt heq hw1 hw'1 he5 he6 he3 he4
have heq2 : w ≠ z := Ne.symm (G.E_id_mt heq hw2)
have hb2 : B w z y := (G.btwn_yzw_of_xyz_xzw hb1 hw1).symm
have hb'2 : B w' z' y' := (G.btwn_yzw_of_xyz_xzw hb'1 hw'1).symm
apply G.five_sgmt heq2 hb2 hb'2 he6.lr he2.lr he7 he4](https://cdn.bsky.app/img/feed_thumbnail/plain/did:plc:zjqh2b7v3wgbcl7p6hyrm36d/bafkreibi25a3ohk52moxo7mjlkmuaqnpdjksi7bkzch4afe6k7m6euf4hy)
