Theorem: LO.FirstOrder.Arith.Model.seqMap_existsUnique (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 ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
Hs : Seq s
⊢ ∃! t, Seq t ∧ lh t = lh s ∧ ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t
Tactic:
rcases Hs.seqMap_exists hf with ⟨t, Ht, hts, h⟩
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 ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
Hs : Seq s
t : M
Ht : Seq t
hts : lh t = lh s
h : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t
⊢ ∃! t, Seq t ∧ lh t = lh s ∧ ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t

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 ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
Hs : Seq s
t : M
Ht : Seq t
hts : lh t = lh s
h : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t
⊢ ∃! t, Seq t ∧ lh t = lh s ∧ ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t
Tactic:
apply ExistsUnique.intro t ⟨Ht, hts, h⟩
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 ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
Hs : Seq s
t : M
Ht : Seq t
hts : lh t = lh s
h : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t
⊢ ∀ (y : M), (Seq y ∧ lh y = lh s ∧ ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ y) → y = t

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 ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
Hs : Seq s
t : M
Ht : Seq t
hts : lh t = lh s
h : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t
⊢ ∀ (y : M), (Seq y ∧ lh y = lh s ∧ ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ y) → y = t
Tactic:
rintro t' ⟨Ht', ht's, h'⟩
State after:
case 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 ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
Hs : Seq s
t : M
Ht : Seq t
hts : lh t = lh s
h : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t
t' : M
Ht' : Seq t'
ht's : lh t' = lh s
h' : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t'
⊢ t' = t

State before:
case 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 ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
Hs : Seq s
t : M
Ht : Seq t
hts : lh t = lh s
h : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t
t' : M
Ht' : Seq t'
ht's : lh t' = lh s
h' : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t'
⊢ t' = t
Tactic:
apply Ht'.eq_of_eq_of_subset Ht (by simp [hts, ht's])
State after:
case 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 ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
Hs : Seq s
t : M
Ht : Seq t
hts : lh t = lh s
h : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t
t' : M
Ht' : Seq t'
ht's : lh t' = lh s
h' : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t'
⊢ t' ⊆ t

State before:
case 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 ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
Hs : Seq s
t : M
Ht : Seq t
hts : lh t = lh s
h : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t
t' : M
Ht' : Seq t'
ht's : lh t' = lh s
h' : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t'
⊢ t' ⊆ t
Tactic:
intro u hu
State after:
case 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 ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
Hs : Seq s
t : M
Ht : Seq t
hts : lh t = lh s
h : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t
t' : M
Ht' : Seq t'
ht's : lh t' = lh s
h' : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t'
u : M
hu : u ∈ t'
⊢ u ∈ t

State before:
case 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 ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
Hs : Seq s
t : M
Ht : Seq t
hts : lh t = lh s
h : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t
t' : M
Ht' : Seq t'
ht's : lh t' = lh s
h' : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t'
u : M
hu : u ∈ t'
⊢ u ∈ t
Tactic:
have : π₁ u < lh s := by simpa [←ht's] using Ht'.lt_lh_of_mem (show ⟪π₁ u, π₂ u⟫ ∈ t' from by simpa using hu)
State after:
case 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 ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
Hs : Seq s
t : M
Ht : Seq t
hts : lh t = lh s
h : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t
t' : M
Ht' : Seq t'
ht's : lh t' = lh s
h' : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t'
u : M
hu : u ∈ t'
this : π₁ u < lh s
⊢ u ∈ t

State before:
case 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 ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
Hs : Seq s
t : M
Ht : Seq t
hts : lh t = lh s
h : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t
t' : M
Ht' : Seq t'
ht's : lh t' = lh s
h' : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t'
u : M
hu : u ∈ t'
this : π₁ u < lh s
⊢ u ∈ t
Tactic:
have : ∃ y, ⟪π₁ u, y⟫ ∈ s := Hs.exists this
State after:
case 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 ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
Hs : Seq s
t : M
Ht : Seq t
hts : lh t = lh s
h : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t
t' : M
Ht' : Seq t'
ht's : lh t' = lh s
h' : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t'
u : M
hu : u ∈ t'
this✝ : π₁ u < lh s
this : ∃ y, ⟪π₁ u, y⟫ ∈ s
⊢ u ∈ t

State before:
case 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 ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
Hs : Seq s
t : M
Ht : Seq t
hts : lh t = lh s
h : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t
t' : M
Ht' : Seq t'
ht's : lh t' = lh s
h' : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t'
u : M
hu : u ∈ t'
this✝ : π₁ u < lh s
this : ∃ y, ⟪π₁ u, y⟫ ∈ s
⊢ u ∈ t
Tactic:
rcases this with ⟨y, hy⟩
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 ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
Hs : Seq s
t : M
Ht : Seq t
hts : lh t = lh s
h : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t
t' : M
Ht' : Seq t'
ht's : lh t' = lh s
h' : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t'
u : M
hu : u ∈ t'
this : π₁ u < lh s
y : M
hy : ⟪π₁ u, y⟫ ∈ s
⊢ u ∈ t

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 ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
Hs : Seq s
t : M
Ht : Seq t
hts : lh t = lh s
h : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t
t' : M
Ht' : Seq t'
ht's : lh t' = lh s
h' : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t'
u : M
hu : u ∈ t'
this : π₁ u < lh s
y : M
hy : ⟪π₁ u, y⟫ ∈ s
⊢ u ∈ t
Tactic:
have : f y = π₂ u := Ht'.isMapping.uniq (h' _ _ hy) (show ⟪π₁ u, π₂ u⟫ ∈ t' from by simpa using hu)
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 ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
Hs : Seq s
t : M
Ht : Seq t
hts : lh t = lh s
h : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t
t' : M
Ht' : Seq t'
ht's : lh t' = lh s
h' : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t'
u : M
hu : u ∈ t'
this✝ : π₁ u < lh s
y : M
hy : ⟪π₁ u, y⟫ ∈ s
this : f y = π₂ u
⊢ u ∈ t

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 ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
Hs : Seq s
t : M
Ht : Seq t
hts : lh t = lh s
h : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t
t' : M
Ht' : Seq t'
ht's : lh t' = lh s
h' : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t'
u : M
hu : u ∈ t'
this✝ : π₁ u < lh s
y : M
hy : ⟪π₁ u, y⟫ ∈ s
this : f y = π₂ u
⊢ u ∈ t
Tactic:
simpa [this] using h _ _ 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 ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
Hs : Seq s
t : M
Ht : Seq t
hts : lh t = lh s
h : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t
t' : M
Ht' : Seq t'
ht's : lh t' = lh s
h' : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t'
⊢ lh t' = lh t
Tactic:
simp [hts, ht'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 ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
Hs : Seq s
t : M
Ht : Seq t
hts : lh t = lh s
h : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t
t' : M
Ht' : Seq t'
ht's : lh t' = lh s
h' : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t'
u : M
hu : u ∈ t'
⊢ π₁ u < lh s
Tactic:
simpa [←ht's] using Ht'.lt_lh_of_mem (show ⟪π₁ u, π₂ u⟫ ∈ t' 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 ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
Hs : Seq s
t : M
Ht : Seq t
hts : lh t = lh s
h : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t
t' : M
Ht' : Seq t'
ht's : lh t' = lh s
h' : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t'
u : M
hu : u ∈ t'
⊢ ⟪π₁ u, π₂ u⟫ ∈ t'
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 ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
Hs : Seq s
t : M
Ht : Seq t
hts : lh t = lh s
h : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t
t' : M
Ht' : Seq t'
ht's : lh t' = lh s
h' : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t'
u : M
hu : u ∈ t'
this : π₁ u < lh s
y : M
hy : ⟪π₁ u, y⟫ ∈ s
⊢ ⟪π₁ u, π₂ u⟫ ∈ t'
Tactic:
simpa using hu
State after:
no goals