Theorem: LO.FirstOrder.Arith.Model.bitSubset_defined (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 ⊧ₘ* 𝐈𝚺₁
⊢ 𝚺₀-Relation fun x x_1 => x ⊆ x_1 via bitSubsetDef
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 ⊧ₘ* 𝐈𝚺₁
v : Fin 2 → M
⊢ (fun v => (fun x x_1 => x ⊆ x_1) (v 0) (v 1)) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val bitSubsetDef)

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 2 → M
⊢ (fun v => (fun x x_1 => x ⊆ x_1) (v 0) (v 1)) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val bitSubsetDef)
Tactic:
simp [bitSubsetDef]
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 2 → M
⊢ v 0 ⊆ v 1 ↔ ∀ x < v 0, x ∈ v 0 → x ∈ v 1

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 2 → M
⊢ v 0 ⊆ v 1 ↔ ∀ x < v 0, x ∈ v 0 → x ∈ v 1
Tactic:
exact ⟨by intro h x _ hx; exact h hx, by intro h x hx; exact 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 ⊧ₘ* 𝐈𝚺₁
v : Fin 2 → M
⊢ v 0 ⊆ v 1 → ∀ x < v 0, x ∈ v 0 → x ∈ v 1
Tactic:
intro h x _ hx
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 2 → M
h : v 0 ⊆ v 1
x : M
a✝ : x < v 0
hx : x ∈ v 0
⊢ x ∈ v 1

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 2 → M
h : v 0 ⊆ v 1
x : M
a✝ : x < v 0
hx : x ∈ v 0
⊢ x ∈ v 1
Tactic:
exact h 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 ⊧ₘ* 𝐈𝚺₁
v : Fin 2 → M
⊢ (∀ x < v 0, x ∈ v 0 → x ∈ v 1) → v 0 ⊆ v 1
Tactic:
intro h x hx
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 2 → M
h : ∀ x < v 0, x ∈ v 0 → x ∈ v 1
x : M
hx : x ∈ v 0
⊢ x ∈ v 1

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 2 → M
h : ∀ x < v 0, x ∈ v 0 → x ∈ v 1
x : M
hx : x ∈ v 0
⊢ x ∈ v 1
Tactic:
exact h x (lt_of_mem hx) hx
State after:
no goals