-- Mathlib/RingTheory/ChainOfDivisors.lean
theorem factor_orderIso_map_one_eq_bot {m : Associates M} {n : Associates N}
    (d : { l : Associates M // l ≤ m } ≃o { l : Associates N // l ≤ n }) :
    (d ⟨1, one_dvd m⟩ : Associates N) = 1

Proof state:
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
N : Type u_2
inst✝ : CancelCommMonoidWithZero N
m : Associates M
n : Associates N
d : { l // l ≤ m } ≃o { l // l ≤ n }
this✝ : OrderBot { l // l ≤ m } := Subtype.orderBot ⋯
this : OrderBot { l // l ≤ n } := Subtype.orderBot ⋯
⊢ ↑(d ⟨1, ⋯⟩) = 1

Tactic:
simp only [← Associates.bot_eq_one, Subtype.mk_bot, bot_le, Subtype.coe_eq_bot_iff]

Result:
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
N : Type u_2
inst✝ : CancelCommMonoidWithZero N
m : Associates M
n : Associates N
d : { l // l ≤ m } ≃o { l // l ≤ n }
this✝ : OrderBot { l // l ≤ m } := Subtype.orderBot ⋯
this : OrderBot { l // l ≤ n } := Subtype.orderBot ⋯
⊢ d ⊥ = ⊥

Proof state:
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
N : Type u_2
inst✝ : CancelCommMonoidWithZero N
m : Associates M
n : Associates N
d : { l // l ≤ m } ≃o { l // l ≤ n }
⊢ ↑(d ⟨1, ⋯⟩) = 1

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

Result:
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
N : Type u_2
inst✝ : CancelCommMonoidWithZero N
m : Associates M
n : Associates N
d : { l // l ≤ m } ≃o { l // l ≤ n }
this : OrderBot { l // l ≤ m } := Subtype.orderBot ⋯
⊢ ↑(d ⟨1, ⋯⟩) = 1

Proof state:
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
N : Type u_2
inst✝ : CancelCommMonoidWithZero N
m : Associates M
n : Associates N
d : { l // l ≤ m } ≃o { l // l ≤ n }
this✝¹ : OrderBot { l // l ≤ m } := Subtype.orderBot ⋯
this✝ : OrderBot { l // l ≤ n } := Subtype.orderBot ⋯
this : BotHomClass ({ l // l ≤ m } ≃o { l // l ≤ n }) { l // l ≤ m } { l // l ≤ n } := OrderIsoClass.toBotHomClass
⊢ d ⊥ = ⊥

Tactic:
exact map_bot d

Result:
no goals

Proof state:
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
N : Type u_2
inst✝ : CancelCommMonoidWithZero N
m : Associates M
n : Associates N
d : { l // l ≤ m } ≃o { l // l ≤ n }
this : OrderBot { l // l ≤ m } := Subtype.orderBot ⋯
⊢ ↑(d ⟨1, ⋯⟩) = 1

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

Result:
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
N : Type u_2
inst✝ : CancelCommMonoidWithZero N
m : Associates M
n : Associates N
d : { l // l ≤ m } ≃o { l // l ≤ n }
this✝ : OrderBot { l // l ≤ m } := Subtype.orderBot ⋯
this : OrderBot { l // l ≤ n } := Subtype.orderBot ⋯
⊢ ↑(d ⟨1, ⋯⟩) = 1

Proof state:
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
N : Type u_2
inst✝ : CancelCommMonoidWithZero N
m : Associates M
n : Associates N
d : { l // l ≤ m } ≃o { l // l ≤ n }
this✝ : OrderBot { l // l ≤ m } := Subtype.orderBot ⋯
this : OrderBot { l // l ≤ n } := Subtype.orderBot ⋯
⊢ d ⊥ = ⊥

Tactic:
letI : BotHomClass ({ l // l ≤ m } ≃o { l // l ≤ n }) _ _ := OrderIsoClass.toBotHomClass

Result:
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
N : Type u_2
inst✝ : CancelCommMonoidWithZero N
m : Associates M
n : Associates N
d : { l // l ≤ m } ≃o { l // l ≤ n }
this✝¹ : OrderBot { l // l ≤ m } := Subtype.orderBot ⋯
this✝ : OrderBot { l // l ≤ n } := Subtype.orderBot ⋯
this : BotHomClass ({ l // l ≤ m } ≃o { l // l ≤ n }) { l // l ≤ m } { l // l ≤ n } := OrderIsoClass.toBotHomClass
⊢ d ⊥ = ⊥