Theorem: LO.FirstOrder.Arith.Model.PR.Construction.cSeq_result_existsUnique (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
⊢ ∃! z, ∃ s, c.CSeq v s ∧ l + 1 = lh s ∧ ⟪l, z⟫ ∈ s
Tactic:
rcases CSeq.exists c v l with ⟨s, Hs, h⟩
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
h : l + 1 = lh s
⊢ ∃! z, ∃ s, c.CSeq v s ∧ l + 1 = lh s ∧ ⟪l, z⟫ ∈ 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
h : l + 1 = lh s
⊢ ∃! z, ∃ s, c.CSeq v s ∧ l + 1 = lh s ∧ ⟪l, z⟫ ∈ s
Tactic:
have : ∃ z, ⟪l, z⟫ ∈ s := Hs.seq.exists (show l < lh s from by simp [←h])
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
h : l + 1 = lh s
this : ∃ z, ⟪l, z⟫ ∈ s
⊢ ∃! z, ∃ s, c.CSeq v s ∧ l + 1 = lh s ∧ ⟪l, z⟫ ∈ 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
h : l + 1 = lh s
this : ∃ z, ⟪l, z⟫ ∈ s
⊢ ∃! z, ∃ s, c.CSeq v s ∧ l + 1 = lh s ∧ ⟪l, z⟫ ∈ 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
h : l + 1 = lh s
z : M
hz : ⟪l, z⟫ ∈ s
⊢ ∃! z, ∃ s, c.CSeq v s ∧ l + 1 = lh s ∧ ⟪l, z⟫ ∈ 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
h : l + 1 = lh s
z : M
hz : ⟪l, z⟫ ∈ s
⊢ ∃! z, ∃ s, c.CSeq v s ∧ l + 1 = lh s ∧ ⟪l, z⟫ ∈ s
Tactic:
exact ExistsUnique.intro z ⟨s, Hs, h, hz⟩ (by
  rintro z' ⟨s', Hs', h', hz'⟩
  exact Eq.symm <| Hs.unique Hs' (by simp [←h, ←h']) (show l < lh s from by simp [←h]) hz hz')
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
h : l + 1 = lh s
⊢ l < lh s
Tactic:
simp [←h]
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
h : l + 1 = lh s
z : M
hz : ⟪l, z⟫ ∈ s
⊢ ∀ (y : M), (∃ s, c.CSeq v s ∧ l + 1 = lh s ∧ ⟪l, y⟫ ∈ s) → y = z
Tactic:
rintro z' ⟨s', Hs', h', 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
h : l + 1 = lh s
z : M
hz : ⟪l, z⟫ ∈ s
z' s' : M
Hs' : c.CSeq v s'
h' : l + 1 = lh s'
hz' : ⟪l, z'⟫ ∈ s'
⊢ z' = z

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
h : l + 1 = lh s
z : M
hz : ⟪l, z⟫ ∈ s
z' s' : M
Hs' : c.CSeq v s'
h' : l + 1 = lh s'
hz' : ⟪l, z'⟫ ∈ s'
⊢ z' = z
Tactic:
exact Eq.symm <| Hs.unique Hs' (by simp [←h, ←h']) (show l < lh s from by simp [←h]) hz hz'
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
h : l + 1 = lh s
z : M
hz : ⟪l, z⟫ ∈ s
z' s' : M
Hs' : c.CSeq v s'
h' : l + 1 = lh s'
hz' : ⟪l, z'⟫ ∈ s'
⊢ lh s ≤ lh s'
Tactic:
simp [←h, ←h']
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
h : l + 1 = lh s
z : M
hz : ⟪l, z⟫ ∈ s
z' s' : M
Hs' : c.CSeq v s'
h' : l + 1 = lh s'
hz' : ⟪l, z'⟫ ∈ s'
⊢ l < lh s
Tactic:
simp [←h]
State after:
no goals