Theorem: LO.FirstOrder.Arith.Model.Seq.eq_of_eq_of_subset (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 ⊧ₘ* 𝐈𝚺₁
s₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
hl : lh s₁ = lh s₂
h : s₁ ⊆ s₂
⊢ s₁ = s₂
Tactic:
apply mem_ext
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₂

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

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

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

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

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

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

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

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

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

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

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
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 ⊧ₘ* 𝐈𝚺₁
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)
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 ⊧ₘ* 𝐈𝚺₁
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
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 ⊧ₘ* 𝐈𝚺₁
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
State after:
no goals