internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.cseq_iff
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
⊢ c.CSeq v s →
    Seq s ∧
      (∃ z < s, z = c.zero v ∧ ⟪0, z⟫ ∈ s) ∧
        ∀ i < 2 * s,
          (∃ l ≤ 2 * s, l = lh s ∧ i + 1 < l) → ∀ z < s, ⟪i, z⟫ ∈ s → ∃ u < s, u = c.succ v i z ∧ ⟪i + 1, u⟫ ∈ s
Tactic:
rintro ⟨Hs, hz, hs⟩
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
s : M
Hs : Seq s
hz : ⟪0, c.zero v⟫ ∈ s
hs : ∀ i < lh s - 1, ∀ (z : M), ⟪i, z⟫ ∈ s → ⟪i + 1, c.succ v i z⟫ ∈ s
⊢ Seq s ∧
    (∃ z < s, z = c.zero v ∧ ⟪0, z⟫ ∈ s) ∧
      ∀ i < 2 * s,
        (∃ l ≤ 2 * s, l = lh s ∧ i + 1 < l) → ∀ z < s, ⟪i, z⟫ ∈ s → ∃ u < s, u = c.succ v i z ∧ ⟪i + 1, u⟫ ∈ s
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.cseq_iff
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
s : M
Hs : Seq s
hz : ⟪0, c.zero v⟫ ∈ s
hs : ∀ i < lh s - 1, ∀ (z : M), ⟪i, z⟫ ∈ s → ⟪i + 1, c.succ v i z⟫ ∈ s
⊢ Seq s ∧
    (∃ z < s, z = c.zero v ∧ ⟪0, z⟫ ∈ s) ∧
      ∀ i < 2 * s,
        (∃ l ≤ 2 * s, l = lh s ∧ i + 1 < l) → ∀ z < s, ⟪i, z⟫ ∈ s → ∃ u < s, u = c.succ v i z ∧ ⟪i + 1, u⟫ ∈ s
Tactic:
exact ⟨Hs, ⟨c.zero v, lt_of_mem_rng hz, rfl, hz⟩, fun i _ hi z _ hiz ↦
⟨c.succ v i z, by
  have := hs i (by rcases hi with ⟨l, _, rfl, hl⟩; simp [lt_tsub_iff_right, hl]) z hiz
  exact ⟨lt_of_mem_rng this, rfl, this⟩⟩⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.cseq_iff
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
Hs : Seq s
hz : ⟪0, c.zero v⟫ ∈ s
hs : ∀ i < lh s - 1, ∀ (z : M), ⟪i, z⟫ ∈ s → ⟪i + 1, c.succ v i z⟫ ∈ s
i : M
x✝¹ : i < 2 * s
hi : ∃ l ≤ 2 * s, l = lh s ∧ i + 1 < l
z : M
x✝ : z < s
hiz : ⟪i, z⟫ ∈ s
⊢ c.succ v i z < s ∧ c.succ v i z = c.succ v i z ∧ ⟪i + 1, c.succ v i z⟫ ∈ s
Tactic:
have := hs i (by rcases hi with ⟨l, _, rfl, hl⟩; simp [lt_tsub_iff_right, hl]) z hiz
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
Hs : Seq s
hz : ⟪0, c.zero v⟫ ∈ s
hs : ∀ i < lh s - 1, ∀ (z : M), ⟪i, z⟫ ∈ s → ⟪i + 1, c.succ v i z⟫ ∈ s
i : M
x✝¹ : i < 2 * s
hi : ∃ l ≤ 2 * s, l = lh s ∧ i + 1 < l
z : M
x✝ : z < s
hiz : ⟪i, z⟫ ∈ s
this : ⟪i + 1, c.succ v i z⟫ ∈ s
⊢ c.succ v i z < s ∧ c.succ v i z = c.succ v i z ∧ ⟪i + 1, c.succ v i z⟫ ∈ s
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.cseq_iff
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
Hs : Seq s
hz : ⟪0, c.zero v⟫ ∈ s
hs : ∀ i < lh s - 1, ∀ (z : M), ⟪i, z⟫ ∈ s → ⟪i + 1, c.succ v i z⟫ ∈ s
i : M
x✝¹ : i < 2 * s
hi : ∃ l ≤ 2 * s, l = lh s ∧ i + 1 < l
z : M
x✝ : z < s
hiz : ⟪i, z⟫ ∈ s
this : ⟪i + 1, c.succ v i z⟫ ∈ s
⊢ c.succ v i z < s ∧ c.succ v i z = c.succ v i z ∧ ⟪i + 1, c.succ v i z⟫ ∈ s
Tactic:
exact ⟨lt_of_mem_rng this, rfl, this⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.cseq_iff
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
Hs : Seq s
hz : ⟪0, c.zero v⟫ ∈ s
hs : ∀ i < lh s - 1, ∀ (z : M), ⟪i, z⟫ ∈ s → ⟪i + 1, c.succ v i z⟫ ∈ s
i : M
x✝¹ : i < 2 * s
hi : ∃ l ≤ 2 * s, l = lh s ∧ i + 1 < l
z : M
x✝ : z < s
hiz : ⟪i, z⟫ ∈ s
⊢ i < lh s - 1
Tactic:
rcases hi with ⟨l, _, rfl, hl⟩
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 : Seq s
hz : ⟪0, c.zero v⟫ ∈ s
hs : ∀ i < lh s - 1, ∀ (z : M), ⟪i, z⟫ ∈ s → ⟪i + 1, c.succ v i z⟫ ∈ s
i : M
x✝¹ : i < 2 * s
z : M
x✝ : z < s
hiz : ⟪i, z⟫ ∈ s
left✝ : lh s ≤ 2 * s
hl : i + 1 < lh s
⊢ i < lh s - 1
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.cseq_iff
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 : Seq s
hz : ⟪0, c.zero v⟫ ∈ s
hs : ∀ i < lh s - 1, ∀ (z : M), ⟪i, z⟫ ∈ s → ⟪i + 1, c.succ v i z⟫ ∈ s
i : M
x✝¹ : i < 2 * s
z : M
x✝ : z < s
hiz : ⟪i, z⟫ ∈ s
left✝ : lh s ≤ 2 * s
hl : i + 1 < lh s
⊢ i < lh s - 1
Tactic:
simp [lt_tsub_iff_right, hl]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.cseq_iff
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
⊢ (Seq s ∧
      (∃ z < s, z = c.zero v ∧ ⟪0, z⟫ ∈ s) ∧
        ∀ i < 2 * s,
          (∃ l ≤ 2 * s, l = lh s ∧ i + 1 < l) → ∀ z < s, ⟪i, z⟫ ∈ s → ∃ u < s, u = c.succ v i z ∧ ⟪i + 1, u⟫ ∈ s) →
    c.CSeq v s
Tactic:
rintro ⟨Hs, ⟨z, _, rfl, hz⟩, h⟩
Proof 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
s : M
Hs : Seq s
h : ∀ i < 2 * s, (∃ l ≤ 2 * s, l = lh s ∧ i + 1 < l) → ∀ z < s, ⟪i, z⟫ ∈ s → ∃ u < s, u = c.succ v i z ∧ ⟪i + 1, u⟫ ∈ s
left✝ : c.zero v < s
hz : ⟪0, c.zero v⟫ ∈ s
⊢ c.CSeq v s
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.cseq_iff
Proof 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
s : M
Hs : Seq s
h : ∀ i < 2 * s, (∃ l ≤ 2 * s, l = lh s ∧ i + 1 < l) → ∀ z < s, ⟪i, z⟫ ∈ s → ∃ u < s, u = c.succ v i z ∧ ⟪i + 1, u⟫ ∈ s
left✝ : c.zero v < s
hz : ⟪0, c.zero v⟫ ∈ s
⊢ c.CSeq v s
Tactic:
exact ⟨Hs, hz, fun i hi z hiz ↦ by
  rcases h i
    (lt_of_lt_of_le hi (by simp; exact le_trans (lh_bound _) (by simp)))
    ⟨lh s, by simp [lt_succ_iff_le], rfl, by simpa [lt_tsub_iff_right] using hi⟩ z (lt_of_mem_rng hiz) hiz with ⟨_, _, rfl, h⟩
  exact h⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.cseq_iff
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
Hs : Seq s
h : ∀ i < 2 * s, (∃ l ≤ 2 * s, l = lh s ∧ i + 1 < l) → ∀ z < s, ⟪i, z⟫ ∈ s → ∃ u < s, u = c.succ v i z ∧ ⟪i + 1, u⟫ ∈ s
left✝ : c.zero v < s
hz : ⟪0, c.zero v⟫ ∈ s
i : M
hi : i < lh s - 1
z : M
hiz : ⟪i, z⟫ ∈ s
⊢ ⟪i + 1, c.succ v i z⟫ ∈ s
Tactic:
rcases h i
  (lt_of_lt_of_le hi (by simp; exact le_trans (lh_bound _) (by simp)))
  ⟨lh s, by simp [lt_succ_iff_le], rfl, by simpa [lt_tsub_iff_right] using hi⟩ z (lt_of_mem_rng hiz) hiz with ⟨_, _, rfl, 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
s : M
Hs : Seq s
h✝ : ∀ i < 2 * s, (∃ l ≤ 2 * s, l = lh s ∧ i + 1 < l) → ∀ z < s, ⟪i, z⟫ ∈ s → ∃ u < s, u = c.succ v i z ∧ ⟪i + 1, u⟫ ∈ s
left✝¹ : c.zero v < s
hz : ⟪0, c.zero v⟫ ∈ s
i : M
hi : i < lh s - 1
z : M
hiz : ⟪i, z⟫ ∈ s
left✝ : c.succ v i z < s
h : ⟪i + 1, c.succ v i z⟫ ∈ s
⊢ ⟪i + 1, c.succ v i z⟫ ∈ s
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.cseq_iff
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 : Seq s
h✝ : ∀ i < 2 * s, (∃ l ≤ 2 * s, l = lh s ∧ i + 1 < l) → ∀ z < s, ⟪i, z⟫ ∈ s → ∃ u < s, u = c.succ v i z ∧ ⟪i + 1, u⟫ ∈ s
left✝¹ : c.zero v < s
hz : ⟪0, c.zero v⟫ ∈ s
i : M
hi : i < lh s - 1
z : M
hiz : ⟪i, z⟫ ∈ s
left✝ : c.succ v i z < s
h : ⟪i + 1, c.succ v i z⟫ ∈ s
⊢ ⟪i + 1, c.succ v i z⟫ ∈ s
Tactic:
exact h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.cseq_iff
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
Hs : Seq s
h : ∀ i < 2 * s, (∃ l ≤ 2 * s, l = lh s ∧ i + 1 < l) → ∀ z < s, ⟪i, z⟫ ∈ s → ∃ u < s, u = c.succ v i z ∧ ⟪i + 1, u⟫ ∈ s
left✝ : c.zero v < s
hz : ⟪0, c.zero v⟫ ∈ s
i : M
hi : i < lh s - 1
z : M
hiz : ⟪i, z⟫ ∈ s
⊢ lh s - 1 ≤ 2 * s
Tactic:
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
Hs : Seq s
h : ∀ i < 2 * s, (∃ l ≤ 2 * s, l = lh s ∧ i + 1 < l) → ∀ z < s, ⟪i, z⟫ ∈ s → ∃ u < s, u = c.succ v i z ∧ ⟪i + 1, u⟫ ∈ s
left✝ : c.zero v < s
hz : ⟪0, c.zero v⟫ ∈ s
i : M
hi : i < lh s - 1
z : M
hiz : ⟪i, z⟫ ∈ s
⊢ lh s ≤ 2 * s + 1
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.cseq_iff
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
Hs : Seq s
h : ∀ i < 2 * s, (∃ l ≤ 2 * s, l = lh s ∧ i + 1 < l) → ∀ z < s, ⟪i, z⟫ ∈ s → ∃ u < s, u = c.succ v i z ∧ ⟪i + 1, u⟫ ∈ s
left✝ : c.zero v < s
hz : ⟪0, c.zero v⟫ ∈ s
i : M
hi : i < lh s - 1
z : M
hiz : ⟪i, z⟫ ∈ s
⊢ lh s ≤ 2 * s + 1
Tactic:
exact le_trans (lh_bound _) (by simp)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.cseq_iff
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
Hs : Seq s
h : ∀ i < 2 * s, (∃ l ≤ 2 * s, l = lh s ∧ i + 1 < l) → ∀ z < s, ⟪i, z⟫ ∈ s → ∃ u < s, u = c.succ v i z ∧ ⟪i + 1, u⟫ ∈ s
left✝ : c.zero v < s
hz : ⟪0, c.zero v⟫ ∈ s
i : M
hi : i < lh s - 1
z : M
hiz : ⟪i, z⟫ ∈ s
⊢ 2 * s ≤ 2 * s + 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.cseq_iff
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
Hs : Seq s
h : ∀ i < 2 * s, (∃ l ≤ 2 * s, l = lh s ∧ i + 1 < l) → ∀ z < s, ⟪i, z⟫ ∈ s → ∃ u < s, u = c.succ v i z ∧ ⟪i + 1, u⟫ ∈ s
left✝ : c.zero v < s
hz : ⟪0, c.zero v⟫ ∈ s
i : M
hi : i < lh s - 1
z : M
hiz : ⟪i, z⟫ ∈ s
⊢ lh s ≤ 2 * s
Tactic:
simp [lt_succ_iff_le]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.cseq_iff
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
Hs : Seq s
h : ∀ i < 2 * s, (∃ l ≤ 2 * s, l = lh s ∧ i + 1 < l) → ∀ z < s, ⟪i, z⟫ ∈ s → ∃ u < s, u = c.succ v i z ∧ ⟪i + 1, u⟫ ∈ s
left✝ : c.zero v < s
hz : ⟪0, c.zero v⟫ ∈ s
i : M
hi : i < lh s - 1
z : M
hiz : ⟪i, z⟫ ∈ s
⊢ i + 1 < lh s
Tactic:
simpa [lt_tsub_iff_right] using hi
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.cseq_defined
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
⊢ Defined (fun v => c.CSeq (fun x => v x.succ) (v 0)) p.cseqDef
Tactic:
intro v
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
v : Fin (k + 1) → M
⊢ (fun v => c.CSeq (fun x => v x.succ) (v 0)) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val p.cseqDef)
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.cseq_defined
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
v : Fin (k + 1) → M
⊢ (fun v => c.CSeq (fun x => v x.succ) (v 0)) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val p.cseqDef)
Tactic:
simp [Formulae.cseqDef, cseq_iff, c.zero_defined.df.iff, c.succ_defined.df.iff]
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
hi : i < lh s₁
z₁ z₂ : M
⊢ ⟪i, z₁⟫ ∈ s₁ → ⟪i, z₂⟫ ∈ s₂ → z₁ = z₂
Tactic:
revert z₁ z₂
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
hi : i < lh s₁
⊢ ∀ {z₁ z₂ : M}, ⟪i, z₁⟫ ∈ s₁ → ⟪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
hi : i < lh s₁
⊢ ∀ {z₁ z₂ : M}, ⟪i, z₁⟫ ∈ s₁ → ⟪i, z₂⟫ ∈ s₂ → z₁ = z₂
Tactic:
suffices ∀ z₁ < s₁, ∀ z₂ < s₂, ⟪i, z₁⟫ ∈ s₁ → ⟪i, z₂⟫ ∈ s₂ → z₁ = z₂
by intro z₁ z₂ hz₁ hz₂; exact this z₁ (lt_of_mem_rng hz₁) z₂ (lt_of_mem_rng hz₂) hz₁ hz₂
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
hi : i < lh s₁
⊢ ∀ z₁ < s₁, ∀ z₂ < s₂, ⟪i, z₁⟫ ∈ s₁ → ⟪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
hi : i < lh s₁
⊢ ∀ z₁ < s₁, ∀ z₂ < s₂, ⟪i, z₁⟫ ∈ s₁ → ⟪i, z₂⟫ ∈ s₂ → z₁ = z₂
Tactic:
intro z₁ hz₁ z₂ hz₂ 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
hi : i < lh s₁
z₁ : M
hz₁ : z₁ < s₁
z₂ : M
hz₂ : z₂ < s₂
h₁ : ⟪i, z₁⟫ ∈ s₁
h₂ : ⟪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
hi : i < lh s₁
z₁ : M
hz₁ : z₁ < s₁
z₂ : M
hz₂ : z₂ < s₂
h₁ : ⟪i, z₁⟫ ∈ s₁
h₂ : ⟪i, z₂⟫ ∈ s₂
⊢ z₁ = z₂
Tactic:
induction i using induction_iSigmaOne generalizing z₁ z₂
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
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₂
⊢ 𝚺₁-Predicate fun {i} => i < lh s₁ → ∀ z₁ < s₁, ∀ z₂ < s₂, ⟪i, z₁⟫ ∈ s₁ → ⟪i, z₂⟫ ∈ s₂ → z₁ = z₂

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 : M
h : c.CSeq v s
s₁ s₂ : M
H₁ : c.CSeq v s₁
H₂ : c.CSeq v s₂
h₁₂ : lh s₁ ≤ lh s₂
hi : 0 < lh s₁
z₁ : M
hz₁ : z₁ < s₁
z₂ : M
hz₂ : z₂ < s₂
h₁ : ⟪0, z₁⟫ ∈ s₁
h₂ : ⟪0, z₂⟫ ∈ s₂
⊢ z₁ = z₂

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
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₂
x✝ : M
a✝ : x✝ < lh s₁ → ∀ z₁ < s₁, ∀ z₂ < s₂, ⟪x✝, z₁⟫ ∈ s₁ → ⟪x✝, z₂⟫ ∈ s₂ → z₁ = z₂
hi : x✝ + 1 < lh s₁
z₁ : M
hz₁ : z₁ < s₁
z₂ : M
hz₂ : z₂ < s₂
h₁ : ⟪x✝ + 1, z₁⟫ ∈ s₁
h₂ : ⟪x✝ + 1, 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₂
hi : 0 < lh s₁
z₁ : M
hz₁ : z₁ < s₁
z₂ : M
hz₂ : z₂ < s₂
h₁ : ⟪0, z₁⟫ ∈ s₁
h₂ : ⟪0, z₂⟫ ∈ s₂
⊢ z₁ = z₂
Tactic:
case zero =>
  have : z₁ = c.zero v := H₁.seq.isMapping.uniq h₁ H₁.zero
  have : z₂ = c.zero v := H₂.seq.isMapping.uniq h₂ H₂.zero
  simp_all
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₂
⊢ z₁ = z₂
Tactic:
case succ i ih =>
  have hi' : i < lh s₁ := lt_of_le_of_lt (by simp) hi
  let z' := H₁.seq.nth hi'
  have ih₁ : ⟪i, z'⟫ ∈ s₁ := H₁.seq.nth_mem hi'
  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]
  have h₁' : ⟪i + 1, c.succ v i z'⟫ ∈ s₁ := H₁.succ i (by simp [lt_tsub_iff_right, hi]) z' ih₁
  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₂
  have e₁ : z₁ = c.succ v i z' := H₁.seq.isMapping.uniq h₁ h₁'
  have e₂ : z₂ = c.succ v i z' := H₂.seq.isMapping.uniq h₂ h₂'
  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
hi : i < lh s₁
this : ∀ z₁ < s₁, ∀ z₂ < s₂, ⟪i, z₁⟫ ∈ s₁ → ⟪i, z₂⟫ ∈ s₂ → z₁ = z₂
⊢ ∀ {z₁ z₂ : M}, ⟪i, z₁⟫ ∈ s₁ → ⟪i, z₂⟫ ∈ s₂ → z₁ = z₂
Tactic:
intro z₁ z₂ hz₁ hz₂
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
hi : i < lh s₁
this : ∀ z₁ < s₁, ∀ z₂ < s₂, ⟪i, z₁⟫ ∈ s₁ → ⟪i, z₂⟫ ∈ s₂ → z₁ = z₂
z₁ z₂ : M
hz₁ : ⟪i, z₁⟫ ∈ s₁
hz₂ : ⟪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
hi : i < lh s₁
this : ∀ z₁ < s₁, ∀ z₂ < s₂, ⟪i, z₁⟫ ∈ s₁ → ⟪i, z₂⟫ ∈ s₂ → z₁ = z₂
z₁ z₂ : M
hz₁ : ⟪i, z₁⟫ ∈ s₁
hz₂ : ⟪i, z₂⟫ ∈ s₂
⊢ z₁ = z₂
Tactic:
exact this z₁ (lt_of_mem_rng hz₁) z₂ (lt_of_mem_rng hz₂) hz₁ hz₂
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.CSeq.unique
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
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₂
⊢ 𝚺₁-Predicate fun {i} => i < lh s₁ → ∀ z₁ < s₁, ∀ z₂ < s₂, ⟪i, z₁⟫ ∈ s₁ → ⟪i, z₂⟫ ∈ s₂ → z₁ = z₂
Tactic:
definability
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₂
hi : 0 < lh s₁
z₁ : M
hz₁ : z₁ < s₁
z₂ : M
hz₂ : z₂ < s₂
h₁ : ⟪0, z₁⟫ ∈ s₁
h₂ : ⟪0, z₂⟫ ∈ s₂
⊢ z₁ = z₂
Tactic:
have : z₁ = c.zero v := H₁.seq.isMapping.uniq h₁ H₁.zero
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₂
hi : 0 < lh s₁
z₁ : M
hz₁ : z₁ < s₁
z₂ : M
hz₂ : z₂ < s₂
h₁ : ⟪0, z₁⟫ ∈ s₁
h₂ : ⟪0, z₂⟫ ∈ s₂
this : z₁ = c.zero v
⊢ 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₂
hi : 0 < lh s₁
z₁ : M
hz₁ : z₁ < s₁
z₂ : M
hz₂ : z₂ < s₂
h₁ : ⟪0, z₁⟫ ∈ s₁
h₂ : ⟪0, z₂⟫ ∈ s₂
this : z₁ = c.zero v
⊢ z₁ = z₂
Tactic:
have : z₂ = c.zero v := H₂.seq.isMapping.uniq h₂ H₂.zero
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₂
hi : 0 < lh s₁
z₁ : M
hz₁ : z₁ < s₁
z₂ : M
hz₂ : z₂ < s₂
h₁ : ⟪0, z₁⟫ ∈ s₁
h₂ : ⟪0, z₂⟫ ∈ s₂
this✝ : z₁ = c.zero v
this : z₂ = c.zero v
⊢ 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₂
hi : 0 < lh s₁
z₁ : M
hz₁ : z₁ < s₁
z₂ : M
hz₂ : z₂ < s₂
h₁ : ⟪0, z₁⟫ ∈ s₁
h₂ : ⟪0, z₂⟫ ∈ s₂
this✝ : z₁ = c.zero v
this : z₂ = c.zero v
⊢ z₁ = z₂
Tactic:
simp_all
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₂
⊢ z₁ = z₂
Tactic:
have hi' : i < lh s₁ := lt_of_le_of_lt (by simp) 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₁ = z₂