Theorem: LO.FirstOrder.Arith.Model.Seq.mem_seqMap_iff (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
H : Seq s
i y : M
⊢ ⟪i, y⟫ ∈ seqMap hf s → ∃ x, f x = y ∧ ⟪i, x⟫ ∈ s
Tactic:
intro hu
State after:
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
H : Seq s
i y : M
hu : ⟪i, y⟫ ∈ seqMap hf s
⊢ ∃ x, f x = y ∧ ⟪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 ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
H : Seq s
i y : M
hu : ⟪i, y⟫ ∈ seqMap hf s
⊢ ∃ x, f x = y ∧ ⟪i, x⟫ ∈ s
Tactic:
have : i < lh s := by simpa [H] using H.seqMap.lt_lh_of_mem hu
State after:
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
H : Seq s
i y : M
hu : ⟪i, y⟫ ∈ seqMap hf s
this : i < lh s
⊢ ∃ x, f x = y ∧ ⟪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 ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
H : Seq s
i y : M
hu : ⟪i, y⟫ ∈ seqMap hf s
this : i < lh s
⊢ ∃ x, f x = y ∧ ⟪i, x⟫ ∈ s
Tactic:
have : ∃ x, ⟪i, x⟫ ∈ s := H.exists this
State after:
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
H : Seq s
i y : M
hu : ⟪i, y⟫ ∈ seqMap hf s
this✝ : i < lh s
this : ∃ x, ⟪i, x⟫ ∈ s
⊢ ∃ x, f x = y ∧ ⟪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 ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
H : Seq s
i y : M
hu : ⟪i, y⟫ ∈ seqMap hf s
this✝ : i < lh s
this : ∃ x, ⟪i, x⟫ ∈ s
⊢ ∃ x, f x = y ∧ ⟪i, x⟫ ∈ s
Tactic:
rcases this with ⟨x, hx⟩
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 ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
H : Seq s
i y : M
hu : ⟪i, y⟫ ∈ seqMap hf s
this : i < lh s
x : M
hx : ⟪i, x⟫ ∈ s
⊢ ∃ x, f x = y ∧ ⟪i, x⟫ ∈ s

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 ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
H : Seq s
i y : M
hu : ⟪i, y⟫ ∈ seqMap hf s
this : i < lh s
x : M
hx : ⟪i, x⟫ ∈ s
⊢ ∃ x, f x = y ∧ ⟪i, x⟫ ∈ s
Tactic:
exact ⟨x, H.seqMap.isMapping.uniq (H.seqMap_spec hx) hu, hx⟩
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
H : Seq s
i y : M
hu : ⟪i, y⟫ ∈ seqMap hf s
⊢ i < lh s
Tactic:
simpa [H] using H.seqMap.lt_lh_of_mem 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
H : Seq s
i y : M
⊢ (∃ x, f x = y ∧ ⟪i, x⟫ ∈ s) → ⟪i, y⟫ ∈ seqMap hf s
Tactic:
rintro ⟨x, rfl, hx⟩
State after:
case 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
H : Seq s
i x : M
hx : ⟪i, x⟫ ∈ s
⊢ ⟪i, f x⟫ ∈ seqMap hf s

State before:
case 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
H : Seq s
i x : M
hx : ⟪i, x⟫ ∈ s
⊢ ⟪i, f x⟫ ∈ seqMap hf s
Tactic:
exact H.seqMap_spec hx
State after:
no goals