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

State before:
c : ASCII.Char
⊢ ¬c.toLower.isUpper = true
Tactic:
simp [-not_and, toLower, isUpper_iff]
State after:
c : ASCII.Char
⊢ ¬(65 ≤ (if h : 65 ≤ c.toNat ∧ c.toNat ≤ 90 then ofNatAux (c.toNat + 32) ⋯ else c).toNat ∧
      (if h : 65 ≤ c.toNat ∧ c.toNat ≤ 90 then ofNatAux (c.toNat + 32) ⋯ else c).toNat ≤ 90)

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

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

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

State before:
c : ASCII.Char
h : 65 ≤ c.toNat ∧ c.toNat ≤ 90
⊢ ¬(65 ≤ (ofNatAux (c.toNat + 32) ⋯).toNat ∧ (ofNatAux (c.toNat + 32) ⋯).toNat ≤ 90)
Tactic:
simp [-not_and, toNat_ofNatAux]
State after:
c : ASCII.Char
h : 65 ≤ c.toNat ∧ c.toNat ≤ 90
⊢ ¬(33 ≤ c.toNat ∧ c.toNat ≤ 58)

State before:
c : ASCII.Char
h : 65 ≤ c.toNat ∧ c.toNat ≤ 90
⊢ ¬(33 ≤ c.toNat ∧ c.toNat ≤ 58)
Tactic:
intro h'
State after:
c : ASCII.Char
h : 65 ≤ c.toNat ∧ c.toNat ≤ 90
h' : 33 ≤ c.toNat ∧ c.toNat ≤ 58
⊢ False

State before:
c : ASCII.Char
h : 65 ≤ c.toNat ∧ c.toNat ≤ 90
h' : 33 ≤ c.toNat ∧ c.toNat ≤ 58
⊢ False
Tactic:
absurd h'.2
State after:
c : ASCII.Char
h : 65 ≤ c.toNat ∧ c.toNat ≤ 90
h' : 33 ≤ c.toNat ∧ c.toNat ≤ 58
⊢ ¬c.toNat ≤ 58

State before:
c : ASCII.Char
h : 65 ≤ c.toNat ∧ c.toNat ≤ 90
h' : 33 ≤ c.toNat ∧ c.toNat ≤ 58
⊢ ¬c.toNat ≤ 58
Tactic:
apply Nat.not_le_of_gt
State after:
case h
c : ASCII.Char
h : 65 ≤ c.toNat ∧ c.toNat ≤ 90
h' : 33 ≤ c.toNat ∧ c.toNat ≤ 58
⊢ c.toNat > 58

State before:
case h
c : ASCII.Char
h : 65 ≤ c.toNat ∧ c.toNat ≤ 90
h' : 33 ≤ c.toNat ∧ c.toNat ≤ 58
⊢ c.toNat > 58
Tactic:
apply Nat.lt_of_lt_of_le _ h.1
State after:
c : ASCII.Char
h : 65 ≤ c.toNat ∧ c.toNat ≤ 90
h' : 33 ≤ c.toNat ∧ c.toNat ≤ 58
⊢ 58 < 65

State before:
c : ASCII.Char
h : 65 ≤ c.toNat ∧ c.toNat ≤ 90
h' : 33 ≤ c.toNat ∧ c.toNat ≤ 58
⊢ 58 < 65
Tactic:
decide
State after:
no goals

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