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

State before:
ξ : Type u_1
n : ?m.110780
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
⊢ 𝚺₀-Relation₃ fun r x y => ⟪x, y⟫ ∈ r via memRel
Tactic:
intro v
State after:
ξ : Type u_1
n : ?m.110780
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 3 → M
⊢ (fun v => (fun r x y => ⟪x, y⟫ ∈ r) (v 0) (v 1) (v 2)) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val memRel)

State before:
ξ : Type u_1
n : ?m.110780
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 3 → M
⊢ (fun v => (fun r x y => ⟪x, y⟫ ∈ r) (v 0) (v 1) (v 2)) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val memRel)
Tactic:
simp [memRel, pair_defined.df.iff, lt_succ_iff_le]
State after:
ξ : Type u_1
n : ?m.110780
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 3 → M
⊢ ⟪v 1, v 2⟫ ∈ v 0 ↔ ∃ x ≤ (v 1 + v 2 + 1) ^ 2, x = ⟪v 1, v 2⟫ ∧ x ∈ v 0

State before:
ξ : Type u_1
n : ?m.110780
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 3 → M
⊢ ⟪v 1, v 2⟫ ∈ v 0 ↔ ∃ x ≤ (v 1 + v 2 + 1) ^ 2, x = ⟪v 1, v 2⟫ ∧ x ∈ v 0
Tactic:
constructor
State after:
case mp
ξ : Type u_1
n : ?m.110780
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 3 → M
⊢ ⟪v 1, v 2⟫ ∈ v 0 → ∃ x ≤ (v 1 + v 2 + 1) ^ 2, x = ⟪v 1, v 2⟫ ∧ x ∈ v 0

case mpr
ξ : Type u_1
n : ?m.110780
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 3 → M
⊢ (∃ x ≤ (v 1 + v 2 + 1) ^ 2, x = ⟪v 1, v 2⟫ ∧ x ∈ v 0) → ⟪v 1, v 2⟫ ∈ v 0

State before:
case mp
ξ : Type u_1
n : ?m.110780
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 3 → M
⊢ ⟪v 1, v 2⟫ ∈ v 0 → ∃ x ≤ (v 1 + v 2 + 1) ^ 2, x = ⟪v 1, v 2⟫ ∧ x ∈ v 0
Tactic:
intro h
State after:
case mp
ξ : Type u_1
n : ?m.110780
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 3 → M
h : ⟪v 1, v 2⟫ ∈ v 0
⊢ ∃ x ≤ (v 1 + v 2 + 1) ^ 2, x = ⟪v 1, v 2⟫ ∧ x ∈ v 0

State before:
case mp
ξ : Type u_1
n : ?m.110780
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 3 → M
h : ⟪v 1, v 2⟫ ∈ v 0
⊢ ∃ x ≤ (v 1 + v 2 + 1) ^ 2, x = ⟪v 1, v 2⟫ ∧ x ∈ v 0
Tactic:
exact ⟨⟪v 1, v 2⟫, by simp, rfl, h⟩
State after:
no goals

State before:
ξ : Type u_1
n : ?m.110780
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 3 → M
h : ⟪v 1, v 2⟫ ∈ v 0
⊢ ⟪v 1, v 2⟫ ≤ (v 1 + v 2 + 1) ^ 2
Tactic:
simp
State after:
no goals

State before:
case mpr
ξ : Type u_1
n : ?m.110780
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 3 → M
⊢ (∃ x ≤ (v 1 + v 2 + 1) ^ 2, x = ⟪v 1, v 2⟫ ∧ x ∈ v 0) → ⟪v 1, v 2⟫ ∈ v 0
Tactic:
rintro ⟨_, _, rfl, h⟩
State after:
case mpr.intro.intro.intro
ξ : Type u_1
n : ?m.110780
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 3 → M
left✝ : ⟪v 1, v 2⟫ ≤ (v 1 + v 2 + 1) ^ 2
h : ⟪v 1, v 2⟫ ∈ v 0
⊢ ⟪v 1, v 2⟫ ∈ v 0

State before:
case mpr.intro.intro.intro
ξ : Type u_1
n : ?m.110780
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 3 → M
left✝ : ⟪v 1, v 2⟫ ≤ (v 1 + v 2 + 1) ^ 2
h : ⟪v 1, v 2⟫ ∈ v 0
⊢ ⟪v 1, v 2⟫ ∈ v 0
Tactic:
exact h
State after:
no goals