-- Mathlib/GroupTheory/GroupAction/Blocks.lean
theorem IsBlock.of_orbit {H : Subgroup G} {a : X} (hH : stabilizer G a ≤ H) :
    IsBlock G (MulAction.orbit H a)

Proof state:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
⊢ IsBlock G (orbit (↥H) a)

Tactic:
rw [isBlock_iff_smul_eq_of_nonempty]

Result:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
⊢ ∀ ⦃g : G⦄, (g • orbit (↥H) a ∩ orbit (↥H) a).Nonempty → g • orbit (↥H) a = orbit (↥H) a

Proof state:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
⊢ ∀ ⦃g : G⦄, (g • orbit (↥H) a ∩ orbit (↥H) a).Nonempty → g • orbit (↥H) a = orbit (↥H) a

Tactic:
rintro g ⟨-, ⟨-, ⟨h₁, rfl⟩, h⟩, h₂, rfl⟩

Result:
case intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h₁ h₂ : ↥H
h : (fun x => g • x) ((fun m => m • a) h₁) = (fun m => m • a) h₂
⊢ g • orbit (↥H) a = orbit (↥H) a

Proof state:
case intro.intro.intro.intro.intro.intro.a
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h₁ h₂ : ↥H
h : (fun x => g • x) ((fun m => m • a) h₁) = (fun m => m • a) h₂
⊢ ↑h₂⁻¹ * g * ↑h₁ ∈ stabilizer G a

Tactic:
simpa only [mem_stabilizer_iff, InvMemClass.coe_inv, mul_smul, inv_smul_eq_iff]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h₁ h₂ : ↥H
h : (fun x => g • x) ((fun m => m • a) h₁) = (fun m => m • a) h₂
⊢ g • orbit (↥H) a = orbit (↥H) a

Tactic:
suffices g ∈ H by
  rw [← Subgroup.coe_mk H g this, ← H.toSubmonoid.smul_def, smul_orbit (⟨g, this⟩ : H) a]

Result:
case intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h₁ h₂ : ↥H
h : (fun x => g • x) ((fun m => m • a) h₁) = (fun m => m • a) h₂
⊢ g ∈ H

Proof state:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h₁ h₂ : ↥H
h : (fun x => g • x) ((fun m => m • a) h₁) = (fun m => m • a) h₂
this : g ∈ H
⊢ g • orbit (↥H) a = orbit (↥H) a

Tactic:
rw [← Subgroup.coe_mk H g this, ← H.toSubmonoid.smul_def, smul_orbit (⟨g, this⟩ : H) a]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h₁ h₂ : ↥H
h : (fun x => g • x) ((fun m => m • a) h₁) = (fun m => m • a) h₂
⊢ g ∈ H

Tactic:
rw [← mul_mem_cancel_left h₂⁻¹.2, ← mul_mem_cancel_right h₁.2]

Result:
case intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h₁ h₂ : ↥H
h : (fun x => g • x) ((fun m => m • a) h₁) = (fun m => m • a) h₂
⊢ ↑h₂⁻¹ * g * ↑h₁ ∈ H

Proof state:
case intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h₁ h₂ : ↥H
h : (fun x => g • x) ((fun m => m • a) h₁) = (fun m => m • a) h₂
⊢ ↑h₂⁻¹ * g * ↑h₁ ∈ H

Tactic:
apply hH

Result:
case intro.intro.intro.intro.intro.intro.a
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h₁ h₂ : ↥H
h : (fun x => g • x) ((fun m => m • a) h₁) = (fun m => m • a) h₂
⊢ ↑h₂⁻¹ * g * ↑h₁ ∈ stabilizer G a