internlm/Lean-Github huggingface dataset:
Theorem: Primrec.w_elimvL_param
Proof state before:
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁸ : Primcodable τ
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
inst✝ : Inhabited (WType β)
fs : τ → α × σ → σ
fγ : τ → σ × α × List γ → γ
g : τ → σ
w : τ → WType β
hfs : Primrec₂ fs
hfγ : Primrec₂ fγ
hg✝ : Primrec g
hw : Primrec w
hm : Primrec fun p => p.2.2.depth
hl : Primrec fun p => List.map (fun w => (p.1, fs p.1 (p.2.2.inversion.1, p.2.1), w)) p.2.2.inversion.2
hg : Primrec₂ fun p l => fγ p.1 (p.2.1, p.2.2.inversion.1, l)
⊢ ∀ (b b' : τ × σ × WType β),
    b' ∈ List.map (fun w => (b.1, fs b.1 (b.2.2.inversion.1, b.2.1), w)) b.2.2.inversion.2 → b'.2.2.depth < b.2.2.depth
Tactic:
rintro ⟨z, x, ⟨a, f⟩⟩ ⟨z', x', w'⟩
Proof state after:
case mk.mk.mk.mk.mk
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁸ : Primcodable τ
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
inst✝ : Inhabited (WType β)
fs : τ → α × σ → σ
fγ : τ → σ × α × List γ → γ
g : τ → σ
w : τ → WType β
hfs : Primrec₂ fs
hfγ : Primrec₂ fγ
hg✝ : Primrec g
hw : Primrec w
hm : Primrec fun p => p.2.2.depth
hl : Primrec fun p => List.map (fun w => (p.1, fs p.1 (p.2.2.inversion.1, p.2.1), w)) p.2.2.inversion.2
hg : Primrec₂ fun p l => fγ p.1 (p.2.1, p.2.2.inversion.1, l)
z : τ
x : σ
a : α
f : β a → WType β
z' : τ
x' : σ
w' : WType β
⊢ (z', x', w') ∈
      List.map
        (fun w =>
          ((z, x, WType.mk a f).1,
            fs (z, x, WType.mk a f).1 ((z, x, WType.mk a f).2.2.inversion.1, (z, x, WType.mk a f).2.1), w))
        (z, x, WType.mk a f).2.2.inversion.2 →
    (z', x', w').2.2.depth < (z, x, WType.mk a f).2.2.depth
Theorem: Primrec.w_elimvL_param
Proof state before:
case mk.mk.mk.mk.mk
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁸ : Primcodable τ
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
inst✝ : Inhabited (WType β)
fs : τ → α × σ → σ
fγ : τ → σ × α × List γ → γ
g : τ → σ
w : τ → WType β
hfs : Primrec₂ fs
hfγ : Primrec₂ fγ
hg✝ : Primrec g
hw : Primrec w
hm : Primrec fun p => p.2.2.depth
hl : Primrec fun p => List.map (fun w => (p.1, fs p.1 (p.2.2.inversion.1, p.2.1), w)) p.2.2.inversion.2
hg : Primrec₂ fun p l => fγ p.1 (p.2.1, p.2.2.inversion.1, l)
z : τ
x : σ
a : α
f : β a → WType β
z' : τ
x' : σ
w' : WType β
⊢ (z', x', w') ∈
      List.map
        (fun w =>
          ((z, x, WType.mk a f).1,
            fs (z, x, WType.mk a f).1 ((z, x, WType.mk a f).2.2.inversion.1, (z, x, WType.mk a f).2.1), w))
        (z, x, WType.mk a f).2.2.inversion.2 →
    (z', x', w').2.2.depth < (z, x, WType.mk a f).2.2.depth
Tactic:
simp[inversion, Function.comp, List.mem_ofFn]
Proof state after:
case mk.mk.mk.mk.mk
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁸ : Primcodable τ
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
inst✝ : Inhabited (WType β)
fs : τ → α × σ → σ
fγ : τ → σ × α × List γ → γ
g : τ → σ
w : τ → WType β
hfs : Primrec₂ fs
hfγ : Primrec₂ fγ
hg✝ : Primrec g
hw : Primrec w
hm : Primrec fun p => p.2.2.depth
hl : Primrec fun p => List.map (fun w => (p.1, fs p.1 (p.2.2.inversion.1, p.2.1), w)) p.2.2.inversion.2
hg : Primrec₂ fun p l => fγ p.1 (p.2.1, p.2.2.inversion.1, l)
z : τ
x : σ
a : α
f : β a → WType β
z' : τ
x' : σ
w' : WType β
⊢ z = z' →
    fs z (a, x) = x' →
      ∀ (x : Fin (Fintype.card (β a))), f (fintypeEquivFin.symm x) = w' → w'.depth < (WType.mk a f).depth
Theorem: Primrec.w_elimvL_param
Proof state before:
case mk.mk.mk.mk.mk
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁸ : Primcodable τ
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
inst✝ : Inhabited (WType β)
fs : τ → α × σ → σ
fγ : τ → σ × α × List γ → γ
g : τ → σ
w : τ → WType β
hfs : Primrec₂ fs
hfγ : Primrec₂ fγ
hg✝ : Primrec g
hw : Primrec w
hm : Primrec fun p => p.2.2.depth
hl : Primrec fun p => List.map (fun w => (p.1, fs p.1 (p.2.2.inversion.1, p.2.1), w)) p.2.2.inversion.2
hg : Primrec₂ fun p l => fγ p.1 (p.2.1, p.2.2.inversion.1, l)
z : τ
x : σ
a : α
f : β a → WType β
z' : τ
x' : σ
w' : WType β
⊢ z = z' →
    fs z (a, x) = x' →
      ∀ (x : Fin (Fintype.card (β a))), f (fintypeEquivFin.symm x) = w' → w'.depth < (WType.mk a f).depth
Tactic:
rintro rfl rfl i rfl
Proof state after:
case mk.mk.mk.mk.mk
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁸ : Primcodable τ
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
inst✝ : Inhabited (WType β)
fs : τ → α × σ → σ
fγ : τ → σ × α × List γ → γ
g : τ → σ
w : τ → WType β
hfs : Primrec₂ fs
hfγ : Primrec₂ fγ
hg✝ : Primrec g
hw : Primrec w
hm : Primrec fun p => p.2.2.depth
hl : Primrec fun p => List.map (fun w => (p.1, fs p.1 (p.2.2.inversion.1, p.2.1), w)) p.2.2.inversion.2
hg : Primrec₂ fun p l => fγ p.1 (p.2.1, p.2.2.inversion.1, l)
z : τ
x : σ
a : α
f : β a → WType β
i : Fin (Fintype.card (β a))
⊢ (f (fintypeEquivFin.symm i)).depth < (WType.mk a f).depth
Theorem: Primrec.w_elimvL_param
Proof state before:
case mk.mk.mk.mk.mk
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁸ : Primcodable τ
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
inst✝ : Inhabited (WType β)
fs : τ → α × σ → σ
fγ : τ → σ × α × List γ → γ
g : τ → σ
w : τ → WType β
hfs : Primrec₂ fs
hfγ : Primrec₂ fγ
hg✝ : Primrec g
hw : Primrec w
hm : Primrec fun p => p.2.2.depth
hl : Primrec fun p => List.map (fun w => (p.1, fs p.1 (p.2.2.inversion.1, p.2.1), w)) p.2.2.inversion.2
hg : Primrec₂ fun p l => fγ p.1 (p.2.1, p.2.2.inversion.1, l)
z : τ
x : σ
a : α
f : β a → WType β
i : Fin (Fintype.card (β a))
⊢ (f (fintypeEquivFin.symm i)).depth < (WType.mk a f).depth
Tactic:
exact depth_lt_depth_mk _ _ _
Proof state after:
no goals
Theorem: Primrec.w_elimvL_param
Proof state before:
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁸ : Primcodable τ
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
inst✝ : Inhabited (WType β)
fs : τ → α × σ → σ
fγ : τ → σ × α × List γ → γ
g : τ → σ
w : τ → WType β
hfs : Primrec₂ fs
hfγ : Primrec₂ fγ
hg✝ : Primrec g
hw : Primrec w
hm : Primrec fun p => p.2.2.depth
hl : Primrec fun p => List.map (fun w => (p.1, fs p.1 (p.2.2.inversion.1, p.2.1), w)) p.2.2.inversion.2
hg : Primrec₂ fun p l => fγ p.1 (p.2.1, p.2.2.inversion.1, l)
⊢ ∀ (b : τ × σ × WType β),
    some
        (fγ b.1
          (b.2.1, b.2.2.inversion.1,
            List.map (fun p => elimvL (fun a x => fs p.1 (a, x)) (fun x a l => fγ p.1 (x, a, l)) p.2.1 p.2.2)
              (List.map (fun w => (b.1, fs b.1 (b.2.2.inversion.1, b.2.1), w)) b.2.2.inversion.2))) =
      some (elimvL (fun a x => fs b.1 (a, x)) (fun x a l => fγ b.1 (x, a, l)) b.2.1 b.2.2)
Tactic:
rintro ⟨z, x, ⟨a, f⟩⟩
Proof state after:
case mk.mk.mk
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁸ : Primcodable τ
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
inst✝ : Inhabited (WType β)
fs : τ → α × σ → σ
fγ : τ → σ × α × List γ → γ
g : τ → σ
w : τ → WType β
hfs : Primrec₂ fs
hfγ : Primrec₂ fγ
hg✝ : Primrec g
hw : Primrec w
hm : Primrec fun p => p.2.2.depth
hl : Primrec fun p => List.map (fun w => (p.1, fs p.1 (p.2.2.inversion.1, p.2.1), w)) p.2.2.inversion.2
hg : Primrec₂ fun p l => fγ p.1 (p.2.1, p.2.2.inversion.1, l)
z : τ
x : σ
a : α
f : β a → WType β
⊢ some
      (fγ (z, x, WType.mk a f).1
        ((z, x, WType.mk a f).2.1, (z, x, WType.mk a f).2.2.inversion.1,
          List.map (fun p => elimvL (fun a x => fs p.1 (a, x)) (fun x a l => fγ p.1 (x, a, l)) p.2.1 p.2.2)
            (List.map
              (fun w =>
                ((z, x, WType.mk a f).1,
                  fs (z, x, WType.mk a f).1 ((z, x, WType.mk a f).2.2.inversion.1, (z, x, WType.mk a f).2.1), w))
              (z, x, WType.mk a f).2.2.inversion.2))) =
    some
      (elimvL (fun a_1 x_1 => fs (z, x, WType.mk a f).1 (a_1, x_1))
        (fun x_1 a_1 l => fγ (z, x, WType.mk a f).1 (x_1, a_1, l)) (z, x, WType.mk a f).2.1 (z, x, WType.mk a f).2.2)
Theorem: Primrec.w_elimvL_param
Proof state before:
case mk.mk.mk
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁸ : Primcodable τ
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
inst✝ : Inhabited (WType β)
fs : τ → α × σ → σ
fγ : τ → σ × α × List γ → γ
g : τ → σ
w : τ → WType β
hfs : Primrec₂ fs
hfγ : Primrec₂ fγ
hg✝ : Primrec g
hw : Primrec w
hm : Primrec fun p => p.2.2.depth
hl : Primrec fun p => List.map (fun w => (p.1, fs p.1 (p.2.2.inversion.1, p.2.1), w)) p.2.2.inversion.2
hg : Primrec₂ fun p l => fγ p.1 (p.2.1, p.2.2.inversion.1, l)
z : τ
x : σ
a : α
f : β a → WType β
⊢ some
      (fγ (z, x, WType.mk a f).1
        ((z, x, WType.mk a f).2.1, (z, x, WType.mk a f).2.2.inversion.1,
          List.map (fun p => elimvL (fun a x => fs p.1 (a, x)) (fun x a l => fγ p.1 (x, a, l)) p.2.1 p.2.2)
            (List.map
              (fun w =>
                ((z, x, WType.mk a f).1,
                  fs (z, x, WType.mk a f).1 ((z, x, WType.mk a f).2.2.inversion.1, (z, x, WType.mk a f).2.1), w))
              (z, x, WType.mk a f).2.2.inversion.2))) =
    some
      (elimvL (fun a_1 x_1 => fs (z, x, WType.mk a f).1 (a_1, x_1))
        (fun x_1 a_1 l => fγ (z, x, WType.mk a f).1 (x_1, a_1, l)) (z, x, WType.mk a f).2.1 (z, x, WType.mk a f).2.2)
Tactic:
simp[inversion, Function.comp, elimvL_mk]
Proof state after:
case mk.mk.mk
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁸ : Primcodable τ
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
inst✝ : Inhabited (WType β)
fs : τ → α × σ → σ
fγ : τ → σ × α × List γ → γ
g : τ → σ
w : τ → WType β
hfs : Primrec₂ fs
hfγ : Primrec₂ fγ
hg✝ : Primrec g
hw : Primrec w
hm : Primrec fun p => p.2.2.depth
hl : Primrec fun p => List.map (fun w => (p.1, fs p.1 (p.2.2.inversion.1, p.2.1), w)) p.2.2.inversion.2
hg : Primrec₂ fun p l => fγ p.1 (p.2.1, p.2.2.inversion.1, l)
z : τ
x : σ
a : α
f : β a → WType β
⊢ fγ z
      (x, a,
        List.ofFn fun x_1 =>
          elimvL (fun a x => fs z (a, x)) (fun x a l => fγ z (x, a, l)) (fs z (a, x)) (f (fintypeEquivFin.symm x_1))) =
    fγ z
      (x, a,
        List.ofFn
          (fintypeArrowEquivFinArrow fun b =>
            elimvL (fun a x => fs z (a, x)) (fun x a l => fγ z (x, a, l)) (fs z (a, x)) (f b)))
Theorem: Primrec.w_elimvL_param
Proof state before:
case mk.mk.mk
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁸ : Primcodable τ
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
inst✝ : Inhabited (WType β)
fs : τ → α × σ → σ
fγ : τ → σ × α × List γ → γ
g : τ → σ
w : τ → WType β
hfs : Primrec₂ fs
hfγ : Primrec₂ fγ
hg✝ : Primrec g
hw : Primrec w
hm : Primrec fun p => p.2.2.depth
hl : Primrec fun p => List.map (fun w => (p.1, fs p.1 (p.2.2.inversion.1, p.2.1), w)) p.2.2.inversion.2
hg : Primrec₂ fun p l => fγ p.1 (p.2.1, p.2.2.inversion.1, l)
z : τ
x : σ
a : α
f : β a → WType β
⊢ fγ z
      (x, a,
        List.ofFn fun x_1 =>
          elimvL (fun a x => fs z (a, x)) (fun x a l => fγ z (x, a, l)) (fs z (a, x)) (f (fintypeEquivFin.symm x_1))) =
    fγ z
      (x, a,
        List.ofFn
          (fintypeArrowEquivFinArrow fun b =>
            elimvL (fun a x => fs z (a, x)) (fun x a l => fγ z (x, a, l)) (fs z (a, x)) (f b)))
Tactic:
congr
Proof state after:
no goals
Theorem: Primrec.w_elimvL
Proof state before:
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁸ : Primcodable τ
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
inst✝ : Inhabited (WType β)
fs : α → σ → σ
fγ : σ → α × List γ → γ
hfs : Primrec₂ fs
hfγ : Primrec₂ fγ
⊢ Primrec fun p => elimvL fs (fun x a l => fγ x (a, l)) p.1 p.2
Tactic:
have hfs : Primrec₂ (fun _ p => fs p.1 p.2 : σ × WType β → α × σ → σ) :=
  hfs.comp₂ (fst.comp₂ Primrec₂.right) (snd.comp₂ Primrec₂.right)
Proof state after:
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁸ : Primcodable τ
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
inst✝ : Inhabited (WType β)
fs : α → σ → σ
fγ : σ → α × List γ → γ
hfs✝ : Primrec₂ fs
hfγ : Primrec₂ fγ
hfs : Primrec₂ fun x p => fs p.1 p.2
⊢ Primrec fun p => elimvL fs (fun x a l => fγ x (a, l)) p.1 p.2
Theorem: Primrec.w_elimvL
Proof state before:
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁸ : Primcodable τ
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
inst✝ : Inhabited (WType β)
fs : α → σ → σ
fγ : σ → α × List γ → γ
hfs✝ : Primrec₂ fs
hfγ : Primrec₂ fγ
hfs : Primrec₂ fun x p => fs p.1 p.2
⊢ Primrec fun p => elimvL fs (fun x a l => fγ x (a, l)) p.1 p.2
Tactic:
have hfγ : Primrec₂ (fun _ p => fγ p.1 p.2 : σ × WType β → σ × α × List γ → γ) :=
  hfγ.comp₂ (fst.comp₂ Primrec₂.right) (snd.comp₂ Primrec₂.right)
Proof state after:
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁸ : Primcodable τ
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
inst✝ : Inhabited (WType β)
fs : α → σ → σ
fγ : σ → α × List γ → γ
hfs✝ : Primrec₂ fs
hfγ✝ : Primrec₂ fγ
hfs : Primrec₂ fun x p => fs p.1 p.2
hfγ : Primrec₂ fun x p => fγ p.1 p.2
⊢ Primrec fun p => elimvL fs (fun x a l => fγ x (a, l)) p.1 p.2
Theorem: Primrec.w_elimvL
Proof state before:
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁸ : Primcodable τ
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
inst✝ : Inhabited (WType β)
fs : α → σ → σ
fγ : σ → α × List γ → γ
hfs✝ : Primrec₂ fs
hfγ✝ : Primrec₂ fγ
hfs : Primrec₂ fun x p => fs p.1 p.2
hfγ : Primrec₂ fun x p => fγ p.1 p.2
⊢ Primrec fun p => elimvL fs (fun x a l => fγ x (a, l)) p.1 p.2
Tactic:
exact w_elimvL_param hfs hfγ fst snd
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.and_inj
Proof state before:
α : Type u_1
p₁ q₁ p₂ q₂ : Formula α
⊢ p₁ ⋏ p₂ = q₁ ⋏ q₂ ↔ p₁ = q₁ ∧ p₂ = q₂
Tactic:
simp[Wedge.wedge]
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.or_inj
Proof state before:
α : Type u_1
p₁ q₁ p₂ q₂ : Formula α
⊢ p₁ ⋎ p₂ = q₁ ⋎ q₂ ↔ p₁ = q₁ ∧ p₂ = q₂
Tactic:
simp[Vee.vee]
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.imp_inj
Proof state before:
α : Type u_1
p₁ q₁ p₂ q₂ : Formula α
⊢ p₁ ⟶ p₂ = q₁ ⟶ q₂ ↔ p₁ = q₁ ∧ p₂ = q₂
Tactic:
simp[Arrow.arrow]
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.neg_inj
Proof state before:
α : Type u_1
p q : Formula α
⊢ ~p = ~q ↔ p = q
Tactic:
simp[Tilde.tilde]
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.iff_def
Proof state before:
α : Type u_1
p q : Formula α
⊢ p ⟷ q = (p ⟶ q) ⋏ (q ⟶ p)
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.toW_ofW
Proof state before:
α : Type u_1
a : α
f✝ : Edge α (Sum.inl a) → WType (Edge α)
⊢ (ofW (WType.mk (Sum.inl a) f✝)).toW = WType.mk (Sum.inl a) f✝
Tactic:
simp [ofW, toW, Empty.eq_elim]
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.toW_ofW
Proof state before:
α : Type u_1
f✝ : Edge α (Sum.inr (Sum.inl true)) → WType (Edge α)
⊢ (ofW (WType.mk (Sum.inr (Sum.inl true)) f✝)).toW = WType.mk (Sum.inr (Sum.inl true)) f✝
Tactic:
simp [ofW, toW, Empty.eq_elim]
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.toW_ofW
Proof state before:
α : Type u_1
f✝ : Edge α (Sum.inr (Sum.inl false)) → WType (Edge α)
⊢ (ofW (WType.mk (Sum.inr (Sum.inl false)) f✝)).toW = WType.mk (Sum.inr (Sum.inl false)) f✝
Tactic:
simp [ofW, toW, Empty.eq_elim]
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.toW_ofW
Proof state before:
α : Type u_1
isLt✝ : 0 < 3
w : Edge α (Sum.inr (Sum.inr ⟨0, isLt✝⟩)) → WType (Edge α)
⊢ (ofW (WType.mk (Sum.inr (Sum.inr ⟨0, isLt✝⟩)) w)).toW = WType.mk (Sum.inr (Sum.inr ⟨0, isLt✝⟩)) w
Tactic:
simp [ofW, toW, toW_ofW (w false), toW_ofW (w true)]
Proof state after:
α : Type u_1
isLt✝ : 0 < 3
w : Edge α (Sum.inr (Sum.inr ⟨0, isLt✝⟩)) → WType (Edge α)
⊢ (fun t => Bool.rec (w false) (w true) t) = w
Theorem: LO.Propositional.Superintuitionistic.Formula.toW_ofW
Proof state before:
α : Type u_1
isLt✝ : 0 < 3
w : Edge α (Sum.inr (Sum.inr ⟨0, isLt✝⟩)) → WType (Edge α)
⊢ (fun t => Bool.rec (w false) (w true) t) = w
Tactic:
ext b
Proof state after:
case h
α : Type u_1
isLt✝ : 0 < 3
w : Edge α (Sum.inr (Sum.inr ⟨0, isLt✝⟩)) → WType (Edge α)
b : Bool
⊢ Bool.rec (w false) (w true) b = w b
Theorem: LO.Propositional.Superintuitionistic.Formula.toW_ofW
Proof state before:
case h
α : Type u_1
isLt✝ : 0 < 3
w : Edge α (Sum.inr (Sum.inr ⟨0, isLt✝⟩)) → WType (Edge α)
b : Bool
⊢ Bool.rec (w false) (w true) b = w b
Tactic:
cases b <;> simp
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.toW_ofW
Proof state before:
α : Type u_1
isLt✝ : 1 < 3
w : Edge α (Sum.inr (Sum.inr ⟨1, isLt✝⟩)) → WType (Edge α)
⊢ (ofW (WType.mk (Sum.inr (Sum.inr ⟨1, isLt✝⟩)) w)).toW = WType.mk (Sum.inr (Sum.inr ⟨1, isLt✝⟩)) w
Tactic:
simp [ofW, toW, toW_ofW (w false), toW_ofW (w true)]
Proof state after:
α : Type u_1
isLt✝ : 1 < 3
w : Edge α (Sum.inr (Sum.inr ⟨1, isLt✝⟩)) → WType (Edge α)
⊢ (fun t => Bool.rec (w false) (w true) t) = w
Theorem: LO.Propositional.Superintuitionistic.Formula.toW_ofW
Proof state before:
α : Type u_1
isLt✝ : 1 < 3
w : Edge α (Sum.inr (Sum.inr ⟨1, isLt✝⟩)) → WType (Edge α)
⊢ (fun t => Bool.rec (w false) (w true) t) = w
Tactic:
ext b
Proof state after:
case h
α : Type u_1
isLt✝ : 1 < 3
w : Edge α (Sum.inr (Sum.inr ⟨1, isLt✝⟩)) → WType (Edge α)
b : Bool
⊢ Bool.rec (w false) (w true) b = w b
Theorem: LO.Propositional.Superintuitionistic.Formula.toW_ofW
Proof state before:
case h
α : Type u_1
isLt✝ : 1 < 3
w : Edge α (Sum.inr (Sum.inr ⟨1, isLt✝⟩)) → WType (Edge α)
b : Bool
⊢ Bool.rec (w false) (w true) b = w b
Tactic:
cases b <;> simp
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.toW_ofW
Proof state before:
α : Type u_1
isLt✝ : 2 < 3
w : Edge α (Sum.inr (Sum.inr ⟨2, isLt✝⟩)) → WType (Edge α)
⊢ (ofW (WType.mk (Sum.inr (Sum.inr ⟨2, isLt✝⟩)) w)).toW = WType.mk (Sum.inr (Sum.inr ⟨2, isLt✝⟩)) w
Tactic:
simp [ofW, toW, toW_ofW (w false), toW_ofW (w true)]
Proof state after:
α : Type u_1
isLt✝ : 2 < 3
w : Edge α (Sum.inr (Sum.inr ⟨2, isLt✝⟩)) → WType (Edge α)
⊢ (fun t => Bool.rec (w false) (w true) t) = w
Theorem: LO.Propositional.Superintuitionistic.Formula.toW_ofW
Proof state before:
α : Type u_1
isLt✝ : 2 < 3
w : Edge α (Sum.inr (Sum.inr ⟨2, isLt✝⟩)) → WType (Edge α)
⊢ (fun t => Bool.rec (w false) (w true) t) = w
Tactic:
ext b
Proof state after:
case h
α : Type u_1
isLt✝ : 2 < 3
w : Edge α (Sum.inr (Sum.inr ⟨2, isLt✝⟩)) → WType (Edge α)
b : Bool
⊢ Bool.rec (w false) (w true) b = w b
Theorem: LO.Propositional.Superintuitionistic.Formula.toW_ofW
Proof state before:
case h
α : Type u_1
isLt✝ : 2 < 3
w : Edge α (Sum.inr (Sum.inr ⟨2, isLt✝⟩)) → WType (Edge α)
b : Bool
⊢ Bool.rec (w false) (w true) b = w b
Tactic:
cases b <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.func0
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
f : L.Func 0
v : Fin 0 → Semiterm L ξ₁ n₁
⊢ ω (func f v) = func f ![]
Tactic:
simp[Rew.func, Matrix.empty_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.func1
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
f : L.Func 1
t : Semiterm L ξ₁ n₁
⊢ ω (func f ![t]) = func f ![ω t]
Tactic:
simp[Matrix.constant_eq_singleton, Rew.func]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.func2
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
f : L.Func 2
t₁ t₂ : Semiterm L ξ₁ n₁
⊢ ω (func f ![t₁, t₂]) = func f ![ω t₁, ω t₂]
Tactic:
simp[Rew.func]
Proof state after:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
f : L.Func 2
t₁ t₂ : Semiterm L ξ₁ n₁
⊢ (fun i => ω (![t₁, t₂] i)) = ![ω t₁, ω t₂]
Theorem: LO.FirstOrder.Rew.func2
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
f : L.Func 2
t₁ t₂ : Semiterm L ξ₁ n₁
⊢ (fun i => ω (![t₁, t₂] i)) = ![ω t₁, ω t₂]
Tactic:
funext i
Proof state after:
case h
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
f : L.Func 2
t₁ t₂ : Semiterm L ξ₁ n₁
i : Fin 2
⊢ ω (![t₁, t₂] i) = ![ω t₁, ω t₂] i
Theorem: LO.FirstOrder.Rew.func2
Proof state before:
case h
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
f : L.Func 2
t₁ t₂ : Semiterm L ξ₁ n₁
i : Fin 2
⊢ ω (![t₁, t₂] i) = ![ω t₁, ω t₂] i
Tactic:
induction i using Fin.induction <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.func3
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
f : L.Func 3
t₁ t₂ t₃ : Semiterm L ξ₁ n₁
⊢ ω (func f ![t₁, t₂, t₃]) = func f ![ω t₁, ω t₂, ω t₃]
Tactic:
simp[Rew.func]
Proof state after:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
f : L.Func 3
t₁ t₂ t₃ : Semiterm L ξ₁ n₁
⊢ (fun i => ω (![t₁, t₂, t₃] i)) = ![ω t₁, ω t₂, ω t₃]