Theorem: LO.FirstOrder.Arith.Model.brange_exists_unique (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 : M
⊢ ∀ x < ‖a‖, ∃! y, Exponential x y
Tactic:
suffices ∀ x < ‖a‖, ∃ y ≤ a, Exponential x y by
  intro x hx; rcases this x hx with ⟨_, _, H⟩
  exact ExistsUnique.intro _ H (fun y' H' ↦ H'.uniq H)
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a : M
⊢ ∀ x < ‖a‖, ∃ y ≤ a, Exponential x y

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
⊢ ∀ x < ‖a‖, ∃ y ≤ a, Exponential x y
Tactic:
intro x
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a x : M
⊢ x < ‖a‖ → ∃ y ≤ a, Exponential x y

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a x : M
⊢ x < ‖a‖ → ∃ y ≤ a, Exponential x y
Tactic:
induction x using induction_iSigmaZero
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 ⊧ₘ* 𝐈𝚫₀
a : M
⊢ 𝚺₀-Predicate fun x => x < ‖a‖ → ∃ y ≤ a, Exponential x y

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

case succ
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a x✝ : M
a✝ : x✝ < ‖a‖ → ∃ y ≤ a, Exponential x✝ y
⊢ x✝ + 1 < ‖a‖ → ∃ y ≤ a, Exponential (x✝ + 1) y

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
⊢ 0 < ‖a‖ → ∃ y ≤ a, Exponential 0 y
Tactic:
case zero =>
  intro ha
  have : 0 < a := pos_of_lt_length ha
  exact ⟨1, pos_iff_one_le.mp this, 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 ⊧ₘ* 𝐈𝚫₀
a x : M
IH : x < ‖a‖ → ∃ y ≤ a, Exponential x y
⊢ x + 1 < ‖a‖ → ∃ y ≤ a, Exponential (x + 1) y
Tactic:
case succ x IH =>
  intro hx
  rcases (IH (lt_of_le_of_lt (by simp) hx) : ∃ y ≤ a, Exponential x y) with ⟨y, hy, H⟩
  have : 0 < a := by by_contra A; rcases (show a = 0 from by simpa using A); simp_all
  have : 2 * y ≤ a := (le_iff_le_log_of_exp H.succ this).mpr (le_log_of_lt_length hx)
  exact ⟨2 * y, this, H.succ⟩
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 : M
this : ∀ x < ‖a‖, ∃ y ≤ a, Exponential x y
⊢ ∀ x < ‖a‖, ∃! y, Exponential x y
Tactic:
intro x hx
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a : M
this : ∀ x < ‖a‖, ∃ y ≤ a, Exponential x y
x : M
hx : x < ‖a‖
⊢ ∃! y, Exponential x y

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
this : ∀ x < ‖a‖, ∃ y ≤ a, Exponential x y
x : M
hx : x < ‖a‖
⊢ ∃! y, Exponential x y
Tactic:
rcases this x hx with ⟨_, _, H⟩
State after:
case intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a : M
this : ∀ x < ‖a‖, ∃ y ≤ a, Exponential x y
x : M
hx : x < ‖a‖
w✝ : M
left✝ : w✝ ≤ a
H : Exponential x w✝
⊢ ∃! y, Exponential x y

State before:
case intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a : M
this : ∀ x < ‖a‖, ∃ y ≤ a, Exponential x y
x : M
hx : x < ‖a‖
w✝ : M
left✝ : w✝ ≤ a
H : Exponential x w✝
⊢ ∃! y, Exponential x y
Tactic:
exact ExistsUnique.intro _ H (fun y' H' ↦ H'.uniq H)
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 ⊧ₘ* 𝐈𝚫₀
a : M
⊢ 𝚺₀-Predicate fun x => x < ‖a‖ → ∃ y ≤ a, Exponential x 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 ⊧ₘ* 𝐈𝚫₀
a : M
⊢ 0 < ‖a‖ → ∃ y ≤ a, Exponential 0 y
Tactic:
intro ha
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a : M
ha : 0 < ‖a‖
⊢ ∃ y ≤ a, Exponential 0 y

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
ha : 0 < ‖a‖
⊢ ∃ y ≤ a, Exponential 0 y
Tactic:
have : 0 < a := pos_of_lt_length ha
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a : M
ha : 0 < ‖a‖
this : 0 < a
⊢ ∃ y ≤ a, Exponential 0 y

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
ha : 0 < ‖a‖
this : 0 < a
⊢ ∃ y ≤ a, Exponential 0 y
Tactic:
exact ⟨1, pos_iff_one_le.mp this, 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 ⊧ₘ* 𝐈𝚫₀
a : M
ha : 0 < ‖a‖
this : 0 < a
⊢ Exponential 0 1
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 ⊧ₘ* 𝐈𝚫₀
a x : M
IH : x < ‖a‖ → ∃ y ≤ a, Exponential x y
⊢ x + 1 < ‖a‖ → ∃ y ≤ a, Exponential (x + 1) y
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 ⊧ₘ* 𝐈𝚫₀
a x : M
IH : x < ‖a‖ → ∃ y ≤ a, Exponential x y
hx : x + 1 < ‖a‖
⊢ ∃ y ≤ a, Exponential (x + 1) y

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a x : M
IH : x < ‖a‖ → ∃ y ≤ a, Exponential x y
hx : x + 1 < ‖a‖
⊢ ∃ y ≤ a, Exponential (x + 1) y
Tactic:
rcases (IH (lt_of_le_of_lt (by simp) hx) : ∃ y ≤ a, Exponential x y) with ⟨y, hy, H⟩
State after:
case intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a x : M
IH : x < ‖a‖ → ∃ y ≤ a, Exponential x y
hx : x + 1 < ‖a‖
y : M
hy : y ≤ a
H : Exponential x y
⊢ ∃ y ≤ a, Exponential (x + 1) y

State before:
case intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a x : M
IH : x < ‖a‖ → ∃ y ≤ a, Exponential x y
hx : x + 1 < ‖a‖
y : M
hy : y ≤ a
H : Exponential x y
⊢ ∃ y ≤ a, Exponential (x + 1) y
Tactic:
have : 0 < a := by by_contra A; rcases (show a = 0 from by simpa using A); simp_all
State after:
case intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a x : M
IH : x < ‖a‖ → ∃ y ≤ a, Exponential x y
hx : x + 1 < ‖a‖
y : M
hy : y ≤ a
H : Exponential x y
this : 0 < a
⊢ ∃ y ≤ a, Exponential (x + 1) y

State before:
case intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a x : M
IH : x < ‖a‖ → ∃ y ≤ a, Exponential x y
hx : x + 1 < ‖a‖
y : M
hy : y ≤ a
H : Exponential x y
this : 0 < a
⊢ ∃ y ≤ a, Exponential (x + 1) y
Tactic:
have : 2 * y ≤ a := (le_iff_le_log_of_exp H.succ this).mpr (le_log_of_lt_length hx)
State after:
case intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a x : M
IH : x < ‖a‖ → ∃ y ≤ a, Exponential x y
hx : x + 1 < ‖a‖
y : M
hy : y ≤ a
H : Exponential x y
this✝ : 0 < a
this : 2 * y ≤ a
⊢ ∃ y ≤ a, Exponential (x + 1) y

State before:
case intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a x : M
IH : x < ‖a‖ → ∃ y ≤ a, Exponential x y
hx : x + 1 < ‖a‖
y : M
hy : y ≤ a
H : Exponential x y
this✝ : 0 < a
this : 2 * y ≤ a
⊢ ∃ y ≤ a, Exponential (x + 1) y
Tactic:
exact ⟨2 * y, this, H.succ⟩
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 x : M
IH : x < ‖a‖ → ∃ y ≤ a, Exponential x y
hx : x + 1 < ‖a‖
⊢ x ≤ x + 1
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 ⊧ₘ* 𝐈𝚫₀
a x : M
IH : x < ‖a‖ → ∃ y ≤ a, Exponential x y
hx : x + 1 < ‖a‖
y : M
hy : y ≤ a
H : Exponential x y
⊢ 0 < a
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 ⊧ₘ* 𝐈𝚫₀
a x : M
IH : x < ‖a‖ → ∃ y ≤ a, Exponential x y
hx : x + 1 < ‖a‖
y : M
hy : y ≤ a
H : Exponential x y
A : ¬0 < a
⊢ False

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a x : M
IH : x < ‖a‖ → ∃ y ≤ a, Exponential x y
hx : x + 1 < ‖a‖
y : M
hy : y ≤ a
H : Exponential x y
A : ¬0 < a
⊢ False
Tactic:
rcases (show a = 0 from by simpa using A)
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 ⊧ₘ* 𝐈𝚫₀
x y : M
H : Exponential x y
IH : x < ‖0‖ → ∃ y ≤ 0, Exponential x y
hx : x + 1 < ‖0‖
hy : y ≤ 0
A : ¬0 < 0
⊢ False

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 ⊧ₘ* 𝐈𝚫₀
x y : M
H : Exponential x y
IH : x < ‖0‖ → ∃ y ≤ 0, Exponential x y
hx : x + 1 < ‖0‖
hy : y ≤ 0
A : ¬0 < 0
⊢ False
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 x : M
IH : x < ‖a‖ → ∃ y ≤ a, Exponential x y
hx : x + 1 < ‖a‖
y : M
hy : y ≤ a
H : Exponential x y
A : ¬0 < a
⊢ a = 0
Tactic:
simpa using A
State after:
no goals