internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.subset_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 b : M
⊢ a ⊆ b ↔ ∀ x ∈ a, x ∈ b
Tactic:
simp [HasSubset.Subset]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_exp_add_succ_sub_one
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 ∈ exp (i + j + 1) - 1
Tactic:
have : exp (i + j + 1) - 1 = (exp j - 1) * exp (i + 1) + exp i + (exp i - 1) := calc
  exp (i + j + 1) - 1 = exp j * exp (i + 1) - 1                             := by simp [exp_add, ←mul_assoc, mul_comm]
  _                   = exp j * exp (i + 1) - exp (i + 1) + exp (i + 1) - 1 := by rw [sub_add_self_of_le]; exact le_mul_of_pos_left (exp_pos j)
  _                   = (exp j - 1) * exp (i + 1) + exp (i + 1) - 1         := by simp [sub_mul]
  _                   = (exp j - 1) * exp (i + 1) + (exp i + exp i) - 1     := by simp [←two_mul, ←exp_succ i]
  _                   = (exp j - 1) * exp (i + 1) + (exp i + exp i - 1)     := by rw [add_tsub_assoc_of_le]; simp [←two_mul, ←pos_iff_one_le]
  _                   = (exp j - 1) * exp (i + 1) + exp i + (exp i - 1)     := by simp [add_assoc, add_tsub_assoc_of_le]
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
this : exp (i + j + 1) - 1 = (exp j - 1) * exp (i + 1) + exp i + (exp i - 1)
⊢ i ∈ exp (i + j + 1) - 1
Theorem: LO.FirstOrder.Arith.Model.mem_exp_add_succ_sub_one
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
this : exp (i + j + 1) - 1 = (exp j - 1) * exp (i + 1) + exp i + (exp i - 1)
⊢ i ∈ exp (i + j + 1) - 1
Tactic:
exact mem_iff_mul_exp_add_exp_add.mpr ⟨exp j - 1, exp i - 1, (tsub_lt_iff_left (by simp)).mpr $ by simp, this⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_exp_add_succ_sub_one
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
⊢ exp (i + j + 1) - 1 = exp j * exp (i + 1) - 1
Tactic:
simp [exp_add, ←mul_assoc, mul_comm]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_exp_add_succ_sub_one
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
⊢ exp j * exp (i + 1) - 1 = exp j * exp (i + 1) - exp (i + 1) + exp (i + 1) - 1
Tactic:
rw [sub_add_self_of_le]
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
⊢ exp (i + 1) ≤ exp j * exp (i + 1)
Theorem: LO.FirstOrder.Arith.Model.mem_exp_add_succ_sub_one
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
⊢ exp (i + 1) ≤ exp j * exp (i + 1)
Tactic:
exact le_mul_of_pos_left (exp_pos j)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_exp_add_succ_sub_one
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
⊢ exp j * exp (i + 1) - exp (i + 1) + exp (i + 1) - 1 = (exp j - 1) * exp (i + 1) + exp (i + 1) - 1
Tactic:
simp [sub_mul]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_exp_add_succ_sub_one
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
⊢ (exp j - 1) * exp (i + 1) + exp (i + 1) - 1 = (exp j - 1) * exp (i + 1) + (exp i + exp i) - 1
Tactic:
simp [←two_mul, ←exp_succ i]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_exp_add_succ_sub_one
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
⊢ (exp j - 1) * exp (i + 1) + (exp i + exp i) - 1 = (exp j - 1) * exp (i + 1) + (exp i + exp i - 1)
Tactic:
rw [add_tsub_assoc_of_le]
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 ⊧ₘ* 𝐈𝚺₁
i j : M
⊢ 1 ≤ exp i + exp i
Theorem: LO.FirstOrder.Arith.Model.mem_exp_add_succ_sub_one
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 ⊧ₘ* 𝐈𝚺₁
i j : M
⊢ 1 ≤ exp i + exp i
Tactic:
simp [←two_mul, ←pos_iff_one_le]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_exp_add_succ_sub_one
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
⊢ (exp j - 1) * exp (i + 1) + (exp i + exp i - 1) = (exp j - 1) * exp (i + 1) + exp i + (exp i - 1)
Tactic:
simp [add_assoc, add_tsub_assoc_of_le]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_exp_add_succ_sub_one
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
this : exp (i + j + 1) - 1 = (exp j - 1) * exp (i + 1) + exp i + (exp i - 1)
⊢ 1 ≤ exp i
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_exp_add_succ_sub_one
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
this : exp (i + j + 1) - 1 = (exp j - 1) * exp (i + 1) + exp i + (exp i - 1)
⊢ exp i < exp i + 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.le_under
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 < under a + 1
Tactic:
simp [under, show exp a - 1 + 1 = exp a from sub_add_self_of_le (by simp)]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.le_under
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
⊢ 1 ≤ exp a
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_under_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 ∈ under j ↔ i < j
Tactic:
constructor
Proof state after:
case mp
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 ∈ under j → i < j

case mpr
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 ∈ under j
Theorem: LO.FirstOrder.Arith.Model.mem_under_iff
Proof state before:
case mp
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 ∈ under j → i < j
Tactic:
intro h
Proof state after:
case mp
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 : i ∈ under j
⊢ i < j
Theorem: LO.FirstOrder.Arith.Model.mem_under_iff
Proof state before:
case mp
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 : i ∈ under j
⊢ i < j
Tactic:
have : exp i < exp j := calc
  exp i ≤ exp j - 1 := exp_le_of_mem h
  _     < exp j     := pred_lt_self_of_pos (exp_pos j)
Proof state after:
case mp
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 : i ∈ under j
this : exp i < exp j
⊢ i < j
Theorem: LO.FirstOrder.Arith.Model.mem_under_iff
Proof state before:
case mp
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 : i ∈ under j
this : exp i < exp j
⊢ i < j
Tactic:
exact exp_monotone.mp this
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_under_iff
Proof state before:
case mpr
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 ∈ under j
Tactic:
intro lt
Proof state after:
case mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i j : M
lt : i < j
⊢ i ∈ under j
Theorem: LO.FirstOrder.Arith.Model.mem_under_iff
Proof state before:
case mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i j : M
lt : i < j
⊢ i ∈ under j
Tactic:
have := lt_iff_succ_le.mp lt
Proof state after:
case mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i j : M
lt : i < j
this : i + 1 ≤ j
⊢ i ∈ under j
Theorem: LO.FirstOrder.Arith.Model.mem_under_iff
Proof state before:
case mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i j : M
lt : i < j
this : i + 1 ≤ j
⊢ i ∈ under j
Tactic:
let k := j - (i + 1)
Proof state after:
case mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i j : M
lt : i < j
this : i + 1 ≤ j
k : M := j - (i + 1)
⊢ i ∈ under j
Theorem: LO.FirstOrder.Arith.Model.mem_under_iff
Proof state before:
case mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i j : M
lt : i < j
this✝ : i + 1 ≤ j
k : M := j - (i + 1)
this : j = i + k + 1
⊢ i ∈ under j
Tactic:
rw [this]
Proof state after:
case mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i j : M
lt : i < j
this✝ : i + 1 ≤ j
k : M := j - (i + 1)
this : j = i + k + 1
⊢ i ∈ under (i + k + 1)
Theorem: LO.FirstOrder.Arith.Model.mem_under_iff
Proof state before:
case mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i j : M
lt : i < j
this✝ : i + 1 ≤ j
k : M := j - (i + 1)
this : j = i + k + 1
⊢ i ∈ under (i + k + 1)
Tactic:
exact mem_exp_add_succ_sub_one i k
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_under_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
lt : i < j
this : i + 1 ≤ j
k : M := j - (i + 1)
⊢ j = i + k + 1
Tactic:
simp [add_assoc, ←sub_sub, k]
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
lt : i < j
this : i + 1 ≤ j
k : M := j - (i + 1)
⊢ j = i + (j - i - 1 + 1)
Theorem: LO.FirstOrder.Arith.Model.mem_under_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
lt : i < j
this : i + 1 ≤ j
k : M := j - (i + 1)
⊢ j = i + (j - i - 1 + 1)
Tactic:
rw [sub_add_self_of_le, add_tsub_self_of_le]
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
lt : i < j
this : i + 1 ≤ j
k : M := j - (i + 1)
⊢ i ≤ j

M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i j : M
lt : i < j
this : i + 1 ≤ j
k : M := j - (i + 1)
⊢ 1 ≤ j - i
Theorem: LO.FirstOrder.Arith.Model.mem_under_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
lt : i < j
this : i + 1 ≤ j
k : M := j - (i + 1)
⊢ i ≤ j
Tactic:
exact le_of_lt lt
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_under_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
lt : i < j
this : i + 1 ≤ j
k : M := j - (i + 1)
⊢ 1 ≤ j - i
Tactic:
exact le_tsub_of_add_le_left this
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.not_mem_under_self
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 i
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.under_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 ⊧ₘ* 𝐈𝚺₁
x y : M
⊢ y = under x → y + 1 = exp x
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 ⊧ₘ* 𝐈𝚺₁
x : M
⊢ under x + 1 = exp x
Theorem: LO.FirstOrder.Arith.Model.under_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 ⊧ₘ* 𝐈𝚺₁
x : M
⊢ under x + 1 = exp x
Tactic:
simp [under, sub_add_self_of_le]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.under_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 ⊧ₘ* 𝐈𝚺₁
x y : M
⊢ y + 1 = exp x → y = under x
Tactic:
intro 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 ⊧ₘ* 𝐈𝚺₁
x y : M
h : y + 1 = exp x
⊢ y = under x
Theorem: LO.FirstOrder.Arith.Model.under_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 ⊧ₘ* 𝐈𝚺₁
x y : M
h : y + 1 = exp x
this : (fun x => x - 1) (y + 1) = (fun x => x - 1) (exp x)
⊢ y = under x
Tactic:
simp [under] at this ⊢
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
x y : M
h : y + 1 = exp x
this : y = exp x - 1
⊢ y = exp x - 1
Theorem: LO.FirstOrder.Arith.Model.under_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 ⊧ₘ* 𝐈𝚺₁
x y : M
h : y + 1 = exp x
this : y = exp x - 1
⊢ y = exp x - 1
Tactic:
exact this
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.under_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₁ under via underDef
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 1) → M
⊢ (fun v => v 0 = (fun v => under (v 0)) fun x => v x.succ) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val underDef)
Theorem: LO.FirstOrder.Arith.Model.under_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 1) → M
⊢ (fun v => v 0 = (fun v => under (v 0)) fun x => v x.succ) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val underDef)
Tactic:
simp [underDef, under_graph]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.eq_zero_of_subset_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 ⊧ₘ* 𝐈𝚺₁
a : M
⊢ a ⊆ 0 → a = 0
Tactic:
intro 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 : M
h : a ⊆ 0
⊢ a = 0
Theorem: LO.FirstOrder.Arith.Model.eq_zero_of_subset_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 ⊧ₘ* 𝐈𝚺₁
a : M
h : a ⊆ 0
⊢ a = 0
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 : a ⊆ 0
A : ¬a = 0
⊢ False
Theorem: LO.FirstOrder.Arith.Model.eq_zero_of_subset_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 ⊧ₘ* 𝐈𝚺₁
a : M
h : a ⊆ 0
A : ¬a = 0
⊢ False
Tactic:
have : log a ∈ (0 : M) := h (log_mem_of_pos (pos_iff_ne_zero.mpr 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 : a ⊆ 0
A : ¬a = 0
this : log a ∈ 0
⊢ False
Theorem: LO.FirstOrder.Arith.Model.eq_zero_of_subset_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 ⊧ₘ* 𝐈𝚺₁
a : M
h : a ⊆ 0
A : ¬a = 0
this : log a ∈ 0
⊢ False
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.subset_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 ⊧ₘ* 𝐈𝚺₁
a b : M
⊢ a ⊆ b → a / 2 ⊆ b / 2
Tactic:
intro ss i 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 ⊧ₘ* 𝐈𝚺₁
a b : M
ss : a ⊆ b
i : M
hi : i ∈ a / 2
⊢ i ∈ b / 2
Theorem: LO.FirstOrder.Arith.Model.subset_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 ⊧ₘ* 𝐈𝚺₁
a b : M
ss : a ⊆ b
i : M
hi : i ∈ a / 2
⊢ i ∈ b / 2
Tactic:
have : i + 1 ∈ a := succ_mem_iff_mem_div_two.mpr 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 ⊧ₘ* 𝐈𝚺₁
a b : M
ss : a ⊆ b
i : M
hi : i ∈ a / 2
this : i + 1 ∈ a
⊢ i ∈ b / 2
Theorem: LO.FirstOrder.Arith.Model.subset_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 ⊧ₘ* 𝐈𝚺₁
a b : M
ss : a ⊆ b
i : M
hi : i ∈ a / 2
this : i + 1 ∈ a
⊢ i ∈ b / 2
Tactic:
exact succ_mem_iff_mem_div_two.mp <| ss this
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.zero_mem_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 : M
⊢ 0 ∉ a ↔ 2 ∣ a
Tactic:
simp [mem_iff_bit, Bit, LenBit]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.zero_not_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 ⊧ₘ* 𝐈𝚺₁
a : M
⊢ 0 ∉ 2 * a
Tactic:
simp [mem_iff_bit, Bit, LenBit]
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 ⊧ₘ* 𝐈𝚺₁
a b : M
h : a ⊆ b
⊢ a ≤ b
Tactic:
induction b using hierarchy_polynomial_induction_oRing_pi₁ generalizing a
Proof state after:
case hP
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
⊢ 𝚷₁-Predicate fun {b} => ∀ {a : M}, a ⊆ b → a ≤ b

case zero
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a : M
h : a ⊆ 0
⊢ a ≤ 0

case even
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
x✝ : M
a✝¹ : x✝ > 0
a✝ : ∀ {a : M}, a ⊆ x✝ → a ≤ x✝
a : M
h : a ⊆ 2 * x✝
⊢ a ≤ 2 * x✝

case odd
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
x✝ : M
a✝ : ∀ {a : M}, a ⊆ x✝ → a ≤ x✝
a : M
h : a ⊆ 2 * x✝ + 1
⊢ a ≤ 2 * x✝ + 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 ⊧ₘ* 𝐈𝚺₁
a : M
h : a ⊆ 0
⊢ a ≤ 0
Tactic:
case zero =>
  simp [eq_zero_of_subset_zero 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
a✝ : b > 0
IH : ∀ {a : M}, a ⊆ b → a ≤ b
a : M
h : a ⊆ 2 * b
⊢ a ≤ 2 * b
Tactic:
case even b _ IH =>
  have IH : a / 2 ≤ b := IH (by simpa using subset_div_two h)
  have : 2 * (a / 2) = a :=
    mul_div_self_of_dvd.mpr (zero_mem_iff.mp $ by intro ha; have : 0 ∈ 2 * b := h ha; simp_all)
  simpa [this] using mul_le_mul_left (a := 2) 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 + 1
Tactic:
case odd b IH =>
  have IH : a / 2 ≤ b := IH (by simpa [div_mul_add' b 2 one_lt_two] using subset_div_two h)
  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:
case hP
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
⊢ 𝚷₁-Predicate fun {b} => ∀ {a : M}, a ⊆ b → a ≤ b
Tactic:
definability
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 ⊧ₘ* 𝐈𝚺₁
a : M
h : a ⊆ 0
⊢ a ≤ 0
Tactic:
simp [eq_zero_of_subset_zero 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
a✝ : b > 0
IH : ∀ {a : M}, a ⊆ b → a ≤ b
a : M
h : a ⊆ 2 * b
⊢ a ≤ 2 * b
Tactic:
have IH : a / 2 ≤ b := IH (by simpa 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
a✝ : b > 0
IH✝ : ∀ {a : M}, a ⊆ b → a ≤ b
a : M
h : a ⊆ 2 * b
IH : a / 2 ≤ b
⊢ a ≤ 2 * b
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
a✝ : b > 0
IH✝ : ∀ {a : M}, a ⊆ b → a ≤ b
a : M
h : a ⊆ 2 * b
IH : a / 2 ≤ b
⊢ a ≤ 2 * b
Tactic:
have : 2 * (a / 2) = a :=
  mul_div_self_of_dvd.mpr (zero_mem_iff.mp $ by intro ha; have : 0 ∈ 2 * b := h ha; simp_all)
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
a✝ : b > 0
IH✝ : ∀ {a : M}, a ⊆ b → a ≤ b
a : M
h : a ⊆ 2 * b
IH : a / 2 ≤ b
this : 2 * (a / 2) = a
⊢ a ≤ 2 * b
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
a✝ : b > 0
IH✝ : ∀ {a : M}, a ⊆ b → a ≤ b
a : M
h : a ⊆ 2 * b
IH : a / 2 ≤ b
this : 2 * (a / 2) = a
⊢ a ≤ 2 * b
Tactic:
simpa [this] using mul_le_mul_left (a := 2) 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
a✝ : b > 0
IH : ∀ {a : M}, a ⊆ b → a ≤ b
a : M
h : a ⊆ 2 * b
⊢ a / 2 ⊆ b
Tactic:
simpa 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
a✝ : b > 0
IH✝ : ∀ {a : M}, a ⊆ b → a ≤ b
a : M
h : a ⊆ 2 * b
IH : a / 2 ≤ b
⊢ 0 ∉ a
Tactic:
intro ha
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
a✝ : b > 0
IH✝ : ∀ {a : M}, a ⊆ b → a ≤ b
a : M
h : a ⊆ 2 * b
IH : a / 2 ≤ b
ha : 0 ∈ a
⊢ False
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
a✝ : b > 0
IH✝ : ∀ {a : M}, a ⊆ b → a ≤ b
a : M
h : a ⊆ 2 * b
IH : a / 2 ≤ b
ha : 0 ∈ a
⊢ False
Tactic:
have : 0 ∈ 2 * b := h ha
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
a✝ : b > 0
IH✝ : ∀ {a : M}, a ⊆ b → a ≤ b
a : M
h : a ⊆ 2 * b
IH : a / 2 ≤ b
ha : 0 ∈ a
this : 0 ∈ 2 * b
⊢ False
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
a✝ : b > 0
IH✝ : ∀ {a : M}, a ⊆ b → a ≤ b
a : M
h : a ⊆ 2 * b
IH : a / 2 ≤ b
ha : 0 ∈ a
this : 0 ∈ 2 * b
⊢ False
Tactic:
simp_all
Proof state after:
no goals