case mk.mk
G : Type u_1
H : Type ?u.2672
A : Type ?u.2675
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
h₃ : ∀ {a : Additive G}, a ∈ s → -a ∈ s
h₁ : 0 ∈ s
h₂ : ∀ {a b : Additive G}, a ∈ s → b ∈ s → a + b ∈ s
⊢ IsSubgroup s
G : Type u_1
H : Type ?u.2672
A : Type ?u.2675
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
⊢ IsAddSubgroup s → IsSubgroup s
rintro ⟨⟨h₁, h₂⟩, h₃⟩
no goals
case mk.mk
G : Type u_1
H : Type ?u.2672
A : Type ?u.2675
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
h₃ : ∀ {a : Additive G}, a ∈ s → -a ∈ s
h₁ : 0 ∈ s
h₂ : ∀ {a b : Additive G}, a ∈ s → b ∈ s → a + b ∈ s
⊢ IsSubgroup s
exact @IsSubgroup.mk G _ _ ⟨h₁, @h₂⟩ @h₃