internlm/Lean-Github huggingface dataset:
Theorem: Encodable.toFinArrowOpt_eq_some_iff
Proof state before:
case h
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
g : ι → α
hf : ∀ (i : ι), f i = some (g i)
i : ι
⊢ (fintypeEquivFin.symm.arrowCongr (Equiv.refl α)) (fun i => g (fintypeEquivFin.symm i)) i = g i
Tactic:
simp
Proof state after:
no goals
Theorem: Encodable.vectorEquivFin_symm_val
Proof state before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
n : ℕ
β : Type u_2
f : Fin n → β
⊢ ((Equiv.vectorEquivFin β n).symm f).toList = List.ofFn f
Tactic:
ext i b
Proof state after:
case a.a
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
n : ℕ
β : Type u_2
f : Fin n → β
i : ℕ
b : β
⊢ b ∈ ((Equiv.vectorEquivFin β n).symm f).toList.get? i ↔ b ∈ (List.ofFn f).get? i
Theorem: Encodable.vectorEquivFin_symm_val
Proof state before:
case a.a
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
n : ℕ
β : Type u_2
f : Fin n → β
i : ℕ
b : β
⊢ b ∈ ((Equiv.vectorEquivFin β n).symm f).toList.get? i ↔ b ∈ (List.ofFn f).get? i
Tactic:
simp[Equiv.vectorEquivFin, Vector.ofFn]
Proof state after:
no goals
Theorem: Encodable.encodeDecode_of_none
Proof state before:
α : Type u_1
inst✝ : Encodable α
e : ℕ
h : decode e = none
⊢ encodeDecode α e = none
Tactic:
simp[encodeDecode, h]
Proof state after:
no goals
Theorem: Encodable.encodeDecode_of_some
Proof state before:
α : Type u_1
inst✝ : Encodable α
e : ℕ
a : α
h : decode e = some a
⊢ encodeDecode α e = some (encode a)
Tactic:
simp[encodeDecode, h]
Proof state after:
no goals
Theorem: Encodable.encodeDecode_eq_encode_map_decode
Proof state before:
α : Type u_1
inst✝ : Encodable α
e : ℕ
⊢ encodeDecode α e = Option.map encode (decode e)
Tactic:
simp[encodeDecode]
Proof state after:
α : Type u_1
inst✝ : Encodable α
e : ℕ
⊢ (encode (decode e)).predO = Option.map encode (decode e)
Theorem: Encodable.encodeDecode_eq_encode_map_decode
Proof state before:
α : Type u_1
inst✝ : Encodable α
e : ℕ
⊢ (encode (decode e)).predO = Option.map encode (decode e)
Tactic:
rcases (decode e) <;> simp
Proof state after:
no goals
Theorem: Encodable.decode_encodeDecode
Proof state before:
α : Type u_1
inst✝ : Encodable α
e i : ℕ
⊢ encodeDecode α e = some i → ∃ a, decode i = some a
Tactic:
simp[encodeDecode]
Proof state after:
α : Type u_1
inst✝ : Encodable α
e i : ℕ
⊢ (encode (decode e)).predO = some i → ∃ a, decode i = some a
Theorem: Encodable.decode_encodeDecode
Proof state before:
α : Type u_1
inst✝ : Encodable α
e i : ℕ
⊢ (encode (decode e)).predO = some i → ∃ a, decode i = some a
Tactic:
cases (decode e : Option α) <;> simp
Proof state after:
case some
α : Type u_1
inst✝ : Encodable α
e i : ℕ
val✝ : α
⊢ encode val✝ = i → ∃ a, decode i = some a
Theorem: Encodable.decode_encodeDecode
Proof state before:
case some
α : Type u_1
inst✝ : Encodable α
e i : ℕ
val✝ : α
⊢ encode val✝ = i → ∃ a, decode i = some a
Tactic:
rintro rfl
Proof state after:
case some
α : Type u_1
inst✝ : Encodable α
e : ℕ
val✝ : α
⊢ ∃ a, decode (encode val✝) = some a
Theorem: Encodable.decode_encodeDecode
Proof state before:
case some
α : Type u_1
inst✝ : Encodable α
e : ℕ
val✝ : α
⊢ ∃ a, decode (encode val✝) = some a
Tactic:
simp
Proof state after:
no goals
Theorem: Encodable.encode_decode_subtype
Proof state before:
α✝ : Type u_1
inst✝² : Encodable α✝
α : Type u_1
P : α → Prop
inst✝¹ : Encodable α
inst✝ : DecidablePred P
e : ℕ
⊢ encode (decode e) = encode ((decode e).bind fun a => if P a then some a else none)
Tactic:
rcases h : decode (α := α) e with (_ | s) <;> simp[*, decode, decodeSubtype, encode, encodeSubtype]
Proof state after:
case some
α✝ : Type u_1
inst✝² : Encodable α✝
α : Type u_1
P : α → Prop
inst✝¹ : Encodable α
inst✝ : DecidablePred P
e : ℕ
s : α
h : decode e = some s
⊢ Option.rec 0 (fun val => encode ↑val + 1) (if h : P s then some ⟨s, ⋯⟩ else none) =
    Option.rec 0 (fun val => encode val + 1) (if P s then some s else none)
Theorem: Encodable.encode_decode_subtype
Proof state before:
case some
α✝ : Type u_1
inst✝² : Encodable α✝
α : Type u_1
P : α → Prop
inst✝¹ : Encodable α
inst✝ : DecidablePred P
e : ℕ
s : α
h : decode e = some s
⊢ Option.rec 0 (fun val => encode ↑val + 1) (if h : P s then some ⟨s, ⋯⟩ else none) =
    Option.rec 0 (fun val => encode val + 1) (if P s then some s else none)
Tactic:
{ by_cases hs : P s <;> simp[hs] }
Proof state after:
no goals
Theorem: Encodable.encode_decode_subtype
Proof state before:
case some
α✝ : Type u_1
inst✝² : Encodable α✝
α : Type u_1
P : α → Prop
inst✝¹ : Encodable α
inst✝ : DecidablePred P
e : ℕ
s : α
h : decode e = some s
⊢ Option.rec 0 (fun val => encode ↑val + 1) (if h : P s then some ⟨s, ⋯⟩ else none) =
    Option.rec 0 (fun val => encode val + 1) (if P s then some s else none)
Tactic:
by_cases hs : P s <;> simp[hs]
Proof state after:
no goals
Theorem: Encodable.encodeDecode_subtype'
Proof state before:
α✝ : Type u_1
inst✝² : Encodable α✝
α : Type u_1
P : α → Prop
inst✝¹ : Encodable α
inst✝ : DecidablePred P
e : ℕ
⊢ encodeDecode { x // P x } e = (decode e).bind fun a => if P a then some (encode a) else none
Tactic:
simp[encodeDecode, encode_decode_subtype]
Proof state after:
α✝ : Type u_1
inst✝² : Encodable α✝
α : Type u_1
P : α → Prop
inst✝¹ : Encodable α
inst✝ : DecidablePred P
e : ℕ
⊢ (encode ((decode e).bind fun a => if P a then some a else none)).predO =
    (decode e).bind fun a => if P a then some (encode a) else none
Theorem: Encodable.encodeDecode_subtype'
Proof state before:
α✝ : Type u_1
inst✝² : Encodable α✝
α : Type u_1
P : α → Prop
inst✝¹ : Encodable α
inst✝ : DecidablePred P
e : ℕ
⊢ (encode ((decode e).bind fun a => if P a then some a else none)).predO =
    (decode e).bind fun a => if P a then some (encode a) else none
Tactic:
rcases (decode e : Option α) with (_ | a) <;> simp
Proof state after:
case some
α✝ : Type u_1
inst✝² : Encodable α✝
α : Type u_1
P : α → Prop
inst✝¹ : Encodable α
inst✝ : DecidablePred P
e : ℕ
a : α
⊢ (encode (if P a then some a else none)).predO = if P a then some (encode a) else none
Theorem: Encodable.encodeDecode_subtype'
Proof state before:
case some
α✝ : Type u_1
inst✝² : Encodable α✝
α : Type u_1
P : α → Prop
inst✝¹ : Encodable α
inst✝ : DecidablePred P
e : ℕ
a : α
⊢ (encode (if P a then some a else none)).predO = if P a then some (encode a) else none
Tactic:
{ by_cases ha : P a <;> simp[*] }
Proof state after:
no goals
Theorem: Encodable.encodeDecode_subtype'
Proof state before:
case some
α✝ : Type u_1
inst✝² : Encodable α✝
α : Type u_1
P : α → Prop
inst✝¹ : Encodable α
inst✝ : DecidablePred P
e : ℕ
a : α
⊢ (encode (if P a then some a else none)).predO = if P a then some (encode a) else none
Tactic:
by_cases ha : P a <;> simp[*]
Proof state after:
no goals
Theorem: Encodable.encodeDecode_subtype
Proof state before:
α✝ : Type u_1
inst✝² : Encodable α✝
α : Type u_1
P : α → Prop
inst✝¹ : Encodable α
inst✝ : DecidablePred P
e : ℕ
⊢ encodeDecode { x // P x } e = (encodeDecode α e).bind fun c => if ∃ a ∈ decode c, P a then some c else none
Tactic:
simp[encodeDecode_subtype', encodeDecode]
Proof state after:
α✝ : Type u_1
inst✝² : Encodable α✝
α : Type u_1
P : α → Prop
inst✝¹ : Encodable α
inst✝ : DecidablePred P
e : ℕ
⊢ ((decode e).bind fun a => if P a then some (encode a) else none) =
    (encode (decode e)).predO.bind fun a => if ∃ a_1, decode a = some a_1 ∧ P a_1 then some a else none
Theorem: Encodable.encodeDecode_subtype
Proof state before:
α✝ : Type u_1
inst✝² : Encodable α✝
α : Type u_1
P : α → Prop
inst✝¹ : Encodable α
inst✝ : DecidablePred P
e : ℕ
⊢ ((decode e).bind fun a => if P a then some (encode a) else none) =
    (encode (decode e)).predO.bind fun a => if ∃ a_1, decode a = some a_1 ∧ P a_1 then some a else none
Tactic:
rcases (decode e : Option α) <;> simp
Proof state after:
no goals
Theorem: Encodable.encodeDecode_ofEquiv
Proof state before:
α✝¹ : Type u_1
inst✝³ : Encodable α✝¹
α✝ : Type u_1
P : α✝ → Prop
inst✝² : Encodable α✝
inst✝¹ : DecidablePred P
α : Type u_2
inst✝ : Encodable α
β : Type u_3
e : β ≃ α
⊢ encodeDecode β = encodeDecode α
Tactic:
funext n
Proof state after:
case h
α✝¹ : Type u_1
inst✝³ : Encodable α✝¹
α✝ : Type u_1
P : α✝ → Prop
inst✝² : Encodable α✝
inst✝¹ : DecidablePred P
α : Type u_2
inst✝ : Encodable α
β : Type u_3
e : β ≃ α
n : ℕ
⊢ encodeDecode β n = encodeDecode α n
Theorem: Encodable.encodeDecode_ofEquiv
Proof state before:
case h
α✝¹ : Type u_1
inst✝³ : Encodable α✝¹
α✝ : Type u_1
P : α✝ → Prop
inst✝² : Encodable α✝
inst✝¹ : DecidablePred P
α : Type u_2
inst✝ : Encodable α
β : Type u_3
e : β ≃ α
n : ℕ
⊢ encodeDecode β n = encodeDecode α n
Tactic:
simp[encodeDecode, Encodable.decode_ofEquiv e]
Proof state after:
case h
α✝¹ : Type u_1
inst✝³ : Encodable α✝¹
α✝ : Type u_1
P : α✝ → Prop
inst✝² : Encodable α✝
inst✝¹ : DecidablePred P
α : Type u_2
inst✝ : Encodable α
β : Type u_3
e : β ≃ α
n : ℕ
⊢ (encode (Option.map (⇑e.symm) (decode n))).predO = (encode (decode n)).predO
Theorem: Encodable.encodeDecode_ofEquiv
Proof state before:
case h
α✝¹ : Type u_1
inst✝³ : Encodable α✝¹
α✝ : Type u_1
P : α✝ → Prop
inst✝² : Encodable α✝
inst✝¹ : DecidablePred P
α : Type u_2
inst✝ : Encodable α
β : Type u_3
e : β ≃ α
n : ℕ
⊢ (encode (Option.map (⇑e.symm) (decode n))).predO = (encode (decode n)).predO
Tactic:
rcases (decode n : Option α) with (_ | ⟨a⟩) <;> simp
Proof state after:
case h.some
α✝¹ : Type u_1
inst✝³ : Encodable α✝¹
α✝ : Type u_1
P : α✝ → Prop
inst✝² : Encodable α✝
inst✝¹ : DecidablePred P
α : Type u_2
inst✝ : Encodable α
β : Type u_3
e : β ≃ α
n : ℕ
a : α
⊢ encode (e.symm a) = encode a
Theorem: Encodable.encodeDecode_ofEquiv
Proof state before:
case h.some
α✝¹ : Type u_1
inst✝³ : Encodable α✝¹
α✝ : Type u_1
P : α✝ → Prop
inst✝² : Encodable α✝
inst✝¹ : DecidablePred P
α : Type u_2
inst✝ : Encodable α
β : Type u_3
e : β ≃ α
n : ℕ
a : α
⊢ encode (e.symm a) = encode a
Tactic:
simpa using Encodable.encode_ofEquiv e (e.symm a)
Proof state after:
no goals
Theorem: Encodable.encode_decode_eq_encodeDecode
Proof state before:
α✝ : Type u_1
inst✝² : Encodable α✝
α : Type u_1
P : α → Prop
inst✝¹ : Encodable α
inst✝ : DecidablePred P
e : ℕ
⊢ encode (decode e) = encode (encodeDecode α e)
Tactic:
simp[encodeDecode]
Proof state after:
α✝ : Type u_1
inst✝² : Encodable α✝
α : Type u_1
P : α → Prop
inst✝¹ : Encodable α
inst✝ : DecidablePred P
e : ℕ
⊢ encode (decode e) = encode (encode (decode e)).predO
Theorem: Encodable.encode_decode_eq_encodeDecode
Proof state before:
α✝ : Type u_1
inst✝² : Encodable α✝
α : Type u_1
P : α → Prop
inst✝¹ : Encodable α
inst✝ : DecidablePred P
e : ℕ
⊢ encode (decode e) = encode (encode (decode e)).predO
Tactic:
cases (decode e : Option α) <;> simp
Proof state after:
no goals
Theorem: Encodable.encode_decode_sigma_s
Proof state before:
α✝ : Type u_1
inst✝³ : Encodable α✝
α : Type u_1
P : α → Prop
inst✝² : Encodable α
inst✝¹ : DecidablePred P
β : α → Type u_2
inst✝ : (a : α) → Encodable (β a)
e : ℕ
⊢ encodeDecode ((a : α) × β a) e =
    (decode e.unpair.1).bind fun a => Option.map (fun b => (encode a).pair b) (encodeDecode (β a) e.unpair.2)
Tactic:
rcases ha : (decode e.unpair.1 : Option α) with (_ | a) <;> simp[*, encodeDecode]
Proof state after:
case some
α✝ : Type u_1
inst✝³ : Encodable α✝
α : Type u_1
P : α → Prop
inst✝² : Encodable α
inst✝¹ : DecidablePred P
β : α → Type u_2
inst✝ : (a : α) → Encodable (β a)
e : ℕ
a : α
ha : decode e.unpair.1 = some a
⊢ (encode (Option.map (Sigma.mk a) (decode e.unpair.2))).predO =
    Option.map (fun b => (encode a).pair b) (encode (decode e.unpair.2)).predO
Theorem: Encodable.encode_decode_sigma_s
Proof state before:
case some
α✝ : Type u_1
inst✝³ : Encodable α✝
α : Type u_1
P : α → Prop
inst✝² : Encodable α
inst✝¹ : DecidablePred P
β : α → Type u_2
inst✝ : (a : α) → Encodable (β a)
e : ℕ
a : α
ha : decode e.unpair.1 = some a
⊢ (encode (Option.map (Sigma.mk a) (decode e.unpair.2))).predO =
    Option.map (fun b => (encode a).pair b) (encode (decode e.unpair.2)).predO
Tactic:
{ rcases (decode e.unpair.2 : Option (β a)) with (_ | b) <;> simp[*] }
Proof state after:
no goals
Theorem: Encodable.encode_decode_sigma_s
Proof state before:
case some
α✝ : Type u_1
inst✝³ : Encodable α✝
α : Type u_1
P : α → Prop
inst✝² : Encodable α
inst✝¹ : DecidablePred P
β : α → Type u_2
inst✝ : (a : α) → Encodable (β a)
e : ℕ
a : α
ha : decode e.unpair.1 = some a
⊢ (encode (Option.map (Sigma.mk a) (decode e.unpair.2))).predO =
    Option.map (fun b => (encode a).pair b) (encode (decode e.unpair.2)).predO
Tactic:
rcases (decode e.unpair.2 : Option (β a)) with (_ | b) <;> simp[*]
Proof state after:
no goals
Theorem: Encodable.encode_decode_sigma_of_none
Proof state before:
α✝ : Type u_1
inst✝³ : Encodable α✝
α : Type u_1
P : α → Prop
inst✝² : Encodable α
inst✝¹ : DecidablePred P
β : α → Type u_2
inst✝ : (a : α) → Encodable (β a)
e : ℕ
h : decode e.unpair.1 = none
⊢ encodeDecode ((a : α) × β a) e = none
Tactic:
simp[encodeDecode, h]
Proof state after:
no goals
Theorem: Encodable.encode_decode_sigma_of_some
Proof state before:
α✝ : Type u_1
inst✝³ : Encodable α✝
α : Type u_1
P : α → Prop
inst✝² : Encodable α
inst✝¹ : DecidablePred P
β : α → Type u_2
inst✝ : (a : α) → Encodable (β a)
e : ℕ
a : α
h : decode e.unpair.1 = some a
⊢ encodeDecode ((a : α) × β a) e = Option.map (fun b => (encode a).pair b) (encodeDecode (β a) e.unpair.2)
Tactic:
simp[encodeDecode, h]
Proof state after:
α✝ : Type u_1
inst✝³ : Encodable α✝
α : Type u_1
P : α → Prop
inst✝² : Encodable α
inst✝¹ : DecidablePred P
β : α → Type u_2
inst✝ : (a : α) → Encodable (β a)
e : ℕ
a : α
h : decode e.unpair.1 = some a
⊢ (encode (Option.map (Sigma.mk a) (decode e.unpair.2))).predO =
    Option.map (fun b => (encode a).pair b) (encode (decode e.unpair.2)).predO
Theorem: Encodable.encode_decode_sigma_of_some
Proof state before:
α✝ : Type u_1
inst✝³ : Encodable α✝
α : Type u_1
P : α → Prop
inst✝² : Encodable α
inst✝¹ : DecidablePred P
β : α → Type u_2
inst✝ : (a : α) → Encodable (β a)
e : ℕ
a : α
h : decode e.unpair.1 = some a
⊢ (encode (Option.map (Sigma.mk a) (decode e.unpair.2))).predO =
    Option.map (fun b => (encode a).pair b) (encode (decode e.unpair.2)).predO
Tactic:
rcases decode e.unpair.2 with (_ | b) <;> simp
Proof state after:
no goals
Theorem: Primrec.decode_iff
Proof state before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → σ
h : Primrec fun n => Option.map f (decode n)
⊢ Primrec f
Tactic:
simp[Primrec]
Proof state after:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → σ
h : Primrec fun n => Option.map f (decode n)
⊢ Nat.Primrec fun n => encode (Option.map f (decode n))
Theorem: Primrec.decode_iff
Proof state before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → σ
h : Primrec fun n => Option.map f (decode n)
⊢ Nat.Primrec fun n => encode (Option.map f (decode n))
Tactic:
exact Primrec.nat_iff.mp (Primrec.encode.comp h)
Proof state after:
no goals
Theorem: Primrec₂.decode_iff₁
Proof state before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → β → σ
h : Primrec₂ fun n b => Option.map (fun x => f x b) (decode n)
⊢ ∀ (a : α) (b : β), Option.map (fun x => f x b) (decode (encode a)) = some (f a b)
Tactic:
simp
Proof state after:
no goals
Theorem: Primrec₂.decode_iff₂
Proof state before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → β → σ
h : Primrec₂ fun a n => Option.map (f a) (decode n)
⊢ ∀ (a : α) (b : β), Option.map (f a) (decode (encode b)) = some (f a b)
Tactic:
simp
Proof state after:
no goals
Theorem: Primrec₂.of_equiv_iff
Proof state before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β✝ : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β✝
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
β : Type u_8
e : β ≃ α
f : σ → τ → β
⊢ (Primrec₂ fun a b => e (f a b)) ↔ Primrec₂ f
Tactic:
simp[Primrec₂, Primrec.of_equiv_iff]
Proof state after:
no goals
Theorem: Primrec.of_equiv_iff'
Proof state before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β✝ : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β✝
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
β : Type u_8
e : β ≃ α
f : β → σ
this : Primcodable β := Primcodable.ofEquiv α e
h : Primrec fun b => f (e.symm b)
⊢ ∀ (n : β), f (e.symm (e n)) = f n
Tactic:
simp
Proof state after:
no goals
Theorem: Primrec₂.of_equiv_iff'2
Proof state before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β✝ : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β✝
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
β : Type u_8
e : β ≃ α₂
f : α₁ → β → σ
this : Primcodable β := Primcodable.ofEquiv α₂ e
h : Primrec₂ fun a b => f a (e.symm b)
⊢ ∀ (n : α₁ × β), f n.1 (e.symm (e n.2)) = f n.1 n.2
Tactic:
simp
Proof state after:
no goals
Theorem: Primrec.nat_strong_rec'
Proof state before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → ℕ → σ
g : α × ℕ → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n : ℕ), g (a, n) (List.map (f a) (List.range n)) = some (f a n)
⊢ Primrec₂ f
Tactic:
let g' : α → List σ → Option σ := fun a l => g (a, l.length) l
Proof state after:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → ℕ → σ
g : α × ℕ → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n : ℕ), g (a, n) (List.map (f a) (List.range n)) = some (f a n)
g' : α → List σ → Option σ := fun a l => g (a, l.length) l
⊢ Primrec₂ f
Theorem: Primrec.nat_strong_rec'
Proof state before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → ℕ → σ
g : α × ℕ → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n : ℕ), g (a, n) (List.map (f a) (List.range n)) = some (f a n)
g' : α → List σ → Option σ := fun a l => g (a, l.length) l
⊢ Primrec₂ f
Tactic:
have : Primrec₂ g' := hg.comp₂ (pair fst (list_length.comp snd)) Primrec₂.right
Proof state after:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → ℕ → σ
g : α × ℕ → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n : ℕ), g (a, n) (List.map (f a) (List.range n)) = some (f a n)
g' : α → List σ → Option σ := fun a l => g (a, l.length) l
this : Primrec₂ g'
⊢ Primrec₂ f
Theorem: Primrec.nat_strong_rec'
Proof state before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → ℕ → σ
g : α × ℕ → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n : ℕ), g (a, n) (List.map (f a) (List.range n)) = some (f a n)
g' : α → List σ → Option σ := fun a l => g (a, l.length) l
this : Primrec₂ g'
⊢ Primrec₂ f
Tactic:
exact nat_strong_rec f this (by simpa [g'] using H)
Proof state after:
no goals
Theorem: Primrec.nat_strong_rec'
Proof state before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → ℕ → σ
g : α × ℕ → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n : ℕ), g (a, n) (List.map (f a) (List.range n)) = some (f a n)
g' : α → List σ → Option σ := fun a l => g (a, l.length) l
this : Primrec₂ g'
⊢ ∀ (a : α) (n : ℕ), g' a (List.map (f a) (List.range n)) = some (f a n)
Tactic:
simpa [g'] using H
Proof state after:
no goals
Theorem: Primrec.nat_strong_rec'2
Proof state before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → ℕ × ℕ → σ
g : α × ℕ × ℕ → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n m : ℕ), g (a, n, m) (List.map (fun i => f a i.unpair) (List.range (n.pair m))) = some (f a (n, m))
⊢ Primrec₂ f
Tactic:
let g' : α × ℕ → List σ → Option σ := fun (a, n) => g (a, n.unpair)
Proof state after:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → ℕ × ℕ → σ
g : α × ℕ × ℕ → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n m : ℕ), g (a, n, m) (List.map (fun i => f a i.unpair) (List.range (n.pair m))) = some (f a (n, m))
g' : α × ℕ → List σ → Option σ :=
  fun x =>
    match (motive := α × ℕ → List σ → Option σ) x with
    | (a, n) => g (a, n.unpair)
⊢ Primrec₂ f
Theorem: Primrec.nat_strong_rec'2
Proof state before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → ℕ × ℕ → σ
g : α × ℕ × ℕ → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n m : ℕ), g (a, n, m) (List.map (fun i => f a i.unpair) (List.range (n.pair m))) = some (f a (n, m))
g' : α × ℕ → List σ → Option σ :=
  fun x =>
    match (motive := α × ℕ → List σ → Option σ) x with
    | (a, n) => g (a, n.unpair)
⊢ Primrec₂ f
Tactic:
have : Primrec₂ g' := hg.comp₂ (pair (fst.comp fst) (unpair.comp $ snd.comp fst)) Primrec₂.right
Proof state after:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → ℕ × ℕ → σ
g : α × ℕ × ℕ → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n m : ℕ), g (a, n, m) (List.map (fun i => f a i.unpair) (List.range (n.pair m))) = some (f a (n, m))
g' : α × ℕ → List σ → Option σ :=
  fun x =>
    match (motive := α × ℕ → List σ → Option σ) x with
    | (a, n) => g (a, n.unpair)
this : Primrec₂ g'
⊢ Primrec₂ f