internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.log_exists_unique_pos
Proof 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⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_exists_unique_pos
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_exists_unique_pos
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_exists_unique_pos
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_exists_unique_pos
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_exists_unique_pos
Proof 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)
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 < 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'
Theorem: LO.FirstOrder.Arith.Model.log_exists_unique_pos
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 < 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
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 < 0 → ∃ x < 0, ∃ y' ≤ 0, Exponential x y' ∧ 0 < 2 * y'
hy : 0 < 2 * 0 + 1
⊢ ∃ y' ≤ 1, y' = 1 ∧ 1 < 2 * y'
Theorem: LO.FirstOrder.Arith.Model.log_exists_unique_pos
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 < 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]⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_exists_unique_pos
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_exists_unique_pos
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 ⊧ₘ* 𝐈𝚫₀
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⟩
Proof 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'
Theorem: LO.FirstOrder.Arith.Model.log_exists_unique_pos
Proof 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⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_exists_unique_pos
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.log_exists_unique_pos
Proof 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)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_exists_unique_pos
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_exists_unique_pos
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_exists_unique_pos
Proof 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'
Proof 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
Theorem: LO.FirstOrder.Arith.Model.log_exists_unique_pos
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.log_exists_unique_pos
Proof 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'
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 ⊧ₘ* 𝐈𝚫₀
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
Theorem: LO.FirstOrder.Arith.Model.log_exists_unique_pos
Proof 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⟩
Proof 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
Theorem: LO.FirstOrder.Arith.Model.log_exists_unique_pos
Proof 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', _⟩
Proof 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
Theorem: LO.FirstOrder.Arith.Model.log_exists_unique_pos
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.log_exists_unique_pos
Proof 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'
Proof 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
Theorem: LO.FirstOrder.Arith.Model.log_exists_unique_pos
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_exists_unique_pos
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 ⊧ₘ* 𝐈𝚫₀
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)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_exists_unique_pos
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_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 ⊧ₘ* 𝐈𝚫₀
y : M
⊢ ∃! x, (y = 0 → x = 0) ∧ (0 < y → x < y ∧ ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y')
Tactic:
by_cases hy : y = 0
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 ⊧ₘ* 𝐈𝚫₀
y : M
hy : y = 0
⊢ ∃! x, (y = 0 → x = 0) ∧ (0 < y → x < y ∧ ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y')

case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y : M
hy : ¬y = 0
⊢ ∃! x, (y = 0 → x = 0) ∧ (0 < y → x < y ∧ ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y')
Theorem: LO.FirstOrder.Arith.Model.log_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 ⊧ₘ* 𝐈𝚫₀
y : M
hy : y = 0
⊢ ∃! x, (y = 0 → x = 0) ∧ (0 < y → x < y ∧ ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y')
Tactic:
rcases hy
Proof state after:
case pos.refl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ ∃! x, (0 = 0 → x = 0) ∧ (0 < 0 → x < 0 ∧ ∃ y' ≤ 0, Exponential x y' ∧ 0 < 2 * y')
Theorem: LO.FirstOrder.Arith.Model.log_exists_unique
Proof state before:
case pos.refl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ ∃! x, (0 = 0 → x = 0) ∧ (0 < 0 → x < 0 ∧ ∃ y' ≤ 0, Exponential x y' ∧ 0 < 2 * y')
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_exists_unique
Proof state before:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y : M
hy : ¬y = 0
⊢ ∃! x, (y = 0 → x = 0) ∧ (0 < y → x < y ∧ ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y')
Tactic:
simp [hy, pos_iff_ne_zero.mpr hy, log_exists_unique_pos]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_le_self
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
⊢ log a ≤ a
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 ⊧ₘ* 𝐈𝚫₀
⊢ log 0 ≤ 0

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
pos : 0 < a
⊢ log a ≤ a
Theorem: LO.FirstOrder.Arith.Model.log_le_self
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 ⊧ₘ* 𝐈𝚫₀
⊢ log 0 ≤ 0
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_le_self
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
pos : 0 < a
⊢ log a ≤ a
Tactic:
exact le_of_lt <| log_lt_self_of_pos pos
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_defined
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ 𝚺₀-Function₁ log via logDef
Tactic:
intro v
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
v : Fin (Nat.succ 1) → M
⊢ (fun v => v 0 = (fun v => log (v 0)) fun x => v x.succ) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val logDef)
Theorem: LO.FirstOrder.Arith.Model.log_defined
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
v : Fin (Nat.succ 1) → M
⊢ (fun v => v 0 = (fun v => log (v 0)) fun x => v x.succ) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val logDef)
Tactic:
simp [logDef, log_graph, ←le_iff_lt_succ, numeral_eq_natCast]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_one
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 < 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_one
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ Exponential 0 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_one
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ 1 ≤ 1
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_one
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ 1 < 2 * 1
Tactic:
simp [one_lt_two]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_two
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
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_two
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ Exponential 1 2
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_two
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ 2 ≤ 2
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_two
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ 2 < 2 * 2
Tactic:
simp [one_lt_two]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_two_mul_of_pos
Proof 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
pos : 0 < y
⊢ log (2 * y) = log y + 1
Tactic:
rcases log_pos pos with ⟨y', hy', H, hy⟩
Proof 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 ⊧ₘ* 𝐈𝚫₀
y : M
pos : 0 < y
y' : M
hy' : y' ≤ y
H : Exponential (log y) y'
hy : y < 2 * y'
⊢ log (2 * y) = log y + 1
Theorem: LO.FirstOrder.Arith.Model.log_two_mul_of_pos
Proof 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 ⊧ₘ* 𝐈𝚫₀
y : M
pos : 0 < y
y' : M
hy' : y' ≤ y
H : Exponential (log y) y'
hy : y < 2 * y'
⊢ log (2 * y) = log y + 1
Tactic:
exact log_eq_of_pos (by simpa using pos) (Exponential.exponential_succ_mul_two.mpr H) (by simpa using hy') (by simpa using hy)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_two_mul_of_pos
Proof 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
pos : 0 < y
y' : M
hy' : y' ≤ y
H : Exponential (log y) y'
hy : y < 2 * y'
⊢ 0 < 2 * y
Tactic:
simpa using pos
Proof state after:
no goals