internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ
Proof state before:
case intro.inl.mpr.intro.intro.intro
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 (2 * x) y
IH : ∀ y_1 < 2 * y, ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
hxy : 2 * x < 2 * y
hy : y ≤ 2 * y
⊢ Exponential (2 * x + 1) (2 * y)
Tactic:
rcases exponential_even.mp H with ⟨y, rfl, H'⟩
Proof state after:
case intro.inl.mpr.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 ⊧ₘ* 𝐈𝚫₀
x y : M
H' : Exponential x y
H : Exponential (2 * x) (y ^ 2)
IH : ∀ y_1 < 2 * y ^ 2, ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
hxy : 2 * x < 2 * y ^ 2
hy : y ^ 2 ≤ 2 * y ^ 2
⊢ Exponential (2 * x + 1) (2 * y ^ 2)
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ
Proof state before:
case intro.inl.mpr.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 ⊧ₘ* 𝐈𝚫₀
x y : M
H' : Exponential x y
H : Exponential (2 * x) (y ^ 2)
IH : ∀ y_1 < 2 * y ^ 2, ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
hxy : 2 * x < 2 * y ^ 2
hy : y ^ 2 ≤ 2 * y ^ 2
⊢ Exponential (2 * x + 1) (2 * y ^ 2)
Tactic:
exact H'.bit_one
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ
Proof state before:
case intro.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 : ∀ y_1 < y, ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
x : M
hxy : 2 * x + 1 < y
⊢ Exponential (2 * x + 1 + 1) y ↔ ∃ z ≤ y, y = 2 * z ∧ Exponential (2 * x + 1) z
Tactic:
constructor
Proof state after:
case intro.inr.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y : M
IH : ∀ y_1 < y, ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
x : M
hxy : 2 * x + 1 < y
⊢ Exponential (2 * x + 1 + 1) y → ∃ z ≤ y, y = 2 * z ∧ Exponential (2 * x + 1) z

case intro.inr.mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y : M
IH : ∀ y_1 < y, ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
x : M
hxy : 2 * x + 1 < y
⊢ (∃ z ≤ y, y = 2 * z ∧ Exponential (2 * x + 1) z) → Exponential (2 * x + 1 + 1) y
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ
Proof state before:
case intro.inr.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y : M
IH : ∀ y_1 < y, ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
x : M
hxy : 2 * x + 1 < y
⊢ Exponential (2 * x + 1 + 1) y → ∃ z ≤ y, y = 2 * z ∧ Exponential (2 * x + 1) z
Tactic:
intro H
Proof state after:
case intro.inr.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y : M
IH : ∀ y_1 < y, ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
x : M
hxy : 2 * x + 1 < y
H : Exponential (2 * x + 1 + 1) y
⊢ ∃ z ≤ y, y = 2 * z ∧ Exponential (2 * x + 1) z
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ
Proof state before:
case intro.inr.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y : M
IH : ∀ y_1 < y, ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
x : M
hxy : 2 * x + 1 < y
H : Exponential (2 * x + 1 + 1) y
⊢ ∃ z ≤ y, y = 2 * z ∧ Exponential (2 * x + 1) z
Tactic:
have : Exponential (2 * (x + 1)) y := by simpa [mul_add, add_assoc, one_add_one_eq_two] using H
Proof state after:
case intro.inr.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y : M
IH : ∀ y_1 < y, ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
x : M
hxy : 2 * x + 1 < y
H : Exponential (2 * x + 1 + 1) y
this : Exponential (2 * (x + 1)) y
⊢ ∃ z ≤ y, y = 2 * z ∧ Exponential (2 * x + 1) z
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ
Proof state before:
case intro.inr.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y : M
IH : ∀ y_1 < y, ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
x : M
hxy : 2 * x + 1 < y
H : Exponential (2 * x + 1 + 1) y
this : Exponential (2 * (x + 1)) y
⊢ ∃ z ≤ y, y = 2 * z ∧ Exponential (2 * x + 1) z
Tactic:
rcases exponential_even.mp this with ⟨y, rfl, H'⟩
Proof state after:
case intro.inr.mp.intro.intro
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 + 1) y
IH : ∀ y_1 < y ^ 2, ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
hxy : 2 * x + 1 < y ^ 2
H : Exponential (2 * x + 1 + 1) (y ^ 2)
this : Exponential (2 * (x + 1)) (y ^ 2)
⊢ ∃ z ≤ y ^ 2, y ^ 2 = 2 * z ∧ Exponential (2 * x + 1) z
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ
Proof state before:
case intro.inr.mp.intro.intro
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 + 1) y
IH : ∀ y_1 < y ^ 2, ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
hxy : 2 * x + 1 < y ^ 2
H : Exponential (2 * x + 1 + 1) (y ^ 2)
this : Exponential (2 * (x + 1)) (y ^ 2)
⊢ ∃ z ≤ y ^ 2, y ^ 2 = 2 * z ∧ Exponential (2 * x + 1) z
Tactic:
have : 1 < y := by
  simpa using (show 1 < y^2 from lt_of_le_of_lt (by simp) hxy)
Proof state after:
case intro.inr.mp.intro.intro
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 + 1) y
IH : ∀ y_1 < y ^ 2, ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
hxy : 2 * x + 1 < y ^ 2
H : Exponential (2 * x + 1 + 1) (y ^ 2)
this✝ : Exponential (2 * (x + 1)) (y ^ 2)
this : 1 < y
⊢ ∃ z ≤ y ^ 2, y ^ 2 = 2 * z ∧ Exponential (2 * x + 1) z
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ
Proof state before:
case intro.inr.mp.intro.intro
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 + 1) y
IH : ∀ y_1 < y ^ 2, ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
hxy : 2 * x + 1 < y ^ 2
H : Exponential (2 * x + 1 + 1) (y ^ 2)
this✝ : Exponential (2 * (x + 1)) (y ^ 2)
this : 1 < y
⊢ ∃ z ≤ y ^ 2, y ^ 2 = 2 * z ∧ Exponential (2 * x + 1) z
Tactic:
have : Exponential (x + 1) y ↔ ∃ z ≤ y, y = 2 * z ∧ Exponential x z :=
  IH y (lt_square_of_lt $ this) (lt_trans _ _ _ (by simp) H'.lt)
Proof state after:
case intro.inr.mp.intro.intro
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 + 1) y
IH : ∀ y_1 < y ^ 2, ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
hxy : 2 * x + 1 < y ^ 2
H : Exponential (2 * x + 1 + 1) (y ^ 2)
this✝¹ : Exponential (2 * (x + 1)) (y ^ 2)
this✝ : 1 < y
this : Exponential (x + 1) y ↔ ∃ z ≤ y, y = 2 * z ∧ Exponential x z
⊢ ∃ z ≤ y ^ 2, y ^ 2 = 2 * z ∧ Exponential (2 * x + 1) z
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ
Proof state before:
case intro.inr.mp.intro.intro
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 + 1) y
IH : ∀ y_1 < y ^ 2, ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
hxy : 2 * x + 1 < y ^ 2
H : Exponential (2 * x + 1 + 1) (y ^ 2)
this✝¹ : Exponential (2 * (x + 1)) (y ^ 2)
this✝ : 1 < y
this : Exponential (x + 1) y ↔ ∃ z ≤ y, y = 2 * z ∧ Exponential x z
⊢ ∃ z ≤ y ^ 2, y ^ 2 = 2 * z ∧ Exponential (2 * x + 1) z
Tactic:
rcases this.mp H' with ⟨y, _, rfl, H''⟩
Proof state after:
case intro.inr.mp.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 ⊧ₘ* 𝐈𝚫₀
x y : M
H'' : Exponential x y
H' : Exponential (x + 1) (2 * y)
IH : ∀ y_1 < (2 * y) ^ 2, ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
hxy : 2 * x + 1 < (2 * y) ^ 2
H : Exponential (2 * x + 1 + 1) ((2 * y) ^ 2)
this✝¹ : Exponential (2 * (x + 1)) ((2 * y) ^ 2)
this✝ : 1 < 2 * y
this : Exponential (x + 1) (2 * y) ↔ ∃ z ≤ 2 * y, 2 * y = 2 * z ∧ Exponential x z
left✝ : y ≤ 2 * y
⊢ ∃ z ≤ (2 * y) ^ 2, (2 * y) ^ 2 = 2 * z ∧ Exponential (2 * x + 1) z
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ
Proof state before:
case intro.inr.mp.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 ⊧ₘ* 𝐈𝚫₀
x y : M
H'' : Exponential x y
H' : Exponential (x + 1) (2 * y)
IH : ∀ y_1 < (2 * y) ^ 2, ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
hxy : 2 * x + 1 < (2 * y) ^ 2
H : Exponential (2 * x + 1 + 1) ((2 * y) ^ 2)
this✝¹ : Exponential (2 * (x + 1)) ((2 * y) ^ 2)
this✝ : 1 < 2 * y
this : Exponential (x + 1) (2 * y) ↔ ∃ z ≤ 2 * y, 2 * y = 2 * z ∧ Exponential x z
left✝ : y ≤ 2 * y
⊢ ∃ z ≤ (2 * y) ^ 2, (2 * y) ^ 2 = 2 * z ∧ Exponential (2 * x + 1) z
Tactic:
exact ⟨2 * y ^ 2, by simp [sq, mul_assoc, mul_left_comm y 2],
  by simp [sq, mul_assoc, mul_left_comm y 2], H''.bit_one⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ
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 : ∀ y_1 < y, ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
x : M
hxy : 2 * x + 1 < y
H : Exponential (2 * x + 1 + 1) y
⊢ Exponential (2 * (x + 1)) y
Tactic:
simpa [mul_add, add_assoc, one_add_one_eq_two] using H
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ
Proof state before:
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 + 1) y
IH : ∀ y_1 < y ^ 2, ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
hxy : 2 * x + 1 < y ^ 2
H : Exponential (2 * x + 1 + 1) (y ^ 2)
this : Exponential (2 * (x + 1)) (y ^ 2)
⊢ 1 < y
Tactic:
simpa using (show 1 < y^2 from lt_of_le_of_lt (by simp) hxy)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ
Proof state before:
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 + 1) y
IH : ∀ y_1 < y ^ 2, ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
hxy : 2 * x + 1 < y ^ 2
H : Exponential (2 * x + 1 + 1) (y ^ 2)
this : Exponential (2 * (x + 1)) (y ^ 2)
⊢ 1 ≤ 2 * x + 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ
Proof state before:
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 + 1) y
IH : ∀ y_1 < y ^ 2, ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
hxy : 2 * x + 1 < y ^ 2
H : Exponential (2 * x + 1 + 1) (y ^ 2)
this✝ : Exponential (2 * (x + 1)) (y ^ 2)
this : 1 < y
⊢ x < x + 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ
Proof state before:
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
H' : Exponential (x + 1) (2 * y)
IH : ∀ y_1 < (2 * y) ^ 2, ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
hxy : 2 * x + 1 < (2 * y) ^ 2
H : Exponential (2 * x + 1 + 1) ((2 * y) ^ 2)
this✝¹ : Exponential (2 * (x + 1)) ((2 * y) ^ 2)
this✝ : 1 < 2 * y
this : Exponential (x + 1) (2 * y) ↔ ∃ z ≤ 2 * y, 2 * y = 2 * z ∧ Exponential x z
left✝ : y ≤ 2 * y
⊢ 2 * y ^ 2 ≤ (2 * y) ^ 2
Tactic:
simp [sq, mul_assoc, mul_left_comm y 2]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ
Proof state before:
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
H' : Exponential (x + 1) (2 * y)
IH : ∀ y_1 < (2 * y) ^ 2, ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
hxy : 2 * x + 1 < (2 * y) ^ 2
H : Exponential (2 * x + 1 + 1) ((2 * y) ^ 2)
this✝¹ : Exponential (2 * (x + 1)) ((2 * y) ^ 2)
this✝ : 1 < 2 * y
this : Exponential (x + 1) (2 * y) ↔ ∃ z ≤ 2 * y, 2 * y = 2 * z ∧ Exponential x z
left✝ : y ≤ 2 * y
⊢ (2 * y) ^ 2 = 2 * (2 * y ^ 2)
Tactic:
simp [sq, mul_assoc, mul_left_comm y 2]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ
Proof state before:
case intro.inr.mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y : M
IH : ∀ y_1 < y, ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
x : M
hxy : 2 * x + 1 < y
⊢ (∃ z ≤ y, y = 2 * z ∧ Exponential (2 * x + 1) z) → Exponential (2 * x + 1 + 1) y
Tactic:
rintro ⟨y, _, rfl, H⟩
Proof state after:
case intro.inr.mpr.intro.intro.intro
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 (2 * x + 1) y
IH : ∀ y_1 < 2 * y, ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
hxy : 2 * x + 1 < 2 * y
left✝ : y ≤ 2 * y
⊢ Exponential (2 * x + 1 + 1) (2 * y)
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ
Proof state before:
case intro.inr.mpr.intro.intro.intro
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 (2 * x + 1) y
IH : ∀ y_1 < 2 * y, ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
hxy : 2 * x + 1 < 2 * y
left✝ : y ≤ 2 * y
⊢ Exponential (2 * x + 1 + 1) (2 * y)
Tactic:
rcases exponential_odd.mp H with ⟨y, rfl, H'⟩
Proof state after:
case intro.inr.mpr.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 ⊧ₘ* 𝐈𝚫₀
x y : M
H' : Exponential x y
H : Exponential (2 * x + 1) (2 * y ^ 2)
IH : ∀ y_1 < 2 * (2 * y ^ 2), ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
hxy : 2 * x + 1 < 2 * (2 * y ^ 2)
left✝ : 2 * y ^ 2 ≤ 2 * (2 * y ^ 2)
⊢ Exponential (2 * x + 1 + 1) (2 * (2 * y ^ 2))
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ
Proof state before:
case intro.inr.mpr.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 ⊧ₘ* 𝐈𝚫₀
x y : M
H' : Exponential x y
H : Exponential (2 * x + 1) (2 * y ^ 2)
IH : ∀ y_1 < 2 * (2 * y ^ 2), ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
hxy : 2 * x + 1 < 2 * (2 * y ^ 2)
left✝ : 2 * y ^ 2 ≤ 2 * (2 * y ^ 2)
⊢ Exponential (2 * x + 1 + 1) (2 * (2 * y ^ 2))
Tactic:
by_cases ne1 : y = 1
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 ⊧ₘ* 𝐈𝚫₀
x y : M
H' : Exponential x y
H : Exponential (2 * x + 1) (2 * y ^ 2)
IH : ∀ y_1 < 2 * (2 * y ^ 2), ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
hxy : 2 * x + 1 < 2 * (2 * y ^ 2)
left✝ : 2 * y ^ 2 ≤ 2 * (2 * y ^ 2)
ne1 : y = 1
⊢ Exponential (2 * x + 1 + 1) (2 * (2 * y ^ 2))

case neg
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
H : Exponential (2 * x + 1) (2 * y ^ 2)
IH : ∀ y_1 < 2 * (2 * y ^ 2), ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
hxy : 2 * x + 1 < 2 * (2 * y ^ 2)
left✝ : 2 * y ^ 2 ≤ 2 * (2 * y ^ 2)
ne1 : ¬y = 1
⊢ Exponential (2 * x + 1 + 1) (2 * (2 * y ^ 2))
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ
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 ⊧ₘ* 𝐈𝚫₀
x y : M
H' : Exponential x y
H : Exponential (2 * x + 1) (2 * y ^ 2)
IH : ∀ y_1 < 2 * (2 * y ^ 2), ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
hxy : 2 * x + 1 < 2 * (2 * y ^ 2)
left✝ : 2 * y ^ 2 ≤ 2 * (2 * y ^ 2)
ne1 : ¬y = 1
⊢ Exponential (2 * x + 1 + 1) (2 * (2 * y ^ 2))
Tactic:
have : y < y^2 := lt_square_of_lt $ one_lt_iff_two_le.mpr $ H'.range_pow2.two_le ne1
Proof state after:
case neg
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
H : Exponential (2 * x + 1) (2 * y ^ 2)
IH : ∀ y_1 < 2 * (2 * y ^ 2), ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
hxy : 2 * x + 1 < 2 * (2 * y ^ 2)
left✝ : 2 * y ^ 2 ≤ 2 * (2 * y ^ 2)
ne1 : ¬y = 1
this : y < y ^ 2
⊢ Exponential (2 * x + 1 + 1) (2 * (2 * y ^ 2))
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ
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 ⊧ₘ* 𝐈𝚫₀
x y : M
H' : Exponential x y
H : Exponential (2 * x + 1) (2 * y ^ 2)
IH : ∀ y_1 < 2 * (2 * y ^ 2), ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
hxy : 2 * x + 1 < 2 * (2 * y ^ 2)
left✝ : 2 * y ^ 2 ≤ 2 * (2 * y ^ 2)
ne1 : ¬y = 1
this : y < y ^ 2
⊢ Exponential (2 * x + 1 + 1) (2 * (2 * y ^ 2))
Tactic:
have : Exponential (x + 1) (2 * y) ↔ ∃ z ≤ 2 * y, 2 * y = 2 * z ∧ Exponential x z :=
  IH (2 * y) (by simp; exact lt_of_lt_of_le this le_two_mul_left)
    (lt_of_lt_of_le H'.lt $ by simp)
Proof state after:
case neg
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
H : Exponential (2 * x + 1) (2 * y ^ 2)
IH : ∀ y_1 < 2 * (2 * y ^ 2), ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
hxy : 2 * x + 1 < 2 * (2 * y ^ 2)
left✝ : 2 * y ^ 2 ≤ 2 * (2 * y ^ 2)
ne1 : ¬y = 1
this✝ : y < y ^ 2
this : Exponential (x + 1) (2 * y) ↔ ∃ z ≤ 2 * y, 2 * y = 2 * z ∧ Exponential x z
⊢ Exponential (2 * x + 1 + 1) (2 * (2 * y ^ 2))
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ
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 ⊧ₘ* 𝐈𝚫₀
x y : M
H' : Exponential x y
H : Exponential (2 * x + 1) (2 * y ^ 2)
IH : ∀ y_1 < 2 * (2 * y ^ 2), ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
hxy : 2 * x + 1 < 2 * (2 * y ^ 2)
left✝ : 2 * y ^ 2 ≤ 2 * (2 * y ^ 2)
ne1 : ¬y = 1
this✝ : y < y ^ 2
this : Exponential (x + 1) (2 * y) ↔ ∃ z ≤ 2 * y, 2 * y = 2 * z ∧ Exponential x z
⊢ Exponential (2 * x + 1 + 1) (2 * (2 * y ^ 2))
Tactic:
have : Exponential (x + 1) (2 * y) := this.mpr ⟨y, by simp, rfl, H'⟩
Proof state after:
case neg
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
H : Exponential (2 * x + 1) (2 * y ^ 2)
IH : ∀ y_1 < 2 * (2 * y ^ 2), ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
hxy : 2 * x + 1 < 2 * (2 * y ^ 2)
left✝ : 2 * y ^ 2 ≤ 2 * (2 * y ^ 2)
ne1 : ¬y = 1
this✝¹ : y < y ^ 2
this✝ : Exponential (x + 1) (2 * y) ↔ ∃ z ≤ 2 * y, 2 * y = 2 * z ∧ Exponential x z
this : Exponential (x + 1) (2 * y)
⊢ Exponential (2 * x + 1 + 1) (2 * (2 * y ^ 2))
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ
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 ⊧ₘ* 𝐈𝚫₀
x y : M
H' : Exponential x y
H : Exponential (2 * x + 1) (2 * y ^ 2)
IH : ∀ y_1 < 2 * (2 * y ^ 2), ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
hxy : 2 * x + 1 < 2 * (2 * y ^ 2)
left✝ : 2 * y ^ 2 ≤ 2 * (2 * y ^ 2)
ne1 : ¬y = 1
this✝¹ : y < y ^ 2
this✝ : Exponential (x + 1) (2 * y) ↔ ∃ z ≤ 2 * y, 2 * y = 2 * z ∧ Exponential x z
this : Exponential (x + 1) (2 * y)
⊢ Exponential (2 * x + 1 + 1) (2 * (2 * y ^ 2))
Tactic:
simpa [sq, mul_add, add_assoc, mul_assoc, one_add_one_eq_two, mul_left_comm y 2] using this.bit_zero
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ
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 ⊧ₘ* 𝐈𝚫₀
x y : M
H' : Exponential x y
H : Exponential (2 * x + 1) (2 * y ^ 2)
IH : ∀ y_1 < 2 * (2 * y ^ 2), ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
hxy : 2 * x + 1 < 2 * (2 * y ^ 2)
left✝ : 2 * y ^ 2 ≤ 2 * (2 * y ^ 2)
ne1 : y = 1
⊢ Exponential (2 * x + 1 + 1) (2 * (2 * y ^ 2))
Tactic:
rcases ne1 with rfl
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 ⊧ₘ* 𝐈𝚫₀
x : M
H' : Exponential x 1
H : Exponential (2 * x + 1) (2 * 1 ^ 2)
IH : ∀ y < 2 * (2 * 1 ^ 2), ∀ {x : M}, x < y → (Exponential (x + 1) y ↔ ∃ z ≤ y, y = 2 * z ∧ Exponential x z)
hxy : 2 * x + 1 < 2 * (2 * 1 ^ 2)
left✝ : 2 * 1 ^ 2 ≤ 2 * (2 * 1 ^ 2)
⊢ Exponential (2 * x + 1 + 1) (2 * (2 * 1 ^ 2))
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ
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 ⊧ₘ* 𝐈𝚫₀
x : M
H' : Exponential x 1
H : Exponential (2 * x + 1) (2 * 1 ^ 2)
IH : ∀ y < 2 * (2 * 1 ^ 2), ∀ {x : M}, x < y → (Exponential (x + 1) y ↔ ∃ z ≤ y, y = 2 * z ∧ Exponential x z)
hxy : 2 * x + 1 < 2 * (2 * 1 ^ 2)
left✝ : 2 * 1 ^ 2 ≤ 2 * (2 * 1 ^ 2)
⊢ Exponential (2 * x + 1 + 1) (2 * (2 * 1 ^ 2))
Tactic:
rcases (show x = 0 from by simpa using H'.lt)
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 ⊧ₘ* 𝐈𝚫₀
IH : ∀ y < 2 * (2 * 1 ^ 2), ∀ {x : M}, x < y → (Exponential (x + 1) y ↔ ∃ z ≤ y, y = 2 * z ∧ Exponential x z)
left✝ : 2 * 1 ^ 2 ≤ 2 * (2 * 1 ^ 2)
H' : Exponential 0 1
H : Exponential (2 * 0 + 1) (2 * 1 ^ 2)
hxy : 2 * 0 + 1 < 2 * (2 * 1 ^ 2)
⊢ Exponential (2 * 0 + 1 + 1) (2 * (2 * 1 ^ 2))
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ
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 ⊧ₘ* 𝐈𝚫₀
IH : ∀ y < 2 * (2 * 1 ^ 2), ∀ {x : M}, x < y → (Exponential (x + 1) y ↔ ∃ z ≤ y, y = 2 * z ∧ Exponential x z)
left✝ : 2 * 1 ^ 2 ≤ 2 * (2 * 1 ^ 2)
H' : Exponential 0 1
H : Exponential (2 * 0 + 1) (2 * 1 ^ 2)
hxy : 2 * 0 + 1 < 2 * (2 * 1 ^ 2)
⊢ Exponential (2 * 0 + 1 + 1) (2 * (2 * 1 ^ 2))
Tactic:
simp [one_add_one_eq_two, two_mul_two_eq_four]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x : M
H' : Exponential x 1
H : Exponential (2 * x + 1) (2 * 1 ^ 2)
IH : ∀ y < 2 * (2 * 1 ^ 2), ∀ {x : M}, x < y → (Exponential (x + 1) y ↔ ∃ z ≤ y, y = 2 * z ∧ Exponential x z)
hxy : 2 * x + 1 < 2 * (2 * 1 ^ 2)
left✝ : 2 * 1 ^ 2 ≤ 2 * (2 * 1 ^ 2)
⊢ x = 0
Tactic:
simpa using H'.lt
Proof state after:
no goals