internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.length_graph
Proof state before:
case inr.mpr
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
⊢ (∃ k ≤ a, k = log a ∧ i = k + 1) → i = log a + 1
Tactic:
rintro ⟨_, _, rfl, rfl⟩
Proof state after:
case inr.mpr.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
left✝ : log a ≤ a
⊢ log a + 1 = log a + 1
Theorem: LO.FirstOrder.Arith.Model.length_graph
Proof state before:
case inr.mpr.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
left✝ : log a ≤ a
⊢ log a + 1 = log a + 1
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.length_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₁ fun x => ‖x‖ via lengthDef
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 => (fun x => ‖x‖) (v 0)) fun x => v x.succ) v ↔
    (Semiformula.Evalbm M v) (HSemiformula.val lengthDef)
Theorem: LO.FirstOrder.Arith.Model.length_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 => (fun x => ‖x‖) (v 0)) fun x => v x.succ) v ↔
    (Semiformula.Evalbm M v) (HSemiformula.val lengthDef)
Tactic:
simp [lengthDef, length_graph, ←le_iff_lt_succ]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.length_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 ⊧ₘ* 𝐈𝚫₀
⊢ ‖1‖ = 1
Tactic:
simp [length_eq_binaryLength]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.length_eq
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 : Exponential x y
⊢ ‖y‖ = x + 1
Tactic:
simp [length_of_pos 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 ⊧ₘ* 𝐈𝚫₀
x y : M
H : Exponential x y
⊢ log y = x
Theorem: LO.FirstOrder.Arith.Model.Exponential.length_eq
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 : Exponential x y
⊢ log y = x
Tactic:
exact H.log_eq_of_exp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.length_two_mul_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
pos : 0 < a
⊢ ‖2 * a‖ = ‖a‖ + 1
Tactic:
simp [pos, length_of_pos, log_two_mul_of_pos]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.length_two_mul_add_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
⊢ ‖2 * a + 1‖ = ‖a‖ + 1
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 ⊧ₘ* 𝐈𝚫₀
⊢ ‖2 * 0 + 1‖ = ‖0‖ + 1

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
⊢ ‖2 * a + 1‖ = ‖a‖ + 1
Theorem: LO.FirstOrder.Arith.Model.length_two_mul_add_one
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 ⊧ₘ* 𝐈𝚫₀
⊢ ‖2 * 0 + 1‖ = ‖0‖ + 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.length_two_mul_add_one
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
⊢ ‖2 * a + 1‖ = ‖a‖ + 1
Tactic:
simp [pos, length_of_pos, log_two_mul_add_one_of_pos]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.length_mul_pow2_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 p b : M
pos : 0 < a
pp : Pow2 p
hb : b < p
⊢ ‖a * p + b‖ = ‖a‖ + log p
Tactic:
simp [length_of_pos, pos, pp.pos, log_mul_pow2_add_of_lt pos pp hb, add_right_comm (log a) (log p) 1]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.length_mul_pow2
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 p : M
pos : 0 < a
pp : Pow2 p
⊢ ‖a * p‖ = ‖a‖ + log p
Tactic:
simp [length_of_pos, pos, pp.pos, log_mul_pow2 pos pp, add_right_comm (log a) (log p) 1]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.length_monotone
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:
rcases zero_le a with (rfl | posa)
Proof state after:
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
b : M
h : 0 ≤ b
⊢ ‖0‖ ≤ ‖b‖

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a b : M
h : a ≤ b
posa : 0 < a
⊢ ‖a‖ ≤ ‖b‖
Theorem: LO.FirstOrder.Arith.Model.length_monotone
Proof state before:
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
b : M
h : 0 ≤ b
⊢ ‖0‖ ≤ ‖b‖
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.length_monotone
Proof state before:
case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a b : M
h : a ≤ b
posa : 0 < a
⊢ ‖a‖ ≤ ‖b‖
Tactic:
simp [length_of_pos posa, length_of_pos (lt_of_lt_of_le posa h)]
Proof state after:
case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a b : M
h : a ≤ b
posa : 0 < a
⊢ log a ≤ log b
Theorem: LO.FirstOrder.Arith.Model.length_monotone
Proof state before:
case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a b : M
h : a ≤ b
posa : 0 < a
⊢ log a ≤ log b
Tactic:
exact log_monotone h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pos_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 ⊧ₘ* 𝐈𝚫₀
a b : M
h : a < ‖b‖
⊢ 0 < b
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 b : M
h : a < ‖b‖
A : ¬0 < b
⊢ False
Theorem: LO.FirstOrder.Arith.Model.pos_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 ⊧ₘ* 𝐈𝚫₀
a b : M
h : a < ‖b‖
A : ¬0 < b
⊢ False
Tactic:
rcases (show b = 0 from by simpa using 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 ⊧ₘ* 𝐈𝚫₀
a : M
h : a < ‖0‖
A : ¬0 < 0
⊢ False
Theorem: LO.FirstOrder.Arith.Model.pos_of_lt_length
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 ⊧ₘ* 𝐈𝚫₀
a : M
h : a < ‖0‖
A : ¬0 < 0
⊢ False
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pos_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 ⊧ₘ* 𝐈𝚫₀
a b : M
h : a < ‖b‖
A : ¬0 < b
⊢ b = 0
Tactic:
simpa using A
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.length_pos_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‖ → 0 < 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 : M
h : 0 < ‖a‖
⊢ 0 < a
Theorem: LO.FirstOrder.Arith.Model.length_pos_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
h : 0 < ‖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 ⊧ₘ* 𝐈𝚫₀
a : M
h : 0 < ‖a‖
A : ¬0 < a
⊢ False
Theorem: LO.FirstOrder.Arith.Model.length_pos_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
h : 0 < ‖a‖
A : ¬0 < a
⊢ False
Tactic:
rcases (show a = 0 from by simpa using 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 ⊧ₘ* 𝐈𝚫₀
h : 0 < ‖0‖
A : ¬0 < 0
⊢ False
Theorem: LO.FirstOrder.Arith.Model.length_pos_iff
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 ⊧ₘ* 𝐈𝚫₀
h : 0 < ‖0‖
A : ¬0 < 0
⊢ False
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.length_pos_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
h : 0 < ‖a‖
A : ¬0 < a
⊢ a = 0
Tactic:
simpa using A
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.length_pos_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 → 0 < ‖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 : M
h : 0 < a
⊢ 0 < ‖a‖
Theorem: LO.FirstOrder.Arith.Model.length_pos_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
h : 0 < a
⊢ 0 < ‖a‖
Tactic:
exact pos_iff_one_le.mpr (by simpa using length_monotone (pos_iff_one_le.mp h))
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.length_pos_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
h : 0 < a
⊢ 1 ≤ ‖a‖
Tactic:
simpa using length_monotone (pos_iff_one_le.mp h)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.length_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 : M
⊢ ¬‖a‖ = 0 ↔ ¬a = 0
Tactic:
simp [←pos_iff_ne_zero]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.le_log_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 ⊧ₘ* 𝐈𝚫₀
a b : M
h : a < ‖b‖
⊢ a ≤ log b
Tactic:
have : 0 < b := pos_of_lt_length 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 b : M
h : a < ‖b‖
this : 0 < b
⊢ a ≤ log b
Theorem: LO.FirstOrder.Arith.Model.le_log_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 ⊧ₘ* 𝐈𝚫₀
a b : M
h : a < ‖b‖
this : 0 < b
⊢ a ≤ log b
Tactic:
exact le_iff_lt_succ.mpr (by simpa [length_of_pos this] using h)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.le_log_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 ⊧ₘ* 𝐈𝚫₀
a b : M
h : a < ‖b‖
this : 0 < b
⊢ a < log b + 1
Tactic:
simpa [length_of_pos this] using h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.exponential_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 b : M
pos : 0 < a
h : Exponential (log a) b
⊢ b ≤ 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 b : M
pos : 0 < a
h : Exponential (log a) b
w✝ : M
left✝ : w✝ ≤ a
H : Exponential (log a) w✝
right✝ : a < 2 * w✝
⊢ b ≤ a
Theorem: LO.FirstOrder.Arith.Model.exponential_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 b : M
pos : 0 < a
h : Exponential (log a) b
w✝ : M
left✝ : w✝ ≤ a
H : Exponential (log a) w✝
right✝ : a < 2 * w✝
⊢ b ≤ a
Tactic:
rcases H.uniq h
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 b : M
pos : 0 < a
h : Exponential (log a) b
left✝ : b ≤ a
H : Exponential (log a) b
right✝ : a < 2 * b
⊢ b ≤ a
Theorem: LO.FirstOrder.Arith.Model.exponential_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 b : M
pos : 0 < a
h : Exponential (log a) b
left✝ : b ≤ a
H : Exponential (log a) b
right✝ : a < 2 * b
⊢ b ≤ a
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lt_exponential_log_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 b : M
h : Exponential (log a) b
⊢ a < 2 * b
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 ⊧ₘ* 𝐈𝚫₀
b : M
h : Exponential (log 0) b
⊢ 0 < 2 * b

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a b : M
h : Exponential (log a) b
pos : 0 < a
⊢ a < 2 * b
Theorem: LO.FirstOrder.Arith.Model.lt_exponential_log_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 b : M
h : Exponential (log a) b
pos : 0 < a
⊢ a < 2 * b
Tactic:
rcases log_pos pos with ⟨_, _, H, _⟩
Proof state after:
case inr.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 b : M
h : Exponential (log a) b
pos : 0 < a
w✝ : M
left✝ : w✝ ≤ a
H : Exponential (log a) w✝
right✝ : a < 2 * w✝
⊢ a < 2 * b
Theorem: LO.FirstOrder.Arith.Model.lt_exponential_log_self
Proof state before:
case inr.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 b : M
h : Exponential (log a) b
pos : 0 < a
w✝ : M
left✝ : w✝ ≤ a
H : Exponential (log a) w✝
right✝ : a < 2 * w✝
⊢ a < 2 * b
Tactic:
rcases H.uniq h
Proof state after:
case inr.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 b : M
h : Exponential (log a) b
pos : 0 < a
left✝ : b ≤ a
H : Exponential (log a) b
right✝ : a < 2 * b
⊢ a < 2 * b
Theorem: LO.FirstOrder.Arith.Model.lt_exponential_log_self
Proof state before:
case inr.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 b : M
h : Exponential (log a) b
pos : 0 < a
left✝ : b ≤ a
H : Exponential (log a) b
right✝ : a < 2 * b
⊢ a < 2 * b
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lt_exponential_log_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 ⊧ₘ* 𝐈𝚫₀
b : M
h : Exponential (log 0) b
⊢ 0 < 2 * b
Tactic:
simp at 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 ⊧ₘ* 𝐈𝚫₀
b : M
h : b = 1
⊢ 0 < 2 * b
Theorem: LO.FirstOrder.Arith.Model.lt_exponential_log_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 ⊧ₘ* 𝐈𝚫₀
b : M
h : b = 1
⊢ 0 < 2 * b
Tactic:
simp [h]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lt_exp_len_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 b : M
h : Exponential ‖a‖ b
⊢ a < b
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 ⊧ₘ* 𝐈𝚫₀
b : M
h : Exponential ‖0‖ b
⊢ 0 < b

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a b : M
h : Exponential ‖a‖ b
pos : 0 < a
⊢ a < b
Theorem: LO.FirstOrder.Arith.Model.lt_exp_len_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 b : M
h : Exponential ‖a‖ b
pos : 0 < a
⊢ a < b
Tactic:
simp [length_of_pos pos] at h
Proof state after:
case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a b : M
pos : 0 < a
h : Exponential (log a + 1) b
⊢ a < b
Theorem: LO.FirstOrder.Arith.Model.lt_exp_len_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 b : M
pos : 0 < a
h : Exponential (log a + 1) b
⊢ a < b
Tactic:
rcases Exponential.exponential_succ.mp h with ⟨b, rfl, H⟩
Proof state after:
case inr.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
b : M
H : Exponential (log a) b
h : Exponential (log a + 1) (2 * b)
⊢ a < 2 * b
Theorem: LO.FirstOrder.Arith.Model.lt_exp_len_self
Proof state before:
case inr.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
b : M
H : Exponential (log a) b
h : Exponential (log a + 1) (2 * b)
⊢ a < 2 * b
Tactic:
exact lt_exponential_log_self H
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lt_exp_len_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 ⊧ₘ* 𝐈𝚫₀
b : M
h : Exponential ‖0‖ b
⊢ 0 < b
Tactic:
simp at 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 ⊧ₘ* 𝐈𝚫₀
b : M
h : b = 1
⊢ 0 < b
Theorem: LO.FirstOrder.Arith.Model.lt_exp_len_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 ⊧ₘ* 𝐈𝚫₀
b : M
h : b = 1
⊢ 0 < b
Tactic:
simp [h]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.le_iff_le_log_of_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 ⊧ₘ* 𝐈𝚫₀
x y a : M
H : Exponential x y
pos : 0 < a
⊢ y ≤ a → x ≤ log a
Tactic:
rcases H.log_eq_of_exp
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 ⊧ₘ* 𝐈𝚫₀
y a : M
pos : 0 < a
H : Exponential (log y) y
⊢ y ≤ a → log y ≤ log a
Theorem: LO.FirstOrder.Arith.Model.le_iff_le_log_of_exp
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 ⊧ₘ* 𝐈𝚫₀
y a : M
pos : 0 < a
H : Exponential (log y) y
⊢ y ≤ a → log y ≤ log a
Tactic:
exact log_monotone
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.le_iff_le_log_of_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 ⊧ₘ* 𝐈𝚫₀
x y a : M
H : Exponential x y
pos : 0 < a
h : x ≤ log a
⊢ y ≤ a
Tactic:
rcases log_pos pos with ⟨a', ha', Haa', _⟩
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 ⊧ₘ* 𝐈𝚫₀
x y a : M
H : Exponential x y
pos : 0 < a
h : x ≤ log a
a' : M
ha' : a' ≤ a
Haa' : Exponential (log a) a'
right✝ : a < 2 * a'
⊢ y ≤ a
Theorem: LO.FirstOrder.Arith.Model.le_iff_le_log_of_exp
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 ⊧ₘ* 𝐈𝚫₀
x y a : M
H : Exponential x y
pos : 0 < a
h : x ≤ log a
a' : M
ha' : a' ≤ a
Haa' : Exponential (log a) a'
right✝ : a < 2 * a'
⊢ y ≤ a
Tactic:
exact le_trans (Exponential.monotone_le H Haa' h) ha'
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.le_iff_lt_length_of_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 ⊧ₘ* 𝐈𝚫₀
x y a : M
H : Exponential x y
⊢ y ≤ a ↔ x < ‖a‖
Tactic:
rcases zero_le a with (rfl | pos)
Proof state after:
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y : M
H : Exponential x y
⊢ y ≤ 0 ↔ x < ‖0‖

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y a : M
H : Exponential x y
pos : 0 < a
⊢ y ≤ a ↔ x < ‖a‖
Theorem: LO.FirstOrder.Arith.Model.le_iff_lt_length_of_exp
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 ⊧ₘ* 𝐈𝚫₀
x y a : M
H : Exponential x y
pos : 0 < a
⊢ y ≤ a ↔ x < ‖a‖
Tactic:
simp [le_iff_le_log_of_exp H pos, length_of_pos pos, ←le_iff_lt_succ]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.le_iff_lt_length_of_exp
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 ⊧ₘ* 𝐈𝚫₀
x y : M
H : Exponential x y
⊢ y ≤ 0 ↔ x < ‖0‖
Tactic:
simp
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 ⊧ₘ* 𝐈𝚫₀
x y : M
H : Exponential x y
⊢ ¬y = 0
Theorem: LO.FirstOrder.Arith.Model.le_iff_lt_length_of_exp
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 ⊧ₘ* 𝐈𝚫₀
x y : M
H : Exponential x y
⊢ ¬y = 0
Tactic:
exact pos_iff_ne_zero.mp H.range_pos
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.lt_iff_log_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 ⊧ₘ* 𝐈𝚫₀
x y a : M
H : Exponential x y
pos : 0 < a
⊢ ¬a < y ↔ ¬log a < x
Tactic:
simpa using le_iff_le_log_of_exp H pos
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.lt_iff_len_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 a : M
H : Exponential x y
⊢ ¬a < y ↔ ¬‖a‖ ≤ x
Tactic:
simpa using le_iff_lt_length_of_exp H
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.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 ⊧ₘ* 𝐈𝚫₀
x y : M
H : Exponential x y
⊢ y ≤ y
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.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 ⊧ₘ* 𝐈𝚫₀
x y : M
H : Exponential x y
⊢ y ≤ y
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lt_exponential_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 ⊧ₘ* 𝐈𝚫₀
a b : M
h : Exponential ‖a‖ b
⊢ a < b
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 ⊧ₘ* 𝐈𝚫₀
b : M
h : Exponential ‖0‖ b
⊢ 0 < b

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a b : M
h : Exponential ‖a‖ b
pos : 0 < a
⊢ a < b