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

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
inst✝² : Primcodable α
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
hsup : Primrec₂ Sup.sup
⊢ Primrec List.sup
Tactic:
have e : ∀ l : List α, l.sup = l.foldr Sup.sup ⊥ := by
  intro l; induction' l with a as ih <;> simp[sup_eq_max, *]
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 τ
α : Type u_8
inst✝² : Primcodable α
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
hsup : Primrec₂ Sup.sup
e : ∀ (l : List α), l.sup = List.foldr Sup.sup ⊥ l
⊢ Primrec List.sup

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
inst✝² : Primcodable α
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
hsup : Primrec₂ Sup.sup
e : ∀ (l : List α), l.sup = List.foldr Sup.sup ⊥ l
⊢ Primrec List.sup
Tactic:
have : Primrec (fun l => l.foldr Sup.sup ⊥ : List α → α) :=
  list_foldr Primrec.id (const _) (hsup.comp₂ (fst.comp₂ Primrec₂.right) (snd.comp₂ Primrec₂.right))
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 τ
α : Type u_8
inst✝² : Primcodable α
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
hsup : Primrec₂ Sup.sup
e : ∀ (l : List α), l.sup = List.foldr Sup.sup ⊥ l
this : Primrec fun l => List.foldr Sup.sup ⊥ l
⊢ Primrec List.sup

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
inst✝² : Primcodable α
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
hsup : Primrec₂ Sup.sup
e : ∀ (l : List α), l.sup = List.foldr Sup.sup ⊥ l
this : Primrec fun l => List.foldr Sup.sup ⊥ l
⊢ Primrec List.sup
Tactic:
exact this.of_eq (by simp[e])
State after:
no goals

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
inst✝² : Primcodable α
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
hsup : Primrec₂ Sup.sup
⊢ ∀ (l : List α), l.sup = List.foldr Sup.sup ⊥ l
Tactic:
intro l
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 τ
α : Type u_8
inst✝² : Primcodable α
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
hsup : Primrec₂ Sup.sup
l : List α
⊢ l.sup = List.foldr Sup.sup ⊥ l

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
inst✝² : Primcodable α
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
hsup : Primrec₂ Sup.sup
l : List α
⊢ l.sup = List.foldr Sup.sup ⊥ l
Tactic:
induction' l with a as ih <;> simp[sup_eq_max, *]
State after:
no goals

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
inst✝² : Primcodable α
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
hsup : Primrec₂ Sup.sup
e : ∀ (l : List α), l.sup = List.foldr Sup.sup ⊥ l
this : Primrec fun l => List.foldr Sup.sup ⊥ l
⊢ ∀ (n : List α), List.foldr Sup.sup ⊥ n = n.sup
Tactic:
simp[e]
State after:
no goals