awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (goal)
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₂))
⊢ ∃ (x : G × X), (x.1 • x.2, x.2) = (x₁, x₂) ∧ (↑𝒰 : Filter (G × X)) ≤ 𝓝 x
have 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
Tactic: rcases h 𝒰 x₁ x₂ hxx with ⟨g, hg1, hg2⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (goal)
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)
⊢ ((g, x₂).1 • (g, x₂).2, (g, x₂).2) = (x₁, x₂)
have simp_rw : (g • x₂, x₂) = (x₁, x₂)
Tactic: simp_rw [hg1]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (goal)
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)
⊢ ∃ (x : G × X), (x.1 • x.2, x.2) = (x₁, x₂) ∧ (↑𝒰 : Filter (G × X)) ≤ 𝓝 x
have refine_2 : (↑𝒰 : Filter (G × X)) ≤ 𝓝 (g, x₂)
Tactic: refine ⟨(g, x₂), by simp_rw [hg1], ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (goal)
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)
⊢ (↑𝒰 : Filter (G × X)) ≤ 𝓝 (g, x₂)
have refine_2 : Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g) ∧ Tendsto snd (↑𝒰 : Filter (G × X)) (𝓝 x₂)
Tactic: rw [nhds_prod_eq, 𝒰.le_prod]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (goal)
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
⊢ 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)
have 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)
Tactic: rw [properSMul_iff_continuousSMul_ultrafilter_tendsto]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (goal)
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)
have 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)
Tactic: refine and_congr_right fun hc ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (goal)
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),
      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)
have 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)
Tactic: congrm ∀ 𝒰 x₁ x₂ hxx, ∃ g, ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (goal)
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
⊢ T2Space.{u_2} (Quotient (MulAction.orbitRel G X))
have rw : IsClosed[instTopologicalSpaceProd] (diagonal (Quotient (MulAction.orbitRel G X)))
Tactic: rw [t2_iff_isClosed_diagonal]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (hypothesis)
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'
⊢ IsClosed[instTopologicalSpaceProd] (diagonal (Quotient R))
have this : IsOpenQuotientMap (Prod.map π π)
Tactic: have : IsOpenQuotientMap (Prod.map π π) :=
    MulAction.isOpenQuotientMap_quotientMk.prodMap MulAction.isOpenQuotientMap_quotientMk
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (goal)
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] (diagonal (Quotient R))
have rw : IsClosed[instTopologicalSpaceProd] (Prod.map π π ⁻¹' diagonal (Quotient R))
Tactic: rw [← this.isQuotientMap.isClosed_preimage]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (goal)
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] (Prod.map π π ⁻¹' diagonal (Quotient R))
have h : Prod.map π π ⁻¹' diagonal (Quotient R) = range fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)
Tactic: convert! ProperSMul.isProperMap_smul_pair.isClosedMap.isClosed_range
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (goal)
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 π π)
⊢ Prod.map π π ⁻¹' diagonal (Quotient R) = range fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)
have 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₂)
Tactic: ext ⟨x₁, x₂⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (goal)
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
⊢ (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₂)
have h : π x₁ = π x₂ ↔ ∃ (a : G), a • x₂ = x₁
Tactic: simp only [mem_preimage, map_apply, mem_diagonal_iff, mem_range, Prod.mk.injEq, Prod.exists,
      exists_eq_right]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (goal)
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
⊢ π x₁ = π x₂ ↔ ∃ (a : G), a • x₂ = x₁
have h : (R : X → X → Prop) x₁ x₂ ↔ ∃ (a : G), a • x₂ = x₁
Tactic: rw [Quotient.eq', MulAction.orbitRel_apply, MulAction.mem_orbit_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (goal)
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₁
⊢ π x₁ = π x₂ ↔ ∃ (a : G), a • x₂ = x₁
have h₁ : x₁ ∈ MulAction.orbit G x₂ ↔ ∃ (a : G), a • x₂ = x₁
Tactic: rw [Quotient.eq', MulAction.orbitRel_apply, MulAction.mem_orbit_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (goal)
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₁
⊢ π x₁ = π x₂ ↔ ∃ (a : G), a • x₂ = x₁
have h₂ : (∃ (x : G), x • x₂ = x₁) ↔ ∃ (a : G), a • x₂ = x₁
Tactic: rw [Quotient.eq', MulAction.orbitRel_apply, MulAction.mem_orbit_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (goal)
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_proper : ProperSMul G X
inst_4 : T1Space G
f : (x : X) → G × X := fun (x : X) ↦ (1, x)
⊢ IsProperMap f
have refine : IsClosed[instTopologicalSpaceProd] (range f)
Tactic: refine IsClosedEmbedding.isProperMap ⟨isEmbedding_prodMkRight 1, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (hypothesis)
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_proper : ProperSMul G X
inst_4 : T1Space G
f : (x : X) → G × X := fun (x : X) ↦ (1, x)
⊢ IsClosed[instTopologicalSpaceProd] (range f)
have this : range f = SProd.sprod (α := Set G) (β := Set X) {1} univ
Tactic: have : range f = ({1} ×ˢ univ) := by simp [f, Set.singleton_prod]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (goal)
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_proper : ProperSMul G X
inst_4 : T1Space G
f : (x : X) → G × X := fun (x : X) ↦ (1, x)
this : range f = SProd.sprod (α := Set G) (β := Set X) {1} univ
⊢ IsClosed[instTopologicalSpaceProd] (range f)
have rw : IsClosed[instTopologicalSpaceProd] (SProd.sprod (α := Set G) (β := Set X) {1} univ)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (hypothesis)
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_proper : ProperSMul G X
inst_4 : T1Space G
f : (x : X) → G × X := fun (x : X) ↦ (1, x)
⊢ T2Space X
have proper_f : IsProperMap f
Tactic: have proper_f : IsProperMap f := by
    refine IsClosedEmbedding.isProperMap ⟨isEmbedding_prodMkRight 1, ?_⟩
    have : range f = ({1} ×ˢ univ) := by simp [f, Set.singleton_prod]
    rw [this]
    exact isClosed_singleton.prod isClosed_univ
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (goal)
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_proper : ProperSMul G X
inst_4 : T1Space G
f : (x : X) → G × X := fun (x : X) ↦ (1, x)
proper_f : IsProperMap f
⊢ T2Space X
have rw : IsClosed[instTopologicalSpaceProd] (diagonal X)
Tactic: rw [t2_iff_isClosed_diagonal]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (hypothesis)
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_proper : ProperSMul G X
inst_4 : T1Space G
f : (x : X) → G × X := fun (x : X) ↦ (1, x)
proper_f : IsProperMap f
g : (gx : G × X) → X × X := fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)
⊢ IsClosed[instTopologicalSpaceProd] (diagonal X)
have proper_g : IsProperMap g
Tactic: have proper_g : IsProperMap g := (properSMul_iff G X).1 h_proper
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (goal)
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_proper : ProperSMul G X
inst_4 : T1Space G
f : (x : X) → G × X := fun (x : X) ↦ (1, x)
proper_f : IsProperMap f
g : (gx : G × X) → X × X := fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)
proper_g : IsProperMap g
⊢ g ∘ f = fun (x : X) ↦ (x, x)
have h : ∀ (x : X), ((g ∘ f) x).1 = (x, x).1
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (goal)
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_proper : ProperSMul G X
inst_4 : T1Space G
f : (x : X) → G × X := fun (x : X) ↦ (1, x)
proper_f : IsProperMap f
g : (gx : G × X) → X × X := fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)
proper_g : IsProperMap g
h : ∀ (x : X), ((g ∘ f) x).1 = (x, x).1
⊢ g ∘ f = fun (x : X) ↦ (x, x)
have h₁ : ∀ (x : X), ((g ∘ f) x).2 = (x, x).2
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (hypothesis)
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_proper : ProperSMul G X
inst_4 : T1Space G
f : (x : X) → G × X := fun (x : X) ↦ (1, x)
proper_f : IsProperMap f
g : (gx : G × X) → X × X := fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)
proper_g : IsProperMap g
⊢ IsClosed[instTopologicalSpaceProd] (diagonal X)
have this : g ∘ f = fun (x : X) ↦ (x, x)
Tactic: have : g ∘ f = fun x ↦ (x, x) := by ext x <;> simp [f, g]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (hypothesis)
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_proper : ProperSMul G X
inst_4 : T1Space G
f : (x : X) → G × X := fun (x : X) ↦ (1, x)
proper_f : IsProperMap f
g : (gx : G × X) → X × X := fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)
proper_g : IsProperMap g
this : g ∘ f = fun (x : X) ↦ (x, x)
⊢ IsClosed[instTopologicalSpaceProd] (diagonal X)
have range_gf : range (g ∘ f) = diagonal X
Tactic: have range_gf : range (g ∘ f) = diagonal X := by simp [this]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (goal)
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_proper : ProperSMul G X
inst_4 : T1Space G
f : (x : X) → G × X := fun (x : X) ↦ (1, x)
proper_f : IsProperMap f
g : (gx : G × X) → X × X := fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)
proper_g : IsProperMap g
this : g ∘ f = fun (x : X) ↦ (x, x)
range_gf : range (g ∘ f) = diagonal X
⊢ IsClosed[instTopologicalSpaceProd] (diagonal X)
have rw : IsClosed[instTopologicalSpaceProd] (range (g ∘ f))
Tactic: rw [← range_gf]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (hypothesis)
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 : Type u_3
inst_4 : Group H
inst_5 : MulAction H X
inst_6 : TopologicalSpace H
inst_7 : ProperSMul G X
f : H →* G
f_clemb : IsClosedEmbedding.{u_3, u_1} (X := H) (Y := G) (⇑f : (a : H) → G)
f_compat : ∀ (h : H) (x : X), HSMul.hSMul.{u_1, u_2, u_2} (α := G) ((f : (a : H) → G) h : G) x = h • x
⊢ IsProperMap (Y := X × X) fun (gx : H × X) ↦ (gx.1 • gx.2, gx.2)
have h : IsProperMap (X := H × X) (Y := G × X) (Prod.map (⇑f : (a : H) → G) fun (x : X) ↦ x)
Tactic: have h : IsProperMap (Prod.map f (fun x : X ↦ x)) := f_clemb.isProperMap.prodMap isProperMap_id
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (hypothesis)
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 : Type u_3
inst_4 : Group H
inst_5 : MulAction H X
inst_6 : TopologicalSpace H
inst_7 : ProperSMul G X
f : H →* G
f_clemb : IsClosedEmbedding.{u_3, u_1} (X := H) (Y := G) (⇑f : (a : H) → G)
f_compat : ∀ (h : H) (x : X), HSMul.hSMul.{u_1, u_2, u_2} (α := G) ((f : (a : H) → G) h : G) x = h • x
h : IsProperMap (X := H × X) (Y := G × X) (Prod.map (⇑f : (a : H) → G) fun (x : X) ↦ x)
⊢ IsProperMap (Y := X × X) fun (gx : H × X) ↦ (gx.1 • gx.2, gx.2)
have this : Eq (α := (hx : H × X) → X × X) (fun (hx : H × X) ↦ (hx.1 • hx.2, hx.2)) fun (hx : H × X) ↦
  (HSMul.hSMul.{u_1, u_2, u_2} (α := G) ((f : (a : H) → G) hx.1 : G) hx.2, hx.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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (goal)
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 : Type u_3
inst_4 : Group H
inst_5 : MulAction H X
inst_6 : TopologicalSpace H
inst_7 : ProperSMul G X
f : H →* G
f_clemb : IsClosedEmbedding.{u_3, u_1} (X := H) (Y := G) (⇑f : (a : H) → G)
f_compat : ∀ (h : H) (x : X), HSMul.hSMul.{u_1, u_2, u_2} (α := G) ((f : (a : H) → G) h : G) x = h • x
h : IsProperMap (X := H × X) (Y := G × X) (Prod.map (⇑f : (a : H) → G) fun (x : X) ↦ x)
this :
  Eq (α := (hx : H × X) → X × X) (fun (hx : H × X) ↦ (hx.1 • hx.2, hx.2)) fun (hx : H × X) ↦
    (HSMul.hSMul.{u_1, u_2, u_2} (α := G) ((f : (a : H) → G) hx.1 : G) hx.2, hx.2)
⊢ IsProperMap (Y := X × X) fun (gx : H × X) ↦ (gx.1 • gx.2, gx.2)
have rw : IsProperMap (Y := X × X) fun (hx : H × X) ↦
  (HSMul.hSMul.{u_1, u_2, u_2} (α := G) ((f : (a : H) → G) hx.1 : G) hx.2, hx.2)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (hypothesis)
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
t : Set X
Φ : G × X → X × X := fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)
⊢ IsProperMap (Y := X × (↑t : Type u_2)) fun (gx : Prod.{u_1, u_2} G (↑t : Type u_2)) ↦ (gx.1 • (↑gx.2 : X), gx.2)
have Φ_proper : IsProperMap Φ
Tactic: have Φ_proper : IsProperMap Φ := ProperSMul.isProperMap_smul_pair
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (goal)
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
t : Set X
Φ : G × X → X × X := fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)
Φ_proper : IsProperMap Φ
⊢ SProd.sprod (α := Set G) univ t = Φ ⁻¹' snd ⁻¹' t
have h : ∀ (x : G × X), x ∈ SProd.sprod (α := Set G) univ t ↔ x ∈ Φ ⁻¹' snd ⁻¹' t
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (hypothesis)
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
s : Set G
t : Set X
hs : IsClosed[inst_2] s
ht : IsCompact t
Ψ : Prod.{u_1, u_2} G (↑t : Type u_2) → X × (↑t : Type u_2) :=
  fun (gx : Prod.{u_1, u_2} G (↑t : Type u_2)) ↦ (gx.1 • (↑gx.2 : X), gx.2)
⊢ IsClosed[inst_3] (s • t)
have Ψ_proper : IsProperMap Ψ
Tactic: have Ψ_proper : IsProperMap Ψ := ProperSMul.isProperMap_smul_pair_set
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (hypothesis)
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
s : Set G
t : Set X
hs : IsClosed[inst_2] s
ht : IsCompact t
Ψ : Prod.{u_1, u_2} G (↑t : Type u_2) → X × (↑t : Type u_2) :=
  fun (gx : Prod.{u_1, u_2} G (↑t : Type u_2)) ↦ (gx.1 • (↑gx.2 : X), gx.2)
Ψ_proper : IsProperMap Ψ
⊢ IsClosed[inst_3] (s • t)
have this : s • t = fst ∘ Ψ '' fst ⁻¹' s
Tactic: have : s • t = (fst ∘ Ψ) '' fst ⁻¹' s :=
    subset_antisymm
      (smul_subset_iff.mpr fun g hg x hx ↦ mem_image_of_mem (fst ∘ Ψ) (x := ⟨g, ⟨x, hx⟩⟩) hg)
      (image_subset_iff.mpr fun ⟨g, ⟨x, hx⟩⟩ hg ↦ smul_mem_smul hg hx)
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (goal)
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
s : Set G
t : Set X
hs : IsClosed[inst_2] s
ht : IsCompact t
Ψ : Prod.{u_1, u_2} G (↑t : Type u_2) → X × (↑t : Type u_2) :=
  fun (gx : Prod.{u_1, u_2} G (↑t : Type u_2)) ↦ (gx.1 • (↑gx.2 : X), gx.2)
Ψ_proper : IsProperMap Ψ
this : s • t = fst ∘ Ψ '' fst ⁻¹' s
⊢ IsClosed[inst_3] (s • t)
have rw : IsClosed[inst_3] (fst ∘ Ψ '' fst ⁻¹' s)
Tactic: rw [this]