Theorem: LO.FirstOrder.Arith.Model.Exponential.inj (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 : M
⊢ Exponential x₁ y → Exponential x₂ y → x₁ = x₂
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 : M
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 : M
h₁ : Exponential x₁ y
h₂ : Exponential x₂ y
⊢ x₁ = x₂
Tactic:
revert x₁ 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 ⊧ₘ* 𝐈𝚫₀
y : M
⊢ ∀ {x₁ x₂ : M}, 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 ⊧ₘ* 𝐈𝚫₀
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₂
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₂

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

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

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₂
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 ⊧ₘ* 𝐈𝚫₀
⊢ 𝚺₀-Predicate fun {y} => ∀ x₁ < 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 ⊧ₘ* 𝐈𝚫₀
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₂
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₂

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

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
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 ⊧ₘ* 𝐈𝚫₀
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
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

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

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
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 ⊧ₘ* 𝐈𝚫₀
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
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

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

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
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 ⊧ₘ* 𝐈𝚫₀
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₁⟩
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

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

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

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