M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
⊢ Irreducible ↑(↑d { val := p, property := (_ : p ∣ m) })
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
⊢ Prime ↑(↑d { val := p, property := (_ : p ∣ m) })
rw [← irreducible_iff_prime]
case refine'_1
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
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) }) ≠ ⊥

case refine'_2
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
hb : b < ↑(↑d { val := p, property := (_ : p ∣ m) })
⊢ b = ⊥
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
⊢ Irreducible ↑(↑d { val := p, property := (_ : p ∣ m) })
refine' (Associates.isAtom_iff <| ne_zero_of_dvd_ne_zero hn (d ⟨p, _⟩).prop).mp ⟨_, fun b hb => _⟩
case refine'_1
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
⊢ ¬p = 1
case refine'_1
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
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) }) ≠ ⊥
rw [Ne.def, ← Associates.isUnit_iff_eq_bot, Associates.isUnit_iff_eq_one,
  coe_factor_orderIso_map_eq_one_iff _ d]
case refine'_1
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hp : 1 ∈ normalizedFactors m
⊢ False
case refine'_1
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
⊢ ¬p = 1
rintro rfl
no goals
case refine'_1
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hp : 1 ∈ normalizedFactors m
⊢ False
exact (prime_of_normalized_factor 1 hp).not_unit isUnit_one
case refine'_2.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)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
hb : b < ↑(↑d { val := p, property := (_ : p ∣ m) })
x : ↑(Set.Iic m)
hx : ↑d x = { val := b, property := (_ : b ≤ n) }
⊢ b = ⊥
case refine'_2
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
hb : b < ↑(↑d { val := p, property := (_ : p ∣ m) })
⊢ b = ⊥
obtain ⟨x, hx⟩ :=
  d.surjective ⟨b, le_trans (le_of_lt hb) (d ⟨p, dvd_of_mem_normalizedFactors hp⟩).prop⟩
case refine'_2.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)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
hb✝ : b < ↑(↑d { val := p, property := (_ : p ∣ m) })
x : ↑(Set.Iic m)
hb : ↑(↑d x) < ↑(↑d { val := p, property := (_ : p ∣ m) })
hx : ↑d x = { val := b, property := (_ : b ≤ n) }
⊢ b = ⊥
case refine'_2.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)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
hb : b < ↑(↑d { val := p, property := (_ : p ∣ m) })
x : ↑(Set.Iic m)
hx : ↑d x = { val := b, property := (_ : b ≤ n) }
⊢ b = ⊥
rw [← Subtype.coe_mk b _, ← hx] at hb
case refine'_2.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)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
hb✝ : b < ↑(↑d { val := p, property := (_ : p ∣ m) })
x : ↑(Set.Iic m)
hb : ↑(↑d x) < ↑(↑d { val := p, property := (_ : p ∣ m) })
hx : ↑d x = { val := b, property := (_ : b ≤ n) }
this : OrderBot { l // l ≤ m } := Subtype.orderBot (_ : ⊥ ≤ m)
⊢ b = ⊥
case refine'_2.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)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
hb✝ : b < ↑(↑d { val := p, property := (_ : p ∣ m) })
x : ↑(Set.Iic m)
hb : ↑(↑d x) < ↑(↑d { val := p, property := (_ : p ∣ m) })
hx : ↑d x = { val := b, property := (_ : b ≤ n) }
⊢ b = ⊥
letI : OrderBot { l : Associates M // l ≤ m } := Subtype.orderBot bot_le
case refine'_2.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)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
hb✝ : b < ↑(↑d { val := p, property := (_ : p ∣ m) })
x : ↑(Set.Iic m)
hb : ↑(↑d x) < ↑(↑d { val := p, property := (_ : p ∣ m) })
hx : ↑d x = { val := b, property := (_ : b ≤ n) }
this✝ : OrderBot { l // l ≤ m } := Subtype.orderBot (_ : ⊥ ≤ m)
this : OrderBot { l // l ≤ n } := Subtype.orderBot (_ : ⊥ ≤ n)
⊢ b = ⊥
case refine'_2.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)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
hb✝ : b < ↑(↑d { val := p, property := (_ : p ∣ m) })
x : ↑(Set.Iic m)
hb : ↑(↑d x) < ↑(↑d { val := p, property := (_ : p ∣ m) })
hx : ↑d x = { val := b, property := (_ : b ≤ n) }
this : OrderBot { l // l ≤ m } := Subtype.orderBot (_ : ⊥ ≤ m)
⊢ b = ⊥
letI : OrderBot { l : Associates N // l ≤ n } := Subtype.orderBot bot_le
case refine'_2.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)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
hb✝ : b < ↑(↑d { val := p, property := (_ : p ∣ m) })
x : ↑(Set.Iic m)
hb : ↑(↑d x) < ↑(↑d { val := p, property := (_ : p ∣ m) })
hx : ↑d x = { val := b, property := (_ : b ≤ n) }
this✝ : OrderBot { l // l ≤ m } := Subtype.orderBot (_ : ⊥ ≤ m)
this : OrderBot { l // l ≤ n } := Subtype.orderBot (_ : ⊥ ≤ n)
⊢ x = ⊥
case refine'_2.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)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
hb✝ : b < ↑(↑d { val := p, property := (_ : p ∣ m) })
x : ↑(Set.Iic m)
hb : ↑(↑d x) < ↑(↑d { val := p, property := (_ : p ∣ m) })
hx : ↑d x = { val := b, property := (_ : b ≤ n) }
this✝ : OrderBot { l // l ≤ m } := Subtype.orderBot (_ : ⊥ ≤ m)
this : OrderBot { l // l ≤ n } := Subtype.orderBot (_ : ⊥ ≤ n)
⊢ b = ⊥
suffices x = ⊥ by
  rw [this, OrderIso.map_bot d] at hx
  refine' (Subtype.mk_eq_bot_iff _ _).mp hx.symm
  simp
case refine'_2.intro.mk
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
hb✝ : b < ↑(↑d { val := p, property := (_ : p ∣ m) })
this✝ : OrderBot { l // l ≤ m } := Subtype.orderBot (_ : ⊥ ≤ m)
this : OrderBot { l // l ≤ n } := Subtype.orderBot (_ : ⊥ ≤ n)
a : Associates M
ha : a ∈ Set.Iic m
hb : ↑(↑d { val := a, property := ha }) < ↑(↑d { val := p, property := (_ : p ∣ m) })
hx : ↑d { val := a, property := ha } = { val := b, property := (_ : b ≤ n) }
⊢ { val := a, property := ha } = ⊥
case refine'_2.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)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
hb✝ : b < ↑(↑d { val := p, property := (_ : p ∣ m) })
x : ↑(Set.Iic m)
hb : ↑(↑d x) < ↑(↑d { val := p, property := (_ : p ∣ m) })
hx : ↑d x = { val := b, property := (_ : b ≤ n) }
this✝ : OrderBot { l // l ≤ m } := Subtype.orderBot (_ : ⊥ ≤ m)
this : OrderBot { l // l ≤ n } := Subtype.orderBot (_ : ⊥ ≤ n)
⊢ x = ⊥
obtain ⟨a, ha⟩ := x
case refine'_2.intro.mk
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
hb✝ : b < ↑(↑d { val := p, property := (_ : p ∣ m) })
this✝ : OrderBot { l // l ≤ m } := Subtype.orderBot (_ : ⊥ ≤ m)
this : OrderBot { l // l ≤ n } := Subtype.orderBot (_ : ⊥ ≤ n)
a : Associates M
ha : a ∈ Set.Iic m
hb : ↑(↑d { val := a, property := ha }) < ↑(↑d { val := p, property := (_ : p ∣ m) })
hx : ↑d { val := a, property := ha } = { val := b, property := (_ : b ≤ n) }
⊢ a = ⊥

case refine'_2.intro.mk.hbot
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
hb✝ : b < ↑(↑d { val := p, property := (_ : p ∣ m) })
this✝ : OrderBot { l // l ≤ m } := Subtype.orderBot (_ : ⊥ ≤ m)
this : OrderBot { l // l ≤ n } := Subtype.orderBot (_ : ⊥ ≤ n)
a : Associates M
ha : a ∈ Set.Iic m
hb : ↑(↑d { val := a, property := ha }) < ↑(↑d { val := p, property := (_ : p ∣ m) })
hx : ↑d { val := a, property := ha } = { val := b, property := (_ : b ≤ n) }
⊢ ⊥ ∈ Set.Iic m
case refine'_2.intro.mk
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
hb✝ : b < ↑(↑d { val := p, property := (_ : p ∣ m) })
this✝ : OrderBot { l // l ≤ m } := Subtype.orderBot (_ : ⊥ ≤ m)
this : OrderBot { l // l ≤ n } := Subtype.orderBot (_ : ⊥ ≤ n)
a : Associates M
ha : a ∈ Set.Iic m
hb : ↑(↑d { val := a, property := ha }) < ↑(↑d { val := p, property := (_ : p ∣ m) })
hx : ↑d { val := a, property := ha } = { val := b, property := (_ : b ≤ n) }
⊢ { val := a, property := ha } = ⊥
rw [Subtype.mk_eq_bot_iff]
no goals
case refine'_2.intro.mk.hbot
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
hb✝ : b < ↑(↑d { val := p, property := (_ : p ∣ m) })
this✝ : OrderBot { l // l ≤ m } := Subtype.orderBot (_ : ⊥ ≤ m)
this : OrderBot { l // l ≤ n } := Subtype.orderBot (_ : ⊥ ≤ n)
a : Associates M
ha : a ∈ Set.Iic m
hb : ↑(↑d { val := a, property := ha }) < ↑(↑d { val := p, property := (_ : p ∣ m) })
hx : ↑d { val := a, property := ha } = { val := b, property := (_ : b ≤ n) }
⊢ ⊥ ∈ Set.Iic m
simp
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
hb✝ : b < ↑(↑d { val := p, property := (_ : p ∣ m) })
x : ↑(Set.Iic m)
hb : ↑(↑d x) < ↑(↑d { val := p, property := (_ : p ∣ m) })
hx : ⊥ = { val := b, property := (_ : b ≤ n) }
this✝¹ : OrderBot { l // l ≤ m } := Subtype.orderBot (_ : ⊥ ≤ m)
this✝ : OrderBot { l // l ≤ n } := Subtype.orderBot (_ : ⊥ ≤ n)
this : x = ⊥
⊢ b = ⊥
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
hb✝ : b < ↑(↑d { val := p, property := (_ : p ∣ m) })
x : ↑(Set.Iic m)
hb : ↑(↑d x) < ↑(↑d { val := p, property := (_ : p ∣ m) })
hx : ↑d x = { val := b, property := (_ : b ≤ n) }
this✝¹ : OrderBot { l // l ≤ m } := Subtype.orderBot (_ : ⊥ ≤ m)
this✝ : OrderBot { l // l ≤ n } := Subtype.orderBot (_ : ⊥ ≤ n)
this : x = ⊥
⊢ b = ⊥
rw [this, OrderIso.map_bot d] at hx
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
hb✝ : b < ↑(↑d { val := p, property := (_ : p ∣ m) })
x : ↑(Set.Iic m)
hb : ↑(↑d x) < ↑(↑d { val := p, property := (_ : p ∣ m) })
hx : ⊥ = { val := b, property := (_ : b ≤ n) }
this✝¹ : OrderBot { l // l ≤ m } := Subtype.orderBot (_ : ⊥ ≤ m)
this✝ : OrderBot { l // l ≤ n } := Subtype.orderBot (_ : ⊥ ≤ n)
this : x = ⊥
⊢ ⊥ ∈ Set.Iic 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)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
hb✝ : b < ↑(↑d { val := p, property := (_ : p ∣ m) })
x : ↑(Set.Iic m)
hb : ↑(↑d x) < ↑(↑d { val := p, property := (_ : p ∣ m) })
hx : ⊥ = { val := b, property := (_ : b ≤ n) }
this✝¹ : OrderBot { l // l ≤ m } := Subtype.orderBot (_ : ⊥ ≤ m)
this✝ : OrderBot { l // l ≤ n } := Subtype.orderBot (_ : ⊥ ≤ n)
this : x = ⊥
⊢ b = ⊥
refine' (Subtype.mk_eq_bot_iff _ _).mp hx.symm
no goals
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
hb✝ : b < ↑(↑d { val := p, property := (_ : p ∣ m) })
x : ↑(Set.Iic m)
hb : ↑(↑d x) < ↑(↑d { val := p, property := (_ : p ∣ m) })
hx : ⊥ = { val := b, property := (_ : b ≤ n) }
this✝¹ : OrderBot { l // l ≤ m } := Subtype.orderBot (_ : ⊥ ≤ m)
this✝ : OrderBot { l // l ≤ n } := Subtype.orderBot (_ : ⊥ ≤ n)
this : x = ⊥
⊢ ⊥ ∈ Set.Iic n
simp
no goals
case refine'_2.intro.mk
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
hb✝ : b < ↑(↑d { val := p, property := (_ : p ∣ m) })
this✝ : OrderBot { l // l ≤ m } := Subtype.orderBot (_ : ⊥ ≤ m)
this : OrderBot { l // l ≤ n } := Subtype.orderBot (_ : ⊥ ≤ n)
a : Associates M
ha : a ∈ Set.Iic m
hb : ↑(↑d { val := a, property := ha }) < ↑(↑d { val := p, property := (_ : p ∣ m) })
hx : ↑d { val := a, property := ha } = { val := b, property := (_ : b ≤ n) }
⊢ a = ⊥
exact
  ((Associates.isAtom_iff <| Prime.ne_zero <| prime_of_normalized_factor p hp).mpr <|
        irreducible_of_normalized_factor p hp).right
    a (Subtype.mk_lt_mk.mp <| d.lt_iff_lt.mp hb)