-- Mathlib/GroupTheory/GroupAction/Defs.lean
theorem quotient_preimage_image_eq_union_mul (U : Set α) :
    letI := orbitRel G α
    Quotient.mk' ⁻¹' (Quotient.mk' '' U) = ⋃ g : G, (g • ·) '' U

Proof state:
case h.mpr
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
hx : ∃ i, a ∈ (fun x => i • x) '' U
⊢ a ∈ f ⁻¹' (f '' U)

Tactic:
obtain ⟨g, u, hu₁, hu₂⟩ := hx

Result:
case h.mpr.intro.intro.intro
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
u : α
hu₁ : u ∈ U
hu₂ : (fun x => g • x) u = a
⊢ a ∈ f ⁻¹' (f '' U)

Proof state:
case h.mp.intro.intro.intro
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
hb : (fun m => m • a) g ∈ U
hab : f ((fun m => m • a) g) = f a
⊢ a ∈ ⋃ g, (fun x => g • x) '' U

Tactic:
rw [Set.mem_iUnion]

Result:
case h.mp.intro.intro.intro
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
hb : (fun m => m • a) g ∈ U
hab : f ((fun m => m • a) g) = f a
⊢ ∃ i, a ∈ (fun x => i • x) '' U

Proof state:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
u : α
hu₁ : u ∈ U
hu₂ : (fun x => g • x) u = a
⊢ (orbitRel G α) (g⁻¹ • a) a

Tactic:
use g⁻¹

Result:
no goals

Proof state:
case h.mpr.intro.intro.intro
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
u : α
hu₁ : u ∈ U
hu₂ : (fun x => g • x) u = a
⊢ ∃ x ∈ U, f x = f a

Tactic:
refine ⟨g⁻¹ • a, ?_, by simp only [f, Quotient.eq']; use g⁻¹⟩

Result:
case h.mpr.intro.intro.intro
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
u : α
hu₁ : u ∈ U
hu₂ : (fun x => g • x) u = a
⊢ g⁻¹ • a ∈ U

Proof state:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
u : α
hu₁ : u ∈ U
hu₂ : (fun x => g • x) u = a
⊢ f (g⁻¹ • a) = f a

Tactic:
simp only [f, Quotient.eq']

Result:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
u : α
hu₁ : u ∈ U
hu₂ : (fun x => g • x) u = a
⊢ (orbitRel G α) (g⁻¹ • a) a

Proof state:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
⊢ Quotient.mk' ⁻¹' (Quotient.mk' '' U) = ⋃ g, (fun x => g • x) '' U

Tactic:
letI := orbitRel G α

Result:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
⊢ Quotient.mk' ⁻¹' (Quotient.mk' '' U) = ⋃ g, (fun x => g • x) '' U

Proof state:
case h.mpr
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
hx : a ∈ ⋃ g, (fun x => g • x) '' U
⊢ a ∈ f ⁻¹' (f '' U)

Tactic:
rw [Set.mem_iUnion] at hx

Result:
case h.mpr
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
hx : ∃ i, a ∈ (fun x => i • x) '' U
⊢ a ∈ f ⁻¹' (f '' U)

Proof state:
case h.mp.intro.intro
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a b : α
hb : b ∈ U
hab : f b = f a
⊢ a ∈ ⋃ g, (fun x => g • x) '' U

Tactic:
obtain ⟨g, rfl⟩ := Quotient.exact hab

Result:
case h.mp.intro.intro.intro
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
hb : (fun m => m • a) g ∈ U
hab : f ((fun m => m • a) g) = f a
⊢ a ∈ ⋃ g, (fun x => g • x) '' U

Proof state:
case h
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
⊢ a ∈ f ⁻¹' (f '' U) ↔ a ∈ ⋃ g, (fun x => g • x) '' U

Tactic:
constructor

Result:
case h.mp
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
⊢ a ∈ f ⁻¹' (f '' U) → a ∈ ⋃ g, (fun x => g • x) '' U

case h.mpr
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
⊢ a ∈ ⋃ g, (fun x => g • x) '' U → a ∈ f ⁻¹' (f '' U)

Proof state:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
⊢ f ⁻¹' (f '' U) = ⋃ g, (fun x => g • x) '' U

Tactic:
ext a

Result:
case h
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
⊢ a ∈ f ⁻¹' (f '' U) ↔ a ∈ ⋃ g, (fun x => g • x) '' U

Proof state:
case h.mp
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
⊢ a ∈ f ⁻¹' (f '' U) → a ∈ ⋃ g, (fun x => g • x) '' U

Tactic:
rintro ⟨b, hb, hab⟩

Result:
case h.mp.intro.intro
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a b : α
hb : b ∈ U
hab : f b = f a
⊢ a ∈ ⋃ g, (fun x => g • x) '' U

Proof state:
case h.mpr
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
⊢ a ∈ ⋃ g, (fun x => g • x) '' U → a ∈ f ⁻¹' (f '' U)

Tactic:
intro hx

Result:
case h.mpr
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
hx : a ∈ ⋃ g, (fun x => g • x) '' U
⊢ a ∈ f ⁻¹' (f '' U)

Proof state:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
⊢ Quotient.mk' ⁻¹' (Quotient.mk' '' U) = ⋃ g, (fun x => g • x) '' U

Tactic:
set f : α → Quotient (MulAction.orbitRel G α) := Quotient.mk'

Result:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
⊢ f ⁻¹' (f '' U) = ⋃ g, (fun x => g • x) '' U

Proof state:
case h.mp.intro.intro.intro
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
hb : (fun m => m • a) g ∈ U
hab : f ((fun m => m • a) g) = f a
⊢ ∃ i, a ∈ (fun x => i • x) '' U

Tactic:
exact ⟨g⁻¹, g • a, hb, inv_smul_smul g a⟩

Result:
no goals

Proof state:
case h.e'_5
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
u : α
hu₁ : u ∈ U
hu₂ : (fun x => g • x) u = a
⊢ g⁻¹ • (fun x => g • x) u = u

Tactic:
simp only [inv_smul_smul]

Result:
no goals