-- Mathlib/RingTheory/ChainOfDivisors.lean
theorem mem_normalizedFactors_factor_dvd_iso_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' : M)) :
    ↑(d ⟨p, dvd_of_mem_normalizedFactors hp⟩) ∈ normalizedFactors n

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'
this : Prime ↑(d ⟨p, ⋯⟩)
⊢ ↑(d ⟨p, ⋯⟩) ∈ normalizedFactors n

Tactic:
obtain ⟨q, hq, hq'⟩ :=
  exists_mem_normalizedFactors_of_dvd hn this.irreducible
    (d ⟨p, by apply dvd_of_mem_normalizedFactors; convert hp⟩).prop

Result:
case 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 : Prime ↑(d ⟨p, ⋯⟩)
q : N
hq : q ∈ normalizedFactors n
hq' : Associated (↑(d ⟨p, ⋯⟩)) q
⊢ ↑(d ⟨p, ⋯⟩) ∈ normalizedFactors n

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_dvd_mk.mpr (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'
this✝ :
  Associates.mk ↑(d ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), ⋯⟩) =
    ↑((mkFactorOrderIsoOfFactorDvdEquiv hd) ⟨associatesEquivOfUniqueUnits.symm p, ⋯⟩)
this : DecidableEq (Associates M) := Classical.decEq (Associates M)
⊢ p ∈ normalizedFactors ?m.86941

Tactic:
convert hp

Result:
no goals

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 : Prime ↑(d ⟨p, ⋯⟩)
⊢ p ∈ normalizedFactors m

Tactic:
convert 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'
⊢ ↑(d ⟨p, ⋯⟩) ∈ normalizedFactors n

Tactic:
suffices
  Prime (d ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), by
          simp [dvd_of_mem_normalizedFactors hp]⟩ : N) by
  simp only [associatesEquivOfUniqueUnits_apply, out_mk, normalize_eq,
    associatesEquivOfUniqueUnits_symm_apply] at this
  obtain ⟨q, hq, hq'⟩ :=
    exists_mem_normalizedFactors_of_dvd hn this.irreducible
      (d ⟨p, by apply dvd_of_mem_normalizedFactors; convert hp⟩).prop
  rwa [associated_iff_eq.mp hq']

Result:
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'
⊢ Prime ↑(d ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), ⋯⟩)