mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
T : TopologicalSpace X
S : Set (Set X)
hTS : T = generateFrom S
s : Set X
h : ∀ P ⊆ S, s ⊆ ⋃₀ P → ∃ Q ⊆ P, Q.Finite ∧ s ⊆ ⋃₀ Q
⊢ ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x

Tactic:
intro F

Goal state after:
X : Type u
T : TopologicalSpace X
S : Set (Set X)
hTS : T = generateFrom S
s : Set X
h : ∀ P ⊆ S, s ⊆ ⋃₀ P → ∃ Q ⊆ P, Q.Finite ∧ s ⊆ ⋃₀ Q
F : Ultrafilter X
⊢ s ∈ F → ∃ x ∈ s, ↑F ≤ 𝓝 x
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ ↑s
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
a : α
ha : a ∈ (⇑toDual ∘ SetLike.coe) s
⊢ a ∈ (⇑toDual ∘ SetLike.coe) (s.sdiff t ⊓ upperClosure t)

Tactic:
obtain hat | hat := em (a ∈ t)

Goal state after:
case inl
α : Type u_1
inst✝ : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ ↑s
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
a : α
ha : a ∈ (⇑toDual ∘ SetLike.coe) s
hat : a ∈ t
⊢ a ∈ (⇑toDual ∘ SetLike.coe) (s.sdiff t ⊓ upperClosure t)

case inr
α : Type u_1
inst✝ : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ ↑s
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
a : α
ha : a ∈ (⇑toDual ∘ SetLike.coe) s
hat : a ∉ t
⊢ a ∈ (⇑toDual ∘ SetLike.coe) (s.sdiff t ⊓ upperClosure t)
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s s' : Set X
hs : IsCompact s
t : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : n ∈ 𝓝ˢ[s' ×ˢ t] (s ×ˢ t)
⊢ ∃ u ∈ 𝓝ˢ[s'] s, u ×ˢ t ⊆ n

Tactic:
by
  rw [hs.nhdsSetWithin_prod_eq ht, nhdsSetWithin_self, Filter.mem_prod_principal] at hn
  exact ⟨_, hn, fun x hx ↦ hx.1 _ hx.2⟩

Goal state after:
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ a ∈ frontier {x | p x}, Tendsto f (𝓝[{x | p x}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ frontier {x | p x}, Tendsto g (𝓝[{x | ¬p x}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f {x | p x}
hg : ContinuousOn g {x | ¬p x}
⊢ Continuous[inst✝², inst✝¹] fun a ↦ if p a then f a else g a

Tactic:
rw [← continuousOn_univ]

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ a ∈ frontier {x | p x}, Tendsto f (𝓝[{x | p x}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ frontier {x | p x}, Tendsto g (𝓝[{x | ¬p x}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f {x | p x}
hg : ContinuousOn g {x | ¬p x}
⊢ ContinuousOn (fun a ↦ if p a then f a else g a) univ
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hp : ∀ a ∈ frontier {x | p x}, f a = g a
hf : ContinuousOn f (closure[inst✝²] {x | p x})
hg : ContinuousOn g (closure[inst✝²] {x | ¬p x})
⊢ Continuous[inst✝², inst✝¹] fun a ↦ if p a then f a else g a

Tactic:
rw [← continuousOn_univ]

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hp : ∀ a ∈ frontier {x | p x}, f a = g a
hf : ContinuousOn f (closure[inst✝²] {x | p x})
hg : ContinuousOn g (closure[inst✝²] {x | ¬p x})
⊢ ContinuousOn (fun a ↦ if p a then f a else g a) univ
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y → α
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
x : X
y : Y
l : Filter α
⊢ Tendsto (uncurry (lift₂ f hf)) (𝓝 (mk x, mk y)) l ↔ Tendsto (uncurry f) (𝓝 (x, y)) l

Tactic:
by
  rw [← map_prod_map_mk_nhds, tendsto_map'_iff]
  rfl

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Set X
hfin : s.Finite
hne : s.Nonempty
ho : IsOpen[inst✝¹] s
⊢ ∃ x ∈ s, IsOpen[inst✝¹] {x}

Tactic:
by
  lift s to Finset X using hfin
  induction s using Finset.strongInductionOn
  rename_i s ihs
  rcases em (∃ t, t ⊂ s ∧ t.Nonempty ∧ IsOpen (t : Set X)) with (⟨t, hts, htne, hto⟩ | ht)
  · rcases ihs t hts htne hto with ⟨x, hxt, hxo⟩
    exact ⟨x, hts.1 hxt, hxo⟩
  · -- Porting note: was `rcases minimal_nonempty_open_eq_singleton ho hne _ with ⟨x, hx⟩`
    --               https://github.com/leanprover-community/batteries/issues/116
    rsuffices ⟨x, hx⟩ : ∃ x, (s : Set X) = {x}
    · exact ⟨x, hx.symm ▸ rfl, hx ▸ ho⟩
    refine minimal_nonempty_open_eq_singleton ho hne ?_
    refine fun t hts htne hto => of_not_not fun hts' => ht ?_
    lift t to Finset X using s.finite_toSet.subset hts
    exact ⟨t, ssubset_iff_subset_ne.2 ⟨hts, mt Finset.coe_inj.2 hts'⟩, htne, hto⟩

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace Y
f : X → Y
⊢ (∀ (i : Set Y), IsCompact i → ∀ᶠ (x : X) in cofinite, f x ∈ iᶜ) ↔ ∀ (K : Set Y), IsCompact K → (f ⁻¹' K).Finite

Tactic:
refine forall₂_congr (fun K _ ↦ ?_)

Goal state after:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace Y
f : X → Y
K : Set Y
x✝ : IsCompact K
⊢ (∀ᶠ (x : X) in cofinite, f x ∈ Kᶜ) ↔ (f ⁻¹' K).Finite
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case neg
X : Type u_1
inst✝ : TopologicalSpace X
s U : Set X
hs : s ∈ codiscreteWithin U
hU : IsClosed[inst✝] U
x : X
hx : x ∈ (U \ s)ᶜ
h₁x : x ∉ U
⊢ ∀ᶠ (y : X) in 𝓝 x, y ∈ (U \ s)ᶜ

Tactic:
rw [eventually_iff_exists_mem]

Goal state after:
case neg
X : Type u_1
inst✝ : TopologicalSpace X
s U : Set X
hs : s ∈ codiscreteWithin U
hU : IsClosed[inst✝] U
x : X
hx : x ∈ (U \ s)ᶜ
h₁x : x ∉ U
⊢ ∃ v ∈ 𝓝 x, ∀ y ∈ v, y ∈ (U \ s)ᶜ
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s U : Set X
⊢ s ∈ codiscreteWithin U ↔ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ s)).Finite

Tactic:
rw [codiscreteWithin_iff_locallyEmptyComplementWithin]

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s U : Set X
⊢ (∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅) ↔ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ s)).Finite
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: ι : Type u_4
X : ι → Type u_5
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), R1Space (X i)
s : Set ((i : ι) → X i)
⊢ IsCompact (closure[topologicalSpace] s) ↔ ∀ (i : ι), IsCompact (closure[inst✝¹ i] (eval i '' s))

Tactic:
by
  simp_rw [← exists_isCompact_superset_iff, Pi.exists_compact_superset_iff, image_subset_iff]

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
h : t.Subsingleton
⊢ s ∈ codiscreteWithin t

Tactic:
rw [codiscreteWithin_iff_locallyEmptyComplementWithin]

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
h : t.Subsingleton
⊢ ∀ z ∈ t, ∃ t_1 ∈ 𝓝[≠] z, t_1 ∩ (t \ s) = ∅
Module: Mathlib.Topology.Order.LeftRight

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ∀ (x : α), (𝓝[<] x).NeBot
s : Set α
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s
⊢ interior s = ∅

Tactic:
by
  refine eq_empty_of_forall_notMem fun x hx ↦ ?_
  have : ∀ᶠ y in 𝓝 x, y ∈ s := mem_interior_iff_mem_nhds.1 hx
  rcases this.exists_lt with ⟨y, hyx, hys⟩
  exact hs hys (interior_subset hx) hyx.ne hyx.le

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s : Set X
x : X
⊢ {x}ᶜ ∈ codiscreteWithin s

Tactic:
rw [codiscreteWithin_iff_locallyEmptyComplementWithin]

Goal state after:
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s : Set X
x : X
⊢ ∀ z ∈ s, ∃ t ∈ 𝓝[≠] z, t ∩ (s \ {x}ᶜ) = ∅
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: α : Type u
ι : Type u_1
F : Filter ι
inst✝³ : F.NeBot
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
a : α
f : ι → α
hlt : ∀ (i : ι), f i < a
hlim : Tendsto f F (𝓝 a)
⊢ ⋃ i, Iic (f i) = Iio a

Tactic:
have obs : a ∉ range f := by
    rw [mem_range]
    rintro ⟨i, rfl⟩
    exact (hlt i).false

Goal state after:
α : Type u
ι : Type u_1
F : Filter ι
inst✝³ : F.NeBot
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
a : α
f : ι → α
hlt : ∀ (i : ι), f i < a
hlim : Tendsto f F (𝓝 a)
obs : a ∉ range f
⊢ ⋃ i, Iic (f i) = Iio a
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝ : CountableInterFilter l✝
l : Set (Set α)
hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
⊢ Filter α

Tactic:
refine .ofCountableInter {s | sᶜ ∈ l} (fun S hSc hSp ↦ ?_) fun s t ht hsub ↦ ?_
  · rw [mem_ofPred_eq, compl_sInter]
    apply hUnion (compl '' S) (hSc.image _)
    intro s hs
    rw [mem_image] at hs
    rcases hs with ⟨t, ht, rfl⟩
    apply hSp ht
  · rw [mem_ofPred_eq]
    rw [← compl_subset_compl] at hsub
    exact hmono sᶜ ht tᶜ hsub

Goal state after:
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_1
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) × X i)
hs : IsConnected s
⊢ ∃ i t, IsConnected t ∧ s = mk i '' t

Tactic:
obtain ⟨⟨i, x⟩, hx⟩ := hs.nonempty

Goal state after:
case refine_1
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) × X i)
hs : IsConnected s
i : ι
x : X i
hx : ⟨i, x⟩ ∈ s
⊢ ∃ i t, IsConnected t ∧ s = mk i '' t
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : IsPreconnected s
t t' : Set α
ht : IsClosed[inst✝] t
ht' : IsClosed[inst✝] t'
htt' : s ⊆ t ∪ t'
x : α
xs : x ∈ s
xt : x ∈ t
y : α
ys : y ∈ s
yt' : y ∈ t'
⊢ (s ∩ (t ∩ t')).Nonempty

Tactic:
rw [← not_disjoint_iff_nonempty_inter, ← subset_compl_iff_disjoint_right, compl_inter]

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : IsPreconnected s
t t' : Set α
ht : IsClosed[inst✝] t
ht' : IsClosed[inst✝] t'
htt' : s ⊆ t ∪ t'
x : α
xs : x ∈ s
xt : x ∈ t
y : α
ys : y ∈ s
yt' : y ∈ t'
⊢ ¬s ⊆ tᶜ ∪ t'ᶜ
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
h :
  ∀ (t t' : Set α),
    IsClosed[inst✝] t → IsClosed[inst✝] t' → s ⊆ t ∪ t' → (s ∩ t).Nonempty → (s ∩ t').Nonempty → (s ∩ (t ∩ t')).Nonempty
u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
huv : s ⊆ u ∪ v
x : α
xs : x ∈ s
xu : x ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
rw [← not_disjoint_iff_nonempty_inter, ← subset_compl_iff_disjoint_right, compl_inter]

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h :
  ∀ (t t' : Set α),
    IsClosed[inst✝] t → IsClosed[inst✝] t' → s ⊆ t ∪ t' → (s ∩ t).Nonempty → (s ∩ t').Nonempty → (s ∩ (t ∩ t')).Nonempty
u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
huv : s ⊆ u ∪ v
x : α
xs : x ∈ s
xu : x ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
⊢ ¬s ⊆ uᶜ ∪ vᶜ
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : LocallyCompactSpace X
inst✝ : RegularSpace X
K : Set X
hK : IsCompact K
U : Set X
hU : IsOpen[inst✝²] U
h_KU : K ⊆ U
L : Set X
hL : IsCompact L
hL' : IsClosed[inst✝²] L
hKL : K ⊆ interior L
hLU : L ⊆ U
⊢ ∃ r ∈ 𝓝ˢ K, (IsCompact r ∧ IsClosed[inst✝²] r) ∧ r ⊆ U

Tactic:
exact ⟨L, by rwa [← subset_interior_iff_mem_nhdsSet], ⟨hL, hL'⟩, hLU⟩

Goal state after:
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompletelyNormalSpace Y
e : X → Y
he : IsInducing e
⊢ CompletelyNormalSpace X

Tactic:
refine ⟨fun s t hd₁ hd₂ => ?_⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompletelyNormalSpace Y
e : X → Y
he : IsInducing e
s t : Set X
hd₁ : Disjoint (closure[inst✝²] s) t
hd₂ : Disjoint s (closure[inst✝²] t)
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsLindelof t
b : Bool
⊢ IsLindelof (bif b then s else t)

Tactic:
cases b <;> assumption

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
l : Filter α
hl : l.NeBot
⊢ Cauchy l ↔ l ×ˢ l ≤ 𝓤 α

Tactic:
simp only [Cauchy, hl, true_and]

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

Goal state before:
pp: α : Type ua
β : Type ub
inst✝ : UniformSpace α
g : SetRel α α → Filter β
f : Filter β
hg : Monotone g
h : ((𝓤 α).lift fun s ↦ g (Prod.swap ⁻¹' s)) ≤ f
⊢ (map Prod.swap (𝓤 α)).lift g ≤ f

Tactic:
rw [map_lift_eq2 hg, image_swap_eq_preimage_swap]

Goal state after:
α : Type ua
β : Type ub
inst✝ : UniformSpace α
g : SetRel α α → Filter β
f : Filter β
hg : Monotone g
h : ((𝓤 α).lift fun s ↦ g (Prod.swap ⁻¹' s)) ≤ f
⊢ (𝓤 α).lift (g ∘ preimage Prod.swap) ≤ f
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : SetRel α β
hs : IsOpen[instTopologicalSpaceProd] s
t : Set α
⊢ IsOpen[inst✝] {b | ∃ a, ∃ (_ : a ∈ t), (a, b) ∈ s}

Tactic:
Set.ofPred_exists

Goal state after:
α : Type ua
β : Type ub
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : SetRel α β
hs : IsOpen[instTopologicalSpaceProd] s
t : Set α
⊢ IsOpen[inst✝] (⋃ i ∈ t, {x | (i, x) ∈ s})
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : SetRel α β
hs : IsClosed[instTopologicalSpaceProd] s
t : Set α
ht : t.Finite
⊢ IsClosed[inst✝] {b | ∃ a, ∃ (_ : a ∈ t), (a, b) ∈ s}

Tactic:
Set.ofPred_exists

Goal state after:
α : Type ua
β : Type ub
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : SetRel α β
hs : IsClosed[instTopologicalSpaceProd] s
t : Set α
ht : t.Finite
⊢ IsClosed[inst✝] (⋃ i ∈ t, {x | (i, x) ∈ s})
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f g : α → β
s : Set α
hf : UniformContinuousOn f s
h : EqOn f g s
⊢ UniformContinuousOn g s

Tactic:
apply hf.congr'

Goal state after:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f g : α → β
s : Set α
hf : UniformContinuousOn f s
h : EqOn f g s
⊢ (fun x ↦ (f x.1, f x.2)) =ᶠ[𝓤 α ⊓ 𝓟 (s ×ˢ s)] fun x ↦ (g x.1, g x.2)
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
a : α
s : Set α
⊢ TotallyBounded (insert a s) ↔ TotallyBounded s

Tactic:
simp_rw [← singleton_union, totallyBounded_union, totallyBounded_singleton, true_and]

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

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
⊢ comap (fun x ↦ (_root_.id x.1, _root_.id x.2)) (𝓤 α) = 𝓤 α

Tactic:
rw [← Prod.map_def, Prod.map_id, comap_id]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
g : β → γ
hg : IsUniformInducing g
f : α → β
⊢ IsUniformInducing (g ∘ f) ↔ IsUniformInducing f

Tactic:
refine ⟨fun h ↦ ?_, hg.comp⟩

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
g : β → γ
hg : IsUniformInducing g
f : α → β
h : IsUniformInducing (g ∘ f)
⊢ IsUniformInducing f
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → SetRel α α
H : (𝓤 α).HasBasis p U
xs : ℕ → α
u : ℕ → ℕ
i : ℕ
a✝ : p i
h_subset : interUnionBalls xs u U ⊆ ⋃ m, ⋃ (_ : m ≤ u i), ball (xs m) (Prod.swap ⁻¹' U i)
x : α
hx : x ∈ interUnionBalls xs u U
⊢ x ∈ ⋃ y ∈ ↑(Finset.image xs (Finset.range (u i + 1))), {x | (x, y) ∈ U i}

Tactic:
simp only [Finset.coe_image, Finset.coe_range, mem_image, mem_Iio, iUnion_exists, biUnion_and',
    iUnion_iUnion_eq_right, Nat.lt_succ_iff]

Goal state after:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → SetRel α α
H : (𝓤 α).HasBasis p U
xs : ℕ → α
u : ℕ → ℕ
i : ℕ
a✝ : p i
h_subset : interUnionBalls xs u U ⊆ ⋃ m, ⋃ (_ : m ≤ u i), ball (xs m) (Prod.swap ⁻¹' U i)
x : α
hx : x ∈ interUnionBalls xs u U
⊢ x ∈ ⋃ y, ⋃ (_ : y ≤ u i), {x | (x, xs y) ∈ U i}
Module: Mathlib.Topology.UniformSpace.Compact

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
A B : Set α
hA : IsCompact A
hB : IsClosed[inst✝.toTopologicalSpace] B
h : Disjoint A B
⊢ ∃ V ∈ 𝓤 α, Disjoint (⋃ x ∈ A, ball x V) (⋃ x ∈ B, ball x V)

Tactic:
have : Bᶜ ∈ 𝓝ˢ A := hB.isOpen_compl.mem_nhdsSet.mpr h.le_compl_right
  rw [(hA.nhdsSet_basis_uniformity (Filter.basis_sets _)).mem_iff] at this
  rcases this with ⟨U, hU, hUAB⟩
  rcases comp_symm_mem_uniformity_sets hU with ⟨V, hV, hVsymm, hVU⟩
  refine ⟨V, hV, Set.disjoint_left.mpr fun x => ?_⟩
  simp only [mem_iUnion₂]
  rintro ⟨a, ha, hxa⟩ ⟨b, hb, hxb⟩
  rw [mem_ball_symmetry] at hxa hxb
  exact hUAB (mem_iUnion₂_of_mem ha <| hVU <| mem_comp_of_mem_ball hxa hxb) hb

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

Goal state before:
pp: γ : Type uc
t : TopologicalSpace γ
inst✝ : CompactSpace γ
u u' : UniformSpace γ
h : u.toTopologicalSpace = t
h' : u'.toTopologicalSpace = t
this✝ : CompactSpace γ
this : CompactSpace γ
⊢ ⨆ x, 𝓝 (x, x) = 𝓤 γ

Tactic:
compactSpace_uniformity,

Goal state after:
γ : Type uc
t : TopologicalSpace γ
inst✝ : CompactSpace γ
u u' : UniformSpace γ
h : u.toTopologicalSpace = t
h' : u'.toTopologicalSpace = t
this✝ : CompactSpace γ
this : CompactSpace γ
⊢ ⨆ x, 𝓝 (x, x) = ⨆ x, 𝓝 (x, x)
Module: Mathlib.Topology.UniformSpace.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst✝ : Nonempty ι
l : (i : ι) → Filter (α i)
hl : ∀ (i : ι), Cauchy (l i)
⊢ Cauchy (Filter.pi l)

Tactic:
have := fun i ↦ (hl i).1
  simpa [cauchy_pi_iff]

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

Goal state before:
pp: α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
f : α ≃ᵤ β
g : β → α
hg : Function.RightInverse g ⇑f
this : g = ⇑f.symm
⊢ UniformContinuous g

Tactic:
convert! f.symm.uniformContinuous

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

Goal state before:
pp: α : Type u
β✝ : Type u_1
γ : Type u_2
δ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β✝
inst✝² : UniformSpace γ
inst✝¹ : UniformSpace δ
ι : Type u_4
ι' : Type u_5
β : ι' → Type u_6
inst✝ : (j : ι') → UniformSpace (β j)
e : ι ≃ ι'
i : ι
⊢ UniformContinuous fun x ↦ (Equiv.piCongrLeft β e).toFun x (e i)

Tactic:
simpa only [Equiv.toFun_as_coe, Equiv.piCongrLeft_apply_apply] using
      Pi.uniformContinuous_proj _ i

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
⊢ TendstoLocallyUniformlyOn F f p s ↔ ∀ x ∈ s, TendstoUniformlyOnFilter F f p (𝓝[s] x)

Tactic:
by
  simp only [TendstoUniformlyOnFilter, eventually_prod_iff]
  constructor
  · rintro h x hx u hu
    obtain ⟨s, hs1, hs2⟩ := h u hu x hx
    exact ⟨_, hs2, _, eventually_of_mem hs1 fun x => id, fun hi y hy => hi y hy⟩
  · rintro h u hu x hx
    obtain ⟨pa, hpa, pb, hpb, h⟩ := h x hx u hu
    exact ⟨{a | pb a}, hpb, eventually_of_mem hpa fun i hi y hy => h hi hy⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
x : α
⊢ map (fun x_1 ↦ ((Function.eval x ∘ ⇑toFun) x_1.1, (Function.eval x ∘ ⇑toFun) x_1.2)) (𝓤 (α →ᵤ β)) ≤ 𝓤 β

Tactic:
rw [map_le_iff_le_comap,
    (UniformFun.hasBasis_uniformity α β).le_basis_iff ((𝓤 _).basis_sets.comap _)]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
x : α
⊢ ∀ i' ∈ 𝓤 β,
    ∃ i ∈ 𝓤 β,
      UniformFun.gen α β i ⊆ (fun x_1 ↦ ((Function.eval x ∘ ⇑toFun) x_1.1, (Function.eval x ∘ ⇑toFun) x_1.2)) ⁻¹' id i'
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : Preorder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b c d : α
⊢ Icc a b * Icc c d ⊆ Icc (a * c) (b * d)

Tactic:
rintro x ⟨y, ⟨hya, hyb⟩, z, ⟨hzc, hzd⟩, rfl⟩

Goal state after:
α : Type u_1
inst✝³ : Mul α
inst✝² : Preorder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b c d y : α
hya : a ≤ y
hyb : y ≤ b
z : α
hzc : c ≤ z
hzd : z ≤ d
⊢ (fun x1 x2 ↦ x1 * x2) y z ∈ Icc (a * c) (b * d)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
this✝ : MulLeftMono α
this : MulRightMono α
⊢ Icc a b * Ico c d ⊆ Ico (a * c) (b * d)

Tactic:
rintro x ⟨y, ⟨hya, hyb⟩, z, ⟨hzc, hzd⟩, rfl⟩

Goal state after:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
this✝ : MulLeftMono α
this : MulRightMono α
y : α
hya : a ≤ y
hyb : y ≤ b
z : α
hzc : c ≤ z
hzd : z < d
⊢ (fun x1 x2 ↦ x1 * x2) y z ∈ Ico (a * c) (b * d)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
this✝ : MulLeftMono α
this : MulRightMono α
⊢ Ico a b * Icc c d ⊆ Ico (a * c) (b * d)

Tactic:
rintro x ⟨y, ⟨hya, hyb⟩, z, ⟨hzc, hzd⟩, rfl⟩

Goal state after:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
this✝ : MulLeftMono α
this : MulRightMono α
y : α
hya : a ≤ y
hyb : y < b
z : α
hzc : c ≤ z
hzd : z ≤ d
⊢ (fun x1 x2 ↦ x1 * x2) y z ∈ Ico (a * c) (b * d)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
this✝ : MulLeftMono α
this : MulRightMono α
⊢ Ioc a b * Ico c d ⊆ Ioo (a * c) (b * d)

Tactic:
rintro x ⟨y, ⟨hya, hyb⟩, z, ⟨hzc, hzd⟩, rfl⟩

Goal state after:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
this✝ : MulLeftMono α
this : MulRightMono α
y : α
hya : a < y
hyb : y ≤ b
z : α
hzc : c ≤ z
hzd : z < d
⊢ (fun x1 x2 ↦ x1 * x2) y z ∈ Ioo (a * c) (b * d)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
this✝ : MulLeftMono α
this : MulRightMono α
⊢ Ico a b * Ioc c d ⊆ Ioo (a * c) (b * d)

Tactic:
rintro x ⟨y, ⟨hya, hyb⟩, z, ⟨hzc, hzd⟩, rfl⟩

Goal state after:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
this✝ : MulLeftMono α
this : MulRightMono α
y : α
hya : a ≤ y
hyb : y < b
z : α
hzc : c < z
hzd : z ≤ d
⊢ (fun x1 x2 ↦ x1 * x2) y z ∈ Ioo (a * c) (b * d)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: case mpr
α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c x : α
⊢ x ∈ Icc (a * b) (a * c) → x ∈ a • Icc b c

Tactic:
rintro ⟨habx, hxac⟩
    obtain ⟨y, hy, rfl⟩ := exists_one_le_mul_of_le habx
    refine ⟨b * y, ⟨le_mul_of_one_le_right' hy, ?_⟩, (mul_assoc ..).symm⟩
    rwa [mul_assoc, mul_le_mul_iff_left] at hxac

Goal state after:
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
b : Bool
⊢ ContinuousSMul M X

Tactic:
cases b <;> assumption

Goal state after: