α : Type u_1
inst✝ : CancelCommMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ b : { x // x ∈ s }
c d : α
h : (fun a => mk a b) c = (fun a => mk a b) d
this : Nonempty { x // x ∈ s }
⊢ c = d
α : Type u_1
inst✝ : CancelCommMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ b : { x // x ∈ s }
c d : α
h : (fun a => mk a b) c = (fun a => mk a b) d
⊢ c = d
have : Nonempty s := One.nonempty
no goals
α : Type u_1
inst✝ : CancelCommMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ b : { x // x ∈ s }
c d : α
h : (fun a => mk a b) c = (fun a => mk a b) d
this : Nonempty { x // x ∈ s }
⊢ c = d
simpa [-mk_eq_monoidOf_mk', mk_eq_mk_iff, r_iff_exists] using h