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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
⊢ LocallyConnectedSpace α ↔ ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst✝] V ∧ x ∈ V ∧ IsConnected V

Tactic:
simp_rw [locallyConnectedSpace_iff_hasBasis_isOpen_isConnected]
  refine forall_congr' fun _ => ?_
  constructor
  · intro h U hU
    rcases h.mem_iff.mp hU with ⟨V, hV, hVU⟩
    exact ⟨V, hVU, hV⟩
  · exact fun h => ⟨fun U => ⟨fun hU =>
      let ⟨V, hVU, hV⟩ := h U hU
      ⟨V, hV, hVU⟩, fun ⟨V, ⟨hV, hxV, _⟩, hVU⟩ => mem_nhds_iff.mpr ⟨V, hVU, hV, hxV⟩⟩⟩

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun i j ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
⊢ IsPreconnected (⋃ n ∈ t, s n)

Tactic:
by
  let R := fun i j : ι => (s i ∩ s j).Nonempty ∧ i ∈ t
  have P : ∀ i, i ∈ t → ∀ j, j ∈ t → ReflTransGen R i j →
      ∃ p, p ⊆ t ∧ i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ j ∈ p, s j) := fun i hi j hj h => by
    induction h with
    | refl =>
      refine ⟨{i}, singleton_subset_iff.mpr hi, mem_singleton i, mem_singleton i, ?_⟩
      rw [biUnion_singleton]
      exact H i hi
    | @tail j k _ hjk ih =>
      obtain ⟨p, hpt, hip, hjp, hp⟩ := ih hjk.2
      refine ⟨insert k p, insert_subset_iff.mpr ⟨hj, hpt⟩, mem_insert_of_mem k hip,
        mem_insert k p, ?_⟩
      rw [biUnion_insert]
      refine (H k hj).union' (hjk.1.mono ?_) hp
      rw [inter_comm]
      exact inter_subset_inter_right _ (subset_biUnion_of_mem hjp)
  refine isPreconnected_of_forall_pair ?_
  intro x hx y hy
  obtain ⟨i : ι, hi : i ∈ t, hxi : x ∈ s i⟩ := mem_iUnion₂.1 hx
  obtain ⟨j : ι, hj : j ∈ t, hyj : y ∈ s j⟩ := mem_iUnion₂.1 hy
  obtain ⟨p, hpt, hip, hjp, hp⟩ := P i hi j hj (K i hi j hj)
  exact ⟨⋃ j ∈ p, s j, biUnion_subset_biUnion_left hpt, mem_biUnion hip hxi,
    mem_biUnion hjp hyj, hp⟩

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

Goal state before:
pp: case refine_2
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
⊢ IsEmpty ((i : ι) → X i) ∨ (∀ (i : ι), LocallyConnectedSpace (X i)) ∧ {i | ¬PreconnectedSpace (X i)}.Finite →
    LocallyConnectedSpace ((i : ι) → X i)

Tactic:
· rintro (he | ⟨hloc, hfin⟩)
    · exact ⟨he.elim⟩
    · exact locallyConnectedSpace_of_finite_not_preconnectedSpace hfin

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

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
⊢ LocallyConnectedSpace ((i : ι) → X i) ↔
    IsEmpty ((i : ι) → X i) ∨ (∀ (i : ι), LocallyConnectedSpace (X i)) ∧ {i | ¬PreconnectedSpace (X i)}.Finite

Tactic:
by
  refine ⟨fun h ↦ ?_, ?_⟩
  · rcases isEmpty_or_nonempty (∀ i, X i) with he | hne
    · exact .inl he
    obtain ⟨x⟩ := hne
    classical
    have : ∀ i, Nonempty (X i) := Classical.nonempty_pi.mp ⟨x⟩
    refine .inr ⟨fun i ↦ ((isOpenMap_eval i).isQuotientMap (continuous_apply i)
      (Function.surjective_eval i)).locallyConnectedSpace, ?_⟩
    have hVn : connectedComponent x ∈ 𝓝 x :=
      isOpen_connectedComponent.mem_nhds mem_connectedComponent
    rw [nhds_pi, Filter.mem_pi] at hVn
    obtain ⟨J, hJ, t, ht, htV⟩ := hVn
    refine hJ.subset fun i hi ↦ by_contra fun hiJ ↦ hi ?_
    suffices himg : Function.eval i '' connectedComponent x = univ from
      ⟨himg ▸ isPreconnected_connectedComponent.image _ (continuous_apply i).continuousOn⟩
    refine (subset_univ _).antisymm fun z _ ↦ ⟨Function.update x i z, htV fun j hj ↦ ?_, by simp⟩
    rw [Function.update_of_ne (ne_of_mem_of_not_mem hj hiJ)]
    exact mem_of_mem_nhds (ht j)
  · rintro (he | ⟨hloc, hfin⟩)
    · exact ⟨he.elim⟩
    · exact locallyConnectedSpace_of_finite_not_preconnectedSpace hfin

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

Goal state before:
pp: case refine_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
hs : IsPreconnected s
hinj : Injective f
hf : IsOpenMap f
u v : Set α
hu : IsOpen[inst✝¹] u
hv : IsOpen[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ (s ∩ f '' u).Nonempty

Tactic:
simpa only [image_preimage_inter] using hsu.image f

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

Goal state before:
pp: case refine_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsClosedMap f
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ (s ∩ f '' u).Nonempty

Tactic:
simpa only [image_preimage_inter] using hsu.image f

Goal state after:
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
i : ι
I : Finset ι
a✝ : i ∉ I
ihI : I.piecewise f g ∈ u → (univ.pi s ∩ (u ∩ v)).Nonempty
hI : update (I.piecewise f g) i (f i) ∈ u
this : I.piecewise f g ∈ univ.pi s
h : I.piecewise f g ∈ v
S : Set ((a : ι) → X a) := update (I.piecewise f g) i '' s i
⊢ S ⊆ univ.pi s

Tactic:
refine image_subset_iff.2 fun z hz => ?_

Goal state after:
ι : 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
i : ι
I : Finset ι
a✝ : i ∉ I
ihI : I.piecewise f g ∈ u → (univ.pi s ∩ (u ∩ v)).Nonempty
hI : update (I.piecewise f g) i (f i) ∈ u
this : I.piecewise f g ∈ univ.pi s
h : I.piecewise f g ∈ v
S : Set ((a : ι) → X a) := update (I.piecewise f g) i '' s i
z : X i
hz : z ∈ s i
⊢ z ∈ update (I.piecewise f g) i ⁻¹' univ.pi s
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)
⊢ IsPreconnected (univ.pi s)

Tactic:
rintro u v uo vo hsuv ⟨f, hfs, hfu⟩ ⟨g, hgs, hgv⟩
  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.Connected.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
F : Set β
hf : ContinuousOn f (f ⁻¹' F)
y : β
⊢ f ⁻¹' connectedComponentIn F y = ⋃ x ∈ f ⁻¹' connectedComponentIn F y, connectedComponentIn (f ⁻¹' F) x

Tactic:
refine subset_antisymm (fun z hz ↦ ?_) (iUnion₂_subset fun x hx z hz ↦ ?_)
  · exact mem_biUnion hz (mem_connectedComponentIn (connectedComponentIn_subset F y hz))
  · rw [mem_preimage, connectedComponentIn_eq hx]
    exact connectedComponentIn_mono _ (image_preimage_subset f F)
      (hf.mapsTo_connectedComponentIn (connectedComponentIn_subset F y hx) hz)

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : PreconnectedSpace ↑s
⊢ IsPreconnected s

Tactic:
simpa using isPreconnected_univ.image ((↑) : s → α) continuous_subtype_val.continuousOn

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

Goal state before:
pp: X : Type u
inst✝³ : TopologicalSpace X
inst✝² : LindelofSpace X
f : Filter X
inst✝¹ : f.NeBot
inst✝ : CountableInterFilter f
⊢ ∃ x, ClusterPt x f

Tactic:
by
  simpa using isLindelof_univ (show f ≤ 𝓟 univ by simp)

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

Goal state before:
pp: α : Type u_3
inst✝ : TopologicalSpace α
⊢ TotallySeparatedSpace α ↔ Pairwise fun x1 x2 ↦ ∃ U, IsClopen U ∧ x1 ∈ U ∧ x2 ∈ Uᶜ

Tactic:
simp only [totallySeparatedSpace_iff, IsTotallySeparated, Set.Pairwise, mem_univ, true_implies]

Goal state after:
α : Type u_3
inst✝ : TopologicalSpace α
⊢ (∀ ⦃x y : α⦄, x ≠ y → ∃ u v, IsOpen[inst✝] u ∧ IsOpen[inst✝] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v) ↔
    Pairwise fun x1 x2 ↦ ∃ U, IsClopen U ∧ x1 ∈ U ∧ x2 ∈ Uᶜ
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
a b : X
ne : connectedComponent a ≠ connectedComponent b
h : connectedComponent a ∩ ⋂ s, ↑s = ∅
fin_a : Finset { s // IsClopen s ∧ b ∈ s }
ha : connectedComponent a ∩ ⋂ i ∈ fin_a, ↑i = ∅
⊢ ∃ U V, IsClopen U ∧ connectedComponent a ∩ U = ∅ ∧ connectedComponent b ⊆ U ∧ mk ⁻¹' V = U

Tactic:
set U : Set X := ⋂ (i : { s // IsClopen s ∧ b ∈ s }) (_ : i ∈ fin_a), i

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
a b : X
ne : connectedComponent a ≠ connectedComponent b
h : connectedComponent a ∩ ⋂ s, ↑s = ∅
fin_a : Finset { s // IsClopen s ∧ b ∈ s }
U : Set X := ⋂ i ∈ fin_a, ↑i
ha : connectedComponent a ∩ U = ∅
⊢ ∃ U V, IsClopen U ∧ connectedComponent a ∩ U = ∅ ∧ connectedComponent b ⊆ U ∧ mk ⁻¹' V = U
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s : Set X
hs : IsOpen[inst✝¹] s
hne : s.Nonempty
h : IsMeagre s
⊢ ?m.17 ∈ residual X

Tactic:
by rwa [IsMeagre] at h

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:
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.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
S : Set α := ⋃ i, s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : l.NeBot
hl' : ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s
⊢ ∃ t ⊆ S, t ∈ l ∧ t ×ˢ t ⊆ U

Tactic:
by
    rcases hl' U hU with ⟨t, htl, htU⟩
    refine ⟨t ∩ S, inter_subset_right, inter_mem htl hls, Subset.trans ?_ htU⟩
    gcongr <;> apply inter_subset_left

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

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
⊢ UniformContinuousOn f s ↔ UniformContinuous (s.domRestrict f)

Tactic:
delta UniformContinuousOn UniformContinuous

Goal state after:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
⊢ Tendsto (fun x ↦ (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 (s ×ˢ s)) (𝓤 β) ↔
    Tendsto (fun x ↦ (s.domRestrict f x.1, s.domRestrict f x.2)) (𝓤 ↑s) (𝓤 β)
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set ((α × β) × α × β)
h : s ∈ 𝓤 (α × β)
⊢ ∃ u ∈ 𝓤 α, ∃ v ∈ 𝓤 β, entourageProd u v ⊆ s

Tactic:
by
  rcases (((𝓤 α).basis_sets.uniformity_prod (𝓤 β).basis_sets).mem_iff' s).1 h with ⟨w, hw⟩
  use w.1, hw.1.1, w.2, hw.1.2, hw.2

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n ↦ F n x) p (𝓝 (f x))
h✝ : p.NeBot
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : SetRel.comp t t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n ↦ F n x.2) p (𝓝 (f x.2))
⊢ ∀ᶠ (y : α × ι) in p' ×ˢ p, (f y.swap.2, F y.swap.1 y.swap.2) ∈ u

Tactic:
have := tendsto_prodAssoc.eventually (tendsto_prod_swap.eventually ((hF t ht).and hmc))

Goal state after:
case inr
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n ↦ F n x) p (𝓝 (f x))
h✝ : p.NeBot
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : SetRel.comp t t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n ↦ F n x.2) p (𝓝 (f x.2))
this :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F ((Equiv.prodAssoc α ι ι) x).swap.1.1 ((Equiv.prodAssoc α ι ι) x).swap.2,
          F ((Equiv.prodAssoc α ι ι) x).swap.1.2 ((Equiv.prodAssoc α ι ι) x).swap.2) ∈
        t ∧
      Tendsto (fun n ↦ F n ((Equiv.prodAssoc α ι ι) x).swap.2) p (𝓝 (f ((Equiv.prodAssoc α ι ι) x).swap.2))
⊢ ∀ᶠ (y : α × ι) in p' ×ˢ p, (f y.swap.2, F y.swap.1 y.swap.2) ∈ u
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
x : α ⊕ β
s✝ : Set (α ⊕ β)
⊢ s✝ ∈ 𝓝 x ↔ s✝ ∈ comap (Prod.mk x) (map (fun p ↦ (inl p.1, inl p.2)) (𝓤 α) ⊔ map (fun p ↦ (inr p.1, inr p.2)) (𝓤 β))

Tactic:
cases x <;> simp [mem_comap', -mem_comap, nhds_inl, nhds_inr, nhds_eq_comap_uniformity,
      Prod.ext_iff]

Goal state after:
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)))
⊢ (∀ (f : Filter β), Cauchy f → f ≤ 𝓟 (m '' s) → ∃ x ∈ m '' s, f ≤ 𝓝 x) ↔
    ∀ (f : Filter α), Cauchy f → f ≤ 𝓟 s → ∃ x ∈ s, f ≤ 𝓝 x

Tactic:
imp.swap (a := Cauchy _),

Goal state after:
α : 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)))
⊢ (∀ f ≤ 𝓟 (m '' s), Cauchy f → ∃ x ∈ m '' s, f ≤ 𝓝 x) ↔ ∀ f ≤ 𝓟 s, Cauchy f → ∃ x ∈ s, f ≤ 𝓝 x
Module: Mathlib.Topology.Algebra.Support

Goal state before:
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:
have hzn : z ∈ n := by
        rw [inter_assoc] at hz
        exact mem_of_mem_inter_left hz

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
hzn : z ∈ n
⊢ (mulSupport fun i ↦ f i z) ⊆ ↑is
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
inst✝ : (𝓤 α).IsCountablyGenerated
hs : ∀ U ∈ 𝓤 α, ∃ t, t.Countable ∧ ⋃ x ∈ t, ball x U = univ
this : ∀ U ∈ 𝓤 α, ∃ t, t.Countable ∧ univ ⊆ ⋃ x ∈ t, ball x U
t : Set α
htc : t.Countable
ht : univ ⊆ closure[uniformSpace.toTopologicalSpace] t
⊢ SeparableSpace α

Tactic:
exact ⟨⟨t, htc, fun x => ht (mem_univ x)⟩⟩

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
inst✝ : (𝓤 α).IsCountablyGenerated
s : Set α
h : TotallyBounded s
U : Set (α × α)
hU : U ∈ 𝓤 α
t : Set α
ht : t.Finite
hst : s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ SetRel.inv U}
⊢ ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, ball x U

Tactic:
exact ⟨t, ht.countable, hst⟩

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 : α → β
p : Filter ι
S : Set (Set α)
hS : ∀ s ∈ S, IsOpen[inst✝¹] s
h : ∀ s ∈ S, TendstoLocallyUniformlyOn F f p s
⊢ TendstoLocallyUniformlyOn F f p (⋃₀ S)

Tactic:
rw [sUnion_eq_biUnion]
  exact tendstoLocallyUniformlyOn_biUnion hS h

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
⊢ Function.LeftInverse g ⇑f

Tactic:
by convert! f.left_inv

Goal state after:
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:
by
  rw [equicontinuousAt_iff_continuousAt, ContinuousAt,
    (UniformFun.hasBasis_nhds_of_basis ι α _ hα).tendsto_right_iff]
  rfl

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

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

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

Goal state after:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set X
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → X → α
x₀ : X
hX : (𝓝 x₀).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
⊢ (∀ (ib : κ₂),
      p₂ ib →
        ∃ ia, p₁ ia ∧ ∀ x ∈ s₁ ia, (⇑ofFun ∘ swap F) x ∈ {g | ((⇑ofFun ∘ swap F) x₀, g) ∈ UniformFun.gen ι α (s₂ ib)}) ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x ∈ s₁ k₁, ∀ (i : ι), (F i x₀, F i x) ∈ s₂ k₂
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₂ (fun a b ↦ m b (n a)) g f = 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 a (n b)) f g = map₂ (fun a b ↦ m a (n b)) f g
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: case refine_2
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : δ → γ → ε
n : α → β → δ
m₁ : α → γ → α'
m₂ : β → γ → β'
n' : α' → β' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m₁ a c) (m₂ b c)
s : Set ε
t₁ : Set α'
u : Set α
hu : u ∈ f
w₁ : Set γ
hw₁ : w₁ ∈ h
ht₁ : image2 m₁ u w₁ ⊆ t₁
t₂ : Set β'
hs : image2 n' t₁ t₂ ⊆ s
v : Set β
hv : v ∈ g
w₂ : Set γ
hw₂ : w₂ ∈ h
ht₂ : image2 m₂ v w₂ ⊆ t₂
⊢ image2 m₂ v (w₁ ∩ w₂) ⊆ t₂

Tactic:
exact (image2_subset_left inter_subset_right).trans ht₂

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c : α
⊢ Icc (a - max b c) (a - min b c) = Icc (min (a - b) (a - c)) (max (a - b) (a - c))

Tactic:
simp only [sub_eq_add_neg, min_add_add_left, max_add_add_left, min_neg_neg, max_neg_neg]

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

Goal state before:
pp: Γ : Type u_4
inst✝³ : Group Γ
T : Type u_5
inst✝² : TopologicalSpace T
inst✝¹ : MulAction Γ T
inst✝ : ContinuousConstSMul Γ T
U : Set T
hU : IsOpen[inst✝²] U
⊢ IsOpen[instTopologicalSpaceQuotient] (Quotient.mk' '' U)

Tactic:
isOpen_coinduced,

Goal state after:
Γ : Type u_4
inst✝³ : Group Γ
T : Type u_5
inst✝² : TopologicalSpace T
inst✝¹ : MulAction Γ T
inst✝ : ContinuousConstSMul Γ T
U : Set T
hU : IsOpen[inst✝²] U
⊢ IsOpen[inst✝²] (Quotient.mk' ⁻¹' Quotient.mk' '' U)
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
l : Filter (M × M)
hl : Disjoint l (cocompact (M × M))
⊢ Tendsto (fun x ↦ x.1 * x.2) ((𝓝 0).coprod (𝓝 0) ⊓ l) (𝓝 0)

Tactic:
by
  have := calc
    (𝓝 0).coprod (𝓝 0) ⊓ l
    _ ≤ (𝓝 0).coprod (𝓝 0) ⊓ map Prod.fst l ×ˢ map Prod.snd l :=
      inf_le_inf_left _ le_prod_map_fst_snd
    _ ≤ 𝓝 0 ×ˢ map Prod.snd l ⊔ map Prod.fst l ×ˢ 𝓝 0 :=
      coprod_inf_prod_le _ _ _ _
  apply (Tendsto.sup _ _).mono_left this
  · apply tendsto_mul_nhds_zero_prod_of_disjoint_cocompact
    exact disjoint_map_cocompact continuous_snd hl
  · apply tendsto_mul_prod_nhds_zero_of_disjoint_cocompact
    exact disjoint_map_cocompact continuous_fst hl

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f✝ : ι → α → M
x : Filter α
a : ι → M
f : ι
l : List ι
h : ∀ i ∈ f :: l, Tendsto (f✝ i) x (𝓝 (a i))
⊢ Tendsto (fun b ↦ (List.map (fun c ↦ f✝ c b) (f :: l)).prod) x (𝓝 (List.map a (f :: l)).prod)

Tactic:
simp only [List.map_cons, List.prod_cons]
    exact
      (h f List.mem_cons_self).mul
        (tendsto_list_prod l fun c hc => h c (List.mem_cons_of_mem _ hc))

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
U : Set G
hU : U ∈ 𝓝 1
V : Set G
V_open : IsOpen[inst✝²] V
V_mem : 1 ∈ V
hV : V * V ⊆ U
⊢ ∃ V ∈ 𝓝 1, IsClosed[inst✝²] V ∧ V⁻¹ = V ∧ V * V ⊆ U

Tactic:
rcases exists_mem_nhds_isClosed_subset (V_open.mem_nhds V_mem) with ⟨W, W_mem, W_closed, hW⟩

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
U : Set G
hU : U ∈ 𝓝 1
V : Set G
V_open : IsOpen[inst✝²] V
V_mem : 1 ∈ V
hV : V * V ⊆ U
W : Set G
W_mem : W ∈ 𝓝 1
W_closed : IsClosed[inst✝²] W
hW : W ⊆ V
⊢ ∃ V ∈ 𝓝 1, IsClosed[inst✝²] V ∧ V⁻¹ = V ∧ V * V ⊆ U