Theorem: LO.FirstOrder.Arith.Model.Seq.seqCons_ext (Arithmetization/ISigmaOne/HFS/Seq.lean)

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
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₂

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
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₂

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₁
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₂

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₂]
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₂

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₂
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₂

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⟩
State after:
no goals

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
State after:
no goals

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₁
State after:
no goals

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₂]
State after:
no goals

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
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₂

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
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₂

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₂)
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₂

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
State after:
no goals

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
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₂

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
State after:
no goals

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
State after:
no goals

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⟩
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₁

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
State after:
no goals