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

State before:
c : ASCII.Char
h : ¬c.isLower = true
⊢ c.toUpper = c
Tactic:
simp [toUpper]
State after:
c : ASCII.Char
h : ¬c.isLower = true
⊢ ∀ (h : c.isLower = true), ofNatAux (c.toNat - 32) ⋯ = c

State before:
c : ASCII.Char
h : ¬c.isLower = true
⊢ ∀ (h : c.isLower = true), ofNatAux (c.toNat - 32) ⋯ = c
Tactic:
intro
State after:
c : ASCII.Char
h : ¬c.isLower = true
h✝ : c.isLower = true
⊢ ofNatAux (c.toNat - 32) ⋯ = c

State before:
c : ASCII.Char
h : ¬c.isLower = true
h✝ : c.isLower = true
⊢ ofNatAux (c.toNat - 32) ⋯ = c
Tactic:
contradiction
State after:
no goals