Theorem: LO.FirstOrder.Arith.Model.Pow2.lt_iff_two_mul_le (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 b : M
ha : Pow2 a
hb : Pow2 b
⊢ a < b ↔ 2 * a ≤ b
Tactic:
by_cases eb : b = 1
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 ⊧ₘ* 𝐈𝚫₀
a b : M
ha : Pow2 a
hb : Pow2 b
eb : b = 1
⊢ a < b ↔ 2 * a ≤ b

case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a b : M
ha : Pow2 a
hb : Pow2 b
eb : ¬b = 1
⊢ a < b ↔ 2 * a ≤ b

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 ⊧ₘ* 𝐈𝚫₀
a b : M
ha : Pow2 a
hb : Pow2 b
eb : b = 1
⊢ a < b ↔ 2 * a ≤ b
Tactic:
simp [eb, ←lt_two_iff_le_one]
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 ⊧ₘ* 𝐈𝚫₀
a b : M
ha : Pow2 a
hb : Pow2 b
eb : ¬b = 1
⊢ a < b ↔ 2 * a ≤ b
Tactic:
rw [←hb.two_mul_div_two eb]
State after:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a b : M
ha : Pow2 a
hb : Pow2 b
eb : ¬b = 1
⊢ a < 2 * (b / 2) ↔ 2 * a ≤ 2 * (b / 2)

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 ⊧ₘ* 𝐈𝚫₀
a b : M
ha : Pow2 a
hb : Pow2 b
eb : ¬b = 1
⊢ a < 2 * (b / 2) ↔ 2 * a ≤ 2 * (b / 2)
Tactic:
simp [le_iff_lt_two ha (hb.div_two eb)]
State after:
no goals