Theorem: LO.FirstOrder.Arith.Model.finset_comprehension_exists_unique (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 ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, m)-Predicate P
a : M
⊢ ∃! s, s < exp a ∧ ∀ i < a, i ∈ s ↔ P i
Tactic:
haveI : M ⊧ₘ* 𝐈𝚺₁ := mod_iSigma_of_le (show 1 ≤ m from Fact.out)
State after:
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
⊢ ∃! s, s < exp a ∧ ∀ i < a, i ∈ s ↔ P i

State before:
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
⊢ ∃! s, s < exp a ∧ ∀ i < a, i ∈ s ↔ P i
Tactic:
rcases finset_comprehension hP a with ⟨s, hs, Hs⟩
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 ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
s : M
hs : s < exp a
Hs : ∀ i < a, i ∈ s ↔ P i
⊢ ∃! s, s < exp a ∧ ∀ i < a, i ∈ s ↔ P i

State before:
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
s : M
hs : s < exp a
Hs : ∀ i < a, i ∈ s ↔ P i
⊢ ∀ (y : M), (y < exp a ∧ ∀ i < a, i ∈ y ↔ P i) → y = s
Tactic:
intro t ⟨ht, Ht⟩
State after:
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
s : M
hs : s < exp a
Hs : ∀ i < a, i ∈ s ↔ P i
t : M
ht : t < exp a
Ht : ∀ i < a, i ∈ t ↔ P i
⊢ t = s

State before:
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
s : M
hs : s < exp a
Hs : ∀ i < a, i ∈ s ↔ P i
t : M
ht : t < exp a
Ht : ∀ i < a, i ∈ t ↔ P i
⊢ t = s
Tactic:
apply mem_ext
State after:
case h
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
s : M
hs : s < exp a
Hs : ∀ i < a, i ∈ s ↔ P i
t : M
ht : t < exp a
Ht : ∀ i < a, i ∈ t ↔ P i
⊢ ∀ (i : M), i ∈ t ↔ i ∈ s

State before:
case h
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
s : M
hs : s < exp a
Hs : ∀ i < a, i ∈ s ↔ P i
t : M
ht : t < exp a
Ht : ∀ i < a, i ∈ t ↔ P i
⊢ ∀ (i : M), i ∈ t ↔ i ∈ s
Tactic:
intro i
State after:
case h
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
s : M
hs : s < exp a
Hs : ∀ i < a, i ∈ s ↔ P i
t : M
ht : t < exp a
Ht : ∀ i < a, i ∈ t ↔ P i
i : M
⊢ i ∈ t ↔ i ∈ s

State before:
case h
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
s : M
hs : s < exp a
Hs : ∀ i < a, i ∈ s ↔ P i
t : M
ht : t < exp a
Ht : ∀ i < a, i ∈ t ↔ P i
i : M
⊢ i ∈ t ↔ i ∈ s
Tactic:
constructor
State after:
case h.mp
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
s : M
hs : s < exp a
Hs : ∀ i < a, i ∈ s ↔ P i
t : M
ht : t < exp a
Ht : ∀ i < a, i ∈ t ↔ P i
i : M
⊢ i ∈ t → i ∈ s

case h.mpr
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
s : M
hs : s < exp a
Hs : ∀ i < a, i ∈ s ↔ P i
t : M
ht : t < exp a
Ht : ∀ i < a, i ∈ t ↔ P i
i : M
⊢ i ∈ s → i ∈ t

State before:
case h.mp
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
s : M
hs : s < exp a
Hs : ∀ i < a, i ∈ s ↔ P i
t : M
ht : t < exp a
Ht : ∀ i < a, i ∈ t ↔ P i
i : M
⊢ i ∈ t → i ∈ s
Tactic:
intro hi
State after:
case h.mp
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
s : M
hs : s < exp a
Hs : ∀ i < a, i ∈ s ↔ P i
t : M
ht : t < exp a
Ht : ∀ i < a, i ∈ t ↔ P i
i : M
hi : i ∈ t
⊢ i ∈ s

State before:
case h.mp
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
s : M
hs : s < exp a
Hs : ∀ i < a, i ∈ s ↔ P i
t : M
ht : t < exp a
Ht : ∀ i < a, i ∈ t ↔ P i
i : M
hi : i ∈ t
⊢ i ∈ s
Tactic:
have hin : i < a := exp_monotone.mp (lt_of_le_of_lt (exp_le_of_mem hi) ht)
State after:
case h.mp
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
s : M
hs : s < exp a
Hs : ∀ i < a, i ∈ s ↔ P i
t : M
ht : t < exp a
Ht : ∀ i < a, i ∈ t ↔ P i
i : M
hi : i ∈ t
hin : i < a
⊢ i ∈ s

State before:
case h.mp
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
s : M
hs : s < exp a
Hs : ∀ i < a, i ∈ s ↔ P i
t : M
ht : t < exp a
Ht : ∀ i < a, i ∈ t ↔ P i
i : M
hi : i ∈ t
hin : i < a
⊢ i ∈ s
Tactic:
exact (Hs i hin).mpr ((Ht i hin).mp hi)
State after:
no goals

State before:
case h.mpr
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
s : M
hs : s < exp a
Hs : ∀ i < a, i ∈ s ↔ P i
t : M
ht : t < exp a
Ht : ∀ i < a, i ∈ t ↔ P i
i : M
⊢ i ∈ s → i ∈ t
Tactic:
intro hi
State after:
case h.mpr
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
s : M
hs : s < exp a
Hs : ∀ i < a, i ∈ s ↔ P i
t : M
ht : t < exp a
Ht : ∀ i < a, i ∈ t ↔ P i
i : M
hi : i ∈ s
⊢ i ∈ t

State before:
case h.mpr
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
s : M
hs : s < exp a
Hs : ∀ i < a, i ∈ s ↔ P i
t : M
ht : t < exp a
Ht : ∀ i < a, i ∈ t ↔ P i
i : M
hi : i ∈ s
⊢ i ∈ t
Tactic:
have hin : i < a := exp_monotone.mp (lt_of_le_of_lt (exp_le_of_mem hi) hs)
State after:
case h.mpr
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
s : M
hs : s < exp a
Hs : ∀ i < a, i ∈ s ↔ P i
t : M
ht : t < exp a
Ht : ∀ i < a, i ∈ t ↔ P i
i : M
hi : i ∈ s
hin : i < a
⊢ i ∈ t

State before:
case h.mpr
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
s : M
hs : s < exp a
Hs : ∀ i < a, i ∈ s ↔ P i
t : M
ht : t < exp a
Ht : ∀ i < a, i ∈ t ↔ P i
i : M
hi : i ∈ s
hin : i < a
⊢ i ∈ t
Tactic:
exact (Ht i hin).mpr ((Hs i hin).mp hi)
State after:
no goals