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

State before:
c : ASCII.Char
⊢ ¬c.toUpper.isLower = true
Tactic:
simp [-not_and, toUpper, isLower_iff]
State after:
c : ASCII.Char
⊢ ¬(97 ≤ (if h : 97 ≤ c.toNat ∧ c.toNat ≤ 122 then ofNatAux (c.toNat - 32) ⋯ else c).toNat ∧
      (if h : 97 ≤ c.toNat ∧ c.toNat ≤ 122 then ofNatAux (c.toNat - 32) ⋯ else c).toNat ≤ 122)

State before:
c : ASCII.Char
⊢ ¬(97 ≤ (if h : 97 ≤ c.toNat ∧ c.toNat ≤ 122 then ofNatAux (c.toNat - 32) ⋯ else c).toNat ∧
      (if h : 97 ≤ c.toNat ∧ c.toNat ≤ 122 then ofNatAux (c.toNat - 32) ⋯ else c).toNat ≤ 122)
Tactic:
split
State after:
case isTrue
c : ASCII.Char
h✝ : 97 ≤ c.toNat ∧ c.toNat ≤ 122
⊢ ¬(97 ≤ (ofNatAux (c.toNat - 32) ⋯).toNat ∧ (ofNatAux (c.toNat - 32) ⋯).toNat ≤ 122)

case isFalse
c : ASCII.Char
h✝ : ¬(97 ≤ c.toNat ∧ c.toNat ≤ 122)
⊢ ¬(97 ≤ c.toNat ∧ c.toNat ≤ 122)

State before:
case isTrue
c : ASCII.Char
h✝ : 97 ≤ c.toNat ∧ c.toNat ≤ 122
⊢ ¬(97 ≤ (ofNatAux (c.toNat - 32) ⋯).toNat ∧ (ofNatAux (c.toNat - 32) ⋯).toNat ≤ 122)
Tactic:
next h =>
simp [-not_and, toNat_ofNatAux]
intro h'
absurd h'.1
apply Nat.not_le_of_gt
apply Nat.lt_of_le_of_lt (Nat.sub_le_sub_right h.2 32)
decide
State after:
no goals

State before:
c : ASCII.Char
h : 97 ≤ c.toNat ∧ c.toNat ≤ 122
⊢ ¬(97 ≤ (ofNatAux (c.toNat - 32) ⋯).toNat ∧ (ofNatAux (c.toNat - 32) ⋯).toNat ≤ 122)
Tactic:
simp [-not_and, toNat_ofNatAux]
State after:
c : ASCII.Char
h : 97 ≤ c.toNat ∧ c.toNat ≤ 122
⊢ ¬(97 ≤ c.toNat - 32 ∧ c.toNat - 32 ≤ 122)

State before:
c : ASCII.Char
h : 97 ≤ c.toNat ∧ c.toNat ≤ 122
⊢ ¬(97 ≤ c.toNat - 32 ∧ c.toNat - 32 ≤ 122)
Tactic:
intro h'
State after:
c : ASCII.Char
h : 97 ≤ c.toNat ∧ c.toNat ≤ 122
h' : 97 ≤ c.toNat - 32 ∧ c.toNat - 32 ≤ 122
⊢ False

State before:
c : ASCII.Char
h : 97 ≤ c.toNat ∧ c.toNat ≤ 122
h' : 97 ≤ c.toNat - 32 ∧ c.toNat - 32 ≤ 122
⊢ False
Tactic:
absurd h'.1
State after:
c : ASCII.Char
h : 97 ≤ c.toNat ∧ c.toNat ≤ 122
h' : 97 ≤ c.toNat - 32 ∧ c.toNat - 32 ≤ 122
⊢ ¬97 ≤ c.toNat - 32

State before:
c : ASCII.Char
h : 97 ≤ c.toNat ∧ c.toNat ≤ 122
h' : 97 ≤ c.toNat - 32 ∧ c.toNat - 32 ≤ 122
⊢ ¬97 ≤ c.toNat - 32
Tactic:
apply Nat.not_le_of_gt
State after:
case h
c : ASCII.Char
h : 97 ≤ c.toNat ∧ c.toNat ≤ 122
h' : 97 ≤ c.toNat - 32 ∧ c.toNat - 32 ≤ 122
⊢ 97 > c.toNat - 32

State before:
case h
c : ASCII.Char
h : 97 ≤ c.toNat ∧ c.toNat ≤ 122
h' : 97 ≤ c.toNat - 32 ∧ c.toNat - 32 ≤ 122
⊢ 97 > c.toNat - 32
Tactic:
apply Nat.lt_of_le_of_lt (Nat.sub_le_sub_right h.2 32)
State after:
case h
c : ASCII.Char
h : 97 ≤ c.toNat ∧ c.toNat ≤ 122
h' : 97 ≤ c.toNat - 32 ∧ c.toNat - 32 ≤ 122
⊢ 122 - 32 < 97

State before:
case h
c : ASCII.Char
h : 97 ≤ c.toNat ∧ c.toNat ≤ 122
h' : 97 ≤ c.toNat - 32 ∧ c.toNat - 32 ≤ 122
⊢ 122 - 32 < 97
Tactic:
decide
State after:
no goals

State before:
case isFalse
c : ASCII.Char
h✝ : ¬(97 ≤ c.toNat ∧ c.toNat ≤ 122)
⊢ ¬(97 ≤ c.toNat ∧ c.toNat ≤ 122)
Tactic:
assumption
State after:
no goals