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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s s' t : Set α
ht : ∀ x ∈ frontier t, x ∈ s ↔ x ∈ s'
hs : Continuous[inst✝, _] fun x ↦ x ∈ s
hs' : Continuous[inst✝, _] fun x ↦ x ∈ s'
x : α
⊢ x ∈ s ∩ t ∪ s' \ t ↔ t.piecewise (Membership.mem s) (Membership.mem s') x

Tactic:
by_cases hx : x ∈ t

Goal state after:
case pos
α : Type u_1
inst✝ : TopologicalSpace α
s s' t : Set α
ht : ∀ x ∈ frontier t, x ∈ s ↔ x ∈ s'
hs : Continuous[inst✝, _] fun x ↦ x ∈ s
hs' : Continuous[inst✝, _] fun x ↦ x ∈ s'
x : α
hx : x ∈ t
⊢ x ∈ s ∩ t ∪ s' \ t ↔ t.piecewise (Membership.mem s) (Membership.mem s') x

case neg
α : Type u_1
inst✝ : TopologicalSpace α
s s' t : Set α
ht : ∀ x ∈ frontier t, x ∈ s ↔ x ∈ s'
hs : Continuous[inst✝, _] fun x ↦ x ∈ s
hs' : Continuous[inst✝, _] fun x ↦ x ∈ s'
x : α
hx : x ∉ t
⊢ x ∈ s ∩ t ∪ s' \ t ↔ t.piecewise (Membership.mem s) (Membership.mem s') x
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s s' t : Set α
ht : s ∩ frontier t = s' ∩ frontier t
⊢ tᶜ.ite s' s ∩ closure[inst✝] tᶜ = s' ∩ closure[inst✝] tᶜ

Tactic:
ite_inter_closure_eq_of_inter_frontier_eq

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s s' t : Set α
ht : s ∩ frontier t = s' ∩ frontier t
⊢ s' ∩ closure[inst✝] tᶜ = s' ∩ closure[inst✝] tᶜ

α : Type u_1
inst✝ : TopologicalSpace α
s s' t : Set α
ht : s ∩ frontier t = s' ∩ frontier t
⊢ s' ∩ frontier tᶜ = s ∩ frontier tᶜ
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: case h.refine_1
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed[inst✝¹] S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen[inst✝¹] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty { U // U ∈ c }
U₀compl : Sᶜ ⊆ U₀
⊢ Sᶜ ⊆ ⋃₀ c

Tactic:
exact fun _ hx => ⟨U₀, hU₀, U₀compl hx⟩

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
hs : s.Finite
ht : t.Finite
h : Disjoint s t
⊢ SeparatedNhds s t

Tactic:
rw [← hs.coe_toFinset, ← ht.coe_toFinset]
  exact SeparatedNhds.of_finset_finset _ _ (Finite.disjoint_toFinset.2 h)

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space X
x : X
s t : Set X
f : X → Y
y : X
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ ContinuousWithinAt f (insert x s) x ↔ ContinuousWithinAt f (insert x t) x

Tactic:
exact continuousWithinAt_congr_set (eventuallyEq_insert h)

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
S : Set X
x : X
h : AccPt x (𝓟 S)
⊢ S.Infinite

Tactic:
intro hs
  have := hs.compl_mem_codiscrete
  rw [mem_codiscrete_accPt, compl_compl] at this
  exact this _ h

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Sort u_3
inst✝ : Finite ι
s : ι → Set X
hs : ∀ (i : ι), IsDiscrete (s i)
hsc : ∀ (i : ι), IsClosed[inst✝¹] (s i)
⊢ IsDiscrete (⋃ i, s i)

Tactic:
suffices (⋃ i, s i)ᶜ ∈ codiscrete X from (compl_mem_codiscrete_iff.mp this).2

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Sort u_3
inst✝ : Finite ι
s : ι → Set X
hs : ∀ (i : ι), IsDiscrete (s i)
hsc : ∀ (i : ι), IsClosed[inst✝¹] (s i)
⊢ (⋃ i, s i)ᶜ ∈ codiscrete X
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Sort u_3
inst✝ : Finite ι
s : ι → Set X
hs : ∀ (i : ι), IsDiscrete (s i)
hsc : ∀ (i : ι), IsClosed[inst✝¹] (s i)
⊢ IsDiscrete (⋃ i, s i)

Tactic:
by
  suffices (⋃ i, s i)ᶜ ∈ codiscrete X from (compl_mem_codiscrete_iff.mp this).2
  simp [compl_mem_codiscrete_iff, *]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : TopologicalSpace β
hf : Continuous[inst✝, inst✝³] f
hg : Continuous[inst✝, inst✝³] g
⊢ Continuous[inst✝, inst✝³] fun b ↦ max (f b) (g b)

Tactic:
simp only [max_def]

Goal state after:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : TopologicalSpace β
hf : Continuous[inst✝, inst✝³] f
hg : Continuous[inst✝, inst✝³] g
⊢ Continuous[inst✝, inst✝³] fun b ↦ if f b ≤ g b then g b else f b
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
f : β → α
l : Filter β
a : α
h : Tendsto f l (𝓝[>] a)
⊢ Tendsto (fun i ↦ max a (f i)) l (𝓝[>] a)

Tactic:
exact Filter.tendsto_nhds_max_right h

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

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β✝ : Type u_3
l✝ : Filter α✝
inst✝² : CountableInterFilter l✝
α : Type u_4
β : Type u_5
l : Filter α
m : Filter β
inst✝¹ : CountableInterFilter l
inst✝ : CountableInterFilter m
⊢ ∀ (S : Set (Set (α × β))), S.Countable → (∀ s ∈ S, s ∈ l.curry m) → ⋂₀ S ∈ l.curry m

Tactic:
intro S

Goal state after:
ι : Sort u_1
α✝ : Type u_2
β✝ : Type u_3
l✝ : Filter α✝
inst✝² : CountableInterFilter l✝
α : Type u_4
β : Type u_5
l : Filter α
m : Filter β
inst✝¹ : CountableInterFilter l
inst✝ : CountableInterFilter m
S : Set (Set (α × β))
⊢ S.Countable → (∀ s ∈ S, s ∈ l.curry m) → ⋂₀ S ∈ l.curry m
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst✝] (U i)
hsU : s ⊆ ⋃ i, U i
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → (∃ r, r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
⊢ ∀ (S : Set (Set X)),
    S.Countable → (∀ s ∈ S, ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i) → ∃ r, r.Countable ∧ ⋃₀ S ⊆ ⋃ i ∈ r, U i

Tactic:
intro S

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst✝] (U i)
hsU : s ⊆ ⋃ i, U i
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → (∃ r, r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
S : Set (Set X)
⊢ S.Countable → (∀ s ∈ S, ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i) → ∃ r, r.Countable ∧ ⋃₀ S ⊆ ⋃ i ∈ r, U i
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: ι : 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
⊢ (univ.pi s ∩ (u ∩ v)).Nonempty

Tactic:
classical
  rcases exists_finset_piecewise_mem_of_mem_nhds (uo.mem_nhds hfu) g with ⟨I, hI⟩
  induction I using Finset.induction_on with
  | empty =>
    refine ⟨g, hgs, ⟨?_, hgv⟩⟩
    simpa using hI
  | insert i I _ ihI =>
    rw [Finset.piecewise_insert] at hI
    have := I.piecewise_mem_set_pi hfs hgs
    refine (hsuv this).elim ihI fun h => ?_
    set S := update (I.piecewise f g) i '' s i
    have hsub : S ⊆ pi univ s := by
      refine image_subset_iff.2 fun z hz => ?_
      rwa [update_preimage_univ_pi]
      exact fun j _ => this j trivial
    have hconn : IsPreconnected S :=
      (hs i).image _ (continuous_const.update i continuous_id).continuousOn
    have hSu : (S ∩ u).Nonempty := ⟨_, mem_image_of_mem _ (hfs _ trivial), hI⟩
    have hSv : (S ∩ v).Nonempty := ⟨_, ⟨_, this _ trivial, update_eq_self _ _⟩, h⟩
    refine (hconn u v uo vo (hsub.trans hsuv) hSu hSv).mono ?_
    exact inter_subset_inter_left _ hsub

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

Goal state before:
pp: case a
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
s : Set X
hs : IsCompact s
y : X
hy : y ∈ nhdsKer s
hy' : ∃ s_1 ∈ 𝓝ˢ s, ∃ t ∈ 𝓝 y, Disjoint s_1 t
⊢ False

Tactic:
obtain ⟨t, hts, t', ht'y, H⟩ := hy'

Goal state after:
case a
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
s : Set X
hs : IsCompact s
y : X
hy : y ∈ nhdsKer s
t : Set X
hts : t ∈ 𝓝ˢ s
t' : Set X
ht'y : t' ∈ 𝓝 y
H : Disjoint t t'
⊢ False
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Continuous[inst✝¹, inst✝] f
y : β
⊢ f ⁻¹' connectedComponent y = ⋃ x ∈ f ⁻¹' connectedComponent y, connectedComponent x

Tactic:
by
  simpa [connectedComponentIn_univ] using
    hf.continuousOn.preimage_connectedComponentIn (F := univ) y

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

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
⊢ ConnectedSpace α → ∃ x, connectedComponent x = univ

Tactic:
rintro ⟨⟨x⟩⟩

Goal state after:
case mp
α : Type u
inst✝ : TopologicalSpace α
toPreconnectedSpace✝ : PreconnectedSpace α
x : α
⊢ ∃ x, connectedComponent x = univ
Module: Mathlib.Topology.Connected.TotallyDisconnected

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
H : IsTotallySeparated s
⊢ IsTotallyDisconnected s

Tactic:
intro t hts ht x x_in y y_in
  by_contra h
  obtain
    ⟨u : Set α, v : Set α, hu : IsOpen u, hv : IsOpen v, hxu : x ∈ u, hyv : y ∈ v, hs : s ⊆ u ∪ v,
      huv⟩ :=
    H (hts x_in) (hts y_in) h
  refine (ht _ _ hu hv (hts.trans hs) ⟨x, x_in, hxu⟩ ⟨y, y_in, hyv⟩).ne_empty ?_
  rw [huv.inter_eq, inter_empty]

Goal state after:
Module: Mathlib.Data.Rel.Cover

Goal state before:
pp: X : Type u_1
U : SetRel X X
s N : Set X
inst✝¹ : U.IsRefl
inst✝ : U.IsSymm
hN : Maximal (fun N ↦ N ⊆ s ∧ U.IsSeparated N) N
⊢ U.IsCover s N

Tactic:
by
  rintro x hx
  by_contra! h
  simpa [U.rfl] using h _ <| hN.2 (y := insert x N) ⟨by simp [insert_subset_iff, hx, hN.1.1],
    hN.1.2.insert fun y hy hxy ↦ (h y hy hxy).elim⟩ (subset_insert _ _) (mem_insert _ _)

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

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : UniformSpace β
F : Filter (α × β)
⊢ Cauchy F ↔ Cauchy (map Prod.fst F) ∧ Cauchy (map Prod.snd F)

Tactic:
← cauchy_comap_uniformSpace,

Goal state after:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : UniformSpace β
F : Filter (α × β)
⊢ Cauchy F ↔ Cauchy F ∧ Cauchy F
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : UniformSpace β
f : Filter α
g : Filter β
hf : Cauchy f
hg : Cauchy g
this : f.NeBot
⊢ Cauchy (f ×ˢ g)

Tactic:
have := hg.1

Goal state after:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : UniformSpace β
f : Filter α
g : Filter β
hf : Cauchy f
hg : Cauchy g
this✝ : f.NeBot
this : g.NeBot
⊢ Cauchy (f ×ˢ g)
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: case right
α : Type u
uniformSpace : UniformSpace α
f : Filter α
x : α
hf : Cauchy f
adhs : ClusterPt x f
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set α
t_mem : t ∈ f
ht : t ×ˢ t ⊆ s
⊢ ∃ y, (x, y) ∈ s ∧ y ∈ t

Tactic:
exact forall_mem_nonempty_iff_neBot.2 adhs _ (inter_mem_inf (mem_nhds_left x hs) t_mem)

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

Goal state before:
pp: case mpr
β : Type ub
V W M : SetRel β β
inst✝ : W.IsSymm
x y : β
⊢ (ball (x, y).1 V ×ˢ ball (x, y).2 W ∩ M).Nonempty → (x, y) ∈ V ○ M ○ W

Tactic:
· rintro ⟨⟨w, z⟩, ⟨w_in, z_in⟩, hwz⟩
    rw [mem_ball_symmetry] at z_in
    exact ⟨z, ⟨w, w_in, hwz⟩, z_in⟩

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
s : Set α
U : SetRel α α
hs : Dense s
hU : U ∈ 𝓤 α
⊢ ⋃ x ∈ s, ball x U = univ

Tactic:
refine iUnion₂_eq_univ_iff.2 fun y => ?_
  rcases hs.inter_nhds_nonempty (mem_nhds_right y hU) with ⟨x, hxs, hxy : (x, y) ∈ U⟩
  exact ⟨x, hxs, hxy⟩

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
s t : Set α
⊢ TotallyBounded (s ∪ t) ↔ TotallyBounded s ∧ TotallyBounded t

Tactic:
rw [union_eq_iUnion, totallyBounded_iUnion]
  simp [and_comm]

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

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
s t : Set α
hst : s ⊆ t
⊢ comap (fun x ↦ (inclusion hst x.1, inclusion hst x.2)) (𝓤 ↑t) = 𝓤 ↑s

Tactic:
uniformity_subtype,

Goal state after:
α : Type u
inst✝ : UniformSpace α
s t : Set α
hst : s ⊆ t
⊢ comap (fun x ↦ (inclusion hst x.1, inclusion hst x.2)) (comap (fun q ↦ (↑q.1, ↑q.2)) (𝓤 α)) = 𝓤 ↑s
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
s t : Set α
hst : s ⊆ t
⊢ comap (fun x ↦ (inclusion hst x.1, inclusion hst x.2)) (comap (fun q ↦ (↑q.1, ↑q.2)) (𝓤 α)) = 𝓤 ↑s

Tactic:
uniformity_subtype,

Goal state after:
α : Type u
inst✝ : UniformSpace α
s t : Set α
hst : s ⊆ t
⊢ comap (fun x ↦ (inclusion hst x.1, inclusion hst x.2)) (comap (fun q ↦ (↑q.1, ↑q.2)) (𝓤 α)) =
    comap (fun q ↦ (↑q.1, ↑q.2)) (𝓤 α)
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 ((β × β') × β × β')
hu : u ∈ 𝓤 (β × β')
⊢ ∀ᶠ (m : (ι × ι') × ι × ι') in (p ×ˢ p') ×ˢ p ×ˢ p',
    ∀ x ∈ s ×ˢ s', ((fun i ↦ Prod.map (F i.1) (F' i.2)) m.1 x, (fun i ↦ Prod.map (F i.1) (F' i.2)) m.2 x) ∈ u

Tactic:
rw [uniformity_prod_eq_prod, mem_map, mem_prod_iff] at hu

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 ((β × β') × β × β')
hu : ∃ t₁ ∈ 𝓤 β, ∃ t₂ ∈ 𝓤 β', t₁ ×ˢ t₂ ⊆ (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' u
⊢ ∀ᶠ (m : (ι × ι') × ι × ι') in (p ×ˢ p') ×ˢ p ×ˢ p',
    ∀ x ∈ s ×ˢ s', ((fun i ↦ Prod.map (F i.1) (F' i.2)) m.1 x, (fun i ↦ Prod.map (F i.1) (F' i.2)) m.2 x) ∈ u
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
p : α → Prop
e : α → β
ue : IsUniformEmbedding e
de : IsDenseEmbedding e
⊢ comap (fun x ↦ (IsDenseEmbedding.subtypeEmb p e x.1, IsDenseEmbedding.subtypeEmb p e x.2))
      (𝓤 { x // x ∈ closure[inst✝.toTopologicalSpace] (e '' {x | p x}) }) =
    𝓤 { x // p x }

Tactic:
by
      simp [comap_comap, Function.comp_def, IsDenseEmbedding.subtypeEmb, uniformity_subtype,
        ue.comap_uniformity.symm]

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
K : Set α
ι : Sort u_2
U : ι → Set α
hK : IsCompact K
hopen : ∀ (i : ι), IsOpen[inst✝.toTopologicalSpace] (U i)
hcover : K ⊆ ⋃ i, U i
x : α
hx : x ∈ K
i : ι
hi : U i ∈ Filter.comap (Prod.mk x) ((𝓤 α).lift' fun s ↦ s ○ s)
⊢ ∃ i, ∃ V ∈ 𝓤 α, ball x (V ○ V) ⊆ U i

Tactic:
exact ⟨i, (((basis_sets _).lift' <| monotone_id.relComp monotone_id).comap _).mem_iff.1 hi⟩

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

Goal state before:
pp: case refine_2
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝¹ : (𝓤 α).IsCountablyGenerated
inst✝ : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
hts : ∀ (i : ℕ), (t i).IsSymm
x : α
V : Set α
hxV : x ∈ V
hVo : IsOpen[uniformSpace.toTopologicalSpace] V
U : Set (α × α)
hU : U ∈ 𝓤 α
hUV : ball x U ⊆ V
U' : Set (α × α)
hU' : U' ∈ 𝓤 α
left✝ : ∀ {a b : α}, (a, b) ∈ U' → (b, a) ∈ U'
hUU' : U' ○ U' ⊆ U
k : ℕ
hk : t k ⊆ U'
y : α
hxy : y ∈ ball x (t k)
hys : y ∈ s
z : α
hz : z ∈ ball y (t k)
⊢ z ∈ V

Tactic:
exact hUV (ball_subset_of_comp_subset (hk hxy) hUU' (hk hz))

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

Goal state before:
pp: case refine_2
X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst✝¹] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i ↦ mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := {i ∈ hnf.toFinset | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset | x ∉ U j}
⊢ ⋂ i ∈ is, U i ∈ 𝓝 x

pp: case refine_3
X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst✝¹] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i ↦ mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := {i ∈ hnf.toFinset | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset | x ∉ U j}
z : X
hz : z ∈ (n ∩ ⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i
⊢ (mulSupport fun i ↦ f i z) ⊆ ↑is

Tactic:
· exact (biInter_finset_mem is).mpr fun i hi => (ho i).mem_nhds (Finset.mem_filter.mp hi).2

Goal state after:
case refine_3
X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst✝¹] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i ↦ mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := {i ∈ hnf.toFinset | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset | x ∉ U j}
z : X
hz : z ∈ (n ∩ ⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i
⊢ (mulSupport fun i ↦ f i z) ⊆ ↑is
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst✝¹] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i ↦ mulSupport (f i)) i ∩ n).Nonempty}.Finite
⊢ ∃ is, ∃ n ∈ 𝓝 x, n ⊆ ⋂ i ∈ is, U i ∧ ∀ z ∈ n, (mulSupport fun i ↦ f i z) ⊆ ↑is

Tactic:
let is := {i ∈ hnf.toFinset | x ∈ U i}
    let js := {j ∈ hnf.toFinset | x ∉ U j}
    refine
      ⟨is, (n ∩ ⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i, inter_mem (inter_mem hn ?_) ?_,
        inter_subset_right, fun z hz => ?_⟩
    · exact (biInter_finset_mem js).mpr fun j hj => IsClosed.compl_mem_nhds (isClosed_mulTSupport _)
        (Set.notMem_subset (hso j) (Finset.mem_filter.mp hj).2)
    · exact (biInter_finset_mem is).mpr fun i hi => (ho i).mem_nhds (Finset.mem_filter.mp hi).2
    · have hzn : z ∈ n := by
        rw [inter_assoc] at hz
        exact mem_of_mem_inter_left hz
      replace hz := mem_of_mem_inter_right (mem_of_mem_inter_left hz)
      simp only [js, Finset.mem_filter, Finite.mem_toFinset, mem_ofPred_eq, mem_iInter,
        and_imp] at hz
      suffices (mulSupport fun i => f i z) ⊆ hnf.toFinset by
        refine hnf.toFinset.subset_coe_filter_of_subset_forall _ this fun i hi => ?_
        specialize hz i ⟨z, ⟨hi, hzn⟩⟩
        contrapose hz
        simp [hz, subset_mulTSupport (f i) hi]
      intro i hi
      simp only [Finite.coe_toFinset, mem_ofPred_eq]
      exact ⟨z, ⟨hi, hzn⟩⟩

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

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
h : ∀ u ∈ 𝓤 β, ∃ F, UniformContinuous F ∧ ∀ (y : α), (f y, F y) ∈ u
⊢ ∀ u ∈ 𝓤 β, ∃ F, UniformContinuousOn F univ ∧ ∀ y ∈ univ, (f y, F y) ∈ u

Tactic:
by simpa [uniformContinuousOn_univ] using h

Goal state after:
Module: Mathlib.Algebra.Order.Group.MinMax

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ min (a / c) (b / c) = min a b / c

Tactic:
simpa only [div_eq_mul_inv] using min_mul_mul_right a b c⁻¹

Goal state after:
Module: Mathlib.Algebra.Order.Group.MinMax

Goal state before:
pp: case refine_1
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ max a b - max c d ≤ max |a - c| |b - d|

pp: case refine_2
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ max c d - max a b ≤ max |a - c| |b - d|

Tactic:
· exact (max_sub_max_le_max _ _ _ _).trans (max_le_max (le_abs_self _) (le_abs_self _))

Goal state after:
case refine_2
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ max c d - max a b ≤ max |a - c| |b - d|
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: case mpr
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
x₀ : X
hx₀ : x₀ ∈ S
H : ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ ∀ᶠ (x : X) in 𝓝[S] x₀, ∀ (i : ι), (F i x₀, F i x) ∈ U

Tactic:
· rcases H U hU with ⟨V, hV, hVU⟩
    filter_upwards [hV] using fun x hx i => hVU x₀ (mem_of_mem_nhdsWithin hx₀ hV) x hx i

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : TopologicalSpace α
f : α →ᵤ[𝔖] β
x : α
h𝔖 : ∃ V ∈ 𝔖, V ∈ 𝓝 x
hc : ContinuousAt ((toFun 𝔖) f) x
⊢ Tendsto (Prod.mk ((toFun 𝔖) (f, x).1 (f, x).2) ∘ fun fx ↦ (toFun 𝔖) fx.1 fx.2) (𝓝 (f, x)) (𝓤 β)

Tactic:
← lift'_comp_uniformity,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : TopologicalSpace α
f : α →ᵤ[𝔖] β
x : α
h𝔖 : ∃ V ∈ 𝔖, V ∈ 𝓝 x
hc : ContinuousAt ((toFun 𝔖) f) x
⊢ Tendsto (Prod.mk ((toFun 𝔖) (f, x).1 (f, x).2) ∘ fun fx ↦ (toFun 𝔖) fx.1 fx.2) (𝓝 (f, x))
    ((𝓤 β).lift' fun s ↦ s.comp s)
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
f : Filter α
s : Set α
hs : s ∈ f
⊢ s⁻¹⁻¹ ∈ f

Tactic:
inv_inv

Goal state after:
α : Type u_2
inst✝ : InvolutiveInv α
f : Filter α
s : Set α
hs : s ∈ f
⊢ s ∈ f
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
f g : Filter α
⊢ f⁻¹⁻¹ ≤ g⁻¹ ↔ f ≤ g⁻¹

Tactic:
inv_inv

Goal state after:
α : Type u_2
inst✝ : InvolutiveInv α
f g : Filter α
⊢ f ≤ g⁻¹ ↔ f ≤ g⁻¹
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
⊢ IsUniformInducing ⇑(Equiv.piComm fun a ↦ δ)

Tactic:
by
    constructor
    change comap (Prod.map Function.swap Function.swap) _ = _
    erw [← uniformity_comap]
    congr
    rw [Pi.uniformSpace, UniformSpace.ofCoreEq_toCore, Pi.uniformSpace,
      UniformSpace.ofCoreEq_toCore, UniformSpace.comap_iInf, UniformOnFun.iInf_eq]
    refine iInf_congr fun i => ?_
    rw [← UniformSpace.comap_comap, UniformOnFun.comap_eq]
    rfl

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

Goal state before:
pp: G₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a : G₀
ha : 0 < a
⊢ Ioi a = Ioi a⁻¹⁻¹

Tactic:
inv_inv

Goal state after:
G₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a : G₀
ha : 0 < a
⊢ Ioi a = Ioi a
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a c : α
h : c < 0
⊢ (fun x ↦ c * x) ⁻¹' Ici a = Iic (a / c)

Tactic:
by
  simpa only [mul_comm] using preimage_mul_const_Ici_of_neg a h

Goal state after: