case mpr.intro.intro
G : Type u_1
G' : Type ?u.10955
inst✝⁶ : Group G
inst✝⁵ : Group G'
A : Type ?u.10964
inst✝⁴ : AddGroup A
M : Type ?u.10970
S : Type u_2
inst✝³ : DivInvMonoid M
inst✝² : SetLike S M
hSM : SubgroupClass S M
H K : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
P : G → Prop
x : G
x_in : x ∈ H
hx : P x
⊢ ∃ x, x ∈ H ∧ P x⁻¹
case mpr
G : Type u_1
G' : Type ?u.10955
inst✝⁶ : Group G
inst✝⁵ : Group G'
A : Type ?u.10964
inst✝⁴ : AddGroup A
M : Type ?u.10970
S : Type u_2
inst✝³ : DivInvMonoid M
inst✝² : SetLike S M
hSM : SubgroupClass S M
H K : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
P : G → Prop
⊢ (∃ x, x ∈ H ∧ P x) → ∃ x, x ∈ H ∧ P x⁻¹
rintro ⟨x, x_in, hx⟩
no goals
case mpr.intro.intro
G : Type u_1
G' : Type ?u.10955
inst✝⁶ : Group G
inst✝⁵ : Group G'
A : Type ?u.10964
inst✝⁴ : AddGroup A
M : Type ?u.10970
S : Type u_2
inst✝³ : DivInvMonoid M
inst✝² : SetLike S M
hSM : SubgroupClass S M
H K : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
P : G → Prop
x : G
x_in : x ∈ H
hx : P x
⊢ ∃ x, x ∈ H ∧ P x⁻¹
exact ⟨x⁻¹, inv_mem x_in, by simp [hx]⟩
no goals
G : Type u_1
G' : Type ?u.10955
inst✝⁶ : Group G
inst✝⁵ : Group G'
A : Type ?u.10964
inst✝⁴ : AddGroup A
M : Type ?u.10970
S : Type u_2
inst✝³ : DivInvMonoid M
inst✝² : SetLike S M
hSM : SubgroupClass S M
H K : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
P : G → Prop
x : G
x_in : x ∈ H
hx : P x
⊢ P x⁻¹⁻¹
simp [hx]