Theorem: LO.FirstOrder.Arith.Model.domain_exists_unique (Arithmetization/ISigmaOne/HFS/Basic.lean)

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
⊢ ∃! d, ∀ (x : M), x ∈ d ↔ ∃ y, ⟪x, y⟫ ∈ s
Tactic:
have : 𝚺₁-Predicate fun x ↦ ∃ y, ⟪x, y⟫ ∈ s :=
  DefinablePred.of_iff (fun x ↦ ∃ y < s, ⟪x, y⟫ ∈ s)
    (fun x ↦ ⟨by rintro ⟨y, hy⟩; exact ⟨y, lt_of_le_of_lt (le_pair_right x y) (lt_of_mem hy), hy⟩,
              by rintro ⟨y, _, hy⟩; exact ⟨y, hy⟩⟩)
    (by definability)
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
this : 𝚺₁-Predicate fun x => ∃ y, ⟪x, y⟫ ∈ s
⊢ ∃! d, ∀ (x : M), x ∈ d ↔ ∃ y, ⟪x, y⟫ ∈ s

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
this : 𝚺₁-Predicate fun x => ∃ y, ⟪x, y⟫ ∈ s
⊢ ∃! d, ∀ (x : M), x ∈ d ↔ ∃ y, ⟪x, y⟫ ∈ s
Tactic:
exact finite_comprehension₁!
  this
  (⟨s, fun x ↦ by rintro ⟨y, hy⟩; exact lt_of_le_of_lt (le_pair_left x y) (lt_of_mem hy)⟩)
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 ⊧ₘ* 𝐈𝚺₁
s x : M
⊢ (∃ y, ⟪x, y⟫ ∈ s) → (fun x => ∃ y < s, ⟪x, y⟫ ∈ s) x
Tactic:
rintro ⟨y, hy⟩
State after:
case intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s x y : M
hy : ⟪x, y⟫ ∈ s
⊢ ∃ y < s, ⟪x, y⟫ ∈ s

State before:
case intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s x y : M
hy : ⟪x, y⟫ ∈ s
⊢ ∃ y < s, ⟪x, y⟫ ∈ s
Tactic:
exact ⟨y, lt_of_le_of_lt (le_pair_right x y) (lt_of_mem hy), hy⟩
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 ⊧ₘ* 𝐈𝚺₁
s x : M
⊢ (fun x => ∃ y < s, ⟪x, y⟫ ∈ s) x → ∃ y, ⟪x, y⟫ ∈ s
Tactic:
rintro ⟨y, _, hy⟩
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 ⊧ₘ* 𝐈𝚺₁
s x y : M
left✝ : y < s
hy : ⟪x, y⟫ ∈ s
⊢ ∃ y, ⟪x, y⟫ ∈ s

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 ⊧ₘ* 𝐈𝚺₁
s x y : M
left✝ : y < s
hy : ⟪x, y⟫ ∈ s
⊢ ∃ y, ⟪x, y⟫ ∈ s
Tactic:
exact ⟨y, hy⟩
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 ⊧ₘ* 𝐈𝚺₁
s : M
⊢ 𝚺₁-Predicate fun x => ∃ y < s, ⟪x, y⟫ ∈ s
Tactic:
definability
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 ⊧ₘ* 𝐈𝚺₁
s : M
this : 𝚺₁-Predicate fun x => ∃ y, ⟪x, y⟫ ∈ s
x : M
⊢ (∃ y, ⟪x, y⟫ ∈ s) → x < s
Tactic:
rintro ⟨y, hy⟩
State after:
case intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
this : 𝚺₁-Predicate fun x => ∃ y, ⟪x, y⟫ ∈ s
x y : M
hy : ⟪x, y⟫ ∈ s
⊢ x < s

State before:
case intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
this : 𝚺₁-Predicate fun x => ∃ y, ⟪x, y⟫ ∈ s
x y : M
hy : ⟪x, y⟫ ∈ s
⊢ x < s
Tactic:
exact lt_of_le_of_lt (le_pair_left x y) (lt_of_mem hy)
State after:
no goals