-- Mathlib/GroupTheory/GroupAction/Defs.lean
@[to_additive (attr := norm_cast, simp)]
lemma orbitRel.Quotient.mem_subgroup_orbit_iff {H : Subgroup G} {x : orbitRel.Quotient G α}
    {a b : x.orbit} : (a : α) ∈ MulAction.orbit H (b : α) ↔ a ∈ MulAction.orbit H b

Proof state:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
⊢ ↑a ∈ MulAction.orbit ↥H ↑b ↔ a ∈ MulAction.orbit (↥H) b

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

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

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

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

Tactic:
rcases h with ⟨g, h⟩

Result:
case refine_1.intro
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
g : ↥H
h : (fun m => m • ↑b) g = ↑a
⊢ a ∈ MulAction.orbit (↥H) b

Proof state:
case refine_1.intro
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
b : ↑x.orbit
g : ↥H
⊢ ↑g • b ∈ MulAction.orbit (↥H) b

Tactic:
exact MulAction.mem_orbit _ g

Result:
no goals

Proof state:
case refine_1.intro
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
g : ↥H
h : ↑g • b = a
⊢ a ∈ MulAction.orbit (↥H) b

Tactic:
subst h

Result:
case refine_1.intro
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
b : ↑x.orbit
g : ↥H
⊢ ↑g • b ∈ MulAction.orbit (↥H) b

Proof state:
case refine_1.intro
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
g : ↥H
h : (fun m => m • ↑b) g = ↑a
⊢ a ∈ MulAction.orbit (↥H) b

Tactic:
dsimp at h

Result:
case refine_1.intro
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
g : ↥H
h : g • ↑b = ↑a
⊢ a ∈ MulAction.orbit (↥H) b

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

Tactic:
rcases h with ⟨g, rfl⟩

Result:
case refine_2.intro
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
b : ↑x.orbit
g : ↥H
⊢ ↑((fun m => m • b) g) ∈ MulAction.orbit ↥H ↑b

Proof state:
case refine_2.intro
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
b : ↑x.orbit
g : ↥H
⊢ ↑((fun m => m • b) g) ∈ MulAction.orbit ↥H ↑b

Tactic:
exact MulAction.mem_orbit _ g

Result:
no goals

Proof state:
case refine_1.intro
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
g : ↥H
h : g • ↑b = ↑a
⊢ a ∈ MulAction.orbit (↥H) b

Tactic:
erw [← orbit.coe_smul, ← Subtype.ext_iff] at h

Result:
case refine_1.intro
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
g : ↥H
h : ↑g • b = a
⊢ a ∈ MulAction.orbit (↥H) b