Theorem: Primrec.list_replicate (Logic/Vorspiel/Computability.lean)

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 α
⊢ Primrec₂ List.replicate
Tactic:
have : Primrec₂ (fun p ih => p.2 :: ih.2 : ℕ × α → ℕ × List α → List α) :=
  list_cons.comp₂ (snd.comp₂ .left) (snd.comp₂ .right)
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 α
this : Primrec₂ fun p ih => p.2 :: ih.2
⊢ Primrec₂ List.replicate

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 α
this : Primrec₂ fun p ih => p.2 :: ih.2
⊢ Primrec₂ List.replicate
Tactic:
exact (Primrec.nat_rec' Primrec.fst (.const []) this).of_eq <| by
  rintro ⟨n, a⟩; simp; induction n <;> simp[*]
State after:
no goals

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 α
this : Primrec₂ fun p ih => p.2 :: ih.2
⊢ ∀ (n : ℕ × α), Nat.rec [] (fun n_1 IH => n.2 :: (n_1, IH).2) n.1 = List.replicate n.1 n.2
Tactic:
rintro ⟨n, a⟩
State after:
case mk
σ : 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 α
this : Primrec₂ fun p ih => p.2 :: ih.2
n : ℕ
a : α
⊢ Nat.rec [] (fun n_1 IH => (n, a).2 :: (n_1, IH).2) (n, a).1 = List.replicate (n, a).1 (n, a).2

State before:
case mk
σ : 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 α
this : Primrec₂ fun p ih => p.2 :: ih.2
n : ℕ
a : α
⊢ Nat.rec [] (fun n_1 IH => (n, a).2 :: (n_1, IH).2) (n, a).1 = List.replicate (n, a).1 (n, a).2
Tactic:
simp
State after:
case mk
σ : 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 α
this : Primrec₂ fun p ih => p.2 :: ih.2
n : ℕ
a : α
⊢ Nat.rec [] (fun n IH => a :: IH) n = List.replicate n a

State before:
case mk
σ : 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 α
this : Primrec₂ fun p ih => p.2 :: ih.2
n : ℕ
a : α
⊢ Nat.rec [] (fun n IH => a :: IH) n = List.replicate n a
Tactic:
induction n <;> simp[*]
State after:
no goals