Theorem: LO.FirstOrder.Arith.Model.log_exists_unique_pos (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 ⊧ₘ* 𝐈𝚫₀
y : M
hy : 0 < y
this : ∃ x < y, ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'
⊢ ∃! x, x < y ∧ ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'
Tactic:
rcases this with ⟨x, hx⟩
State after:
case intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y : M
hy : 0 < y
x : M
hx : x < y ∧ ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'
⊢ ∃! x, x < y ∧ ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'

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
hy : 0 < y
⊢ ∃ x < y, ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'
Tactic:
induction y using hierarchy_polynomial_induction_oRing_sigma₀
State after:
case hP
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ 𝚺₀-Predicate fun {y} => 0 < y → ∃ x < y, ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'

case zero
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
hy : 0 < 0
⊢ ∃ x < 0, ∃ y' ≤ 0, Exponential x y' ∧ 0 < 2 * y'

case even
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x✝ : M
a✝¹ : x✝ > 0
a✝ : 0 < x✝ → ∃ x < x✝, ∃ y' ≤ x✝, Exponential x y' ∧ x✝ < 2 * y'
hy : 0 < 2 * x✝
⊢ ∃ x < 2 * x✝, ∃ y' ≤ 2 * x✝, Exponential x y' ∧ 2 * x✝ < 2 * y'

case odd
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x✝ : M
a✝ : 0 < x✝ → ∃ x < x✝, ∃ y' ≤ x✝, Exponential x y' ∧ x✝ < 2 * y'
hy : 0 < 2 * x✝ + 1
⊢ ∃ x < 2 * x✝ + 1, ∃ y' ≤ 2 * x✝ + 1, Exponential x y' ∧ 2 * x✝ + 1 < 2 * y'

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
hy : 0 < 0
⊢ ∃ x < 0, ∃ y' ≤ 0, Exponential x y' ∧ 0 < 2 * y'
Tactic:
case zero => simp at hy
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 ⊧ₘ* 𝐈𝚫₀
y : M
a✝ : y > 0
IH : 0 < y → ∃ x < y, ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'
hy : 0 < 2 * y
⊢ ∃ x < 2 * y, ∃ y' ≤ 2 * y, Exponential x y' ∧ 2 * y < 2 * y'
Tactic:
case even y _ IH =>
  rcases (IH (by simpa using hy) : ∃ x < y, ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y') with ⟨x, hxy, y', gey, H, lty⟩
  exact ⟨x + 1, lt_of_lt_of_le (by simp [hxy]) (succ_le_double_of_pos (pos_of_gt hxy)),
    2 * y', by simpa using gey, Exponential.exponential_succ_mul_two.mpr H, by simpa using lty⟩
State after:
no goals

State before:
case hP
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ 𝚺₀-Predicate fun {y} => 0 < y → ∃ x < y, ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'
Tactic:
definability
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 ⊧ₘ* 𝐈𝚫₀
hy : 0 < 0
⊢ ∃ x < 0, ∃ y' ≤ 0, Exponential x y' ∧ 0 < 2 * y'
Tactic:
simp at hy
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 ⊧ₘ* 𝐈𝚫₀
y : M
a✝ : y > 0
IH : 0 < y → ∃ x < y, ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'
hy : 0 < 2 * y
⊢ ∃ x < 2 * y, ∃ y' ≤ 2 * y, Exponential x y' ∧ 2 * y < 2 * y'
Tactic:
rcases (IH (by simpa using hy) : ∃ x < y, ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y') with ⟨x, hxy, y', gey, H, lty⟩
State after:
case 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 ⊧ₘ* 𝐈𝚫₀
y : M
a✝ : y > 0
IH : 0 < y → ∃ x < y, ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'
hy : 0 < 2 * y
x : M
hxy : x < y
y' : M
gey : y' ≤ y
H : Exponential x y'
lty : y < 2 * y'
⊢ ∃ x < 2 * y, ∃ y' ≤ 2 * y, Exponential x y' ∧ 2 * y < 2 * y'

State before:
case 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 ⊧ₘ* 𝐈𝚫₀
y : M
a✝ : y > 0
IH : 0 < y → ∃ x < y, ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'
hy : 0 < 2 * y
x : M
hxy : x < y
y' : M
gey : y' ≤ y
H : Exponential x y'
lty : y < 2 * y'
⊢ ∃ x < 2 * y, ∃ y' ≤ 2 * y, Exponential x y' ∧ 2 * y < 2 * y'
Tactic:
exact ⟨x + 1, lt_of_lt_of_le (by simp [hxy]) (succ_le_double_of_pos (pos_of_gt hxy)),
  2 * y', by simpa using gey, Exponential.exponential_succ_mul_two.mpr H, by simpa using lty⟩
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 ⊧ₘ* 𝐈𝚫₀
y : M
a✝ : y > 0
IH : 0 < y → ∃ x < y, ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'
hy : 0 < 2 * y
⊢ 0 < y
Tactic:
simpa using hy
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 ⊧ₘ* 𝐈𝚫₀
y : M
a✝ : y > 0
IH : 0 < y → ∃ x < y, ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'
hy : 0 < 2 * y
x : M
hxy : x < y
y' : M
gey : y' ≤ y
H : Exponential x y'
lty : y < 2 * y'
⊢ x + 1 < y + 1
Tactic:
simp [hxy]
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 ⊧ₘ* 𝐈𝚫₀
y : M
a✝ : y > 0
IH : 0 < y → ∃ x < y, ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'
hy : 0 < 2 * y
x : M
hxy : x < y
y' : M
gey : y' ≤ y
H : Exponential x y'
lty : y < 2 * y'
⊢ 2 * y' ≤ 2 * y
Tactic:
simpa using gey
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 ⊧ₘ* 𝐈𝚫₀
y : M
a✝ : y > 0
IH : 0 < y → ∃ x < y, ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'
hy : 0 < 2 * y
x : M
hxy : x < y
y' : M
gey : y' ≤ y
H : Exponential x y'
lty : y < 2 * y'
⊢ 2 * y < 2 * (2 * y')
Tactic:
simpa using lty
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 ⊧ₘ* 𝐈𝚫₀
y : M
IH : 0 < y → ∃ x < y, ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'
hy : 0 < 2 * y + 1
⊢ ∃ x < 2 * y + 1, ∃ y' ≤ 2 * y + 1, Exponential x y' ∧ 2 * y + 1 < 2 * y'
Tactic:
rcases (zero_le y : 0 ≤ y) with (rfl | pos)
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 ⊧ₘ* 𝐈𝚫₀
IH : 0 < 0 → ∃ x < 0, ∃ y' ≤ 0, Exponential x y' ∧ 0 < 2 * y'
hy : 0 < 2 * 0 + 1
⊢ ∃ x < 2 * 0 + 1, ∃ y' ≤ 2 * 0 + 1, Exponential x y' ∧ 2 * 0 + 1 < 2 * y'

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y : M
IH : 0 < y → ∃ x < y, ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'
hy : 0 < 2 * y + 1
pos : 0 < y
⊢ ∃ x < 2 * y + 1, ∃ y' ≤ 2 * y + 1, Exponential x y' ∧ 2 * y + 1 < 2 * y'

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 ⊧ₘ* 𝐈𝚫₀
IH : 0 < 0 → ∃ x < 0, ∃ y' ≤ 0, Exponential x y' ∧ 0 < 2 * y'
hy : 0 < 2 * 0 + 1
⊢ ∃ x < 2 * 0 + 1, ∃ y' ≤ 2 * 0 + 1, Exponential x y' ∧ 2 * 0 + 1 < 2 * y'
Tactic:
simp
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 ⊧ₘ* 𝐈𝚫₀
IH : 0 < 0 → ∃ x < 0, ∃ y' ≤ 0, Exponential x y' ∧ 0 < 2 * y'
hy : 0 < 2 * 0 + 1
⊢ ∃ y' ≤ 1, y' = 1 ∧ 1 < 2 * y'

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 ⊧ₘ* 𝐈𝚫₀
IH : 0 < 0 → ∃ x < 0, ∃ y' ≤ 0, Exponential x y' ∧ 0 < 2 * y'
hy : 0 < 2 * 0 + 1
⊢ ∃ y' ≤ 1, y' = 1 ∧ 1 < 2 * y'
Tactic:
exact ⟨1, by simp [one_lt_two]⟩
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 ⊧ₘ* 𝐈𝚫₀
IH : 0 < 0 → ∃ x < 0, ∃ y' ≤ 0, Exponential x y' ∧ 0 < 2 * y'
hy : 0 < 2 * 0 + 1
⊢ 1 ≤ 1 ∧ 1 = 1 ∧ 1 < 2 * 1
Tactic:
simp [one_lt_two]
State after:
no goals

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 ⊧ₘ* 𝐈𝚫₀
y : M
IH : 0 < y → ∃ x < y, ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'
hy : 0 < 2 * y + 1
pos : 0 < y
⊢ ∃ x < 2 * y + 1, ∃ y' ≤ 2 * y + 1, Exponential x y' ∧ 2 * y + 1 < 2 * y'
Tactic:
rcases (IH pos : ∃ x < y, ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y') with ⟨x, hxy, y', gey, H, lty⟩
State after:
case inr.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 ⊧ₘ* 𝐈𝚫₀
y : M
IH : 0 < y → ∃ x < y, ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'
hy : 0 < 2 * y + 1
pos : 0 < y
x : M
hxy : x < y
y' : M
gey : y' ≤ y
H : Exponential x y'
lty : y < 2 * y'
⊢ ∃ x < 2 * y + 1, ∃ y' ≤ 2 * y + 1, Exponential x y' ∧ 2 * y + 1 < 2 * y'

State before:
case inr.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 ⊧ₘ* 𝐈𝚫₀
y : M
IH : 0 < y → ∃ x < y, ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'
hy : 0 < 2 * y + 1
pos : 0 < y
x : M
hxy : x < y
y' : M
gey : y' ≤ y
H : Exponential x y'
lty : y < 2 * y'
⊢ ∃ x < 2 * y + 1, ∃ y' ≤ 2 * y + 1, Exponential x y' ∧ 2 * y + 1 < 2 * y'
Tactic:
exact ⟨x + 1, by simp; exact lt_of_lt_of_le hxy (by simp),
  2 * y', le_trans (by simpa using gey) le_self_add, Exponential.exponential_succ_mul_two.mpr H, two_mul_add_one_lt_two_mul_of_lt lty⟩
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 ⊧ₘ* 𝐈𝚫₀
y : M
IH : 0 < y → ∃ x < y, ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'
hy : 0 < 2 * y + 1
pos : 0 < y
x : M
hxy : x < y
y' : M
gey : y' ≤ y
H : Exponential x y'
lty : y < 2 * y'
⊢ x + 1 < 2 * y + 1
Tactic:
simp
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y : M
IH : 0 < y → ∃ x < y, ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'
hy : 0 < 2 * y + 1
pos : 0 < y
x : M
hxy : x < y
y' : M
gey : y' ≤ y
H : Exponential x y'
lty : y < 2 * y'
⊢ x < 2 * y

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
IH : 0 < y → ∃ x < y, ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'
hy : 0 < 2 * y + 1
pos : 0 < y
x : M
hxy : x < y
y' : M
gey : y' ≤ y
H : Exponential x y'
lty : y < 2 * y'
⊢ x < 2 * y
Tactic:
exact lt_of_lt_of_le hxy (by simp)
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 ⊧ₘ* 𝐈𝚫₀
y : M
IH : 0 < y → ∃ x < y, ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'
hy : 0 < 2 * y + 1
pos : 0 < y
x : M
hxy : x < y
y' : M
gey : y' ≤ y
H : Exponential x y'
lty : y < 2 * y'
⊢ y ≤ 2 * y
Tactic:
simp
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 ⊧ₘ* 𝐈𝚫₀
y : M
IH : 0 < y → ∃ x < y, ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'
hy : 0 < 2 * y + 1
pos : 0 < y
x : M
hxy : x < y
y' : M
gey : y' ≤ y
H : Exponential x y'
lty : y < 2 * y'
⊢ 2 * y' ≤ 2 * y
Tactic:
simpa using gey
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 ⊧ₘ* 𝐈𝚫₀
y : M
hy : 0 < y
x : M
hx : x < y ∧ ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'
x' : M
⊢ (x' < y ∧ ∃ y' ≤ y, Exponential x' y' ∧ y < 2 * y') → x' = x
Tactic:
intro hx'
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y : M
hy : 0 < y
x : M
hx : x < y ∧ ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'
x' : M
hx' : x' < y ∧ ∃ y' ≤ y, Exponential x' y' ∧ y < 2 * y'
⊢ x' = x

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
hy : 0 < y
x : M
hx : x < y ∧ ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'
x' : M
hx' : x' < y ∧ ∃ y' ≤ y, Exponential x' y' ∧ y < 2 * y'
⊢ x' = x
Tactic:
by_contra A
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y : M
hy : 0 < y
x : M
hx : x < y ∧ ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'
x' : M
hx' : x' < y ∧ ∃ y' ≤ y, Exponential x' y' ∧ y < 2 * y'
A : ¬x' = x
⊢ False

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
hy : 0 < y
x : M
hx : x < y ∧ ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'
x' : M
hx' : x' < y ∧ ∃ y' ≤ y, Exponential x' y' ∧ y < 2 * y'
A : ¬x' = x
⊢ False
Tactic:
wlog lt : x < x'
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 ⊧ₘ* 𝐈𝚫₀
y : M
hy : 0 < y
x : M
hx : x < y ∧ ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'
x' : M
hx' : x' < y ∧ ∃ y' ≤ y, Exponential x' y' ∧ y < 2 * y'
A : ¬x' = x
this :
  ∀ {M : Type u_1} [inst : Zero M] [inst_1 : One M] [inst_2 : Add M] [inst_3 : Mul M] [inst_4 : LT M]
    [inst_5 : M ⊧ₘ* 𝐈𝚫₀] {y : M},
    0 < y →
      ∀ (x : M),
        (x < y ∧ ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y') →
          ∀ (x' : M), (x' < y ∧ ∃ y' ≤ y, Exponential x' y' ∧ y < 2 * y') → ¬x' = x → x < x' → False
lt : ¬x < x'
⊢ False

M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y : M
hy : 0 < y
x : M
hx : x < y ∧ ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'
x' : M
hx' : x' < y ∧ ∃ y' ≤ y, Exponential x' y' ∧ y < 2 * y'
A : ¬x' = x
lt : x < x'
⊢ False

State before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y : M
hy : 0 < y
x : M
hx : x < y ∧ ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'
x' : M
hx' : x' < y ∧ ∃ y' ≤ y, Exponential x' y' ∧ y < 2 * y'
A : ¬x' = x
lt : x < x'
⊢ False
Tactic:
rcases hx with ⟨_, z, _, H, hyz⟩
State after:
case 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✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y : M
hy : 0 < y
x x' : M
hx' : x' < y ∧ ∃ y' ≤ y, Exponential x' y' ∧ y < 2 * y'
A : ¬x' = x
lt : x < x'
left✝¹ : x < y
z : M
left✝ : z ≤ y
H : Exponential x z
hyz : y < 2 * z
⊢ False

State before:
case 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✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y : M
hy : 0 < y
x x' : M
hx' : x' < y ∧ ∃ y' ≤ y, Exponential x' y' ∧ y < 2 * y'
A : ¬x' = x
lt : x < x'
left✝¹ : x < y
z : M
left✝ : z ≤ y
H : Exponential x z
hyz : y < 2 * z
⊢ False
Tactic:
rcases hx' with ⟨_, z', hzy', H', _⟩
State after:
case intro.intro.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✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y : M
hy : 0 < y
x x' : M
A : ¬x' = x
lt : x < x'
left✝² : x < y
z : M
left✝¹ : z ≤ y
H : Exponential x z
hyz : y < 2 * z
left✝ : x' < y
z' : M
hzy' : z' ≤ y
H' : Exponential x' z'
right✝ : y < 2 * z'
⊢ False

State before:
case intro.intro.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✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y : M
hy : 0 < y
x x' : M
A : ¬x' = x
lt : x < x'
left✝² : x < y
z : M
left✝¹ : z ≤ y
H : Exponential x z
hyz : y < 2 * z
left✝ : x' < y
z' : M
hzy' : z' ≤ y
H' : Exponential x' z'
right✝ : y < 2 * z'
⊢ False
Tactic:
have : z < z' := Exponential.monotone H H' lt
State after:
case intro.intro.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✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y : M
hy : 0 < y
x x' : M
A : ¬x' = x
lt : x < x'
left✝² : x < y
z : M
left✝¹ : z ≤ y
H : Exponential x z
hyz : y < 2 * z
left✝ : x' < y
z' : M
hzy' : z' ≤ y
H' : Exponential x' z'
right✝ : y < 2 * z'
this : z < z'
⊢ False

State before:
case intro.intro.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✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y : M
hy : 0 < y
x x' : M
A : ¬x' = x
lt : x < x'
left✝² : x < y
z : M
left✝¹ : z ≤ y
H : Exponential x z
hyz : y < 2 * z
left✝ : x' < y
z' : M
hzy' : z' ≤ y
H' : Exponential x' z'
right✝ : y < 2 * z'
this : z < z'
⊢ False
Tactic:
have : y < y := calc
  y < 2 * z := hyz
  _ ≤ z'    := (Pow2.lt_iff_two_mul_le H.range_pow2 H'.range_pow2).mp this
  _ ≤ y     := hzy'
State after:
case intro.intro.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✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y : M
hy : 0 < y
x x' : M
A : ¬x' = x
lt : x < x'
left✝² : x < y
z : M
left✝¹ : z ≤ y
H : Exponential x z
hyz : y < 2 * z
left✝ : x' < y
z' : M
hzy' : z' ≤ y
H' : Exponential x' z'
right✝ : y < 2 * z'
this✝ : z < z'
this : y < y
⊢ False

State before:
case intro.intro.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✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y : M
hy : 0 < y
x x' : M
A : ¬x' = x
lt : x < x'
left✝² : x < y
z : M
left✝¹ : z ≤ y
H : Exponential x z
hyz : y < 2 * z
left✝ : x' < y
z' : M
hzy' : z' ≤ y
H' : Exponential x' z'
right✝ : y < 2 * z'
this✝ : z < z'
this : y < y
⊢ False
Tactic:
simp at this
State after:
no goals

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 ⊧ₘ* 𝐈𝚫₀
y : M
hy : 0 < y
x : M
hx : x < y ∧ ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'
x' : M
hx' : x' < y ∧ ∃ y' ≤ y, Exponential x' y' ∧ y < 2 * y'
A : ¬x' = x
this :
  ∀ {M : Type u_1} [inst : Zero M] [inst_1 : One M] [inst_2 : Add M] [inst_3 : Mul M] [inst_4 : LT M]
    [inst_5 : M ⊧ₘ* 𝐈𝚫₀] {y : M},
    0 < y →
      ∀ (x : M),
        (x < y ∧ ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y') →
          ∀ (x' : M), (x' < y ∧ ∃ y' ≤ y, Exponential x' y' ∧ y < 2 * y') → ¬x' = x → x < x' → False
lt : ¬x < x'
⊢ False
Tactic:
exact this hy x' hx' x hx (Ne.symm A) (lt_of_le_of_ne (by simpa using lt) A)
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 ⊧ₘ* 𝐈𝚫₀
y : M
hy : 0 < y
x : M
hx : x < y ∧ ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'
x' : M
hx' : x' < y ∧ ∃ y' ≤ y, Exponential x' y' ∧ y < 2 * y'
A : ¬x' = x
this :
  ∀ {M : Type u_1} [inst : Zero M] [inst_1 : One M] [inst_2 : Add M] [inst_3 : Mul M] [inst_4 : LT M]
    [inst_5 : M ⊧ₘ* 𝐈𝚫₀] {y : M},
    0 < y →
      ∀ (x : M),
        (x < y ∧ ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y') →
          ∀ (x' : M), (x' < y ∧ ∃ y' ≤ y, Exponential x' y' ∧ y < 2 * y') → ¬x' = x → x < x' → False
lt : ¬x < x'
⊢ x' ≤ x
Tactic:
simpa using lt
State after:
no goals