-- Mathlib/RingTheory/Multiplicity.lean
theorem finiteMultiplicity_mul_aux {p : α} (hp : Prime p) {a b : α} :
    ∀ {n m : ℕ}, ¬p ^ (n + 1) ∣ a → ¬p ^ (m + 1) ∣ b → ¬p ^ (n + m + 1) ∣ a * b
  | n, m => fun ha hb ⟨s, hs⟩ =>
    have : p ∣ a * b := ⟨p ^ (n + m) * s, by simp [hs, pow_add, mul_comm, mul_assoc, mul_left_comm]⟩
    (hp.2.2 a b this).elim
      (fun ⟨x, hx⟩ =>
        have hn0 : 0 < n :=
          Nat.pos_of_ne_zero fun hn0 => by simp [hx, hn0] at ha
        have hpx : ¬p ^ (n - 1 + 1) ∣ x := fun ⟨y, hy⟩ =>
          ha (hx.symm ▸ ⟨y, mul_right_cancel₀ hp.1 <| by
            rw [tsub_add_cancel_of_le (succ_le_of_lt hn0)] at hy
            simp [hy, pow_add, mul_comm, mul_assoc, mul_left_comm]⟩)
        have : 1 ≤ n + m := le_trans hn0 (Nat.le_add_right n m)
        finiteMultiplicity_mul_aux hp hpx hb
          ⟨s, mul_right_cancel₀ hp.1 (by
                rw [tsub_add_eq_add_tsub (succ_le_of_lt hn0), tsub_add_cancel_of_le this]
                simp_all [mul_comm, mul_assoc, mul_left_comm, pow_add])⟩)
      fun ⟨x, hx⟩ =>
        have hm0 : 0 < m :=
          Nat.pos_of_ne_zero fun hm0 => by simp [hx, hm0] at hb
        have hpx : ¬p ^ (m - 1 + 1) ∣ x := fun ⟨y, hy⟩ =>
          hb
            (hx.symm ▸
              ⟨y,
                mul_right_cancel₀ hp.1 <| by
                  rw [tsub_add_cancel_of_le (succ_le_of_lt hm0)] at hy
                  simp [hy, pow_add, mul_comm, mul_assoc, mul_left_comm]⟩)
        finiteMultiplicity_mul_aux hp ha hpx
        ⟨s, mul_right_cancel₀ hp.1 (by
              rw [add_assoc, tsub_add_cancel_of_le (succ_le_of_lt hm0)]
              simp_all [mul_comm, mul_assoc, mul_left_comm, pow_add])⟩

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝¹ : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
x✝ : p ∣ b
x : α
hx : b = p * x
hm0 : m = 0
⊢ False

Tactic:
simp [hx, hm0] at hb

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝¹ : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
x✝ : p ∣ b
x : α
hx : b = p * x
hm0 : 0 < m
hpx : ¬p ^ (m - 1 + 1) ∣ x
⊢ a * x * p = p ^ (n + (m - 1) + 1) * s * p

Tactic:
rw [add_assoc, tsub_add_cancel_of_le (succ_le_of_lt hm0)]

Result:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝¹ : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
x✝ : p ∣ b
x : α
hx : b = p * x
hm0 : 0 < m
hpx : ¬p ^ (m - 1 + 1) ∣ x
⊢ a * x * p = p ^ (n + m) * s * p

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝² : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
x✝¹ : p ∣ b
x : α
hx : b = p * x
hm0 : 0 < m
x✝ : p ^ (m - 1 + 1) ∣ x
y : α
hy : x = p ^ m * y
⊢ p * x * p = p ^ (m + 1) * y * p

Tactic:
simp [hy, pow_add, mul_comm, mul_assoc, mul_left_comm]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝ : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
⊢ a * b = p * (p ^ (n + m) * s)

Tactic:
simp [hs, pow_add, mul_comm, mul_assoc, mul_left_comm]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝² : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
x✝¹ : p ∣ a
x : α
hx : a = p * x
hn0 : 0 < n
x✝ : p ^ (n - 1 + 1) ∣ x
y : α
hy : x = p ^ n * y
⊢ p * x * p = p ^ (n + 1) * y * p

Tactic:
simp [hy, pow_add, mul_comm, mul_assoc, mul_left_comm]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝² : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
x✝¹ : p ∣ b
x : α
hx : b = p * x
hm0 : 0 < m
x✝ : p ^ (m - 1 + 1) ∣ x
y : α
hy : x = p ^ (m - 1 + 1) * y
⊢ p * x * p = p ^ (m + 1) * y * p

Tactic:
rw [tsub_add_cancel_of_le (succ_le_of_lt hm0)] at hy

Result:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝² : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
x✝¹ : p ∣ b
x : α
hx : b = p * x
hm0 : 0 < m
x✝ : p ^ (m - 1 + 1) ∣ x
y : α
hy : x = p ^ m * y
⊢ p * x * p = p ^ (m + 1) * y * p

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝² : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
x✝¹ : p ∣ a
x : α
hx : a = p * x
hn0 : 0 < n
x✝ : p ^ (n - 1 + 1) ∣ x
y : α
hy : x = p ^ (n - 1 + 1) * y
⊢ p * x * p = p ^ (n + 1) * y * p

Tactic:
rw [tsub_add_cancel_of_le (succ_le_of_lt hn0)] at hy

Result:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝² : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
x✝¹ : p ∣ a
x : α
hx : a = p * x
hn0 : 0 < n
x✝ : p ^ (n - 1 + 1) ∣ x
y : α
hy : x = p ^ n * y
⊢ p * x * p = p ^ (n + 1) * y * p

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝¹ : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
x✝ : p ∣ b
x : α
hx : b = p * x
hm0 : 0 < m
hpx : ¬p ^ (m - 1 + 1) ∣ x
⊢ a * x * p = p ^ (n + m) * s * p

Tactic:
simp_all [mul_comm, mul_assoc, mul_left_comm, pow_add]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝¹ : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this✝ : p ∣ a * b
x✝ : p ∣ a
x : α
hx : a = p * x
hn0 : 0 < n
hpx : ¬p ^ (n - 1 + 1) ∣ x
this : 1 ≤ n + m
⊢ x * b * p = p ^ (n - 1 + m + 1) * s * p

Tactic:
rw [tsub_add_eq_add_tsub (succ_le_of_lt hn0), tsub_add_cancel_of_le this]

Result:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝¹ : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this✝ : p ∣ a * b
x✝ : p ∣ a
x : α
hx : a = p * x
hn0 : 0 < n
hpx : ¬p ^ (n - 1 + 1) ∣ x
this : 1 ≤ n + m
⊢ x * b * p = p ^ (n + m) * s * p

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝¹ : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
x✝ : p ∣ a
x : α
hx : a = p * x
hn0 : n = 0
⊢ False

Tactic:
simp [hx, hn0] at ha

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝¹ : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this✝ : p ∣ a * b
x✝ : p ∣ a
x : α
hx : a = p * x
hn0 : 0 < n
hpx : ¬p ^ (n - 1 + 1) ∣ x
this : 1 ≤ n + m
⊢ x * b * p = p ^ (n + m) * s * p

Tactic:
simp_all [mul_comm, mul_assoc, mul_left_comm, pow_add]

Result:
no goals