-- Mathlib/RingTheory/ChainOfDivisors.lean
theorem emultiplicity_prime_le_emultiplicity_image_by_factor_orderIso {m p : Associates M}
    {n : Associates N} (hp : p ∈ normalizedFactors m) (d : Set.Iic m ≃o Set.Iic n) :
    emultiplicity p m ≤ emultiplicity (↑(d ⟨p, dvd_of_mem_normalizedFactors hp⟩)) n

Proof state:
case neg
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
N : Type u_2
inst✝² : CancelCommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid 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 ⟨p, ⋯⟩) ^ multiplicity p m ∣ n

Tactic:
apply pow_image_of_prime_by_factor_orderIso_dvd hn hp d (pow_multiplicity_dvd ..)

Result:
no goals

Proof state:
case neg
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
N : Type u_2
inst✝² : CancelCommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid 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
⊢ emultiplicity p m ≤ emultiplicity (↑(d ⟨p, ⋯⟩)) n

Tactic:
rw [FiniteMultiplicity.of_prime_left (prime_of_normalized_factor p hp) hm
  |>.emultiplicity_eq_multiplicity, ← pow_dvd_iff_le_emultiplicity]

Result:
case neg
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
N : Type u_2
inst✝² : CancelCommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid 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 ⟨p, ⋯⟩) ^ multiplicity p m ∣ n

Proof state:
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
N : Type u_2
inst✝² : CancelCommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
⊢ emultiplicity p m ≤ emultiplicity (↑(d ⟨p, ⋯⟩)) n

Tactic:
by_cases hn : n = 0

Result:
case pos
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
N : Type u_2
inst✝² : CancelCommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hn : n = 0
⊢ emultiplicity p m ≤ emultiplicity (↑(d ⟨p, ⋯⟩)) n

case neg
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
N : Type u_2
inst✝² : CancelCommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hn : ¬n = 0
⊢ emultiplicity p m ≤ emultiplicity (↑(d ⟨p, ⋯⟩)) n

Proof state:
case pos
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
N : Type u_2
inst✝² : CancelCommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid 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
⊢ emultiplicity p m ≤ emultiplicity (↑(d ⟨p, ⋯⟩)) n

Tactic:
simp [hm] at hp

Result:
no goals

Proof state:
case pos
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
N : Type u_2
inst✝² : CancelCommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hn : n = 0
⊢ emultiplicity p m ≤ emultiplicity (↑(d ⟨p, ⋯⟩)) n

Tactic:
simp [hn]

Result:
no goals

Proof state:
case neg
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
N : Type u_2
inst✝² : CancelCommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hn : ¬n = 0
⊢ emultiplicity p m ≤ emultiplicity (↑(d ⟨p, ⋯⟩)) n

Tactic:
by_cases hm : m = 0

Result:
case pos
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
N : Type u_2
inst✝² : CancelCommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid 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
⊢ emultiplicity p m ≤ emultiplicity (↑(d ⟨p, ⋯⟩)) n

case neg
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
N : Type u_2
inst✝² : CancelCommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid 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
⊢ emultiplicity p m ≤ emultiplicity (↑(d ⟨p, ⋯⟩)) n