-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem pow_dvd_pow_iff_pow_le_pow {k l : Nat} :
    ∀ {x : Nat}, 0 < x → (x ^ k ∣ x ^ l ↔ x ^ k ≤ x ^ l)
  | x + 1, w => by
    constructor
    · intro a
      exact le_of_dvd (Nat.pow_pos (succ_pos x)) a
    · intro a
      cases x
      case zero => simp
      case succ x =>
        have le :=
          (Nat.pow_le_pow_iff_right (Nat.succ_le_succ (Nat.succ_le_succ (Nat.zero_le _)))).mp a
        refine ⟨(x + 2) ^ (l - k), ?_⟩
        rw [← Nat.pow_add, Nat.add_comm k, Nat.sub_add_cancel le]

Proof state:
k l x : Nat
w : 0 < x + 1 + 1
a : (x + 1 + 1) ^ k ≤ (x + 1 + 1) ^ l
le : k ≤ l
⊢ (x + 1 + 1) ^ l = (x + 1 + 1) ^ k * (x + 2) ^ (l - k)

Tactic:
rw [← Nat.pow_add, Nat.add_comm k, Nat.sub_add_cancel le]

Result:
no goals

Proof state:
case mp
k l x : Nat
w : 0 < x + 1
⊢ (x + 1) ^ k ∣ (x + 1) ^ l → (x + 1) ^ k ≤ (x + 1) ^ l

Tactic:
intro a

Result:
case mp
k l x : Nat
w : 0 < x + 1
a : (x + 1) ^ k ∣ (x + 1) ^ l
⊢ (x + 1) ^ k ≤ (x + 1) ^ l

Proof state:
case mpr.succ
k l n✝ : Nat
w : 0 < n✝ + 1 + 1
a : (n✝ + 1 + 1) ^ k ≤ (n✝ + 1 + 1) ^ l
⊢ (n✝ + 1 + 1) ^ k ∣ (n✝ + 1 + 1) ^ l

Tactic:
case succ x =>
  have le :=
    (Nat.pow_le_pow_iff_right (Nat.succ_le_succ (Nat.succ_le_succ (Nat.zero_le _)))).mp a
  refine ⟨(x + 2) ^ (l - k), ?_⟩
  rw [← Nat.pow_add, Nat.add_comm k, Nat.sub_add_cancel le]

Result:
no goals

Proof state:
k l x : Nat
w : 0 < x + 1 + 1
a : (x + 1 + 1) ^ k ≤ (x + 1 + 1) ^ l
le : k ≤ l
⊢ (x + 1 + 1) ^ k ∣ (x + 1 + 1) ^ l

Tactic:
refine ⟨(x + 2) ^ (l - k), ?_⟩

Result:
k l x : Nat
w : 0 < x + 1 + 1
a : (x + 1 + 1) ^ k ≤ (x + 1 + 1) ^ l
le : k ≤ l
⊢ (x + 1 + 1) ^ l = (x + 1 + 1) ^ k * (x + 2) ^ (l - k)

Proof state:
case mp
k l x : Nat
w : 0 < x + 1
a : (x + 1) ^ k ∣ (x + 1) ^ l
⊢ (x + 1) ^ k ≤ (x + 1) ^ l

Tactic:
exact le_of_dvd (Nat.pow_pos (succ_pos x)) a

Result:
no goals

Proof state:
k l x : Nat
w : 0 < x + 1
⊢ (x + 1) ^ k ∣ (x + 1) ^ l ↔ (x + 1) ^ k ≤ (x + 1) ^ l

Tactic:
constructor

Result:
case mp
k l x : Nat
w : 0 < x + 1
⊢ (x + 1) ^ k ∣ (x + 1) ^ l → (x + 1) ^ k ≤ (x + 1) ^ l

case mpr
k l x : Nat
w : 0 < x + 1
⊢ (x + 1) ^ k ≤ (x + 1) ^ l → (x + 1) ^ k ∣ (x + 1) ^ l

Proof state:
k l : Nat
w : 0 < 0 + 1
a : (0 + 1) ^ k ≤ (0 + 1) ^ l
⊢ (0 + 1) ^ k ∣ (0 + 1) ^ l

Tactic:
simp

Result:
no goals

Proof state:
case mpr
k l x : Nat
w : 0 < x + 1
⊢ (x + 1) ^ k ≤ (x + 1) ^ l → (x + 1) ^ k ∣ (x + 1) ^ l

Tactic:
intro a

Result:
case mpr
k l x : Nat
w : 0 < x + 1
a : (x + 1) ^ k ≤ (x + 1) ^ l
⊢ (x + 1) ^ k ∣ (x + 1) ^ l

Proof state:
case mpr.zero
k l : Nat
w : 0 < 0 + 1
a : (0 + 1) ^ k ≤ (0 + 1) ^ l
⊢ (0 + 1) ^ k ∣ (0 + 1) ^ l

case mpr.succ
k l n✝ : Nat
w : 0 < n✝ + 1 + 1
a : (n✝ + 1 + 1) ^ k ≤ (n✝ + 1 + 1) ^ l
⊢ (n✝ + 1 + 1) ^ k ∣ (n✝ + 1 + 1) ^ l

Tactic:
case zero => simp

Result:
case mpr.succ
k l n✝ : Nat
w : 0 < n✝ + 1 + 1
a : (n✝ + 1 + 1) ^ k ≤ (n✝ + 1 + 1) ^ l
⊢ (n✝ + 1 + 1) ^ k ∣ (n✝ + 1 + 1) ^ l

Proof state:
k l x : Nat
w : 0 < x + 1 + 1
a : (x + 1 + 1) ^ k ≤ (x + 1 + 1) ^ l
⊢ (x + 1 + 1) ^ k ∣ (x + 1 + 1) ^ l

Tactic:
have le :=
  (Nat.pow_le_pow_iff_right (Nat.succ_le_succ (Nat.succ_le_succ (Nat.zero_le _)))).mp a

Result:
k l x : Nat
w : 0 < x + 1 + 1
a : (x + 1 + 1) ^ k ≤ (x + 1 + 1) ^ l
le : k ≤ l
⊢ (x + 1 + 1) ^ k ∣ (x + 1 + 1) ^ l

Proof state:
case mpr
k l x : Nat
w : 0 < x + 1
a : (x + 1) ^ k ≤ (x + 1) ^ l
⊢ (x + 1) ^ k ∣ (x + 1) ^ l

Tactic:
cases x

Result:
case mpr.zero
k l : Nat
w : 0 < 0 + 1
a : (0 + 1) ^ k ≤ (0 + 1) ^ l
⊢ (0 + 1) ^ k ∣ (0 + 1) ^ l

case mpr.succ
k l n✝ : Nat
w : 0 < n✝ + 1 + 1
a : (n✝ + 1 + 1) ^ k ≤ (n✝ + 1 + 1) ^ l
⊢ (n✝ + 1 + 1) ^ k ∣ (n✝ + 1 + 1) ^ l