mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α : Type ua
β : Type ub
inst✝ : UniformSpace α
x : α
g : Set α → Filter β
hg : Monotone g
⊢ (comap (Prod.mk x) (𝓤 α)).lift g = (𝓤 α).lift fun s ↦ g (ball x s)

Tactic:
comap_lift_eq2 hg

Goal state after:
α : Type ua
β : Type ub
inst✝ : UniformSpace α
x : α
g : Set α → Filter β
hg : Monotone g
⊢ (𝓤 α).lift (g ∘ preimage (Prod.mk x)) = (𝓤 α).lift fun s ↦ g (ball x s)
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α : Type ua
β : Type ub
inst✝ : UniformSpace α
x : α
g : Set α → Filter β
hg : Monotone g
⊢ (comap (fun y ↦ (y, x)) (𝓤 α)).lift g = (𝓤 α).lift fun s ↦ g {y | (y, x) ∈ s}

Tactic:
comap_lift_eq2 hg

Goal state after:
α : Type ua
β : Type ub
inst✝ : UniformSpace α
x : α
g : Set α → Filter β
hg : Monotone g
⊢ (𝓤 α).lift (g ∘ preimage fun y ↦ (y, x)) = (𝓤 α).lift fun s ↦ g {y | (y, x) ∈ s}
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : SetRel β β
f : α → α → β
hf : UniformContinuous fun p ↦ f p.1 p.2
hs : s ∈ 𝓤 β
⊢ ∃ u ∈ 𝓤 α, ∀ (a b c : α), (a, b) ∈ u → (f a c, f b c) ∈ s

Tactic:
rw [UniformContinuous, uniformity_prod_eq_prod, tendsto_map'_iff] at hf

Goal state after:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : SetRel β β
f : α → α → β
hf : Tendsto ((fun x ↦ (f x.1.1 x.1.2, f x.2.1 x.2.2)) ∘ fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 α) (𝓤 β)
hs : s ∈ 𝓤 β
⊢ ∃ u ∈ 𝓤 α, ∀ (a b c : α), (a, b) ∈ u → (f a c, f b c) ∈ s
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: α : Type u_1
u : UniformSpace α
inst✝ : IndiscreteTopology α
x : α × α
⊢ x ∈ (𝓤 α).ker ↔ x ∈ univ

Tactic:
← inseparable_iff_ker_uniformity

Goal state after:
α : Type u_1
u : UniformSpace α
inst✝ : IndiscreteTopology α
x : α × α
⊢ Inseparable x.1 x.2 ↔ x ∈ univ
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set ((α ⊕ β) × (α ⊕ β))
hs : s ∈ map (fun p ↦ (inl p.1, inl p.2)) (𝓤 α) ⊔ map (fun p ↦ (inr p.1, inr p.2)) (𝓤 β)
⊢ s ∈ (map (fun p ↦ (inl p.1, inl p.2)) (𝓤 α) ⊔ map (fun p ↦ (inr p.1, inr p.2)) (𝓤 β)).lift' fun s ↦ s ○ s

Tactic:
by
    rcases comp_mem_uniformity_sets hs.1 with ⟨tα, htα, Htα⟩
    rcases comp_mem_uniformity_sets hs.2 with ⟨tβ, htβ, Htβ⟩
    filter_upwards [mem_lift' (union_mem_sup (image_mem_map htα) (image_mem_map htβ))]
    rintro ⟨_, _⟩ ⟨z, ⟨⟨a, b⟩, hab, ⟨⟩⟩ | ⟨⟨a, b⟩, hab, ⟨⟩⟩, ⟨⟨_, c⟩, hbc, ⟨⟩⟩ | ⟨⟨_, c⟩, hbc, ⟨⟩⟩⟩
    exacts [@Htα (_, _) ⟨b, hab, hbc⟩, @Htβ (_, _) ⟨b, hab, hbc⟩]

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 : IsUniformEmbedding g
f : α → β
⊢ IsUniformEmbedding (g ∘ f) ↔ IsUniformEmbedding f

Tactic:
by
  simp_rw [isUniformEmbedding_iff, hg.isUniformInducing.of_comp_iff, hg.injective.of_comp_iff f]

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 ι
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst✝ : UniformSpace β'
F' : ι' → α' → β'
p' : Filter ι'
s' : Set α'
h : UniformCauchySeqOn F p s
h' : UniformCauchySeqOn F' p' s'
u : Set ((β × β') × β × β')
v : Set (β × β)
hv : v ∈ 𝓤 β
w : Set (β' × β')
hw : w ∈ 𝓤 β'
hvw : (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) '' v ×ˢ w ⊆ u
x : (ι × ι') × ι × ι'
hx :
  (∀ x_1 ∈ s, (F ((x.1.1, x.2.1), x.1.2, x.2.2).1.1 x_1, F ((x.1.1, x.2.1), x.1.2, x.2.2).1.2 x_1) ∈ v) ∧
    ∀ x_1 ∈ s', (F' ((x.1.1, x.2.1), x.1.2, x.2.2).2.1 x_1, F' ((x.1.1, x.2.1), x.1.2, x.2.2).2.2 x_1) ∈ w
⊢ ∀ (a : α) (b : α'), a ∈ s → b ∈ s' → ((F x.1.1 a, F' x.1.2 b), F x.2.1 a, F' x.2.2 b) ∈ u

Tactic:
a

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst✝ : UniformSpace β'
F' : ι' → α' → β'
p' : Filter ι'
s' : Set α'
h : UniformCauchySeqOn F p s
h' : UniformCauchySeqOn F' p' s'
u : Set ((β × β') × β × β')
v : Set (β × β)
hv : v ∈ 𝓤 β
w : Set (β' × β')
hw : w ∈ 𝓤 β'
hvw : (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) '' v ×ˢ w ⊆ u
x : (ι × ι') × ι × ι'
hx :
  (∀ x_1 ∈ s, (F ((x.1.1, x.2.1), x.1.2, x.2.2).1.1 x_1, F ((x.1.1, x.2.1), x.1.2, x.2.2).1.2 x_1) ∈ v) ∧
    ∀ x_1 ∈ s', (F' ((x.1.1, x.2.1), x.1.2, x.2.2).2.1 x_1, F' ((x.1.1, x.2.1), x.1.2, x.2.2).2.2 x_1) ∈ w
a : α
⊢ ∀ (b : α'), a ∈ s → b ∈ s' → ((F x.1.1 a, F' x.1.2 b), F x.2.1 a, F' x.2.2 b) ∈ u
Module: Mathlib.Topology.UniformSpace.Compact

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : SetRel α β
hs : IsClosed s
t : Set β
ht : IsCompact t
⊢ IsClosed (s.preimage t)

Tactic:
by
  rw [← isOpen_compl_iff, isOpen_iff_eventually] at hs ⊢
  simp_rw [Set.mem_compl_iff, SetRel.mem_preimage, not_exists, not_and]
  exact fun y hy => ht.eventually_forall_of_forall_eventually fun x hx => hs _ <| hy _ hx

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

Goal state before:
pp: case refine_1
α : 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 : ℕ
hn : B n ⊆ V
y : α
hy : y ∈ t n
hyx : x ∈ ball y (B n)
⊢ o n ⟨y, hy⟩ ⋯ ∈ ball x U

Tactic:
apply ball_mono ((SetRel.comp_subset_comp hn hn).trans hVU)
    exact mem_ball_comp (mem_ball_symmetry.2 hyx) (hox n ⟨y, hy⟩ ⟨x, hyx, hx⟩)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
x : α
⊢ UniformContinuous (Function.eval x ∘ ⇑toFun)

Tactic:
change _ ≤ _

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
x : α
⊢ map (fun x_1 ↦ ((Function.eval x ∘ ⇑toFun) x_1.1, (Function.eval x ∘ ⇑toFun) x_1.2)) (𝓤 (α →ᵤ β)) ≤ 𝓤 β
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 → α
S : Set X
⊢ EquicontinuousOn F S ↔ ContinuousOn (⇑ofFun ∘ swap F) S

Tactic:
by
  simp_rw [EquicontinuousOn, ContinuousOn, equicontinuousWithinAt_iff_continuousWithinAt]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : s ∈ 𝔖
⊢ UniformContinuous (⇑UniformFun.ofFun ∘ s.domRestrict ∘ ⇑(toFun 𝔖))

Tactic:
change _ ≤ _

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : s ∈ 𝔖
⊢ map
      (fun x ↦
        ((⇑UniformFun.ofFun ∘ s.domRestrict ∘ ⇑(toFun 𝔖)) x.1, (⇑UniformFun.ofFun ∘ s.domRestrict ∘ ⇑(toFun 𝔖)) x.2))
      (𝓤 (α →ᵤ[𝔖] β)) ≤
    𝓤 (↑s →ᵤ β)
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
ι : Sort u_5
p : ι → Prop
V : ι → Set (β × β)
h : (𝓤 β).HasBasis p V
⊢ ⨅ i ∈ 𝔖,
      ⨅ i_1,
        ⨅ (_ : p i_1),
          𝓟
            (Prod.map (⇑UniformFun.ofFun ∘ i.domRestrict ∘ ⇑(toFun 𝔖))
                (⇑UniformFun.ofFun ∘ i.domRestrict ∘ ⇑(toFun 𝔖)) ⁻¹'
              {uv | ∀ (x : ↑i), (UniformFun.toFun uv.1 x, UniformFun.toFun uv.2 x) ∈ V i_1}) =
    ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), 𝓟 (UniformOnFun.gen 𝔖 s (V i))

Tactic:
Subtype.forall,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
ι : Sort u_5
p : ι → Prop
V : ι → Set (β × β)
h : (𝓤 β).HasBasis p V
⊢ ⨅ i ∈ 𝔖,
      ⨅ i_1,
        ⨅ (_ : p i_1),
          𝓟
            (Prod.map (⇑UniformFun.ofFun ∘ i.domRestrict ∘ ⇑(toFun 𝔖))
                (⇑UniformFun.ofFun ∘ i.domRestrict ∘ ⇑(toFun 𝔖)) ⁻¹'
              {uv | ∀ (a : α) (b : a ∈ i), (UniformFun.toFun uv.1 ⟨a, b⟩, UniformFun.toFun uv.2 ⟨a, b⟩) ∈ V i_1}) =
    ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), 𝓟 (UniformOnFun.gen 𝔖 s (V i))
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
γ : Type u_3
ι : Type u_4
𝔖 : Set (Set α)
u : ι → UniformSpace γ
⊢ uniformSpace α γ 𝔖 = ⨅ i, uniformSpace α γ 𝔖

Tactic:
UniformOnFun.uniformSpace,

Goal state after:
α : Type u_1
γ : Type u_3
ι : Type u_4
𝔖 : Set (Set α)
u : ι → UniformSpace γ
⊢ ⨅ s ∈ 𝔖, UniformSpace.comap (⇑UniformFun.ofFun ∘ s.domRestrict ∘ ⇑(toFun 𝔖)) (UniformFun.uniformSpace (↑s) γ) =
    ⨅ i, ⨅ s ∈ 𝔖, UniformSpace.comap (⇑UniformFun.ofFun ∘ s.domRestrict ∘ ⇑(toFun 𝔖)) (UniformFun.uniformSpace (↑s) γ)
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : UniformSpace β
𝔖 : Set (Set α)
f : γ → β
⊢ uniformSpace α γ 𝔖 = UniformSpace.comap (fun x ↦ f ∘ x) (uniformSpace α β 𝔖)

Tactic:
UniformOnFun.uniformSpace,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : UniformSpace β
𝔖 : Set (Set α)
f : γ → β
⊢ ⨅ s ∈ 𝔖, UniformSpace.comap (⇑UniformFun.ofFun ∘ s.domRestrict ∘ ⇑(toFun 𝔖)) (UniformFun.uniformSpace (↑s) γ) =
    UniformSpace.comap (fun x ↦ f ∘ x)
      (⨅ s ∈ 𝔖, UniformSpace.comap (⇑UniformFun.ofFun ∘ s.domRestrict ∘ ⇑(toFun 𝔖)) (UniformFun.uniformSpace (↑s) β))
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: G₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a : G₀
ha : 0 < a
x : G₀
⊢ x ∈ (Ioo 0 a)⁻¹ ↔ x ∈ Ioi a⁻¹

Tactic:
exact ⟨fun h ↦ inv_lt_of_inv_lt₀ (inv_pos.1 h.1) h.2,
         fun h ↦ ⟨inv_pos.2 <| (inv_pos.2 ha).trans h, inv_lt_of_inv_lt₀ ha h⟩⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
φ : (i : ι) → δ i → α
𝔗 : (i : ι) → Set (Set (δ i))
h_image : ∀ (i : ι), MapsTo (fun x ↦ φ i '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun x ↦ φ i ⁻¹' x) 𝔖 (𝔗 i)
h_cover : ∀ S ∈ 𝔖, ∃ I, I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i)
ψ : (S : Set α) → (i : ι) → ↑(φ i ⁻¹' S) → ↑S := fun S i ↦ S.restrictPreimage (φ i)
S : Set α
hS : S ∈ 𝔖
⊢ UniformFun.uniformSpace (↑S) β =
    ⨅ i, UniformSpace.comap (fun x ↦ x ∘ ψ S i) (UniformFun.uniformSpace (↑(φ i ⁻¹' S)) β)

Tactic:
rcases h_cover S hS with ⟨I, I_finite, I_cover⟩

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
φ : (i : ι) → δ i → α
𝔗 : (i : ι) → Set (Set (δ i))
h_image : ∀ (i : ι), MapsTo (fun x ↦ φ i '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun x ↦ φ i ⁻¹' x) 𝔖 (𝔗 i)
h_cover : ∀ S ∈ 𝔖, ∃ I, I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i)
ψ : (S : Set α) → (i : ι) → ↑(φ i ⁻¹' S) → ↑S := fun S i ↦ S.restrictPreimage (φ i)
S : Set α
hS : S ∈ 𝔖
I : Set ι
I_finite : I.Finite
I_cover : S ⊆ ⋃ i ∈ I, range (φ i)
⊢ UniformFun.uniformSpace (↑S) β =
    ⨅ i, UniformSpace.comap (fun x ↦ x ∘ ψ S i) (UniformFun.uniformSpace (↑(φ i ⁻¹' S)) β)
Module: Mathlib.Topology.Algebra.ConstMulAction

Goal state before:
pp: α : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : ContinuousConstSMul G α
c : G
s : Set α
hs : closure[inst✝³] s = univ
⊢ closure[inst✝³] (c • s) = univ

Tactic:
rw [closure_smul, hs, smul_set_univ]

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

Goal state before:
pp: case mk.mk
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
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
i✝ : Quotient (MulAction.orbitRel Γ T)
x₀ : T
j✝ : Quotient (MulAction.orbitRel Γ T)
y₀ : T
hxy : f x₀ ≠ f y₀
hγx₀y₀ : ∀ (γ : Γ), γ • x₀ ≠ y₀
K₀ : Set T
hK₀ : IsCompact K₀
K₀_in : K₀ ∈ 𝓝 x₀
L₀ : Set T
hL₀ : IsCompact L₀
L₀_in : L₀ ∈ 𝓝 y₀
bad_Γ_set : Set Γ := {γ | ((fun x ↦ γ • x) '' K₀ ∩ L₀).Nonempty}
bad_Γ_finite : bad_Γ_set.Finite
u v : Γ → Set T
hu : ∀ (γ : Γ), u γ ∈ 𝓝 (γ • x₀)
hv : ∀ (γ : Γ), v γ ∈ 𝓝 y₀
u_v_disjoint : ∀ (γ : Γ), Disjoint (u γ) (v γ)
U₀₀ : Set T := ⋂ γ ∈ bad_Γ_set, (fun x ↦ γ • x) ⁻¹' u γ
U₀ : Set T := U₀₀ ∩ K₀
V₀₀ : Set T := ⋂ γ ∈ bad_Γ_set, v γ
V₀ : Set T := V₀₀ ∩ L₀
U_nhds : f '' U₀ ∈ 𝓝 (f x₀)
V_nhds : f '' V₀ ∈ 𝓝 (f y₀)
⊢ ∀ x ∈ U₀, ∀ (g : Γ), g • x ∉ V₀

Tactic:
rintro x ⟨x_in_U₀₀, x_in_K₀⟩ γ

Goal state after:
case mk.mk
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
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
i✝ : Quotient (MulAction.orbitRel Γ T)
x₀ : T
j✝ : Quotient (MulAction.orbitRel Γ T)
y₀ : T
hxy : f x₀ ≠ f y₀
hγx₀y₀ : ∀ (γ : Γ), γ • x₀ ≠ y₀
K₀ : Set T
hK₀ : IsCompact K₀
K₀_in : K₀ ∈ 𝓝 x₀
L₀ : Set T
hL₀ : IsCompact L₀
L₀_in : L₀ ∈ 𝓝 y₀
bad_Γ_set : Set Γ := {γ | ((fun x ↦ γ • x) '' K₀ ∩ L₀).Nonempty}
bad_Γ_finite : bad_Γ_set.Finite
u v : Γ → Set T
hu : ∀ (γ : Γ), u γ ∈ 𝓝 (γ • x₀)
hv : ∀ (γ : Γ), v γ ∈ 𝓝 y₀
u_v_disjoint : ∀ (γ : Γ), Disjoint (u γ) (v γ)
U₀₀ : Set T := ⋂ γ ∈ bad_Γ_set, (fun x ↦ γ • x) ⁻¹' u γ
U₀ : Set T := U₀₀ ∩ K₀
V₀₀ : Set T := ⋂ γ ∈ bad_Γ_set, v γ
V₀ : Set T := V₀₀ ∩ L₀
U_nhds : f '' U₀ ∈ 𝓝 (f x₀)
V_nhds : f '' V₀ ∈ 𝓝 (f y₀)
x : T
x_in_U₀₀ : x ∈ U₀₀
x_in_K₀ : x ∈ K₀
γ : Γ
⊢ γ • x ∉ V₀
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: case mpr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space Y
y : Y
⊢ CompactSpace X →
    (Continuous[inst✝², inst✝¹] fun x ↦ y) ∧ (IsClosedMap fun x ↦ y) ∧ ∀ (y_1 : Y), IsCompact ((fun x ↦ y) ⁻¹' {y_1})

Tactic:
intro H
    refine ⟨continuous_const, isClosedMap_const, fun y' ↦ ?_⟩
    simp [preimage_const, mem_singleton_iff, apply_ite, isCompact_univ]

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

Goal state before:
pp: G : Type w
ι' : Sort u_1
inst✝ : Inv G
ts' : ι' → TopologicalSpace G
h' : ∀ (i : ι'), ContinuousInv G
⊢ ContinuousInv G

Tactic:
by
  rw [← sInf_range]
  exact continuousInv_sInf (Set.forall_mem_range.mpr h')

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

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : TopologicalSpace G
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hinv : Tendsto (fun x ↦ x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun x ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : G), 𝓝 x₀ = map (fun x ↦ x * x₀) (𝓝 1)
x₀ : G
⊢ map (fun x ↦ x₀ * x * x₀⁻¹) (𝓝 1) = 𝓝 1

Tactic:
rw [show (fun x => x₀ * x * x₀⁻¹) = (fun x => x * x₀⁻¹) ∘ fun x => x₀ * x from rfl, ←
              map_map, ← hleft, hright, map_map]

Goal state after:
G : Type u
inst✝¹ : Group G
inst✝ : TopologicalSpace G
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hinv : Tendsto (fun x ↦ x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun x ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : G), 𝓝 x₀ = map (fun x ↦ x * x₀) (𝓝 1)
x₀ : G
⊢ map ((fun x ↦ x * x₀⁻¹) ∘ fun x ↦ x * x₀) (𝓝 1) = 𝓝 1
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : UniformSpace α
inst✝⁶ : Group α
inst✝⁵ : IsUniformGroup α
hom : Type u_3
inst✝⁴ : UniformSpace β
inst✝³ : Group β
inst✝² : IsUniformGroup β
inst✝¹ : FunLike hom α β
inst✝ : MonoidHomClass hom α β
f : hom
h : Continuous[inst✝⁷.toTopologicalSpace, inst✝⁴.toTopologicalSpace] ⇑f
this : Tendsto (⇑f) (𝓝 1) (𝓝 (f 1))
⊢ Tendsto (⇑f) (𝓝 1) (𝓝 1)

Tactic:
rwa [map_one] at this

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

Goal state before:
pp: G : Type u_3
inst✝³ : Group G
inst✝² : UniformSpace G
inst✝¹ : IsRightUniformGroup G
inst✝ : WeaklyLocallyCompactSpace G
f : Filter G
hf : Cauchy f
this : f.NeBot
K : Set G
K_compact : IsCompact K
K_mem : K ∈ 𝓝 1
x : G
hx : ∀ᶠ (y : G) in f, y ∈ MulOpposite.op x • K
⊢ ∃ x, f ≤ 𝓝 x

Tactic:
have Kx_complete : IsComplete (K <• x) := K_compact.smul _ |>.isComplete

Goal state after:
G : Type u_3
inst✝³ : Group G
inst✝² : UniformSpace G
inst✝¹ : IsRightUniformGroup G
inst✝ : WeaklyLocallyCompactSpace G
f : Filter G
hf : Cauchy f
this : f.NeBot
K : Set G
K_compact : IsCompact K
K_mem : K ∈ 𝓝 1
x : G
hx : ∀ᶠ (y : G) in f, y ∈ MulOpposite.op x • K
Kx_complete : IsComplete (MulOpposite.op x • K)
⊢ ∃ x, f ≤ 𝓝 x
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: case refine_3.inl
ι : 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) i = x i

Tactic:
exact Function.update_self ..

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) = ∅
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
H : a < b
⊢ y a ≤ b

Tactic:
by_contra!

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
H : a < b
this : b < y a
⊢ False
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 : α ≃ β
s : Set α
x : α
hx : x ∈ s
⊢ e.symm (e x) ∈ s

Tactic:
e.symm_apply_apply

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : PartialEquiv α β
e' : PartialEquiv β γ
e : α ≃ β
s : Set α
x : α
hx : x ∈ s
⊢ x ∈ s
Module: Mathlib.Topology.OpenPartialHomeomorph.Defs

Goal state before:
pp: X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace X'
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Y'
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
e✝ : OpenPartialHomeomorph X Y
e : X ≃ₜ Y
s : Set X
hs : IsOpen[inst✝⁵] s
t : Set Y
h : ⇑e '' s = t
⊢ IsOpen[inst✝³] (e.toPartialHomeomorphOfImageEq s t h).target

Tactic:
simpa [← h]

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

Goal state before:
pp: case refine_2
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst✝² : Preorder α
inst✝¹ : OrderTopology α
inst✝ : Countable α
⊢ ts = generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a}

Tactic:
· exact OrderTopology.topology_eq_generate_intervals

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case h
𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
y : 𝕜
hx✝ : ↑y ∈ {x | n • x = 0}
hx : n • y ∈ zmultiples p
m' : ℤ
this : NeZero n
m : ℤ × Fin n := (Int.divModEquiv n) m'
hm : (fun x ↦ x • p) (m.1 * ↑n + ↑↑m.2) = n • y
⊢ True ∧ n • y = ↑m.2 • p + n • m.1 • p

Tactic:
← hm,

Goal state after:
case h
𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
y : 𝕜
hx✝ : ↑y ∈ {x | n • x = 0}
hx : n • y ∈ zmultiples p
m' : ℤ
this : NeZero n
m : ℤ × Fin n := (Int.divModEquiv n) m'
hm : (fun x ↦ x • p) (m.1 * ↑n + ↑↑m.2) = n • y
⊢ True ∧ (fun x ↦ x • p) (m.1 * ↑n + ↑↑m.2) = ↑m.2 • p + n • m.1 • p
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SeparableSpace α
s : Set α
s_count : s.Countable
hs : Dense s
x✝ : BddAbove s
x : α
hx : x ∈ upperBounds s
h : ∀ (x : α), ∃ x_1, x < x_1
y : α
hy : y ∈ s
hxy : y ∈ Ioi x
⊢ False

Tactic:
exact (hx hy).not_gt hxy

Goal state after:
Module: Mathlib.Algebra.Category.Grp.LeftExactFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
F : C ⥤ AddCommGrpCat
inst✝ : PreservesFiniteLimits F
X : C
⊢ commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X)) ≅
    (F ⋙ forget AddCommGrpCat).mapCommGrp.obj (Preadditive.commGrpEquivalence.functor.obj X)

Tactic:
letI : (F ⋙ forget AddCommGrpCat).Braided := .ofChosenFiniteProducts _
  letI : F.Monoidal := .ofChosenFiniteProducts _
  refine CommGrp.mkIso Multiplicative.toAdd.toIso (by
    rw [Functor.obj.η_def X (F := F ⋙ forget AddCommGrpCat)]
    cat_disch) ?_
  dsimp [-Functor.comp_map, -ConcreteCategory.forget_map_eq_ofHom]
  have : F.Additive := Functor.additive_of_preserves_binary_products _
  simp only [Category.id_comp]
  rw [Functor.obj.μ_def X (F := F ⋙ forget AddCommGrpCat), Preadditive.mul_def X,
    Functor.comp_map, F.map_add,
    Functor.Monoidal.μ_comp F (forget AddCommGrpCat) X X,
    Category.assoc, ← Functor.map_comp, Preadditive.comp_add, Functor.Monoidal.μ_fst,
    Functor.Monoidal.μ_snd]
  ext
  -- `simp [types_tensorObj_def]` says
  simp only [types_tensorObj_def, TypeCat.Fun.toFun_apply, CategoryTheory.comp_apply,
    Equiv.toIso_hom_hom_apply, Functor.comp_obj, hom_add, tensor_apply, TypeCat.hom_ofHom,
    TypeCat.Fun.coe_mk, AddMonoidHom.add_apply]
  rw [dsimp% [types_tensorObj_def, types_tensorUnit_def] μ_forget_apply]
  rfl

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case left
𝕜 : Type u_1
B : Type u_2
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
⊢ ContinuousWithinAt (fun x ↦ Quot.mk (EndpointIdent p a) ⟨toIocMod ⋯ a x, ⋯⟩) (Iic x) x

Tactic:
apply continuous_quot_mk.continuousAt.comp_continuousWithinAt

Goal state after:
case left
𝕜 : Type u_1
B : Type u_2
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
⊢ ContinuousWithinAt (fun x ↦ ⟨toIocMod ⋯ a x, ⋯⟩) (Iic x) x
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case right
𝕜 : Type u_1
B : Type u_2
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
⊢ ContinuousWithinAt (fun x ↦ Quot.mk (EndpointIdent p a) ⟨toIcoMod ⋯ a x, ⋯⟩) (Ici x) x

Tactic:
apply continuous_quot_mk.continuousAt.comp_continuousWithinAt

Goal state after:
case right
𝕜 : Type u_1
B : Type u_2
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
⊢ ContinuousWithinAt (fun x ↦ ⟨toIcoMod ⋯ a x, ⋯⟩) (Ici x) x
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
a✝ : Epi f
A : C
⊢ ∀ (y : A ⟶ Y), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ f

Tactic:
a

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
a✝ : Epi f
A : C
a : A ⟶ Y
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ a = x ≫ f