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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
S : Set (Set α)
K : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) S
H : ∀ s ∈ S, IsPreconnected s
u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
Huv : ⋃₀ S ⊆ u ∪ v
a : α
hau : a ∈ u
s : Set α
hsS : s ∈ S
has : a ∈ s
b : α
hbv : b ∈ v
t : Set α
htS : t ∈ S
hbt : b ∈ t
r : Set α
hrS : r ∈ S
hsr : s ⊆ r
htr : t ⊆ r
⊢ (⋃₀ S ∩ (u ∩ v)).Nonempty

Tactic:
have Hnuv : (r ∩ (u ∩ v)).Nonempty :=
    H _ hrS u v hu hv ((subset_sUnion_of_mem hrS).trans Huv) ⟨a, hsr has, hau⟩ ⟨b, htr hbt, hbv⟩

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
S : Set (Set α)
K : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) S
H : ∀ s ∈ S, IsPreconnected s
u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
Huv : ⋃₀ S ⊆ u ∪ v
a : α
hau : a ∈ u
s : Set α
hsS : s ∈ S
has : a ∈ s
b : α
hbv : b ∈ v
t : Set α
htS : t ∈ S
hbt : b ∈ t
r : Set α
hrS : r ∈ S
hsr : s ⊆ r
htr : t ⊆ r
Hnuv : (r ∩ (u ∩ v)).Nonempty
⊢ (⋃₀ S ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.Connected.Clopen

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

Tactic:
obtain rfl | h := s.eq_empty_or_nonempty
    · exact ⟨Classical.choice hι, ∅, isPreconnected_empty, (Set.image_empty _).symm⟩
    · obtain ⟨a, t, ht, rfl⟩ := Sigma.isConnected_iff.1 ⟨h, hs⟩
      exact ⟨a, t, ht.isPreconnected, rfl⟩

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

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

Tactic:
← not_disjoint_iff_nonempty_inter,

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

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

Tactic:
← not_disjoint_iff_nonempty_inter,

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

Goal state before:
pp: α : Type u
ι : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
inst✝ : Finite ι
h_closed : ∀ (i : ι), IsClosed[inst✝²] (s i)
h_Union : ⋃ i, s i = univ
⊢ Subsingleton ι

Tactic:
by
  refine subsingleton_of_disjoint_isClopen h_nonempty h_disj (fun i ↦ ⟨h_closed i, ?_⟩)
  rw [← isClosed_compl_iff, compl_eq_univ_sdiff, ← h_Union, iUnion_sdiff]
  refine isClosed_iUnion_of_finite (fun j ↦ ?_)
  rcases eq_or_ne i j with rfl | h_ne
  · simp
  · simpa only [(h_disj h_ne.symm).sdiff_eq_left] using h_closed j

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

Goal state before:
pp: X : Type u_3
T : Set (TopologicalSpace X)
h : ∀ t ∈ T, RegularSpace X
x✝ : TopologicalSpace X := sInf T
a : X
⊢ (⨅ i, 𝓝 a).HasBasis (fun If ↦ If.fst.Finite ∧ ∀ (i : ↑If.fst), If.snd i ∈ 𝓝 a ∧ IsClosed[↑↑i] (If.snd i)) fun If ↦
    ⋂ i, If.snd i

Tactic:
exact .iInf fun t : T => @closed_nhds_basis X t (h t t.2) a

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

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

Tactic:
exact mem_biUnion hz (mem_connectedComponentIn (connectedComponentIn_subset F y hz))

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : ConnectedSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Surjective f
hf' : Continuous[inst✝², inst✝] f
⊢ ConnectedSpace β

Tactic:
by
  rw [connectedSpace_iff_univ, ← hf.range_eq]
  exact isConnected_range hf'

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

Goal state before:
pp: case mpr
α : Type u
inst✝ : TopologicalSpace α
x : α
h : connectedComponent x = univ
this : PreconnectedSpace α
⊢ ConnectedSpace α

Tactic:
exact ⟨⟨x⟩⟩

Goal state after:
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
inst✝ : T2Space β
di : IsDenseInducing i
hd : Dense (range i)ᶜ
s : Set α
hs : IsCompact s
⊢ interior s = ∅

Tactic:
refine eq_empty_iff_forall_notMem.2 fun x hx => ?_
  rw [mem_interior_iff_mem_nhds] at hx
  have := di.closure_image_mem_nhds hx
  rw [(hs.image di.continuous).isClosed.closure_eq] at this
  rcases hd.inter_nhds_nonempty this with ⟨y, hyi, hys⟩
  exact hyi (image_subset_range _ _ hys)

Goal state after:
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
e : α → β
de : IsDenseEmbedding e
p : α → Prop
⊢ closure[instTopologicalSpaceSubtype] (range (subtypeEmb p e)) = univ

Tactic:
ext ⟨x, hx⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
e : α → β
de : IsDenseEmbedding e
p : α → Prop
x : β
hx : x ∈ closure[inst✝] (e '' {x | p x})
⊢ ⟨x, hx⟩ ∈ closure[instTopologicalSpaceSubtype] (range (subtypeEmb p e)) ↔ ⟨x, hx⟩ ∈ univ
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
hs : IsClosed[inst✝²] (⋂ s, ↑s)
a b : Set X
ha : IsClosed[inst✝²] a
hb : IsClosed[inst✝²] b
hab : ⋂ s, ↑s ⊆ a ∪ b
ab_disj : Disjoint a b
u v : Set X
hu : IsOpen[inst✝²] u
hv : IsOpen[inst✝²] v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
H1 : (∀ (u_1 : Finset { s // IsClopen s ∧ x ∈ s }), ((u ∪ v)ᶜ ∩ ⋂ i ∈ u_1, ↑i).Nonempty) → ((u ∪ v)ᶜ ∩ ⋂ i, ↑i).Nonempty
⊢ ∃ s, IsClopen s ∧ x ∈ s ∧ s ⊆ u ∪ v

Tactic:
← not_disjoint_iff_nonempty_inter,

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
hs : IsClosed[inst✝²] (⋂ s, ↑s)
a b : Set X
ha : IsClosed[inst✝²] a
hb : IsClosed[inst✝²] b
hab : ⋂ s, ↑s ⊆ a ∪ b
ab_disj : Disjoint a b
u v : Set X
hu : IsOpen[inst✝²] u
hv : IsOpen[inst✝²] v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
H1 : (∀ (u_1 : Finset { s // IsClopen s ∧ x ∈ s }), ((u ∪ v)ᶜ ∩ ⋂ i ∈ u_1, ↑i).Nonempty) → ¬Disjoint (u ∪ v)ᶜ (⋂ i, ↑i)
⊢ ∃ s, IsClopen s ∧ x ∈ s ∧ s ⊆ u ∪ v
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
ι' : Sort u_4
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι'
T : ι' → Set (Set X)
hTo : ∀ (i : ι'), ∀ t ∈ T i, IsOpen[inst✝¹] t
hTc : ∀ (i : ι'), (T i).Countable
hTs : ∀ (i : ι'), (fun i ↦ ⋂₀ T i) i = ⋂₀ T i
⊢ ∀ t ∈ ⋃ i, T i, IsOpen[inst✝¹] t

Tactic:
simpa [@forall_comm ι'] using hTo

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hS : S.Finite
h : ∀ s ∈ S, IsGδ s
⊢ IsGδ (⋃₀ S)

Tactic:
by
  induction S, hS using Set.Finite.induction_on with
  | empty => simp
  | insert _ _ ih =>
    simp only [forall_mem_insert, sUnion_insert] at *
    exact h.1.union (ih h.2)

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

Goal state before:
pp: case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ S, (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S) →
    ∃ x, (∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed[inst✝] x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable ∧ s ⊆ ⋃₀ x

Tactic:
intro ⟨S, hS, hc, hsub⟩
    use closure '' S
    rw [forall_mem_image]
    exact ⟨fun s hs ↦ ⟨isClosed_closure, (hS s hs).closure⟩,
      (hc.image _).image _, hsub.trans (sUnion_mono_subsets fun s ↦ subset_closure)⟩

Goal state after:
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
S : Set (Set X)
ho : ∀ s ∈ S, IsOpen[inst✝¹] s
hS : S.Countable
hd : ∀ s ∈ S, Dense s
⊢ Dense (⋂₀ S)

Tactic:
rcases S.eq_empty_or_nonempty with h | h

Goal state after:
case inl
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
S : Set (Set X)
ho : ∀ s ∈ S, IsOpen[inst✝¹] s
hS : S.Countable
hd : ∀ s ∈ S, Dense s
h : S = ∅
⊢ Dense (⋂₀ S)

case inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
S : Set (Set X)
ho : ∀ s ∈ S, IsOpen[inst✝¹] s
hS : S.Countable
hd : ∀ s ∈ S, Dense s
h : S.Nonempty
⊢ Dense (⋂₀ S)
Module: Mathlib.Topology.Algebra.Constructions

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : Monoid M
inst✝¹ : TopologicalSpace N
inst✝ : Monoid N
f : M →* N
hf : IsInducing ⇑f
⊢ IsInducing ⇑(map f)

Tactic:
refine .of_comp (continuous_map hf.continuous) continuous_embedProduct ?_
  exact hf.prodMap (opHomeomorph.isInducing.comp <| hf.comp opHomeomorph.symm.isInducing)
    |>.comp isInducing_embedProduct

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

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : Infinite (ConnectedComponents α)
n : ℕ
hn : 0 < n
⊢ ∃ U, (∀ (i : Fin n), IsClopen (U i)) ∧ (∀ (i : Fin n), (U i).Nonempty) ∧ Pairwise (Disjoint on U) ∧ ⋃ i, U i = univ

Tactic:
by
  cases isEmpty_or_nonempty α
  · exact (not_finite (ConnectedComponents α)).elim
  obtain (_ | n) := n
  · simp at hn
  clear hn
  induction n with
  | zero => exact ⟨![.univ], by simp [isClopen_univ, Set.iUnion_fin_add_one_eq_iUnion_succ]⟩
  | succ n IH =>
    obtain ⟨U, h₁, h₂, h₃, h₄⟩ := IH
    obtain ⟨i, hi⟩ : ∃ i, ¬ IsConnected (U i) := by
      simp_rw [isConnected_iff_connectedSpace, ← not_forall]
      exact fun _ ↦ not_finite_iff_infinite.mpr ‹_› (.of_equiv _ (equivOfIsClopen h₁ h₃ h₄).symm)
    obtain ⟨U, rfl⟩ := (Equiv.piCongrLeft (fun _ ↦ Set α) (Equiv.swap 0 i)).symm.surjective U
    cases U using Fin.consCases with | cons s U =>
    simp only [Equiv.piCongrLeft_symm_apply, Equiv.swap_apply_right, Fin.cons_zero] at *
    obtain ⟨a, b, ha, hb, ha', hb', hab, rfl⟩ := (show IsClopen s by simpa using h₁ i)
      |>.not_isPreconnected_iff.mp (mt (⟨by simpa using h₂ i, ·⟩) hi)
    refine ⟨Fin.cons a (Fin.cons b U), ?_, ?_, ?_, ?_⟩
    · simpa [Fin.forall_iff_succ, *] using fun x ↦ h₁ (Equiv.swap 0 i (.succ x))
    · simpa [Fin.forall_iff_succ, *] using fun x ↦ h₂ (Equiv.swap 0 i (.succ x))
    · have h₃' (j : _) : Disjoint (U j) a ∧ Disjoint (U j) b := by
        simpa [onFun] using h₃ ((Equiv.swap 0 i).injective.ne (Fin.succ_ne_zero j))
      simpa [Pairwise, Fin.forall_iff_succ, onFun, hab, disjoint_comm (a := a),
        disjoint_comm (a := b), h₃'] using
        h₃.comp_of_injective ((Equiv.swap 0 i).injective.comp (Fin.succ_injective _))
    · simpa [← union_assoc, (Equiv.surjective _).iUnion_comp] using h₄

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

Goal state before:
pp: α : Type ua
β : Type ub
inst✝ : UniformSpace α
f : SetRel α α → Filter β
h : Monotone f
⊢ ((𝓤 α).lift fun s ↦ f (s ○ s)) = ((𝓤 α).lift' fun s ↦ s ○ s).lift f

Tactic:
rw [lift_lift'_assoc]

Goal state after:
case hg
α : Type ua
β : Type ub
inst✝ : UniformSpace α
f : SetRel α α → Filter β
h : Monotone f
⊢ Monotone fun s ↦ s ○ s

case hh
α : Type ua
β : Type ub
inst✝ : UniformSpace α
f : SetRel α α → Filter β
h : Monotone f
⊢ Monotone f
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: case refine_2
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → SetRel α α
H : (𝓤 α).HasBasis p s
h : ∀ (i : γ), p i → ∃ N, ∀ n ≥ N, (u n, u N) ∈ s i
i : γ
hi : p i
⊢ ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i

Tactic:
rcases comp_symm_of_uniformity (H.mem_of_mem hi) with ⟨t, ht, ht', hts⟩
    rcases H.mem_iff.1 ht with ⟨j, hj, hjt⟩
    refine (h j hj).imp fun N hN m hm n hn => hts ⟨u N, hjt ?_, ht' <| hjt ?_⟩
    exacts [hN m hm, hN n hn]

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

Goal state before:
pp: α : Type u
inst✝¹ : UniformSpace α
inst✝ : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : s.Pairwise fun x y ↦ (x, y) ∉ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SetRel.IsSymm V₁
h_comp : SetRel.comp V₁ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
V : Set (α × α)
V_in : V ∈ 𝓤 α
a✝ : SetRel.IsSymm V
z : α
hz : z ∈ ball x (V₁ ∩ V)
hz' : z ∈ s
hzy : ¬z = y
⊢ False

Tactic:
exact hs hz' hy' hzy (h_comp <| mem_comp_of_mem_ball (ball_inter_left x _ _ hz) hy)

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
ι : Sort u_1
ι' : Sort u_2
p : ι → Prop
p' : ι' → Prop
s : ι → Set (α × α)
s' : ι' → Set (β × β)
h : (𝓤 α).HasBasis p s
h' : (𝓤 β).HasBasis p' s'
f : α → β
⊢ IsUniformInducing f ↔
    (∀ (i : ι'), p' i → ∃ j, p j ∧ ∀ (x y : α), (x, y) ∈ s j → (f x, f y) ∈ s' i) ∧
      ∀ (j : ι), p j → ∃ i, p' i ∧ ∀ (x y : α), (f x, f y) ∈ s' i → (x, y) ∈ s j

Tactic:
by
  simp [isUniformInducing_iff', h.uniformContinuous_iff h', (h'.comap _).le_basis_iff h, subset_def]

Goal state after:
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
this : f ≤ g
c : Filter α
hcf : c ≤ f
hc : Cauchy c
⊢ False

Tactic:
rcases mem_prod_same_iff.1 (hc.2 hd) with ⟨m, hm, hmd⟩

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
c : Filter α
hcf : c ≤ f
hc : Cauchy c
m : Set α
hm : m ∈ c
hmd : m ×ˢ m ⊆ d
⊢ False
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
p : Filter ι
h : TendstoLocallyUniformlyOn F f p s
h' : s' ⊆ s
⊢ TendstoLocallyUniformlyOn F f p s'

Tactic:
by
  intro u hu x hx
  rcases h u hu x (h' hx) with ⟨t, ht, H⟩
  exact ⟨t, nhdsWithin_mono x h' ht, H.mono fun n => id⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ IsUniformInducing ⇑(Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ)

Tactic:
by
    constructor
    change
      comap (Prod.map (Equiv.arrowProdEquivProdArrow _ _ _) (Equiv.arrowProdEquivProdArrow _ _ _))
          _ = _
    simp_rw [UniformFun]
    rw [← uniformity_comap]
    congr
    unfold instUniformSpaceProd
    rw [UniformSpace.comap_inf, ← UniformSpace.comap_comap, ← UniformSpace.comap_comap]
    have := (@UniformFun.inf_eq α (β × γ)
      (UniformSpace.comap Prod.fst ‹_›) (UniformSpace.comap Prod.snd ‹_›)).symm
    rwa [UniformFun.comap_eq, UniformFun.comap_eq] at this

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
X : Type u_3
α' : Type u_7
tX : TopologicalSpace X
u : κ → UniformSpace α'
F : ι → X → α'
⊢ Equicontinuous F ↔ ∀ (k : κ), Equicontinuous F

Tactic:
simp_rw +instances [equicontinuous_iff_continuous (uα := _), UniformFun.topologicalSpace]

Goal state after:
ι : Type u_1
κ : Type u_2
X : Type u_3
α' : Type u_7
tX : TopologicalSpace X
u : κ → UniformSpace α'
F : ι → X → α'
⊢ Continuous[tX, inferInstance] (⇑ofFun ∘ swap F) ↔ ∀ (k : κ), Continuous[tX, inferInstance] (⇑ofFun ∘ swap F)
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
⊢ uniformSpace α β =
    UniformSpace.comap (⇑ofFun ∘ (fun x ↦ x ∘ φ₁) ∘ ⇑toFun) (uniformSpace δ₁ β) ⊓
      UniformSpace.comap (⇑ofFun ∘ (fun x ↦ x ∘ φ₂) ∘ ⇑toFun) (uniformSpace δ₂ β)

Tactic:
by
  ext : 1
  refine le_antisymm (le_inf ?_ ?_) ?_
  · exact tendsto_iff_comap.mp UniformFun.precomp_uniformContinuous
  · exact tendsto_iff_comap.mp UniformFun.precomp_uniformContinuous
  · refine
      (UniformFun.hasBasis_uniformity δ₁ β |>.comap _).inf
      (UniformFun.hasBasis_uniformity δ₂ β |>.comap _)
        |>.le_basis_iff (UniformFun.hasBasis_uniformity α β) |>.mpr fun U hU ↦
        ⟨⟨U, U⟩, ⟨hU, hU⟩, fun ⟨f, g⟩ hfg x ↦ ?_⟩
    rcases h_cover.ge <| mem_univ x with (⟨y, rfl⟩ | ⟨y, rfl⟩)
    · exact hfg.1 y
    · exact hfg.2 y

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
ι' : Type u_6
inst✝ : Nonempty ι
t : ι → Set α
p : ι' → Prop
V : ι' → Set (β × β)
ht : ∀ (i : ι), t i ∈ 𝔖
hdir : Directed (fun x1 x2 ↦ x1 ⊆ x2) t
hex : ∀ s ∈ 𝔖, ∃ i, s ⊆ t i
hb : (𝓤 β).HasBasis p V
hne : 𝔖.Nonempty
s₁ : Set α
hs₁ : s₁ ∈ 𝔖
s₂ : Set α
hs₂ : s₂ ∈ 𝔖
⊢ ∃ z ∈ 𝔖, (fun x1 x2 ↦ x1 ⊆ x2) s₁ z ∧ (fun x1 x2 ↦ x1 ⊆ x2) s₂ z

Tactic:
rcases hex s₁ hs₁, hex s₂ hs₂ with ⟨⟨i₁, his₁⟩, i₂, his₂⟩
    rcases hdir i₁ i₂ with ⟨i, hi₁, hi₂⟩
    exact ⟨t i, ht _, his₁.trans hi₁, his₂.trans hi₂⟩

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 → α
S : Set X
x₀ : X
hX : (𝓝[S] x₀).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
⊢ EquicontinuousWithinAt F S x₀ ↔ ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x ∈ s₁ k₁, ∀ (i : ι), (F i x₀, F i x) ∈ s₂ k₂

Tactic:
rw [equicontinuousWithinAt_iff_continuousWithinAt, ContinuousWithinAt,
    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 → α
S : Set X
x₀ : X
hX : (𝓝[S] 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.Pointwise

Goal state before:
pp: case mp
α : Type u_2
inst✝ : DivisionMonoid α
f : Filter α
⊢ IsUnit f → ∃ a, f = pure a ∧ IsUnit a

Tactic:
rintro ⟨u, rfl⟩

Goal state after:
case mp
α : Type u_2
inst✝ : DivisionMonoid α
u : (Filter α)ˣ
⊢ ∃ a, ↑u = pure a ∧ IsUnit a
Module: Mathlib.Topology.ContinuousMap.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
f : α → β
g : C(↑s, β)
x : ↑s
hf : ContinuousOn f s
⊢ (mkD (s.domRestrict f) g) x = f ↑x

Tactic:
by rw [mkD_of_continuousOn hf, coe_mk, Set.domRestrict_apply]

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

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
δ₁ : Type u_5
δ₂ : Type u_6
φ₁ : δ₁ → α
φ₂ : δ₂ → α
𝔗₁ : Set (Set δ₁)
𝔗₂ : Set (Set δ₂)
h_image₁ : MapsTo (fun x ↦ φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun x ↦ φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun x ↦ φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun x ↦ φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂
ψ₁ : (S : Set α) → ↑(φ₁ ⁻¹' S) → ↑S := fun S ↦ S.restrictPreimage φ₁
ψ₂ : (S : Set α) → ↑(φ₂ ⁻¹' S) → ↑S := fun S ↦ S.restrictPreimage φ₂
this :
  ∀ S ∈ 𝔖,
    UniformFun.uniformSpace (↑S) β =
      UniformSpace.comap (fun x ↦ x ∘ ψ₁ S) (UniformFun.uniformSpace (↑(φ₁ ⁻¹' S)) β) ⊓
        UniformSpace.comap (fun x ↦ x ∘ ψ₂ S) (UniformFun.uniformSpace (↑(φ₂ ⁻¹' S)) β)
S : Set α
hS : S ∈ 𝔖
⊢ UniformSpace.comap (⇑(ofFun 𝔗₁) ∘ (fun x ↦ x ∘ φ₁) ∘ ⇑(toFun 𝔖)) (uniformSpace δ₁ β 𝔗₁) ⊓
      UniformSpace.comap (⇑(ofFun 𝔗₂) ∘ (fun x ↦ x ∘ φ₂) ∘ ⇑(toFun 𝔖)) (uniformSpace δ₂ β 𝔗₂) ≤
    UniformSpace.comap (⇑UniformFun.ofFun ∘ S.domRestrict ∘ ⇑(toFun 𝔖)) (UniformFun.uniformSpace (↑S) β)

Tactic:
· simp_rw [this S hS, uniformSpace, UniformSpace.comap_iInf, UniformSpace.comap_inf,
      ← UniformSpace.comap_comap]
    exact inf_le_inf
      (iInf₂_le_of_le _ (h_preimage₁ hS) le_rfl)
      (iInf₂_le_of_le _ (h_preimage₂ hS) le_rfl)

Goal state after:
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: case right
ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous[inst✝¹ i, inst✝ i] (f i) ∧
      ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄, Tendsto (f i) (↑𝒰) (𝓝 y) → ∃ x, f i x = y ∧ ↑𝒰 ≤ 𝓝 x
⊢ ∀ ⦃𝒰 : Ultrafilter ((i : ι) → X i)⦄ ⦃y : (i : ι) → Y i⦄,
    Tendsto (fun x i ↦ f i (x i)) (↑𝒰) (𝓝 y) → ∃ x, (fun i ↦ f i (x i)) = y ∧ ↑𝒰 ≤ 𝓝 x

Tactic:
intro 𝒰 y hy

Goal state after:
case right
ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous[inst✝¹ i, inst✝ i] (f i) ∧
      ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄, Tendsto (f i) (↑𝒰) (𝓝 y) → ∃ x, f i x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter ((i : ι) → X i)
y : (i : ι) → Y i
hy : Tendsto (fun x i ↦ f i (x i)) (↑𝒰) (𝓝 y)
⊢ ∃ x, (fun i ↦ f i (x i)) = y ∧ ↑𝒰 ≤ 𝓝 x
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
x✝ : ∀ i ∈ [], Tendsto (f i) x (𝓝 (a i))
⊢ Tendsto (fun b ↦ (List.map (fun c ↦ f c b) []).prod) x (𝓝 (List.map a []).prod)

Tactic:
by simp [tendsto_const_nhds]

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
c a : G
⊢ map (fun x ↦ x * c) (𝓝[≠] a) = 𝓝[≠] (a * c)

Tactic:
convert! (Homeomorph.mulRight c).isEmbedding.map_nhdsWithin_eq .. using 2

Goal state after:
case e'_3.e'_4
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
c a : G
⊢ {a * c}ᶜ = ⇑(Homeomorph.mulRight c) '' {a}ᶜ
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul αᵐᵒᵖ α
s : Set α
a : α
h : s ∈ 𝓝 1
⊢ s * {a} ∈ 𝓝 a

Tactic:
by
  simpa only [one_mul] using mul_singleton_mem_nhds a h

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

Goal state before:
pp: H : Type x
inst✝⁴ : TopologicalSpace H
inst✝³ : CommGroup H
inst✝² : PartialOrder H
inst✝¹ : IsOrderedMonoid H
inst✝ : ContinuousMul H
c a : H
⊢ map (fun x ↦ x * c) (𝓝[>] a) = 𝓝[>] (a * c)

Tactic:
convert! (Homeomorph.mulRight c).isEmbedding.map_nhdsWithin_eq .. using 2

Goal state after:
case e'_3.e'_4
H : Type x
inst✝⁴ : TopologicalSpace H
inst✝³ : CommGroup H
inst✝² : PartialOrder H
inst✝¹ : IsOrderedMonoid H
inst✝ : ContinuousMul H
c a : H
⊢ Ioi (a * c) = ⇑(Homeomorph.mulRight c) '' Ioi a