-- Mathlib/RingTheory/ChainOfDivisors.lean
theorem emultiplicity_factor_dvd_iso_eq_emultiplicity_of_mem_normalizedFactors {m p : M} {n : N}
    (hm : m ≠ 0) (hn : n ≠ 0) (hp : p ∈ normalizedFactors m)
    {d : { l : M // l ∣ m } ≃ { l : N // l ∣ n }} (hd : ∀ l l', (d l : N) ∣ d l' ↔ (l : M) ∣ l') :
    emultiplicity (d ⟨p, dvd_of_mem_normalizedFactors hp⟩ : N) n = emultiplicity p m

Proof state:
case h
M : Type u_1
inst✝⁵ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁴ : CancelCommMonoidWithZero N
inst✝³ : Subsingleton Mˣ
inst✝² : Subsingleton Nˣ
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : UniqueFactorizationMonoid N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'
⊢ emultiplicity (Associates.mk p) (Associates.mk m) =
    emultiplicity (Associates.mk ↑(d ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), ⋯⟩))
      (Associates.mk n)

Tactic:
have : Associates.mk (d ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), by
  simp only [dvd_of_mem_normalizedFactors hp, associatesEquivOfUniqueUnits_symm_apply,
    associatesEquivOfUniqueUnits_apply, out_mk, normalize_eq]⟩ : N) =
  ↑(mkFactorOrderIsoOfFactorDvdEquiv hd ⟨associatesEquivOfUniqueUnits.symm p, by
    rw [associatesEquivOfUniqueUnits_symm_apply]
    exact mk_le_mk_of_dvd (dvd_of_mem_normalizedFactors hp)⟩) := by
  rw [mkFactorOrderIsoOfFactorDvdEquiv_apply_coe]

Result:
case h
M : Type u_1
inst✝⁵ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁴ : CancelCommMonoidWithZero N
inst✝³ : Subsingleton Mˣ
inst✝² : Subsingleton Nˣ
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : UniqueFactorizationMonoid N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'
this :
  Associates.mk ↑(d ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), ⋯⟩) =
    ↑((mkFactorOrderIsoOfFactorDvdEquiv hd) ⟨associatesEquivOfUniqueUnits.symm p, ⋯⟩)
⊢ emultiplicity (Associates.mk p) (Associates.mk m) =
    emultiplicity (Associates.mk ↑(d ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), ⋯⟩))
      (Associates.mk n)

Proof state:
case h
M : Type u_1
inst✝⁵ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁴ : CancelCommMonoidWithZero N
inst✝³ : Subsingleton Mˣ
inst✝² : Subsingleton Nˣ
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : UniqueFactorizationMonoid N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'
⊢ emultiplicity p m = emultiplicity (↑(d ⟨p, ⋯⟩)) n

Tactic:
suffices emultiplicity (Associates.mk p) (Associates.mk m) = emultiplicity (Associates.mk
  ↑(d ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), by
    simp [dvd_of_mem_normalizedFactors hp]⟩)) (Associates.mk n) by
  simpa only [emultiplicity_mk_eq_emultiplicity, associatesEquivOfUniqueUnits_symm_apply,
    associatesEquivOfUniqueUnits_apply, out_mk, normalize_eq] using this

Result:
case h
M : Type u_1
inst✝⁵ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁴ : CancelCommMonoidWithZero N
inst✝³ : Subsingleton Mˣ
inst✝² : Subsingleton Nˣ
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : UniqueFactorizationMonoid N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'
⊢ emultiplicity (Associates.mk p) (Associates.mk m) =
    emultiplicity (Associates.mk ↑(d ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), ⋯⟩))
      (Associates.mk n)

Proof state:
case h
M : Type u_1
inst✝⁵ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁴ : CancelCommMonoidWithZero N
inst✝³ : Subsingleton Mˣ
inst✝² : Subsingleton Nˣ
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : UniqueFactorizationMonoid N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'
this :
  Associates.mk ↑(d ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), ⋯⟩) =
    ↑((mkFactorOrderIsoOfFactorDvdEquiv hd) ⟨associatesEquivOfUniqueUnits.symm p, ⋯⟩)
⊢ Associates.mk p ∈ normalizedFactors (Associates.mk m)

Tactic:
obtain ⟨q, hq, hq'⟩ :=
  exists_mem_normalizedFactors_of_dvd (mk_ne_zero.mpr hm)
    (prime_mk.mpr (prime_of_normalized_factor p hp)).irreducible
    (mk_le_mk_of_dvd (dvd_of_mem_normalizedFactors hp))

Result:
case h.intro.intro
M : Type u_1
inst✝⁵ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁴ : CancelCommMonoidWithZero N
inst✝³ : Subsingleton Mˣ
inst✝² : Subsingleton Nˣ
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : UniqueFactorizationMonoid N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'
this :
  Associates.mk ↑(d ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), ⋯⟩) =
    ↑((mkFactorOrderIsoOfFactorDvdEquiv hd) ⟨associatesEquivOfUniqueUnits.symm p, ⋯⟩)
q : Associates M
hq : q ∈ normalizedFactors (Associates.mk m)
hq' : Associated (Associates.mk p) q
⊢ Associates.mk p ∈ normalizedFactors (Associates.mk m)

Proof state:
M : Type u_1
inst✝⁵ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁴ : CancelCommMonoidWithZero N
inst✝³ : Subsingleton Mˣ
inst✝² : Subsingleton Nˣ
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : UniqueFactorizationMonoid N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'
⊢ associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p) ∣ m

Tactic:
simp [dvd_of_mem_normalizedFactors hp]

Result:
no goals

Proof state:
M : Type u_1
inst✝⁵ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁴ : CancelCommMonoidWithZero N
inst✝³ : Subsingleton Mˣ
inst✝² : Subsingleton Nˣ
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : UniqueFactorizationMonoid N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'
⊢ associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p) ∣ m

Tactic:
simp only [dvd_of_mem_normalizedFactors hp, associatesEquivOfUniqueUnits_symm_apply,
  associatesEquivOfUniqueUnits_apply, out_mk, normalize_eq]

Result:
no goals

Proof state:
M : Type u_1
inst✝⁵ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁴ : CancelCommMonoidWithZero N
inst✝³ : Subsingleton Mˣ
inst✝² : Subsingleton Nˣ
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : UniqueFactorizationMonoid N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'
⊢ Associates.mk p ∈ Set.Iic (Associates.mk m)

Tactic:
exact mk_le_mk_of_dvd (dvd_of_mem_normalizedFactors hp)

Result:
no goals