mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Connected.LocallyConnected

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), LocallyConnectedSpace (X i)
hfinite : {i | ¬PreconnectedSpace (X i)}.Finite
x : (i : ι) → X i
U : Set ((i : ι) → X i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htU : J.pi t ⊆ U
K : Set ι := J ∪ {i | ¬PreconnectedSpace (X i)}
⊢ IsPreconnected (K.pi fun i ↦ connectedComponentIn (t i) (x i))

Tactic:
classical
  rw [← univ_pi_piecewise_univ]
  refine isPreconnected_univ_pi fun i ↦ ?_
  by_cases hi : i ∈ K
  · rw [piecewise_eq_of_mem _ _ _ hi]
    exact isPreconnected_connectedComponentIn
  · rw [piecewise_eq_of_notMem _ _ _ hi]
    have : PreconnectedSpace (X i) := not_not.mp (not_or.1 hi).2
    exact isPreconnected_univ

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

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
P : α → α → Prop
h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y ∧ P y x
h' : IsTrans α P
x y : α
u : Set α := {z | P x z}
A : IsClosed[inst✝¹] u
⊢ IsOpen[inst✝¹] u

Tactic:
apply isOpen_iff_mem_nhds.2 (fun z hz ↦ ?_)

Goal state after:
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
P : α → α → Prop
h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y ∧ P y x
h' : IsTrans α P
x y : α
u : Set α := {z | P x z}
A : IsClosed[inst✝¹] u
z : α
hz : z ∈ u
⊢ u ∈ 𝓝 z
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : LocallyCompactSpace X
inst✝ : RegularSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
L : Set X
L_compact : IsCompact L
L_closed : IsClosed[inst✝²] L
KL : K ⊆ interior L
LU : L ⊆ U
A : closure[inst✝²] (interior L) ⊆ L
⊢ IsCompact (closure[inst✝²] (interior L))

Tactic:
exact L_compact.closure_of_subset interior_subset

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
x : α
F : Set α
hx : x ∈ F
⊢ x ∈ connectedComponentIn F x

Tactic:
simp [connectedComponentIn_eq_image hx, mem_connectedComponent, hx]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
s : Set (SeparationQuotient X)
hs : IsClosed s
a : X
ha : SeparationQuotient.mk a ∉ s
⊢ Disjoint (comap SeparationQuotient.mk (𝓝ˢ s)) (comap SeparationQuotient.mk (𝓝 (SeparationQuotient.mk a)))

Tactic:
comap_mk_nhds_mk,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
s : Set (SeparationQuotient X)
hs : IsClosed s
a : X
ha : SeparationQuotient.mk a ∉ s
⊢ Disjoint (comap SeparationQuotient.mk (𝓝ˢ s)) (𝓝 a)
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: case mp.refine_2
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f' : Y → ι
h₁ : IsLindelof (⋃ i, (b ∘ f') i)
h₂ : IsOpen[inst✝] (⋃ i, (b ∘ f') i)
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Set Y
ht : t.Countable ∧ ⋃ i, (b ∘ f') i ⊆ ⋃ i ∈ t, (b ∘ f') i
i : ι
hi : i ∈ f' '' t
⊢ b i ⊆ ⋃ i, (b ∘ f') i

Tactic:
obtain ⟨j, -, rfl⟩ := (mem_image ..).mp hi

Goal state after:
case mp.refine_2
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f' : Y → ι
h₁ : IsLindelof (⋃ i, (b ∘ f') i)
h₂ : IsOpen[inst✝] (⋃ i, (b ∘ f') i)
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Set Y
ht : t.Countable ∧ ⋃ i, (b ∘ f') i ⊆ ⋃ i ∈ t, (b ∘ f') i
j : Y
hi : f' j ∈ f' '' t
⊢ b (f' j) ⊆ ⋃ i, (b ∘ f') i
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
hf' : IsClosed[inst✝] (range f)
K : Set Y
hK : IsLindelof K
⊢ IsLindelof (f ⁻¹' K)

Tactic:
replace hK := hK.inter_right hf'

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
hf' : IsClosed[inst✝] (range f)
K : Set Y
hK : IsLindelof (K ∩ range f)
⊢ IsLindelof (f ⁻¹' K)
Module: Mathlib.Topology.Connected.TotallyDisconnected

Goal state before:
pp: case mpr
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), (connectedComponent x).Subsingleton
s : Set α
⊢ s ⊆ univ → IsPreconnected s → s.Subsingleton

Tactic:
s_sub

Goal state after:
case mpr
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), (connectedComponent x).Subsingleton
s : Set α
s_sub : s ⊆ univ
⊢ IsPreconnected s → s.Subsingleton
Module: Mathlib.Topology.Connected.TotallyDisconnected

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : IsEmbedding f
hs : IsTotallyDisconnected s
u : Set β
hus : u ⊆ f '' s
hu : IsPreconnected u
⊢ u ∩ f '' s = u

Tactic:
inter_eq_left

Goal state after:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : IsEmbedding f
hs : IsTotallyDisconnected s
u : Set β
hus : u ⊆ f '' s
hu : IsPreconnected u
⊢ u ⊆ f '' s
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
W : Type u_3
Z : Type u_4
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace W
inst✝² : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst✝¹ : TopologicalSpace X'
inst✝ : TopologicalSpace Y'
ι : Type u_7
ι' : Type u_8
i✝ : ι ⊕ ι'
i : ι'
⊢ Continuous[instTopologicalSpaceProd, inst✝⁵] fun a ↦ (Equiv.sumArrowEquivProdArrow ι ι' X).invFun a (Sum.inr i)

Tactic:
by apply (continuous_apply _).comp' continuous_snd

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

Goal state before:
pp: β : Type v
ι : Sort u_1
u : ι → UniformSpace β
l : Filter β
inst✝ : l.NeBot
⊢ l ×ˢ l ≤ ⨅ i, 𝓤 β ↔ ∀ (i : ι), l ×ˢ l ≤ 𝓤 β

Tactic:
le_iInf_iff

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
⊢ (CauchySeq fun n ↦ u (n + k)) ↔ CauchySeq u

Tactic:
by
  constructor <;> intro h
  · rw [cauchySeq_iff] at h ⊢
    intro V mV
    obtain ⟨N, h⟩ := h V mV
    use N + k
    intro a ha b hb
    convert! h (a - k) (Nat.le_sub_of_add_le ha) (b - k) (Nat.le_sub_of_add_le hb) <;> lia
  · exact h.comp_tendsto (tendsto_add_atTop_nat k)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
h : TendstoUniformlyOnFilter F f p p'
g : γ → α
⊢ TendstoUniformlyOnFilter (fun n ↦ F n ∘ g) (f ∘ g) p (comap g p')

Tactic:
rw [tendstoUniformlyOnFilter_iff_tendsto] at h ⊢

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
h : Tendsto (fun q ↦ (f q.2, F q.1 q.2)) (p ×ˢ p') (𝓤 β)
g : γ → α
⊢ Tendsto (fun q ↦ ((f ∘ g) q.2, (F q.1 ∘ g) q.2)) (p ×ˢ comap g p') (𝓤 β)
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst✝ : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
q : Filter ι'
q' : Filter α'
h : TendstoUniformlyOnFilter F f p p'
h' : TendstoUniformlyOnFilter F' f' q q'
⊢ TendstoUniformlyOnFilter (fun i ↦ Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ q) (p' ×ˢ q')

Tactic:
rw [tendstoUniformlyOnFilter_iff_tendsto] at h h' ⊢

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst✝ : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
q : Filter ι'
q' : Filter α'
h : Tendsto (fun q ↦ (f q.2, F q.1 q.2)) (p ×ˢ p') (𝓤 β)
h' : Tendsto (fun q ↦ (f' q.2, F' q.1 q.2)) (q ×ˢ q') (𝓤 β')
⊢ Tendsto (fun q ↦ (Prod.map f f' q.2, Prod.map (F q.1.1) (F' q.1.2) q.2)) ((p ×ˢ q) ×ˢ p' ×ˢ q') (𝓤 (β × β'))
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : SetRel α α
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
⊢ IsComplete (⋃ i, s i)

Tactic:
set S := ⋃ i, s i

Goal state after:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : SetRel α α
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
S : Set α := ⋃ i, s i
⊢ IsComplete S
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: α : Type u
inst✝¹ : UniformSpace α
ι : Type u_1
inst✝ : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst✝¹.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst✝¹.toTopologicalSpace] t)
S : Bool → Set α := fun b ↦ Bool.casesOn b s t
U : (b : Bool) → ↑(S b) → ι
hU : ∀ (b : Bool) (x : ↑(S b)), Disjoint (ball (↑x) ((B (U b x)).comp (B (U b x)).inv)) (S !b)
hUS : ∀ (b : Bool), ⋃ x, ball (↑x) (B (U b x)) ∈ 𝓝ˢ (S b)
b : Bool
x : ↑(S b)
y : ↑(S !b)
hxy : U b x ≤ U (!b) y
z : α
⊢ z ∈ ball (↑x) (B (U b x)) ∩ ball (↑y) (B (U (!b) y)) → z ∈ ∅

Tactic:
hz

Goal state after:
α : Type u
inst✝¹ : UniformSpace α
ι : Type u_1
inst✝ : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst✝¹.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst✝¹.toTopologicalSpace] t)
S : Bool → Set α := fun b ↦ Bool.casesOn b s t
U : (b : Bool) → ↑(S b) → ι
hU : ∀ (b : Bool) (x : ↑(S b)), Disjoint (ball (↑x) ((B (U b x)).comp (B (U b x)).inv)) (S !b)
hUS : ∀ (b : Bool), ⋃ x, ball (↑x) (B (U b x)) ∈ 𝓝ˢ (S b)
b : Bool
x : ↑(S b)
y : ↑(S !b)
hxy : U b x ≤ U (!b) y
z : α
hz : z ∈ ball (↑x) (B (U b x)) ∩ ball (↑y) (B (U (!b) y))
⊢ z ∈ ∅
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
x : α
| Filter.comap mk (𝓝 (mk x))

Tactic:
comap_mk_nhds_mk,

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
x : α
| 𝓝 x
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort u_1
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type ?u.21
β : Type ?u.25
γ : Type ?u.29
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous fun p ↦ f p.1 p.2
⊢ Sort ?u.31

Tactic:
haveI := ua1 ⊓ ua2

Goal state after:
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort u_1
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type ?u.21
β : Type ?u.25
γ : Type ?u.29
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous fun p ↦ f p.1 p.2
this : UniformSpace α
⊢ Sort ?u.31
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
⊢ ⊥.TotallyBounded

Tactic:
by
  rw [← principal_empty, totallyBounded_principal_iff]
  exact totallyBounded_empty

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
x : α
hx : x ∈ s
L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∃ F, ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u
u₀ : Set (β × β)
hu₀ : u₀ ∈ 𝓤 β
u₁ : Set (β × β)
h₁ : u₁ ∈ 𝓤 β
u₁₀ : u₁ ○ u₁ ⊆ u₀
u₂ : Set (β × β)
h₂ : u₂ ∈ 𝓤 β
hsymm : ∀ {a b : β}, (a, b) ∈ u₂ → (b, a) ∈ u₂
u₂₁ : u₂ ○ u₂ ⊆ u₁
t : Set α
tx : t ∈ 𝓝[s] x
F : α → β
hFc : ContinuousWithinAt F s x
hF : ∀ y ∈ t, (f y, F y) ∈ u₂
A : ∀ᶠ (y : α) in 𝓝[s] x, (f y, F y) ∈ u₂
⊢ u₀ ∈ map (fun x_1 ↦ (f x_1, f x)) (𝓝[s] x)

Tactic:
have B : ∀ᶠ y in 𝓝[s] x, (F y, F x) ∈ u₂ := Uniform.continuousWithinAt_iff'_left.1 hFc h₂

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
x : α
hx : x ∈ s
L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∃ F, ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u
u₀ : Set (β × β)
hu₀ : u₀ ∈ 𝓤 β
u₁ : Set (β × β)
h₁ : u₁ ∈ 𝓤 β
u₁₀ : u₁ ○ u₁ ⊆ u₀
u₂ : Set (β × β)
h₂ : u₂ ∈ 𝓤 β
hsymm : ∀ {a b : β}, (a, b) ∈ u₂ → (b, a) ∈ u₂
u₂₁ : u₂ ○ u₂ ⊆ u₁
t : Set α
tx : t ∈ 𝓝[s] x
F : α → β
hFc : ContinuousWithinAt F s x
hF : ∀ y ∈ t, (f y, F y) ∈ u₂
A : ∀ᶠ (y : α) in 𝓝[s] x, (f y, F y) ∈ u₂
B : ∀ᶠ (y : α) in 𝓝[s] x, (F y, F x) ∈ u₂
⊢ u₀ ∈ map (fun x_1 ↦ (f x_1, f x)) (𝓝[s] x)
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
U : α → Set α
hU : ∀ (x : α), U x ∈ 𝓝 x ∧ ∀ᶠ (n : ι) in p, ∀ y ∈ U x, (f y, F n y) ∈ V
t : Finset ↑univ
ht : univ ⊆ ⋃ x ∈ t, U ↑x
⊢ ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V

Tactic:
replace hU := fun x : t => (hU x).2

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
U : α → Set α
t : Finset ↑univ
ht : univ ⊆ ⋃ x ∈ t, U ↑x
hU : ∀ (x : ↥t), ∀ᶠ (n : ι) in p, ∀ y ∈ U ↑↑x, (f y, F n y) ∈ V
⊢ ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
⊢ 𝓤 (α →ᵤ β) ≤ 𝓤 (α →ᵤ β)

pp: case refine_2
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
⊢ 𝓤 (α →ᵤ β) ≤ 𝓤 (α →ᵤ β)

pp: case refine_3
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
⊢ 𝓤 (α →ᵤ β) ≤ 𝓤 (α →ᵤ β)

Tactic:
· exact tendsto_iff_comap.mp UniformFun.precomp_uniformContinuous

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
⊢ 𝓤 (α →ᵤ β) ≤ 𝓤 (α →ᵤ β)

case refine_3
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
⊢ 𝓤 (α →ᵤ β) ≤ 𝓤 (α →ᵤ β)
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
⊢ 𝓤 (α →ᵤ β) ≤ 𝓤 (α →ᵤ β)

pp: case refine_3
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
⊢ 𝓤 (α →ᵤ β) ≤ 𝓤 (α →ᵤ β)

Tactic:
· exact tendsto_iff_comap.mp UniformFun.precomp_uniformContinuous

Goal state after:
case refine_3
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
⊢ 𝓤 (α →ᵤ β) ≤ 𝓤 (α →ᵤ β)
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
κ : Type u_2
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
p : κ → Prop
s : κ → Set (α × α)
F : ι → X → α
x₀ : X
hα : (𝓤 α).HasBasis p s
⊢ EquicontinuousAt F x₀ ↔ ∀ (k : κ), p k → ∀ᶠ (x : X) in 𝓝 x₀, ∀ (i : ι), (F i x₀, F i x) ∈ s k

Tactic:
rw [equicontinuousAt_iff_continuousAt, ContinuousAt,
    (UniformFun.hasBasis_nhds_of_basis ι α _ hα).tendsto_right_iff]
  rfl

Goal state after:
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : α → δ → ε
n : β → γ → δ
m₁ : α → β → β'
m₂ : α → γ → γ'
n' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' (m₁ a b) (m₂ a c)
⊢ map₂ m f (map₂ n g h) ≤ map₂ n' (map₂ m₁ f g) (map₂ m₂ f h)

Tactic:
rintro s ⟨t₁, ⟨u₁, hu₁, v, hv, ht₁⟩, t₂, ⟨u₂, hu₂, w, hw, ht₂⟩, hs⟩
  refine ⟨u₁ ∩ u₂, inter_mem hu₁ hu₂, _, image2_mem_map₂ hv hw, ?_⟩
  refine (image2_distrib_subset_left h_distrib).trans ((image2_subset ?_ ?_).trans hs)
  · exact (image2_subset_right inter_subset_left).trans ht₁
  · exact (image2_subset_right inter_subset_right).trans ht₂

Goal state after:
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: case refine_1
α : Type u_2
inst✝ : DivisionMonoid α
f g : Filter α
hfg✝ : f * g = 1
t₁ : Set α
h₁ : t₁ ∈ f
t₂ : Set α
h₂ : t₂ ∈ g
h : t₁ * t₂ = 1
hfg : (f * g).NeBot
⊢ ∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1

Tactic:
Set.mul_eq_one_iff

Goal state after:
case refine_1
α : Type u_2
inst✝ : DivisionMonoid α
f g : Filter α
hfg✝ : f * g = 1
t₁ : Set α
h₁ : t₁ ∈ f
t₂ : Set α
h₂ : t₂ ∈ g
h : ∃ a b, t₁ = {a} ∧ t₂ = {b} ∧ a * b = 1
hfg : (f * g).NeBot
⊢ ∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1
Module: Mathlib.Topology.Algebra.MulAction

Goal state before:
pp: M : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : TopologicalSpace X
inst✝¹ : SMul M X
inst✝ : ContinuousSMul M X
k : Set M
u : Set X
hk : IsCompact k
hu : IsCompact u
⊢ IsCompact ((fun x ↦ x.1 • x.2) '' k ×ˢ u)

Tactic:
exact IsCompact.image (hk.prod hu) continuous_smul

Goal state after:
Module: Mathlib.Topology.Algebra.MulAction

Goal state before:
pp: M : Type u_1
X : Type u_2
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace X
inst✝⁴ : Monoid M
inst✝³ : MulAction M X
inst✝² : ContinuousSMul M X
N : Type u_5
inst✝¹ : TopologicalSpace N
inst✝ : Monoid N
f : N →* M
hf : Continuous[inst✝¹, inst✝⁶] ⇑f
⊢ ContinuousSMul N X

Tactic:
by
  let _ : MulAction N X := MulAction.compHom _ f
  exact ⟨(hf.comp continuous_fst).smul continuous_snd⟩

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)
a : Y
⊢ ((fun g ↦ hf.lift ↑g ⋯) ((fun g ↦ ⟨g.comp f, ⋯⟩) g)) a = g a

Tactic:
simpa using congrArg g (Function.rightInverse_surjInv hf.surjective a)

Goal state after:
Module: Mathlib.Topology.Algebra.IsUniformGroup.Constructions

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Sort u_4
us' : ι → UniformSpace G
h' : ∀ (i : ι), IsUniformGroup G
⊢ IsUniformGroup G

Tactic:
rw [← sInf_range]

Goal state after:
G : Type u_1
inst✝ : Group G
ι : Sort u_4
us' : ι → UniformSpace G
h' : ∀ (i : ι), IsUniformGroup G
⊢ IsUniformGroup G
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: case neg
M : Type u_3
inst✝⁴ : GroupWithZero M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousMul M
inst✝¹ : CompactSpace M
inst✝ : T1Space M
U : Set M
hU : IsOpen[inst✝³] U
h0U : 0 ∈ U
h1U : 1 ∉ U
W : Set M
hW : W ∈ 𝓝 0
hW' : univ * W ⊆ U
H : ¬∃ x, x ≠ 0 ∧ x ∈ W
⊢ IsOpen[inst✝³] {0}

Tactic:
obtain rfl : W = {0} := subset_antisymm
      (by simpa [not_imp_not] using H) (by simpa using mem_of_mem_nhds hW)
    simpa [isOpen_iff_mem_nhds]

Goal state after:
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M : Type u_3
ι' : Sort u_6
inst✝ : Mul M
ts : ι' → TopologicalSpace M
h' : ∀ (i : ι'), ContinuousMul M
⊢ ContinuousMul M

Tactic:
rw [← sInf_range]

Goal state after:
M : Type u_3
ι' : Sort u_6
inst✝ : Mul M
ts : ι' → TopologicalSpace M
h' : ∀ (i : ι'), ContinuousMul M
⊢ ContinuousMul M
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : T1Space Y
f_cont : Continuous[inst✝², inst✝¹] f
x✝ : IsClosedMap f
H : ∀ (x : Y), (f ⁻¹' {x})ᶜ ∈ cocompact X
y : Y
K : Set X
hK : IsCompact K
hKy : Kᶜ ⊆ (f ⁻¹' {y})ᶜ
⊢ IsCompact (f ⁻¹' {y})

Tactic:
exact hK.of_isClosed_subset (isClosed_singleton.preimage f_cont)
    (compl_le_compl_iff_le.mp hKy)

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
ι' : Sort u_1
inst✝ : Inv G
ts' : ι' → TopologicalSpace G
h' : ∀ (i : ι'), ContinuousInv G
⊢ ContinuousInv G

Tactic:
rw [← sInf_range]

Goal state after:
G : Type w
ι' : Sort u_1
inst✝ : Inv G
ts' : ι' → TopologicalSpace G
h' : ∀ (i : ι'), ContinuousInv G
⊢ ContinuousInv G
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
x : G
s : Set G
⊢ x ∈ closure[inst✝²] s ↔ ∀ U ∈ 𝓝 1, ∃ y ∈ s, y / x ∈ U

Tactic:
by
  rw [mem_closure_iff_nhds_basis ((𝓝 1 : Filter G).basis_sets.nhds_of_one x)]
  simp_rw [Set.mem_ofPred, id]

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: case refine_2
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
x : G
h : K ∈ 𝓝 x
y : G
⊢ (y * x⁻¹) • K ∈ 𝓝 y

Tactic:
· rw [← preimage_smul_inv]
    exact (continuous_const_smul _).continuousAt.preimage_mem_nhds (by simpa using h)

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Field

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k : α
hk : 0 < k
a b : α
x✝ : 1 ≤ b
⊢ a / k ≤ b ↔ a ≤ k * b

Tactic:
div_le_iff₀' hk

Goal state after:
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k : α
hk : 0 < k
a b : α
x✝ : 1 ≤ b
⊢ a ≤ k * b ↔ a ≤ k * b
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
x : G
hx : x ∈ K
⊢ U ∈ 𝓝 (x * 1)

Tactic:
simpa using hU.mem_nhds (hKU hx)

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
ι : Sort u_1
inst✝ : Group G
ts' : ι → TopologicalSpace G
h' : ∀ (i : ι), IsTopologicalGroup G
⊢ IsTopologicalGroup G

Tactic:
rw [← sInf_range]

Goal state after:
G : Type w
ι : Sort u_1
inst✝ : Group G
ts' : ι → TopologicalSpace G
h' : ∀ (i : ι), IsTopologicalGroup G
⊢ IsTopologicalGroup G
Module: Mathlib.Topology.Algebra.Field

Goal state before:
pp: K✝ : Type u_1
inst✝⁴ : DivisionRing K✝
inst✝³ : TopologicalSpace K✝
α : Type u_2
inst✝² : Field α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalDivisionRing α
K : Subfield α
x : α
hx : x ∈ closure ↑K
⊢ x⁻¹ ∈ closure ↑K

Tactic:
rcases eq_or_ne x 0 with (rfl | h)
      · rwa [inv_zero]
      · rw [← inv_coe_set, ← Set.image_inv_eq_inv]
        exact mem_closure_image (continuousAt_inv₀ h) hx

Goal state after:
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
⊢ update f i '' Ico a b = Ico (update f i a) (update f i b)

Tactic:
rw [← Icc_sdiff_right, ← Icc_sdiff_right, image_sdiff (update_injective _ _), image_singleton,
    image_update_Icc]

Goal state after:
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
t : Set α := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
x : α
hx : x ∈ s ∧ (∃ u ∈ 𝓝 x, u ∩ (s ∩ Ioi x) = ∅) ∧ ∃ x_1, x < x_1
u : Set α
hu : u ∈ 𝓝 x
y : α
hxy : x < y
hy : Ico x y ⊆ u
h'u : (s ∩ Ioo x y).Nonempty
z : α
⊢ z ∈ s ∩ Ioo x y → z ∈ u ∩ (s ∩ Ioi x)

Tactic:
hz

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
t : Set α := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
x : α
hx : x ∈ s ∧ (∃ u ∈ 𝓝 x, u ∩ (s ∩ Ioi x) = ∅) ∧ ∃ x_1, x < x_1
u : Set α
hu : u ∈ 𝓝 x
y : α
hxy : x < y
hy : Ico x y ⊆ u
h'u : (s ∩ Ioo x y).Nonempty
z : α
hz : z ∈ s ∩ Ioo x y
⊢ z ∈ u ∩ (s ∩ Ioi x)