-- Mathlib/GroupTheory/GroupAction/Blocks.lean
@[to_additive]
lemma smul_orbit_eq_orbit_smul (N : Subgroup G) [nN : N.Normal] (a : X) (g : G) :
    g • orbit N a = orbit N (g • a)

Proof state:
case h.mpr
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g : G
x✝ : X
⊢ (∃ y, y • g • a = x✝) → ∃ y, g • y • a = x✝

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

Result:
case h.mpr.intro.mk
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g k : G
hk : k ∈ N
⊢ ∃ y, g • y • a = ⟨k, hk⟩ • g • a

Proof state:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g k : G
hk : k ∈ N
⊢ g • (g⁻¹ * k * g) • a = k • g • a

Tactic:
simp only [← mul_assoc, ← smul_smul, smul_inv_smul, inv_inv]

Result:
no goals

Proof state:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g k : G
hk : k ∈ N
⊢ (g * k * g⁻¹) • g • a = g • k • a

Tactic:
rw [smul_smul, inv_mul_cancel_right, ← smul_smul]

Result:
no goals

Proof state:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g : G
x✝ : X
⊢ (x✝ ∈ range fun i => g • i • a) ↔ x✝ ∈ range fun m => m • g • a

Tactic:
simp only [Set.mem_range]

Result:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g : G
x✝ : X
⊢ (∃ y, g • y • a = x✝) ↔ ∃ y, y • g • a = x✝

Proof state:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g : G
x✝ : X
⊢ (∃ y, g • y • a = x✝) ↔ ∃ y, y • g • a = x✝

Tactic:
constructor

Result:
case h.mp
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g : G
x✝ : X
⊢ (∃ y, g • y • a = x✝) → ∃ y, y • g • a = x✝

case h.mpr
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g : G
x✝ : X
⊢ (∃ y, y • g • a = x✝) → ∃ y, g • y • a = x✝

Proof state:
case h.mpr.intro.mk
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g k : G
hk : k ∈ N
⊢ ∃ y, g • y • a = ⟨k, hk⟩ • g • a

Tactic:
use ⟨g⁻¹ * k * g, nN.conj_mem' k hk g⟩

Result:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g k : G
hk : k ∈ N
⊢ g • ⟨g⁻¹ * k * g, ⋯⟩ • a = ⟨k, hk⟩ • g • a

Proof state:
case h.mp.intro.mk
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g k : G
hk : k ∈ N
⊢ ∃ y, y • g • a = g • ⟨k, hk⟩ • a

Tactic:
use ⟨g * k * g⁻¹, nN.conj_mem k hk g⟩

Result:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g k : G
hk : k ∈ N
⊢ ⟨g * k * g⁻¹, ⋯⟩ • g • a = g • ⟨k, hk⟩ • a

Proof state:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g : G
⊢ g • orbit (↥N) a = orbit (↥N) (g • a)

Tactic:
simp only [orbit, Set.image_smul, Set.smul_set_range]

Result:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g : G
⊢ (range fun i => g • i • a) = range fun m => m • g • a

Proof state:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g k : G
hk : k ∈ N
⊢ ⟨g * k * g⁻¹, ⋯⟩ • g • a = g • ⟨k, hk⟩ • a

Tactic:
simp only [Subgroup.mk_smul]

Result:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g k : G
hk : k ∈ N
⊢ (g * k * g⁻¹) • g • a = g • k • a

Proof state:
case h.mp
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g : G
x✝ : X
⊢ (∃ y, g • y • a = x✝) → ∃ y, y • g • a = x✝

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

Result:
case h.mp.intro.mk
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g k : G
hk : k ∈ N
⊢ ∃ y, y • g • a = g • ⟨k, hk⟩ • a

Proof state:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g k : G
hk : k ∈ N
⊢ g • ⟨g⁻¹ * k * g, ⋯⟩ • a = ⟨k, hk⟩ • g • a

Tactic:
simp only [Subgroup.mk_smul]

Result:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g k : G
hk : k ∈ N
⊢ g • (g⁻¹ * k * g) • a = k • g • a

Proof state:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g : G
⊢ (range fun i => g • i • a) = range fun m => m • g • a

Tactic:
ext

Result:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g : G
x✝ : X
⊢ (x✝ ∈ range fun i => g • i • a) ↔ x✝ ∈ range fun m => m • g • a