Theorem: nullable_char' (Katydid/Conal/Calculus.lean)

State before:
α : Type u_1
⊢ (c : α) → ν' (char c) → PEmpty.{u_2}
Tactic:
intro
State after:
α : Type u_1
c✝ : α
⊢ ν' (char c✝) → PEmpty.{u_2}

State before:
α : Type u_1
c✝ : α
⊢ ν' (char c✝) → PEmpty.{u_2}
Tactic:
refine (fun x => ?c)
State after:
case c
α : Type u_1
c✝ : α
x : ν' (char c✝)
⊢ PEmpty.{u_2}

State before:
case c
α : Type u_1
c✝ : α
x : ν' (char c✝)
⊢ PEmpty.{u_2}
Tactic:
simp at x
State after:
case c
α : Type u_1
c✝ : α
x : [] ≡ [c✝]
⊢ PEmpty.{u_2}

State before:
case c
α : Type u_1
c✝ : α
x : [] ≡ [c✝]
⊢ PEmpty.{u_2}
Tactic:
cases x with
| mk x =>
  contradiction
State after:
no goals

State before:
case c.mk
α : Type u_1
c✝ : α
x : [] = [c✝]
⊢ PEmpty.{u_2}
Tactic:
contradiction
State after:
no goals