enumeration method in Lean

Stream: new members

[tsuki]

How can I use the enumeration method to complete this 'sorry' by explaining that b+1 is not equal to 1, 3, or 7 to prove that b+1=21?

import Mathlib
import Aesop
set_option maxHeartbeats 0
set_option maxRecDepth 100000
open BigOperators Real Nat Topology Rat

theorem amc12_2001_p21 (a b c d : ℕ) (h₀ : a * b * c * d = 8!) (h₁ : a * b + a + b = 524)    (h₂ : b * c + b + c = 146) (h₃ : c * d + c + d = 104) : a - d = 10:= by
  have h: a = 24 ∧ b = 20 ∧ c = 6 ∧ d = 14 := by
    have hab : (a+1)*(b+1) = 525 := by
      calc (a+1)*(b+1) = a*b + a + b + 1 := by ring
                      _ = 524 + 1 := by rw [h₁]
                      _ = 525 := by ring

    have hbc : (b+1)*(c+1) = 147 := by
      calc (b+1)*(c+1) = b*c + b + c + 1 := by ring
                      _ = 146 + 1 := by rw [h₂]
                      _ = 147 := by ring

    have hcd : (c+1)*(d+1) = 105 := by
      calc (c+1)*(d+1) = c*d + c + d + 1 := by ring
                      _ = 104 + 1 := by rw [h₃]
                      _ = 105 := by ring

    have habcd : a*b*c*d = 40320 := by
      exact h₀

    have h₃ : (b + 1) ∣ 525 := by
      exact Dvd.intro_left (a + 1) hab
    have h₄ : (b + 1) ∣ 147 := by
      exact Dvd.intro (c + 1) hbc
    have h₅ : (b + 1) ∣ Nat.gcd 525 147:= by
      exact Nat.dvd_gcd h₃ h₄
    simp at h₅
    have h₆ : b+1 ≠ 1 -> b+1≠ 3 -> b+1 ≠ 7 -> b+1=21 :=by sorry

[Ilmārs Cīrulis]

My try:

import Mathlib
open Nat

theorem amc12_2001_p21 (a b c d : ℕ) (h₀ : a * b * c * d = 8!) (h₁ : a * b + a + b = 524) (h₂ : b * c + b + c = 146) (h₃ : c * d + c + d = 104) : a - d = 10:= by
  have h: a = 24 ∧ b = 20 ∧ c = 6 ∧ d = 14 := by
    have hab : (a+1)*(b+1) = 525 := by
      calc (a+1)*(b+1) = a*b + a + b + 1 := by ring
                      _ = 524 + 1 := by rw [h₁]
                      _ = 525 := by ring

    have hbc : (b+1)*(c+1) = 147 := by
      calc (b+1)*(c+1) = b*c + b + c + 1 := by ring
                      _ = 146 + 1 := by rw [h₂]
                      _ = 147 := by ring

    have hcd : (c+1)*(d+1) = 105 := by
      calc (c+1)*(d+1) = c*d + c + d + 1 := by ring
                      _ = 104 + 1 := by rw [h₃]
                      _ = 105 := by ring

    have habcd : a*b*c*d = 40320 := by
      exact h₀

    have h₃ : (b + 1) ∣ 525 := by
      exact Dvd.intro_left (a + 1) hab
    have h₄ : (b + 1) ∣ 147 := by
      exact Dvd.intro (c + 1) hbc
    have h₅ : (b + 1) ∣ Nat.gcd 525 147:= by
      exact Nat.dvd_gcd h₃ h₄
    simp at h₅

    --- aux should be in Mathlib in some form
    have aux (x y: ℕ) (Hx: x ≠ 0) (Hy: y ≠ 0) (Hxy: x ∣ y): x ≤ y := by
      cases Hxy with | intro w h =>
      subst y
      cases w with
      | zero => simp at Hy
      | succ n => nlinarith
    have h₆ := aux (b + 1) 21 (by omega) (by norm_num) h₅

    have h₇: b ≤ 20 := by omega
    interval_cases b <;> simp at *
    . have ha: a = 174 := by omega
      have hc: c = 48 := by omega
      subst a c; norm_num at *
      omega
    . have ha: a = 74 := by omega
      have hc: c = 20 := by omega
      subst a c; norm_num at *
      omega
    . have ha: a = 24 := by omega
      have hc: c = 6 := by omega
      subst a c; norm_num at *
      omega

  omega