-- Mathlib/RingTheory/ChainOfDivisors.lean
theorem emultiplicity_prime_eq_emultiplicity_image_by_factor_orderIso {m p : Associates M}
    {n : Associates N} (hn : n ≠ 0) (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:
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
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
⊢ emultiplicity (↑(d ⟨p, ⋯⟩)) n ≤ emultiplicity (↑(d.symm (d ⟨p, ⋯⟩))) m

Tactic:
letI := Classical.decEq (Associates N)

Result:
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
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
this : DecidableEq (Associates N) := Classical.decEq (Associates N)
⊢ emultiplicity (↑(d ⟨p, ⋯⟩)) n ≤ emultiplicity (↑(d.symm (d ⟨p, ⋯⟩))) m

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
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
this : emultiplicity (↑(d ⟨p, ⋯⟩)) n ≤ emultiplicity (↑(d.symm (d ⟨p, ⋯⟩))) m
⊢ emultiplicity (↑(d ⟨p, ⋯⟩)) n ≤ emultiplicity p m

Tactic:
rw [d.symm_apply_apply ⟨p, dvd_of_mem_normalizedFactors hp⟩, Subtype.coe_mk] at this

Result:
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
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
this : emultiplicity (↑(d ⟨p, ⋯⟩)) n ≤ emultiplicity (↑⟨p, ⋯⟩) m
⊢ emultiplicity (↑(d ⟨p, ⋯⟩)) n ≤ emultiplicity p m

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
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
⊢ emultiplicity (↑(d ⟨p, ⋯⟩)) n ≤ emultiplicity p m

Tactic:
suffices emultiplicity (↑(d ⟨p, dvd_of_mem_normalizedFactors hp⟩)) n ≤
    emultiplicity (↑(d.symm (d ⟨p, dvd_of_mem_normalizedFactors hp⟩))) m by
  rw [d.symm_apply_apply ⟨p, dvd_of_mem_normalizedFactors hp⟩, Subtype.coe_mk] at this
  exact this

Result:
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
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
⊢ emultiplicity (↑(d ⟨p, ⋯⟩)) n ≤ emultiplicity (↑(d.symm (d ⟨p, ⋯⟩))) m

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
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
⊢ emultiplicity p m = emultiplicity (↑(d ⟨p, ⋯⟩)) n

Tactic:
refine le_antisymm (emultiplicity_prime_le_emultiplicity_image_by_factor_orderIso hp d) ?_

Result:
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
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
⊢ emultiplicity (↑(d ⟨p, ⋯⟩)) n ≤ emultiplicity p m

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
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
this : DecidableEq (Associates N) := Classical.decEq (Associates N)
⊢ emultiplicity (↑(d ⟨p, ⋯⟩)) n ≤ emultiplicity (↑(d.symm (d ⟨p, ⋯⟩))) m

Tactic:
simpa only [Subtype.coe_eta] using
  emultiplicity_prime_le_emultiplicity_image_by_factor_orderIso
    (mem_normalizedFactors_factor_orderIso_of_mem_normalizedFactors hn hp d) d.symm

Result:
no goals

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
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
this : emultiplicity (↑(d ⟨p, ⋯⟩)) n ≤ emultiplicity (↑⟨p, ⋯⟩) m
⊢ emultiplicity (↑(d ⟨p, ⋯⟩)) n ≤ emultiplicity p m

Tactic:
exact this

Result:
no goals