Theorem: LO.FirstOrder.Arith.FirstIncompleteness.codeAux_sigma_one (Logic/FirstOrder/Arith/Representation.lean)

State before:
k : ℕ
c : Code k
⊢ Hierarchy 𝚺 1 (codeAux c)
Tactic:
induction c <;> simp[codeAux, Matrix.fun_eq_vec₂]
State after:
case comp
k m✝ n✝ : ℕ
a✝¹ : Code n✝
a✝ : Fin n✝ → Code m✝
a_ih✝¹ : Hierarchy 𝚺 1 (codeAux a✝¹)
a_ih✝ : ∀ (a : Fin n✝), Hierarchy 𝚺 1 (codeAux (a✝ a))
⊢ Hierarchy 𝚺 1
    (∃*
      (Rew.bind ![] (&0 :> fun x => #x)).hom (codeAux a✝¹) ⋏
        Matrix.conj fun i => (Rew.bind ![] (#i :> fun x => &x.succ)).hom (codeAux (a✝ i)))

case rfind
k n✝ : ℕ
a✝ : Code (n✝ + 1)
a_ih✝ : Hierarchy 𝚺 1 (codeAux a✝)
⊢ Hierarchy 𝚺 1 (codeAux a✝) ∧
    Hierarchy 𝚺 1
      (“(∀[!!(![#0, &0] 0) < !!(![#0, &0] 1)]
            ∃'
              (¬!!(![#0, ‘0’] 0) = !!(![#0, ‘0’] 1) ∧
                  !((Rew.bind ![] (#0 :> #1 :> fun x => &x.succ)).hom (codeAux a✝))))”)

State before:
k m✝ n✝ : ℕ
c : Code n✝
d : Fin n✝ → Code m✝
ihc : Hierarchy 𝚺 1 (codeAux c)
ihg : ∀ (a : Fin n✝), Hierarchy 𝚺 1 (codeAux (d a))
⊢ Hierarchy 𝚺 1
    (∃*
      (Rew.bind ![] (&0 :> fun x => #x)).hom (codeAux c) ⋏
        Matrix.conj fun i => (Rew.bind ![] (#i :> fun x => &x.succ)).hom (codeAux (d i)))
Tactic:
case comp c d ihc ihg =>
  exact Hierarchy.exClosure (by simp [ihc, ihg])
State after:
no goals

State before:
k✝ k : ℕ
c : Code (k + 1)
ih : Hierarchy 𝚺 1 (codeAux c)
⊢ Hierarchy 𝚺 1 (codeAux c) ∧
    Hierarchy 𝚺 1
      (“(∀[!!(![#0, &0] 0) < !!(![#0, &0] 1)]
            ∃'
              (¬!!(![#0, ‘0’] 0) = !!(![#0, ‘0’] 1) ∧
                  !((Rew.bind ![] (#0 :> #1 :> fun x => &x.succ)).hom (codeAux c))))”)
Tactic:
case rfind k c ih => simp [ih]
State after:
no goals

State before:
k m✝ n✝ : ℕ
c : Code n✝
d : Fin n✝ → Code m✝
ihc : Hierarchy 𝚺 1 (codeAux c)
ihg : ∀ (a : Fin n✝), Hierarchy 𝚺 1 (codeAux (d a))
⊢ Hierarchy 𝚺 1
    (∃*
      (Rew.bind ![] (&0 :> fun x => #x)).hom (codeAux c) ⋏
        Matrix.conj fun i => (Rew.bind ![] (#i :> fun x => &x.succ)).hom (codeAux (d i)))
Tactic:
exact Hierarchy.exClosure (by simp [ihc, ihg])
State after:
no goals

State before:
k m✝ n✝ : ℕ
c : Code n✝
d : Fin n✝ → Code m✝
ihc : Hierarchy 𝚺 1 (codeAux c)
ihg : ∀ (a : Fin n✝), Hierarchy 𝚺 1 (codeAux (d a))
⊢ Hierarchy 𝚺 (0 + 1)
    ((Rew.bind ![] (&0 :> fun x => #x)).hom (codeAux c) ⋏
      Matrix.conj fun i => (Rew.bind ![] (#i :> fun x => &x.succ)).hom (codeAux (d i)))
Tactic:
simp [ihc, ihg]
State after:
no goals

State before:
k✝ k : ℕ
c : Code (k + 1)
ih : Hierarchy 𝚺 1 (codeAux c)
⊢ Hierarchy 𝚺 1 (codeAux c) ∧
    Hierarchy 𝚺 1
      (“(∀[!!(![#0, &0] 0) < !!(![#0, &0] 1)]
            ∃'
              (¬!!(![#0, ‘0’] 0) = !!(![#0, ‘0’] 1) ∧
                  !((Rew.bind ![] (#0 :> #1 :> fun x => &x.succ)).hom (codeAux c))))”)
Tactic:
simp [ih]
State after:
no goals