Theorem: ASCII.Char.isLower_iff (ASCII/Lemmas.lean)

State before:
c : ASCII.Char
⊢ c.isLower = true ↔ 97 ≤ c.toNat ∧ c.toNat ≤ 122
Tactic:
simp [isLower]
State after:
c : ASCII.Char
⊢ 97 ≤ c.toByte ∧ c.toByte ≤ 122 ↔ 97 ≤ c.toNat ∧ c.toNat ≤ 122

State before:
c : ASCII.Char
⊢ 97 ≤ c.toByte ∧ c.toByte ≤ 122 ↔ 97 ≤ c.toNat ∧ c.toNat ≤ 122
Tactic:
rfl
State after:
no goals