internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.Nuon.nuonAux_defined
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
v : Fin 3 → M
⊢ SeriesSegment ((2 * v 0 + 1) ^ 128) (bexp (2 * v 0) (√‖v 0‖)) (‖bexp (2 * v 0) (√‖v 0‖)‖ ^ 2) (v 0) (v 1) (v 2) ↔
    ‖v 0‖ ≤ v 0 ∧
      √‖v 0‖ ≤ ‖v 0‖ ∧
        bexp (2 * v 0) (√‖v 0‖) ≤ 2 * v 0 ∧
          ‖bexp (2 * v 0) (√‖v 0‖)‖ ≤ bexp (2 * v 0) (√‖v 0‖) ∧
            SeriesSegment ((2 * v 0 + 1) ^ 128) (bexp (2 * v 0) (√‖v 0‖)) (‖bexp (2 * v 0) (√‖v 0‖)‖ ^ 2) (v 0) (v 1)
              (v 2)
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.initial
Proof 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 < polyU A
Tactic:
simp [polyU]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.initial_iff
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A n : M
⊢ n = 0 → NuonAux A 0 n
Tactic:
rintro rfl
Proof 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
⊢ NuonAux A 0 0
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.initial_iff
Proof 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
⊢ NuonAux A 0 0
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.zero
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
k : M
⊢ 0 < polyU 0
Tactic:
simp [polyU]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.succ
Proof 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
H : NuonAux A k n
hk : k ≤ ‖A‖
⊢ NuonAux A (k + 1) (n + fbit A k)
Tactic:
rcases zero_le A with (rfl | pos)
Proof state after:
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
n k : M
H : NuonAux 0 k n
hk : k ≤ ‖0‖
⊢ NuonAux 0 (k + 1) (n + fbit 0 k)

case inr
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
H : NuonAux A k n
hk : k ≤ ‖A‖
pos : 0 < A
⊢ NuonAux A (k + 1) (n + fbit A k)
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.succ
Proof state before:
case inr
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
H : NuonAux A k n
hk : k ≤ ‖A‖
pos : 0 < A
⊢ NuonAux A (k + 1) (n + fbit A k)
Tactic:
exact SeriesSegment.succ (sq_polyI_hash_polyL_polybounded pos) (by simp [polyL]) (lt_of_le_of_lt hk $ polyI_le pos) H
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.succ
Proof state before:
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
n k : M
H : NuonAux 0 k n
hk : k ≤ ‖0‖
⊢ NuonAux 0 (k + 1) (n + fbit 0 k)
Tactic:
rcases show n = 0 from H.uniq (NuonAux.zero k)
Proof state after:
case inl.refl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
k : M
hk : k ≤ ‖0‖
H : NuonAux 0 k 0
⊢ NuonAux 0 (k + 1) (0 + fbit 0 k)
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.succ
Proof state before:
case inl.refl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
k : M
hk : k ≤ ‖0‖
H : NuonAux 0 k 0
⊢ NuonAux 0 (k + 1) (0 + fbit 0 k)
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.succ
Proof 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
H : NuonAux A k n
hk : k ≤ ‖A‖
pos : 0 < A
⊢ ‖‖polyI A‖ ^ 2‖ ≤ ‖polyL A‖
Tactic:
simp [polyL]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.exists
Proof 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⟩
Proof 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
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.exists
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.exists
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.exists
Proof 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⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.exists
Proof 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)⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.exists
Proof 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⟩
Proof 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
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.exists
Proof 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⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.exists
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.exists
Proof 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 _
Proof 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
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.exists
Proof 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⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.exists
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.exists
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.exists
Proof 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⟩
Proof 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
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.exists
Proof 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)⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.exists
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.exists
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.exists
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.succ_elim
Proof 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'⟩
Proof 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'
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.succ_elim
Proof 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)
Proof 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
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.succ_elim
Proof 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'⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.succ_iff
Proof 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
Proof 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)
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.succ_iff
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.succ_iff
Proof 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'⟩
Proof 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
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.succ_iff
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.succ_iff
Proof 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'
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.succ_iff
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.two_mul
Proof 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 n : M
hk : k ≤ ‖A‖
⊢ NuonAux A k n → NuonAux (2 * A) (k + 1) n
Tactic:
revert n hk
Proof 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
⊢ ∀ {n : M}, k ≤ ‖A‖ → NuonAux A k n → NuonAux (2 * A) (k + 1) n
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.two_mul
Proof 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
⊢ ∀ {n : M}, k ≤ ‖A‖ → NuonAux A k n → NuonAux (2 * A) (k + 1) n
Tactic:
suffices ∀ n ≤ k, k ≤ ‖A‖ → NuonAux A k n → NuonAux (2 * A) (k + 1) n by
  intro n hk H
  exact this n H.le hk H
Proof 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
⊢ ∀ n ≤ k, k ≤ ‖A‖ → NuonAux A k n → NuonAux (2 * A) (k + 1) n
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.two_mul
Proof 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
⊢ ∀ n ≤ k, k ≤ ‖A‖ → NuonAux A k n → NuonAux (2 * A) (k + 1) n
Tactic:
induction k using induction_iSigmaZero
Proof 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} => ∀ n ≤ k, k ≤ ‖A‖ → NuonAux A k n → NuonAux (2 * A) (k + 1) 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
⊢ ∀ n ≤ 0, 0 ≤ ‖A‖ → NuonAux A 0 n → NuonAux (2 * A) (0 + 1) 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✝ : ∀ n ≤ x✝, x✝ ≤ ‖A‖ → NuonAux A x✝ n → NuonAux (2 * A) (x✝ + 1) n
⊢ ∀ n ≤ x✝ + 1, x✝ + 1 ≤ ‖A‖ → NuonAux A (x✝ + 1) n → NuonAux (2 * A) (x✝ + 1 + 1) n
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.two_mul
Proof 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 ≤ 0, 0 ≤ ‖A‖ → NuonAux A 0 n → NuonAux (2 * A) (0 + 1) n
Tactic:
case zero =>
  simp; simpa using (NuonAux.initial (2 * A)).succ (by simp)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.two_mul
Proof 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 : ∀ n ≤ k, k ≤ ‖A‖ → NuonAux A k n → NuonAux (2 * A) (k + 1) n
⊢ ∀ n ≤ k + 1, k + 1 ≤ ‖A‖ → NuonAux A (k + 1) n → NuonAux (2 * A) (k + 1 + 1) n
Tactic:
case succ k IH =>
  intro n hn hk H
  rcases H.succ_elim (le_trans (by simp) hk) with ⟨n', rfl, H'⟩
  have IH : NuonAux (2 * A) (k + 1) n' := IH n' H'.le (le_trans (by simp) hk) H'
  simpa using IH.succ (le_trans hk (length_monotone $ by simp))
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.two_mul
Proof 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
this : ∀ n ≤ k, k ≤ ‖A‖ → NuonAux A k n → NuonAux (2 * A) (k + 1) n
⊢ ∀ {n : M}, k ≤ ‖A‖ → NuonAux A k n → NuonAux (2 * A) (k + 1) n
Tactic:
intro n hk H
Proof 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
this : ∀ n ≤ k, k ≤ ‖A‖ → NuonAux A k n → NuonAux (2 * A) (k + 1) n
n : M
hk : k ≤ ‖A‖
H : NuonAux A k n
⊢ NuonAux (2 * A) (k + 1) n
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.two_mul
Proof 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
this : ∀ n ≤ k, k ≤ ‖A‖ → NuonAux A k n → NuonAux (2 * A) (k + 1) n
n : M
hk : k ≤ ‖A‖
H : NuonAux A k n
⊢ NuonAux (2 * A) (k + 1) n
Tactic:
exact this n H.le hk H
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.two_mul
Proof 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} => ∀ n ≤ k, k ≤ ‖A‖ → NuonAux A k n → NuonAux (2 * A) (k + 1) n
Tactic:
definability
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.two_mul
Proof 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 ≤ 0, 0 ≤ ‖A‖ → NuonAux A 0 n → NuonAux (2 * A) (0 + 1) n
Tactic:
simp
Proof 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
⊢ NuonAux (2 * A) 1 0
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.two_mul
Proof 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
⊢ NuonAux (2 * A) 1 0
Tactic:
simpa using (NuonAux.initial (2 * A)).succ (by simp)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.two_mul
Proof 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 ≤ ‖2 * A‖
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.two_mul
Proof 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 : ∀ n ≤ k, k ≤ ‖A‖ → NuonAux A k n → NuonAux (2 * A) (k + 1) n
⊢ ∀ n ≤ k + 1, k + 1 ≤ ‖A‖ → NuonAux A (k + 1) n → NuonAux (2 * A) (k + 1 + 1) n
Tactic:
intro n hn hk H
Proof 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 : ∀ n ≤ k, k ≤ ‖A‖ → NuonAux A k n → NuonAux (2 * A) (k + 1) n
n : M
hn : n ≤ k + 1
hk : k + 1 ≤ ‖A‖
H : NuonAux A (k + 1) n
⊢ NuonAux (2 * A) (k + 1 + 1) n
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.two_mul
Proof 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 : ∀ n ≤ k, k ≤ ‖A‖ → NuonAux A k n → NuonAux (2 * A) (k + 1) n
n : M
hn : n ≤ k + 1
hk : k + 1 ≤ ‖A‖
H : NuonAux A (k + 1) n
⊢ NuonAux (2 * A) (k + 1 + 1) n
Tactic:
rcases H.succ_elim (le_trans (by simp) hk) with ⟨n', rfl, H'⟩
Proof 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 : ∀ n ≤ k, k ≤ ‖A‖ → NuonAux A k n → NuonAux (2 * A) (k + 1) n
hk : k + 1 ≤ ‖A‖
n' : M
H' : NuonAux A k n'
hn : n' + fbit A k ≤ k + 1
H : NuonAux A (k + 1) (n' + fbit A k)
⊢ NuonAux (2 * A) (k + 1 + 1) (n' + fbit A k)
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.two_mul
Proof 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 : ∀ n ≤ k, k ≤ ‖A‖ → NuonAux A k n → NuonAux (2 * A) (k + 1) n
hk : k + 1 ≤ ‖A‖
n' : M
H' : NuonAux A k n'
hn : n' + fbit A k ≤ k + 1
H : NuonAux A (k + 1) (n' + fbit A k)
⊢ NuonAux (2 * A) (k + 1 + 1) (n' + fbit A k)
Tactic:
have IH : NuonAux (2 * A) (k + 1) n' := IH n' H'.le (le_trans (by simp) hk) H'
Proof 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✝ : ∀ n ≤ k, k ≤ ‖A‖ → NuonAux A k n → NuonAux (2 * A) (k + 1) n
hk : k + 1 ≤ ‖A‖
n' : M
H' : NuonAux A k n'
hn : n' + fbit A k ≤ k + 1
H : NuonAux A (k + 1) (n' + fbit A k)
IH : NuonAux (2 * A) (k + 1) n'
⊢ NuonAux (2 * A) (k + 1 + 1) (n' + fbit A k)
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.two_mul
Proof 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✝ : ∀ n ≤ k, k ≤ ‖A‖ → NuonAux A k n → NuonAux (2 * A) (k + 1) n
hk : k + 1 ≤ ‖A‖
n' : M
H' : NuonAux A k n'
hn : n' + fbit A k ≤ k + 1
H : NuonAux A (k + 1) (n' + fbit A k)
IH : NuonAux (2 * A) (k + 1) n'
⊢ NuonAux (2 * A) (k + 1 + 1) (n' + fbit A k)
Tactic:
simpa using IH.succ (le_trans hk (length_monotone $ by simp))
Proof state after:
no goals