internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.le_of_subset
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
b : M
IH : ∀ {a : M}, a ⊆ b → a ≤ b
a : M
h : a ⊆ 2 * b + 1
⊢ a ≤ 2 * b + 1
Tactic:
have IH : a / 2 ≤ b := IH (by simpa [div_mul_add' b 2 one_lt_two] using subset_div_two h)
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
b : M
IH✝ : ∀ {a : M}, a ⊆ b → a ≤ b
a : M
h : a ⊆ 2 * b + 1
IH : a / 2 ≤ b
⊢ a ≤ 2 * b + 1
Theorem: LO.FirstOrder.Arith.Model.le_of_subset
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
b : M
IH✝ : ∀ {a : M}, a ⊆ b → a ≤ b
a : M
h : a ⊆ 2 * b + 1
IH : a / 2 ≤ b
⊢ a ≤ 2 * b + 1
Tactic:
exact le_trans (le_two_mul_div_two_add_one a) (by simpa using IH)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.le_of_subset
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
b : M
IH : ∀ {a : M}, a ⊆ b → a ≤ b
a : M
h : a ⊆ 2 * b + 1
⊢ a / 2 ⊆ b
Tactic:
simpa [div_mul_add' b 2 one_lt_two] using subset_div_two h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.le_of_subset
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
b : M
IH✝ : ∀ {a : M}, a ⊆ b → a ≤ b
a : M
h : a ⊆ 2 * b + 1
IH : a / 2 ≤ b
⊢ 2 * (a / 2) + 1 ≤ 2 * b + 1
Tactic:
simpa using IH
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.nonempty_of_pos
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a : M
h : 0 < a
⊢ ∃ i, i ∈ a
Tactic:
by_contra A
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a : M
h : 0 < a
A : ¬∃ i, i ∈ a
⊢ False
Theorem: LO.FirstOrder.Arith.Model.nonempty_of_pos
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a : M
h : 0 < a
A : ¬∃ i, i ∈ a
⊢ False
Tactic:
have : a = 0 := mem_ext (by simpa using A)
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a : M
h : 0 < a
A : ¬∃ i, i ∈ a
this : a = 0
⊢ False
Theorem: LO.FirstOrder.Arith.Model.nonempty_of_pos
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a : M
h : 0 < a
A : ¬∃ i, i ∈ a
this : a = 0
⊢ False
Tactic:
simp [this] at h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.nonempty_of_pos
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a : M
h : 0 < a
A : ¬∃ i, i ∈ a
⊢ ∀ (i : M), i ∈ a ↔ i ∈ 0
Tactic:
simpa using A
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.eq_empty_or_nonempty
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a : M
⊢ a = ∅ ∨ ∃ i, i ∈ a
Tactic:
rcases zero_le a with (rfl | pos)
Proof state after:
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
⊢ 0 = ∅ ∨ ∃ i, i ∈ 0

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a : M
pos : 0 < a
⊢ a = ∅ ∨ ∃ i, i ∈ a
Theorem: LO.FirstOrder.Arith.Model.eq_empty_or_nonempty
Proof state before:
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
⊢ 0 = ∅ ∨ ∃ i, i ∈ 0
Tactic:
simp [emptyset_def]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.eq_empty_or_nonempty
Proof state before:
case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a : M
pos : 0 < a
⊢ a = ∅ ∨ ∃ i, i ∈ a
Tactic:
right
Proof state after:
case inr.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a : M
pos : 0 < a
⊢ ∃ i, i ∈ a
Theorem: LO.FirstOrder.Arith.Model.eq_empty_or_nonempty
Proof state before:
case inr.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a : M
pos : 0 < a
⊢ ∃ i, i ∈ a
Tactic:
exact nonempty_of_pos pos
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.nonempty_iff
Proof 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
⊢ s ≠ ∅ ↔ ∃ x, x ∈ s
Tactic:
rcases eq_empty_or_nonempty s with ⟨rfl, hy⟩ <;> simp
Proof state after:
case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h✝ : ∃ i, i ∈ s
⊢ ¬s = ∅ ↔ ∃ x, x ∈ s
Theorem: LO.FirstOrder.Arith.Model.nonempty_iff
Proof state before:
case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h✝ : ∃ i, i ∈ s
⊢ ¬s = ∅ ↔ ∃ x, x ∈ s
Tactic:
simp [show s ≠ ∅ from by rintro rfl; simp_all]
Proof state after:
case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h✝ : ∃ i, i ∈ s
⊢ ∃ x, x ∈ s
Theorem: LO.FirstOrder.Arith.Model.nonempty_iff
Proof state before:
case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h✝ : ∃ i, i ∈ s
⊢ ∃ x, x ∈ s
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.nonempty_iff
Proof 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
h✝ : ∃ i, i ∈ s
⊢ s ≠ ∅
Tactic:
rintro rfl
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
h✝ : ∃ i, i ∈ ∅
⊢ False
Theorem: LO.FirstOrder.Arith.Model.nonempty_iff
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
h✝ : ∃ i, i ∈ ∅
⊢ False
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.isempty_iff
Proof 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
⊢ s = ∅ ↔ ∀ (x : M), x ∉ s
Tactic:
simpa using not_iff_not.mpr (nonempty_iff (s := s))
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lt_of_lt_log
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a b : M
pos : 0 < b
h : ∀ i ∈ a, i < log b
⊢ a < b
Tactic:
rcases zero_le a with (rfl | apos)
Proof state after:
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
b : M
pos : 0 < b
h : ∀ i ∈ 0, i < log b
⊢ 0 < b

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a b : M
pos : 0 < b
h : ∀ i ∈ a, i < log b
apos : 0 < a
⊢ a < b
Theorem: LO.FirstOrder.Arith.Model.lt_of_lt_log
Proof state before:
case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a b : M
pos : 0 < b
h : ∀ i ∈ a, i < log b
apos : 0 < a
⊢ a < b
Tactic:
by_contra A
Proof state after:
case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a b : M
pos : 0 < b
h : ∀ i ∈ a, i < log b
apos : 0 < a
A : ¬a < b
⊢ False
Theorem: LO.FirstOrder.Arith.Model.lt_of_lt_log
Proof state before:
case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a b : M
pos : 0 < b
h : ∀ i ∈ a, i < log b
apos : 0 < a
A : ¬a < b
⊢ False
Tactic:
exact not_lt_of_le (log_monotone <| show b ≤ a by simpa using A) (h (log a) (log_mem_of_pos apos))
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lt_of_lt_log
Proof state before:
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
b : M
pos : 0 < b
h : ∀ i ∈ 0, i < log b
⊢ 0 < b
Tactic:
exact pos
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lt_of_lt_log
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a b : M
pos : 0 < b
h : ∀ i ∈ a, i < log b
apos : 0 < a
A : ¬a < b
⊢ b ≤ a
Tactic:
simpa using A
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.under_inj
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i j : M
h : under i = under j
⊢ i = j
Tactic:
by_contra ne
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i j : M
h : under i = under j
ne : ¬i = j
⊢ False
Theorem: LO.FirstOrder.Arith.Model.under_inj
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i j : M
h : under i = under j
ne : ¬i = j
⊢ False
Tactic:
wlog lt : i < j
Proof state after:
case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i j : M
h : under i = under j
ne : ¬i = j
this :
  ∀ {M : Type u_1} [inst : Zero M] [inst_1 : One M] [inst_2 : Add M] [inst_3 : Mul M] [inst_4 : LT M]
    [inst_5 : M ⊧ₘ* 𝐈𝚺₁] {i j : M}, under i = under j → ¬i = j → i < j → False
lt : ¬i < j
⊢ False

M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚺₁
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i j : M
h : under i = under j
ne : ¬i = j
lt : i < j
⊢ False
Theorem: LO.FirstOrder.Arith.Model.under_inj
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 : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i j : M
h : under i = under j
ne : ¬i = j
lt : i < j
⊢ False
Tactic:
have : i ∉ under i := by simp
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 : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i j : M
h : under i = under j
ne : ¬i = j
lt : i < j
this : i ∉ under i
⊢ False
Theorem: LO.FirstOrder.Arith.Model.under_inj
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 : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i j : M
h : under i = under j
ne : ¬i = j
lt : i < j
this : i ∉ under i
⊢ False
Tactic:
have : i ∈ under i := by rw [h]; simp [mem_under_iff, 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 : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i j : M
h : under i = under j
ne : ¬i = j
lt : i < j
this✝ : i ∉ under i
this : i ∈ under i
⊢ False
Theorem: LO.FirstOrder.Arith.Model.under_inj
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 : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i j : M
h : under i = under j
ne : ¬i = j
lt : i < j
this✝ : i ∉ under i
this : i ∈ under i
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.under_inj
Proof state before:
case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i j : M
h : under i = under j
ne : ¬i = j
this :
  ∀ {M : Type u_1} [inst : Zero M] [inst_1 : One M] [inst_2 : Add M] [inst_3 : Mul M] [inst_4 : LT M]
    [inst_5 : M ⊧ₘ* 𝐈𝚺₁] {i j : M}, under i = under j → ¬i = j → i < j → False
lt : ¬i < j
⊢ False
Tactic:
exact this (Eq.symm h) (Ne.symm ne) (lt_of_le_of_ne (by simpa using lt) (Ne.symm ne))
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.under_inj
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i j : M
h : under i = under j
ne : ¬i = j
this :
  ∀ {M : Type u_1} [inst : Zero M] [inst_1 : One M] [inst_2 : Add M] [inst_3 : Mul M] [inst_4 : LT M]
    [inst_5 : M ⊧ₘ* 𝐈𝚺₁] {i j : M}, under i = under j → ¬i = j → i < j → False
lt : ¬i < j
⊢ j ≤ i
Tactic:
simpa using lt
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.under_inj
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 : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i j : M
h : under i = under j
ne : ¬i = j
lt : i < j
⊢ i ∉ under i
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.under_inj
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 : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i j : M
h : under i = under j
ne : ¬i = j
lt : i < j
this : i ∉ under i
⊢ i ∈ under i
Tactic:
rw [h]
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 : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i j : M
h : under i = under j
ne : ¬i = j
lt : i < j
this : i ∉ under i
⊢ i ∈ under j
Theorem: LO.FirstOrder.Arith.Model.under_inj
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 : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i j : M
h : under i = under j
ne : ¬i = j
lt : i < j
this : i ∉ under i
⊢ i ∈ under j
Tactic:
simp [mem_under_iff, lt]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.under_inj
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i j : M
⊢ i = j → under i = under j
Tactic:
rintro rfl
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i : M
⊢ under i = under i
Theorem: LO.FirstOrder.Arith.Model.under_inj
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i : M
⊢ under i = under i
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.under_zero
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
⊢ ∀ (i : M), i ∈ under 0 ↔ i ∈ ∅
Tactic:
simp [mem_under_iff]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.under_succ
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i : M
⊢ ∀ (i_1 : M), i_1 ∈ under (i + 1) ↔ i_1 ∈ insert i (under i)
Tactic:
simp [mem_under_iff, lt_succ_iff_le, le_iff_eq_or_lt]
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
⊢ ∃ 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
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
⊢ ∃ s < exp a, ∀ i < a, i ∈ s ↔ 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 < exp a, ∀ i < a, i ∈ s ↔ P i
Tactic:
have : ∃ s < exp a, ∀ i < a, P i → i ∈ s :=
  ⟨under a, pred_lt_self_of_pos (by simp), fun i hi _ ↦ by simpa [mem_under_iff] using 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 ⊧ₘ* 𝐈𝚺₁
this : ∃ s < exp a, ∀ i < a, P i → i ∈ s
⊢ ∃ s < exp a, ∀ i < a, i ∈ s ↔ 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 ⊧ₘ* 𝐈𝚺₁
this : ∃ s < exp a, ∀ i < a, P i → i ∈ s
⊢ ∃ s < exp a, ∀ i < a, i ∈ s ↔ P i
Tactic:
rcases this with ⟨s, hsn, 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
Γ : 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
⊢ ∃ s < exp a, ∀ i < a, i ∈ s ↔ P i
Theorem: LO.FirstOrder.Arith.Model.finset_comprehension_aux
Proof 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 ⊧ₘ* 𝐈𝚺₁
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
⊢ ∃ s < exp a, ∀ i < a, i ∈ s ↔ P i
Tactic:
have : (Γ.alt, m)-Predicate (fun s : M ↦ ∀ i < a, P i → i ∈ s) := by
  apply Definable.ball_lt₀; simp; apply Definable.imp <;> definability
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
Γ : 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
⊢ ∃ s < exp a, ∀ i < a, i ∈ s ↔ P i
Theorem: LO.FirstOrder.Arith.Model.finset_comprehension_aux
Proof 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 ⊧ₘ* 𝐈𝚺₁
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
⊢ ∃ s < exp a, ∀ i < a, i ∈ s ↔ P i
Tactic:
have : ∃ t, (∀ i < a, P i → i ∈ t) ∧ ∀ t' < t, ∃ x < a, P x ∧ x ∉ (t' : M) := by
  simpa using least_number_h (L := ℒₒᵣ) Γ.alt m this 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
Γ : 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
this : ∃ t, (∀ i < a, P i → i ∈ t) ∧ ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
⊢ ∃ s < exp a, ∀ i < a, i ∈ s ↔ P i
Theorem: LO.FirstOrder.Arith.Model.finset_comprehension_aux
Proof 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 ⊧ₘ* 𝐈𝚺₁
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
this : ∃ t, (∀ i < a, P i → i ∈ t) ∧ ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
⊢ ∃ s < exp a, ∀ i < a, i ∈ s ↔ P i
Tactic:
rcases this with ⟨t, ht, t_minimal⟩
Proof state after:
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'
⊢ ∃ s < exp a, ∀ i < a, i ∈ s ↔ P i
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'
⊢ ∃ s < exp a, ∀ i < a, i ∈ s ↔ P i
Tactic:
have t_le_s : t ≤ s := not_lt.mp (by
  intro lt
  rcases t_minimal s lt with ⟨i, hin, hi, his⟩
  exact his (hs i hin hi))
Proof state after:
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
⊢ ∃ s < exp a, ∀ i < a, i ∈ s ↔ P i
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
⊢ ∃ s < exp a, ∀ i < a, i ∈ s ↔ P i
Tactic:
have : ∀ i < a, i ∈ t → P i := by
  intro i _ hit
  by_contra Hi
  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)
  rcases this with ⟨j, hjn, Hj, hm⟩
  rcases hm (ht j hjn Hj); contradiction
Proof state after:
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