Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.succ_elim (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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
n A k : M
hk : k ≤ ‖A‖
H : NuonAux A (k + 1) n
⊢ ∃ n', n = n' + fbit A k ∧ NuonAux A k n'
Tactic:
rcases NuonAux.exists hk with ⟨n', 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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
n A k : M
hk : k ≤ ‖A‖
H : NuonAux A (k + 1) n
n' : M
H' : NuonAux A k n'
⊢ ∃ n', n = n' + fbit A k ∧ NuonAux A k 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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
n A k : M
hk : k ≤ ‖A‖
H : NuonAux A (k + 1) n
n' : M
H' : NuonAux A k n'
⊢ ∃ n', n = n' + fbit A k ∧ NuonAux A k n'
Tactic:
rcases H.uniq (H'.succ hk)
State after:
case intro.refl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A k : M
hk : k ≤ ‖A‖
n' : M
H' : NuonAux A k n'
H : NuonAux A (k + 1) (n' + fbit A k)
⊢ ∃ n'_1, n' + fbit A k = n'_1 + fbit A k ∧ NuonAux A k n'_1

State before:
case intro.refl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A k : M
hk : k ≤ ‖A‖
n' : M
H' : NuonAux A k n'
H : NuonAux A (k + 1) (n' + fbit A k)
⊢ ∃ n'_1, n' + fbit A k = n'_1 + fbit A k ∧ NuonAux A k n'_1
Tactic:
exact ⟨n', rfl, H'⟩
State after:
no goals