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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht' : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
T₁_u : f ⁻¹' T₁ = f ⁻¹' t ∩ u
T₂_v : f ⁻¹' T₂ = f ⁻¹' t ∩ v
hT₁ : IsClosed[inst✝] T₁
hT₂ : IsClosed[inst✝] T₂
T_decomp : t ⊆ T₁ ∪ T₂
T_disjoint : Disjoint T₁ T₂
⊢ f ⁻¹' t ⊆ u ∨ f ⁻¹' t ⊆ v

Tactic:
rcases (isPreconnected_iff_subset_of_fully_disjoint_closed ht).1
    ht'.isPreconnected T₁ T₂ hT₁ hT₂ T_decomp T_disjoint with h | h

Goal state after:
case inl
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht' : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
T₁_u : f ⁻¹' T₁ = f ⁻¹' t ∩ u
T₂_v : f ⁻¹' T₂ = f ⁻¹' t ∩ v
hT₁ : IsClosed[inst✝] T₁
hT₂ : IsClosed[inst✝] T₂
T_decomp : t ⊆ T₁ ∪ T₂
T_disjoint : Disjoint T₁ T₂
h : t ⊆ T₁
⊢ f ⁻¹' t ⊆ u ∨ f ⁻¹' t ⊆ v

case inr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht' : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
T₁_u : f ⁻¹' T₁ = f ⁻¹' t ∩ u
T₂_v : f ⁻¹' T₂ = f ⁻¹' t ∩ v
hT₁ : IsClosed[inst✝] T₁
hT₂ : IsClosed[inst✝] T₂
T_decomp : t ⊆ T₁ ∪ T₂
T_disjoint : Disjoint T₁ T₂
h : t ⊆ T₂
⊢ f ⁻¹' t ⊆ u ∨ f ⁻¹' t ⊆ v
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
⊢ ⋂ s, ↑s ⊆ a ∨ ⋂ s, ↑s ⊆ b

Tactic:
obtain ⟨s, H⟩ : ∃ s : Set X, IsClopen s ∧ x ∈ s ∧ s ⊆ u ∪ v := by
    /- Now we find a clopen set `s` around `x`, contained in `u ∪ v`. We utilize the fact that
    `X \ u ∪ v` will be compact, so there must be some finite intersection of clopen neighbourhoods
    of `X` disjoint to it, but a finite intersection of clopen sets is clopen,
    so we let this be our `s`. -/
    have H1 := (hu.union hv).isClosed_compl.isCompact.inter_iInter_nonempty
      (fun s : { s : Set X // IsClopen s ∧ x ∈ s } => s) fun s => s.2.1.1
    rw [← not_disjoint_iff_nonempty_inter, imp_not_comm, not_forall] at H1
    obtain ⟨si, H2⟩ :=
      H1 (disjoint_compl_left_iff_subset.2 <| hab.trans <| union_subset_union hau hbv)
    refine ⟨⋂ U ∈ si, Subtype.val U, ?_, ?_, ?_⟩
    · exact isClopen_biInter_finset fun s _ => s.2.1
    · exact mem_iInter₂.2 fun s _ => s.2.2
    · rwa [← disjoint_compl_left_iff_subset, disjoint_iff_inter_eq_empty,
        ← not_nonempty_iff_eq_empty]

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
s : Set X
H : IsClopen s ∧ x ∈ s ∧ s ⊆ u ∪ v
⊢ ⋂ s, ↑s ⊆ a ∨ ⋂ s, ↑s ⊆ b
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case inr.succ.zero
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : Infinite (ConnectedComponents α)
h✝ : Nonempty α
⊢ ∃ U,
    (∀ (i : Fin (0 + 1)), IsClopen (U i)) ∧
      (∀ (i : Fin (0 + 1)), (U i).Nonempty) ∧ Pairwise (Disjoint on U) ∧ ⋃ i, U i = univ

Tactic:
exact ⟨![.univ], by simp [isClopen_univ, Set.iUnion_fin_add_one_eq_iUnion_succ]⟩

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

Goal state before:
pp: X : Type u_1
R : SetRel X X
s : Set X
x : X
inst✝ : R.IsSymm
⊢ R.IsSeparated (insert x s) ↔ R.IsSeparated s ∧ ∀ (y : X), y ∈ s → (x, y) ∈ R → x = y

Tactic:
have : Std.Symm fun x y ↦ ¬(x, y) ∈ R := { symm _ _ := mt R.symm }

Goal state after:
X : Type u_1
R : SetRel X X
s : Set X
x : X
inst✝ : R.IsSymm
this : Std.Symm fun x y ↦ ¬(x, y) ∈ R
⊢ R.IsSeparated (insert x s) ↔ R.IsSeparated s ∧ ∀ (y : X), y ∈ s → (x, y) ∈ R → x = y
Module: Mathlib.Data.Rel.Separated

Goal state before:
pp: X : Type u_1
R : SetRel X X
s : Set X
x : X
inst✝ : R.IsSymm
this : Std.Symm fun x y ↦ ¬(x, y) ∈ R
⊢ R.IsSeparated (insert x s) ↔ R.IsSeparated s ∧ ∀ (y : X), y ∈ s → (x, y) ∈ R → x = y

Tactic:
simpa [not_imp_not, IsSeparated] using pairwise_insert_of_symm (r := fun x y ↦ ¬(x, y) ∈ R)

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

Goal state before:
pp: case inr.succ.succ.cons.refine_1
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : Infinite (ConnectedComponents α)
h✝ : Nonempty α
n : ℕ
i : Fin (n + 1)
U : Fin n → Set α
a b : Set α
ha : IsClopen a
hb : IsClopen b
ha' : a.Nonempty
hb' : b.Nonempty
hab : Disjoint a b
h₃ : Pairwise (Disjoint on (Equiv.piCongrLeft (fun x ↦ Set α) (Equiv.swap 0 i)).symm (Fin.cons (a ∪ b) U))
h₁ : ∀ (i_1 : Fin (n + 1)), IsClopen (Fin.cons (a ∪ b) U ((Equiv.swap 0 i) i_1))
h₂ : ∀ (i_1 : Fin (n + 1)), (Fin.cons (a ∪ b) U ((Equiv.swap 0 i) i_1)).Nonempty
h₄ : ⋃ i_1, Fin.cons (a ∪ b) U ((Equiv.swap 0 i) i_1) = univ
hi : ¬IsConnected (a ∪ b)
⊢ ∀ (i : Fin (n + 1 + 1)), IsClopen (Fin.cons a (Fin.cons b U) i)

Tactic:
simpa [Fin.forall_iff_succ, *] using fun x ↦ h₁ (Equiv.swap 0 i (.succ x))

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
⊢ (∃ t ∈ 𝓤 α, Prod.mk x ⁻¹' t ⊆ s) ↔ ∃ V ∈ 𝓤 α, ball x V ⊆ s

Tactic:
simp_rw [ball]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
⊢ UniformCauchySeqOn F p s ↔ UniformCauchySeqOnFilter F p (𝓟 s)

Tactic:
simp only [UniformCauchySeqOn, UniformCauchySeqOnFilter]
  refine forall₂_congr fun u hu => ?_
  rw [eventually_prod_principal_iff]

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
a : α
s : Set α
⊢ TotallyBounded (insert a s) ↔ TotallyBounded s

Tactic:
← singleton_union,

Goal state after:
α : Type u
uniformSpace : UniformSpace α
a : α
s : Set α
⊢ TotallyBounded ({a} ∪ s) ↔ TotallyBounded s
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: α : Type u_2
M : Type u_7
R : Type u_8
inst✝² : TopologicalSpace α
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
f : α → R
f' : α → M
hf : HasCompactSupport f'
⊢ HasCompactSupport (f • f')

Tactic:
by
  rw [hasCompactSupport_iff_eventuallyEq] at hf ⊢
  exact hf.mono fun x hx => by simp_rw [Pi.smul_apply', hx, Pi.zero_apply, smul_zero]

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
inst✝ : (𝓤 α).IsCountablyGenerated
s : Set α
B : ℕ → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
right✝ : ∀ (n : ℕ), (B n).IsSymm
t : ℕ → Set α
tC : ∀ (n : ℕ), (t n).Countable
ht : ∀ (n : ℕ), s ⊆ ⋃ x ∈ t n, ball x (B n)
this : ∀ (n : ℕ), Countable ↑(t n)
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ closure[uniformSpace.toTopologicalSpace] t

Tactic:
choose o hox hos using fun (n : ℕ) (x : t n) (hx : (ball x.1 (B n) ∩ s).Nonempty) => hx

Goal state after:
α : Type u
uniformSpace : UniformSpace α
inst✝ : (𝓤 α).IsCountablyGenerated
s : Set α
B : ℕ → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
right✝ : ∀ (n : ℕ), (B n).IsSymm
t : ℕ → Set α
tC : ∀ (n : ℕ), (t n).Countable
ht : ∀ (n : ℕ), s ⊆ ⋃ x ∈ t n, ball x (B n)
this : ∀ (n : ℕ), Countable ↑(t n)
o : (n : ℕ) → (x : ↑(t n)) → (ball (↑x) (B n) ∩ s).Nonempty → α
hox : ∀ (n : ℕ) (x : ↑(t n)) (hx : (ball (↑x) (B n) ∩ s).Nonempty), o n x hx ∈ ball (↑x) (B n)
hos : ∀ (n : ℕ) (x : ↑(t n)) (hx : (ball (↑x) (B n) ∩ s).Nonempty), o n x hx ∈ s
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ closure[uniformSpace.toTopologicalSpace] t
Module: Mathlib.Topology.UniformSpace.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
S : Set ι
⊢ UniformSpace.comap S.domRestrict (uniformSpace fun i ↦ α ↑i) = ⨅ i ∈ S, UniformSpace.comap (eval i) (U i)

Tactic:
by
  simp +unfoldPartialApp
    [← iInf_subtype'', ← uniformSpace_comap_precomp' _ ((↑) : S → ι), Set.domRestrict]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
x : α
hx : x ∈ s
L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∃ F, ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u
u₀ : Set (β × β)
hu₀ : u₀ ∈ 𝓤 β
u₁ : Set (β × β)
h₁ : u₁ ∈ 𝓤 β
u₁₀ : u₁ ○ u₁ ⊆ u₀
u₂ : Set (β × β)
h₂ : u₂ ∈ 𝓤 β
hsymm : ∀ {a b : β}, (a, b) ∈ u₂ → (b, a) ∈ u₂
u₂₁ : u₂ ○ u₂ ⊆ u₁
⊢ u₀ ∈ map (fun x_1 ↦ (f x_1, f x)) (𝓝[s] x)

Tactic:
rcases L u₂ h₂ with ⟨t, tx, F, hFc, hF⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
x : α
hx : x ∈ s
L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∃ F, ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u
u₀ : Set (β × β)
hu₀ : u₀ ∈ 𝓤 β
u₁ : Set (β × β)
h₁ : u₁ ∈ 𝓤 β
u₁₀ : u₁ ○ u₁ ⊆ u₀
u₂ : Set (β × β)
h₂ : u₂ ∈ 𝓤 β
hsymm : ∀ {a b : β}, (a, b) ∈ u₂ → (b, a) ∈ u₂
u₂₁ : u₂ ○ u₂ ⊆ u₁
t : Set α
tx : t ∈ 𝓝[s] x
F : α → β
hFc : ContinuousWithinAt F s x
hF : ∀ y ∈ t, (f y, F y) ∈ u₂
⊢ u₀ ∈ map (fun x_1 ↦ (f x_1, f x)) (𝓝[s] x)
Module: Mathlib.Topology.UniformSpace.UniformApproximation

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
g : ι → α
h : ContinuousAt f x
hg : Tendsto g p (𝓝 x)
hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
⊢ Tendsto (fun n ↦ F n (g n)) p (𝓝 (f x))

Tactic:
rw [← continuousWithinAt_univ] at h
  rw [← nhdsWithin_univ] at hunif hg
  exact tendsto_comp_of_locally_uniform_limit_within h hg hunif

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 ι
h : ∀ (x : α), ∃ t ∈ 𝓝 x, TendstoUniformlyOn F f p t
⊢ ∀ x ∈ univ, ∃ t ∈ 𝓝[univ] x, TendstoUniformlyOn F f p t

Tactic:
by simpa using h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
⊢ UniformContinuous ⇑toFun

Tactic:
rw [uniformContinuous_pi]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
⊢ ∀ (i : α), UniformContinuous fun x ↦ toFun x i
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
⊢ (∀ (x₀ : X), EquicontinuousAt F x₀) ↔ Continuous[tX, topologicalSpace ι α] (⇑ofFun ∘ swap F)

Tactic:
continuous_iff_continuousAt,

Goal state after:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
⊢ (∀ (x₀ : X), EquicontinuousAt F x₀) ↔ ∀ (x : X), ContinuousAt (⇑ofFun ∘ swap F) x
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
hd : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) 𝔖
x✝¹ : Set α × ι'
s : Set α
i' : ι'
x✝ : (s, i').1 ∈ 𝔖 ∧ p (s, i').2
hs : (s, i').1 ∈ 𝔖
hi' : p (s, i').2
i : ι
hi : s ⊆ t i
⊢ ∃ i'_1, p i'_1.2 ∧ UniformOnFun.gen 𝔖 (t i'_1.1) (V i'_1.2) ⊆ UniformOnFun.gen 𝔖 (s, i').1 (V (s, i').2)

Tactic:
exact ⟨(i, i'), hi', UniformOnFun.gen_mono hi Subset.rfl⟩

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝² : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
t : ι → Set α
V : ι → Set (β × β)
ht : ∀ (n : ι), t n ∈ 𝔖
hmono : Monotone t
hex : ∀ s ∈ 𝔖, ∃ n, s ⊆ t n
hb : (𝓤 β).HasAntitoneBasis V
this : Nonempty ι
⊢ Antitone fun n ↦ UniformOnFun.gen 𝔖 (t n) (V n)

Tactic:
exact fun k l h ↦ UniformOnFun.gen_mono (hmono h) (hb.2 h)

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

Goal state before:
pp: Y : Type u_5
α : Type u_6
β : Type u_8
tY : TopologicalSpace Y
uα : UniformSpace α
uβ : UniformSpace β
A : Set Y
u : Y → β → α
hA : UniformEquicontinuous (u ∘ Subtype.val)
hu : Continuous[tY, Pi.topologicalSpace] u
⊢ UniformEquicontinuous (u ∘ Subtype.val)

Tactic:
rw [← uniformEquicontinuousOn_univ] at hA ⊢
  exact hA.closure' (Pi.continuous_domRestrict _ |>.comp hu)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
⊢ UniformContinuous ((⋃₀ 𝔖).domRestrict ∘ ⇑(toFun 𝔖))

Tactic:
rw [uniformContinuous_pi]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
⊢ ∀ (i : ↑(⋃₀ 𝔖)), UniformContinuous fun x ↦ ((⋃₀ 𝔖).domRestrict ∘ ⇑(toFun 𝔖)) x i
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : ⋃₀ 𝔖 = univ
⊢ UniformContinuous ⇑(toFun 𝔖)

Tactic:
rw [uniformContinuous_pi]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : ⋃₀ 𝔖 = univ
⊢ ∀ (i : α), UniformContinuous fun x ↦ (toFun 𝔖) x i
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: case refine_1.refine_2
α : Type u_2
inst✝ : DivisionMonoid α
f g : Filter α
hfg✝ : f * g = 1
hfg : (f * g).NeBot
a b : α
h₁ : {a} ∈ f
h : a * b = 1
h₂ : {b} ∈ g
⊢ g = pure b

Tactic:
· rwa [← hfg.of_mul_right.le_pure_iff, le_pure_iff]

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

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
inst✝³ : T2Space T
inst✝² : LocallyCompactSpace T
inst✝¹ : ContinuousConstSMul Γ T
inst✝ : ProperlyDiscontinuousSMul Γ T
⊢ T2Space (Quotient (MulAction.orbitRel Γ T))

Tactic:
by
  let := MulAction.orbitRel Γ T
  set Q := Quotient (MulAction.orbitRel Γ T)
  rw [t2Space_iff_nhds]
  let f : T → Q := Quotient.mk'
  have f_op : IsOpenMap f := isOpenMap_quotient_mk'_mul
  rintro ⟨x₀⟩ ⟨y₀⟩ (hxy : f x₀ ≠ f y₀)
  change ∃ U ∈ 𝓝 (f x₀), ∃ V ∈ 𝓝 (f y₀), _
  have hγx₀y₀ : ∀ γ : Γ, γ • x₀ ≠ y₀ := not_exists.mp (mt Quotient.sound hxy.symm :)
  obtain ⟨K₀, hK₀, K₀_in⟩ := exists_compact_mem_nhds x₀
  obtain ⟨L₀, hL₀, L₀_in⟩ := exists_compact_mem_nhds y₀
  let bad_Γ_set := { γ : Γ | ((γ • ·) '' K₀ ∩ L₀).Nonempty }
  have bad_Γ_finite : bad_Γ_set.Finite := finite_disjoint_inter_image (Γ := Γ) hK₀ hL₀
  choose u v hu hv u_v_disjoint using fun γ => t2_separation_nhds (hγx₀y₀ γ)
  let U₀₀ := ⋂ γ ∈ bad_Γ_set, (γ • ·) ⁻¹' u γ
  let U₀ := U₀₀ ∩ K₀
  let V₀₀ := ⋂ γ ∈ bad_Γ_set, v γ
  let V₀ := V₀₀ ∩ L₀
  have U_nhds : f '' U₀ ∈ 𝓝 (f x₀) := by
    refine f_op.image_mem_nhds (inter_mem ((biInter_mem bad_Γ_finite).mpr fun γ _ => ?_) K₀_in)
    exact (continuous_const_smul _).continuousAt (hu γ)
  have V_nhds : f '' V₀ ∈ 𝓝 (f y₀) :=
    f_op.image_mem_nhds (inter_mem ((biInter_mem bad_Γ_finite).mpr fun γ _ => hv γ) L₀_in)
  refine ⟨f '' U₀, U_nhds, f '' V₀, V_nhds, MulAction.disjoint_image_image_iff.2 ?_⟩
  rintro x ⟨x_in_U₀₀, x_in_K₀⟩ γ
  by_cases H : γ ∈ bad_Γ_set
  · exact fun h => (u_v_disjoint γ).le_bot ⟨mem_iInter₂.mp x_in_U₀₀ γ H, mem_iInter₂.mp h.1 γ H⟩
  · rintro ⟨-, h'⟩
    simp only [bad_Γ_set, image_smul, not_nonempty_iff_eq_empty, mem_ofPred_eq] at H
    exact eq_empty_iff_forall_notMem.mp H (γ • x) ⟨mem_image_of_mem _ x_in_K₀, h'⟩

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

Goal state before:
pp: case mp
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : IsProperMap f
⊢ Continuous[inst✝¹, inst✝] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})

Tactic:
exact ⟨H.continuous, H.isClosedMap, fun y ↦ H.isCompact_preimage isCompact_singleton⟩

Goal state after:
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: Gₗ : Type u_2
inst✝² : UniformSpace Gₗ
inst✝¹ : Group Gₗ
inst✝ : IsLeftUniformGroup Gₗ
⊢ 𝓤 Gₗ = comap (fun x ↦ x.2⁻¹ * x.1) (𝓝 1)

Tactic:
by
  rw [← comap_swap_uniformity, uniformity_eq_comap_inv_mul_nhds_one, comap_comap, Function.comp_def]
  simp

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
K : Set G
hK : IsCompact K
x : G
h : K ∈ 𝓝 x
y : G
⊢ K ∈ 𝓝 ((y * x⁻¹)⁻¹ • y)

Tactic:
by simpa using h

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Monoid

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedCancelMonoid M
l : Filter α
f g : α → M
hfg : Tendsto (fun x ↦ f x * g x) l atTop
C : M
hC : ∀ᶠ (x : M) in map f l, (fun x1 x2 ↦ x1 ≤ x2) x C
x✝¹ : α
x✝ : (fun x1 x2 ↦ x1 ≤ x2) (f x✝¹) C
⊢ (fun x ↦ f x * g x) x✝¹ ≤ (fun x ↦ C * g x) x✝¹

Tactic:
dsimp; gcongr

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Monoid

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedCancelMonoid M
l : Filter α
f g : α → M
h : Tendsto (fun x ↦ f x * g x) l atTop
C : M
hC : ∀ᶠ (x : M) in map g l, (fun x1 x2 ↦ x1 ≤ x2) x C
x✝¹ : α
x✝ : (fun x1 x2 ↦ x1 ≤ x2) (g x✝¹) C
⊢ (fun x ↦ f x * g x) x✝¹ ≤ (fun x ↦ f x * C) x✝¹

Tactic:
dsimp; gcongr

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (⇑S.subtype) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
⊢ {γ | ((fun x ↦ γ • x) '' K ∩ L).Nonempty}.Finite

Tactic:
have H : Set.Finite _ := hS ((hL.prod hK).image continuous_div').compl_mem_cocompact

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (⇑S.subtype) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
H : (⇑S.subtype ⁻¹' ((fun p ↦ p.1 / p.2) '' L ×ˢ K)ᶜ)ᶜ.Finite
⊢ {γ | ((fun x ↦ γ • x) '' K ∩ L).Nonempty}.Finite
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: α : Type u
inst✝³ : Monoid α
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : ContinuousMul α
⊢ IsClosed[instTopologicalSpaceProd] (range ⇑(embedProduct α))

Tactic:
rw [range_embedProduct]

Goal state after:
α : Type u
inst✝³ : Monoid α
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : ContinuousMul α
⊢ IsClosed[instTopologicalSpaceProd] {p | p.1 * unop p.2 = 1 ∧ unop p.2 * p.1 = 1}
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: case refine_1
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
x : (a : ι) → α a
⊢ x ∈ update f i '' Icc a b → x ∈ univ.pi fun i_1 ↦ Icc (update f i a i_1) (update f i b i_1)

pp: case refine_2
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
x : (a : ι) → α a
h : x ∈ univ.pi fun i_1 ↦ Icc (update f i a i_1) (update f i b i_1)
⊢ x i ∈ Icc a b

pp: case refine_3
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
x : (a : ι) → α a
h : x ∈ univ.pi fun i_1 ↦ Icc (update f i a i_1) (update f i b i_1)
⊢ update f i (x i) = x

Tactic:
· rintro ⟨c, hc, rfl⟩
    simpa [update_le_update_iff]

Goal state after:
case refine_2
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
x : (a : ι) → α a
h : x ∈ univ.pi fun i_1 ↦ Icc (update f i a i_1) (update f i b i_1)
⊢ x i ∈ Icc a b

case refine_3
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
x : (a : ι) → α a
h : x ∈ univ.pi fun i_1 ↦ Icc (update f i a i_1) (update f i b i_1)
⊢ update f i (x i) = x
Module: Mathlib.Topology.Algebra.Order.Group

Goal state before:
pp: G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
⊢ ∀ (a b ε : G), ε > 1 → ∀ᶠ (b_1 : G × G) in 𝓝 (a, b), |b_1.1 * b_1.2 / (a * b)|ₘ < ε

Tactic:
intro a b ε hε

Goal state after:
G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a b ε : G
hε : ε > 1
⊢ ∀ᶠ (b_1 : G × G) in 𝓝 (a, b), |b_1.1 * b_1.2 / (a * b)|ₘ < ε
Module: Mathlib.Topology.Algebra.Order.Field

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℕ
c d : 𝕜
⊢ Tendsto (fun x ↦ c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)
  · simp [tendsto_const_nhds_iff]
  rcases lt_trichotomy c 0 with (hc | rfl | hc)
  · have := tendsto_const_mul_pow_atBot_iff.2 ⟨hn, hc⟩
    simp [not_tendsto_nhds_of_tendsto_atBot this, hc.ne, hn]
  · simp [tendsto_const_nhds_iff]
  · have := tendsto_const_mul_pow_atTop_iff.2 ⟨hn, hc⟩
    simp [not_tendsto_nhds_of_tendsto_atTop this, hc.ne', hn]

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: case left
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
he : e ≈ e'
s : Set α
⊢ (e.restr s).source = (e'.restr s).source

Tactic:
simp [he.1]

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : PartialEquiv α β
e'✝ : PartialEquiv β γ
e : PartialEquiv α β
e' : PartialEquiv γ δ
p : α × γ
hp : p ∈ e.source ×ˢ e'.source
⊢ (↑e p.1, ↑e' p.2) ∈ e.target ×ˢ e'.target

Tactic:
by simp_all

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : PartialEquiv α β
e'✝ : PartialEquiv β γ
e : PartialEquiv α β
e' : PartialEquiv γ δ
p : β × δ
hp : p ∈ e.target ×ˢ e'.target
⊢ (↑e.symm p.1, ↑e'.symm p.2) ∈ e.source ×ˢ e'.source

Tactic:
by simp_all

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : PartialEquiv α β
e'✝ : PartialEquiv β γ
e : PartialEquiv α β
e' : PartialEquiv γ δ
p : α × γ
hp : p ∈ e.source ×ˢ e'.source
⊢ (↑e.symm (↑e p.1, ↑e' p.2).1, ↑e'.symm (↑e p.1, ↑e' p.2).2) = p

Tactic:
by simp_all

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : PartialEquiv α β
e'✝ : PartialEquiv β γ
e : PartialEquiv α β
e' : PartialEquiv γ δ
p : β × δ
hp : p ∈ e.target ×ˢ e'.target
⊢ (↑e (↑e.symm p.1, ↑e'.symm p.2).1, ↑e' (↑e.symm p.1, ↑e'.symm p.2).2) = p

Tactic:
by simp_all

Goal state after: