Theorem: groupInclusionHom_injective' (UnitConjecture/GroupRing.lean)

State before:
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
hR : 1 ≠ 0
⊢ Function.Injective ↑(groupInclusionHom G)
Tactic:
intro _ _
State after:
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
hR : 1 ≠ 0
a₁✝ a₂✝ : G
⊢ ↑(groupInclusionHom G) a₁✝ = ↑(groupInclusionHom G) a₂✝ → a₁✝ = a₂✝

State before:
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
hR : 1 ≠ 0
a₁✝ a₂✝ : G
⊢ ↑(groupInclusionHom G) a₁✝ = ↑(groupInclusionHom G) a₂✝ → a₁✝ = a₂✝
Tactic:
apply baseInclusion_injective (1 : R) hR (X := G)
State after:
no goals