-- Mathlib/Topology/Algebra/ProperAction/Basic.lean
theorem properSMul_iff_continuousSMul_ultrafilter_tendsto :
    ProperSMul G X ↔ ContinuousSMul G X ∧
      (∀ 𝒰 : Ultrafilter (G × X), ∀ x₁ x₂ : X,
        Tendsto (fun gx : G × X ↦ (gx.1 • gx.2, gx.2)) 𝒰 (𝓝 (x₁, x₂)) →
      ∃ g : G, g • x₂ = x₁ ∧ Tendsto (Prod.fst : G × X → G) 𝒰 (𝓝 g))

Proof state:
case refine_1.intro.intro
G : Type u_1
X : Type u_2
inst✝³ : Group G
inst✝² : MulAction G X
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalSpace X
h :
  (Continuous fun gx => (gx.1 • gx.2, gx.2)) ∧
    ∀ ⦃𝒰 : Ultrafilter (G × X)⦄ ⦃y : X × X⦄,
      Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 y) → ∃ x, (x.1 • x.2, x.2) = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter (G × X)
x₁ x₂ : X
h' : Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂))
gx : G × X
hgx1 : (gx.1 • gx.2, gx.2) = (x₁, x₂)
hgx2 : ↑𝒰 ≤ 𝓝 gx
⊢ gx.1 • x₂ = x₁

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

Result:
case refine_1.intro.intro
G : Type u_1
X : Type u_2
inst✝³ : Group G
inst✝² : MulAction G X
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalSpace X
h :
  (Continuous fun gx => (gx.1 • gx.2, gx.2)) ∧
    ∀ ⦃𝒰 : Ultrafilter (G × X)⦄ ⦃y : X × X⦄,
      Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 y) → ∃ x, (x.1 • x.2, x.2) = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter (G × X)
x₁ x₂ : X
h' : Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂))
gx : G × X
hgx2 : ↑𝒰 ≤ 𝓝 gx
hgx1 : gx.1 • gx.2 = x₁ ∧ gx.2 = x₂
⊢ gx.1 • x₂ = x₁

Proof state:
case refine_1
G : Type u_1
X : Type u_2
inst✝³ : Group G
inst✝² : MulAction G X
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalSpace X
h : ProperSMul G X
𝒰 : Ultrafilter (G × X)
x₁ x₂ : X
h' : Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂))
⊢ ∃ g, g • x₂ = x₁ ∧ Tendsto fst (↑𝒰) (𝓝 g)

Tactic:
rw [properSMul_iff, isProperMap_iff_ultrafilter] at h

Result:
case refine_1
G : Type u_1
X : Type u_2
inst✝³ : Group G
inst✝² : MulAction G X
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalSpace X
h :
  (Continuous fun gx => (gx.1 • gx.2, gx.2)) ∧
    ∀ ⦃𝒰 : Ultrafilter (G × X)⦄ ⦃y : X × X⦄,
      Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 y) → ∃ x, (x.1 • x.2, x.2) = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter (G × X)
x₁ x₂ : X
h' : Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂))
⊢ ∃ g, g • x₂ = x₁ ∧ Tendsto fst (↑𝒰) (𝓝 g)

Proof state:
G : Type u_1
X : Type u_2
inst✝³ : Group G
inst✝² : MulAction G X
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalSpace X
x✝¹ :
  ContinuousSMul G X ∧
    ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
      Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, g • x₂ = x₁ ∧ Tendsto fst (↑𝒰) (𝓝 g)
cont : ContinuousSMul G X
h :
  ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
    Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, g • x₂ = x₁ ∧ Tendsto fst (↑𝒰) (𝓝 g)
𝒰 : Ultrafilter (G × X)
x✝ : X × X
x₁ x₂ : X
hxx : Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂))
g : G
hg1 : g • x₂ = x₁
hg2 : Tendsto fst (↑𝒰) (𝓝 g)
⊢ ((g, x₂).1 • (g, x₂).2, (g, x₂).2) = (x₁, x₂)

Tactic:
simp_rw [hg1]

Result:
no goals

Proof state:
case refine_2
G : Type u_1
X : Type u_2
inst✝³ : Group G
inst✝² : MulAction G X
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalSpace X
x✝ :
  ContinuousSMul G X ∧
    ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
      Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, g • x₂ = x₁ ∧ Tendsto fst (↑𝒰) (𝓝 g)
cont : ContinuousSMul G X
h :
  ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
    Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, g • x₂ = x₁ ∧ Tendsto fst (↑𝒰) (𝓝 g)
⊢ (Continuous fun gx => (gx.1 • gx.2, gx.2)) ∧
    ∀ ⦃𝒰 : Ultrafilter (G × X)⦄ ⦃y : X × X⦄,
      Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 y) → ∃ x, (x.1 • x.2, x.2) = y ∧ ↑𝒰 ≤ 𝓝 x

Tactic:
refine ⟨by fun_prop, fun 𝒰 (x₁, x₂) hxx ↦ ?_⟩

Result:
case refine_2
G : Type u_1
X : Type u_2
inst✝³ : Group G
inst✝² : MulAction G X
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalSpace X
x✝¹ :
  ContinuousSMul G X ∧
    ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
      Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, g • x₂ = x₁ ∧ Tendsto fst (↑𝒰) (𝓝 g)
cont : ContinuousSMul G X
h :
  ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
    Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, g • x₂ = x₁ ∧ Tendsto fst (↑𝒰) (𝓝 g)
𝒰 : Ultrafilter (G × X)
x✝ : X × X
x₁ x₂ : X
hxx : Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂))
⊢ ∃ x, (x.1 • x.2, x.2) = (x₁, x₂) ∧ ↑𝒰 ≤ 𝓝 x

Proof state:
case refine_2
G : Type u_1
X : Type u_2
inst✝³ : Group G
inst✝² : MulAction G X
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalSpace X
x✝ :
  ContinuousSMul G X ∧
    ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
      Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, g • x₂ = x₁ ∧ Tendsto fst (↑𝒰) (𝓝 g)
cont : ContinuousSMul G X
h :
  ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
    Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, g • x₂ = x₁ ∧ Tendsto fst (↑𝒰) (𝓝 g)
⊢ ProperSMul G X

Tactic:
rw [properSMul_iff, isProperMap_iff_ultrafilter]

Result:
case refine_2
G : Type u_1
X : Type u_2
inst✝³ : Group G
inst✝² : MulAction G X
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalSpace X
x✝ :
  ContinuousSMul G X ∧
    ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
      Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, g • x₂ = x₁ ∧ Tendsto fst (↑𝒰) (𝓝 g)
cont : ContinuousSMul G X
h :
  ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
    Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, g • x₂ = x₁ ∧ Tendsto fst (↑𝒰) (𝓝 g)
⊢ (Continuous fun gx => (gx.1 • gx.2, gx.2)) ∧
    ∀ ⦃𝒰 : Ultrafilter (G × X)⦄ ⦃y : X × X⦄,
      Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 y) → ∃ x, (x.1 • x.2, x.2) = y ∧ ↑𝒰 ≤ 𝓝 x

Proof state:
G : Type u_1
X : Type u_2
inst✝³ : Group G
inst✝² : MulAction G X
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalSpace X
⊢ ProperSMul G X ↔
    ContinuousSMul G X ∧
      ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
        Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, g • x₂ = x₁ ∧ Tendsto fst (↑𝒰) (𝓝 g)

Tactic:
refine ⟨fun h ↦ ⟨inferInstance, fun 𝒰 x₁ x₂ h' ↦ ?_⟩, fun ⟨cont, h⟩ ↦ ?_⟩

Result:
case refine_1
G : Type u_1
X : Type u_2
inst✝³ : Group G
inst✝² : MulAction G X
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalSpace X
h : ProperSMul G X
𝒰 : Ultrafilter (G × X)
x₁ x₂ : X
h' : Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂))
⊢ ∃ g, g • x₂ = x₁ ∧ Tendsto fst (↑𝒰) (𝓝 g)

case refine_2
G : Type u_1
X : Type u_2
inst✝³ : Group G
inst✝² : MulAction G X
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalSpace X
x✝ :
  ContinuousSMul G X ∧
    ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
      Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, g • x₂ = x₁ ∧ Tendsto fst (↑𝒰) (𝓝 g)
cont : ContinuousSMul G X
h :
  ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
    Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, g • x₂ = x₁ ∧ Tendsto fst (↑𝒰) (𝓝 g)
⊢ ProperSMul G X