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
α : α✝
⊢ ν' (char α) ≃ PEmpty.{u_2}

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

State before:
α✝ : Type u_1
α : α✝
⊢ [] ≡ [α] ≃ PEmpty.{u_2}
Tactic:
apply Equiv.mk
State after:
case left_inv
α✝ : Type u_1
α : α✝
⊢ Function.LeftInverse ?invFun ?toFun

case right_inv
α✝ : Type u_1
α : α✝
⊢ Function.RightInverse ?invFun ?toFun

case toFun
α✝ : Type u_1
α : α✝
⊢ [] ≡ [α] → PEmpty.{u_2}

case invFun
α✝ : Type u_1
α : α✝
⊢ PEmpty.{u_2} → [] ≡ [α]

State before:
case left_inv
α✝ : Type u_1
α : α✝
⊢ Function.LeftInverse ?invFun ?toFun

case right_inv
α✝ : Type u_1
α : α✝
⊢ Function.RightInverse ?invFun ?toFun

case toFun
α✝ : Type u_1
α : α✝
⊢ [] ≡ [α] → PEmpty.{u_2}

case invFun
α✝ : Type u_1
α : α✝
⊢ PEmpty.{u_2} → [] ≡ [α]
Tactic:
intro x
State after:
case left_inv
α✝ : Type u_1
α : α✝
x : [] ≡ [α]
⊢ ?invFun (?toFun x) = x

case right_inv
α✝ : Type u_1
α : α✝
⊢ Function.RightInverse ?invFun ?toFun

case toFun
α✝ : Type u_1
α : α✝
⊢ [] ≡ [α] → PEmpty.{u_2}

case invFun
α✝ : Type u_1
α : α✝
⊢ PEmpty.{u_2} → [] ≡ [α]

State before:
case left_inv
α✝ : Type u_1
α : α✝
x : [] ≡ [α]
⊢ ?invFun (?toFun x) = x

case right_inv
α✝ : Type u_1
α : α✝
⊢ Function.RightInverse ?invFun ?toFun

case toFun
α✝ : Type u_1
α : α✝
⊢ [] ≡ [α] → PEmpty.{u_2}

case invFun
α✝ : Type u_1
α : α✝
⊢ PEmpty.{u_2} → [] ≡ [α]
Tactic:
cases x with
| mk x =>
  contradiction
State after:
case right_inv
α✝ : Type u_1
α : α✝
⊢ Function.RightInverse ?invFun ?toFun

case toFun
α✝ : Type u_1
α : α✝
⊢ [] ≡ [α] → PEmpty.{u_2}

case invFun
α✝ : Type u_1
α : α✝
⊢ PEmpty.{u_2} → [] ≡ [α]

State before:
case right_inv
α✝ : Type u_1
α : α✝
⊢ Function.RightInverse ?invFun ?toFun

case toFun
α✝ : Type u_1
α : α✝
⊢ [] ≡ [α] → PEmpty.{u_2}

case invFun
α✝ : Type u_1
α : α✝
⊢ PEmpty.{u_2} → [] ≡ [α]
Tactic:
intro
State after:
case right_inv
α✝ : Type u_1
α : α✝
x✝ : PEmpty.{u_2}
⊢ ?toFun (?invFun x✝) = x✝

case toFun
α✝ : Type u_1
α : α✝
⊢ [] ≡ [α] → PEmpty.{u_2}

case invFun
α✝ : Type u_1
α : α✝
⊢ PEmpty.{u_2} → [] ≡ [α]

State before:
case right_inv
α✝ : Type u_1
α : α✝
x✝ : PEmpty.{u_2}
⊢ ?toFun (?invFun x✝) = x✝

case toFun
α✝ : Type u_1
α : α✝
⊢ [] ≡ [α] → PEmpty.{u_2}

case invFun
α✝ : Type u_1
α : α✝
⊢ PEmpty.{u_2} → [] ≡ [α]
Tactic:
contradiction
State after:
case toFun
α✝ : Type u_1
α : α✝
⊢ [] ≡ [α] → PEmpty.{u_2}

case invFun
α✝ : Type u_1
α : α✝
⊢ PEmpty.{u_2} → [] ≡ [α]

State before:
case toFun
α✝ : Type u_1
α : α✝
⊢ [] ≡ [α] → PEmpty.{u_2}

case invFun
α✝ : Type u_1
α : α✝
⊢ PEmpty.{u_2} → [] ≡ [α]
Tactic:
sorry
State after:
case invFun
α✝ : Type u_1
α : α✝
⊢ PEmpty.{u_2} → [] ≡ [α]

State before:
case invFun
α✝ : Type u_1
α : α✝
⊢ PEmpty.{u_2} → [] ≡ [α]
Tactic:
sorry
State after:
no goals

State before:
case left_inv.mk
α✝ : Type u_1
α : α✝
x : [] = [α]
⊢ ?invFun (?toFun (TEq.mk x)) = TEq.mk x
Tactic:
contradiction
State after:
no goals