Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_graph (Arithmetization/OmegaOne/Nuon.lean)

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
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]
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)

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)
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)

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]
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)

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
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

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
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)

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]⟩
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
S L i : M
le : ‖S‖ ≤ i * ‖L‖
⊢ ‖S‖ ≤ S
Tactic:
simp
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
S L i : M
le : ‖S‖ ≤ i * ‖L‖
⊢ ‖L‖ ≤ L
Tactic:
simp
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
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]
State after:
no goals

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, _⟩
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

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
State after:
no goals

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]
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)

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
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

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⟩
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)

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, ?_⟩
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)

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]
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

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⟩
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
S L i : M
lt : i * ‖L‖ < ‖S‖
b : M
hb : b ≤ S
Hb : Exponential (i * ‖L‖) b
⊢ ‖S‖ ≤ S
Tactic:
simp
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
S L i : M
lt : i * ‖L‖ < ‖S‖
b : M
hb : b ≤ S
Hb : Exponential (i * ‖L‖) b
⊢ ‖L‖ ≤ L
Tactic:
simp
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
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
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
S L i : M
lt : i * ‖L‖ < ‖S‖
b : M
hb : b ≤ S
Hb : Exponential (i * ‖L‖) b
⊢ S / b ≤ S
Tactic:
simp
State after:
no goals

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⟩
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

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⟩
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

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)]⟩
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
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)]
State after:
no goals