Theorem: LO.FirstOrder.Arith.Model.LenBit.add_pow2_iff_of_lt (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 ⊧ₘ* 𝐈𝚫₀
a i j : M
pi : Pow2 i
pj : Pow2 j
h : a < j
⊢ LenBit i (a + j) ↔ i = j ∨ LenBit i a
Tactic:
rcases show i < j ∨ i = j ∨ i > j from lt_trichotomy i j with (hij | rfl | hij)
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 ⊧ₘ* 𝐈𝚫₀
a i j : M
pi : Pow2 i
pj : Pow2 j
h : a < j
hij : i < j
⊢ LenBit i (a + j) ↔ i = j ∨ LenBit i a

case inr.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a i : M
pi pj : Pow2 i
h : a < i
⊢ LenBit i (a + i) ↔ i = i ∨ LenBit i a

case inr.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a i j : M
pi : Pow2 i
pj : Pow2 j
h : a < j
hij : i > j
⊢ LenBit i (a + j) ↔ i = j ∨ LenBit i a

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 ⊧ₘ* 𝐈𝚫₀
a i j : M
pi : Pow2 i
pj : Pow2 j
h : a < j
hij : i < j
⊢ LenBit i (a + j) ↔ i = j ∨ LenBit i a
Tactic:
simp [LenBit.add_pow2 pi pj hij, hij.ne]
State after:
no goals

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 ⊧ₘ* 𝐈𝚫₀
a i : M
pi pj : Pow2 i
h : a < i
⊢ LenBit i (a + i) ↔ i = i ∨ LenBit i a
Tactic:
simp [LenBit.add_self h]
State after:
no goals

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 ⊧ₘ* 𝐈𝚫₀
a i j : M
pi : Pow2 i
pj : Pow2 j
h : a < j
hij : i > j
⊢ LenBit i (a + j) ↔ i = j ∨ LenBit i a
Tactic:
have : a + j < i := calc
  a + j < 2 * j  := by simp[two_mul, h]
  _     ≤ i      := (pj.lt_iff_two_mul_le pi).mp hij
State after:
case inr.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a i j : M
pi : Pow2 i
pj : Pow2 j
h : a < j
hij : i > j
this : a + j < i
⊢ LenBit i (a + j) ↔ i = j ∨ LenBit i a

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 ⊧ₘ* 𝐈𝚫₀
a i j : M
pi : Pow2 i
pj : Pow2 j
h : a < j
hij : i > j
this : a + j < i
⊢ LenBit i (a + j) ↔ i = j ∨ LenBit i a
Tactic:
simp [not_lenbit_of_lt this, not_lenbit_of_lt (show a < i from lt_trans _ _ _ h hij), hij.ne.symm]
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 ⊧ₘ* 𝐈𝚫₀
a i j : M
pi : Pow2 i
pj : Pow2 j
h : a < j
hij : i > j
⊢ a + j < 2 * j
Tactic:
simp[two_mul, h]
State after:
no goals