no goals
Γ : Type u_2
R : Type u_1
inst✝² : OrderedCancelAddCommMonoid Γ
Γ' : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ'
inst✝ : NonAssocSemiring R
f : Γ →+ Γ'
hfi : Injective ↑f
hf : ∀ (g g' : Γ), ↑f g ≤ ↑f g' ↔ g ≤ g'
r : R
⊢ ↑(single (↑{ toEmbedding := { toFun := ↑f, inj' := hfi }, map_rel_iff' := (_ : ∀ {a b : Γ}, ↑f a ≤ ↑f b ↔ a ≤ b) } 0))
      r =
    ↑C r
simp