internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.bexp_exists_unique
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 ⊧ₘ* 𝐈𝚫₀
a x : M
hx : ¬x < ‖a‖
⊢ ∃! y, (x < ‖a‖ → Exponential x y) ∧ (‖a‖ ≤ x → y = 0)
Tactic:
simp [hx, show ‖a‖ ≤ x from by simpa using hx]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.bexp_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 ⊧ₘ* 𝐈𝚫₀
a x : M
hx : ¬x < ‖a‖
⊢ ‖a‖ ≤ x
Tactic:
simpa using hx
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.bexp_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 ⊧ₘ* 𝐈𝚫₀
x : M
⊢ ‖0‖ ≤ x
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.exp_bexp_of_lt_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 x : M
⊢ Exponential x (bexp a x) → x < ‖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 ⊧ₘ* 𝐈𝚫₀
a x : M
h : Exponential x (bexp a x)
⊢ x < ‖a‖
Theorem: LO.FirstOrder.Arith.Model.exp_bexp_of_lt_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 x : M
h : Exponential x (bexp a x)
⊢ x < ‖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 x : M
h : Exponential x (bexp a x)
A : ¬x < ‖a‖
⊢ False
Theorem: LO.FirstOrder.Arith.Model.exp_bexp_of_lt_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 x : M
h : Exponential x (bexp a x)
A : ¬x < ‖a‖
⊢ False
Tactic:
have : bexp a x = 0 := bexp_eq_zero_of_le (not_lt.mp 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 x : M
h : Exponential x (bexp a x)
A : ¬x < ‖a‖
this : bexp a x = 0
⊢ False
Theorem: LO.FirstOrder.Arith.Model.exp_bexp_of_lt_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 x : M
h : Exponential x (bexp a x)
A : ¬x < ‖a‖
this : bexp a x = 0
⊢ False
Tactic:
simp [this] at 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 x : M
A : ¬x < ‖a‖
this : bexp a x = 0
h : Exponential x 0
⊢ False
Theorem: LO.FirstOrder.Arith.Model.exp_bexp_of_lt_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 x : M
A : ¬x < ‖a‖
this : bexp a x = 0
h : Exponential x 0
⊢ False
Tactic:
have := h.range_pos
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 x : M
A : ¬x < ‖a‖
this✝ : bexp a x = 0
h : Exponential x 0
this : 0 < 0
⊢ False
Theorem: LO.FirstOrder.Arith.Model.exp_bexp_of_lt_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 x : M
A : ¬x < ‖a‖
this✝ : bexp a x = 0
h : Exponential x 0
this : 0 < 0
⊢ False
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.bexp_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 x : M
⊢ bexp a x ≤ a
Tactic:
rcases show x < ‖a‖ ∨ ‖a‖ ≤ x from lt_or_ge _ _ with (lt | le)
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 ⊧ₘ* 𝐈𝚫₀
a x : M
lt : x < ‖a‖
⊢ bexp a x ≤ a

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a x : M
le : ‖a‖ ≤ x
⊢ bexp a x ≤ a
Theorem: LO.FirstOrder.Arith.Model.bexp_le_self
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 ⊧ₘ* 𝐈𝚫₀
a x : M
lt : x < ‖a‖
⊢ bexp a x ≤ a
Tactic:
have : 0 < a := pos_of_lt_length lt
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 ⊧ₘ* 𝐈𝚫₀
a x : M
lt : x < ‖a‖
this : 0 < a
⊢ bexp a x ≤ a
Theorem: LO.FirstOrder.Arith.Model.bexp_le_self
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 ⊧ₘ* 𝐈𝚫₀
a x : M
lt : x < ‖a‖
this : 0 < a
⊢ bexp a x ≤ a
Tactic:
exact (le_iff_le_log_of_exp (exp_bexp_of_lt lt) this).mpr (le_log_of_lt_length lt)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.bexp_le_self
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 x : M
le : ‖a‖ ≤ x
⊢ bexp a x ≤ a
Tactic:
simp [bexp_eq_zero_of_le le]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.bexp_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 ⊧ₘ* 𝐈𝚫₀
y a x : M
⊢ y = bexp a x → ∃ l ≤ a, l = ‖a‖ ∧ (x < l → Exponential x y) ∧ (l ≤ x → y = 0)
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 ⊧ₘ* 𝐈𝚫₀
a x : M
⊢ ∃ l ≤ a, l = ‖a‖ ∧ (x < l → Exponential x (bexp a x)) ∧ (l ≤ x → bexp a x = 0)
Theorem: LO.FirstOrder.Arith.Model.bexp_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 ⊧ₘ* 𝐈𝚫₀
a x : M
⊢ ∃ l ≤ a, l = ‖a‖ ∧ (x < l → Exponential x (bexp a x)) ∧ (l ≤ x → bexp a x = 0)
Tactic:
exact ⟨‖a‖, by simp, rfl, exp_bexp_of_lt, bexp_eq_zero_of_le⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.bexp_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 ⊧ₘ* 𝐈𝚫₀
a x : M
⊢ ‖a‖ ≤ a
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.bexp_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 ⊧ₘ* 𝐈𝚫₀
y a x : M
⊢ (∃ l ≤ a, l = ‖a‖ ∧ (x < l → Exponential x y) ∧ (l ≤ x → y = 0)) → y = bexp a x
Tactic:
rintro ⟨_, _, rfl, hlt, hle⟩
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 ⊧ₘ* 𝐈𝚫₀
y a x : M
left✝ : ‖a‖ ≤ a
hlt : x < ‖a‖ → Exponential x y
hle : ‖a‖ ≤ x → y = 0
⊢ y = bexp a x
Theorem: LO.FirstOrder.Arith.Model.bexp_graph
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 ⊧ₘ* 𝐈𝚫₀
y a x : M
left✝ : ‖a‖ ≤ a
hlt : x < ‖a‖ → Exponential x y
hle : ‖a‖ ≤ x → y = 0
⊢ y = bexp a x
Tactic:
rcases show x < ‖a‖ ∨ ‖a‖ ≤ x from lt_or_ge _ _ with (lt | le)
Proof state after:
case intro.intro.intro.intro.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y a x : M
left✝ : ‖a‖ ≤ a
hlt : x < ‖a‖ → Exponential x y
hle : ‖a‖ ≤ x → y = 0
lt : x < ‖a‖
⊢ y = bexp a x

case intro.intro.intro.intro.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y a x : M
left✝ : ‖a‖ ≤ a
hlt : x < ‖a‖ → Exponential x y
hle : ‖a‖ ≤ x → y = 0
le : ‖a‖ ≤ x
⊢ y = bexp a x
Theorem: LO.FirstOrder.Arith.Model.bexp_graph
Proof state before:
case intro.intro.intro.intro.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y a x : M
left✝ : ‖a‖ ≤ a
hlt : x < ‖a‖ → Exponential x y
hle : ‖a‖ ≤ x → y = 0
lt : x < ‖a‖
⊢ y = bexp a x
Tactic:
exact (hlt lt).uniq (exp_bexp_of_lt lt)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.bexp_graph
Proof state before:
case intro.intro.intro.intro.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y a x : M
left✝ : ‖a‖ ≤ a
hlt : x < ‖a‖ → Exponential x y
hle : ‖a‖ ≤ x → y = 0
le : ‖a‖ ≤ x
⊢ y = bexp a x
Tactic:
rcases hle le
Proof state after:
case intro.intro.intro.intro.inr.refl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a x : M
left✝ : ‖a‖ ≤ a
le : ‖a‖ ≤ x
hlt : x < ‖a‖ → Exponential x 0
hle : ‖a‖ ≤ x → 0 = 0
⊢ 0 = bexp a x
Theorem: LO.FirstOrder.Arith.Model.bexp_graph
Proof state before:
case intro.intro.intro.intro.inr.refl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a x : M
left✝ : ‖a‖ ≤ a
le : ‖a‖ ≤ x
hlt : x < ‖a‖ → Exponential x 0
hle : ‖a‖ ≤ x → 0 = 0
⊢ 0 = bexp a x
Tactic:
simp [bexp_eq_zero_of_le le]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.bexp_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₂ bexp via bexpDef
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 => bexp (v 0) (v 1)) fun x => v x.succ) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val bexpDef)
Theorem: LO.FirstOrder.Arith.Model.bexp_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 => bexp (v 0) (v 1)) fun x => v x.succ) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val bexpDef)
Tactic:
simp [bexpDef, bexp_graph, ←le_iff_lt_succ]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.bexp_monotone_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 j : M
hi : i < ‖a‖
hj : j < ‖a‖
⊢ Exponential i (bexp a i)
Tactic:
simp [hi]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.bexp_monotone_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 j : M
hi : i < ‖a‖
hj : j < ‖a‖
⊢ Exponential j (bexp a j)
Tactic:
simp [hj]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.bexp_monotone_le_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 j : M
hi : i < ‖a‖
hj : j < ‖a‖
⊢ Exponential i (bexp a i)
Tactic:
simp [hi]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.bexp_monotone_le_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 j : M
hi : i < ‖a‖
hj : j < ‖a‖
⊢ Exponential j (bexp a j)
Tactic:
simp [hj]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.bexp_eq_of_lt_length
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 a' : M
ha : i < ‖a‖
ha' : i < ‖a'‖
⊢ bexp a i = bexp a' i
Tactic:
have H : Exponential i (bexp a i) := by simp [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 ⊧ₘ* 𝐈𝚫₀
i a a' : M
ha : i < ‖a‖
ha' : i < ‖a'‖
H : Exponential i (bexp a i)
⊢ bexp a i = bexp a' i
Theorem: LO.FirstOrder.Arith.Model.bexp_eq_of_lt_length
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 a' : M
ha : i < ‖a‖
ha' : i < ‖a'‖
H : Exponential i (bexp a i)
⊢ bexp a i = bexp a' i
Tactic:
have H' : Exponential i (bexp a' i) := by simp [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 ⊧ₘ* 𝐈𝚫₀
i a a' : M
ha : i < ‖a‖
ha' : i < ‖a'‖
H : Exponential i (bexp a i)
H' : Exponential i (bexp a' i)
⊢ bexp a i = bexp a' i
Theorem: LO.FirstOrder.Arith.Model.bexp_eq_of_lt_length
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 a' : M
ha : i < ‖a‖
ha' : i < ‖a'‖
H : Exponential i (bexp a i)
H' : Exponential i (bexp a' i)
⊢ bexp a i = bexp a' i
Tactic:
exact H.uniq H'
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.bexp_eq_of_lt_length
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 a' : M
ha : i < ‖a‖
ha' : i < ‖a'‖
⊢ Exponential i (bexp a i)
Tactic:
simp [ha]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.bexp_eq_of_lt_length
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 a' : M
ha : i < ‖a‖
ha' : i < ‖a'‖
H : Exponential i (bexp a i)
⊢ Exponential i (bexp a' i)
Tactic:
simp [ha']
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.len_bexp
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 x : M
h : x < ‖a‖
⊢ ‖bexp a x‖ = x + 1
Tactic:
rw [length_of_pos (bexp_pos h), log_bexp h]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.bexp_zero_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 ⊧ₘ* 𝐈𝚫₀
⊢ ‖0‖ ≤ 0
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.bexp_pos_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 : 0 < a
⊢ 0 < ‖a‖
Tactic:
simpa
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.bexp_pos_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 : 0 < a
⊢ Exponential 0 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.bexp_two_mul_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 ⊧ₘ* 𝐈𝚫₀
a i : M
⊢ bexp (2 * a) (i + 1) = 2 * bexp a i
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 ⊧ₘ* 𝐈𝚫₀
i : M
⊢ bexp (2 * 0) (i + 1) = 2 * bexp 0 i

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a i : M
pos : 0 < a
⊢ bexp (2 * a) (i + 1) = 2 * bexp a i
Theorem: LO.FirstOrder.Arith.Model.bexp_two_mul_succ
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 i : M
pos : 0 < a
⊢ bexp (2 * a) (i + 1) = 2 * bexp a i
Tactic:
rcases show i ≥ ‖a‖ ∨ i < ‖a‖ from le_or_lt ‖a‖ i with (h | h)
Proof state after:
case inr.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a i : M
pos : 0 < a
h : i ≥ ‖a‖
⊢ bexp (2 * a) (i + 1) = 2 * bexp a i

case inr.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a i : M
pos : 0 < a
h : i < ‖a‖
⊢ bexp (2 * a) (i + 1) = 2 * bexp a i
Theorem: LO.FirstOrder.Arith.Model.bexp_two_mul_succ
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 ⊧ₘ* 𝐈𝚫₀
i : M
⊢ bexp (2 * 0) (i + 1) = 2 * bexp 0 i
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.bexp_two_mul_succ
Proof state before:
case inr.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a i : M
pos : 0 < a
h : i ≥ ‖a‖
⊢ bexp (2 * a) (i + 1) = 2 * bexp a i
Tactic:
simp [bexp_eq_zero_of_le, h, show ‖2 * a‖ ≤ i + 1 from by simp [length_two_mul_of_pos pos, h]]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.bexp_two_mul_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 ⊧ₘ* 𝐈𝚫₀
a i : M
pos : 0 < a
h : i ≥ ‖a‖
⊢ ‖2 * a‖ ≤ i + 1
Tactic:
simp [length_two_mul_of_pos pos, h]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.bexp_two_mul_succ
Proof state before:
case inr.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a i : M
pos : 0 < a
h : i < ‖a‖
⊢ bexp (2 * a) (i + 1) = 2 * bexp a i
Tactic:
exact bexp_eq_of_exp (by simp [length_two_mul_of_pos pos, h]) (exp_bexp_of_lt h).succ
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.bexp_two_mul_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 ⊧ₘ* 𝐈𝚫₀
a i : M
pos : 0 < a
h : i < ‖a‖
⊢ i + 1 < ‖2 * a‖
Tactic:
simp [length_two_mul_of_pos pos, h]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.bexp_two_mul_add_one_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 ⊧ₘ* 𝐈𝚫₀
a i : M
⊢ bexp (2 * a + 1) (i + 1) = 2 * bexp a i
Tactic:
rcases show i ≥ ‖a‖ ∨ i < ‖a‖ from le_or_lt ‖a‖ i with (h | h)
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 ⊧ₘ* 𝐈𝚫₀
a i : M
h : i ≥ ‖a‖
⊢ bexp (2 * a + 1) (i + 1) = 2 * bexp a i

case inr
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 : i < ‖a‖
⊢ bexp (2 * a + 1) (i + 1) = 2 * bexp a i
Theorem: LO.FirstOrder.Arith.Model.bexp_two_mul_add_one_succ
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 ⊧ₘ* 𝐈𝚫₀
a i : M
h : i ≥ ‖a‖
⊢ bexp (2 * a + 1) (i + 1) = 2 * bexp a i
Tactic:
simp [bexp_eq_zero_of_le, h, show ‖2 * a + 1‖ ≤ i + 1 from by simp [length_two_mul_add_one, h]]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.bexp_two_mul_add_one_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 ⊧ₘ* 𝐈𝚫₀
a i : M
h : i ≥ ‖a‖
⊢ ‖2 * a + 1‖ ≤ i + 1
Tactic:
simp [length_two_mul_add_one, h]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.bexp_two_mul_add_one_succ
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 i : M
h : i < ‖a‖
⊢ bexp (2 * a + 1) (i + 1) = 2 * bexp a i
Tactic:
exact bexp_eq_of_exp (by simp [length_two_mul_add_one, h]) (exp_bexp_of_lt h).succ
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.bexp_two_mul_add_one_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 ⊧ₘ* 𝐈𝚫₀
a i : M
h : i < ‖a‖
⊢ i + 1 < ‖2 * a + 1‖
Tactic:
simp [length_two_mul_add_one, h]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.fbit_lt_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 i : M
⊢ fbit a i < 2
Tactic:
simp [fbit]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.fbit_le_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 i : M
⊢ fbit a i < 2
Tactic:
simp [fbit]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.fbit_eq_one_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
⊢ fbit a i = 1 ↔ LenBit (bexp a i) a
Tactic:
simp [fbit, LenBit.iff_rem]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.fbit_eq_zero_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
⊢ fbit a i = 0 ↔ ¬LenBit (bexp a i) a
Tactic:
simp [fbit, LenBit.iff_rem]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.fbit_eq_zero_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 ⊧ₘ* 𝐈𝚫₀
a i : M
hi : ‖a‖ ≤ i
⊢ fbit a i = 0
Tactic:
simp [fbit, bexp_eq_zero_of_le hi]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.fbit_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₂ fbit via fbitDef
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 => fbit (v 0) (v 1)) fun x => v x.succ) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val fbitDef)
Theorem: LO.FirstOrder.Arith.Model.fbit_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 => fbit (v 0) (v 1)) fun x => v x.succ) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val fbitDef)
Tactic:
simp [fbitDef, ←le_iff_lt_succ, fbit, numeral_eq_natCast]
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
⊢ v 0 = v 1 / bexp (v 1) (v 2) % 2 ↔ ∃ x ≤ v 1, x = bexp (v 1) (v 2) ∧ ∃ x_1 ≤ v 1, x_1 = v 1 / x ∧ v 0 = x_1 % 2
Theorem: LO.FirstOrder.Arith.Model.fbit_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
⊢ v 0 = v 1 / bexp (v 1) (v 2) % 2 ↔ ∃ x ≤ v 1, x = bexp (v 1) (v 2) ∧ ∃ x_1 ≤ v 1, x_1 = v 1 / x ∧ v 0 = x_1 % 2
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 ⊧ₘ* 𝐈𝚫₀
v : Fin (Nat.succ 2) → M
⊢ v 0 = v 1 / bexp (v 1) (v 2) % 2 → ∃ x ≤ v 1, x = bexp (v 1) (v 2) ∧ ∃ x_1 ≤ v 1, x_1 = v 1 / x ∧ v 0 = x_1 % 2

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
Theorem: LO.FirstOrder.Arith.Model.fbit_defined
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 ⊧ₘ* 𝐈𝚫₀
v : Fin (Nat.succ 2) → M
⊢ v 0 = v 1 / bexp (v 1) (v 2) % 2 → ∃ x ≤ v 1, x = bexp (v 1) (v 2) ∧ ∃ x_1 ≤ v 1, x_1 = v 1 / x ∧ v 0 = x_1 % 2
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 ⊧ₘ* 𝐈𝚫₀
v : Fin (Nat.succ 2) → M
h : v 0 = v 1 / bexp (v 1) (v 2) % 2
⊢ ∃ x ≤ v 1, x = bexp (v 1) (v 2) ∧ ∃ x_1 ≤ v 1, x_1 = v 1 / x ∧ v 0 = x_1 % 2
Theorem: LO.FirstOrder.Arith.Model.fbit_defined
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 ⊧ₘ* 𝐈𝚫₀
v : Fin (Nat.succ 2) → M
h : v 0 = v 1 / bexp (v 1) (v 2) % 2
⊢ ∃ x ≤ v 1, x = bexp (v 1) (v 2) ∧ ∃ x_1 ≤ v 1, x_1 = v 1 / x ∧ v 0 = x_1 % 2
Tactic:
exact ⟨bexp (v 1) (v 2), by simp, rfl, _, by simp, rfl, h⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.fbit_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
h : v 0 = v 1 / bexp (v 1) (v 2) % 2
⊢ bexp (v 1) (v 2) ≤ v 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.fbit_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
h : v 0 = v 1 / bexp (v 1) (v 2) % 2
⊢ v 1 / bexp (v 1) (v 2) ≤ v 1
Tactic:
simp
Proof state after:
no goals