Theorem: LO.FirstOrder.Arith.Model.PR.Construction.result_graph (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
z u : M
⊢ z = c.result v u → ∃ s, c.CSeq v s ∧ ⟪u, z⟫ ∈ s
Tactic:
rintro rfl
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
u : M
⊢ ∃ s, c.CSeq v s ∧ ⟪u, c.result v u⟫ ∈ 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
u : M
⊢ ∃ s, c.CSeq v s ∧ ⟪u, c.result v u⟫ ∈ s
Tactic:
rcases c.result_spec v u with ⟨s, Hs, _, h⟩
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
u s : M
Hs : c.CSeq v s
left✝ : u + 1 = lh s
h : ⟪u, c.result v u⟫ ∈ s
⊢ ∃ s, c.CSeq v s ∧ ⟪u, c.result v u⟫ ∈ 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
u s : M
Hs : c.CSeq v s
left✝ : u + 1 = lh s
h : ⟪u, c.result v u⟫ ∈ s
⊢ ∃ s, c.CSeq v s ∧ ⟪u, c.result v u⟫ ∈ s
Tactic:
exact ⟨s, Hs, 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
z u : M
⊢ (∃ s, c.CSeq v s ∧ ⟪u, z⟫ ∈ s) → z = c.result v u
Tactic:
rintro ⟨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
z u s : M
Hs : c.CSeq v s
h : ⟪u, z⟫ ∈ s
⊢ z = c.result v u

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
z u s : M
Hs : c.CSeq v s
h : ⟪u, z⟫ ∈ s
⊢ z = c.result v u
Tactic:
rcases c.result_spec v u with ⟨s', Hs', hu, h'⟩
State after:
case intro.intro.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
z u s : M
Hs : c.CSeq v s
h : ⟪u, z⟫ ∈ s
s' : M
Hs' : c.CSeq v s'
hu : u + 1 = lh s'
h' : ⟪u, c.result v u⟫ ∈ s'
⊢ z = c.result v u

State before:
case intro.intro.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
z u s : M
Hs : c.CSeq v s
h : ⟪u, z⟫ ∈ s
s' : M
Hs' : c.CSeq v s'
hu : u + 1 = lh s'
h' : ⟪u, c.result v u⟫ ∈ s'
⊢ z = c.result v u
Tactic:
exact Eq.symm <| Hs'.unique Hs
  (by simp [←hu, succ_le_iff_lt]; exact Hs.seq.lt_lh_iff.mpr (mem_domain_of_pair_mem h))
  (by simp [←hu]) 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
z u s : M
Hs : c.CSeq v s
h : ⟪u, z⟫ ∈ s
s' : M
Hs' : c.CSeq v s'
hu : u + 1 = lh s'
h' : ⟪u, c.result v u⟫ ∈ s'
⊢ lh s' ≤ lh s
Tactic:
simp [←hu, succ_le_iff_lt]
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
z u s : M
Hs : c.CSeq v s
h : ⟪u, z⟫ ∈ s
s' : M
Hs' : c.CSeq v s'
hu : u + 1 = lh s'
h' : ⟪u, c.result v u⟫ ∈ s'
⊢ u < 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
z u s : M
Hs : c.CSeq v s
h : ⟪u, z⟫ ∈ s
s' : M
Hs' : c.CSeq v s'
hu : u + 1 = lh s'
h' : ⟪u, c.result v u⟫ ∈ s'
⊢ u < lh s
Tactic:
exact Hs.seq.lt_lh_iff.mpr (mem_domain_of_pair_mem 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
z u s : M
Hs : c.CSeq v s
h : ⟪u, z⟫ ∈ s
s' : M
Hs' : c.CSeq v s'
hu : u + 1 = lh s'
h' : ⟪u, c.result v u⟫ ∈ s'
⊢ u < lh s'
Tactic:
simp [←hu]
State after:
no goals