-- Mathlib/GroupTheory/GroupAction/Basic.lean
@[to_additive]
lemma orbitRel_subgroupOf (H K : Subgroup G) :
    orbitRel (H.subgroupOf K) α = orbitRel (H ⊓ K : Subgroup G) α

Proof state:
case a.refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
x b✝ : α
h : x ∈ orbit (↥(Subgroup.map K.subtype (H.subgroupOf K))) b✝
⊢ x ∈ orbit (↥(H.subgroupOf K)) b✝

Tactic:
rcases h with ⟨⟨gv, gp⟩, rfl⟩

Result:
case a.refine_2.intro.mk
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
b✝ : α
gv : G
gp : gv ∈ Subgroup.map K.subtype (H.subgroupOf K)
⊢ (fun m => m • b✝) ⟨gv, gp⟩ ∈ orbit (↥(H.subgroupOf K)) b✝

Proof state:
case a.refine_2.intro.mk.refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
b✝ : α
gv : G
gp✝ : gv ∈ Subgroup.map K.subtype (H.subgroupOf K)
gp : gv ∈ H ∧ gv ∈ K
⊢ ⟨gv, ⋯⟩ ∈ H.subgroupOf K

Tactic:
simp only [Subgroup.mem_subgroupOf]

Result:
case a.refine_2.intro.mk.refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
b✝ : α
gv : G
gp✝ : gv ∈ Subgroup.map K.subtype (H.subgroupOf K)
gp : gv ∈ H ∧ gv ∈ K
⊢ gv ∈ H

Proof state:
case a
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
x b✝ : α
⊢ (orbitRel (↥(H.subgroupOf K)) α) x b✝ ↔ (orbitRel (↥(Subgroup.map K.subtype (H.subgroupOf K))) α) x b✝

Tactic:
simp_rw [orbitRel_apply]

Result:
case a
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
x b✝ : α
⊢ x ∈ orbit (↥(H.subgroupOf K)) b✝ ↔ x ∈ orbit (↥(Subgroup.map K.subtype (H.subgroupOf K))) b✝

Proof state:
case a.refine_1
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
x b✝ : α
h : x ∈ orbit (↥(H.subgroupOf K)) b✝
⊢ x ∈ orbit (↥(Subgroup.map K.subtype (H.subgroupOf K))) b✝

Tactic:
rcases h with ⟨⟨gv, gp⟩, rfl⟩

Result:
case a.refine_1.intro.mk
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
b✝ : α
gv : ↥K
gp : gv ∈ H.subgroupOf K
⊢ (fun m => m • b✝) ⟨gv, gp⟩ ∈ orbit (↥(Subgroup.map K.subtype (H.subgroupOf K))) b✝

Proof state:
case a.refine_1.intro.mk
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
b✝ : α
gv : ↥K
gp : gv ∈ H.subgroupOf K
⊢ ↑gv ∈ Subgroup.map K.subtype (H.subgroupOf K)

Tactic:
simpa using gp

Result:
no goals

Proof state:
case a.refine_2.intro.mk.refine_1
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
b✝ : α
gv : G
gp✝ : gv ∈ Subgroup.map K.subtype (H.subgroupOf K)
gp : gv ∈ H ∧ gv ∈ K
⊢ gv ∈ K

Tactic:
exact gp.2

Result:
no goals

Proof state:
case a.refine_2.intro.mk.refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
b✝ : α
gv : G
gp✝ : gv ∈ Subgroup.map K.subtype (H.subgroupOf K)
gp : gv ∈ H ∧ gv ∈ K
⊢ gv ∈ H

Tactic:
exact gp.1

Result:
no goals

Proof state:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
⊢ orbitRel (↥(H.subgroupOf K)) α = orbitRel (↥(H ⊓ K)) α

Tactic:
rw [← Subgroup.subgroupOf_map_subtype]

Result:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
⊢ orbitRel (↥(H.subgroupOf K)) α = orbitRel (↥(Subgroup.map K.subtype (H.subgroupOf K))) α

Proof state:
case a.refine_2.intro.mk
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
b✝ : α
gv : G
gp✝ : gv ∈ Subgroup.map K.subtype (H.subgroupOf K)
gp : gv ∈ H ∧ gv ∈ K
⊢ ⟨gv, gp✝⟩ • b✝ ∈ orbit (↥(H.subgroupOf K)) b✝

Tactic:
refine mem_orbit _ (⟨⟨gv, ?_⟩, ?_⟩ : H.subgroupOf K)

Result:
case a.refine_2.intro.mk.refine_1
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
b✝ : α
gv : G
gp✝ : gv ∈ Subgroup.map K.subtype (H.subgroupOf K)
gp : gv ∈ H ∧ gv ∈ K
⊢ gv ∈ K

case a.refine_2.intro.mk.refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
b✝ : α
gv : G
gp✝ : gv ∈ Subgroup.map K.subtype (H.subgroupOf K)
gp : gv ∈ H ∧ gv ∈ K
⊢ ⟨gv, ?a.refine_2.intro.mk.refine_1✝⟩ ∈ H.subgroupOf K

Proof state:
case a.refine_1.intro.mk
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
b✝ : α
gv : ↥K
gp : gv ∈ H.subgroupOf K
⊢ (fun m => m • b✝) ⟨gv, gp⟩ ∈ orbit (↥(Subgroup.map K.subtype (H.subgroupOf K))) b✝

Tactic:
simp only [Submonoid.mk_smul]

Result:
case a.refine_1.intro.mk
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
b✝ : α
gv : ↥K
gp : gv ∈ H.subgroupOf K
⊢ ⟨gv, gp⟩ • b✝ ∈ orbit (↥(Subgroup.map K.subtype (H.subgroupOf K))) b✝

Proof state:
case a.refine_2.intro.mk
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
b✝ : α
gv : G
gp : gv ∈ Subgroup.map K.subtype (H.subgroupOf K)
⊢ ⟨gv, gp⟩ • b✝ ∈ orbit (↥(H.subgroupOf K)) b✝

Tactic:
simp only [Subgroup.subgroupOf_map_subtype, Subgroup.mem_inf] at gp

Result:
case a.refine_2.intro.mk
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
b✝ : α
gv : G
gp✝ : gv ∈ Subgroup.map K.subtype (H.subgroupOf K)
gp : gv ∈ H ∧ gv ∈ K
⊢ ⟨gv, gp✝⟩ • b✝ ∈ orbit (↥(H.subgroupOf K)) b✝

Proof state:
case a.refine_1.intro.mk
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
b✝ : α
gv : ↥K
gp : gv ∈ H.subgroupOf K
⊢ ⟨gv, gp⟩ • b✝ ∈ orbit (↥(Subgroup.map K.subtype (H.subgroupOf K))) b✝

Tactic:
refine mem_orbit _ (⟨gv, ?_⟩ : Subgroup.map K.subtype (H.subgroupOf K))

Result:
case a.refine_1.intro.mk
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
b✝ : α
gv : ↥K
gp : gv ∈ H.subgroupOf K
⊢ ↑gv ∈ Subgroup.map K.subtype (H.subgroupOf K)

Proof state:
case a
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
x b✝ : α
⊢ x ∈ orbit (↥(H.subgroupOf K)) b✝ ↔ x ∈ orbit (↥(Subgroup.map K.subtype (H.subgroupOf K))) b✝

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Result:
case a.refine_1
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
x b✝ : α
h : x ∈ orbit (↥(H.subgroupOf K)) b✝
⊢ x ∈ orbit (↥(Subgroup.map K.subtype (H.subgroupOf K))) b✝

case a.refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
x b✝ : α
h : x ∈ orbit (↥(Subgroup.map K.subtype (H.subgroupOf K))) b✝
⊢ x ∈ orbit (↥(H.subgroupOf K)) b✝

Proof state:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
⊢ orbitRel (↥(H.subgroupOf K)) α = orbitRel (↥(Subgroup.map K.subtype (H.subgroupOf K))) α

Tactic:
ext x

Result:
case a
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
x b✝ : α
⊢ (orbitRel (↥(H.subgroupOf K)) α) x b✝ ↔ (orbitRel (↥(Subgroup.map K.subtype (H.subgroupOf K))) α) x b✝

Proof state:
case a.refine_2.intro.mk
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
b✝ : α
gv : G
gp : gv ∈ Subgroup.map K.subtype (H.subgroupOf K)
⊢ (fun m => m • b✝) ⟨gv, gp⟩ ∈ orbit (↥(H.subgroupOf K)) b✝

Tactic:
simp only [Submonoid.mk_smul]

Result:
case a.refine_2.intro.mk
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
b✝ : α
gv : G
gp : gv ∈ Subgroup.map K.subtype (H.subgroupOf K)
⊢ ⟨gv, gp⟩ • b✝ ∈ orbit (↥(H.subgroupOf K)) b✝