Theorem: LO.FirstOrder.Arith.Model.Exponential.monotone (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₁ x₂ y₁ y₂ : M
⊢ Exponential x₁ y₁ → Exponential x₂ y₂ → x₁ < x₂ → y₁ < y₂
Tactic:
suffices ∀ x₁ < y₁, ∀ y₂ ≤ y₁, ∀ x₂ < y₂, Exponential x₁ y₁ → Exponential x₂ y₂ → x₂ ≤ x₁ by
  intro h₁ h₂; contrapose; simp
  intro hy
  exact this x₁ h₁.lt y₂ hy x₂ h₂.lt h₁ h₂
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ x₂ y₁ y₂ : M
⊢ ∀ x₁ < y₁, ∀ y₂ ≤ y₁, ∀ x₂ < y₂, Exponential x₁ y₁ → Exponential x₂ y₂ → x₂ ≤ x₁

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ x₂ y₁ y₂ : M
⊢ ∀ x₁ < y₁, ∀ y₂ ≤ y₁, ∀ x₂ < y₂, Exponential x₁ y₁ → Exponential x₂ y₂ → x₂ ≤ x₁
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 ⊧ₘ* 𝐈𝚫₀
x₁ x₂ y₂ : M
⊢ 𝚺₀-Predicate fun {y₁} => ∀ x₁ < y₁, ∀ y₂ ≤ y₁, ∀ x₂ < y₂, Exponential x₁ y₁ → Exponential x₂ y₂ → x₂ ≤ x₁

case ind
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ x₂ y₂ x✝ : M
a✝ : ∀ y < x✝, ∀ x₁ < y, ∀ y₂ ≤ y, ∀ x₂ < y₂, Exponential x₁ y → Exponential x₂ y₂ → x₂ ≤ x₁
⊢ ∀ x₁ < x✝, ∀ y₂ ≤ x✝, ∀ x₂ < y₂, Exponential x₁ x✝ → Exponential x₂ y₂ → x₂ ≤ x₁

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ x₂ y₁ y₂ : M
this : ∀ x₁ < y₁, ∀ y₂ ≤ y₁, ∀ x₂ < y₂, Exponential x₁ y₁ → Exponential x₂ y₂ → x₂ ≤ x₁
⊢ Exponential x₁ y₁ → Exponential x₂ y₂ → x₁ < x₂ → y₁ < y₂
Tactic:
intro h₁ h₂
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ x₂ y₁ y₂ : M
this : ∀ x₁ < y₁, ∀ y₂ ≤ y₁, ∀ x₂ < y₂, Exponential x₁ y₁ → Exponential x₂ y₂ → x₂ ≤ x₁
h₁ : Exponential x₁ y₁
h₂ : Exponential x₂ y₂
⊢ x₁ < x₂ → y₁ < y₂

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ x₂ y₁ y₂ : M
this : ∀ x₁ < y₁, ∀ y₂ ≤ y₁, ∀ x₂ < y₂, Exponential x₁ y₁ → Exponential x₂ y₂ → x₂ ≤ x₁
h₁ : Exponential x₁ y₁
h₂ : Exponential x₂ y₂
⊢ x₁ < x₂ → y₁ < y₂
Tactic:
contrapose
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ x₂ y₁ y₂ : M
this : ∀ x₁ < y₁, ∀ y₂ ≤ y₁, ∀ x₂ < y₂, Exponential x₁ y₁ → Exponential x₂ y₂ → x₂ ≤ x₁
h₁ : Exponential x₁ y₁
h₂ : Exponential x₂ y₂
⊢ ¬y₁ < y₂ → ¬x₁ < x₂

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ x₂ y₁ y₂ : M
this : ∀ x₁ < y₁, ∀ y₂ ≤ y₁, ∀ x₂ < y₂, Exponential x₁ y₁ → Exponential x₂ y₂ → x₂ ≤ x₁
h₁ : Exponential x₁ y₁
h₂ : Exponential x₂ y₂
⊢ ¬y₁ < y₂ → ¬x₁ < x₂
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₁ x₂ y₁ y₂ : M
this : ∀ x₁ < y₁, ∀ y₂ ≤ y₁, ∀ x₂ < y₂, Exponential x₁ y₁ → Exponential x₂ y₂ → x₂ ≤ x₁
h₁ : Exponential x₁ y₁
h₂ : Exponential x₂ y₂
⊢ y₂ ≤ y₁ → x₂ ≤ x₁

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ x₂ y₁ y₂ : M
this : ∀ x₁ < y₁, ∀ y₂ ≤ y₁, ∀ x₂ < y₂, Exponential x₁ y₁ → Exponential x₂ y₂ → x₂ ≤ x₁
h₁ : Exponential x₁ y₁
h₂ : Exponential x₂ y₂
⊢ y₂ ≤ y₁ → x₂ ≤ x₁
Tactic:
intro hy
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ x₂ y₁ y₂ : M
this : ∀ x₁ < y₁, ∀ y₂ ≤ y₁, ∀ x₂ < y₂, Exponential x₁ y₁ → Exponential x₂ y₂ → x₂ ≤ x₁
h₁ : Exponential x₁ y₁
h₂ : Exponential x₂ y₂
hy : y₂ ≤ y₁
⊢ x₂ ≤ x₁

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ x₂ y₁ y₂ : M
this : ∀ x₁ < y₁, ∀ y₂ ≤ y₁, ∀ x₂ < y₂, Exponential x₁ y₁ → Exponential x₂ y₂ → x₂ ≤ x₁
h₁ : Exponential x₁ y₁
h₂ : Exponential x₂ y₂
hy : y₂ ≤ y₁
⊢ x₂ ≤ x₁
Tactic:
exact this x₁ h₁.lt y₂ hy x₂ h₂.lt h₁ h₂
State after:
no goals

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 ⊧ₘ* 𝐈𝚫₀
x₁ x₂ y₂ : M
⊢ 𝚺₀-Predicate fun {y₁} => ∀ x₁ < y₁, ∀ y₂ ≤ y₁, ∀ x₂ < y₂, Exponential x₁ y₁ → Exponential x₂ y₂ → x₂ ≤ x₁
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 ⊧ₘ* 𝐈𝚫₀
x₁ x₂ y₂ y₁ : M
IH : ∀ y < y₁, ∀ x₁ < y, ∀ y₂ ≤ y, ∀ x₂ < y₂, Exponential x₁ y → Exponential x₂ y₂ → x₂ ≤ x₁
⊢ ∀ x₁ < y₁, ∀ y₂ ≤ y₁, ∀ x₂ < y₂, Exponential x₁ y₁ → Exponential x₂ y₂ → x₂ ≤ x₁
Tactic:
intro x₁ _ y₂ hy x₂ _ h₁ h₂
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁✝ x₂✝ y₂✝ y₁ : M
IH : ∀ y < y₁, ∀ x₁ < y, ∀ y₂ ≤ y, ∀ x₂ < y₂, Exponential x₁ y → Exponential x₂ y₂ → x₂ ≤ x₁
x₁ : M
a✝¹ : x₁ < y₁
y₂ : M
hy : y₂ ≤ y₁
x₂ : M
a✝ : x₂ < y₂
h₁ : Exponential x₁ y₁
h₂ : Exponential x₂ y₂
⊢ x₂ ≤ x₁

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁✝ x₂✝ y₂✝ y₁ : M
IH : ∀ y < y₁, ∀ x₁ < y, ∀ y₂ ≤ y, ∀ x₂ < y₂, Exponential x₁ y → Exponential x₂ y₂ → x₂ ≤ x₁
x₁ : M
a✝¹ : x₁ < y₁
y₂ : M
hy : y₂ ≤ y₁
x₂ : M
a✝ : x₂ < y₂
h₁ : Exponential x₁ y₁
h₂ : Exponential x₂ y₂
⊢ x₂ ≤ x₁
Tactic:
rcases zero_or_succ x₁ with (rfl | ⟨x₁, rfl⟩) <;> rcases zero_or_succ x₂ with (rfl | ⟨x₂, rfl⟩)
State after:
case inl.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ x₂ y₂✝ y₁ : M
IH : ∀ y < y₁, ∀ x₁ < y, ∀ y₂ ≤ y, ∀ x₂ < y₂, Exponential x₁ y → Exponential x₂ y₂ → x₂ ≤ x₁
y₂ : M
hy : y₂ ≤ y₁
a✝¹ : 0 < y₁
h₁ : Exponential 0 y₁
a✝ : 0 < y₂
h₂ : Exponential 0 y₂
⊢ 0 ≤ 0

case inl.inr.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ x₂✝ y₂✝ y₁ : M
IH : ∀ y < y₁, ∀ x₁ < y, ∀ y₂ ≤ y, ∀ x₂ < y₂, Exponential x₁ y → Exponential x₂ y₂ → x₂ ≤ x₁
y₂ : M
hy : y₂ ≤ y₁
a✝¹ : 0 < y₁
h₁ : Exponential 0 y₁
x₂ : M
a✝ : x₂ + 1 < y₂
h₂ : Exponential (x₂ + 1) y₂
⊢ x₂ + 1 ≤ 0

case inr.intro.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁✝ x₂ y₂✝ y₁ : M
IH : ∀ y < y₁, ∀ x₁ < y, ∀ y₂ ≤ y, ∀ x₂ < y₂, Exponential x₁ y → Exponential x₂ y₂ → x₂ ≤ x₁
y₂ : M
hy : y₂ ≤ y₁
x₁ : M
a✝¹ : x₁ + 1 < y₁
h₁ : Exponential (x₁ + 1) y₁
a✝ : 0 < y₂
h₂ : Exponential 0 y₂
⊢ 0 ≤ x₁ + 1

case inr.intro.inr.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁✝ x₂✝ y₂✝ y₁ : M
IH : ∀ y < y₁, ∀ x₁ < y, ∀ y₂ ≤ y, ∀ x₂ < y₂, Exponential x₁ y → Exponential x₂ y₂ → x₂ ≤ x₁
y₂ : M
hy : y₂ ≤ y₁
x₁ : M
a✝¹ : x₁ + 1 < y₁
h₁ : Exponential (x₁ + 1) y₁
x₂ : M
a✝ : x₂ + 1 < y₂
h₂ : Exponential (x₂ + 1) y₂
⊢ x₂ + 1 ≤ x₁ + 1

State before:
case inl.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ x₂ y₂✝ y₁ : M
IH : ∀ y < y₁, ∀ x₁ < y, ∀ y₂ ≤ y, ∀ x₂ < y₂, Exponential x₁ y → Exponential x₂ y₂ → x₂ ≤ x₁
y₂ : M
hy : y₂ ≤ y₁
a✝¹ : 0 < y₁
h₁ : Exponential 0 y₁
a✝ : 0 < y₂
h₂ : Exponential 0 y₂
⊢ 0 ≤ 0
Tactic:
simp
State after:
no goals

State before:
case inl.inr.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ x₂✝ y₂✝ y₁ : M
IH : ∀ y < y₁, ∀ x₁ < y, ∀ y₂ ≤ y, ∀ x₂ < y₂, Exponential x₁ y → Exponential x₂ y₂ → x₂ ≤ x₁
y₂ : M
hy : y₂ ≤ y₁
a✝¹ : 0 < y₁
h₁ : Exponential 0 y₁
x₂ : M
a✝ : x₂ + 1 < y₂
h₂ : Exponential (x₂ + 1) y₂
⊢ x₂ + 1 ≤ 0
Tactic:
rcases show y₁ = 1 from h₁.zero_uniq
State after:
case inl.inr.intro.refl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ x₂✝ y₂✝ y₂ x₂ : M
a✝¹ : x₂ + 1 < y₂
h₂ : Exponential (x₂ + 1) y₂
IH : ∀ y < 1, ∀ x₁ < y, ∀ y₂ ≤ y, ∀ x₂ < y₂, Exponential x₁ y → Exponential x₂ y₂ → x₂ ≤ x₁
hy : y₂ ≤ 1
a✝ : 0 < 1
h₁ : Exponential 0 1
⊢ x₂ + 1 ≤ 0

State before:
case inl.inr.intro.refl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ x₂✝ y₂✝ y₂ x₂ : M
a✝¹ : x₂ + 1 < y₂
h₂ : Exponential (x₂ + 1) y₂
IH : ∀ y < 1, ∀ x₁ < y, ∀ y₂ ≤ y, ∀ x₂ < y₂, Exponential x₁ y → Exponential x₂ y₂ → x₂ ≤ x₁
hy : y₂ ≤ 1
a✝ : 0 < 1
h₁ : Exponential 0 1
⊢ x₂ + 1 ≤ 0
Tactic:
rcases le_one_iff_eq_zero_or_one.mp hy with (rfl | rfl)
State after:
case inl.inr.intro.refl.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ x₂✝ y₂ x₂ : M
IH : ∀ y < 1, ∀ x₁ < y, ∀ y₂ ≤ y, ∀ x₂ < y₂, Exponential x₁ y → Exponential x₂ y₂ → x₂ ≤ x₁
a✝¹ : 0 < 1
h₁ : Exponential 0 1
a✝ : x₂ + 1 < 0
h₂ : Exponential (x₂ + 1) 0
hy : 0 ≤ 1
⊢ x₂ + 1 ≤ 0

case inl.inr.intro.refl.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ x₂✝ y₂ x₂ : M
IH : ∀ y < 1, ∀ x₁ < y, ∀ y₂ ≤ y, ∀ x₂ < y₂, Exponential x₁ y → Exponential x₂ y₂ → x₂ ≤ x₁
a✝¹ : 0 < 1
h₁ : Exponential 0 1
a✝ : x₂ + 1 < 1
h₂ : Exponential (x₂ + 1) 1
hy : 1 ≤ 1
⊢ x₂ + 1 ≤ 0

State before:
case inl.inr.intro.refl.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ x₂✝ y₂ x₂ : M
IH : ∀ y < 1, ∀ x₁ < y, ∀ y₂ ≤ y, ∀ x₂ < y₂, Exponential x₁ y → Exponential x₂ y₂ → x₂ ≤ x₁
a✝¹ : 0 < 1
h₁ : Exponential 0 1
a✝ : x₂ + 1 < 0
h₂ : Exponential (x₂ + 1) 0
hy : 0 ≤ 1
⊢ x₂ + 1 ≤ 0
Tactic:
have := h₂.range_pos
State after:
case inl.inr.intro.refl.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ x₂✝ y₂ x₂ : M
IH : ∀ y < 1, ∀ x₁ < y, ∀ y₂ ≤ y, ∀ x₂ < y₂, Exponential x₁ y → Exponential x₂ y₂ → x₂ ≤ x₁
a✝¹ : 0 < 1
h₁ : Exponential 0 1
a✝ : x₂ + 1 < 0
h₂ : Exponential (x₂ + 1) 0
hy : 0 ≤ 1
this : 0 < 0
⊢ x₂ + 1 ≤ 0

State before:
case inl.inr.intro.refl.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ x₂✝ y₂ x₂ : M
IH : ∀ y < 1, ∀ x₁ < y, ∀ y₂ ≤ y, ∀ x₂ < y₂, Exponential x₁ y → Exponential x₂ y₂ → x₂ ≤ x₁
a✝¹ : 0 < 1
h₁ : Exponential 0 1
a✝ : x₂ + 1 < 0
h₂ : Exponential (x₂ + 1) 0
hy : 0 ≤ 1
this : 0 < 0
⊢ x₂ + 1 ≤ 0
Tactic:
simp at this
State after:
no goals

State before:
case inl.inr.intro.refl.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ x₂✝ y₂ x₂ : M
IH : ∀ y < 1, ∀ x₁ < y, ∀ y₂ ≤ y, ∀ x₂ < y₂, Exponential x₁ y → Exponential x₂ y₂ → x₂ ≤ x₁
a✝¹ : 0 < 1
h₁ : Exponential 0 1
a✝ : x₂ + 1 < 1
h₂ : Exponential (x₂ + 1) 1
hy : 1 ≤ 1
⊢ x₂ + 1 ≤ 0
Tactic:
exact False.elim <| not_lt.mpr h₂.succ_lt_s one_lt_two
State after:
no goals

State before:
case inr.intro.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁✝ x₂ y₂✝ y₁ : M
IH : ∀ y < y₁, ∀ x₁ < y, ∀ y₂ ≤ y, ∀ x₂ < y₂, Exponential x₁ y → Exponential x₂ y₂ → x₂ ≤ x₁
y₂ : M
hy : y₂ ≤ y₁
x₁ : M
a✝¹ : x₁ + 1 < y₁
h₁ : Exponential (x₁ + 1) y₁
a✝ : 0 < y₂
h₂ : Exponential 0 y₂
⊢ 0 ≤ x₁ + 1
Tactic:
simp
State after:
no goals

State before:
case inr.intro.inr.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁✝ x₂✝ y₂✝ y₁ : M
IH : ∀ y < y₁, ∀ x₁ < y, ∀ y₂ ≤ y, ∀ x₂ < y₂, Exponential x₁ y → Exponential x₂ y₂ → x₂ ≤ x₁
y₂ : M
hy : y₂ ≤ y₁
x₁ : M
a✝¹ : x₁ + 1 < y₁
h₁ : Exponential (x₁ + 1) y₁
x₂ : M
a✝ : x₂ + 1 < y₂
h₂ : Exponential (x₂ + 1) y₂
⊢ x₂ + 1 ≤ x₁ + 1
Tactic:
rcases exponential_succ.mp h₁ with ⟨y₁, rfl, h₁'⟩
State after:
case inr.intro.inr.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₁✝ x₂✝ y₂✝ y₂ x₁ x₂ : M
a✝¹ : x₂ + 1 < y₂
h₂ : Exponential (x₂ + 1) y₂
y₁ : M
h₁' : Exponential x₁ y₁
IH : ∀ y < 2 * y₁, ∀ x₁ < y, ∀ y₂ ≤ y, ∀ x₂ < y₂, Exponential x₁ y → Exponential x₂ y₂ → x₂ ≤ x₁
hy : y₂ ≤ 2 * y₁
a✝ : x₁ + 1 < 2 * y₁
h₁ : Exponential (x₁ + 1) (2 * y₁)
⊢ x₂ + 1 ≤ x₁ + 1

State before:
case inr.intro.inr.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₁✝ x₂✝ y₂✝ y₂ x₁ x₂ : M
a✝¹ : x₂ + 1 < y₂
h₂ : Exponential (x₂ + 1) y₂
y₁ : M
h₁' : Exponential x₁ y₁
IH : ∀ y < 2 * y₁, ∀ x₁ < y, ∀ y₂ ≤ y, ∀ x₂ < y₂, Exponential x₁ y → Exponential x₂ y₂ → x₂ ≤ x₁
hy : y₂ ≤ 2 * y₁
a✝ : x₁ + 1 < 2 * y₁
h₁ : Exponential (x₁ + 1) (2 * y₁)
⊢ x₂ + 1 ≤ x₁ + 1
Tactic:
rcases exponential_succ.mp h₂ with ⟨y₂, rfl, h₂'⟩
State after:
case inr.intro.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 ⊧ₘ* 𝐈𝚫₀
x₁✝ x₂✝ y₂✝ x₁ x₂ y₁ : M
h₁' : Exponential x₁ y₁
IH : ∀ y < 2 * y₁, ∀ x₁ < y, ∀ y₂ ≤ y, ∀ x₂ < y₂, Exponential x₁ y → Exponential x₂ y₂ → x₂ ≤ x₁
a✝¹ : x₁ + 1 < 2 * y₁
h₁ : Exponential (x₁ + 1) (2 * y₁)
y₂ : M
h₂' : Exponential x₂ y₂
a✝ : x₂ + 1 < 2 * y₂
h₂ : Exponential (x₂ + 1) (2 * y₂)
hy : 2 * y₂ ≤ 2 * y₁
⊢ x₂ + 1 ≤ x₁ + 1

State before:
case inr.intro.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 ⊧ₘ* 𝐈𝚫₀
x₁✝ x₂✝ y₂✝ x₁ x₂ y₁ : M
h₁' : Exponential x₁ y₁
IH : ∀ y < 2 * y₁, ∀ x₁ < y, ∀ y₂ ≤ y, ∀ x₂ < y₂, Exponential x₁ y → Exponential x₂ y₂ → x₂ ≤ x₁
a✝¹ : x₁ + 1 < 2 * y₁
h₁ : Exponential (x₁ + 1) (2 * y₁)
y₂ : M
h₂' : Exponential x₂ y₂
a✝ : x₂ + 1 < 2 * y₂
h₂ : Exponential (x₂ + 1) (2 * y₂)
hy : 2 * y₂ ≤ 2 * y₁
⊢ x₂ + 1 ≤ x₁ + 1
Tactic:
have : x₂ ≤ x₁ := IH y₁ (lt_mul_of_pos_of_one_lt_left h₁'.range_pos one_lt_two)
  x₁ h₁'.lt y₂ (le_of_mul_le_mul_left hy (by simp)) x₂ h₂'.lt h₁' h₂'
State after:
case inr.intro.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 ⊧ₘ* 𝐈𝚫₀
x₁✝ x₂✝ y₂✝ x₁ x₂ y₁ : M
h₁' : Exponential x₁ y₁
IH : ∀ y < 2 * y₁, ∀ x₁ < y, ∀ y₂ ≤ y, ∀ x₂ < y₂, Exponential x₁ y → Exponential x₂ y₂ → x₂ ≤ x₁
a✝¹ : x₁ + 1 < 2 * y₁
h₁ : Exponential (x₁ + 1) (2 * y₁)
y₂ : M
h₂' : Exponential x₂ y₂
a✝ : x₂ + 1 < 2 * y₂
h₂ : Exponential (x₂ + 1) (2 * y₂)
hy : 2 * y₂ ≤ 2 * y₁
this : x₂ ≤ x₁
⊢ x₂ + 1 ≤ x₁ + 1

State before:
case inr.intro.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 ⊧ₘ* 𝐈𝚫₀
x₁✝ x₂✝ y₂✝ x₁ x₂ y₁ : M
h₁' : Exponential x₁ y₁
IH : ∀ y < 2 * y₁, ∀ x₁ < y, ∀ y₂ ≤ y, ∀ x₂ < y₂, Exponential x₁ y → Exponential x₂ y₂ → x₂ ≤ x₁
a✝¹ : x₁ + 1 < 2 * y₁
h₁ : Exponential (x₁ + 1) (2 * y₁)
y₂ : M
h₂' : Exponential x₂ y₂
a✝ : x₂ + 1 < 2 * y₂
h₂ : Exponential (x₂ + 1) (2 * y₂)
hy : 2 * y₂ ≤ 2 * y₁
this : x₂ ≤ x₁
⊢ x₂ + 1 ≤ x₁ + 1
Tactic:
simpa using this
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₁✝ x₂✝ y₂✝ x₁ x₂ y₁ : M
h₁' : Exponential x₁ y₁
IH : ∀ y < 2 * y₁, ∀ x₁ < y, ∀ y₂ ≤ y, ∀ x₂ < y₂, Exponential x₁ y → Exponential x₂ y₂ → x₂ ≤ x₁
a✝¹ : x₁ + 1 < 2 * y₁
h₁ : Exponential (x₁ + 1) (2 * y₁)
y₂ : M
h₂' : Exponential x₂ y₂
a✝ : x₂ + 1 < 2 * y₂
h₂ : Exponential (x₂ + 1) (2 * y₂)
hy : 2 * y₂ ≤ 2 * y₁
⊢ 0 < 2
Tactic:
simp
State after:
no goals