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

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✝¹ : LocallyConnectedSpace α
inst✝ : LocallyConnectedSpace β
⊢ LocallyConnectedSpace (α × β)

Tactic:
locallyConnectedSpace_iff_connected_subsets

Goal state after:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝³ : TopologicalSpace α
s t u v : Set α
inst✝² : TopologicalSpace β
inst✝¹ : LocallyConnectedSpace α
inst✝ : LocallyConnectedSpace β
⊢ ∀ (x : α × β), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_1
α : Type u
inst✝ : TopologicalSpace α
s : Set α
x✝ : s.Nonempty ∧ ∀ (u v : Set α), IsOpen[inst✝] u → IsOpen[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
U : Finset (Set α)
hU : ∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v
hUo : ∀ u ∈ U, IsOpen[inst✝] u
hsU : s ⊆ ⋃₀ ↑U
hne : s.Nonempty
h : ∀ (u v : Set α), IsOpen[inst✝] u → IsOpen[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
⊢ ∃ u ∈ U, s ⊆ u

pp: case refine_2
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h :
  ∀ (U : Finset (Set α)),
    (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
      (∀ u ∈ U, IsOpen[inst✝] u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u
⊢ s.Nonempty

pp: case refine_3
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h :
  ∀ (U : Finset (Set α)),
    (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
      (∀ u ∈ U, IsOpen[inst✝] u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u
u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
hsuv : s ∩ (u ∩ v) = ∅
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
· induction U using Finset.induction_on with
    | empty => exact absurd (by simpa using hsU) hne.not_subset_empty
    | insert u U uU IH =>
      simp only [← forall_cond_comm, Finset.forall_mem_insert, Finset.exists_mem_insert,
        Finset.coe_insert, sUnion_insert, implies_true, true_and] at *
      refine (h _ hUo.1 (⋃₀ ↑U) (isOpen_sUnion hUo.2) hsU ?_).imp_right ?_
      · refine subset_empty_iff.1 fun x ⟨hxs, hxu, v, hvU, hxv⟩ => ?_
        exact ne_of_mem_of_not_mem hvU uU (hU.1 v hvU ⟨x, hxs, hxu, hxv⟩).symm
      · exact IH (fun u hu => (hU.2 u hu).2) hUo.2

Goal state after:
case refine_2
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h :
  ∀ (U : Finset (Set α)),
    (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
      (∀ u ∈ U, IsOpen[inst✝] u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u
⊢ s.Nonempty

case refine_3
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h :
  ∀ (U : Finset (Set α)),
    (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
      (∀ u ∈ U, IsOpen[inst✝] u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u
u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
hsuv : s ∩ (u ∩ v) = ∅
⊢ s ⊆ u ∨ s ⊆ v
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_3
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h :
  ∀ (U : Finset (Set α)),
    (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
      (∀ u ∈ U, IsOpen[inst✝] u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u
u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
hsuv : ¬(s ∩ (u ∩ v)).Nonempty
this : ¬(s ∩ (v ∩ u)).Nonempty
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
(Tactic.simpa
 "simpa"
 []
 []
 (Tactic.simpaArgsRest
  (Tactic.optConfig [])
  []
  []
  [(Tactic.simpArgs
    "["
    [(Tactic.simpStar "*") "," (Tactic.simpLemma [] [] `or_imp) "," (Tactic.simpLemma [] [] `forall_and)]
    "]")]
  ["using"
   (Term.app
    `h
    [(choice
      («term{_}» "{" [`u "," `v] "}")
      (Term.structInst
       "{"
       []
       (Term.structInstFields
        [(Term.structInstField (Term.structInstLVal `u []) [])
         ","
         (Term.structInstField (Term.structInstLVal `v []) [])])
       (Term.optEllipsis [])
       []
       "}"))])]))

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set (SeparationQuotient X)
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
⊢ Disjoint (𝓝ˢ (mk ⁻¹' s)) (𝓝ˢ (mk ⁻¹' t))

Tactic:
exact disjoint_nhdsSet_nhdsSet (hs.preimage continuous_mk) (ht.preimage continuous_mk)
      (hd.preimage mk)

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

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : DiscreteTopology X
hs : IsLindelof s
⊢ s.Countable

Tactic:
by
  have : ∀ x : X, ({x} : Set X) ∈ 𝓝 x := by simp [nhds_discrete]
  rcases hs.elim_nhds_subcover (fun x => {x}) fun x _ => this x with ⟨t, ht, _, hssubt⟩
  rw [biUnion_of_singleton] at hssubt
  exact ht.mono hssubt

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hs : IsGδ s
ht : IsGδ t
⊢ IsGδ (s ∩ t)

Tactic:
rw [inter_eq_iInter]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hs : IsGδ s
ht : IsGδ t
⊢ IsGδ (⋂ b, bif b then s else t)
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: 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
⊢ Dense (s ∩ t)

Tactic:
rw [inter_eq_iInter]

Goal state after:
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
⊢ Dense (⋂ b, bif b then s else t)
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_2
α : Type u
β : Type v
ι✝ : Type u_1
X : ι✝ → Type u_2
inst✝ : TopologicalSpace α
s t u v : Set α
ι : Type u_3
U : ι → Set α
hclopen : ∀ (i : ι), IsClopen (U i)
hdisj : Pairwise (Disjoint on U)
hunion : ⋃ i, U i = univ
hconn : ∀ (i : ι), IsPreconnected (U i)
heq : ∀ {x : α} {i : ι} (hx : x ∈ U i), Subtype.val '' connectedComponent ⟨x, hx⟩ = connectedComponent x
x : ConnectedComponents α
⊢ ∃ a,
    (fun x ↦
          match x with
          | ⟨i, x⟩ => Quotient.lift (mk ∘ Subtype.val) ⋯ x)
        a =
      x

Tactic:
· obtain ⟨x, rfl⟩ := ConnectedComponents.surjective_coe x
    obtain ⟨i, hi⟩ := Set.iUnion_eq_univ_iff.mp hunion x
    simp only [Sigma.exists]
    use i, .mk ⟨x, hi⟩
    rfl

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
⊢ DiscreteTopology (ConnectedComponents α) ↔ ∀ (x : α), IsOpen[inst✝] (connectedComponent x)

Tactic:
simp_rw [discreteTopology_iff_isOpen_singleton, ← connectedComponents_preimage_singleton,
    isQuotientMap_coe.isOpen_preimage, surjective_coe.forall]

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

Goal state before:
pp: β : Type v
u : UniformSpace β
α : Type u_1
f : α → β
l : Filter α
⊢ Cauchy l ↔ Cauchy (map f l)

Tactic:
by
  simp only [Cauchy, map_neBot_iff, prod_map_map_eq, map_le_iff_le_comap]
  rfl

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
V : ℕ → SetRel α α
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
hu : CauchySeq u
f g : ℕ → ℕ
hf : Tendsto f atTop atTop
hg : Tendsto g atTop atTop
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), ((u ∘ f ∘ φ) n, (u ∘ g ∘ φ) n) ∈ V n

Tactic:
by
  rw [cauchySeq_iff_tendsto] at hu
  exact ((hu.comp <| hf.prod_atTop hg).comp tendsto_atTop_diagonal).subseq_mem hV

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
f : Filter α
h : f.TotallyBounded
V : SetRel α α
hV : V ∈ 𝓤 α ∧ IsClosed[instTopologicalSpaceProd] V
t : Set α
htf : t.Finite
hst : V.preimage t ∈ f
x : α
hx : x ∈ {x | ClusterPt x f}
⊢ x ∈ ⋃ y ∈ t, {x | (x, y) ∈ id V}

Tactic:
rw [← SetRel.preimage_eq_biUnion, id, ← (hV.2.relPreimage_of_finite htf).closure_eq]

Goal state after:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
h : f.TotallyBounded
V : SetRel α α
hV : V ∈ 𝓤 α ∧ IsClosed[instTopologicalSpaceProd] V
t : Set α
htf : t.Finite
hst : V.preimage t ∈ f
x : α
hx : x ∈ {x | ClusterPt x f}
⊢ x ∈ closure[uniformSpace.toTopologicalSpace] (V.preimage t)
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
⊢ TotallyBounded ∅

Tactic:
exact totallyBounded_empty

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
g : β → γ
hg : IsUniformInducing g
f : α → β
h : IsUniformInducing (g ∘ f)
⊢ comap ((fun x ↦ (g x.1, g x.2)) ∘ fun x ↦ (f x.1, f x.2)) (𝓤 γ) = 𝓤 α

Tactic:
← h.comap_uniformity,

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
g : β → γ
hg : IsUniformInducing g
f : α → β
h : IsUniformInducing (g ∘ f)
⊢ comap ((fun x ↦ (g x.1, g x.2)) ∘ fun x ↦ (f x.1, f x.2)) (𝓤 γ) = comap (fun x ↦ ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 γ)
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 : α
n : ι
hx : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t
hm' : Tendsto (fun x_1 ↦ (f x, F x_1 x)) p (𝓤 β)
⊢ (f x, F n x) ∈ SetRel.comp t t

Tactic:
have := hx.and (hm' ht)

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 : ι
hx : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t
hm' : Tendsto (fun x_1 ↦ (f x, F x_1 x)) p (𝓤 β)
this : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t ∧ (fun x_2 ↦ (f x, F x_2 x)) x_1 ∈ t
⊢ (f x, F n x) ∈ SetRel.comp t t
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
hg : IsUniformInducing g
⊢ map (fun x ↦ (f x.1, f x.2)) (𝓤 α) ≤ 𝓤 β ↔ map (fun x ↦ ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 α) ≤ 𝓤 γ

Tactic:
simp only [← hg.comap_uniformity, ← map_le_iff_le_comap, Filter.map_map, Function.comp_def]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α ≃ β
h₁ : UniformContinuous ⇑f
h₂ : UniformContinuous ⇑f.symm
⊢ comap (⇑(f.prodCongr f)) (𝓤 β) ≤ 𝓤 α

Tactic:
← map_equiv_symm

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α ≃ β
h₁ : UniformContinuous ⇑f
h₂ : UniformContinuous ⇑f.symm
⊢ map (⇑(f.prodCongr f).symm) (𝓤 β) ≤ 𝓤 α
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
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
x : α
hx : x ∈ s
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVU : V ○ V ⊆ U
n : ℕ
ht : x ∈ ⋃ x ∈ t n, ball x (B n)
hn : B n ⊆ V
⊢ (ball x U ∩ ⋃ n, ⋃ x, range (o n x)).Nonempty

Tactic:
rw [mem_iUnion₂] at ht

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
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
x : α
hx : x ∈ s
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVU : V ○ V ⊆ U
n : ℕ
ht : ∃ i, ∃ (_ : i ∈ t n), x ∈ ball i (B n)
hn : B n ⊆ V
⊢ (ball x U ∩ ⋃ n, ⋃ x, range (o n x)).Nonempty
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:
by
  refine of_isClosed fun t ht ↦ IsSeqClosed.isClosed fun u x hut hux ↦ ?_
  rcases isClosed_induced_iff.1 (ht _ (h hux)) with ⟨s, hsc, hst⟩
  rw [Subtype.preimage_val_eq_preimage_val_iff, Set.ext_iff] at hst
  suffices x ∈ s by specialize hst x; simp_all
  refine hsc.mem_of_tendsto hux <| Eventually.of_forall fun k ↦ ?_
  specialize hst (u k)
  simp_all

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

Goal state before:
pp: case e_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
this : UniformSpace.comap (fun x ↦ Prod.fst ∘ x) (uniformSpace α β) ⊓ uniformSpace α (β × γ) = uniformSpace α (β × γ)
⊢ UniformSpace.comap (Prod.fst ∘ ⇑(Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ)) (uniformSpace α β) ⊓
      UniformSpace.comap (Prod.snd ∘ ⇑(Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ)) (uniformSpace α γ) =
    uniformSpace α (β × γ)

Tactic:
UniformFun.comap_eq

Goal state after:
case e_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
this :
  UniformSpace.comap (fun x ↦ Prod.fst ∘ x) (uniformSpace α β) ⊓
      UniformSpace.comap (fun x ↦ Prod.snd ∘ x) (uniformSpace α γ) =
    uniformSpace α (β × γ)
⊢ UniformSpace.comap (Prod.fst ∘ ⇑(Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ)) (uniformSpace α β) ⊓
      UniformSpace.comap (Prod.snd ∘ ⇑(Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ)) (uniformSpace α γ) =
    uniformSpace α (β × γ)
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: case e_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst✝¹ : UniformSpace β
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
i : ι
⊢ UniformSpace.comap (Function.eval i ∘ Function.swap) ((fun i ↦ uniformSpace α (δ i)) i) =
    uniformSpace α ((i : ι) → δ i)

Tactic:
UniformFun.comap_eq

Goal state after:
case e_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst✝¹ : UniformSpace β
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
i : ι
⊢ UniformSpace.comap (Function.eval i ∘ Function.swap) ((fun i ↦ uniformSpace α (δ i)) i) =
    UniformSpace.comap (fun x ↦ Function.eval i ∘ x) (uniformSpace α (δ i))
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
h : c < 0
⊢ (fun x ↦ c * x) ⁻¹' Icc a b = Icc (b / c) (a / c)

Tactic:
simpa only [mul_comm] using preimage_mul_const_Icc_of_neg a b h

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

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
ha : a < 0
x : α
⊢ x ∈ (Ioo a 0)⁻¹ ↔ x ∈ Iio a⁻¹

Tactic:
refine ⟨fun h ↦ (lt_inv_of_neg (inv_neg''.1 h.2) ha).2 h.1, fun h ↦ ?_⟩

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
ha : a < 0
x : α
h : x ∈ Iio a⁻¹
⊢ x ∈ (Ioo a 0)⁻¹
Module: Mathlib.Topology.Algebra.ConstMulAction

Goal state before:
pp: G : Type u_4
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousConstSMul G G
g : G
s : Set G
⊢ g • s ∈ 𝓝 g ↔ s ∈ 𝓝 1

Tactic:
rw [← smul_mem_nhds_smul_iff g⁻¹]; simp

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

Goal state before:
pp: Γ : Type u_4
T : Type u_5
inst✝² : TopologicalSpace T
inst✝¹ : SMul Γ T
inst✝ : ProperlyDiscontinuousSMul Γ T
x : T
⊢ {γ | (HSMul.hSMul γ '' {x} ∩ {x}).Nonempty}.Finite

Tactic:
exact finite_disjoint_inter_image isCompact_singleton isCompact_singleton

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
hg : IsProperMap g
hf : IsProperMap f
ℱ : Filter X
z : Z
h : MapClusterPt z ℱ (g ∘ f)
⊢ ∃ x, (g ∘ f) x = z ∧ ClusterPt x ℱ

Tactic:
mapClusterPt_comp

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
hg : IsProperMap g
hf : IsProperMap f
ℱ : Filter X
z : Z
h : MapClusterPt z (map f ℱ) g
⊢ ∃ x, (g ∘ f) x = z ∧ ClusterPt x ℱ
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: ι : Type u_1
M : Type u_3
X : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f : ι → X → M
l : List ι
t : Set X
h : ∀ i ∈ l, ContinuousOn (f i) t
⊢ ContinuousOn (fun a ↦ (List.map (fun i ↦ f i a) l).prod) t

Tactic:
intro x hx
  rw [continuousWithinAt_iff_continuousAt_domRestrict _ hx]
  refine tendsto_list_prod _ fun i hi => ?_
  specialize h i hi x hx
  rw [continuousWithinAt_iff_continuousAt_domRestrict _ hx] at h
  exact h

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

Goal state before:
pp: α : Type u
β : Type v
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : Group α
inst✝² : MulAction α β
inst✝¹ : ContinuousInv α
inst✝ : ContinuousSMul α β
s : Set α
t : Set β
ht : IsClosed[inst✝⁴] t
hs : IsCompact s
Φ : ↑s × β ≃ₜ ↑s × β :=
  { toFun := fun gx ↦ (gx.1, ↑gx.1 • gx.2), invFun := fun gx ↦ (gx.1, (↑gx.1)⁻¹ • gx.2), left_inv := ⋯, right_inv := ⋯,
    continuous_toFun := ⋯, continuous_invFun := ⋯ }
this✝ : s • t = snd ∘ ⇑Φ '' snd ⁻¹' t
this : CompactSpace ↑s
⊢ IsClosed[inst✝⁴] (snd ∘ ⇑Φ '' snd ⁻¹' t)

Tactic:
exact (isProperMap_snd_of_compactSpace.comp Φ.isProperMap).isClosedMap _
    (ht.preimage continuous_snd)

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

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this :
  (fun x ↦ x.1.2 * x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹)) = (fun p ↦ p.1 * p.2⁻¹) ∘ fun p ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹)
⊢ Tendsto (fun p ↦ p.1 * p.2⁻¹) (𝓝 (1, 1)) (𝓝 1)

Tactic:
nth_rewrite 3 [show (1 : G) = 1 * 1⁻¹ by simp]

Goal state after:
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this :
  (fun x ↦ x.1.2 * x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹)) = (fun p ↦ p.1 * p.2⁻¹) ∘ fun p ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹)
⊢ Tendsto (fun p ↦ p.1 * p.2⁻¹) (𝓝 (1, 1)) (𝓝 (1 * 1⁻¹))
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ¬K * L⁻¹ = univ
⊢ ∃ g, Disjoint K (g • L)

Tactic:
obtain ⟨g, hg⟩ : ∃ g, g ∉ K * L⁻¹ := by
    contrapose! A
    exact eq_univ_iff_forall.2 A

Goal state after:
G : Type w
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ¬K * L⁻¹ = univ
g : G
hg : g ∉ K * L⁻¹
⊢ ∃ g, Disjoint K (g • L)
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
x y : G
⊢ map₂ (fun a b ↦ x * a * (b * y)) (𝓝 1) (𝓝 1) = map₂ (fun a b ↦ x * a * b) (𝓝 1) (map (fun x ↦ x * y) (𝓝 1))

Tactic:
map₂_map_right

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
x y : G
⊢ map₂ (fun a b ↦ x * a * (b * y)) (𝓝 1) (𝓝 1) = map₂ (fun a b ↦ x * a * (b * y)) (𝓝 1) (𝓝 1)
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
⊢ G ≃ᵤ G

Tactic:
have A : @UniformContinuous G G (IsTopologicalGroup.rightUniformSpace G)
      (IsTopologicalGroup.leftUniformSpace G) (Equiv.inv G) := by
    apply uniformContinuous_iff_le_comap.2
    rw [← comap_inv_leftUniformSpace]

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
A : UniformContinuous ⇑(Equiv.inv G)
⊢ G ≃ᵤ G
Module: Mathlib.Order.Filter.AtTopBot.CompleteLattice

Goal state before:
pp: α : Type u_6
inst✝¹ : Subsingleton α
inst✝ : Preorder α
s : Set α
hs : s ∈ atTop
x : α
⊢ x ∈ s

Tactic:
atTop,

Goal state after:
α : Type u_6
inst✝¹ : Subsingleton α
inst✝ : Preorder α
s : Set α
hs : s ∈ ⨅ a, 𝓟 (Ici a)
x : α
⊢ x ∈ s
Module: Mathlib.Order.OrdContinuous

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : α → β
hf : LeftOrdContinuous f
s : Set α
hs : s.Nonempty
⊢ f (sSup s) = ⨆ x ∈ s, f x

Tactic:
rw [hf.map_sSup' hs, sSup_image]

Goal state after:
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → Preorder (α i)
x y✝ y : (i : ι) → α i
⊢ (y ∈ univ.pi fun i ↦ Icc (x i) (y✝ i)) ↔ y ∈ Icc x y✝

Tactic:
simp [Pi.le_def, forall_and]

Goal state after:
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a : α i
⊢ update f i '' Ico a (f i) = Ico (update f i a) f

Tactic:
by simpa using image_update_Ico f i a (f i)

Goal state after:
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
t : Set α := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
y : α → α
hy : ∀ x ∈ t, y x > x
h'y : ∀ x ∈ t, s ∩ Ioo x (y x) = ∅
⊢ ∀ ⦃x : α⦄, x ∈ t → ∀ ⦃y_1 : α⦄, y_1 ∈ t → x ≠ y_1 → Disjoint (Ioo x (y x)) (Ioo y_1 (y y_1))

Tactic:
intro a ha b hb hab

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
t : Set α := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
y : α → α
hy : ∀ x ∈ t, y x > x
h'y : ∀ x ∈ t, s ∩ Ioo x (y x) = ∅
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
⊢ Disjoint (Ioo a (y a)) (Ioo b (y b))