Theorem: ringInclusionHom_injective' (UnitConjecture/GroupRing.lean)

State before:
R : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
G✝ : Type
inst✝³ : Group G✝
inst✝² : DecidableEq G✝
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
⊢ Function.Injective ↑(ringInclusionHom G)
Tactic:
intro _ _
State after:
R : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
G✝ : Type
inst✝³ : Group G✝
inst✝² : DecidableEq G✝
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
a₁✝ a₂✝ : R
⊢ ↑(ringInclusionHom G) a₁✝ = ↑(ringInclusionHom G) a₂✝ → a₁✝ = a₂✝

State before:
R : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
G✝ : Type
inst✝³ : Group G✝
inst✝² : DecidableEq G✝
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
a₁✝ a₂✝ : R
⊢ ↑(ringInclusionHom G) a₁✝ = ↑(ringInclusionHom G) a₂✝ → a₁✝ = a₂✝
Tactic:
apply coeffInclusion_injective
State after:
no goals