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

State before:
c : ASCII.Char
⊢ c.isLower = true → ¬c.isUpper = true
Tactic:
simp only [isLower_iff, isUpper_iff]
State after:
c : ASCII.Char
⊢ 97 ≤ c.toNat ∧ c.toNat ≤ 122 → ¬(65 ≤ c.toNat ∧ c.toNat ≤ 90)

State before:
c : ASCII.Char
⊢ 97 ≤ c.toNat ∧ c.toNat ≤ 122 → ¬(65 ≤ c.toNat ∧ c.toNat ≤ 90)
Tactic:
intro ⟨hl, _⟩ ⟨_, hu⟩
State after:
c : ASCII.Char
hl : 97 ≤ c.toNat
right✝ : c.toNat ≤ 122
left✝ : 65 ≤ c.toNat
hu : c.toNat ≤ 90
⊢ False

State before:
c : ASCII.Char
hl : 97 ≤ c.toNat
right✝ : c.toNat ≤ 122
left✝ : 65 ≤ c.toNat
hu : c.toNat ≤ 90
⊢ False
Tactic:
apply Nat.lt_irrefl c.toNat
State after:
c : ASCII.Char
hl : 97 ≤ c.toNat
right✝ : c.toNat ≤ 122
left✝ : 65 ≤ c.toNat
hu : c.toNat ≤ 90
⊢ c.toNat < c.toNat

State before:
c : ASCII.Char
hl : 97 ≤ c.toNat
right✝ : c.toNat ≤ 122
left✝ : 65 ≤ c.toNat
hu : c.toNat ≤ 90
⊢ c.toNat < c.toNat
Tactic:
apply Nat.lt_of_le_of_lt hu
State after:
c : ASCII.Char
hl : 97 ≤ c.toNat
right✝ : c.toNat ≤ 122
left✝ : 65 ≤ c.toNat
hu : c.toNat ≤ 90
⊢ 90 < c.toNat

State before:
c : ASCII.Char
hl : 97 ≤ c.toNat
right✝ : c.toNat ≤ 122
left✝ : 65 ≤ c.toNat
hu : c.toNat ≤ 90
⊢ 90 < c.toNat
Tactic:
apply Nat.lt_of_lt_of_le _ hl
State after:
c : ASCII.Char
hl : 97 ≤ c.toNat
right✝ : c.toNat ≤ 122
left✝ : 65 ≤ c.toNat
hu : c.toNat ≤ 90
⊢ 90 < 97

State before:
c : ASCII.Char
hl : 97 ≤ c.toNat
right✝ : c.toNat ≤ 122
left✝ : 65 ≤ c.toNat
hu : c.toNat ≤ 90
⊢ 90 < 97
Tactic:
decide
State after:
no goals