mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
δ₁ : Type u_5
δ₂ : Type u_6
φ₁ : δ₁ → α
φ₂ : δ₂ → α
𝔗₁ : Set (Set δ₁)
𝔗₂ : Set (Set δ₂)
h_image₁ : MapsTo (fun x ↦ φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun x ↦ φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun x ↦ φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun x ↦ φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂
ψ₁ : (S : Set α) → ↑(φ₁ ⁻¹' S) → ↑S := fun S ↦ S.restrictPreimage φ₁
ψ₂ : (S : Set α) → ↑(φ₂ ⁻¹' S) → ↑S := fun S ↦ S.restrictPreimage φ₂
this :
  ∀ S ∈ 𝔖,
    UniformFun.uniformSpace (↑S) β =
      UniformSpace.comap (fun x ↦ x ∘ ψ₁ S) (UniformFun.uniformSpace (↑(φ₁ ⁻¹' S)) β) ⊓
        UniformSpace.comap (fun x ↦ x ∘ ψ₂ S) (UniformFun.uniformSpace (↑(φ₂ ⁻¹' S)) β)
⊢ UniformContinuous (⇑(ofFun 𝔗₁) ∘ (fun x ↦ x ∘ φ₁) ∘ ⇑(toFun 𝔖))

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
δ₁ : Type u_5
δ₂ : Type u_6
φ₁ : δ₁ → α
φ₂ : δ₂ → α
𝔗₁ : Set (Set δ₁)
𝔗₂ : Set (Set δ₂)
h_image₁ : MapsTo (fun x ↦ φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun x ↦ φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun x ↦ φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun x ↦ φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂
ψ₁ : (S : Set α) → ↑(φ₁ ⁻¹' S) → ↑S := fun S ↦ S.restrictPreimage φ₁
ψ₂ : (S : Set α) → ↑(φ₂ ⁻¹' S) → ↑S := fun S ↦ S.restrictPreimage φ₂
this :
  ∀ S ∈ 𝔖,
    UniformFun.uniformSpace (↑S) β =
      UniformSpace.comap (fun x ↦ x ∘ ψ₁ S) (UniformFun.uniformSpace (↑(φ₁ ⁻¹' S)) β) ⊓
        UniformSpace.comap (fun x ↦ x ∘ ψ₂ S) (UniformFun.uniformSpace (↑(φ₂ ⁻¹' S)) β)
⊢ UniformContinuous (⇑(ofFun 𝔗₁) ∘ (fun x ↦ x ∘ φ₁) ∘ ⇑(toFun 𝔖))
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: K : Type u_2
inst✝⁴ : DivisionSemiring K
inst✝³ : PartialOrder K
inst✝² : PosMulReflectLT K
inst✝¹ : IsOrderedCancelAddMonoid K
inst✝ : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
this : (fun x ↦ a * x + b) '' Ioc c d = Ioc (a * c + b) (a * d + b)
⊢ (fun x ↦ a * x + b) '' Ioc c d = Ioc (a * c + b) (a * d + b)

Tactic:
]

Goal state after:
K : Type u_2
inst✝⁴ : DivisionSemiring K
inst✝³ : PartialOrder K
inst✝² : PosMulReflectLT K
inst✝¹ : IsOrderedCancelAddMonoid K
inst✝ : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
this : (fun x ↦ a * x + b) '' Ioc c d = Ioc (a * c + b) (a * d + b)
⊢ (fun x ↦ a * x + b) '' Ioc c d = Ioc (a * c + b) (a * d + b)
Module: Mathlib.Topology.Algebra.MulAction

Goal state before:
pp: M : Type u_1
X : Type u_2
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace X
inst✝³ : Group M
inst✝² : IsTopologicalGroup M
inst✝¹ : MulAction M X
inst✝ : DiscreteTopology X
h : ∀ (x : X), IsOpen[inst✝⁵] ↑(MulAction.stabilizer M x)
⊢ ∀ (b : X), Continuous[inst✝⁵, inst✝⁴] fun x ↦ (x, b).1 • (x, b).2

Tactic:
]

Goal state after:
M : Type u_1
X : Type u_2
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace X
inst✝³ : Group M
inst✝² : IsTopologicalGroup M
inst✝¹ : MulAction M X
inst✝ : DiscreteTopology X
h : ∀ (x : X), IsOpen[inst✝⁵] ↑(MulAction.stabilizer M x)
⊢ ∀ (b : X), Continuous[inst✝⁵, inst✝⁴] fun x ↦ (x, b).1 • (x, b).2
Module: Mathlib.Topology.Algebra.MulAction

Goal state before:
pp: M : Type u_1
X : Type u_2
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace X
inst✝³ : Group M
inst✝² : IsTopologicalGroup M
inst✝¹ : MulAction M X
inst✝ : DiscreteTopology X
h : ∀ (x : X), IsOpen[inst✝⁵] ↑(MulAction.stabilizer M x)
y : X
⊢ ∀ (b : X), IsOpen[inst✝⁵] ((fun x ↦ (x, y).1 • (x, y).2) ⁻¹' {b})

Tactic:
]

Goal state after:
M : Type u_1
X : Type u_2
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace X
inst✝³ : Group M
inst✝² : IsTopologicalGroup M
inst✝¹ : MulAction M X
inst✝ : DiscreteTopology X
h : ∀ (x : X), IsOpen[inst✝⁵] ↑(MulAction.stabilizer M x)
y : X
⊢ ∀ (b : X), IsOpen[inst✝⁵] ((fun x ↦ (x, y).1 • (x, y).2) ⁻¹' {b})
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: K : Type u_2
inst✝⁴ : DivisionSemiring K
inst✝³ : PartialOrder K
inst✝² : PosMulReflectLT K
inst✝¹ : IsOrderedCancelAddMonoid K
inst✝ : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
⊢ Ioc (a * c + b) (a * d + b) = Ioc (a * c + b) (a * d + b)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: K : Type u_2
inst✝⁴ : DivisionSemiring K
inst✝³ : PartialOrder K
inst✝² : PosMulReflectLT K
inst✝¹ : IsOrderedCancelAddMonoid K
inst✝ : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
this : (fun x ↦ a * x + b) '' Ioo c d = Ioo (a * c + b) (a * d + b)
⊢ (fun x ↦ a * x + b) '' Ioo c d = Ioo (a * c + b) (a * d + b)

Tactic:
]

Goal state after:
K : Type u_2
inst✝⁴ : DivisionSemiring K
inst✝³ : PartialOrder K
inst✝² : PosMulReflectLT K
inst✝¹ : IsOrderedCancelAddMonoid K
inst✝ : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
this : (fun x ↦ a * x + b) '' Ioo c d = Ioo (a * c + b) (a * d + b)
⊢ (fun x ↦ a * x + b) '' Ioo c d = Ioo (a * c + b) (a * d + b)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: K : Type u_2
inst✝⁴ : DivisionSemiring K
inst✝³ : PartialOrder K
inst✝² : PosMulReflectLT K
inst✝¹ : IsOrderedCancelAddMonoid K
inst✝ : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
⊢ Ioo (a * c + b) (a * d + b) = Ioo (a * c + b) (a * d + b)

Tactic:
]

Goal state after:
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
δ₁ : Type u_5
δ₂ : Type u_6
φ₁ : δ₁ → α
φ₂ : δ₂ → α
𝔗₁ : Set (Set δ₁)
𝔗₂ : Set (Set δ₂)
h_image₁ : MapsTo (fun x ↦ φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun x ↦ φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun x ↦ φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun x ↦ φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂
ψ₁ : (S : Set α) → ↑(φ₁ ⁻¹' S) → ↑S := fun S ↦ S.restrictPreimage φ₁
ψ₂ : (S : Set α) → ↑(φ₂ ⁻¹' S) → ↑S := fun S ↦ S.restrictPreimage φ₂
this :
  ∀ S ∈ 𝔖,
    UniformFun.uniformSpace (↑S) β =
      UniformSpace.comap (fun x ↦ x ∘ ψ₁ S) (UniformFun.uniformSpace (↑(φ₁ ⁻¹' S)) β) ⊓
        UniformSpace.comap (fun x ↦ x ∘ ψ₂ S) (UniformFun.uniformSpace (↑(φ₂ ⁻¹' S)) β)
⊢ UniformContinuous (⇑(ofFun 𝔗₂) ∘ (fun x ↦ x ∘ φ₂) ∘ ⇑(toFun 𝔖))

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
δ₁ : Type u_5
δ₂ : Type u_6
φ₁ : δ₁ → α
φ₂ : δ₂ → α
𝔗₁ : Set (Set δ₁)
𝔗₂ : Set (Set δ₂)
h_image₁ : MapsTo (fun x ↦ φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun x ↦ φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun x ↦ φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun x ↦ φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂
ψ₁ : (S : Set α) → ↑(φ₁ ⁻¹' S) → ↑S := fun S ↦ S.restrictPreimage φ₁
ψ₂ : (S : Set α) → ↑(φ₂ ⁻¹' S) → ↑S := fun S ↦ S.restrictPreimage φ₂
this :
  ∀ S ∈ 𝔖,
    UniformFun.uniformSpace (↑S) β =
      UniformSpace.comap (fun x ↦ x ∘ ψ₁ S) (UniformFun.uniformSpace (↑(φ₁ ⁻¹' S)) β) ⊓
        UniformSpace.comap (fun x ↦ x ∘ ψ₂ S) (UniformFun.uniformSpace (↑(φ₂ ⁻¹' S)) β)
⊢ UniformContinuous (⇑(ofFun 𝔗₂) ∘ (fun x ↦ x ∘ φ₂) ∘ ⇑(toFun 𝔖))
Module: Mathlib.Topology.Algebra.MulAction

Goal state before:
pp: G₀ : Type u_5
X : Type u_6
inst✝⁶ : GroupWithZero G₀
inst✝⁵ : Zero X
inst✝⁴ : MulActionWithZero G₀ X
inst✝³ : TopologicalSpace G₀
inst✝² : (𝓝[≠] 0).NeBot
inst✝¹ : TopologicalSpace X
inst✝ : ContinuousSMul G₀ X
⊢ ∀ (i : Unit × Set X), True ∧ i.2 ∈ 𝓝 0 → Set.univ • id i.2 = Set.univ

Tactic:
]

Goal state after:
G₀ : Type u_5
X : Type u_6
inst✝⁶ : GroupWithZero G₀
inst✝⁵ : Zero X
inst✝⁴ : MulActionWithZero G₀ X
inst✝³ : TopologicalSpace G₀
inst✝² : (𝓝[≠] 0).NeBot
inst✝¹ : TopologicalSpace X
inst✝ : ContinuousSMul G₀ X
⊢ ∀ (i : Unit × Set X), True ∧ i.2 ∈ 𝓝 0 → Set.univ • id i.2 = Set.univ
Module: Mathlib.Topology.Algebra.MulAction

Goal state before:
pp: M : Type u_2
X : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : SMul M X
ts : Set (TopologicalSpace X)
h : ∀ t ∈ ts, ContinuousSMul M X
x✝ : TopologicalSpace X := sInf ts
⊢ Continuous[instTopologicalSpaceProd, sInf ts] fun p ↦ p.1 • p.2

Tactic:
]

Goal state after:
M : Type u_2
X : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : SMul M X
ts : Set (TopologicalSpace X)
h : ∀ t ∈ ts, ContinuousSMul M X
x✝ : TopologicalSpace X := sInf ts
⊢ Continuous[instTopologicalSpaceProd, sInf ts] fun p ↦ p.1 • p.2
Module: Mathlib.Topology.Algebra.MulAction

Goal state before:
pp: M : Type u_2
X : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : SMul M X
t₁ t₂ : TopologicalSpace X
inst✝¹ : ContinuousSMul M X
inst✝ : ContinuousSMul M X
⊢ ContinuousSMul M X

Tactic:
]

Goal state after:
M : Type u_2
X : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : SMul M X
t₁ t₂ : TopologicalSpace X
inst✝¹ : ContinuousSMul M X
inst✝ : ContinuousSMul M X
⊢ ContinuousSMul M X
Module: Mathlib.Topology.Algebra.MulAction

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝⁵ : AddGroup G
inst✝⁴ : AddTorsor G P
inst✝³ : TopologicalSpace G
inst✝² : PreconnectedSpace G
inst✝¹ : TopologicalSpace P
inst✝ : ContinuousVAdd G P
⊢ Set.univ = Set.univ

Tactic:
]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : C(β, γ)
g₁ g₂ : C(α, β)
hf : Injective ⇑f
h : f.comp g₁ = f.comp g₂
a : α
⊢ f (g₂ a) = f (g₂ a)

Tactic:
]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
g : C(α, β)
x : α
hf : Continuous[inst✝¹, inst✝] f
⊢ f x = f x

Tactic:
]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
f : α → β
g : C(↑s, β)
hf : ¬Continuous[instTopologicalSpaceSubtype, inst✝] (s.domRestrict f)
⊢ mkD (s.domRestrict f) g = g

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
f : α → β
g : C(↑s, β)
hf : ¬Continuous[instTopologicalSpaceSubtype, inst✝] (s.domRestrict f)
⊢ mkD (s.domRestrict f) g = g
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: case h.inl
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
hb✝ : a ≠ 0
U V : Set α
hV : V = (fun x ↦ a * x) ⁻¹' U
aU : α
haU : U = Ioi aU
hb : a < 0
⊢ Iio (a⁻¹ * aU) = Iio (a⁻¹ * aU)

Tactic:
]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
f : α → β
g : C(↑s, β)
x : ↑s
hf : ContinuousOn f s
⊢ f ↑x = f ↑x

Tactic:
]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g : C(α, β)
ι : Type u_5
S : ι → Set α
φ : (i : ι) → C(↑(S i), β)
hφ : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), (φ i) ⟨x, hxi⟩ = (φ j) ⟨x, hxj⟩
hS : ∀ (x : α), ∃ i, S i ∈ 𝓝 x
H : ⋃ i, S i = Set.univ
i : ι
⊢ Continuous[instTopologicalSpaceSubtype, inst✝²] ((S i).domRestrict (Set.liftCover S (fun i ↦ ⇑(φ i)) hφ H))

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g : C(α, β)
ι : Type u_5
S : ι → Set α
φ : (i : ι) → C(↑(S i), β)
hφ : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), (φ i) ⟨x, hxi⟩ = (φ j) ⟨x, hxj⟩
hS : ∀ (x : α), ∃ i, S i ∈ 𝓝 x
H : ⋃ i, S i = Set.univ
i : ι
⊢ Continuous[instTopologicalSpaceSubtype, inst✝²] ((S i).domRestrict (Set.liftCover S (fun i ↦ ⇑(φ i)) hφ H))
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: case h.inr
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
hb✝ : a ≠ 0
U V : Set α
hV : V = (fun x ↦ a * x) ⁻¹' U
aU : α
haU : U = Ioi aU
hb : 0 < a
⊢ Ioi (a⁻¹ * aU) = Ioi (a⁻¹ * aU)

Tactic:
]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
ι : Type u_5
S : ι → Set α
φ : (i : ι) → C(↑(S i), β)
hφ : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), (φ i) ⟨x, hxi⟩ = (φ j) ⟨x, hxj⟩
hS : ∀ (x : α), ∃ i, S i ∈ 𝓝 x
i : ι
x : ↑(S i)
⊢ (φ i) x = (φ i) x

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: case h.inl
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
hb✝ : a ≠ 0
U V : Set α
hV : V = (fun x ↦ a * x) ⁻¹' U
aU : α
haU : U = Iio aU
hb : a < 0
⊢ Ioi (a⁻¹ * aU) = Ioi (a⁻¹ * aU)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: case h.inr
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
hb✝ : a ≠ 0
U V : Set α
hV : V = (fun x ↦ a * x) ⁻¹' U
aU : α
haU : U = Iio aU
hb : 0 < a
⊢ Iio (a⁻¹ * aU) = Iio (a⁻¹ * aU)

Tactic:
]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(X, Y)
hf : IsQuotientMap ⇑f
⊢ Continuous[inst✝², instTopologicalSpaceQuotient] ((Setoid.quotientKerEquivOfSurjective ⇑f ⋯).invFun ∘ ⇑f)

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(X, Y)
hf : IsQuotientMap ⇑f
⊢ Continuous[inst✝², instTopologicalSpaceQuotient] ((Setoid.quotientKerEquivOfSurjective ⇑f ⋯).invFun ∘ ⇑f)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
ha : a < 0
⊢ Iio a = Iio a

Tactic:
]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(X, Y)
hf : IsQuotientMap ⇑f
g✝ : C(X, Z)
h✝ : FactorsThrough ⇑g✝ ⇑f
g : C(Y, Z)
x✝¹ x✝ : X
h : f x✝¹ = f x✝
⊢ g (f x✝) = g (f x✝)

Tactic:
]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α ≃ₜ β
⊢ ContinuousMap.id α = ContinuousMap.id α

Tactic:
]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α ≃ₜ β
⊢ ContinuousMap.id β = ContinuousMap.id β

Tactic:
]

Goal state after:
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
φ : (i : ι) → δ i → α
𝔗 : (i : ι) → Set (Set (δ i))
h_image : ∀ (i : ι), MapsTo (fun x ↦ φ i '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun x ↦ φ i ⁻¹' x) 𝔖 (𝔗 i)
h_cover : ∀ S ∈ 𝔖, ∃ I, I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i)
ψ : (S : Set α) → (i : ι) → ↑(φ i ⁻¹' S) → ↑S := fun S i ↦ S.restrictPreimage (φ i)
this :
  ∀ S ∈ 𝔖,
    UniformFun.uniformSpace (↑S) β =
      ⨅ i, UniformSpace.comap (fun x ↦ x ∘ ψ S i) (UniformFun.uniformSpace (↑(φ i ⁻¹' S)) β)
i : ι
⊢ UniformContinuous (⇑(ofFun (𝔗 i)) ∘ (fun x ↦ x ∘ φ i) ∘ ⇑(toFun 𝔖))

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
φ : (i : ι) → δ i → α
𝔗 : (i : ι) → Set (Set (δ i))
h_image : ∀ (i : ι), MapsTo (fun x ↦ φ i '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun x ↦ φ i ⁻¹' x) 𝔖 (𝔗 i)
h_cover : ∀ S ∈ 𝔖, ∃ I, I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i)
ψ : (S : Set α) → (i : ι) → ↑(φ i ⁻¹' S) → ↑S := fun S i ↦ S.restrictPreimage (φ i)
this :
  ∀ S ∈ 𝔖,
    UniformFun.uniformSpace (↑S) β =
      ⨅ i, UniformSpace.comap (fun x ↦ x ∘ ψ S i) (UniformFun.uniformSpace (↑(φ i ⁻¹' S)) β)
i : ι
⊢ UniformContinuous (⇑(ofFun (𝔗 i)) ∘ (fun x ↦ x ∘ φ i) ∘ ⇑(toFun 𝔖))
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hF : ∀ (i : ι) (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
hg : UniformContinuous (s.domRestrict g)
h : TendstoUniformly F f p
⊢ TendstoUniformly (fun i x ↦ g (F i x)) (fun x ↦ g (f x)) p

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hF : ∀ (i : ι) (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
hg : UniformContinuous (s.domRestrict g)
h : TendstoUniformly F f p
⊢ TendstoUniformly (fun i x ↦ g (F i x)) (fun x ↦ g (f x)) p
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hg : UniformContinuous (s.domRestrict g)
F' : ι → α → ↑s
hF' : (fun i i_1 ↦ ↑(F' i i_1)) = F
f' : α → ↑s
hf' : (fun i ↦ ↑(f' i)) = f
comp_tendstoUniformly :
  (∀ (i : ι) (x : α), ↑(F' i x) ∈ s) →
    (∀ (x : α), ↑(f' x) ∈ s) →
      UniformContinuousOn g s →
        TendstoUniformly (fun i i_1 ↦ ↑(F' i i_1)) (fun i ↦ ↑(f' i)) p →
          TendstoUniformly (fun i x ↦ g ↑(F' i x)) (fun x ↦ g ↑(f' x)) p
h : Tendsto (fun q ↦ (↑(f' q.2), ↑(F' q.1 q.2))) (p ×ˢ ⊤) (𝓤 β)
⊢ TendstoUniformly (fun i x ↦ g ↑(F' i x)) (fun x ↦ g ↑(f' x)) p

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hg : UniformContinuous (s.domRestrict g)
F' : ι → α → ↑s
hF' : (fun i i_1 ↦ ↑(F' i i_1)) = F
f' : α → ↑s
hf' : (fun i ↦ ↑(f' i)) = f
comp_tendstoUniformly :
  (∀ (i : ι) (x : α), ↑(F' i x) ∈ s) →
    (∀ (x : α), ↑(f' x) ∈ s) →
      UniformContinuousOn g s →
        TendstoUniformly (fun i i_1 ↦ ↑(F' i i_1)) (fun i ↦ ↑(f' i)) p →
          TendstoUniformly (fun i x ↦ g ↑(F' i x)) (fun x ↦ g ↑(f' x)) p
h : Tendsto (fun q ↦ (↑(f' q.2), ↑(F' q.1 q.2))) (p ×ˢ ⊤) (𝓤 β)
⊢ TendstoUniformly (fun i x ↦ g ↑(F' i x)) (fun x ↦ g ↑(f' x)) p
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hg : UniformContinuous (s.domRestrict g)
F' : ι → α → ↑s
hF' : (fun i i_1 ↦ ↑(F' i i_1)) = F
f' : α → ↑s
hf' : (fun i ↦ ↑(f' i)) = f
comp_tendstoUniformly :
  (∀ (i : ι) (x : α), ↑(F' i x) ∈ s) →
    (∀ (x : α), ↑(f' x) ∈ s) →
      UniformContinuousOn g s →
        TendstoUniformly (fun i i_1 ↦ ↑(F' i i_1)) (fun i ↦ ↑(f' i)) p →
          TendstoUniformly (fun i x ↦ g ↑(F' i x)) (fun x ↦ g ↑(f' x)) p
h : Tendsto (fun q ↦ (↑(f' q.2), ↑(F' q.1 q.2))) (p ×ˢ ⊤) (𝓤 β)
this : TendstoUniformly F' f' p
⊢ TendstoUniformly F' f' p

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hg : UniformContinuous (s.domRestrict g)
F' : ι → α → ↑s
hF' : (fun i i_1 ↦ ↑(F' i i_1)) = F
f' : α → ↑s
hf' : (fun i ↦ ↑(f' i)) = f
comp_tendstoUniformly :
  (∀ (i : ι) (x : α), ↑(F' i x) ∈ s) →
    (∀ (x : α), ↑(f' x) ∈ s) →
      UniformContinuousOn g s →
        TendstoUniformly (fun i i_1 ↦ ↑(F' i i_1)) (fun i ↦ ↑(f' i)) p →
          TendstoUniformly (fun i x ↦ g ↑(F' i x)) (fun x ↦ g ↑(f' x)) p
h : Tendsto (fun q ↦ (↑(f' q.2), ↑(F' q.1 q.2))) (p ×ˢ ⊤) (𝓤 β)
this : TendstoUniformly F' f' p
⊢ TendstoUniformly F' f' p
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hF : ∀ᶠ (i : ι) in p, ∀ (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
hg : UniformContinuousOn g s
h : TendstoUniformly F f p
s' : Set ι
hs' : s' ∈ p
hs : ∀ y ∈ s', ∀ (x : α), F y x ∈ s
F' : ι → α → β := fun i x ↦ if i ∈ s' then F i x else f x
⊢ ∃ s ∈ p, EqOn F F' s

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hF : ∀ᶠ (i : ι) in p, ∀ (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
hg : UniformContinuousOn g s
h : TendstoUniformly F f p
s' : Set ι
hs' : s' ∈ p
hs : ∀ y ∈ s', ∀ (x : α), F y x ∈ s
F' : ι → α → β := fun i x ↦ if i ∈ s' then F i x else f x
⊢ ∃ s ∈ p, EqOn F F' s
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hF✝ : ∀ᶠ (i : ι) in p, ∀ (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
hg : UniformContinuousOn g s
s' : Set ι
hs' : s' ∈ p
hs : ∀ y ∈ s', ∀ (x : α), F y x ∈ s
F' : ι → α → β := fun i x ↦ if i ∈ s' then F i x else f x
h : TendstoUniformly F' f p
hF : F =ᶠ[p] F'
⊢ TendstoUniformly F' f p

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hF✝ : ∀ᶠ (i : ι) in p, ∀ (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
hg : UniformContinuousOn g s
s' : Set ι
hs' : s' ∈ p
hs : ∀ y ∈ s', ∀ (x : α), F y x ∈ s
F' : ι → α → β := fun i x ↦ if i ∈ s' then F i x else f x
h : TendstoUniformly F' f p
hF : F =ᶠ[p] F'
⊢ TendstoUniformly F' f p
Module: Mathlib.Topology.Algebra.ConstMulAction

Goal state before:
pp: α : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : ContinuousConstSMul G α
c : G
s : Set α
hs : closure[inst✝³] s = univ
⊢ closure[inst✝³] (c • s) = univ

Tactic:
]

Goal state after:
α : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : ContinuousConstSMul G α
c : G
s : Set α
hs : closure[inst✝³] s = univ
⊢ closure[inst✝³] (c • s) = univ
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hF✝ : ∀ᶠ (i : ι) in p, ∀ (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
hg : UniformContinuousOn g s
h : TendstoUniformly F f p
s' : Set ι
hs' : s' ∈ p
hs : ∀ y ∈ s', ∀ (x : α), F y x ∈ s
F' : ι → α → β := fun i x ↦ if i ∈ s' then F i x else f x
hF : F =ᶠ[p] F'
h' : TendstoUniformly F' f p
⊢ ∃ s ∈ p, EqOn (fun i x ↦ g (F i x)) (fun i x ↦ g (F' i x)) s

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hF✝ : ∀ᶠ (i : ι) in p, ∀ (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
hg : UniformContinuousOn g s
h : TendstoUniformly F f p
s' : Set ι
hs' : s' ∈ p
hs : ∀ y ∈ s', ∀ (x : α), F y x ∈ s
F' : ι → α → β := fun i x ↦ if i ∈ s' then F i x else f x
hF : F =ᶠ[p] F'
h' : TendstoUniformly F' f p
⊢ ∃ s ∈ p, EqOn (fun i x ↦ g (F i x)) (fun i x ↦ g (F' i x)) s
Module: Mathlib.Topology.Algebra.ConstMulAction

Goal state before:
pp: α : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : ContinuousConstSMul G α
c : G
s : Set α
hs : closure[inst✝³] s = univ
⊢ univ = univ

Tactic:
]

Goal state after: