Theorem: LO.FirstOrder.Arith.Model.finset_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
a : M
⊢ ∃! s, s < exp a ∧ ∀ i < a, i ∈ s ↔ P i
Tactic:
rcases finset_comprehension₁ hP a with ⟨s, hs, Ha⟩
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 ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
a s : M
hs : s < exp a
Ha : ∀ 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 ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
a s : M
hs : s < exp a
Ha : ∀ i < a, i ∈ s ↔ P i
⊢ ∀ (y : M), (y < exp a ∧ ∀ i < a, i ∈ y ↔ P i) → y = s
Tactic:
rintro b ⟨hb, Hb⟩
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
a s : M
hs : s < exp a
Ha : ∀ i < a, i ∈ s ↔ P i
b : M
hb : b < exp a
Hb : ∀ i < a, i ∈ b ↔ P i
⊢ b = 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 ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
a s : M
hs : s < exp a
Ha : ∀ i < a, i ∈ s ↔ P i
b : M
hb : b < exp a
Hb : ∀ i < a, i ∈ b ↔ P i
⊢ b = s
Tactic:
apply mem_ext
State after:
case intro.h
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
a s : M
hs : s < exp a
Ha : ∀ i < a, i ∈ s ↔ P i
b : M
hb : b < exp a
Hb : ∀ i < a, i ∈ b ↔ P i
⊢ ∀ (i : M), i ∈ b ↔ i ∈ s

State before:
case intro.h
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
a s : M
hs : s < exp a
Ha : ∀ i < a, i ∈ s ↔ P i
b : M
hb : b < exp a
Hb : ∀ i < a, i ∈ b ↔ P i
⊢ ∀ (i : M), i ∈ b ↔ i ∈ s
Tactic:
intro x
State after:
case intro.h
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
a s : M
hs : s < exp a
Ha : ∀ i < a, i ∈ s ↔ P i
b : M
hb : b < exp a
Hb : ∀ i < a, i ∈ b ↔ P i
x : M
⊢ x ∈ b ↔ x ∈ s

State before:
case intro.h
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
a s : M
hs : s < exp a
Ha : ∀ i < a, i ∈ s ↔ P i
b : M
hb : b < exp a
Hb : ∀ i < a, i ∈ b ↔ P i
x : M
⊢ x ∈ b ↔ x ∈ s
Tactic:
constructor
State after:
case intro.h.mp
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
a s : M
hs : s < exp a
Ha : ∀ i < a, i ∈ s ↔ P i
b : M
hb : b < exp a
Hb : ∀ i < a, i ∈ b ↔ P i
x : M
⊢ x ∈ b → x ∈ s

case intro.h.mpr
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
a s : M
hs : s < exp a
Ha : ∀ i < a, i ∈ s ↔ P i
b : M
hb : b < exp a
Hb : ∀ i < a, i ∈ b ↔ P i
x : M
⊢ x ∈ s → x ∈ b

State before:
case intro.h.mp
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
a s : M
hs : s < exp a
Ha : ∀ i < a, i ∈ s ↔ P i
b : M
hb : b < exp a
Hb : ∀ i < a, i ∈ b ↔ P i
x : M
⊢ x ∈ b → x ∈ s
Tactic:
intro hx
State after:
case intro.h.mp
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
a s : M
hs : s < exp a
Ha : ∀ i < a, i ∈ s ↔ P i
b : M
hb : b < exp a
Hb : ∀ i < a, i ∈ b ↔ P i
x : M
hx : x ∈ b
⊢ x ∈ s

State before:
case intro.h.mp
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
a s : M
hs : s < exp a
Ha : ∀ i < a, i ∈ s ↔ P i
b : M
hb : b < exp a
Hb : ∀ i < a, i ∈ b ↔ P i
x : M
hx : x ∈ b
⊢ x ∈ s
Tactic:
have : x < a := exp_monotone.mp <| LE.le.trans_lt (exp_le_of_mem hx) hb
State after:
case intro.h.mp
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
a s : M
hs : s < exp a
Ha : ∀ i < a, i ∈ s ↔ P i
b : M
hb : b < exp a
Hb : ∀ i < a, i ∈ b ↔ P i
x : M
hx : x ∈ b
this : x < a
⊢ x ∈ s

State before:
case intro.h.mp
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
a s : M
hs : s < exp a
Ha : ∀ i < a, i ∈ s ↔ P i
b : M
hb : b < exp a
Hb : ∀ i < a, i ∈ b ↔ P i
x : M
hx : x ∈ b
this : x < a
⊢ x ∈ s
Tactic:
exact (Ha x this).mpr <| (Hb x this).mp hx
State after:
no goals

State before:
case intro.h.mpr
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
a s : M
hs : s < exp a
Ha : ∀ i < a, i ∈ s ↔ P i
b : M
hb : b < exp a
Hb : ∀ i < a, i ∈ b ↔ P i
x : M
⊢ x ∈ s → x ∈ b
Tactic:
intro hx
State after:
case intro.h.mpr
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
a s : M
hs : s < exp a
Ha : ∀ i < a, i ∈ s ↔ P i
b : M
hb : b < exp a
Hb : ∀ i < a, i ∈ b ↔ P i
x : M
hx : x ∈ s
⊢ x ∈ b

State before:
case intro.h.mpr
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
a s : M
hs : s < exp a
Ha : ∀ i < a, i ∈ s ↔ P i
b : M
hb : b < exp a
Hb : ∀ i < a, i ∈ b ↔ P i
x : M
hx : x ∈ s
⊢ x ∈ b
Tactic:
have : x < a := exp_monotone.mp <| LE.le.trans_lt (exp_le_of_mem hx) hs
State after:
case intro.h.mpr
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
a s : M
hs : s < exp a
Ha : ∀ i < a, i ∈ s ↔ P i
b : M
hb : b < exp a
Hb : ∀ i < a, i ∈ b ↔ P i
x : M
hx : x ∈ s
this : x < a
⊢ x ∈ b

State before:
case intro.h.mpr
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
a s : M
hs : s < exp a
Ha : ∀ i < a, i ∈ s ↔ P i
b : M
hb : b < exp a
Hb : ∀ i < a, i ∈ b ↔ P i
x : M
hx : x ∈ s
this : x < a
⊢ x ∈ b
Tactic:
exact (Hb x this).mpr <| (Ha x this).mp hx
State after:
no goals