apply groupInclusionHom_injective'
R : Type
inst✝⁷ : Ring R
inst✝⁶ : DecidableEq R
G✝ : Type
inst✝⁵ : Group G✝
inst✝⁴ : DecidableEq G✝
F : Type
inst✝³ : Field F
inst✝² : DecidableEq F
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
a₁✝ a₂✝ : G
⊢ ↑(groupInclusionHom G) a₁✝ = ↑(groupInclusionHom G) a₂✝ → a₁✝ = a₂✝
case hR
R : Type
inst✝⁷ : Ring R
inst✝⁶ : DecidableEq R
G✝ : Type
inst✝⁵ : Group G✝
inst✝⁴ : DecidableEq G✝
F : Type
inst✝³ : Field F
inst✝² : DecidableEq F
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
a₁✝ a₂✝ : G
⊢ 1 ≠ 0