awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
Γ : Type u_4
T : Type u_5
inst : TopologicalSpace T
inst_1 : SMul Γ T
inst_2 : ProperlyDiscontinuousSMul Γ T
inst_3 : T2Space T
inst_4 : LocallyCompactSpace T
inst_5 : ContinuousConstSMul Γ T
x : T
V : Set T
V_cpt : IsCompact V
V_nhd : V ∈ 𝓝 x
Γ₀ : Set Γ := {γ : Γ | ((fun (x : T) ↦ γ • x) '' V ∩ V).Nonempty ∧ γ • x ≠ x}
this : Finite.{u_4 + 1} (↑Γ₀ : Type u_4)
u v : (γ : (↑Γ₀ : Type u_4)) → Set T
hu : ∀ (γ : (↑Γ₀ : Type u_4)), u γ ∈ 𝓝 ((↑γ : Γ) • x)
hv : ∀ (γ : (↑Γ₀ : Type u_4)), v γ ∈ 𝓝 x
u_v_disjoint : ∀ (γ : (↑Γ₀ : Type u_4)), Disjoint (u γ) (v γ)
refine :
  ∀ (γ : Γ)
    (hγ :
      ((fun (x : T) ↦ γ • x) '' (V ∩ ⋂ (γ : (↑Γ₀ : Type u_4)), (fun (x : T) ↦ (↑γ : Γ) • x) ⁻¹' u γ ∩ v γ) ∩
          (V ∩ ⋂ (γ : (↑Γ₀ : Type u_4)), (fun (x : T) ↦ (↑γ : Γ) • x) ⁻¹' u γ ∩ v γ)).Nonempty),
    γ • x = x
⊢ ∃ U ∈ 𝓝 x, ∀ (γ : Γ), ((fun (x : T) ↦ γ • x) '' U ∩ U).Nonempty → γ • x = x

Tactic:
refine ⟨V ∩ ⋂ γ : Γ₀, (γ.1 • ·) ⁻¹' u γ ∩ v γ, inter_mem V_nhd (iInter_mem.mpr fun γ ↦
    inter_mem ((continuous_const_smul _).continuousAt <| hu γ) (hv γ)), fun γ hγ ↦ ?_⟩
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
Γ : Type u_4
T : Type u_5
inst : TopologicalSpace T
inst_1 : SMul Γ T
inst_2 : ProperlyDiscontinuousSMul Γ T
inst_3 : T2Space T
inst_4 : LocallyCompactSpace T
inst_5 : ContinuousConstSMul Γ T
x : T
V : Set T
V_cpt : IsCompact V
V_nhd : V ∈ 𝓝 x
Γ₀ : Set Γ := {γ : Γ | ((fun (x : T) ↦ γ • x) '' V ∩ V).Nonempty ∧ γ • x ≠ x}
this : Finite.{u_4 + 1} (↑Γ₀ : Type u_4)
u v : (γ : (↑Γ₀ : Type u_4)) → Set T
hu : ∀ (γ : (↑Γ₀ : Type u_4)), u γ ∈ 𝓝 ((↑γ : Γ) • x)
hv : ∀ (γ : (↑Γ₀ : Type u_4)), v γ ∈ 𝓝 x
u_v_disjoint : ∀ (γ : (↑Γ₀ : Type u_4)), Disjoint (u γ) (v γ)
γ : Γ
hγ :
  ((fun (x : T) ↦ γ • x) '' (V ∩ ⋂ (γ : (↑Γ₀ : Type u_4)), (fun (x : T) ↦ (↑γ : Γ) • x) ⁻¹' u γ ∩ v γ) ∩
      (V ∩ ⋂ (γ : (↑Γ₀ : Type u_4)), (fun (x : T) ↦ (↑γ : Γ) • x) ⁻¹' u γ ∩ v γ)).Nonempty
obtain :
  ∀ (z : T) (hz : z ∈ V ∩ ⋂ (γ : (↑Γ₀ : Type u_4)), (fun (x : T) ↦ (↑γ : Γ) • x) ⁻¹' u γ ∩ v γ)
    (hγz : (fun (x : T) ↦ γ • x) z ∈ V ∩ ⋂ (γ : (↑Γ₀ : Type u_4)), (fun (x : T) ↦ (↑γ : Γ) • x) ⁻¹' u γ ∩ v γ),
    γ • x = x
⊢ γ • x = x

Tactic:
obtain ⟨_, ⟨z, hz, rfl⟩, hγz⟩ := hγ

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
Γ : Type u_4
T : Type u_5
inst : TopologicalSpace T
inst_1 : SMul Γ T
inst_2 : ProperlyDiscontinuousSMul Γ T
inst_3 : T2Space T
inst_4 : LocallyCompactSpace T
inst_5 : ContinuousConstSMul Γ T
x : T
V : Set T
V_cpt : IsCompact V
V_nhd : V ∈ 𝓝 x
Γ₀ : Set Γ := {γ : Γ | ((fun (x : T) ↦ γ • x) '' V ∩ V).Nonempty ∧ γ • x ≠ x}
this : Finite.{u_4 + 1} (↑Γ₀ : Type u_4)
u v : (γ : (↑Γ₀ : Type u_4)) → Set T
hu : ∀ (γ : (↑Γ₀ : Type u_4)), u γ ∈ 𝓝 ((↑γ : Γ) • x)
hv : ∀ (γ : (↑Γ₀ : Type u_4)), v γ ∈ 𝓝 x
u_v_disjoint : ∀ (γ : (↑Γ₀ : Type u_4)), Disjoint (u γ) (v γ)
γ : Γ
z : T
hz : z ∈ V ∩ ⋂ (γ : (↑Γ₀ : Type u_4)), (fun (x : T) ↦ (↑γ : Γ) • x) ⁻¹' u γ ∩ v γ
hγz : (fun (x : T) ↦ γ • x) z ∈ V ∩ ⋂ (γ : (↑Γ₀ : Type u_4)), (fun (x : T) ↦ (↑γ : Γ) • x) ⁻¹' u γ ∩ v γ
by_contra : ∀ (h : ¬γ • x = x), False
⊢ γ • x = x

Tactic:
by_contra h
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
Γ : Type u_4
T : Type u_5
inst : TopologicalSpace T
inst_1 : SMul Γ T
inst_2 : ProperlyDiscontinuousSMul Γ T
inst_3 : T2Space T
inst_4 : LocallyCompactSpace T
inst_5 : ContinuousConstSMul Γ T
x : T
V : Set T
V_cpt : IsCompact V
V_nhd : V ∈ 𝓝 x
Γ₀ : Set Γ := {γ : Γ | ((fun (x : T) ↦ γ • x) '' V ∩ V).Nonempty ∧ γ • x ≠ x}
this : Finite.{u_4 + 1} (↑Γ₀ : Type u_4)
u v : (γ : (↑Γ₀ : Type u_4)) → Set T
hu : ∀ (γ : (↑Γ₀ : Type u_4)), u γ ∈ 𝓝 ((↑γ : Γ) • x)
hv : ∀ (γ : (↑Γ₀ : Type u_4)), v γ ∈ 𝓝 x
u_v_disjoint : ∀ (γ : (↑Γ₀ : Type u_4)), Disjoint (u γ) (v γ)
γ : Γ
z : T
hz : z ∈ V ∩ ⋂ (γ : (↑Γ₀ : Type u_4)), (fun (x : T) ↦ (↑γ : Γ) • x) ⁻¹' u γ ∩ v γ
hγz : (fun (x : T) ↦ γ • x) z ∈ V ∩ ⋂ (γ : (↑Γ₀ : Type u_4)), (fun (x : T) ↦ (↑γ : Γ) • x) ⁻¹' u γ ∩ v γ
h : ¬γ • x = x
⊢ z ∈ V ∧ ∀ (i : (↑Γ₀ : Type u_4)), z ∈ (fun (x : T) ↦ (↑i : Γ) • x) ⁻¹' u i ∩ v i

Tactic:
rw [mem_inter_iff, mem_iInter] at hz hγz

Premises used: Set.mem_inter_iff, Set.mem_iInter
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
Γ : Type u_4
T : Type u_5
inst : TopologicalSpace T
inst_1 : SMul Γ T
inst_2 : ProperlyDiscontinuousSMul Γ T
inst_3 : T2Space T
inst_4 : LocallyCompactSpace T
inst_5 : ContinuousConstSMul Γ T
x : T
V : Set T
V_cpt : IsCompact V
V_nhd : V ∈ 𝓝 x
Γ₀ : Set Γ := {γ : Γ | ((fun (x : T) ↦ γ • x) '' V ∩ V).Nonempty ∧ γ • x ≠ x}
this : Finite.{u_4 + 1} (↑Γ₀ : Type u_4)
u v : (γ : (↑Γ₀ : Type u_4)) → Set T
hu : ∀ (γ : (↑Γ₀ : Type u_4)), u γ ∈ 𝓝 ((↑γ : Γ) • x)
hv : ∀ (γ : (↑Γ₀ : Type u_4)), v γ ∈ 𝓝 x
u_v_disjoint : ∀ (γ : (↑Γ₀ : Type u_4)), Disjoint (u γ) (v γ)
γ : Γ
z : T
hz : z ∈ V ∩ ⋂ (γ : (↑Γ₀ : Type u_4)), (fun (x : T) ↦ (↑γ : Γ) • x) ⁻¹' u γ ∩ v γ
hγz : (fun (x : T) ↦ γ • x) z ∈ V ∩ ⋂ (γ : (↑Γ₀ : Type u_4)), (fun (x : T) ↦ (↑γ : Γ) • x) ⁻¹' u γ ∩ v γ
h : ¬γ • x = x
hz₁ : z ∈ V ∧ ∀ (i : (↑Γ₀ : Type u_4)), z ∈ (fun (x : T) ↦ (↑i : Γ) • x) ⁻¹' u i ∩ v i
⊢ (fun (x : T) ↦ γ • x) z ∈ V ∧
    ∀ (i : (↑Γ₀ : Type u_4)), (fun (x : T) ↦ γ • x) z ∈ (fun (x : T) ↦ (↑i : Γ) • x) ⁻¹' u i ∩ v i

Tactic:
rw [mem_inter_iff, mem_iInter] at hz hγz

Premises used: Set.mem_inter_iff, Set.mem_iInter
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
Γ : Type u_4
T : Type u_5
inst : TopologicalSpace T
inst_1 : SMul Γ T
inst_2 : ProperlyDiscontinuousSMul Γ T
inst_3 : T2Space T
inst_4 : LocallyCompactSpace T
inst_5 : ContinuousConstSMul Γ T
x : T
V : Set T
V_cpt : IsCompact V
V_nhd : V ∈ 𝓝 x
Γ₀ : Set Γ := {γ : Γ | ((fun (x : T) ↦ γ • x) '' V ∩ V).Nonempty ∧ γ • x ≠ x}
this : Finite.{u_4 + 1} (↑Γ₀ : Type u_4)
u v : (γ : (↑Γ₀ : Type u_4)) → Set T
hu : ∀ (γ : (↑Γ₀ : Type u_4)), u γ ∈ 𝓝 ((↑γ : Γ) • x)
hv : ∀ (γ : (↑Γ₀ : Type u_4)), v γ ∈ 𝓝 x
u_v_disjoint : ∀ (γ : (↑Γ₀ : Type u_4)), Disjoint (u γ) (v γ)
γ : Γ
z : T
hz : z ∈ V ∩ ⋂ (γ : (↑Γ₀ : Type u_4)), (fun (x : T) ↦ (↑γ : Γ) • x) ⁻¹' u γ ∩ v γ
hγz : (fun (x : T) ↦ γ • x) z ∈ V ∩ ⋂ (γ : (↑Γ₀ : Type u_4)), (fun (x : T) ↦ (↑γ : Γ) • x) ⁻¹' u γ ∩ v γ
h : ¬γ • x = x
hz₁ : z ∈ V ∧ ∀ (i : (↑Γ₀ : Type u_4)), z ∈ (fun (x : T) ↦ (↑i : Γ) • x) ⁻¹' u i ∩ v i
hγz₁ :
  (fun (x : T) ↦ γ • x) z ∈ V ∧
    ∀ (i : (↑Γ₀ : Type u_4)), (fun (x : T) ↦ γ • x) z ∈ (fun (x : T) ↦ (↑i : Γ) • x) ⁻¹' u i ∩ v i
⊢ ¬γ • x = x

Tactic:
rw [mem_inter_iff, mem_iInter] at hz hγz

Premises used: Set.mem_inter_iff, Set.mem_iInter
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
Γ : Type u_4
T : Type u_5
inst : TopologicalSpace T
inst_1 : SMul Γ T
inst_2 : ProperlyDiscontinuousSMul Γ T
inst_3 : T2Space T
inst_4 : LocallyCompactSpace T
inst_5 : ContinuousConstSMul Γ T
x : T
V : Set T
V_cpt : IsCompact V
V_nhd : V ∈ 𝓝 x
Γ₀ : Set Γ := {γ : Γ | ((fun (x : T) ↦ γ • x) '' V ∩ V).Nonempty ∧ γ • x ≠ x}
this : Finite.{u_4 + 1} (↑Γ₀ : Type u_4)
u v : (γ : (↑Γ₀ : Type u_4)) → Set T
hu : ∀ (γ : (↑Γ₀ : Type u_4)), u γ ∈ 𝓝 ((↑γ : Γ) • x)
hv : ∀ (γ : (↑Γ₀ : Type u_4)), v γ ∈ 𝓝 x
u_v_disjoint : ∀ (γ : (↑Γ₀ : Type u_4)), Disjoint (u γ) (v γ)
γ_1 : Γ
z : T
hz : z ∈ V ∧ ∀ (i : (↑Γ₀ : Type u_4)), z ∈ (fun (x : T) ↦ (↑i : Γ) • x) ⁻¹' u i ∩ v i
hγz :
  (fun (x : T) ↦ γ_1 • x) z ∈ V ∧
    ∀ (i : (↑Γ₀ : Type u_4)), (fun (x : T) ↦ γ_1 • x) z ∈ (fun (x : T) ↦ (↑i : Γ) • x) ⁻¹' u i ∩ v i
h : ¬γ_1 • x = x
γ : (↑Γ₀ : Type u_4) := Subtype.mk (p := fun (x : Γ) ↦ x ∈ Γ₀) γ_1 ⋯
⊢ False

Tactic:
(u_v_disjoint γ).le_bot ⟨(hz.2 γ).1, (hγz.2 γ).2⟩

Premises used: Disjoint.le_bot, Set.Mem, And.right, And.left, And.intro
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
Γ : Type u_4
T : Type u_5
inst : TopologicalSpace T
inst_1 : SMul Γ T
inst_2 : ProperlyDiscontinuousSMul Γ T
inst_3 : T2Space T
inst_4 : LocallyCompactSpace T
inst_5 : ContinuousConstSMul Γ T
x : T
V : Set T
V_cpt : IsCompact V
V_nhd : V ∈ 𝓝 x
Γ₀ : Set Γ := {γ : Γ | ((fun (x : T) ↦ γ • x) '' V ∩ V).Nonempty ∧ γ • x ≠ x}
this : Finite.{u_4 + 1} (↑Γ₀ : Type u_4)
u v : (γ : (↑Γ₀ : Type u_4)) → Set T
hu : ∀ (γ : (↑Γ₀ : Type u_4)), u γ ∈ 𝓝 ((↑γ : Γ) • x)
hv : ∀ (γ : (↑Γ₀ : Type u_4)), v γ ∈ 𝓝 x
u_v_disjoint : ∀ (γ : (↑Γ₀ : Type u_4)), Disjoint (u γ) (v γ)
γ_1 : Γ
z : T
hz : z ∈ V ∧ ∀ (i : (↑Γ₀ : Type u_4)), z ∈ (fun (x : T) ↦ (↑i : Γ) • x) ⁻¹' u i ∩ v i
hγz :
  (fun (x : T) ↦ γ_1 • x) z ∈ V ∧
    ∀ (i : (↑Γ₀ : Type u_4)), (fun (x : T) ↦ γ_1 • x) z ∈ (fun (x : T) ↦ (↑i : Γ) • x) ⁻¹' u i ∩ v i
h : ¬γ_1 • x = x
γ : (↑Γ₀ : Type u_4) := Subtype.mk (p := fun (x : Γ) ↦ x ∈ Γ₀) γ_1 ⋯
⊢ False

Tactic:
exact (u_v_disjoint γ).le_bot ⟨(hz.2 γ).1, (hγz.2 γ).2⟩

Premises used: Disjoint.le_bot, And.right, And.left, And.intro
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
Γ : Type u_4
T : Type u_5
inst : TopologicalSpace T
inst_1 : SMul Γ T
inst_2 : ProperlyDiscontinuousSMul Γ T
inst_3 : T2Space T
inst_4 : LocallyCompactSpace T
inst_5 : ContinuousConstSMul Γ T
x : T
⊢ ∃ U ∈ 𝓝 x, ∀ (γ : Γ), ((fun (x : T) ↦ γ • x) '' U ∩ U).Nonempty → γ • x = x

Tactic:
exists_nhds_image_smul_eq_self Γ x

Premises used: ProperlyDiscontinuousSMul.exists_nhds_image_smul_eq_self
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
Γ : Type u_4
T : Type u_5
inst : TopologicalSpace T
inst_1 : SMul Γ T
inst_2 : ProperlyDiscontinuousSMul Γ T
inst_3 : T2Space T
inst_4 : LocallyCompactSpace T
inst_5 : ContinuousConstSMul Γ T
x : T
h :
  ∀ (x_1 : Set T) (a : Γ),
    a • x ≠ x → Disjoint ((fun (x : T) ↦ a • x) '' x_1) x_1 ↔ ((fun (x : T) ↦ a • x) '' x_1 ∩ x_1).Nonempty → a • x = x
⊢ ∃ U ∈ 𝓝 x, ∀ (γ : Γ), γ • x ≠ x → Disjoint ((fun (x : T) ↦ γ • x) '' U) U

Tactic:
convert! exists_nhds_image_smul_eq_self Γ x using 4

Premises used: ProperlyDiscontinuousSMul.exists_nhds_image_smul_eq_self
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
Γ : Type u_4
T : Type u_5
inst : TopologicalSpace T
inst_1 : SMul Γ T
inst_2 : ProperlyDiscontinuousSMul Γ T
inst_3 : T2Space T
inst_4 : LocallyCompactSpace T
inst_5 : ContinuousConstSMul Γ T
x : T
x_1 : Set T
a : Γ
h :
  ¬Disjoint ((fun (x : T) ↦ a • x) '' x_1) x_1 → ¬a • x ≠ x ↔ ((fun (x : T) ↦ a • x) '' x_1 ∩ x_1).Nonempty → a • x = x
⊢ a • x ≠ x → Disjoint ((fun (x : T) ↦ a • x) '' x_1) x_1 ↔ ((fun (x : T) ↦ a • x) '' x_1 ∩ x_1).Nonempty → a • x = x

Tactic:
rw [← not_imp_not]

Premises used: not_imp_not
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
Γ : Type u_4
T : Type u_5
inst : TopologicalSpace T
inst_1 : SMul Γ T
inst_2 : ProperlyDiscontinuousSMul Γ T
inst_3 : T2Space T
inst_4 : LocallyCompactSpace T
inst_5 : ContinuousConstSMul Γ T
x : T
x_1 : Set T
a : Γ
⊢ ¬Disjoint ((fun (x : T) ↦ a • x) '' x_1) x_1 → ¬a • x ≠ x ↔ ((fun (x : T) ↦ a • x) '' x_1 ∩ x_1).Nonempty → a • x = x

Tactic:
simp [Set.not_disjoint_iff_nonempty_inter]

Premises used: Set.not_disjoint_iff_nonempty_inter
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
Γ : Type u_4
inst : Group Γ
T : Type u_5
inst_1 : TopologicalSpace T
inst_2 : MulAction Γ T
inst_3 : ProperlyDiscontinuousSMul Γ T
x : T
⊢ (↑(MulAction.stabilizer Γ x) : Set Γ).Finite

Tactic:
ProperlyDiscontinuousSMul.finite_stabilizer' Γ x

Premises used: setOf, ProperlyDiscontinuousSMul.finite_stabilizer'
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
Γ : Type u_4
inst : Group Γ
T : Type u_5
inst_1 : TopologicalSpace T
inst_2 : MulAction Γ T
inst_3 : ContinuousConstSMul Γ T
U : Set T
hU : IsOpen[inst_1] U
rw : IsOpen[inst_1] (⋃ (g : Γ), (fun (x : T) ↦ g • x) '' U)
⊢ IsOpen[instTopologicalSpaceQuotient] (Quotient.mk' '' U)

Tactic:
rw [isOpen_coinduced, MulAction.quotient_preimage_image_eq_union_mul U]

Premises used: isOpen_coinduced, MulAction.quotient_preimage_image_eq_union_mul
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
Γ : Type u_4
inst : Group Γ
T : Type u_5
inst_1 : TopologicalSpace T
inst_2 : MulAction Γ T
inst_3 : ContinuousConstSMul Γ T
U : Set T
hU : IsOpen[inst_1] U
⊢ IsOpen[inst_1] (⋃ (g : Γ), (fun (x : T) ↦ g • x) '' U)

Tactic:
isOpen_iUnion fun γ => isOpenMap_smul γ U hU

Premises used: isOpen_iUnion, isOpenMap_smul
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
Γ : Type u_4
inst : Group Γ
T : Type u_5
inst_1 : TopologicalSpace T
inst_2 : MulAction Γ T
inst_3 : ContinuousConstSMul Γ T
U : Set T
hU : IsOpen[inst_1] U
⊢ IsOpen[inst_1] (⋃ (g : Γ), (fun (x : T) ↦ g • x) '' U)

Tactic:
exact isOpen_iUnion fun γ => isOpenMap_smul γ U hU

Premises used: isOpen_iUnion, isOpenMap_smul
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
Γ : Type u_4
inst : Group Γ
T : Type u_5
inst_1 : TopologicalSpace T
inst_2 : MulAction Γ T
inst_3 : ContinuousConstSMul Γ T
⊢ IsOpenQuotientMap (Quotient.mk (orbitRel Γ T))

Tactic:
⟨Quot.mk_surjective, continuous_quot_mk, isOpenMap_quotient_mk'_mul⟩

Premises used: IsOpenQuotientMap.mk, isOpenMap_quotient_mk'_mul, continuous_quot_mk, Quot.mk_surjective
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst : Group Γ
T : Type u_5
inst_1 : TopologicalSpace T
inst_2 : MulAction Γ T
inst_3 : T2Space T
inst_4 : LocallyCompactSpace T
inst_5 : ContinuousConstSMul Γ T
inst_6 : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
rw : Pairwise fun (x y : Quotient (MulAction.orbitRel Γ T)) ↦ ∃ U ∈ 𝓝 x, ∃ V ∈ 𝓝 y, Disjoint U V
⊢ T2Space.{u_5} (Quotient (MulAction.orbitRel Γ T))

Tactic:
rw [t2Space_iff_nhds]

Premises used: t2Space_iff_nhds
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst : Group Γ
T : Type u_5
inst_1 : TopologicalSpace T
inst_2 : MulAction Γ T
inst_3 : T2Space T
inst_4 : LocallyCompactSpace T
inst_5 : ContinuousConstSMul Γ T
inst_6 : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
⊢ IsOpenMap f

Tactic:
have f_op : IsOpenMap f := isOpenMap_quotient_mk'_mul
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst : Group Γ
T : Type u_5
inst_1 : TopologicalSpace T
inst_2 : MulAction Γ T
inst_3 : T2Space T
inst_4 : LocallyCompactSpace T
inst_5 : ContinuousConstSMul Γ T
inst_6 : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
i : Quotient (MulAction.orbitRel Γ T)
x₀ : T
j : Quotient (MulAction.orbitRel Γ T)
y₀ : T
hxy : f x₀ ≠ f y₀
mk : ∃ U ∈ 𝓝 (f x₀), ∃ V ∈ 𝓝 (f y₀), Disjoint U V
⊢ ∃ (U : Set (Quotient (MulAction.orbitRel Γ T))),
    Membership.mem (γ := Filter (Quotient (MulAction.orbitRel Γ T)))
        (𝓝 (Quot.mk (⇑(MulAction.orbitRel Γ T) : T → T → Prop) x₀)) U ∧
      ∃ (V : Set (Quotient (MulAction.orbitRel Γ T))),
        Membership.mem (γ := Filter (Quotient (MulAction.orbitRel Γ T)))
            (𝓝 (Quot.mk (⇑(MulAction.orbitRel Γ T) : T → T → Prop) y₀)) V ∧
          Disjoint U V

Tactic:
change ∃ U ∈ 𝓝 (f x₀), ∃ V ∈ 𝓝 (f y₀), _

Premises used: nhds
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst : Group Γ
T : Type u_5
inst_1 : TopologicalSpace T
inst_2 : MulAction Γ T
inst_3 : T2Space T
inst_4 : LocallyCompactSpace T
inst_5 : ContinuousConstSMul Γ T
inst_6 : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
i : Quotient (MulAction.orbitRel Γ T)
x₀ : T
j : Quotient (MulAction.orbitRel Γ T)
y₀ : T
hxy : f x₀ ≠ f y₀
⊢ ∀ (γ : Γ), γ • x₀ ≠ y₀

Tactic:
have hγx₀y₀ : ∀ γ : Γ, γ • x₀ ≠ y₀ := not_exists.mp (mt Quotient.sound hxy.symm :)
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst : Group Γ
T : Type u_5
inst_1 : TopologicalSpace T
inst_2 : MulAction Γ T
inst_3 : T2Space T
inst_4 : LocallyCompactSpace T
inst_5 : ContinuousConstSMul Γ T
inst_6 : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
i : Quotient (MulAction.orbitRel Γ T)
x₀ : T
j : Quotient (MulAction.orbitRel Γ T)
y₀ : T
hxy : f x₀ ≠ f y₀
hγx₀y₀ : ∀ (γ : Γ), γ • x₀ ≠ y₀
mk : ∀ (K₀ : Set T) (hK₀ : IsCompact K₀) (K₀_in : K₀ ∈ 𝓝 x₀), ∃ U ∈ 𝓝 (f x₀), ∃ V ∈ 𝓝 (f y₀), Disjoint U V
⊢ ∃ U ∈ 𝓝 (f x₀), ∃ V ∈ 𝓝 (f y₀), Disjoint U V

Tactic:
obtain ⟨K₀, hK₀, K₀_in⟩ := exists_compact_mem_nhds x₀

Premises used: WeaklyLocallyCompactSpace.exists_compact_mem_nhds
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst : Group Γ
T : Type u_5
inst_1 : TopologicalSpace T
inst_2 : MulAction Γ T
inst_3 : T2Space T
inst_4 : LocallyCompactSpace T
inst_5 : ContinuousConstSMul Γ T
inst_6 : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
i : Quotient (MulAction.orbitRel Γ T)
x₀ : T
j : Quotient (MulAction.orbitRel Γ T)
y₀ : T
hxy : f x₀ ≠ f y₀
hγx₀y₀ : ∀ (γ : Γ), γ • x₀ ≠ y₀
K₀ : Set T
hK₀ : IsCompact K₀
K₀_in : K₀ ∈ 𝓝 x₀
mk : ∀ (L₀ : Set T) (hL₀ : IsCompact L₀) (L₀_in : L₀ ∈ 𝓝 y₀), ∃ U ∈ 𝓝 (f x₀), ∃ V ∈ 𝓝 (f y₀), Disjoint U V
⊢ ∃ U ∈ 𝓝 (f x₀), ∃ V ∈ 𝓝 (f y₀), Disjoint U V

Tactic:
obtain ⟨L₀, hL₀, L₀_in⟩ := exists_compact_mem_nhds y₀

Premises used: WeaklyLocallyCompactSpace.exists_compact_mem_nhds
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst : Group Γ
T : Type u_5
inst_1 : TopologicalSpace T
inst_2 : MulAction Γ T
inst_3 : T2Space T
inst_4 : LocallyCompactSpace T
inst_5 : ContinuousConstSMul Γ T
inst_6 : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
i : Quotient (MulAction.orbitRel Γ T)
x₀ : T
j : Quotient (MulAction.orbitRel Γ T)
y₀ : T
hxy : f x₀ ≠ f y₀
hγx₀y₀ : ∀ (γ : Γ), γ • x₀ ≠ y₀
K₀ : Set T
hK₀ : IsCompact K₀
K₀_in : K₀ ∈ 𝓝 x₀
L₀ : Set T
hL₀ : IsCompact L₀
L₀_in : L₀ ∈ 𝓝 y₀
bad_Γ_set : Set Γ := {γ : Γ | ((fun (x : T) ↦ γ • x) '' K₀ ∩ L₀).Nonempty}
⊢ bad_Γ_set.Finite

Tactic:
have bad_Γ_finite : bad_Γ_set.Finite := finite_disjoint_inter_image (Γ := Γ) hK₀ hL₀
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst : Group Γ
T : Type u_5
inst_1 : TopologicalSpace T
inst_2 : MulAction Γ T
inst_3 : T2Space T
inst_4 : LocallyCompactSpace T
inst_5 : ContinuousConstSMul Γ T
inst_6 : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
i : Quotient (MulAction.orbitRel Γ T)
x₀ : T
j : Quotient (MulAction.orbitRel Γ T)
y₀ : T
hxy : f x₀ ≠ f y₀
hγx₀y₀ : ∀ (γ : Γ), γ • x₀ ≠ y₀
K₀ : Set T
hK₀ : IsCompact K₀
K₀_in : K₀ ∈ 𝓝 x₀
L₀ : Set T
hL₀ : IsCompact L₀
L₀_in : L₀ ∈ 𝓝 y₀
bad_Γ_set : Set Γ := {γ : Γ | ((fun (x : T) ↦ γ • x) '' K₀ ∩ L₀).Nonempty}
bad_Γ_finite : bad_Γ_set.Finite
mk :
  ∀ (u v : (γ : Γ) → Set T) (hu : ∀ (γ : Γ), u γ ∈ 𝓝 (γ • x₀)) (hv : ∀ (γ : Γ), v γ ∈ 𝓝 y₀)
    (u_v_disjoint : ∀ (γ : Γ), Disjoint (u γ) (v γ)), ∃ U ∈ 𝓝 (f x₀), ∃ V ∈ 𝓝 (f y₀), Disjoint U V
⊢ ∃ U ∈ 𝓝 (f x₀), ∃ V ∈ 𝓝 (f y₀), Disjoint U V

Tactic:
choose u v hu hv u_v_disjoint using fun γ => t2_separation_nhds (hγx₀y₀ γ)

Premises used: t2_separation_nhds
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst : Group Γ
T : Type u_5
inst_1 : TopologicalSpace T
inst_2 : MulAction Γ T
inst_3 : T2Space T
inst_4 : LocallyCompactSpace T
inst_5 : ContinuousConstSMul Γ T
inst_6 : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
i : Quotient (MulAction.orbitRel Γ T)
x₀ : T
j : Quotient (MulAction.orbitRel Γ T)
y₀ : T
hxy : f x₀ ≠ f y₀
hγx₀y₀ : ∀ (γ : Γ), γ • x₀ ≠ y₀
K₀ : Set T
hK₀ : IsCompact K₀
K₀_in : K₀ ∈ 𝓝 x₀
L₀ : Set T
hL₀ : IsCompact L₀
L₀_in : L₀ ∈ 𝓝 y₀
bad_Γ_set : Set Γ := {γ : Γ | ((fun (x : T) ↦ γ • x) '' K₀ ∩ L₀).Nonempty}
bad_Γ_finite : bad_Γ_set.Finite
u v : (γ : Γ) → Set T
hu : ∀ (γ : Γ), u γ ∈ 𝓝 (γ • x₀)
hv : ∀ (γ : Γ), v γ ∈ 𝓝 y₀
u_v_disjoint : ∀ (γ : Γ), Disjoint (u γ) (v γ)
U₀₀ : Set T := ⋂ γ ∈ bad_Γ_set, (fun (x : T) ↦ γ • x) ⁻¹' u γ
U₀ : Set T := U₀₀ ∩ K₀
V₀₀ : Set T := ⋂ γ ∈ bad_Γ_set, v γ
V₀ : Set T := V₀₀ ∩ L₀
⊢ f '' U₀ ∈ 𝓝 (f x₀)

Tactic:
f_op.image_mem_nhds (inter_mem ((biInter_mem bad_Γ_finite).mpr fun γ _ => ?_) K₀_in)

Premises used: Iff.mpr, Filter.inter_mem, IsOpenMap.image_mem_nhds, Filter.biInter_mem
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst : Group Γ
T : Type u_5
inst_1 : TopologicalSpace T
inst_2 : MulAction Γ T
inst_3 : T2Space T
inst_4 : LocallyCompactSpace T
inst_5 : ContinuousConstSMul Γ T
inst_6 : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
i : Quotient (MulAction.orbitRel Γ T)
x₀ : T
j : Quotient (MulAction.orbitRel Γ T)
y₀ : T
hxy : f x₀ ≠ f y₀
hγx₀y₀ : ∀ (γ : Γ), γ • x₀ ≠ y₀
K₀ : Set T
hK₀ : IsCompact K₀
K₀_in : K₀ ∈ 𝓝 x₀
L₀ : Set T
hL₀ : IsCompact L₀
L₀_in : L₀ ∈ 𝓝 y₀
bad_Γ_set : Set Γ := {γ : Γ | ((fun (x : T) ↦ γ • x) '' K₀ ∩ L₀).Nonempty}
bad_Γ_finite : bad_Γ_set.Finite
u v : (γ : Γ) → Set T
hu : ∀ (γ : Γ), u γ ∈ 𝓝 (γ • x₀)
hv : ∀ (γ : Γ), v γ ∈ 𝓝 y₀
u_v_disjoint : ∀ (γ : Γ), Disjoint (u γ) (v γ)
U₀₀ : Set T := ⋂ γ ∈ bad_Γ_set, (fun (x : T) ↦ γ • x) ⁻¹' u γ
U₀ : Set T := U₀₀ ∩ K₀
V₀₀ : Set T := ⋂ γ ∈ bad_Γ_set, v γ
V₀ : Set T := V₀₀ ∩ L₀
refine : ∀ γ ∈ bad_Γ_set, (fun (x : T) ↦ γ • x) ⁻¹' u γ ∈ 𝓝 x₀
⊢ f '' U₀ ∈ 𝓝 (f x₀)

Tactic:
refine f_op.image_mem_nhds (inter_mem ((biInter_mem bad_Γ_finite).mpr fun γ _ => ?_) K₀_in)

Premises used: Iff.mpr, Filter.inter_mem, IsOpenMap.image_mem_nhds, Filter.biInter_mem
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst : Group Γ
T : Type u_5
inst_1 : TopologicalSpace T
inst_2 : MulAction Γ T
inst_3 : T2Space T
inst_4 : LocallyCompactSpace T
inst_5 : ContinuousConstSMul Γ T
inst_6 : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
i : Quotient (MulAction.orbitRel Γ T)
x₀ : T
j : Quotient (MulAction.orbitRel Γ T)
y₀ : T
hxy : f x₀ ≠ f y₀
hγx₀y₀ : ∀ (γ : Γ), γ • x₀ ≠ y₀
K₀ : Set T
hK₀ : IsCompact K₀
K₀_in : K₀ ∈ 𝓝 x₀
L₀ : Set T
hL₀ : IsCompact L₀
L₀_in : L₀ ∈ 𝓝 y₀
bad_Γ_set : Set Γ := {γ : Γ | ((fun (x : T) ↦ γ • x) '' K₀ ∩ L₀).Nonempty}
bad_Γ_finite : bad_Γ_set.Finite
u v : (γ : Γ) → Set T
hu : ∀ (γ : Γ), u γ ∈ 𝓝 (γ • x₀)
hv : ∀ (γ : Γ), v γ ∈ 𝓝 y₀
u_v_disjoint : ∀ (γ : Γ), Disjoint (u γ) (v γ)
U₀₀ : Set T := ⋂ γ ∈ bad_Γ_set, (fun (x : T) ↦ γ • x) ⁻¹' u γ
U₀ : Set T := U₀₀ ∩ K₀
V₀₀ : Set T := ⋂ γ ∈ bad_Γ_set, v γ
V₀ : Set T := V₀₀ ∩ L₀
γ : Γ
h : γ ∈ bad_Γ_set
⊢ (fun (x : T) ↦ γ • x) ⁻¹' u γ ∈ 𝓝 x₀

Tactic:
(continuous_const_smul _).continuousAt (hu γ)

Premises used: ContinuousConstSMul.continuous_const_smul, Set.Mem, setOf, Continuous.continuousAt, Set.preimage