-- Mathlib/Algebra/GroupWithZero/Divisibility.lean
lemma pow_dvd_pow_iff (ha₀ : a ≠ 0) (ha : ¬IsUnit a) : a ^ n ∣ a ^ m ↔ n ≤ m

Proof state:
case mp
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
h : a ^ n ∣ a ^ m
hmn : m < n
⊢ IsUnit a

Tactic:
have : a ^ m * a ∣ a ^ m * 1 := by
  rw [← pow_succ, mul_one]
  exact (pow_dvd_pow _ (Nat.succ_le_of_lt hmn)).trans h

Result:
case mp
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
h : a ^ n ∣ a ^ m
hmn : m < n
this : a ^ m * a ∣ a ^ m * 1
⊢ IsUnit a

Proof state:
case mpr
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
⊢ n ≤ m → a ^ n ∣ a ^ m

Tactic:
apply pow_dvd_pow

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
h : a ^ n ∣ a ^ m
hmn : m < n
⊢ a ^ (m + 1) ∣ a ^ m

Tactic:
exact (pow_dvd_pow _ (Nat.succ_le_of_lt hmn)).trans h

Result:
no goals

Proof state:
case mp
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
h : a ^ n ∣ a ^ m
hmn : m < n
this : a ^ m * a ∣ a ^ m * 1
⊢ IsUnit a

Tactic:
rwa [mul_dvd_mul_iff_left, ← isUnit_iff_dvd_one] at this

Result:
case mp
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
h : a ^ n ∣ a ^ m
hmn : m < n
this : a ^ m * a ∣ a ^ m * 1
⊢ a ^ m ≠ 0

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
⊢ a ^ n ∣ a ^ m ↔ n ≤ m

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
⊢ a ^ n ∣ a ^ m → n ≤ m

case mpr
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
⊢ n ≤ m → a ^ n ∣ a ^ m

Proof state:
case mp
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
⊢ a ^ n ∣ a ^ m → n ≤ m

Tactic:
intro h

Result:
case mp
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
h : a ^ n ∣ a ^ m
⊢ n ≤ m

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
h : a ^ n ∣ a ^ m
hmn : m < n
⊢ a ^ m * a ∣ a ^ m * 1

Tactic:
rw [← pow_succ, mul_one]

Result:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
h : a ^ n ∣ a ^ m
hmn : m < n
⊢ a ^ (m + 1) ∣ a ^ m

Proof state:
case mp
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
h : a ^ n ∣ a ^ m
⊢ ¬m < n

Tactic:
intro hmn

Result:
case mp
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
h : a ^ n ∣ a ^ m
hmn : m < n
⊢ False

Proof state:
case mp
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
h : a ^ n ∣ a ^ m
hmn : m < n
this : a ^ m * a ∣ a ^ m * 1
⊢ a ^ m ≠ 0

Tactic:
apply pow_ne_zero m ha₀

Result:
no goals

Proof state:
case mp
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
h : a ^ n ∣ a ^ m
hmn : m < n
⊢ False

Tactic:
apply ha

Result:
case mp
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
h : a ^ n ∣ a ^ m
hmn : m < n
⊢ IsUnit a

Proof state:
case mp
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
h : a ^ n ∣ a ^ m
⊢ n ≤ m

Tactic:
rw [← not_lt]

Result:
case mp
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
h : a ^ n ∣ a ^ m
⊢ ¬m < n