Theorem: LO.FirstOrder.Arith.Model.pow2_mul_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 ⊧ₘ* 𝐈open
a : M
⊢ Pow2 (2 * a) → Pow2 a
Tactic:
intro H
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
a : M
H : Pow2 (2 * a)
⊢ Pow2 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
a : M
H : Pow2 (2 * a)
⊢ Pow2 a
Tactic:
have : ∀ r ≤ a, 1 < r → r ∣ a → 2 ∣ r := by
  intro r hr ltr dvd
  exact H.dvd (show r ≤ 2 * a from le_trans hr (le_mul_of_one_le_left (by simp) one_le_two)) ltr (Dvd.dvd.mul_left dvd 2)
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
a : M
H : Pow2 (2 * a)
this : ∀ r ≤ a, 1 < r → r ∣ a → 2 ∣ r
⊢ Pow2 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
a : M
H : Pow2 (2 * a)
this : ∀ r ≤ a, 1 < r → r ∣ a → 2 ∣ r
⊢ Pow2 a
Tactic:
exact ⟨by simpa using H.pos, 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 ⊧ₘ* 𝐈open
a : M
H : Pow2 (2 * a)
⊢ ∀ r ≤ a, 1 < r → r ∣ a → 2 ∣ r
Tactic:
intro r hr ltr dvd
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
a : M
H : Pow2 (2 * a)
r : M
hr : r ≤ a
ltr : 1 < r
dvd : r ∣ a
⊢ 2 ∣ r

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
a : M
H : Pow2 (2 * a)
r : M
hr : r ≤ a
ltr : 1 < r
dvd : r ∣ a
⊢ 2 ∣ r
Tactic:
exact H.dvd (show r ≤ 2 * a from le_trans hr (le_mul_of_one_le_left (by simp) one_le_two)) ltr (Dvd.dvd.mul_left dvd 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 ⊧ₘ* 𝐈open
a : M
H : Pow2 (2 * a)
r : M
hr : r ≤ a
ltr : 1 < r
dvd : r ∣ a
⊢ 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
a : M
H : Pow2 (2 * a)
this : ∀ r ≤ a, 1 < r → r ∣ a → 2 ∣ r
⊢ 0 < a
Tactic:
simpa using H.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
a : M
⊢ Pow2 a → Pow2 (2 * a)
Tactic:
intro H
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
a : M
H : Pow2 a
⊢ Pow2 (2 * 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
a : M
H : Pow2 a
⊢ 0 < 2 * a
Tactic:
simpa using H.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
a : M
H : Pow2 a
⊢ ∀ r ≤ 2 * a, 1 < r → r ∣ 2 * a → 2 ∣ r
Tactic:
intro r _ hr hd
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
a : M
H : Pow2 a
r : M
a✝ : r ≤ 2 * a
hr : 1 < r
hd : r ∣ 2 * a
⊢ 2 ∣ r

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
a : M
H : Pow2 a
r : M
a✝ : r ≤ 2 * a
hr : 1 < r
hd : r ∣ 2 * a
⊢ 2 ∣ r
Tactic:
rcases two_prime.left_dvd_or_dvd_right_of_dvd_mul hd with (hd | hd)
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 : M
H : Pow2 a
r : M
a✝ : r ≤ 2 * a
hr : 1 < r
hd✝ : r ∣ 2 * a
hd : 2 ∣ r
⊢ 2 ∣ r

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
a : M
H : Pow2 a
r : M
a✝ : r ≤ 2 * a
hr : 1 < r
hd✝ : r ∣ 2 * a
hd : r ∣ a
⊢ 2 ∣ r

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 : M
H : Pow2 a
r : M
a✝ : r ≤ 2 * a
hr : 1 < r
hd✝ : r ∣ 2 * a
hd : 2 ∣ r
⊢ 2 ∣ r
Tactic:
exact hd
State after:
no goals

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
a : M
H : Pow2 a
r : M
a✝ : r ≤ 2 * a
hr : 1 < r
hd✝ : r ∣ 2 * a
hd : r ∣ a
⊢ 2 ∣ r
Tactic:
exact H.dvd (show r ≤ a from le_of_dvd H.pos hd) hr hd
State after:
no goals