internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.Exponential.ext_le_ext_of_seq₀_of_seqₛ
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 X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH✝ : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → ext y_1 X < ext y_1 Y
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ne4 : ¬i = 4
IH : ext (√i) X < ext (√i) Y
hodd : Seqₛ.Odd X Y (√i)
⊢ 2 * ext (√i) Y ^ 2 = ext i Y
Tactic:
simpa [ppi.sq_sqrt_eq ne2] using Eq.symm hodd.2
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.range_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 ⊧ₘ* 𝐈𝚫₀
x y : M
h : Exponential x y
⊢ 0 < y
Tactic:
rcases h with (⟨rfl, rfl⟩ | ⟨X, bX, Y, bY, H₀, Hₛ, ⟨u, hu, ne2, ppu, rfl, rfl⟩⟩)
Proof state after:
case inl.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ 0 < 1

case inr.intro.intro.intro.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 ⊧ₘ* 𝐈𝚫₀
X Y : M
H₀ : Seq₀ X Y
u : M
ne2 : u ≠ 2
ppu : PPow2 u
bX : X ≤ ext u Y ^ 4
bY : Y ≤ ext u Y ^ 4
Hₛ : Seqₛ (ext u Y) X Y
hu : u ≤ ext u Y ^ 2
⊢ 0 < ext u Y
Theorem: LO.FirstOrder.Arith.Model.Exponential.range_pos
Proof state before:
case inl.intro
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.Exponential.range_pos
Proof state before:
case inr.intro.intro.intro.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 ⊧ₘ* 𝐈𝚫₀
X Y : M
H₀ : Seq₀ X Y
u : M
ne2 : u ≠ 2
ppu : PPow2 u
bX : X ≤ ext u Y ^ 4
bY : Y ≤ ext u Y ^ 4
Hₛ : Seqₛ (ext u Y) X Y
hu : u ≤ ext u Y ^ 2
⊢ 0 < ext u Y
Tactic:
have : 2 ≤ ext u Y := two_le_ext_of_seq₀_of_seqₛ H₀ Hₛ ne2 hu ppu
Proof state after:
case inr.intro.intro.intro.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 ⊧ₘ* 𝐈𝚫₀
X Y : M
H₀ : Seq₀ X Y
u : M
ne2 : u ≠ 2
ppu : PPow2 u
bX : X ≤ ext u Y ^ 4
bY : Y ≤ ext u Y ^ 4
Hₛ : Seqₛ (ext u Y) X Y
hu : u ≤ ext u Y ^ 2
this : 2 ≤ ext u Y
⊢ 0 < ext u Y
Theorem: LO.FirstOrder.Arith.Model.Exponential.range_pos
Proof state before:
case inr.intro.intro.intro.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 ⊧ₘ* 𝐈𝚫₀
X Y : M
H₀ : Seq₀ X Y
u : M
ne2 : u ≠ 2
ppu : PPow2 u
bX : X ≤ ext u Y ^ 4
bY : Y ≤ ext u Y ^ 4
Hₛ : Seqₛ (ext u Y) X Y
hu : u ≤ ext u Y ^ 2
this : 2 ≤ ext u Y
⊢ 0 < ext u Y
Tactic:
exact lt_of_lt_of_le (by simp) this
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.range_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 ⊧ₘ* 𝐈𝚫₀
X Y : M
H₀ : Seq₀ X Y
u : M
ne2 : u ≠ 2
ppu : PPow2 u
bX : X ≤ ext u Y ^ 4
bY : Y ≤ ext u Y ^ 4
Hₛ : Seqₛ (ext u Y) X Y
hu : u ≤ ext u Y ^ 2
this : 2 ≤ ext u Y
⊢ 0 < 2
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.lt
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
⊢ x < y
Tactic:
rcases h with (⟨rfl, rfl⟩ | ⟨X, bX, Y, bY, H₀, Hₛ, ⟨u, hu, ne2, ppu, rfl, rfl⟩⟩)
Proof state after:
case inl.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ 0 < 1

case inr.intro.intro.intro.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 ⊧ₘ* 𝐈𝚫₀
X Y : M
H₀ : Seq₀ X Y
u : M
ne2 : u ≠ 2
ppu : PPow2 u
bX : X ≤ ext u Y ^ 4
bY : Y ≤ ext u Y ^ 4
Hₛ : Seqₛ (ext u Y) X Y
hu : u ≤ ext u Y ^ 2
⊢ ext u X < ext u Y
Theorem: LO.FirstOrder.Arith.Model.Exponential.lt
Proof state before:
case inl.intro
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.Exponential.lt
Proof state before:
case inr.intro.intro.intro.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 ⊧ₘ* 𝐈𝚫₀
X Y : M
H₀ : Seq₀ X Y
u : M
ne2 : u ≠ 2
ppu : PPow2 u
bX : X ≤ ext u Y ^ 4
bY : Y ≤ ext u Y ^ 4
Hₛ : Seqₛ (ext u Y) X Y
hu : u ≤ ext u Y ^ 2
⊢ ext u X < ext u Y
Tactic:
exact ext_le_ext_of_seq₀_of_seqₛ H₀ Hₛ ne2 hu ppu
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.not_exponential_of_le
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 : x ≤ y
⊢ ¬Exponential y x
Tactic:
intro hxy
Proof state after:
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 : x ≤ y
hxy : Exponential y x
⊢ False
Theorem: LO.FirstOrder.Arith.Model.Exponential.not_exponential_of_le
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 : x ≤ y
hxy : Exponential y x
⊢ False
Tactic:
exact not_le.mpr (lt hxy) h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.one_not_even
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
⊢ 1 ≠ 2 * a
Tactic:
intro 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
h : 1 = 2 * a
⊢ False
Theorem: LO.FirstOrder.Arith.Model.Exponential.one_not_even
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
h : 1 = 2 * a
⊢ False
Tactic:
have : (2 : M) ∣ 1 := by rw [h]; 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 ⊧ₘ* 𝐈𝚫₀
a : M
h : 1 = 2 * a
this : 2 ∣ 1
⊢ False
Theorem: LO.FirstOrder.Arith.Model.Exponential.one_not_even
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
h : 1 = 2 * a
this : 2 ∣ 1
⊢ False
Tactic:
have : ¬(2 : M) ∣ 1 := not_dvd_of_lt (by simp) one_lt_two
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
h : 1 = 2 * a
this✝ : 2 ∣ 1
this : ¬2 ∣ 1
⊢ False
Theorem: LO.FirstOrder.Arith.Model.Exponential.one_not_even
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
h : 1 = 2 * a
this✝ : 2 ∣ 1
this : ¬2 ∣ 1
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.one_not_even
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
h : 1 = 2 * a
⊢ 2 ∣ 1
Tactic:
rw [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
h : 1 = 2 * a
⊢ 2 ∣ 2 * a
Theorem: LO.FirstOrder.Arith.Model.Exponential.one_not_even
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
h : 1 = 2 * a
⊢ 2 ∣ 2 * a
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.one_not_even
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
h : 1 = 2 * a
this : 2 ∣ 1
⊢ 0 < 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_two_four
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 2 4
Tactic:
simpa [two_pow_two_eq_four] using (show Exponential (1 : M) 2 from by simp).bit_zero
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_two_four
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.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
this : x < y → (Exponential (x + 1) y ↔ ∃ z ≤ y, y = 2 * z ∧ Exponential x z)
⊢ Exponential (x + 1) y ↔ ∃ z, y = 2 * z ∧ Exponential x z
Tactic:
by_cases hxy : x < y
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
this : x < y → (Exponential (x + 1) y ↔ ∃ z ≤ y, y = 2 * z ∧ Exponential x z)
hxy : x < y
⊢ Exponential (x + 1) y ↔ ∃ z, y = 2 * z ∧ Exponential x z

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
this : x < y → (Exponential (x + 1) y ↔ ∃ z ≤ y, y = 2 * z ∧ Exponential x z)
hxy : ¬x < y
⊢ Exponential (x + 1) y ↔ ∃ z, y = 2 * z ∧ Exponential x z
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
this : x < y → (Exponential (x + 1) y ↔ ∃ z ≤ y, y = 2 * z ∧ Exponential x z)
hxy : x < y
⊢ Exponential (x + 1) y ↔ ∃ z, y = 2 * z ∧ Exponential x z
Tactic:
simp [this hxy]
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
this : x < y → (Exponential (x + 1) y ↔ ∃ z ≤ y, y = 2 * z ∧ Exponential x z)
hxy : x < y
⊢ (∃ z ≤ y, y = 2 * z ∧ Exponential x z) ↔ ∃ z, y = 2 * z ∧ Exponential x z
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
this : x < y → (Exponential (x + 1) y ↔ ∃ z ≤ y, y = 2 * z ∧ Exponential x z)
hxy : x < y
⊢ (∃ z ≤ y, y = 2 * z ∧ Exponential x z) ↔ ∃ z, y = 2 * z ∧ Exponential x z
Tactic:
exact ⟨by rintro ⟨z, _, rfl, hz⟩; exact ⟨z, rfl, hz⟩,
       by rintro ⟨z, rfl, hz⟩; exact ⟨z, by simpa using hz⟩⟩
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
this : x < y → (Exponential (x + 1) y ↔ ∃ z ≤ y, y = 2 * z ∧ Exponential x z)
hxy : x < y
⊢ (∃ z ≤ y, y = 2 * z ∧ Exponential x z) → ∃ z, y = 2 * z ∧ Exponential x z
Tactic:
rintro ⟨z, _, rfl, hz⟩
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 ⊧ₘ* 𝐈𝚫₀
x z : M
hz : Exponential x z
this : x < 2 * z → (Exponential (x + 1) (2 * z) ↔ ∃ z_1 ≤ 2 * z, 2 * z = 2 * z_1 ∧ Exponential x z_1)
hxy : x < 2 * z
left✝ : z ≤ 2 * z
⊢ ∃ z_1, 2 * z = 2 * z_1 ∧ Exponential x z_1
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ
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 ⊧ₘ* 𝐈𝚫₀
x z : M
hz : Exponential x z
this : x < 2 * z → (Exponential (x + 1) (2 * z) ↔ ∃ z_1 ≤ 2 * z, 2 * z = 2 * z_1 ∧ Exponential x z_1)
hxy : x < 2 * z
left✝ : z ≤ 2 * z
⊢ ∃ z_1, 2 * z = 2 * z_1 ∧ Exponential x z_1
Tactic:
exact ⟨z, rfl, hz⟩
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
this : x < y → (Exponential (x + 1) y ↔ ∃ z ≤ y, y = 2 * z ∧ Exponential x z)
hxy : x < y
⊢ (∃ z, y = 2 * z ∧ Exponential x z) → ∃ z ≤ y, y = 2 * z ∧ Exponential x z
Tactic:
rintro ⟨z, rfl, hz⟩
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 ⊧ₘ* 𝐈𝚫₀
x z : M
hz : Exponential x z
this : x < 2 * z → (Exponential (x + 1) (2 * z) ↔ ∃ z_1 ≤ 2 * z, 2 * z = 2 * z_1 ∧ Exponential x z_1)
hxy : x < 2 * z
⊢ ∃ z_1 ≤ 2 * z, 2 * z = 2 * z_1 ∧ Exponential x z_1
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ
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 ⊧ₘ* 𝐈𝚫₀
x z : M
hz : Exponential x z
this : x < 2 * z → (Exponential (x + 1) (2 * z) ↔ ∃ z_1 ≤ 2 * z, 2 * z = 2 * z_1 ∧ Exponential x z_1)
hxy : x < 2 * z
⊢ ∃ z_1 ≤ 2 * z, 2 * z = 2 * z_1 ∧ Exponential x z_1
Tactic:
exact ⟨z, by simpa using hz⟩
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 z : M
hz : Exponential x z
this : x < 2 * z → (Exponential (x + 1) (2 * z) ↔ ∃ z_1 ≤ 2 * z, 2 * z = 2 * z_1 ∧ Exponential x z_1)
hxy : x < 2 * z
⊢ z ≤ 2 * z ∧ 2 * z = 2 * z ∧ Exponential x z
Tactic:
simpa using hz
Proof state after:
no goals
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
this : x < y → (Exponential (x + 1) y ↔ ∃ z ≤ y, y = 2 * z ∧ Exponential x z)
hxy : ¬x < y
⊢ Exponential (x + 1) y ↔ ∃ z, y = 2 * z ∧ Exponential x z
Tactic:
simp [not_exponential_of_le (show y ≤ x + 1 from le_add_right (by simpa using hxy))]
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
this : x < y → (Exponential (x + 1) y ↔ ∃ z ≤ y, y = 2 * z ∧ Exponential x z)
hxy : ¬x < y
⊢ ∀ (x_1 : M), y = 2 * x_1 → ¬Exponential x x_1
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
this : x < y → (Exponential (x + 1) y ↔ ∃ z ≤ y, y = 2 * z ∧ Exponential x z)
hxy : ¬x < y
⊢ ∀ (x_1 : M), y = 2 * x_1 → ¬Exponential x x_1
Tactic:
rintro z rfl
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 z : M
this : x < 2 * z → (Exponential (x + 1) (2 * z) ↔ ∃ z_1 ≤ 2 * z, 2 * z = 2 * z_1 ∧ Exponential x z_1)
hxy : ¬x < 2 * z
⊢ ¬Exponential x z
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 z : M
this : x < 2 * z → (Exponential (x + 1) (2 * z) ↔ ∃ z_1 ≤ 2 * z, 2 * z = 2 * z_1 ∧ Exponential x z_1)
hxy : ¬x < 2 * z
⊢ ¬Exponential x z
Tactic:
exact not_exponential_of_le (le_trans le_two_mul_left $  by simpa using 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
this : x < y → (Exponential (x + 1) y ↔ ∃ z ≤ y, y = 2 * z ∧ Exponential x z)
hxy : ¬x < y
⊢ y ≤ x
Tactic:
simpa using 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 z : M
this : x < 2 * z → (Exponential (x + 1) (2 * z) ↔ ∃ z_1 ≤ 2 * z, 2 * z = 2 * z_1 ∧ Exponential x z_1)
hxy : ¬x < 2 * z
⊢ 2 * z ≤ x
Tactic:
simpa using 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
⊢ x < y → (Exponential (x + 1) y ↔ ∃ z ≤ y, y = 2 * z ∧ Exponential x z)
Tactic:
revert 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 ⊧ₘ* 𝐈𝚫₀
y : M
⊢ ∀ {x : M}, x < y → (Exponential (x + 1) y ↔ ∃ z ≤ y, y = 2 * z ∧ Exponential x z)
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
⊢ ∀ {x : M}, x < y → (Exponential (x + 1) y ↔ ∃ z ≤ y, y = 2 * z ∧ Exponential x z)
Tactic:
induction y using order_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 ⊧ₘ* 𝐈𝚫₀
⊢ 𝚺₀-Predicate fun {y} => ∀ {x : M}, x < y → (Exponential (x + 1) y ↔ ∃ z ≤ y, y = 2 * z ∧ Exponential x z)

case ind
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x✝ : M
a✝ : ∀ y < x✝, ∀ {x : M}, x < y → (Exponential (x + 1) y ↔ ∃ z ≤ y, y = 2 * z ∧ Exponential x z)
⊢ ∀ {x : M}, x < x✝ → (Exponential (x + 1) x✝ ↔ ∃ z ≤ x✝, x✝ = 2 * z ∧ Exponential x z)
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ
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 {y} => ∀ {x : M}, x < y → (Exponential (x + 1) y ↔ ∃ z ≤ y, y = 2 * z ∧ Exponential x z)
Tactic:
definability
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}, x < y → (Exponential (x + 1) y ↔ ∃ z ≤ y, y = 2 * z ∧ Exponential x z)
Tactic:
intro x hxy
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 : ∀ 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 : x < y
⊢ Exponential (x + 1) y ↔ ∃ z ≤ y, y = 2 * z ∧ Exponential x z
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 : x < y
⊢ Exponential (x + 1) y ↔ ∃ z ≤ y, y = 2 * z ∧ Exponential x z
Tactic:
rcases even_or_odd x with ⟨x, (rfl | rfl)⟩
Proof state after:
case intro.inl
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 < y
⊢ Exponential (2 * x + 1) y ↔ ∃ z ≤ y, y = 2 * z ∧ Exponential (2 * x) z

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
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ
Proof state before:
case intro.inl
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 < y
⊢ Exponential (2 * x + 1) y ↔ ∃ z ≤ y, y = 2 * z ∧ Exponential (2 * x) z
Tactic:
constructor
Proof state after:
case intro.inl.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 < y
⊢ Exponential (2 * x + 1) y → ∃ z ≤ y, y = 2 * z ∧ Exponential (2 * x) z

case intro.inl.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 < y
⊢ (∃ z ≤ y, y = 2 * z ∧ Exponential (2 * x) z) → Exponential (2 * x + 1) y
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ
Proof state before:
case intro.inl.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 < y
⊢ Exponential (2 * x + 1) y → ∃ z ≤ y, y = 2 * z ∧ Exponential (2 * x) z
Tactic:
intro H
Proof state after:
case intro.inl.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 < y
H : Exponential (2 * x + 1) y
⊢ ∃ z ≤ y, y = 2 * z ∧ Exponential (2 * x) z
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ
Proof state before:
case intro.inl.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 < y
H : Exponential (2 * x + 1) y
⊢ ∃ z ≤ y, y = 2 * z ∧ Exponential (2 * x) z
Tactic:
rcases exponential_odd.mp H with ⟨y, rfl, H'⟩
Proof state after:
case intro.inl.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 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 < 2 * y ^ 2
H : Exponential (2 * x + 1) (2 * y ^ 2)
⊢ ∃ z ≤ 2 * y ^ 2, 2 * y ^ 2 = 2 * z ∧ Exponential (2 * x) z
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ
Proof state before:
case intro.inl.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 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 < 2 * y ^ 2
H : Exponential (2 * x + 1) (2 * y ^ 2)
⊢ ∃ z ≤ 2 * y ^ 2, 2 * y ^ 2 = 2 * z ∧ Exponential (2 * x) z
Tactic:
exact ⟨y^2, by simp, rfl, H'.bit_zero⟩
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
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
H : Exponential (2 * x + 1) (2 * y ^ 2)
⊢ y ^ 2 ≤ 2 * y ^ 2
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ
Proof state before:
case intro.inl.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 < y
⊢ (∃ z ≤ y, y = 2 * z ∧ Exponential (2 * x) z) → Exponential (2 * x + 1) y
Tactic:
rintro ⟨y, hy, rfl, H⟩
Proof state after:
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)