internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.Seq.mem_seqCons_iff_of_lt
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 s x z : M
hi : i < lh s
⊢ ⟪i, x⟫ ∈ s ⁀' z ↔ ⟪i, x⟫ ∈ s
Tactic:
simp [seqCons, 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 ⊧ₘ* 𝐈𝚺₁
i s x z : M
hi : i < lh s
⊢ i = lh s → x = z → ⟪i, x⟫ ∈ s
Theorem: LO.FirstOrder.Arith.Model.Seq.mem_seqCons_iff_of_lt
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 s x z : M
hi : i < lh s
⊢ i = lh s → x = z → ⟪i, x⟫ ∈ 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 ⊧ₘ* 𝐈𝚺₁
s x z : M
hi : lh s < lh s
⊢ x = z → ⟪lh s, x⟫ ∈ s
Theorem: LO.FirstOrder.Arith.Model.Seq.mem_seqCons_iff_of_lt
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
hi : lh s < lh s
⊢ x = z → ⟪lh s, x⟫ ∈ s
Tactic:
simp at hi
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.seqCons_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 ⊧ₘ* 𝐈𝚺₁
t x s : M
⊢ t = s ⁀' x → ∃ l ≤ 2 * s, l = lh s ∧ ∃ p ≤ (2 * s + x + 1) ^ 2, p = ⟪l, x⟫ ∧ t = insert p 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 ⊧ₘ* 𝐈𝚺₁
x s : M
⊢ ∃ l ≤ 2 * s, l = lh s ∧ ∃ p ≤ (2 * s + x + 1) ^ 2, p = ⟪l, x⟫ ∧ s ⁀' x = insert p s
Theorem: LO.FirstOrder.Arith.Model.seqCons_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 ⊧ₘ* 𝐈𝚺₁
x s : M
⊢ ∃ l ≤ 2 * s, l = lh s ∧ ∃ p ≤ (2 * s + x + 1) ^ 2, p = ⟪l, x⟫ ∧ s ⁀' x = insert p s
Tactic:
exact ⟨lh s, by simp[lt_succ_iff_le], rfl, ⟪lh s, x⟫,
  le_trans (pair_le_pair_left (by simp) x) (pair_polybound (2 * s) x), rfl, by rfl⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.seqCons_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 ⊧ₘ* 𝐈𝚺₁
x s : M
⊢ lh s ≤ 2 * s
Tactic:
simp[lt_succ_iff_le]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.seqCons_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 ⊧ₘ* 𝐈𝚺₁
x s : M
⊢ lh s ≤ 2 * s
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.seqCons_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 ⊧ₘ* 𝐈𝚺₁
x s : M
⊢ s ⁀' x = insert ⟪lh s, x⟫ s
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.seqCons_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 ⊧ₘ* 𝐈𝚺₁
t x s : M
⊢ (∃ l ≤ 2 * s, l = lh s ∧ ∃ p ≤ (2 * s + x + 1) ^ 2, p = ⟪l, x⟫ ∧ t = insert p s) → t = s ⁀' x
Tactic:
rintro ⟨l, _, rfl, p, _, rfl, rfl⟩
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 ⊧ₘ* 𝐈𝚺₁
x s : M
left✝¹ : lh s ≤ 2 * s
left✝ : ⟪lh s, x⟫ ≤ (2 * s + x + 1) ^ 2
⊢ insert ⟪lh s, x⟫ s = s ⁀' x
Theorem: LO.FirstOrder.Arith.Model.seqCons_graph
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 ⊧ₘ* 𝐈𝚺₁
x s : M
left✝¹ : lh s ≤ 2 * s
left✝ : ⟪lh s, x⟫ ≤ (2 * s + x + 1) ^ 2
⊢ insert ⟪lh s, x⟫ s = s ⁀' x
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.seqCons_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₂ seqCons via seqConsDef
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 2) → M
⊢ (fun v => v 0 = (fun v => v 0 ⁀' v 1) fun x => v x.succ) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val seqConsDef)
Theorem: LO.FirstOrder.Arith.Model.seqCons_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 2) → M
⊢ (fun v => v 0 = (fun v => v 0 ⁀' v 1) fun x => v x.succ) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val seqConsDef)
Tactic:
simp [seqConsDef, seqCons_graph]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Seq.restr
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
hi : i ≤ lh s
⊢ under i ⊆ domain s
Tactic:
simp [H.domain_eq, hi]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Seq.restr_lh
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
hi : i ≤ lh s
⊢ under i ⊆ domain s
Tactic:
simp [H.domain_eq, hi]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.domain_bitRemove_of_isMapping_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 ⊧ₘ* 𝐈𝚺₁
x y s : M
hs : IsMapping s
hxy : ⟪x, y⟫ ∈ s
⊢ domain (bitRemove ⟪x, y⟫ s) = bitRemove x (domain 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 ⊧ₘ* 𝐈𝚺₁
x y s : M
hs : IsMapping s
hxy : ⟪x, y⟫ ∈ s
⊢ ∀ (i : M), i ∈ domain (bitRemove ⟪x, y⟫ s) ↔ i ∈ bitRemove x (domain s)
Theorem: LO.FirstOrder.Arith.Model.domain_bitRemove_of_isMapping_of_mem
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 ⊧ₘ* 𝐈𝚺₁
x y s : M
hs : IsMapping s
hxy : ⟪x, y⟫ ∈ s
⊢ ∀ (i : M), i ∈ domain (bitRemove ⟪x, y⟫ s) ↔ i ∈ bitRemove x (domain s)
Tactic:
simp [mem_domain_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 ⊧ₘ* 𝐈𝚺₁
x y s : M
hs : IsMapping s
hxy : ⟪x, y⟫ ∈ s
⊢ ∀ (i : M), (∃ y_1, (i = x → ¬y_1 = y) ∧ ⟪i, y_1⟫ ∈ s) ↔ ¬i = x ∧ ∃ y, ⟪i, y⟫ ∈ s
Theorem: LO.FirstOrder.Arith.Model.domain_bitRemove_of_isMapping_of_mem
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 ⊧ₘ* 𝐈𝚺₁
x y s : M
hs : IsMapping s
hxy : ⟪x, y⟫ ∈ s
⊢ ∀ (i : M), (∃ y_1, (i = x → ¬y_1 = y) ∧ ⟪i, y_1⟫ ∈ s) ↔ ¬i = x ∧ ∃ y, ⟪i, y⟫ ∈ 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 ⊧ₘ* 𝐈𝚺₁
x y s : M
hs : IsMapping s
hxy : ⟪x, y⟫ ∈ s
x₁ : M
⊢ (∃ y_1, (x₁ = x → ¬y_1 = y) ∧ ⟪x₁, y_1⟫ ∈ s) ↔ ¬x₁ = x ∧ ∃ y, ⟪x₁, y⟫ ∈ s
Theorem: LO.FirstOrder.Arith.Model.domain_bitRemove_of_isMapping_of_mem
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 ⊧ₘ* 𝐈𝚺₁
x y s : M
hs : IsMapping s
hxy : ⟪x, y⟫ ∈ s
x₁ : M
⊢ (∃ y_1, (x₁ = x → ¬y_1 = y) ∧ ⟪x₁, y_1⟫ ∈ s) ↔ ¬x₁ = x ∧ ∃ y, ⟪x₁, y⟫ ∈ s
Tactic:
constructor
Proof state after:
case h.mp
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
hs : IsMapping s
hxy : ⟪x, y⟫ ∈ s
x₁ : M
⊢ (∃ y_1, (x₁ = x → ¬y_1 = y) ∧ ⟪x₁, y_1⟫ ∈ s) → ¬x₁ = x ∧ ∃ y, ⟪x₁, y⟫ ∈ s

case h.mpr
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
hs : IsMapping s
hxy : ⟪x, y⟫ ∈ s
x₁ : M
⊢ (¬x₁ = x ∧ ∃ y, ⟪x₁, y⟫ ∈ s) → ∃ y_1, (x₁ = x → ¬y_1 = y) ∧ ⟪x₁, y_1⟫ ∈ s
Theorem: LO.FirstOrder.Arith.Model.domain_bitRemove_of_isMapping_of_mem
Proof state before:
case h.mp
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
hs : IsMapping s
hxy : ⟪x, y⟫ ∈ s
x₁ : M
⊢ (∃ y_1, (x₁ = x → ¬y_1 = y) ∧ ⟪x₁, y_1⟫ ∈ s) → ¬x₁ = x ∧ ∃ y, ⟪x₁, y⟫ ∈ s
Tactic:
rintro ⟨y₁, hy₁, hx₁y₁⟩
Proof state after:
case h.mp.intro.intro
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
hs : IsMapping s
hxy : ⟪x, y⟫ ∈ s
x₁ y₁ : M
hy₁ : x₁ = x → ¬y₁ = y
hx₁y₁ : ⟪x₁, y₁⟫ ∈ s
⊢ ¬x₁ = x ∧ ∃ y, ⟪x₁, y⟫ ∈ s
Theorem: LO.FirstOrder.Arith.Model.domain_bitRemove_of_isMapping_of_mem
Proof state before:
case h.mp.intro.intro
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
hs : IsMapping s
hxy : ⟪x, y⟫ ∈ s
x₁ y₁ : M
hy₁ : x₁ = x → ¬y₁ = y
hx₁y₁ : ⟪x₁, y₁⟫ ∈ s
⊢ ¬x₁ = x ∧ ∃ y, ⟪x₁, y⟫ ∈ s
Tactic:
exact ⟨by rintro rfl; exact hy₁ rfl (hs.uniq hx₁y₁ hxy), y₁, hx₁y₁⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.domain_bitRemove_of_isMapping_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 ⊧ₘ* 𝐈𝚺₁
x y s : M
hs : IsMapping s
hxy : ⟪x, y⟫ ∈ s
x₁ y₁ : M
hy₁ : x₁ = x → ¬y₁ = y
hx₁y₁ : ⟪x₁, y₁⟫ ∈ s
⊢ ¬x₁ = x
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 ⊧ₘ* 𝐈𝚺₁
y s : M
hs : IsMapping s
x₁ y₁ : M
hx₁y₁ : ⟪x₁, y₁⟫ ∈ s
hxy : ⟪x₁, y⟫ ∈ s
hy₁ : x₁ = x₁ → ¬y₁ = y
⊢ False
Theorem: LO.FirstOrder.Arith.Model.domain_bitRemove_of_isMapping_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 ⊧ₘ* 𝐈𝚺₁
y s : M
hs : IsMapping s
x₁ y₁ : M
hx₁y₁ : ⟪x₁, y₁⟫ ∈ s
hxy : ⟪x₁, y⟫ ∈ s
hy₁ : x₁ = x₁ → ¬y₁ = y
⊢ False
Tactic:
exact hy₁ rfl (hs.uniq hx₁y₁ hxy)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.domain_bitRemove_of_isMapping_of_mem
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 ⊧ₘ* 𝐈𝚺₁
x y s : M
hs : IsMapping s
hxy : ⟪x, y⟫ ∈ s
x₁ : M
⊢ (¬x₁ = x ∧ ∃ y, ⟪x₁, y⟫ ∈ s) → ∃ y_1, (x₁ = x → ¬y_1 = y) ∧ ⟪x₁, y_1⟫ ∈ s
Tactic:
intro ⟨hx, y₁, hx₁y₁⟩
Proof state after:
case h.mpr
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
hs : IsMapping s
hxy : ⟪x, y⟫ ∈ s
x₁ : M
hx : ¬x₁ = x
y₁ : M
hx₁y₁ : ⟪x₁, y₁⟫ ∈ s
⊢ ∃ y_1, (x₁ = x → ¬y_1 = y) ∧ ⟪x₁, y_1⟫ ∈ s
Theorem: LO.FirstOrder.Arith.Model.domain_bitRemove_of_isMapping_of_mem
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 ⊧ₘ* 𝐈𝚺₁
x y s : M
hs : IsMapping s
hxy : ⟪x, y⟫ ∈ s
x₁ : M
hx : ¬x₁ = x
y₁ : M
hx₁y₁ : ⟪x₁, y₁⟫ ∈ s
⊢ ∃ y_1, (x₁ = x → ¬y_1 = y) ∧ ⟪x₁, y_1⟫ ∈ s
Tactic:
exact ⟨y₁, by intro _; contradiction, hx₁y₁⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.domain_bitRemove_of_isMapping_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 ⊧ₘ* 𝐈𝚺₁
x y s : M
hs : IsMapping s
hxy : ⟪x, y⟫ ∈ s
x₁ : M
hx : ¬x₁ = x
y₁ : M
hx₁y₁ : ⟪x₁, y₁⟫ ∈ s
⊢ x₁ = x → ¬y₁ = y
Tactic:
intro _
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 y s : M
hs : IsMapping s
hxy : ⟪x, y⟫ ∈ s
x₁ : M
hx : ¬x₁ = x
y₁ : M
hx₁y₁ : ⟪x₁, y₁⟫ ∈ s
a✝ : x₁ = x
⊢ ¬y₁ = y
Theorem: LO.FirstOrder.Arith.Model.domain_bitRemove_of_isMapping_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 ⊧ₘ* 𝐈𝚺₁
x y s : M
hs : IsMapping s
hxy : ⟪x, y⟫ ∈ s
x₁ : M
hx : ¬x₁ = x
y₁ : M
hx₁y₁ : ⟪x₁, y₁⟫ ∈ s
a✝ : x₁ = x
⊢ ¬y₁ = y
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Seq.eq_of_eq_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₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
hl : lh s₁ = lh s₂
h : s₁ ⊆ s₂
⊢ s₁ = 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 ⊧ₘ* 𝐈𝚺₁
s₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
hl : lh s₁ = lh s₂
h : s₁ ⊆ s₂
⊢ ∀ (i : M), i ∈ s₁ ↔ i ∈ s₂
Theorem: LO.FirstOrder.Arith.Model.Seq.eq_of_eq_of_subset
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 ⊧ₘ* 𝐈𝚺₁
s₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
hl : lh s₁ = lh s₂
h : s₁ ⊆ s₂
⊢ ∀ (i : M), i ∈ s₁ ↔ i ∈ s₂
Tactic:
intro u
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 ⊧ₘ* 𝐈𝚺₁
s₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
hl : lh s₁ = lh s₂
h : s₁ ⊆ s₂
u : M
⊢ u ∈ s₁ ↔ u ∈ s₂
Theorem: LO.FirstOrder.Arith.Model.Seq.eq_of_eq_of_subset
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 ⊧ₘ* 𝐈𝚺₁
s₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
hl : lh s₁ = lh s₂
h : s₁ ⊆ s₂
u : M
⊢ u ∈ s₁ ↔ u ∈ s₂
Tactic:
constructor
Proof state after:
case h.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
hl : lh s₁ = lh s₂
h : s₁ ⊆ s₂
u : M
⊢ u ∈ s₁ → u ∈ s₂

case h.mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
hl : lh s₁ = lh s₂
h : s₁ ⊆ s₂
u : M
⊢ u ∈ s₂ → u ∈ s₁
Theorem: LO.FirstOrder.Arith.Model.Seq.eq_of_eq_of_subset
Proof state before:
case h.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
hl : lh s₁ = lh s₂
h : s₁ ⊆ s₂
u : M
⊢ u ∈ s₁ → u ∈ s₂
Tactic:
intro hu
Proof state after:
case h.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
hl : lh s₁ = lh s₂
h : s₁ ⊆ s₂
u : M
hu : u ∈ s₁
⊢ u ∈ s₂
Theorem: LO.FirstOrder.Arith.Model.Seq.eq_of_eq_of_subset
Proof state before:
case h.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
hl : lh s₁ = lh s₂
h : s₁ ⊆ s₂
u : M
hu : u ∈ s₁
⊢ u ∈ s₂
Tactic:
exact h hu
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Seq.eq_of_eq_of_subset
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 ⊧ₘ* 𝐈𝚺₁
s₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
hl : lh s₁ = lh s₂
h : s₁ ⊆ s₂
u : M
⊢ u ∈ s₂ → u ∈ s₁
Tactic:
intro hu
Proof state after:
case h.mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
hl : lh s₁ = lh s₂
h : s₁ ⊆ s₂
u : M
hu : u ∈ s₂
⊢ u ∈ s₁
Theorem: LO.FirstOrder.Arith.Model.Seq.eq_of_eq_of_subset
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 ⊧ₘ* 𝐈𝚺₁
s₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
hl : lh s₁ = lh s₂
h : s₁ ⊆ s₂
u : M
hu : u ∈ s₂
⊢ u ∈ s₁
Tactic:
have : π₁ u < lh s₁ := by simpa [hl] using H₂.lt_lh_of_mem (show ⟪π₁ u, π₂ u⟫ ∈ s₂ from by simpa using hu)
Proof state after:
case h.mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
hl : lh s₁ = lh s₂
h : s₁ ⊆ s₂
u : M
hu : u ∈ s₂
this : π₁ u < lh s₁
⊢ u ∈ s₁
Theorem: LO.FirstOrder.Arith.Model.Seq.eq_of_eq_of_subset
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 ⊧ₘ* 𝐈𝚺₁
s₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
hl : lh s₁ = lh s₂
h : s₁ ⊆ s₂
u : M
hu : u ∈ s₂
this : π₁ u < lh s₁
⊢ u ∈ s₁
Tactic:
have : ∃ y, ⟪π₁ u, y⟫ ∈ s₁ := H₁.exists this
Proof state after:
case h.mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
hl : lh s₁ = lh s₂
h : s₁ ⊆ s₂
u : M
hu : u ∈ s₂
this✝ : π₁ u < lh s₁
this : ∃ y, ⟪π₁ u, y⟫ ∈ s₁
⊢ u ∈ s₁
Theorem: LO.FirstOrder.Arith.Model.Seq.eq_of_eq_of_subset
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 ⊧ₘ* 𝐈𝚺₁
s₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
hl : lh s₁ = lh s₂
h : s₁ ⊆ s₂
u : M
hu : u ∈ s₂
this✝ : π₁ u < lh s₁
this : ∃ y, ⟪π₁ u, y⟫ ∈ s₁
⊢ u ∈ s₁
Tactic:
rcases this with ⟨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 ⊧ₘ* 𝐈𝚺₁
s₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
hl : lh s₁ = lh s₂
h : s₁ ⊆ s₂
u : M
hu : u ∈ s₂
this : π₁ u < lh s₁
y : M
hy : ⟪π₁ u, y⟫ ∈ s₁
⊢ u ∈ s₁
Theorem: LO.FirstOrder.Arith.Model.Seq.eq_of_eq_of_subset
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 ⊧ₘ* 𝐈𝚺₁
s₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
hl : lh s₁ = lh s₂
h : s₁ ⊆ s₂
u : M
hu : u ∈ s₂
this : π₁ u < lh s₁
y : M
hy : ⟪π₁ u, y⟫ ∈ s₁
⊢ u ∈ s₁
Tactic:
have : y = π₂ u := H₂.isMapping.uniq (h hy) (show ⟪π₁ u, π₂ u⟫ ∈ s₂ from by simpa using hu)
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 ⊧ₘ* 𝐈𝚺₁
s₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
hl : lh s₁ = lh s₂
h : s₁ ⊆ s₂
u : M
hu : u ∈ s₂
this✝ : π₁ u < lh s₁
y : M
hy : ⟪π₁ u, y⟫ ∈ s₁
this : y = π₂ u
⊢ u ∈ s₁
Theorem: LO.FirstOrder.Arith.Model.Seq.eq_of_eq_of_subset
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 ⊧ₘ* 𝐈𝚺₁
s₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
hl : lh s₁ = lh s₂
h : s₁ ⊆ s₂
u : M
hu : u ∈ s₂
this✝ : π₁ u < lh s₁
y : M
hy : ⟪π₁ u, y⟫ ∈ s₁
this : y = π₂ u
⊢ u ∈ s₁
Tactic:
rcases this with rfl
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 ⊧ₘ* 𝐈𝚺₁
s₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
hl : lh s₁ = lh s₂
h : s₁ ⊆ s₂
u : M
hu : u ∈ s₂
this : π₁ u < lh s₁
hy : ⟪π₁ u, π₂ u⟫ ∈ s₁
⊢ u ∈ s₁
Theorem: LO.FirstOrder.Arith.Model.Seq.eq_of_eq_of_subset
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 ⊧ₘ* 𝐈𝚺₁
s₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
hl : lh s₁ = lh s₂
h : s₁ ⊆ s₂
u : M
hu : u ∈ s₂
this : π₁ u < lh s₁
hy : ⟪π₁ u, π₂ u⟫ ∈ s₁
⊢ u ∈ s₁
Tactic:
simpa using hy
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Seq.eq_of_eq_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₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
hl : lh s₁ = lh s₂
h : s₁ ⊆ s₂
u : M
hu : u ∈ s₂
⊢ π₁ u < lh s₁
Tactic:
simpa [hl] using H₂.lt_lh_of_mem (show ⟪π₁ u, π₂ u⟫ ∈ s₂ from by simpa using hu)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Seq.eq_of_eq_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₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
hl : lh s₁ = lh s₂
h : s₁ ⊆ s₂
u : M
hu : u ∈ s₂
⊢ ⟪π₁ u, π₂ u⟫ ∈ s₂
Tactic:
simpa using hu
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Seq.eq_of_eq_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₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
hl : lh s₁ = lh s₂
h : s₁ ⊆ s₂
u : M
hu : u ∈ s₂
this : π₁ u < lh s₁
y : M
hy : ⟪π₁ u, y⟫ ∈ s₁
⊢ ⟪π₁ u, π₂ u⟫ ∈ s₂
Tactic:
simpa using hu
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.subset_pair
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 : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, x⟫ ∈ t
⊢ s ⊆ t
Tactic:
intro u hu
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 : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, x⟫ ∈ t
u : M
hu : u ∈ s
⊢ u ∈ t
Theorem: LO.FirstOrder.Arith.Model.subset_pair
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 : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, x⟫ ∈ t
u : M
hu : u ∈ s
⊢ u ∈ t
Tactic:
simpa using h (π₁ u) (π₂ u) (by simpa using hu)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.subset_pair
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 : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, x⟫ ∈ t
u : M
hu : u ∈ s
⊢ ⟪π₁ u, π₂ u⟫ ∈ s
Tactic:
simpa using hu
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Seq.seqCons_ext
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₁ a₂ s₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
⊢ s₁ ⁀' a₁ = s₂ ⁀' a₂ → a₁ = a₂ ∧ s₁ = 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 ⊧ₘ* 𝐈𝚺₁
a₁ a₂ s₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
h : s₁ ⁀' a₁ = s₂ ⁀' a₂
⊢ a₁ = a₂ ∧ s₁ = s₂
Theorem: LO.FirstOrder.Arith.Model.Seq.seqCons_ext
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₁ a₂ s₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
h : s₁ ⁀' a₁ = s₂ ⁀' a₂
⊢ a₁ = a₂ ∧ s₁ = s₂
Tactic:
have hs₁s₂ : lh s₁ = lh s₂ := by simpa [H₁, H₂] using congr_arg lh 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 ⊧ₘ* 𝐈𝚺₁
a₁ a₂ s₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
h : s₁ ⁀' a₁ = s₂ ⁀' a₂
hs₁s₂ : lh s₁ = lh s₂
⊢ a₁ = a₂ ∧ s₁ = s₂
Theorem: LO.FirstOrder.Arith.Model.Seq.seqCons_ext
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₁ a₂ s₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
h : s₁ ⁀' a₁ = s₂ ⁀' a₂
hs₁s₂ : lh s₁ = lh s₂
⊢ a₁ = a₂ ∧ s₁ = s₂
Tactic:
have hs₁ : ⟪lh s₁, a₁⟫ ∈ s₂ ⁀' a₂ := by simpa [h] using lh_mem_seqCons s₁ 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 ⊧ₘ* 𝐈𝚺₁
a₁ a₂ s₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
h : s₁ ⁀' a₁ = s₂ ⁀' a₂
hs₁s₂ : lh s₁ = lh s₂
hs₁ : ⟪lh s₁, a₁⟫ ∈ s₂ ⁀' a₂
⊢ a₁ = a₂ ∧ s₁ = s₂
Theorem: LO.FirstOrder.Arith.Model.Seq.seqCons_ext
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₁ a₂ s₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
h : s₁ ⁀' a₁ = s₂ ⁀' a₂
hs₁s₂ : lh s₁ = lh s₂
hs₁ : ⟪lh s₁, a₁⟫ ∈ s₂ ⁀' a₂
⊢ a₁ = a₂ ∧ s₁ = s₂
Tactic:
have hs₂ : ⟪lh s₁, a₂⟫ ∈ s₂ ⁀' a₂ := by simp [hs₁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 ⊧ₘ* 𝐈𝚺₁
a₁ a₂ s₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
h : s₁ ⁀' a₁ = s₂ ⁀' a₂
hs₁s₂ : lh s₁ = lh s₂
hs₁ : ⟪lh s₁, a₁⟫ ∈ s₂ ⁀' a₂
hs₂ : ⟪lh s₁, a₂⟫ ∈ s₂ ⁀' a₂
⊢ a₁ = a₂ ∧ s₁ = s₂
Theorem: LO.FirstOrder.Arith.Model.Seq.seqCons_ext
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₁ a₂ s₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
h : s₁ ⁀' a₁ = s₂ ⁀' a₂
hs₁s₂ : lh s₁ = lh s₂
hs₁ : ⟪lh s₁, a₁⟫ ∈ s₂ ⁀' a₂
hs₂ : ⟪lh s₁, a₂⟫ ∈ s₂ ⁀' a₂
⊢ a₁ = a₂ ∧ s₁ = s₂
Tactic:
have ha₁a₂ : a₁ = a₂ := (H₂.seqCons a₂).isMapping.uniq hs₁ hs₂
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₁ a₂ s₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
h : s₁ ⁀' a₁ = s₂ ⁀' a₂
hs₁s₂ : lh s₁ = lh s₂
hs₁ : ⟪lh s₁, a₁⟫ ∈ s₂ ⁀' a₂
hs₂ : ⟪lh s₁, a₂⟫ ∈ s₂ ⁀' a₂
ha₁a₂ : a₁ = a₂
⊢ a₁ = a₂ ∧ s₁ = s₂