Theorem: Tutorial.Subgroup.coe_one (Tutorial/Advanced/Algebra/Lecture5.lean)

State before:
G H : Type
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
K : Subgroup G
⊢ 1 ∈ K
Tactic:
simp
State after:
no goals