internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.memRel_defined
Proof state before:
ξ : Type u_1
n : ?m.110780
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 3 → M
⊢ ⟪v 1, v 2⟫ ∈ v 0 ↔ ∃ x ≤ (v 1 + v 2 + 1) ^ 2, x = ⟪v 1, v 2⟫ ∧ x ∈ v 0
Tactic:
constructor
Proof state after:
case mp
ξ : Type u_1
n : ?m.110780
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 3 → M
⊢ ⟪v 1, v 2⟫ ∈ v 0 → ∃ x ≤ (v 1 + v 2 + 1) ^ 2, x = ⟪v 1, v 2⟫ ∧ x ∈ v 0

case mpr
ξ : Type u_1
n : ?m.110780
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 3 → M
⊢ (∃ x ≤ (v 1 + v 2 + 1) ^ 2, x = ⟪v 1, v 2⟫ ∧ x ∈ v 0) → ⟪v 1, v 2⟫ ∈ v 0
Theorem: LO.FirstOrder.Arith.Model.memRel_defined
Proof state before:
case mp
ξ : Type u_1
n : ?m.110780
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 3 → M
⊢ ⟪v 1, v 2⟫ ∈ v 0 → ∃ x ≤ (v 1 + v 2 + 1) ^ 2, x = ⟪v 1, v 2⟫ ∧ x ∈ v 0
Tactic:
intro h
Proof state after:
case mp
ξ : Type u_1
n : ?m.110780
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 3 → M
h : ⟪v 1, v 2⟫ ∈ v 0
⊢ ∃ x ≤ (v 1 + v 2 + 1) ^ 2, x = ⟪v 1, v 2⟫ ∧ x ∈ v 0
Theorem: LO.FirstOrder.Arith.Model.memRel_defined
Proof state before:
case mp
ξ : Type u_1
n : ?m.110780
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 3 → M
h : ⟪v 1, v 2⟫ ∈ v 0
⊢ ∃ x ≤ (v 1 + v 2 + 1) ^ 2, x = ⟪v 1, v 2⟫ ∧ x ∈ v 0
Tactic:
exact ⟨⟪v 1, v 2⟫, by simp, rfl, h⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.memRel_defined
Proof state before:
ξ : Type u_1
n : ?m.110780
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 3 → M
h : ⟪v 1, v 2⟫ ∈ v 0
⊢ ⟪v 1, v 2⟫ ≤ (v 1 + v 2 + 1) ^ 2
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.memRel_defined
Proof state before:
case mpr
ξ : Type u_1
n : ?m.110780
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 3 → M
⊢ (∃ x ≤ (v 1 + v 2 + 1) ^ 2, x = ⟪v 1, v 2⟫ ∧ x ∈ v 0) → ⟪v 1, v 2⟫ ∈ v 0
Tactic:
rintro ⟨_, _, rfl, h⟩
Proof state after:
case mpr.intro.intro.intro
ξ : Type u_1
n : ?m.110780
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 3 → M
left✝ : ⟪v 1, v 2⟫ ≤ (v 1 + v 2 + 1) ^ 2
h : ⟪v 1, v 2⟫ ∈ v 0
⊢ ⟪v 1, v 2⟫ ∈ v 0
Theorem: LO.FirstOrder.Arith.Model.memRel_defined
Proof state before:
case mpr.intro.intro.intro
ξ : Type u_1
n : ?m.110780
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 3 → M
left✝ : ⟪v 1, v 2⟫ ≤ (v 1 + v 2 + 1) ^ 2
h : ⟪v 1, v 2⟫ ∈ v 0
⊢ ⟪v 1, v 2⟫ ∈ v 0
Tactic:
exact h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.eval_memRel
Proof state before:
ξ : Type u_1
n : ?m.134755
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
x y r : M
⊢ memRelOpr.val ![r, x, y] ↔ ⟪x, y⟫ ∈ r
Tactic:
unfold Semiformula.Operator.val
Proof state after:
ξ : Type u_1
n : ?m.134755
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
x y r : M
⊢ (Semiformula.Eval (standardModel M) ![r, x, y] Empty.elim) memRelOpr.sentence ↔ ⟪x, y⟫ ∈ r
Theorem: LO.FirstOrder.Arith.eval_memRel
Proof state before:
ξ : Type u_1
n : ?m.134755
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
x y r : M
⊢ (Semiformula.Eval (standardModel M) ![r, x, y] Empty.elim) memRelOpr.sentence ↔ ⟪x, y⟫ ∈ r
Tactic:
simp [memRelOpr, pair_defined.df.iff, memRel_defined.df.iff]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_iff_mul_exp_add_exp_add
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 a : M
⊢ i ∈ a ↔ ∃ k, ∃ r < exp i, a = k * exp (i + 1) + exp i + r
Tactic:
simp [mem_iff_bit, exp_succ]
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 a : M
⊢ Bit i a ↔ ∃ k, ∃ r < exp i, a = k * (2 * exp i) + exp i + r
Theorem: LO.FirstOrder.Arith.Model.mem_iff_mul_exp_add_exp_add
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 a : M
⊢ Bit i a ↔ ∃ k, ∃ r < exp i, a = k * (2 * exp i) + exp i + r
Tactic:
exact lenbit_iff_add_mul (exp_pow2 i) (a := a)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.not_mem_iff_mul_exp_add
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 a : M
⊢ i ∉ a ↔ ∃ k, ∃ r < exp i, a = k * exp (i + 1) + r
Tactic:
simp [mem_iff_bit, exp_succ]
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 a : M
⊢ ¬Bit i a ↔ ∃ k, ∃ r < exp i, a = k * (2 * exp i) + r
Theorem: LO.FirstOrder.Arith.Model.not_mem_iff_mul_exp_add
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 a : M
⊢ ¬Bit i a ↔ ∃ k, ∃ r < exp i, a = k * (2 * exp i) + r
Tactic:
exact not_lenbit_iff_add_mul (exp_pow2 i) (a := a)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.not_mem_empty
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 ∉ ∅
Tactic:
simp [emptyset_def, mem_iff_bit, Bit]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.not_mem_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 ∉ 0
Tactic:
simp [mem_iff_bit, Bit]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.singleton_eq_insert
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} = insert i ∅
Tactic:
simp [singleton_def, insert, bitInsert, emptyset_def]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_bitInsert_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 ⊧ₘ* 𝐈𝚺₁
i j a : M
⊢ i ∈ insert j a ↔ i = j ∨ i ∈ a
Tactic:
by_cases h : j ∈ a <;> simp [h, insert_eq, bitInsert]
Proof state after:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i j a : M
h : j ∈ a
⊢ i = j → i ∈ a

case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i j a : M
h : j ∉ a
⊢ i ∈ a + exp j ↔ i = j ∨ i ∈ a
Theorem: LO.FirstOrder.Arith.Model.mem_bitInsert_iff
Proof state before:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i j a : M
h : j ∈ a
⊢ i = j → i ∈ a
Tactic:
by_cases e : i = j <;> simp [h, e]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_bitInsert_iff
Proof state before:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i j a : M
h : j ∉ a
⊢ i ∈ a + exp j ↔ i = j ∨ i ∈ a
Tactic:
simpa [exp_inj.eq_iff] using
  lenbit_add_pow2_iff_of_not_lenbit (exp_pow2 i) (exp_pow2 j) h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_bitRemove_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 ⊧ₘ* 𝐈𝚺₁
i j a : M
⊢ i ∈ bitRemove j a ↔ i ≠ j ∧ i ∈ a
Tactic:
by_cases h : j ∈ a <;> simp [h, bitRemove]
Proof state after:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i j a : M
h : j ∈ a
⊢ i ∈ a - exp j ↔ ¬i = j ∧ i ∈ a

case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i j a : M
h : j ∉ a
⊢ i ∈ a → ¬i = j
Theorem: LO.FirstOrder.Arith.Model.mem_bitRemove_iff
Proof state before:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i j a : M
h : j ∈ a
⊢ i ∈ a - exp j ↔ ¬i = j ∧ i ∈ a
Tactic:
simpa [exp_inj.eq_iff] using
  lenbit_sub_pow2_iff_of_lenbit (exp_pow2 i) (exp_pow2 j) h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_bitRemove_iff
Proof state before:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i j a : M
h : j ∉ a
⊢ i ∈ a → ¬i = j
Tactic:
rintro _ rfl
Proof state after:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i a : M
a✝ : i ∈ a
h : i ∉ a
⊢ False
Theorem: LO.FirstOrder.Arith.Model.mem_bitRemove_iff
Proof state before:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i a : M
a✝ : i ∈ a
h : i ∉ a
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.insert_graph
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 i a : M
⊢ b = insert i a → i ∈ a ∧ b = a ∨ i ∉ a ∧ ∃ e ≤ b, e = exp i ∧ b = a + e
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 a : M
⊢ i ∈ a ∧ insert i a = a ∨ i ∉ a ∧ ∃ e ≤ insert i a, e = exp i ∧ insert i a = a + e
Theorem: LO.FirstOrder.Arith.Model.insert_graph
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 a : M
⊢ i ∈ a ∧ insert i a = a ∨ i ∉ a ∧ ∃ e ≤ insert i a, e = exp i ∧ insert i a = a + e
Tactic:
by_cases hi : i ∈ a <;> simp [hi, insert, bitInsert]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.insert_graph
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 i a : M
⊢ (i ∈ a ∧ b = a ∨ i ∉ a ∧ ∃ e ≤ b, e = exp i ∧ b = a + e) → b = insert i a
Tactic:
by_cases hi : i ∈ a <;> simp only [hi, true_and, not_true_eq_false, false_and,
  or_false, insert, bitInsert, ↓reduceIte, imp_self,
  not_false_eq_true, true_and, false_or, forall_exists_index, and_imp]
Proof state after:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
b i a : M
hi : i ∉ a
⊢ ∀ x ≤ b, x = exp i → b = a + x → b = a + exp i
Theorem: LO.FirstOrder.Arith.Model.insert_graph
Proof state before:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
b i a : M
hi : i ∉ a
⊢ ∀ x ≤ b, x = exp i → b = a + x → b = a + exp i
Tactic:
rintro x _ rfl rfl
Proof state after:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i a : M
hi : i ∉ a
a✝ : exp i ≤ a + exp i
⊢ a + exp i = a + exp i
Theorem: LO.FirstOrder.Arith.Model.insert_graph
Proof state before:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i a : M
hi : i ∉ a
a✝ : exp i ≤ a + exp i
⊢ a + exp i = a + exp i
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.insert_defined
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
⊢ 𝚺₀-Function₂ insert via insertDef
Tactic:
intro v
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin (Nat.succ 2) → M
⊢ (fun v => v 0 = (fun v => insert (v 0) (v 1)) fun x => v x.succ) v ↔
    (Semiformula.Evalbm M v) (HSemiformula.val insertDef)
Theorem: LO.FirstOrder.Arith.Model.insert_defined
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin (Nat.succ 2) → M
⊢ (fun v => v 0 = (fun v => insert (v 0) (v 1)) fun x => v x.succ) v ↔
    (Semiformula.Evalbm M v) (HSemiformula.val insertDef)
Tactic:
simp [insertDef, insert_graph]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.insert_le_of_le_of_le
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 a b : M
hij : i ≤ j
hab : a ≤ b
⊢ insert i a ≤ b + exp j
Tactic:
simp [insert, bitInsert]
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 a b : M
hij : i ≤ j
hab : a ≤ b
⊢ (if i ∈ a then a else a + exp i) ≤ b + exp j
Theorem: LO.FirstOrder.Arith.Model.insert_le_of_le_of_le
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 a b : M
hij : i ≤ j
hab : a ≤ b
⊢ (if i ∈ a then a else a + exp i) ≤ b + exp j
Tactic:
by_cases hi : i ∈ a <;> simp [hi]
Proof state after:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i j a b : M
hij : i ≤ j
hab : a ≤ b
hi : i ∈ a
⊢ a ≤ b + exp j

case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i j a b : M
hij : i ≤ j
hab : a ≤ b
hi : i ∉ a
⊢ a + exp i ≤ b + exp j
Theorem: LO.FirstOrder.Arith.Model.insert_le_of_le_of_le
Proof state before:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i j a b : M
hij : i ≤ j
hab : a ≤ b
hi : i ∈ a
⊢ a ≤ b + exp j
Tactic:
exact le_trans hab (by simp)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.insert_le_of_le_of_le
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 a b : M
hij : i ≤ j
hab : a ≤ b
hi : i ∈ a
⊢ b ≤ b + exp j
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.insert_le_of_le_of_le
Proof state before:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i j a b : M
hij : i ≤ j
hab : a ≤ b
hi : i ∉ a
⊢ a + exp i ≤ b + exp j
Tactic:
exact add_le_add hab (exp_monotone_le.mpr hij)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.one_eq_singleton
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
⊢ 1 = {∅}
Tactic:
simp [singleton_eq_insert, insert, bitInsert, emptyset_def]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_singleton_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 ⊧ₘ* 𝐈𝚺₁
i j : M
⊢ i ∈ {j} ↔ i = j
Tactic:
simp [singleton_eq_insert]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.bitRemove_lt_of_mem
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 a : M
h : i ∈ a
⊢ bitRemove i a < a
Tactic:
simp [h, bitRemove, tsub_lt_iff_left (exp_le_of_mem h)]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pos_of_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 ⊧ₘ* 𝐈𝚺₁
i a : M
h : i ∈ a
⊢ 0 < 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 ⊧ₘ* 𝐈𝚺₁
i a : M
h : i ∈ a
A : ¬0 < a
⊢ False
Theorem: LO.FirstOrder.Arith.Model.pos_of_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 ⊧ₘ* 𝐈𝚺₁
i a : M
h : i ∈ a
A : ¬0 < a
⊢ False
Tactic:
simp at 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 ⊧ₘ* 𝐈𝚺₁
i a : M
h : i ∈ a
A : a = 0
⊢ False
Theorem: LO.FirstOrder.Arith.Model.pos_of_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 ⊧ₘ* 𝐈𝚺₁
i a : M
h : i ∈ a
A : a = 0
⊢ False
Tactic:
rcases A
Proof state after:
case refl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i : M
h : i ∈ 0
⊢ False
Theorem: LO.FirstOrder.Arith.Model.pos_of_nonempty
Proof state before:
case refl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i : M
h : i ∈ 0
⊢ False
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_insert
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 a : M
⊢ i ∈ insert i a
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_mem_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 < exp log a + exp log a
Tactic:
rw [←two_mul]
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 < 2 * exp log a
Theorem: LO.FirstOrder.Arith.Model.log_mem_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 < 2 * exp log a
Tactic:
exact lt_two_mul_exponential_log h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_mem_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 = 0 * exp (log a + 1) + exp log a + (a - exp log a)
Tactic:
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 ⊧ₘ* 𝐈𝚺₁
a : M
h : 0 < a
⊢ a = exp log a + (a - exp log a)
Theorem: LO.FirstOrder.Arith.Model.log_mem_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 = exp log a + (a - exp log a)
Tactic:
exact Eq.symm <| add_tsub_self_of_le (exp_log_le_self h)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.succ_mem_iff_mem_div_two
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 a : M
⊢ i + 1 ∈ a ↔ i ∈ a / 2
Tactic:
simp [mem_iff_bit, Bit, LenBit.iff_rem, exp_succ, div_mul]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lt_length_of_mem
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 a : M
h : i ∈ a
⊢ i < ‖a‖
Tactic:
simpa [length_of_pos (pos_of_nonempty h), ←le_iff_lt_succ] using le_log_of_mem h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lt_exp_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 ⊧ₘ* 𝐈𝚺₁
a i : M
⊢ (∀ j ∈ a, j < i) → a < exp i
Tactic:
contrapose
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 i : M
⊢ ¬a < exp i → ¬∀ j ∈ a, j < i
Theorem: LO.FirstOrder.Arith.Model.lt_exp_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 ⊧ₘ* 𝐈𝚺₁
a i : M
⊢ ¬a < exp i → ¬∀ j ∈ a, j < i
Tactic:
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 ⊧ₘ* 𝐈𝚺₁
a i : M
⊢ exp i ≤ a → ∃ x ∈ a, i ≤ x
Theorem: LO.FirstOrder.Arith.Model.lt_exp_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 ⊧ₘ* 𝐈𝚺₁
a i : M
⊢ exp i ≤ a → ∃ x ∈ a, i ≤ x
Tactic:
intro (h : exp i ≤ 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 i : M
h : exp i ≤ a
⊢ ∃ x ∈ a, i ≤ x
Theorem: LO.FirstOrder.Arith.Model.lt_exp_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 ⊧ₘ* 𝐈𝚺₁
a i : M
h : exp i ≤ a
⊢ ∃ x ∈ a, i ≤ x
Tactic:
have pos : 0 < a := lt_of_lt_of_le (by simp) 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 ⊧ₘ* 𝐈𝚺₁
a i : M
h : exp i ≤ a
pos : 0 < a
⊢ ∃ x ∈ a, i ≤ x
Theorem: LO.FirstOrder.Arith.Model.lt_exp_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 ⊧ₘ* 𝐈𝚺₁
a i : M
h : exp i ≤ a
pos : 0 < a
⊢ ∃ x ∈ a, i ≤ x
Tactic:
exact ⟨log a, log_mem_of_pos pos, (exp_le_iff_le_log pos).mp h⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lt_exp_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 ⊧ₘ* 𝐈𝚺₁
a i : M
h : exp i ≤ a
⊢ 0 < exp i
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.bitSubset_defined
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
⊢ 𝚺₀-Relation fun x x_1 => x ⊆ x_1 via bitSubsetDef
Tactic:
intro v
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 2 → M
⊢ (fun v => (fun x x_1 => x ⊆ x_1) (v 0) (v 1)) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val bitSubsetDef)
Theorem: LO.FirstOrder.Arith.Model.bitSubset_defined
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 2 → M
⊢ (fun v => (fun x x_1 => x ⊆ x_1) (v 0) (v 1)) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val bitSubsetDef)
Tactic:
simp [bitSubsetDef]
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 2 → M
⊢ v 0 ⊆ v 1 ↔ ∀ x < v 0, x ∈ v 0 → x ∈ v 1
Theorem: LO.FirstOrder.Arith.Model.bitSubset_defined
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 2 → M
⊢ v 0 ⊆ v 1 ↔ ∀ x < v 0, x ∈ v 0 → x ∈ v 1
Tactic:
exact ⟨by intro h x _ hx; exact h hx, by intro h x hx; exact h x (lt_of_mem hx) hx⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.bitSubset_defined
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 2 → M
⊢ v 0 ⊆ v 1 → ∀ x < v 0, x ∈ v 0 → x ∈ v 1
Tactic:
intro h x _ hx
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 2 → M
h : v 0 ⊆ v 1
x : M
a✝ : x < v 0
hx : x ∈ v 0
⊢ x ∈ v 1
Theorem: LO.FirstOrder.Arith.Model.bitSubset_defined
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 2 → M
h : v 0 ⊆ v 1
x : M
a✝ : x < v 0
hx : x ∈ v 0
⊢ x ∈ v 1
Tactic:
exact h hx
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.bitSubset_defined
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 2 → M
⊢ (∀ x < v 0, x ∈ v 0 → x ∈ v 1) → v 0 ⊆ v 1
Tactic:
intro h x hx
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 2 → M
h : ∀ x < v 0, x ∈ v 0 → x ∈ v 1
x : M
hx : x ∈ v 0
⊢ x ∈ v 1
Theorem: LO.FirstOrder.Arith.Model.bitSubset_defined
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 2 → M
h : ∀ x < v 0, x ∈ v 0 → x ∈ v 1
x : M
hx : x ∈ v 0
⊢ x ∈ v 1
Tactic:
exact h x (lt_of_mem hx) hx
Proof state after:
no goals