internlm/Lean-Github huggingface dataset:
Theorem: nullable_emptyStr
Proof 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 _
Proof 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
Theorem: nullable_emptyStr
Proof 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
Proof 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
Theorem: nullable_emptyStr
Proof 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 _
Proof 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
Theorem: nullable_emptyStr
Proof 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
Proof 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
Theorem: nullable_emptyStr
Proof 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
Proof 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
Theorem: nullable_emptyStr
Proof 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
Proof 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
Theorem: nullable_emptyStr
Proof 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
Proof state after:
case c
α : Type
c : ν' ε
⊢ TEq.mk (_ : [] = []) = c

case d
α : Type
⊢ Function.RightInverse (fun a => TEq.mk (_ : [] = [])) fun a => PUnit.unit
Theorem: nullable_emptyStr
Proof state before:
case c
α : Type
c : ν' ε
⊢ TEq.mk (_ : [] = []) = c

case d
α : Type
⊢ Function.RightInverse (fun a => TEq.mk (_ : [] = [])) fun a => PUnit.unit
Tactic:
constructor
Proof state after:
case d
α : Type
⊢ Function.RightInverse (fun a => TEq.mk (_ : [] = [])) fun a => PUnit.unit
Theorem: nullable_emptyStr
Proof state before:
case d
α : Type
⊢ Function.RightInverse (fun a => TEq.mk (_ : [] = [])) fun a => PUnit.unit
Tactic:
intro _
Proof state after:
case d
α : Type
x✝ : PUnit.{u_1}
⊢ (fun a => PUnit.unit) ((fun a => TEq.mk (_ : [] = [])) x✝) = x✝
Theorem: nullable_emptyStr
Proof state before:
case d
α : Type
x✝ : PUnit.{u_1}
⊢ (fun a => PUnit.unit) ((fun a => TEq.mk (_ : [] = [])) x✝) = x✝
Tactic:
simp
Proof state after:
no goals
Theorem: nullable_emptyStr'
Proof state before:
x✝¹ : Type
x✝ : PUnit.{u_1}
⊢ ν' ε
Tactic:
constructor
Proof state after:
case a
x✝¹ : Type
x✝ : PUnit.{u_1}
⊢ [] = []
Theorem: nullable_emptyStr'
Proof state before:
case a
x✝¹ : Type
x✝ : PUnit.{u_1}
⊢ [] = []
Tactic:
rfl
Proof state after:
no goals
Theorem: nullable_char
Proof state before:
α : Type u_1
⊢ (c : α) → ν' (char c) ≃ PEmpty.{u_2}
Tactic:
intro α
Proof state after:
α✝ : Type u_1
α : α✝
⊢ ν' (char α) ≃ PEmpty.{u_2}
Theorem: nullable_char
Proof state before:
α✝ : Type u_1
α : α✝
⊢ ν' (char α) ≃ PEmpty.{u_2}
Tactic:
simp
Proof state after:
α✝ : Type u_1
α : α✝
⊢ [] ≡ [α] ≃ PEmpty.{u_2}
Theorem: nullable_char
Proof state before:
α✝ : Type u_1
α : α✝
⊢ [] ≡ [α] ≃ PEmpty.{u_2}
Tactic:
apply Equiv.mk
Proof 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} → [] ≡ [α]
Theorem: nullable_char
Proof 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
Proof 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} → [] ≡ [α]
Theorem: nullable_char
Proof 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
Proof 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} → [] ≡ [α]
Theorem: nullable_char
Proof 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
Proof 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} → [] ≡ [α]
Theorem: nullable_char
Proof 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
Proof state after:
case toFun
α✝ : Type u_1
α : α✝
⊢ [] ≡ [α] → PEmpty.{u_2}

case invFun
α✝ : Type u_1
α : α✝
⊢ PEmpty.{u_2} → [] ≡ [α]
Theorem: nullable_char
Proof state before:
case toFun
α✝ : Type u_1
α : α✝
⊢ [] ≡ [α] → PEmpty.{u_2}

case invFun
α✝ : Type u_1
α : α✝
⊢ PEmpty.{u_2} → [] ≡ [α]
Tactic:
sorry
Proof state after:
case invFun
α✝ : Type u_1
α : α✝
⊢ PEmpty.{u_2} → [] ≡ [α]
Theorem: nullable_char
Proof state before:
case invFun
α✝ : Type u_1
α : α✝
⊢ PEmpty.{u_2} → [] ≡ [α]
Tactic:
sorry
Proof state after:
no goals
Theorem: nullable_char
Proof state before:
case left_inv.mk
α✝ : Type u_1
α : α✝
x : [] = [α]
⊢ ?invFun (?toFun (TEq.mk x)) = TEq.mk x
Tactic:
contradiction
Proof state after:
no goals
Theorem: nullable_char'
Proof state before:
α : Type u_1
⊢ (c : α) → ν' (char c) → PEmpty.{u_2}
Tactic:
intro
Proof state after:
α : Type u_1
c✝ : α
⊢ ν' (char c✝) → PEmpty.{u_2}
Theorem: nullable_char'
Proof state before:
α : Type u_1
c✝ : α
⊢ ν' (char c✝) → PEmpty.{u_2}
Tactic:
refine (fun x => ?c)
Proof state after:
case c
α : Type u_1
c✝ : α
x : ν' (char c✝)
⊢ PEmpty.{u_2}
Theorem: nullable_char'
Proof state before:
case c
α : Type u_1
c✝ : α
x : ν' (char c✝)
⊢ PEmpty.{u_2}
Tactic:
simp at x
Proof state after:
case c
α : Type u_1
c✝ : α
x : [] ≡ [c✝]
⊢ PEmpty.{u_2}
Theorem: nullable_char'
Proof state before:
case c
α : Type u_1
c✝ : α
x : [] ≡ [c✝]
⊢ PEmpty.{u_2}
Tactic:
cases x with
| mk x =>
  contradiction
Proof state after:
no goals
Theorem: nullable_char'
Proof state before:
case c.mk
α : Type u_1
c✝ : α
x : [] = [c✝]
⊢ PEmpty.{u_2}
Tactic:
contradiction
Proof state after:
no goals
Theorem: nullable_or
Proof state before:
α : Type (max u_1 u_2)
⊢ (P Q : dLang α) → ν' (P ⋃ Q) ≡ (ν' P ⊕ ν' Q)
Tactic:
intro P Q
Proof state after:
α : Type (max u_1 u_2)
P Q : dLang α
⊢ ν' (P ⋃ Q) ≡ (ν' P ⊕ ν' Q)
Theorem: nullable_or
Proof state before:
α : Type (max u_1 u_2)
P Q : dLang α
⊢ ν' (P ⋃ Q) ≡ (ν' P ⊕ ν' Q)
Tactic:
constructor
Proof state after:
case a
α : Type (max u_1 u_2)
P Q : dLang α
⊢ ν' (P ⋃ Q) = (ν' P ⊕ ν' Q)
Theorem: nullable_or
Proof state before:
case a
α : Type (max u_1 u_2)
P Q : dLang α
⊢ ν' (P ⋃ Q) = (ν' P ⊕ ν' Q)
Tactic:
rfl
Proof state after:
no goals
Theorem: nullable_and
Proof state before:
α : Type (max u_1 u_2)
⊢ (P Q : dLang α) → ν' (P ⋂ Q) ≡ (ν' P × ν' Q)
Tactic:
intro P Q
Proof state after:
α : Type (max u_1 u_2)
P Q : dLang α
⊢ ν' (P ⋂ Q) ≡ (ν' P × ν' Q)
Theorem: nullable_and
Proof state before:
α : Type (max u_1 u_2)
P Q : dLang α
⊢ ν' (P ⋂ Q) ≡ (ν' P × ν' Q)
Tactic:
constructor
Proof state after:
case a
α : Type (max u_1 u_2)
P Q : dLang α
⊢ ν' (P ⋂ Q) = (ν' P × ν' Q)
Theorem: nullable_and
Proof state before:
case a
α : Type (max u_1 u_2)
P Q : dLang α
⊢ ν' (P ⋂ Q) = (ν' P × ν' Q)
Tactic:
rfl
Proof state after:
no goals
Theorem: nullable_scalar
Proof state before:
α : Type
⊢ (s : Type) → (P : dLang α) → ν' (s · P) ≡ (s × ν' P)
Tactic:
intro P Q
Proof state after:
α P : Type
Q : dLang α
⊢ ν' (P · Q) ≡ (P × ν' Q)
Theorem: nullable_scalar
Proof state before:
α P : Type
Q : dLang α
⊢ ν' (P · Q) ≡ (P × ν' Q)
Tactic:
constructor
Proof state after:
case a
α P : Type
Q : dLang α
⊢ ν' (P · Q) = (P × ν' Q)
Theorem: nullable_scalar
Proof state before:
case a
α P : Type
Q : dLang α
⊢ ν' (P · Q) = (P × ν' Q)
Tactic:
rfl
Proof state after:
no goals
Theorem: nullable_concat
Proof state before:
α : Type u_1
⊢ (P Q : dLang α) → ν' (P , Q) ≃ ν' Q × ν' P
Tactic:
sorry
Proof state after:
no goals
Theorem: nullable_star
Proof state before:
α : Type u_1
⊢ (P : dLang α) → ν' (P*) ≃ List (ν' P)
Tactic:
sorry
Proof state after:
no goals
Theorem: derivative_emptySet
Proof state before:
α : Type u_1
⊢ (a : α) → δ' ∅ a ≡ ∅
Tactic:
intro a
Proof state after:
α : Type u_1
a : α
⊢ δ' ∅ a ≡ ∅
Theorem: derivative_emptySet
Proof state before:
α : Type u_1
a : α
⊢ δ' ∅ a ≡ ∅
Tactic:
constructor
Proof state after:
case a
α : Type u_1
a : α
⊢ δ' ∅ a = ∅
Theorem: derivative_emptySet
Proof state before:
case a
α : Type u_1
a : α
⊢ δ' ∅ a = ∅
Tactic:
rfl
Proof state after:
no goals
Theorem: derivative_universal
Proof state before:
α : Type u_1
⊢ (a : α) → δ' 𝒰 a ≡ 𝒰
Tactic:
intro a
Proof state after:
α : Type u_1
a : α
⊢ δ' 𝒰 a ≡ 𝒰
Theorem: derivative_universal
Proof state before:
α : Type u_1
a : α
⊢ δ' 𝒰 a ≡ 𝒰
Tactic:
constructor
Proof state after:
case a
α : Type u_1
a : α
⊢ δ' 𝒰 a = 𝒰
Theorem: derivative_universal
Proof state before:
case a
α : Type u_1
a : α
⊢ δ' 𝒰 a = 𝒰
Tactic:
rfl
Proof state after:
no goals
Theorem: derivative_emptyStr
Proof state before:
α : Type u_1
⊢ (a : α) → δ' ε a ≡ ∅
Tactic:
sorry
Proof state after:
no goals
Theorem: derivative_char
Proof state before:
α : Type u_1
⊢ (a c : α) → δ' (char c) a ≡ (a ≡ c · ε)
Tactic:
intros a c
Proof state after:
α : Type u_1
a c : α
⊢ δ' (char c) a ≡ (a ≡ c · ε)
Theorem: derivative_char
Proof state before:
α : Type u_1
a c : α
⊢ δ' (char c) a ≡ (a ≡ c · ε)
Tactic:
unfold δ'
Proof state after:
α : Type u_1
a c : α
⊢ (fun w => char c (a :: w)) ≡ (a ≡ c · ε)
Theorem: derivative_char
Proof state before:
α : Type u_1
a c : α
⊢ (fun w => char c (a :: w)) ≡ (a ≡ c · ε)
Tactic:
unfold char
Proof state after:
α : Type u_1
a c : α
⊢ (fun w => a :: w ≡ [c]) ≡ (a ≡ c · ε)
Theorem: derivative_char
Proof state before:
α : Type u_1
a c : α
⊢ (fun w => a :: w ≡ [c]) ≡ (a ≡ c · ε)
Tactic:
unfold emptyStr
Proof state after:
α : Type u_1
a c : α
⊢ (fun w => a :: w ≡ [c]) ≡ (a ≡ c · fun w => w ≡ [])
Theorem: derivative_char
Proof state before:
α : Type u_1
a c : α
⊢ (fun w => a :: w ≡ [c]) ≡ (a ≡ c · fun w => w ≡ [])
Tactic:
unfold scalar
Proof state after:
α : Type u_1
a c : α
⊢ (fun w => a :: w ≡ [c]) ≡ fun w => a ≡ c × (fun w => w ≡ []) w
Theorem: derivative_char
Proof state before:
α : Type u_1
a c : α
⊢ (fun w => a :: w ≡ [c]) ≡ fun w => a ≡ c × (fun w => w ≡ []) w
Tactic:
sorry
Proof state after:
no goals
Theorem: derivative_or
Proof state before:
α : Type u_1
⊢ (a : α) → (P Q : dLang α) → δ' (P ⋃ Q) a ≡ (δ' P a ⋃ δ' Q a)
Tactic:
intro a P Q
Proof state after:
α : Type u_1
a : α
P Q : dLang α
⊢ δ' (P ⋃ Q) a ≡ (δ' P a ⋃ δ' Q a)
Theorem: derivative_or
Proof state before:
α : Type u_1
a : α
P Q : dLang α
⊢ δ' (P ⋃ Q) a ≡ (δ' P a ⋃ δ' Q a)
Tactic:
constructor
Proof state after:
case a
α : Type u_1
a : α
P Q : dLang α
⊢ δ' (P ⋃ Q) a = (δ' P a ⋃ δ' Q a)
Theorem: derivative_or
Proof state before:
case a
α : Type u_1
a : α
P Q : dLang α
⊢ δ' (P ⋃ Q) a = (δ' P a ⋃ δ' Q a)
Tactic:
rfl
Proof state after:
no goals
Theorem: derivative_and
Proof state before:
α : Type u_1
⊢ (a : α) → (P Q : dLang α) → δ' (P ⋂ Q) a ≡ (δ' P a ⋂ δ' Q a)
Tactic:
intro a P Q
Proof state after:
α : Type u_1
a : α
P Q : dLang α
⊢ δ' (P ⋂ Q) a ≡ (δ' P a ⋂ δ' Q a)
Theorem: derivative_and
Proof state before:
α : Type u_1
a : α
P Q : dLang α
⊢ δ' (P ⋂ Q) a ≡ (δ' P a ⋂ δ' Q a)
Tactic:
constructor
Proof state after:
case a
α : Type u_1
a : α
P Q : dLang α
⊢ δ' (P ⋂ Q) a = (δ' P a ⋂ δ' Q a)
Theorem: derivative_and
Proof state before:
case a
α : Type u_1
a : α
P Q : dLang α
⊢ δ' (P ⋂ Q) a = (δ' P a ⋂ δ' Q a)
Tactic:
rfl
Proof state after:
no goals
Theorem: derivative_scalar
Proof state before:
α : Type
⊢ (a : α) → (s : Type) → (P : dLang α) → δ (s · P) a ≡ (s · δ' P a)
Tactic:
intro a s P
Proof state after:
α : Type
a : α
s : Type
P : dLang α
⊢ δ (s · P) a ≡ (s · δ' P a)
Theorem: derivative_scalar
Proof state before:
α : Type
a : α
s : Type
P : dLang α
⊢ δ (s · P) a ≡ (s · δ' P a)
Tactic:
constructor
Proof state after:
case a
α : Type
a : α
s : Type
P : dLang α
⊢ δ (s · P) a = (s · δ' P a)
Theorem: derivative_scalar
Proof state before:
case a
α : Type
a : α
s : Type
P : dLang α
⊢ δ (s · P) a = (s · δ' P a)
Tactic:
rfl
Proof state after:
no goals
Theorem: derivative_concat
Proof state before:
α : Type u_1
⊢ (a : α) → (P Q : dLang α) → δ' (P , Q) a ≡ (ν' P · δ' Q a ⋃ (δ' P a , Q))
Tactic:
sorry
Proof state after:
no goals
Theorem: derivative_star
Proof state before:
α : Type u_1
⊢ (a : α) → (P : dLang α) → δ' (P*) a ≡ (List (ν' P) · δ' P a , P*)
Tactic:
sorry
Proof state after:
no goals
Theorem: ASCII.Char.toNat_eq_iff_ofNatAux_eq
Proof state before:
c : ASCII.Char
n : Nat
hn : n < 128
⊢ c.toNat = n ↔ ofNatAux n hn = c
Tactic:
simp only [toNat, ofNatAux]
Proof state after:
c : ASCII.Char
n : Nat
hn : n < 128
⊢ c.toByte.toNat = n ↔ { toByte := { val := ⟨n, ⋯⟩ }, valid := hn } = c
Theorem: ASCII.Char.toNat_eq_iff_ofNatAux_eq
Proof state before:
c : ASCII.Char
n : Nat
hn : n < 128
⊢ c.toByte.toNat = n ↔ { toByte := { val := ⟨n, ⋯⟩ }, valid := hn } = c
Tactic:
constructor
Proof state after:
case mp
c : ASCII.Char
n : Nat
hn : n < 128
⊢ c.toByte.toNat = n → { toByte := { val := ⟨n, ⋯⟩ }, valid := hn } = c

case mpr
c : ASCII.Char
n : Nat
hn : n < 128
⊢ { toByte := { val := ⟨n, ⋯⟩ }, valid := hn } = c → c.toByte.toNat = n
Theorem: ASCII.Char.toNat_eq_iff_ofNatAux_eq
Proof state before:
case mp
c : ASCII.Char
n : Nat
hn : n < 128
⊢ c.toByte.toNat = n → { toByte := { val := ⟨n, ⋯⟩ }, valid := hn } = c
Tactic:
intro h
Proof state after:
case mp
c : ASCII.Char
n : Nat
hn : n < 128
h : c.toByte.toNat = n
⊢ { toByte := { val := ⟨n, ⋯⟩ }, valid := hn } = c
Theorem: ASCII.Char.toNat_eq_iff_ofNatAux_eq
Proof state before:
case mp
c : ASCII.Char
n : Nat
hn : n < 128
h : c.toByte.toNat = n
⊢ { toByte := { val := ⟨n, ⋯⟩ }, valid := hn } = c
Tactic:
cases h
Proof state after:
case mp.refl
c : ASCII.Char
hn : c.toByte.toNat < 128
⊢ { toByte := { val := ⟨c.toByte.toNat, ⋯⟩ }, valid := hn } = c
Theorem: ASCII.Char.toNat_eq_iff_ofNatAux_eq
Proof state before:
case mp.refl
c : ASCII.Char
hn : c.toByte.toNat < 128
⊢ { toByte := { val := ⟨c.toByte.toNat, ⋯⟩ }, valid := hn } = c
Tactic:
ext
Proof state after:
case mp.refl.a.a
c : ASCII.Char
hn : c.toByte.toNat < 128
⊢ { toByte := { val := ⟨c.toByte.toNat, ⋯⟩ }, valid := hn }.toByte.toNat = c.toByte.toNat
Theorem: ASCII.Char.toNat_eq_iff_ofNatAux_eq
Proof state before:
case mp.refl.a.a
c : ASCII.Char
hn : c.toByte.toNat < 128
⊢ { toByte := { val := ⟨c.toByte.toNat, ⋯⟩ }, valid := hn }.toByte.toNat = c.toByte.toNat
Tactic:
simp only [dif_pos c.toNat_lt, UInt8.toNat]
Proof state after:
no goals
Theorem: ASCII.Char.toNat_eq_iff_ofNatAux_eq
Proof state before:
case mpr
c : ASCII.Char
n : Nat
hn : n < 128
⊢ { toByte := { val := ⟨n, ⋯⟩ }, valid := hn } = c → c.toByte.toNat = n
Tactic:
intro h
Proof state after:
case mpr
c : ASCII.Char
n : Nat
hn : n < 128
h : { toByte := { val := ⟨n, ⋯⟩ }, valid := hn } = c
⊢ c.toByte.toNat = n
Theorem: ASCII.Char.toNat_eq_iff_ofNatAux_eq
Proof state before:
case mpr
c : ASCII.Char
n : Nat
hn : n < 128
h : { toByte := { val := ⟨n, ⋯⟩ }, valid := hn } = c
⊢ c.toByte.toNat = n
Tactic:
cases h
Proof state after:
case mpr.refl
n : Nat
hn : n < 128
⊢ { toByte := { val := ⟨n, ⋯⟩ }, valid := hn }.toByte.toNat = n
Theorem: ASCII.Char.toNat_eq_iff_ofNatAux_eq
Proof state before:
case mpr.refl
n : Nat
hn : n < 128
⊢ { toByte := { val := ⟨n, ⋯⟩ }, valid := hn }.toByte.toNat = n
Tactic:
simp only [dif_pos hn, ofNatAux, UInt8.toNat]
Proof state after:
no goals
Theorem: ASCII.Char.toNat_ofNatAux
Proof state before:
n : Nat
hn : n < 128
⊢ (ofNatAux n hn).toNat = n
Tactic:
rw [toNat_eq_iff_ofNatAux_eq]
Proof state after:
no goals
Theorem: ASCII.Char.ofNatAux_toNat
Proof state before:
c : ASCII.Char
⊢ ofNatAux c.toNat ⋯ = c
Tactic:
rw [← toNat_eq_iff_ofNatAux_eq]
Proof state after:
no goals
Theorem: ASCII.Char.toNat_eq_iff_ofNat_eq
Proof state before:
c : ASCII.Char
n : Nat
hn : n < 128
⊢ c.toNat = n ↔ ofNat n = c
Tactic:
rw [ofNat, dif_pos hn]
Proof state after:
c : ASCII.Char
n : Nat
hn : n < 128
⊢ c.toNat = n ↔ ofNatAux n hn = c
Theorem: ASCII.Char.toNat_eq_iff_ofNat_eq
Proof state before:
c : ASCII.Char
n : Nat
hn : n < 128
⊢ c.toNat = n ↔ ofNatAux n hn = c
Tactic:
exact toNat_eq_iff_ofNatAux_eq ..
Proof state after:
no goals
Theorem: ASCII.Char.toNat_ofNat
Proof state before:
n : Nat
hn : n < 128
⊢ (ofNat n).toNat = n
Tactic:
rw [toNat_eq_iff_ofNat_eq]
Proof state after:
case hn
n : Nat
hn : n < 128
⊢ n < 128
Theorem: ASCII.Char.toNat_ofNat
Proof state before:
case hn
n : Nat
hn : n < 128
⊢ n < 128
Tactic:
exact hn
Proof state after:
no goals
Theorem: ASCII.Char.ofNat_toNat
Proof state before:
c : ASCII.Char
⊢ ofNat c.toNat = c
Tactic:
rw [← toNat_eq_iff_ofNat_eq]
Proof state after:
case hn
c : ASCII.Char
⊢ c.toNat < 128
Theorem: ASCII.Char.ofNat_toNat
Proof state before:
case hn
c : ASCII.Char
⊢ c.toNat < 128
Tactic:
exact c.toNat_lt
Proof state after:
no goals
Theorem: ASCII.Char.toUnicode_eq_iff_ofUnicode_eq
Proof state before:
c : ASCII.Char
u : Unicode.Char
hu : Char.isASCII u = true
⊢ ↑c = u ↔ ofUnicode u hu = c
Tactic:
simp only [Char.toUnicode, ofUnicode]
Proof state after:
c : ASCII.Char
u : Unicode.Char
hu : Char.isASCII u = true
⊢ { val := c.toByte.toUInt32, valid := ⋯ } = u ↔ { toByte := u.val.toUInt8, valid := ⋯ } = c
Theorem: ASCII.Char.toUnicode_eq_iff_ofUnicode_eq
Proof state before:
c : ASCII.Char
u : Unicode.Char
hu : Char.isASCII u = true
⊢ { val := c.toByte.toUInt32, valid := ⋯ } = u ↔ { toByte := u.val.toUInt8, valid := ⋯ } = c
Tactic:
constructor
Proof state after:
case mp
c : ASCII.Char
u : Unicode.Char
hu : Char.isASCII u = true
⊢ { val := c.toByte.toUInt32, valid := ⋯ } = u → { toByte := u.val.toUInt8, valid := ⋯ } = c

case mpr
c : ASCII.Char
u : Unicode.Char
hu : Char.isASCII u = true
⊢ { toByte := u.val.toUInt8, valid := ⋯ } = c → { val := c.toByte.toUInt32, valid := ⋯ } = u
Theorem: ASCII.Char.toUnicode_eq_iff_ofUnicode_eq
Proof state before:
case mp
c : ASCII.Char
u : Unicode.Char
hu : Char.isASCII u = true
⊢ { val := c.toByte.toUInt32, valid := ⋯ } = u → { toByte := u.val.toUInt8, valid := ⋯ } = c
Tactic:
intro h
Proof state after:
case mp
c : ASCII.Char
u : Unicode.Char
hu : Char.isASCII u = true
h : { val := c.toByte.toUInt32, valid := ⋯ } = u
⊢ { toByte := u.val.toUInt8, valid := ⋯ } = c
Theorem: ASCII.Char.toUnicode_eq_iff_ofUnicode_eq
Proof state before:
case mp
c : ASCII.Char
u : Unicode.Char
hu : Char.isASCII u = true
h : { val := c.toByte.toUInt32, valid := ⋯ } = u
⊢ { toByte := u.val.toUInt8, valid := ⋯ } = c
Tactic:
cases h
Proof state after:
case mp.refl
c : ASCII.Char
hu : { val := c.toByte.toUInt32, valid := ⋯ }.isASCII = true
⊢ { toByte := { val := c.toByte.toUInt32, valid := ⋯ }.val.toUInt8, valid := ⋯ } = c
Theorem: ASCII.Char.toUnicode_eq_iff_ofUnicode_eq
Proof state before:
case mp.refl
c : ASCII.Char
hu : { val := c.toByte.toUInt32, valid := ⋯ }.isASCII = true
⊢ { toByte := { val := c.toByte.toUInt32, valid := ⋯ }.val.toUInt8, valid := ⋯ } = c
Tactic:
simp [_root_.Char.isASCII, _root_.Char.toNat] at hu
Proof state after:
case mp.refl
c : ASCII.Char
hu✝ : { val := c.toByte.toUInt32, valid := ⋯ }.isASCII = true
hu : c.toByte.toNat < 128
⊢ { toByte := { val := c.toByte.toUInt32, valid := ⋯ }.val.toUInt8, valid := ⋯ } = c
Theorem: ASCII.Char.toUnicode_eq_iff_ofUnicode_eq
Proof state before:
case mp.refl
c : ASCII.Char
hu✝ : { val := c.toByte.toUInt32, valid := ⋯ }.isASCII = true
hu : c.toByte.toNat < 128
⊢ { toByte := { val := c.toByte.toUInt32, valid := ⋯ }.val.toUInt8, valid := ⋯ } = c
Tactic:
have hlt : c.toNat < 256 := by apply Nat.lt_trans hu; decide
Proof state after:
case mp.refl
c : ASCII.Char
hu✝ : { val := c.toByte.toUInt32, valid := ⋯ }.isASCII = true
hu : c.toByte.toNat < 128
hlt : c.toNat < 256
⊢ { toByte := { val := c.toByte.toUInt32, valid := ⋯ }.val.toUInt8, valid := ⋯ } = c
Theorem: ASCII.Char.toUnicode_eq_iff_ofUnicode_eq
Proof state before:
case mp.refl
c : ASCII.Char
hu✝ : { val := c.toByte.toUInt32, valid := ⋯ }.isASCII = true
hu : c.toByte.toNat < 128
hlt : c.toNat < 256
⊢ { toByte := { val := c.toByte.toUInt32, valid := ⋯ }.val.toUInt8, valid := ⋯ } = c
Tactic:
ext
Proof state after:
case mp.refl.a.a
c : ASCII.Char
hu✝ : { val := c.toByte.toUInt32, valid := ⋯ }.isASCII = true
hu : c.toByte.toNat < 128
hlt : c.toNat < 256
⊢ { toByte := { val := c.toByte.toUInt32, valid := ⋯ }.val.toUInt8, valid := ⋯ }.toByte.toNat = c.toByte.toNat
Theorem: ASCII.Char.toUnicode_eq_iff_ofUnicode_eq
Proof state before:
case mp.refl.a.a
c : ASCII.Char
hu✝ : { val := c.toByte.toUInt32, valid := ⋯ }.isASCII = true
hu : c.toByte.toNat < 128
hlt : c.toNat < 256
⊢ { toByte := { val := c.toByte.toUInt32, valid := ⋯ }.val.toUInt8, valid := ⋯ }.toByte.toNat = c.toByte.toNat
Tactic:
simp [Nat.mod_eq_of_lt hlt]
Proof state after:
no goals
Theorem: ASCII.Char.toUnicode_eq_iff_ofUnicode_eq
Proof state before:
c : ASCII.Char
hu✝ : { val := c.toByte.toUInt32, valid := ⋯ }.isASCII = true
hu : c.toByte.toNat < 128
⊢ c.toNat < 256
Tactic:
apply Nat.lt_trans hu
Proof state after:
c : ASCII.Char
hu✝ : { val := c.toByte.toUInt32, valid := ⋯ }.isASCII = true
hu : c.toByte.toNat < 128
⊢ 128 < 256
Theorem: ASCII.Char.toUnicode_eq_iff_ofUnicode_eq
Proof state before:
c : ASCII.Char
hu✝ : { val := c.toByte.toUInt32, valid := ⋯ }.isASCII = true
hu : c.toByte.toNat < 128
⊢ 128 < 256
Tactic:
decide
Proof state after:
no goals
Theorem: ASCII.Char.toUnicode_eq_iff_ofUnicode_eq
Proof state before:
case mpr
c : ASCII.Char
u : Unicode.Char
hu : Char.isASCII u = true
⊢ { toByte := u.val.toUInt8, valid := ⋯ } = c → { val := c.toByte.toUInt32, valid := ⋯ } = u
Tactic:
intro h
Proof state after:
case mpr
c : ASCII.Char
u : Unicode.Char
hu : Char.isASCII u = true
h : { toByte := u.val.toUInt8, valid := ⋯ } = c
⊢ { val := c.toByte.toUInt32, valid := ⋯ } = u