Theorem: allPrimeNums (FromTheBook/Ch02/Bertrand/LandauTrick.lean)

State before:
⊢ List.All₂ Nat.Prime nums
Tactic:
simp (config := {decide := false}) [nums]
State after:
⊢ Nat.Prime 2 ∧
    Nat.Prime 3 ∧
      Nat.Prime 5 ∧
        Nat.Prime 7 ∧
          Nat.Prime 13 ∧
            Nat.Prime 23 ∧
              Nat.Prime 43 ∧
                Nat.Prime 83 ∧
                  Nat.Prime 163 ∧ Nat.Prime 317 ∧ Nat.Prime 631 ∧ Nat.Prime 1259 ∧ Nat.Prime 2503 ∧ Nat.Prime 4001

State before:
⊢ Nat.Prime 2 ∧
    Nat.Prime 3 ∧
      Nat.Prime 5 ∧
        Nat.Prime 7 ∧
          Nat.Prime 13 ∧
            Nat.Prime 23 ∧
              Nat.Prime 43 ∧
                Nat.Prime 83 ∧
                  Nat.Prime 163 ∧ Nat.Prime 317 ∧ Nat.Prime 631 ∧ Nat.Prime 1259 ∧ Nat.Prime 2503 ∧ Nat.Prime 4001
Tactic:
norm_num1
State after:
⊢ True ∧ True ∧ True ∧ True ∧ True ∧ True ∧ True ∧ True ∧ True ∧ True ∧ True ∧ True ∧ True ∧ True

State before:
⊢ True ∧ True ∧ True ∧ True ∧ True ∧ True ∧ True ∧ True ∧ True ∧ True ∧ True ∧ True ∧ True ∧ True
Tactic:
simp
State after:
no goals