Theorem: LO.FirstOrder.Arith.Model.LenBit.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 ⊧ₘ* 𝐈open
i a b : M
h : 2 * i ∣ b
⊢ LenBit i (a + b) ↔ LenBit i a
Tactic:
have : 0 ≤ i := zero_le i
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a b : M
h : 2 * i ∣ b
this : 0 ≤ i
⊢ LenBit i (a + b) ↔ LenBit i a

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a b : M
h : 2 * i ∣ b
this : 0 ≤ i
⊢ LenBit i (a + b) ↔ LenBit i a
Tactic:
rcases (eq_or_lt_of_le this) with (rfl | pos)
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 ⊧ₘ* 𝐈open
a b : M
h : 2 * 0 ∣ b
this : 0 ≤ 0
⊢ LenBit 0 (a + b) ↔ LenBit 0 a

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a b : M
h : 2 * i ∣ b
this : 0 ≤ i
pos : 0 < i
⊢ LenBit i (a + b) ↔ LenBit i a

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 ⊧ₘ* 𝐈open
i a b : M
h : 2 * i ∣ b
this : 0 ≤ i
pos : 0 < i
⊢ LenBit i (a + b) ↔ LenBit i a
Tactic:
rcases h with ⟨b', hb'⟩
State after:
case inr.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a b : M
this : 0 ≤ i
pos : 0 < i
b' : M
hb' : b = 2 * i * b'
⊢ LenBit i (a + b) ↔ LenBit i a

State before:
case inr.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a b : M
this : 0 ≤ i
pos : 0 < i
b' : M
hb' : b = 2 * i * b'
⊢ LenBit i (a + b) ↔ LenBit i a
Tactic:
have hb' : b = 2 * b' * i := by simp [hb', mul_right_comm]
State after:
case inr.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a b : M
this : 0 ≤ i
pos : 0 < i
b' : M
hb'✝ : b = 2 * i * b'
hb' : b = 2 * b' * i
⊢ LenBit i (a + b) ↔ LenBit i a

State before:
case inr.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a b : M
this : 0 ≤ i
pos : 0 < i
b' : M
hb'✝ : b = 2 * i * b'
hb' : b = 2 * b' * i
⊢ LenBit i (a + b) ↔ LenBit i a
Tactic:
calc
  LenBit i (a + b) ↔ ((a + b) / i) % 2 = 1    := LenBit.iff_rem
  _                ↔ (a / i + 2 * b') % 2 = 1 := by rw [hb', div_add_mul_self _ _ pos]
  _                ↔ LenBit i a               := by simp [LenBit.iff_rem]
State after:
no goals

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 ⊧ₘ* 𝐈open
a b : M
h : 2 * 0 ∣ b
this : 0 ≤ 0
⊢ LenBit 0 (a + b) ↔ LenBit 0 a
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 ⊧ₘ* 𝐈open
i a b : M
this : 0 ≤ i
pos : 0 < i
b' : M
hb' : b = 2 * i * b'
⊢ b = 2 * b' * i
Tactic:
simp [hb', mul_right_comm]
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 ⊧ₘ* 𝐈open
i a b : M
this : 0 ≤ i
pos : 0 < i
b' : M
hb'✝ : b = 2 * i * b'
hb' : b = 2 * b' * i
⊢ (a + b) / i % 2 = 1 ↔ (a / i + 2 * b') % 2 = 1
Tactic:
rw [hb', div_add_mul_self _ _ pos]
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 ⊧ₘ* 𝐈open
i a b : M
this : 0 ≤ i
pos : 0 < i
b' : M
hb'✝ : b = 2 * i * b'
hb' : b = 2 * b' * i
⊢ (a / i + 2 * b') % 2 = 1 ↔ LenBit i a
Tactic:
simp [LenBit.iff_rem]
State after:
no goals