Theorem: LO.FirstOrder.Arith.Model.hash_exists_unique (Arithmetization/OmegaOne/Basic.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 : M
⊢ ∃! z, Exponential (‖x‖ * ‖y‖) z
Tactic:
wlog le : x ≤ 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 : M
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 : M), x ≤ y → ∃! z, Exponential (‖x‖ * ‖y‖) z
le : ¬x ≤ y
⊢ ∃! z, Exponential (‖x‖ * ‖y‖) z

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
le : x ≤ y
⊢ ∃! z, Exponential (‖x‖ * ‖y‖) z

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
le : x ≤ y
⊢ ∃! z, Exponential (‖x‖ * ‖y‖) z
Tactic:
rcases exists_exponential_sq_length y with ⟨z, h⟩
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✝ ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
x y : M
le : x ≤ y
z : M
h : Exponential (‖y‖ ^ 2) z
⊢ ∃! z, Exponential (‖x‖ * ‖y‖) z

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✝ ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
x y : M
le : x ≤ y
z : M
h : Exponential (‖y‖ ^ 2) z
⊢ ∃! z, Exponential (‖x‖ * ‖y‖) z
Tactic:
have : ‖x‖ * ‖y‖ < ‖z‖ :=
  lt_of_le_of_lt (by simp [sq]; exact mul_le_mul_right (length_monotone le)) h.lt_length
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✝ ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
x y : M
le : x ≤ y
z : M
h : Exponential (‖y‖ ^ 2) z
this : ‖x‖ * ‖y‖ < ‖z‖
⊢ ∃! z, Exponential (‖x‖ * ‖y‖) z

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✝ ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
x y : M
le : x ≤ y
z : M
h : Exponential (‖y‖ ^ 2) z
this : ‖x‖ * ‖y‖ < ‖z‖
⊢ ∃! z, Exponential (‖x‖ * ‖y‖) z
Tactic:
have : Exponential (‖x‖ * ‖y‖) (bexp z (‖x‖ * ‖y‖)) := exp_bexp_of_lt (a := z) (x := ‖x‖ * ‖y‖) this
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✝ ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
x y : M
le : x ≤ y
z : M
h : Exponential (‖y‖ ^ 2) z
this✝ : ‖x‖ * ‖y‖ < ‖z‖
this : Exponential (‖x‖ * ‖y‖) (bexp z (‖x‖ * ‖y‖))
⊢ ∃! z, Exponential (‖x‖ * ‖y‖) z

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✝ ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
x y : M
le : x ≤ y
z : M
h : Exponential (‖y‖ ^ 2) z
this✝ : ‖x‖ * ‖y‖ < ‖z‖
this : Exponential (‖x‖ * ‖y‖) (bexp z (‖x‖ * ‖y‖))
⊢ ∃! z, Exponential (‖x‖ * ‖y‖) z
Tactic:
exact ExistsUnique.intro (bexp z (‖x‖ * ‖y‖)) this (fun z' H' ↦ H'.uniq this)
State after:
no goals

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 : M
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 : M), x ≤ y → ∃! z, Exponential (‖x‖ * ‖y‖) z
le : ¬x ≤ y
⊢ ∃! z, Exponential (‖x‖ * ‖y‖) z
Tactic:
simpa [mul_comm] using this y x (le_of_not_ge le)
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
le : x ≤ y
z : M
h : Exponential (‖y‖ ^ 2) z
⊢ ‖x‖ * ‖y‖ ≤ ‖y‖ ^ 2
Tactic:
simp [sq]
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
le : x ≤ y
z : M
h : Exponential (‖y‖ ^ 2) z
⊢ ‖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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
x y : M
le : x ≤ y
z : M
h : Exponential (‖y‖ ^ 2) z
⊢ ‖x‖ * ‖y‖ ≤ ‖y‖ * ‖y‖
Tactic:
exact mul_le_mul_right (length_monotone le)
State after:
no goals