no goals
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
x : α
n : ℕ
⊢ Multiset.Rel Associated (factors (x ^ 0)) (0 • factors x)
rw [zero_smul, pow_zero, factors_one, Multiset.rel_zero_right]
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
x : α
n✝ n : ℕ
h0 : x = 0
⊢ Multiset.Rel Associated (factors (x ^ (n + 1))) ((n + 1) • factors x)

case neg
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
x : α
n✝ n : ℕ
h0 : ¬x = 0
⊢ Multiset.Rel Associated (factors (x ^ (n + 1))) ((n + 1) • factors x)
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
x : α
n✝ n : ℕ
⊢ Multiset.Rel Associated (factors (x ^ (n + 1))) ((n + 1) • factors x)
by_cases h0 : x = 0
no goals
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
x : α
n✝ n : ℕ
h0 : x = 0
⊢ Multiset.Rel Associated (factors (x ^ (n + 1))) ((n + 1) • factors x)
simp [h0, zero_pow n.succ_pos, smul_zero]
case neg
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
x : α
n✝ n : ℕ
h0 : ¬x = 0
⊢ Multiset.Rel Associated (factors (x * x ^ n)) (factors x + n • factors x)
case neg
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
x : α
n✝ n : ℕ
h0 : ¬x = 0
⊢ Multiset.Rel Associated (factors (x ^ (n + 1))) ((n + 1) • factors x)
rw [pow_succ, succ_nsmul]
case neg
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
x : α
n✝ n : ℕ
h0 : ¬x = 0
⊢ Multiset.Rel Associated (factors x + factors (x ^ n)) (factors x + n • factors x)
case neg
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
x : α
n✝ n : ℕ
h0 : ¬x = 0
⊢ Multiset.Rel Associated (factors (x * x ^ n)) (factors x + n • factors x)
refine' Multiset.Rel.trans _ (factors_mul h0 (pow_ne_zero n h0)) _
case neg
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
x : α
n✝ n : ℕ
h0 : ¬x = 0
⊢ Multiset.Rel Associated (factors x) (factors x)
case neg
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
x : α
n✝ n : ℕ
h0 : ¬x = 0
⊢ Multiset.Rel Associated (factors x + factors (x ^ n)) (factors x + n • factors x)
refine' Multiset.Rel.add _ <| factors_pow n
no goals
case neg
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
x : α
n✝ n : ℕ
h0 : ¬x = 0
⊢ Multiset.Rel Associated (factors x) (factors x)
exact Multiset.rel_refl_of_refl_on fun y _ => Associated.refl _