-- Mathlib/GroupTheory/GroupAction/Blocks.lean
theorem IsBlock.orbit_stabilizer_eq [IsPretransitive G X] (hB : IsBlock G B) {a : X} (ha : a ∈ B) :
    MulAction.orbit (stabilizer G B) a = B

Proof state:
case h.mp.intro.mk
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
B : Set X
inst✝ : IsPretransitive G X
hB : IsBlock G B
a : X
ha : a ∈ B
k : G
k_mem : k ∈ stabilizer G B
⊢ k • a ∈ B

Tactic:
rw [← k_mem, Set.smul_mem_smul_set_iff]

Result:
case h.mp.intro.mk
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
B : Set X
inst✝ : IsPretransitive G X
hB : IsBlock G B
a : X
ha : a ∈ B
k : G
k_mem : k ∈ stabilizer G B
⊢ a ∈ B

Proof state:
case h.mp.intro.mk
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
B : Set X
inst✝ : IsPretransitive G X
hB : IsBlock G B
a : X
ha : a ∈ B
k : G
k_mem : k ∈ stabilizer G B
⊢ a ∈ B

Tactic:
exact ha

Result:
no goals

Proof state:
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
B : Set X
inst✝ : IsPretransitive G X
hB : IsBlock G B
a : X
ha : a ∈ B
⊢ orbit (↥(stabilizer G B)) a = B

Tactic:
ext x

Result:
case h
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
B : Set X
inst✝ : IsPretransitive G X
hB : IsBlock G B
a : X
ha : a ∈ B
x : X
⊢ x ∈ orbit (↥(stabilizer G B)) a ↔ x ∈ B

Proof state:
case h
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
B : Set X
inst✝ : IsPretransitive G X
hB : IsBlock G B
a : X
ha : a ∈ B
x : X
⊢ x ∈ orbit (↥(stabilizer G B)) a ↔ x ∈ B

Tactic:
constructor

Result:
case h.mp
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
B : Set X
inst✝ : IsPretransitive G X
hB : IsBlock G B
a : X
ha : a ∈ B
x : X
⊢ x ∈ orbit (↥(stabilizer G B)) a → x ∈ B

case h.mpr
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
B : Set X
inst✝ : IsPretransitive G X
hB : IsBlock G B
a : X
ha : a ∈ B
x : X
⊢ x ∈ B → x ∈ orbit (↥(stabilizer G B)) a

Proof state:
case h.mpr
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
B : Set X
inst✝ : IsPretransitive G X
hB : IsBlock G B
a : X
ha : a ∈ B
x : X
⊢ x ∈ B → x ∈ orbit (↥(stabilizer G B)) a

Tactic:
intro hx

Result:
case h.mpr
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
B : Set X
inst✝ : IsPretransitive G X
hB : IsBlock G B
a : X
ha : a ∈ B
x : X
hx : x ∈ B
⊢ x ∈ orbit (↥(stabilizer G B)) a

Proof state:
case h.mp
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
B : Set X
inst✝ : IsPretransitive G X
hB : IsBlock G B
a : X
ha : a ∈ B
x : X
⊢ x ∈ orbit (↥(stabilizer G B)) a → x ∈ B

Tactic:
rintro ⟨⟨k, k_mem⟩, rfl⟩

Result:
case h.mp.intro.mk
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
B : Set X
inst✝ : IsPretransitive G X
hB : IsBlock G B
a : X
ha : a ∈ B
k : G
k_mem : k ∈ stabilizer G B
⊢ (fun m => m • a) ⟨k, k_mem⟩ ∈ B

Proof state:
case h.mpr.intro
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
B : Set X
inst✝ : IsPretransitive G X
hB : IsBlock G B
a : X
ha : a ∈ B
k : G
hx : k • a ∈ B
⊢ k • a ∈ orbit (↥(stabilizer G B)) a

Tactic:
exact ⟨⟨k, hB.smul_eq_of_mem ha hx⟩, rfl⟩

Result:
no goals

Proof state:
case h.mpr
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
B : Set X
inst✝ : IsPretransitive G X
hB : IsBlock G B
a : X
ha : a ∈ B
x : X
hx : x ∈ B
⊢ x ∈ orbit (↥(stabilizer G B)) a

Tactic:
obtain ⟨k, rfl⟩ := exists_smul_eq G a x

Result:
case h.mpr.intro
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
B : Set X
inst✝ : IsPretransitive G X
hB : IsBlock G B
a : X
ha : a ∈ B
k : G
hx : k • a ∈ B
⊢ k • a ∈ orbit (↥(stabilizer G B)) a

Proof state:
case h.mp.intro.mk
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
B : Set X
inst✝ : IsPretransitive G X
hB : IsBlock G B
a : X
ha : a ∈ B
k : G
k_mem : k ∈ stabilizer G B
⊢ (fun m => m • a) ⟨k, k_mem⟩ ∈ B

Tactic:
simp only [Subgroup.mk_smul]

Result:
case h.mp.intro.mk
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
B : Set X
inst✝ : IsPretransitive G X
hB : IsBlock G B
a : X
ha : a ∈ B
k : G
k_mem : k ∈ stabilizer G B
⊢ k • a ∈ B