internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.lt_exponential_length
Proof 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 : Exponential ‖a‖ b
pos : 0 < a
⊢ a < b
Tactic:
simp [length_of_pos pos] at h
Proof 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 ⊧ₘ* 𝐈𝚫₀
a b : M
pos : 0 < a
h : Exponential (log a + 1) b
⊢ a < b
Theorem: LO.FirstOrder.Arith.Model.lt_exponential_length
Proof 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
pos : 0 < a
h : Exponential (log a + 1) b
⊢ a < b
Tactic:
rcases Exponential.exponential_succ.mp h with ⟨b, rfl, H⟩
Proof state after:
case inr.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
pos : 0 < a
b : M
H : Exponential (log a) b
h : Exponential (log a + 1) (2 * b)
⊢ a < 2 * b
Theorem: LO.FirstOrder.Arith.Model.lt_exponential_length
Proof state before:
case inr.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
pos : 0 < a
b : M
H : Exponential (log a) b
h : Exponential (log a + 1) (2 * b)
⊢ a < 2 * b
Tactic:
exact lt_exponential_log_self H
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lt_exponential_length
Proof 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 : Exponential ‖0‖ b
⊢ 0 < b
Tactic:
simp at h
Proof 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 : b = 1
⊢ 0 < b
Theorem: LO.FirstOrder.Arith.Model.lt_exponential_length
Proof 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 : b = 1
⊢ 0 < b
Tactic:
simp [h]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sq_len_le_three_mul
Proof 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
⊢ ‖a‖ ^ 2 ≤ 3 * a
Tactic:
induction a using hierarchy_polynomial_induction_oRing_sigma₀
Proof 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 a => ‖a‖ ^ 2 ≤ 3 * a

case zero
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ ‖0‖ ^ 2 ≤ 3 * 0

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✝ : ‖x✝‖ ^ 2 ≤ 3 * x✝
⊢ ‖2 * x✝‖ ^ 2 ≤ 3 * (2 * x✝)

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✝ : ‖x✝‖ ^ 2 ≤ 3 * x✝
⊢ ‖2 * x✝ + 1‖ ^ 2 ≤ 3 * (2 * x✝ + 1)
Theorem: LO.FirstOrder.Arith.Model.sq_len_le_three_mul
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ ‖0‖ ^ 2 ≤ 3 * 0
Tactic:
case zero => simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sq_len_le_three_mul
Proof 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
pos : a > 0
IH : ‖a‖ ^ 2 ≤ 3 * a
⊢ ‖2 * a‖ ^ 2 ≤ 3 * (2 * a)
Tactic:
case even a pos IH =>
  calc
    ‖2 * a‖ ^ 2 = (‖a‖ + 1) ^ 2         := by rw [length_two_mul_of_pos pos]
    _           = ‖a‖ ^ 2 + 2 * ‖a‖ + 1 := by simp [sq, add_mul_self_eq]
    _           ≤ 3 * a + 2 * ‖a‖ + 1   := by simpa using IH
    _           ≤ 3 * a + 2 * a + 1     := by simp
    _           ≤ 3 * a + 2 * a + a     := by simp [←pos_iff_one_le, pos]
    _           = 3 * (2 * a)           := by simp_all only [←two_add_one_eq_three, two_mul, add_mul, add_assoc, one_mul]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sq_len_le_three_mul
Proof 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 a => ‖a‖ ^ 2 ≤ 3 * a
Tactic:
definability
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sq_len_le_three_mul
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ ‖0‖ ^ 2 ≤ 3 * 0
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sq_len_le_three_mul
Proof 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
pos : a > 0
IH : ‖a‖ ^ 2 ≤ 3 * a
⊢ ‖2 * a‖ ^ 2 ≤ 3 * (2 * a)
Tactic:
calc
  ‖2 * a‖ ^ 2 = (‖a‖ + 1) ^ 2         := by rw [length_two_mul_of_pos pos]
  _           = ‖a‖ ^ 2 + 2 * ‖a‖ + 1 := by simp [sq, add_mul_self_eq]
  _           ≤ 3 * a + 2 * ‖a‖ + 1   := by simpa using IH
  _           ≤ 3 * a + 2 * a + 1     := by simp
  _           ≤ 3 * a + 2 * a + a     := by simp [←pos_iff_one_le, pos]
  _           = 3 * (2 * a)           := by simp_all only [←two_add_one_eq_three, two_mul, add_mul, add_assoc, one_mul]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sq_len_le_three_mul
Proof 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
pos : a > 0
IH : ‖a‖ ^ 2 ≤ 3 * a
⊢ ‖2 * a‖ ^ 2 = (‖a‖ + 1) ^ 2
Tactic:
rw [length_two_mul_of_pos pos]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sq_len_le_three_mul
Proof 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
pos : a > 0
IH : ‖a‖ ^ 2 ≤ 3 * a
⊢ (‖a‖ + 1) ^ 2 = ‖a‖ ^ 2 + 2 * ‖a‖ + 1
Tactic:
simp [sq, add_mul_self_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sq_len_le_three_mul
Proof 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
pos : a > 0
IH : ‖a‖ ^ 2 ≤ 3 * a
⊢ ‖a‖ ^ 2 + 2 * ‖a‖ + 1 ≤ 3 * a + 2 * ‖a‖ + 1
Tactic:
simpa using IH
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sq_len_le_three_mul
Proof 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
pos : a > 0
IH : ‖a‖ ^ 2 ≤ 3 * a
⊢ 3 * a + 2 * ‖a‖ + 1 ≤ 3 * a + 2 * a + 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sq_len_le_three_mul
Proof 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
pos : a > 0
IH : ‖a‖ ^ 2 ≤ 3 * a
⊢ 3 * a + 2 * a + 1 ≤ 3 * a + 2 * a + a
Tactic:
simp [←pos_iff_one_le, pos]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sq_len_le_three_mul
Proof 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
pos : a > 0
IH : ‖a‖ ^ 2 ≤ 3 * a
⊢ 3 * a + 2 * a + a = 3 * (2 * a)
Tactic:
simp_all only [←two_add_one_eq_three, two_mul, add_mul, add_assoc, one_mul]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sq_len_le_three_mul
Proof 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
IH : ‖a‖ ^ 2 ≤ 3 * a
⊢ ‖2 * a + 1‖ ^ 2 ≤ 3 * (2 * a + 1)
Tactic:
rcases zero_le a with (rfl | pos)
Proof 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‖ ^ 2 ≤ 3 * 0
⊢ ‖2 * 0 + 1‖ ^ 2 ≤ 3 * (2 * 0 + 1)

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a : M
IH : ‖a‖ ^ 2 ≤ 3 * a
pos : 0 < a
⊢ ‖2 * a + 1‖ ^ 2 ≤ 3 * (2 * a + 1)
Theorem: LO.FirstOrder.Arith.Model.sq_len_le_three_mul
Proof 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 : M
IH : ‖a‖ ^ 2 ≤ 3 * a
pos : 0 < a
⊢ ‖2 * a + 1‖ ^ 2 ≤ 3 * (2 * a + 1)
Tactic:
calc
  ‖2 * a + 1‖ ^ 2 = (‖a‖ + 1) ^ 2         := by rw [length_two_mul_add_one a]
  _               = ‖a‖ ^ 2 + 2 * ‖a‖ + 1 := by simp [sq, add_mul_self_eq]
  _               ≤ 3 * a + 2 * ‖a‖ + 1   := by simpa using IH
  _               ≤ 3 * a + 2 * a + 1     := by simp
  _               ≤ 3 * a + 2 * a + a     := by simp [←pos_iff_one_le, pos]
  _               = 3 * (2 * a)           := by simp_all only [←two_add_one_eq_three, two_mul, add_mul, add_assoc, one_mul]
  _               ≤ 3 * (2 * a + 1)       := by simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sq_len_le_three_mul
Proof 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‖ ^ 2 ≤ 3 * 0
⊢ ‖2 * 0 + 1‖ ^ 2 ≤ 3 * (2 * 0 + 1)
Tactic:
simp [←two_add_one_eq_three]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sq_len_le_three_mul
Proof 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
IH : ‖a‖ ^ 2 ≤ 3 * a
pos : 0 < a
⊢ ‖2 * a + 1‖ ^ 2 = (‖a‖ + 1) ^ 2
Tactic:
rw [length_two_mul_add_one a]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sq_len_le_three_mul
Proof 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
IH : ‖a‖ ^ 2 ≤ 3 * a
pos : 0 < a
⊢ (‖a‖ + 1) ^ 2 = ‖a‖ ^ 2 + 2 * ‖a‖ + 1
Tactic:
simp [sq, add_mul_self_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sq_len_le_three_mul
Proof 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
IH : ‖a‖ ^ 2 ≤ 3 * a
pos : 0 < a
⊢ ‖a‖ ^ 2 + 2 * ‖a‖ + 1 ≤ 3 * a + 2 * ‖a‖ + 1
Tactic:
simpa using IH
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sq_len_le_three_mul
Proof 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
IH : ‖a‖ ^ 2 ≤ 3 * a
pos : 0 < a
⊢ 3 * a + 2 * ‖a‖ + 1 ≤ 3 * a + 2 * a + 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sq_len_le_three_mul
Proof 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
IH : ‖a‖ ^ 2 ≤ 3 * a
pos : 0 < a
⊢ 3 * a + 2 * a + 1 ≤ 3 * a + 2 * a + a
Tactic:
simp [←pos_iff_one_le, pos]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sq_len_le_three_mul
Proof 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
IH : ‖a‖ ^ 2 ≤ 3 * a
pos : 0 < a
⊢ 3 * a + 2 * a + a = 3 * (2 * a)
Tactic:
simp_all only [←two_add_one_eq_three, two_mul, add_mul, add_assoc, one_mul]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sq_len_le_three_mul
Proof 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
IH : ‖a‖ ^ 2 ≤ 3 * a
pos : 0 < a
⊢ 3 * (2 * a) ≤ 3 * (2 * a + 1)
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.brange_exists_unique
Proof 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)
Proof 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
Theorem: LO.FirstOrder.Arith.Model.brange_exists_unique
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.brange_exists_unique
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.brange_exists_unique
Proof 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⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.brange_exists_unique
Proof 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⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.brange_exists_unique
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.brange_exists_unique
Proof 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⟩
Proof 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
Theorem: LO.FirstOrder.Arith.Model.brange_exists_unique
Proof 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)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.brange_exists_unique
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.brange_exists_unique
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.brange_exists_unique
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.brange_exists_unique
Proof 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⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.brange_exists_unique
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.brange_exists_unique
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.brange_exists_unique
Proof 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⟩
Proof 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
Theorem: LO.FirstOrder.Arith.Model.brange_exists_unique
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.brange_exists_unique
Proof 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)
Proof 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
Theorem: LO.FirstOrder.Arith.Model.brange_exists_unique
Proof 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⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.brange_exists_unique
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.brange_exists_unique
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.brange_exists_unique
Proof 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)
Proof 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
Theorem: LO.FirstOrder.Arith.Model.brange_exists_unique
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.brange_exists_unique
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.bexp_exists_unique
Proof 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
⊢ ∃! y, (x < ‖a‖ → Exponential x y) ∧ (‖a‖ ≤ x → y = 0)
Tactic:
by_cases hx : x < ‖a‖
Proof state after:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a x : M
hx : x < ‖a‖
⊢ ∃! y, (x < ‖a‖ → Exponential x y) ∧ (‖a‖ ≤ x → y = 0)

case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a x : M
hx : ¬x < ‖a‖
⊢ ∃! y, (x < ‖a‖ → Exponential x y) ∧ (‖a‖ ≤ x → y = 0)
Theorem: LO.FirstOrder.Arith.Model.bexp_exists_unique
Proof state before:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a x : M
hx : x < ‖a‖
⊢ ∃! y, (x < ‖a‖ → Exponential x y) ∧ (‖a‖ ≤ x → y = 0)
Tactic:
simp [hx, show ¬‖a‖ ≤ x from by simpa using hx, log_exists_unique_pos]
Proof state after:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a x : M
hx : x < ‖a‖
⊢ ∃! y, Exponential x y
Theorem: LO.FirstOrder.Arith.Model.bexp_exists_unique
Proof state before:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a x : M
hx : x < ‖a‖
⊢ ∃! y, Exponential x y
Tactic:
exact brange_exists_unique a x hx
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.bexp_exists_unique
Proof 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
hx : x < ‖a‖
⊢ ¬‖a‖ ≤ x
Tactic:
simpa using hx
Proof state after:
no goals