Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.exists (Arithmetization/ISigmaOne/HFS/PRF.lean)

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
p : Formulae k
c : Construction M p
v : Fin k → M
l : M
⊢ ∃ s, c.CSeq v s ∧ l + 1 = lh s
Tactic:
induction l using induction_iSigmaOne
State after:
case hP
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
p : Formulae k
c : Construction M p
v : Fin k → M
⊢ 𝚺₁-Predicate fun l => ∃ s, c.CSeq v s ∧ l + 1 = lh s

case zero
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
p : Formulae k
c : Construction M p
v : Fin k → M
⊢ ∃ s, c.CSeq v s ∧ 0 + 1 = lh s

case succ
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
p : Formulae k
c : Construction M p
v : Fin k → M
x✝ : M
a✝ : ∃ s, c.CSeq v s ∧ x✝ + 1 = lh s
⊢ ∃ s, c.CSeq v s ∧ x✝ + 1 + 1 = lh s

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
p : Formulae k
c : Construction M p
v : Fin k → M
⊢ ∃ s, c.CSeq v s ∧ 0 + 1 = lh s
Tactic:
case zero =>
  exact ⟨!⟨c.zero v⟩, CSeq.initial, by simp⟩
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
p : Formulae k
c : Construction M p
v : Fin k → M
l : M
ih : ∃ s, c.CSeq v s ∧ l + 1 = lh s
⊢ ∃ s, c.CSeq v s ∧ l + 1 + 1 = lh s
Tactic:
case succ l ih =>
  rcases ih with ⟨s, Hs, hls⟩
  have hl : l < lh s := by simp [←hls]
  have : ∃ z, ⟪l, z⟫ ∈ s := Hs.seq.exists hl
  rcases this with ⟨z, hz⟩
  exact ⟨s ⁀' c.succ v l z, Hs.successor hls hz, by simp [Hs.seq, hls]⟩
State after:
no goals

State before:
case hP
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
p : Formulae k
c : Construction M p
v : Fin k → M
⊢ 𝚺₁-Predicate fun l => ∃ s, c.CSeq v s ∧ l + 1 = lh s
Tactic:
apply Definable.ex
State after:
case hP.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
p : Formulae k
c : Construction M p
v : Fin k → M
⊢ Definable ℒₒᵣ (𝚺, 0 + 1) fun w => c.CSeq v (w 0) ∧ (fun x => w x.succ) 0 + 1 = lh (w 0)

State before:
case hP.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
p : Formulae k
c : Construction M p
v : Fin k → M
⊢ Definable ℒₒᵣ (𝚺, 0 + 1) fun w => c.CSeq v (w 0) ∧ (fun x => w x.succ) 0 + 1 = lh (w 0)
Tactic:
apply Definable.and
State after:
case hP.h.h₁
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
p : Formulae k
c : Construction M p
v : Fin k → M
⊢ Definable ℒₒᵣ (𝚺, 0 + 1) fun v_1 => c.CSeq v (v_1 0)

case hP.h.h₂
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
p : Formulae k
c : Construction M p
v : Fin k → M
⊢ Definable ℒₒᵣ (𝚺, 0 + 1) fun v => (fun x => v x.succ) 0 + 1 = lh (v 0)

State before:
case hP.h.h₁
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
p : Formulae k
c : Construction M p
v : Fin k → M
⊢ Definable ℒₒᵣ (𝚺, 0 + 1) fun v_1 => c.CSeq v (v_1 0)
Tactic:
exact ⟨p.cseqDef.rew (Rew.embSubsts <| #0 :> fun i ↦ &(v i)), by
  intro w; simpa using c.cseq_defined_iff (w 0 :> v) |>.symm⟩
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
p : Formulae k
c : Construction M p
v : Fin k → M
⊢ DefinedWithParam (fun v_1 => c.CSeq v (v_1 0)) (HSemiformula.rew (Rew.embSubsts (#0 :> fun i => &(v i))) p.cseqDef)
Tactic:
intro w
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
p : Formulae k
c : Construction M p
v : Fin k → M
w : Fin (Nat.succ 1) → M
⊢ (fun v_1 => c.CSeq v (v_1 0)) w ↔
    (Semiformula.Evalm M w id) (HSemiformula.rew (Rew.embSubsts (#0 :> fun i => &(v i))) p.cseqDef).val

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
p : Formulae k
c : Construction M p
v : Fin k → M
w : Fin (Nat.succ 1) → M
⊢ (fun v_1 => c.CSeq v (v_1 0)) w ↔
    (Semiformula.Evalm M w id) (HSemiformula.rew (Rew.embSubsts (#0 :> fun i => &(v i))) p.cseqDef).val
Tactic:
simpa using c.cseq_defined_iff (w 0 :> v) |>.symm
State after:
no goals

State before:
case hP.h.h₂
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
p : Formulae k
c : Construction M p
v : Fin k → M
⊢ Definable ℒₒᵣ (𝚺, 0 + 1) fun v => (fun x => v x.succ) 0 + 1 = lh (v 0)
Tactic:
definability
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
p : Formulae k
c : Construction M p
v : Fin k → M
⊢ ∃ s, c.CSeq v s ∧ 0 + 1 = lh s
Tactic:
exact ⟨!⟨c.zero v⟩, CSeq.initial, by simp⟩
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
p : Formulae k
c : Construction M p
v : Fin k → M
⊢ 0 + 1 = lh (∅ ⁀' c.zero v)
Tactic:
simp
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
p : Formulae k
c : Construction M p
v : Fin k → M
l : M
ih : ∃ s, c.CSeq v s ∧ l + 1 = lh s
⊢ ∃ s, c.CSeq v s ∧ l + 1 + 1 = lh s
Tactic:
rcases ih with ⟨s, Hs, hls⟩
State after:
case intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
p : Formulae k
c : Construction M p
v : Fin k → M
l s : M
Hs : c.CSeq v s
hls : l + 1 = lh s
⊢ ∃ s, c.CSeq v s ∧ l + 1 + 1 = lh s

State before:
case intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
p : Formulae k
c : Construction M p
v : Fin k → M
l s : M
Hs : c.CSeq v s
hls : l + 1 = lh s
⊢ ∃ s, c.CSeq v s ∧ l + 1 + 1 = lh s
Tactic:
have hl : l < lh s := by simp [←hls]
State after:
case intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
p : Formulae k
c : Construction M p
v : Fin k → M
l s : M
Hs : c.CSeq v s
hls : l + 1 = lh s
hl : l < lh s
⊢ ∃ s, c.CSeq v s ∧ l + 1 + 1 = lh s

State before:
case intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
p : Formulae k
c : Construction M p
v : Fin k → M
l s : M
Hs : c.CSeq v s
hls : l + 1 = lh s
hl : l < lh s
⊢ ∃ s, c.CSeq v s ∧ l + 1 + 1 = lh s
Tactic:
have : ∃ z, ⟪l, z⟫ ∈ s := Hs.seq.exists hl
State after:
case intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
p : Formulae k
c : Construction M p
v : Fin k → M
l s : M
Hs : c.CSeq v s
hls : l + 1 = lh s
hl : l < lh s
this : ∃ z, ⟪l, z⟫ ∈ s
⊢ ∃ s, c.CSeq v s ∧ l + 1 + 1 = lh s

State before:
case intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
p : Formulae k
c : Construction M p
v : Fin k → M
l s : M
Hs : c.CSeq v s
hls : l + 1 = lh s
hl : l < lh s
this : ∃ z, ⟪l, z⟫ ∈ s
⊢ ∃ s, c.CSeq v s ∧ l + 1 + 1 = lh s
Tactic:
rcases this with ⟨z, hz⟩
State after:
case intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
p : Formulae k
c : Construction M p
v : Fin k → M
l s : M
Hs : c.CSeq v s
hls : l + 1 = lh s
hl : l < lh s
z : M
hz : ⟪l, z⟫ ∈ s
⊢ ∃ s, c.CSeq v s ∧ l + 1 + 1 = lh s

State before:
case intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
p : Formulae k
c : Construction M p
v : Fin k → M
l s : M
Hs : c.CSeq v s
hls : l + 1 = lh s
hl : l < lh s
z : M
hz : ⟪l, z⟫ ∈ s
⊢ ∃ s, c.CSeq v s ∧ l + 1 + 1 = lh s
Tactic:
exact ⟨s ⁀' c.succ v l z, Hs.successor hls hz, by simp [Hs.seq, hls]⟩
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
p : Formulae k
c : Construction M p
v : Fin k → M
l s : M
Hs : c.CSeq v s
hls : l + 1 = lh s
⊢ l < lh s
Tactic:
simp [←hls]
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
p : Formulae k
c : Construction M p
v : Fin k → M
l s : M
Hs : c.CSeq v s
hls : l + 1 = lh s
hl : l < lh s
z : M
hz : ⟪l, z⟫ ∈ s
⊢ l + 1 + 1 = lh (s ⁀' c.succ v l z)
Tactic:
simp [Hs.seq, hls]
State after:
no goals