internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_graph
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‖
⊢ (∃ 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:
rintro ⟨b, hb, Hb, rfl⟩
Proof state after:
case inr.mp.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‖
b : M
hb : b ≤ S
Hb : Exponential (i * ‖L‖) b
⊢ ∃ lS ≤ S,
    lS = ‖S‖ ∧
      ∃ lL ≤ L,
        lL = ‖L‖ ∧
          (lS ≤ i * lL → S / b % L # 1 = 0) ∧
            (i * lL < lS →
              ∃ b_1 ≤ S,
                Exponential (i * lL) b_1 ∧
                  ∃ hL ≤ 2 * L + 1, Exponential lL hL ∧ ∃ divS ≤ S, divS = S / b_1 ∧ S / b % L # 1 = divS % hL)
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_graph
Proof state before:
case inr.mp.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‖
b : M
hb : b ≤ S
Hb : Exponential (i * ‖L‖) b
⊢ ∃ lS ≤ S,
    lS = ‖S‖ ∧
      ∃ lL ≤ L,
        lL = ‖L‖ ∧
          (lS ≤ i * lL → S / b % L # 1 = 0) ∧
            (i * lL < lS →
              ∃ b_1 ≤ S,
                Exponential (i * lL) b_1 ∧
                  ∃ hL ≤ 2 * L + 1, Exponential lL hL ∧ ∃ divS ≤ S, divS = S / b_1 ∧ S / b % L # 1 = divS % hL)
Tactic:
refine ⟨‖S‖, by simp, rfl, ‖L‖, by simp, rfl, ?_⟩
Proof state after:
case inr.mp.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‖
b : M
hb : b ≤ S
Hb : Exponential (i * ‖L‖) b
⊢ (‖S‖ ≤ i * ‖L‖ → S / b % L # 1 = 0) ∧
    (i * ‖L‖ < ‖S‖ →
      ∃ b_1 ≤ S,
        Exponential (i * ‖L‖) b_1 ∧
          ∃ hL ≤ 2 * L + 1, Exponential ‖L‖ hL ∧ ∃ divS ≤ S, divS = S / b_1 ∧ S / b % L # 1 = divS % hL)
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_graph
Proof state before:
case inr.mp.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‖
b : M
hb : b ≤ S
Hb : Exponential (i * ‖L‖) b
⊢ (‖S‖ ≤ i * ‖L‖ → S / b % L # 1 = 0) ∧
    (i * ‖L‖ < ‖S‖ →
      ∃ b_1 ≤ S,
        Exponential (i * ‖L‖) b_1 ∧
          ∃ hL ≤ 2 * L + 1, Exponential ‖L‖ hL ∧ ∃ divS ≤ S, divS = S / b_1 ∧ S / b % L # 1 = divS % hL)
Tactic:
simp [not_le.mpr lt, lt]
Proof state after:
case inr.mp.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‖
b : M
hb : b ≤ S
Hb : Exponential (i * ‖L‖) b
⊢ ∃ b_1 ≤ S,
    Exponential (i * ‖L‖) b_1 ∧
      ∃ hL ≤ 2 * L + 1, Exponential ‖L‖ hL ∧ ∃ divS ≤ S, divS = S / b_1 ∧ S / b % L # 1 = divS % hL
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_graph
Proof state before:
case inr.mp.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‖
b : M
hb : b ≤ S
Hb : Exponential (i * ‖L‖) b
⊢ ∃ b_1 ≤ S,
    Exponential (i * ‖L‖) b_1 ∧
      ∃ hL ≤ 2 * L + 1, Exponential ‖L‖ hL ∧ ∃ divS ≤ S, divS = S / b_1 ∧ S / b % L # 1 = divS % hL
Tactic:
exact ⟨b, hb, Hb, L # 1, by simp, exponential_hash_one L, S / b, by simp, rfl, 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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
S L i : M
lt : i * ‖L‖ < ‖S‖
b : M
hb : b ≤ S
Hb : Exponential (i * ‖L‖) b
⊢ ‖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
lt : i * ‖L‖ < ‖S‖
b : M
hb : b ≤ S
Hb : Exponential (i * ‖L‖) b
⊢ ‖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
lt : i * ‖L‖ < ‖S‖
b : M
hb : b ≤ S
Hb : Exponential (i * ‖L‖) b
⊢ L # 1 ≤ 2 * L + 1
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
lt : i * ‖L‖ < ‖S‖
b : M
hb : b ≤ S
Hb : Exponential (i * ‖L‖) b
⊢ S / b ≤ S
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_graph
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‖
⊢ (∃ 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
Tactic:
rintro ⟨_, _, rfl, _, _, rfl, _, h⟩
Proof state after:
case inr.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
lt : i * ‖L‖ < ‖S‖
left✝² : ‖S‖ ≤ S
left✝¹ : ‖L‖ ≤ L
left✝ : ‖S‖ ≤ i * ‖L‖ → z = 0
h :
  i * ‖L‖ < ‖S‖ →
    ∃ b ≤ S, Exponential (i * ‖L‖) b ∧ ∃ hL ≤ 2 * L + 1, Exponential ‖L‖ hL ∧ ∃ divS ≤ S, divS = S / b ∧ z = divS % hL
⊢ ∃ b ≤ S, Exponential (i * ‖L‖) b ∧ z = S / b % L # 1
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_graph
Proof state before:
case inr.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
lt : i * ‖L‖ < ‖S‖
left✝² : ‖S‖ ≤ S
left✝¹ : ‖L‖ ≤ L
left✝ : ‖S‖ ≤ i * ‖L‖ → z = 0
h :
  i * ‖L‖ < ‖S‖ →
    ∃ b ≤ S, Exponential (i * ‖L‖) b ∧ ∃ hL ≤ 2 * L + 1, Exponential ‖L‖ hL ∧ ∃ divS ≤ S, divS = S / b ∧ z = divS % hL
⊢ ∃ b ≤ S, Exponential (i * ‖L‖) b ∧ z = S / b % L # 1
Tactic:
rcases h lt with ⟨b, hb, Hb, hL, _, HhL, _, _, rfl, rfl⟩
Proof state after:
case inr.mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro.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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
S L i : M
lt : i * ‖L‖ < ‖S‖
left✝⁴ : ‖S‖ ≤ S
left✝³ : ‖L‖ ≤ L
b : M
hb : b ≤ S
Hb : Exponential (i * ‖L‖) b
hL : M
left✝² : hL ≤ 2 * L + 1
HhL : Exponential ‖L‖ hL
left✝¹ : S / b ≤ S
left✝ : ‖S‖ ≤ i * ‖L‖ → S / b % hL = 0
h :
  i * ‖L‖ < ‖S‖ →
    ∃ b_1 ≤ S,
      Exponential (i * ‖L‖) b_1 ∧
        ∃ hL_1 ≤ 2 * L + 1, Exponential ‖L‖ hL_1 ∧ ∃ divS ≤ S, divS = S / b_1 ∧ S / b % hL = divS % hL_1
⊢ ∃ b_1 ≤ S, Exponential (i * ‖L‖) b_1 ∧ S / b % hL = S / b_1 % L # 1
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_graph
Proof state before:
case inr.mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro.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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
S L i : M
lt : i * ‖L‖ < ‖S‖
left✝⁴ : ‖S‖ ≤ S
left✝³ : ‖L‖ ≤ L
b : M
hb : b ≤ S
Hb : Exponential (i * ‖L‖) b
hL : M
left✝² : hL ≤ 2 * L + 1
HhL : Exponential ‖L‖ hL
left✝¹ : S / b ≤ S
left✝ : ‖S‖ ≤ i * ‖L‖ → S / b % hL = 0
h :
  i * ‖L‖ < ‖S‖ →
    ∃ b_1 ≤ S,
      Exponential (i * ‖L‖) b_1 ∧
        ∃ hL_1 ≤ 2 * L + 1, Exponential ‖L‖ hL_1 ∧ ∃ divS ≤ S, divS = S / b_1 ∧ S / b % hL = divS % hL_1
⊢ ∃ b_1 ≤ S, Exponential (i * ‖L‖) b_1 ∧ S / b % hL = S / b_1 % L # 1
Tactic:
exact ⟨b, hb, Hb, by rw [HhL.uniq (exponential_hash_one L)]⟩
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
lt : i * ‖L‖ < ‖S‖
left✝⁴ : ‖S‖ ≤ S
left✝³ : ‖L‖ ≤ L
b : M
hb : b ≤ S
Hb : Exponential (i * ‖L‖) b
hL : M
left✝² : hL ≤ 2 * L + 1
HhL : Exponential ‖L‖ hL
left✝¹ : S / b ≤ S
left✝ : ‖S‖ ≤ i * ‖L‖ → S / b % hL = 0
h :
  i * ‖L‖ < ‖S‖ →
    ∃ b_1 ≤ S,
      Exponential (i * ‖L‖) b_1 ∧
        ∃ hL_1 ≤ 2 * L + 1, Exponential ‖L‖ hL_1 ∧ ∃ divS ≤ S, divS = S / b_1 ∧ S / b % hL = divS % hL_1
⊢ S / b % hL = S / b % L # 1
Tactic:
rw [HhL.uniq (exponential_hash_one L)]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.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₃ ext 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 3) → M
⊢ (fun v => v 0 = (fun v => v 1{v 0}[v 2]) fun x => v x.succ) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val extDef)
Theorem: LO.FirstOrder.Arith.Model.Nuon.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 3) → M
⊢ (fun v => v 0 = (fun v => v 1{v 0}[v 2]) fun x => v x.succ) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val extDef)
Tactic:
simp [extDef, length_defined.df.iff, Exponential.defined.df.iff,
div_defined.df.iff, rem_defined.df.iff, lt_succ_iff_le, ext_graph, numeral_eq_natCast]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L i : M
⊢ 0{L}[i] = 0
Tactic:
simp [ext]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_zero_eq_self_of_le
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 : M
h : ‖S‖ ≤ ‖L‖
⊢ S{L}[0] = S
Tactic:
rcases zero_le S 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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L : M
h : ‖0‖ ≤ ‖L‖
⊢ 0{L}[0] = 0

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S : M
h : ‖S‖ ≤ ‖L‖
pos : 0 < S
⊢ S{L}[0] = S
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_zero_eq_self_of_le
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L : M
h : ‖0‖ ≤ ‖L‖
⊢ 0{L}[0] = 0
Tactic:
simp [ext]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_zero_eq_self_of_le
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S : M
h : ‖S‖ ≤ ‖L‖
pos : 0 < S
⊢ S{L}[0] = S
Tactic:
simp [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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S : M
h : ‖S‖ ≤ ‖L‖
pos : 0 < S
⊢ S / bexp S 0 % L # 1 = S
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_zero_eq_self_of_le
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S : M
h : ‖S‖ ≤ ‖L‖
pos : 0 < S
⊢ S / bexp S 0 % L # 1 = S
Tactic:
have : bexp S 0 = 1 := (exp_bexp_of_lt (show 0 < ‖S‖ from by simp [pos])).zero_uniq
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S : M
h : ‖S‖ ≤ ‖L‖
pos : 0 < S
this : bexp S 0 = 1
⊢ S / bexp S 0 % L # 1 = S
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_zero_eq_self_of_le
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S : M
h : ‖S‖ ≤ ‖L‖
pos : 0 < S
this : bexp S 0 = 1
⊢ S / bexp S 0 % L # 1 = S
Tactic:
simp [this, lt_hash_one_iff.mpr h]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_zero_eq_self_of_le
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 : M
h : ‖S‖ ≤ ‖L‖
pos : 0 < S
⊢ 0 < ‖S‖
Tactic:
simp [pos]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_eq_of_ge
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 S' i : M
h : S ≤ S'
⊢ S / bexp S' (i * ‖L‖) % L # 1 = S{L}[i]
Tactic:
rcases show i * ‖L‖ < ‖S‖ ∨ ‖S‖ ≤ i * ‖L‖ from lt_or_ge (i * ‖L‖) ‖S‖ with (lt | 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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S S' i : M
h : S ≤ S'
lt : i * ‖L‖ < ‖S‖
⊢ S / bexp S' (i * ‖L‖) % L # 1 = S{L}[i]

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S S' i : M
h : S ≤ S'
le : ‖S‖ ≤ i * ‖L‖
⊢ S / bexp S' (i * ‖L‖) % L # 1 = S{L}[i]
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_eq_of_ge
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S S' i : M
h : S ≤ S'
lt : i * ‖L‖ < ‖S‖
⊢ S / bexp S' (i * ‖L‖) % L # 1 = S{L}[i]
Tactic:
unfold ext
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S S' i : M
h : S ≤ S'
lt : i * ‖L‖ < ‖S‖
⊢ S / bexp S' (i * ‖L‖) % L # 1 = S / bexp S (i * ‖L‖) % L # 1
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_eq_of_ge
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S S' i : M
h : S ≤ S'
lt : i * ‖L‖ < ‖S‖
⊢ S / bexp S' (i * ‖L‖) % L # 1 = S / bexp S (i * ‖L‖) % L # 1
Tactic:
congr 2
Proof state after:
case inl.e_a.e_a
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S S' i : M
h : S ≤ S'
lt : i * ‖L‖ < ‖S‖
⊢ bexp S' (i * ‖L‖) = bexp S (i * ‖L‖)
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_eq_of_ge
Proof state before:
case inl.e_a.e_a
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S S' i : M
h : S ≤ S'
lt : i * ‖L‖ < ‖S‖
⊢ bexp S' (i * ‖L‖) = bexp S (i * ‖L‖)
Tactic:
exact bexp_eq_of_lt_length (lt_of_lt_of_le lt $ length_monotone h) lt
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_eq_of_ge
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S S' i : M
h : S ≤ S'
le : ‖S‖ ≤ i * ‖L‖
⊢ S / bexp S' (i * ‖L‖) % L # 1 = S{L}[i]
Tactic:
simp [ext_eq_zero_of_lt le]
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S S' i : M
h : S ≤ S'
le : ‖S‖ ≤ i * ‖L‖
⊢ S / bexp S' (i * ‖L‖) % L # 1 = 0
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_eq_of_ge
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S S' i : M
h : S ≤ S'
le : ‖S‖ ≤ i * ‖L‖
⊢ S / bexp S' (i * ‖L‖) % L # 1 = 0
Tactic:
rcases show i * ‖L‖ < ‖S'‖ ∨ ‖S'‖ ≤ i * ‖L‖ from lt_or_ge (i * ‖L‖) ‖S'‖ with (lt' | le')
Proof state after:
case inr.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S S' i : M
h : S ≤ S'
le : ‖S‖ ≤ i * ‖L‖
lt' : i * ‖L‖ < ‖S'‖
⊢ S / bexp S' (i * ‖L‖) % L # 1 = 0

case inr.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S S' i : M
h : S ≤ S'
le : ‖S‖ ≤ i * ‖L‖
le' : ‖S'‖ ≤ i * ‖L‖
⊢ S / bexp S' (i * ‖L‖) % L # 1 = 0
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_eq_of_ge
Proof state before:
case inr.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S S' i : M
h : S ≤ S'
le : ‖S‖ ≤ i * ‖L‖
lt' : i * ‖L‖ < ‖S'‖
⊢ S / bexp S' (i * ‖L‖) % L # 1 = 0
Tactic:
have : S < bexp S' (i * ‖L‖) := ((exp_bexp_of_lt lt').lt_iff_len_le).mpr le
Proof state after:
case inr.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S S' i : M
h : S ≤ S'
le : ‖S‖ ≤ i * ‖L‖
lt' : i * ‖L‖ < ‖S'‖
this : S < bexp S' (i * ‖L‖)
⊢ S / bexp S' (i * ‖L‖) % L # 1 = 0
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_eq_of_ge
Proof state before:
case inr.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S S' i : M
h : S ≤ S'
le : ‖S‖ ≤ i * ‖L‖
lt' : i * ‖L‖ < ‖S'‖
this : S < bexp S' (i * ‖L‖)
⊢ S / bexp S' (i * ‖L‖) % L # 1 = 0
Tactic:
simp [this]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_eq_of_ge
Proof state before:
case inr.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S S' i : M
h : S ≤ S'
le : ‖S‖ ≤ i * ‖L‖
le' : ‖S'‖ ≤ i * ‖L‖
⊢ S / bexp S' (i * ‖L‖) % L # 1 = 0
Tactic:
simp [bexp_eq_zero_of_le le']
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_eq_of_gt
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 S' i : M
h : i * ‖L‖ < ‖S'‖
⊢ S / bexp S' (i * ‖L‖) % L # 1 = S{L}[i]
Tactic:
rcases show i * ‖L‖ < ‖S‖ ∨ ‖S‖ ≤ i * ‖L‖ from lt_or_ge (i * ‖L‖) ‖S‖ with (lt | 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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S S' i : M
h : i * ‖L‖ < ‖S'‖
lt : i * ‖L‖ < ‖S‖
⊢ S / bexp S' (i * ‖L‖) % L # 1 = S{L}[i]

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S S' i : M
h : i * ‖L‖ < ‖S'‖
le : ‖S‖ ≤ i * ‖L‖
⊢ S / bexp S' (i * ‖L‖) % L # 1 = S{L}[i]
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_eq_of_gt
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S S' i : M
h : i * ‖L‖ < ‖S'‖
lt : i * ‖L‖ < ‖S‖
⊢ S / bexp S' (i * ‖L‖) % L # 1 = S{L}[i]
Tactic:
unfold ext
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S S' i : M
h : i * ‖L‖ < ‖S'‖
lt : i * ‖L‖ < ‖S‖
⊢ S / bexp S' (i * ‖L‖) % L # 1 = S / bexp S (i * ‖L‖) % L # 1
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_eq_of_gt
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S S' i : M
h : i * ‖L‖ < ‖S'‖
lt : i * ‖L‖ < ‖S‖
⊢ S / bexp S' (i * ‖L‖) % L # 1 = S / bexp S (i * ‖L‖) % L # 1
Tactic:
congr 2
Proof state after:
case inl.e_a.e_a
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S S' i : M
h : i * ‖L‖ < ‖S'‖
lt : i * ‖L‖ < ‖S‖
⊢ bexp S' (i * ‖L‖) = bexp S (i * ‖L‖)
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_eq_of_gt
Proof state before:
case inl.e_a.e_a
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S S' i : M
h : i * ‖L‖ < ‖S'‖
lt : i * ‖L‖ < ‖S‖
⊢ bexp S' (i * ‖L‖) = bexp S (i * ‖L‖)
Tactic:
exact bexp_eq_of_lt_length h lt
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_eq_of_gt
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S S' i : M
h : i * ‖L‖ < ‖S'‖
le : ‖S‖ ≤ i * ‖L‖
⊢ S / bexp S' (i * ‖L‖) % L # 1 = S{L}[i]
Tactic:
simp [ext_eq_zero_of_lt le]
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S S' i : M
h : i * ‖L‖ < ‖S'‖
le : ‖S‖ ≤ i * ‖L‖
⊢ S / bexp S' (i * ‖L‖) % L # 1 = 0
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_eq_of_gt
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S S' i : M
h : i * ‖L‖ < ‖S'‖
le : ‖S‖ ≤ i * ‖L‖
⊢ S / bexp S' (i * ‖L‖) % L # 1 = 0
Tactic:
have : S < bexp S' (i * ‖L‖) := ((exp_bexp_of_lt h).lt_iff_len_le).mpr le
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S S' i : M
h : i * ‖L‖ < ‖S'‖
le : ‖S‖ ≤ i * ‖L‖
this : S < bexp S' (i * ‖L‖)
⊢ S / bexp S' (i * ‖L‖) % L # 1 = 0
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_eq_of_gt
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S S' i : M
h : i * ‖L‖ < ‖S'‖
le : ‖S‖ ≤ i * ‖L‖
this : S < bexp S' (i * ‖L‖)
⊢ S / bexp S' (i * ‖L‖) % L # 1 = 0
Tactic:
simp [this]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_add₁_pow2
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 i S₁ S₂ p : M
pp : Pow2 p
h : (i + 1) * ‖L‖ < ‖p‖
⊢ (S₁ + S₂ * p){L}[i] = S₁{L}[i]
Tactic:
rcases zero_le S₂ 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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L i S₁ p : M
pp : Pow2 p
h : (i + 1) * ‖L‖ < ‖p‖
⊢ (S₁ + 0 * p){L}[i] = S₁{L}[i]

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L i S₁ S₂ p : M
pp : Pow2 p
h : (i + 1) * ‖L‖ < ‖p‖
pos₂ : 0 < S₂
⊢ (S₁ + S₂ * p){L}[i] = S₁{L}[i]
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_add₁_pow2
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L i S₁ S₂ p : M
pp : Pow2 p
h : (i + 1) * ‖L‖ < ‖p‖
pos₂ : 0 < S₂
⊢ (S₁ + S₂ * p){L}[i] = S₁{L}[i]
Tactic:
have lt_len : i * ‖L‖ < ‖S₁ + S₂ * p‖ := calc
      i * ‖L‖ ≤ (i + 1) * ‖L‖ := mul_le_mul_right (by simp)
      _       < ‖p‖           := h
      _       ≤ ‖S₁ + S₂ * p‖ := length_monotone (le_add_left (le_mul_of_pos_left pos₂))
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L i S₁ S₂ p : M
pp : Pow2 p
h : (i + 1) * ‖L‖ < ‖p‖
pos₂ : 0 < S₂
lt_len : i * ‖L‖ < ‖S₁ + S₂ * p‖
⊢ (S₁ + S₂ * p){L}[i] = S₁{L}[i]
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_add₁_pow2
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L i S₁ S₂ p : M
pp : Pow2 p
h : (i + 1) * ‖L‖ < ‖p‖
pos₂ : 0 < S₂
lt_len : i * ‖L‖ < ‖S₁ + S₂ * p‖
⊢ (S₁ + S₂ * p){L}[i] = S₁{L}[i]
Tactic:
have : Exponential ((i + 1) * ‖L‖) (bexp (S₁ + S₂ * p) (i * ‖L‖) * L # 1) := by
  simp [add_mul]
  exact Exponential.add_mul (by simp [lt_len]) (by simpa using exponential_hash L 1)
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L i S₁ S₂ p : M
pp : Pow2 p
h : (i + 1) * ‖L‖ < ‖p‖
pos₂ : 0 < S₂
lt_len : i * ‖L‖ < ‖S₁ + S₂ * p‖
this : Exponential ((i + 1) * ‖L‖) (bexp (S₁ + S₂ * p) (i * ‖L‖) * L # 1)
⊢ (S₁ + S₂ * p){L}[i] = S₁{L}[i]