Theorem: LO.FirstOrder.UFormula.toW_ofW (Logic/FirstOrder/Computability/Formula.lean)

State before:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
fst✝ : ℕ
r : L.Rel fst✝
v : Fin fst✝ → UTerm L μ
f✝ : Edge L μ (true, Sum.inl ⟨fst✝, (r, v)⟩) → WType (Edge L μ)
⊢ (ofW (WType.mk (true, Sum.inl ⟨fst✝, (r, v)⟩) f✝)).toW = WType.mk (true, Sum.inl ⟨fst✝, (r, v)⟩) f✝
Tactic:
simp[ofW, toW, Empty.eq_elim]
State after:
no goals

State before:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
fst✝ : ℕ
r : L.Rel fst✝
v : Fin fst✝ → UTerm L μ
f✝ : Edge L μ (false, Sum.inl ⟨fst✝, (r, v)⟩) → WType (Edge L μ)
⊢ (ofW (WType.mk (false, Sum.inl ⟨fst✝, (r, v)⟩) f✝)).toW = WType.mk (false, Sum.inl ⟨fst✝, (r, v)⟩) f✝
Tactic:
simp[ofW, toW, Empty.eq_elim]
State after:
no goals

State before:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
f✝ : Edge L μ (true, Sum.inr (Sum.inl ())) → WType (Edge L μ)
⊢ (ofW (WType.mk (true, Sum.inr (Sum.inl ())) f✝)).toW = WType.mk (true, Sum.inr (Sum.inl ())) f✝
Tactic:
simp[ofW, toW, Empty.eq_elim]
State after:
no goals

State before:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
f✝ : Edge L μ (false, Sum.inr (Sum.inl ())) → WType (Edge L μ)
⊢ (ofW (WType.mk (false, Sum.inr (Sum.inl ())) f✝)).toW = WType.mk (false, Sum.inr (Sum.inl ())) f✝
Tactic:
simp[ofW, toW, Empty.eq_elim]
State after:
no goals

State before:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
w : Edge L μ (true, Sum.inr (Sum.inr (Sum.inl ()))) → WType (Edge L μ)
⊢ (ofW (WType.mk (true, Sum.inr (Sum.inr (Sum.inl ()))) w)).toW = WType.mk (true, Sum.inr (Sum.inr (Sum.inl ()))) w
Tactic:
simp[ofW, toW, toW_ofW (w false), toW_ofW (w true)]
State after:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
w : Edge L μ (true, Sum.inr (Sum.inr (Sum.inl ()))) → WType (Edge L μ)
⊢ (fun t => Bool.rec (w false) (w true) t) = w

State before:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
w : Edge L μ (true, Sum.inr (Sum.inr (Sum.inl ()))) → WType (Edge L μ)
⊢ (fun t => Bool.rec (w false) (w true) t) = w
Tactic:
ext b
State after:
case h
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
w : Edge L μ (true, Sum.inr (Sum.inr (Sum.inl ()))) → WType (Edge L μ)
b : Bool
⊢ Bool.rec (w false) (w true) b = w b

State before:
case h
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
w : Edge L μ (true, Sum.inr (Sum.inr (Sum.inl ()))) → WType (Edge L μ)
b : Bool
⊢ Bool.rec (w false) (w true) b = w b
Tactic:
cases b <;> simp
State after:
no goals

State before:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
w : Edge L μ (false, Sum.inr (Sum.inr (Sum.inl ()))) → WType (Edge L μ)
⊢ (ofW (WType.mk (false, Sum.inr (Sum.inr (Sum.inl ()))) w)).toW = WType.mk (false, Sum.inr (Sum.inr (Sum.inl ()))) w
Tactic:
simp[ofW, toW, toW_ofW (w false), toW_ofW (w true)]
State after:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
w : Edge L μ (false, Sum.inr (Sum.inr (Sum.inl ()))) → WType (Edge L μ)
⊢ (fun t => Bool.rec (w false) (w true) t) = w

State before:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
w : Edge L μ (false, Sum.inr (Sum.inr (Sum.inl ()))) → WType (Edge L μ)
⊢ (fun t => Bool.rec (w false) (w true) t) = w
Tactic:
ext b
State after:
case h
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
w : Edge L μ (false, Sum.inr (Sum.inr (Sum.inl ()))) → WType (Edge L μ)
b : Bool
⊢ Bool.rec (w false) (w true) b = w b

State before:
case h
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
w : Edge L μ (false, Sum.inr (Sum.inr (Sum.inl ()))) → WType (Edge L μ)
b : Bool
⊢ Bool.rec (w false) (w true) b = w b
Tactic:
cases b <;> simp
State after:
no goals

State before:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
w : Edge L μ (true, Sum.inr (Sum.inr (Sum.inr ()))) → WType (Edge L μ)
⊢ (ofW (WType.mk (true, Sum.inr (Sum.inr (Sum.inr ()))) w)).toW = WType.mk (true, Sum.inr (Sum.inr (Sum.inr ()))) w
Tactic:
simp[ofW, toW, toW_ofW (w ())]
State after:
no goals

State before:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
w : Edge L μ (false, Sum.inr (Sum.inr (Sum.inr ()))) → WType (Edge L μ)
⊢ (ofW (WType.mk (false, Sum.inr (Sum.inr (Sum.inr ()))) w)).toW = WType.mk (false, Sum.inr (Sum.inr (Sum.inr ()))) w
Tactic:
simp[ofW, toW, toW_ofW (w ())]
State after:
no goals