internlm/Lean-Github huggingface dataset:
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₂
ha₁a₂ : a₁ = a₂
this : s₁ ⊆ s₂
⊢ a₁ = a₂ ∧ s₁ = s₂
Tactic:
exact ⟨ha₁a₂, H₁.eq_of_eq_of_subset H₂ hs₁s₂ this⟩
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₂
h : s₁ ⁀' a₁ = s₂ ⁀' a₂
⊢ lh s₁ = lh s₂
Tactic:
simpa [H₁, H₂] using congr_arg lh h
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₂
h : s₁ ⁀' a₁ = s₂ ⁀' a₂
hs₁s₂ : lh s₁ = lh s₂
⊢ ⟪lh s₁, a₁⟫ ∈ s₂ ⁀' a₂
Tactic:
simpa [h] using lh_mem_seqCons s₁ a₁
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₂
h : s₁ ⁀' a₁ = s₂ ⁀' a₂
hs₁s₂ : lh s₁ = lh s₂
hs₁ : ⟪lh s₁, a₁⟫ ∈ s₂ ⁀' a₂
⊢ ⟪lh s₁, a₂⟫ ∈ s₂ ⁀' a₂
Tactic:
simp [hs₁s₂]
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₂
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₂
⊢ ∀ (i x : M), ⟪i, x⟫ ∈ s₁ → ⟪i, x⟫ ∈ s₂
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 ⊧ₘ* 𝐈𝚺₁
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₂
i x : M
hix : ⟪i, x⟫ ∈ s₁
⊢ ⟪i, x⟫ ∈ 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₂
ha₁a₂ : a₁ = a₂
i x : M
hix : ⟪i, x⟫ ∈ s₁
⊢ ⟪i, x⟫ ∈ s₂
Tactic:
have : i = lh s₂ ∧ x = a₂ ∨ ⟪i, x⟫ ∈ s₂ := by simpa [mem_seqCons_iff, h] using Seq.subset_seqCons s₁ a₁ 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 ⊧ₘ* 𝐈𝚺₁
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₂
i x : M
hix : ⟪i, x⟫ ∈ s₁
this : i = lh s₂ ∧ x = a₂ ∨ ⟪i, x⟫ ∈ s₂
⊢ ⟪i, x⟫ ∈ 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₂
ha₁a₂ : a₁ = a₂
i x : M
hix : ⟪i, x⟫ ∈ s₁
this : i = lh s₂ ∧ x = a₂ ∨ ⟪i, x⟫ ∈ s₂
⊢ ⟪i, x⟫ ∈ s₂
Tactic:
rcases this with (⟨rfl, rfl⟩ | hix₂)
Proof state after:
case inl.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a₁ s₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
hs₁s₂ : lh s₁ = lh s₂
x : M
hix : ⟪lh s₂, x⟫ ∈ s₁
h : s₁ ⁀' a₁ = s₂ ⁀' x
hs₁ : ⟪lh s₁, a₁⟫ ∈ s₂ ⁀' x
hs₂ : ⟪lh s₁, x⟫ ∈ s₂ ⁀' x
ha₁a₂ : a₁ = x
⊢ ⟪lh s₂, x⟫ ∈ s₂

case inr
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₂
i x : M
hix : ⟪i, x⟫ ∈ s₁
hix₂ : ⟪i, x⟫ ∈ s₂
⊢ ⟪i, x⟫ ∈ 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₂
ha₁a₂ : a₁ = a₂
i x : M
hix : ⟪i, x⟫ ∈ s₁
⊢ i = lh s₂ ∧ x = a₂ ∨ ⟪i, x⟫ ∈ s₂
Tactic:
simpa [mem_seqCons_iff, h] using Seq.subset_seqCons s₁ a₁ hix
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Seq.seqCons_ext
Proof state before:
case inl.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a₁ s₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
hs₁s₂ : lh s₁ = lh s₂
x : M
hix : ⟪lh s₂, x⟫ ∈ s₁
h : s₁ ⁀' a₁ = s₂ ⁀' x
hs₁ : ⟪lh s₁, a₁⟫ ∈ s₂ ⁀' x
hs₂ : ⟪lh s₁, x⟫ ∈ s₂ ⁀' x
ha₁a₂ : a₁ = x
⊢ ⟪lh s₂, x⟫ ∈ s₂
Tactic:
have := H₁.lt_lh_of_mem hix
Proof state after:
case inl.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a₁ s₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
hs₁s₂ : lh s₁ = lh s₂
x : M
hix : ⟪lh s₂, x⟫ ∈ s₁
h : s₁ ⁀' a₁ = s₂ ⁀' x
hs₁ : ⟪lh s₁, a₁⟫ ∈ s₂ ⁀' x
hs₂ : ⟪lh s₁, x⟫ ∈ s₂ ⁀' x
ha₁a₂ : a₁ = x
this : lh s₂ < lh s₁
⊢ ⟪lh s₂, x⟫ ∈ s₂
Theorem: LO.FirstOrder.Arith.Model.Seq.seqCons_ext
Proof state before:
case inl.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a₁ s₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
hs₁s₂ : lh s₁ = lh s₂
x : M
hix : ⟪lh s₂, x⟫ ∈ s₁
h : s₁ ⁀' a₁ = s₂ ⁀' x
hs₁ : ⟪lh s₁, a₁⟫ ∈ s₂ ⁀' x
hs₂ : ⟪lh s₁, x⟫ ∈ s₂ ⁀' x
ha₁a₂ : a₁ = x
this : lh s₂ < lh s₁
⊢ ⟪lh s₂, x⟫ ∈ s₂
Tactic:
simp [hs₁s₂] at this
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Seq.seqCons_ext
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₁ 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₂
i x : M
hix : ⟪i, x⟫ ∈ s₁
hix₂ : ⟪i, x⟫ ∈ s₂
⊢ ⟪i, x⟫ ∈ s₂
Tactic:
assumption
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₂
⊢ a₁ = a₂ ∧ s₁ = s₂ → s₁ ⁀' a₁ = s₂ ⁀' a₂
Tactic:
rintro ⟨rfl, rfl⟩
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 ⊧ₘ* 𝐈𝚺₁
a₁ s₁ : M
H₁ H₂ : Seq s₁
⊢ s₁ ⁀' a₁ = s₁ ⁀' a₁
Theorem: LO.FirstOrder.Arith.Model.Seq.seqCons_ext
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 ⊧ₘ* 𝐈𝚺₁
a₁ s₁ : M
H₁ H₂ : Seq s₁
⊢ s₁ ⁀' a₁ = s₁ ⁀' a₁
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Seq.cases_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
⊢ s = ∅ ∨ ∃ x s', Seq s' ∧ s = s' ⁀' x
Tactic:
by_cases hs : lh s = 0
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
hs : lh s = 0
⊢ s = ∅ ∨ ∃ x s', Seq s' ∧ s = s' ⁀' x

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
hs : ¬lh s = 0
⊢ s = ∅ ∨ ∃ x s', Seq s' ∧ s = s' ⁀' x
Theorem: LO.FirstOrder.Arith.Model.Seq.cases_iff
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
hs : lh s = 0
⊢ s = ∅ ∨ ∃ x s', Seq s' ∧ s = s' ⁀' x
Tactic:
left
Proof state after:
case pos.h
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
hs : lh s = 0
⊢ s = ∅
Theorem: LO.FirstOrder.Arith.Model.Seq.cases_iff
Proof state before:
case pos.h
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
hs : lh s = 0
⊢ s = ∅
Tactic:
simpa [hs] using h.domain_eq
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Seq.cases_iff
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
hs : ¬lh s = 0
⊢ s = ∅ ∨ ∃ x s', Seq s' ∧ s = s' ⁀' x
Tactic:
right
Proof state after:
case neg.h
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
hs : ¬lh s = 0
⊢ ∃ x s', Seq s' ∧ s = s' ⁀' x
Theorem: LO.FirstOrder.Arith.Model.Seq.cases_iff
Proof state before:
case neg.h
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
hs : ¬lh s = 0
⊢ ∃ x s', Seq s' ∧ s = s' ⁀' x
Tactic:
let i := lh s - 1
Proof state after:
case neg.h
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
hs : ¬lh s = 0
i : M := lh s - 1
⊢ ∃ x s', Seq s' ∧ s = s' ⁀' x
Theorem: LO.FirstOrder.Arith.Model.Seq.cases_iff
Proof state before:
case neg.h
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
hs : ¬lh s = 0
i : M := lh s - 1
⊢ ∃ x s', Seq s' ∧ s = s' ⁀' x
Tactic:
have hi : i < lh s := pred_lt_self_of_pos (pos_iff_ne_zero.mpr hs)
Proof state after:
case neg.h
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
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
⊢ ∃ x s', Seq s' ∧ s = s' ⁀' x
Theorem: LO.FirstOrder.Arith.Model.Seq.cases_iff
Proof state before:
case neg.h
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
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
⊢ ∃ x s', Seq s' ∧ s = s' ⁀' x
Tactic:
have lhs_eq : lh s = i + 1 := Eq.symm <| tsub_add_cancel_of_le <| ne_zero_iff_one_le.mp hs
Proof state after:
case neg.h
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
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
⊢ ∃ x s', Seq s' ∧ s = s' ⁀' x
Theorem: LO.FirstOrder.Arith.Model.Seq.cases_iff
Proof state before:
case neg.h
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
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
⊢ ∃ x s', Seq s' ∧ s = s' ⁀' x
Tactic:
let s' := bitRemove ⟪i, h.nth hi⟫ s
Proof state after:
case neg.h
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
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
⊢ ∃ x s', Seq s' ∧ s = s' ⁀' x
Theorem: LO.FirstOrder.Arith.Model.Seq.cases_iff
Proof state before:
case neg.h
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
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
⊢ ∃ x s', Seq s' ∧ s = s' ⁀' x
Tactic:
have his : ⟪i, h.nth hi⟫ ∈ s := h.nth_mem hi
Proof state after:
case neg.h
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
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
⊢ ∃ x s', Seq s' ∧ s = s' ⁀' x
Theorem: LO.FirstOrder.Arith.Model.Seq.cases_iff
Proof state before:
case neg.h
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
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
⊢ ∃ x s', Seq s' ∧ s = s' ⁀' x
Tactic:
have hdoms' : domain s' = under i := by
  simp only [domain_bitRemove_of_isMapping_of_mem h.isMapping his, h.domain_eq, s']
  apply mem_ext
  simp [lhs_eq, and_or_left]
  intro j hj; exact ne_of_lt hj
Proof state after:
case neg.h
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
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
hdoms' : domain s' = under i
⊢ ∃ x s', Seq s' ∧ s = s' ⁀' x
Theorem: LO.FirstOrder.Arith.Model.Seq.cases_iff
Proof state before:
case neg.h
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
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
hdoms' : domain s' = under i
⊢ ∃ x s', Seq s' ∧ s = s' ⁀' x
Tactic:
have hs' : Seq s' := ⟨ h.isMapping.of_subset (by simp [s']), i, hdoms' ⟩
Proof state after:
case neg.h
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
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
hdoms' : domain s' = under i
hs' : Seq s'
⊢ ∃ x s', Seq s' ∧ s = s' ⁀' x
Theorem: LO.FirstOrder.Arith.Model.Seq.cases_iff
Proof state before:
case neg.h
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
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
hdoms' : domain s' = under i
hs' : Seq s'
⊢ ∃ x s', Seq s' ∧ s = s' ⁀' x
Tactic:
have hs'i : lh s' = i := by simpa [hs'.domain_eq] using hdoms'
Proof state after:
case neg.h
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
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
hdoms' : domain s' = under i
hs' : Seq s'
hs'i : lh s' = i
⊢ ∃ x s', Seq s' ∧ s = s' ⁀' x
Theorem: LO.FirstOrder.Arith.Model.Seq.cases_iff
Proof state before:
case neg.h
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
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
hdoms' : domain s' = under i
hs' : Seq s'
hs'i : lh s' = i
⊢ ∃ x s', Seq s' ∧ s = s' ⁀' x
Tactic:
exact ⟨h.nth hi, s', hs', mem_ext <| fun v ↦ by
  simp only [seqCons, hs'i, mem_bitInsert_iff]
  simp [s']
  by_cases hv : v = ⟪i, h.nth hi⟫ <;> simp [hv]⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Seq.cases_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
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
⊢ domain s' = under i
Tactic:
simp only [domain_bitRemove_of_isMapping_of_mem h.isMapping his, h.domain_eq, 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
h : Seq s
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
⊢ bitRemove i (under (lh s)) = under i
Theorem: LO.FirstOrder.Arith.Model.Seq.cases_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
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
⊢ bitRemove i (under (lh s)) = under i
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 : M
h : Seq s
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
⊢ ∀ (i_1 : M), i_1 ∈ bitRemove i (under (lh s)) ↔ i_1 ∈ under i
Theorem: LO.FirstOrder.Arith.Model.Seq.cases_iff
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 : M
h : Seq s
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
⊢ ∀ (i_1 : M), i_1 ∈ bitRemove i (under (lh s)) ↔ i_1 ∈ under i
Tactic:
simp [lhs_eq, and_or_left]
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 : M
h : Seq s
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
⊢ ∀ i_1 < i, ¬i_1 = i
Theorem: LO.FirstOrder.Arith.Model.Seq.cases_iff
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 : M
h : Seq s
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
⊢ ∀ i_1 < i, ¬i_1 = i
Tactic:
intro j hj
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 : M
h : Seq s
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
j : M
hj : j < i
⊢ ¬j = i
Theorem: LO.FirstOrder.Arith.Model.Seq.cases_iff
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 : M
h : Seq s
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
j : M
hj : j < i
⊢ ¬j = i
Tactic:
exact ne_of_lt hj
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Seq.cases_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
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
hdoms' : domain s' = under i
⊢ s' ⊆ s
Tactic:
simp [s']
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Seq.cases_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
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
hdoms' : domain s' = under i
hs' : Seq s'
⊢ lh s' = i
Tactic:
simpa [hs'.domain_eq] using hdoms'
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Seq.cases_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
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
hdoms' : domain s' = under i
hs' : Seq s'
hs'i : lh s' = i
v : M
⊢ v ∈ s ↔ v ∈ s' ⁀' h.nth hi
Tactic:
simp only [seqCons, hs'i, mem_bitInsert_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
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
hdoms' : domain s' = under i
hs' : Seq s'
hs'i : lh s' = i
v : M
⊢ v ∈ s ↔ v = ⟪i, h.nth hi⟫ ∨ v ∈ s'
Theorem: LO.FirstOrder.Arith.Model.Seq.cases_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
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
hdoms' : domain s' = under i
hs' : Seq s'
hs'i : lh s' = i
v : M
⊢ v ∈ s ↔ v = ⟪i, h.nth hi⟫ ∨ v ∈ s'
Tactic:
simp [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
h : Seq s
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
hdoms' : domain s' = under i
hs' : Seq s'
hs'i : lh s' = i
v : M
⊢ v ∈ s ↔ v = ⟪i, h.nth hi⟫ ∨ ¬v = ⟪i, h.nth hi⟫ ∧ v ∈ s
Theorem: LO.FirstOrder.Arith.Model.Seq.cases_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
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
hdoms' : domain s' = under i
hs' : Seq s'
hs'i : lh s' = i
v : M
⊢ v ∈ s ↔ v = ⟪i, h.nth hi⟫ ∨ ¬v = ⟪i, h.nth hi⟫ ∧ v ∈ s
Tactic:
by_cases hv : v = ⟪i, h.nth hi⟫ <;> simp [hv]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Seq.cases_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
⊢ (s = ∅ ∨ ∃ x s', Seq s' ∧ s = s' ⁀' x) → Seq s
Tactic:
rintro (rfl | ⟨x, s', hs', rfl⟩)
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 ⊧ₘ* 𝐈𝚺₁
⊢ Seq ∅

case inr.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
hs' : Seq s'
⊢ Seq (s' ⁀' x)
Theorem: LO.FirstOrder.Arith.Model.Seq.cases_iff
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 ⊧ₘ* 𝐈𝚺₁
⊢ Seq ∅
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Seq.cases_iff
Proof state before:
case inr.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
hs' : Seq s'
⊢ Seq (s' ⁀' x)
Tactic:
exact hs'.seqCons x
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.seq_induction
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
hnil : P ∅
hcons : ∀ (s x : M), Seq s → P s → P (s ⁀' x)
⊢ ∀ {s : M}, Seq s → P s
Tactic:
intro s sseq
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
hnil : P ∅
hcons : ∀ (s x : M), Seq s → P s → P (s ⁀' x)
s : M
sseq : Seq s
⊢ P s
Theorem: LO.FirstOrder.Arith.Model.seq_induction
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
hnil : P ∅
hcons : ∀ (s x : M), Seq s → P s → P (s ⁀' x)
s : M
sseq : Seq s
⊢ P s
Tactic:
induction s using order_induction_h_iSigmaOne
Proof state after:
case Γ
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
hnil : P ∅
hcons : ∀ (s x : M), Seq s → P s → P (s ⁀' x)
⊢ SigmaPiDelta

case hP
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
hnil : P ∅
hcons : ∀ (s x : M), Seq s → P s → P (s ⁀' x)
⊢ (?Γ, 1)-Predicate fun {s} => Seq s → P s

case ind
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
hnil : P ∅
hcons : ∀ (s x : M), Seq s → P s → P (s ⁀' x)
x✝ : M
a✝ : ∀ y < x✝, Seq y → P y
sseq : Seq x✝
⊢ P x✝