internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.successor
Proof state before:
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
Tactic:
simp at hi
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.successor
Proof state before:
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
Tactic:
assumption
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 : M
hi : i < lh s
w : M
hiw : ⟪i, w⟫ ∈ s ⁀' c.succ v l z
hiws : ⟪i, w⟫ ∈ s
⊢ i ≤ l
Tactic:
simpa [←hl, lt_succ_iff_le] using hi
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.successor
Proof state before:
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
Tactic:
have : w = z := Hs.seq.isMapping.uniq hiws hz
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
this : w = z
⊢ ⟪i + 1, c.succ v i w⟫ ∈ s ⁀' c.succ v i z
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.successor
Proof state before:
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
this : w = z
⊢ ⟪i + 1, c.succ v i w⟫ ∈ s ⁀' c.succ v i z
Tactic:
simp [this, hl]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.successor
Proof state before:
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
Tactic:
simp [mem_seqCons_iff]
Proof state after:
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 = lh s ∧ c.succ v i w = c.succ v l z ∨ ⟪i + 1, c.succ v i w⟫ ∈ s
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.successor
Proof state before:
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 = lh s ∧ c.succ v i w = c.succ v l z ∨ ⟪i + 1, c.succ v i w⟫ ∈ s
Tactic:
right
Proof state after:
case inr.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
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
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.successor
Proof state before:
case inr.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
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
Tactic:
exact Hs.succ i (by simp [←hl, hil]) w hiws
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 : M
hi : i < lh s
w : M
hiw : ⟪i, w⟫ ∈ s ⁀' c.succ v l z
hiws : ⟪i, w⟫ ∈ s
hil : i < l
⊢ i < lh s - 1
Tactic:
simp [←hl, hil]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.exists
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
l : M
⊢ ∃ s, c.CSeq v s ∧ l + 1 = lh s
Tactic:
induction l using induction_iSigmaOne
Proof 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
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.exists
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, c.CSeq v s ∧ 0 + 1 = lh s
Tactic:
case zero =>
  exact ⟨!⟨c.zero v⟩, CSeq.initial, by simp⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.exists
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
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]⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.exists
Proof 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
Proof 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)
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.exists
Proof 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
Proof 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)
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.exists
Proof 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⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.exists
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
⊢ DefinedWithParam (fun v_1 => c.CSeq v (v_1 0)) (HSemiformula.rew (Rew.embSubsts (#0 :> fun i => &(v i))) p.cseqDef)
Tactic:
intro w
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
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
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.exists
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
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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.exists
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.exists
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, c.CSeq v s ∧ 0 + 1 = lh s
Tactic:
exact ⟨!⟨c.zero v⟩, CSeq.initial, by simp⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.exists
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 + 1 = lh (∅ ⁀' c.zero v)
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.exists
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
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⟩
Proof 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
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.exists
Proof 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]
Proof 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
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.exists
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.exists
Proof 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⟩
Proof 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
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.exists
Proof 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]⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.exists
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
l s : M
Hs : c.CSeq v s
hls : l + 1 = lh s
⊢ l < lh s
Tactic:
simp [←hls]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.exists
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
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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.cSeq_result_existsUnique
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
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⟩
Proof 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
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.cSeq_result_existsUnique
Proof 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])
Proof 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
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.cSeq_result_existsUnique
Proof 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⟩
Proof 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
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.cSeq_result_existsUnique
Proof 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')
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.cSeq_result_existsUnique
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
l s : M
Hs : c.CSeq v s
h : l + 1 = lh s
⊢ l < lh s
Tactic:
simp [←h]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.cSeq_result_existsUnique
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
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'⟩
Proof 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
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.cSeq_result_existsUnique
Proof 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'
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.cSeq_result_existsUnique
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
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']
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.cSeq_result_existsUnique
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
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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.result_zero
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
⊢ c.result v 0 = c.zero v
Tactic:
rcases c.result_spec v 0 with ⟨s, Hs, _, h0⟩
Proof 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
s : M
Hs : c.CSeq v s
left✝ : 0 + 1 = lh s
h0 : ⟪0, c.result v 0⟫ ∈ s
⊢ c.result v 0 = c.zero v
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.result_zero
Proof 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
s : M
Hs : c.CSeq v s
left✝ : 0 + 1 = lh s
h0 : ⟪0, c.result v 0⟫ ∈ s
⊢ c.result v 0 = c.zero v
Tactic:
exact Hs.seq.isMapping.uniq h0 Hs.zero
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.result_succ
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
u : M
⊢ c.result v (u + 1) = c.succ v u (c.result v u)
Tactic:
rcases c.result_spec v u with ⟨s, Hs, hk, h⟩
Proof 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
hk : u + 1 = lh s
h : ⟪u, c.result v u⟫ ∈ s
⊢ c.result v (u + 1) = c.succ v u (c.result v u)
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.result_succ
Proof 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
hk : u + 1 = lh s
h : ⟪u, c.result v u⟫ ∈ s
⊢ c.result v (u + 1) = c.succ v u (c.result v u)
Tactic:
have : CSeq c v (s ⁀' c.succ v u (result c v u) ) := Hs.successor hk h
Proof 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
hk : u + 1 = lh s
h : ⟪u, c.result v u⟫ ∈ s
this : c.CSeq v (s ⁀' c.succ v u (c.result v u))
⊢ c.result v (u + 1) = c.succ v u (c.result v u)
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.result_succ
Proof 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
hk : u + 1 = lh s
h : ⟪u, c.result v u⟫ ∈ s
this : c.CSeq v (s ⁀' c.succ v u (c.result v u))
⊢ c.result v (u + 1) = c.succ v u (c.result v u)
Tactic:
exact Eq.symm
  <| Classical.choose_uniq (c.cSeq_result_existsUnique v (u + 1))
  ⟨_, this, by simp [Hs.seq, hk], by simp [hk]⟩
Proof state after:
no goals