bug in Lean problem statement of mathd_numbertheory_780

[dwrensha]

The Lean statement of mathd_numbertheory_780 has a bug in it:

miniF2F/lean/src/valid.lean

Lines 57 to 66 in 4e433ff

	theorem mathd_numbertheory_780
	(m x : ℕ)
	(h₀ : 10 ≤ m)
	(h₁ : m ≤ 99)
	(h₂ : (6 * x) % m = 1)
	(h₃ : (x - 6^2) % m = 0) :
	m = 43 :=
	begin
	sorry
	end

The subtraction in h₃ can be degenerate when x < 36, in which case x - 6^2 = 0 (because Lean defines subtraction as a total function taking values on the natural numbers).

Assuming that the theorem is true as stated, we can derive a contradiction:

theorem mathd_numbertheory_780
    (m x : ℕ)
    (h₀ : 10 ≤ m)
    (h₁ : m ≤ 99)
    (h₂ : (6 * x) % m = 1)
    (h₃ : (x - 6^2) % m = 0) :
    m = 43 := sorry

example : false :=
begin
  have h := mathd_numbertheory_780 11 2
           (by norm_num) (by norm_num) (by norm_num) (by norm_num),
  norm_num at h
end

One way around this could be to use integers rather than natural numbers in the problem statement.

[DyeKuu]

Nice catch David! I will push a fix to it.