case mk.mk
G : Type ?u.3681
H : Type ?u.3684
A : Type u_1
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set A
h₃ : ∀ {a : Multiplicative A}, a ∈ s → a⁻¹ ∈ s
h₁ : 1 ∈ s
h₂ : ∀ {a b : Multiplicative A}, a ∈ s → b ∈ s → a * b ∈ s
⊢ IsAddSubgroup s
G : Type ?u.3681
H : Type ?u.3684
A : Type u_1
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set A
⊢ IsSubgroup s → IsAddSubgroup s
rintro ⟨⟨h₁, h₂⟩, h₃⟩
no goals
case mk.mk
G : Type ?u.3681
H : Type ?u.3684
A : Type u_1
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set A
h₃ : ∀ {a : Multiplicative A}, a ∈ s → a⁻¹ ∈ s
h₁ : 1 ∈ s
h₂ : ∀ {a b : Multiplicative A}, a ∈ s → b ∈ s → a * b ∈ s
⊢ IsAddSubgroup s
exact @IsAddSubgroup.mk A _ _ ⟨h₁, @h₂⟩ @h₃