Theorem: LO.FirstOrder.Arith.Model.Definable.bex_mem (Arithmetization/ISigmaOne/Bit.lean)

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
Γ : SigmaPiDelta
m : ℕ
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction ℒₒᵣ (𝚺, m + 1) f
h : Definable ℒₒᵣ (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
⊢ Definable ℒₒᵣ (Γ, m + 1) fun v => ∃ x ∈ f v, P v x
Tactic:
have : Definable ℒₒᵣ (Γ, m + 1) (fun v ↦ ∃ x < f v, x ∈ f v ∧ P v x) :=
  .bex_lt hf (.and (by simpa using Definable.comp₂ (by simp) (hf.retraction _) (by simp)) h)
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
Γ : SigmaPiDelta
m : ℕ
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction ℒₒᵣ (𝚺, m + 1) f
h : Definable ℒₒᵣ (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
this : Definable ℒₒᵣ (Γ, m + 1) fun v => ∃ x < f v, x ∈ f v ∧ P v x
⊢ Definable ℒₒᵣ (Γ, m + 1) fun v => ∃ x ∈ f v, P v x

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
Γ : SigmaPiDelta
m : ℕ
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction ℒₒᵣ (𝚺, m + 1) f
h : Definable ℒₒᵣ (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
this : Definable ℒₒᵣ (Γ, m + 1) fun v => ∃ x < f v, x ∈ f v ∧ P v x
⊢ Definable ℒₒᵣ (Γ, m + 1) fun v => ∃ x ∈ f v, P v x
Tactic:
exact this.of_iff <| by
  intro v; exact ⟨by rintro ⟨x, hx, hxv⟩; exact ⟨x, lt_of_mem hx, hx, hxv⟩, by rintro ⟨x, _, hx, hvx⟩; exact ⟨x, hx, hvx⟩⟩
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 ⊧ₘ* 𝐈𝚺₁
k : ℕ
Γ : SigmaPiDelta
m : ℕ
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction ℒₒᵣ (𝚺, m + 1) f
h : Definable ℒₒᵣ (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
⊢ Definable ℒₒᵣ (Γ, m + 1) fun w => w 0 ∈ f fun x => w x.succ
Tactic:
simpa using Definable.comp₂ (by simp) (hf.retraction _) (by simp)
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 ⊧ₘ* 𝐈𝚺₁
k : ℕ
Γ : SigmaPiDelta
m : ℕ
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction ℒₒᵣ (𝚺, m + 1) f
h : Definable ℒₒᵣ (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
⊢ DefinableFunction ℒₒᵣ (𝚺, m + 1) fun w => w 0
Tactic:
simp
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 ⊧ₘ* 𝐈𝚺₁
k : ℕ
Γ : SigmaPiDelta
m : ℕ
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction ℒₒᵣ (𝚺, m + 1) f
h : Definable ℒₒᵣ (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
⊢ (Γ, m + 1)-Relation Membership.mem
Tactic:
simp
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 ⊧ₘ* 𝐈𝚺₁
k : ℕ
Γ : SigmaPiDelta
m : ℕ
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction ℒₒᵣ (𝚺, m + 1) f
h : Definable ℒₒᵣ (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
this : Definable ℒₒᵣ (Γ, m + 1) fun v => ∃ x < f v, x ∈ f v ∧ P v x
⊢ ∀ (x : Fin k → M), (∃ x_1 ∈ f x, P x x_1) ↔ ∃ x_1 < f x, x_1 ∈ f x ∧ P x x_1
Tactic:
intro v
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
Γ : SigmaPiDelta
m : ℕ
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction ℒₒᵣ (𝚺, m + 1) f
h : Definable ℒₒᵣ (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
this : Definable ℒₒᵣ (Γ, m + 1) fun v => ∃ x < f v, x ∈ f v ∧ P v x
v : Fin k → M
⊢ (∃ x ∈ f v, P v x) ↔ ∃ x < f v, x ∈ f v ∧ P v x

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
Γ : SigmaPiDelta
m : ℕ
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction ℒₒᵣ (𝚺, m + 1) f
h : Definable ℒₒᵣ (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
this : Definable ℒₒᵣ (Γ, m + 1) fun v => ∃ x < f v, x ∈ f v ∧ P v x
v : Fin k → M
⊢ (∃ x ∈ f v, P v x) ↔ ∃ x < f v, x ∈ f v ∧ P v x
Tactic:
exact ⟨by rintro ⟨x, hx, hxv⟩; exact ⟨x, lt_of_mem hx, hx, hxv⟩, by rintro ⟨x, _, hx, hvx⟩; exact ⟨x, hx, hvx⟩⟩
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 ⊧ₘ* 𝐈𝚺₁
k : ℕ
Γ : SigmaPiDelta
m : ℕ
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction ℒₒᵣ (𝚺, m + 1) f
h : Definable ℒₒᵣ (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
this : Definable ℒₒᵣ (Γ, m + 1) fun v => ∃ x < f v, x ∈ f v ∧ P v x
v : Fin k → M
⊢ (∃ x ∈ f v, P v x) → ∃ x < f v, x ∈ f v ∧ P v x
Tactic:
rintro ⟨x, hx, hxv⟩
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 ⊧ₘ* 𝐈𝚺₁
k : ℕ
Γ : SigmaPiDelta
m : ℕ
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction ℒₒᵣ (𝚺, m + 1) f
h : Definable ℒₒᵣ (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
this : Definable ℒₒᵣ (Γ, m + 1) fun v => ∃ x < f v, x ∈ f v ∧ P v x
v : Fin k → M
x : M
hx : x ∈ f v
hxv : P v x
⊢ ∃ x < f v, x ∈ f v ∧ P v x

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 ⊧ₘ* 𝐈𝚺₁
k : ℕ
Γ : SigmaPiDelta
m : ℕ
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction ℒₒᵣ (𝚺, m + 1) f
h : Definable ℒₒᵣ (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
this : Definable ℒₒᵣ (Γ, m + 1) fun v => ∃ x < f v, x ∈ f v ∧ P v x
v : Fin k → M
x : M
hx : x ∈ f v
hxv : P v x
⊢ ∃ x < f v, x ∈ f v ∧ P v x
Tactic:
exact ⟨x, lt_of_mem hx, hx, hxv⟩
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 ⊧ₘ* 𝐈𝚺₁
k : ℕ
Γ : SigmaPiDelta
m : ℕ
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction ℒₒᵣ (𝚺, m + 1) f
h : Definable ℒₒᵣ (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
this : Definable ℒₒᵣ (Γ, m + 1) fun v => ∃ x < f v, x ∈ f v ∧ P v x
v : Fin k → M
⊢ (∃ x < f v, x ∈ f v ∧ P v x) → ∃ x ∈ f v, P v x
Tactic:
rintro ⟨x, _, hx, hvx⟩
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 ⊧ₘ* 𝐈𝚺₁
k : ℕ
Γ : SigmaPiDelta
m : ℕ
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction ℒₒᵣ (𝚺, m + 1) f
h : Definable ℒₒᵣ (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
this : Definable ℒₒᵣ (Γ, m + 1) fun v => ∃ x < f v, x ∈ f v ∧ P v x
v : Fin k → M
x : M
left✝ : x < f v
hx : x ∈ f v
hvx : P v x
⊢ ∃ x ∈ f v, P v x

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 ⊧ₘ* 𝐈𝚺₁
k : ℕ
Γ : SigmaPiDelta
m : ℕ
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction ℒₒᵣ (𝚺, m + 1) f
h : Definable ℒₒᵣ (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
this : Definable ℒₒᵣ (Γ, m + 1) fun v => ∃ x < f v, x ∈ f v ∧ P v x
v : Fin k → M
x : M
left✝ : x < f v
hx : x ∈ f v
hvx : P v x
⊢ ∃ x ∈ f v, P v x
Tactic:
exact ⟨x, hx, hvx⟩
State after:
no goals