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

Goal state before:
pp: case empty
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → X i)
uo : IsOpen[Pi.topologicalSpace] u
vo : IsOpen[Pi.topologicalSpace] v
hsuv : univ.pi s ⊆ u ∪ v
f : (i : ι) → X i
hfs : f ∈ univ.pi s
hfu : f ∈ u
g : (i : ι) → X i
hgs : g ∈ univ.pi s
hgv : g ∈ v
hI : ∅.piecewise f g ∈ u
⊢ (univ.pi s ∩ (u ∩ v)).Nonempty

Tactic:
refine ⟨g, hgs, ⟨?_, hgv⟩⟩

Goal state after:
case empty
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → X i)
uo : IsOpen[Pi.topologicalSpace] u
vo : IsOpen[Pi.topologicalSpace] v
hsuv : univ.pi s ⊆ u ∪ v
f : (i : ι) → X i
hfs : f ∈ univ.pi s
hfu : f ∈ u
g : (i : ι) → X i
hgs : g ∈ univ.pi s
hgv : g ∈ v
hI : ∅.piecewise f g ∈ u
⊢ g ∈ u
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case mpr.inr
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
h : s ⊆ v
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
· rcases hsu with ⟨x, hxs, hxu⟩
      exact ⟨x, hxs, ⟨hxu, h hxs⟩⟩

Goal state after:
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
Y : Type v
ι : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s✝ t : Set X
inst✝ : NonLindelofSpace X
s : Set X
hs : IsLindelof s
⊢ sᶜ.Nonempty

Tactic:
contrapose hs

Goal state after:
X : Type u
Y : Type v
ι : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s✝ t : Set X
inst✝ : NonLindelofSpace X
s : Set X
hs : ¬sᶜ.Nonempty
⊢ ¬IsLindelof s
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: case inr
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : HereditarilyLindelofSpace X
ι : Type u_2
inst✝ : Nonempty ι
U : ι → Set X
h : ∀ (i : ι), IsOpen[inst✝²] (U i)
k : ℕ → ι
htc : (range k).Countable
htu : ⋃ i ∈ range k, U i = ⋃ i, U i
t_ne : (range k).Nonempty
⊢ ∃ k, ⋃ n, U (k n) = ⋃ i, U i

Tactic:
use k

Goal state after:
case h
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : HereditarilyLindelofSpace X
ι : Type u_2
inst✝ : Nonempty ι
U : ι → Set X
h : ∀ (i : ι), IsOpen[inst✝²] (U i)
k : ℕ → ι
htc : (range k).Countable
htu : ⋃ i ∈ range k, U i = ⋃ i, U i
t_ne : (range k).Nonempty
⊢ ⋃ n, U (k n) = ⋃ i, U i
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
ι' : Sort u_4
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι'
f : ι' → Set X
hs : ∀ (i : ι'), IsMeagre (f i)
⊢ IsMeagre (⋃ i, f i)

Tactic:
rw [IsMeagre, compl_iUnion]

Goal state after:
X : Type u_1
ι' : Sort u_4
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι'
f : ι' → Set X
hs : ∀ (i : ι'), IsMeagre (f i)
⊢ ⋂ i, (f i)ᶜ ∈ residual X
Module: Mathlib.Topology.Connected.TotallyDisconnected

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
β : Type u_3
inst✝ : TopologicalSpace β
f : α → β
hf : IsCoinducing f
⊢ IsCoinducing ⋯.connectedComponentsMap

Tactic:
rw [← ConnectedComponents.isQuotientMap_coe.isCoinducing.of_comp_iff]
  exact ConnectedComponents.isQuotientMap_coe.isCoinducing.comp hf

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

Goal state before:
pp: β : Type v
u v : UniformSpace β
F : Filter β
⊢ Cauchy F ↔ Cauchy F ∧ Cauchy F

Tactic:
unfold Cauchy

Goal state after:
β : Type v
u v : UniformSpace β
F : Filter β
⊢ F.NeBot ∧ F ×ˢ F ≤ 𝓤 β ↔ (F.NeBot ∧ F ×ˢ F ≤ 𝓤 β) ∧ F.NeBot ∧ F ×ˢ F ≤ 𝓤 β
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: β : Type v
ι : Sort u_1
inst✝ : Nonempty ι
u : ι → UniformSpace β
l : Filter β
⊢ Cauchy l ↔ ∀ (i : ι), Cauchy l

Tactic:
unfold Cauchy

Goal state after:
β : Type v
ι : Sort u_1
inst✝ : Nonempty ι
u : ι → UniformSpace β
l : Filter β
⊢ l.NeBot ∧ l ×ˢ l ≤ 𝓤 β ↔ ∀ (i : ι), l.NeBot ∧ l ×ˢ l ≤ 𝓤 β
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: β : Type ub
V W : SetRel β β
x y z : β
inst✝ : V.IsSymm
hx : x ∈ ball z V
hy : y ∈ ball z W
⊢ (x, y) ∈ V ○ W

Tactic:
rw [mem_ball_symmetry] at hx

Goal state after:
β : Type ub
V W : SetRel β β
x y z : β
inst✝ : V.IsSymm
hx : z ∈ ball x V
hy : y ∈ ball z W
⊢ (x, y) ∈ V ○ W
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
d s : SetRel α α
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
x✝ : α × α
x y : α
hp : (x, y) ∈ s
⊢ cl_d ∈ (𝓤 α).lift' fun s ↦ {y | (y, x) ∈ s} ×ˢ {y_1 | (y, y_1) ∈ s}

Tactic:
mem_lift'_sets

Goal state after:
α : Type ua
inst✝ : UniformSpace α
d s : SetRel α α
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
x✝ : α × α
x y : α
hp : (x, y) ∈ s
⊢ ∃ t ∈ 𝓤 α, {y | (y, x) ∈ t} ×ˢ {y_1 | (y, y_1) ∈ t} ⊆ cl_d

case hh
α : Type ua
inst✝ : UniformSpace α
d s : SetRel α α
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
x✝ : α × α
x y : α
hp : (x, y) ∈ s
⊢ Monotone fun s ↦ {y | (y, x) ∈ s} ×ˢ {y_1 | (y, y_1) ∈ s}
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
a b : α
⊢ 𝓝 a ×ˢ 𝓝 b = (𝓤 α).lift fun s ↦ (𝓤 α).lift' fun t ↦ {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ t}

Tactic:
nhds_eq_uniformity',

Goal state after:
α : Type ua
inst✝ : UniformSpace α
a b : α
⊢ ((𝓤 α).lift' fun s ↦ {y | (y, a) ∈ s}) ×ˢ 𝓝 b =
    (𝓤 α).lift fun s ↦ (𝓤 α).lift' fun t ↦ {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ t}
Module: Mathlib.Topology.UniformSpace.UniformConvergence

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

Tactic:
exact h.prodMap h'

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
s : Set α
⊢ IsOpen[inst✝.toTopologicalSpace] s ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] V ∧ ball x V ⊆ s

Tactic:
by
  rw [isOpen_iff_ball_subset]
  constructor <;> intro h x hx
  · obtain ⟨V, hV, hV'⟩ := h x hx
    exact
      ⟨interior V, interior_mem_uniformity hV, isOpen_interior,
        (ball_mono interior_subset x).trans hV'⟩
  · obtain ⟨V, hV, -, hV'⟩ := h x hx
    exact ⟨V, hV, hV'⟩

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

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

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

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

Goal state before:
pp: case mpr
α : Type u
uniformSpace : UniformSpace α
g : Filter α
⊢ (∀ (f : Filter α), f.NeBot → f ≤ g → ∃ c ≤ f, Cauchy c) → g.TotallyBounded

Tactic:
intro H d hd

Goal state after:
case mpr
α : Type u
uniformSpace : UniformSpace α
g : Filter α
H : ∀ (f : Filter α), f.NeBot → f ≤ g → ∃ c ≤ f, Cauchy c
d : SetRel α α
hd : d ∈ 𝓤 α
⊢ ∃ t, t.Finite ∧ d.preimage t ∈ g
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: case mpr
α : Type u
uniformSpace : UniformSpace α
g : Filter α
d : SetRel α α
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), t.Finite → d.preimage t ∉ g
f : Filter α := ⨅ t, g ⊓ 𝓟 (d.preimage ↑t)ᶜ
hb : Antitone fun t ↦ g ⊓ 𝓟 (d.preimage ↑t)ᶜ
this : f.NeBot
⊢ ∃ f, f.NeBot ∧ f ≤ g ∧ ∀ c ≤ f, ¬Cauchy c

Tactic:
have : f ≤ g := iInf_le_of_le ∅ (by simp)

Goal state after:
case mpr
α : Type u
uniformSpace : UniformSpace α
g : Filter α
d : SetRel α α
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), t.Finite → d.preimage t ∉ g
f : Filter α := ⨅ t, g ⊓ 𝓟 (d.preimage ↑t)ᶜ
hb : Antitone fun t ↦ g ⊓ 𝓟 (d.preimage ↑t)ᶜ
this✝ : f.NeBot
this : f ≤ g
⊢ ∃ f, f.NeBot ∧ f ≤ g ∧ ∀ c ≤ f, ¬Cauchy c
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst✝ : UniformSpace β'
F' : ι' → α' → β'
p' : Filter ι'
s' : Set α'
h : UniformCauchySeqOn F p s
h' : UniformCauchySeqOn F' p' s'
u : Set ((β × β') × β × β')
v : Set (β × β)
hv : v ∈ 𝓤 β
w : Set (β' × β')
hw : w ∈ 𝓤 β'
hvw : v ×ˢ w ⊆ (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' u
⊢ ∀ᶠ (m : (ι × ι') × ι × ι') in (p ×ˢ p') ×ˢ p ×ˢ p',
    ∀ (a : α) (b : α'),
      a ∈ s → b ∈ s' → (Prod.map (F m.1.1) (F' m.1.2) (a, b), Prod.map (F m.2.1) (F' m.2.2) (a, b)) ∈ u

Tactic:
Prod.map_apply

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst✝ : UniformSpace β'
F' : ι' → α' → β'
p' : Filter ι'
s' : Set α'
h : UniformCauchySeqOn F p s
h' : UniformCauchySeqOn F' p' s'
u : Set ((β × β') × β × β')
v : Set (β × β)
hv : v ∈ 𝓤 β
w : Set (β' × β')
hw : w ∈ 𝓤 β'
hvw : v ×ˢ w ⊆ (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' u
⊢ ∀ᶠ (m : (ι × ι') × ι × ι') in (p ×ˢ p') ×ˢ p ×ˢ p',
    ∀ (a : α) (b : α'), a ∈ s → b ∈ s' → ((F m.1.1 a, F' m.1.2 b), F m.2.1 a, F' m.2.2 b) ∈ u
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
m : α → β
s : Set α
hm : IsUniformInducing m
fact1 : SurjOn (map m) (Iic (𝓟 s)) (Iic (𝓟 (m '' s)))
fact2 : MapsTo (map m) (Iic (𝓟 s)) (Iic (𝓟 (m '' s)))
⊢ (∀ x ∈ Iic (𝓟 s), Cauchy x → ∃ x_1 ∈ s, x ≤ comap m (𝓝 (m x_1))) ↔ ∀ f ∈ Iic (𝓟 s), Cauchy f → ∃ x ∈ s, f ≤ 𝓝 x

Tactic:
hm.isInducing.nhds_eq_comap

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

Goal state before:
pp: case refine_2
α : Type u
uniformSpace : UniformSpace α
inst✝ : (𝓤 α).IsCountablyGenerated
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ a, Tendsto u atTop (𝓝 a)
U' : ℕ → Set (α × α)
hU' : ∀ {s : Set (α × α)}, s ∈ 𝓤 α ↔ ∃ i, U' i ⊆ s
Hmem : ∀ (n : ℕ), U n ∩ U' n ∈ 𝓤 α
f✝ : Filter α
hf : Cauchy f✝
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ ∃ n, U n ∩ U' n ⊆ s

Tactic:
rcases hU'.1 hs with ⟨N, hN⟩

Goal state after:
case refine_2
α : Type u
uniformSpace : UniformSpace α
inst✝ : (𝓤 α).IsCountablyGenerated
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ a, Tendsto u atTop (𝓝 a)
U' : ℕ → Set (α × α)
hU' : ∀ {s : Set (α × α)}, s ∈ 𝓤 α ↔ ∃ i, U' i ⊆ s
Hmem : ∀ (n : ℕ), U n ∩ U' n ∈ 𝓤 α
f✝ : Filter α
hf : Cauchy f✝
s : Set (α × α)
hs : s ∈ 𝓤 α
N : ℕ
hN : U' N ⊆ s
⊢ ∃ n, U n ∩ U' n ⊆ s
Module: Mathlib.Topology.Coherent

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
h : ∀ (f : X → Prop), (∀ s ∈ S, ContinuousOn f s) → Continuous[inst✝, _] f
u : Set X
hu : ∀ s ∈ S, IsOpen[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' u)
⊢ IsOpen[inst✝] u

Tactic:
simp only [continuousOn_iff_continuous_domRestrict, continuous_Prop] at *

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
u : Set X
hu : ∀ s ∈ S, IsOpen[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' u)
h : ∀ (f : X → Prop), (∀ s ∈ S, IsOpen[instTopologicalSpaceSubtype] {x | s.domRestrict f x}) → IsOpen[inst✝] {x | f x}
⊢ IsOpen[inst✝] u
Module: Mathlib.Topology.UniformSpace.UniformApproximation

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
f : α → β
x : α
L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∃ F, ContinuousAt F x ∧ ∀ y ∈ t, (f y, F y) ∈ u
⊢ ContinuousAt f x

Tactic:
by
  rw [← continuousWithinAt_univ]
  apply continuousWithinAt_of_locally_uniform_approx_of_continuousWithinAt (mem_univ _) _
  simpa only [exists_prop, nhdsWithin_univ, continuousWithinAt_univ] using L

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
x : β
h_cont : Continuous[inst✝¹.toTopologicalSpace, inst✝.toTopologicalSpace] f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SetRel.IsSymm t
htr : SetRel.comp t t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y | (x, y) ∈ t}
b₁ b₂ : α
h : (b₁, b₂) ∈ SetRel.symmetrize {x | x.1 ∈ s → (f x.1, f x.2) ∈ SetRel.symmetrize r}
h₁ : b₁ ∉ s
h₂ : b₂ ∈ s
⊢ (b₁, b₂) ∈ {x | (f x.1, f x.2) ∈ r}

Tactic:
exact (h.2 h₂).2

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

Goal state before:
pp: ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
S : Set β
⊢ UniformEquicontinuousOn F S ↔ UniformContinuousOn (⇑ofFun ∘ swap F) S

Tactic:
rw [UniformContinuousOn, (UniformFun.hasBasis_uniformity ι α).tendsto_right_iff]

Goal state after:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
S : Set β
⊢ UniformEquicontinuousOn F S ↔
    ∀ i ∈ 𝓤 α, ∀ᶠ (x : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S), ((⇑ofFun ∘ swap F) x.1, (⇑ofFun ∘ swap F) x.2) ∈ UniformFun.gen ι α i
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
f : Filter α
g : Filter β
inst✝ : f.NeBot
⊢ map₂ (fun x y ↦ y) f g = g

Tactic:
map₂_swap,

Goal state after:
α : Type u_1
β : Type u_3
f : Filter α
g : Filter β
inst✝ : f.NeBot
⊢ map₂ (fun a b ↦ a) g f = g
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
f : Filter α
g : Filter β
m : α → γ → δ
n : β → γ
⊢ map₂ m f (map n g) = map₂ (fun a b ↦ m a (n b)) f g

Tactic:
map₂_swap,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
f : Filter α
g : Filter β
m : α → γ → δ
n : β → γ
⊢ map₂ (fun a b ↦ m b a) (map n g) f = map₂ (fun a b ↦ m a (n b)) f g
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 𝔗 : Set (Set α)
h : ∀ s ∈ 𝔖, ∃ T ⊆ 𝔗, T.Finite ∧ s ⊆ ⋃₀ T
V : Set (β × β)
hV : V ∈ 𝓤 β
s : Set α
hs : s ∈ 𝔖
⊢ ∃ I,
    I.Finite ∧
      (∀ i ∈ I, i ∈ 𝔗) ∧
        ⋂ i ∈ I, UniformOnFun.gen 𝔗 i V ⊆
          {x | ((⇑(ofFun 𝔗) ∘ ⇑(toFun 𝔖)) x.1, (⇑(ofFun 𝔗) ∘ ⇑(toFun 𝔖)) x.2) ∈ UniformOnFun.gen 𝔖 s V}

Tactic:
obtain ⟨T, hT𝔗, hT, hsT⟩ := h s hs

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 𝔗 : Set (Set α)
h : ∀ s ∈ 𝔖, ∃ T ⊆ 𝔗, T.Finite ∧ s ⊆ ⋃₀ T
V : Set (β × β)
hV : V ∈ 𝓤 β
s : Set α
hs : s ∈ 𝔖
T : Set (Set α)
hT𝔗 : T ⊆ 𝔗
hT : T.Finite
hsT : s ⊆ ⋃₀ T
⊢ ∃ I,
    I.Finite ∧
      (∀ i ∈ I, i ∈ 𝔗) ∧
        ⋂ i ∈ I, UniformOnFun.gen 𝔗 i V ⊆
          {x | ((⇑(ofFun 𝔗) ∘ ⇑(toFun 𝔖)) x.1, (⇑(ofFun 𝔗) ∘ ⇑(toFun 𝔖)) x.2) ∈ UniformOnFun.gen 𝔖 s V}
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : CompleteSpace β
h✝ : Nonempty β
F : Filter (α →ᵤ[𝔖] β)
hF : Cauchy F
this : F.NeBot
g : α → β
hg : ∀ x ∈ ⋃₀ 𝔖, Tendsto (fun x_1 ↦ (toFun 𝔖) x_1 x) F (𝓝 (g x))
⊢ F ≤ 𝓝 ((ofFun 𝔖) g)

Tactic:
UniformOnFun.nhds_eq_of_basis _ _ uniformity_hasBasis_closed,

Goal state after:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : CompleteSpace β
h✝ : Nonempty β
F : Filter (α →ᵤ[𝔖] β)
hF : Cauchy F
this : F.NeBot
g : α → β
hg : ∀ x ∈ ⋃₀ 𝔖, Tendsto (fun x_1 ↦ (toFun 𝔖) x_1 x) F (𝓝 (g x))
⊢ F ≤
    ⨅ s ∈ 𝔖,
      ⨅ i,
        ⨅ (_ : i ∈ 𝓤 β ∧ IsClosed[instTopologicalSpaceProd] i),
          𝓟 {g_1 | ∀ x ∈ s, ((toFun 𝔖) ((ofFun 𝔖) g) x, (toFun 𝔖) g_1 x) ∈ id i}
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ a * x) ⁻¹' Icc b c = Icc (b / a) (c / a)

Tactic:
simp [← Ici_inter_Iic]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ x * a) ⁻¹' Icc b c = Icc (b / a) (c / a)

Tactic:
simp [← Ici_inter_Iic]

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
⊢ (fun x ↦ a * x) ⁻¹' Iio aU = Iio (a⁻¹ * aU)

Tactic:
rw [Set.preimage_const_mul_Iio₀ _ hb, div_eq_inv_mul]

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

Goal state before:
pp: α : Type u_2
inst✝³ : Monoid α
inst✝² : Preorder α
inst✝¹ : CanonicallyOrderedMul α
inst✝ : MulRightMono α
a b c : α
c_in : c ∈ Ici (a * b)
d : α
hd : c = a * b * d
⊢ b * d ∈ Ici b ∧ a * (b * d) = c

Tactic:
simp [← mul_assoc, hd]

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.comp f) x✝¹ = (g.comp f) x✝

Tactic:
simp only [ContinuousMap.comp_apply]

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
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✝)
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous[inst✝¹, inst✝] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
ℱ : Filter X
y : Y
hy : (ℱ.lift' closure[inst✝¹] ⊓ 𝓟 (f ⁻¹' {y})).NeBot
x : X
hxy : x ∈ f ⁻¹' {y}
hx : ClusterPt x (ℱ.lift' closure[inst✝¹] ⊓ 𝓟 (f ⁻¹' {y}))
⊢ ClusterPt x ℱ

Tactic:
← clusterPt_lift'_closure_iff

Goal state after:
case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous[inst✝¹, inst✝] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
ℱ : Filter X
y : Y
hy : (ℱ.lift' closure[inst✝¹] ⊓ 𝓟 (f ⁻¹' {y})).NeBot
x : X
hxy : x ∈ f ⁻¹' {y}
hx : ClusterPt x (ℱ.lift' closure[inst✝¹] ⊓ 𝓟 (f ⁻¹' {y}))
⊢ ClusterPt x (ℱ.lift' closure[inst✝¹])
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
g h : G
hg : g ∈ connectedComponent 1
hh : h ∈ connectedComponent 1
⊢ g ∈ (fun x ↦ g * x) '' connectedComponent 1

Tactic:
exact ⟨(1 : G), mem_connectedComponent, by simp only [mul_one]⟩

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

Goal state before:
pp: G : Type u_2
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
⊢ comap mabs atTop = atBot ⊔ atTop

Tactic:
refine
    le_antisymm (((atTop_basis.comap _).le_basis_iff (atBot_basis.sup atTop_basis)).2 ?_)
      (sup_le tendsto_mabs_atBot_atTop.le_comap tendsto_mabs_atTop_atTop.le_comap)

Goal state after:
G : Type u_2
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
⊢ ∀ (i' : G × G), True ∧ True → ∃ i, True ∧ mabs ⁻¹' Ici i ⊆ Iic i'.1 ∪ Ici i'.2
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
⊢ 𝓝[>] a = ⊥ ↔ IsTop a ∨ ∃ b, a ⋖ b

Tactic:
by_cases ha : IsTop a
  · simp [ha, ha.isMax.Ioi_eq]
  · simp only [ha, false_or]
    rw [isTop_iff_isMax, not_isMax_iff] at ha
    simp only [(nhdsGT_basis_of_exists_gt ha).eq_bot_iff, covBy_iff_Ioo_eq]

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
inst✝¹ : (i : α) → Decidable (i ∈ s)
inst✝ : (i : β) → Decidable (i ∈ t)
h : e.IsImage s t
h' : e'.IsImage s t
x : α
he : x ∈ e.source
hs : x ∈ s
⊢ t.piecewise (↑e.symm) (↑e'.symm) (s.piecewise (↑e) (↑e') x) = x

Tactic:
rw [piecewise_eq_of_mem _ _ _ hs, piecewise_eq_of_mem _ _ _ ((h he).2 hs), e.left_inv he]

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
h : e.IsImage s t
h' : e'.IsImage s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e) (↑e') (e.source ∩ s)
⊢ e.target ∩ t = e'.target ∩ t

Tactic:
rw [← h.image_eq, ← h'.image_eq, ← hs, heq.image_eq]

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

Goal state before:
pp: α : Type u
ts : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
⊢ ⨅ s, ⨅ (_ : (∃ x, s = Ioi x) ∧ a ∈ s ∨ (∃ x, s = Iio x) ∧ a ∈ s), 𝓟 s =
    (⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b)

Tactic:
iInf_or,

Goal state after:
α : Type u
ts : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
⊢ ⨅ s, (⨅ (_ : (∃ x, s = Ioi x) ∧ a ∈ s), 𝓟 s) ⊓ ⨅ (_ : (∃ x, s = Iio x) ∧ a ∈ s), 𝓟 s =
    (⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b)
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case inr.a
α : Type u
ts : TopologicalSpace α
inst✝² : Preorder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
hα : Nonempty α
t : Set (Set α)
t_subs : t ⊆ {s | ∃ a, s = Ioi a ∨ s = Iio a}
t_count : t.Countable
ht : ts = generateFrom t
a : Set α → α
ha : ∀ s ∈ t, s = Ioi (a s) ∨ s = Iio (a s)
⊢ ts ≤ generateFrom {s | ∃ a_1 ∈ a '' t, s = Ioi a_1 ∨ s = Iio a_1}

Tactic:
apply le_generateFrom_iff_subset_isOpen.2

Goal state after:
case inr.a
α : Type u
ts : TopologicalSpace α
inst✝² : Preorder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
hα : Nonempty α
t : Set (Set α)
t_subs : t ⊆ {s | ∃ a, s = Ioi a ∨ s = Iio a}
t_count : t.Countable
ht : ts = generateFrom t
a : Set α → α
ha : ∀ s ∈ t, s = Ioi (a s) ∨ s = Iio (a s)
⊢ {s | ∃ a_1 ∈ a '' t, s = Ioi a_1 ∨ s = Iio a_1} ⊆ {s | IsOpen[ts] s}
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : SeparableSpace α
⊢ SecondCountableTopology α

Tactic:
rcases exists_countable_dense α with ⟨s, hc, hd⟩
  refine ⟨⟨_, ?_, hd.topology_eq_generateFrom⟩⟩
  exact (hc.image _).union (hc.image _)

Goal state after:
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case mpr.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.δlast.Exact
h' : (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact
i : ℕ
hi : i + 2 ≤ n + 2
⊢ (S.sc ⋯ i hi).Exact

Tactic:
simp only [Nat.add_le_add_iff_right] at hi
      obtain hi | rfl := hi.lt_or_eq
      · exact h.exact i
      · exact h'.exact 0

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
A : C
x₂ : A ⟶ S.L₀'.X₂
hx₂ : x₂ ≫ S.L₀'.g = 0
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.L₀'.f

Tactic:
dsimp [L₀'] at x₂ hx₂

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
A : C
x₂ : A ⟶ S.P
hx₂ : x₂ ≫ pullback.snd S.L₁.g S.v₀₁.τ₃ = 0
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.L₀'.f
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.op.δ.unop = S.δ

Tactic:
← cancel_mono (pushout.inr _ _ : _ ⟶ S.P'),

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.op.δ.unop ≫ pushout.inr S.L₂.f S.v₂₃.τ₁ = S.δ ≫ pushout.inr S.L₂.f S.v₂₃.τ₁
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : SnakeInput C
f : S₁ ⟶ S₂
⊢ S₁.φ₁ ≫ f.f₂.τ₁ = functorP.map f ≫ S₂.φ₁

Tactic:
simp only [← cancel_mono S₂.L₂.f, assoc, φ₁_L₂_f, ← naturality_φ₂, f.f₂.comm₁₂, φ₁_L₂_f_assoc]

Goal state after: