awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
h :
  (Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ∧
    ∀ ⦃𝒰 : Ultrafilter (G × X)⦄ ⦃y : X × X⦄,
      Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 y) →
        ∃ (x : G × X), (x.1 • x.2, x.2) = y ∧ (↑𝒰 : Filter (G × X)) ≤ 𝓝 x
𝒰 : Ultrafilter (G × X)
x₁ x₂ : X
h' : Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂))
gx : G × X
hgx1 : (gx.1 • gx.2, gx.2) = (x₁, x₂)
hgx2 : (↑𝒰 : Filter (G × X)) ≤ 𝓝 gx
⊢ ∃ (g : G), g • x₂ = x₁ ∧ Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)

Tactic:
⟨gx.1, ?_, (continuous_fst.tendsto gx).mono_left hgx2⟩

Premises used: continuous_fst, Prod.fst, Continuous.tendsto, And.intro, Exists.intro, Filter.Tendsto.mono_left
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
h :
  (Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ∧
    ∀ ⦃𝒰 : Ultrafilter (G × X)⦄ ⦃y : X × X⦄,
      Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 y) →
        ∃ (x : G × X), (x.1 • x.2, x.2) = y ∧ (↑𝒰 : Filter (G × X)) ≤ 𝓝 x
𝒰 : Ultrafilter (G × X)
x₁ x₂ : X
h' : Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂))
gx : G × X
hgx1 : (gx.1 • gx.2, gx.2) = (x₁, x₂)
hgx2 : (↑𝒰 : Filter (G × X)) ≤ 𝓝 gx
refine_1 : gx.1 • x₂ = x₁
⊢ ∃ (g : G), g • x₂ = x₁ ∧ Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)

Tactic:
refine ⟨gx.1, ?_, (continuous_fst.tendsto gx).mono_left hgx2⟩
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
h :
  (Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ∧
    ∀ ⦃𝒰 : Ultrafilter (G × X)⦄ ⦃y : X × X⦄,
      Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 y) →
        ∃ (x : G × X), (x.1 • x.2, x.2) = y ∧ (↑𝒰 : Filter (G × X)) ≤ 𝓝 x
𝒰 : Ultrafilter (G × X)
x₁ x₂ : X
h' : Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂))
gx : G × X
hgx1 : (gx.1 • gx.2, gx.2) = (x₁, x₂)
hgx2 : (↑𝒰 : Filter (G × X)) ≤ 𝓝 gx
⊢ gx.1 • gx.2 = x₁ ∧ gx.2 = x₂

Tactic:
simp only [Prod.mk.injEq] at hgx1

Premises used: Prod.mk.injEq
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
h :
  (Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ∧
    ∀ ⦃𝒰 : Ultrafilter (G × X)⦄ ⦃y : X × X⦄,
      Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 y) →
        ∃ (x : G × X), (x.1 • x.2, x.2) = y ∧ (↑𝒰 : Filter (G × X)) ≤ 𝓝 x
𝒰 : Ultrafilter (G × X)
x₁ x₂ : X
h' : Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂))
gx : G × X
hgx2 : (↑𝒰 : Filter (G × X)) ≤ 𝓝 gx
hgx1 : gx.1 • gx.2 = x₁ ∧ gx.2 = x₂
refine_1 : gx.1 • gx.2 = x₁
refine_1₁ refine_1₂ : x₁ = x₁
⊢ gx.1 • x₂ = x₁

Tactic:
rw [← hgx1.2, hgx1.1]

Premises used: And.right, And.left
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
h_1 :
  ContinuousSMul G X ∧
    ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
      Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂)) →
        ∃ (g : G), g • x₂ = x₁ ∧ Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)
cont : ContinuousSMul G X
h :
  ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
    Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂)) →
      ∃ (g : G), g • x₂ = x₁ ∧ Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)
refine_2 :
  (Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ∧
    ∀ ⦃𝒰 : Ultrafilter (G × X)⦄ ⦃y : X × X⦄,
      Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 y) →
        ∃ (x : G × X), (x.1 • x.2, x.2) = y ∧ (↑𝒰 : Filter (G × X)) ≤ 𝓝 x
⊢ ProperSMul G X

Tactic:
rw [properSMul_iff, isProperMap_iff_ultrafilter]

Premises used: properSMul_iff, isProperMap_iff_ultrafilter
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
h_1 :
  ContinuousSMul G X ∧
    ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
      Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂)) →
        ∃ (g : G), g • x₂ = x₁ ∧ Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)
cont : ContinuousSMul G X
h :
  ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
    Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂)) →
      ∃ (g : G), g • x₂ = x₁ ∧ Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
h_1 :
  ContinuousSMul G X ∧
    ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
      Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂)) →
        ∃ (g : G), g • x₂ = x₁ ∧ Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)
cont : ContinuousSMul G X
h :
  ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
    Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂)) →
      ∃ (g : G), g • x₂ = x₁ ∧ Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)
refine_2 :
  ∀ (𝒰 : Ultrafilter (G × X)) (x : X × X) (x₁ x₂ : X)
    (hxx : Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂))),
    ∃ (x : G × X), (x.1 • x.2, x.2) = (x₁, x₂) ∧ (↑𝒰 : Filter (G × X)) ≤ 𝓝 x
⊢ (Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ∧
    ∀ ⦃𝒰 : Ultrafilter (G × X)⦄ ⦃y : X × X⦄,
      Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 y) →
        ∃ (x : G × X), (x.1 • x.2, x.2) = y ∧ (↑𝒰 : Filter (G × X)) ≤ 𝓝 x

Tactic:
refine ⟨by fun_prop, fun 𝒰 (x₁, x₂) hxx ↦ ?_⟩
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
h_1 :
  ContinuousSMul G X ∧
    ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
      Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂)) →
        ∃ (g : G), g • x₂ = x₁ ∧ Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)
cont : ContinuousSMul G X
h :
  ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
    Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂)) →
      ∃ (g : G), g • x₂ = x₁ ∧ Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)
𝒰 : Ultrafilter (G × X)
x : X × X
x₁ x₂ : X
hxx : Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂))
refine_2 :
  ∀ (g : G) (hg1 : g • x₂ = x₁) (hg2 : Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)),
    ∃ (x : G × X), (x.1 • x.2, x.2) = (x₁, x₂) ∧ (↑𝒰 : Filter (G × X)) ≤ 𝓝 x
⊢ ∃ (x : G × X), (x.1 • x.2, x.2) = (x₁, x₂) ∧ (↑𝒰 : Filter (G × X)) ≤ 𝓝 x

Tactic:
rcases h 𝒰 x₁ x₂ hxx with ⟨g, hg1, hg2⟩
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
h_1 :
  ContinuousSMul G X ∧
    ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
      Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂)) →
        ∃ (g : G), g • x₂ = x₁ ∧ Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)
cont : ContinuousSMul G X
h :
  ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
    Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂)) →
      ∃ (g : G), g • x₂ = x₁ ∧ Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)
𝒰 : Ultrafilter (G × X)
x : X × X
x₁ x₂ : X
hxx : Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂))
g : G
hg1 : g • x₂ = x₁
hg2 : Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)
simp_rw simp_rw₁ : (g • x₂, x₂) = (x₁, x₂)
⊢ ((g, x₂).1 • (g, x₂).2, (g, x₂).2) = (x₁, x₂)

Tactic:
simp_rw [hg1]
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
h_1 :
  ContinuousSMul G X ∧
    ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
      Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂)) →
        ∃ (g : G), g • x₂ = x₁ ∧ Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)
cont : ContinuousSMul G X
h :
  ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
    Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂)) →
      ∃ (g : G), g • x₂ = x₁ ∧ Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)
𝒰 : Ultrafilter (G × X)
x : X × X
x₁ x₂ : X
hxx : Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂))
g : G
hg1 : g • x₂ = x₁
hg2 : Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)
refine_2 : (↑𝒰 : Filter (G × X)) ≤ 𝓝 (g, x₂)
⊢ ∃ (x : G × X), (x.1 • x.2, x.2) = (x₁, x₂) ∧ (↑𝒰 : Filter (G × X)) ≤ 𝓝 x

Tactic:
refine ⟨(g, x₂), by simp_rw [hg1], ?_⟩
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
h_1 :
  ContinuousSMul G X ∧
    ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
      Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂)) →
        ∃ (g : G), g • x₂ = x₁ ∧ Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)
cont : ContinuousSMul G X
h :
  ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
    Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂)) →
      ∃ (g : G), g • x₂ = x₁ ∧ Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)
𝒰 : Ultrafilter (G × X)
x : X × X
x₁ x₂ : X
hxx : Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂))
g : G
hg1 : g • x₂ = x₁
hg2 : Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)
refine_2 : Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g) ∧ Tendsto snd (↑𝒰 : Filter (G × X)) (𝓝 x₂)
⊢ (↑𝒰 : Filter (G × X)) ≤ 𝓝 (g, x₂)

Tactic:
rw [nhds_prod_eq, 𝒰.le_prod]

Premises used: Filter.le_prod, nhds_prod_eq
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
h_1 :
  ContinuousSMul G X ∧
    ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
      Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂)) →
        ∃ (g : G), g • x₂ = x₁ ∧ Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)
cont : ContinuousSMul G X
h :
  ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
    Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂)) →
      ∃ (g : G), g • x₂ = x₁ ∧ Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)
𝒰 : Ultrafilter (G × X)
x : X × X
x₁ x₂ : X
hxx : Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂))
g : G
hg1 : g • x₂ = x₁
hg2 : Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)
⊢ Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g) ∧ Tendsto snd (↑𝒰 : Filter (G × X)) (𝓝 x₂)

Tactic:
⟨hg2, (continuous_snd.tendsto _).comp hxx⟩

Premises used: continuous_snd, Continuous.tendsto, And.intro, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
h_1 :
  ContinuousSMul G X ∧
    ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
      Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂)) →
        ∃ (g : G), g • x₂ = x₁ ∧ Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)
cont : ContinuousSMul G X
h :
  ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
    Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂)) →
      ∃ (g : G), g • x₂ = x₁ ∧ Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)
𝒰 : Ultrafilter (G × X)
x : X × X
x₁ x₂ : X
hxx : Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂))
g : G
hg1 : g • x₂ = x₁
hg2 : Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)
⊢ Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g) ∧ Tendsto snd (↑𝒰 : Filter (G × X)) (𝓝 x₂)

Tactic:
exact ⟨hg2, (continuous_snd.tendsto _).comp hxx⟩
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
inst_4 : T2Space X
rw :
  (ContinuousSMul G X ∧
      ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
        Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂)) →
          ∃ (g : G), g • x₂ = x₁ ∧ Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)) ↔
    ContinuousSMul G X ∧
      ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
        Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂)) →
          ∃ (g : G), Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)
⊢ ProperSMul G X ↔
    ContinuousSMul G X ∧
      ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
        Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂)) →
          ∃ (g : G), Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)

Tactic:
rw [properSMul_iff_continuousSMul_ultrafilter_tendsto]

Premises used: properSMul_iff_continuousSMul_ultrafilter_tendsto
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
inst_4 : T2Space X
⊢ (ContinuousSMul G X ∧
      ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
        Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂)) →
          ∃ (g : G), g • x₂ = x₁ ∧ Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)) ↔
    ContinuousSMul G X ∧
      ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
        Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂)) →
          ∃ (g : G), Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)

Tactic:
and_congr_right fun hc ↦ ?_

Premises used: and_congr_right
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
inst_4 : T2Space X
refine :
  ∀ (hc : ContinuousSMul G X),
    (∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
        Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂)) →
          ∃ (g : G), g • x₂ = x₁ ∧ Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)) ↔
      ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
        Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂)) →
          ∃ (g : G), Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)
⊢ (ContinuousSMul G X ∧
      ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
        Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂)) →
          ∃ (g : G), g • x₂ = x₁ ∧ Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)) ↔
    ContinuousSMul G X ∧
      ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
        Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂)) →
          ∃ (g : G), Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)

Tactic:
refine and_congr_right fun hc ↦ ?_

Premises used: and_congr_right
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
inst_4 : T2Space X
hc : ContinuousSMul G X
a :
  ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X)
    (hxx : Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂))) (g : G),
    g • x₂ = x₁ ∧ Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g) ↔ Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)
⊢ (∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
      Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂)) →
        ∃ (g : G), g • x₂ = x₁ ∧ Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)) ↔
    ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
      Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂)) →
        ∃ (g : G), Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)

Tactic:
congrm ∀ 𝒰 x₁ x₂ hxx, ∃ g, ?_
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
inst_4 : T2Space X
hc : ContinuousSMul G X
𝒰 : Ultrafilter (G × X)
x₁ x₂ : X
hxx : Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂))
g : G
⊢ g • x₂ = x₁ ∧ Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g) ↔ Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)

Tactic:
and_iff_right_of_imp fun hg ↦ tendsto_nhds_unique
    (hg.smul ((continuous_snd.tendsto _).comp hxx)) ((continuous_fst.tendsto _).comp hxx)

Premises used: continuous_snd, continuous_fst, Prod.mk, Continuous.tendsto, Filter.Tendsto.smul, Filter.Tendsto.comp, and_iff_right_of_imp, tendsto_nhds_unique
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
inst_4 : T2Space X
hc : ContinuousSMul G X
𝒰 : Ultrafilter (G × X)
x₁ x₂ : X
hxx : Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂))
g : G
⊢ g • x₂ = x₁ ∧ Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g) ↔ Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)

Tactic:
exact and_iff_right_of_imp fun hg ↦ tendsto_nhds_unique
    (hg.smul ((continuous_snd.tendsto _).comp hxx)) ((continuous_fst.tendsto _).comp hxx)

Premises used: continuous_fst, Prod.mk, Continuous.tendsto, Filter.Tendsto.comp, and_iff_right_of_imp, tendsto_nhds_unique
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
inst_4 : ProperSMul G X
rw : IsClosed[instTopologicalSpaceProd] (diagonal (Quotient (MulAction.orbitRel G X)))
⊢ T2Space.{u_2} (Quotient (MulAction.orbitRel G X))

Tactic:
rw [t2_iff_isClosed_diagonal]

Premises used: t2_iff_isClosed_diagonal
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
inst_4 : ProperSMul G X
set :
  let R := MulAction.orbitRel G X;
  IsClosed[instTopologicalSpaceProd] (diagonal (Quotient R))
⊢ IsClosed[instTopologicalSpaceProd] (diagonal (Quotient (MulAction.orbitRel G X)))

Tactic:
set R := MulAction.orbitRel G X

Premises used: MulAction.orbitRel
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
inst_4 : ProperSMul G X
R : Setoid X := MulAction.orbitRel G X
π : X → Quotient R := Quotient.mk'
⊢ IsOpenQuotientMap (Prod.map π π)

Tactic:
have : IsOpenQuotientMap (Prod.map π π) :=
    MulAction.isOpenQuotientMap_quotientMk.prodMap MulAction.isOpenQuotientMap_quotientMk
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
inst_4 : ProperSMul G X
R : Setoid X := MulAction.orbitRel G X
π : X → Quotient R := Quotient.mk'
this : IsOpenQuotientMap (Prod.map π π)
rw : IsClosed[instTopologicalSpaceProd] (Prod.map π π ⁻¹' diagonal (Quotient R))
⊢ IsClosed[instTopologicalSpaceProd] (diagonal (Quotient R))

Tactic:
rw [← this.isQuotientMap.isClosed_preimage]

Premises used: Topology.IsCoinducing.isClosed_preimage, Topology.IsQuotientMap.isCoinducing, IsOpenQuotientMap.isQuotientMap
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
inst_4 : ProperSMul G X
R : Setoid X := MulAction.orbitRel G X
π : X → Quotient R := Quotient.mk'
this : IsOpenQuotientMap (Prod.map π π)
⊢ IsClosed[instTopologicalSpaceProd] (range fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2))

Tactic:
ProperSMul.isProperMap_smul_pair.isClosedMap.isClosed_range

Premises used: IsProperMap.isClosedMap, ProperSMul.isProperMap_smul_pair, IsClosedMap.isClosed_range
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
inst_4 : ProperSMul G X
R : Setoid X := MulAction.orbitRel G X
π : X → Quotient R := Quotient.mk'
this : IsOpenQuotientMap (Prod.map π π)
h : Prod.map π π ⁻¹' diagonal (Quotient R) = range fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)
convert_1 : Type u_1
convert_3 : TopologicalSpace G
convert_5 : Group G
convert_6 : MulAction G X
convert_7 : ProperSMul G X
⊢ IsClosed[instTopologicalSpaceProd] (Prod.map π π ⁻¹' diagonal (Quotient R))

Tactic:
convert! ProperSMul.isProperMap_smul_pair.isClosedMap.isClosed_range

Premises used: IsProperMap.isClosedMap, ProperSMul.isProperMap_smul_pair, IsClosedMap.isClosed_range
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
inst_4 : ProperSMul G X
R : Setoid X := MulAction.orbitRel G X
π : X → Quotient R := Quotient.mk'
this : IsOpenQuotientMap (Prod.map π π)
h :
  ∀ (x₁ x₂ : X),
    (x₁, x₂) ∈ Prod.map π π ⁻¹' diagonal (Quotient R) ↔
      Membership.mem (γ := Set (X × X)) (range fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (x₁, x₂)
⊢ Prod.map π π ⁻¹' diagonal (Quotient R) = range fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)

Tactic:
ext ⟨x₁, x₂⟩
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
inst_4 : ProperSMul G X
R : Setoid X := MulAction.orbitRel G X
π : X → Quotient R := Quotient.mk'
this : IsOpenQuotientMap (Prod.map π π)
x₁ x₂ : X
h : π x₁ = π x₂ ↔ ∃ (a : G), a • x₂ = x₁
⊢ (x₁, x₂) ∈ Prod.map π π ⁻¹' diagonal (Quotient R) ↔
    Membership.mem (γ := Set (X × X)) (range fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (x₁, x₂)

Tactic:
simp only [mem_preimage, map_apply, mem_diagonal_iff, mem_range, Prod.mk.injEq, Prod.exists,
      exists_eq_right]

Premises used: Set.mem_range, exists_eq_right, Set.mem_diagonal_iff, Prod.mk.injEq, Prod.map_apply, Prod.exists, Set.mem_preimage
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
inst_4 : ProperSMul G X
R : Setoid X := MulAction.orbitRel G X
π : X → Quotient R := Quotient.mk'
this : IsOpenQuotientMap (Prod.map π π)
x₁ x₂ : X
h : (R : X → X → Prop) x₁ x₂ ↔ ∃ (a : G), a • x₂ = x₁
h₁ : x₁ ∈ MulAction.orbit G x₂ ↔ ∃ (a : G), a • x₂ = x₁
h₂ h₃ : (∃ (x : G), x • x₂ = x₁) ↔ ∃ (a : G), a • x₂ = x₁
⊢ π x₁ = π x₂ ↔ ∃ (a : G), a • x₂ = x₁

Tactic:
rw [Quotient.eq', MulAction.orbitRel_apply, MulAction.mem_orbit_iff]

Premises used: MulAction.mem_orbit_iff, Quotient.eq', MulAction.orbitRel_apply
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
inst_4 : ProperSMul G X
R : Setoid X := MulAction.orbitRel G X
π : X → Quotient R := Quotient.mk'
this : IsOpenQuotientMap (Prod.map π π)
⊢ TopologicalSpace G

Tactic:
infer_instance
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
inst_4 : ProperSMul G X
R : Setoid X := MulAction.orbitRel G X
π : X → Quotient R := Quotient.mk'
this : IsOpenQuotientMap (Prod.map π π)
⊢ ProperSMul G X

Tactic:
infer_instance