Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ (Arithmetization/ISigmaZero/Exponential/Exp.lean)

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
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

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]
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

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⟩⟩
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
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⟩
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

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⟩
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
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⟩
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

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⟩
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
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
State after:
no goals

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))]
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

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
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

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)
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
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
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
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
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y : M
⊢ x < y → (Exponential (x + 1) y ↔ ∃ z ≤ y, y = 2 * z ∧ Exponential x z)
Tactic:
revert x
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)

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
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)

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
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
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
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

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)⟩
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

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
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

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
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

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'⟩
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

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⟩
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
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
State after:
no goals

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⟩
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)

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'⟩
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)

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
State after:
no goals

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
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

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
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

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
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

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'⟩
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

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)
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

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)
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

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''⟩
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

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⟩
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
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
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
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)
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
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
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
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
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
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]
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
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]
State after:
no goals

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⟩
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)

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'⟩
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))

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
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))

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
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))

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)
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))

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'⟩
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))

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
State after:
no goals

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
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))

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)
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))

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]
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
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
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
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
⊢ 2 * y < 2 * (2 * y ^ 2)
Tactic:
simp
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' : 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
⊢ y < 2 * y ^ 2

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 (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
⊢ y < 2 * y ^ 2
Tactic:
exact lt_of_lt_of_le this le_two_mul_left
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
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
⊢ y ≤ 2 * y
Tactic:
simp
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
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
⊢ y ≤ 2 * y
Tactic:
simp
State after:
no goals