Theorem: LO.FirstOrder.Arith.Model.Nuon.exists_unique (Arithmetization/OmegaOne/Nuon.lean)

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A : M
⊢ ∃! n, Nuon A n
Tactic:
rcases show ∃ n, Nuon A n from NuonAux.exists (by simp) with ⟨n, hn⟩
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A n : M
hn : Nuon A n
⊢ ∃! n, Nuon A n

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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A n : M
hn : Nuon A n
⊢ ∃! n, Nuon A n
Tactic:
exact ExistsUnique.intro n hn (fun n' hn' ↦ hn'.uniq hn)
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A : M
⊢ ‖A‖ ≤ ‖A‖
Tactic:
simp
State after:
no goals