internlm/Lean-Github huggingface dataset:
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
⊢ k ≤ k + 1
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
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)
⊢ k ≤ k + 1
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
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'
⊢ A ≤ 2 * A
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.two_mul_add_one
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 + 1) (k + 1) (n + 1)
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 + 1) (k + 1) (n + 1)
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.two_mul_add_one
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 + 1) (k + 1) (n + 1)
Tactic:
suffices ∀ n ≤ k, k ≤ ‖A‖ → NuonAux A k n → NuonAux (2 * A + 1) (k + 1) (n + 1) 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 + 1) (k + 1) (n + 1)
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.two_mul_add_one
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 + 1) (k + 1) (n + 1)
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 + 1) (k + 1) (n + 1)

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 + 1) (0 + 1) (n + 1)

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 + 1) (x✝ + 1) (n + 1)
⊢ ∀ n ≤ x✝ + 1, x✝ + 1 ≤ ‖A‖ → NuonAux A (x✝ + 1) n → NuonAux (2 * A + 1) (x✝ + 1 + 1) (n + 1)
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.two_mul_add_one
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 + 1) (0 + 1) (n + 1)
Tactic:
case zero =>
  simpa using (NuonAux.initial (2 * A + 1)).succ (by simp)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.two_mul_add_one
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 + 1) (k + 1) (n + 1)
⊢ ∀ n ≤ k + 1, k + 1 ≤ ‖A‖ → NuonAux A (k + 1) n → NuonAux (2 * A + 1) (k + 1 + 1) (n + 1)
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 + 1) (k + 1) (n' + 1) := IH n' H'.le (le_trans (by simp) hk) H'
  simpa [add_right_comm n' 1] using IH.succ (le_trans hk (by simp [length_two_mul_add_one]))
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.two_mul_add_one
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 + 1) (k + 1) (n + 1)
⊢ ∀ {n : M}, k ≤ ‖A‖ → NuonAux A k n → NuonAux (2 * A + 1) (k + 1) (n + 1)
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 + 1) (k + 1) (n + 1)
n : M
hk : k ≤ ‖A‖
H : NuonAux A k n
⊢ NuonAux (2 * A + 1) (k + 1) (n + 1)
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.two_mul_add_one
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 + 1) (k + 1) (n + 1)
n : M
hk : k ≤ ‖A‖
H : NuonAux A k n
⊢ NuonAux (2 * A + 1) (k + 1) (n + 1)
Tactic:
exact this n H.le hk H
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.two_mul_add_one
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 + 1) (k + 1) (n + 1)
Tactic:
definability
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.two_mul_add_one
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 + 1) (0 + 1) (n + 1)
Tactic:
simpa using (NuonAux.initial (2 * A + 1)).succ (by simp)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.two_mul_add_one
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 + 1‖
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.two_mul_add_one
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 + 1) (k + 1) (n + 1)
⊢ ∀ n ≤ k + 1, k + 1 ≤ ‖A‖ → NuonAux A (k + 1) n → NuonAux (2 * A + 1) (k + 1 + 1) (n + 1)
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 + 1) (k + 1) (n + 1)
n : M
hn : n ≤ k + 1
hk : k + 1 ≤ ‖A‖
H : NuonAux A (k + 1) n
⊢ NuonAux (2 * A + 1) (k + 1 + 1) (n + 1)
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.two_mul_add_one
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 + 1) (k + 1) (n + 1)
n : M
hn : n ≤ k + 1
hk : k + 1 ≤ ‖A‖
H : NuonAux A (k + 1) n
⊢ NuonAux (2 * A + 1) (k + 1 + 1) (n + 1)
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 + 1) (k + 1) (n + 1)
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 + 1) (k + 1 + 1) (n' + fbit A k + 1)
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.two_mul_add_one
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 + 1) (k + 1) (n + 1)
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 + 1) (k + 1 + 1) (n' + fbit A k + 1)
Tactic:
have IH : NuonAux (2 * A + 1) (k + 1) (n' + 1) := 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 + 1) (k + 1) (n + 1)
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 + 1) (k + 1) (n' + 1)
⊢ NuonAux (2 * A + 1) (k + 1 + 1) (n' + fbit A k + 1)
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.two_mul_add_one
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 + 1) (k + 1) (n + 1)
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 + 1) (k + 1) (n' + 1)
⊢ NuonAux (2 * A + 1) (k + 1 + 1) (n' + fbit A k + 1)
Tactic:
simpa [add_right_comm n' 1] using IH.succ (le_trans hk (by simp [length_two_mul_add_one]))
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.two_mul_add_one
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 + 1) (k + 1) (n + 1)
n : M
hn : n ≤ k + 1
hk : k + 1 ≤ ‖A‖
H : NuonAux A (k + 1) n
⊢ k ≤ k + 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.two_mul_add_one
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 + 1) (k + 1) (n + 1)
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)
⊢ k ≤ k + 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.two_mul_add_one
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 + 1) (k + 1) (n + 1)
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 + 1) (k + 1) (n' + 1)
⊢ ‖A‖ ≤ ‖2 * A + 1‖
Tactic:
simp [length_two_mul_add_one]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.exists_unique
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, Nuon A n
Tactic:
rcases show ∃ n, Nuon A n from NuonAux.exists (by simp) with ⟨n, hn⟩
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A n : M
hn : Nuon A n
⊢ ∃! n, Nuon A n
Theorem: LO.FirstOrder.Arith.Model.Nuon.exists_unique
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A n : M
hn : Nuon A n
⊢ ∃! n, Nuon A n
Tactic:
exact ExistsUnique.intro n hn (fun n' hn' ↦ hn'.uniq hn)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.exists_unique
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
⊢ ‖A‖ ≤ ‖A‖
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.nuon_bit0
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
⊢ nuon (2 * a) = nuon a
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
⊢ nuon (2 * 0) = nuon 0

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
a : M
pos : 0 < a
⊢ nuon (2 * a) = nuon a
Theorem: LO.FirstOrder.Arith.Model.nuon_bit0
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
⊢ nuon (2 * 0) = nuon 0
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.nuon_bit0
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
a : M
pos : 0 < a
⊢ nuon (2 * a) = nuon a
Tactic:
have : Nuon (2 * a) (nuon a) := by simpa [Nuon, length_two_mul_of_pos pos] using (nuon_nuon a).two_mul (by simp)
Proof state after:
case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
a : M
pos : 0 < a
this : Nuon (2 * a) (nuon a)
⊢ nuon (2 * a) = nuon a
Theorem: LO.FirstOrder.Arith.Model.nuon_bit0
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
a : M
pos : 0 < a
this : Nuon (2 * a) (nuon a)
⊢ nuon (2 * a) = nuon a
Tactic:
exact this.nuon_eq
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.nuon_bit0
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
pos : 0 < a
⊢ Nuon (2 * a) (nuon a)
Tactic:
simpa [Nuon, length_two_mul_of_pos pos] using (nuon_nuon a).two_mul (by simp)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.nuon_bit0
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
pos : 0 < a
⊢ ‖a‖ ≤ ‖a‖
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.nuon_bit1
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
⊢ nuon (2 * a + 1) = nuon a + 1
Tactic:
have : Nuon (2 * a + 1) (nuon a + 1) := by simpa [Nuon, length_two_mul_add_one] using (nuon_nuon a).two_mul_add_one (by 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
this : Nuon (2 * a + 1) (nuon a + 1)
⊢ nuon (2 * a + 1) = nuon a + 1
Theorem: LO.FirstOrder.Arith.Model.nuon_bit1
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
this : Nuon (2 * a + 1) (nuon a + 1)
⊢ nuon (2 * a + 1) = nuon a + 1
Tactic:
exact this.nuon_eq
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.nuon_bit1
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
⊢ Nuon (2 * a + 1) (nuon a + 1)
Tactic:
simpa [Nuon, length_two_mul_add_one] using (nuon_nuon a).two_mul_add_one (by simp)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.nuon_bit1
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
⊢ ‖a‖ ≤ ‖a‖
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.nuon_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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
⊢ 𝚺₀-Function₁ nuon via nuonDef
Tactic:
intro v
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
v : Fin (Nat.succ 1) → M
⊢ (fun v => v 0 = (fun v => nuon (v 0)) fun x => v x.succ) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val nuonDef)
Theorem: LO.FirstOrder.Arith.Model.nuon_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 (Nat.succ 1) → M
⊢ (fun v => v 0 = (fun v => nuon (v 0)) fun x => v x.succ) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val nuonDef)
Tactic:
simp [Nuon.nuon_eq_iff, Nuon, nuonDef,
length_defined.df.iff, Nuon.nuonAux_defined.df.iff, lt_succ_iff_le]
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
v : Fin (Nat.succ 1) → M
⊢ Nuon.NuonAux (v 1) ‖v 1‖ (v 0) ↔ ∃ x ≤ v 1, x = ‖v 1‖ ∧ Nuon.NuonAux (v 1) x (v 0)
Theorem: LO.FirstOrder.Arith.Model.nuon_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 (Nat.succ 1) → M
⊢ Nuon.NuonAux (v 1) ‖v 1‖ (v 0) ↔ ∃ x ≤ v 1, x = ‖v 1‖ ∧ Nuon.NuonAux (v 1) x (v 0)
Tactic:
rw [Nuon.bex_eq_le_iff]
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
v : Fin (Nat.succ 1) → M
⊢ Nuon.NuonAux (v 1) ‖v 1‖ (v 0) ↔ ‖v 1‖ ≤ v 1 ∧ Nuon.NuonAux (v 1) ‖v 1‖ (v 0)
Theorem: LO.FirstOrder.Arith.Model.nuon_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 (Nat.succ 1) → M
⊢ Nuon.NuonAux (v 1) ‖v 1‖ (v 0) ↔ ‖v 1‖ ≤ v 1 ∧ Nuon.NuonAux (v 1) ‖v 1‖ (v 0)
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.ext_graph
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 b c : M
⊢ a = ext b c ↔ ∃ x ≤ c, x = c / b ∧ a = x % b
Tactic:
simp [ext]
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 b c : M
⊢ a = c / b % b ↔ ∃ x ≤ c, x = c / b ∧ a = x % b
Theorem: LO.FirstOrder.Arith.Model.ext_graph
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 b c : M
⊢ a = c / b % b ↔ ∃ x ≤ c, x = c / b ∧ a = x % b
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 ⊧ₘ* 𝐈𝚫₀
a b c : M
⊢ a = c / b % b → ∃ x ≤ c, x = c / b ∧ a = x % b

case mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a b c : M
⊢ (∃ x ≤ c, x = c / b ∧ a = x % b) → a = c / b % b
Theorem: LO.FirstOrder.Arith.Model.ext_graph
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 ⊧ₘ* 𝐈𝚫₀
a b c : M
⊢ a = c / b % b → ∃ x ≤ c, x = c / b ∧ a = x % b
Tactic:
rintro rfl
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 ⊧ₘ* 𝐈𝚫₀
b c : M
⊢ ∃ x ≤ c, x = c / b ∧ c / b % b = x % b
Theorem: LO.FirstOrder.Arith.Model.ext_graph
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 ⊧ₘ* 𝐈𝚫₀
b c : M
⊢ ∃ x ≤ c, x = c / b ∧ c / b % b = x % b
Tactic:
exact ⟨c / b, by simp, rfl, by rfl⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.ext_graph
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
b c : M
⊢ c / b ≤ c
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.ext_graph
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
b c : M
⊢ c / b % b = c / b % b
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.ext_graph
Proof state before:
case mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a b c : M
⊢ (∃ x ≤ c, x = c / b ∧ a = x % b) → a = c / b % b
Tactic:
rintro ⟨_, _, rfl, rfl⟩
Proof state after:
case mpr.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
b c : M
left✝ : c / b ≤ c
⊢ c / b % b = c / b % b
Theorem: LO.FirstOrder.Arith.Model.ext_graph
Proof state before:
case mpr.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
b c : M
left✝ : c / b ≤ c
⊢ c / b % b = c / b % b
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.ext_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 ⊧ₘ* 𝐈𝚫₀
⊢ 𝚺₀-Function₂ fun a b => ext a b via extDef
Tactic:
intro v
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
v : Fin (Nat.succ 2) → M
⊢ (fun v => v 0 = (fun v => (fun a b => ext a b) (v 0) (v 1)) fun x => v x.succ) v ↔
    (Semiformula.Evalbm M v) (HSemiformula.val extDef)
Theorem: LO.FirstOrder.Arith.Model.ext_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 (Nat.succ 2) → M
⊢ (fun v => v 0 = (fun v => (fun a b => ext a b) (v 0) (v 1)) fun x => v x.succ) v ↔
    (Semiformula.Evalbm M v) (HSemiformula.val extDef)
Tactic:
simp [Matrix.vecHead, Matrix.vecTail, extDef,
ext_graph, Semiformula.eval_substs, div_defined.df.iff, rem_defined.df.iff, le_iff_lt_succ]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.ext_le_add
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
u z : M
⊢ z / u ≤ z
Tactic:
simp [add_comm]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.ext_lt
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
u z : M
pos : 0 < u
⊢ ext u z < u
Tactic:
simp [ext, pos]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.ext_add_of_dvd_sq_right
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
u z₁ z₂ : M
pos : 0 < u
h : u ^ 2 ∣ z₂
⊢ ext u (z₁ + z₂) = ext u z₁
Tactic:
simp [ext]
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
u z₁ z₂ : M
pos : 0 < u
h : u ^ 2 ∣ z₂
⊢ (z₁ + z₂) / u % u = z₁ / u % u
Theorem: LO.FirstOrder.Arith.Model.ext_add_of_dvd_sq_right
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
u z₁ z₂ : M
pos : 0 < u
h : u ^ 2 ∣ z₂
⊢ (z₁ + z₂) / u % u = z₁ / u % u
Tactic:
have : ∃ z', z₂ = z' * u * u := by rcases h with ⟨u', rfl⟩; exact ⟨u', by simp [mul_comm _ u', mul_assoc]; simp [sq]⟩
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
u z₁ z₂ : M
pos : 0 < u
h : u ^ 2 ∣ z₂
this : ∃ z', z₂ = z' * u * u
⊢ (z₁ + z₂) / u % u = z₁ / u % u
Theorem: LO.FirstOrder.Arith.Model.ext_add_of_dvd_sq_right
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
u z₁ z₂ : M
pos : 0 < u
h : u ^ 2 ∣ z₂
this : ∃ z', z₂ = z' * u * u
⊢ (z₁ + z₂) / u % u = z₁ / u % u
Tactic:
rcases this with ⟨z₂, rfl⟩
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 ⊧ₘ* 𝐈𝚫₀
u z₁ : M
pos : 0 < u
z₂ : M
h : u ^ 2 ∣ z₂ * u * u
⊢ (z₁ + z₂ * u * u) / u % u = z₁ / u % u
Theorem: LO.FirstOrder.Arith.Model.ext_add_of_dvd_sq_right
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 ⊧ₘ* 𝐈𝚫₀
u z₁ : M
pos : 0 < u
z₂ : M
h : u ^ 2 ∣ z₂ * u * u
⊢ (z₁ + z₂ * u * u) / u % u = z₁ / u % u
Tactic:
simp [div_add_mul_self, pos]
Proof state after:
no goals