Theorem: LO.FirstOrder.Arith.Model.pow2_one (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
⊢ 0 < 1
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
⊢ ∀ r ≤ 1, 1 < r → r ∣ 1 → 2 ∣ r
Tactic:
intro r hr hhr 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
r : M
hr : r ≤ 1
hhr : 1 < r
hd : r ∣ 1
⊢ 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
r : M
hr : r ≤ 1
hhr : 1 < r
hd : r ∣ 1
⊢ 2 ∣ r
Tactic:
rcases show r = 0 ∨ r = 1 from le_one_iff_eq_zero_or_one.mp hr with (rfl | rfl)
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
hr : 0 ≤ 1
hhr : 1 < 0
hd : 0 ∣ 1
⊢ 2 ∣ 0

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

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
hr : 0 ≤ 1
hhr : 1 < 0
hd : 0 ∣ 1
⊢ 2 ∣ 0
Tactic:
simp
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
hr : 1 ≤ 1
hhr : 1 < 1
hd : 1 ∣ 1
⊢ 2 ∣ 1
Tactic:
simp at hhr
State after:
no goals