internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.exp_defined_deltaZero
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
⊢ 𝚺₀-Function₁ exp via expDef
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 ⊧ₘ* 𝐈𝚺₁
v : Fin (Nat.succ 1) → M
⊢ (fun v => v 0 = (fun v => exp v 0) fun x => v x.succ) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val expDef)
Theorem: LO.FirstOrder.Arith.Model.exp_defined_deltaZero
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin (Nat.succ 1) → M
⊢ (fun v => v 0 = (fun v => exp v 0) fun x => v x.succ) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val expDef)
Tactic:
simp [expDef, exponential_graph]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.exp_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 ⊧ₘ* 𝐈𝚺₁
⊢ Exponential 0 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.exp_one
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
⊢ Exponential 1 2
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.one_le_exp
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a : M
⊢ 0 < exp a
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.seq_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 ⊧ₘ* 𝐈𝚺₁
s : M
⊢ Seq s → IsMapping s ∧ ∃ l ≤ 2 * s, ∃ d ≤ 2 * s, d = domain s ∧ d = under l
Tactic:
rintro ⟨hs, l, 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 ⊧ₘ* 𝐈𝚺₁
s : M
hs : IsMapping s
l : M
h : domain s = under l
⊢ IsMapping s ∧ ∃ l ≤ 2 * s, ∃ d ≤ 2 * s, d = domain s ∧ d = under l
Theorem: LO.FirstOrder.Arith.Model.seq_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 ⊧ₘ* 𝐈𝚺₁
s : M
hs : IsMapping s
l : M
h : domain s = under l
⊢ IsMapping s ∧ ∃ l ≤ 2 * s, ∃ d ≤ 2 * s, d = domain s ∧ d = under l
Tactic:
exact ⟨hs, l, (by
calc
  l ≤ domain s := by simp [h]
  _ ≤ 2 * s    := by simp), ⟨domain s , by simp,  rfl, h⟩⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.seq_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 ⊧ₘ* 𝐈𝚺₁
s : M
hs : IsMapping s
l : M
h : domain s = under l
⊢ l ≤ 2 * s
Tactic:
calc
  l ≤ domain s := by simp [h]
  _ ≤ 2 * s    := by simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.seq_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 ⊧ₘ* 𝐈𝚺₁
s : M
hs : IsMapping s
l : M
h : domain s = under l
⊢ l ≤ domain s
Tactic:
simp [h]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.seq_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 ⊧ₘ* 𝐈𝚺₁
s : M
hs : IsMapping s
l : M
h : domain s = under l
⊢ domain s ≤ 2 * s
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.seq_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 ⊧ₘ* 𝐈𝚺₁
s : M
⊢ (IsMapping s ∧ ∃ l ≤ 2 * s, ∃ d ≤ 2 * s, d = domain s ∧ d = under l) → Seq s
Tactic:
rintro ⟨hs, l, _, _, _, rfl, h⟩
Proof state after:
case intro.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 ⊧ₘ* 𝐈𝚺₁
s : M
hs : IsMapping s
l : M
left✝¹ : l ≤ 2 * s
left✝ : domain s ≤ 2 * s
h : domain s = under l
⊢ Seq s
Theorem: LO.FirstOrder.Arith.Model.seq_iff
Proof state before:
case intro.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 ⊧ₘ* 𝐈𝚺₁
s : M
hs : IsMapping s
l : M
left✝¹ : l ≤ 2 * s
left✝ : domain s ≤ 2 * s
h : domain s = under l
⊢ Seq s
Tactic:
exact ⟨hs, l, h⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.seq_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 ⊧ₘ* 𝐈𝚺₁
⊢ 𝚺₀-Predicate Seq via seqDef
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 ⊧ₘ* 𝐈𝚺₁
v : Fin 1 → M
⊢ (fun v => Seq (v 0)) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val seqDef)
Theorem: LO.FirstOrder.Arith.Model.seq_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 ⊧ₘ* 𝐈𝚺₁
v : Fin 1 → M
⊢ (fun v => Seq (v 0)) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val seqDef)
Tactic:
simp [seqDef, seq_iff]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lh_exists_uniq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
⊢ ∃! l, (Seq s → domain s = under l) ∧ (¬Seq s → l = 0)
Tactic:
by_cases h : Seq s
Proof state after:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
⊢ ∃! l, (Seq s → domain s = under l) ∧ (¬Seq s → l = 0)

case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : ¬Seq s
⊢ ∃! l, (Seq s → domain s = under l) ∧ (¬Seq s → l = 0)
Theorem: LO.FirstOrder.Arith.Model.lh_exists_uniq
Proof state before:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
⊢ ∃! l, (Seq s → domain s = under l) ∧ (¬Seq s → l = 0)
Tactic:
rcases h with ⟨h, l, hl⟩
Proof state after:
case pos.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : IsMapping s
l : M
hl : domain s = under l
⊢ ∃! l, (Seq s → domain s = under l) ∧ (¬Seq s → l = 0)
Theorem: LO.FirstOrder.Arith.Model.lh_exists_uniq
Proof state before:
case pos.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : IsMapping s
l : M
hl : domain s = under l
⊢ ∃! l, (Seq s → domain s = under l) ∧ (¬Seq s → l = 0)
Tactic:
exact ExistsUnique.intro l
  (by simp [show Seq s from ⟨h, l, hl⟩, hl])
  (by simp [show Seq s from ⟨h, l, hl⟩, hl])
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lh_exists_uniq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : IsMapping s
l : M
hl : domain s = under l
⊢ (Seq s → domain s = under l) ∧ (¬Seq s → l = 0)
Tactic:
simp [show Seq s from ⟨h, l, hl⟩, hl]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lh_exists_uniq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : IsMapping s
l : M
hl : domain s = under l
⊢ ∀ (y : M), (Seq s → domain s = under y) ∧ (¬Seq s → y = 0) → y = l
Tactic:
simp [show Seq s from ⟨h, l, hl⟩, hl]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lh_exists_uniq
Proof state before:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : ¬Seq s
⊢ ∃! l, (Seq s → domain s = under l) ∧ (¬Seq s → l = 0)
Tactic:
simp [h]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lh_bound
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
⊢ lh s ≤ 2 * s
Tactic:
by_cases hs : Seq s
Proof state after:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hs : Seq s
⊢ lh s ≤ 2 * s

case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hs : ¬Seq s
⊢ lh s ≤ 2 * s
Theorem: LO.FirstOrder.Arith.Model.lh_bound
Proof state before:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hs : Seq s
⊢ lh s ≤ 2 * s
Tactic:
calc
  lh s ≤ under (lh s) := le_under _
  _    ≤ 2 * s        := by simp [←hs.domain_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lh_bound
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hs : Seq s
⊢ under (lh s) ≤ 2 * s
Tactic:
simp [←hs.domain_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lh_bound
Proof state before:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hs : ¬Seq s
⊢ lh s ≤ 2 * s
Tactic:
simp [lh_prop_of_not_seq hs]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lh_graph
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
l s : M
⊢ l = lh s → (Seq s → ∃ d ≤ 2 * s, d = domain s ∧ d = under l) ∧ (¬Seq s → l = 0)
Tactic:
rintro rfl
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
⊢ (Seq s → ∃ d ≤ 2 * s, d = domain s ∧ d = under (lh s)) ∧ (¬Seq s → lh s = 0)
Theorem: LO.FirstOrder.Arith.Model.lh_graph
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
⊢ (Seq s → ∃ d ≤ 2 * s, d = domain s ∧ d = under (lh s)) ∧ (¬Seq s → lh s = 0)
Tactic:
by_cases Hs : Seq s <;> simp [Hs, ←Seq.domain_eq, lh_prop_of_not_seq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lh_graph
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
l s : M
⊢ (Seq s → ∃ d ≤ 2 * s, d = domain s ∧ d = under l) ∧ (¬Seq s → l = 0) → l = lh s
Tactic:
rintro ⟨h, hn⟩
Proof state after:
case intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
l s : M
h : Seq s → ∃ d ≤ 2 * s, d = domain s ∧ d = under l
hn : ¬Seq s → l = 0
⊢ l = lh s
Theorem: LO.FirstOrder.Arith.Model.lh_graph
Proof state before:
case intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
l s : M
h : Seq s → ∃ d ≤ 2 * s, d = domain s ∧ d = under l
hn : ¬Seq s → l = 0
⊢ l = lh s
Tactic:
by_cases Hs : Seq s
Proof state after:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
l s : M
h : Seq s → ∃ d ≤ 2 * s, d = domain s ∧ d = under l
hn : ¬Seq s → l = 0
Hs : Seq s
⊢ l = lh s

case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
l s : M
h : Seq s → ∃ d ≤ 2 * s, d = domain s ∧ d = under l
hn : ¬Seq s → l = 0
Hs : ¬Seq s
⊢ l = lh s
Theorem: LO.FirstOrder.Arith.Model.lh_graph
Proof state before:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
l s : M
h : Seq s → ∃ d ≤ 2 * s, d = domain s ∧ d = under l
hn : ¬Seq s → l = 0
Hs : Seq s
⊢ l = lh s
Tactic:
rcases h Hs with ⟨_, _, rfl, h⟩
Proof state after:
case pos.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
l s : M
h✝ : Seq s → ∃ d ≤ 2 * s, d = domain s ∧ d = under l
hn : ¬Seq s → l = 0
Hs : Seq s
left✝ : domain s ≤ 2 * s
h : domain s = under l
⊢ l = lh s
Theorem: LO.FirstOrder.Arith.Model.lh_graph
Proof state before:
case pos.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
l s : M
h✝ : Seq s → ∃ d ≤ 2 * s, d = domain s ∧ d = under l
hn : ¬Seq s → l = 0
Hs : Seq s
left✝ : domain s ≤ 2 * s
h : domain s = under l
⊢ l = lh s
Tactic:
simpa [h] using Hs.domain_eq
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lh_graph
Proof state before:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
l s : M
h : Seq s → ∃ d ≤ 2 * s, d = domain s ∧ d = under l
hn : ¬Seq s → l = 0
Hs : ¬Seq s
⊢ l = lh s
Tactic:
simp [lh_prop_of_not_seq Hs, hn Hs]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lh_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 ⊧ₘ* 𝐈𝚺₁
⊢ 𝚺₀-Function₁ lh via lhDef
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 ⊧ₘ* 𝐈𝚺₁
v : Fin (Nat.succ 1) → M
⊢ (fun v => v 0 = (fun v => lh (v 0)) fun x => v x.succ) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val lhDef)
Theorem: LO.FirstOrder.Arith.Model.lh_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 ⊧ₘ* 𝐈𝚺₁
v : Fin (Nat.succ 1) → M
⊢ (fun v => v 0 = (fun v => lh (v 0)) fun x => v x.succ) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val lhDef)
Tactic:
simp [lhDef, -exists_eq_right_right, lh_graph]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Seq.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 ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
x : M
hx : x < lh s
⊢ x ∈ domain s
Tactic:
simpa [h.domain_eq] using hx
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Seq.nth_exists_uniq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
x : M
hx : x < lh s
⊢ x ∈ domain s
Tactic:
simpa [h.domain_eq] using hx
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Seq.nth_uniq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
x y : M
hx : x < lh s
hy : ⟪x, y⟫ ∈ s
⊢ ⟪x, h.nth hx⟫ ∈ s
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Seq.lh_eq_of
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
H : Seq s
l : M
h : domain s = under l
⊢ lh s = l
Tactic:
simpa [H.domain_eq] using h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Seq.lt_lh_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 ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
i : M
⊢ i < lh s ↔ i ∈ domain s
Tactic:
simp [h.domain_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Seq.lt_lh_of_mem
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
i x : M
hix : ⟪i, x⟫ ∈ s
⊢ i < lh s
Tactic:
simp [h.lt_lh_iff, mem_domain_iff]
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
i x : M
hix : ⟪i, x⟫ ∈ s
⊢ ∃ y, ⟪i, y⟫ ∈ s
Theorem: LO.FirstOrder.Arith.Model.Seq.lt_lh_of_mem
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
i x : M
hix : ⟪i, x⟫ ∈ s
⊢ ∃ y, ⟪i, y⟫ ∈ s
Tactic:
exact ⟨x, hix⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.seq_empty
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
⊢ IsMapping ∅
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.seq_empty
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
⊢ domain ∅ = under 0
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lh_empty
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
⊢ lh ∅ = 0
Tactic:
have : under (lh ∅ : M) = under 0 := by simpa using Eq.symm <| Seq.domain_eq (M := M) (s := ∅) (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 ⊧ₘ* 𝐈𝚺₁
this : under (lh ∅) = under 0
⊢ lh ∅ = 0
Theorem: LO.FirstOrder.Arith.Model.lh_empty
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
this : under (lh ∅) = under 0
⊢ lh ∅ = 0
Tactic:
exact under_inj.mp this
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lh_empty
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
⊢ under (lh ∅) = under 0
Tactic:
simpa using Eq.symm <| Seq.domain_eq (M := M) (s := ∅) (by simp)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lh_empty
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
⊢ Seq ∅
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Seq.isempty_of_lh_eq_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 ⊧ₘ* 𝐈𝚺₁
s : M
Hs : Seq s
h : lh s = 0
⊢ s = ∅
Tactic:
simpa [h] using Hs.domain_eq
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Seq.subset_seqCons
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s x : M
⊢ s ⊆ s ⁀' x
Tactic:
simp [seqCons]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Seq.lt_seqCons
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hs : Seq s
x : M
⊢ s ⊆ s ⁀' x
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Seq.lt_seqCons
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hs : Seq s
x : M
⊢ s ≠ s ⁀' x
Tactic:
simp [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 ⊧ₘ* 𝐈𝚺₁
s : M
hs : Seq s
x : M
⊢ ¬s = insert ⟪lh s, x⟫ s
Theorem: LO.FirstOrder.Arith.Model.Seq.lt_seqCons
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hs : Seq s
x : M
⊢ ¬s = insert ⟪lh s, x⟫ s
Tactic:
intro A
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hs : Seq s
x : M
A : s = insert ⟪lh s, x⟫ s
⊢ False
Theorem: LO.FirstOrder.Arith.Model.Seq.lt_seqCons
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hs : Seq s
x : M
A : s = insert ⟪lh s, x⟫ s
⊢ False
Tactic:
have : ⟪lh s, x⟫ ∈ s := by simpa [←A] using mem_insert ⟪lh s, x⟫ s
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hs : Seq s
x : M
A : s = insert ⟪lh s, x⟫ s
this : ⟪lh s, x⟫ ∈ s
⊢ False
Theorem: LO.FirstOrder.Arith.Model.Seq.lt_seqCons
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hs : Seq s
x : M
A : s = insert ⟪lh s, x⟫ s
this : ⟪lh s, x⟫ ∈ s
⊢ False
Tactic:
simpa using hs.lt_lh_of_mem this
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Seq.lt_seqCons
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hs : Seq s
x : M
A : s = insert ⟪lh s, x⟫ s
⊢ ⟪lh s, x⟫ ∈ s
Tactic:
simpa [←A] using mem_insert ⟪lh s, x⟫ s
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Seq.mem_seqCons
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s x : M
⊢ ⟪lh s, x⟫ ∈ s ⁀' x
Tactic:
simp [seqCons]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Seq.seqCons
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
x : M
⊢ lh s ∉ domain s
Tactic:
simp [h.domain_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Seq.seqCons
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
x : M
⊢ domain (s ⁀' x) = under (lh s + 1)
Tactic:
simp [seqCons, h.domain_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Seq.lh_seqCons
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
x s : M
h : Seq s
⊢ lh (s ⁀' x) = lh s + 1
Tactic:
have : under (lh s + 1) = under (lh (s ⁀' x)) := by
  simpa [seqCons, h.domain_eq] using (h.seqCons x).domain_eq
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
x s : M
h : Seq s
this : under (lh s + 1) = under (lh (s ⁀' x))
⊢ lh (s ⁀' x) = lh s + 1
Theorem: LO.FirstOrder.Arith.Model.Seq.lh_seqCons
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
x s : M
h : Seq s
this : under (lh s + 1) = under (lh (s ⁀' x))
⊢ lh (s ⁀' x) = lh s + 1
Tactic:
exact Eq.symm <| under_inj.mp this
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Seq.lh_seqCons
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
x s : M
h : Seq s
⊢ under (lh s + 1) = under (lh (s ⁀' x))
Tactic:
simpa [seqCons, h.domain_eq] using (h.seqCons x).domain_eq
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_seqCons_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 ⊧ₘ* 𝐈𝚺₁
i x z s : M
⊢ ⟪i, x⟫ ∈ s ⁀' z ↔ i = lh s ∧ x = z ∨ ⟪i, x⟫ ∈ s
Tactic:
simp [seqCons]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lh_mem_seqCons
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s z : M
⊢ ⟪lh s, z⟫ ∈ s ⁀' z
Tactic:
simp [seqCons]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lh_mem_seqCons_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 ⊧ₘ* 𝐈𝚺₁
s x z : M
H : Seq s
⊢ ⟪lh s, x⟫ ∈ s ⁀' z ↔ x = z
Tactic:
simp [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 ⊧ₘ* 𝐈𝚺₁
s x z : M
H : Seq s
⊢ ⟪lh s, x⟫ ∈ s → x = z
Theorem: LO.FirstOrder.Arith.Model.lh_mem_seqCons_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 ⊧ₘ* 𝐈𝚺₁
s x z : M
H : Seq s
⊢ ⟪lh s, x⟫ ∈ s → x = z
Tactic:
intro 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 ⊧ₘ* 𝐈𝚺₁
s x z : M
H : Seq s
h : ⟪lh s, x⟫ ∈ s
⊢ x = z
Theorem: LO.FirstOrder.Arith.Model.lh_mem_seqCons_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 ⊧ₘ* 𝐈𝚺₁
s x z : M
H : Seq s
h : ⟪lh s, x⟫ ∈ s
⊢ x = z
Tactic:
have := H.lt_lh_of_mem 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 ⊧ₘ* 𝐈𝚺₁
s x z : M
H : Seq s
h : ⟪lh s, x⟫ ∈ s
this : lh s < lh s
⊢ x = z
Theorem: LO.FirstOrder.Arith.Model.lh_mem_seqCons_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 ⊧ₘ* 𝐈𝚺₁
s x z : M
H : Seq s
h : ⟪lh s, x⟫ ∈ s
this : lh s < lh s
⊢ x = z
Tactic:
simp at this
Proof state after:
no goals