-- Mathlib/Topology/Algebra/ProperAction/Basic.lean
theorem properSMul_iff_continuousSMul_ultrafilter_tendsto_t2 [T2Space X] :
    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, Tendsto (Prod.fst : G × X → G) 𝒰 (𝓝 g))

Proof state:
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
hc : 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)) ↔
    ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
      Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, Tendsto fst (↑𝒰) (𝓝 g)

Tactic:
congrm ∀ 𝒰 x₁ x₂ hxx, ∃ g, ?_

Result:
case a
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
hc : ContinuousSMul G X
𝒰 : Ultrafilter (G × X)
x₁ x₂ : X
hxx : Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂))
g : G
⊢ g • x₂ = x₁ ∧ Tendsto fst (↑𝒰) (𝓝 g) ↔ 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
inst✝ : T2Space 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)) ↔
    ContinuousSMul G X ∧
      ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
        Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, Tendsto fst (↑𝒰) (𝓝 g)

Tactic:
refine and_congr_right fun hc ↦ ?_

Result:
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
hc : 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)) ↔
    ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
      Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, Tendsto fst (↑𝒰) (𝓝 g)

Proof state:
case a
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
hc : ContinuousSMul G X
𝒰 : Ultrafilter (G × X)
x₁ x₂ : X
hxx : Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂))
g : G
⊢ g • x₂ = x₁ ∧ Tendsto fst (↑𝒰) (𝓝 g) ↔ Tendsto fst (↑𝒰) (𝓝 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)

Result:
no goals

Proof state:
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : T2Space 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, Tendsto fst (↑𝒰) (𝓝 g)

Tactic:
rw [properSMul_iff_continuousSMul_ultrafilter_tendsto]

Result:
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : T2Space 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)) ↔
    ContinuousSMul G X ∧
      ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
        Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, Tendsto fst (↑𝒰) (𝓝 g)