on_sides タクティク実装例 - Githubissues

lean-ja / lean-by-example

コード例で学ぶ Lean 言語

https://lean-ja.github.io/lean-by-example/

MIT License

15 stars 5 forks source link

on_sides タクティク実装例 #391

Open Seasawher opened 5 days ago

Seasawher commented 5 days ago

Zulip: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60on_sides.60.20tactic/near/434803235