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 (_ : ⊥ ≤ m)
⊢ ↑(↑d { val := 1, property := (_ : 1 ∣ m) }) = 1
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 { val := 1, property := (_ : 1 ∣ m) }) = 1
letI : OrderBot { l : Associates M // l ≤ m } := Subtype.orderBot bot_le
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 (_ : ⊥ ≤ m)
this : OrderBot { l // l ≤ n } := Subtype.orderBot (_ : ⊥ ≤ n)
⊢ ↑(↑d { val := 1, property := (_ : 1 ∣ m) }) = 1
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 (_ : ⊥ ≤ m)
⊢ ↑(↑d { val := 1, property := (_ : 1 ∣ m) }) = 1
letI : OrderBot { l : Associates N // l ≤ n } := Subtype.orderBot bot_le
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 (_ : ⊥ ≤ m)
this : OrderBot { l // l ≤ n } := Subtype.orderBot (_ : ⊥ ≤ n)
⊢ ↑d ⊥ = ⊥
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 (_ : ⊥ ≤ m)
this : OrderBot { l // l ≤ n } := Subtype.orderBot (_ : ⊥ ≤ n)
⊢ ↑(↑d { val := 1, property := (_ : 1 ∣ m) }) = 1
simp only [← Associates.bot_eq_one, Subtype.mk_bot, bot_le, Subtype.coe_eq_bot_iff]
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 (_ : ⊥ ≤ m)
this✝ : OrderBot { l // l ≤ n } := Subtype.orderBot (_ : ⊥ ≤ n)
this : BotHomClass ({ l // l ≤ m } ≃o { l // l ≤ n }) { l // l ≤ m } { l // l ≤ n } := OrderIsoClass.toBotHomClass
⊢ ↑d ⊥ = ⊥
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 (_ : ⊥ ≤ m)
this : OrderBot { l // l ≤ n } := Subtype.orderBot (_ : ⊥ ≤ n)
⊢ ↑d ⊥ = ⊥
letI : BotHomClass ({ l // l ≤ m } ≃o { l // l ≤ n }) _ _ := OrderIsoClass.toBotHomClass
no goals
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 (_ : ⊥ ≤ m)
this✝ : OrderBot { l // l ≤ n } := Subtype.orderBot (_ : ⊥ ≤ n)
this : BotHomClass ({ l // l ≤ m } ≃o { l // l ≤ n }) { l // l ≤ m } { l // l ≤ n } := OrderIsoClass.toBotHomClass
⊢ ↑d ⊥ = ⊥
exact map_bot d