Theorem: LO.FirstOrder.Arith.Model.lenbit_mul_add (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 j a r : M
pi : Pow2 i
pj : Pow2 j
hr : r < j
⊢ LenBit (i * j) (a * j + r) ↔ LenBit i a
Tactic:
by_cases h : LenBit i a <;> simp [h]
State after:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i j a r : M
pi : Pow2 i
pj : Pow2 j
hr : r < j
h : LenBit i a
⊢ LenBit (i * j) (a * j + r)

case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i j a r : M
pi : Pow2 i
pj : Pow2 j
hr : r < j
h : ¬LenBit i a
⊢ ¬LenBit (i * j) (a * j + r)

State before:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i j a r : M
pi : Pow2 i
pj : Pow2 j
hr : r < j
h : LenBit i a
⊢ LenBit (i * j) (a * j + r)
Tactic:
rcases (lenbit_iff_add_mul pi).mp h with ⟨a, b, hb, rfl⟩
State after:
case pos.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 j r : M
pi : Pow2 i
pj : Pow2 j
hr : r < j
a b : M
hb : b < i
h : LenBit i (a * (2 * i) + i + b)
⊢ LenBit (i * j) ((a * (2 * i) + i + b) * j + r)

State before:
case pos.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 j r : M
pi : Pow2 i
pj : Pow2 j
hr : r < j
a b : M
hb : b < i
h : LenBit i (a * (2 * i) + i + b)
⊢ LenBit (i * j) ((a * (2 * i) + i + b) * j + r)
Tactic:
have : b * j + r < i * j :=
  pj.mul_add_lt_of_mul_lt_of_pos (by simp[pi, pj]) ((mul_lt_mul_right pj.pos).mpr hb)  hr (lt_of_lt_of_le hr $ le_mul_of_pos_left $ pi.pos)
State after:
case pos.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 j r : M
pi : Pow2 i
pj : Pow2 j
hr : r < j
a b : M
hb : b < i
h : LenBit i (a * (2 * i) + i + b)
this : b * j + r < i * j
⊢ LenBit (i * j) ((a * (2 * i) + i + b) * j + r)

State before:
case pos.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 j r : M
pi : Pow2 i
pj : Pow2 j
hr : r < j
a b : M
hb : b < i
h : LenBit i (a * (2 * i) + i + b)
this : b * j + r < i * j
⊢ LenBit (i * j) ((a * (2 * i) + i + b) * j + r)
Tactic:
exact (lenbit_iff_add_mul (by simp [pi, pj])).mpr ⟨a, b * j + r, this, by simp [add_mul, add_assoc, mul_assoc]⟩
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 j r : M
pi : Pow2 i
pj : Pow2 j
hr : r < j
a b : M
hb : b < i
h : LenBit i (a * (2 * i) + i + b)
⊢ Pow2 (i * j)
Tactic:
simp[pi, pj]
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 j r : M
pi : Pow2 i
pj : Pow2 j
hr : r < j
a b : M
hb : b < i
h : LenBit i (a * (2 * i) + i + b)
this : b * j + r < i * j
⊢ Pow2 (i * j)
Tactic:
simp [pi, pj]
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 j r : M
pi : Pow2 i
pj : Pow2 j
hr : r < j
a b : M
hb : b < i
h : LenBit i (a * (2 * i) + i + b)
this : b * j + r < i * j
⊢ (a * (2 * i) + i + b) * j + r = a * (2 * (i * j)) + i * j + (b * j + r)
Tactic:
simp [add_mul, add_assoc, mul_assoc]
State after:
no goals

State before:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i j a r : M
pi : Pow2 i
pj : Pow2 j
hr : r < j
h : ¬LenBit i a
⊢ ¬LenBit (i * j) (a * j + r)
Tactic:
rcases (not_lenbit_iff_add_mul pi).mp h with ⟨a, b, hb, rfl⟩
State after:
case neg.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 j r : M
pi : Pow2 i
pj : Pow2 j
hr : r < j
a b : M
hb : b < i
h : ¬LenBit i (a * (2 * i) + b)
⊢ ¬LenBit (i * j) ((a * (2 * i) + b) * j + r)

State before:
case neg.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 j r : M
pi : Pow2 i
pj : Pow2 j
hr : r < j
a b : M
hb : b < i
h : ¬LenBit i (a * (2 * i) + b)
⊢ ¬LenBit (i * j) ((a * (2 * i) + b) * j + r)
Tactic:
have : b * j + r < i * j :=
  pj.mul_add_lt_of_mul_lt_of_pos (by simp[pi, pj]) ((mul_lt_mul_right pj.pos).mpr hb) hr (lt_of_lt_of_le hr $ le_mul_of_pos_left $ pi.pos)
State after:
case neg.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 j r : M
pi : Pow2 i
pj : Pow2 j
hr : r < j
a b : M
hb : b < i
h : ¬LenBit i (a * (2 * i) + b)
this : b * j + r < i * j
⊢ ¬LenBit (i * j) ((a * (2 * i) + b) * j + r)

State before:
case neg.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 j r : M
pi : Pow2 i
pj : Pow2 j
hr : r < j
a b : M
hb : b < i
h : ¬LenBit i (a * (2 * i) + b)
this : b * j + r < i * j
⊢ ¬LenBit (i * j) ((a * (2 * i) + b) * j + r)
Tactic:
exact (not_lenbit_iff_add_mul (by simp [pi, pj])).mpr ⟨a, b * j + r, this, by simp [add_mul, add_assoc, mul_assoc]⟩
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 j r : M
pi : Pow2 i
pj : Pow2 j
hr : r < j
a b : M
hb : b < i
h : ¬LenBit i (a * (2 * i) + b)
⊢ Pow2 (i * j)
Tactic:
simp[pi, pj]
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 j r : M
pi : Pow2 i
pj : Pow2 j
hr : r < j
a b : M
hb : b < i
h : ¬LenBit i (a * (2 * i) + b)
this : b * j + r < i * j
⊢ Pow2 (i * j)
Tactic:
simp [pi, pj]
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 j r : M
pi : Pow2 i
pj : Pow2 j
hr : r < j
a b : M
hb : b < i
h : ¬LenBit i (a * (2 * i) + b)
this : b * j + r < i * j
⊢ (a * (2 * i) + b) * j + r = a * (2 * (i * j)) + (b * j + r)
Tactic:
simp [add_mul, add_assoc, mul_assoc]
State after:
no goals