case refine'_1
α : Type ?u.110756
G : Type u_1
A : Type ?u.110762
S : Type ?u.110765
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 • subgroupOf P H ≤ subgroupOf (↑MulAut.conj ↑h • P) H

case refine'_2
α : Type ?u.110756
G : Type u_1
A : Type ?u.110762
S : Type ?u.110765
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 }
⊢ subgroupOf (↑MulAut.conj ↑h • P) H ≤ ↑MulAut.conj h • subgroupOf P H
α : Type ?u.110756
G : Type u_1
A : Type ?u.110762
S : Type ?u.110765
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 • subgroupOf P H = subgroupOf (↑MulAut.conj ↑h • P) H
refine' le_antisymm _ _
case refine'_1.intro.intro
α : Type ?u.110756
G : Type u_1
A : Type ?u.110762
S : Type ?u.110765
inst✝³ : Group G
inst✝² : AddGroup A
s : Set G
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction α G
P H : Subgroup G
hP : P ≤ H
h g : { x // x ∈ H }
hg : g ∈ ↑(subgroupOf P H)
⊢ ↑(↑(MulDistribMulAction.toMonoidEnd ((fun x => MulAut { x // x ∈ H }) h) { x // x ∈ H }) (↑MulAut.conj h)) g ∈
    subgroupOf (↑MulAut.conj ↑h • P) H
case refine'_1
α : Type ?u.110756
G : Type u_1
A : Type ?u.110762
S : Type ?u.110765
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 • subgroupOf P H ≤ subgroupOf (↑MulAut.conj ↑h • P) H
rintro - ⟨g, hg, rfl⟩
no goals
case refine'_1.intro.intro
α : Type ?u.110756
G : Type u_1
A : Type ?u.110762
S : Type ?u.110765
inst✝³ : Group G
inst✝² : AddGroup A
s : Set G
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction α G
P H : Subgroup G
hP : P ≤ H
h g : { x // x ∈ H }
hg : g ∈ ↑(subgroupOf P H)
⊢ ↑(↑(MulDistribMulAction.toMonoidEnd ((fun x => MulAut { x // x ∈ H }) h) { x // x ∈ H }) (↑MulAut.conj h)) g ∈
    subgroupOf (↑MulAut.conj ↑h • P) H
exact ⟨g, hg, rfl⟩
case refine'_2.intro.intro
α : Type ?u.110756
G : Type u_1
A : Type ?u.110762
S : Type ?u.110765
inst✝³ : Group G
inst✝² : AddGroup A
s : Set G
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction α G
P H : Subgroup G
hP : P ≤ H
h p : { x // x ∈ H }
g : G
hg : g ∈ ↑P
hp : ↑(↑(MulDistribMulAction.toMonoidEnd ((fun x => MulAut G) ↑h) G) (↑MulAut.conj ↑h)) g = ↑(Subgroup.subtype H) p
⊢ p ∈ ↑MulAut.conj h • subgroupOf P H
case refine'_2
α : Type ?u.110756
G : Type u_1
A : Type ?u.110762
S : Type ?u.110765
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 }
⊢ subgroupOf (↑MulAut.conj ↑h • P) H ≤ ↑MulAut.conj h • subgroupOf P H
rintro p ⟨g, hg, hp⟩
no goals
case refine'_2.intro.intro
α : Type ?u.110756
G : Type u_1
A : Type ?u.110762
S : Type ?u.110765
inst✝³ : Group G
inst✝² : AddGroup A
s : Set G
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction α G
P H : Subgroup G
hP : P ≤ H
h p : { x // x ∈ H }
g : G
hg : g ∈ ↑P
hp : ↑(↑(MulDistribMulAction.toMonoidEnd ((fun x => MulAut G) ↑h) G) (↑MulAut.conj ↑h)) g = ↑(Subgroup.subtype H) p
⊢ p ∈ ↑MulAut.conj h • subgroupOf P H
exact ⟨⟨g, hP hg⟩, hg, Subtype.ext hp⟩