internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.fbit_defined
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 ⊧ₘ* 𝐈𝚫₀
v : Fin (Nat.succ 2) → M
⊢ (∃ x ≤ v 1, x = bexp (v 1) (v 2) ∧ ∃ x_1 ≤ v 1, x_1 = v 1 / x ∧ v 0 = x_1 % 2) → v 0 = v 1 / bexp (v 1) (v 2) % 2
Tactic:
rintro ⟨_, _, rfl, _, _, rfl, h⟩
Proof state after:
case mpr.intro.intro.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 ⊧ₘ* 𝐈𝚫₀
v : Fin (Nat.succ 2) → M
left✝¹ : bexp (v 1) (v 2) ≤ v 1
left✝ : v 1 / bexp (v 1) (v 2) ≤ v 1
h : v 0 = v 1 / bexp (v 1) (v 2) % 2
⊢ v 0 = v 1 / bexp (v 1) (v 2) % 2
Theorem: LO.FirstOrder.Arith.Model.fbit_defined
Proof state before:
case mpr.intro.intro.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 ⊧ₘ* 𝐈𝚫₀
v : Fin (Nat.succ 2) → M
left✝¹ : bexp (v 1) (v 2) ≤ v 1
left✝ : v 1 / bexp (v 1) (v 2) ≤ v 1
h : v 0 = v 1 / bexp (v 1) (v 2) % 2
⊢ v 0 = v 1 / bexp (v 1) (v 2) % 2
Tactic:
exact h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.fbit_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
⊢ fbit 0 i = 0
Tactic:
simp [fbit]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.fbit_mul_two_mul
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
⊢ fbit (2 * a) (i + 1) = fbit a i
Tactic:
simp [fbit, bexp_two_mul_succ, div_cancel_left]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.fbit_mul_two_add_one_mul
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
⊢ fbit (2 * a + 1) (i + 1) = fbit a i
Tactic:
simp [fbit, bexp_two_mul_add_one_succ, div_cancel_left, div_mul]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.fbit_two_mul_zero_eq_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
⊢ fbit (2 * a) 0 = 0
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 ⊧ₘ* 𝐈𝚫₀
⊢ fbit (2 * 0) 0 = 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
⊢ fbit (2 * a) 0 = 0
Theorem: LO.FirstOrder.Arith.Model.fbit_two_mul_zero_eq_zero
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 ⊧ₘ* 𝐈𝚫₀
⊢ fbit (2 * 0) 0 = 0
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.fbit_two_mul_zero_eq_zero
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
⊢ fbit (2 * a) 0 = 0
Tactic:
have : bexp (2 * a) 0 = 1 := bexp_eq_of_exp (by simp [pos]) (by 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 ⊧ₘ* 𝐈𝚫₀
a : M
pos : 0 < a
this : bexp (2 * a) 0 = 1
⊢ fbit (2 * a) 0 = 0
Theorem: LO.FirstOrder.Arith.Model.fbit_two_mul_zero_eq_zero
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
this : bexp (2 * a) 0 = 1
⊢ fbit (2 * a) 0 = 0
Tactic:
simp [fbit, this]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.fbit_two_mul_zero_eq_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
pos : 0 < a
⊢ 0 < ‖2 * a‖
Tactic:
simp [pos]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.fbit_two_mul_zero_eq_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
pos : 0 < a
⊢ Exponential 0 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.fbit_two_mul_add_one_zero_eq_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 ⊧ₘ* 𝐈𝚫₀
a : M
⊢ fbit (2 * a + 1) 0 = 1
Tactic:
simp [fbit, one_lt_two]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.exp_log_le_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 ⊧ₘ* 𝐈𝚺₁
a : M
pos : 0 < a
⊢ exp log a ≤ a
Tactic:
rcases log_pos pos with ⟨_, _, H, _⟩
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 ⊧ₘ* 𝐈𝚺₁
a : M
pos : 0 < a
w✝ : M
left✝ : w✝ ≤ a
H : Exponential (log a) w✝
right✝ : a < 2 * w✝
⊢ exp log a ≤ a
Theorem: LO.FirstOrder.Arith.Model.exp_log_le_self
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 ⊧ₘ* 𝐈𝚺₁
a : M
pos : 0 < a
w✝ : M
left✝ : w✝ ≤ a
H : Exponential (log a) w✝
right✝ : a < 2 * w✝
⊢ exp log a ≤ a
Tactic:
rcases H.uniq (exponential_exp (log a))
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 ⊧ₘ* 𝐈𝚺₁
a : M
pos : 0 < a
left✝ : exp log a ≤ a
H : Exponential (log a) (exp log a)
right✝ : a < 2 * exp log a
⊢ exp log a ≤ a
Theorem: LO.FirstOrder.Arith.Model.exp_log_le_self
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 ⊧ₘ* 𝐈𝚺₁
a : M
pos : 0 < a
left✝ : exp log a ≤ a
H : Exponential (log a) (exp log a)
right✝ : a < 2 * exp log a
⊢ exp log a ≤ a
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lt_two_mul_exponential_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 : M
pos : 0 < a
⊢ a < 2 * exp log a
Tactic:
rcases log_pos pos with ⟨_, _, H, _⟩
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 ⊧ₘ* 𝐈𝚺₁
a : M
pos : 0 < a
w✝ : M
left✝ : w✝ ≤ a
H : Exponential (log a) w✝
right✝ : a < 2 * w✝
⊢ a < 2 * exp log a
Theorem: LO.FirstOrder.Arith.Model.lt_two_mul_exponential_log
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 ⊧ₘ* 𝐈𝚺₁
a : M
pos : 0 < a
w✝ : M
left✝ : w✝ ≤ a
H : Exponential (log a) w✝
right✝ : a < 2 * w✝
⊢ a < 2 * exp log a
Tactic:
rcases H.uniq (exponential_exp (log a))
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 ⊧ₘ* 𝐈𝚺₁
a : M
pos : 0 < a
left✝ : exp log a ≤ a
H : Exponential (log a) (exp log a)
right✝ : a < 2 * exp log a
⊢ a < 2 * exp log a
Theorem: LO.FirstOrder.Arith.Model.lt_two_mul_exponential_log
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 ⊧ₘ* 𝐈𝚺₁
a : M
pos : 0 < a
left✝ : exp log a ≤ a
H : Exponential (log a) (exp log a)
right✝ : a < 2 * exp log a
⊢ a < 2 * exp log a
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.length_exponential
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
⊢ ‖exp a‖ = a + 1
Tactic:
simp [length_of_pos (exp_pos a)]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_mul_exp_add_of_lt
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 < a
i : M
hb : b < exp i
⊢ log (a * exp i + b) = log a + i
Tactic:
simp [log_mul_pow2_add_of_lt pos (exp_pow2 i) hb]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_mul_exp
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
pos : 0 < a
i : M
⊢ log (a * exp i) = log a + i
Tactic:
simp [log_mul_pow2 pos (exp_pow2 i)]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.length_mul_exp_add_of_lt
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 < a
i : M
hb : b < exp i
⊢ ‖a * exp i + b‖ = ‖a‖ + i
Tactic:
simp [length_mul_pow2_add_of_lt pos (exp_pow2 i) hb]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.length_mul_exp
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
pos : 0 < a
i : M
⊢ ‖a * exp i‖ = ‖a‖ + i
Tactic:
simp [length_mul_pow2 pos (exp_pow2 i)]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.exp_le_iff_le_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 ⊧ₘ* 𝐈𝚺₁
i a : M
pos : 0 < a
⊢ exp i ≤ a → i ≤ log a
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 ⊧ₘ* 𝐈𝚺₁
i a : M
pos : 0 < a
h : exp i ≤ a
⊢ i ≤ log a
Theorem: LO.FirstOrder.Arith.Model.exp_le_iff_le_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 ⊧ₘ* 𝐈𝚺₁
i a : M
pos : 0 < a
h : exp i ≤ a
⊢ i ≤ log a
Tactic:
simpa using log_monotone h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.seqCons_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 ⊧ₘ* 𝐈𝚺₁
x y s t : M
hxy : x ≤ y
hst : s ≤ t
⊢ s ⁀' x ≤ t + exp ((2 * t + y + 1) ^ 2)
Tactic:
have : s ⁀' x ≤ t + exp ⟪2 * t, y⟫ := by
  simp [seqCons]; exact insert_le_of_le_of_le (pair_le_pair (le_trans (lh_bound s) (by simp [hst])) hxy) hst
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 s t : M
hxy : x ≤ y
hst : s ≤ t
this : s ⁀' x ≤ t + exp ⟪2 * t, y⟫
⊢ s ⁀' x ≤ t + exp ((2 * t + y + 1) ^ 2)
Theorem: LO.FirstOrder.Arith.Model.seqCons_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 ⊧ₘ* 𝐈𝚺₁
x y s t : M
hxy : x ≤ y
hst : s ≤ t
this : s ⁀' x ≤ t + exp ⟪2 * t, y⟫
⊢ s ⁀' x ≤ t + exp ((2 * t + y + 1) ^ 2)
Tactic:
exact le_trans this (by simp)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.seqCons_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 ⊧ₘ* 𝐈𝚺₁
x y s t : M
hxy : x ≤ y
hst : s ≤ t
⊢ s ⁀' x ≤ t + exp ⟪2 * t, y⟫
Tactic:
simp [seqCons]
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 s t : M
hxy : x ≤ y
hst : s ≤ t
⊢ insert ⟪lh s, x⟫ s ≤ t + exp ⟪2 * t, y⟫
Theorem: LO.FirstOrder.Arith.Model.seqCons_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 ⊧ₘ* 𝐈𝚺₁
x y s t : M
hxy : x ≤ y
hst : s ≤ t
⊢ insert ⟪lh s, x⟫ s ≤ t + exp ⟪2 * t, y⟫
Tactic:
exact insert_le_of_le_of_le (pair_le_pair (le_trans (lh_bound s) (by simp [hst])) hxy) hst
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.seqCons_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 ⊧ₘ* 𝐈𝚺₁
x y s t : M
hxy : x ≤ y
hst : s ≤ t
⊢ 2 * s ≤ 2 * t
Tactic:
simp [hst]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.seqCons_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 ⊧ₘ* 𝐈𝚺₁
x y s t : M
hxy : x ≤ y
hst : s ≤ t
this : s ⁀' x ≤ t + exp ⟪2 * t, y⟫
⊢ t + exp ⟪2 * t, y⟫ ≤ t + exp ((2 * t + y + 1) ^ 2)
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.seqProduct_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 ⊧ₘ* 𝐈𝚺₁
s a : M
⊢ ∃! t, ∀ (x : M), x ∈ t ↔ ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
Tactic:
have : 𝚺₁-Predicate fun x ↦ ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u := by definability
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s a : M
this : 𝚺₁-Predicate fun x => ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
⊢ ∃! t, ∀ (x : M), x ∈ t ↔ ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
Theorem: LO.FirstOrder.Arith.Model.seqProduct_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 ⊧ₘ* 𝐈𝚺₁
s a : M
this : 𝚺₁-Predicate fun x => ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
⊢ ∃! t, ∀ (x : M), x ∈ t ↔ ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
Tactic:
exact finite_comprehension₁! this ⟨log s + exp ((2 * log s + log a + 1)^2) + 1, by
  rintro x ⟨v, hv, u, hu, rfl⟩
  exact lt_succ_iff_le.mpr <| seqCons_le (le_log_of_mem hu) (le_log_of_mem hv)⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.seqProduct_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 ⊧ₘ* 𝐈𝚺₁
s a : M
⊢ 𝚺₁-Predicate fun x => ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
Tactic:
definability
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.seqProduct_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 ⊧ₘ* 𝐈𝚺₁
s a : M
this : 𝚺₁-Predicate fun x => ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
⊢ ∀ (i : M), (∃ v ∈ s, ∃ u ∈ a, i = v ⁀' u) → i < log s + exp ((2 * log s + log a + 1) ^ 2) + 1
Tactic:
rintro x ⟨v, hv, u, hu, rfl⟩
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 ⊧ₘ* 𝐈𝚺₁
s a : M
this : 𝚺₁-Predicate fun x => ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
v : M
hv : v ∈ s
u : M
hu : u ∈ a
⊢ v ⁀' u < log s + exp ((2 * log s + log a + 1) ^ 2) + 1
Theorem: LO.FirstOrder.Arith.Model.seqProduct_exists_unique
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 ⊧ₘ* 𝐈𝚺₁
s a : M
this : 𝚺₁-Predicate fun x => ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
v : M
hv : v ∈ s
u : M
hu : u ∈ a
⊢ v ⁀' u < log s + exp ((2 * log s + log a + 1) ^ 2) + 1
Tactic:
exact lt_succ_iff_le.mpr <| seqCons_le (le_log_of_mem hu) (le_log_of_mem hv)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_seqProduct_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 ⊧ₘ* 𝐈𝚺₁
u v a s : M
Hv : Seq v
Hs : ∀ w ∈ s, Seq w
⊢ v ⁀' u ∈ s ×ˢ a → v ∈ s ∧ u ∈ a
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 ⊧ₘ* 𝐈𝚺₁
u v a s : M
Hv : Seq v
Hs : ∀ w ∈ s, Seq w
h : v ⁀' u ∈ s ×ˢ a
⊢ v ∈ s ∧ u ∈ a
Theorem: LO.FirstOrder.Arith.Model.mem_seqProduct_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 ⊧ₘ* 𝐈𝚺₁
u v a s : M
Hv : Seq v
Hs : ∀ w ∈ s, Seq w
h : v ⁀' u ∈ s ×ˢ a
⊢ v ∈ s ∧ u ∈ a
Tactic:
rcases mem_seqProduct_iff.mp h with ⟨v', hv', u', hu', e⟩
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 ⊧ₘ* 𝐈𝚺₁
u v a s : M
Hv : Seq v
Hs : ∀ w ∈ s, Seq w
h : v ⁀' u ∈ s ×ˢ a
v' : M
hv' : v' ∈ s
u' : M
hu' : u' ∈ a
e : v ⁀' u = v' ⁀' u'
⊢ v ∈ s ∧ u ∈ a
Theorem: LO.FirstOrder.Arith.Model.mem_seqProduct_iff'
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 ⊧ₘ* 𝐈𝚺₁
u v a s : M
Hv : Seq v
Hs : ∀ w ∈ s, Seq w
h : v ⁀' u ∈ s ×ˢ a
v' : M
hv' : v' ∈ s
u' : M
hu' : u' ∈ a
e : v ⁀' u = v' ⁀' u'
⊢ v ∈ s ∧ u ∈ a
Tactic:
have : u = u' ∧ v = v' := by simpa [Hv, Hs v' hv'] using e
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 ⊧ₘ* 𝐈𝚺₁
u v a s : M
Hv : Seq v
Hs : ∀ w ∈ s, Seq w
h : v ⁀' u ∈ s ×ˢ a
v' : M
hv' : v' ∈ s
u' : M
hu' : u' ∈ a
e : v ⁀' u = v' ⁀' u'
this : u = u' ∧ v = v'
⊢ v ∈ s ∧ u ∈ a
Theorem: LO.FirstOrder.Arith.Model.mem_seqProduct_iff'
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 ⊧ₘ* 𝐈𝚺₁
u v a s : M
Hv : Seq v
Hs : ∀ w ∈ s, Seq w
h : v ⁀' u ∈ s ×ˢ a
v' : M
hv' : v' ∈ s
u' : M
hu' : u' ∈ a
e : v ⁀' u = v' ⁀' u'
this : u = u' ∧ v = v'
⊢ v ∈ s ∧ u ∈ a
Tactic:
rcases this with ⟨rfl, rfl⟩
Proof state after:
case intro.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 ⊧ₘ* 𝐈𝚺₁
u v a s : M
Hv : Seq v
Hs : ∀ w ∈ s, Seq w
h : v ⁀' u ∈ s ×ˢ a
hu' : u ∈ a
hv' : v ∈ s
e : v ⁀' u = v ⁀' u
⊢ v ∈ s ∧ u ∈ a
Theorem: LO.FirstOrder.Arith.Model.mem_seqProduct_iff'
Proof state before:
case intro.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 ⊧ₘ* 𝐈𝚺₁
u v a s : M
Hv : Seq v
Hs : ∀ w ∈ s, Seq w
h : v ⁀' u ∈ s ×ˢ a
hu' : u ∈ a
hv' : v ∈ s
e : v ⁀' u = v ⁀' u
⊢ v ∈ s ∧ u ∈ a
Tactic:
constructor <;> assumption
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_seqProduct_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 ⊧ₘ* 𝐈𝚺₁
u v a s : M
Hv : Seq v
Hs : ∀ w ∈ s, Seq w
h : v ⁀' u ∈ s ×ˢ a
v' : M
hv' : v' ∈ s
u' : M
hu' : u' ∈ a
e : v ⁀' u = v' ⁀' u'
⊢ u = u' ∧ v = v'
Tactic:
simpa [Hv, Hs v' hv'] using e
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_seqProduct_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 ⊧ₘ* 𝐈𝚺₁
u v a s : M
Hv : Seq v
Hs : ∀ w ∈ s, Seq w
⊢ v ∈ s ∧ u ∈ a → v ⁀' u ∈ s ×ˢ a
Tactic:
rintro ⟨hv, hu⟩
Proof state after:
case intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u v a s : M
Hv : Seq v
Hs : ∀ w ∈ s, Seq w
hv : v ∈ s
hu : u ∈ a
⊢ v ⁀' u ∈ s ×ˢ a
Theorem: LO.FirstOrder.Arith.Model.mem_seqProduct_iff'
Proof state before:
case intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u v a s : M
Hv : Seq v
Hs : ∀ w ∈ s, Seq w
hv : v ∈ s
hu : u ∈ a
⊢ v ⁀' u ∈ s ×ˢ a
Tactic:
exact mem_seqProduct_iff.mpr ⟨v, hv, u, hu, rfl⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_seqProduct_bound
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 s a : M
h : x ∈ s ×ˢ a
⊢ x ≤ s + exp ((2 * s + a + 1) ^ 2)
Tactic:
rcases mem_seqProduct_iff.mp h with ⟨v, hv, u, hu, rfl⟩
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 ⊧ₘ* 𝐈𝚺₁
s a v : M
hv : v ∈ s
u : M
hu : u ∈ a
h : v ⁀' u ∈ s ×ˢ a
⊢ v ⁀' u ≤ s + exp ((2 * s + a + 1) ^ 2)
Theorem: LO.FirstOrder.Arith.Model.mem_seqProduct_bound
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 ⊧ₘ* 𝐈𝚺₁
s a v : M
hv : v ∈ s
u : M
hu : u ∈ a
h : v ⁀' u ∈ s ×ˢ a
⊢ v ⁀' u ≤ s + exp ((2 * s + a + 1) ^ 2)
Tactic:
exact seqCons_le (le_of_lt <| lt_of_mem hu) (le_of_lt <| lt_of_mem hv)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.seqProduct_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 ⊧ₘ* 𝐈𝚺₁
t s a : M
⊢ t = s ×ˢ a → ∃ e, e = exp ((2 * s + a + 1) ^ 2) ∧ ∀ x ≤ t + s + e, x ∈ t ↔ ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
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 ⊧ₘ* 𝐈𝚺₁
s a : M
⊢ ∃ e, e = exp ((2 * s + a + 1) ^ 2) ∧ ∀ x ≤ (s ×ˢ a) + s + e, x ∈ s ×ˢ a ↔ ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
Theorem: LO.FirstOrder.Arith.Model.seqProduct_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 ⊧ₘ* 𝐈𝚺₁
s a : M
⊢ ∃ e, e = exp ((2 * s + a + 1) ^ 2) ∧ ∀ x ≤ (s ×ˢ a) + s + e, x ∈ s ×ˢ a ↔ ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
Tactic:
exact ⟨exp ((2 * s + a + 1)^2), rfl, by intro x _; simp [mem_seqProduct_iff]⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.seqProduct_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 ⊧ₘ* 𝐈𝚺₁
s a : M
⊢ ∀ x ≤ (s ×ˢ a) + s + exp ((2 * s + a + 1) ^ 2), x ∈ s ×ˢ a ↔ ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
Tactic:
intro x _
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s a x : M
a✝ : x ≤ (s ×ˢ a) + s + exp ((2 * s + a + 1) ^ 2)
⊢ x ∈ s ×ˢ a ↔ ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
Theorem: LO.FirstOrder.Arith.Model.seqProduct_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 ⊧ₘ* 𝐈𝚺₁
s a x : M
a✝ : x ≤ (s ×ˢ a) + s + exp ((2 * s + a + 1) ^ 2)
⊢ x ∈ s ×ˢ a ↔ ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
Tactic:
simp [mem_seqProduct_iff]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.seqProduct_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 ⊧ₘ* 𝐈𝚺₁
t s a : M
⊢ (∃ e, e = exp ((2 * s + a + 1) ^ 2) ∧ ∀ x ≤ t + s + e, x ∈ t ↔ ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u) → t = s ×ˢ a
Tactic:
rintro ⟨_, rfl, h⟩
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 ⊧ₘ* 𝐈𝚺₁
t s a : M
h : ∀ x ≤ t + s + exp ((2 * s + a + 1) ^ 2), x ∈ t ↔ ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
⊢ t = s ×ˢ a
Theorem: LO.FirstOrder.Arith.Model.seqProduct_graph
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 ⊧ₘ* 𝐈𝚺₁
t s a : M
h : ∀ x ≤ t + s + exp ((2 * s + a + 1) ^ 2), x ∈ t ↔ ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
⊢ t = s ×ˢ a
Tactic:
apply mem_ext
Proof state after:
case intro.intro.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
t s a : M
h : ∀ x ≤ t + s + exp ((2 * s + a + 1) ^ 2), x ∈ t ↔ ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
⊢ ∀ (i : M), i ∈ t ↔ i ∈ s ×ˢ a
Theorem: LO.FirstOrder.Arith.Model.seqProduct_graph
Proof state before:
case intro.intro.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
t s a : M
h : ∀ x ≤ t + s + exp ((2 * s + a + 1) ^ 2), x ∈ t ↔ ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
⊢ ∀ (i : M), i ∈ t ↔ i ∈ s ×ˢ a
Tactic:
intro x
Proof state after:
case intro.intro.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
t s a : M
h : ∀ x ≤ t + s + exp ((2 * s + a + 1) ^ 2), x ∈ t ↔ ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
x : M
⊢ x ∈ t ↔ x ∈ s ×ˢ a
Theorem: LO.FirstOrder.Arith.Model.seqProduct_graph
Proof state before:
case intro.intro.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
t s a : M
h : ∀ x ≤ t + s + exp ((2 * s + a + 1) ^ 2), x ∈ t ↔ ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
x : M
⊢ x ∈ t ↔ x ∈ s ×ˢ a
Tactic:
constructor
Proof state after:
case intro.intro.h.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
t s a : M
h : ∀ x ≤ t + s + exp ((2 * s + a + 1) ^ 2), x ∈ t ↔ ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
x : M
⊢ x ∈ t → x ∈ s ×ˢ a

case intro.intro.h.mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
t s a : M
h : ∀ x ≤ t + s + exp ((2 * s + a + 1) ^ 2), x ∈ t ↔ ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
x : M
⊢ x ∈ s ×ˢ a → x ∈ t