-- Mathlib/RingTheory/ChainOfDivisors.lean
theorem map_prime_of_factor_orderIso {m p : Associates M} {n : Associates N} (hn : n ≠ 0)
    (hp : p ∈ normalizedFactors m) (d : Set.Iic m ≃o Set.Iic n) :
    Prime (d ⟨p, dvd_of_mem_normalizedFactors hp⟩ : Associates N)

Proof state:
case refine_2.intro
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
N : Type u_2
inst✝² : CancelCommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid 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 ⟨p, ⋯⟩)
x : ↑(Set.Iic m)
hb : ↑(d x) < ↑(d ⟨p, ⋯⟩)
hx : d x = ⟨b, ⋯⟩
this : OrderBot { l // l ≤ m } := Subtype.orderBot ⋯
⊢ b = ⊥

Tactic:
letI : OrderBot { l : Associates N // l ≤ n } := Subtype.orderBot bot_le

Result:
case refine_2.intro
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
N : Type u_2
inst✝² : CancelCommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid 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 ⟨p, ⋯⟩)
x : ↑(Set.Iic m)
hb : ↑(d x) < ↑(d ⟨p, ⋯⟩)
hx : d x = ⟨b, ⋯⟩
this✝ : OrderBot { l // l ≤ m } := Subtype.orderBot ⋯
this : OrderBot { l // l ≤ n } := Subtype.orderBot ⋯
⊢ b = ⊥

Proof state:
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
N : Type u_2
inst✝² : CancelCommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid 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 ⟨p, ⋯⟩)

Tactic:
refine (Associates.isAtom_iff <|
  ne_zero_of_dvd_ne_zero hn (d ⟨p, _⟩).prop).mp ⟨?_, fun b hb => ?_⟩

Result:
case refine_1
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
N : Type u_2
inst✝² : CancelCommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
⊢ ↑(d ⟨p, ⋯⟩) ≠ ⊥

case refine_2
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
N : Type u_2
inst✝² : CancelCommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid 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 ⟨p, ⋯⟩)
⊢ b = ⊥

Proof state:
case refine_2.intro
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
N : Type u_2
inst✝² : CancelCommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid 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 ⟨p, ⋯⟩)
x : ↑(Set.Iic m)
hb : ↑(d x) < ↑(d ⟨p, ⋯⟩)
hx : d x = ⟨b, ⋯⟩
⊢ b = ⊥

Tactic:
letI : OrderBot { l : Associates M // l ≤ m } := Subtype.orderBot bot_le

Result:
case refine_2.intro
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
N : Type u_2
inst✝² : CancelCommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid 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 ⟨p, ⋯⟩)
x : ↑(Set.Iic m)
hb : ↑(d x) < ↑(d ⟨p, ⋯⟩)
hx : d x = ⟨b, ⋯⟩
this : OrderBot { l // l ≤ m } := Subtype.orderBot ⋯
⊢ b = ⊥

Proof state:
case refine_1
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
N : Type u_2
inst✝² : CancelCommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
⊢ ↑(d ⟨p, ⋯⟩) ≠ ⊥

Tactic:
rw [Ne, ← Associates.isUnit_iff_eq_bot, Associates.isUnit_iff_eq_one,
  coe_factor_orderIso_map_eq_one_iff _ d]

Result:
case refine_1
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
N : Type u_2
inst✝² : CancelCommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid 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

Proof state:
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
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 ⟨p, ⋯⟩)
this✝ : OrderBot { l // l ≤ m } := Subtype.orderBot ⋯
this : OrderBot { l // l ≤ n } := Subtype.orderBot ⋯
a : Associates M
ha : a ∈ Set.Iic m
hb : ↑(d ⟨a, ha⟩) < ↑(d ⟨p, ⋯⟩)
hx : d ⟨a, ha⟩ = ⟨b, ⋯⟩
⊢ ⟨a, ha⟩ = ⊥

Tactic:
rw [Subtype.mk_eq_bot_iff]

Result:
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
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 ⟨p, ⋯⟩)
this✝ : OrderBot { l // l ≤ m } := Subtype.orderBot ⋯
this : OrderBot { l // l ≤ n } := Subtype.orderBot ⋯
a : Associates M
ha : a ∈ Set.Iic m
hb : ↑(d ⟨a, ha⟩) < ↑(d ⟨p, ⋯⟩)
hx : d ⟨a, ha⟩ = ⟨b, ⋯⟩
⊢ 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
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 ⟨p, ⋯⟩)
this✝ : OrderBot { l // l ≤ m } := Subtype.orderBot ⋯
this : OrderBot { l // l ≤ n } := Subtype.orderBot ⋯
a : Associates M
ha : a ∈ Set.Iic m
hb : ↑(d ⟨a, ha⟩) < ↑(d ⟨p, ⋯⟩)
hx : d ⟨a, ha⟩ = ⟨b, ⋯⟩
⊢ ⊥ ∈ Set.Iic m

Proof state:
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
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 ⟨p, ⋯⟩)
this✝ : OrderBot { l // l ≤ m } := Subtype.orderBot ⋯
this : OrderBot { l // l ≤ n } := Subtype.orderBot ⋯
a : Associates M
ha : a ∈ Set.Iic m
hb : ↑(d ⟨a, ha⟩) < ↑(d ⟨p, ⋯⟩)
hx : d ⟨a, ha⟩ = ⟨b, ⋯⟩
⊢ a = ⊥

Tactic:
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)

Result:
no goals

Proof state:
case refine_2.intro
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
N : Type u_2
inst✝² : CancelCommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid 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 ⟨p, ⋯⟩)
x : ↑(Set.Iic m)
hb : ↑(d x) < ↑(d ⟨p, ⋯⟩)
hx : d x = ⟨b, ⋯⟩
this✝ : OrderBot { l // l ≤ m } := Subtype.orderBot ⋯
this : OrderBot { l // l ≤ n } := Subtype.orderBot ⋯
⊢ x = ⊥

Tactic:
obtain ⟨a, ha⟩ := x

Result:
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
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 ⟨p, ⋯⟩)
this✝ : OrderBot { l // l ≤ m } := Subtype.orderBot ⋯
this : OrderBot { l // l ≤ n } := Subtype.orderBot ⋯
a : Associates M
ha : a ∈ Set.Iic m
hb : ↑(d ⟨a, ha⟩) < ↑(d ⟨p, ⋯⟩)
hx : d ⟨a, ha⟩ = ⟨b, ⋯⟩
⊢ ⟨a, ha⟩ = ⊥