Theorem: LO.FirstOrder.Arith.Model.eq_one_or_eq_of_dvd_of_prime (Arithmetization/Basic/PeanoMinus.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 c p a : M
pp : Prime p
hxp : a ∣ p
⊢ a = 1 ∨ a = p
Tactic:
have : p ∣ a ∨ a ∣ 1 := pp.left_dvd_or_dvd_right_of_dvd_mul (show a ∣ p * 1 from by simpa using hxp)
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 c p a : M
pp : Prime p
hxp : a ∣ p
this : p ∣ a ∨ a ∣ 1
⊢ a = 1 ∨ a = p

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 c p a : M
pp : Prime p
hxp : a ∣ p
this : p ∣ a ∨ a ∣ 1
⊢ a = 1 ∨ a = p
Tactic:
rcases this with (hx | hx)
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✝ b c p a : M
pp : Prime p
hxp : a ∣ p
hx : p ∣ a
⊢ a = 1 ∨ a = p

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ b c p a : M
pp : Prime p
hxp : a ∣ p
hx : a ∣ 1
⊢ a = 1 ∨ a = p

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 c p a : M
pp : Prime p
hxp : a ∣ p
⊢ a ∣ p * 1
Tactic:
simpa using hxp
State after:
no goals

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✝ b c p a : M
pp : Prime p
hxp : a ∣ p
hx : p ∣ a
⊢ a = 1 ∨ a = p
Tactic:
right
State after:
case inl.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ b c p a : M
pp : Prime p
hxp : a ∣ p
hx : p ∣ a
⊢ a = p

State before:
case inl.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ b c p a : M
pp : Prime p
hxp : a ∣ p
hx : p ∣ a
⊢ a = p
Tactic:
exact dvd_antisymm hxp hx
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 ⊧ₘ* 𝐏𝐀⁻
a✝ b c p a : M
pp : Prime p
hxp : a ∣ p
hx : a ∣ 1
⊢ a = 1 ∨ a = p
Tactic:
left
State after:
case inr.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ b c p a : M
pp : Prime p
hxp : a ∣ p
hx : a ∣ 1
⊢ a = 1

State before:
case inr.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ b c p a : M
pp : Prime p
hxp : a ∣ p
hx : a ∣ 1
⊢ a = 1
Tactic:
exact dvd_one_iff.mp hx
State after:
no goals