Theorem: LO.FirstOrder.Arith.Model.Exponential.uniq (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 y₁ y₂ : M
⊢ Exponential x y₁ → Exponential x y₂ → 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 y₁ y₂ : M
h₁ : Exponential x y₁
h₂ : Exponential x y₂
⊢ 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 y₁ y₂ : M
h₁ : Exponential x y₁
h₂ : Exponential x y₂
⊢ y₁ = y₂
Tactic:
wlog h : y₁ ≤ y₂
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 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₂

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₁ y₂ : M
h₁ : Exponential x y₁
h₂ : Exponential x y₂
h : y₁ ≤ y₂
⊢ 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✝ ⊧ₘ* 𝐈𝚫₀
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₂
h : y₁ ≤ y₂
⊢ y₁ = y₂
Tactic:
revert x h y₁
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
⊢ ∀ {x y₁ : M}, Exponential x y₁ → Exponential x y₂ → y₁ ≤ y₂ → 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✝ ⊧ₘ* 𝐈𝚫₀
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₁ : M}, Exponential x y₁ → Exponential x y₂ → y₁ ≤ y₂ → y₁ = y₂
Tactic:
suffices ∀ x < y₂, ∀ y₁ ≤ y₂, Exponential x y₁ → Exponential x y₂ → y₁ = y₂ by
  intro x y₁ h₁ h₂ hy; exact this x h₂.lt y₁ hy 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✝ ⊧ₘ* 𝐈𝚫₀
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₂

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

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

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

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

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

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₁'⟩
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₂

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

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

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]
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✝ ⊧ₘ* 𝐈𝚫₀
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
State after:
no goals