Hi Jon! I think eqtri is at least a plausible way to go here.
I think something along these lines could get you there? I entered the first eqtri manually here as the model fails to make useful progress early on. https://mmproofassistant.azurewebsites.net/#eJydV9uSojAQ/ZUUT1qDbiDIxap9UJ92q+YLZueB6xjuEmBE13/fgEIiIqvWVE2FDNPndJ/TnXAUcO5GRFgehX1i+Dqy8rB+yKvUFZZCaFpuKIhCamZunAvLuAhDUSC5Sf+p2RCiapZmSeLRl7BDn1kUUQgT08Hxl7D0zJC4J1EIHB8rhl6WHITjEjvDaY6TeBRoskniPMNWkbsOsCoggsXsdxHOZCjD+bSFZwgUjqQoN5xQ5eG2VZrkW5dgMoq2Au4cbDZtWBbp/FpBKyYkqRvXMKUXbO1gGzsczFdijtdtAlbgJ5DAjz9/wJquZDC9qZgo2EkYmilxnW6nocMQB+iQnSWnplkYz2e97mXdRRqAcQ0j0mB2cJ+HqXN/o1lPad6oBWPxBsB2FQmlg6fkr4BNAAL7OcWcUtQJrTR9qMFreK2FZwgD8FIi6Xak7hEHn5t2jm0O+kaVlsHHB/g7A+m2+U3A52e9mNQbtfh0ZwqOx/pxefHE6dRsELpxtsbpVHuj6cWlkEZoLuOWN6PW502NaYYFpQrnECqqApGsaCoyVGUBNZpUluulISsL/b5tb6Kz9qA8H/crgxooLgpI6GF5O9I+d3k05XmcB4Ma4CFj0yPld/Q1KnI/lWuR67qs60VNbHORetWsqaKrRuGzuhu6bpVe0/UEaGDWupM1SP1zpb67o0OwFZ9RHhNfliUVSoZiIEPXDaggmqznB3YWBAtppOj96Lz49+k+rgbjMKCGgwMf+gmBLxAcqeVTtmUcBgjGBYx3qPTgqF36Ifp2aebt2TDdcsOWE7r/Rjdq4qtucqzA7DI9O1tpV1a6Sfzac5ydSGGZjpPhzlIsrRFLIU2XEISSpC00SUe6Suth+8VeSv1oNyJYP3hbDa07dx5UhoENWWcfJS4OUvUFJgO1e5IaQx90tR99RxgaL1CTnmbSgQ0w0SzV+TYNXL1UpIEyvVFrtSfqgwQZhwGCpozzA4qxNdpf/RDPjuORVPiGuryEen/cXDrv3nxmOYw0k6Ip9FyWJWgodE7LqkKTVzwjLHFcpiPq9IM/pM5tKo/LxUgNyAUr4oXlYT82r//LGL3mI4Z9Q+xUK1MlBYX5uPo2YR8K4vXtnrvz8ldS/n7IX/T4mwl/N+DPJv6g4w8Evr/4icaPEL6JebPzteSF4WvBrjuf4qV3fsVp0V2Tmw+39/fz4+kfOGw5mQ== On Sun, Jul 19, 2020 at 10:28 AM Jon P <[email protected]> wrote: > Hi Thierry, > > That's is very nice progress! I have been playing around with the tool and > I like it, it seems to have an obsession with eqtri however that also seems > to work out quite often so it's probably right to think highly of it. I > have done all the practice problems and I'm searching for some theorems I > might be able to prove with it. > > One thing I noticed doing Filip's practice problems is that the 4th > problem of his is much more difficult than the others and I have not yet > been able to solve it using suggestions from the tool. I found this a bit > surprising. My solutions are here > <https://docs.google.com/document/d/1cpbz2ZJ60qR0220fUTvCWAv4NYX4y8JTClCwGnzryXc/edit?usp=sharing>if > anyone is also trying the practice problems. I don't know if anyone else > has found anything similar. > > -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/50a189c7-3f29-40ef-bd32-ee6246c2eceeo%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/50a189c7-3f29-40ef-bd32-ee6246c2eceeo%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CACZd_0ziez2n4aeVEyBS_sK7fLTfRsSc3iXP5Mn7O42ciP0eMw%40mail.gmail.com.
