α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U : Set β
this : Setoid β := orbitRel α β
⊢ Quotient.mk' ⁻¹' (Quotient.mk' '' U) = ⋃ (a : α), (fun x x_1 => x • x_1) a '' U
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U : Set β
⊢ Quotient.mk' ⁻¹' (Quotient.mk' '' U) = ⋃ (a : α), (fun x x_1 => x • x_1) a '' U
letI := orbitRel α β
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
⊢ f ⁻¹' (f '' U) = ⋃ (a : α), (fun x x_1 => x • x_1) a '' U
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U : Set β
this : Setoid β := orbitRel α β
⊢ Quotient.mk' ⁻¹' (Quotient.mk' '' U) = ⋃ (a : α), (fun x x_1 => x • x_1) a '' U
set f : β → Quotient (MulAction.orbitRel α β) := Quotient.mk'
case h
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
x : β
⊢ x ∈ f ⁻¹' (f '' U) ↔ x ∈ ⋃ (a : α), (fun x x_1 => x • x_1) a '' U
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
⊢ f ⁻¹' (f '' U) = ⋃ (a : α), (fun x x_1 => x • x_1) a '' U
ext x
case h.mp
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
x : β
⊢ x ∈ f ⁻¹' (f '' U) → x ∈ ⋃ (a : α), (fun x x_1 => x • x_1) a '' U

case h.mpr
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
x : β
⊢ (x ∈ ⋃ (a : α), (fun x x_1 => x • x_1) a '' U) → x ∈ f ⁻¹' (f '' U)
case h
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
x : β
⊢ x ∈ f ⁻¹' (f '' U) ↔ x ∈ ⋃ (a : α), (fun x x_1 => x • x_1) a '' U
constructor
case h.mp.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
x y : β
hy : y ∈ U
hxy : f y = f x
⊢ x ∈ ⋃ (a : α), (fun x x_1 => x • x_1) a '' U
case h.mp
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
x : β
⊢ x ∈ f ⁻¹' (f '' U) → x ∈ ⋃ (a : α), (fun x x_1 => x • x_1) a '' U
rintro ⟨y, hy, hxy⟩
case h.mp.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
x : β
a : α
hy : (fun x_1 => x_1 • x) a ∈ U
hxy : f ((fun x_1 => x_1 • x) a) = f x
⊢ x ∈ ⋃ (a : α), (fun x x_1 => x • x_1) a '' U
case h.mp.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
x y : β
hy : y ∈ U
hxy : f y = f x
⊢ x ∈ ⋃ (a : α), (fun x x_1 => x • x_1) a '' U
obtain ⟨a, rfl⟩ := Quotient.exact hxy
case h.mp.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
x : β
a : α
hy : (fun x_1 => x_1 • x) a ∈ U
hxy : f ((fun x_1 => x_1 • x) a) = f x
⊢ ∃ i, x ∈ (fun x x_1 => x • x_1) i '' U
case h.mp.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
x : β
a : α
hy : (fun x_1 => x_1 • x) a ∈ U
hxy : f ((fun x_1 => x_1 • x) a) = f x
⊢ x ∈ ⋃ (a : α), (fun x x_1 => x • x_1) a '' U
rw [Set.mem_iUnion]
no goals
case h.mp.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
x : β
a : α
hy : (fun x_1 => x_1 • x) a ∈ U
hxy : f ((fun x_1 => x_1 • x) a) = f x
⊢ ∃ i, x ∈ (fun x x_1 => x • x_1) i '' U
exact ⟨a⁻¹, a • x, hy, inv_smul_smul a x⟩
case h.mpr
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
x : β
hx : x ∈ ⋃ (a : α), (fun x x_1 => x • x_1) a '' U
⊢ x ∈ f ⁻¹' (f '' U)
case h.mpr
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
x : β
⊢ (x ∈ ⋃ (a : α), (fun x x_1 => x • x_1) a '' U) → x ∈ f ⁻¹' (f '' U)
intro hx
case h.mpr
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
x : β
hx : ∃ i, x ∈ (fun x x_1 => x • x_1) i '' U
⊢ x ∈ f ⁻¹' (f '' U)
case h.mpr
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
x : β
hx : x ∈ ⋃ (a : α), (fun x x_1 => x • x_1) a '' U
⊢ x ∈ f ⁻¹' (f '' U)
rw [Set.mem_iUnion] at hx
case h.mpr.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
x : β
a : α
u : β
hu₁ : u ∈ U
hu₂ : (fun x x_1 => x • x_1) a u = x
⊢ x ∈ f ⁻¹' (f '' U)
case h.mpr
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
x : β
hx : ∃ i, x ∈ (fun x x_1 => x • x_1) i '' U
⊢ x ∈ f ⁻¹' (f '' U)
obtain ⟨a, u, hu₁, hu₂⟩ := hx
case h.mpr.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
x : β
a : α
u : β
hu₁ : u ∈ U
hu₂ : (fun x x_1 => x • x_1) a u = x
⊢ ∃ x_1 x_2, f x_1 = f x
case h.mpr.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
x : β
a : α
u : β
hu₁ : u ∈ U
hu₂ : (fun x x_1 => x • x_1) a u = x
⊢ x ∈ f ⁻¹' (f '' U)
rw [Set.mem_preimage, Set.mem_image_iff_bex]
case h.mpr.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
x : β
a : α
u : β
hu₁ : u ∈ U
hu₂ : (fun x x_1 => x • x_1) a u = x
⊢ a⁻¹ • x ∈ U
case h.mpr.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
x : β
a : α
u : β
hu₁ : u ∈ U
hu₂ : (fun x x_1 => x • x_1) a u = x
⊢ ∃ x_1 x_2, f x_1 = f x
refine' ⟨a⁻¹ • x, _, by simp only [Quotient.eq']; use a⁻¹⟩
case h.mpr.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
x : β
a : α
u : β
hu₁ : u ∈ U
hu₂ : (fun x x_1 => x • x_1) a u = x
⊢ a⁻¹ • (fun x x_1 => x • x_1) a u ∈ U
case h.mpr.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
x : β
a : α
u : β
hu₁ : u ∈ U
hu₂ : (fun x x_1 => x • x_1) a u = x
⊢ a⁻¹ • x ∈ U
rw [← hu₂]
case h.e'_4
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
x : β
a : α
u : β
hu₁ : u ∈ U
hu₂ : (fun x x_1 => x • x_1) a u = x
⊢ a⁻¹ • (fun x x_1 => x • x_1) a u = u
case h.mpr.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
x : β
a : α
u : β
hu₁ : u ∈ U
hu₂ : (fun x x_1 => x • x_1) a u = x
⊢ a⁻¹ • (fun x x_1 => x • x_1) a u ∈ U
convert hu₁
no goals
case h.e'_4
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
x : β
a : α
u : β
hu₁ : u ∈ U
hu₂ : (fun x x_1 => x • x_1) a u = x
⊢ a⁻¹ • (fun x x_1 => x • x_1) a u = u
simp only [inv_smul_smul]
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
x : β
a : α
u : β
hu₁ : u ∈ U
hu₂ : (fun x x_1 => x • x_1) a u = x
⊢ Setoid.r (a⁻¹ • x) x
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
x : β
a : α
u : β
hu₁ : u ∈ U
hu₂ : (fun x x_1 => x • x_1) a u = x
⊢ f (a⁻¹ • x) = f x
simp only [Quotient.eq']
no goals
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
x : β
a : α
u : β
hu₁ : u ∈ U
hu₂ : (fun x x_1 => x • x_1) a u = x
⊢ Setoid.r (a⁻¹ • x) x
use a⁻¹