Theorem: nullable_emptyStr (Katydid/Conal/Calculus.lean)

State before:
⊢ (α : Type) → ν' ε ≃ PUnit.{u_1}
Tactic:
intro α
State after:
α : Type
⊢ ν' ε ≃ PUnit.{u_1}

State before:
α : Type
⊢ ν' ε ≃ PUnit.{u_1}
Tactic:
refine Equiv.mk ?a ?b ?c ?d
State after:
case a
α : Type
⊢ ν' ε → PUnit.{u_1}

case b
α : Type
⊢ PUnit.{u_1} → ν' ε

case c
α : Type
⊢ Function.LeftInverse ?b ?a

case d
α : Type
⊢ Function.RightInverse ?b ?a

State before:
case a
α : Type
⊢ ν' ε → PUnit.{u_1}

case b
α : Type
⊢ PUnit.{u_1} → ν' ε

case c
α : Type
⊢ Function.LeftInverse ?b ?a

case d
α : Type
⊢ Function.RightInverse ?b ?a
Tactic:
intro _
State after:
case a
α : Type
a✝ : ν' ε
⊢ PUnit.{u_1}

case b
α : Type
⊢ PUnit.{u_1} → ν' ε

case c
α : Type
⊢ Function.LeftInverse ?b fun a => ?m.3703 a

case d
α : Type
⊢ Function.RightInverse ?b fun a => ?m.3703 a

State before:
case a
α : Type
a✝ : ν' ε
⊢ PUnit.{u_1}

case b
α : Type
⊢ PUnit.{u_1} → ν' ε

case c
α : Type
⊢ Function.LeftInverse ?b fun a => ?m.3703 a

case d
α : Type
⊢ Function.RightInverse ?b fun a => ?m.3703 a
Tactic:
exact PUnit.unit
State after:
case b
α : Type
⊢ PUnit.{u_1} → ν' ε

case c
α : Type
⊢ Function.LeftInverse ?b fun a => PUnit.unit

case d
α : Type
⊢ Function.RightInverse ?b fun a => PUnit.unit

State before:
case b
α : Type
⊢ PUnit.{u_1} → ν' ε

case c
α : Type
⊢ Function.LeftInverse ?b fun a => PUnit.unit

case d
α : Type
⊢ Function.RightInverse ?b fun a => PUnit.unit
Tactic:
intro _
State after:
case b
α : Type
a✝ : PUnit.{u_1}
⊢ ν' ε

case c
α : Type
⊢ Function.LeftInverse (fun a => ?m.3707 a) fun a => PUnit.unit

case d
α : Type
⊢ Function.RightInverse (fun a => ?m.3707 a) fun a => PUnit.unit

State before:
case b
α : Type
a✝ : PUnit.{u_1}
⊢ ν' ε

case c
α : Type
⊢ Function.LeftInverse (fun a => ?m.3707 a) fun a => PUnit.unit

case d
α : Type
⊢ Function.RightInverse (fun a => ?m.3707 a) fun a => PUnit.unit
Tactic:
constructor
State after:
case b.a
α : Type
a✝ : PUnit.{u_1}
⊢ [] = []

case c
α : Type
⊢ Function.LeftInverse (fun a => ?m.3707 a) fun a => PUnit.unit

case d
α : Type
⊢ Function.RightInverse (fun a => ?m.3707 a) fun a => PUnit.unit

State before:
case b.a
α : Type
a✝ : PUnit.{u_1}
⊢ [] = []

case c
α : Type
⊢ Function.LeftInverse (fun a => ?m.3707 a) fun a => PUnit.unit

case d
α : Type
⊢ Function.RightInverse (fun a => ?m.3707 a) fun a => PUnit.unit
Tactic:
rfl
State after:
case c
α : Type
⊢ Function.LeftInverse (fun a => TEq.mk (_ : [] = [])) fun a => PUnit.unit

case d
α : Type
⊢ Function.RightInverse (fun a => TEq.mk (_ : [] = [])) fun a => PUnit.unit

State before:
case c
α : Type
⊢ Function.LeftInverse (fun a => TEq.mk (_ : [] = [])) fun a => PUnit.unit

case d
α : Type
⊢ Function.RightInverse (fun a => TEq.mk (_ : [] = [])) fun a => PUnit.unit
Tactic:
intro c
State after:
case c
α : Type
c : ν' ε
⊢ (fun a => TEq.mk (_ : [] = [])) ((fun a => PUnit.unit) c) = c

case d
α : Type
⊢ Function.RightInverse (fun a => TEq.mk (_ : [] = [])) fun a => PUnit.unit

State before:
case c
α : Type
c : ν' ε
⊢ (fun a => TEq.mk (_ : [] = [])) ((fun a => PUnit.unit) c) = c

case d
α : Type
⊢ Function.RightInverse (fun a => TEq.mk (_ : [] = [])) fun a => PUnit.unit
Tactic:
simp
State after:
case c
α : Type
c : ν' ε
⊢ TEq.mk (_ : [] = []) = c

case d
α : Type
⊢ Function.RightInverse (fun a => TEq.mk (_ : [] = [])) fun a => PUnit.unit

State before:
case c
α : Type
c : ν' ε
⊢ TEq.mk (_ : [] = []) = c

case d
α : Type
⊢ Function.RightInverse (fun a => TEq.mk (_ : [] = [])) fun a => PUnit.unit
Tactic:
constructor
State after:
case d
α : Type
⊢ Function.RightInverse (fun a => TEq.mk (_ : [] = [])) fun a => PUnit.unit

State before:
case d
α : Type
⊢ Function.RightInverse (fun a => TEq.mk (_ : [] = [])) fun a => PUnit.unit
Tactic:
intro _
State after:
case d
α : Type
x✝ : PUnit.{u_1}
⊢ (fun a => PUnit.unit) ((fun a => TEq.mk (_ : [] = [])) x✝) = x✝

State before:
case d
α : Type
x✝ : PUnit.{u_1}
⊢ (fun a => PUnit.unit) ((fun a => TEq.mk (_ : [] = [])) x✝) = x✝
Tactic:
simp
State after:
no goals