Theorem: Section15sheet2Solutions.lemma2 (FormalisingMathematics2024/Solutions/Section15numberTheory/Sheet2.lean)

State before:
x : ℤ
⊢ x ∣ 24 ↔ x ∈ {-24, -12, -8, -6, -4, -3, -2, -1, 1, 2, 3, 4, 6, 8, 12, 24}
Tactic:
suffices : x ∣ 24 ↔ x.natAbs ∈ ({1, 2, 3, 4, 6, 8, 12, 24} : Finset ℕ)
State after:
x : ℤ
this : x ∣ 24 ↔ Int.natAbs x ∈ {1, 2, 3, 4, 6, 8, 12, 24}
⊢ x ∣ 24 ↔ x ∈ {-24, -12, -8, -6, -4, -3, -2, -1, 1, 2, 3, 4, 6, 8, 12, 24}

case this
x : ℤ
⊢ x ∣ 24 ↔ Int.natAbs x ∈ {1, 2, 3, 4, 6, 8, 12, 24}

State before:
case this
x : ℤ
⊢ x ∣ 24 ↔ Int.natAbs x ∈ {1, 2, 3, 4, 6, 8, 12, 24}
Tactic:
exact int_dvd_iff _ 24 (by norm_num)
State after:
no goals

State before:
x : ℤ
this : x ∣ 24 ↔ Int.natAbs x ∈ {1, 2, 3, 4, 6, 8, 12, 24}
⊢ x ∣ 24 ↔ x ∈ {-24, -12, -8, -6, -4, -3, -2, -1, 1, 2, 3, 4, 6, 8, 12, 24}
Tactic:
simp only [Set.mem_insert_iff, Set.mem_singleton_iff]
State after:
x : ℤ
this : x ∣ 24 ↔ Int.natAbs x ∈ {1, 2, 3, 4, 6, 8, 12, 24}
⊢ x ∣ 24 ↔
    x = -24 ∨
      x = -12 ∨
        x = -8 ∨
          x = -6 ∨ x = -4 ∨ x = -3 ∨ x = -2 ∨ x = -1 ∨ x = 1 ∨ x = 2 ∨ x = 3 ∨ x = 4 ∨ x = 6 ∨ x = 8 ∨ x = 12 ∨ x = 24

State before:
x : ℤ
this : x ∣ 24 ↔ Int.natAbs x ∈ {1, 2, 3, 4, 6, 8, 12, 24}
⊢ x ∣ 24 ↔
    x = -24 ∨
      x = -12 ∨
        x = -8 ∨
          x = -6 ∨ x = -4 ∨ x = -3 ∨ x = -2 ∨ x = -1 ∨ x = 1 ∨ x = 2 ∨ x = 3 ∨ x = 4 ∨ x = 6 ∨ x = 8 ∨ x = 12 ∨ x = 24
Tactic:
simp only [Finset.mem_insert, Int.natAbs_eq_iff, Nat.cast_one,
  Nat.cast_ofNat, Finset.mem_singleton] at this
State after:
x : ℤ
this :
  x ∣ 24 ↔
    (x = 1 ∨ x = -1) ∨
      (x = 2 ∨ x = -2) ∨
        (x = 3 ∨ x = -3) ∨
          (x = 4 ∨ x = -4) ∨ (x = 6 ∨ x = -6) ∨ (x = 8 ∨ x = -8) ∨ (x = 12 ∨ x = -12) ∨ x = 24 ∨ x = -24
⊢ x ∣ 24 ↔
    x = -24 ∨
      x = -12 ∨
        x = -8 ∨
          x = -6 ∨ x = -4 ∨ x = -3 ∨ x = -2 ∨ x = -1 ∨ x = 1 ∨ x = 2 ∨ x = 3 ∨ x = 4 ∨ x = 6 ∨ x = 8 ∨ x = 12 ∨ x = 24

State before:
x : ℤ
this :
  x ∣ 24 ↔
    (x = 1 ∨ x = -1) ∨
      (x = 2 ∨ x = -2) ∨
        (x = 3 ∨ x = -3) ∨
          (x = 4 ∨ x = -4) ∨ (x = 6 ∨ x = -6) ∨ (x = 8 ∨ x = -8) ∨ (x = 12 ∨ x = -12) ∨ x = 24 ∨ x = -24
⊢ x ∣ 24 ↔
    x = -24 ∨
      x = -12 ∨
        x = -8 ∨
          x = -6 ∨ x = -4 ∨ x = -3 ∨ x = -2 ∨ x = -1 ∨ x = 1 ∨ x = 2 ∨ x = 3 ∨ x = 4 ∨ x = 6 ∨ x = 8 ∨ x = 12 ∨ x = 24
Tactic:
tauto
State after:
no goals

State before:
x : ℤ
⊢ 24 ≠ 0
Tactic:
norm_num
State after:
no goals