M : Type ?u.114054
N : Type ?u.114057
inst✝⁵ : Monoid M
inst✝⁴ : AddMonoid N
G : Type u_1
H✝ : Type ?u.114069
inst✝³ : Group G
inst✝² : AddGroup H✝
H : Subgroup G
inst✝¹ inst✝ : Group.FG { x // x ∈ H }
⊢ Group.rank { x // x ∈ H } = Group.rank { x // x ∈ H }
M : Type ?u.114054
N : Type ?u.114057
inst✝⁵ : Monoid M
inst✝⁴ : AddMonoid N
G : Type u_1
H✝ : Type ?u.114069
inst✝³ : Group G
inst✝² : AddGroup H✝
H K : Subgroup G
inst✝¹ : Group.FG { x // x ∈ H }
inst✝ : Group.FG { x // x ∈ K }
h : H = K
⊢ Group.rank { x // x ∈ H } = Group.rank { x // x ∈ K }
subst h
no goals
M : Type ?u.114054
N : Type ?u.114057
inst✝⁵ : Monoid M
inst✝⁴ : AddMonoid N
G : Type u_1
H✝ : Type ?u.114069
inst✝³ : Group G
inst✝² : AddGroup H✝
H : Subgroup G
inst✝¹ inst✝ : Group.FG { x // x ∈ H }
⊢ Group.rank { x // x ∈ H } = Group.rank { x // x ∈ H }
rfl