Theorem: LO.FirstOrder.Arith.Model.log_mul_pow2_add_of_lt (Arithmetization/ISigmaZero/Exponential/Log.lean)

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⟩
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

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⟩
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

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))
State after:
no goals

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)
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)

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)
State after:
no goals

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]
State after:
no goals

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]
State after:
no goals

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]
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

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)
State after:
no goals