awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
Goal:
G₀ : Type u_4
inst : GroupWithZero G₀
E : Type u_5
inst_1 : Zero E
inst_2 : MulActionWithZero G₀ E
inst_3 : TopologicalSpace E
inst_4 : T1Space E
inst_5 : ContinuousConstSMul G₀ E
c : G₀
inl : IsClosedMap (Y := E) fun (x : E) ↦ HSMul.hSMul.{u_4, u_5, u_5} (α := G₀) 0 x
⊢ IsClosedMap (Y := E) fun (x : E) ↦ c • x
have inr : ∀ (hne : c ≠ 0), IsClosedMap (Y := E) fun (x : E) ↦ c • x
Tactic: rcases eq_or_ne c 0 with (rfl | hne)
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
Goal:
G₀ : Type u_4
inst : GroupWithZero G₀
E : Type u_5
inst_1 : Zero E
inst_2 : MulActionWithZero G₀ E
inst_3 : TopologicalSpace E
inst_4 : T1Space E
inst_5 : ContinuousConstSMul G₀ E
⊢ IsClosedMap (Y := E) fun (x : E) ↦ HSMul.hSMul.{u_4, u_5, u_5} (α := G₀) 0 x
have inl : IsClosedMap (Y := E) fun (x : E) ↦ 0
Tactic: simp only [zero_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Monoid M
inst_1 : TopologicalSpace α
inst_2 : MulAction M α
inst_3 : ContinuousConstSMul M α
S : Type u_4
β : Type u_5
inst_4 : SMul S M
inst_5 : SMul S α
inst_6 : IsScalarTower S M α
inst_7 : SMul S β
f : MulActionHom.{u_4, u_4, u_2, u_5} (M := S) id α β
inst_8 : TopologicalSpace β
hf : IsQuotientMap.{u_2, u_5} (X := α) (Y := β) (⇑f : (a : α) → β)
c : S
hc : IsUnit (HSMul.hSMul (β := M) c 1)
⊢ IsQuotientMap.{u_2, u_5} (X := α) (Y := β) ((fun (x : β) ↦ c • x) ∘ (⇑f : (a : α) → β))
have h : Eq (α := α → β) ((fun (x : β) ↦ c • x) ∘ (⇑f : (a : α) → β))
  (Function.comp (β := α) (⇑f : (a : α) → β) fun (x : α) ↦ HSMul.hSMul (β := M) c 1 • x)
Tactic: convert! hf.comp hc.isHomeomorph_smul.isQuotientMap
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Monoid M
inst_1 : TopologicalSpace α
inst_2 : MulAction M α
inst_3 : ContinuousConstSMul M α
S : Type u_4
β : Type u_5
inst_4 : SMul S M
inst_5 : SMul S α
inst_6 : IsScalarTower S M α
inst_7 : SMul S β
f : MulActionHom.{u_4, u_4, u_2, u_5} (M := S) id α β
inst_8 : TopologicalSpace β
hf : IsQuotientMap.{u_2, u_5} (X := α) (Y := β) (⇑f : (a : α) → β)
c : S
hc : IsUnit (HSMul.hSMul (β := M) c 1)
⊢ Eq (α := α → β) ((fun (x : β) ↦ c • x) ∘ (⇑f : (a : α) → β))
    (Function.comp (β := α) (⇑f : (a : α) → β) fun (x : α) ↦ HSMul.hSMul (β := M) c 1 • x)
have h : ∀ (x : α),
  Eq.{u_5 + 1} (α := β) (((fun (x : β) ↦ c • x) ∘ (⇑f : (a : α) → β)) x)
    (Function.comp (β := α) (⇑f : (a : α) → β) (fun (x : α) ↦ HSMul.hSMul (β := M) c 1 • x) x)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
Goal:
Γ : Type u_4
T : Type u_5
inst : TopologicalSpace T
inst_1 : SMul Γ T
inst_2 : ProperlyDiscontinuousSMul Γ T
x : T
⊢ Set.Finite.{u_4} (α := Γ) {γ : Γ | γ • x = x}
have simp_rw : Set.Finite.{u_4} (α := Γ) {γ : Γ | (image (α := T) (HSMul.hSMul γ) {x} ∩ {x}).Nonempty}
Tactic: simp_rw [← mem_singleton_iff, ← singleton_inter_nonempty, ← image_singleton]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
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
have obtain : ∀ (V : Set T) (V_cpt : IsCompact V) (V_nhd : V ∈ 𝓝 x),
  ∃ U ∈ 𝓝 x, ∀ (γ : Γ), ((fun (x : T) ↦ γ • x) '' U ∩ U).Nonempty → γ • x = x
Tactic: obtain ⟨V, V_cpt, V_nhd⟩ := exists_compact_mem_nhds x
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (hypothesis)
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}
⊢ ∃ U ∈ 𝓝 x, ∀ (γ : Γ), ((fun (x : T) ↦ γ • x) '' U ∩ U).Nonempty → γ • x = x
have this : Finite.{u_4 + 1} (↑Γ₀ : Type u_4)
Tactic: have : Finite Γ₀ := (finite_disjoint_inter_image V_cpt V_cpt).subset fun _ ↦ And.left
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
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 ∈ 𝓝 x, ∀ (γ : Γ), ((fun (x : T) ↦ γ • x) '' U ∩ U).Nonempty → γ • x = x
have choose : ∀ (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 γ)),
  ∃ U ∈ 𝓝 x, ∀ (γ : Γ), ((fun (x : T) ↦ γ • x) '' U ∩ U).Nonempty → γ • x = x
Tactic: choose u v hu hv u_v_disjoint using fun γ : Γ₀ ↦ t2_separation_nhds γ.2.2
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
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 γ)
⊢ ∃ U ∈ 𝓝 x, ∀ (γ : Γ), ((fun (x : T) ↦ γ • x) '' U ∩ U).Nonempty → γ • x = x
have 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
Tactic: refine ⟨V ∩ ⋂ γ : Γ₀, (γ.1 • ·) ⁻¹' u γ ∩ v γ, inter_mem V_nhd (iInter_mem.mpr fun γ ↦
    inter_mem ((continuous_const_smul _).continuousAt <| hu γ) (hv γ)), fun γ hγ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
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
⊢ γ • x = x
have 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
Tactic: obtain ⟨_, ⟨z, hz, rfl⟩, hγz⟩ := hγ
Cleared hypotheses: hγ
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
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 γ
⊢ γ • x = x
have by_contra : ∀ (h : ¬γ • x = x), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (hypothesis)
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
⊢ False
have hz₁ : 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
Cleared hypotheses: hz, hγz, h
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (hypothesis)
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
⊢ False
have 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
Tactic: rw [mem_inter_iff, mem_iInter] at hz hγz
Cleared hypotheses: hz, hγz, h
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
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, ∀ (γ : Γ), γ • x ≠ x → Disjoint ((fun (x : T) ↦ γ • x) '' U) U
have 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
Tactic: convert! exists_nhds_image_smul_eq_self Γ x using 4
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
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 : Γ
⊢ 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
have 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
Tactic: rw [← not_imp_not]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
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[instTopologicalSpaceQuotient] (Quotient.mk' '' U)
have rw : IsOpen[inst_1] (⋃ (g : Γ), (fun (x : T) ↦ g • x) '' U)
Tactic: rw [isOpen_coinduced, MulAction.quotient_preimage_image_eq_union_mul U]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
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)
⊢ T2Space.{u_5} (Quotient (MulAction.orbitRel Γ T))
have rw : Pairwise fun (x y : Quotient (MulAction.orbitRel Γ T)) ↦ ∃ U ∈ 𝓝 x, ∃ V ∈ 𝓝 y, Disjoint U V
Tactic: rw [t2Space_iff_nhds]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (hypothesis)
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'
⊢ Pairwise fun (x y : Quotient (MulAction.orbitRel Γ T)) ↦ ∃ U ∈ 𝓝 x, ∃ V ∈ 𝓝 y, Disjoint U V
have f_op : IsOpenMap f
Tactic: have f_op : IsOpenMap f := isOpenMap_quotient_mk'_mul
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
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₀
⊢ ∃ (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
have mk : ∃ U ∈ 𝓝 (f x₀), ∃ V ∈ 𝓝 (f y₀), Disjoint U V
Tactic: change ∃ U ∈ 𝓝 (f x₀), ∃ V ∈ 𝓝 (f y₀), _
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (hypothesis)
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₀
⊢ ∃ U ∈ 𝓝 (f x₀), ∃ V ∈ 𝓝 (f y₀), Disjoint U V
have hγx₀y₀ : ∀ (γ : Γ), γ • x₀ ≠ y₀
Tactic: have hγx₀y₀ : ∀ γ : Γ, γ • x₀ ≠ y₀ := not_exists.mp (mt Quotient.sound hxy.symm :)
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
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₀
⊢ ∃ U ∈ 𝓝 (f x₀), ∃ V ∈ 𝓝 (f y₀), Disjoint U V
have mk : ∀ (K₀ : Set T) (hK₀ : IsCompact K₀) (K₀_in : K₀ ∈ 𝓝 x₀), ∃ U ∈ 𝓝 (f x₀), ∃ V ∈ 𝓝 (f y₀), Disjoint U V
Tactic: obtain ⟨K₀, hK₀, K₀_in⟩ := exists_compact_mem_nhds x₀
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
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₀
⊢ ∃ U ∈ 𝓝 (f x₀), ∃ V ∈ 𝓝 (f y₀), Disjoint U V
have mk : ∀ (L₀ : Set T) (hL₀ : IsCompact L₀) (L₀_in : L₀ ∈ 𝓝 y₀), ∃ U ∈ 𝓝 (f x₀), ∃ V ∈ 𝓝 (f y₀), Disjoint U V
Tactic: obtain ⟨L₀, hL₀, L₀_in⟩ := exists_compact_mem_nhds y₀
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (hypothesis)
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}
⊢ ∃ U ∈ 𝓝 (f x₀), ∃ V ∈ 𝓝 (f y₀), Disjoint U V
have bad_Γ_finite : bad_Γ_set.Finite
Tactic: have bad_Γ_finite : bad_Γ_set.Finite := finite_disjoint_inter_image (Γ := Γ) hK₀ hL₀
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
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 ∈ 𝓝 (f x₀), ∃ V ∈ 𝓝 (f y₀), Disjoint U V
have 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
Tactic: choose u v hu hv u_v_disjoint using fun γ => t2_separation_nhds (hγx₀y₀ γ)
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
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₀)
have refine : ∀ γ ∈ bad_Γ_set, (fun (x : T) ↦ γ • x) ⁻¹' u γ ∈ 𝓝 x₀
Tactic: refine f_op.image_mem_nhds (inter_mem ((biInter_mem bad_Γ_finite).mpr fun γ _ => ?_) K₀_in)
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (hypothesis)
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 ∈ 𝓝 (f x₀), ∃ V ∈ 𝓝 (f y₀), Disjoint U V
have U_nhds : 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 γ)
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (hypothesis)
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₀)
⊢ ∃ U ∈ 𝓝 (f x₀), ∃ V ∈ 𝓝 (f y₀), Disjoint U V
have V_nhds : 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)
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
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
have mk : ∀ x ∈ U₀, ∀ (g : Γ), g • x ∉ V₀
Tactic: refine ⟨f '' U₀, U_nhds, f '' V₀, V_nhds, MulAction.disjoint_image_image_iff.2 ?_⟩