Theorem: Computable.list_all (Logic/Vorspiel/Computability.lean)

State before:
α✝ : Type u_1
β✝ : Type u_2
σ : Type u_3
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β✝
inst✝² : Primcodable σ
α : Type u_4
β : Type u_5
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
l : α → List β
hp : Computable₂ p
hl : Computable l
⊢ Computable fun a => (l a).all (p a)
Tactic:
let f : α → ℕ → Bool := fun a n => n.recOn true (fun m ih => ((l a).reverse.get? m).casesOn false (fun b => p a b && ih))
State after:
α✝ : Type u_1
β✝ : Type u_2
σ : Type u_3
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β✝
inst✝² : Primcodable σ
α : Type u_4
β : Type u_5
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
l : α → List β
hp : Computable₂ p
hl : Computable l
f : α → ℕ → Bool :=
  fun a n => Nat.recOn n true fun m ih => Option.casesOn ((l a).reverse.get? m) false fun b => p a b && ih
⊢ Computable fun a => (l a).all (p a)

State before:
α✝ : Type u_1
β✝ : Type u_2
σ : Type u_3
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β✝
inst✝² : Primcodable σ
α : Type u_4
β : Type u_5
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
l : α → List β
hp : Computable₂ p
hl : Computable l
f : α → ℕ → Bool :=
  fun a n => Nat.recOn n true fun m ih => Option.casesOn ((l a).reverse.get? m) false fun b => p a b && ih
⊢ Computable fun a => (l a).all (p a)
Tactic:
have : Computable₂ (fun q₁ q₂ => ((l q₁.1).reverse.get? q₂.1).casesOn false (fun b => p q₁.1 b && q₂.2)
  : α × ℕ → ℕ × Bool → Bool) :=
  to₂' <| option_casesOn
    (list_get?.comp (list_reverse.comp $ hl.comp $ fst.comp fst) (fst.comp snd))
    (const false) (by apply dom_bool₂.comp₂ (hp.comp₂ (fst.comp₂ $ fst.comp₂ .left) .right) (snd.comp₂ $ snd.comp₂ .left))
State after:
α✝ : Type u_1
β✝ : Type u_2
σ : Type u_3
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β✝
inst✝² : Primcodable σ
α : Type u_4
β : Type u_5
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
l : α → List β
hp : Computable₂ p
hl : Computable l
f : α → ℕ → Bool :=
  fun a n => Nat.recOn n true fun m ih => Option.casesOn ((l a).reverse.get? m) false fun b => p a b && ih
this : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
⊢ Computable fun a => (l a).all (p a)

State before:
α✝ : Type u_1
β✝ : Type u_2
σ : Type u_3
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β✝
inst✝² : Primcodable σ
α : Type u_4
β : Type u_5
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
l : α → List β
hp : Computable₂ p
hl : Computable l
f : α → ℕ → Bool :=
  fun a n => Nat.recOn n true fun m ih => Option.casesOn ((l a).reverse.get? m) false fun b => p a b && ih
this : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
⊢ Computable fun a => (l a).all (p a)
Tactic:
have hf : Computable₂ f := (nat_rec snd (const true) this).to₂
State after:
α✝ : Type u_1
β✝ : Type u_2
σ : Type u_3
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β✝
inst✝² : Primcodable σ
α : Type u_4
β : Type u_5
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
l : α → List β
hp : Computable₂ p
hl : Computable l
f : α → ℕ → Bool :=
  fun a n => Nat.recOn n true fun m ih => Option.casesOn ((l a).reverse.get? m) false fun b => p a b && ih
this : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
⊢ Computable fun a => (l a).all (p a)

State before:
α✝ : Type u_1
β✝ : Type u_2
σ : Type u_3
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β✝
inst✝² : Primcodable σ
α : Type u_4
β : Type u_5
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
l : α → List β
hp : Computable₂ p
hl : Computable l
f : α → ℕ → Bool :=
  fun a n => Nat.recOn n true fun m ih => Option.casesOn ((l a).reverse.get? m) false fun b => p a b && ih
⊢ Computable₂ fun p_1 val => (fun b => p p_1.1.1 b && p_1.2.2) val
Tactic:
apply dom_bool₂.comp₂ (hp.comp₂ (fst.comp₂ $ fst.comp₂ .left) .right) (snd.comp₂ $ snd.comp₂ .left)
State after:
no goals

State before:
α✝ : Type u_1
β✝ : Type u_2
σ : Type u_3
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β✝
inst✝² : Primcodable σ
α : Type u_4
β : Type u_5
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
l : α → List β
hp : Computable₂ p
hl : Computable l
f : α → ℕ → Bool :=
  fun a n => Nat.recOn n true fun m ih => Option.casesOn ((l a).reverse.get? m) false fun b => p a b && ih
this : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
⊢ ∀ (n : α), f (id n) (l n).length = (l n).all (p n)
Tactic:
intro a
State after:
α✝ : Type u_1
β✝ : Type u_2
σ : Type u_3
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β✝
inst✝² : Primcodable σ
α : Type u_4
β : Type u_5
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
l : α → List β
hp : Computable₂ p
hl : Computable l
f : α → ℕ → Bool :=
  fun a n => Nat.recOn n true fun m ih => Option.casesOn ((l a).reverse.get? m) false fun b => p a b && ih
this : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
a : α
⊢ f (id a) (l a).length = (l a).all (p a)

State before:
α✝ : Type u_1
β✝ : Type u_2
σ : Type u_3
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β✝
inst✝² : Primcodable σ
α : Type u_4
β : Type u_5
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
l : α → List β
hp : Computable₂ p
hl : Computable l
f : α → ℕ → Bool :=
  fun a n => Nat.recOn n true fun m ih => Option.casesOn ((l a).reverse.get? m) false fun b => p a b && ih
this : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
a : α
⊢ f (id a) (l a).length = (l a).all (p a)
Tactic:
simp [f]
State after:
α✝ : Type u_1
β✝ : Type u_2
σ : Type u_3
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β✝
inst✝² : Primcodable σ
α : Type u_4
β : Type u_5
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
l : α → List β
hp : Computable₂ p
hl : Computable l
f : α → ℕ → Bool :=
  fun a n => Nat.recOn n true fun m ih => Option.casesOn ((l a).reverse.get? m) false fun b => p a b && ih
this : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
a : α
⊢ Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) ((l a).reverse.get? m)) (l a).length =
    (l a).all (p a)

State before:
α✝ : Type u_1
β✝ : Type u_2
σ : Type u_3
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β✝
inst✝² : Primcodable σ
α : Type u_4
β : Type u_5
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
l : α → List β
hp : Computable₂ p
hl : Computable l
f : α → ℕ → Bool :=
  fun a n => Nat.recOn n true fun m ih => Option.casesOn ((l a).reverse.get? m) false fun b => p a b && ih
this : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
a : α
⊢ Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) ((l a).reverse.get? m)) (l a).length =
    (l a).all (p a)
Tactic:
generalize l a = la
State after:
α✝ : Type u_1
β✝ : Type u_2
σ : Type u_3
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β✝
inst✝² : Primcodable σ
α : Type u_4
β : Type u_5
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
l : α → List β
hp : Computable₂ p
hl : Computable l
f : α → ℕ → Bool :=
  fun a n => Nat.recOn n true fun m ih => Option.casesOn ((l a).reverse.get? m) false fun b => p a b && ih
this : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
a : α
la : List β
⊢ Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) (la.reverse.get? m)) la.length = la.all (p a)

State before:
α✝ : Type u_1
β✝ : Type u_2
σ : Type u_3
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β✝
inst✝² : Primcodable σ
α : Type u_4
β : Type u_5
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
l : α → List β
hp : Computable₂ p
hl : Computable l
f : α → ℕ → Bool :=
  fun a n => Nat.recOn n true fun m ih => Option.casesOn ((l a).reverse.get? m) false fun b => p a b && ih
this : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
a : α
la : List β
⊢ Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) (la.reverse.get? m)) la.length = la.all (p a)
Tactic:
induction' la with b la' ih <;> simp
State after:
case cons
α✝ : Type u_1
β✝ : Type u_2
σ : Type u_3
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β✝
inst✝² : Primcodable σ
α : Type u_4
β : Type u_5
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
l : α → List β
hp : Computable₂ p
hl : Computable l
f : α → ℕ → Bool :=
  fun a n => Nat.recOn n true fun m ih => Option.casesOn ((l a).reverse.get? m) false fun b => p a b && ih
this : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
a : α
b : β
la' : List β
ih :
  Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) (la'.reverse.get? m)) la'.length = la'.all (p a)
⊢ Option.rec false
      (fun val =>
        p a val &&
          Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) ((la'.reverse ++ [b]).get? m))
            la'.length)
      ((la'.reverse ++ [b]).get? la'.length) =
    (p a b && la'.all (p a))

State before:
case cons
α✝ : Type u_1
β✝ : Type u_2
σ : Type u_3
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β✝
inst✝² : Primcodable σ
α : Type u_4
β : Type u_5
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
l : α → List β
hp : Computable₂ p
hl : Computable l
f : α → ℕ → Bool :=
  fun a n => Nat.recOn n true fun m ih => Option.casesOn ((l a).reverse.get? m) false fun b => p a b && ih
this : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
a : α
b : β
la' : List β
ih :
  Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) (la'.reverse.get? m)) la'.length = la'.all (p a)
⊢ Option.rec false
      (fun val =>
        p a val &&
          Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) ((la'.reverse ++ [b]).get? m))
            la'.length)
      ((la'.reverse ++ [b]).get? la'.length) =
    (p a b && la'.all (p a))
Tactic:
have : List.get? (List.reverse la' ++ [b]) la'.length = some b := by
  simpa using List.get?_concat_length la'.reverse b
State after:
case cons
α✝ : Type u_1
β✝ : Type u_2
σ : Type u_3
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β✝
inst✝² : Primcodable σ
α : Type u_4
β : Type u_5
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
l : α → List β
hp : Computable₂ p
hl : Computable l
f : α → ℕ → Bool :=
  fun a n => Nat.recOn n true fun m ih => Option.casesOn ((l a).reverse.get? m) false fun b => p a b && ih
this✝ : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
a : α
b : β
la' : List β
ih :
  Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) (la'.reverse.get? m)) la'.length = la'.all (p a)
this : (la'.reverse ++ [b]).get? la'.length = some b
⊢ Option.rec false
      (fun val =>
        p a val &&
          Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) ((la'.reverse ++ [b]).get? m))
            la'.length)
      ((la'.reverse ++ [b]).get? la'.length) =
    (p a b && la'.all (p a))

State before:
case cons
α✝ : Type u_1
β✝ : Type u_2
σ : Type u_3
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β✝
inst✝² : Primcodable σ
α : Type u_4
β : Type u_5
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
l : α → List β
hp : Computable₂ p
hl : Computable l
f : α → ℕ → Bool :=
  fun a n => Nat.recOn n true fun m ih => Option.casesOn ((l a).reverse.get? m) false fun b => p a b && ih
this✝ : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
a : α
b : β
la' : List β
ih :
  Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) (la'.reverse.get? m)) la'.length = la'.all (p a)
this : (la'.reverse ++ [b]).get? la'.length = some b
⊢ Option.rec false
      (fun val =>
        p a val &&
          Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) ((la'.reverse ++ [b]).get? m))
            la'.length)
      ((la'.reverse ++ [b]).get? la'.length) =
    (p a b && la'.all (p a))
Tactic:
simp [this]
State after:
case cons
α✝ : Type u_1
β✝ : Type u_2
σ : Type u_3
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β✝
inst✝² : Primcodable σ
α : Type u_4
β : Type u_5
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
l : α → List β
hp : Computable₂ p
hl : Computable l
f : α → ℕ → Bool :=
  fun a n => Nat.recOn n true fun m ih => Option.casesOn ((l a).reverse.get? m) false fun b => p a b && ih
this✝ : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
a : α
b : β
la' : List β
ih :
  Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) (la'.reverse.get? m)) la'.length = la'.all (p a)
this : (la'.reverse ++ [b]).get? la'.length = some b
⊢ (p a b &&
      Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) ((la'.reverse ++ [b]).get? m)) la'.length) =
    (p a b && la'.all (p a))

State before:
case cons
α✝ : Type u_1
β✝ : Type u_2
σ : Type u_3
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β✝
inst✝² : Primcodable σ
α : Type u_4
β : Type u_5
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
l : α → List β
hp : Computable₂ p
hl : Computable l
f : α → ℕ → Bool :=
  fun a n => Nat.recOn n true fun m ih => Option.casesOn ((l a).reverse.get? m) false fun b => p a b && ih
this✝ : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
a : α
b : β
la' : List β
ih :
  Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) (la'.reverse.get? m)) la'.length = la'.all (p a)
this : (la'.reverse ++ [b]).get? la'.length = some b
⊢ (p a b &&
      Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) ((la'.reverse ++ [b]).get? m)) la'.length) =
    (p a b && la'.all (p a))
Tactic:
rw [←ih]
State after:
case cons
α✝ : Type u_1
β✝ : Type u_2
σ : Type u_3
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β✝
inst✝² : Primcodable σ
α : Type u_4
β : Type u_5
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
l : α → List β
hp : Computable₂ p
hl : Computable l
f : α → ℕ → Bool :=
  fun a n => Nat.recOn n true fun m ih => Option.casesOn ((l a).reverse.get? m) false fun b => p a b && ih
this✝ : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
a : α
b : β
la' : List β
ih :
  Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) (la'.reverse.get? m)) la'.length = la'.all (p a)
this : (la'.reverse ++ [b]).get? la'.length = some b
⊢ (p a b &&
      Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) ((la'.reverse ++ [b]).get? m)) la'.length) =
    (p a b && Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) (la'.reverse.get? m)) la'.length)

State before:
α✝ : Type u_1
β✝ : Type u_2
σ : Type u_3
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β✝
inst✝² : Primcodable σ
α : Type u_4
β : Type u_5
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
l : α → List β
hp : Computable₂ p
hl : Computable l
f : α → ℕ → Bool :=
  fun a n => Nat.recOn n true fun m ih => Option.casesOn ((l a).reverse.get? m) false fun b => p a b && ih
this : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
a : α
b : β
la' : List β
ih :
  Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) (la'.reverse.get? m)) la'.length = la'.all (p a)
⊢ (la'.reverse ++ [b]).get? la'.length = some b
Tactic:
simpa using List.get?_concat_length la'.reverse b
State after:
no goals

State before:
α✝ : Type u_1
β✝ : Type u_2
σ : Type u_3
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β✝
inst✝² : Primcodable σ
α : Type u_4
β : Type u_5
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
l : α → List β
hp : Computable₂ p
hl : Computable l
f : α → ℕ → Bool :=
  fun a n => Nat.recOn n true fun m ih => Option.casesOn ((l a).reverse.get? m) false fun b => p a b && ih
this✝ : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
a : α
b : β
la' : List β
ih :
  Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) (la'.reverse.get? m)) la'.length = la'.all (p a)
this : (la'.reverse ++ [b]).get? la'.length = some b
⊢ ∀ m < la'.length,
    ∀ (a_2 : Bool),
      Option.rec false (fun val => p a val && a_2) ((la'.reverse ++ [b]).get? m) =
        Option.rec false (fun val => p a val && a_2) (la'.reverse.get? m)
Tactic:
intro m hm k
State after:
α✝ : Type u_1
β✝ : Type u_2
σ : Type u_3
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β✝
inst✝² : Primcodable σ
α : Type u_4
β : Type u_5
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
l : α → List β
hp : Computable₂ p
hl : Computable l
f : α → ℕ → Bool :=
  fun a n => Nat.recOn n true fun m ih => Option.casesOn ((l a).reverse.get? m) false fun b => p a b && ih
this✝ : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
a : α
b : β
la' : List β
ih :
  Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) (la'.reverse.get? m)) la'.length = la'.all (p a)
this : (la'.reverse ++ [b]).get? la'.length = some b
m : ℕ
hm : m < la'.length
k : Bool
⊢ Option.rec false (fun val => p a val && k) ((la'.reverse ++ [b]).get? m) =
    Option.rec false (fun val => p a val && k) (la'.reverse.get? m)

State before:
α✝ : Type u_1
β✝ : Type u_2
σ : Type u_3
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β✝
inst✝² : Primcodable σ
α : Type u_4
β : Type u_5
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
l : α → List β
hp : Computable₂ p
hl : Computable l
f : α → ℕ → Bool :=
  fun a n => Nat.recOn n true fun m ih => Option.casesOn ((l a).reverse.get? m) false fun b => p a b && ih
this✝ : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
a : α
b : β
la' : List β
ih :
  Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) (la'.reverse.get? m)) la'.length = la'.all (p a)
this : (la'.reverse ++ [b]).get? la'.length = some b
m : ℕ
hm : m < la'.length
k : Bool
⊢ Option.rec false (fun val => p a val && k) ((la'.reverse ++ [b]).get? m) =
    Option.rec false (fun val => p a val && k) (la'.reverse.get? m)
Tactic:
have : (la'.reverse ++ [b]).get? m = la'.reverse.get? m := List.get?_append (by simp[hm])
State after:
α✝ : Type u_1
β✝ : Type u_2
σ : Type u_3
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β✝
inst✝² : Primcodable σ
α : Type u_4
β : Type u_5
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
l : α → List β
hp : Computable₂ p
hl : Computable l
f : α → ℕ → Bool :=
  fun a n => Nat.recOn n true fun m ih => Option.casesOn ((l a).reverse.get? m) false fun b => p a b && ih
this✝¹ : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
a : α
b : β
la' : List β
ih :
  Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) (la'.reverse.get? m)) la'.length = la'.all (p a)
this✝ : (la'.reverse ++ [b]).get? la'.length = some b
m : ℕ
hm : m < la'.length
k : Bool
this : (la'.reverse ++ [b]).get? m = la'.reverse.get? m
⊢ Option.rec false (fun val => p a val && k) ((la'.reverse ++ [b]).get? m) =
    Option.rec false (fun val => p a val && k) (la'.reverse.get? m)

State before:
α✝ : Type u_1
β✝ : Type u_2
σ : Type u_3
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β✝
inst✝² : Primcodable σ
α : Type u_4
β : Type u_5
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
l : α → List β
hp : Computable₂ p
hl : Computable l
f : α → ℕ → Bool :=
  fun a n => Nat.recOn n true fun m ih => Option.casesOn ((l a).reverse.get? m) false fun b => p a b && ih
this✝¹ : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
a : α
b : β
la' : List β
ih :
  Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) (la'.reverse.get? m)) la'.length = la'.all (p a)
this✝ : (la'.reverse ++ [b]).get? la'.length = some b
m : ℕ
hm : m < la'.length
k : Bool
this : (la'.reverse ++ [b]).get? m = la'.reverse.get? m
⊢ Option.rec false (fun val => p a val && k) ((la'.reverse ++ [b]).get? m) =
    Option.rec false (fun val => p a val && k) (la'.reverse.get? m)
Tactic:
simp [this]
State after:
no goals

State before:
α✝ : Type u_1
β✝ : Type u_2
σ : Type u_3
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β✝
inst✝² : Primcodable σ
α : Type u_4
β : Type u_5
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
l : α → List β
hp : Computable₂ p
hl : Computable l
f : α → ℕ → Bool :=
  fun a n => Nat.recOn n true fun m ih => Option.casesOn ((l a).reverse.get? m) false fun b => p a b && ih
this✝ : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
a : α
b : β
la' : List β
ih :
  Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) (la'.reverse.get? m)) la'.length = la'.all (p a)
this : (la'.reverse ++ [b]).get? la'.length = some b
m : ℕ
hm : m < la'.length
k : Bool
⊢ m < la'.reverse.length
Tactic:
simp[hm]
State after:
no goals