Theorem: LO.FirstOrder.Arith.Model.not_lenbit_iff_add_mul (Arithmetization/ISigmaZero/Exponential/Pow2.lean)

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i a : M
hi : Pow2 i
⊢ ¬LenBit i a ↔ ∃ k, ∃ r < i, a = k * (2 * i) + r
Tactic:
constructor
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 ⊧ₘ* 𝐈𝚫₀
i a : M
hi : Pow2 i
⊢ ¬LenBit i a → ∃ k, ∃ r < i, a = k * (2 * i) + r

case mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i a : M
hi : Pow2 i
⊢ (∃ k, ∃ r < i, a = k * (2 * i) + r) → ¬LenBit i a

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 ⊧ₘ* 𝐈𝚫₀
i a : M
hi : Pow2 i
⊢ ¬LenBit i a → ∃ k, ∃ r < i, a = k * (2 * i) + r
Tactic:
intro h
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 ⊧ₘ* 𝐈𝚫₀
i a : M
hi : Pow2 i
h : ¬LenBit i a
⊢ ∃ k, ∃ r < i, a = k * (2 * i) + r

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 ⊧ₘ* 𝐈𝚫₀
i a : M
hi : Pow2 i
h : ¬LenBit i a
⊢ ∃ k, ∃ r < i, a = k * (2 * i) + r
Tactic:
have : 2 * ((a / i) / 2) = a / i := by simpa [not_lenbit_iff_rem.mp h] using div_add_mod (a / i) 2
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 ⊧ₘ* 𝐈𝚫₀
i a : M
hi : Pow2 i
h : ¬LenBit i a
this : 2 * (a / i / 2) = a / i
⊢ ∃ k, ∃ r < i, a = k * (2 * i) + r

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 ⊧ₘ* 𝐈𝚫₀
i a : M
hi : Pow2 i
h : ¬LenBit i a
this : 2 * (a / i / 2) = a / i
⊢ ∃ k, ∃ r < i, a = k * (2 * i) + r
Tactic:
have : a = ((a / i) / 2) * (2 * i) + (a % i) := calc
  a = i * (a / i) + (a % i)              := Eq.symm <| div_add_mod a i
  _ = i * (2 * ((a / i) / 2)) + (a % i) := by simp [this]
  _ = ((a / i) / 2) * (2 * i) + (a % i) := by simp [mul_add, ←mul_assoc, mul_comm i 2, mul_comm (2 * i)]
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 ⊧ₘ* 𝐈𝚫₀
i a : M
hi : Pow2 i
h : ¬LenBit i a
this✝ : 2 * (a / i / 2) = a / i
this : a = a / i / 2 * (2 * i) + a % i
⊢ ∃ k, ∃ r < i, a = k * (2 * i) + r

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 ⊧ₘ* 𝐈𝚫₀
i a : M
hi : Pow2 i
h : ¬LenBit i a
this✝ : 2 * (a / i / 2) = a / i
this : a = a / i / 2 * (2 * i) + a % i
⊢ ∃ k, ∃ r < i, a = k * (2 * i) + r
Tactic:
exact ⟨(a / i) / 2, a % i, by simp [hi.pos], this⟩
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 ⊧ₘ* 𝐈𝚫₀
i a : M
hi : Pow2 i
h : ¬LenBit i a
⊢ 2 * (a / i / 2) = a / i
Tactic:
simpa [not_lenbit_iff_rem.mp h] using div_add_mod (a / i) 2
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 ⊧ₘ* 𝐈𝚫₀
i a : M
hi : Pow2 i
h : ¬LenBit i a
this : 2 * (a / i / 2) = a / i
⊢ i * (a / i) + a % i = i * (2 * (a / i / 2)) + a % i
Tactic:
simp [this]
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 ⊧ₘ* 𝐈𝚫₀
i a : M
hi : Pow2 i
h : ¬LenBit i a
this : 2 * (a / i / 2) = a / i
⊢ i * (2 * (a / i / 2)) + a % i = a / i / 2 * (2 * i) + a % i
Tactic:
simp [mul_add, ←mul_assoc, mul_comm i 2, mul_comm (2 * i)]
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 ⊧ₘ* 𝐈𝚫₀
i a : M
hi : Pow2 i
h : ¬LenBit i a
this✝ : 2 * (a / i / 2) = a / i
this : a = a / i / 2 * (2 * i) + a % i
⊢ a % i < i
Tactic:
simp [hi.pos]
State after:
no goals

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 ⊧ₘ* 𝐈𝚫₀
i a : M
hi : Pow2 i
⊢ (∃ k, ∃ r < i, a = k * (2 * i) + r) → ¬LenBit i a
Tactic:
rintro ⟨k, r, h, rfl⟩
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 ⊧ₘ* 𝐈𝚫₀
i : M
hi : Pow2 i
k r : M
h : r < i
⊢ ¬LenBit i (k * (2 * i) + r)

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 ⊧ₘ* 𝐈𝚫₀
i : M
hi : Pow2 i
k r : M
h : r < i
⊢ ¬LenBit i (k * (2 * i) + r)
Tactic:
simp [not_lenbit_iff_rem, ←mul_assoc, add_assoc, div_mul_add_self, hi.pos, h]
State after:
no goals