-- Mathlib/Algebra/GroupWithZero/Associated.lean
@[simp]
lemma prime_pow_iff [CancelCommMonoidWithZero M] {p : M} {n : ℕ} :
    Prime (p ^ n) ↔ Prime p ∧ n = 1

Proof state:
case succ.inr.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
n : ℕ
hp : IsUnit p
hpn : Prime (p ^ n)
⊢ False

Tactic:
exact hpn.not_unit (hp.pow n)

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
n : ℕ
⊢ Prime (p ^ n) ↔ Prime p ∧ n = 1

Tactic:
refine ⟨fun hp ↦ ?_, fun ⟨hp, hn⟩ ↦ by simpa [hn]⟩

Result:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
n : ℕ
hp : Prime (p ^ n)
⊢ Prime p ∧ n = 1

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
n : ℕ
hp : Prime (p ^ n)
⊢ Prime p ∧ n = 1

Tactic:
suffices n = 1 by aesop

Result:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
n : ℕ
hp : Prime (p ^ n)
⊢ n = 1

Proof state:
case succ.inl.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
n : ℕ
hp : Prime p
hpn : IsUnit (p ^ n)
⊢ n = 0

Tactic:
by_contra contra

Result:
case succ.inl.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
n : ℕ
hp : Prime p
hpn : IsUnit (p ^ n)
contra : ¬n = 0
⊢ False

Proof state:
case zero
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
hp : Prime (p ^ 0)
⊢ 0 = 1

Tactic:
simp at hp

Result:
no goals

Proof state:
case succ.inl.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
n : ℕ
hp : Prime p
hpn : IsUnit (p ^ n)
contra : ¬n = 0
⊢ False

Tactic:
rw [isUnit_pow_iff contra] at hpn

Result:
case succ.inl.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
n : ℕ
hp : Prime p
hpn : IsUnit p
contra : ¬n = 0
⊢ False

Proof state:
case succ
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
n : ℕ
hp : Prime (p ^ (n + 1))
⊢ n + 1 = 1

Tactic:
rw [Nat.succ.injEq]

Result:
case succ
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
n : ℕ
hp : Prime (p ^ (n + 1))
⊢ n = 0

Proof state:
case succ
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
n : ℕ
hp : Prime p ∧ IsUnit (p ^ n) ∨ IsUnit p ∧ Prime (p ^ n)
⊢ n = 0

Tactic:
rcases hp with ⟨hp, hpn⟩ | ⟨hp, hpn⟩

Result:
case succ.inl.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
n : ℕ
hp : Prime p
hpn : IsUnit (p ^ n)
⊢ n = 0

case succ.inr.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
n : ℕ
hp : IsUnit p
hpn : Prime (p ^ n)
⊢ n = 0

Proof state:
case succ.inl.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
n : ℕ
hp : Prime p
hpn : IsUnit p
contra : ¬n = 0
⊢ False

Tactic:
exact hp.not_unit hpn

Result:
no goals

Proof state:
case succ.inr.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
n : ℕ
hp : IsUnit p
hpn : Prime (p ^ n)
⊢ n = 0

Tactic:
exfalso

Result:
case succ.inr.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
n : ℕ
hp : IsUnit p
hpn : Prime (p ^ n)
⊢ False

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
n : ℕ
x✝ : Prime p ∧ n = 1
hp : Prime p
hn : n = 1
⊢ Prime (p ^ n)

Tactic:
simpa [hn]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
n : ℕ
hp : Prime (p ^ n)
⊢ n = 1

Tactic:
rcases n with - | n

Result:
case zero
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
hp : Prime (p ^ 0)
⊢ 0 = 1

case succ
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
n : ℕ
hp : Prime (p ^ (n + 1))
⊢ n + 1 = 1

Proof state:
case succ
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
n : ℕ
hp : Prime (p ^ (n + 1))
⊢ n = 0

Tactic:
rw [pow_succ', prime_mul_iff] at hp

Result:
case succ
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
n : ℕ
hp : Prime p ∧ IsUnit (p ^ n) ∨ IsUnit p ∧ Prime (p ^ n)
⊢ n = 0

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
n : ℕ
hp : Prime (p ^ n)
this : n = 1
⊢ Prime p ∧ n = 1

Tactic:
aesop

Result:
no goals