awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact (continuous_const_smul _).continuousAt (hu γ)

Premises used: ContinuousConstSMul.continuous_const_smul, Continuous.continuousAt
-- 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:
have U_nhds : f '' U₀ ∈ 𝓝 (f x₀) := by
    refine f_op.image_mem_nhds (inter_mem ((biInter_mem bad_Γ_finite).mpr fun γ _ => ?_) K₀_in)
    exact (continuous_const_smul _).continuousAt (hu γ)
-- 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₀
U_nhds : f '' U₀ ∈ 𝓝 (f x₀)
⊢ f '' V₀ ∈ 𝓝 (f y₀)

Tactic:
have V_nhds : f '' V₀ ∈ 𝓝 (f y₀) :=
    f_op.image_mem_nhds (inter_mem ((biInter_mem bad_Γ_finite).mpr fun γ _ => hv γ) L₀_in)
-- 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₀
U_nhds : f '' U₀ ∈ 𝓝 (f x₀)
V_nhds : f '' V₀ ∈ 𝓝 (f y₀)
⊢ ∃ U ∈ 𝓝 (f x₀), ∃ V ∈ 𝓝 (f y₀), Disjoint U V

Tactic:
⟨f '' U₀, U_nhds, f '' V₀, V_nhds, MulAction.disjoint_image_image_iff.2 ?_⟩

Premises used: Iff.mpr, MulAction.disjoint_image_image_iff, And.intro, Exists.intro, Set.image
-- 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₀
U_nhds : f '' U₀ ∈ 𝓝 (f x₀)
V_nhds : f '' V₀ ∈ 𝓝 (f y₀)
mk : ∀ x ∈ U₀, ∀ (g : Γ), g • x ∉ V₀
⊢ ∃ U ∈ 𝓝 (f x₀), ∃ V ∈ 𝓝 (f y₀), Disjoint U V

Tactic:
refine ⟨f '' U₀, U_nhds, f '' V₀, V_nhds, MulAction.disjoint_image_image_iff.2 ?_⟩
-- 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₀
U_nhds : f '' U₀ ∈ 𝓝 (f x₀)
V_nhds : f '' V₀ ∈ 𝓝 (f y₀)
x : T
x_in_U₀₀ : x ∈ U₀₀
x_in_K₀ : x ∈ K₀
γ : Γ
pos : ∀ (H : γ ∈ bad_Γ_set), γ • x ∉ V₀
neg : ∀ (H : γ ∉ bad_Γ_set), γ • x ∉ V₀
⊢ γ • x ∉ V₀

Tactic:
by_cases H : γ ∈ bad_Γ_set
-- 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₀
U_nhds : f '' U₀ ∈ 𝓝 (f x₀)
V_nhds : f '' V₀ ∈ 𝓝 (f y₀)
x : T
x_in_U₀₀ : x ∈ U₀₀
x_in_K₀ : x ∈ K₀
γ : Γ
H : γ ∈ bad_Γ_set
⊢ γ • x ∉ V₀

Tactic:
fun h => (u_v_disjoint γ).le_bot ⟨mem_iInter₂.mp x_in_U₀₀ γ H, mem_iInter₂.mp h.1 γ H⟩

Premises used: Disjoint.le_bot, Set.Mem, Set.mem_iInter₂, And.left, And.intro, Iff.mp, Not
-- 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₀
U_nhds : f '' U₀ ∈ 𝓝 (f x₀)
V_nhds : f '' V₀ ∈ 𝓝 (f y₀)
x : T
x_in_U₀₀ : x ∈ U₀₀
x_in_K₀ : x ∈ K₀
γ : Γ
H : γ ∈ bad_Γ_set
⊢ γ • x ∉ V₀

Tactic:
exact fun h => (u_v_disjoint γ).le_bot ⟨mem_iInter₂.mp x_in_U₀₀ γ H, mem_iInter₂.mp h.1 γ H⟩

Premises used: Disjoint.le_bot, Set.mem_iInter₂, And.intro, Iff.mp
-- 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₀
U_nhds : f '' U₀ ∈ 𝓝 (f x₀)
V_nhds : f '' V₀ ∈ 𝓝 (f y₀)
x : T
x_in_U₀₀ : x ∈ U₀₀
x_in_K₀ : x ∈ K₀
γ : Γ
H : γ ∉ bad_Γ_set
h' : γ • x ∈ L₀
⊢ γ • K₀ ∩ L₀ = ∅

Tactic:
simp only [bad_Γ_set, image_smul, not_nonempty_iff_eq_empty, mem_setOf_eq] at H

Premises used: Set.image_smul, Set.not_nonempty_iff_eq_empty, Set.mem_setOf_eq
-- 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₀
U_nhds : f '' U₀ ∈ 𝓝 (f x₀)
V_nhds : f '' V₀ ∈ 𝓝 (f y₀)
x : T
x_in_U₀₀ : x ∈ U₀₀
x_in_K₀ : x ∈ K₀
γ : Γ
h' : γ • x ∈ L₀
H : γ • K₀ ∩ L₀ = ∅
⊢ False

Tactic:
eq_empty_iff_forall_notMem.mp H (γ • x) ⟨mem_image_of_mem _ x_in_K₀, h'⟩

Premises used: Set.eq_empty_iff_forall_notMem, Set.mem_image_of_mem, And.intro, Iff.mp, HSMul.hSMul
-- 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₀
U_nhds : f '' U₀ ∈ 𝓝 (f x₀)
V_nhds : f '' V₀ ∈ 𝓝 (f y₀)
x : T
x_in_U₀₀ : x ∈ U₀₀
x_in_K₀ : x ∈ K₀
γ : Γ
h' : γ • x ∈ L₀
H : γ • K₀ ∩ L₀ = ∅
⊢ False

Tactic:
exact eq_empty_iff_forall_notMem.mp H (γ • x) ⟨mem_image_of_mem _ x_in_K₀, h'⟩

Premises used: Set.eq_empty_iff_forall_notMem, Set.mem_image_of_mem, And.intro, Iff.mp, HSMul.hSMul
-- 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 : SecondCountableTopology T
inst_4 : ContinuousConstSMul Γ T
⊢ SecondCountableTopology.{u_5} (Quotient (MulAction.orbitRel Γ T))

Tactic:
TopologicalSpace.Quotient.secondCountableTopology isOpenMap_quotient_mk'_mul

Premises used: TopologicalSpace.Quotient.secondCountableTopology, isOpenMap_quotient_mk'_mul
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
G₀ : Type u_6
inst : GroupWithZero G₀
inst_1 : MulAction G₀ α
inst_2 : TopologicalSpace α
inst_3 : ContinuousConstSMul G₀ α
c : G₀
s : Set α
x : α
hc : c ≠ 0
⊢ c • s ∈ 𝓝 (c • x) ↔ s ∈ 𝓝 x

Tactic:
smul_mem_nhds_smul_iff (Units.mk0 c hc)

Premises used: Set.Mem, Units.mk0, smul_mem_nhds_smul_iff
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
G₀ : Type u_6
inst : GroupWithZero G₀
inst_1 : AddMonoid α
inst_2 : DistribMulAction G₀ α
inst_3 : TopologicalSpace α
inst_4 : ContinuousConstSMul G₀ α
s : Set α
c : G₀
hc : c ≠ 0
⊢ Membership.mem (γ := Filter α) (𝓝 0) (c • s) ↔ Membership.mem (γ := Filter α) (𝓝 0) s

Tactic:
Iff.trans ?_ (smul_mem_nhds_smul_iff₀ hc)

Premises used: smul_mem_nhds_smul_iff₀, Iff.trans
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
G₀ : Type u_6
inst : GroupWithZero G₀
inst_1 : AddMonoid α
inst_2 : DistribMulAction G₀ α
inst_3 : TopologicalSpace α
inst_4 : ContinuousConstSMul G₀ α
s : Set α
c : G₀
hc : c ≠ 0
refine : Membership.mem (γ := Filter α) (𝓝 0) (c • s) ↔ c • s ∈ 𝓝 (HSMul.hSMul (β := α) c 0)
⊢ Membership.mem (γ := Filter α) (𝓝 0) (c • s) ↔ Membership.mem (γ := Filter α) (𝓝 0) s

Tactic:
refine Iff.trans ?_ (smul_mem_nhds_smul_iff₀ hc)

Premises used: smul_mem_nhds_smul_iff₀, Iff.trans
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
G₀ : Type u_6
inst : GroupWithZero G₀
inst_1 : AddMonoid α
inst_2 : DistribMulAction G₀ α
inst_3 : TopologicalSpace α
inst_4 : ContinuousConstSMul G₀ α
s : Set α
c : G₀
hc : c ≠ 0
rw rw₁ : Membership.mem (γ := Filter α) (𝓝 0) (c • s) ↔ Membership.mem (γ := Filter α) (𝓝 0) (c • s)
⊢ Membership.mem (γ := Filter α) (𝓝 0) (c • s) ↔ c • s ∈ 𝓝 (HSMul.hSMul (β := α) c 0)

Tactic:
rw [smul_zero]

Premises used: smul_zero
-- Module: Mathlib.Topology.Algebra.Constructions.DomMulAct
Goal:
M : Type u_1
inst : TopologicalSpace M
⊢ Continuous[inst, instTopologicalSpace] (⇑mk : (a : M) → Mᵈᵐᵃ)

Tactic:
continuous_induced_rng.2 continuous_id

Premises used: Iff.mpr, continuous_id, continuous_induced_rng
-- Module: Mathlib.Topology.Algebra.Constructions.DomMulAct
Goal:
M : Type u_1
inst : TopologicalSpace M
⊢ Continuous[instTopologicalSpace, inst] (⇑(Equiv.symm mk) : (a : Mᵈᵐᵃ) → M)

Tactic:
continuous_induced_dom

Premises used: continuous_induced_dom
-- Module: Mathlib.Topology.Algebra.Constructions.DomMulAct
Goal:
M : Type u_1
inst : TopologicalSpace M
⊢ Eq.{u_1 + 1} (α := (a : M) → Mᵈᵐᵃ) (⇑mkHomeomorph : (a : M) → Mᵈᵐᵃ) (⇑mk : (a : M) → Mᵈᵐᵃ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Constructions.DomMulAct
Goal:
M : Type u_1
inst : TopologicalSpace M
⊢ Eq.{u_1 + 1} (α := (a : Mᵈᵐᵃ) → M) (⇑(Homeomorph.symm mkHomeomorph) : (a : Mᵈᵐᵃ) → M)
    (⇑(Equiv.symm mk) : (a : Mᵈᵐᵃ) → M)

Tactic:
rfl

Premises used: MulOpposite.opEquiv, DomMulAct.mk, rfl
-- Module: Mathlib.Topology.Algebra.Constructions.DomMulAct
Goal:
M : Type u_1
inst : TopologicalSpace M
⊢ IsInducing.{u_1, u_1} (X := M) (Y := Mᵈᵐᵃ) (⇑mk : (a : M) → Mᵈᵐᵃ)

Tactic:
mkHomeomorph.isInducing

Premises used: Homeomorph.isInducing, DomMulAct.mkHomeomorph
-- Module: Mathlib.Topology.Algebra.Constructions.DomMulAct
Goal:
M : Type u_1
inst : TopologicalSpace M
⊢ IsEmbedding.{u_1, u_1} (X := M) (Y := Mᵈᵐᵃ) (⇑mk : (a : M) → Mᵈᵐᵃ)

Tactic:
mkHomeomorph.isEmbedding

Premises used: Homeomorph.isEmbedding, DomMulAct.mkHomeomorph
-- Module: Mathlib.Topology.Algebra.Constructions.DomMulAct
Goal:
M : Type u_1
inst : TopologicalSpace M
⊢ IsOpenEmbedding.{u_1, u_1} (X := M) (Y := Mᵈᵐᵃ) (⇑mk : (a : M) → Mᵈᵐᵃ)

Tactic:
mkHomeomorph.isOpenEmbedding

Premises used: DomMulAct.mkHomeomorph, Homeomorph.isOpenEmbedding
-- Module: Mathlib.Topology.Algebra.Constructions.DomMulAct
Goal:
M : Type u_1
inst : TopologicalSpace M
⊢ IsClosedEmbedding.{u_1, u_1} (X := M) (Y := Mᵈᵐᵃ) (⇑mk : (a : M) → Mᵈᵐᵃ)

Tactic:
mkHomeomorph.isClosedEmbedding

Premises used: DomMulAct.mkHomeomorph, Homeomorph.isClosedEmbedding
-- Module: Mathlib.Topology.Algebra.Constructions.DomMulAct
Goal:
M : Type u_1
inst : TopologicalSpace M
⊢ IsQuotientMap.{u_1, u_1} (X := M) (Y := Mᵈᵐᵃ) (⇑mk : (a : M) → Mᵈᵐᵃ)

Tactic:
mkHomeomorph.isQuotientMap

Premises used: DomMulAct.mkHomeomorph, Homeomorph.isQuotientMap
-- Module: Mathlib.Topology.Algebra.Constructions.DomMulAct
Goal:
M : Type u_1
inst : TopologicalSpace M
⊢ IsInducing.{u_1, u_1} (X := Mᵈᵐᵃ) (Y := M) (⇑(Equiv.symm mk) : (a : Mᵈᵐᵃ) → M)

Tactic:
mkHomeomorph.symm.isInducing

Premises used: Homeomorph.isInducing, MulOpposite.opEquiv, DomMulAct.mkHomeomorph, DomMulAct.mk, Homeomorph.symm
-- Module: Mathlib.Topology.Algebra.Constructions.DomMulAct
Goal:
M : Type u_1
inst : TopologicalSpace M
⊢ IsEmbedding.{u_1, u_1} (X := Mᵈᵐᵃ) (Y := M) (⇑(Equiv.symm mk) : (a : Mᵈᵐᵃ) → M)

Tactic:
mkHomeomorph.symm.isEmbedding

Premises used: MulOpposite.opEquiv, Homeomorph.isEmbedding, DomMulAct.mkHomeomorph, DomMulAct.mk, Homeomorph.symm
-- Module: Mathlib.Topology.Algebra.Constructions.DomMulAct
Goal:
M : Type u_1
inst : TopologicalSpace M
⊢ IsOpenEmbedding.{u_1, u_1} (X := Mᵈᵐᵃ) (Y := M) (⇑(Equiv.symm mk) : (a : Mᵈᵐᵃ) → M)

Tactic:
mkHomeomorph.symm.isOpenEmbedding

Premises used: MulOpposite.opEquiv, DomMulAct.mkHomeomorph, DomMulAct.mk, Homeomorph.symm, Homeomorph.isOpenEmbedding
-- Module: Mathlib.Topology.Algebra.Constructions.DomMulAct
Goal:
M : Type u_1
inst : TopologicalSpace M
⊢ IsClosedEmbedding.{u_1, u_1} (X := Mᵈᵐᵃ) (Y := M) (⇑(Equiv.symm mk) : (a : Mᵈᵐᵃ) → M)

Tactic:
mkHomeomorph.symm.isClosedEmbedding

Premises used: MulOpposite.opEquiv, DomMulAct.mkHomeomorph, DomMulAct.mk, Homeomorph.symm, Homeomorph.isClosedEmbedding
-- Module: Mathlib.Topology.Algebra.Constructions.DomMulAct
Goal:
M : Type u_1
inst : TopologicalSpace M
⊢ IsQuotientMap.{u_1, u_1} (X := Mᵈᵐᵃ) (Y := M) (⇑(Equiv.symm mk) : (a : Mᵈᵐᵃ) → M)

Tactic:
mkHomeomorph.symm.isQuotientMap

Premises used: MulOpposite.opEquiv, DomMulAct.mkHomeomorph, DomMulAct.mk, Homeomorph.symm, Homeomorph.isQuotientMap
-- Module: Mathlib.Topology.Algebra.Constructions.DomMulAct
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : T0Space M
⊢ T0Space.{u_1} Mᵈᵐᵃ

Tactic:
mkHomeomorph.t0Space

Premises used: DomMulAct.mkHomeomorph, Homeomorph.t0Space
-- Module: Mathlib.Topology.Algebra.Constructions.DomMulAct
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : T1Space M
⊢ T1Space.{u_1} Mᵈᵐᵃ

Tactic:
mkHomeomorph.t1Space

Premises used: DomMulAct.mkHomeomorph, Homeomorph.t1Space
-- Module: Mathlib.Topology.Algebra.Constructions.DomMulAct
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : T2Space M
⊢ T2Space.{u_1} Mᵈᵐᵃ

Tactic:
mkHomeomorph.t2Space

Premises used: DomMulAct.mkHomeomorph, Homeomorph.t2Space
-- Module: Mathlib.Topology.Algebra.Constructions.DomMulAct
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : T25Space M
⊢ T25Space.{u_1} Mᵈᵐᵃ

Tactic:
mkHomeomorph.t25Space

Premises used: DomMulAct.mkHomeomorph, Homeomorph.t25Space
-- Module: Mathlib.Topology.Algebra.Constructions.DomMulAct
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : T3Space M
⊢ T3Space.{u_1} Mᵈᵐᵃ

Tactic:
mkHomeomorph.t3Space

Premises used: DomMulAct.mkHomeomorph, Homeomorph.t3Space
-- Module: Mathlib.Topology.Algebra.Constructions.DomMulAct
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : T4Space M
⊢ T4Space.{u_1} Mᵈᵐᵃ

Tactic:
mkHomeomorph.t4Space

Premises used: DomMulAct.mkHomeomorph, Homeomorph.t4Space
-- Module: Mathlib.Topology.Algebra.Constructions.DomMulAct
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : T5Space M
⊢ T5Space.{u_1} Mᵈᵐᵃ

Tactic:
mkHomeomorph.t5Space

Premises used: DomMulAct.mkHomeomorph, Homeomorph.t5Space
-- Module: Mathlib.Topology.Algebra.Constructions.DomMulAct
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : R0Space M
⊢ R0Space.{u_1} Mᵈᵐᵃ

Tactic:
isEmbedding_mk_symm.r0Space

Premises used: Topology.IsInducing.r0Space, Topology.IsEmbedding.toIsInducing, DomMulAct.isEmbedding_mk_symm
-- Module: Mathlib.Topology.Algebra.Constructions.DomMulAct
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : R1Space M
⊢ R1Space.{u_1} Mᵈᵐᵃ

Tactic:
isEmbedding_mk_symm.r1Space

Premises used: Topology.IsInducing.r1Space, Topology.IsEmbedding.toIsInducing, DomMulAct.isEmbedding_mk_symm
-- Module: Mathlib.Topology.Algebra.Constructions.DomMulAct
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : RegularSpace M
⊢ RegularSpace.{u_1} Mᵈᵐᵃ

Tactic:
isEmbedding_mk_symm.regularSpace

Premises used: Topology.IsEmbedding.toIsInducing, Topology.IsInducing.regularSpace, DomMulAct.isEmbedding_mk_symm
-- Module: Mathlib.Topology.Algebra.Constructions.DomMulAct
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : NormalSpace M
⊢ NormalSpace.{u_1} Mᵈᵐᵃ

Tactic:
mkHomeomorph.normalSpace

Premises used: DomMulAct.mkHomeomorph, Homeomorph.normalSpace
-- Module: Mathlib.Topology.Algebra.Constructions.DomMulAct
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : CompletelyNormalSpace M
⊢ CompletelyNormalSpace.{u_1} Mᵈᵐᵃ

Tactic:
isEmbedding_mk_symm.completelyNormalSpace

Premises used: DomMulAct.isEmbedding_mk_symm, Topology.IsEmbedding.completelyNormalSpace