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

Goal state before:
pp: X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
inst✝¹ : Nonempty X
inst✝ : Nonempty Z
f : X → Y
g : Z → W
⊢ IsOpenMap (Prod.map f g) ↔ IsOpenMap f ∧ IsOpenMap g

Tactic:
refine ⟨fun h ↦ ⟨?_, ?_⟩, fun ⟨hf, hg⟩ ↦ hf.prodMap hg⟩

Goal state after:
case refine_1
X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
inst✝¹ : Nonempty X
inst✝ : Nonempty Z
f : X → Y
g : Z → W
h : IsOpenMap (Prod.map f g)
⊢ IsOpenMap f

case refine_2
X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
inst✝¹ : Nonempty X
inst✝ : Nonempty Z
f : X → Y
g : Z → W
h : IsOpenMap (Prod.map f g)
⊢ IsOpenMap g
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: case refine_2
α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s u : Set α
this : TopologicalSpace α := TopologicalSpace.induced f t
x✝ : ∃ v, (∃ U, IsOpen[t] U ∧ f '' s ⊆ U ∧ U ⊆ v) ∧ f ⁻¹' v ⊆ u
v v' : Set β
hv' : IsOpen[t] v' ∧ f '' s ⊆ v' ∧ v' ⊆ v
hv : f ⁻¹' v ⊆ u
⊢ ∃ U, (∃ t_1, IsOpen[t] t_1 ∧ f ⁻¹' t_1 = U) ∧ s ⊆ U ∧ U ⊆ u

Tactic:
exact ⟨f ⁻¹' v', ⟨v', hv'.1, rfl⟩, image_subset_iff.1 hv'.2.1, (preimage_mono hv'.2.2).trans hv⟩

Goal state after:
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
h : IsInducing (Sum.elim f g)
⊢ Disjoint (closure[inst✝] (range f)) (range g)

Tactic:
by
  rcases h.isClosed_iff.mp isClosed_range_inl with ⟨C, C_closed, hC⟩
  have A : closure (range f) ⊆ C := by
    rw [C_closed.closure_subset_iff, ← elim_comp_inl f g, range_comp, image_subset_iff, hC]
  have B : Disjoint C (range g) := by
    rw [← image_univ, disjoint_image_right, ← elim_comp_inr f g, preimage_comp, hC,
        ← disjoint_image_right, ← image_univ]
    exact disjoint_image_inl_image_inr
  exact B.mono_left A

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : IsOpenMap (s.domRestrict f)
finv : β → α
hleft : LeftInvOn finv f s
t : Set α
ht : IsOpen[inst✝¹] t
⊢ finv ⁻¹' t ∩ f '' s = f '' (t ∩ s) ∩ f '' s

Tactic:
· rw [inter_eq_self_of_subset_left (image_mono inter_subset_right), hleft.image_inter']

Goal state after:
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: α : Type u_1
s : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ (n : ℕ), s n ≠ univ
⊢ ∀ (n : ℕ), accumulate s n ≠ univ

Tactic:
n

Goal state after:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ (n : ℕ), s n ≠ univ
n : ℕ
⊢ accumulate s n ≠ univ
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
I : Set ι
hI : I.Finite
s : (i : ι) → Set (A i)
⊢ interior (I.pi s) = I.pi fun i ↦ interior (s i)

Tactic:
ext a

Goal state after:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
I : Set ι
hI : I.Finite
s : (i : ι) → Set (A i)
a : (i : ι) → A i
⊢ a ∈ interior (I.pi s) ↔ a ∈ I.pi fun i ↦ interior (s i)
Module: Mathlib.Order.Filter.Ultrafilter.Defs

Goal state before:
pp: α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
⊢ map m (ofComapInfPrincipal h) = g

Tactic:
by
  let f := Filter.comap m g ⊓ 𝓟 s
  have : f.NeBot := comap_inf_principal_neBot_of_image_mem h
  apply eq_of_le
  calc
    Filter.map m (of f) ≤ Filter.map m f := map_mono (of_le _)
    _ ≤ (Filter.map m <| Filter.comap m g) ⊓ Filter.map m (𝓟 s) := map_inf_le
    _ = (Filter.map m <| Filter.comap m g) ⊓ (𝓟 <| m '' s) := by rw [map_principal]
    _ ≤ ↑g ⊓ (𝓟 <| m '' s) := inf_le_inf_right _ map_comap_le
    _ = ↑g := inf_of_le_left (le_principal_iff.mpr h)

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case a
α : Type u
t : TopologicalSpace α
inst✝¹ : Countable α
inst✝ : FirstCountableTopology α
b : α → ℕ → Set α
hxb : ∀ (x : α) (i : ℕ), x ∈ b x i ∧ IsOpen[t] (b x i)
hbb : ∀ (x : α), (𝓝 x).HasAntitoneBasis fun i ↦ b x i
x : α
⊢ ∀ (i' : ℕ), True → b x i' ∈ 𝓝 x

Tactic:
intro n _

Goal state after:
case a
α : Type u
t : TopologicalSpace α
inst✝¹ : Countable α
inst✝ : FirstCountableTopology α
b : α → ℕ → Set α
hxb : ∀ (x : α) (i : ℕ), x ∈ b x i ∧ IsOpen[t] (b x i)
hbb : ∀ (x : α), (𝓝 x).HasAntitoneBasis fun i ↦ b x i
x : α
n : ℕ
a✝ : True
⊢ b x n ∈ 𝓝 x
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set (ULift.{v, u} X)
⊢ IsOpen[induced down inst✝] s ↔ IsOpen[inst✝] (up ⁻¹' s)

Tactic:
← Equiv.ulift_apply,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set (ULift.{v, u} X)
⊢ IsOpen[induced (⇑Equiv.ulift) inst✝] s ↔ IsOpen[inst✝] (up ⁻¹' s)
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set (ULift.{v, u} X)
⊢ IsClosed[topologicalSpace] s ↔ IsClosed[inst✝] (up ⁻¹' s)

Tactic:
by
  rw [← isOpen_compl_iff, ← isOpen_compl_iff, isOpen_iff, preimage_compl]

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst✝] t
f : Filter X
hnf : f.NeBot
hstf : f ≤ 𝓟 (s ∩ t)
x : X
hsx : x ∈ s
hx : ClusterPt x f
this : x ∈ t
⊢ ∃ x ∈ s ∩ t, ClusterPt x f

Tactic:
exact ⟨x, ⟨hsx, this⟩, hx⟩

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
h : ∀ t ⊆ S, ∃ u, IsOpen[inst✝] u ∧ u ∩ S = t
s : Set X
sS : s ⊆ S
U : Set X
Uo : IsOpen[inst✝] U
Us : U ∩ S = sᶜ ∩ S
⊢ Uᶜ ∩ S = s ∩ S

Tactic:
simp_all [Set.ext_iff]

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
h : ∀ s ⊆ S, ∃ U, IsClosed[inst✝] U ∧ U ∩ S = s
s : Set X
sS : s ⊆ S
U : Set X
Uo : IsClosed[inst✝] U
Us : U ∩ S = sᶜ ∩ S
⊢ Uᶜ ∩ S = s ∩ S

Tactic:
simp_all [Set.ext_iff]

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

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : ∀ (x : X), (𝓝[≠] x).NeBot
s : Set X
hs : Dense s
t : Set X
ht : t.Finite
⊢ Dense (s \ t)

Tactic:
convert! hs.sdiff_finset ht.toFinset
  exact (Finite.coe_toFinset _).symm

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
⊢ CountableInterFilter ⊤

Tactic:
rw [← principal_univ]
  apply countableInterFilter_principal

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
x y : α
hx : x ∈ s
hy : y ∈ s
Q : ↑s → ↑s → Prop := fun a b ↦ P ↑a ↑b
⊢ Q ⟨x, hx⟩ ⟨y, hy⟩

Tactic:
have : PreconnectedSpace s := Subtype.preconnectedSpace hs

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
x y : α
hx : x ∈ s
hy : y ∈ s
Q : ↑s → ↑s → Prop := fun a b ↦ P ↑a ↑b
this : PreconnectedSpace ↑s
⊢ Q ⟨x, hx⟩ ⟨y, hy⟩
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case h'
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
x y : α
hx : x ∈ s
hy : y ∈ s
Q : ↑s → ↑s → Prop := ⋯
this : PreconnectedSpace ↑s
⊢ IsTrans { x // x ∈ s } Q

Tactic:
exact ⟨fun ⟨a, ha⟩ ⟨b, hb⟩ ⟨c, hc⟩ ↦ h' a b c ha hb hc⟩

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)
hne : (univ.pi s).Nonempty
hc : IsPreconnected (univ.pi s)
i : ι
⊢ IsPreconnected (s i)

Tactic:
rw [← eval_image_univ_pi hne]

Goal state after:
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hne : (univ.pi s).Nonempty
hc : IsPreconnected (univ.pi s)
i : ι
⊢ IsPreconnected ((fun f ↦ f i) '' univ.pi s)
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
i : α → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : IsDenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := di.extend f
⊢ ContinuousAt φ b

Tactic:
have := di.comap_nhds_neBot

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
i : α → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : IsDenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := di.extend f
this : ∀ (b : β), (comap i (𝓝 b)).NeBot
⊢ ContinuousAt φ b
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : ∃ K, (∀ (n : ℕ), IsCompact (K n)) ∧ ⋃ n, K n = s
⊢ IsLindelof s

Tactic:
rcases hs with ⟨K, ⟨hc, huniv⟩⟩

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
K : ℕ → Set X
hc : ∀ (n : ℕ), IsCompact (K n)
huniv : ⋃ n, K n = s
⊢ IsLindelof s
Module: Mathlib.Topology.Connected.TotallyDisconnected

Goal state before:
pp: α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝³ : TopologicalSpace α
s t u v : Set α
inst✝² : TopologicalSpace β
inst✝¹ : TotallyDisconnectedSpace α
inst✝ : TotallyDisconnectedSpace β
⊢ TotallyDisconnectedSpace (α ⊕ β)

Tactic:
refine ⟨fun s _ hs => ?_⟩

Goal state after:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝³ : TopologicalSpace α
s✝ t u v : Set α
inst✝² : TopologicalSpace β
inst✝¹ : TotallyDisconnectedSpace α
inst✝ : TotallyDisconnectedSpace β
s : Set (α ⊕ β)
x✝ : s ⊆ univ
hs : IsPreconnected s
⊢ s.Subsingleton
Module: Mathlib.Topology.Connected.TotallyDisconnected

Goal state before:
pp: α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝² : TopologicalSpace α
s t u v : Set α
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), TotallyDisconnectedSpace (X i)
⊢ TotallyDisconnectedSpace ((i : ι) × X i)

Tactic:
refine ⟨fun s _ hs => ?_⟩

Goal state after:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝² : TopologicalSpace α
s✝ t u v : Set α
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), TotallyDisconnectedSpace (X i)
s : Set ((i : ι) × X i)
x✝ : s ⊆ univ
hs : IsPreconnected s
⊢ s.Subsingleton
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsOpen[inst✝] s
⊢ ∀ t ∈ {s}, IsOpen[inst✝] t

Tactic:
by simp [h]

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ x ∈ s, ∀ y ∈ s, f x = f y
u v : Set α
u_op : IsOpen[inst✝] u
v_op : IsOpen[inst✝] v
hsuv : s ⊆ u ∪ v
x : α
x_in_s : x ∈ s
x_in_u : x ∈ u
H : s ∩ (u ∩ v) = ∅
y : α
y_in_s : y ∈ s
y_in_v : y ∈ v
hy : y ∉ u
⊢ IsOpen[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' u)

Tactic:
· exact u_op.preimage continuous_subtype_val

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

Goal state before:
pp: α : Type ua
u₁ u₂ : UniformSpace α
h : 𝓤 α = 𝓤 α
x : α
⊢ 𝓝 x = 𝓝 x

Tactic:
rw [u₁.nhds_eq_comap_uniformity, u₂.nhds_eq_comap_uniformity]

Goal state after:
α : Type ua
u₁ u₂ : UniformSpace α
h : 𝓤 α = 𝓤 α
x : α
⊢ comap (Prod.mk x) UniformSpace.uniformity = comap (Prod.mk x) UniformSpace.uniformity
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : SetRel α β
t : SetRel β γ
hs : IsOpen[instTopologicalSpaceProd] s
ht : IsOpen[instTopologicalSpaceProd] t
⊢ IsOpen[instTopologicalSpaceProd] (s ○ t)

Tactic:
conv =>
    arg 1; equals ⋃ b, (fun p => (p.1, b)) ⁻¹' s ∩ (fun p => (b, p.2)) ⁻¹' t => ext ⟨_, _⟩; simp

Goal state after:
α : Type ua
β : Type ub
γ : Type uc
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : SetRel α β
t : SetRel β γ
hs : IsOpen[instTopologicalSpaceProd] s
ht : IsOpen[instTopologicalSpaceProd] t
⊢ IsOpen[instTopologicalSpaceProd] (⋃ b, (fun p ↦ (p.1, b)) ⁻¹' s ∩ (fun p ↦ (b, p.2)) ⁻¹' t)
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
n : ℕ
⊢ ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, (fun x ↦ t ○ x)^[n] t ⊆ s

Tactic:
suffices ∀ᶠ t in (𝓤 α).smallSets, t ⊆ s ∧ (t ○ ·)^[n] t ⊆ s from (eventually_and.1 this).2

Goal state after:
α : Type ua
inst✝ : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
n : ℕ
⊢ ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun x ↦ t ○ x)^[n] t ⊆ s
Module: Mathlib.Topology.UniformSpace.Separation

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

Tactic:
disjoint_iUnion_right

Goal state after:
α : Type u
inst✝¹ : UniformSpace α
ι : Type u_1
inst✝ : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst✝¹.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst✝¹.toTopologicalSpace] t)
S : Bool → Set α := fun b ↦ Bool.casesOn b s t
U : (b : Bool) → ↑(S b) → ι
hU : ∀ (b : Bool) (x : ↑(S b)), Disjoint (ball (↑x) ((B (U b x)).comp (B (U b x)).inv)) (S !b)
hUS : ∀ (b : Bool), ⋃ x, ball (↑x) (B (U b x)) ∈ 𝓝ˢ (S b)
hdj :
  ∀ (b : Bool) (x : ↑(S b)) (y : ↑(S !b)),
    U b x ≤ U (!b) y → Disjoint (ball (↑x) (B (U b x))) (ball (↑y) (B (U (!b) y)))
⊢ ∀ (i : ↑(S false)) (i_1 : ↑(S true)), Disjoint (ball (↑i) (B (U false i))) (ball (↑i_1) (B (U true i_1)))
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))
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))
x : α
⊢ ∀ (b : ι), (∀ᶠ (x_1 : ι) in p, (F b x, F x_1 x) ∈ t) → Tendsto (fun n ↦ F n x) p (𝓝 (f x)) → (f x, F b x) ∈ u

Tactic:
n

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))
x : α
n : ι
⊢ (∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t) → Tendsto (fun n ↦ F n x) p (𝓝 (f x)) → (f x, F n x) ∈ u
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: case refine_2
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
p : α × α
hp : p ∈ setSeq hf U_mem m ×ˢ setSeq hf U_mem n
⊢ p.2 ∈ setSeq hf U_mem N

Tactic:
· exact setSeq_mono hf U_mem hn hp.2

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
⊢ ∃ v, (∃ i ∈ s, ∃ y, ball i (t y) = v) ∧ x ∈ v ∧ v ⊆ V

Tactic:
rcases h_basis.toHasBasis.mem_iff.1 hU' with ⟨k, -, hk⟩

Goal state after:
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'
⊢ ∃ v, (∃ i ∈ s, ∃ y, ball i (t y) = v) ∧ x ∈ v ∧ v ⊆ V
Module: Mathlib.Topology.UniformSpace.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst✝ : Nonempty ι
l : (i : ι) → Filter (α i)
hl : ∀ (i : ι), Cauchy (l i)
⊢ Cauchy (Filter.pi l)

Tactic:
by
  have := fun i ↦ (hl i).1
  simpa [cauchy_pi_iff]

Goal state after:
Module: Mathlib.Topology.Coherent

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
S : Set (Set X)
inst✝ : SequentialSpace X
h : ∀ ⦃u : ℕ → X⦄ ⦃x : X⦄, Tendsto u atTop (𝓝 x) → insert x (range u) ∈ S
⊢ IsCoherentWith S

Tactic:
refine of_isClosed fun t ht ↦ IsSeqClosed.isClosed fun u x hut hux ↦ ?_

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
S : Set (Set X)
inst✝ : SequentialSpace X
h : ∀ ⦃u : ℕ → X⦄ ⦃x : X⦄, Tendsto u atTop (𝓝 x) → insert x (range u) ∈ S
t : Set X
ht : ∀ s ∈ S, IsClosed[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' t)
u : ℕ → X
x : X
hut : ∀ (n : ℕ), u n ∈ t
hux : Tendsto u atTop (𝓝 x)
⊢ x ∈ t
Module: Mathlib.Topology.Coherent

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
S : Set (Set X)
inst✝ : SequentialSpace X
h : ∀ ⦃u : ℕ → X⦄ ⦃x : X⦄, Tendsto u atTop (𝓝 x) → insert x (range u) ∈ S
t : Set X
ht : ∀ s ∈ S, IsClosed[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' t)
u : ℕ → X
x : X
hut : ∀ (n : ℕ), u n ∈ t
hux : Tendsto u atTop (𝓝 x)
s : Set X
hsc : IsClosed[inst✝¹] s
hst : Subtype.val ⁻¹' s = Subtype.val ⁻¹' t
⊢ x ∈ t

Tactic:
rw [Subtype.preimage_val_eq_preimage_val_iff, Set.ext_iff] at hst

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
S : Set (Set X)
inst✝ : SequentialSpace X
h : ∀ ⦃u : ℕ → X⦄ ⦃x : X⦄, Tendsto u atTop (𝓝 x) → insert x (range u) ∈ S
t : Set X
ht : ∀ s ∈ S, IsClosed[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' t)
u : ℕ → X
x : X
hut : ∀ (n : ℕ), u n ∈ t
hux : Tendsto u atTop (𝓝 x)
s : Set X
hsc : IsClosed[inst✝¹] s
hst : ∀ (x_1 : X), x_1 ∈ insert x (range u) ∩ s ↔ x_1 ∈ insert x (range u) ∩ t
⊢ x ∈ t
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : UniformSpace γ
G : ι → α → γ
g : α → γ
hF : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
hG : ∀ x ∈ s, Tendsto (fun y ↦ (g y.2, G y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 γ)
x : α
hx : x ∈ s
⊢ Tendsto (fun y ↦ ((f y.2, g y.2), F y.1 y.2, G y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 (β × γ))

Tactic:
rw [uniformity_prod_eq_comap_prod, tendsto_comap_iff]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : UniformSpace γ
G : ι → α → γ
g : α → γ
hF : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
hG : ∀ x ∈ s, Tendsto (fun y ↦ (g y.2, G y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 γ)
x : α
hx : x ∈ s
⊢ Tendsto ((fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ∘ fun y ↦ ((f y.2, g y.2), F y.1 y.2, G y.1 y.2)) (p ×ˢ 𝓝[s] x)
    (𝓤 β ×ˢ 𝓤 γ)
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
inst✝ : Finite ι
F : ι → X → α
S : Set X
x₀ : X
⊢ EquicontinuousWithinAt F S x₀ ↔ ∀ (i : ι), ContinuousWithinAt (F i) S x₀

Tactic:
by
  simp [EquicontinuousWithinAt, ContinuousWithinAt,
    (nhds_basis_uniformity' (𝓤 α).basis_sets).tendsto_right_iff, UniformSpace.ball,
    @forall_comm _ ι]

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α' : Type u_7
β : Type u_8
uβ : UniformSpace β
u : κ → UniformSpace α'
F : ι → β → α'
S : Set β
⊢ UniformEquicontinuousOn F S ↔ ∀ (k : κ), UniformEquicontinuousOn F S

Tactic:
by
  simp_rw [uniformEquicontinuousOn_iff_uniformContinuousOn (uα := _)]
  unfold UniformContinuousOn
  rw [UniformFun.iInf_eq, iInf_uniformity, tendsto_iInf]

Goal state after:
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 α)
h : univ ∈ 𝔖
⊢ UniformContinuous fun f ↦ UniformFun.ofFun ((toFun 𝔖) f)

Tactic:
by
    simp only [UniformContinuous, (UniformFun.hasBasis_uniformity _ _).tendsto_right_iff]
    intro U hU
    filter_upwards [UniformOnFun.gen_mem_uniformity _ _ h hU] with f hf x using hf x (mem_univ _)

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c x : α
⊢ x ∈ Icc (a * b) (a * c) → x ∈ a • Icc b c

Tactic:
· rintro ⟨habx, hxac⟩
    obtain ⟨y, hy, rfl⟩ := exists_one_le_mul_of_le habx
    refine ⟨b * y, ⟨le_mul_of_one_le_right' hy, ?_⟩, (mul_assoc ..).symm⟩
    rwa [mul_assoc, mul_le_mul_iff_left] at hxac

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✝ : MulPosReflectLT G₀
c a : G₀
h : 0 < c
⊢ (fun x ↦ x * c) ⁻¹' Ici a = Ici (a / c)

Tactic:
by
  simpa only [division_def] using! (OrderIso.mulRight₀ c h).preimage_Ici a

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

Goal state before:
pp: K : Type u_2
inst✝⁴ : DivisionSemiring K
inst✝³ : PartialOrder K
inst✝² : PosMulReflectLT K
inst✝¹ : IsOrderedCancelAddMonoid K
inst✝ : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
this : (fun x ↦ x + b) '' (fun x ↦ a * x) '' Icc c d = Icc (a * c + b) (a * d + b)
⊢ (fun x ↦ a * x + b) '' Icc c d = Icc (a * c + b) (a * d + b)

Tactic:
rwa [Set.image_image] at this

Goal state after: