Theorem: LO.FirstOrder.Arith.Model.bit_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 bitDef
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 bitDef)

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 bitDef)
Tactic:
simp [bitDef, ←le_iff_lt_succ]
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 1, x = exp v 0 ∧ LenBit 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 1, x = exp v 0 ∧ LenBit x (v 1)
Tactic:
constructor
State after:
case mp
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 1, x = exp v 0 ∧ LenBit x (v 1)

case mpr
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 1, x = exp v 0 ∧ LenBit x (v 1)) → v 0 ∈ v 1

State before:
case mp
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 1, x = exp v 0 ∧ LenBit x (v 1)
Tactic:
intro h
State after:
case mp
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 ≤ v 1, x = exp v 0 ∧ LenBit x (v 1)

State before:
case mp
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 ≤ v 1, x = exp v 0 ∧ LenBit x (v 1)
Tactic:
exact ⟨exp (v 0), by simp [h.le], rfl, h⟩
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
h : v 0 ∈ v 1
⊢ exp v 0 ≤ v 1
Tactic:
simp [h.le]
State after:
no goals

State before:
case mpr
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 1, x = exp v 0 ∧ LenBit x (v 1)) → v 0 ∈ v 1
Tactic:
rintro ⟨_, _, rfl, h⟩
State after:
case mpr.intro.intro.intro
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
left✝ : exp v 0 ≤ v 1
h : LenBit (exp v 0) (v 1)
⊢ v 0 ∈ v 1

State before:
case mpr.intro.intro.intro
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
left✝ : exp v 0 ≤ v 1
h : LenBit (exp v 0) (v 1)
⊢ v 0 ∈ v 1
Tactic:
exact h
State after:
no goals