internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.domain_graph
Proof state before:
case h.mpr
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 ↔ ∃ y < s, ∃ z ∈ s, z = ⟪x, y⟫
x : M
⊢ (∃ y, ⟪x, y⟫ ∈ s) → x ∈ u
Tactic:
rintro ⟨y, hy⟩
Proof state after:
case h.mpr.intro
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 ↔ ∃ y < s, ∃ z ∈ s, z = ⟪x, y⟫
x y : M
hy : ⟪x, y⟫ ∈ s
⊢ x ∈ u
Theorem: LO.FirstOrder.Arith.Model.domain_graph
Proof state before:
case h.mpr.intro
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 ↔ ∃ y < s, ∃ z ∈ s, z = ⟪x, y⟫
x y : M
hy : ⟪x, y⟫ ∈ s
⊢ x ∈ u
Tactic:
exact h x (lt_of_lt_of_le (lt_of_le_of_lt (le_pair_left x y) (lt_of_mem hy)) (by simp))
  |>.mpr ⟨y, lt_of_le_of_lt (le_pair_right x y) (lt_of_mem hy), _, hy, rfl⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.domain_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 ↔ ∃ y < s, ∃ z ∈ s, z = ⟪x, y⟫
x y : M
hy : ⟪x, y⟫ ∈ s
⊢ s ≤ u + s
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.domain_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₁ domain via domainDef
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 => domain (v 0)) fun x => v x.succ) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val domainDef)
Theorem: LO.FirstOrder.Arith.Model.domain_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 => domain (v 0)) fun x => v x.succ) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val domainDef)
Tactic:
simp [domainDef, domain_graph]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.domain_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 ∈ domain ∅ ↔ i ∈ ∅
Tactic:
simp [mem_domain_iff]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.domain_union
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 b : M
⊢ ∀ (i : M), i ∈ domain (a ∪ b) ↔ i ∈ domain a ∪ domain b
Tactic:
simp [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 ⊧ₘ* 𝐈𝚺₁
a b : M
⊢ ∀ (i : M), (∃ y, ⟪i, y⟫ ∈ a ∨ ⟪i, y⟫ ∈ b) ↔ (∃ y, ⟪i, y⟫ ∈ a) ∨ ∃ y, ⟪i, y⟫ ∈ b
Theorem: LO.FirstOrder.Arith.Model.domain_union
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 b : M
⊢ ∀ (i : M), (∃ y, ⟪i, y⟫ ∈ a ∨ ⟪i, y⟫ ∈ b) ↔ (∃ y, ⟪i, y⟫ ∈ a) ∨ ∃ y, ⟪i, y⟫ ∈ b
Tactic:
intro 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 ⊧ₘ* 𝐈𝚺₁
a b x : M
⊢ (∃ y, ⟪x, y⟫ ∈ a ∨ ⟪x, y⟫ ∈ b) ↔ (∃ y, ⟪x, y⟫ ∈ a) ∨ ∃ y, ⟪x, y⟫ ∈ b
Theorem: LO.FirstOrder.Arith.Model.domain_union
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 b x : M
⊢ (∃ y, ⟪x, y⟫ ∈ a ∨ ⟪x, y⟫ ∈ b) ↔ (∃ y, ⟪x, y⟫ ∈ a) ∨ ∃ y, ⟪x, y⟫ ∈ b
Tactic:
constructor
Proof state after:
case mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a b x : M
⊢ (∃ y, ⟪x, y⟫ ∈ a ∨ ⟪x, y⟫ ∈ b) → (∃ y, ⟪x, y⟫ ∈ a) ∨ ∃ y, ⟪x, y⟫ ∈ b

case mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a b x : M
⊢ ((∃ y, ⟪x, y⟫ ∈ a) ∨ ∃ y, ⟪x, y⟫ ∈ b) → ∃ y, ⟪x, y⟫ ∈ a ∨ ⟪x, y⟫ ∈ b
Theorem: LO.FirstOrder.Arith.Model.domain_union
Proof state before:
case mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a b x : M
⊢ (∃ y, ⟪x, y⟫ ∈ a ∨ ⟪x, y⟫ ∈ b) → (∃ y, ⟪x, y⟫ ∈ a) ∨ ∃ y, ⟪x, y⟫ ∈ b
Tactic:
rintro ⟨y, (hy | hy)⟩
Proof state after:
case mp.intro.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a b x y : M
hy : ⟪x, y⟫ ∈ a
⊢ (∃ y, ⟪x, y⟫ ∈ a) ∨ ∃ y, ⟪x, y⟫ ∈ b

case mp.intro.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a b x y : M
hy : ⟪x, y⟫ ∈ b
⊢ (∃ y, ⟪x, y⟫ ∈ a) ∨ ∃ y, ⟪x, y⟫ ∈ b
Theorem: LO.FirstOrder.Arith.Model.domain_union
Proof state before:
case mp.intro.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a b x y : M
hy : ⟪x, y⟫ ∈ a
⊢ (∃ y, ⟪x, y⟫ ∈ a) ∨ ∃ y, ⟪x, y⟫ ∈ b
Tactic:
left
Proof state after:
case mp.intro.inl.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a b x y : M
hy : ⟪x, y⟫ ∈ a
⊢ ∃ y, ⟪x, y⟫ ∈ a
Theorem: LO.FirstOrder.Arith.Model.domain_union
Proof state before:
case mp.intro.inl.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a b x y : M
hy : ⟪x, y⟫ ∈ a
⊢ ∃ y, ⟪x, y⟫ ∈ a
Tactic:
exact ⟨y, hy⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.domain_union
Proof state before:
case mp.intro.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a b x y : M
hy : ⟪x, y⟫ ∈ b
⊢ (∃ y, ⟪x, y⟫ ∈ a) ∨ ∃ y, ⟪x, y⟫ ∈ b
Tactic:
right
Proof state after:
case mp.intro.inr.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a b x y : M
hy : ⟪x, y⟫ ∈ b
⊢ ∃ y, ⟪x, y⟫ ∈ b
Theorem: LO.FirstOrder.Arith.Model.domain_union
Proof state before:
case mp.intro.inr.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a b x y : M
hy : ⟪x, y⟫ ∈ b
⊢ ∃ y, ⟪x, y⟫ ∈ b
Tactic:
exact ⟨y, hy⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.domain_union
Proof state before:
case mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a b x : M
⊢ ((∃ y, ⟪x, y⟫ ∈ a) ∨ ∃ y, ⟪x, y⟫ ∈ b) → ∃ y, ⟪x, y⟫ ∈ a ∨ ⟪x, y⟫ ∈ b
Tactic:
rintro (⟨y, hy⟩ | ⟨y, hy⟩)
Proof state after:
case mpr.inl.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a b x y : M
hy : ⟪x, y⟫ ∈ a
⊢ ∃ y, ⟪x, y⟫ ∈ a ∨ ⟪x, y⟫ ∈ b

case mpr.inr.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a b x y : M
hy : ⟪x, y⟫ ∈ b
⊢ ∃ y, ⟪x, y⟫ ∈ a ∨ ⟪x, y⟫ ∈ b
Theorem: LO.FirstOrder.Arith.Model.domain_union
Proof state before:
case mpr.inl.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a b x y : M
hy : ⟪x, y⟫ ∈ a
⊢ ∃ y, ⟪x, y⟫ ∈ a ∨ ⟪x, y⟫ ∈ b
Tactic:
exact ⟨y, Or.inl hy⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.domain_union
Proof state before:
case mpr.inr.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a b x y : M
hy : ⟪x, y⟫ ∈ b
⊢ ∃ y, ⟪x, y⟫ ∈ a ∨ ⟪x, y⟫ ∈ b
Tactic:
exact ⟨y, Or.inr hy⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.domain_singleton
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
⊢ ∀ (i : M), i ∈ domain {⟪x, y⟫} ↔ i ∈ {x}
Tactic:
simp [mem_domain_iff]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.domain_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 y s : M
⊢ domain (insert ⟪x, y⟫ s) = insert x (domain s)
Tactic:
simp [insert_eq_union_singleton]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.domain_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
⊢ 0 < 2 * s + 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.domain_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
⊢ ∀ i ∈ domain s, i < log (2 * s + 1)
Tactic:
simp [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
⊢ ∀ (i x : M), ⟪i, x⟫ ∈ s → i < log (2 * s + 1)
Theorem: LO.FirstOrder.Arith.Model.domain_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
⊢ ∀ (i x : M), ⟪i, x⟫ ∈ s → i < log (2 * s + 1)
Tactic:
intro i x hix
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 i x : M
hix : ⟪i, x⟫ ∈ s
⊢ i < log (2 * s + 1)
Theorem: LO.FirstOrder.Arith.Model.domain_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 i x : M
hix : ⟪i, x⟫ ∈ s
⊢ i < log (2 * s + 1)
Tactic:
exact lt_of_le_of_lt (le_trans (le_pair_left i x) (le_log_of_mem hix))
  (by simp [log_two_mul_add_one_of_pos (pos_of_nonempty hix)])
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.domain_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 i x : M
hix : ⟪i, x⟫ ∈ s
⊢ log s < log (2 * s + 1)
Tactic:
simp [log_two_mul_add_one_of_pos (pos_of_nonempty hix)]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.domain_subset_domain_of_subset
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 t : M
h : s ⊆ t
⊢ domain s ⊆ domain t
Tactic:
intro x 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 ⊧ₘ* 𝐈𝚺₁
s t : M
h : s ⊆ t
x : M
hx : x ∈ domain s
⊢ x ∈ domain t
Theorem: LO.FirstOrder.Arith.Model.domain_subset_domain_of_subset
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 t : M
h : s ⊆ t
x : M
hx : x ∈ domain s
⊢ x ∈ domain t
Tactic:
rcases mem_domain_iff.mp hx with ⟨y, hy⟩
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 ⊧ₘ* 𝐈𝚺₁
s t : M
h : s ⊆ t
x : M
hx : x ∈ domain s
y : M
hy : ⟪x, y⟫ ∈ s
⊢ x ∈ domain t
Theorem: LO.FirstOrder.Arith.Model.domain_subset_domain_of_subset
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 ⊧ₘ* 𝐈𝚺₁
s t : M
h : s ⊆ t
x : M
hx : x ∈ domain s
y : M
hy : ⟪x, y⟫ ∈ s
⊢ x ∈ domain t
Tactic:
exact mem_domain_iff.mpr ⟨y, h hy⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.domain_eq_empty_iff_eq_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 ⊧ₘ* 𝐈𝚺₁
s : M
⊢ domain s = ∅ → s = ∅
Tactic:
simp [isempty_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
⊢ (∀ (x x_1 : M), ⟪x, x_1⟫ ∉ s) → ∀ (x : M), x ∉ s
Theorem: LO.FirstOrder.Arith.Model.domain_eq_empty_iff_eq_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 ⊧ₘ* 𝐈𝚺₁
s : M
⊢ (∀ (x x_1 : M), ⟪x, x_1⟫ ∉ s) → ∀ (x : M), x ∉ s
Tactic:
intro h x 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 ⊧ₘ* 𝐈𝚺₁
s : M
h : ∀ (x x_1 : M), ⟪x, x_1⟫ ∉ s
x : M
hx : x ∈ s
⊢ False
Theorem: LO.FirstOrder.Arith.Model.domain_eq_empty_iff_eq_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 ⊧ₘ* 𝐈𝚺₁
s : M
h : ∀ (x x_1 : M), ⟪x, x_1⟫ ∉ s
x : M
hx : x ∈ s
⊢ False
Tactic:
exact h (π₁ x) (π₂ x) (by simpa using hx)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.domain_eq_empty_iff_eq_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 ⊧ₘ* 𝐈𝚺₁
s : M
h : ∀ (x x_1 : M), ⟪x, x_1⟫ ∉ s
x : M
hx : x ∈ s
⊢ ⟪π₁ x, π₂ x⟫ ∈ s
Tactic:
simpa using hx
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.domain_eq_empty_iff_eq_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 ⊧ₘ* 𝐈𝚺₁
s : M
⊢ s = ∅ → domain 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 ⊧ₘ* 𝐈𝚺₁
⊢ domain ∅ = ∅
Theorem: LO.FirstOrder.Arith.Model.domain_eq_empty_iff_eq_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 ∅ = ∅
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Disjoint.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 t : M
⊢ Disjoint s t ↔ ∀ (x : M), x ∉ s ∨ x ∉ t
Tactic:
simp [Disjoint, isempty_iff, imp_iff_not_or]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Disjoint.not_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 t x : M
hs : x ∈ s
ht : x ∈ t
⊢ ¬Disjoint s t
Tactic:
simp [Disjoint.iff, not_or]
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 t x : M
hs : x ∈ s
ht : x ∈ t
⊢ ∃ x ∈ s, x ∈ t
Theorem: LO.FirstOrder.Arith.Model.Disjoint.not_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 t x : M
hs : x ∈ s
ht : x ∈ t
⊢ ∃ x ∈ s, x ∈ t
Tactic:
exact ⟨x, hs, ht⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Disjoint.symm
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 t : M
h : Disjoint s t
⊢ Disjoint t s
Tactic:
simpa [Disjoint, inter_comm t s] using h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Disjoint.singleton_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 a : M
⊢ Disjoint {a} s ↔ a ∉ s
Tactic:
simp [Disjoint, isempty_iff]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.isMapping_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 ⊧ₘ* 𝐈𝚺₁
m : M
⊢ IsMapping m → ∃ d ≤ 2 * m, d = domain m ∧ ∀ x ∈ d, ∃ y < m, ⟪x, y⟫ ∈ m ∧ ∀ y' < m, ⟪x, y'⟫ ∈ m → y' = y
Tactic:
intro hm
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m : M
hm : IsMapping m
⊢ ∃ d ≤ 2 * m, d = domain m ∧ ∀ x ∈ d, ∃ y < m, ⟪x, y⟫ ∈ m ∧ ∀ y' < m, ⟪x, y'⟫ ∈ m → y' = y
Theorem: LO.FirstOrder.Arith.Model.isMapping_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 ⊧ₘ* 𝐈𝚺₁
m : M
hm : IsMapping m
⊢ ∃ d ≤ 2 * m, d = domain m ∧ ∀ x ∈ d, ∃ y < m, ⟪x, y⟫ ∈ m ∧ ∀ y' < m, ⟪x, y'⟫ ∈ m → y' = y
Tactic:
exact ⟨domain m, by simp, rfl, fun x hx ↦ by
  rcases hm x hx with ⟨y, hy, uniq⟩
  exact ⟨y, lt_of_mem_rng hy, hy, fun y' _ h' ↦ uniq y' h'⟩⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.isMapping_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 ⊧ₘ* 𝐈𝚺₁
m : M
hm : IsMapping m
⊢ domain m ≤ 2 * m
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.isMapping_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 ⊧ₘ* 𝐈𝚺₁
m : M
hm : IsMapping m
x : M
hx : x ∈ domain m
⊢ ∃ y < m, ⟪x, y⟫ ∈ m ∧ ∀ y' < m, ⟪x, y'⟫ ∈ m → y' = y
Tactic:
rcases hm x hx with ⟨y, hy, uniq⟩
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 ⊧ₘ* 𝐈𝚺₁
m : M
hm : IsMapping m
x : M
hx : x ∈ domain m
y : M
hy : ⟪x, y⟫ ∈ m
uniq : ∀ (y_1 : M), (fun y => ⟪x, y⟫ ∈ m) y_1 → y_1 = y
⊢ ∃ y < m, ⟪x, y⟫ ∈ m ∧ ∀ y' < m, ⟪x, y'⟫ ∈ m → y' = y
Theorem: LO.FirstOrder.Arith.Model.isMapping_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 ⊧ₘ* 𝐈𝚺₁
m : M
hm : IsMapping m
x : M
hx : x ∈ domain m
y : M
hy : ⟪x, y⟫ ∈ m
uniq : ∀ (y_1 : M), (fun y => ⟪x, y⟫ ∈ m) y_1 → y_1 = y
⊢ ∃ y < m, ⟪x, y⟫ ∈ m ∧ ∀ y' < m, ⟪x, y'⟫ ∈ m → y' = y
Tactic:
exact ⟨y, lt_of_mem_rng hy, hy, fun y' _ h' ↦ uniq y' h'⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.isMapping_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 ⊧ₘ* 𝐈𝚺₁
m : M
⊢ (∃ d ≤ 2 * m, d = domain m ∧ ∀ x ∈ d, ∃ y < m, ⟪x, y⟫ ∈ m ∧ ∀ y' < m, ⟪x, y'⟫ ∈ m → y' = y) → IsMapping m
Tactic:
rintro ⟨_, _, rfl, h⟩ x hx
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 ⊧ₘ* 𝐈𝚺₁
m : M
left✝ : domain m ≤ 2 * m
h : ∀ x ∈ domain m, ∃ y < m, ⟪x, y⟫ ∈ m ∧ ∀ y' < m, ⟪x, y'⟫ ∈ m → y' = y
x : M
hx : x ∈ domain m
⊢ ∃! y, ⟪x, y⟫ ∈ m
Theorem: LO.FirstOrder.Arith.Model.isMapping_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 ⊧ₘ* 𝐈𝚺₁
m : M
left✝ : domain m ≤ 2 * m
h : ∀ x ∈ domain m, ∃ y < m, ⟪x, y⟫ ∈ m ∧ ∀ y' < m, ⟪x, y'⟫ ∈ m → y' = y
x : M
hx : x ∈ domain m
⊢ ∃! y, ⟪x, y⟫ ∈ m
Tactic:
rcases h x hx with ⟨y, _, hxy, 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 ⊧ₘ* 𝐈𝚺₁
m : M
left✝¹ : domain m ≤ 2 * m
h✝ : ∀ x ∈ domain m, ∃ y < m, ⟪x, y⟫ ∈ m ∧ ∀ y' < m, ⟪x, y'⟫ ∈ m → y' = y
x : M
hx : x ∈ domain m
y : M
left✝ : y < m
hxy : ⟪x, y⟫ ∈ m
h : ∀ y' < m, ⟪x, y'⟫ ∈ m → y' = y
⊢ ∃! y, ⟪x, y⟫ ∈ m
Theorem: LO.FirstOrder.Arith.Model.isMapping_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 ⊧ₘ* 𝐈𝚺₁
m : M
left✝¹ : domain m ≤ 2 * m
h✝ : ∀ x ∈ domain m, ∃ y < m, ⟪x, y⟫ ∈ m ∧ ∀ y' < m, ⟪x, y'⟫ ∈ m → y' = y
x : M
hx : x ∈ domain m
y : M
left✝ : y < m
hxy : ⟪x, y⟫ ∈ m
h : ∀ y' < m, ⟪x, y'⟫ ∈ m → y' = y
⊢ ∃! y, ⟪x, y⟫ ∈ m
Tactic:
exact ExistsUnique.intro y hxy (fun y' hxy' ↦ h y' (lt_of_mem_rng hxy') hxy')
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.isMapping_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 IsMapping via isMappingDef
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 => IsMapping (v 0)) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val isMappingDef)
Theorem: LO.FirstOrder.Arith.Model.isMapping_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 => IsMapping (v 0)) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val isMappingDef)
Tactic:
simp [isMappingDef, isMapping_iff, lt_succ_iff_le]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.IsMapping.get_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 ⊧ₘ* 𝐈𝚺₁
y m : M
h : IsMapping m
x : M
hx : x ∈ domain m
hy : ⟪x, y⟫ ∈ m
⊢ ⟪x, h.get hx⟫ ∈ m
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.IsMapping.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:
intro 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 ⊧ₘ* 𝐈𝚺₁
x : M
⊢ x ∈ domain ∅ → ∃! y, ⟪x, y⟫ ∈ ∅
Theorem: LO.FirstOrder.Arith.Model.IsMapping.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 ⊧ₘ* 𝐈𝚺₁
x : M
⊢ x ∈ domain ∅ → ∃! y, ⟪x, y⟫ ∈ ∅
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.IsMapping.union_of_disjoint_domain
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
⊢ IsMapping (m₁ ∪ m₂)
Tactic:
intro 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 ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
⊢ x ∈ domain (m₁ ∪ m₂) → ∃! y, ⟪x, y⟫ ∈ m₁ ∪ m₂
Theorem: LO.FirstOrder.Arith.Model.IsMapping.union_of_disjoint_domain
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
⊢ x ∈ domain (m₁ ∪ m₂) → ∃! y, ⟪x, y⟫ ∈ m₁ ∪ m₂
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 ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
⊢ x ∈ domain m₁ ∨ x ∈ domain m₂ → ∃! y, ⟪x, y⟫ ∈ m₁ ∨ ⟪x, y⟫ ∈ m₂
Theorem: LO.FirstOrder.Arith.Model.IsMapping.union_of_disjoint_domain
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
⊢ x ∈ domain m₁ ∨ x ∈ domain m₂ → ∃! y, ⟪x, y⟫ ∈ m₁ ∨ ⟪x, y⟫ ∈ m₂
Tactic:
rintro (hx | hx)
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 ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
hx : x ∈ domain m₁
⊢ ∃! y, ⟪x, y⟫ ∈ m₁ ∨ ⟪x, y⟫ ∈ m₂

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
hx : x ∈ domain m₂
⊢ ∃! y, ⟪x, y⟫ ∈ m₁ ∨ ⟪x, y⟫ ∈ m₂
Theorem: LO.FirstOrder.Arith.Model.IsMapping.union_of_disjoint_domain
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
hx : x ∈ domain m₁
⊢ ⟪x, h₁.get hx⟫ ∈ m₁ ∨ ⟪x, h₁.get hx⟫ ∈ m₂
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.IsMapping.union_of_disjoint_domain
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
hx : x ∈ domain m₁
⊢ ∀ (y : M), ⟪x, y⟫ ∈ m₁ ∨ ⟪x, y⟫ ∈ m₂ → y = h₁.get hx
Tactic:
intro y
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
hx : x ∈ domain m₁
y : M
⊢ ⟪x, y⟫ ∈ m₁ ∨ ⟪x, y⟫ ∈ m₂ → y = h₁.get hx