α : Type u_1
inst✝ : CancelCommMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : { x // x ∈ s }
this : Nonempty { x // x ∈ s }
⊢ mk a₁ a₂ = mk b₁ b₂ ↔ ↑b₂ * a₁ = ↑a₂ * b₁
α : Type u_1
inst✝ : CancelCommMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : { x // x ∈ s }
⊢ mk a₁ a₂ = mk b₁ b₂ ↔ ↑b₂ * a₁ = ↑a₂ * b₁
have : Nonempty s := One.nonempty
no goals
α : Type u_1
inst✝ : CancelCommMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : { x // x ∈ s }
this : Nonempty { x // x ∈ s }
⊢ mk a₁ a₂ = mk b₁ b₂ ↔ ↑b₂ * a₁ = ↑a₂ * b₁
simp_rw [mk_eq_mk_iff, r_iff_exists, mul_left_cancel_iff, exists_const]