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

Goal state before:
pp: case ho
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s t : Set X
hs : IsGδ s
ht : IsGδ t
hsc : Dense s
htc : Dense t
⊢ ∀ (s_1 : Bool), IsGδ (bif s_1 then s else t)

pp: case hd
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s t : Set X
hs : IsGδ s
ht : IsGδ t
hsc : Dense s
htc : Dense t
⊢ ∀ (s_1 : Bool), Dense (bif s_1 then s else t)

Tactic:
<;>

Goal state after:
case ho
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s t : Set X
hs : IsGδ s
ht : IsGδ t
hsc : Dense s
htc : Dense t
⊢ ∀ (s_1 : Bool), IsGδ (bif s_1 then s else t)

case hd
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s t : Set X
hs : IsGδ s
ht : IsGδ t
hsc : Dense s
htc : Dense t
⊢ ∀ (s_1 : Bool), Dense (bif s_1 then s else t)
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : Infinite (ConnectedComponents α)
h✝ : Nonempty α
n : ℕ
U : Fin (n + 1) → Set α
h₁ : ∀ (i : Fin (n + 1)), IsClopen (U i)
h₂ : ∀ (i : Fin (n + 1)), (U i).Nonempty
h₃ : Pairwise (Disjoint on U)
h₄ : ⋃ i, U i = univ
⊢ ∃ i, ¬ConnectedSpace ↑(U i)

Tactic:
← not_forall

Goal state after:
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : Infinite (ConnectedComponents α)
h✝ : Nonempty α
n : ℕ
U : Fin (n + 1) → Set α
h₁ : ∀ (i : Fin (n + 1)), IsClopen (U i)
h₂ : ∀ (i : Fin (n + 1)), (U i).Nonempty
h₃ : Pairwise (Disjoint on U)
h₄ : ⋃ i, U i = univ
⊢ ¬∀ (x : Fin (n + 1)), ConnectedSpace ↑(U x)
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: case inl
X : Type u_1
Y : Type u_2
W : Type u_3
Z : Type u_4
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : TopologicalSpace W
inst✝³ : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Y'
S : Type u_7
T : Type u_8
A : S ⊕ T → Type u_9
inst✝ : (st : S ⊕ T) → TopologicalSpace (A st)
s : S
⊢ Continuous[instTopologicalSpaceProd, inst✝ (Sum.inl s)] fun a ↦ (Equiv.sumPiEquivProdPi A).invFun a (Sum.inl s)

pp: case inr
X : Type u_1
Y : Type u_2
W : Type u_3
Z : Type u_4
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : TopologicalSpace W
inst✝³ : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Y'
S : Type u_7
T : Type u_8
A : S ⊕ T → Type u_9
inst✝ : (st : S ⊕ T) → TopologicalSpace (A st)
t : T
⊢ Continuous[instTopologicalSpaceProd, inst✝ (Sum.inr t)] fun a ↦ (Equiv.sumPiEquivProdPi A).invFun a (Sum.inr t)

Tactic:
<;>

Goal state after:
case inl
X : Type u_1
Y : Type u_2
W : Type u_3
Z : Type u_4
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : TopologicalSpace W
inst✝³ : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Y'
S : Type u_7
T : Type u_8
A : S ⊕ T → Type u_9
inst✝ : (st : S ⊕ T) → TopologicalSpace (A st)
s : S
⊢ Continuous[instTopologicalSpaceProd, inst✝ (Sum.inl s)] fun a ↦ (Equiv.sumPiEquivProdPi A).invFun a (Sum.inl s)

case inr
X : Type u_1
Y : Type u_2
W : Type u_3
Z : Type u_4
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : TopologicalSpace W
inst✝³ : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Y'
S : Type u_7
T : Type u_8
A : S ⊕ T → Type u_9
inst✝ : (st : S ⊕ T) → TopologicalSpace (A st)
t : T
⊢ Continuous[instTopologicalSpaceProd, inst✝ (Sum.inr t)] fun a ↦ (Equiv.sumPiEquivProdPi A).invFun a (Sum.inr t)
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: case inl
X : Type u_1
Y : Type u_2
W : Type u_3
Z : Type u_4
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : TopologicalSpace W
inst✝³ : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Y'
S : Type u_7
T : Type u_8
A : S ⊕ T → Type u_9
inst✝ : (st : S ⊕ T) → TopologicalSpace (A st)
s : S
⊢ Continuous[instTopologicalSpaceProd, inst✝ (Sum.inl s)] fun a ↦ a.1 s

pp: case inr
X : Type u_1
Y : Type u_2
W : Type u_3
Z : Type u_4
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : TopologicalSpace W
inst✝³ : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Y'
S : Type u_7
T : Type u_8
A : S ⊕ T → Type u_9
inst✝ : (st : S ⊕ T) → TopologicalSpace (A st)
t : T
⊢ Continuous[instTopologicalSpaceProd, inst✝ (Sum.inr t)] fun a ↦ a.2 t

Tactic:
<;>

Goal state after:
case inl
X : Type u_1
Y : Type u_2
W : Type u_3
Z : Type u_4
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : TopologicalSpace W
inst✝³ : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Y'
S : Type u_7
T : Type u_8
A : S ⊕ T → Type u_9
inst✝ : (st : S ⊕ T) → TopologicalSpace (A st)
s : S
⊢ Continuous[instTopologicalSpaceProd, inst✝ (Sum.inl s)] fun a ↦ a.1 s

case inr
X : Type u_1
Y : Type u_2
W : Type u_3
Z : Type u_4
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : TopologicalSpace W
inst✝³ : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Y'
S : Type u_7
T : Type u_8
A : S ⊕ T → Type u_9
inst✝ : (st : S ⊕ T) → TopologicalSpace (A st)
t : T
⊢ Continuous[instTopologicalSpaceProd, inst✝ (Sum.inr t)] fun a ↦ a.2 t
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: case fst
X : Type u_1
inst✝ : TopologicalSpace X
m n : ℕ
x : Fin (m + n) → X
i : Fin m
⊢ ((Fin.appendEquiv m n).symm x).1 i =
    ((sumArrowHomeomorphProdArrow.symm.trans (piCongrLeft finSumFinEquiv)).symm x).1 i

pp: case snd
X : Type u_1
inst✝ : TopologicalSpace X
m n : ℕ
x : Fin (m + n) → X
i : Fin n
⊢ ((Fin.appendEquiv m n).symm x).2 i =
    ((sumArrowHomeomorphProdArrow.symm.trans (piCongrLeft finSumFinEquiv)).symm x).2 i

Tactic:
<;>

Goal state after:
case fst
X : Type u_1
inst✝ : TopologicalSpace X
m n : ℕ
x : Fin (m + n) → X
i : Fin m
⊢ ((Fin.appendEquiv m n).symm x).1 i =
    ((sumArrowHomeomorphProdArrow.symm.trans (piCongrLeft finSumFinEquiv)).symm x).1 i

case snd
X : Type u_1
inst✝ : TopologicalSpace X
m n : ℕ
x : Fin (m + n) → X
i : Fin n
⊢ ((Fin.appendEquiv m n).symm x).2 i =
    ((sumArrowHomeomorphProdArrow.symm.trans (piCongrLeft finSumFinEquiv)).symm x).2 i
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : X ≃ Y
⊢ IsHomeomorph ⇑e ↔ Continuous[inst✝¹, inst✝] ⇑e ∧ Continuous[inst✝, inst✝¹] ⇑e.symm

Tactic:
by
  rw [e.continuous_symm_iff]
  exact ⟨fun h ↦ ⟨h.continuous, h.isOpenMap⟩, fun ⟨hc, ho⟩ ↦ ⟨hc, ho, e.bijective⟩⟩

Goal state after:
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 : IsEmbedding ⇑f
⊢ IsEmbedding ⇑(map f)

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

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
U : Set α
⊢ ConnectedComponents.mk ⁻¹' ConnectedComponents.mk '' U = ⋃ x ∈ U, connectedComponent x

Tactic:
by
  simp only [connectedComponents_preimage_singleton, preimage_iUnion₂, image_eq_iUnion]

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

Goal state before:
pp: case inl
α : Type u
inst✝ : TopologicalSpace α
h✝ : ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
f : α → Bool
hf : Continuous[inst✝, _] f
x y : α
this : f ⁻¹' {false} = (f ⁻¹' {true})ᶜ
h : f ⁻¹' {true} = ∅
⊢ f x = f y

pp: case inr
α : Type u
inst✝ : TopologicalSpace α
h✝ : ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
f : α → Bool
hf : Continuous[inst✝, _] f
x y : α
this : f ⁻¹' {false} = (f ⁻¹' {true})ᶜ
h : f ⁻¹' {true} = univ
⊢ f x = f y

Tactic:
<;>

Goal state after:
case inl
α : Type u
inst✝ : TopologicalSpace α
h✝ : ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
f : α → Bool
hf : Continuous[inst✝, _] f
x y : α
this : f ⁻¹' {false} = (f ⁻¹' {true})ᶜ
h : f ⁻¹' {true} = ∅
⊢ f x = f y

case inr
α : Type u
inst✝ : TopologicalSpace α
h✝ : ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
f : α → Bool
hf : Continuous[inst✝, _] f
x y : α
this : f ⁻¹' {false} = (f ⁻¹' {true})ᶜ
h : f ⁻¹' {true} = univ
⊢ f x = f y
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
  exact isOpen_iUnion fun a ↦ hs.preimage (by fun_prop) |>.inter <| ht.preimage (by fun_prop)

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

Goal state before:
pp: case mp
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
⊢ (CauchySeq fun n ↦ u (n + k)) → CauchySeq u

pp: case mpr
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
⊢ CauchySeq u → CauchySeq fun n ↦ u (n + k)

Tactic:
<;>

Goal state after:
case mp
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
⊢ (CauchySeq fun n ↦ u (n + k)) → CauchySeq u

case mpr
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
⊢ CauchySeq u → CauchySeq fun n ↦ u (n + k)
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: case e'_3
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h✝ : ∀ V ∈ 𝓤 α, ∃ N, ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
V : Set (α × α)
mV : V ∈ 𝓤 α
N : ℕ
h : ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
a : ℕ
ha : a ≥ N + k
b : ℕ
hb : b ≥ N + k
⊢ a = a - k + k

pp: case e'_4
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h✝ : ∀ V ∈ 𝓤 α, ∃ N, ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
V : Set (α × α)
mV : V ∈ 𝓤 α
N : ℕ
h : ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
a : ℕ
ha : a ≥ N + k
b : ℕ
hb : b ≥ N + k
⊢ b = b - k + k

Tactic:
<;>

Goal state after:
case e'_3
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h✝ : ∀ V ∈ 𝓤 α, ∃ N, ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
V : Set (α × α)
mV : V ∈ 𝓤 α
N : ℕ
h : ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
a : ℕ
ha : a ≥ N + k
b : ℕ
hb : b ≥ N + k
⊢ a = a - k + k

case e'_4
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h✝ : ∀ V ∈ 𝓤 α, ∃ N, ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
V : Set (α × α)
mV : V ∈ 𝓤 α
N : ℕ
h : ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
a : ℕ
ha : a ≥ N + k
b : ℕ
hb : b ≥ N + k
⊢ b = b - k + k
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
s : Set α
H : ∀ (l : Ultrafilter α), Cauchy ↑l → ↑l ≤ 𝓟 s → ∃ x ∈ s, ↑l ≤ 𝓝 x
l : Filter α
hl : Cauchy l
hls : l ≤ 𝓟 s
⊢ ∃ x ∈ s, ClusterPt x l

Tactic:
have := hl.1

Goal state after:
α : Type u
uniformSpace : UniformSpace α
s : Set α
H : ∀ (l : Ultrafilter α), Cauchy ↑l → ↑l ≤ 𝓟 s → ∃ x ∈ s, ↑l ≤ 𝓝 x
l : Filter α
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
⊢ ∃ x ∈ s, ClusterPt x l
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: case hs
α : 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 α := ⋯
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : l.NeBot
hl' : ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s
t : Set α
htl : t ∈ l
htU : t ×ˢ t ⊆ U
⊢ t ∩ S ⊆ t

pp: case ht
α : 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 α := ⋯
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : l.NeBot
hl' : ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s
t : Set α
htl : t ∈ l
htU : t ×ˢ t ⊆ U
⊢ t ∩ S ⊆ t

Tactic:
<;>

Goal state after:
case hs
α : 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 α := ⋯
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : l.NeBot
hl' : ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s
t : Set α
htl : t ∈ l
htU : t ×ˢ t ⊆ U
⊢ t ∩ S ⊆ t

case ht
α : 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 α := ⋯
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : l.NeBot
hl' : ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s
t : Set α
htl : t ∈ l
htU : t ×ˢ t ⊆ U
⊢ t ∩ S ⊆ t
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: case mp
α : Type ua
inst✝ : UniformSpace α
s : Set α
⊢ (∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s) → ∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] V ∧ ball x V ⊆ s

pp: case mpr
α : Type ua
inst✝ : UniformSpace α
s : Set α
⊢ (∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] V ∧ ball x V ⊆ s) → ∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s

Tactic:
<;>

Goal state after:
case mp
α : Type ua
inst✝ : UniformSpace α
s : Set α
⊢ (∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s) → ∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] V ∧ ball x V ⊆ s

case mpr
α : Type ua
inst✝ : UniformSpace α
s : Set α
⊢ (∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] V ∧ ball x V ⊆ s) → ∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: case left
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : CompleteSpace α
inst✝ : CompleteSpace β
f✝ : Filter (α × β)
hf : Cauchy f✝
x1 : α
hx1 : map (fun p ↦ p.1) f✝ ≤ 𝓝 x1
x2 : β
hx2 : map (fun p ↦ p.2) f✝ ≤ 𝓝 x2
⊢ Tendsto Prod.fst f✝ (𝓝 x1)

pp: case right
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : CompleteSpace α
inst✝ : CompleteSpace β
f✝ : Filter (α × β)
hf : Cauchy f✝
x1 : α
hx1 : map (fun p ↦ p.1) f✝ ≤ 𝓝 x1
x2 : β
hx2 : map (fun p ↦ p.2) f✝ ≤ 𝓝 x2
⊢ Tendsto Prod.snd f✝ (𝓝 x2)

Tactic:
<;>

Goal state after:
case left
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : CompleteSpace α
inst✝ : CompleteSpace β
f✝ : Filter (α × β)
hf : Cauchy f✝
x1 : α
hx1 : map (fun p ↦ p.1) f✝ ≤ 𝓝 x1
x2 : β
hx2 : map (fun p ↦ p.2) f✝ ≤ 𝓝 x2
⊢ Tendsto Prod.fst f✝ (𝓝 x1)

case right
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : CompleteSpace α
inst✝ : CompleteSpace β
f✝ : Filter (α × β)
hf : Cauchy f✝
x1 : α
hx1 : map (fun p ↦ p.1) f✝ ≤ 𝓝 x1
x2 : β
hx2 : map (fun p ↦ p.2) f✝ ≤ 𝓝 x2
⊢ Tendsto Prod.snd f✝ (𝓝 x2)
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : DiscreteUniformity α
f : Filter α
hf : Cauchy f
⊢ ∃ x, f ≤ 𝓝 x

Tactic:
by
    obtain ⟨x, rfl⟩ := eq_pure_of_cauchy hf
    exact ⟨x, pure_le_nhds x⟩

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

Goal state before:
pp: α : Type ua
β : Type ub
f : α → β
u₁ : Set (UniformSpace α)
u₂ : UniformSpace β
u : UniformSpace α
h₁ : u ∈ u₁
hf : UniformContinuous f
⊢ Tendsto (fun x ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)

Tactic:
sInf_eq_iInf',

Goal state after:
α : Type ua
β : Type ub
f : α → β
u₁ : Set (UniformSpace α)
u₂ : UniformSpace β
u : UniformSpace α
h₁ : u ∈ u₁
hf : UniformContinuous f
⊢ Tendsto (fun x ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
f : α → β
u₁ : UniformSpace α
u₂ : Set (UniformSpace β)
⊢ Tendsto (fun x ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β) ↔ ∀ u ∈ u₂, Tendsto (fun x ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)

Tactic:
sInf_eq_iInf',

Goal state after:
α : Type ua
β : Type ub
f : α → β
u₁ : UniformSpace α
u₂ : Set (UniformSpace β)
⊢ Tendsto (fun x ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β) ↔ ∀ u ∈ u₂, Tendsto (fun x ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p' : Filter α
hF : UniformCauchySeqOnFilter F ⊥ p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n ↦ F n x) ⊥ (𝓝 (f x))
⊢ TendstoUniformlyOnFilter F f ⊥ p'

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
⊢ TendstoUniformlyOnFilter F f p p'

Tactic:
· simp only [TendstoUniformlyOnFilter, bot_prod, eventually_bot, implies_true]

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
⊢ TendstoUniformlyOnFilter F f p p'
Module: Mathlib.Topology.UniformSpace.Basic

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

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

Tactic:
<;>

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

case inr
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s✝ : Set (α ⊕ β)
val✝ : β
⊢ s✝ ∈ 𝓝 (inr val✝) ↔
    s✝ ∈ comap (Prod.mk (inr val✝)) (map (fun p ↦ (inl p.1, inl p.2)) (𝓤 α) ⊔ map (fun p ↦ (inr p.1, inr p.2)) (𝓤 β))
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
f : β → α
b : β
⊢ ContinuousAt f b ↔ Tendsto (fun x ↦ (f b, f x)) (𝓝 b) (𝓤 α)

Tactic:
ContinuousAt,

Goal state after:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
f : β → α
b : β
⊢ Tendsto f (𝓝 b) (𝓝 (f b)) ↔ Tendsto (fun x ↦ (f b, f x)) (𝓝 b) (𝓤 α)
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
f : β → α
b : β
⊢ ContinuousAt f b ↔ Tendsto (fun x ↦ (f x, f b)) (𝓝 b) (𝓤 α)

Tactic:
ContinuousAt,

Goal state after:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
f : β → α
b : β
⊢ Tendsto f (𝓝 b) (𝓝 (f b)) ↔ Tendsto (fun x ↦ (f x, f b)) (𝓝 b) (𝓤 α)
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
g : Filter α
⊢ g.TotallyBounded ↔ ∀ (f : Ultrafilter α), ↑f ≤ g → Cauchy ↑f

Tactic:
refine ⟨fun hg f hf => f.cauchy_of_totallyBounded' <| hg.mono hf,
    fun H => g.totallyBounded_iff_filter.2 ?_⟩

Goal state after:
α : Type u
uniformSpace : UniformSpace α
g : Filter α
H : ∀ (f : Ultrafilter α), ↑f ≤ g → Cauchy ↑f
⊢ ∀ (f : Filter α), f.NeBot → f ≤ g → ∃ c ≤ f, Cauchy c
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: case refine_1
α : 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.1 ∈ ↑(setSeqAux hf U_mem N)

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 ∈ ↑(setSeqAux hf U_mem N)

Tactic:
<;>

Goal state after:
case refine_1
α : 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.1 ∈ ↑(setSeqAux hf U_mem N)

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 ∈ ↑(setSeqAux hf U_mem N)
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e : β → α
h_e : IsUniformInducing e
h_dense : DenseRange e
f : β → γ
h_f : UniformContinuous f
inst✝ : CompleteSpace γ
d : Set (γ × γ)
hd : d ∈ 𝓤 γ
s : Set (γ × γ)
hs : s ∈ 𝓤 γ
hs_comp : s ○ (s ○ s) ⊆ d
h_pnt : ∀ {a : α} {m : Set α}, m ∈ 𝓝 a → ∃ c ∈ f '' e ⁻¹' m, (c, ⋯.extend f a) ∈ s ∧ (⋯.extend f a, c) ∈ s
this : Prod.map f f ⁻¹' s ∈ 𝓤 β
⊢ Prod.map f f ⁻¹' s ∈ comap (Prod.map e e) (𝓤 α)

Tactic:
rwa [← h_e.comap_uniformity] at this

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

Goal state before:
pp: case inl
α : Type u_2
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : One β
f : α → β
K : Set α
inst✝ : TopologicalSpace β
hf : Continuous[inst✝², inst✝] f
hk : IsCompact K
h'f : mulSupport f ⊆ K
h2 : range f = f '' K
⊢ IsCompact (range f)

pp: case inr
α : Type u_2
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : One β
f : α → β
K : Set α
inst✝ : TopologicalSpace β
hf : Continuous[inst✝², inst✝] f
hk : IsCompact K
h'f : mulSupport f ⊆ K
h2 : range f = insert 1 (f '' K)
⊢ IsCompact (range f)

Tactic:
<;>

Goal state after:
case inl
α : Type u_2
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : One β
f : α → β
K : Set α
inst✝ : TopologicalSpace β
hf : Continuous[inst✝², inst✝] f
hk : IsCompact K
h'f : mulSupport f ⊆ K
h2 : range f = f '' K
⊢ IsCompact (range f)

case inr
α : Type u_2
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : One β
f : α → β
K : Set α
inst✝ : TopologicalSpace β
hf : Continuous[inst✝², inst✝] f
hk : IsCompact K
h'f : mulSupport f ⊆ K
h2 : range f = insert 1 (f '' K)
⊢ IsCompact (range f)
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:
have := fun i ↦ (hl i).1

Goal state after:
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst✝ : Nonempty ι
l : (i : ι) → Filter (α i)
hl : ∀ (i : ι), Cauchy (l i)
this : ∀ (i : ι), (l i).NeBot
⊢ Cauchy (Filter.pi l)
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
p : Filter ι
hs₁ : IsOpen[inst✝¹] s
hs₂ : IsOpen[inst✝¹] s'
h₁ : TendstoLocallyUniformlyOn F f p s
h₂ : TendstoLocallyUniformlyOn F f p s'
⊢ ∀ s_1 ∈ {s, s'}, IsOpen[inst✝¹] s_1

pp: case refine_2
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
p : Filter ι
hs₁ : IsOpen[inst✝¹] s
hs₂ : IsOpen[inst✝¹] s'
h₁ : TendstoLocallyUniformlyOn F f p s
h₂ : TendstoLocallyUniformlyOn F f p s'
⊢ ∀ s_1 ∈ {s, s'}, TendstoLocallyUniformlyOn F f p s_1

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
p : Filter ι
hs₁ : IsOpen[inst✝¹] s
hs₂ : IsOpen[inst✝¹] s'
h₁ : TendstoLocallyUniformlyOn F f p s
h₂ : TendstoLocallyUniformlyOn F f p s'
⊢ ∀ s_1 ∈ {s, s'}, IsOpen[inst✝¹] s_1

case refine_2
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
p : Filter ι
hs₁ : IsOpen[inst✝¹] s
hs₂ : IsOpen[inst✝¹] s'
h₁ : TendstoLocallyUniformlyOn F f p s
h₂ : TendstoLocallyUniformlyOn F f p s'
⊢ ∀ s_1 ∈ {s, s'}, TendstoLocallyUniformlyOn F f p s_1