awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
N : Type u_2
inst_2 : CommMonoidWithZero N
inst_3 : Subsingleton.{u_1 + 1} Mˣ
inst_4 : Subsingleton.{u_2 + 1} Nˣ
inst_5 : UniqueFactorizationMonoid M
inst_6 : UniqueFactorizationMonoid N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : Equiv.{max 1 (u_1 + 1), max 1 (u_2 + 1)} { l : M // l ∣ m } { l : N // l ∣ n }
hd :
  ∀ (l l' : { l : M // l ∣ m }),
    Dvd.dvd.{u_2} (α := N) (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) l) : N)
        (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) l') : N) ↔
      (↑l : M) ∣ (↑l' : M)
this :
  Eq.{u_2 + 1} (α := Associates N)
    (Associates.mk
      (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n })
            (Subtype.mk (p := fun (l : M) ↦ l ∣ m)
              ((associatesEquivOfUniqueUnits : (a : Associates M) → M)
                ((MulEquiv.symm associatesEquivOfUniqueUnits : (a : M) → Associates M) p : Associates M))
              ⋯)) :
        N))
    (↑((mkFactorOrderIsoOfFactorDvdEquiv hd :
            (a : (↑(Set.Iic (Associates.mk m)) : Type u_1)) → (↑(Set.Iic (Associates.mk n)) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦
            Membership.mem (γ := Set (Associates M)) (Set.Iic (Associates.mk m)) x)
            ((MulEquiv.symm associatesEquivOfUniqueUnits : (a : M) → Associates M) p) ⋯)) :
      Associates N)
rw :
  Prime.{u_2} (M := Associates N)
    (↑((mkFactorOrderIsoOfFactorDvdEquiv hd :
            (a : (↑(Set.Iic (Associates.mk m)) : Type u_1)) → (↑(Set.Iic (Associates.mk n)) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦
            Membership.mem (γ := Set (Associates M)) (Set.Iic (Associates.mk m)) x)
            ((MulEquiv.symm associatesEquivOfUniqueUnits : (a : M) → Associates M) p) ⋯)) :
      Associates N)
⊢ Prime.{u_2} (M := N)
    (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n })
          (Subtype.mk (p := fun (l : M) ↦ l ∣ m)
            ((associatesEquivOfUniqueUnits : (a : Associates M) → M)
              ((MulEquiv.symm associatesEquivOfUniqueUnits : (a : M) → Associates M) p : Associates M))
            ⋯)) :
      N)

Tactic:
rw [← Associates.prime_mk, this]

Premises used: Associates.prime_mk
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
N : Type u_2
inst_2 : CommMonoidWithZero N
inst_3 : Subsingleton.{u_1 + 1} Mˣ
inst_4 : Subsingleton.{u_2 + 1} Nˣ
inst_5 : UniqueFactorizationMonoid M
inst_6 : UniqueFactorizationMonoid N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : Equiv.{max 1 (u_1 + 1), max 1 (u_2 + 1)} { l : M // l ∣ m } { l : N // l ∣ n }
hd :
  ∀ (l l' : { l : M // l ∣ m }),
    Dvd.dvd.{u_2} (α := N) (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) l) : N)
        (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) l') : N) ↔
      (↑l : M) ∣ (↑l' : M)
this_1 :
  Eq.{u_2 + 1} (α := Associates N)
    (Associates.mk
      (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n })
            (Subtype.mk (p := fun (l : M) ↦ l ∣ m)
              ((associatesEquivOfUniqueUnits : (a : Associates M) → M)
                ((MulEquiv.symm associatesEquivOfUniqueUnits : (a : M) → Associates M) p : Associates M))
              ⋯)) :
        N))
    (↑((mkFactorOrderIsoOfFactorDvdEquiv hd :
            (a : (↑(Set.Iic (Associates.mk m)) : Type u_1)) → (↑(Set.Iic (Associates.mk n)) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦
            Membership.mem (γ := Set (Associates M)) (Set.Iic (Associates.mk m)) x)
            ((MulEquiv.symm associatesEquivOfUniqueUnits : (a : M) → Associates M) p) ⋯)) :
      Associates N)
this : DecidableEq (Associates M) := Classical.decEq (Associates M)
⊢ Prime.{u_2} (M := Associates N)
    (↑((mkFactorOrderIsoOfFactorDvdEquiv hd :
            (a : (↑(Set.Iic (Associates.mk m)) : Type u_1)) → (↑(Set.Iic (Associates.mk n)) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦
            Membership.mem (γ := Set (Associates M)) (Set.Iic (Associates.mk m)) x)
            ((MulEquiv.symm associatesEquivOfUniqueUnits : (a : M) → Associates M) p) ⋯)) :
      Associates N)

Tactic:
map_prime_of_factor_orderIso (mk_ne_zero.mpr hn) ?_ _

Premises used: Iff.mpr, Associates.mk_ne_zero, map_prime_of_factor_orderIso
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
N : Type u_2
inst_2 : CommMonoidWithZero N
inst_3 : Subsingleton.{u_1 + 1} Mˣ
inst_4 : Subsingleton.{u_2 + 1} Nˣ
inst_5 : UniqueFactorizationMonoid M
inst_6 : UniqueFactorizationMonoid N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : Equiv.{max 1 (u_1 + 1), max 1 (u_2 + 1)} { l : M // l ∣ m } { l : N // l ∣ n }
hd :
  ∀ (l l' : { l : M // l ∣ m }),
    Dvd.dvd.{u_2} (α := N) (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) l) : N)
        (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) l') : N) ↔
      (↑l : M) ∣ (↑l' : M)
this_1 :
  Eq.{u_2 + 1} (α := Associates N)
    (Associates.mk
      (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n })
            (Subtype.mk (p := fun (l : M) ↦ l ∣ m)
              ((associatesEquivOfUniqueUnits : (a : Associates M) → M)
                ((MulEquiv.symm associatesEquivOfUniqueUnits : (a : M) → Associates M) p : Associates M))
              ⋯)) :
        N))
    (↑((mkFactorOrderIsoOfFactorDvdEquiv hd :
            (a : (↑(Set.Iic (Associates.mk m)) : Type u_1)) → (↑(Set.Iic (Associates.mk n)) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦
            Membership.mem (γ := Set (Associates M)) (Set.Iic (Associates.mk m)) x)
            ((MulEquiv.symm associatesEquivOfUniqueUnits : (a : M) → Associates M) p) ⋯)) :
      Associates N)
this : DecidableEq (Associates M) := Classical.decEq (Associates M)
refine :
  Membership.mem (α := Associates M) (γ := Multiset (Associates M)) (normalizedFactors (Associates.mk m))
    ((MulEquiv.symm associatesEquivOfUniqueUnits : (a : M) → Associates M) p : Associates M)
⊢ Prime.{u_2} (M := Associates N)
    (↑((mkFactorOrderIsoOfFactorDvdEquiv hd :
            (a : (↑(Set.Iic (Associates.mk m)) : Type u_1)) → (↑(Set.Iic (Associates.mk n)) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦
            Membership.mem (γ := Set (Associates M)) (Set.Iic (Associates.mk m)) x)
            ((MulEquiv.symm associatesEquivOfUniqueUnits : (a : M) → Associates M) p) ⋯)) :
      Associates N)

Tactic:
refine map_prime_of_factor_orderIso (mk_ne_zero.mpr hn) ?_ _

Premises used: Iff.mpr, Associates.mk_ne_zero, map_prime_of_factor_orderIso
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
N : Type u_2
inst_2 : CommMonoidWithZero N
inst_3 : Subsingleton.{u_1 + 1} Mˣ
inst_4 : Subsingleton.{u_2 + 1} Nˣ
inst_5 : UniqueFactorizationMonoid M
inst_6 : UniqueFactorizationMonoid N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : Equiv.{max 1 (u_1 + 1), max 1 (u_2 + 1)} { l : M // l ∣ m } { l : N // l ∣ n }
hd :
  ∀ (l l' : { l : M // l ∣ m }),
    Dvd.dvd.{u_2} (α := N) (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) l) : N)
        (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) l') : N) ↔
      (↑l : M) ∣ (↑l' : M)
this_1 :
  Eq.{u_2 + 1} (α := Associates N)
    (Associates.mk
      (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n })
            (Subtype.mk (p := fun (l : M) ↦ l ∣ m)
              ((associatesEquivOfUniqueUnits : (a : Associates M) → M)
                ((MulEquiv.symm associatesEquivOfUniqueUnits : (a : M) → Associates M) p : Associates M))
              ⋯)) :
        N))
    (↑((mkFactorOrderIsoOfFactorDvdEquiv hd :
            (a : (↑(Set.Iic (Associates.mk m)) : Type u_1)) → (↑(Set.Iic (Associates.mk n)) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦
            Membership.mem (γ := Set (Associates M)) (Set.Iic (Associates.mk m)) x)
            ((MulEquiv.symm associatesEquivOfUniqueUnits : (a : M) → Associates M) p) ⋯)) :
      Associates N)
this : DecidableEq (Associates M) := Classical.decEq (Associates M)
⊢ p ∈ normalizedFactors m

Tactic:
hp
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
N : Type u_2
inst_2 : CommMonoidWithZero N
inst_3 : Subsingleton.{u_1 + 1} Mˣ
inst_4 : Subsingleton.{u_2 + 1} Nˣ
inst_5 : UniqueFactorizationMonoid M
inst_6 : UniqueFactorizationMonoid N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : Equiv.{max 1 (u_1 + 1), max 1 (u_2 + 1)} { l : M // l ∣ m } { l : N // l ∣ n }
hd :
  ∀ (l l' : { l : M // l ∣ m }),
    Dvd.dvd.{u_2} (α := N) (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) l) : N)
        (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) l') : N) ↔
      (↑l : M) ∣ (↑l' : M)
this_1 :
  Eq.{u_2 + 1} (α := Associates N)
    (Associates.mk
      (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n })
            (Subtype.mk (p := fun (l : M) ↦ l ∣ m)
              ((associatesEquivOfUniqueUnits : (a : Associates M) → M)
                ((MulEquiv.symm associatesEquivOfUniqueUnits : (a : M) → Associates M) p : Associates M))
              ⋯)) :
        N))
    (↑((mkFactorOrderIsoOfFactorDvdEquiv hd :
            (a : (↑(Set.Iic (Associates.mk m)) : Type u_1)) → (↑(Set.Iic (Associates.mk n)) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦
            Membership.mem (γ := Set (Associates M)) (Set.Iic (Associates.mk m)) x)
            ((MulEquiv.symm associatesEquivOfUniqueUnits : (a : M) → Associates M) p) ⋯)) :
      Associates N)
this : DecidableEq (Associates M) := Classical.decEq (Associates M)
⊢ p ∈ normalizedFactors m

Tactic:
convert! hp
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
N : Type u_2
inst_2 : CommMonoidWithZero N
inst_3 : Subsingleton.{u_1 + 1} Mˣ
inst_4 : Subsingleton.{u_2 + 1} Nˣ
inst_5 : UniqueFactorizationMonoid M
inst_6 : UniqueFactorizationMonoid N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : Equiv.{max 1 (u_1 + 1), max 1 (u_2 + 1)} { l : M // l ∣ m } { l : N // l ∣ n }
hd :
  ∀ (l l' : { l : M // l ∣ m }),
    Dvd.dvd.{u_2} (α := N) (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) l) : N)
        (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) l') : N) ↔
      (↑l : M) ∣ (↑l' : M)
this_1 :
  Eq.{u_2 + 1} (α := Associates N)
    (Associates.mk
      (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n })
            (Subtype.mk (p := fun (l : M) ↦ l ∣ m)
              ((associatesEquivOfUniqueUnits : (a : Associates M) → M)
                ((MulEquiv.symm associatesEquivOfUniqueUnits : (a : M) → Associates M) p : Associates M))
              ⋯)) :
        N))
    (↑((mkFactorOrderIsoOfFactorDvdEquiv hd :
            (a : (↑(Set.Iic (Associates.mk m)) : Type u_1)) → (↑(Set.Iic (Associates.mk n)) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦
            Membership.mem (γ := Set (Associates M)) (Set.Iic (Associates.mk m)) x)
            ((MulEquiv.symm associatesEquivOfUniqueUnits : (a : M) → Associates M) p) ⋯)) :
      Associates N)
this : DecidableEq (Associates M) := Classical.decEq (Associates M)
obtain :
  ∀ (q : Associates M) (hq : Membership.mem (γ := Multiset (Associates M)) (normalizedFactors (Associates.mk m)) q)
    (hq' : Associated (Associates.mk p) q),
    Membership.mem (α := Associates M) (γ := Multiset (Associates M)) (normalizedFactors (Associates.mk m))
      ((MulEquiv.symm associatesEquivOfUniqueUnits : (a : M) → Associates M) p : Associates M)
⊢ Membership.mem (α := Associates M) (γ := Multiset (Associates M)) (normalizedFactors (Associates.mk m))
    ((MulEquiv.symm associatesEquivOfUniqueUnits : (a : M) → Associates M) p : Associates M)

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

Premises used: Prime.irreducible, Iff.mpr, UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors, UniqueFactorizationMonoid.exists_mem_normalizedFactors_of_dvd, UniqueFactorizationMonoid.prime_of_normalized_factor, Associates.prime_mk, Associates.mk_le_mk_of_dvd, Associates.mk_ne_zero
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
N : Type u_2
inst_2 : CommMonoidWithZero N
inst_3 : Subsingleton.{u_1 + 1} Mˣ
inst_4 : Subsingleton.{u_2 + 1} Nˣ
inst_5 : UniqueFactorizationMonoid M
inst_6 : UniqueFactorizationMonoid N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : Equiv.{max 1 (u_1 + 1), max 1 (u_2 + 1)} { l : M // l ∣ m } { l : N // l ∣ n }
hd :
  ∀ (l l' : { l : M // l ∣ m }),
    Dvd.dvd.{u_2} (α := N) (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) l) : N)
        (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) l') : N) ↔
      (↑l : M) ∣ (↑l' : M)
this_1 :
  Eq.{u_2 + 1} (α := Associates N)
    (Associates.mk
      (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n })
            (Subtype.mk (p := fun (l : M) ↦ l ∣ m)
              ((associatesEquivOfUniqueUnits : (a : Associates M) → M)
                ((MulEquiv.symm associatesEquivOfUniqueUnits : (a : M) → Associates M) p : Associates M))
              ⋯)) :
        N))
    (↑((mkFactorOrderIsoOfFactorDvdEquiv hd :
            (a : (↑(Set.Iic (Associates.mk m)) : Type u_1)) → (↑(Set.Iic (Associates.mk n)) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦
            Membership.mem (γ := Set (Associates M)) (Set.Iic (Associates.mk m)) x)
            ((MulEquiv.symm associatesEquivOfUniqueUnits : (a : M) → Associates M) p) ⋯)) :
      Associates N)
this : DecidableEq (Associates M) := Classical.decEq (Associates M)
q : Associates M
hq : Membership.mem (γ := Multiset (Associates M)) (normalizedFactors (Associates.mk m)) q
hq' : Associated (Associates.mk p) q
⊢ Membership.mem (α := Associates M) (γ := Multiset (Associates M)) (normalizedFactors (Associates.mk m))
    ((MulEquiv.symm associatesEquivOfUniqueUnits : (a : M) → Associates M) p : Associates M)

Tactic:
simpa only [associated_iff_eq.mp hq', associatesEquivOfUniqueUnits_symm_apply] using hq

Premises used: associatesEquivOfUniqueUnits_symm_apply, associated_iff_eq, Iff.mp
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
N : Type u_2
inst_2 : CommMonoidWithZero N
inst_3 : Subsingleton.{u_1 + 1} Mˣ
inst_4 : Subsingleton.{u_2 + 1} Nˣ
inst_5 : UniqueFactorizationMonoid M
inst_6 : UniqueFactorizationMonoid N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : Equiv.{max 1 (u_1 + 1), max 1 (u_2 + 1)} { l : M // l ∣ m } { l : N // l ∣ n }
hd :
  ∀ (l l' : { l : M // l ∣ m }),
    Dvd.dvd.{u_2} (α := N) (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) l) : N)
        (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) l') : N) ↔
      (↑l : M) ∣ (↑l' : M)
h :
  emultiplicity p m =
    emultiplicity
      (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) (Subtype.mk (p := fun (l : M) ↦ l ∣ m) p ⋯)) : N) n
⊢ emultiplicity (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) (Subtype.mk (p := fun (l : M) ↦ l ∣ m) p ⋯)) : N)
      n =
    emultiplicity p m

Tactic:
apply Eq.symm

Premises used: Eq.symm
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
N : Type u_2
inst_2 : CommMonoidWithZero N
inst_3 : Subsingleton.{u_1 + 1} Mˣ
inst_4 : Subsingleton.{u_2 + 1} Nˣ
inst_5 : UniqueFactorizationMonoid M
inst_6 : UniqueFactorizationMonoid N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : Equiv.{max 1 (u_1 + 1), max 1 (u_2 + 1)} { l : M // l ∣ m } { l : N // l ∣ n }
hd :
  ∀ (l l' : { l : M // l ∣ m }),
    Dvd.dvd.{u_2} (α := N) (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) l) : N)
        (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) l') : N) ↔
      (↑l : M) ∣ (↑l' : M)
this :
  emultiplicity (α := Associates M) (Associates.mk p) (Associates.mk m) =
    emultiplicity (α := Associates N)
      (Associates.mk
        (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n })
              (Subtype.mk (p := fun (l : M) ↦ l ∣ m)
                ((associatesEquivOfUniqueUnits : (a : Associates M) → M)
                  ((MulEquiv.symm associatesEquivOfUniqueUnits : (a : M) → Associates M) p : Associates M))
                ⋯)) :
          N))
      (Associates.mk n)
⊢ emultiplicity p m =
    emultiplicity
      (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) (Subtype.mk (p := fun (l : M) ↦ l ∣ m) p ⋯)) : N) n

Tactic:
simpa only [emultiplicity_mk_eq_emultiplicity, associatesEquivOfUniqueUnits_symm_apply,
      associatesEquivOfUniqueUnits_apply, out_mk, normalize_eq] using this

Premises used: associatesEquivOfUniqueUnits_symm_apply, emultiplicity_mk_eq_emultiplicity, Associates.out_mk, associatesEquivOfUniqueUnits_apply, normalize_eq
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
N : Type u_2
inst_2 : CommMonoidWithZero N
inst_3 : Subsingleton.{u_1 + 1} Mˣ
inst_4 : Subsingleton.{u_2 + 1} Nˣ
inst_5 : UniqueFactorizationMonoid M
inst_6 : UniqueFactorizationMonoid N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : Equiv.{max 1 (u_1 + 1), max 1 (u_2 + 1)} { l : M // l ∣ m } { l : N // l ∣ n }
hd :
  ∀ (l l' : { l : M // l ∣ m }),
    Dvd.dvd.{u_2} (α := N) (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) l) : N)
        (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) l') : N) ↔
      (↑l : M) ∣ (↑l' : M)
h :
  emultiplicity (α := Associates M) (Associates.mk p) (Associates.mk m) =
    emultiplicity (α := Associates N)
      (Associates.mk
        (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n })
              (Subtype.mk (p := fun (l : M) ↦ l ∣ m)
                ((associatesEquivOfUniqueUnits : (a : Associates M) → M)
                  ((MulEquiv.symm associatesEquivOfUniqueUnits : (a : M) → Associates M) p : Associates M))
                ⋯)) :
          N))
      (Associates.mk n)
⊢ emultiplicity p m =
    emultiplicity
      (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) (Subtype.mk (p := fun (l : M) ↦ l ∣ m) p ⋯)) : N) 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
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
N : Type u_2
inst_2 : CommMonoidWithZero N
inst_3 : Subsingleton.{u_1 + 1} Mˣ
inst_4 : Subsingleton.{u_2 + 1} Nˣ
inst_5 : UniqueFactorizationMonoid M
inst_6 : UniqueFactorizationMonoid N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : Equiv.{max 1 (u_1 + 1), max 1 (u_2 + 1)} { l : M // l ∣ m } { l : N // l ∣ n }
hd :
  ∀ (l l' : { l : M // l ∣ m }),
    Dvd.dvd.{u_2} (α := N) (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) l) : N)
        (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) l') : N) ↔
      (↑l : M) ∣ (↑l' : M)
⊢ (associatesEquivOfUniqueUnits : (a : Associates M) → M)
      ((MulEquiv.symm associatesEquivOfUniqueUnits : (a : M) → Associates M) p : Associates M) ∣
    m

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

Premises used: associatesEquivOfUniqueUnits_symm_apply, UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors, Associates.out_mk, associatesEquivOfUniqueUnits_apply, normalize_eq
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
N : Type u_2
inst_2 : CommMonoidWithZero N
inst_3 : Subsingleton.{u_1 + 1} Mˣ
inst_4 : Subsingleton.{u_2 + 1} Nˣ
inst_5 : UniqueFactorizationMonoid M
inst_6 : UniqueFactorizationMonoid N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : Equiv.{max 1 (u_1 + 1), max 1 (u_2 + 1)} { l : M // l ∣ m } { l : N // l ∣ n }
hd :
  ∀ (l l' : { l : M // l ∣ m }),
    Dvd.dvd.{u_2} (α := N) (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) l) : N)
        (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) l') : N) ↔
      (↑l : M) ∣ (↑l' : M)
⊢ Membership.mem (γ := Set (Associates M)) (Set.Iic (Associates.mk m)) (Associates.mk p)

Tactic:
mk_le_mk_of_dvd (dvd_of_mem_normalizedFactors hp)

Premises used: Set.Mem, UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors, setOf, Associates.mk_le_mk_of_dvd, Set.Iic
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
N : Type u_2
inst_2 : CommMonoidWithZero N
inst_3 : Subsingleton.{u_1 + 1} Mˣ
inst_4 : Subsingleton.{u_2 + 1} Nˣ
inst_5 : UniqueFactorizationMonoid M
inst_6 : UniqueFactorizationMonoid N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : Equiv.{max 1 (u_1 + 1), max 1 (u_2 + 1)} { l : M // l ∣ m } { l : N // l ∣ n }
hd :
  ∀ (l l' : { l : M // l ∣ m }),
    Dvd.dvd.{u_2} (α := N) (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) l) : N)
        (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) l') : N) ↔
      (↑l : M) ∣ (↑l' : M)
⊢ Membership.mem (γ := Set (Associates M)) (Set.Iic (Associates.mk m)) (Associates.mk p)

Tactic:
exact mk_le_mk_of_dvd (dvd_of_mem_normalizedFactors hp)

Premises used: UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors, Associates.mk_le_mk_of_dvd
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
N : Type u_2
inst_2 : CommMonoidWithZero N
inst_3 : Subsingleton.{u_1 + 1} Mˣ
inst_4 : Subsingleton.{u_2 + 1} Nˣ
inst_5 : UniqueFactorizationMonoid M
inst_6 : UniqueFactorizationMonoid N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : Equiv.{max 1 (u_1 + 1), max 1 (u_2 + 1)} { l : M // l ∣ m } { l : N // l ∣ n }
hd :
  ∀ (l l' : { l : M // l ∣ m }),
    Dvd.dvd.{u_2} (α := N) (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) l) : N)
        (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) l') : N) ↔
      (↑l : M) ∣ (↑l' : M)
⊢ Eq.{u_2 + 1} (α := Associates N)
    (Associates.mk
      (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n })
            (Subtype.mk (p := fun (l : M) ↦ l ∣ m)
              ((associatesEquivOfUniqueUnits : (a : Associates M) → M)
                ((MulEquiv.symm associatesEquivOfUniqueUnits : (a : M) → Associates M) p : Associates M))
              ⋯)) :
        N))
    (↑((mkFactorOrderIsoOfFactorDvdEquiv hd :
            (a : (↑(Set.Iic (Associates.mk m)) : Type u_1)) → (↑(Set.Iic (Associates.mk n)) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦
            Membership.mem (γ := Set (Associates M)) (Set.Iic (Associates.mk m)) x)
            ((MulEquiv.symm associatesEquivOfUniqueUnits : (a : M) → Associates M) p) ⋯)) :
      Associates 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]