internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.Exponential.uniq
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 ⊧ₘ* 𝐈𝚫₀
y₂ : M
⊢ ∀ x < y₂, ∀ y₁ ≤ y₂, Exponential x y₁ → Exponential x y₂ → y₁ = y₂
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✝ ⊧ₘ* 𝐈𝚫₀
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 < y₂, ∀ y₁ ≤ y₂, Exponential x y₁ → Exponential x y₂ → y₁ = y₂

case ind
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✝ : M
a✝ : ∀ y < x✝, ∀ x < y, ∀ y₁ ≤ y, Exponential x y₁ → Exponential x y → y₁ = y
⊢ ∀ x < x✝, ∀ y₁ ≤ x✝, Exponential x y₁ → Exponential x x✝ → y₁ = x✝
Theorem: LO.FirstOrder.Arith.Model.Exponential.uniq
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 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 y₁ y₂ : M}, Exponential x y₁ → Exponential x y₂ → y₁ ≤ y₂ → y₁ = y₂
h : ¬y₁ ≤ y₂
⊢ y₁ = y₂
Tactic:
exact Eq.symm <| this h₂ h₁ (show y₂ ≤ y₁ from le_of_not_ge h)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.uniq
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 ⊧ₘ* 𝐈𝚫₀
y₂ : M
this : ∀ x < y₂, ∀ y₁ ≤ y₂, Exponential x y₁ → Exponential x y₂ → y₁ = y₂
⊢ ∀ {x y₁ : M}, Exponential x y₁ → Exponential x y₂ → y₁ ≤ y₂ → y₁ = y₂
Tactic:
intro x y₁ h₁ 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 ⊧ₘ* 𝐈𝚫₀
y₂ : M
this : ∀ x < y₂, ∀ y₁ ≤ y₂, Exponential x y₁ → Exponential x y₂ → y₁ = y₂
x y₁ : M
h₁ : Exponential x y₁
h₂ : Exponential x y₂
hy : y₁ ≤ y₂
⊢ y₁ = y₂
Theorem: LO.FirstOrder.Arith.Model.Exponential.uniq
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 ⊧ₘ* 𝐈𝚫₀
y₂ : M
this : ∀ x < y₂, ∀ y₁ ≤ y₂, Exponential x y₁ → Exponential x y₂ → y₁ = y₂
x y₁ : M
h₁ : Exponential x y₁
h₂ : Exponential x y₂
hy : y₁ ≤ y₂
⊢ y₁ = y₂
Tactic:
exact this x h₂.lt y₁ hy h₁ h₂
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.uniq
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 ⊧ₘ* 𝐈𝚫₀
⊢ 𝚺₀-Predicate fun {y₂} => ∀ x < y₂, ∀ y₁ ≤ y₂, Exponential x y₁ → Exponential x y₂ → y₁ = y₂
Tactic:
definability
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.uniq
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 ⊧ₘ* 𝐈𝚫₀
y₂ : M
IH : ∀ y < y₂, ∀ x < y, ∀ y₁ ≤ y, Exponential x y₁ → Exponential x y → y₁ = y
⊢ ∀ x < y₂, ∀ y₁ ≤ y₂, Exponential x y₁ → Exponential x y₂ → y₁ = y₂
Tactic:
intro x _ y₁ h 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✝ ⊧ₘ* 𝐈𝚫₀
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 < y₂, ∀ x < y, ∀ y₁ ≤ y, Exponential x y₁ → Exponential x y → y₁ = y
x : M
a✝ : x < y₂
y₁ : M
h : y₁ ≤ y₂
h₁ : Exponential x y₁
h₂ : Exponential x y₂
⊢ y₁ = y₂
Theorem: LO.FirstOrder.Arith.Model.Exponential.uniq
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 ⊧ₘ* 𝐈𝚫₀
y₂ : M
IH : ∀ y < y₂, ∀ x < y, ∀ y₁ ≤ y, Exponential x y₁ → Exponential x y → y₁ = y
x : M
a✝ : x < y₂
y₁ : M
h : y₁ ≤ y₂
h₁ : Exponential x y₁
h₂ : Exponential x y₂
⊢ y₁ = 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✝ ⊧ₘ* 𝐈𝚫₀
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 < y₂, ∀ x < y, ∀ y₁ ≤ y, Exponential x y₁ → Exponential x y → y₁ = y
y₁ : M
h : y₁ ≤ y₂
a✝ : 0 < y₂
h₁ : Exponential 0 y₁
h₂ : Exponential 0 y₂
⊢ y₁ = 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✝ ⊧ₘ* 𝐈𝚫₀
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 < y₂, ∀ x < y, ∀ y₁ ≤ y, Exponential x y₁ → Exponential x y → y₁ = y
y₁ : M
h : y₁ ≤ y₂
x : M
a✝ : x + 1 < y₂
h₁ : Exponential (x + 1) y₁
h₂ : Exponential (x + 1) y₂
⊢ y₁ = y₂
Theorem: LO.FirstOrder.Arith.Model.Exponential.uniq
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✝ ⊧ₘ* 𝐈𝚫₀
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 < y₂, ∀ x < y, ∀ y₁ ≤ y, Exponential x y₁ → Exponential x y → y₁ = y
y₁ : M
h : y₁ ≤ y₂
a✝ : 0 < y₂
h₁ : Exponential 0 y₁
h₂ : Exponential 0 y₂
⊢ y₁ = y₂
Tactic:
simp [h₁.zero_uniq, h₂.zero_uniq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.uniq
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✝ ⊧ₘ* 𝐈𝚫₀
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 < y₂, ∀ x < y, ∀ y₁ ≤ y, Exponential x y₁ → Exponential x y → y₁ = y
y₁ : M
h : y₁ ≤ y₂
x : M
a✝ : x + 1 < y₂
h₁ : Exponential (x + 1) y₁
h₂ : Exponential (x + 1) y₂
⊢ y₁ = y₂
Tactic:
rcases exponential_succ.mp h₁ with ⟨y₁, rfl, h₁'⟩
Proof state after:
case 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✝ ⊧ₘ* 𝐈𝚫₀
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 < y₂, ∀ x < y, ∀ y₁ ≤ y, Exponential x y₁ → Exponential x y → y₁ = y
x : M
a✝ : x + 1 < y₂
h₂ : Exponential (x + 1) y₂
y₁ : M
h₁' : Exponential x y₁
h : 2 * y₁ ≤ y₂
h₁ : Exponential (x + 1) (2 * y₁)
⊢ 2 * y₁ = y₂
Theorem: LO.FirstOrder.Arith.Model.Exponential.uniq
Proof state before:
case 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✝ ⊧ₘ* 𝐈𝚫₀
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 < y₂, ∀ x < y, ∀ y₁ ≤ y, Exponential x y₁ → Exponential x y → y₁ = y
x : M
a✝ : x + 1 < y₂
h₂ : Exponential (x + 1) y₂
y₁ : M
h₁' : Exponential x y₁
h : 2 * y₁ ≤ y₂
h₁ : Exponential (x + 1) (2 * y₁)
⊢ 2 * y₁ = y₂
Tactic:
rcases exponential_succ.mp h₂ with ⟨y₂, rfl, h₂'⟩
Proof state after:
case 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✝ ⊧ₘ* 𝐈𝚫₀
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₁)
y₂ : M
h₂' : Exponential x y₂
IH : ∀ y < 2 * y₂, ∀ x < y, ∀ y₁ ≤ y, Exponential x y₁ → Exponential x y → y₁ = y
a✝ : x + 1 < 2 * y₂
h₂ : Exponential (x + 1) (2 * y₂)
h : 2 * y₁ ≤ 2 * y₂
⊢ 2 * y₁ = 2 * y₂
Theorem: LO.FirstOrder.Arith.Model.Exponential.uniq
Proof state before:
case 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✝ ⊧ₘ* 𝐈𝚫₀
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₁)
y₂ : M
h₂' : Exponential x y₂
IH : ∀ y < 2 * y₂, ∀ x < y, ∀ y₁ ≤ y, Exponential x y₁ → Exponential x y → y₁ = y
a✝ : x + 1 < 2 * y₂
h₂ : Exponential (x + 1) (2 * y₂)
h : 2 * y₁ ≤ 2 * y₂
⊢ 2 * y₁ = 2 * y₂
Tactic:
have : y₁ = y₂ := IH y₂ (lt_mul_of_pos_of_one_lt_left h₂'.range_pos one_lt_two)
  x h₂'.lt y₁ (by simpa using h) h₁' h₂'
Proof state after:
case 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✝ ⊧ₘ* 𝐈𝚫₀
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₁)
y₂ : M
h₂' : Exponential x y₂
IH : ∀ y < 2 * y₂, ∀ x < y, ∀ y₁ ≤ y, Exponential x y₁ → Exponential x y → y₁ = y
a✝ : x + 1 < 2 * y₂
h₂ : Exponential (x + 1) (2 * y₂)
h : 2 * y₁ ≤ 2 * y₂
this : y₁ = y₂
⊢ 2 * y₁ = 2 * y₂
Theorem: LO.FirstOrder.Arith.Model.Exponential.uniq
Proof state before:
case 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✝ ⊧ₘ* 𝐈𝚫₀
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₁)
y₂ : M
h₂' : Exponential x y₂
IH : ∀ y < 2 * y₂, ∀ x < y, ∀ y₁ ≤ y, Exponential x y₁ → Exponential x y → y₁ = y
a✝ : x + 1 < 2 * y₂
h₂ : Exponential (x + 1) (2 * y₂)
h : 2 * y₁ ≤ 2 * y₂
this : y₁ = y₂
⊢ 2 * y₁ = 2 * y₂
Tactic:
simp [this]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.uniq
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₁
h₁ : Exponential (x + 1) (2 * y₁)
y₂ : M
h₂' : Exponential x y₂
IH : ∀ y < 2 * y₂, ∀ x < y, ∀ y₁ ≤ y, Exponential x y₁ → Exponential x y → y₁ = y
a✝ : x + 1 < 2 * y₂
h₂ : Exponential (x + 1) (2 * y₂)
h : 2 * y₁ ≤ 2 * y₂
⊢ y₁ ≤ y₂
Tactic:
simpa using h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.inj
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 : M
⊢ Exponential x₁ y → Exponential x₂ y → x₁ = x₂
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 : M
h₁ : Exponential x₁ y
h₂ : Exponential x₂ y
⊢ x₁ = x₂
Theorem: LO.FirstOrder.Arith.Model.Exponential.inj
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 : M
h₁ : Exponential x₁ y
h₂ : Exponential x₂ y
⊢ x₁ = x₂
Tactic:
revert x₁ 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 ⊧ₘ* 𝐈𝚫₀
y : M
⊢ ∀ {x₁ x₂ : M}, Exponential x₁ y → Exponential x₂ y → x₁ = x₂
Theorem: LO.FirstOrder.Arith.Model.Exponential.inj
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y : M
⊢ ∀ {x₁ x₂ : M}, Exponential x₁ y → Exponential x₂ y → x₁ = x₂
Tactic:
suffices ∀ x₁ < y, ∀ x₂ < y, Exponential x₁ y → Exponential x₂ y → x₁ = x₂ by
  intro x₁ x₂ h₁ h₂; exact this x₁ h₁.lt 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 ⊧ₘ* 𝐈𝚫₀
y : M
⊢ ∀ x₁ < y, ∀ x₂ < y, Exponential x₁ y → Exponential x₂ y → x₁ = x₂
Theorem: LO.FirstOrder.Arith.Model.Exponential.inj
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y : M
⊢ ∀ x₁ < 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 ⊧ₘ* 𝐈𝚫₀
⊢ 𝚺₀-Predicate fun {y} => ∀ x₁ < 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✝ : M
a✝ : ∀ y < x✝, ∀ x₁ < y, ∀ x₂ < y, Exponential x₁ y → Exponential x₂ y → x₁ = x₂
⊢ ∀ x₁ < x✝, ∀ x₂ < x✝, Exponential x₁ x✝ → Exponential x₂ x✝ → x₁ = x₂
Theorem: LO.FirstOrder.Arith.Model.Exponential.inj
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y : M
this : ∀ x₁ < y, ∀ x₂ < y, Exponential x₁ y → Exponential x₂ y → x₁ = x₂
⊢ ∀ {x₁ x₂ : M}, Exponential x₁ y → Exponential x₂ y → x₁ = x₂
Tactic:
intro x₁ 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 ⊧ₘ* 𝐈𝚫₀
y : M
this : ∀ x₁ < y, ∀ x₂ < y, Exponential x₁ y → Exponential x₂ y → x₁ = x₂
x₁ x₂ : M
h₁ : Exponential x₁ y
h₂ : Exponential x₂ y
⊢ x₁ = x₂
Theorem: LO.FirstOrder.Arith.Model.Exponential.inj
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y : M
this : ∀ x₁ < y, ∀ x₂ < y, Exponential x₁ y → Exponential x₂ y → x₁ = x₂
x₁ x₂ : M
h₁ : Exponential x₁ y
h₂ : Exponential x₂ y
⊢ x₁ = x₂
Tactic:
exact this x₁ h₁.lt x₂ h₂.lt h₁ h₂
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.inj
Proof state before:
case hP
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ 𝚺₀-Predicate fun {y} => ∀ x₁ < y, ∀ x₂ < y, Exponential x₁ y → Exponential x₂ y → x₁ = x₂
Tactic:
definability
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.inj
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y : M
IH : ∀ y_1 < y, ∀ x₁ < y_1, ∀ x₂ < y_1, Exponential x₁ y_1 → Exponential x₂ y_1 → x₁ = x₂
⊢ ∀ x₁ < y, ∀ x₂ < y, Exponential x₁ y → Exponential x₂ y → x₁ = x₂
Tactic:
intro x₁ _ 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 ⊧ₘ* 𝐈𝚫₀
y : M
IH : ∀ y_1 < y, ∀ x₁ < y_1, ∀ x₂ < y_1, Exponential x₁ y_1 → Exponential x₂ y_1 → x₁ = x₂
x₁ : M
a✝¹ : x₁ < y
x₂ : M
a✝ : x₂ < y
h₁ : Exponential x₁ y
h₂ : Exponential x₂ y
⊢ x₁ = x₂
Theorem: LO.FirstOrder.Arith.Model.Exponential.inj
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y : M
IH : ∀ y_1 < y, ∀ x₁ < y_1, ∀ x₂ < y_1, Exponential x₁ y_1 → Exponential x₂ y_1 → x₁ = x₂
x₁ : M
a✝¹ : x₁ < 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 ⊧ₘ* 𝐈𝚫₀
y : M
IH : ∀ y_1 < y, ∀ x₁ < y_1, ∀ x₂ < y_1, Exponential x₁ y_1 → Exponential x₂ y_1 → x₁ = x₂
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 ⊧ₘ* 𝐈𝚫₀
y : M
IH : ∀ y_1 < y, ∀ x₁ < y_1, ∀ x₂ < y_1, Exponential x₁ y_1 → Exponential x₂ y_1 → x₁ = x₂
a✝¹ : 0 < y
h₁ : Exponential 0 y
x₂ : M
a✝ : x₂ + 1 < y
h₂ : Exponential (x₂ + 1) y
⊢ 0 = x₂ + 1

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 ⊧ₘ* 𝐈𝚫₀
y : M
IH : ∀ y_1 < y, ∀ x₁ < y_1, ∀ x₂ < y_1, Exponential x₁ y_1 → Exponential x₂ y_1 → x₁ = x₂
x₁ : M
a✝¹ : x₁ + 1 < y
h₁ : Exponential (x₁ + 1) y
a✝ : 0 < y
h₂ : Exponential 0 y
⊢ x₁ + 1 = 0

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 ⊧ₘ* 𝐈𝚫₀
y : M
IH : ∀ y_1 < y, ∀ x₁ < y_1, ∀ x₂ < y_1, Exponential x₁ y_1 → Exponential x₂ y_1 → x₁ = x₂
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.inj
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 ⊧ₘ* 𝐈𝚫₀
y : M
IH : ∀ y_1 < y, ∀ x₁ < y_1, ∀ x₂ < y_1, Exponential x₁ y_1 → Exponential x₂ y_1 → x₁ = x₂
a✝¹ : 0 < y
h₁ : Exponential 0 y
a✝ : 0 < y
h₂ : Exponential 0 y
⊢ 0 = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.inj
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 ⊧ₘ* 𝐈𝚫₀
y : M
IH : ∀ y_1 < y, ∀ x₁ < y_1, ∀ x₂ < y_1, Exponential x₁ y_1 → Exponential x₂ y_1 → x₁ = x₂
a✝¹ : 0 < y
h₁ : Exponential 0 y
x₂ : M
a✝ : x₂ + 1 < y
h₂ : Exponential (x₂ + 1) y
⊢ 0 = x₂ + 1
Tactic:
rcases 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₂ : M
IH : ∀ y < 1, ∀ x₁ < 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
⊢ 0 = x₂ + 1
Theorem: LO.FirstOrder.Arith.Model.Exponential.inj
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₂ : M
IH : ∀ y < 1, ∀ x₁ < 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
⊢ 0 = x₂ + 1
Tactic:
rcases exponential_succ.mp h₂ with ⟨z, hz⟩
Proof state after:
case inl.inr.intro.refl.intro
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 < 1, ∀ x₁ < 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
z : M
hz : 1 = 2 * z ∧ Exponential x₂ z
⊢ 0 = x₂ + 1
Theorem: LO.FirstOrder.Arith.Model.Exponential.inj
Proof state before:
case inl.inr.intro.refl.intro
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 < 1, ∀ x₁ < 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
z : M
hz : 1 = 2 * z ∧ Exponential x₂ z
⊢ 0 = x₂ + 1
Tactic:
simp at hz
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.inj
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 ⊧ₘ* 𝐈𝚫₀
y : M
IH : ∀ y_1 < y, ∀ x₁ < y_1, ∀ x₂ < y_1, Exponential x₁ y_1 → Exponential x₂ y_1 → x₁ = x₂
x₁ : M
a✝¹ : x₁ + 1 < y
h₁ : Exponential (x₁ + 1) y
a✝ : 0 < y
h₂ : Exponential 0 y
⊢ x₁ + 1 = 0
Tactic:
rcases h₂.zero_uniq
Proof state after:
case inr.intro.inl.refl
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 < 1, ∀ x₁ < y, ∀ x₂ < y, Exponential x₁ y → Exponential x₂ y → x₁ = x₂
a✝¹ : x₁ + 1 < 1
h₁ : Exponential (x₁ + 1) 1
a✝ : 0 < 1
h₂ : Exponential 0 1
⊢ x₁ + 1 = 0
Theorem: LO.FirstOrder.Arith.Model.Exponential.inj
Proof state before:
case inr.intro.inl.refl
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 < 1, ∀ x₁ < y, ∀ x₂ < y, Exponential x₁ y → Exponential x₂ y → x₁ = x₂
a✝¹ : x₁ + 1 < 1
h₁ : Exponential (x₁ + 1) 1
a✝ : 0 < 1
h₂ : Exponential 0 1
⊢ x₁ + 1 = 0
Tactic:
rcases exponential_succ.mp h₁ with ⟨z, hz⟩
Proof state after:
case inr.intro.inl.refl.intro
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 < 1, ∀ x₁ < y, ∀ x₂ < y, Exponential x₁ y → Exponential x₂ y → x₁ = x₂
a✝¹ : x₁ + 1 < 1
h₁ : Exponential (x₁ + 1) 1
a✝ : 0 < 1
h₂ : Exponential 0 1
z : M
hz : 1 = 2 * z ∧ Exponential x₁ z
⊢ x₁ + 1 = 0
Theorem: LO.FirstOrder.Arith.Model.Exponential.inj
Proof state before:
case inr.intro.inl.refl.intro
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 < 1, ∀ x₁ < y, ∀ x₂ < y, Exponential x₁ y → Exponential x₂ y → x₁ = x₂
a✝¹ : x₁ + 1 < 1
h₁ : Exponential (x₁ + 1) 1
a✝ : 0 < 1
h₂ : Exponential 0 1
z : M
hz : 1 = 2 * z ∧ Exponential x₁ z
⊢ x₁ + 1 = 0
Tactic:
simp at hz
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.inj
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 ⊧ₘ* 𝐈𝚫₀
y : M
IH : ∀ y_1 < y, ∀ x₁ < y_1, ∀ x₂ < y_1, Exponential x₁ y_1 → Exponential x₂ y_1 → x₁ = x₂
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, 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)
⊢ 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)
⊢ x₁ + 1 = x₂ + 1
Tactic:
have hy₂ : Exponential x₂ y := h₂.of_succ_two_mul
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
⊢ x₁ + 1 = x₂ + 1