Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.exists (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 k : M
hk : k ≤ ‖A‖
⊢ ∃ n, NuonAux A k n
Tactic:
suffices ∃ n ≤ k, NuonAux A k n by
  rcases this with ⟨n, _, h⟩; exact ⟨n, h⟩
State after:
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 ≤ k, NuonAux A k n

State before:
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 ≤ k, NuonAux A k n
Tactic:
revert hk
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A k : M
⊢ k ≤ ‖A‖ → ∃ n ≤ k, NuonAux A k n

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A k : M
⊢ k ≤ ‖A‖ → ∃ n ≤ k, NuonAux A k n
Tactic:
induction k using induction_iSigmaZero
State after:
case hP
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A : M
⊢ 𝚺₀-Predicate fun {k} => k ≤ ‖A‖ → ∃ n ≤ k, NuonAux A k n

case zero
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A : M
⊢ 0 ≤ ‖A‖ → ∃ n ≤ 0, NuonAux A 0 n

case succ
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A x✝ : M
a✝ : x✝ ≤ ‖A‖ → ∃ n ≤ x✝, NuonAux A x✝ n
⊢ x✝ + 1 ≤ ‖A‖ → ∃ n ≤ x✝ + 1, NuonAux A (x✝ + 1) n

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
⊢ 0 ≤ ‖A‖ → ∃ n ≤ 0, NuonAux A 0 n
Tactic:
case zero =>
  intro _; exact ⟨0, by simp⟩
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 k : M
IH : k ≤ ‖A‖ → ∃ n ≤ k, NuonAux A k n
⊢ k + 1 ≤ ‖A‖ → ∃ n ≤ k + 1, NuonAux A (k + 1) n
Tactic:
case succ k IH =>
  intro hk
  rcases IH (le_trans (by simp) hk) with ⟨n, hn, Hn⟩
  exact ⟨n + fbit A k, add_le_add hn (by simp), Hn.succ (le_trans (by simp) hk)⟩
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 k : M
hk : k ≤ ‖A‖
this : ∃ n ≤ k, NuonAux A k n
⊢ ∃ n, NuonAux A k n
Tactic:
rcases this with ⟨n, _, h⟩
State after:
case intro.intro
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
left✝ : n ≤ k
h : NuonAux A k n
⊢ ∃ n, NuonAux A k n

State before:
case intro.intro
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
left✝ : n ≤ k
h : NuonAux A k n
⊢ ∃ n, NuonAux A k n
Tactic:
exact ⟨n, h⟩
State after:
no goals

State before:
case hP
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A : M
⊢ 𝚺₀-Predicate fun {k} => k ≤ ‖A‖ → ∃ n ≤ k, NuonAux A k n
Tactic:
definability
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
⊢ 0 ≤ ‖A‖ → ∃ n ≤ 0, NuonAux A 0 n
Tactic:
intro _
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A : M
hk✝ : 0 ≤ ‖A‖
⊢ ∃ n ≤ 0, NuonAux A 0 n

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
hk✝ : 0 ≤ ‖A‖
⊢ ∃ n ≤ 0, NuonAux A 0 n
Tactic:
exact ⟨0, by simp⟩
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
hk✝ : 0 ≤ ‖A‖
⊢ 0 ≤ 0 ∧ NuonAux A 0 0
Tactic:
simp
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 k : M
IH : k ≤ ‖A‖ → ∃ n ≤ k, NuonAux A k n
⊢ k + 1 ≤ ‖A‖ → ∃ n ≤ k + 1, NuonAux A (k + 1) n
Tactic:
intro hk
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A k : M
IH : k ≤ ‖A‖ → ∃ n ≤ k, NuonAux A k n
hk : k + 1 ≤ ‖A‖
⊢ ∃ n ≤ k + 1, NuonAux A (k + 1) n

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A k : M
IH : k ≤ ‖A‖ → ∃ n ≤ k, NuonAux A k n
hk : k + 1 ≤ ‖A‖
⊢ ∃ n ≤ k + 1, NuonAux A (k + 1) n
Tactic:
rcases IH (le_trans (by simp) hk) with ⟨n, hn, Hn⟩
State after:
case intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A k : M
IH : k ≤ ‖A‖ → ∃ n ≤ k, NuonAux A k n
hk : k + 1 ≤ ‖A‖
n : M
hn : n ≤ k
Hn : NuonAux A k n
⊢ ∃ n ≤ k + 1, NuonAux A (k + 1) n

State before:
case intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A k : M
IH : k ≤ ‖A‖ → ∃ n ≤ k, NuonAux A k n
hk : k + 1 ≤ ‖A‖
n : M
hn : n ≤ k
Hn : NuonAux A k n
⊢ ∃ n ≤ k + 1, NuonAux A (k + 1) n
Tactic:
exact ⟨n + fbit A k, add_le_add hn (by simp), Hn.succ (le_trans (by simp) hk)⟩
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 k : M
IH : k ≤ ‖A‖ → ∃ n ≤ k, NuonAux A k n
hk : k + 1 ≤ ‖A‖
⊢ k ≤ k + 1
Tactic:
simp
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 k : M
IH : k ≤ ‖A‖ → ∃ n ≤ k, NuonAux A k n
hk : k + 1 ≤ ‖A‖
n : M
hn : n ≤ k
Hn : NuonAux A k n
⊢ fbit A k ≤ 1
Tactic:
simp
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 k : M
IH : k ≤ ‖A‖ → ∃ n ≤ k, NuonAux A k n
hk : k + 1 ≤ ‖A‖
n : M
hn : n ≤ k
Hn : NuonAux A k n
⊢ k ≤ k + 1
Tactic:
simp
State after:
no goals