α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U V : Set β
this : Setoid β := orbitRel α β
⊢ Disjoint (Quotient.mk' '' U) (Quotient.mk' '' V) ↔ ∀ (x : β), x ∈ U → ∀ (a : α), ¬a • x ∈ V
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U V : Set β
⊢ Disjoint (Quotient.mk' '' U) (Quotient.mk' '' V) ↔ ∀ (x : β), x ∈ U → ∀ (a : α), ¬a • x ∈ V
letI := orbitRel α β
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U V : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
⊢ Disjoint (f '' U) (f '' V) ↔ ∀ (x : β), x ∈ U → ∀ (a : α), ¬a • x ∈ V
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U V : Set β
this : Setoid β := orbitRel α β
⊢ Disjoint (Quotient.mk' '' U) (Quotient.mk' '' V) ↔ ∀ (x : β), x ∈ U → ∀ (a : α), ¬a • x ∈ V
set f : β → Quotient (MulAction.orbitRel α β) := Quotient.mk'
case refine'_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U V : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
h : Disjoint (f '' U) (f '' V)
x : β
x_in_U : x ∈ U
a : α
a_in_V : a • x ∈ V
⊢ (fun x_1 => x_1 • a • x) a⁻¹ = x

case refine'_2
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U V : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
⊢ (∀ (x : β), x ∈ U → ∀ (a : α), ¬a • x ∈ V) → Disjoint (f '' U) (f '' V)
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U V : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
⊢ Disjoint (f '' U) (f '' V) ↔ ∀ (x : β), x ∈ U → ∀ (a : α), ¬a • x ∈ V
refine'
  ⟨fun h x x_in_U a a_in_V =>
    h.le_bot ⟨⟨x, x_in_U, Quotient.sound ⟨a⁻¹, _⟩⟩, ⟨a • x, a_in_V, rfl⟩⟩, _⟩
no goals
case refine'_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U V : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
h : Disjoint (f '' U) (f '' V)
x : β
x_in_U : x ∈ U
a : α
a_in_V : a • x ∈ V
⊢ (fun x_1 => x_1 • a • x) a⁻¹ = x
simp
case refine'_2
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U V : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
h : ∀ (x : β), x ∈ U → ∀ (a : α), ¬a • x ∈ V
⊢ Disjoint (f '' U) (f '' V)
case refine'_2
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U V : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
⊢ (∀ (x : β), x ∈ U → ∀ (a : α), ¬a • x ∈ V) → Disjoint (f '' U) (f '' V)
intro h
case refine'_2
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U V : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
h : ∀ (x : β), x ∈ U → ∀ (a : α), ¬a • x ∈ V
⊢ ∀ ⦃a : Quotient (orbitRel α β)⦄, a ∈ f '' U → ¬a ∈ f '' V
case refine'_2
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U V : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
h : ∀ (x : β), x ∈ U → ∀ (a : α), ¬a • x ∈ V
⊢ Disjoint (f '' U) (f '' V)
rw [Set.disjoint_left]
case refine'_2.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U V : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
h : ∀ (x : β), x ∈ U → ∀ (a : α), ¬a • x ∈ V
x : Quotient (orbitRel α β)
y : β
hy₁ : y ∈ U
hy₂ : f y = x
z : β
hz₁ : z ∈ V
hz₂ : f z = x
⊢ False
case refine'_2
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U V : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
h : ∀ (x : β), x ∈ U → ∀ (a : α), ¬a • x ∈ V
⊢ ∀ ⦃a : Quotient (orbitRel α β)⦄, a ∈ f '' U → ¬a ∈ f '' V
rintro x ⟨y, hy₁, hy₂⟩ ⟨z, hz₁, hz₂⟩
case refine'_2.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U V : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
h : ∀ (x : β), x ∈ U → ∀ (a : α), ¬a • x ∈ V
x : Quotient (orbitRel α β)
y : β
hy₁ : y ∈ U
hy₂ : f y = x
a : α
hz₁ : (fun x => x • y) a ∈ V
hz₂ : f ((fun x => x • y) a) = x
⊢ False
case refine'_2.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U V : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
h : ∀ (x : β), x ∈ U → ∀ (a : α), ¬a • x ∈ V
x : Quotient (orbitRel α β)
y : β
hy₁ : y ∈ U
hy₂ : f y = x
z : β
hz₁ : z ∈ V
hz₂ : f z = x
⊢ False
obtain ⟨a, rfl⟩ := Quotient.exact (hz₂.trans hy₂.symm)
no goals
case refine'_2.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
U V : Set β
this : Setoid β := orbitRel α β
f : β → Quotient (orbitRel α β) := Quotient.mk'
h : ∀ (x : β), x ∈ U → ∀ (a : α), ¬a • x ∈ V
x : Quotient (orbitRel α β)
y : β
hy₁ : y ∈ U
hy₂ : f y = x
a : α
hz₁ : (fun x => x • y) a ∈ V
hz₂ : f ((fun x => x • y) a) = x
⊢ False
exact h y hy₁ a hz₁