internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.Exponential.inj
Proof 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 : M
hy₁ : Exponential x₁ y
IH : ∀ y_1 < 2 * y, ∀ x₁ < y_1, ∀ x₂ < y_1, Exponential x₁ y_1 → Exponential x₂ y_1 → x₁ = x₂
a✝¹ : x₁ + 1 < 2 * y
h₁ : Exponential (x₁ + 1) (2 * y)
a✝ : x₂ + 1 < 2 * y
h₂ : Exponential (x₂ + 1) (2 * y)
hy₂ : Exponential x₂ y
⊢ x₁ + 1 = x₂ + 1
Tactic:
have : x₁ = x₂ :=
  IH y (lt_mul_of_pos_of_one_lt_left hy₁.range_pos one_lt_two)
    x₁ hy₁.lt x₂ hy₂.lt hy₁ hy₂
Proof 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 : M
hy₁ : Exponential x₁ y
IH : ∀ y_1 < 2 * y, ∀ x₁ < y_1, ∀ x₂ < y_1, Exponential x₁ y_1 → Exponential x₂ y_1 → x₁ = x₂
a✝¹ : x₁ + 1 < 2 * y
h₁ : Exponential (x₁ + 1) (2 * y)
a✝ : x₂ + 1 < 2 * y
h₂ : Exponential (x₂ + 1) (2 * y)
hy₂ : Exponential x₂ y
this : x₁ = x₂
⊢ x₁ + 1 = x₂ + 1
Theorem: LO.FirstOrder.Arith.Model.Exponential.inj
Proof 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 : M
hy₁ : Exponential x₁ y
IH : ∀ y_1 < 2 * y, ∀ x₁ < y_1, ∀ x₂ < y_1, Exponential x₁ y_1 → Exponential x₂ y_1 → x₁ = x₂
a✝¹ : x₁ + 1 < 2 * y
h₁ : Exponential (x₁ + 1) (2 * y)
a✝ : x₂ + 1 < 2 * y
h₂ : Exponential (x₂ + 1) (2 * y)
hy₂ : Exponential x₂ y
this : x₁ = x₂
⊢ x₁ + 1 = x₂ + 1
Tactic:
simp [this]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_elim
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
⊢ Exponential x y → x = 0 ∧ y = 1 ∨ ∃ x' y', x = x' + 1 ∧ y = 2 * y' ∧ Exponential x' y'
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 ⊧ₘ* 𝐈𝚫₀
x y : M
h : Exponential x y
⊢ x = 0 ∧ y = 1 ∨ ∃ x' y', x = x' + 1 ∧ y = 2 * y' ∧ Exponential x' y'
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_elim
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 = 0 ∧ y = 1 ∨ ∃ x' y', x = x' + 1 ∧ y = 2 * y' ∧ Exponential x' y'
Tactic:
rcases zero_or_succ x with (rfl | ⟨x', rfl⟩)
Proof state after:
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y : M
h : Exponential 0 y
⊢ 0 = 0 ∧ y = 1 ∨ ∃ x' y', 0 = x' + 1 ∧ y = 2 * y' ∧ Exponential x' y'

case inr.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y x' : M
h : Exponential (x' + 1) y
⊢ x' + 1 = 0 ∧ y = 1 ∨ ∃ x'_1 y', x' + 1 = x'_1 + 1 ∧ y = 2 * y' ∧ Exponential x'_1 y'
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_elim
Proof state before:
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y : M
h : Exponential 0 y
⊢ 0 = 0 ∧ y = 1 ∨ ∃ x' y', 0 = x' + 1 ∧ y = 2 * y' ∧ Exponential x' y'
Tactic:
simp [h.zero_uniq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_elim
Proof state before:
case inr.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y x' : M
h : Exponential (x' + 1) y
⊢ x' + 1 = 0 ∧ y = 1 ∨ ∃ x'_1 y', x' + 1 = x'_1 + 1 ∧ y = 2 * y' ∧ Exponential x'_1 y'
Tactic:
right
Proof state after:
case inr.intro.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y x' : M
h : Exponential (x' + 1) y
⊢ ∃ x'_1 y', x' + 1 = x'_1 + 1 ∧ y = 2 * y' ∧ Exponential x'_1 y'
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_elim
Proof state before:
case inr.intro.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y x' : M
h : Exponential (x' + 1) y
⊢ ∃ x'_1 y', x' + 1 = x'_1 + 1 ∧ y = 2 * y' ∧ Exponential x'_1 y'
Tactic:
rcases exponential_succ.mp h with ⟨y', rfl, H⟩
Proof state after:
case inr.intro.h.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')
⊢ ∃ x'_1 y'_1, x' + 1 = x'_1 + 1 ∧ 2 * y' = 2 * y'_1 ∧ Exponential x'_1 y'_1
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_elim
Proof state before:
case inr.intro.h.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')
⊢ ∃ x'_1 y'_1, x' + 1 = x'_1 + 1 ∧ 2 * y' = 2 * y'_1 ∧ Exponential x'_1 y'_1
Tactic:
exact ⟨x', y', rfl, rfl, H⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_elim
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 = 0 ∧ y = 1 ∨ ∃ x' y', x = x' + 1 ∧ y = 2 * y' ∧ Exponential x' y') → Exponential x y
Tactic:
rintro (⟨rfl, rfl⟩ | ⟨x, y, rfl, rfl, h⟩)
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 ⊧ₘ* 𝐈𝚫₀
⊢ Exponential 0 1

case inr.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
⊢ Exponential (x + 1) (2 * y)
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_elim
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 ⊧ₘ* 𝐈𝚫₀
⊢ Exponential 0 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_elim
Proof state before:
case inr.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
⊢ Exponential (x + 1) (2 * y)
Tactic:
exact h.succ
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.monotone
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₁ 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₂
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₁ x₂ y₁ y₂ : M
⊢ ∀ x₁ < y₁, ∀ y₂ ≤ y₁, ∀ x₂ < y₂, Exponential x₁ y₁ → Exponential x₂ y₂ → x₂ ≤ x₁
Theorem: LO.FirstOrder.Arith.Model.Exponential.monotone
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₁ 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
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 ⊧ₘ* 𝐈𝚫₀
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₁
Theorem: LO.FirstOrder.Arith.Model.Exponential.monotone
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₁ 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₂
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₁ 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₂
Theorem: LO.FirstOrder.Arith.Model.Exponential.monotone
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₁ 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
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₁ 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₂
Theorem: LO.FirstOrder.Arith.Model.Exponential.monotone
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₁ 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
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₁ 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₁
Theorem: LO.FirstOrder.Arith.Model.Exponential.monotone
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₁ 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
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₁ 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₁
Theorem: LO.FirstOrder.Arith.Model.Exponential.monotone
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₁ 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₂
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.monotone
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 ⊧ₘ* 𝐈𝚫₀
x₁ x₂ y₂ : M
⊢ 𝚺₀-Predicate fun {y₁} => ∀ x₁ < y₁, ∀ y₂ ≤ y₁, ∀ x₂ < y₂, Exponential x₁ y₁ → Exponential x₂ y₂ → x₂ ≤ x₁
Tactic:
definability
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.monotone
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₁ 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₂
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₁✝ 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₁
Theorem: LO.FirstOrder.Arith.Model.Exponential.monotone
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₁✝ 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⟩)
Proof 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
Theorem: LO.FirstOrder.Arith.Model.Exponential.monotone
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.monotone
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.Exponential.monotone
Proof 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)
Proof 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
Theorem: LO.FirstOrder.Arith.Model.Exponential.monotone
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.Exponential.monotone
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.monotone
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.monotone
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.monotone
Proof 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₁'⟩
Proof 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
Theorem: LO.FirstOrder.Arith.Model.Exponential.monotone
Proof 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₂'⟩
Proof 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
Theorem: LO.FirstOrder.Arith.Model.Exponential.monotone
Proof 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₂'
Proof 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
Theorem: LO.FirstOrder.Arith.Model.Exponential.monotone
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.monotone
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₁✝ 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.monotone_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₁ x₂ y₁ y₂ : M
h₁ : Exponential x₁ y₁
h₂ : Exponential x₂ y₂
⊢ x₁ ≤ x₂ → y₁ ≤ y₂
Tactic:
rintro (rfl | h)
Proof state after:
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ y₁ y₂ : M
h₁ : Exponential x₁ y₁
h₂ : Exponential x₁ y₂
⊢ y₁ ≤ y₂

case 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₁ y₂ : M
h₁ : Exponential x₁ y₁
h₂ : Exponential x₂ y₂
h : x₁ < x₂
⊢ y₁ ≤ y₂
Theorem: LO.FirstOrder.Arith.Model.Exponential.monotone_le
Proof state before:
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ y₁ y₂ : M
h₁ : Exponential x₁ y₁
h₂ : Exponential x₁ y₂
⊢ y₁ ≤ y₂
Tactic:
exact (h₁.uniq h₂).le
Proof state after:
no goals