α : Type ?u.1007137
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq R
a b : R
n : ℕ
ha : Irreducible a
hb : b ≠ 0
⊢ a ^ n ∣ b ↔ replicate n (↑normalize a) ≤ normalizedFactors b
α : Type ?u.1007137
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq R
a b : R
n : ℕ
ha : Irreducible a
hb : b ≠ 0
⊢ ↑n ≤ multiplicity a b ↔ replicate n (↑normalize a) ≤ normalizedFactors b
rw [← pow_dvd_iff_le_multiplicity]
α : Type ?u.1007137
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq R
a : R
n : ℕ
ha : Irreducible a
⊢ ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (↑normalize a) ≤ normalizedFactors b)
α : Type ?u.1007137
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq R
a b : R
n : ℕ
ha : Irreducible a
hb : b ≠ 0
⊢ a ^ n ∣ b ↔ replicate n (↑normalize a) ≤ normalizedFactors b
revert b
case zero
α : Type ?u.1007137
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq R
a : R
ha : Irreducible a
⊢ ∀ {b : R}, b ≠ 0 → (a ^ Nat.zero ∣ b ↔ replicate Nat.zero (↑normalize a) ≤ normalizedFactors b)

case succ
α : Type ?u.1007137
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq 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 ^ Nat.succ n ∣ b ↔ replicate (Nat.succ n) (↑normalize a) ≤ normalizedFactors b)
α : Type ?u.1007137
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq R
a : R
n : ℕ
ha : Irreducible a
⊢ ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (↑normalize a) ≤ normalizedFactors b)
induction' n with n ih
case succ
α : Type ?u.1007137
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq 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 ^ Nat.succ n ∣ b ↔ replicate (Nat.succ n) (↑normalize a) ≤ normalizedFactors b
case succ
α : Type ?u.1007137
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq 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 ^ Nat.succ n ∣ b ↔ replicate (Nat.succ n) (↑normalize a) ≤ normalizedFactors b)
intro b hb
case succ.mp
α : Type ?u.1007137
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq 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 ^ Nat.succ n ∣ b → replicate (Nat.succ n) (↑normalize a) ≤ normalizedFactors b

case succ.mpr
α : Type ?u.1007137
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq 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 (Nat.succ n) (↑normalize a) ≤ normalizedFactors b → a ^ Nat.succ n ∣ b
case succ
α : Type ?u.1007137
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq 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 ^ Nat.succ n ∣ b ↔ replicate (Nat.succ n) (↑normalize a) ≤ normalizedFactors b
constructor
no goals
case zero
α : Type ?u.1007137
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq R
a : R
ha : Irreducible a
⊢ ∀ {b : R}, b ≠ 0 → (a ^ Nat.zero ∣ b ↔ replicate Nat.zero (↑normalize a) ≤ normalizedFactors b)
simp
case succ.mp.intro
α : Type ?u.1007137
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq 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 ^ Nat.succ n * c ≠ 0
⊢ replicate (Nat.succ n) (↑normalize a) ≤ normalizedFactors (a ^ Nat.succ n * c)
case succ.mp
α : Type ?u.1007137
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq 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 ^ Nat.succ n ∣ b → replicate (Nat.succ n) (↑normalize a) ≤ normalizedFactors b
rintro ⟨c, rfl⟩
case succ.mp.intro
α : Type ?u.1007137
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq 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 (Nat.succ n) (↑normalize a) ≤ normalizedFactors (a ^ Nat.succ n * c)
case succ.mp.intro
α : Type ?u.1007137
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq 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 ^ Nat.succ n * c ≠ 0
⊢ replicate (Nat.succ n) (↑normalize a) ≤ normalizedFactors (a ^ Nat.succ n * c)
rw [Ne.def, pow_succ, mul_assoc, mul_eq_zero, not_or] at hb
case succ.mp.intro
α : Type ?u.1007137
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq 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
case succ.mp.intro
α : Type ?u.1007137
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq 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 (Nat.succ n) (↑normalize a) ≤ normalizedFactors (a ^ Nat.succ n * c)
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]
no goals
case succ.mp.intro
α : Type ?u.1007137
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq 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
apply Dvd.intro _ rfl
case succ.mpr
α : Type ?u.1007137
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq 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 (Nat.succ n) (↑normalize a) + u) → a ^ Nat.succ n ∣ b
case succ.mpr
α : Type ?u.1007137
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq 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 (Nat.succ n) (↑normalize a) ≤ normalizedFactors b → a ^ Nat.succ n ∣ b
rw [Multiset.le_iff_exists_add]
case succ.mpr.intro
α : Type ?u.1007137
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq 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 ((fun x => R) a)
hu : normalizedFactors b = replicate (Nat.succ n) (↑normalize a) + u
⊢ a ^ Nat.succ n ∣ b
case succ.mpr
α : Type ?u.1007137
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq 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 (Nat.succ n) (↑normalize a) + u) → a ^ Nat.succ n ∣ b
rintro ⟨u, hu⟩
case succ.mpr.intro
α : Type ?u.1007137
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq 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 ((fun x => R) a)
hu : normalizedFactors b = replicate (Nat.succ n) (↑normalize a) + u
⊢ a ^ Nat.succ n ∣ ↑normalize a ^ Nat.succ n * prod u
case succ.mpr.intro
α : Type ?u.1007137
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq 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 ((fun x => R) a)
hu : normalizedFactors b = replicate (Nat.succ n) (↑normalize a) + u
⊢ a ^ Nat.succ n ∣ b
rw [← (normalizedFactors_prod hb).dvd_iff_dvd_right, hu, prod_add, prod_replicate]
no goals
case succ.mpr.intro
α : Type ?u.1007137
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq 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 ((fun x => R) a)
hu : normalizedFactors b = replicate (Nat.succ n) (↑normalize a) + u
⊢ a ^ Nat.succ n ∣ ↑normalize a ^ Nat.succ n * prod u
exact (Associated.pow_pow <| associated_normalize a).dvd.trans (Dvd.intro u.prod rfl)