Theorem: LO.FirstOrder.Arith.Model.Nuon.bex_eq_le_iff (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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z : M
p : M → Prop
b : M
⊢ (∃ a ≤ z, a = b ∧ p a) → b ≤ z ∧ p b
Tactic:
rintro ⟨a, hp, rfl, hr⟩
State after:
case intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z : M
p : M → Prop
a : M
hp : a ≤ z
hr : p a
⊢ a ≤ z ∧ p a

State before:
case intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z : M
p : M → Prop
a : M
hp : a ≤ z
hr : p a
⊢ a ≤ z ∧ p a
Tactic:
exact ⟨hp, hr⟩
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z : M
p : M → Prop
b : M
⊢ b ≤ z ∧ p b → ∃ a ≤ z, a = b ∧ p a
Tactic:
rintro ⟨hp, hr⟩
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z : M
p : M → Prop
b : M
hp : b ≤ z
hr : p b
⊢ ∃ a ≤ z, a = b ∧ p a

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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z : M
p : M → Prop
b : M
hp : b ≤ z
hr : p b
⊢ ∃ a ≤ z, a = b ∧ p a
Tactic:
exact ⟨b, hp, rfl, hr⟩
State after:
no goals