case pos
M : Type u_1
inst✝⁶ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁵ : CancelCommMonoidWithZero N
inst✝⁴ : UniqueFactorizationMonoid N
inst✝³ : UniqueFactorizationMonoid M
inst✝² : DecidableRel fun x x_1 => x ∣ x_1
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hn : n = 0
⊢ multiplicity p m ≤ multiplicity (↑(↑d { val := p, property := (_ : p ∣ m) })) n

case neg
M : Type u_1
inst✝⁶ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁵ : CancelCommMonoidWithZero N
inst✝⁴ : UniqueFactorizationMonoid N
inst✝³ : UniqueFactorizationMonoid M
inst✝² : DecidableRel fun x x_1 => x ∣ x_1
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hn : ¬n = 0
⊢ multiplicity p m ≤ multiplicity (↑(↑d { val := p, property := (_ : p ∣ m) })) n
M : Type u_1
inst✝⁶ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁵ : CancelCommMonoidWithZero N
inst✝⁴ : UniqueFactorizationMonoid N
inst✝³ : UniqueFactorizationMonoid M
inst✝² : DecidableRel fun x x_1 => x ∣ x_1
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
⊢ multiplicity p m ≤ multiplicity (↑(↑d { val := p, property := (_ : p ∣ m) })) n
by_cases hn : n = 0
case pos
M : Type u_1
inst✝⁶ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁵ : CancelCommMonoidWithZero N
inst✝⁴ : UniqueFactorizationMonoid N
inst✝³ : UniqueFactorizationMonoid M
inst✝² : DecidableRel fun x x_1 => x ∣ x_1
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hn : ¬n = 0
hm : m = 0
⊢ multiplicity p m ≤ multiplicity (↑(↑d { val := p, property := (_ : p ∣ m) })) n

case neg
M : Type u_1
inst✝⁶ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁵ : CancelCommMonoidWithZero N
inst✝⁴ : UniqueFactorizationMonoid N
inst✝³ : UniqueFactorizationMonoid M
inst✝² : DecidableRel fun x x_1 => x ∣ x_1
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hn : ¬n = 0
hm : ¬m = 0
⊢ multiplicity p m ≤ multiplicity (↑(↑d { val := p, property := (_ : p ∣ m) })) n
case neg
M : Type u_1
inst✝⁶ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁵ : CancelCommMonoidWithZero N
inst✝⁴ : UniqueFactorizationMonoid N
inst✝³ : UniqueFactorizationMonoid M
inst✝² : DecidableRel fun x x_1 => x ∣ x_1
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hn : ¬n = 0
⊢ multiplicity p m ≤ multiplicity (↑(↑d { val := p, property := (_ : p ∣ m) })) n
by_cases hm : m = 0
case neg
M : Type u_1
inst✝⁶ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁵ : CancelCommMonoidWithZero N
inst✝⁴ : UniqueFactorizationMonoid N
inst✝³ : UniqueFactorizationMonoid M
inst✝² : DecidableRel fun x x_1 => x ∣ x_1
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hn : ¬n = 0
hm : ¬m = 0
⊢ ↑(↑d { val := p, property := (_ : p ∣ m) }) ^ Part.get (multiplicity p m) (_ : (multiplicity p m).Dom) ∣ n
case neg
M : Type u_1
inst✝⁶ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁵ : CancelCommMonoidWithZero N
inst✝⁴ : UniqueFactorizationMonoid N
inst✝³ : UniqueFactorizationMonoid M
inst✝² : DecidableRel fun x x_1 => x ∣ x_1
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hn : ¬n = 0
hm : ¬m = 0
⊢ multiplicity p m ≤ multiplicity (↑(↑d { val := p, property := (_ : p ∣ m) })) n
rw [←
  PartENat.natCast_get
    (finite_iff_dom.1 <| finite_prime_left (prime_of_normalized_factor p hp) hm),
  ← pow_dvd_iff_le_multiplicity]
no goals
case neg
M : Type u_1
inst✝⁶ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁵ : CancelCommMonoidWithZero N
inst✝⁴ : UniqueFactorizationMonoid N
inst✝³ : UniqueFactorizationMonoid M
inst✝² : DecidableRel fun x x_1 => x ∣ x_1
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hn : ¬n = 0
hm : ¬m = 0
⊢ ↑(↑d { val := p, property := (_ : p ∣ m) }) ^ Part.get (multiplicity p m) (_ : (multiplicity p m).Dom) ∣ n
exact pow_image_of_prime_by_factor_orderIso_dvd hn hp d (pow_multiplicity_dvd _)
no goals
case pos
M : Type u_1
inst✝⁶ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁵ : CancelCommMonoidWithZero N
inst✝⁴ : UniqueFactorizationMonoid N
inst✝³ : UniqueFactorizationMonoid M
inst✝² : DecidableRel fun x x_1 => x ∣ x_1
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hn : n = 0
⊢ multiplicity p m ≤ multiplicity (↑(↑d { val := p, property := (_ : p ∣ m) })) n
simp [hn]
no goals
case pos
M : Type u_1
inst✝⁶ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁵ : CancelCommMonoidWithZero N
inst✝⁴ : UniqueFactorizationMonoid N
inst✝³ : UniqueFactorizationMonoid M
inst✝² : DecidableRel fun x x_1 => x ∣ x_1
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hn : ¬n = 0
hm : m = 0
⊢ multiplicity p m ≤ multiplicity (↑(↑d { val := p, property := (_ : p ∣ m) })) n
simp [hm] at hp