-- Mathlib/RingTheory/UniqueFactorizationDomain/Multiplicity.lean
theorem le_emultiplicity_iff_replicate_le_normalizedFactors {a b : R} {n : ℕ} (ha : Irreducible a)
    (hb : b ≠ 0) :
    ↑n ≤ emultiplicity a b ↔ replicate n (normalize a) ≤ normalizedFactors b

Proof state:
case succ.mpr
R : Type u_2
inst✝² : CancelCommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
b : R
hb : b ≠ 0
⊢ replicate (n + 1) (normalize a) ≤ normalizedFactors b → a ^ (n + 1) ∣ b

Tactic:
rw [Multiset.le_iff_exists_add]

Result:
case succ.mpr
R : Type u_2
inst✝² : CancelCommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
b : R
hb : b ≠ 0
⊢ (∃ u, normalizedFactors b = replicate (n + 1) (normalize a) + u) → a ^ (n + 1) ∣ b

Proof state:
case zero
R : Type u_2
inst✝² : CancelCommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
⊢ ∀ {b : R}, b ≠ 0 → (a ^ 0 ∣ b ↔ replicate 0 (normalize a) ≤ normalizedFactors b)

Tactic:
simp

Result:
no goals

Proof state:
case succ
R : Type u_2
inst✝² : CancelCommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
b : R
hb : b ≠ 0
⊢ a ^ (n + 1) ∣ b ↔ replicate (n + 1) (normalize a) ≤ normalizedFactors b

Tactic:
constructor

Result:
case succ.mp
R : Type u_2
inst✝² : CancelCommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
b : R
hb : b ≠ 0
⊢ a ^ (n + 1) ∣ b → replicate (n + 1) (normalize a) ≤ normalizedFactors b

case succ.mpr
R : Type u_2
inst✝² : CancelCommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
b : R
hb : b ≠ 0
⊢ replicate (n + 1) (normalize a) ≤ normalizedFactors b → a ^ (n + 1) ∣ b

Proof state:
case succ.mp
R : Type u_2
inst✝² : CancelCommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
b : R
hb : b ≠ 0
⊢ a ^ (n + 1) ∣ b → replicate (n + 1) (normalize a) ≤ normalizedFactors b

Tactic:
rintro ⟨c, rfl⟩

Result:
case succ.mp.intro
R : Type u_2
inst✝² : CancelCommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
c : R
hb : a ^ (n + 1) * c ≠ 0
⊢ replicate (n + 1) (normalize a) ≤ normalizedFactors (a ^ (n + 1) * c)

Proof state:
case succ.mp.intro
R : Type u_2
inst✝² : CancelCommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
c : R
hb : a ^ (n + 1) * c ≠ 0
⊢ replicate (n + 1) (normalize a) ≤ normalizedFactors (a ^ (n + 1) * c)

Tactic:
rw [Ne, pow_succ', mul_assoc, mul_eq_zero, not_or] at hb

Result:
case succ.mp.intro
R : Type u_2
inst✝² : CancelCommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
c : R
hb : ¬a = 0 ∧ ¬a ^ n * c = 0
⊢ replicate (n + 1) (normalize a) ≤ normalizedFactors (a ^ (n + 1) * c)

Proof state:
case succ.mp.intro
R : Type u_2
inst✝² : CancelCommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
c : R
hb : ¬a = 0 ∧ ¬a ^ n * c = 0
⊢ replicate (n + 1) (normalize a) ≤ normalizedFactors (a ^ (n + 1) * c)

Tactic:
rw [pow_succ', mul_assoc, normalizedFactors_mul hb.1 hb.2, replicate_succ,
  normalizedFactors_irreducible ha, singleton_add, cons_le_cons_iff, ← ih hb.2]

Result:
case succ.mp.intro
R : Type u_2
inst✝² : CancelCommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
c : R
hb : ¬a = 0 ∧ ¬a ^ n * c = 0
⊢ a ^ n ∣ a ^ n * c

Proof state:
case succ.mp.intro
R : Type u_2
inst✝² : CancelCommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
c : R
hb : ¬a = 0 ∧ ¬a ^ n * c = 0
⊢ a ^ n ∣ a ^ n * c

Tactic:
apply Dvd.intro _ rfl

Result:
no goals

Proof state:
case succ.mpr.intro
R : Type u_2
inst✝² : CancelCommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
b : R
hb : b ≠ 0
u : Multiset R
hu : normalizedFactors b = replicate (n + 1) (normalize a) + u
⊢ a ^ (n + 1) ∣ normalize a ^ (n + 1) * u.prod

Tactic:
exact (Associated.pow_pow <| associated_normalize a).dvd.trans (Dvd.intro u.prod rfl)

Result:
no goals

Proof state:
R : Type u_2
inst✝² : CancelCommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a b : R
n : ℕ
ha : Irreducible a
hb : b ≠ 0
⊢ a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b

Tactic:
revert b

Result:
R : Type u_2
inst✝² : CancelCommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
n : ℕ
ha : Irreducible a
⊢ ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)

Proof state:
R : Type u_2
inst✝² : CancelCommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a b : R
n : ℕ
ha : Irreducible a
hb : b ≠ 0
⊢ ↑n ≤ emultiplicity a b ↔ replicate n (normalize a) ≤ normalizedFactors b

Tactic:
rw [← pow_dvd_iff_le_emultiplicity]

Result:
R : Type u_2
inst✝² : CancelCommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a b : R
n : ℕ
ha : Irreducible a
hb : b ≠ 0
⊢ a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b

Proof state:
case succ
R : Type u_2
inst✝² : CancelCommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
⊢ ∀ {b : R}, b ≠ 0 → (a ^ (n + 1) ∣ b ↔ replicate (n + 1) (normalize a) ≤ normalizedFactors b)

Tactic:
intro b hb

Result:
case succ
R : Type u_2
inst✝² : CancelCommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
b : R
hb : b ≠ 0
⊢ a ^ (n + 1) ∣ b ↔ replicate (n + 1) (normalize a) ≤ normalizedFactors b