internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.UFormula.relL_primrec
Proof state before:
case mk
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 r l =>
    if l.length = r.fst then Nat.pair 1 ((Nat.pair 1 ((2 * r.fst.pair) ((encode r.snd).pair (encode l)))).pair 0) + 1
    else 0
k : ℕ
r : L.Rel k
l : List (UTerm L μ)
⊢ (if l.length = ⟨k, r⟩.fst then
      Nat.pair 1 ((Nat.pair 1 ((2 * ⟨k, r⟩.fst.pair) ((encode ⟨k, r⟩.snd).pair (encode l)))).pair 0) + 1
    else 0) =
    encode (relL ⟨k, r⟩ l)
Tactic:
by_cases hl : l.length = k <;> simp[hl, relL, primcodable, Primcodable.ofEquiv_toEncodable]
Proof state after:
case pos
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 r l =>
    if l.length = r.fst then Nat.pair 1 ((Nat.pair 1 ((2 * r.fst.pair) ((encode r.snd).pair (encode l)))).pair 0) + 1
    else 0
k : ℕ
r : L.Rel k
l : List (UTerm L μ)
hl : l.length = k
⊢ Nat.pair 1 ((Nat.pair 1 (2 * k.pair ((encode r).pair (encode l)))).pair 0) =
    encode (rel r fun i => l.get (Fin.cast ⋯ i))
Theorem: LO.FirstOrder.UFormula.relL_primrec
Proof state before:
case pos
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 r l =>
    if l.length = r.fst then Nat.pair 1 ((Nat.pair 1 ((2 * r.fst.pair) ((encode r.snd).pair (encode l)))).pair 0) + 1
    else 0
k : ℕ
r : L.Rel k
l : List (UTerm L μ)
hl : l.length = k
⊢ Nat.pair 1 ((Nat.pair 1 (2 * k.pair ((encode r).pair (encode l)))).pair 0) =
    encode (rel r fun i => l.get (Fin.cast ⋯ i))
Tactic:
{ rcases hl with rfl
  simp[encode_rel, encode_finArrow, List.ofFn_get] }
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.relL_primrec
Proof state before:
case pos
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 r l =>
    if l.length = r.fst then Nat.pair 1 ((Nat.pair 1 ((2 * r.fst.pair) ((encode r.snd).pair (encode l)))).pair 0) + 1
    else 0
k : ℕ
r : L.Rel k
l : List (UTerm L μ)
hl : l.length = k
⊢ Nat.pair 1 ((Nat.pair 1 (2 * k.pair ((encode r).pair (encode l)))).pair 0) =
    encode (rel r fun i => l.get (Fin.cast ⋯ i))
Tactic:
rcases hl with rfl
Proof state after:
case pos
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 r l =>
    if l.length = r.fst then Nat.pair 1 ((Nat.pair 1 ((2 * r.fst.pair) ((encode r.snd).pair (encode l)))).pair 0) + 1
    else 0
l : List (UTerm L μ)
r : L.Rel l.length
⊢ Nat.pair 1 ((Nat.pair 1 (2 * l.length.pair ((encode r).pair (encode l)))).pair 0) =
    encode (rel r fun i => l.get (Fin.cast ⋯ i))
Theorem: LO.FirstOrder.UFormula.relL_primrec
Proof state before:
case pos
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 r l =>
    if l.length = r.fst then Nat.pair 1 ((Nat.pair 1 ((2 * r.fst.pair) ((encode r.snd).pair (encode l)))).pair 0) + 1
    else 0
l : List (UTerm L μ)
r : L.Rel l.length
⊢ Nat.pair 1 ((Nat.pair 1 (2 * l.length.pair ((encode r).pair (encode l)))).pair 0) =
    encode (rel r fun i => l.get (Fin.cast ⋯ i))
Tactic:
simp[encode_rel, encode_finArrow, List.ofFn_get]
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.nrelL_primrec
Proof 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 r l =>
    if l.length = r.fst then Nat.pair 1 ((Nat.pair 0 ((2 * r.fst.pair) ((encode r.snd).pair (encode l)))).pair 0) + 1
    else 0
⊢ ∀ (a : (k : ℕ) × L.Rel k) (b : List (UTerm L μ)),
    (if b.length = a.fst then Nat.pair 1 ((Nat.pair 0 ((2 * a.fst.pair) ((encode a.snd).pair (encode b)))).pair 0) + 1
      else 0) =
      encode (nrelL a b)
Tactic:
rintro ⟨k, r⟩ l
Proof state after:
case mk
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 r l =>
    if l.length = r.fst then Nat.pair 1 ((Nat.pair 0 ((2 * r.fst.pair) ((encode r.snd).pair (encode l)))).pair 0) + 1
    else 0
k : ℕ
r : L.Rel k
l : List (UTerm L μ)
⊢ (if l.length = ⟨k, r⟩.fst then
      Nat.pair 1 ((Nat.pair 0 ((2 * ⟨k, r⟩.fst.pair) ((encode ⟨k, r⟩.snd).pair (encode l)))).pair 0) + 1
    else 0) =
    encode (nrelL ⟨k, r⟩ l)
Theorem: LO.FirstOrder.UFormula.nrelL_primrec
Proof state before:
case mk
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 r l =>
    if l.length = r.fst then Nat.pair 1 ((Nat.pair 0 ((2 * r.fst.pair) ((encode r.snd).pair (encode l)))).pair 0) + 1
    else 0
k : ℕ
r : L.Rel k
l : List (UTerm L μ)
⊢ (if l.length = ⟨k, r⟩.fst then
      Nat.pair 1 ((Nat.pair 0 ((2 * ⟨k, r⟩.fst.pair) ((encode ⟨k, r⟩.snd).pair (encode l)))).pair 0) + 1
    else 0) =
    encode (nrelL ⟨k, r⟩ l)
Tactic:
by_cases hl : l.length = k <;> simp[hl, nrelL, primcodable, Primcodable.ofEquiv_toEncodable]
Proof state after:
case pos
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 r l =>
    if l.length = r.fst then Nat.pair 1 ((Nat.pair 0 ((2 * r.fst.pair) ((encode r.snd).pair (encode l)))).pair 0) + 1
    else 0
k : ℕ
r : L.Rel k
l : List (UTerm L μ)
hl : l.length = k
⊢ Nat.pair 1 ((Nat.pair 0 (2 * k.pair ((encode r).pair (encode l)))).pair 0) =
    encode (nrel r fun i => l.get (Fin.cast ⋯ i))
Theorem: LO.FirstOrder.UFormula.nrelL_primrec
Proof state before:
case pos
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 r l =>
    if l.length = r.fst then Nat.pair 1 ((Nat.pair 0 ((2 * r.fst.pair) ((encode r.snd).pair (encode l)))).pair 0) + 1
    else 0
k : ℕ
r : L.Rel k
l : List (UTerm L μ)
hl : l.length = k
⊢ Nat.pair 1 ((Nat.pair 0 (2 * k.pair ((encode r).pair (encode l)))).pair 0) =
    encode (nrel r fun i => l.get (Fin.cast ⋯ i))
Tactic:
{ rcases hl with rfl
  simp[encode_nrel, encode_finArrow, List.ofFn_get] }
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.nrelL_primrec
Proof state before:
case pos
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 r l =>
    if l.length = r.fst then Nat.pair 1 ((Nat.pair 0 ((2 * r.fst.pair) ((encode r.snd).pair (encode l)))).pair 0) + 1
    else 0
k : ℕ
r : L.Rel k
l : List (UTerm L μ)
hl : l.length = k
⊢ Nat.pair 1 ((Nat.pair 0 (2 * k.pair ((encode r).pair (encode l)))).pair 0) =
    encode (nrel r fun i => l.get (Fin.cast ⋯ i))
Tactic:
rcases hl with rfl
Proof state after:
case pos
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 r l =>
    if l.length = r.fst then Nat.pair 1 ((Nat.pair 0 ((2 * r.fst.pair) ((encode r.snd).pair (encode l)))).pair 0) + 1
    else 0
l : List (UTerm L μ)
r : L.Rel l.length
⊢ Nat.pair 1 ((Nat.pair 0 (2 * l.length.pair ((encode r).pair (encode l)))).pair 0) =
    encode (nrel r fun i => l.get (Fin.cast ⋯ i))
Theorem: LO.FirstOrder.UFormula.nrelL_primrec
Proof state before:
case pos
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 r l =>
    if l.length = r.fst then Nat.pair 1 ((Nat.pair 0 ((2 * r.fst.pair) ((encode r.snd).pair (encode l)))).pair 0) + 1
    else 0
l : List (UTerm L μ)
r : L.Rel l.length
⊢ Nat.pair 1 ((Nat.pair 0 (2 * l.length.pair ((encode r).pair (encode l)))).pair 0) =
    encode (nrel r fun i => l.get (Fin.cast ⋯ i))
Tactic:
simp[encode_nrel, encode_finArrow, List.ofFn_get]
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.and_primrec
Proof 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 _)
Proof 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
Theorem: LO.FirstOrder.UFormula.and_primrec
Proof 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))
Proof 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
Theorem: LO.FirstOrder.UFormula.and_primrec
Proof 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)
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.and_primrec
Proof 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 ⟨⟩
Proof 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
Theorem: LO.FirstOrder.UFormula.and_primrec
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.and_primrec
Proof 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
Proof 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
Theorem: LO.FirstOrder.UFormula.and_primrec
Proof 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]
Proof 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
Theorem: LO.FirstOrder.UFormula.and_primrec
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.or_primrec
Proof 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₂ or
Tactic:
have := w_mk₂ (β := Edge L μ) (fun (_ : Unit) => (false, Sum.inr $ Sum.inr $ Sum.inl ())) (by rintro ⟨⟩; simp[Edge]) (const _)
Proof 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 => (false, Sum.inr (Sum.inr (Sum.inl ())))) x) ((fintypeArrowEquivFinArrow' ⋯).symm ![w.1, w.2])
⊢ Primrec₂ or
Theorem: LO.FirstOrder.UFormula.or_primrec
Proof 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 => (false, Sum.inr (Sum.inr (Sum.inl ())))) x) ((fintypeArrowEquivFinArrow' ⋯).symm ![w.1, w.2])
⊢ Primrec₂ or
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))
Proof 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 => (false, 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 => (false, 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₂ or
Theorem: LO.FirstOrder.UFormula.or_primrec
Proof 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 => (false, 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 => (false, 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₂ or
Tactic:
exact this.of_eq (fun p q => by simp; rw [fintypeEquivFin_false, fintypeEquivFin_true]; simp)
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.or_primrec
Proof 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 => (false, Sum.inr (Sum.inr (Sum.inl ())))) x)) = 2
Tactic:
rintro ⟨⟩
Proof 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 => (false, Sum.inr (Sum.inr (Sum.inl ())))) PUnit.unit)) = 2
Theorem: LO.FirstOrder.UFormula.or_primrec
Proof 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 => (false, Sum.inr (Sum.inr (Sum.inl ())))) PUnit.unit)) = 2
Tactic:
simp[Edge]
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.or_primrec
Proof 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 => (false, 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 => (false, 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 => (false, 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.or q
Tactic:
simp
Proof 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 => (false, 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 => (false, 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