internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.unique
Proof 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 : M
h : c.CSeq v s
s₁ s₂ : M
H₁ : c.CSeq v s₁
H₂ : c.CSeq v s₂
h₁₂ : lh s₁ ≤ lh s₂
i : M
ih : i < lh s₁ → ∀ z₁ < s₁, ∀ z₂ < s₂, ⟪i, z₁⟫ ∈ s₁ → ⟪i, z₂⟫ ∈ s₂ → z₁ = z₂
hi : i + 1 < lh s₁
z₁ : M
hz₁ : z₁ < s₁
z₂ : M
hz₂ : z₂ < s₂
h₁ : ⟪i + 1, z₁⟫ ∈ s₁
h₂ : ⟪i + 1, z₂⟫ ∈ s₂
hi' : i < lh s₁
⊢ z₁ = z₂
Tactic:
let z' := H₁.seq.nth hi'
Proof 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
s : M
h : c.CSeq v s
s₁ s₂ : M
H₁ : c.CSeq v s₁
H₂ : c.CSeq v s₂
h₁₂ : lh s₁ ≤ lh s₂
i : M
ih : i < lh s₁ → ∀ z₁ < s₁, ∀ z₂ < s₂, ⟪i, z₁⟫ ∈ s₁ → ⟪i, z₂⟫ ∈ s₂ → z₁ = z₂
hi : i + 1 < lh s₁
z₁ : M
hz₁ : z₁ < s₁
z₂ : M
hz₂ : z₂ < s₂
h₁ : ⟪i + 1, z₁⟫ ∈ s₁
h₂ : ⟪i + 1, z₂⟫ ∈ s₂
hi' : i < lh s₁
z' : M := ⋯.nth hi'
⊢ z₁ = z₂
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.unique
Proof 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 : M
h : c.CSeq v s
s₁ s₂ : M
H₁ : c.CSeq v s₁
H₂ : c.CSeq v s₂
h₁₂ : lh s₁ ≤ lh s₂
i : M
ih : i < lh s₁ → ∀ z₁ < s₁, ∀ z₂ < s₂, ⟪i, z₁⟫ ∈ s₁ → ⟪i, z₂⟫ ∈ s₂ → z₁ = z₂
hi : i + 1 < lh s₁
z₁ : M
hz₁ : z₁ < s₁
z₂ : M
hz₂ : z₂ < s₂
h₁ : ⟪i + 1, z₁⟫ ∈ s₁
h₂ : ⟪i + 1, z₂⟫ ∈ s₂
hi' : i < lh s₁
z' : M := ⋯.nth hi'
⊢ z₁ = z₂
Tactic:
have ih₁ : ⟪i, z'⟫ ∈ s₁ := H₁.seq.nth_mem hi'
Proof 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
s : M
h : c.CSeq v s
s₁ s₂ : M
H₁ : c.CSeq v s₁
H₂ : c.CSeq v s₂
h₁₂ : lh s₁ ≤ lh s₂
i : M
ih : i < lh s₁ → ∀ z₁ < s₁, ∀ z₂ < s₂, ⟪i, z₁⟫ ∈ s₁ → ⟪i, z₂⟫ ∈ s₂ → z₁ = z₂
hi : i + 1 < lh s₁
z₁ : M
hz₁ : z₁ < s₁
z₂ : M
hz₂ : z₂ < s₂
h₁ : ⟪i + 1, z₁⟫ ∈ s₁
h₂ : ⟪i + 1, z₂⟫ ∈ s₂
hi' : i < lh s₁
z' : M := ⋯.nth hi'
ih₁ : ⟪i, z'⟫ ∈ s₁
⊢ z₁ = z₂
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.unique
Proof 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 : M
h : c.CSeq v s
s₁ s₂ : M
H₁ : c.CSeq v s₁
H₂ : c.CSeq v s₂
h₁₂ : lh s₁ ≤ lh s₂
i : M
ih : i < lh s₁ → ∀ z₁ < s₁, ∀ z₂ < s₂, ⟪i, z₁⟫ ∈ s₁ → ⟪i, z₂⟫ ∈ s₂ → z₁ = z₂
hi : i + 1 < lh s₁
z₁ : M
hz₁ : z₁ < s₁
z₂ : M
hz₂ : z₂ < s₂
h₁ : ⟪i + 1, z₁⟫ ∈ s₁
h₂ : ⟪i + 1, z₂⟫ ∈ s₂
hi' : i < lh s₁
z' : M := ⋯.nth hi'
ih₁ : ⟪i, z'⟫ ∈ s₁
⊢ z₁ = z₂
Tactic:
have ih₂ : ⟪i, z'⟫ ∈ s₂ := by
  have : z' = H₂.seq.nth (lt_of_lt_of_le hi' h₁₂) :=
    ih hi' z' (by simp [z']) (H₂.seq.nth (lt_of_lt_of_le hi' h₁₂)) (by simp [z']) (by simp [z']) (by simp)
  simp [this]
Proof 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
s : M
h : c.CSeq v s
s₁ s₂ : M
H₁ : c.CSeq v s₁
H₂ : c.CSeq v s₂
h₁₂ : lh s₁ ≤ lh s₂
i : M
ih : i < lh s₁ → ∀ z₁ < s₁, ∀ z₂ < s₂, ⟪i, z₁⟫ ∈ s₁ → ⟪i, z₂⟫ ∈ s₂ → z₁ = z₂
hi : i + 1 < lh s₁
z₁ : M
hz₁ : z₁ < s₁
z₂ : M
hz₂ : z₂ < s₂
h₁ : ⟪i + 1, z₁⟫ ∈ s₁
h₂ : ⟪i + 1, z₂⟫ ∈ s₂
hi' : i < lh s₁
z' : M := ⋯.nth hi'
ih₁ : ⟪i, z'⟫ ∈ s₁
ih₂ : ⟪i, z'⟫ ∈ s₂
⊢ z₁ = z₂
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.unique
Proof 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 : M
h : c.CSeq v s
s₁ s₂ : M
H₁ : c.CSeq v s₁
H₂ : c.CSeq v s₂
h₁₂ : lh s₁ ≤ lh s₂
i : M
ih : i < lh s₁ → ∀ z₁ < s₁, ∀ z₂ < s₂, ⟪i, z₁⟫ ∈ s₁ → ⟪i, z₂⟫ ∈ s₂ → z₁ = z₂
hi : i + 1 < lh s₁
z₁ : M
hz₁ : z₁ < s₁
z₂ : M
hz₂ : z₂ < s₂
h₁ : ⟪i + 1, z₁⟫ ∈ s₁
h₂ : ⟪i + 1, z₂⟫ ∈ s₂
hi' : i < lh s₁
z' : M := ⋯.nth hi'
ih₁ : ⟪i, z'⟫ ∈ s₁
ih₂ : ⟪i, z'⟫ ∈ s₂
⊢ z₁ = z₂
Tactic:
have h₁' : ⟪i + 1, c.succ v i z'⟫ ∈ s₁ := H₁.succ i (by simp [lt_tsub_iff_right, hi]) z' ih₁
Proof 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
s : M
h : c.CSeq v s
s₁ s₂ : M
H₁ : c.CSeq v s₁
H₂ : c.CSeq v s₂
h₁₂ : lh s₁ ≤ lh s₂
i : M
ih : i < lh s₁ → ∀ z₁ < s₁, ∀ z₂ < s₂, ⟪i, z₁⟫ ∈ s₁ → ⟪i, z₂⟫ ∈ s₂ → z₁ = z₂
hi : i + 1 < lh s₁
z₁ : M
hz₁ : z₁ < s₁
z₂ : M
hz₂ : z₂ < s₂
h₁ : ⟪i + 1, z₁⟫ ∈ s₁
h₂ : ⟪i + 1, z₂⟫ ∈ s₂
hi' : i < lh s₁
z' : M := ⋯.nth hi'
ih₁ : ⟪i, z'⟫ ∈ s₁
ih₂ : ⟪i, z'⟫ ∈ s₂
h₁' : ⟪i + 1, c.succ v i z'⟫ ∈ s₁
⊢ z₁ = z₂
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.unique
Proof 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 : M
h : c.CSeq v s
s₁ s₂ : M
H₁ : c.CSeq v s₁
H₂ : c.CSeq v s₂
h₁₂ : lh s₁ ≤ lh s₂
i : M
ih : i < lh s₁ → ∀ z₁ < s₁, ∀ z₂ < s₂, ⟪i, z₁⟫ ∈ s₁ → ⟪i, z₂⟫ ∈ s₂ → z₁ = z₂
hi : i + 1 < lh s₁
z₁ : M
hz₁ : z₁ < s₁
z₂ : M
hz₂ : z₂ < s₂
h₁ : ⟪i + 1, z₁⟫ ∈ s₁
h₂ : ⟪i + 1, z₂⟫ ∈ s₂
hi' : i < lh s₁
z' : M := ⋯.nth hi'
ih₁ : ⟪i, z'⟫ ∈ s₁
ih₂ : ⟪i, z'⟫ ∈ s₂
h₁' : ⟪i + 1, c.succ v i z'⟫ ∈ s₁
⊢ z₁ = z₂
Tactic:
have h₂' : ⟪i + 1, c.succ v i z'⟫ ∈ s₂ := H₂.succ i (by simp [lt_tsub_iff_right]; exact lt_of_lt_of_le hi h₁₂) z' ih₂
Proof 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
s : M
h : c.CSeq v s
s₁ s₂ : M
H₁ : c.CSeq v s₁
H₂ : c.CSeq v s₂
h₁₂ : lh s₁ ≤ lh s₂
i : M
ih : i < lh s₁ → ∀ z₁ < s₁, ∀ z₂ < s₂, ⟪i, z₁⟫ ∈ s₁ → ⟪i, z₂⟫ ∈ s₂ → z₁ = z₂
hi : i + 1 < lh s₁
z₁ : M
hz₁ : z₁ < s₁
z₂ : M
hz₂ : z₂ < s₂
h₁ : ⟪i + 1, z₁⟫ ∈ s₁
h₂ : ⟪i + 1, z₂⟫ ∈ s₂
hi' : i < lh s₁
z' : M := ⋯.nth hi'
ih₁ : ⟪i, z'⟫ ∈ s₁
ih₂ : ⟪i, z'⟫ ∈ s₂
h₁' : ⟪i + 1, c.succ v i z'⟫ ∈ s₁
h₂' : ⟪i + 1, c.succ v i z'⟫ ∈ s₂
⊢ z₁ = z₂
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.unique
Proof 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 : M
h : c.CSeq v s
s₁ s₂ : M
H₁ : c.CSeq v s₁
H₂ : c.CSeq v s₂
h₁₂ : lh s₁ ≤ lh s₂
i : M
ih : i < lh s₁ → ∀ z₁ < s₁, ∀ z₂ < s₂, ⟪i, z₁⟫ ∈ s₁ → ⟪i, z₂⟫ ∈ s₂ → z₁ = z₂
hi : i + 1 < lh s₁
z₁ : M
hz₁ : z₁ < s₁
z₂ : M
hz₂ : z₂ < s₂
h₁ : ⟪i + 1, z₁⟫ ∈ s₁
h₂ : ⟪i + 1, z₂⟫ ∈ s₂
hi' : i < lh s₁
z' : M := ⋯.nth hi'
ih₁ : ⟪i, z'⟫ ∈ s₁
ih₂ : ⟪i, z'⟫ ∈ s₂
h₁' : ⟪i + 1, c.succ v i z'⟫ ∈ s₁
h₂' : ⟪i + 1, c.succ v i z'⟫ ∈ s₂
⊢ z₁ = z₂
Tactic:
have e₁ : z₁ = c.succ v i z' := H₁.seq.isMapping.uniq h₁ h₁'
Proof 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
s : M
h : c.CSeq v s
s₁ s₂ : M
H₁ : c.CSeq v s₁
H₂ : c.CSeq v s₂
h₁₂ : lh s₁ ≤ lh s₂
i : M
ih : i < lh s₁ → ∀ z₁ < s₁, ∀ z₂ < s₂, ⟪i, z₁⟫ ∈ s₁ → ⟪i, z₂⟫ ∈ s₂ → z₁ = z₂
hi : i + 1 < lh s₁
z₁ : M
hz₁ : z₁ < s₁
z₂ : M
hz₂ : z₂ < s₂
h₁ : ⟪i + 1, z₁⟫ ∈ s₁
h₂ : ⟪i + 1, z₂⟫ ∈ s₂
hi' : i < lh s₁
z' : M := ⋯.nth hi'
ih₁ : ⟪i, z'⟫ ∈ s₁
ih₂ : ⟪i, z'⟫ ∈ s₂
h₁' : ⟪i + 1, c.succ v i z'⟫ ∈ s₁
h₂' : ⟪i + 1, c.succ v i z'⟫ ∈ s₂
e₁ : z₁ = c.succ v i z'
⊢ z₁ = z₂
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.unique
Proof 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 : M
h : c.CSeq v s
s₁ s₂ : M
H₁ : c.CSeq v s₁
H₂ : c.CSeq v s₂
h₁₂ : lh s₁ ≤ lh s₂
i : M
ih : i < lh s₁ → ∀ z₁ < s₁, ∀ z₂ < s₂, ⟪i, z₁⟫ ∈ s₁ → ⟪i, z₂⟫ ∈ s₂ → z₁ = z₂
hi : i + 1 < lh s₁
z₁ : M
hz₁ : z₁ < s₁
z₂ : M
hz₂ : z₂ < s₂
h₁ : ⟪i + 1, z₁⟫ ∈ s₁
h₂ : ⟪i + 1, z₂⟫ ∈ s₂
hi' : i < lh s₁
z' : M := ⋯.nth hi'
ih₁ : ⟪i, z'⟫ ∈ s₁
ih₂ : ⟪i, z'⟫ ∈ s₂
h₁' : ⟪i + 1, c.succ v i z'⟫ ∈ s₁
h₂' : ⟪i + 1, c.succ v i z'⟫ ∈ s₂
e₁ : z₁ = c.succ v i z'
⊢ z₁ = z₂
Tactic:
have e₂ : z₂ = c.succ v i z' := H₂.seq.isMapping.uniq h₂ h₂'
Proof 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
s : M
h : c.CSeq v s
s₁ s₂ : M
H₁ : c.CSeq v s₁
H₂ : c.CSeq v s₂
h₁₂ : lh s₁ ≤ lh s₂
i : M
ih : i < lh s₁ → ∀ z₁ < s₁, ∀ z₂ < s₂, ⟪i, z₁⟫ ∈ s₁ → ⟪i, z₂⟫ ∈ s₂ → z₁ = z₂
hi : i + 1 < lh s₁
z₁ : M
hz₁ : z₁ < s₁
z₂ : M
hz₂ : z₂ < s₂
h₁ : ⟪i + 1, z₁⟫ ∈ s₁
h₂ : ⟪i + 1, z₂⟫ ∈ s₂
hi' : i < lh s₁
z' : M := ⋯.nth hi'
ih₁ : ⟪i, z'⟫ ∈ s₁
ih₂ : ⟪i, z'⟫ ∈ s₂
h₁' : ⟪i + 1, c.succ v i z'⟫ ∈ s₁
h₂' : ⟪i + 1, c.succ v i z'⟫ ∈ s₂
e₁ : z₁ = c.succ v i z'
e₂ : z₂ = c.succ v i z'
⊢ z₁ = z₂
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.unique
Proof 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 : M
h : c.CSeq v s
s₁ s₂ : M
H₁ : c.CSeq v s₁
H₂ : c.CSeq v s₂
h₁₂ : lh s₁ ≤ lh s₂
i : M
ih : i < lh s₁ → ∀ z₁ < s₁, ∀ z₂ < s₂, ⟪i, z₁⟫ ∈ s₁ → ⟪i, z₂⟫ ∈ s₂ → z₁ = z₂
hi : i + 1 < lh s₁
z₁ : M
hz₁ : z₁ < s₁
z₂ : M
hz₂ : z₂ < s₂
h₁ : ⟪i + 1, z₁⟫ ∈ s₁
h₂ : ⟪i + 1, z₂⟫ ∈ s₂
hi' : i < lh s₁
z' : M := ⋯.nth hi'
ih₁ : ⟪i, z'⟫ ∈ s₁
ih₂ : ⟪i, z'⟫ ∈ s₂
h₁' : ⟪i + 1, c.succ v i z'⟫ ∈ s₁
h₂' : ⟪i + 1, c.succ v i z'⟫ ∈ s₂
e₁ : z₁ = c.succ v i z'
e₂ : z₂ = c.succ v i z'
⊢ z₁ = z₂
Tactic:
simp [e₁, e₂]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.unique
Proof 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 : M
h : c.CSeq v s
s₁ s₂ : M
H₁ : c.CSeq v s₁
H₂ : c.CSeq v s₂
h₁₂ : lh s₁ ≤ lh s₂
i : M
ih : i < lh s₁ → ∀ z₁ < s₁, ∀ z₂ < s₂, ⟪i, z₁⟫ ∈ s₁ → ⟪i, z₂⟫ ∈ s₂ → z₁ = z₂
hi : i + 1 < lh s₁
z₁ : M
hz₁ : z₁ < s₁
z₂ : M
hz₂ : z₂ < s₂
h₁ : ⟪i + 1, z₁⟫ ∈ s₁
h₂ : ⟪i + 1, z₂⟫ ∈ s₂
⊢ i ≤ i + 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.unique
Proof 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 : M
h : c.CSeq v s
s₁ s₂ : M
H₁ : c.CSeq v s₁
H₂ : c.CSeq v s₂
h₁₂ : lh s₁ ≤ lh s₂
i : M
ih : i < lh s₁ → ∀ z₁ < s₁, ∀ z₂ < s₂, ⟪i, z₁⟫ ∈ s₁ → ⟪i, z₂⟫ ∈ s₂ → z₁ = z₂
hi : i + 1 < lh s₁
z₁ : M
hz₁ : z₁ < s₁
z₂ : M
hz₂ : z₂ < s₂
h₁ : ⟪i + 1, z₁⟫ ∈ s₁
h₂ : ⟪i + 1, z₂⟫ ∈ s₂
hi' : i < lh s₁
z' : M := ⋯.nth hi'
ih₁ : ⟪i, z'⟫ ∈ s₁
⊢ ⟪i, z'⟫ ∈ s₂
Tactic:
have : z' = H₂.seq.nth (lt_of_lt_of_le hi' h₁₂) :=
  ih hi' z' (by simp [z']) (H₂.seq.nth (lt_of_lt_of_le hi' h₁₂)) (by simp [z']) (by simp [z']) (by simp)
Proof 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
s : M
h : c.CSeq v s
s₁ s₂ : M
H₁ : c.CSeq v s₁
H₂ : c.CSeq v s₂
h₁₂ : lh s₁ ≤ lh s₂
i : M
ih : i < lh s₁ → ∀ z₁ < s₁, ∀ z₂ < s₂, ⟪i, z₁⟫ ∈ s₁ → ⟪i, z₂⟫ ∈ s₂ → z₁ = z₂
hi : i + 1 < lh s₁
z₁ : M
hz₁ : z₁ < s₁
z₂ : M
hz₂ : z₂ < s₂
h₁ : ⟪i + 1, z₁⟫ ∈ s₁
h₂ : ⟪i + 1, z₂⟫ ∈ s₂
hi' : i < lh s₁
z' : M := ⋯.nth hi'
ih₁ : ⟪i, z'⟫ ∈ s₁
this : z' = ⋯.nth ⋯
⊢ ⟪i, z'⟫ ∈ s₂
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.unique
Proof 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 : M
h : c.CSeq v s
s₁ s₂ : M
H₁ : c.CSeq v s₁
H₂ : c.CSeq v s₂
h₁₂ : lh s₁ ≤ lh s₂
i : M
ih : i < lh s₁ → ∀ z₁ < s₁, ∀ z₂ < s₂, ⟪i, z₁⟫ ∈ s₁ → ⟪i, z₂⟫ ∈ s₂ → z₁ = z₂
hi : i + 1 < lh s₁
z₁ : M
hz₁ : z₁ < s₁
z₂ : M
hz₂ : z₂ < s₂
h₁ : ⟪i + 1, z₁⟫ ∈ s₁
h₂ : ⟪i + 1, z₂⟫ ∈ s₂
hi' : i < lh s₁
z' : M := ⋯.nth hi'
ih₁ : ⟪i, z'⟫ ∈ s₁
this : z' = ⋯.nth ⋯
⊢ ⟪i, z'⟫ ∈ s₂
Tactic:
simp [this]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.unique
Proof 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 : M
h : c.CSeq v s
s₁ s₂ : M
H₁ : c.CSeq v s₁
H₂ : c.CSeq v s₂
h₁₂ : lh s₁ ≤ lh s₂
i : M
ih : i < lh s₁ → ∀ z₁ < s₁, ∀ z₂ < s₂, ⟪i, z₁⟫ ∈ s₁ → ⟪i, z₂⟫ ∈ s₂ → z₁ = z₂
hi : i + 1 < lh s₁
z₁ : M
hz₁ : z₁ < s₁
z₂ : M
hz₂ : z₂ < s₂
h₁ : ⟪i + 1, z₁⟫ ∈ s₁
h₂ : ⟪i + 1, z₂⟫ ∈ s₂
hi' : i < lh s₁
z' : M := ⋯.nth hi'
ih₁ : ⟪i, z'⟫ ∈ s₁
⊢ z' < s₁
Tactic:
simp [z']
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.unique
Proof 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 : M
h : c.CSeq v s
s₁ s₂ : M
H₁ : c.CSeq v s₁
H₂ : c.CSeq v s₂
h₁₂ : lh s₁ ≤ lh s₂
i : M
ih : i < lh s₁ → ∀ z₁ < s₁, ∀ z₂ < s₂, ⟪i, z₁⟫ ∈ s₁ → ⟪i, z₂⟫ ∈ s₂ → z₁ = z₂
hi : i + 1 < lh s₁
z₁ : M
hz₁ : z₁ < s₁
z₂ : M
hz₂ : z₂ < s₂
h₁ : ⟪i + 1, z₁⟫ ∈ s₁
h₂ : ⟪i + 1, z₂⟫ ∈ s₂
hi' : i < lh s₁
z' : M := ⋯.nth hi'
ih₁ : ⟪i, z'⟫ ∈ s₁
⊢ ⋯.nth ⋯ < s₂
Tactic:
simp [z']
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.unique
Proof 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 : M
h : c.CSeq v s
s₁ s₂ : M
H₁ : c.CSeq v s₁
H₂ : c.CSeq v s₂
h₁₂ : lh s₁ ≤ lh s₂
i : M
ih : i < lh s₁ → ∀ z₁ < s₁, ∀ z₂ < s₂, ⟪i, z₁⟫ ∈ s₁ → ⟪i, z₂⟫ ∈ s₂ → z₁ = z₂
hi : i + 1 < lh s₁
z₁ : M
hz₁ : z₁ < s₁
z₂ : M
hz₂ : z₂ < s₂
h₁ : ⟪i + 1, z₁⟫ ∈ s₁
h₂ : ⟪i + 1, z₂⟫ ∈ s₂
hi' : i < lh s₁
z' : M := ⋯.nth hi'
ih₁ : ⟪i, z'⟫ ∈ s₁
⊢ ⟪i, z'⟫ ∈ s₁
Tactic:
simp [z']
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.unique
Proof 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 : M
h : c.CSeq v s
s₁ s₂ : M
H₁ : c.CSeq v s₁
H₂ : c.CSeq v s₂
h₁₂ : lh s₁ ≤ lh s₂
i : M
ih : i < lh s₁ → ∀ z₁ < s₁, ∀ z₂ < s₂, ⟪i, z₁⟫ ∈ s₁ → ⟪i, z₂⟫ ∈ s₂ → z₁ = z₂
hi : i + 1 < lh s₁
z₁ : M
hz₁ : z₁ < s₁
z₂ : M
hz₂ : z₂ < s₂
h₁ : ⟪i + 1, z₁⟫ ∈ s₁
h₂ : ⟪i + 1, z₂⟫ ∈ s₂
hi' : i < lh s₁
z' : M := ⋯.nth hi'
ih₁ : ⟪i, z'⟫ ∈ s₁
⊢ ⟪i, ⋯.nth ⋯⟫ ∈ s₂
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.unique
Proof 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 : M
h : c.CSeq v s
s₁ s₂ : M
H₁ : c.CSeq v s₁
H₂ : c.CSeq v s₂
h₁₂ : lh s₁ ≤ lh s₂
i : M
ih : i < lh s₁ → ∀ z₁ < s₁, ∀ z₂ < s₂, ⟪i, z₁⟫ ∈ s₁ → ⟪i, z₂⟫ ∈ s₂ → z₁ = z₂
hi : i + 1 < lh s₁
z₁ : M
hz₁ : z₁ < s₁
z₂ : M
hz₂ : z₂ < s₂
h₁ : ⟪i + 1, z₁⟫ ∈ s₁
h₂ : ⟪i + 1, z₂⟫ ∈ s₂
hi' : i < lh s₁
z' : M := ⋯.nth hi'
ih₁ : ⟪i, z'⟫ ∈ s₁
ih₂ : ⟪i, z'⟫ ∈ s₂
⊢ i < lh s₁ - 1
Tactic:
simp [lt_tsub_iff_right, hi]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.unique
Proof 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 : M
h : c.CSeq v s
s₁ s₂ : M
H₁ : c.CSeq v s₁
H₂ : c.CSeq v s₂
h₁₂ : lh s₁ ≤ lh s₂
i : M
ih : i < lh s₁ → ∀ z₁ < s₁, ∀ z₂ < s₂, ⟪i, z₁⟫ ∈ s₁ → ⟪i, z₂⟫ ∈ s₂ → z₁ = z₂
hi : i + 1 < lh s₁
z₁ : M
hz₁ : z₁ < s₁
z₂ : M
hz₂ : z₂ < s₂
h₁ : ⟪i + 1, z₁⟫ ∈ s₁
h₂ : ⟪i + 1, z₂⟫ ∈ s₂
hi' : i < lh s₁
z' : M := ⋯.nth hi'
ih₁ : ⟪i, z'⟫ ∈ s₁
ih₂ : ⟪i, z'⟫ ∈ s₂
h₁' : ⟪i + 1, c.succ v i z'⟫ ∈ s₁
⊢ i < lh s₂ - 1
Tactic:
simp [lt_tsub_iff_right]
Proof 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
s : M
h : c.CSeq v s
s₁ s₂ : M
H₁ : c.CSeq v s₁
H₂ : c.CSeq v s₂
h₁₂ : lh s₁ ≤ lh s₂
i : M
ih : i < lh s₁ → ∀ z₁ < s₁, ∀ z₂ < s₂, ⟪i, z₁⟫ ∈ s₁ → ⟪i, z₂⟫ ∈ s₂ → z₁ = z₂
hi : i + 1 < lh s₁
z₁ : M
hz₁ : z₁ < s₁
z₂ : M
hz₂ : z₂ < s₂
h₁ : ⟪i + 1, z₁⟫ ∈ s₁
h₂ : ⟪i + 1, z₂⟫ ∈ s₂
hi' : i < lh s₁
z' : M := ⋯.nth hi'
ih₁ : ⟪i, z'⟫ ∈ s₁
ih₂ : ⟪i, z'⟫ ∈ s₂
h₁' : ⟪i + 1, c.succ v i z'⟫ ∈ s₁
⊢ i + 1 < lh s₂
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.unique
Proof 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 : M
h : c.CSeq v s
s₁ s₂ : M
H₁ : c.CSeq v s₁
H₂ : c.CSeq v s₂
h₁₂ : lh s₁ ≤ lh s₂
i : M
ih : i < lh s₁ → ∀ z₁ < s₁, ∀ z₂ < s₂, ⟪i, z₁⟫ ∈ s₁ → ⟪i, z₂⟫ ∈ s₂ → z₁ = z₂
hi : i + 1 < lh s₁
z₁ : M
hz₁ : z₁ < s₁
z₂ : M
hz₂ : z₂ < s₂
h₁ : ⟪i + 1, z₁⟫ ∈ s₁
h₂ : ⟪i + 1, z₂⟫ ∈ s₂
hi' : i < lh s₁
z' : M := ⋯.nth hi'
ih₁ : ⟪i, z'⟫ ∈ s₁
ih₂ : ⟪i, z'⟫ ∈ s₂
h₁' : ⟪i + 1, c.succ v i z'⟫ ∈ s₁
⊢ i + 1 < lh s₂
Tactic:
exact lt_of_lt_of_le hi h₁₂
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.initial
Proof 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
⊢ Seq (∅ ⁀' c.zero v)
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.initial
Proof 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, c.zero v⟫ ∈ ∅ ⁀' c.zero v
Tactic:
simp [seqCons]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.initial
Proof 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
⊢ ∀ i < lh (∅ ⁀' c.zero v) - 1, ∀ (z : M), ⟪i, z⟫ ∈ ∅ ⁀' c.zero v → ⟪i + 1, c.succ v i z⟫ ∈ ∅ ⁀' c.zero v
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.successor
Proof 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 l z : M
Hs : c.CSeq v s
hl : l + 1 = lh s
hz : ⟪l, z⟫ ∈ s
⊢ ⟪0, c.zero v⟫ ∈ s ⁀' c.succ v l z
Tactic:
simp [seqCons, Hs.zero]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.successor
Proof 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 l z : M
Hs : c.CSeq v s
hl : l + 1 = lh s
hz : ⟪l, z⟫ ∈ s
⊢ ∀ i < lh (s ⁀' c.succ v l z) - 1,
    ∀ (z_1 : M), ⟪i, z_1⟫ ∈ s ⁀' c.succ v l z → ⟪i + 1, c.succ v i z_1⟫ ∈ s ⁀' c.succ v l z
Tactic:
simp [Hs.seq.lh_seqCons]
Proof 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
s l z : M
Hs : c.CSeq v s
hl : l + 1 = lh s
hz : ⟪l, z⟫ ∈ s
⊢ ∀ i < lh s, ∀ (z_1 : M), ⟪i, z_1⟫ ∈ s ⁀' c.succ v l z → ⟪i + 1, c.succ v i z_1⟫ ∈ s ⁀' c.succ v l z
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.successor
Proof 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 l z : M
Hs : c.CSeq v s
hl : l + 1 = lh s
hz : ⟪l, z⟫ ∈ s
⊢ ∀ i < lh s, ∀ (z_1 : M), ⟪i, z_1⟫ ∈ s ⁀' c.succ v l z → ⟪i + 1, c.succ v i z_1⟫ ∈ s ⁀' c.succ v l z
Tactic:
intro i hi w hiw
Proof 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
s l z : M
Hs : c.CSeq v s
hl : l + 1 = lh s
hz : ⟪l, z⟫ ∈ s
i : M
hi : i < lh s
w : M
hiw : ⟪i, w⟫ ∈ s ⁀' c.succ v l z
⊢ ⟪i + 1, c.succ v i w⟫ ∈ s ⁀' c.succ v l z
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.successor
Proof 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 l z : M
Hs : c.CSeq v s
hl : l + 1 = lh s
hz : ⟪l, z⟫ ∈ s
i : M
hi : i < lh s
w : M
hiw : ⟪i, w⟫ ∈ s ⁀' c.succ v l z
hiws : ⟪i, w⟫ ∈ s
⊢ ⟪i + 1, c.succ v i w⟫ ∈ s ⁀' c.succ v l z
Tactic:
have : i ≤ l := by simpa [←hl, lt_succ_iff_le] using hi
Proof 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
s l z : M
Hs : c.CSeq v s
hl : l + 1 = lh s
hz : ⟪l, z⟫ ∈ s
i : M
hi : i < lh s
w : M
hiw : ⟪i, w⟫ ∈ s ⁀' c.succ v l z
hiws : ⟪i, w⟫ ∈ s
this : i ≤ l
⊢ ⟪i + 1, c.succ v i w⟫ ∈ s ⁀' c.succ v l z
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.successor
Proof 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 l z : M
Hs : c.CSeq v s
hl : l + 1 = lh s
hz : ⟪l, z⟫ ∈ s
i : M
hi : i < lh s
w : M
hiw : ⟪i, w⟫ ∈ s ⁀' c.succ v l z
hiws : ⟪i, w⟫ ∈ s
this : i ≤ l
⊢ ⟪i + 1, c.succ v i w⟫ ∈ s ⁀' c.succ v l z
Tactic:
rcases this with (rfl | hil)
Proof state after:
case inl
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 z : M
Hs : c.CSeq v s
i : M
hi : i < lh s
w : M
hiws : ⟪i, w⟫ ∈ s
hl : i + 1 = lh s
hz : ⟪i, z⟫ ∈ s
hiw : ⟪i, w⟫ ∈ s ⁀' c.succ v i z
⊢ ⟪i + 1, c.succ v i w⟫ ∈ s ⁀' c.succ v i z

case inr
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 l z : M
Hs : c.CSeq v s
hl : l + 1 = lh s
hz : ⟪l, z⟫ ∈ s
i : M
hi : i < lh s
w : M
hiw : ⟪i, w⟫ ∈ s ⁀' c.succ v l z
hiws : ⟪i, w⟫ ∈ s
hil : i < l
⊢ ⟪i + 1, c.succ v i w⟫ ∈ s ⁀' c.succ v l z
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.successor
Proof 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 l z : M
Hs : c.CSeq v s
hl : l + 1 = lh s
hz : ⟪l, z⟫ ∈ s
i : M
hi : i < lh s
w : M
hiw : ⟪i, w⟫ ∈ s ⁀' c.succ v l z
⊢ ⟪i, w⟫ ∈ s
Tactic:
simp [mem_seqCons_iff] at hiw
Proof 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
s l z : M
Hs : c.CSeq v s
hl : l + 1 = lh s
hz : ⟪l, z⟫ ∈ s
i : M
hi : i < lh s
w : M
hiw : i = lh s ∧ w = c.succ v l z ∨ ⟪i, w⟫ ∈ s
⊢ ⟪i, w⟫ ∈ s
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.successor
Proof 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 l z : M
Hs : c.CSeq v s
hl : l + 1 = lh s
hz : ⟪l, z⟫ ∈ s
i : M
hi : i < lh s
w : M
hiw : i = lh s ∧ w = c.succ v l z ∨ ⟪i, w⟫ ∈ s
⊢ ⟪i, w⟫ ∈ s
Tactic:
rcases hiw with (⟨rfl, rfl⟩ | h)
Proof state after:
case inl.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
s l z : M
Hs : c.CSeq v s
hl : l + 1 = lh s
hz : ⟪l, z⟫ ∈ s
hi : lh s < lh s
⊢ ⟪lh s, c.succ v l z⟫ ∈ s

case inr
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 l z : M
Hs : c.CSeq v s
hl : l + 1 = lh s
hz : ⟪l, z⟫ ∈ s
i : M
hi : i < lh s
w : M
h : ⟪i, w⟫ ∈ s
⊢ ⟪i, w⟫ ∈ s