Theorem: l1_2_2_bc (AlgebraI/Subgroups.lean)

State before:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ Set.Nonempty ↑H ∧ ∀ (h₁ h₂ : G), h₁ ∈ ↑H → h₂ ∈ ↑H → h₁ * h₂⁻¹ ∈ ↑H
Tactic:
refine' ⟨⟨1, SetLike.mem_coe.mpr (one_mem _)⟩, fun h₁ h₂ h₁mem h₂mem => _⟩
State after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h₁ h₂ : G
h₁mem : h₁ ∈ ↑H
h₂mem : h₂ ∈ ↑H
⊢ h₁ * h₂⁻¹ ∈ ↑H

State before:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h₁ h₂ : G
h₁mem : h₁ ∈ ↑H
h₂mem : h₂ ∈ ↑H
⊢ h₁ * h₂⁻¹ ∈ ↑H
Tactic:
rw [SetLike.mem_coe] at h₁mem h₂mem ⊢
State after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h₁ h₂ : G
h₁mem : h₁ ∈ H
h₂mem : h₂ ∈ H
⊢ h₁ * h₂⁻¹ ∈ H

State before:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h₁ h₂ : G
h₁mem : h₁ ∈ H
h₂mem : h₂ ∈ H
⊢ h₁ * h₂⁻¹ ∈ H
Tactic:
exact Subgroup.mul_mem _ h₁mem (Subgroup.inv_mem _ h₂mem)
State after:
no goals