Theorem: LO.FirstOrder.Arith.Model.exponential_of_pow2 (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 ⊧ₘ* 𝐈𝚫₀
p : M
pp : Pow2 p
⊢ Exponential (log p) p
Tactic:
rcases log_pos pp.pos with ⟨q, hq, H, hp⟩
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

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

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

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

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

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
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 ⊧ₘ* 𝐈𝚫₀
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
State after:
no goals