M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
N : Type u_2
inst✝ : CancelCommMonoidWithZero N
m u : Associates M
n : Associates N
hu' : u ≤ m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hu : ↑(↑d { val := u, property := hu' }) = 1
⊢ ↑(↑(OrderIso.symm d)
        { val := ↑(↑d { val := u, property := hu' }),
          property := (_ : ↑(↑d { val := u, property := hu' }) ∈ Set.Iic n) }) =
    1
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
N : Type u_2
inst✝ : CancelCommMonoidWithZero N
m u : Associates M
n : Associates N
hu' : u ≤ m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hu : ↑(↑d { val := u, property := hu' }) = 1
⊢ u = 1
rw [show u = (d.symm ⟨d ⟨u, hu'⟩, (d ⟨u, hu'⟩).prop⟩) by
    simp only [Subtype.coe_eta, OrderIso.symm_apply_apply, Subtype.coe_mk]]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
N : Type u_2
inst✝ : CancelCommMonoidWithZero N
m u : Associates M
n : Associates N
hu' : u ≤ m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hu : ↑(↑d { val := u, property := hu' }) = 1
⊢ ↑(↑(OrderIso.symm d)
        { val := ↑(↑d { val := u, property := hu' }),
          property := (_ : ↑(↑d { val := u, property := hu' }) ∈ Set.Iic n) }) =
    ↑(↑(OrderIso.symm d) { val := 1, property := (_ : 1 ∣ n) })
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
N : Type u_2
inst✝ : CancelCommMonoidWithZero N
m u : Associates M
n : Associates N
hu' : u ≤ m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hu : ↑(↑d { val := u, property := hu' }) = 1
⊢ ↑(↑(OrderIso.symm d)
        { val := ↑(↑d { val := u, property := hu' }),
          property := (_ : ↑(↑d { val := u, property := hu' }) ∈ Set.Iic n) }) =
    1
conv_rhs => rw [← factor_orderIso_map_one_eq_bot d.symm]
no goals
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
N : Type u_2
inst✝ : CancelCommMonoidWithZero N
m u : Associates M
n : Associates N
hu' : u ≤ m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hu : ↑(↑d { val := u, property := hu' }) = 1
⊢ ↑(↑(OrderIso.symm d)
        { val := ↑(↑d { val := u, property := hu' }),
          property := (_ : ↑(↑d { val := u, property := hu' }) ∈ Set.Iic n) }) =
    ↑(↑(OrderIso.symm d) { val := 1, property := (_ : 1 ∣ n) })
congr
no goals
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
N : Type u_2
inst✝ : CancelCommMonoidWithZero N
m u : Associates M
n : Associates N
hu' : u ≤ m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hu : ↑(↑d { val := u, property := hu' }) = 1
⊢ u =
    ↑(↑(OrderIso.symm d)
        { val := ↑(↑d { val := u, property := hu' }),
          property := (_ : ↑(↑d { val := u, property := hu' }) ∈ Set.Iic n) })
simp only [Subtype.coe_eta, OrderIso.symm_apply_apply, Subtype.coe_mk]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
N : Type u_2
inst✝ : CancelCommMonoidWithZero N
m u : Associates M
n : Associates N
hu' : u ≤ m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hu : u = 1
⊢ ↑(↑d { val := 1, property := (_ : (fun x => x ∈ Set.Iic m) 1) }) = 1
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
N : Type u_2
inst✝ : CancelCommMonoidWithZero N
m u : Associates M
n : Associates N
hu' : u ≤ m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hu : u = 1
⊢ ↑(↑d { val := u, property := hu' }) = 1
simp_rw [hu]
no goals
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
N : Type u_2
inst✝ : CancelCommMonoidWithZero N
m u : Associates M
n : Associates N
hu' : u ≤ m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hu : u = 1
⊢ ↑(↑d { val := 1, property := (_ : (fun x => x ∈ Set.Iic m) 1) }) = 1
conv_rhs =>  rw [← factor_orderIso_map_one_eq_bot d]