About do not use exhaustive search

Stream: new members

[tooball]

import Mathlib
/-How many two-digit positive integers are congruent to 1 (mod 3)?-/
set_option maxHeartbeats 8000000
set_option maxRecDepth 200000
example :
    Set.ncard {n : ℕ | n ∈ Finset.Icc 10 99 ∧ n ≡ 1 [MOD 3]} = 30 := by
    have  heq :  {n : ℕ | n ∈ Finset.Icc 10 99 ∧ n ≡ 1 [MOD 3]} = {10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82,85,88,91,94,97}:= by
      ext n
      constructor
      ·
        intro h
        cases h with
        | intro left right =>
          fin_cases left
          any_goals  contradiction
          simp
          all_goals clear right;
          all_goals ring_nf;
          all_goals tauto

      ·
        simp
        intro h
        aesop
        all_goals tauto
    rw [heq]
    rw [Set.ncard_eq_toFinset_card']
    simp


example : IsGreatest {x | 17 ∣ x ∧ x < 1000 ∧ (x + 1) % 8 = 0} 935 := by sorry

About the above question, I used fin_cases, but this is clearly not a good way,If I don't use exhaustive search,how can i prove it?
The second example is a similar one.

[Kyle Miller]

You can make a function that enumerates the elements of the set, fun i => 3 * i + 10 for 0 <= i < 30, and then use docs#Set.ncard_eq_of_bijective` to prove it.

example : Set.ncard {n : ℕ | n ∈ Set.Icc 10 99 ∧ n ≡ 1 [MOD 3]} = 30 := by
  apply Set.ncard_eq_of_bijective (f := fun i _ => 3 * i + 10)
  · simp only [mem_Icc, mem_setOf_eq, exists_prop, and_imp] -- simp?
    intro n h1 h2 h3
    use (n - 10) / 3
    constructor
    · omega
    · zify [h1]
      have : (3 : ℤ) ∣ n - 10 := by
        rw [← Int.natCast_modEq_iff, Nat.cast_one] at h3
        rw [← Int.modEq_iff_dvd]
        refine Int.ModEq.trans ?_ h3.symm
        simp [Int.ModEq]
      qify [this]
      ring
  · simp [Nat.ModEq]
    omega
  · omega

[tooball]

Thank you. This is helpful.
The second example,if i make a function, then which tactic should i use ?

[Kyle Miller]

Here's a possible start:

example : IsGreatest {x | 17 ∣ x ∧ x < 1000 ∧ (x + 1) % 8 = 0} 935 := by
  constructor
  · norm_num
  · rw [mem_upperBounds]
    simp only [mem_setOf_eq, and_imp]
    intro n h1 h2 h3
    sorry

[Kyle Miller]

I imagine using the chinese remainder theorem would be helpful here.

I'm not sure I've ever used mathlib's version, but there's stuff starting here: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/ModEq.html#Nat.chineseRemainder