internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.Exponential.monotone_le
Proof state before:
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₂
Tactic:
exact le_of_lt (monotone h₁ h₂ h)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.monotone_iff
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:
constructor
Proof state after:
case mp
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₂

case mpr
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₂
⊢ y₁ < y₂ → x₁ < x₂
Theorem: LO.FirstOrder.Arith.Model.Exponential.monotone_iff
Proof state before:
case mp
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:
exact monotone h₁ h₂
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.monotone_iff
Proof state before:
case mpr
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₂
⊢ y₁ < y₂ → x₁ < x₂
Tactic:
contrapose
Proof state after:
case mpr
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₂
Theorem: LO.FirstOrder.Arith.Model.Exponential.monotone_iff
Proof state before:
case mpr
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:
simp
Proof state after:
case mpr
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₁
Theorem: LO.FirstOrder.Arith.Model.Exponential.monotone_iff
Proof state before:
case mpr
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:
exact monotone_le h₂ h₁
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.monotone_le_iff
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:
constructor
Proof state after:
case mp
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₂

case mpr
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₂
⊢ y₁ ≤ y₂ → x₁ ≤ x₂
Theorem: LO.FirstOrder.Arith.Model.Exponential.monotone_le_iff
Proof state before:
case mp
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:
exact monotone_le h₁ h₂
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.monotone_le_iff
Proof state before:
case mpr
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₂
⊢ y₁ ≤ y₂ → x₁ ≤ x₂
Tactic:
contrapose
Proof state after:
case mpr
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₂
Theorem: LO.FirstOrder.Arith.Model.Exponential.monotone_le_iff
Proof state before:
case mpr
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:
simp
Proof state after:
case mpr
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₁
Theorem: LO.FirstOrder.Arith.Model.Exponential.monotone_le_iff
Proof state before:
case mpr
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:
exact monotone h₂ h₁
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.add_mul
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₂
⊢ Exponential (x₁ + x₂) (y₁ * y₂)
Tactic:
wlog hy : y₁ ≥ y₂
Proof state after:
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₂
this :
  ∀ {M : Type u_1} [inst : Zero M] [inst_1 : One M] [inst_2 : Add M] [inst_3 : Mul M] [inst_4 : LT M]
    [inst_5 : M ⊧ₘ* 𝐈𝚫₀] {x₁ x₂ y₁ y₂ : M},
    Exponential x₁ y₁ → Exponential x₂ y₂ → y₁ ≥ y₂ → Exponential (x₁ + x₂) (y₁ * y₂)
hy : ¬y₁ ≥ y₂
⊢ Exponential (x₁ + x₂) (y₁ * y₂)

M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
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₂
hy : y₁ ≥ y₂
⊢ Exponential (x₁ + x₂) (y₁ * y₂)
Theorem: LO.FirstOrder.Arith.Model.Exponential.add_mul
Proof state before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
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₂
hy : y₁ ≥ y₂
⊢ Exponential (x₁ + x₂) (y₁ * y₂)
Tactic:
revert y₂
Proof state after:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
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
h₁ : Exponential x₁ y₁
⊢ ∀ {y₂ : M}, Exponential x₂ y₂ → y₁ ≥ y₂ → Exponential (x₁ + x₂) (y₁ * y₂)
Theorem: LO.FirstOrder.Arith.Model.Exponential.add_mul
Proof state before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
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
h₁ : Exponential x₁ y₁
⊢ ∀ {y₂ : M}, Exponential x₂ y₂ → y₁ ≥ y₂ → Exponential (x₁ + x₂) (y₁ * y₂)
Tactic:
suffices ∀ y₂ ≤ y₁, Exponential x₂ y₂ → Exponential (x₁ + x₂) (y₁ * y₂) by
  intro y₂ h₂ hy; exact this y₂ hy 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✝ ⊧ₘ* 𝐈𝚫₀
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
h₁ : Exponential x₁ y₁
⊢ ∀ y₂ ≤ y₁, Exponential x₂ y₂ → Exponential (x₁ + x₂) (y₁ * y₂)
Theorem: LO.FirstOrder.Arith.Model.Exponential.add_mul
Proof state before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
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
h₁ : Exponential x₁ y₁
⊢ ∀ y₂ ≤ y₁, Exponential x₂ y₂ → Exponential (x₁ + x₂) (y₁ * y₂)
Tactic:
induction x₂ using 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✝ ⊧ₘ* 𝐈𝚫₀
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₁
⊢ 𝚺₀-Predicate fun {x₂} => ∀ y₂ ≤ y₁, Exponential x₂ y₂ → Exponential (x₁ + x₂) (y₁ * y₂)

case zero
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
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₁
⊢ ∀ y₂ ≤ y₁, Exponential 0 y₂ → Exponential (x₁ + 0) (y₁ * y₂)

case succ
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
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✝ : M
a✝ : ∀ y₂ ≤ y₁, Exponential x✝ y₂ → Exponential (x₁ + x✝) (y₁ * y₂)
⊢ ∀ y₂ ≤ y₁, Exponential (x✝ + 1) y₂ → Exponential (x₁ + (x✝ + 1)) (y₁ * y₂)
Theorem: LO.FirstOrder.Arith.Model.Exponential.add_mul
Proof state before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
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₁
⊢ ∀ y₂ ≤ y₁, Exponential 0 y₂ → Exponential (x₁ + 0) (y₁ * y₂)
Tactic:
case zero =>
  intro y₂ _ h₂
  simpa [show y₂ = 1 from h₂.zero_uniq] using h₁
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.add_mul
Proof state before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
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₂ : M
IH : ∀ y₂ ≤ y₁, Exponential x₂ y₂ → Exponential (x₁ + x₂) (y₁ * y₂)
⊢ ∀ y₂ ≤ y₁, Exponential (x₂ + 1) y₂ → Exponential (x₁ + (x₂ + 1)) (y₁ * y₂)
Tactic:
case succ x₂ IH =>
  intro y₂ hy h₂
  rcases exponential_succ.mp h₂ with ⟨y₂, rfl, H₂⟩
  have : Exponential (x₁ + x₂) (y₁ * y₂) := IH y₂ (le_trans (by simp) hy) H₂
  simpa [←add_assoc, mul_left_comm y₁ 2 y₂] using this.succ
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.add_mul
Proof state before:
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₂
this :
  ∀ {M : Type u_1} [inst : Zero M] [inst_1 : One M] [inst_2 : Add M] [inst_3 : Mul M] [inst_4 : LT M]
    [inst_5 : M ⊧ₘ* 𝐈𝚫₀] {x₁ x₂ y₁ y₂ : M},
    Exponential x₁ y₁ → Exponential x₂ y₂ → y₁ ≥ y₂ → Exponential (x₁ + x₂) (y₁ * y₂)
hy : ¬y₁ ≥ y₂
⊢ Exponential (x₁ + x₂) (y₁ * y₂)
Tactic:
simpa [add_comm, mul_comm] using this h₂ h₁ (le_of_not_ge hy)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.add_mul
Proof state before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
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
h₁ : Exponential x₁ y₁
this : ∀ y₂ ≤ y₁, Exponential x₂ y₂ → Exponential (x₁ + x₂) (y₁ * y₂)
⊢ ∀ {y₂ : M}, Exponential x₂ y₂ → y₁ ≥ y₂ → Exponential (x₁ + x₂) (y₁ * y₂)
Tactic:
intro y₂ h₂ 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✝ ⊧ₘ* 𝐈𝚫₀
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
h₁ : Exponential x₁ y₁
this : ∀ y₂ ≤ y₁, Exponential x₂ y₂ → Exponential (x₁ + x₂) (y₁ * y₂)
y₂ : M
h₂ : Exponential x₂ y₂
hy : y₁ ≥ y₂
⊢ Exponential (x₁ + x₂) (y₁ * y₂)
Theorem: LO.FirstOrder.Arith.Model.Exponential.add_mul
Proof state before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
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
h₁ : Exponential x₁ y₁
this : ∀ y₂ ≤ y₁, Exponential x₂ y₂ → Exponential (x₁ + x₂) (y₁ * y₂)
y₂ : M
h₂ : Exponential x₂ y₂
hy : y₁ ≥ y₂
⊢ Exponential (x₁ + x₂) (y₁ * y₂)
Tactic:
exact this y₂ hy h₂
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.add_mul
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✝ ⊧ₘ* 𝐈𝚫₀
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₁
⊢ 𝚺₀-Predicate fun {x₂} => ∀ y₂ ≤ y₁, Exponential x₂ y₂ → Exponential (x₁ + x₂) (y₁ * y₂)
Tactic:
definability
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.add_mul
Proof state before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
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₁
⊢ ∀ y₂ ≤ y₁, Exponential 0 y₂ → Exponential (x₁ + 0) (y₁ * y₂)
Tactic:
intro y₂ _ 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✝ ⊧ₘ* 𝐈𝚫₀
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₁
y₂ : M
a✝ : y₂ ≤ y₁
h₂ : Exponential 0 y₂
⊢ Exponential (x₁ + 0) (y₁ * y₂)
Theorem: LO.FirstOrder.Arith.Model.Exponential.add_mul
Proof state before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
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₁
y₂ : M
a✝ : y₂ ≤ y₁
h₂ : Exponential 0 y₂
⊢ Exponential (x₁ + 0) (y₁ * y₂)
Tactic:
simpa [show y₂ = 1 from h₂.zero_uniq] using h₁
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.add_mul
Proof state before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
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₂ : M
IH : ∀ y₂ ≤ y₁, Exponential x₂ y₂ → Exponential (x₁ + x₂) (y₁ * y₂)
⊢ ∀ y₂ ≤ y₁, Exponential (x₂ + 1) y₂ → Exponential (x₁ + (x₂ + 1)) (y₁ * y₂)
Tactic:
intro y₂ hy 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✝ ⊧ₘ* 𝐈𝚫₀
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₂ : M
IH : ∀ y₂ ≤ y₁, Exponential x₂ y₂ → Exponential (x₁ + x₂) (y₁ * y₂)
y₂ : M
hy : y₂ ≤ y₁
h₂ : Exponential (x₂ + 1) y₂
⊢ Exponential (x₁ + (x₂ + 1)) (y₁ * y₂)
Theorem: LO.FirstOrder.Arith.Model.Exponential.add_mul
Proof state before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
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₂ : M
IH : ∀ y₂ ≤ y₁, Exponential x₂ y₂ → Exponential (x₁ + x₂) (y₁ * y₂)
y₂ : M
hy : y₂ ≤ y₁
h₂ : Exponential (x₂ + 1) y₂
⊢ Exponential (x₁ + (x₂ + 1)) (y₁ * y₂)
Tactic:
rcases exponential_succ.mp h₂ with ⟨y₂, rfl, H₂⟩
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✝ ⊧ₘ* 𝐈𝚫₀
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₂ : M
IH : ∀ y₂ ≤ y₁, Exponential x₂ y₂ → Exponential (x₁ + x₂) (y₁ * y₂)
y₂ : M
H₂ : Exponential x₂ y₂
hy : 2 * y₂ ≤ y₁
h₂ : Exponential (x₂ + 1) (2 * y₂)
⊢ Exponential (x₁ + (x₂ + 1)) (y₁ * (2 * y₂))
Theorem: LO.FirstOrder.Arith.Model.Exponential.add_mul
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✝ ⊧ₘ* 𝐈𝚫₀
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₂ : M
IH : ∀ y₂ ≤ y₁, Exponential x₂ y₂ → Exponential (x₁ + x₂) (y₁ * y₂)
y₂ : M
H₂ : Exponential x₂ y₂
hy : 2 * y₂ ≤ y₁
h₂ : Exponential (x₂ + 1) (2 * y₂)
⊢ Exponential (x₁ + (x₂ + 1)) (y₁ * (2 * y₂))
Tactic:
have : Exponential (x₁ + x₂) (y₁ * y₂) := IH y₂ (le_trans (by simp) hy) H₂
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✝ ⊧ₘ* 𝐈𝚫₀
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₂ : M
IH : ∀ y₂ ≤ y₁, Exponential x₂ y₂ → Exponential (x₁ + x₂) (y₁ * y₂)
y₂ : M
H₂ : Exponential x₂ y₂
hy : 2 * y₂ ≤ y₁
h₂ : Exponential (x₂ + 1) (2 * y₂)
this : Exponential (x₁ + x₂) (y₁ * y₂)
⊢ Exponential (x₁ + (x₂ + 1)) (y₁ * (2 * y₂))
Theorem: LO.FirstOrder.Arith.Model.Exponential.add_mul
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✝ ⊧ₘ* 𝐈𝚫₀
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₂ : M
IH : ∀ y₂ ≤ y₁, Exponential x₂ y₂ → Exponential (x₁ + x₂) (y₁ * y₂)
y₂ : M
H₂ : Exponential x₂ y₂
hy : 2 * y₂ ≤ y₁
h₂ : Exponential (x₂ + 1) (2 * y₂)
this : Exponential (x₁ + x₂) (y₁ * y₂)
⊢ Exponential (x₁ + (x₂ + 1)) (y₁ * (2 * y₂))
Tactic:
simpa [←add_assoc, mul_left_comm y₁ 2 y₂] using this.succ
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.add_mul
Proof state before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
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₂ : M
IH : ∀ y₂ ≤ y₁, Exponential x₂ y₂ → Exponential (x₁ + x₂) (y₁ * y₂)
y₂ : M
H₂ : Exponential x₂ y₂
hy : 2 * y₂ ≤ y₁
h₂ : Exponential (x₂ + 1) (2 * y₂)
⊢ y₂ ≤ 2 * y₂
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.range_exists
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
x : M
⊢ ∃ y, Exponential x y
Tactic:
induction x using induction_iSigmaOne
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 x => ∃ y, Exponential x y

case zero
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
⊢ ∃ y, Exponential 0 y

case succ
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, Exponential x✝ y
⊢ ∃ y, Exponential (x✝ + 1) y
Theorem: LO.FirstOrder.Arith.Model.Exponential.range_exists
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, Exponential 0 y
Tactic:
case zero => exact ⟨1, by simp⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.range_exists
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
x : M
IH : ∃ y, Exponential x y
⊢ ∃ y, Exponential (x + 1) y
Tactic:
case succ x IH =>
  rcases IH with ⟨y, IH⟩
  exact ⟨2 * y, IH.succ⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.range_exists
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 x => ∃ y, Exponential x y
Tactic:
apply Definable.ex
Proof state after:
case hP.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
⊢ Definable ℒₒᵣ (𝚺, 0 + 1) fun w => Exponential ((fun x => w x.succ) 0) (w 0)
Theorem: LO.FirstOrder.Arith.Model.Exponential.range_exists
Proof state before:
case hP.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
⊢ Definable ℒₒᵣ (𝚺, 0 + 1) fun w => Exponential ((fun x => w x.succ) 0) (w 0)
Tactic:
definability
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.range_exists
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, Exponential 0 y
Tactic:
exact ⟨1, by simp⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.range_exists
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 0 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.range_exists
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
x : M
IH : ∃ y, Exponential x y
⊢ ∃ y, Exponential (x + 1) y
Tactic:
rcases IH with ⟨y, IH⟩
Proof state after:
case 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
IH : Exponential x y
⊢ ∃ y, Exponential (x + 1) y
Theorem: LO.FirstOrder.Arith.Model.Exponential.range_exists
Proof state before:
case 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
IH : Exponential x y
⊢ ∃ y, Exponential (x + 1) y
Tactic:
exact ⟨2 * y, IH.succ⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.range_exists_unique
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
x : M
⊢ ∃! y, Exponential x y
Tactic:
rcases range_exists x with ⟨y, h⟩
Proof state after:
case 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
⊢ ∃! y, Exponential x y
Theorem: LO.FirstOrder.Arith.Model.Exponential.range_exists_unique
Proof state before:
case 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
⊢ ∃! y, Exponential x y
Tactic:
exact ExistsUnique.intro y h (by intro y' h'; exact h'.uniq h)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.range_exists_unique
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
⊢ ∀ (y_1 : M), Exponential x y_1 → y_1 = y
Tactic:
intro y' 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
y' : M
h' : Exponential x y'
⊢ y' = y
Theorem: LO.FirstOrder.Arith.Model.Exponential.range_exists_unique
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
y' : M
h' : Exponential x y'
⊢ y' = y
Tactic:
exact h'.uniq h
Proof state after:
no goals