internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.log_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 ⊧ₘ* 𝐈𝚫₀
y : M
pos : 0 < y
y' : M
hy' : y' ≤ y
H : Exponential (log y) y'
hy : y < 2 * y'
⊢ 2 * y' ≤ 2 * y
Tactic:
simpa using hy'
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_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 ⊧ₘ* 𝐈𝚫₀
y : M
pos : 0 < y
y' : M
hy' : y' ≤ y
H : Exponential (log y) y'
hy : y < 2 * y'
⊢ 2 * y < 2 * (2 * y')
Tactic:
simpa using hy
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_two_mul_add_one_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 ⊧ₘ* 𝐈𝚫₀
y : M
pos : 0 < y
⊢ log (2 * y + 1) = log y + 1
Tactic:
rcases log_pos pos with ⟨y', hy', H, hy⟩
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 ⊧ₘ* 𝐈𝚫₀
y : M
pos : 0 < y
y' : M
hy' : y' ≤ y
H : Exponential (log y) y'
hy : y < 2 * y'
⊢ log (2 * y + 1) = log y + 1
Theorem: LO.FirstOrder.Arith.Model.log_two_mul_add_one_of_pos
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 ⊧ₘ* 𝐈𝚫₀
y : M
pos : 0 < y
y' : M
hy' : y' ≤ y
H : Exponential (log y) y'
hy : y < 2 * y'
⊢ log (2 * y + 1) = log y + 1
Tactic:
exact log_eq_of_pos (by simp) (Exponential.exponential_succ_mul_two.mpr H)
  (le_trans (by simpa using hy') le_self_add) (two_mul_add_one_lt_two_mul_of_lt hy)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_two_mul_add_one_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 ⊧ₘ* 𝐈𝚫₀
y : M
pos : 0 < y
y' : M
hy' : y' ≤ y
H : Exponential (log y) y'
hy : y < 2 * y'
⊢ 0 < 2 * y + 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_two_mul_add_one_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 ⊧ₘ* 𝐈𝚫₀
y : M
pos : 0 < y
y' : M
hy' : y' ≤ y
H : Exponential (log y) y'
hy : y < 2 * y'
⊢ 2 * y' ≤ 2 * y
Tactic:
simpa using hy'
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.log_eq_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 : M
H : Exponential x y
⊢ y ≤ y
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.exponential_of_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 ⊧ₘ* 𝐈𝚫₀
p : M
pp : Pow2 p
⊢ Exponential (log p) p
Tactic:
rcases log_pos pp.pos with ⟨q, hq, H, hp⟩
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 ⊧ₘ* 𝐈𝚫₀
p : M
pp : Pow2 p
q : M
hq : q ≤ p
H : Exponential (log p) q
hp : p < 2 * q
⊢ Exponential (log p) p
Theorem: LO.FirstOrder.Arith.Model.exponential_of_pow2
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 ⊧ₘ* 𝐈𝚫₀
p : M
pp : Pow2 p
q : M
hq : q ≤ p
H : Exponential (log p) q
hp : p < 2 * q
⊢ Exponential (log p) p
Tactic:
suffices p = q by simpa [this] using 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 ⊧ₘ* 𝐈𝚫₀
p : M
pp : Pow2 p
q : M
hq : q ≤ p
H : Exponential (log p) q
hp : p < 2 * q
⊢ p = q
Theorem: LO.FirstOrder.Arith.Model.exponential_of_pow2
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 ⊧ₘ* 𝐈𝚫₀
p : M
pp : Pow2 p
q : M
hq : q ≤ p
H : Exponential (log p) q
hp : p < 2 * q
⊢ p = q
Tactic:
by_contra ne
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 ⊧ₘ* 𝐈𝚫₀
p : M
pp : Pow2 p
q : M
hq : q ≤ p
H : Exponential (log p) q
hp : p < 2 * q
ne : ¬p = q
⊢ False
Theorem: LO.FirstOrder.Arith.Model.exponential_of_pow2
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 ⊧ₘ* 𝐈𝚫₀
p : M
pp : Pow2 p
q : M
hq : q ≤ p
H : Exponential (log p) q
hp : p < 2 * q
ne : ¬p = q
⊢ False
Tactic:
have : q < p := lt_of_le_of_ne hq (Ne.symm ne)
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 ⊧ₘ* 𝐈𝚫₀
p : M
pp : Pow2 p
q : M
hq : q ≤ p
H : Exponential (log p) q
hp : p < 2 * q
ne : ¬p = q
this : q < p
⊢ False
Theorem: LO.FirstOrder.Arith.Model.exponential_of_pow2
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 ⊧ₘ* 𝐈𝚫₀
p : M
pp : Pow2 p
q : M
hq : q ≤ p
H : Exponential (log p) q
hp : p < 2 * q
ne : ¬p = q
this : q < p
⊢ False
Tactic:
have : 2 * q < 2 * q := calc
  2 * q ≤ p     := (Pow2.lt_iff_two_mul_le H.range_pow2 pp).mp this
  _     < 2 * q := hp
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 ⊧ₘ* 𝐈𝚫₀
p : M
pp : Pow2 p
q : M
hq : q ≤ p
H : Exponential (log p) q
hp : p < 2 * q
ne : ¬p = q
this✝ : q < p
this : 2 * q < 2 * q
⊢ False
Theorem: LO.FirstOrder.Arith.Model.exponential_of_pow2
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 ⊧ₘ* 𝐈𝚫₀
p : M
pp : Pow2 p
q : M
hq : q ≤ p
H : Exponential (log p) q
hp : p < 2 * q
ne : ¬p = q
this✝ : q < p
this : 2 * q < 2 * q
⊢ False
Tactic:
simp at this
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.exponential_of_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 ⊧ₘ* 𝐈𝚫₀
p : M
pp : Pow2 p
q : M
hq : q ≤ p
H : Exponential (log p) q
hp : p < 2 * q
this : p = q
⊢ Exponential (log p) p
Tactic:
simpa [this] using H
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_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
⊢ log (a * p + b) = log a + log p
Tactic:
rcases log_pos pos with ⟨a', ha', Ha, ha⟩
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 p b : M
pos : 0 < a
pp : Pow2 p
hb : b < p
a' : M
ha' : a' ≤ a
Ha : Exponential (log a) a'
ha : a < 2 * a'
⊢ log (a * p + b) = log a + log p
Theorem: LO.FirstOrder.Arith.Model.log_mul_pow2_add_of_lt
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 p b : M
pos : 0 < a
pp : Pow2 p
hb : b < p
a' : M
ha' : a' ≤ a
Ha : Exponential (log a) a'
ha : a < 2 * a'
⊢ log (a * p + b) = log a + log p
Tactic:
rcases log_pos pp.pos with ⟨p', hp', Hp, hp⟩
Proof state after:
case 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 ⊧ₘ* 𝐈𝚫₀
a p b : M
pos : 0 < a
pp : Pow2 p
hb : b < p
a' : M
ha' : a' ≤ a
Ha : Exponential (log a) a'
ha : a < 2 * a'
p' : M
hp' : p' ≤ p
Hp : Exponential (log p) p'
hp : p < 2 * p'
⊢ log (a * p + b) = log a + log p
Theorem: LO.FirstOrder.Arith.Model.log_mul_pow2_add_of_lt
Proof state before:
case 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 ⊧ₘ* 𝐈𝚫₀
a p b : M
pos : 0 < a
pp : Pow2 p
hb : b < p
a' : M
ha' : a' ≤ a
Ha : Exponential (log a) a'
ha : a < 2 * a'
p' : M
hp' : p' ≤ p
Hp : Exponential (log p) p'
hp : p < 2 * p'
⊢ log (a * p + b) = log a + log p
Tactic:
exact log_eq_of_pos (lt_of_lt_of_le (mul_pos pos pp.pos) le_self_add)
  (Exponential.add_mul Ha Hp) (le_trans (mul_le_mul' ha' hp') le_self_add) (by
    rcases Hp.uniq (exponential_of_pow2 pp)
    calc
      a * p + b < a * p + p    := by simp [hb]
      _         = (a + 1) * p  := by simp [add_mul]
      _         ≤ 2 * (a' * p) := by simp [←mul_assoc]; exact mul_le_mul_right (lt_iff_succ_le.mp ha))
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_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' : M
ha' : a' ≤ a
Ha : Exponential (log a) a'
ha : a < 2 * a'
p' : M
hp' : p' ≤ p
Hp : Exponential (log p) p'
hp : p < 2 * p'
⊢ a * p + b < 2 * (a' * p')
Tactic:
rcases Hp.uniq (exponential_of_pow2 pp)
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 p b : M
pos : 0 < a
pp : Pow2 p
hb : b < p
a' : M
ha' : a' ≤ a
Ha : Exponential (log a) a'
ha : a < 2 * a'
hp' : p ≤ p
Hp : Exponential (log p) p
hp : p < 2 * p
⊢ a * p + b < 2 * (a' * p)
Theorem: LO.FirstOrder.Arith.Model.log_mul_pow2_add_of_lt
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 p b : M
pos : 0 < a
pp : Pow2 p
hb : b < p
a' : M
ha' : a' ≤ a
Ha : Exponential (log a) a'
ha : a < 2 * a'
hp' : p ≤ p
Hp : Exponential (log p) p
hp : p < 2 * p
⊢ a * p + b < 2 * (a' * p)
Tactic:
calc
  a * p + b < a * p + p    := by simp [hb]
  _         = (a + 1) * p  := by simp [add_mul]
  _         ≤ 2 * (a' * p) := by simp [←mul_assoc]; exact mul_le_mul_right (lt_iff_succ_le.mp ha)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_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' : M
ha' : a' ≤ a
Ha : Exponential (log a) a'
ha : a < 2 * a'
hp' : p ≤ p
Hp : Exponential (log p) p
hp : p < 2 * p
⊢ a * p + b < a * p + p
Tactic:
simp [hb]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_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' : M
ha' : a' ≤ a
Ha : Exponential (log a) a'
ha : a < 2 * a'
hp' : p ≤ p
Hp : Exponential (log p) p
hp : p < 2 * p
⊢ a * p + p = (a + 1) * p
Tactic:
simp [add_mul]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_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' : M
ha' : a' ≤ a
Ha : Exponential (log a) a'
ha : a < 2 * a'
hp' : p ≤ p
Hp : Exponential (log p) p
hp : p < 2 * p
⊢ (a + 1) * p ≤ 2 * (a' * p)
Tactic:
simp [←mul_assoc]
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 p b : M
pos : 0 < a
pp : Pow2 p
hb : b < p
a' : M
ha' : a' ≤ a
Ha : Exponential (log a) a'
ha : a < 2 * a'
hp' : p ≤ p
Hp : Exponential (log p) p
hp : p < 2 * p
⊢ (a + 1) * p ≤ 2 * a' * p
Theorem: LO.FirstOrder.Arith.Model.log_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' : M
ha' : a' ≤ a
Ha : Exponential (log a) a'
ha : a < 2 * a'
hp' : p ≤ p
Hp : Exponential (log p) p
hp : p < 2 * p
⊢ (a + 1) * p ≤ 2 * a' * p
Tactic:
exact mul_le_mul_right (lt_iff_succ_le.mp ha)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_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
⊢ log (a * p) = log a + log p
Tactic:
simpa using log_mul_pow2_add_of_lt pos pp pp.pos
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_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
⊢ log a ≤ log 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
⊢ log 0 ≤ log 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
⊢ log a ≤ log b
Theorem: LO.FirstOrder.Arith.Model.log_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:
rcases zero_le b with (rfl | posb)
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 : M
posa : 0 < a
h : a ≤ 0
⊢ log a ≤ log 0

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 b : M
h : a ≤ b
posa : 0 < a
posb : 0 < b
⊢ log a ≤ log b
Theorem: LO.FirstOrder.Arith.Model.log_monotone
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 b : M
h : a ≤ b
posa : 0 < a
posb : 0 < b
⊢ log a ≤ log b
Tactic:
rcases log_pos posa with ⟨a', ha', Ha, _⟩
Proof state after:
case inr.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 : a ≤ b
posa : 0 < a
posb : 0 < b
a' : M
ha' : a' ≤ a
Ha : Exponential (log a) a'
right✝ : a < 2 * a'
⊢ log a ≤ log b
Theorem: LO.FirstOrder.Arith.Model.log_monotone
Proof state before:
case inr.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 : a ≤ b
posa : 0 < a
posb : 0 < b
a' : M
ha' : a' ≤ a
Ha : Exponential (log a) a'
right✝ : a < 2 * a'
⊢ log a ≤ log b
Tactic:
rcases log_pos posb with ⟨b', _, Hb, hb⟩
Proof state after:
case inr.inr.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 ⊧ₘ* 𝐈𝚫₀
a b : M
h : a ≤ b
posa : 0 < a
posb : 0 < b
a' : M
ha' : a' ≤ a
Ha : Exponential (log a) a'
right✝ : a < 2 * a'
b' : M
left✝ : b' ≤ b
Hb : Exponential (log b) b'
hb : b < 2 * b'
⊢ log a ≤ log b
Theorem: LO.FirstOrder.Arith.Model.log_monotone
Proof state before:
case inr.inr.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 ⊧ₘ* 𝐈𝚫₀
a b : M
h : a ≤ b
posa : 0 < a
posb : 0 < b
a' : M
ha' : a' ≤ a
Ha : Exponential (log a) a'
right✝ : a < 2 * a'
b' : M
left✝ : b' ≤ b
Hb : Exponential (log b) b'
hb : b < 2 * b'
⊢ log a ≤ log b
Tactic:
by_contra lt
Proof state after:
case inr.inr.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 ⊧ₘ* 𝐈𝚫₀
a b : M
h : a ≤ b
posa : 0 < a
posb : 0 < b
a' : M
ha' : a' ≤ a
Ha : Exponential (log a) a'
right✝ : a < 2 * a'
b' : M
left✝ : b' ≤ b
Hb : Exponential (log b) b'
hb : b < 2 * b'
lt : ¬log a ≤ log b
⊢ False
Theorem: LO.FirstOrder.Arith.Model.log_monotone
Proof state before:
case inr.inr.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 ⊧ₘ* 𝐈𝚫₀
a b : M
h : a ≤ b
posa : 0 < a
posb : 0 < b
a' : M
ha' : a' ≤ a
Ha : Exponential (log a) a'
right✝ : a < 2 * a'
b' : M
left✝ : b' ≤ b
Hb : Exponential (log b) b'
hb : b < 2 * b'
lt : ¬log a ≤ log b
⊢ False
Tactic:
have : b' < a' := (Exponential.monotone_iff Hb Ha).mp (by simpa using lt)
Proof state after:
case inr.inr.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 ⊧ₘ* 𝐈𝚫₀
a b : M
h : a ≤ b
posa : 0 < a
posb : 0 < b
a' : M
ha' : a' ≤ a
Ha : Exponential (log a) a'
right✝ : a < 2 * a'
b' : M
left✝ : b' ≤ b
Hb : Exponential (log b) b'
hb : b < 2 * b'
lt : ¬log a ≤ log b
this : b' < a'
⊢ False
Theorem: LO.FirstOrder.Arith.Model.log_monotone
Proof state before:
case inr.inr.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 ⊧ₘ* 𝐈𝚫₀
a b : M
h : a ≤ b
posa : 0 < a
posb : 0 < b
a' : M
ha' : a' ≤ a
Ha : Exponential (log a) a'
right✝ : a < 2 * a'
b' : M
left✝ : b' ≤ b
Hb : Exponential (log b) b'
hb : b < 2 * b'
lt : ¬log a ≤ log b
this : b' < a'
⊢ False
Tactic:
have : b < b := calc
  b < 2 * b' := hb
  _ ≤ a'     := (Pow2.lt_iff_two_mul_le Hb.range_pow2 Ha.range_pow2).mp this
  _ ≤ a      := ha'
  _ ≤ b      := h
Proof state after:
case inr.inr.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 ⊧ₘ* 𝐈𝚫₀
a b : M
h : a ≤ b
posa : 0 < a
posb : 0 < b
a' : M
ha' : a' ≤ a
Ha : Exponential (log a) a'
right✝ : a < 2 * a'
b' : M
left✝ : b' ≤ b
Hb : Exponential (log b) b'
hb : b < 2 * b'
lt : ¬log a ≤ log b
this✝ : b' < a'
this : b < b
⊢ False
Theorem: LO.FirstOrder.Arith.Model.log_monotone
Proof state before:
case inr.inr.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 ⊧ₘ* 𝐈𝚫₀
a b : M
h : a ≤ b
posa : 0 < a
posb : 0 < b
a' : M
ha' : a' ≤ a
Ha : Exponential (log a) a'
right✝ : a < 2 * a'
b' : M
left✝ : b' ≤ b
Hb : Exponential (log b) b'
hb : b < 2 * b'
lt : ¬log a ≤ log b
this✝ : b' < a'
this : b < b
⊢ False
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_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
⊢ log 0 ≤ log b
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_monotone
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 : M
posa : 0 < a
h : a ≤ 0
⊢ log a ≤ log 0
Tactic:
have := lt_of_lt_of_le posa 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 : M
posa : 0 < a
h : a ≤ 0
this : 0 < 0
⊢ log a ≤ log 0
Theorem: LO.FirstOrder.Arith.Model.log_monotone
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 : M
posa : 0 < a
h : a ≤ 0
this : 0 < 0
⊢ log a ≤ log 0
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_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
posa : 0 < a
posb : 0 < b
a' : M
ha' : a' ≤ a
Ha : Exponential (log a) a'
right✝ : a < 2 * a'
b' : M
left✝ : b' ≤ b
Hb : Exponential (log b) b'
hb : b < 2 * b'
lt : ¬log a ≤ log b
⊢ log b < log a
Tactic:
simpa using lt
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.length_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 [length_eq_binaryLength]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.length_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
⊢ ‖a‖ = log a + 1
Tactic:
simp [length_eq_binaryLength, pos]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.length_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 : M
⊢ ‖a‖ ≤ 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 ⊧ₘ* 𝐈𝚫₀
⊢ ‖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
⊢ ‖a‖ ≤ a
Theorem: LO.FirstOrder.Arith.Model.length_le
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 ⊧ₘ* 𝐈𝚫₀
⊢ ‖0‖ ≤ 0
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.length_le
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
⊢ ‖a‖ ≤ a
Tactic:
simp [pos, length_of_pos, ←lt_iff_succ_le, log_lt_self_of_pos]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.length_graph
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i a : M
⊢ i = ‖a‖ ↔ (0 < a → ∃ k ≤ a, k = log a ∧ i = k + 1) ∧ (a = 0 → i = 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 ⊧ₘ* 𝐈𝚫₀
i : M
⊢ i = ‖0‖ ↔ (0 < 0 → ∃ k ≤ 0, k = log 0 ∧ i = k + 1) ∧ (0 = 0 → i = 0)

case inr
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
⊢ i = ‖a‖ ↔ (0 < a → ∃ k ≤ a, k = log a ∧ i = k + 1) ∧ (a = 0 → i = 0)
Theorem: LO.FirstOrder.Arith.Model.length_graph
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
⊢ i = ‖0‖ ↔ (0 < 0 → ∃ k ≤ 0, k = log 0 ∧ i = k + 1) ∧ (0 = 0 → i = 0)
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.length_graph
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 ⊧ₘ* 𝐈𝚫₀
i a : M
pos : 0 < a
⊢ i = ‖a‖ ↔ (0 < a → ∃ k ≤ a, k = log a ∧ i = k + 1) ∧ (a = 0 → i = 0)
Tactic:
simp [length_of_pos, pos, pos_iff_ne_zero.mp pos]
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 ⊧ₘ* 𝐈𝚫₀
i a : M
pos : 0 < a
⊢ i = log a + 1 ↔ ∃ k ≤ a, k = log a ∧ i = k + 1
Theorem: LO.FirstOrder.Arith.Model.length_graph
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 ⊧ₘ* 𝐈𝚫₀
i a : M
pos : 0 < a
⊢ i = log a + 1 ↔ ∃ k ≤ a, k = log a ∧ i = k + 1
Tactic:
constructor
Proof state after:
case inr.mp
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
⊢ i = log a + 1 → ∃ k ≤ a, k = log a ∧ i = k + 1

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
Theorem: LO.FirstOrder.Arith.Model.length_graph
Proof state before:
case inr.mp
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
⊢ i = log a + 1 → ∃ k ≤ a, k = log a ∧ i = k + 1
Tactic:
rintro rfl
Proof state after:
case inr.mp
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
⊢ ∃ k ≤ a, k = log a ∧ log a + 1 = k + 1
Theorem: LO.FirstOrder.Arith.Model.length_graph
Proof state before:
case inr.mp
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
⊢ ∃ k ≤ a, k = log a ∧ log a + 1 = k + 1
Tactic:
exact ⟨log a, by simp⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.length_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 : M
pos : 0 < a
⊢ log a ≤ a ∧ log a = log a ∧ log a + 1 = log a + 1
Tactic:
simp
Proof state after:
no goals