Skip to content

refactor(NumberTheory): golf Mathlib/NumberTheory/Dioph #38457

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
yuanyi-350 wants to merge 2 commits into
base: master
Choose a base branch
from
Open

refactor(NumberTheory): golf Mathlib/NumberTheory/Dioph #38457

Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
14367bd
refactor(NumberTheory): golf Mathlib/NumberTheory/Dioph
yuanyi-350 Apr 24, 2026
cb9c110
.
yuanyi-350 Apr 25, 2026
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
22 changes: 6 additions & 16 deletions Mathlib/NumberTheory/Dioph.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -567,12 +567,8 @@ theorem sub_dioph : DiophFn fun v => f v - g v :=
(diophFn_vec _).2 <|
ext (D&1 D= D&0 D+ D&2 D∨ D&1 D≤ D&2 D∧ D&0 D= D.0) <|
(vectorAll_iff_forall _).1 fun x y z =>
show y = x + z ∨ y ≤ z ∧ x = 0 ↔ y - z = x from
⟨fun o => by
rcases o with (ae | ⟨yz, x0⟩)
· rw [ae, add_tsub_cancel_right]
· rw [x0, tsub_eq_zero_iff_le.mpr yz], by
lia⟩
show y = x + z ∨ y ≤ z ∧ x = 0 ↔ y - z = x by
grind
Comment thread
yuanyi-350 marked this conversation as resolved.
Outdated

@[inherit_doc]
scoped infixl:80 " D- " => Dioph.sub_dioph
Expand Down Expand Up @@ -623,16 +619,10 @@ theorem div_dioph : DiophFn fun v => f v / g v :=
ext this <|
(vectorAll_iff_forall _).1 fun z x y =>
show y = 0 ∧ z = 0 ∨ z * y ≤ x ∧ x < (z + 1) * y ↔ x / y = z by
refine Iff.trans ?_ eq_comm
exact y.eq_zero_or_pos.elim
(fun y0 => by
rw [y0, Nat.div_zero]
exact ⟨fun o => (o.resolve_right fun ⟨_, h2⟩ => Nat.not_lt_zero _ h2).right,
fun z0 => Or.inl ⟨rfl, z0⟩⟩)
fun ypos =>
Iff.trans ⟨fun o => o.resolve_left fun ⟨h1, _⟩ => Nat.ne_of_gt ypos h1, Or.inr⟩
(le_antisymm_iff.trans <| and_congr (Nat.le_div_iff_mul_le ypos) <|
Iff.trans ⟨lt_succ_of_le, le_of_lt_succ⟩ (div_lt_iff_lt_mul ypos)).symm
rcases y.eq_zero_or_pos with rfl | hy
· simp [eq_comm]
Copy link
Copy Markdown
Contributor

@grunweg grunweg Apr 24, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why do you need eq_comm here?

Copy link
Copy Markdown
Collaborator Author

@yuanyi-350 yuanyi-350 Apr 25, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

simp can simplify this expression to z = 0 ↔ 0 = z, and then eq_comm is needed.

· rw [Nat.div_eq_iff hy, Nat.succ_mul]
grind

end

Expand Down
Loading