Theorem: LO.FirstOrder.Arith.Model.Definable.ball_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) :=
  .ball_lt hf (.imp (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 ⟨fun h x _ hxv ↦ h x hxv, fun h x hx ↦ h x (lt_of_mem hx) 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 ⊧ₘ* 𝐈𝚺₁
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 ℒₒᵣ (Γ.alt, 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)
⊢ (Γ.alt, 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 ⟨fun h x _ hxv ↦ h x hxv, fun h x hx ↦ h x (lt_of_mem hx) hx⟩
State after:
no goals