mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: case mpr
z : ℍ
r : ℝ
w : ℂ
⊢ w ∈ sphere (↑(z.center r)) (z.im * Real.sinh r) → w ∈ UpperHalfPlane.coe '' sphere z r

Tactic:
·

Goal state after:
case mpr
z : ℍ
r : ℝ
w : ℂ
⊢ w ∈ sphere (↑(z.center r)) (z.im * Real.sinh r) → w ∈ UpperHalfPlane.coe '' sphere z r
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: 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)

pp: 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:
·

Goal state after:
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)
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: 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:
·

Goal state after:
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
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: case pos
z w : ℍ
r : ℝ
g : SL(2, ℝ)
h₀ : Isometry fun z ↦ ModularGroup.S • z
hc : ↑g 1 0 = 0
⊢ Isometry fun x ↦ g • x

pp: case neg
z w : ℍ
r : ℝ
g : SL(2, ℝ)
h₀ : Isometry fun z ↦ ModularGroup.S • z
hc : ¬↑g 1 0 = 0
⊢ Isometry fun x ↦ g • x

Tactic:
·

Goal state after:
case pos
z w : ℍ
r : ℝ
g : SL(2, ℝ)
h₀ : Isometry fun z ↦ ModularGroup.S • z
hc : ↑g 1 0 = 0
⊢ Isometry fun x ↦ g • x
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: case neg
z w : ℍ
r : ℝ
g : SL(2, ℝ)
h₀ : Isometry fun z ↦ ModularGroup.S • z
hc : ¬↑g 1 0 = 0
⊢ Isometry fun x ↦ g • x

Tactic:
·

Goal state after:
case neg
z w : ℍ
r : ℝ
g : SL(2, ℝ)
h₀ : Isometry fun z ↦ ModularGroup.S • z
hc : ¬↑g 1 0 = 0
⊢ Isometry fun x ↦ g • x
Module: Mathlib.Topology.Category.CompHaus.Basic

Goal state before:
pp: X : TopCat
Y : CompHaus
f : ↑(stoneCechObj X).toTop → ↑Y.toTop
hf : Continuous f
x : ↑(of (fun x ↦ True) (StoneCech ↑X)).toTop
⊢ Set.EqOn (stoneCechExtend ⋯) f (Set.range stoneCechUnit)

Tactic:
·

Goal state after:
X : TopCat
Y : CompHaus
f : ↑(stoneCechObj X).toTop → ↑Y.toTop
hf : Continuous f
x : ↑(of (fun x ↦ True) (StoneCech ↑X)).toTop
⊢ Set.EqOn (stoneCechExtend ⋯) f (Set.range stoneCechUnit)
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : 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))

Tactic:
convert! ProperSMul.isProperMap_smul_pair.isClosedMap.isClosed_range

Goal state after:
case e'_3
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : 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 ↦ (gx.1 • gx.2, gx.2)

case convert_1
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : ProperSMul G X
R : Setoid X := ⋯
π : X → Quotient R := ⋯
this : IsOpenQuotientMap (Prod.map π π)
⊢ Type ?u.52

case convert_3
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : ProperSMul G X
R : Setoid X := ⋯
π : X → Quotient R := ⋯
this : IsOpenQuotientMap (Prod.map π π)
⊢ TopologicalSpace ?convert_1

case convert_5
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : ProperSMul G X
R : Setoid X := ⋯
π : X → Quotient R := ⋯
this : IsOpenQuotientMap (Prod.map π π)
⊢ Group ?convert_1

case convert_6
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : ProperSMul G X
R : Setoid X := ⋯
π : X → Quotient R := ⋯
this : IsOpenQuotientMap (Prod.map π π)
⊢ MulAction ?convert_1 X

case convert_7
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : ProperSMul G X
R : Setoid X := ⋯
π : X → Quotient R := ⋯
this : IsOpenQuotientMap (Prod.map π π)
⊢ ProperSMul ?convert_1 X
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: case e'_3
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : 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 ↦ (gx.1 • gx.2, gx.2)

pp: case convert_1
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : ProperSMul G X
R : Setoid X := ⋯
π : X → Quotient R := ⋯
this : IsOpenQuotientMap (Prod.map π π)
⊢ Type ?u.52

pp: case convert_3
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : ProperSMul G X
R : Setoid X := ⋯
π : X → Quotient R := ⋯
this : IsOpenQuotientMap (Prod.map π π)
⊢ TopologicalSpace ?convert_1

pp: case convert_5
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : ProperSMul G X
R : Setoid X := ⋯
π : X → Quotient R := ⋯
this : IsOpenQuotientMap (Prod.map π π)
⊢ Group ?convert_1

pp: case convert_6
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : ProperSMul G X
R : Setoid X := ⋯
π : X → Quotient R := ⋯
this : IsOpenQuotientMap (Prod.map π π)
⊢ MulAction ?convert_1 X

pp: case convert_7
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : ProperSMul G X
R : Setoid X := ⋯
π : X → Quotient R := ⋯
this : IsOpenQuotientMap (Prod.map π π)
⊢ ProperSMul ?convert_1 X

Tactic:
·

Goal state after:
case e'_3
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : 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 ↦ (gx.1 • gx.2, gx.2)
Module: Mathlib.Topology.Category.CompHaus.Basic

Goal state before:
pp: case hf
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := ⋯
this :
  {u | ∀ {i j : J} (f : i ⟶ j), (ConcreteCategory.hom (F.map f)) (u i) = u j} =
    ⋂ i, ⋂ j, ⋂ f, {u | (ConcreteCategory.hom (F.map f)) (u i) = u j}
i j : J
f : i ⟶ j
⊢ Continuous fun y ↦ (ConcreteCategory.hom (F.map f)) (y i)

pp: case hg
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := ⋯
this :
  {u | ∀ {i j : J} (f : i ⟶ j), (ConcreteCategory.hom (F.map f)) (u i) = u j} =
    ⋂ i, ⋂ j, ⋂ f, {u | (ConcreteCategory.hom (F.map f)) (u i) = u j}
i j : J
f : i ⟶ j
⊢ Continuous fun y ↦ y j

Tactic:
·

Goal state after:
case hf
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := ⋯
this :
  {u | ∀ {i j : J} (f : i ⟶ j), (ConcreteCategory.hom (F.map f)) (u i) = u j} =
    ⋂ i, ⋂ j, ⋂ f, {u | (ConcreteCategory.hom (F.map f)) (u i) = u j}
i j : J
f : i ⟶ j
⊢ Continuous fun y ↦ (ConcreteCategory.hom (F.map f)) (y i)
Module: Mathlib.Topology.Category.CompHaus.Basic

Goal state before:
pp: case hg
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := ⋯
this :
  {u | ∀ {i j : J} (f : i ⟶ j), (ConcreteCategory.hom (F.map f)) (u i) = u j} =
    ⋂ i, ⋂ j, ⋂ f, {u | (ConcreteCategory.hom (F.map f)) (u i) = u j}
i j : J
f : i ⟶ j
⊢ Continuous fun y ↦ y j

Tactic:
·

Goal state after:
case hg
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := ⋯
this :
  {u | ∀ {i j : J} (f : i ⟶ j), (ConcreteCategory.hom (F.map f)) (u i) = u j} =
    ⋂ i, ⋂ j, ⋂ f, {u | (ConcreteCategory.hom (F.map f)) (u i) = u j}
i j : J
f : i ⟶ j
⊢ Continuous fun y ↦ y j
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: case a
X : Type w
t : TopologicalSpace X
inst✝ : UCompactlyGeneratedSpace X
⊢ t ≤ compactlyGenerated X

pp: case a
X : Type w
t : TopologicalSpace X
inst✝ : UCompactlyGeneratedSpace X
⊢ compactlyGenerated X ≤ t

Tactic:
·

Goal state after:
case a
X : Type w
t : TopologicalSpace X
inst✝ : UCompactlyGeneratedSpace X
⊢ t ≤ compactlyGenerated X
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: case a
X : Type w
t : TopologicalSpace X
inst✝ : UCompactlyGeneratedSpace X
⊢ compactlyGenerated X ≤ t

Tactic:
·

Goal state after:
case a
X : Type w
t : TopologicalSpace X
inst✝ : UCompactlyGeneratedSpace X
⊢ compactlyGenerated X ≤ t
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
⊢ ∀ (i : Set (OnePoint X)),
    ∞ ∈ i ∧ IsOpen[instTopologicalSpace] i → ∃ i', (IsClosed[inst✝] i' ∧ IsCompact i') ∧ some '' i'ᶜ ⊆ i ∩ {∞}ᶜ

pp: case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
⊢ ∀ (i' : Set X),
    IsClosed[inst✝] i' ∧ IsCompact i' → ∃ i, (∞ ∈ i ∧ IsOpen[instTopologicalSpace] i) ∧ i ∩ {∞}ᶜ ⊆ some '' i'ᶜ

Tactic:
·

Goal state after:
case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
⊢ ∀ (i : Set (OnePoint X)),
    ∞ ∈ i ∧ IsOpen[instTopologicalSpace] i → ∃ i', (IsClosed[inst✝] i' ∧ IsCompact i') ∧ some '' i'ᶜ ⊆ i ∩ {∞}ᶜ
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
⊢ ∀ (i' : Set X),
    IsClosed[inst✝] i' ∧ IsCompact i' → ∃ i, (∞ ∈ i ∧ IsOpen[instTopologicalSpace] i) ∧ i ∩ {∞}ᶜ ⊆ some '' i'ᶜ

Tactic:
·

Goal state after:
case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
⊢ ∀ (i' : Set X),
    IsClosed[inst✝] i' ∧ IsCompact i' → ∃ i, (∞ ∈ i ∧ IsOpen[instTopologicalSpace] i) ∧ i ∩ {∞}ᶜ ⊆ some '' i'ᶜ
Module: Mathlib.Topology.Category.CompHaus.Basic

Goal state before:
pp: case mp
X Y : CompHaus
f : X ⟶ Y
⊢ Epi f → Function.Surjective ⇑(ConcreteCategory.hom f)

pp: case mpr
X Y : CompHaus
f : X ⟶ Y
⊢ Function.Surjective ⇑(ConcreteCategory.hom f) → Epi f

Tactic:
·

Goal state after:
case mp
X Y : CompHaus
f : X ⟶ Y
⊢ Epi f → Function.Surjective ⇑(ConcreteCategory.hom f)
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: case refine_1
X : Type u_1
Y✝ : Type u_2
inst✝⁴ : TopologicalSpace X
s : Set (OnePoint X)
Y : Type u_3
inst✝³ : DiscreteTopology X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
inst✝ : Infinite X
f : C(OnePoint X, Y)
x : OnePoint X
⊢ ((fun f ↦
          {
            toFun := fun x ↦
              match x with
              | none => Classical.choose ⋯
              | Option.some x => ↑f x,
            continuous_toFun := ⋯ })
        ((fun f ↦ ⟨fun x ↦ f ↑x, ⋯⟩) f))
      ∞ =
    f ∞

pp: case refine_2
X : Type u_1
Y✝ : Type u_2
inst✝⁴ : TopologicalSpace X
s : Set (OnePoint X)
Y : Type u_3
inst✝³ : DiscreteTopology X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
inst✝ : Infinite X
f : C(OnePoint X, Y)
x : OnePoint X
⊢ ∀ (x : X),
    ((fun f ↦
            {
              toFun := fun x ↦
                match x with
                | none => Classical.choose ⋯
                | Option.some x => ↑f x,
              continuous_toFun := ⋯ })
          ((fun f ↦ ⟨fun x ↦ f ↑x, ⋯⟩) f))
        ↑x =
      f ↑x

Tactic:
·

Goal state after:
case refine_1
X : Type u_1
Y✝ : Type u_2
inst✝⁴ : TopologicalSpace X
s : Set (OnePoint X)
Y : Type u_3
inst✝³ : DiscreteTopology X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
inst✝ : Infinite X
f : C(OnePoint X, Y)
x : OnePoint X
⊢ ((fun f ↦
          {
            toFun := fun x ↦
              match x with
              | none => Classical.choose ⋯
              | Option.some x => ↑f x,
            continuous_toFun := ⋯ })
        ((fun f ↦ ⟨fun x ↦ f ↑x, ⋯⟩) f))
      ∞ =
    f ∞
Module: Mathlib.Topology.Category.CompHaus.Basic

Goal state before:
pp: case mpr
X Y : CompHaus
f : X ⟶ Y
⊢ Function.Surjective ⇑(ConcreteCategory.hom f) → Epi f

Tactic:
·

Goal state after:
case mpr
X Y : CompHaus
f : X ⟶ Y
⊢ Function.Surjective ⇑(ConcreteCategory.hom f) → Epi f
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: case refine_2
X : Type u_1
Y✝ : Type u_2
inst✝⁴ : TopologicalSpace X
s : Set (OnePoint X)
Y : Type u_3
inst✝³ : DiscreteTopology X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
inst✝ : Infinite X
f : C(OnePoint X, Y)
x : OnePoint X
⊢ ∀ (x : X),
    ((fun f ↦
            {
              toFun := fun x ↦
                match x with
                | none => Classical.choose ⋯
                | Option.some x => ↑f x,
              continuous_toFun := ⋯ })
          ((fun f ↦ ⟨fun x ↦ f ↑x, ⋯⟩) f))
        ↑x =
      f ↑x

Tactic:
·

Goal state after:
case refine_2
X : Type u_1
Y✝ : Type u_2
inst✝⁴ : TopologicalSpace X
s : Set (OnePoint X)
Y : Type u_3
inst✝³ : DiscreteTopology X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
inst✝ : Infinite X
f : C(OnePoint X, Y)
x : OnePoint X
⊢ ∀ (x : X),
    ((fun f ↦
            {
              toFun := fun x ↦
                match x with
                | none => Classical.choose ⋯
                | Option.some x => ↑f x,
              continuous_toFun := ⋯ })
          ((fun f ↦ ⟨fun x ↦ f ↑x, ⋯⟩) f))
        ↑x =
      f ↑x
Module: Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated

Goal state before:
pp: case ht
G : Type u_1
X : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : MulAction G X
inst✝² : CompactlyGeneratedSpace (X × X)
inst✝¹ : T2Space X
inst✝ : ContinuousSMul G X
h : ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact {g | (g • U ∩ V).Nonempty}
K : Set (X × X)
hK : IsCompact K
U : Set X := ⋯
V : Set X := ⋯
hU : IsCompact U
hV : IsCompact V
⊢ IsClosed ((fun gx ↦ (gx.1 • gx.2, gx.2)) ⁻¹' U ×ˢ V)

pp: case h
G : Type u_1
X : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : MulAction G X
inst✝² : CompactlyGeneratedSpace (X × X)
inst✝¹ : T2Space X
inst✝ : ContinuousSMul G X
h : ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact {g | (g • U ∩ V).Nonempty}
K : Set (X × X)
hK : IsCompact K
U : Set X := ⋯
V : Set X := ⋯
hU : IsCompact U
hV : IsCompact V
⊢ (fun gx ↦ (gx.1 • gx.2, gx.2)) ⁻¹' U ×ˢ V ⊆ {g | (g • V ∩ U).Nonempty} ×ˢ V

Tactic:
·

Goal state after:
case ht
G : Type u_1
X : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : MulAction G X
inst✝² : CompactlyGeneratedSpace (X × X)
inst✝¹ : T2Space X
inst✝ : ContinuousSMul G X
h : ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact {g | (g • U ∩ V).Nonempty}
K : Set (X × X)
hK : IsCompact K
U : Set X := ⋯
V : Set X := ⋯
hU : IsCompact U
hV : IsCompact V
⊢ IsClosed ((fun gx ↦ (gx.1 • gx.2, gx.2)) ⁻¹' U ×ˢ V)
Module: Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated

Goal state before:
pp: case h
G : Type u_1
X : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : MulAction G X
inst✝² : CompactlyGeneratedSpace (X × X)
inst✝¹ : T2Space X
inst✝ : ContinuousSMul G X
h : ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact {g | (g • U ∩ V).Nonempty}
K : Set (X × X)
hK : IsCompact K
U : Set X := ⋯
V : Set X := ⋯
hU : IsCompact U
hV : IsCompact V
⊢ (fun gx ↦ (gx.1 • gx.2, gx.2)) ⁻¹' U ×ˢ V ⊆ {g | (g • V ∩ U).Nonempty} ×ˢ V

Tactic:
·

Goal state after:
case h
G : Type u_1
X : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : MulAction G X
inst✝² : CompactlyGeneratedSpace (X × X)
inst✝¹ : T2Space X
inst✝ : ContinuousSMul G X
h : ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact {g | (g • U ∩ V).Nonempty}
K : Set (X × X)
hK : IsCompact K
U : Set X := ⋯
V : Set X := ⋯
hU : IsCompact U
hV : IsCompact V
⊢ (fun gx ↦ (gx.1 • gx.2, gx.2)) ⁻¹' U ×ˢ V ⊆ {g | (g • V ∩ U).Nonempty} ×ˢ V
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: case refine_1
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝¹ : UCompactlyGeneratedSpace X
inst✝ : UCompactlyGeneratedSpace Y
s : Set (X ⊕ Y)
h : ∀ (S : CompHaus) (f : C(↑S.toTop, X ⊕ Y)), IsClosed (⇑f ⁻¹' s)
S : CompHaus
x✝ : C(↑S.toTop, X)
f : ↑S.toTop → X
hf : Continuous[_, tX] f
⊢ IsClosed (⇑{ toFun := f, continuous_toFun := hf } ⁻¹' Sum.inl ⁻¹' s)

pp: case refine_2
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝¹ : UCompactlyGeneratedSpace X
inst✝ : UCompactlyGeneratedSpace Y
s : Set (X ⊕ Y)
h : ∀ (S : CompHaus) (f : C(↑S.toTop, X ⊕ Y)), IsClosed (⇑f ⁻¹' s)
S : CompHaus
x✝ : C(↑S.toTop, Y)
f : ↑S.toTop → Y
hf : Continuous[_, tY] f
⊢ IsClosed (⇑{ toFun := f, continuous_toFun := hf } ⁻¹' Sum.inr ⁻¹' s)

Tactic:
·

Goal state after:
case refine_1
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝¹ : UCompactlyGeneratedSpace X
inst✝ : UCompactlyGeneratedSpace Y
s : Set (X ⊕ Y)
h : ∀ (S : CompHaus) (f : C(↑S.toTop, X ⊕ Y)), IsClosed (⇑f ⁻¹' s)
S : CompHaus
x✝ : C(↑S.toTop, X)
f : ↑S.toTop → X
hf : Continuous[_, tX] f
⊢ IsClosed (⇑{ toFun := f, continuous_toFun := hf } ⁻¹' Sum.inl ⁻¹' s)
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: case infty
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
inst✝ : T1Space X
⊢ IsClosed[instTopologicalSpace] {∞}

pp: case coe
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
inst✝ : T1Space X
x✝ : X
⊢ IsClosed[instTopologicalSpace] {↑x✝}

Tactic:
·

Goal state after:
case infty
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
inst✝ : T1Space X
⊢ IsClosed[instTopologicalSpace] {∞}
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: case refine_2
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝¹ : UCompactlyGeneratedSpace X
inst✝ : UCompactlyGeneratedSpace Y
s : Set (X ⊕ Y)
h : ∀ (S : CompHaus) (f : C(↑S.toTop, X ⊕ Y)), IsClosed (⇑f ⁻¹' s)
S : CompHaus
x✝ : C(↑S.toTop, Y)
f : ↑S.toTop → Y
hf : Continuous[_, tY] f
⊢ IsClosed (⇑{ toFun := f, continuous_toFun := hf } ⁻¹' Sum.inr ⁻¹' s)

Tactic:
·

Goal state after:
case refine_2
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝¹ : UCompactlyGeneratedSpace X
inst✝ : UCompactlyGeneratedSpace Y
s : Set (X ⊕ Y)
h : ∀ (S : CompHaus) (f : C(↑S.toTop, X ⊕ Y)), IsClosed (⇑f ⁻¹' s)
S : CompHaus
x✝ : C(↑S.toTop, Y)
f : ↑S.toTop → Y
hf : Continuous[_, tY] f
⊢ IsClosed (⇑{ toFun := f, continuous_toFun := hf } ⁻¹' Sum.inr ⁻¹' s)
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: case coe
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
inst✝ : T1Space X
x✝ : X
⊢ IsClosed[instTopologicalSpace] {↑x✝}

Tactic:
·

Goal state after:
case coe
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
inst✝ : T1Space X
x✝ : X
⊢ IsClosed[instTopologicalSpace] {↑x✝}
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: case infty.infty
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
⊢ ∞ ⤳ ∞ ∨ Disjoint (𝓝 ∞) (𝓝 ∞)

pp: case infty.coe
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
x✝ : X
⊢ ∞ ⤳ ↑x✝ ∨ Disjoint (𝓝 ∞) (𝓝 ↑x✝)

pp: case coe.infty
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
x✝ : X
⊢ ↑x✝ ⤳ ∞ ∨ Disjoint (𝓝 ↑x✝) (𝓝 ∞)

pp: case coe.coe
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
x✝¹ x✝ : X
⊢ ↑x✝¹ ⤳ ↑x✝ ∨ Disjoint (𝓝 ↑x✝¹) (𝓝 ↑x✝)

Tactic:
·

Goal state after:
case infty.infty
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
⊢ ∞ ⤳ ∞ ∨ Disjoint (𝓝 ∞) (𝓝 ∞)
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: case infty.coe
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
x✝ : X
⊢ ∞ ⤳ ↑x✝ ∨ Disjoint (𝓝 ∞) (𝓝 ↑x✝)

pp: case coe.infty
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
x✝ : X
⊢ ↑x✝ ⤳ ∞ ∨ Disjoint (𝓝 ↑x✝) (𝓝 ∞)

pp: case coe.coe
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
x✝¹ x✝ : X
⊢ ↑x✝¹ ⤳ ↑x✝ ∨ Disjoint (𝓝 ↑x✝¹) (𝓝 ↑x✝)

Tactic:
·

Goal state after:
case infty.coe
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
x✝ : X
⊢ ∞ ⤳ ↑x✝ ∨ Disjoint (𝓝 ∞) (𝓝 ↑x✝)
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: case coe.infty
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
x✝ : X
⊢ ↑x✝ ⤳ ∞ ∨ Disjoint (𝓝 ↑x✝) (𝓝 ∞)

pp: case coe.coe
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
x✝¹ x✝ : X
⊢ ↑x✝¹ ⤳ ↑x✝ ∨ Disjoint (𝓝 ↑x✝¹) (𝓝 ↑x✝)

Tactic:
·

Goal state after:
case coe.infty
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
x✝ : X
⊢ ↑x✝ ⤳ ∞ ∨ Disjoint (𝓝 ↑x✝) (𝓝 ∞)