Theorem: LO.FirstOrder.UFormula.and_primrec (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 μ
⊢ Primrec₂ and
Tactic:
have := w_mk₂ (β := Edge L μ) (fun (_ : Unit) => (true, Sum.inr $ Sum.inr $ Sum.inl ())) (by rintro ⟨⟩; simp[Edge]) (const _)
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 μ
this :
  Primrec₂ fun x w =>
    WType.mk ((fun x => (true, Sum.inr (Sum.inr (Sum.inl ())))) x) ((fintypeArrowEquivFinArrow' ⋯).symm ![w.1, w.2])
⊢ Primrec₂ and

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 μ
this :
  Primrec₂ fun x w =>
    WType.mk ((fun x => (true, Sum.inr (Sum.inr (Sum.inl ())))) x) ((fintypeArrowEquivFinArrow' ⋯).symm ![w.1, w.2])
⊢ Primrec₂ and
Tactic:
have := (Primrec.of_equiv_symm (e := equivW L μ)).comp₂
  ((this.comp₂ (Primrec₂.const ()) Primrec.id.to₂).comp₂
    ((Primrec.of_equiv (e := equivW L μ)).comp₂ Primrec₂.left)
    ((Primrec.of_equiv (e := equivW L μ)).comp₂ Primrec₂.right))
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 μ
this✝ :
  Primrec₂ fun x w =>
    WType.mk ((fun x => (true, Sum.inr (Sum.inr (Sum.inl ())))) x) ((fintypeArrowEquivFinArrow' ⋯).symm ![w.1, w.2])
this :
  Primrec₂ fun a b =>
    (equivW L μ).symm
      (WType.mk ((fun x => (true, Sum.inr (Sum.inr (Sum.inl ())))) ())
        ((fintypeArrowEquivFinArrow' ⋯).symm
          ![(id ((equivW L μ) a, (equivW L μ) b)).1, (id ((equivW L μ) a, (equivW L μ) b)).2]))
⊢ Primrec₂ and

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 μ
this✝ :
  Primrec₂ fun x w =>
    WType.mk ((fun x => (true, Sum.inr (Sum.inr (Sum.inl ())))) x) ((fintypeArrowEquivFinArrow' ⋯).symm ![w.1, w.2])
this :
  Primrec₂ fun a b =>
    (equivW L μ).symm
      (WType.mk ((fun x => (true, Sum.inr (Sum.inr (Sum.inl ())))) ())
        ((fintypeArrowEquivFinArrow' ⋯).symm
          ![(id ((equivW L μ) a, (equivW L μ) b)).1, (id ((equivW L μ) a, (equivW L μ) b)).2]))
⊢ Primrec₂ and
Tactic:
exact this.of_eq (fun p q => by simp; rw [fintypeEquivFin_false, fintypeEquivFin_true]; 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 μ
⊢ ∀ (x : Unit), Fintype.card (Edge L μ ((fun x => (true, Sum.inr (Sum.inr (Sum.inl ())))) x)) = 2
Tactic:
rintro ⟨⟩
State after:
case unit
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 μ
⊢ Fintype.card (Edge L μ ((fun x => (true, Sum.inr (Sum.inr (Sum.inl ())))) PUnit.unit)) = 2

State before:
case unit
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 μ
⊢ Fintype.card (Edge L μ ((fun x => (true, Sum.inr (Sum.inr (Sum.inl ())))) PUnit.unit)) = 2
Tactic:
simp[Edge]
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 μ
this✝ :
  Primrec₂ fun x w =>
    WType.mk ((fun x => (true, Sum.inr (Sum.inr (Sum.inl ())))) x) ((fintypeArrowEquivFinArrow' ⋯).symm ![w.1, w.2])
this :
  Primrec₂ fun a b =>
    (equivW L μ).symm
      (WType.mk ((fun x => (true, Sum.inr (Sum.inr (Sum.inl ())))) ())
        ((fintypeArrowEquivFinArrow' ⋯).symm
          ![(id ((equivW L μ) a, (equivW L μ) b)).1, (id ((equivW L μ) a, (equivW L μ) b)).2]))
p q : UFormula L μ
⊢ (equivW L μ).symm
      (WType.mk ((fun x => (true, Sum.inr (Sum.inr (Sum.inl ())))) ())
        ((fintypeArrowEquivFinArrow' ⋯).symm
          ![(id ((equivW L μ) p, (equivW L μ) q)).1, (id ((equivW L μ) p, (equivW L μ) q)).2])) =
    p.and q
Tactic:
simp
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 μ
this✝ :
  Primrec₂ fun x w =>
    WType.mk ((fun x => (true, Sum.inr (Sum.inr (Sum.inl ())))) x) ((fintypeArrowEquivFinArrow' ⋯).symm ![w.1, w.2])
this :
  Primrec₂ fun a b =>
    (equivW L μ).symm
      (WType.mk ((fun x => (true, Sum.inr (Sum.inr (Sum.inl ())))) ())
        ((fintypeArrowEquivFinArrow' ⋯).symm
          ![(id ((equivW L μ) a, (equivW L μ) b)).1, (id ((equivW L μ) a, (equivW L μ) b)).2]))
p q : UFormula L μ
⊢ (equivW L μ).symm (![(equivW L μ) p, (equivW L μ) q] (fintypeEquivFin false)) = p ∧
    (equivW L μ).symm (![(equivW L μ) p, (equivW L μ) q] (fintypeEquivFin true)) = q

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 μ
this✝ :
  Primrec₂ fun x w =>
    WType.mk ((fun x => (true, Sum.inr (Sum.inr (Sum.inl ())))) x) ((fintypeArrowEquivFinArrow' ⋯).symm ![w.1, w.2])
this :
  Primrec₂ fun a b =>
    (equivW L μ).symm
      (WType.mk ((fun x => (true, Sum.inr (Sum.inr (Sum.inl ())))) ())
        ((fintypeArrowEquivFinArrow' ⋯).symm
          ![(id ((equivW L μ) a, (equivW L μ) b)).1, (id ((equivW L μ) a, (equivW L μ) b)).2]))
p q : UFormula L μ
⊢ (equivW L μ).symm (![(equivW L μ) p, (equivW L μ) q] (fintypeEquivFin false)) = p ∧
    (equivW L μ).symm (![(equivW L μ) p, (equivW L μ) q] (fintypeEquivFin true)) = q
Tactic:
rw [fintypeEquivFin_false, fintypeEquivFin_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 μ
this✝ :
  Primrec₂ fun x w =>
    WType.mk ((fun x => (true, Sum.inr (Sum.inr (Sum.inl ())))) x) ((fintypeArrowEquivFinArrow' ⋯).symm ![w.1, w.2])
this :
  Primrec₂ fun a b =>
    (equivW L μ).symm
      (WType.mk ((fun x => (true, Sum.inr (Sum.inr (Sum.inl ())))) ())
        ((fintypeArrowEquivFinArrow' ⋯).symm
          ![(id ((equivW L μ) a, (equivW L μ) b)).1, (id ((equivW L μ) a, (equivW L μ) b)).2]))
p q : UFormula L μ
⊢ (equivW L μ).symm (![(equivW L μ) p, (equivW L μ) q] 0) = p ∧
    (equivW L μ).symm (![(equivW L μ) p, (equivW L μ) q] 1) = q

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 μ
this✝ :
  Primrec₂ fun x w =>
    WType.mk ((fun x => (true, Sum.inr (Sum.inr (Sum.inl ())))) x) ((fintypeArrowEquivFinArrow' ⋯).symm ![w.1, w.2])
this :
  Primrec₂ fun a b =>
    (equivW L μ).symm
      (WType.mk ((fun x => (true, Sum.inr (Sum.inr (Sum.inl ())))) ())
        ((fintypeArrowEquivFinArrow' ⋯).symm
          ![(id ((equivW L μ) a, (equivW L μ) b)).1, (id ((equivW L μ) a, (equivW L μ) b)).2]))
p q : UFormula L μ
⊢ (equivW L μ).symm (![(equivW L μ) p, (equivW L μ) q] 0) = p ∧
    (equivW L μ).symm (![(equivW L μ) p, (equivW L μ) q] 1) = q
Tactic:
simp
State after:
no goals