case intro.intro
M : Type u_1
inst✝⁵ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁴ : CancelCommMonoidWithZero N
inst✝³ : UniqueFactorizationMonoid N
inst✝² : UniqueFactorizationMonoid M
inst✝¹ : DecidableEq (Associates M)
inst✝ : DecidableEq (Associates N)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
q : Associates N
hq : q ∈ normalizedFactors n
hq' : Associated (↑(↑d { val := p, property := (_ : p ∣ m) })) q
⊢ ↑(↑d { val := p, property := (_ : p ∣ m) }) ∈ normalizedFactors n
M : Type u_1
inst✝⁵ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁴ : CancelCommMonoidWithZero N
inst✝³ : UniqueFactorizationMonoid N
inst✝² : UniqueFactorizationMonoid M
inst✝¹ : DecidableEq (Associates M)
inst✝ : DecidableEq (Associates N)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
⊢ ↑(↑d { val := p, property := (_ : p ∣ m) }) ∈ normalizedFactors n
obtain ⟨q, hq, hq'⟩ :=
  exists_mem_normalizedFactors_of_dvd hn (map_prime_of_factor_orderIso hn hp d).irreducible
    (d ⟨p, dvd_of_mem_normalizedFactors hp⟩).prop
case intro.intro
M : Type u_1
inst✝⁵ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁴ : CancelCommMonoidWithZero N
inst✝³ : UniqueFactorizationMonoid N
inst✝² : UniqueFactorizationMonoid M
inst✝¹ : DecidableEq (Associates M)
inst✝ : DecidableEq (Associates N)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
q : Associates N
hq : q ∈ normalizedFactors n
hq' : ↑(↑d { val := p, property := (_ : p ∣ m) }) = q
⊢ ↑(↑d { val := p, property := (_ : p ∣ m) }) ∈ normalizedFactors n
case intro.intro
M : Type u_1
inst✝⁵ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁴ : CancelCommMonoidWithZero N
inst✝³ : UniqueFactorizationMonoid N
inst✝² : UniqueFactorizationMonoid M
inst✝¹ : DecidableEq (Associates M)
inst✝ : DecidableEq (Associates N)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
q : Associates N
hq : q ∈ normalizedFactors n
hq' : Associated (↑(↑d { val := p, property := (_ : p ∣ m) })) q
⊢ ↑(↑d { val := p, property := (_ : p ∣ m) }) ∈ normalizedFactors n
rw [associated_iff_eq] at hq'
no goals
case intro.intro
M : Type u_1
inst✝⁵ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁴ : CancelCommMonoidWithZero N
inst✝³ : UniqueFactorizationMonoid N
inst✝² : UniqueFactorizationMonoid M
inst✝¹ : DecidableEq (Associates M)
inst✝ : DecidableEq (Associates N)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
q : Associates N
hq : q ∈ normalizedFactors n
hq' : ↑(↑d { val := p, property := (_ : p ∣ m) }) = q
⊢ ↑(↑d { val := p, property := (_ : p ∣ m) }) ∈ normalizedFactors n
rwa [hq']