internlm/Lean-Github huggingface dataset:
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 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))
⊢ u + 1 + 1 = lh (s ⁀' c.succ v u (c.result v u))
Tactic:
simp [Hs.seq, hk]
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 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))
⊢ ⟪u + 1, c.succ v u (c.result v u)⟫ ∈ s ⁀' c.succ v u (c.result v u)
Tactic:
simp [hk]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.result_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 ⊧ₘ* 𝐈𝚺₁
k : ℕ
p : Formulae k
c : Construction M p
v : Fin k → M
z u : M
⊢ z = c.result v u → ∃ s, c.CSeq v s ∧ ⟪u, z⟫ ∈ s
Tactic:
rintro rfl
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
u : M
⊢ ∃ s, c.CSeq v s ∧ ⟪u, c.result v u⟫ ∈ s
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.result_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 ⊧ₘ* 𝐈𝚺₁
k : ℕ
p : Formulae k
c : Construction M p
v : Fin k → M
u : M
⊢ ∃ s, c.CSeq v s ∧ ⟪u, c.result v u⟫ ∈ s
Tactic:
rcases c.result_spec v u with ⟨s, Hs, _, h⟩
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
left✝ : u + 1 = lh s
h : ⟪u, c.result v u⟫ ∈ s
⊢ ∃ s, c.CSeq v s ∧ ⟪u, c.result v u⟫ ∈ s
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.result_graph
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
left✝ : u + 1 = lh s
h : ⟪u, c.result v u⟫ ∈ s
⊢ ∃ s, c.CSeq v s ∧ ⟪u, c.result v u⟫ ∈ s
Tactic:
exact ⟨s, Hs, h⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.result_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 ⊧ₘ* 𝐈𝚺₁
k : ℕ
p : Formulae k
c : Construction M p
v : Fin k → M
z u : M
⊢ (∃ s, c.CSeq v s ∧ ⟪u, z⟫ ∈ s) → z = c.result v u
Tactic:
rintro ⟨s, Hs, h⟩
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
z u s : M
Hs : c.CSeq v s
h : ⟪u, z⟫ ∈ s
⊢ z = c.result v u
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.result_graph
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
z u s : M
Hs : c.CSeq v s
h : ⟪u, z⟫ ∈ s
⊢ z = c.result v u
Tactic:
rcases c.result_spec v u with ⟨s', Hs', hu, h'⟩
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
z u s : M
Hs : c.CSeq v s
h : ⟪u, z⟫ ∈ s
s' : M
Hs' : c.CSeq v s'
hu : u + 1 = lh s'
h' : ⟪u, c.result v u⟫ ∈ s'
⊢ z = c.result v u
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.result_graph
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
z u s : M
Hs : c.CSeq v s
h : ⟪u, z⟫ ∈ s
s' : M
Hs' : c.CSeq v s'
hu : u + 1 = lh s'
h' : ⟪u, c.result v u⟫ ∈ s'
⊢ z = c.result v u
Tactic:
exact Eq.symm <| Hs'.unique Hs
  (by simp [←hu, succ_le_iff_lt]; exact Hs.seq.lt_lh_iff.mpr (mem_domain_of_pair_mem h))
  (by simp [←hu]) h' h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.result_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 ⊧ₘ* 𝐈𝚺₁
k : ℕ
p : Formulae k
c : Construction M p
v : Fin k → M
z u s : M
Hs : c.CSeq v s
h : ⟪u, z⟫ ∈ s
s' : M
Hs' : c.CSeq v s'
hu : u + 1 = lh s'
h' : ⟪u, c.result v u⟫ ∈ s'
⊢ lh s' ≤ lh s
Tactic:
simp [←hu, succ_le_iff_lt]
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
z u s : M
Hs : c.CSeq v s
h : ⟪u, z⟫ ∈ s
s' : M
Hs' : c.CSeq v s'
hu : u + 1 = lh s'
h' : ⟪u, c.result v u⟫ ∈ s'
⊢ u < lh s
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.result_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 ⊧ₘ* 𝐈𝚺₁
k : ℕ
p : Formulae k
c : Construction M p
v : Fin k → M
z u s : M
Hs : c.CSeq v s
h : ⟪u, z⟫ ∈ s
s' : M
Hs' : c.CSeq v s'
hu : u + 1 = lh s'
h' : ⟪u, c.result v u⟫ ∈ s'
⊢ u < lh s
Tactic:
exact Hs.seq.lt_lh_iff.mpr (mem_domain_of_pair_mem h)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.result_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 ⊧ₘ* 𝐈𝚺₁
k : ℕ
p : Formulae k
c : Construction M p
v : Fin k → M
z u s : M
Hs : c.CSeq v s
h : ⟪u, z⟫ ∈ s
s' : M
Hs' : c.CSeq v s'
hu : u + 1 = lh s'
h' : ⟪u, c.result v u⟫ ∈ s'
⊢ u < lh s'
Tactic:
simp [←hu]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.result_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
⊢ DefinedFunction ℒₒᵣ 𝚺₁ (fun v => c.result (fun x => v x.succ) (v 0)) p.resultDef
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).succ → M
⊢ (fun v => v 0 = (fun v => c.result (fun x => v x.succ) (v 0)) fun x => v x.succ) v ↔
    (Semiformula.Evalbm M v) (HSemiformula.val p.resultDef)
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.result_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).succ → M
⊢ (fun v => v 0 = (fun v => c.result (fun x => v x.succ) (v 0)) fun x => v x.succ) v ↔
    (Semiformula.Evalbm M v) (HSemiformula.val p.resultDef)
Tactic:
simp [Formulae.resultDef, result_graph]
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).succ → M
⊢ (∃ s, c.CSeq (fun x => v x.succ.succ) s ∧ ⟪v 1, v 0⟫ ∈ s) ↔
    ∃ x,
      (Semiformula.Eval (standardModel M) (x :> fun i => v i.succ.succ) Empty.elim) (HSemiformula.val p.cseqDef) ∧
        ⟪v (Fin.succ 0), v 0⟫ ∈ x
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.result_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).succ → M
⊢ (∃ s, c.CSeq (fun x => v x.succ.succ) s ∧ ⟪v 1, v 0⟫ ∈ s) ↔
    ∃ x,
      (Semiformula.Eval (standardModel M) (x :> fun i => v i.succ.succ) Empty.elim) (HSemiformula.val p.cseqDef) ∧
        ⟪v (Fin.succ 0), v 0⟫ ∈ x
Tactic:
apply exists_congr
Proof state after:
case 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
v : Fin (k + 1).succ → M
⊢ ∀ (a : M),
    c.CSeq (fun x => v x.succ.succ) a ∧ ⟪v 1, v 0⟫ ∈ a ↔
      (Semiformula.Eval (standardModel M) (a :> fun i => v i.succ.succ) Empty.elim) (HSemiformula.val p.cseqDef) ∧
        ⟪v (Fin.succ 0), v 0⟫ ∈ a
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.result_defined
Proof state before:
case 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
v : Fin (k + 1).succ → M
⊢ ∀ (a : M),
    c.CSeq (fun x => v x.succ.succ) a ∧ ⟪v 1, v 0⟫ ∈ a ↔
      (Semiformula.Eval (standardModel M) (a :> fun i => v i.succ.succ) Empty.elim) (HSemiformula.val p.cseqDef) ∧
        ⟪v (Fin.succ 0), v 0⟫ ∈ a
Tactic:
intro x
Proof state after:
case 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
v : Fin (k + 1).succ → M
x : M
⊢ c.CSeq (fun x => v x.succ.succ) x ∧ ⟪v 1, v 0⟫ ∈ x ↔
    (Semiformula.Eval (standardModel M) (x :> fun i => v i.succ.succ) Empty.elim) (HSemiformula.val p.cseqDef) ∧
      ⟪v (Fin.succ 0), v 0⟫ ∈ x
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.result_defined
Proof state before:
case 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
v : Fin (k + 1).succ → M
x : M
⊢ c.CSeq (fun x => v x.succ.succ) x ∧ ⟪v 1, v 0⟫ ∈ x ↔
    (Semiformula.Eval (standardModel M) (x :> fun i => v i.succ.succ) Empty.elim) (HSemiformula.val p.cseqDef) ∧
      ⟪v (Fin.succ 0), v 0⟫ ∈ x
Tactic:
simp [c.cseq_defined_iff]
Proof state after:
case 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
v : Fin (k + 1).succ → M
x : M
⊢ c.CSeq (fun x => v x.succ.succ) x → (⟪v 1, v 0⟫ ∈ x ↔ ⟪v (Fin.succ 0), v 0⟫ ∈ x)
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.result_defined
Proof state before:
case 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
v : Fin (k + 1).succ → M
x : M
⊢ c.CSeq (fun x => v x.succ.succ) x → (⟪v 1, v 0⟫ ∈ x ↔ ⟪v (Fin.succ 0), v 0⟫ ∈ x)
Tactic:
intros
Proof state after:
case 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
v : Fin (k + 1).succ → M
x : M
a✝ : c.CSeq (fun x => v x.succ.succ) x
⊢ ⟪v 1, v 0⟫ ∈ x ↔ ⟪v (Fin.succ 0), v 0⟫ ∈ x
Theorem: LO.FirstOrder.Arith.Model.PR.Construction.result_defined
Proof state before:
case 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
v : Fin (k + 1).succ → M
x : M
a✝ : c.CSeq (fun x => v x.succ.succ) x
⊢ ⟪v 1, v 0⟫ ∈ x ↔ ⟪v (Fin.succ 0), v 0⟫ ∈ x
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.susbset_insert
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 a : M
⊢ a ⊆ insert x a
Tactic:
intro z 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 ⊧ₘ* 𝐈𝚺₁
x a z : M
hz : z ∈ a
⊢ z ∈ insert x a
Theorem: LO.FirstOrder.Arith.Model.susbset_insert
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 a z : M
hz : z ∈ a
⊢ z ∈ insert x a
Tactic:
simp [hz]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.bitRemove_susbset
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 a : M
⊢ bitRemove x a ⊆ a
Tactic:
intro 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 ⊧ₘ* 𝐈𝚺₁
x a z : M
⊢ z ∈ bitRemove x a → z ∈ a
Theorem: LO.FirstOrder.Arith.Model.bitRemove_susbset
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 a z : M
⊢ z ∈ bitRemove x a → z ∈ a
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lt_of_mem_dom
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 y m : M
h : ⟪x, y⟫ ∈ m
⊢ x ≤ ⟪x, y⟫
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lt_of_mem_rng
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 y m : M
h : ⟪x, y⟫ ∈ m
⊢ y ≤ ⟪x, y⟫
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.under_subset_under_of_le
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 j : M
⊢ under i ⊆ under j → i ≤ j
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 ⊧ₘ* 𝐈𝚺₁
i j : M
h : under i ⊆ under j
⊢ i ≤ j
Theorem: LO.FirstOrder.Arith.Model.under_subset_under_of_le
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 j : M
h : under i ⊆ under j
⊢ i ≤ j
Tactic:
by_contra hij
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i j : M
h : under i ⊆ under j
hij : ¬i ≤ j
⊢ False
Theorem: LO.FirstOrder.Arith.Model.under_subset_under_of_le
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 j : M
h : under i ⊆ under j
hij : ¬i ≤ j
⊢ False
Tactic:
have : j < i := by simpa using hij
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i j : M
h : under i ⊆ under j
hij : ¬i ≤ j
this : j < i
⊢ False
Theorem: LO.FirstOrder.Arith.Model.under_subset_under_of_le
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 j : M
h : under i ⊆ under j
hij : ¬i ≤ j
this : j < i
⊢ False
Tactic:
simpa using h (mem_under_iff.mpr this)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.under_subset_under_of_le
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 j : M
h : under i ⊆ under j
hij : ¬i ≤ j
⊢ j < i
Tactic:
simpa using hij
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.under_subset_under_of_le
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 j : M
⊢ i ≤ j → under i ⊆ under j
Tactic:
intro hij x
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i j : M
hij : i ≤ j
x : M
⊢ x ∈ under i → x ∈ under j
Theorem: LO.FirstOrder.Arith.Model.under_subset_under_of_le
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 j : M
hij : i ≤ j
x : M
⊢ x ∈ under i → x ∈ under j
Tactic:
simp only [mem_under_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 ⊧ₘ* 𝐈𝚺₁
i j : M
hij : i ≤ j
x : M
⊢ x < i → x < j
Theorem: LO.FirstOrder.Arith.Model.under_subset_under_of_le
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 j : M
hij : i ≤ j
x : M
⊢ x < i → x < j
Tactic:
intro hx
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i j : M
hij : i ≤ j
x : M
hx : x < i
⊢ x < j
Theorem: LO.FirstOrder.Arith.Model.under_subset_under_of_le
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 j : M
hij : i ≤ j
x : M
hx : x < i
⊢ x < j
Tactic:
exact lt_of_lt_of_le hx hij
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sUnion_exists_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 ⊧ₘ* 𝐈𝚺₁
s : M
⊢ ∃! u, ∀ (x : M), x ∈ u ↔ ∃ t ∈ s, x ∈ t
Tactic:
have : 𝚺₁-Predicate fun x ↦ ∃ t ∈ s, x ∈ t := by definability
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
this : 𝚺₁-Predicate fun x => ∃ t ∈ s, x ∈ t
⊢ ∃! u, ∀ (x : M), x ∈ u ↔ ∃ t ∈ s, x ∈ t
Theorem: LO.FirstOrder.Arith.Model.sUnion_exists_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 ⊧ₘ* 𝐈𝚺₁
s : M
this : 𝚺₁-Predicate fun x => ∃ t ∈ s, x ∈ t
⊢ ∃! u, ∀ (x : M), x ∈ u ↔ ∃ t ∈ s, x ∈ t
Tactic:
exact finite_comprehension₁! this
  ⟨s, fun i ↦ by
    rintro ⟨t, ht, hi⟩; exact lt_trans _ _ _ (lt_of_mem hi) (lt_of_mem ht)⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sUnion_exists_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 ⊧ₘ* 𝐈𝚺₁
s : M
⊢ 𝚺₁-Predicate fun x => ∃ t ∈ s, x ∈ t
Tactic:
definability
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sUnion_exists_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 ⊧ₘ* 𝐈𝚺₁
s : M
this : 𝚺₁-Predicate fun x => ∃ t ∈ s, x ∈ t
i : M
⊢ (∃ t ∈ s, i ∈ t) → i < s
Tactic:
rintro ⟨t, ht, hi⟩
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
this : 𝚺₁-Predicate fun x => ∃ t ∈ s, x ∈ t
i t : M
ht : t ∈ s
hi : i ∈ t
⊢ i < s
Theorem: LO.FirstOrder.Arith.Model.sUnion_exists_unique
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
this : 𝚺₁-Predicate fun x => ∃ t ∈ s, x ∈ t
i t : M
ht : t ∈ s
hi : i ∈ t
⊢ i < s
Tactic:
exact lt_trans _ _ _ (lt_of_mem hi) (lt_of_mem ht)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sUnion_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 ⊧ₘ* 𝐈𝚺₁
⊢ ∀ (i : M), i ∈ ⋃ʰᶠ ∅ ↔ i ∈ ∅
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sUnion_lt_of_pos
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
ha : 0 < a
⊢ ∀ i ∈ ⋃ʰᶠ a, i < log a
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 ⊧ₘ* 𝐈𝚺₁
a : M
ha : 0 < a
⊢ ∀ (i x : M), x ∈ a → i ∈ x → i < log a
Theorem: LO.FirstOrder.Arith.Model.sUnion_lt_of_pos
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
ha : 0 < a
⊢ ∀ (i x : M), x ∈ a → i ∈ x → i < log a
Tactic:
intro i x hx 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 ⊧ₘ* 𝐈𝚺₁
a : M
ha : 0 < a
i x : M
hx : x ∈ a
hi : i ∈ x
⊢ i < log a
Theorem: LO.FirstOrder.Arith.Model.sUnion_lt_of_pos
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
ha : 0 < a
i x : M
hx : x ∈ a
hi : i ∈ x
⊢ i < log a
Tactic:
exact lt_of_lt_of_le (lt_of_mem hi) (le_log_of_mem hx)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sUnion_le
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
⊢ ⋃ʰᶠ a ≤ a
Tactic:
rcases zero_le a with (rfl | pos)
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 ⊧ₘ* 𝐈𝚺₁
⊢ ⋃ʰᶠ 0 ≤ 0

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a : M
pos : 0 < a
⊢ ⋃ʰᶠ a ≤ a
Theorem: LO.FirstOrder.Arith.Model.sUnion_le
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 ⊧ₘ* 𝐈𝚺₁
⊢ ⋃ʰᶠ 0 ≤ 0
Tactic:
simp [←emptyset_def]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sUnion_le
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 ⊧ₘ* 𝐈𝚺₁
a : M
pos : 0 < a
⊢ ⋃ʰᶠ a ≤ a
Tactic:
exact le_of_lt (sUnion_lt_of_pos pos)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sUnion_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 ⊧ₘ* 𝐈𝚺₁
u s : M
⊢ u = ⋃ʰᶠ s → ∀ x < u + s, x ∈ u ↔ ∃ t ∈ s, x ∈ t
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
⊢ ∀ x < ⋃ʰᶠ s + s, x ∈ ⋃ʰᶠ s ↔ ∃ t ∈ s, x ∈ t
Theorem: LO.FirstOrder.Arith.Model.sUnion_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
⊢ ∀ x < ⋃ʰᶠ s + s, x ∈ ⋃ʰᶠ s ↔ ∃ t ∈ s, x ∈ t
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sUnion_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 ⊧ₘ* 𝐈𝚺₁
u s : M
⊢ (∀ x < u + s, x ∈ u ↔ ∃ t ∈ s, x ∈ t) → u = ⋃ʰᶠ s
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 ⊧ₘ* 𝐈𝚺₁
u s : M
h : ∀ x < u + s, x ∈ u ↔ ∃ t ∈ s, x ∈ t
⊢ u = ⋃ʰᶠ s
Theorem: LO.FirstOrder.Arith.Model.sUnion_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 ⊧ₘ* 𝐈𝚺₁
u s : M
h : ∀ x < u + s, x ∈ u ↔ ∃ t ∈ s, x ∈ t
⊢ u = ⋃ʰᶠ s
Tactic:
apply mem_ext
Proof state after:
case h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s : M
h : ∀ x < u + s, x ∈ u ↔ ∃ t ∈ s, x ∈ t
⊢ ∀ (i : M), i ∈ u ↔ i ∈ ⋃ʰᶠ s
Theorem: LO.FirstOrder.Arith.Model.sUnion_graph
Proof state before:
case h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s : M
h : ∀ x < u + s, x ∈ u ↔ ∃ t ∈ s, x ∈ t
⊢ ∀ (i : M), i ∈ u ↔ i ∈ ⋃ʰᶠ s
Tactic:
intro x
Proof state after:
case h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s : M
h : ∀ x < u + s, x ∈ u ↔ ∃ t ∈ s, x ∈ t
x : M
⊢ x ∈ u ↔ x ∈ ⋃ʰᶠ s
Theorem: LO.FirstOrder.Arith.Model.sUnion_graph
Proof state before:
case h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s : M
h : ∀ x < u + s, x ∈ u ↔ ∃ t ∈ s, x ∈ t
x : M
⊢ x ∈ u ↔ x ∈ ⋃ʰᶠ s
Tactic:
simp
Proof state after:
case h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s : M
h : ∀ x < u + s, x ∈ u ↔ ∃ t ∈ s, x ∈ t
x : M
⊢ x ∈ u ↔ ∃ c ∈ s, x ∈ c