internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.finset_comprehension_aux
Proof state before:
case intro.intro.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
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝¹ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this✝ : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
t : M
ht : ∀ i < a, P i → i ∈ t
t_minimal : ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
t_le_s : t ≤ s
this : ∀ i < a, i ∈ t → P i
⊢ ∃ s < exp a, ∀ i < a, i ∈ s ↔ P i
Tactic:
exact ⟨t, lt_of_le_of_lt t_le_s hsn, fun i hi ↦ ⟨this i hi, ht i hi⟩⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.finset_comprehension_aux
Proof 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
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
⊢ 0 < exp a
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.finset_comprehension_aux
Proof 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
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
i : M
hi : i < a
x✝ : P i
⊢ i ∈ under a
Tactic:
simpa [mem_under_iff] using hi
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.finset_comprehension_aux
Proof 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
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
⊢ (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
Tactic:
apply Definable.ball_lt₀
Proof state after:
case hf
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
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
⊢ DefinableBoundedFunction ℒₒᵣ (Γ.alt.coe, m) fun v => a

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
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
⊢ Definable ℒₒᵣ (Γ.alt.coe, m) fun w => P (w 0) → w 0 ∈ (fun x => w x.succ) 0
Theorem: LO.FirstOrder.Arith.Model.finset_comprehension_aux
Proof state before:
case hf
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
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
⊢ DefinableBoundedFunction ℒₒᵣ (Γ.alt.coe, m) fun v => a

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
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
⊢ Definable ℒₒᵣ (Γ.alt.coe, m) fun w => P (w 0) → w 0 ∈ (fun x => w x.succ) 0
Tactic:
simp
Proof 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
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
⊢ Definable ℒₒᵣ (Γ.alt.coe, m) fun w => P (w 0) → w 0 ∈ (fun x => w x.succ) 0
Theorem: LO.FirstOrder.Arith.Model.finset_comprehension_aux
Proof 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
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
⊢ Definable ℒₒᵣ (Γ.alt.coe, m) fun w => P (w 0) → w 0 ∈ (fun x => w x.succ) 0
Tactic:
apply Definable.imp <;> definability
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.finset_comprehension_aux
Proof 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
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
⊢ ∃ t, (∀ i < a, P i → i ∈ t) ∧ ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
Tactic:
simpa using least_number_h (L := ℒₒᵣ) Γ.alt m this hs
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.finset_comprehension_aux
Proof 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
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
t : M
ht : ∀ i < a, P i → i ∈ t
t_minimal : ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
⊢ ¬s < t
Tactic:
intro lt
Proof 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
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
t : M
ht : ∀ i < a, P i → i ∈ t
t_minimal : ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
lt : s < t
⊢ False
Theorem: LO.FirstOrder.Arith.Model.finset_comprehension_aux
Proof 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
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
t : M
ht : ∀ i < a, P i → i ∈ t
t_minimal : ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
lt : s < t
⊢ False
Tactic:
rcases t_minimal s lt with ⟨i, hin, hi, his⟩
Proof 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 ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
t : M
ht : ∀ i < a, P i → i ∈ t
t_minimal : ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
lt : s < t
i : M
hin : i < a
hi : P i
his : i ∉ s
⊢ False
Theorem: LO.FirstOrder.Arith.Model.finset_comprehension_aux
Proof 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 ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
t : M
ht : ∀ i < a, P i → i ∈ t
t_minimal : ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
lt : s < t
i : M
hin : i < a
hi : P i
his : i ∉ s
⊢ False
Tactic:
exact his (hs i hin hi)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.finset_comprehension_aux
Proof 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
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
t : M
ht : ∀ i < a, P i → i ∈ t
t_minimal : ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
t_le_s : t ≤ s
⊢ ∀ i < a, i ∈ t → P i
Tactic:
intro i _ hit
Proof 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
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
t : M
ht : ∀ i < a, P i → i ∈ t
t_minimal : ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
t_le_s : t ≤ s
i : M
a✝ : i < a
hit : i ∈ t
⊢ P i
Theorem: LO.FirstOrder.Arith.Model.finset_comprehension_aux
Proof 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
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
t : M
ht : ∀ i < a, P i → i ∈ t
t_minimal : ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
t_le_s : t ≤ s
i : M
a✝ : i < a
hit : i ∈ t
⊢ P i
Tactic:
by_contra Hi
Proof 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
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
t : M
ht : ∀ i < a, P i → i ∈ t
t_minimal : ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
t_le_s : t ≤ s
i : M
a✝ : i < a
hit : i ∈ t
Hi : ¬P i
⊢ False
Theorem: LO.FirstOrder.Arith.Model.finset_comprehension_aux
Proof 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
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
t : M
ht : ∀ i < a, P i → i ∈ t
t_minimal : ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
t_le_s : t ≤ s
i : M
a✝ : i < a
hit : i ∈ t
Hi : ¬P i
⊢ False
Tactic:
have : ∃ j < a, P j ∧ (j ∈ t → j = i) := by
  simpa [not_imp_not] using t_minimal (bitRemove i t) (bitRemove_lt_of_mem hit)
Proof 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
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝¹ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this✝ : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
t : M
ht : ∀ i < a, P i → i ∈ t
t_minimal : ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
t_le_s : t ≤ s
i : M
a✝ : i < a
hit : i ∈ t
Hi : ¬P i
this : ∃ j < a, P j ∧ (j ∈ t → j = i)
⊢ False
Theorem: LO.FirstOrder.Arith.Model.finset_comprehension_aux
Proof 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
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝¹ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this✝ : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
t : M
ht : ∀ i < a, P i → i ∈ t
t_minimal : ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
t_le_s : t ≤ s
i : M
a✝ : i < a
hit : i ∈ t
Hi : ¬P i
this : ∃ j < a, P j ∧ (j ∈ t → j = i)
⊢ False
Tactic:
rcases this with ⟨j, hjn, Hj, hm⟩
Proof 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 ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
t : M
ht : ∀ i < a, P i → i ∈ t
t_minimal : ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
t_le_s : t ≤ s
i : M
a✝ : i < a
hit : i ∈ t
Hi : ¬P i
j : M
hjn : j < a
Hj : P j
hm : j ∈ t → j = i
⊢ False
Theorem: LO.FirstOrder.Arith.Model.finset_comprehension_aux
Proof 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 ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
t : M
ht : ∀ i < a, P i → i ∈ t
t_minimal : ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
t_le_s : t ≤ s
i : M
a✝ : i < a
hit : i ∈ t
Hi : ¬P i
j : M
hjn : j < a
Hj : P j
hm : j ∈ t → j = i
⊢ False
Tactic:
rcases hm (ht j hjn Hj)
Proof state after:
case intro.intro.intro.refl
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
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
t : M
ht : ∀ i < a, P i → i ∈ t
t_minimal : ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
t_le_s : t ≤ s
i : M
a✝ : i < a
hit : i ∈ t
Hi : ¬P i
hjn : i < a
Hj : P i
hm : i ∈ t → i = i
⊢ False
Theorem: LO.FirstOrder.Arith.Model.finset_comprehension_aux
Proof state before:
case intro.intro.intro.refl
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
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
t : M
ht : ∀ i < a, P i → i ∈ t
t_minimal : ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
t_le_s : t ≤ s
i : M
a✝ : i < a
hit : i ∈ t
Hi : ¬P i
hjn : i < a
Hj : P i
hm : i ∈ t → i = i
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.finset_comprehension_aux
Proof 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
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
t : M
ht : ∀ i < a, P i → i ∈ t
t_minimal : ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
t_le_s : t ≤ s
i : M
a✝ : i < a
hit : i ∈ t
Hi : ¬P i
⊢ ∃ j < a, P j ∧ (j ∈ t → j = i)
Tactic:
simpa [not_imp_not] using t_minimal (bitRemove i t) (bitRemove_lt_of_mem hit)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.finset_comprehension_exists_unique
Proof 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)
Proof 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
Theorem: LO.FirstOrder.Arith.Model.finset_comprehension_exists_unique
Proof 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⟩
Proof 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
Theorem: LO.FirstOrder.Arith.Model.finset_comprehension_exists_unique
Proof 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⟩
Proof 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
Theorem: LO.FirstOrder.Arith.Model.finset_comprehension_exists_unique
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.finset_comprehension_exists_unique
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.finset_comprehension_exists_unique
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.finset_comprehension_exists_unique
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.finset_comprehension_exists_unique
Proof 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)
Proof 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
Theorem: LO.FirstOrder.Arith.Model.finset_comprehension_exists_unique
Proof 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)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.finset_comprehension_exists_unique
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.finset_comprehension_exists_unique
Proof 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)
Proof 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