Skip to content

§2.5: explain how to call inf_le_left when arguments are not inferrable #323

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
darijgr wants to merge 2 commits into
base: master
Choose a base branch
from
Open

§2.5: explain how to call inf_le_left when arguments are not inferrable #323

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
0aec0fd
Update S05_Proving_Facts_about_Algebraic_Structures.lean
darijgr Oct 18, 2025
5d590da
Update S04_More_Induction.lean
darijgr Oct 23, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions MIL/C02_Basics/S05_Proving_Facts_about_Algebraic_Structures.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -157,8 +157,8 @@ Alternatively, you can use the ``trans`` tactic
which takes ``y`` as an argument and produces the expected goals ``x ≤ y`` and
``y ≤ z``.
Of course you can also avoid this issue by providing directly a full proof such as
``exact le_trans inf_le_left inf_le_right``, but this requires a lot more
planning.
``exact le_trans (inf_le_left : (x ⊓ y) ⊓ z ≤ x ⊓ y) (inf_le_right : x ⊓ y ≤ y)``;
but this requires a lot more planning.
TEXT. -/
-- QUOTE:
example : x ⊓ y = y ⊓ x := by
Expand Down
2 changes: 1 addition & 1 deletion MIL/C05_Elementary_Number_Theory/S04_More_Induction.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -105,7 +105,7 @@ example (n : ℕ) : fib (n + 2) = fib n + fib (n + 1) := by rw [fib]
/- TEXT:
Using Lean's notation for recursive functions, you can carry out proofs by induction on the
natural numbers that mirror the recursive definition of ``fib``.
The following example provides an explicit formula for the nth Fibonacci number in terms of
The following example provides an explicit formula for the ``n``th Fibonacci number in terms of
the golden mean, ``φ``, and its conjugate, ``φ'``.
We have to tell Lean that we don't expect our definitions to generate code because the
arithmetic operations on the real numbers are not computable.
Expand Down