Theorem: LO.FirstOrder.Arith.Model.log_monotone (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 b : M
h : a ≤ b
⊢ log a ≤ log b
Tactic:
rcases zero_le a with (rfl | posa)
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

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

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

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

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

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

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

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

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

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

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