case mk
G : Type u_1
H : Type ?u.20782
A : Type ?u.20785
a a₁ a₂ b c : G
inst✝ : Group G
s : Set G
h₁ : IsAddSubgroup s
h₂ : ∀ (n : Additive G), n ∈ s → ∀ (g : Additive G), g + n + -g ∈ s
⊢ IsNormalSubgroup s
G : Type u_1
H : Type ?u.20782
A : Type ?u.20785
a a₁ a₂ b c : G
inst✝ : Group G
s : Set G
⊢ IsNormalAddSubgroup s → IsNormalSubgroup s
rintro ⟨h₁, h₂⟩
no goals
case mk
G : Type u_1
H : Type ?u.20782
A : Type ?u.20785
a a₁ a₂ b c : G
inst✝ : Group G
s : Set G
h₁ : IsAddSubgroup s
h₂ : ∀ (n : Additive G), n ∈ s → ∀ (g : Additive G), g + n + -g ∈ s
⊢ IsNormalSubgroup s
exact @IsNormalSubgroup.mk G _ _ (Additive.isAddSubgroup_iff.1 h₁) @h₂