internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.Nuon.llen_lt_len_hash_len
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
⊢ ‖‖K‖‖ < ‖K # ‖K‖‖
Tactic:
simp [length_hash, 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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
K : M
⊢ ‖‖K‖‖ ≤ ‖K‖ * ‖‖K‖‖
Theorem: LO.FirstOrder.Arith.Model.Nuon.llen_lt_len_hash_len
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
⊢ ‖‖K‖‖ ≤ ‖K‖ * ‖‖K‖‖
Tactic:
rcases zero_le ‖K‖ with (hK | 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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
K : M
hK : 0 = ‖K‖
⊢ ‖‖K‖‖ ≤ ‖K‖ * ‖‖K‖‖

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
K : M
pos : 0 < ‖K‖
⊢ ‖‖K‖‖ ≤ ‖K‖ * ‖‖K‖‖
Theorem: LO.FirstOrder.Arith.Model.Nuon.llen_lt_len_hash_len
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
K : M
hK : 0 = ‖K‖
⊢ ‖‖K‖‖ ≤ ‖K‖ * ‖‖K‖‖
Tactic:
simp [←hK]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.llen_lt_len_hash_len
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
K : M
pos : 0 < ‖K‖
⊢ ‖‖K‖‖ ≤ ‖K‖ * ‖‖K‖‖
Tactic:
exact le_mul_of_pos_left pos
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.mul_len_lt_len_hash
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
i I L : M
hi : i ≤ ‖I‖
⊢ i * ‖L‖ < ‖I # L‖
Tactic:
simp [length_hash, 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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
i I L : M
hi : i ≤ ‖I‖
⊢ i * ‖L‖ ≤ ‖I‖ * ‖L‖
Theorem: LO.FirstOrder.Arith.Model.Nuon.mul_len_lt_len_hash
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
i I L : M
hi : i ≤ ‖I‖
⊢ i * ‖L‖ ≤ ‖I‖ * ‖L‖
Tactic:
exact mul_le_mul_right' hi ‖L‖
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.mul_len_lt_len_hash'
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
i K z : M
hi : i ≤ ‖z‖
⊢ i * ‖‖K‖‖ < ‖z # ‖K‖‖
Tactic:
simp [length_hash, 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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
i K z : M
hi : i ≤ ‖z‖
⊢ i * ‖‖K‖‖ ≤ ‖z‖ * ‖‖K‖‖
Theorem: LO.FirstOrder.Arith.Model.Nuon.mul_len_lt_len_hash'
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
i K z : M
hi : i ≤ ‖z‖
⊢ i * ‖‖K‖‖ ≤ ‖z‖ * ‖‖K‖‖
Tactic:
exact mul_le_mul_right' hi ‖‖K‖‖
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_eq_zero_of_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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S i : M
h : ‖S‖ ≤ i * ‖L‖
⊢ S{L}[i] = 0
Tactic:
simp [ext, bexp_eq_zero_of_le h]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_le_self
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S i : M
⊢ S / bexp S (i * ‖L‖) ≤ S
Tactic:
simp [ext]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_graph_aux
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z S L i : M
⊢ z = S{L}[i] ↔ (‖S‖ ≤ i * ‖L‖ → z = 0) ∧ (i * ‖L‖ < ‖S‖ → ∃ b ≤ S, Exponential (i * ‖L‖) b ∧ z = S / b % L # 1)
Tactic:
rcases show ‖S‖ ≤ i * ‖L‖ ∨ i * ‖L‖ < ‖S‖ from le_or_lt _ _ with (le | lt)
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z S L i : M
le : ‖S‖ ≤ i * ‖L‖
⊢ z = S{L}[i] ↔ (‖S‖ ≤ i * ‖L‖ → z = 0) ∧ (i * ‖L‖ < ‖S‖ → ∃ b ≤ S, Exponential (i * ‖L‖) b ∧ z = S / b % L # 1)

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z S L i : M
lt : i * ‖L‖ < ‖S‖
⊢ z = S{L}[i] ↔ (‖S‖ ≤ i * ‖L‖ → z = 0) ∧ (i * ‖L‖ < ‖S‖ → ∃ b ≤ S, Exponential (i * ‖L‖) b ∧ z = S / b % L # 1)
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_graph_aux
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z S L i : M
le : ‖S‖ ≤ i * ‖L‖
⊢ z = S{L}[i] ↔ (‖S‖ ≤ i * ‖L‖ → z = 0) ∧ (i * ‖L‖ < ‖S‖ → ∃ b ≤ S, Exponential (i * ‖L‖) b ∧ z = S / b % L # 1)
Tactic:
simp [ext_eq_zero_of_lt le, le, not_lt.mpr le]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_graph_aux
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z S L i : M
lt : i * ‖L‖ < ‖S‖
⊢ z = S{L}[i] ↔ (‖S‖ ≤ i * ‖L‖ → z = 0) ∧ (i * ‖L‖ < ‖S‖ → ∃ b ≤ S, Exponential (i * ‖L‖) b ∧ z = S / b % L # 1)
Tactic:
simp [lt, not_le.mpr lt, ext]
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z S L i : M
lt : i * ‖L‖ < ‖S‖
⊢ z = S / bexp S (i * ‖L‖) % L # 1 ↔ ∃ b ≤ S, Exponential (i * ‖L‖) b ∧ z = S / b % L # 1
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_graph_aux
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z S L i : M
lt : i * ‖L‖ < ‖S‖
⊢ z = S / bexp S (i * ‖L‖) % L # 1 ↔ ∃ b ≤ S, Exponential (i * ‖L‖) b ∧ z = S / b % L # 1
Tactic:
have := exp_bexp_of_lt lt
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z S L i : M
lt : i * ‖L‖ < ‖S‖
this : Exponential (i * ‖L‖) (bexp S (i * ‖L‖))
⊢ z = S / bexp S (i * ‖L‖) % L # 1 ↔ ∃ b ≤ S, Exponential (i * ‖L‖) b ∧ z = S / b % L # 1
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_graph_aux
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z S L i : M
lt : i * ‖L‖ < ‖S‖
this : Exponential (i * ‖L‖) (bexp S (i * ‖L‖))
⊢ z = S / bexp S (i * ‖L‖) % L # 1 ↔ ∃ b ≤ S, Exponential (i * ‖L‖) b ∧ z = S / b % L # 1
Tactic:
constructor
Proof state after:
case inr.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z S L i : M
lt : i * ‖L‖ < ‖S‖
this : Exponential (i * ‖L‖) (bexp S (i * ‖L‖))
⊢ z = S / bexp S (i * ‖L‖) % L # 1 → ∃ b ≤ S, Exponential (i * ‖L‖) b ∧ z = S / b % L # 1

case inr.mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z S L i : M
lt : i * ‖L‖ < ‖S‖
this : Exponential (i * ‖L‖) (bexp S (i * ‖L‖))
⊢ (∃ b ≤ S, Exponential (i * ‖L‖) b ∧ z = S / b % L # 1) → z = S / bexp S (i * ‖L‖) % L # 1
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_graph_aux
Proof state before:
case inr.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z S L i : M
lt : i * ‖L‖ < ‖S‖
this : Exponential (i * ‖L‖) (bexp S (i * ‖L‖))
⊢ z = S / bexp S (i * ‖L‖) % L # 1 → ∃ b ≤ S, Exponential (i * ‖L‖) b ∧ z = S / b % L # 1
Tactic:
rintro rfl
Proof state after:
case inr.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
S L i : M
lt : i * ‖L‖ < ‖S‖
this : Exponential (i * ‖L‖) (bexp S (i * ‖L‖))
⊢ ∃ b ≤ S, Exponential (i * ‖L‖) b ∧ S / bexp S (i * ‖L‖) % L # 1 = S / b % L # 1
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_graph_aux
Proof state before:
case inr.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
S L i : M
lt : i * ‖L‖ < ‖S‖
this : Exponential (i * ‖L‖) (bexp S (i * ‖L‖))
⊢ ∃ b ≤ S, Exponential (i * ‖L‖) b ∧ S / bexp S (i * ‖L‖) % L # 1 = S / b % L # 1
Tactic:
exact ⟨bexp S (i * ‖L‖), by simp, exp_bexp_of_lt lt, rfl⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_graph_aux
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
S L i : M
lt : i * ‖L‖ < ‖S‖
this : Exponential (i * ‖L‖) (bexp S (i * ‖L‖))
⊢ bexp S (i * ‖L‖) ≤ S
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_graph_aux
Proof state before:
case inr.mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z S L i : M
lt : i * ‖L‖ < ‖S‖
this : Exponential (i * ‖L‖) (bexp S (i * ‖L‖))
⊢ (∃ b ≤ S, Exponential (i * ‖L‖) b ∧ z = S / b % L # 1) → z = S / bexp S (i * ‖L‖) % L # 1
Tactic:
rintro ⟨b, _, H, rfl⟩
Proof state after:
case inr.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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
S L i : M
lt : i * ‖L‖ < ‖S‖
this : Exponential (i * ‖L‖) (bexp S (i * ‖L‖))
b : M
left✝ : b ≤ S
H : Exponential (i * ‖L‖) b
⊢ S / b % L # 1 = S / bexp S (i * ‖L‖) % L # 1
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_graph_aux
Proof state before:
case inr.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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
S L i : M
lt : i * ‖L‖ < ‖S‖
this : Exponential (i * ‖L‖) (bexp S (i * ‖L‖))
b : M
left✝ : b ≤ S
H : Exponential (i * ‖L‖) b
⊢ S / b % L # 1 = S / bexp S (i * ‖L‖) % L # 1
Tactic:
rcases H.uniq (exp_bexp_of_lt lt)
Proof state after:
case inr.mpr.intro.intro.intro.refl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
S L i : M
lt : i * ‖L‖ < ‖S‖
this : Exponential (i * ‖L‖) (bexp S (i * ‖L‖))
left✝ : bexp S (i * ‖L‖) ≤ S
H : Exponential (i * ‖L‖) (bexp S (i * ‖L‖))
⊢ S / bexp S (i * ‖L‖) % L # 1 = S / bexp S (i * ‖L‖) % L # 1
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_graph_aux
Proof state before:
case inr.mpr.intro.intro.intro.refl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
S L i : M
lt : i * ‖L‖ < ‖S‖
this : Exponential (i * ‖L‖) (bexp S (i * ‖L‖))
left✝ : bexp S (i * ‖L‖) ≤ S
H : Exponential (i * ‖L‖) (bexp S (i * ‖L‖))
⊢ S / bexp S (i * ‖L‖) % L # 1 = S / bexp S (i * ‖L‖) % L # 1
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z S L i : M
⊢ z = S{L}[i] ↔
    ∃ lS ≤ S,
      lS = ‖S‖ ∧
        ∃ lL ≤ L,
          lL = ‖L‖ ∧
            (lS ≤ i * lL → z = 0) ∧
              (i * lL < lS →
                ∃ b ≤ S,
                  Exponential (i * lL) b ∧
                    ∃ hL ≤ 2 * L + 1, Exponential lL hL ∧ ∃ divS ≤ S, divS = S / b ∧ z = divS % hL)
Tactic:
rw [ext_graph_aux]
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z S L i : M
⊢ (‖S‖ ≤ i * ‖L‖ → z = 0) ∧ (i * ‖L‖ < ‖S‖ → ∃ b ≤ S, Exponential (i * ‖L‖) b ∧ z = S / b % L # 1) ↔
    ∃ lS ≤ S,
      lS = ‖S‖ ∧
        ∃ lL ≤ L,
          lL = ‖L‖ ∧
            (lS ≤ i * lL → z = 0) ∧
              (i * lL < lS →
                ∃ b ≤ S,
                  Exponential (i * lL) b ∧
                    ∃ hL ≤ 2 * L + 1, Exponential lL hL ∧ ∃ divS ≤ S, divS = S / b ∧ z = divS % hL)
Theorem: LO.FirstOrder.Arith.Model.Nuon.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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z S L i : M
⊢ (‖S‖ ≤ i * ‖L‖ → z = 0) ∧ (i * ‖L‖ < ‖S‖ → ∃ b ≤ S, Exponential (i * ‖L‖) b ∧ z = S / b % L # 1) ↔
    ∃ lS ≤ S,
      lS = ‖S‖ ∧
        ∃ lL ≤ L,
          lL = ‖L‖ ∧
            (lS ≤ i * lL → z = 0) ∧
              (i * lL < lS →
                ∃ b ≤ S,
                  Exponential (i * lL) b ∧
                    ∃ hL ≤ 2 * L + 1, Exponential lL hL ∧ ∃ divS ≤ S, divS = S / b ∧ z = divS % hL)
Tactic:
rcases show ‖S‖ ≤ i * ‖L‖ ∨ i * ‖L‖ < ‖S‖ from le_or_lt _ _ with (le | lt)
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z S L i : M
le : ‖S‖ ≤ i * ‖L‖
⊢ (‖S‖ ≤ i * ‖L‖ → z = 0) ∧ (i * ‖L‖ < ‖S‖ → ∃ b ≤ S, Exponential (i * ‖L‖) b ∧ z = S / b % L # 1) ↔
    ∃ lS ≤ S,
      lS = ‖S‖ ∧
        ∃ lL ≤ L,
          lL = ‖L‖ ∧
            (lS ≤ i * lL → z = 0) ∧
              (i * lL < lS →
                ∃ b ≤ S,
                  Exponential (i * lL) b ∧
                    ∃ hL ≤ 2 * L + 1, Exponential lL hL ∧ ∃ divS ≤ S, divS = S / b ∧ z = divS % hL)

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z S L i : M
lt : i * ‖L‖ < ‖S‖
⊢ (‖S‖ ≤ i * ‖L‖ → z = 0) ∧ (i * ‖L‖ < ‖S‖ → ∃ b ≤ S, Exponential (i * ‖L‖) b ∧ z = S / b % L # 1) ↔
    ∃ lS ≤ S,
      lS = ‖S‖ ∧
        ∃ lL ≤ L,
          lL = ‖L‖ ∧
            (lS ≤ i * lL → z = 0) ∧
              (i * lL < lS →
                ∃ b ≤ S,
                  Exponential (i * lL) b ∧
                    ∃ hL ≤ 2 * L + 1, Exponential lL hL ∧ ∃ divS ≤ S, divS = S / b ∧ z = divS % hL)
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_graph
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z S L i : M
le : ‖S‖ ≤ i * ‖L‖
⊢ (‖S‖ ≤ i * ‖L‖ → z = 0) ∧ (i * ‖L‖ < ‖S‖ → ∃ b ≤ S, Exponential (i * ‖L‖) b ∧ z = S / b % L # 1) ↔
    ∃ lS ≤ S,
      lS = ‖S‖ ∧
        ∃ lL ≤ L,
          lL = ‖L‖ ∧
            (lS ≤ i * lL → z = 0) ∧
              (i * lL < lS →
                ∃ b ≤ S,
                  Exponential (i * lL) b ∧
                    ∃ hL ≤ 2 * L + 1, Exponential lL hL ∧ ∃ divS ≤ S, divS = S / b ∧ z = divS % hL)
Tactic:
simp [ext_eq_zero_of_lt le, le, not_lt.mpr le]
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z S L i : M
le : ‖S‖ ≤ i * ‖L‖
⊢ z = 0 ↔
    ∃ lS ≤ S,
      lS = ‖S‖ ∧
        ∃ lL ≤ L,
          lL = ‖L‖ ∧
            (lS ≤ i * lL → z = 0) ∧
              (i * lL < lS →
                ∃ b ≤ S,
                  Exponential (i * lL) b ∧
                    ∃ hL ≤ 2 * L + 1, Exponential lL hL ∧ ∃ divS ≤ S, divS = S / b ∧ z = divS % hL)
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_graph
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z S L i : M
le : ‖S‖ ≤ i * ‖L‖
⊢ z = 0 ↔
    ∃ lS ≤ S,
      lS = ‖S‖ ∧
        ∃ lL ≤ L,
          lL = ‖L‖ ∧
            (lS ≤ i * lL → z = 0) ∧
              (i * lL < lS →
                ∃ b ≤ S,
                  Exponential (i * lL) b ∧
                    ∃ hL ≤ 2 * L + 1, Exponential lL hL ∧ ∃ divS ≤ S, divS = S / b ∧ z = divS % hL)
Tactic:
constructor
Proof state after:
case inl.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z S L i : M
le : ‖S‖ ≤ i * ‖L‖
⊢ z = 0 →
    ∃ lS ≤ S,
      lS = ‖S‖ ∧
        ∃ lL ≤ L,
          lL = ‖L‖ ∧
            (lS ≤ i * lL → z = 0) ∧
              (i * lL < lS →
                ∃ b ≤ S,
                  Exponential (i * lL) b ∧
                    ∃ hL ≤ 2 * L + 1, Exponential lL hL ∧ ∃ divS ≤ S, divS = S / b ∧ z = divS % hL)

case inl.mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z S L i : M
le : ‖S‖ ≤ i * ‖L‖
⊢ (∃ lS ≤ S,
      lS = ‖S‖ ∧
        ∃ lL ≤ L,
          lL = ‖L‖ ∧
            (lS ≤ i * lL → z = 0) ∧
              (i * lL < lS →
                ∃ b ≤ S,
                  Exponential (i * lL) b ∧
                    ∃ hL ≤ 2 * L + 1, Exponential lL hL ∧ ∃ divS ≤ S, divS = S / b ∧ z = divS % hL)) →
    z = 0
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_graph
Proof state before:
case inl.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z S L i : M
le : ‖S‖ ≤ i * ‖L‖
⊢ z = 0 →
    ∃ lS ≤ S,
      lS = ‖S‖ ∧
        ∃ lL ≤ L,
          lL = ‖L‖ ∧
            (lS ≤ i * lL → z = 0) ∧
              (i * lL < lS →
                ∃ b ≤ S,
                  Exponential (i * lL) b ∧
                    ∃ hL ≤ 2 * L + 1, Exponential lL hL ∧ ∃ divS ≤ S, divS = S / b ∧ z = divS % hL)
Tactic:
rintro rfl
Proof state after:
case inl.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
S L i : M
le : ‖S‖ ≤ i * ‖L‖
⊢ ∃ lS ≤ S,
    lS = ‖S‖ ∧
      ∃ lL ≤ L,
        lL = ‖L‖ ∧
          (lS ≤ i * lL → 0 = 0) ∧
            (i * lL < lS →
              ∃ b ≤ S,
                Exponential (i * lL) b ∧ ∃ hL ≤ 2 * L + 1, Exponential lL hL ∧ ∃ divS ≤ S, divS = S / b ∧ 0 = divS % hL)
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_graph
Proof state before:
case inl.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
S L i : M
le : ‖S‖ ≤ i * ‖L‖
⊢ ∃ lS ≤ S,
    lS = ‖S‖ ∧
      ∃ lL ≤ L,
        lL = ‖L‖ ∧
          (lS ≤ i * lL → 0 = 0) ∧
            (i * lL < lS →
              ∃ b ≤ S,
                Exponential (i * lL) b ∧ ∃ hL ≤ 2 * L + 1, Exponential lL hL ∧ ∃ divS ≤ S, divS = S / b ∧ 0 = divS % hL)
Tactic:
exact ⟨‖S‖, by simp, rfl, ‖L‖, by simp, rfl, by simp [not_lt.mpr le]⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
S L i : M
le : ‖S‖ ≤ i * ‖L‖
⊢ ‖S‖ ≤ S
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
S L i : M
le : ‖S‖ ≤ i * ‖L‖
⊢ ‖L‖ ≤ L
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
S L i : M
le : ‖S‖ ≤ i * ‖L‖
⊢ (‖S‖ ≤ i * ‖L‖ → 0 = 0) ∧
    (i * ‖L‖ < ‖S‖ →
      ∃ b ≤ S,
        Exponential (i * ‖L‖) b ∧ ∃ hL ≤ 2 * L + 1, Exponential ‖L‖ hL ∧ ∃ divS ≤ S, divS = S / b ∧ 0 = divS % hL)
Tactic:
simp [not_lt.mpr le]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_graph
Proof state before:
case inl.mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z S L i : M
le : ‖S‖ ≤ i * ‖L‖
⊢ (∃ lS ≤ S,
      lS = ‖S‖ ∧
        ∃ lL ≤ L,
          lL = ‖L‖ ∧
            (lS ≤ i * lL → z = 0) ∧
              (i * lL < lS →
                ∃ b ≤ S,
                  Exponential (i * lL) b ∧
                    ∃ hL ≤ 2 * L + 1, Exponential lL hL ∧ ∃ divS ≤ S, divS = S / b ∧ z = divS % hL)) →
    z = 0
Tactic:
rintro ⟨_, _, rfl, _, _, rfl, h, _⟩
Proof state after:
case inl.mpr.intro.intro.intro.intro.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z S L i : M
le : ‖S‖ ≤ i * ‖L‖
left✝¹ : ‖S‖ ≤ S
left✝ : ‖L‖ ≤ L
h : ‖S‖ ≤ i * ‖L‖ → z = 0
right✝ :
  i * ‖L‖ < ‖S‖ →
    ∃ b ≤ S, Exponential (i * ‖L‖) b ∧ ∃ hL ≤ 2 * L + 1, Exponential ‖L‖ hL ∧ ∃ divS ≤ S, divS = S / b ∧ z = divS % hL
⊢ z = 0
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_graph
Proof state before:
case inl.mpr.intro.intro.intro.intro.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z S L i : M
le : ‖S‖ ≤ i * ‖L‖
left✝¹ : ‖S‖ ≤ S
left✝ : ‖L‖ ≤ L
h : ‖S‖ ≤ i * ‖L‖ → z = 0
right✝ :
  i * ‖L‖ < ‖S‖ →
    ∃ b ≤ S, Exponential (i * ‖L‖) b ∧ ∃ hL ≤ 2 * L + 1, Exponential ‖L‖ hL ∧ ∃ divS ≤ S, divS = S / b ∧ z = divS % hL
⊢ z = 0
Tactic:
exact h le
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_graph
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z S L i : M
lt : i * ‖L‖ < ‖S‖
⊢ (‖S‖ ≤ i * ‖L‖ → z = 0) ∧ (i * ‖L‖ < ‖S‖ → ∃ b ≤ S, Exponential (i * ‖L‖) b ∧ z = S / b % L # 1) ↔
    ∃ lS ≤ S,
      lS = ‖S‖ ∧
        ∃ lL ≤ L,
          lL = ‖L‖ ∧
            (lS ≤ i * lL → z = 0) ∧
              (i * lL < lS →
                ∃ b ≤ S,
                  Exponential (i * lL) b ∧
                    ∃ hL ≤ 2 * L + 1, Exponential lL hL ∧ ∃ divS ≤ S, divS = S / b ∧ z = divS % hL)
Tactic:
simp [lt, not_le.mpr lt]
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z S L i : M
lt : i * ‖L‖ < ‖S‖
⊢ (∃ b ≤ S, Exponential (i * ‖L‖) b ∧ z = S / b % L # 1) ↔
    ∃ lS ≤ S,
      lS = ‖S‖ ∧
        ∃ lL ≤ L,
          lL = ‖L‖ ∧
            (lS ≤ i * lL → z = 0) ∧
              (i * lL < lS →
                ∃ b ≤ S,
                  Exponential (i * lL) b ∧
                    ∃ hL ≤ 2 * L + 1, Exponential lL hL ∧ ∃ divS ≤ S, divS = S / b ∧ z = divS % hL)
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_graph
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z S L i : M
lt : i * ‖L‖ < ‖S‖
⊢ (∃ b ≤ S, Exponential (i * ‖L‖) b ∧ z = S / b % L # 1) ↔
    ∃ lS ≤ S,
      lS = ‖S‖ ∧
        ∃ lL ≤ L,
          lL = ‖L‖ ∧
            (lS ≤ i * lL → z = 0) ∧
              (i * lL < lS →
                ∃ b ≤ S,
                  Exponential (i * lL) b ∧
                    ∃ hL ≤ 2 * L + 1, Exponential lL hL ∧ ∃ divS ≤ S, divS = S / b ∧ z = divS % hL)
Tactic:
constructor
Proof state after:
case inr.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z S L i : M
lt : i * ‖L‖ < ‖S‖
⊢ (∃ b ≤ S, Exponential (i * ‖L‖) b ∧ z = S / b % L # 1) →
    ∃ lS ≤ S,
      lS = ‖S‖ ∧
        ∃ lL ≤ L,
          lL = ‖L‖ ∧
            (lS ≤ i * lL → z = 0) ∧
              (i * lL < lS →
                ∃ b ≤ S,
                  Exponential (i * lL) b ∧
                    ∃ hL ≤ 2 * L + 1, Exponential lL hL ∧ ∃ divS ≤ S, divS = S / b ∧ z = divS % hL)

case inr.mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z S L i : M
lt : i * ‖L‖ < ‖S‖
⊢ (∃ lS ≤ S,
      lS = ‖S‖ ∧
        ∃ lL ≤ L,
          lL = ‖L‖ ∧
            (lS ≤ i * lL → z = 0) ∧
              (i * lL < lS →
                ∃ b ≤ S,
                  Exponential (i * lL) b ∧
                    ∃ hL ≤ 2 * L + 1, Exponential lL hL ∧ ∃ divS ≤ S, divS = S / b ∧ z = divS % hL)) →
    ∃ b ≤ S, Exponential (i * ‖L‖) b ∧ z = S / b % L # 1