-- Mathlib/Topology/Algebra/ProperAction/Basic.lean
theorem properSMul_of_isClosedEmbedding {H : Type*} [Group H] [MulAction H X] [TopologicalSpace H]
    [ProperSMul G X] (f : H →* G) (f_clemb : IsClosedEmbedding f)
    (f_compat : ∀ (h : H) (x : X), f h • x = h • x) : ProperSMul H X where
  isProperMap_smul_pair

Proof state:
G : Type u_1
X : Type u_2
inst✝⁷ : Group G
inst✝⁶ : MulAction G X
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace X
H : Type u_3
inst✝³ : Group H
inst✝² : MulAction H X
inst✝¹ : TopologicalSpace H
inst✝ : ProperSMul G X
f : H →* G
f_clemb : IsClosedEmbedding ⇑f
f_compat : ∀ (h : H) (x : X), f h • x = h • x
h : IsProperMap (Prod.map ⇑f fun x => x)
this : (fun hx => (hx.1 • hx.2, hx.2)) = fun hx => (f hx.1 • hx.2, hx.2)
⊢ IsProperMap fun hx => (f hx.1 • hx.2, hx.2)

Tactic:
exact h.comp <| ProperSMul.isProperMap_smul_pair

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
H : Type u_3
inst✝³ : Group H
inst✝² : MulAction H X
inst✝¹ : TopologicalSpace H
inst✝ : ProperSMul G X
f : H →* G
f_clemb : IsClosedEmbedding ⇑f
f_compat : ∀ (h : H) (x : X), f h • x = h • x
h : IsProperMap (Prod.map ⇑f fun x => x)
⊢ IsProperMap fun gx => (gx.1 • gx.2, gx.2)

Tactic:
have : (fun hx : H × X ↦ (hx.1 • hx.2, hx.2)) = (fun hx ↦ (f hx.1 • hx.2, hx.2)) := by
  simp [f_compat]

Result:
G : Type u_1
X : Type u_2
inst✝⁷ : Group G
inst✝⁶ : MulAction G X
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace X
H : Type u_3
inst✝³ : Group H
inst✝² : MulAction H X
inst✝¹ : TopologicalSpace H
inst✝ : ProperSMul G X
f : H →* G
f_clemb : IsClosedEmbedding ⇑f
f_compat : ∀ (h : H) (x : X), f h • x = h • x
h : IsProperMap (Prod.map ⇑f fun x => x)
this : (fun hx => (hx.1 • hx.2, hx.2)) = fun hx => (f hx.1 • hx.2, hx.2)
⊢ IsProperMap fun gx => (gx.1 • gx.2, gx.2)

Proof state:
G : Type u_1
X : Type u_2
inst✝⁷ : Group G
inst✝⁶ : MulAction G X
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace X
H : Type u_3
inst✝³ : Group H
inst✝² : MulAction H X
inst✝¹ : TopologicalSpace H
inst✝ : ProperSMul G X
f : H →* G
f_clemb : IsClosedEmbedding ⇑f
f_compat : ∀ (h : H) (x : X), f h • x = h • x
⊢ IsProperMap fun gx => (gx.1 • gx.2, gx.2)

Tactic:
have h : IsProperMap (Prod.map f (fun x : X ↦ x)) := f_clemb.isProperMap.prodMap isProperMap_id

Result:
G : Type u_1
X : Type u_2
inst✝⁷ : Group G
inst✝⁶ : MulAction G X
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace X
H : Type u_3
inst✝³ : Group H
inst✝² : MulAction H X
inst✝¹ : TopologicalSpace H
inst✝ : ProperSMul G X
f : H →* G
f_clemb : IsClosedEmbedding ⇑f
f_compat : ∀ (h : H) (x : X), f h • x = h • x
h : IsProperMap (Prod.map ⇑f fun x => x)
⊢ IsProperMap fun gx => (gx.1 • gx.2, gx.2)

Proof state:
G : Type u_1
X : Type u_2
inst✝⁷ : Group G
inst✝⁶ : MulAction G X
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace X
H : Type u_3
inst✝³ : Group H
inst✝² : MulAction H X
inst✝¹ : TopologicalSpace H
inst✝ : ProperSMul G X
f : H →* G
f_clemb : IsClosedEmbedding ⇑f
f_compat : ∀ (h : H) (x : X), f h • x = h • x
h : IsProperMap (Prod.map ⇑f fun x => x)
this : (fun hx => (hx.1 • hx.2, hx.2)) = fun hx => (f hx.1 • hx.2, hx.2)
⊢ IsProperMap fun gx => (gx.1 • gx.2, gx.2)

Tactic:
rw [this]

Result:
G : Type u_1
X : Type u_2
inst✝⁷ : Group G
inst✝⁶ : MulAction G X
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace X
H : Type u_3
inst✝³ : Group H
inst✝² : MulAction H X
inst✝¹ : TopologicalSpace H
inst✝ : ProperSMul G X
f : H →* G
f_clemb : IsClosedEmbedding ⇑f
f_compat : ∀ (h : H) (x : X), f h • x = h • x
h : IsProperMap (Prod.map ⇑f fun x => x)
this : (fun hx => (hx.1 • hx.2, hx.2)) = fun hx => (f hx.1 • hx.2, hx.2)
⊢ IsProperMap fun hx => (f hx.1 • hx.2, hx.2)

Proof state:
G : Type u_1
X : Type u_2
inst✝⁷ : Group G
inst✝⁶ : MulAction G X
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace X
H : Type u_3
inst✝³ : Group H
inst✝² : MulAction H X
inst✝¹ : TopologicalSpace H
inst✝ : ProperSMul G X
f : H →* G
f_clemb : IsClosedEmbedding ⇑f
f_compat : ∀ (h : H) (x : X), f h • x = h • x
h : IsProperMap (Prod.map ⇑f fun x => x)
⊢ (fun hx => (hx.1 • hx.2, hx.2)) = fun hx => (f hx.1 • hx.2, hx.2)

Tactic:
simp [f_compat]

Result:
no goals