internlm/Lean-Github huggingface dataset:
Theorem: Primrec.finArrow_map
Proof 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 γ
f : α → σ
hf : Primrec f
k : ℕ
this :
  Primrec fun e => encode ((encodeDecode (Fin k → α) e).bind fun c => Option.map (fun l => List.map f l) (decode c))
e : ℕ
⊢ encode
      ((Option.map encode ((decode e).bind fun l => Option.map (⇑(Equiv.vectorEquivFin α k)) (List.toVector k l))).bind
        fun a => Option.map (fun l => List.map f l) (decode a)) =
    encode
      (Option.map (fun v i => f (v i))
        ((decode e).bind fun l => Option.map (⇑(Equiv.vectorEquivFin α k)) (List.toVector k l)))
Tactic:
rcases (decode e) with (_ | as) <;> simp [Function.comp]
Proof state after:
case some
σ : 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 γ
f : α → σ
hf : Primrec f
k : ℕ
this :
  Primrec fun e => encode ((encodeDecode (Fin k → α) e).bind fun c => Option.map (fun l => List.map f l) (decode c))
e : ℕ
as : List α
⊢ encode
      ((Option.map (fun x => encode ((Equiv.vectorEquivFin α k) x)) (List.toVector k as)).bind fun a =>
        Option.map (fun l => List.map f l) (decode a)) =
    encode (Option.map (fun x i => f ((Equiv.vectorEquivFin α k) x i)) (List.toVector k as))
Theorem: Primrec.finArrow_map
Proof state before:
case some
σ : 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 γ
f : α → σ
hf : Primrec f
k : ℕ
this :
  Primrec fun e => encode ((encodeDecode (Fin k → α) e).bind fun c => Option.map (fun l => List.map f l) (decode c))
e : ℕ
as : List α
⊢ encode
      ((Option.map (fun x => encode ((Equiv.vectorEquivFin α k) x)) (List.toVector k as)).bind fun a =>
        Option.map (fun l => List.map f l) (decode a)) =
    encode (Option.map (fun x i => f ((Equiv.vectorEquivFin α k) x i)) (List.toVector k as))
Tactic:
{ rcases (as.toVector k) with (_ | v) <;> simp
  { simp[encode_finArrow, Function.comp] } }
Proof state after:
no goals
Theorem: Primrec.finArrow_map
Proof state before:
case some
σ : 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 γ
f : α → σ
hf : Primrec f
k : ℕ
this :
  Primrec fun e => encode ((encodeDecode (Fin k → α) e).bind fun c => Option.map (fun l => List.map f l) (decode c))
e : ℕ
as : List α
⊢ encode
      ((Option.map (fun x => encode ((Equiv.vectorEquivFin α k) x)) (List.toVector k as)).bind fun a =>
        Option.map (fun l => List.map f l) (decode a)) =
    encode (Option.map (fun x i => f ((Equiv.vectorEquivFin α k) x i)) (List.toVector k as))
Tactic:
rcases (as.toVector k) with (_ | v) <;> simp
Proof state after:
case some.some
σ : 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 γ
f : α → σ
hf : Primrec f
k : ℕ
this :
  Primrec fun e => encode ((encodeDecode (Fin k → α) e).bind fun c => Option.map (fun l => List.map f l) (decode c))
e : ℕ
as : List α
v : Vector α k
⊢ encode (Option.map (fun l => List.map f l) (decode (encode ((Equiv.vectorEquivFin α k) v)))) =
    (encode fun i => f ((Equiv.vectorEquivFin α k) v i)) + 1
Theorem: Primrec.finArrow_map
Proof state before:
case some.some
σ : 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 γ
f : α → σ
hf : Primrec f
k : ℕ
this :
  Primrec fun e => encode ((encodeDecode (Fin k → α) e).bind fun c => Option.map (fun l => List.map f l) (decode c))
e : ℕ
as : List α
v : Vector α k
⊢ encode (Option.map (fun l => List.map f l) (decode (encode ((Equiv.vectorEquivFin α k) v)))) =
    (encode fun i => f ((Equiv.vectorEquivFin α k) v i)) + 1
Tactic:
{ simp[encode_finArrow, Function.comp] }
Proof state after:
no goals
Theorem: Primrec.finArrow_map
Proof state before:
case some.some
σ : 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 γ
f : α → σ
hf : Primrec f
k : ℕ
this :
  Primrec fun e => encode ((encodeDecode (Fin k → α) e).bind fun c => Option.map (fun l => List.map f l) (decode c))
e : ℕ
as : List α
v : Vector α k
⊢ encode (Option.map (fun l => List.map f l) (decode (encode ((Equiv.vectorEquivFin α k) v)))) =
    (encode fun i => f ((Equiv.vectorEquivFin α k) v i)) + 1
Tactic:
simp[encode_finArrow, Function.comp]
Proof state after:
no goals
Theorem: Primrec.finArrow_app
Proof 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 γ
n : ℕ
v : σ → Fin n → α
f : σ → Fin n
hv : Primrec v
hf : Primrec f
this : Primrec fun x => (List.ofFn (v x)).get? ↑(f x)
x : σ
⊢ (List.ofFn (v x)).get? ↑(f x) = some (v x (f x))
Tactic:
simp[List.ofFnNthVal]
Proof state after:
no goals
Theorem: Primrec.finite_change
Proof 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 γ
f : ℕ → α
hf : Primrec f
g : ℕ → α
h : ∃ m, ∀ x ≥ m, g x = f x
⊢ Primrec g
Tactic:
rcases h with ⟨m, h⟩
Proof state after:
case intro
σ : 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 γ
f : ℕ → α
hf : Primrec f
g : ℕ → α
m : ℕ
h : ∀ x ≥ m, g x = f x
⊢ Primrec g
Theorem: Primrec.finite_change
Proof state before:
case intro
σ : 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 γ
f : ℕ → α
hf : Primrec f
g : ℕ → α
m : ℕ
h : ∀ x ≥ m, g x = f x
⊢ Primrec g
Tactic:
induction' m with m ih generalizing g
Proof state after:
case intro.zero
σ : 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 γ
f : ℕ → α
hf : Primrec f
g : ℕ → α
h : ∀ x ≥ 0, g x = f x
⊢ Primrec g

case intro.succ
σ : 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 γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
⊢ Primrec g
Theorem: Primrec.finite_change
Proof state before:
case intro.zero
σ : 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 γ
f : ℕ → α
hf : Primrec f
g : ℕ → α
h : ∀ x ≥ 0, g x = f x
⊢ Primrec g
Tactic:
exact hf.of_eq <| by intro n; exact Eq.symm <| h n (Nat.zero_le n)
Proof state after:
no goals
Theorem: Primrec.finite_change
Proof 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 γ
f : ℕ → α
hf : Primrec f
g : ℕ → α
h : ∀ x ≥ 0, g x = f x
⊢ ∀ (n : ℕ), f n = g n
Tactic:
intro n
Proof 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 γ
f : ℕ → α
hf : Primrec f
g : ℕ → α
h : ∀ x ≥ 0, g x = f x
n : ℕ
⊢ f n = g n
Theorem: Primrec.finite_change
Proof 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 γ
f : ℕ → α
hf : Primrec f
g : ℕ → α
h : ∀ x ≥ 0, g x = f x
n : ℕ
⊢ f n = g n
Tactic:
exact Eq.symm <| h n (Nat.zero_le n)
Proof state after:
no goals
Theorem: Primrec.finite_change
Proof state before:
case intro.succ
σ : 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 γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
⊢ Primrec g
Tactic:
let g' : ℕ → α := fun x => if x < m then g x else f x
Proof state after:
case intro.succ
σ : 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 γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
⊢ Primrec g
Theorem: Primrec.finite_change
Proof state before:
case intro.succ
σ : 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 γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
⊢ Primrec g
Tactic:
have : Primrec g' :=
  ih g' (by simp [g']; intro x hx lt; exact (False.elim $ Nat.not_le.mpr lt hx))
Proof state after:
case intro.succ
σ : 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 γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
this : Primrec g'
⊢ Primrec g
Theorem: Primrec.finite_change
Proof state before:
case intro.succ
σ : 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 γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
this : Primrec g'
⊢ Primrec g
Tactic:
have : Primrec (fun x => if x = m then g m else g' x) :=
  Primrec.ite (Primrec.eq.comp Primrec.id (const m)) (const (g m)) this
Proof state after:
case intro.succ
σ : 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 γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
this✝ : Primrec g'
this : Primrec fun x => if x = m then g m else g' x
⊢ Primrec g
Theorem: Primrec.finite_change
Proof state before:
case intro.succ
σ : 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 γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
this✝ : Primrec g'
this : Primrec fun x => if x = m then g m else g' x
⊢ Primrec g
Tactic:
exact this.of_eq <| by
  intro x; simp [g']
  by_cases hx : x = m <;> simp[hx]
  intro hhx
  have : m < x := Ne.lt_of_le' hx hhx
  exact Eq.symm <| h x this
Proof state after:
no goals
Theorem: Primrec.finite_change
Proof 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 γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
⊢ ∀ x ≥ m, g' x = f x
Tactic:
simp [g']
Proof 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 γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
⊢ ∀ (x : ℕ), m ≤ x → x < m → g x = f x
Theorem: Primrec.finite_change
Proof 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 γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
⊢ ∀ (x : ℕ), m ≤ x → x < m → g x = f x
Tactic:
intro x hx lt
Proof 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 γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
x : ℕ
hx : m ≤ x
lt : x < m
⊢ g x = f x
Theorem: Primrec.finite_change
Proof 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 γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
x : ℕ
hx : m ≤ x
lt : x < m
⊢ g x = f x
Tactic:
exact (False.elim $ Nat.not_le.mpr lt hx)
Proof state after:
no goals
Theorem: Primrec.finite_change
Proof 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 γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
this✝ : Primrec g'
this : Primrec fun x => if x = m then g m else g' x
⊢ ∀ (n : ℕ), (if n = m then g m else g' n) = g n
Tactic:
intro x
Proof 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 γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
this✝ : Primrec g'
this : Primrec fun x => if x = m then g m else g' x
x : ℕ
⊢ (if x = m then g m else g' x) = g x
Theorem: Primrec.finite_change
Proof 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 γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
this✝ : Primrec g'
this : Primrec fun x => if x = m then g m else g' x
x : ℕ
⊢ (if x = m then g m else g' x) = g x
Tactic:
simp [g']
Proof 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 γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
this✝ : Primrec g'
this : Primrec fun x => if x = m then g m else g' x
x : ℕ
⊢ (if x = m then g m else if x < m then g x else f x) = g x
Theorem: Primrec.finite_change
Proof 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 γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
this✝ : Primrec g'
this : Primrec fun x => if x = m then g m else g' x
x : ℕ
⊢ (if x = m then g m else if x < m then g x else f x) = g x
Tactic:
by_cases hx : x = m <;> simp[hx]
Proof state after:
case neg
σ : 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 γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
this✝ : Primrec g'
this : Primrec fun x => if x = m then g m else g' x
x : ℕ
hx : ¬x = m
⊢ m ≤ x → f x = g x
Theorem: Primrec.finite_change
Proof state before:
case neg
σ : 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 γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
this✝ : Primrec g'
this : Primrec fun x => if x = m then g m else g' x
x : ℕ
hx : ¬x = m
⊢ m ≤ x → f x = g x
Tactic:
intro hhx
Proof state after:
case neg
σ : 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 γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
this✝ : Primrec g'
this : Primrec fun x => if x = m then g m else g' x
x : ℕ
hx : ¬x = m
hhx : m ≤ x
⊢ f x = g x
Theorem: Primrec.finite_change
Proof state before:
case neg
σ : 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 γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
this✝ : Primrec g'
this : Primrec fun x => if x = m then g m else g' x
x : ℕ
hx : ¬x = m
hhx : m ≤ x
⊢ f x = g x
Tactic:
have : m < x := Ne.lt_of_le' hx hhx
Proof state after:
case neg
σ : 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 γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
this✝¹ : Primrec g'
this✝ : Primrec fun x => if x = m then g m else g' x
x : ℕ
hx : ¬x = m
hhx : m ≤ x
this : m < x
⊢ f x = g x
Theorem: Primrec.finite_change
Proof state before:
case neg
σ : 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 γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
this✝¹ : Primrec g'
this✝ : Primrec fun x => if x = m then g m else g' x
x : ℕ
hx : ¬x = m
hhx : m ≤ x
this : m < x
⊢ f x = g x
Tactic:
exact Eq.symm <| h x this
Proof state after:
no goals
Theorem: Primrec.of_subtype_iff
Proof 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 γ
β : Type u_5
inst✝¹ : Primcodable β
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
f : β → { a // p a }
this : Primcodable (Subtype p) := Primcodable.subtype hp
hf : Primrec fun x => ↑(f x)
⊢ ∀ (n : β), encode ↑(f n) = encode (f n)
Tactic:
intro b
Proof 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 γ
β : Type u_5
inst✝¹ : Primcodable β
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
f : β → { a // p a }
this : Primcodable (Subtype p) := Primcodable.subtype hp
hf : Primrec fun x => ↑(f x)
b : β
⊢ encode ↑(f b) = encode (f b)