Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.succ_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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
n A k : M
hk : k ≤ ‖A‖
⊢ NuonAux A (k + 1) (n + fbit A k) ↔ NuonAux A k n
Tactic:
constructor
State after:
case mp
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‖
⊢ NuonAux A (k + 1) (n + fbit A k) → NuonAux A k n

case mpr
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‖
⊢ NuonAux A k n → NuonAux A (k + 1) (n + fbit A k)

State before:
case mp
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‖
⊢ NuonAux A (k + 1) (n + fbit A k) → NuonAux A k n
Tactic:
intro H
State after:
case mp
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 + fbit A k)
⊢ NuonAux A k n

State before:
case mp
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 + fbit A k)
⊢ NuonAux A k n
Tactic:
rcases NuonAux.exists hk with ⟨n', H'⟩
State after:
case mp.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 + fbit A k)
n' : M
H' : NuonAux A k n'
⊢ NuonAux A k n

State before:
case mp.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 + fbit A k)
n' : M
H' : NuonAux A k n'
⊢ NuonAux A k n
Tactic:
rcases show n' = n from by simpa using (H'.succ hk).uniq H
State after:
case mp.intro.refl
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 + fbit A k)
H' : NuonAux A k n
⊢ NuonAux A k n

State before:
case mp.intro.refl
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 + fbit A k)
H' : NuonAux A k n
⊢ NuonAux A k n
Tactic:
exact 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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
n A k : M
hk : k ≤ ‖A‖
H : NuonAux A (k + 1) (n + fbit A k)
n' : M
H' : NuonAux A k n'
⊢ n' = n
Tactic:
simpa using (H'.succ hk).uniq H
State after:
no goals