Theorem: Primrec.lawfulbeq (Logic/Vorspiel/Computability.lean)

State before:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁸ : Primcodable σ
inst✝⁷ : Primcodable α
inst✝⁶ : (a : α) → Fintype (β a)
inst✝⁵ : (a : α) → DecidableEq (β a)
inst✝⁴ : (a : α) → Primcodable (β a)
inst✝³ : PrimrecCard β
inst✝² : Primcodable γ
inst✝¹ : BEq α
inst✝ : LawfulBEq α
⊢ Primrec₂ BEq.beq
Tactic:
haveI : DecidableEq α := Encodable.decidableEqOfEncodable α
State after:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁸ : Primcodable σ
inst✝⁷ : Primcodable α
inst✝⁶ : (a : α) → Fintype (β a)
inst✝⁵ : (a : α) → DecidableEq (β a)
inst✝⁴ : (a : α) → Primcodable (β a)
inst✝³ : PrimrecCard β
inst✝² : Primcodable γ
inst✝¹ : BEq α
inst✝ : LawfulBEq α
this : DecidableEq α
⊢ Primrec₂ BEq.beq

State before:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁸ : Primcodable σ
inst✝⁷ : Primcodable α
inst✝⁶ : (a : α) → Fintype (β a)
inst✝⁵ : (a : α) → DecidableEq (β a)
inst✝⁴ : (a : α) → Primcodable (β a)
inst✝³ : PrimrecCard β
inst✝² : Primcodable γ
inst✝¹ : BEq α
inst✝ : LawfulBEq α
this : DecidableEq α
⊢ Primrec₂ BEq.beq
Tactic:
exact Primrec₂.of_eq Primrec.eq (by intro a b; simp[decide_eq_iff])
State after:
no goals

State before:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁸ : Primcodable σ
inst✝⁷ : Primcodable α
inst✝⁶ : (a : α) → Fintype (β a)
inst✝⁵ : (a : α) → DecidableEq (β a)
inst✝⁴ : (a : α) → Primcodable (β a)
inst✝³ : PrimrecCard β
inst✝² : Primcodable γ
inst✝¹ : BEq α
inst✝ : LawfulBEq α
this : DecidableEq α
⊢ ∀ (a b : α), decide (a = b) = (a == b)
Tactic:
intro a b
State after:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁸ : Primcodable σ
inst✝⁷ : Primcodable α
inst✝⁶ : (a : α) → Fintype (β a)
inst✝⁵ : (a : α) → DecidableEq (β a)
inst✝⁴ : (a : α) → Primcodable (β a)
inst✝³ : PrimrecCard β
inst✝² : Primcodable γ
inst✝¹ : BEq α
inst✝ : LawfulBEq α
this : DecidableEq α
a b : α
⊢ decide (a = b) = (a == b)

State before:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁸ : Primcodable σ
inst✝⁷ : Primcodable α
inst✝⁶ : (a : α) → Fintype (β a)
inst✝⁵ : (a : α) → DecidableEq (β a)
inst✝⁴ : (a : α) → Primcodable (β a)
inst✝³ : PrimrecCard β
inst✝² : Primcodable γ
inst✝¹ : BEq α
inst✝ : LawfulBEq α
this : DecidableEq α
a b : α
⊢ decide (a = b) = (a == b)
Tactic:
simp[decide_eq_iff]
State after:
no goals