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

case mpr
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 < 2 * b → a ≤ b

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 ⊧ₘ* 𝐈𝚫₀
a b : M
ha : Pow2 a
hb : Pow2 b
⊢ a ≤ b → a < 2 * b
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 ⊧ₘ* 𝐈𝚫₀
a b : M
ha : Pow2 a
hb : Pow2 b
h : a ≤ b
⊢ a < 2 * b

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 ⊧ₘ* 𝐈𝚫₀
a b : M
ha : Pow2 a
hb : Pow2 b
h : a ≤ b
⊢ a < 2 * b
Tactic:
exact lt_of_le_of_lt h (lt_two_mul_self hb.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 ⊧ₘ* 𝐈𝚫₀
a b : M
ha : Pow2 a
hb : Pow2 b
⊢ a < 2 * b → a ≤ b
Tactic:
intro h
State after:
case mpr
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
h : a < 2 * b
⊢ a ≤ b

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 ⊧ₘ* 𝐈𝚫₀
a b : M
ha : Pow2 a
hb : Pow2 b
h : a < 2 * b
⊢ a ≤ b
Tactic:
by_cases ea : a = 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
h : a < 2 * b
ea : a = 1
⊢ 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
h : a < 2 * b
ea : ¬a = 1
⊢ 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
h : a < 2 * b
ea : a = 1
⊢ a ≤ b
Tactic:
rcases ea with rfl
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 ⊧ₘ* 𝐈𝚫₀
b : M
hb : Pow2 b
ha : Pow2 1
h : 1 < 2 * b
⊢ 1 ≤ 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 ⊧ₘ* 𝐈𝚫₀
b : M
hb : Pow2 b
ha : Pow2 1
h : 1 < 2 * b
⊢ 1 ≤ b
Tactic:
simpa [←pos_iff_one_le] using hb.pos
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
h : a < 2 * b
ea : ¬a = 1
⊢ a ≤ b
Tactic:
suffices a ∣ b from le_of_dvd hb.pos this
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
h : a < 2 * b
ea : ¬a = 1
⊢ a ∣ b

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
h : a < 2 * b
ea : ¬a = 1
⊢ a ∣ b
Tactic:
have : a / 2 ∣ b := by
  have : 2 * (a / 2) ∣ 2 * b := by
    simpa [ha.two_mul_div_two ea] using dvd_of_le ha (by simpa using hb) (LT.lt.le h)
  exact (mul_dvd_mul_iff_left (by simp)).mp this
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
h : a < 2 * b
ea : ¬a = 1
this : a / 2 ∣ b
⊢ a ∣ b

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
h : a < 2 * b
ea : ¬a = 1
this : a / 2 ∣ b
⊢ a ∣ b
Tactic:
rcases this with ⟨b', rfl⟩
State after:
case neg.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a : M
ha : Pow2 a
ea : ¬a = 1
b' : M
hb : Pow2 (a / 2 * b')
h : a < 2 * (a / 2 * b')
⊢ a ∣ a / 2 * b'

State before:
case neg.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a : M
ha : Pow2 a
ea : ¬a = 1
b' : M
hb : Pow2 (a / 2 * b')
h : a < 2 * (a / 2 * b')
⊢ a ∣ a / 2 * b'
Tactic:
have hb' : Pow2 b' := by simp at hb; exact hb.2
State after:
case neg.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a : M
ha : Pow2 a
ea : ¬a = 1
b' : M
hb : Pow2 (a / 2 * b')
h : a < 2 * (a / 2 * b')
hb' : Pow2 b'
⊢ a ∣ a / 2 * b'

State before:
case neg.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a : M
ha : Pow2 a
ea : ¬a = 1
b' : M
hb : Pow2 (a / 2 * b')
h : a < 2 * (a / 2 * b')
hb' : Pow2 b'
⊢ a ∣ a / 2 * b'
Tactic:
have : 2 ∣ b' := hb'.two_dvd' (by rintro rfl; simp [ha.two_mul_div_two ea] at h)
State after:
case neg.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a : M
ha : Pow2 a
ea : ¬a = 1
b' : M
hb : Pow2 (a / 2 * b')
h : a < 2 * (a / 2 * b')
hb' : Pow2 b'
this : 2 ∣ b'
⊢ a ∣ a / 2 * b'

State before:
case neg.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a : M
ha : Pow2 a
ea : ¬a = 1
b' : M
hb : Pow2 (a / 2 * b')
h : a < 2 * (a / 2 * b')
hb' : Pow2 b'
this : 2 ∣ b'
⊢ a ∣ a / 2 * b'
Tactic:
rcases this with ⟨b'', rfl⟩
State after:
case neg.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a : M
ha : Pow2 a
ea : ¬a = 1
b'' : M
hb : Pow2 (a / 2 * (2 * b''))
h : a < 2 * (a / 2 * (2 * b''))
hb' : Pow2 (2 * b'')
⊢ a ∣ a / 2 * (2 * b'')

State before:
case neg.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a : M
ha : Pow2 a
ea : ¬a = 1
b'' : M
hb : Pow2 (a / 2 * (2 * b''))
h : a < 2 * (a / 2 * (2 * b''))
hb' : Pow2 (2 * b'')
⊢ a ∣ a / 2 * (2 * b'')
Tactic:
simp [←mul_assoc, ha.div_two_mul_two ea]
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 b : M
ha : Pow2 a
hb : Pow2 b
h : a < 2 * b
ea : ¬a = 1
⊢ a / 2 ∣ b
Tactic:
have : 2 * (a / 2) ∣ 2 * b := by
  simpa [ha.two_mul_div_two ea] using dvd_of_le ha (by simpa using hb) (LT.lt.le h)
State after:
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
h : a < 2 * b
ea : ¬a = 1
this : 2 * (a / 2) ∣ 2 * b
⊢ a / 2 ∣ b

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
h : a < 2 * b
ea : ¬a = 1
this : 2 * (a / 2) ∣ 2 * b
⊢ a / 2 ∣ b
Tactic:
exact (mul_dvd_mul_iff_left (by simp)).mp 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 ⊧ₘ* 𝐈𝚫₀
a b : M
ha : Pow2 a
hb : Pow2 b
h : a < 2 * b
ea : ¬a = 1
⊢ 2 * (a / 2) ∣ 2 * b
Tactic:
simpa [ha.two_mul_div_two ea] using dvd_of_le ha (by simpa using hb) (LT.lt.le h)
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 b : M
ha : Pow2 a
hb : Pow2 b
h : a < 2 * b
ea : ¬a = 1
⊢ Pow2 (2 * b)
Tactic:
simpa using hb
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 b : M
ha : Pow2 a
hb : Pow2 b
h : a < 2 * b
ea : ¬a = 1
this : 2 * (a / 2) ∣ 2 * b
⊢ 2 ≠ 0
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 ⊧ₘ* 𝐈𝚫₀
a : M
ha : Pow2 a
ea : ¬a = 1
b' : M
hb : Pow2 (a / 2 * b')
h : a < 2 * (a / 2 * b')
⊢ Pow2 b'
Tactic:
simp at hb
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a : M
ha : Pow2 a
ea : ¬a = 1
b' : M
h : a < 2 * (a / 2 * b')
hb : Pow2 (a / 2) ∧ Pow2 b'
⊢ Pow2 b'

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a : M
ha : Pow2 a
ea : ¬a = 1
b' : M
h : a < 2 * (a / 2 * b')
hb : Pow2 (a / 2) ∧ Pow2 b'
⊢ Pow2 b'
Tactic:
exact hb.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 ⊧ₘ* 𝐈𝚫₀
a : M
ha : Pow2 a
ea : ¬a = 1
b' : M
hb : Pow2 (a / 2 * b')
h : a < 2 * (a / 2 * b')
hb' : Pow2 b'
⊢ b' ≠ 1
Tactic:
rintro rfl
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a : M
ha : Pow2 a
ea : ¬a = 1
hb : Pow2 (a / 2 * 1)
h : a < 2 * (a / 2 * 1)
hb' : Pow2 1
⊢ False

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a : M
ha : Pow2 a
ea : ¬a = 1
hb : Pow2 (a / 2 * 1)
h : a < 2 * (a / 2 * 1)
hb' : Pow2 1
⊢ False
Tactic:
simp [ha.two_mul_div_two ea] at h
State after:
no goals