Theorem: LO.FirstOrder.Arith.Model.finite_comprehension₁! (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 ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
fin : ∃ m, ∀ (i : M), P i → i < m
⊢ ∃! s, ∀ (i : M), i ∈ s ↔ P i
Tactic:
rcases fin with ⟨m, mh⟩
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 ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
m : M
mh : ∀ (i : M), P i → i < m
⊢ ∃! s, ∀ (i : M), i ∈ s ↔ P i

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 ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
m : M
mh : ∀ (i : M), P i → i < m
⊢ ∃! s, ∀ (i : M), i ∈ s ↔ P i
Tactic:
rcases finset_comprehension₁ hP m with ⟨s, hs, Hs⟩
State after:
case intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
m : M
mh : ∀ (i : M), P i → i < m
s : M
hs : s < exp m
Hs : ∀ i < m, i ∈ s ↔ P i
⊢ ∃! s, ∀ (i : M), i ∈ s ↔ P i

State before:
case intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
m : M
mh : ∀ (i : M), P i → i < m
s : M
hs : s < exp m
Hs : ∀ i < m, i ∈ s ↔ P i
⊢ ∃! s, ∀ (i : M), i ∈ s ↔ P i
Tactic:
have H : ∀ i, i ∈ s ↔ P i :=
  fun i ↦ ⟨
    fun h ↦ (Hs i (exp_monotone.mp (lt_of_le_of_lt (exp_le_of_mem h) hs))).mp h,
    fun h ↦ (Hs i (mh i h)).mpr h⟩
State after:
case intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
m : M
mh : ∀ (i : M), P i → i < m
s : M
hs : s < exp m
Hs : ∀ i < m, i ∈ s ↔ P i
H : ∀ (i : M), i ∈ s ↔ P i
⊢ ∃! s, ∀ (i : M), i ∈ s ↔ P i

State before:
case intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
m : M
mh : ∀ (i : M), P i → i < m
s : M
hs : s < exp m
Hs : ∀ i < m, i ∈ s ↔ P i
H : ∀ (i : M), i ∈ s ↔ P i
⊢ ∃! s, ∀ (i : M), i ∈ s ↔ P i
Tactic:
exact ExistsUnique.intro s H (fun s' H' ↦ mem_ext <| fun i ↦ by simp [H, 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 ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
m : M
mh : ∀ (i : M), P i → i < m
s : M
hs : s < exp m
Hs : ∀ i < m, i ∈ s ↔ P i
H : ∀ (i : M), i ∈ s ↔ P i
s' : M
H' : ∀ (i : M), i ∈ s' ↔ P i
i : M
⊢ i ∈ s' ↔ i ∈ s
Tactic:
simp [H, H']
State after:
no goals