case intro.intro
α : Type ?u.101125
G : Type u_1
A : Type ?u.101131
S : Type ?u.101134
inst✝³ : Group G
inst✝² : AddGroup A
s : Set G
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction α G
P H : Subgroup G
hP : P ≤ H
h : { x // x ∈ H }
g : G
hg : g ∈ ↑P
⊢ ↑(↑(MulDistribMulAction.toMonoidEnd ((fun x => MulAut G) ↑h) G) (↑MulAut.conj ↑h)) g ∈ H
α : Type ?u.101125
G : Type u_1
A : Type ?u.101131
S : Type ?u.101134
inst✝³ : Group G
inst✝² : AddGroup A
s : Set G
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction α G
P H : Subgroup G
hP : P ≤ H
h : { x // x ∈ H }
⊢ ↑MulAut.conj ↑h • P ≤ H
rintro - ⟨g, hg, rfl⟩
no goals
case intro.intro
α : Type ?u.101125
G : Type u_1
A : Type ?u.101131
S : Type ?u.101134
inst✝³ : Group G
inst✝² : AddGroup A
s : Set G
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction α G
P H : Subgroup G
hP : P ≤ H
h : { x // x ∈ H }
g : G
hg : g ∈ ↑P
⊢ ↑(↑(MulDistribMulAction.toMonoidEnd ((fun x => MulAut G) ↑h) G) (↑MulAut.conj ↑h)) g ∈ H
exact H.mul_mem (H.mul_mem h.2 (hP hg)) (H.inv_mem h.2)