mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
s : Set ι
hs : s.Countable
t : (i : ι) → i ∈ s → Set X
ht : ∀ (i : ι) (hi : i ∈ s), IsGδ (t i hi)
⊢ IsGδ (⋂ i, ⋂ (h : i ∈ s), t i h)

Tactic:
rw [biInter_eq_iInter]
  have := hs.to_subtype
  exact .iInter fun x => ht x x.2

Goal state after:
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
H1 : (∀ (u_1 : Finset { s // IsClopen s ∧ x ∈ s }), ((u ∪ v)ᶜ ∩ ⋂ i ∈ u_1, ↑i).Nonempty) → ¬Disjoint (u ∪ v)ᶜ (⋂ i, ↑i)
⊢ ∃ s, IsClopen s ∧ x ∈ s ∧ s ⊆ u ∪ v

Tactic:
imp_not_comm,

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
H1 : Disjoint (u ∪ v)ᶜ (⋂ i, ↑i) → ¬∀ (u_1 : Finset { s // IsClopen s ∧ x ∈ s }), ((u ∪ v)ᶜ ∩ ⋂ i ∈ u_1, ↑i).Nonempty
⊢ ∃ s, IsClopen s ∧ x ∈ s ∧ s ⊆ u ∪ v
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
U : ι → Set α
hclopen : ∀ (i : ι), IsClopen (U i)
hdisj : Pairwise (Disjoint on U)
hunion : ⋃ i, U i = univ
i : ι
x : α
hx : x ∈ U i
⊢ (equivOfIsClopen hclopen hdisj hunion) (mk x) = ⟨i, mk ⟨x, hx⟩⟩

Tactic:
by
  apply (equivOfIsClopen hclopen hdisj hunion).symm.injective
  simp

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

Goal state before:
pp: X : Type u_1
u : UniformSpace X
inst✝³ : DiscreteUniformity X
Y : Type u_2
inst✝² : Finite Y
inst✝¹ : UniformSpace Y
inst✝ : DiscreteTopology Y
h : SetRel.id = ⋂ y, {p | p.2 = y → p.1 ∈ {y}}
⊢ ∀ (i : Y), i ∈ {i}

Tactic:
Set.mem_singleton_iff,

Goal state after:
X : Type u_1
u : UniformSpace X
inst✝³ : DiscreteUniformity X
Y : Type u_2
inst✝² : Finite Y
inst✝¹ : UniformSpace Y
inst✝ : DiscreteTopology Y
h : SetRel.id = ⋂ y, {p | p.2 = y → p.1 ∈ {y}}
⊢ ∀ (i : Y), True
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'
⊢ UniformCauchySeqOn (fun i ↦ Prod.map (F i.1) (F' i.2)) (p ×ˢ p') (s ×ˢ s')

Tactic:
intro u hu
  rw [uniformity_prod_eq_prod, mem_map, mem_prod_iff] at hu
  obtain ⟨v, hv, w, hw, hvw⟩ := hu
  simp_rw [mem_prod, and_imp, Prod.forall, Prod.map_apply]
  rw [← Set.image_subset_iff] at hvw
  apply (tendsto_swap4_prod.eventually ((h v hv).prod_mk (h' w hw))).mono
  intro x hx a b ha hb
  exact hvw ⟨_, mk_mem_prod (hx.1 a ha) (hx.2 b hb), rfl⟩

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 α
x : α
p : Filter ι
hp : p.NeBot
hf : UniformCauchySeqOn F p s
hx : x ∈ s
⊢ Cauchy (map (fun i ↦ F i x) p)

Tactic:
simp only [cauchy_map_iff, hp, true_and]
  intro u hu
  rw [mem_map]
  filter_upwards [hf u hu] with p hp using hp x hx

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
hf : IsUniformInducing f
⊢ TotallyBounded (f '' s) ↔ TotallyBounded s

Tactic:
simp_rw [← totallyBounded_principal_iff, ← map_principal, totallyBounded_map_iff hf]

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
U_le : ∀ s ∈ 𝓤 α, ∃ n, U n ⊆ s
a : α
ha : Tendsto (seq hf U_mem) atTop (𝓝 a)
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ y, (a, y) ∈ s ∧ y ∈ t

Tactic:
rcases U_le s hs with ⟨m, hm⟩

Goal state after:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
U_le : ∀ s ∈ 𝓤 α, ∃ n, U n ⊆ s
a : α
ha : Tendsto (seq hf U_mem) atTop (𝓝 a)
s : Set (α × α)
hs : s ∈ 𝓤 α
m : ℕ
hm : U m ⊆ s
⊢ ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ y, (a, y) ∈ s ∧ y ∈ t
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst✝¹] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i ↦ mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := {i ∈ hnf.toFinset | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset | x ∉ U j}
z : X
hz : z ∈ n ∩ ((⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i)
⊢ z ∈ n

Tactic:
exact mem_of_mem_inter_left hz

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)

Goal state after:
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 (B n ○ B n)
Module: Mathlib.Topology.UniformSpace.Pi

Goal state before:
pp: ι : Type u_4
X : Type u_5
u : ι → UniformSpace X
hu : ∀ (i : ι), CompleteSpace X
a✝ : Nontrivial X
t : TopologicalSpace X
ht : T2Space X
hut : ∀ (i : ι), (u i).toTopologicalSpace ≤ t
⊢ ⨅ i, Filter.comap (fun x ↦ x) (𝓤 X) = ⨅ i, 𝓤 X

Tactic:
comap_id'

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
X' : Type u_4
α : Type u_6
uα : UniformSpace α
t : κ → TopologicalSpace X'
F : ι → X' → α
S : Set X'
x₀ : X'
k : κ
hk : Tendsto (⇑ofFun ∘ swap F) (𝓝 x₀ ⊓ 𝓟 S) (𝓝 ((⇑ofFun ∘ swap F) x₀))
⊢ Tendsto (⇑ofFun ∘ swap F) (𝓝 x₀ ⊓ 𝓟 S) (𝓝 ((⇑ofFun ∘ swap F) x₀))

Tactic:
rw [nhds_iInf]

Goal state after:
ι : Type u_1
κ : Type u_2
X' : Type u_4
α : Type u_6
uα : UniformSpace α
t : κ → TopologicalSpace X'
F : ι → X' → α
S : Set X'
x₀ : X'
k : κ
hk : Tendsto (⇑ofFun ∘ swap F) (𝓝 x₀ ⊓ 𝓟 S) (𝓝 ((⇑ofFun ∘ swap F) x₀))
⊢ Tendsto (⇑ofFun ∘ swap F) ((⨅ i, 𝓝 x₀) ⊓ 𝓟 S) (𝓝 ((⇑ofFun ∘ swap F) x₀))
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : InvolutiveInv α
f✝ g : Filter α
s : Set α
f : Filter α
⊢ map (Inv.inv ∘ Inv.inv) f = f

Tactic:
inv_involutive.comp_self,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : InvolutiveInv α
f✝ g : Filter α
s : Set α
f : Filter α
⊢ map id f = f
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: case inr
G₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
ha✝ : 0 ≤ a
hbc : b ≤ c
ha : 0 < a
⊢ (fun x ↦ a * x) '' Icc b c = Icc (a * b) (a * c)

Tactic:
exact image_mul_left_Icc' ha b c

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hg : UniformContinuous (s.domRestrict g)
F' : ι → α → ↑s
hF' : (fun i i_1 ↦ ↑(F' i i_1)) = F
f' : α → ↑s
hf' : (fun i ↦ ↑(f' i)) = f
comp_tendstoUniformly :
  (∀ (i : ι) (x : α), ↑(F' i x) ∈ s) →
    (∀ (x : α), ↑(f' x) ∈ s) →
      UniformContinuousOn g s →
        TendstoUniformly (fun i i_1 ↦ ↑(F' i i_1)) (fun i ↦ ↑(f' i)) p →
          TendstoUniformly (fun i x ↦ g ↑(F' i x)) (fun x ↦ g ↑(f' x)) p
h : Tendsto (fun q ↦ (↑(f' q.2), ↑(F' q.1 q.2))) (p ×ˢ ⊤) (𝓤 β)
⊢ TendstoUniformly (fun i x ↦ g ↑(F' i x)) (fun x ↦ g ↑(f' x)) p

Tactic:
have : Tendsto (fun q ↦ (f' q.2, F' q.1 q.2)) (p ×ˢ ⊤) (𝓤 s) :=
    h.of_tendsto_comp isUniformEmbedding_subtype_val.comap_uniformity.le

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hg : UniformContinuous (s.domRestrict g)
F' : ι → α → ↑s
hF' : (fun i i_1 ↦ ↑(F' i i_1)) = F
f' : α → ↑s
hf' : (fun i ↦ ↑(f' i)) = f
comp_tendstoUniformly :
  (∀ (i : ι) (x : α), ↑(F' i x) ∈ s) →
    (∀ (x : α), ↑(f' x) ∈ s) →
      UniformContinuousOn g s →
        TendstoUniformly (fun i i_1 ↦ ↑(F' i i_1)) (fun i ↦ ↑(f' i)) p →
          TendstoUniformly (fun i x ↦ g ↑(F' i x)) (fun x ↦ g ↑(f' x)) p
h : Tendsto (fun q ↦ (↑(f' q.2), ↑(F' q.1 q.2))) (p ×ˢ ⊤) (𝓤 β)
this : Tendsto (fun q ↦ (f' q.2, F' q.1 q.2)) (p ×ˢ ⊤) (𝓤 ↑s)
⊢ TendstoUniformly (fun i x ↦ g ↑(F' i x)) (fun x ↦ g ↑(f' x)) p
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
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₀
γ : Γ
x✝ : γ ∈ bad_Γ_set
⊢ (fun x ↦ γ • x) ⁻¹' u γ ∈ 𝓝 x₀

Tactic:
exact (continuous_const_smul _).continuousAt (hu γ)

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

Goal state before:
pp: case pos
M : Type u_3
inst✝⁴ : GroupWithZero M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousMul M
inst✝¹ : CompactSpace M
inst✝ : T1Space M
U : Set M
hU : IsOpen[inst✝³] U
h0U : 0 ∈ U
h1U : 1 ∉ U
W : Set M
hW : W ∈ 𝓝 0
hW' : univ * W ⊆ U
H : ∃ x, x ≠ 0 ∧ x ∈ W
⊢ IsOpen[inst✝³] {0}

Tactic:
obtain ⟨x, hx, hxW⟩ := H
    cases h1U (hW' (by simpa [hx] using Set.mul_mem_mul (Set.mem_univ x⁻¹) hxW))

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

Goal state before:
pp: case right
ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous[inst✝¹ i, inst✝ i] (f i) ∧
      ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄, Tendsto (f i) (↑𝒰) (𝓝 y) → ∃ x, f i x = y ∧ ↑𝒰 ≤ 𝓝 x
⊢ ∀ ⦃𝒰 : Ultrafilter ((i : ι) → X i)⦄ ⦃y : (i : ι) → Y i⦄,
    Tendsto (fun x i ↦ f i (x i)) (↑𝒰) (𝓝 y) → ∃ x, (fun i ↦ f i (x i)) = y ∧ ↑𝒰 ≤ 𝓝 x

Tactic:
intro 𝒰 y hy
  -- That means that each `f i` tends to `y i` along `map (eval i) 𝒰`.
    have : ∀ i, Tendsto (f i) (Ultrafilter.map (eval i) 𝒰) (𝓝 (y i)) := by
      simpa [tendsto_pi_nhds] using! hy
  -- Thus, by properness of all the `f i`s, we can choose some `x : Π i, X i` such that, for all
  -- `i`, `f i (x i) = y i` and `map (eval i) 𝒰` tends to  `x i`.
    choose x hxy hx using fun i ↦ (h i).2 (this i)
  -- By the properties of the product topology, that means that `𝒰` tends to `x`,
  -- which completes the proof since `(Π i, f i) x = y`.
    refine ⟨x, funext hxy, ?_⟩
    rwa [nhds_pi, le_pi]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace M
inst✝⁶ : Monoid M
inst✝⁵ : ContinuousMul M
R : Type u_6
A : Type u_7
inst✝⁴ : Monoid A
inst✝³ : SMul R A
inst✝² : SMulCommClass R A A
inst✝¹ : TopologicalSpace A
inst✝ : SeparatelyContinuousMul A
q : R
⊢ Continuous[inst✝¹, inst✝¹] fun x ↦ q • x

Tactic:
simp +singlePass only [← mul_smul_one q (_ : A)]
    fun_prop

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

Goal state before:
pp: G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
N : Subgroup G
γ : G
⊢ Continuous[instTopologicalSpace N, instTopologicalSpace N] fun x ↦ γ • x

Tactic:
← isOpenQuotientMap_mk.continuous_comp_iff

Goal state after:
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
N : Subgroup G
γ : G
⊢ Continuous[inst✝², instTopologicalSpace N] ((fun x ↦ γ • x) ∘ mk)
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
M : Type u_1
hom : Type u_2
inst✝⁴ : MulOneClass M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousMul M
inst✝¹ : FunLike hom G M
inst✝ : MonoidHomClass hom G M
f : hom
hf : Tendsto (⇑f) (𝓝 1) (𝓝 1)
x : G
⊢ ContinuousAt (⇑f) x

Tactic:
by
    simpa only [ContinuousAt, ← map_mul_left_nhds_one x, tendsto_map'_iff, Function.comp_def,
      map_mul, mul_one] using hf.const_mul (f x)

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

Goal state before:
pp: β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
dr : β × β → β := fun xy ↦ xy.2 * xy.1⁻¹
dl : β × β → β := fun xy ↦ xy.1⁻¹ * xy.2
conj : β × β → β := fun gx ↦ gx.1 * gx.2 * gx.1⁻¹
φ : β × β ≃ β × β := (Equiv.refl β).prodShear fun b ↦ Equiv.symm (Equiv.mulLeft b)
conj_φ : conj ∘ ⇑φ = dr
snd_φ : snd ∘ ⇑φ = dl
⊢ comap dr (𝓝 1) = 𝓤 β

Tactic:
← uniformity_eq_comap_mul_inv_nhds_one

Goal state after:
β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
dr : β × β → β := fun xy ↦ xy.2 * xy.1⁻¹
dl : β × β → β := fun xy ↦ xy.1⁻¹ * xy.2
conj : β × β → β := fun gx ↦ gx.1 * gx.2 * gx.1⁻¹
φ : β × β ≃ β × β := (Equiv.refl β).prodShear fun b ↦ Equiv.symm (Equiv.mulLeft b)
conj_φ : conj ∘ ⇑φ = dr
snd_φ : snd ∘ ⇑φ = dl
⊢ 𝓤 β = 𝓤 β
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: A : Type u_1
inst✝⁶ : Group A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : ContinuousMul A
B : Type u_2
inst✝³ : Group B
inst✝² : TopologicalSpace B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap ⇑φ
U : Set A
hU : IsOpen[inst✝⁵] U
⊢ IsOpen[inst✝⁵] (⇑φ ⁻¹' ⇑φ '' U)

Tactic:
suffices ⇑φ ⁻¹' ⇑φ '' U = ⋃ k ∈ ker (φ : A →* B), (fun x ↦ x * k) ⁻¹' U by
        exact this ▸ isOpen_biUnion (fun k _ ↦ Continuous.isOpen_preimage (by fun_prop) _ hU)

Goal state after:
A : Type u_1
inst✝⁶ : Group A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : ContinuousMul A
B : Type u_2
inst✝³ : Group B
inst✝² : TopologicalSpace B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap ⇑φ
U : Set A
hU : IsOpen[inst✝⁵] U
⊢ ⇑φ ⁻¹' ⇑φ '' U = ⋃ k ∈ (↑φ).ker, (fun x ↦ x * k) ⁻¹' U
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
h : IsClosed[inst✝²] {1}
x : G
⊢ IsClosed[inst✝²] {x}

Tactic:
by simpa using isClosedMap_mul_right x _ h

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

Goal state before:
pp: G : Type w
H : Type x
inst✝⁴ : Group G
inst✝³ : Monoid H
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace H
inst✝ : ContinuousInv G
f : G →* Hˣ
hf : Continuous[inst✝², inst✝¹] ⇑((Units.coeHom H).comp f)
⊢ Continuous[inst✝², instTopologicalSpaceMulOpposite] fun x ↦ op ↑(f x⁻¹)

Tactic:
exact MulOpposite.continuous_op.comp (hf.comp continuous_inv)

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

Goal state before:
pp: G : Type u_4
inst✝² : Group G
inst✝¹ : UniformSpace G
inst✝ : IsUniformGroup G
𝓕 : Filter G
⊢ Cauchy 𝓕 ↔ 𝓕.NeBot ∧ Tendsto (fun p ↦ p.2 / p.1) (𝓕 ×ˢ 𝓕) (𝓝 1)

Tactic:
simp [Cauchy, uniformity_eq_comap_nhds_one, ← tendsto_iff_comap]

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, f ≤ 𝓝 x

Tactic:
obtain ⟨x, hx⟩ : ∃ x, ∀ᶠ y in f, y / x ∈ K := by
      rw [cauchy_iff_le, uniformity_eq_comap_nhds_one, ← tendsto_iff_comap] at hf
      exact hf.eventually_mem K_mem |>.curry.exists

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 / x ∈ K
⊢ ∃ x, f ≤ 𝓝 x
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
G : Type u_3
inst✝² : Group G
u : UniformSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : TopologicalSpace α
F : ι → α → G
f : α → G
p : Filter ι
hu : rightUniformSpace G = u
⊢ TendstoLocallyUniformly F f p ↔ ∀ u_1 ∈ 𝓝 1, ∀ (x : α), ∃ t ∈ 𝓝 x, ∀ᶠ (i : ι) in p, ∀ a ∈ t, F i a * (f a)⁻¹ ∈ u_1

Tactic:
exact hu ▸ ⟨fun h u hu => h _ ⟨u, hu, fun _ => id⟩, fun h _ ⟨u, hu, hv⟩ x =>
    Exists.imp (fun _ ⟨h, hp⟩ => ⟨h, mem_of_superset hp fun _ hi a ha => hv (hi a ha)⟩)
      (h u hu x)⟩

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ≤ y i₀
this : Ioc (x i₀) m = Iic m ∩ Ioc (x i₀) (y i₀)
⊢ (univ.pi fun i ↦ Ioc (x i) (update y i₀ m i)) = {z | z i₀ ≤ m} ∩ univ.pi fun i ↦ Ioc (x i) (y i)

Tactic:
univ_pi_update i₀ y m fun i z ↦ Ioc (x i) z,

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ≤ y i₀
this : Ioc (x i₀) m = Iic m ∩ Ioc (x i₀) (y i₀)
⊢ ({x_1 | x_1 i₀ ∈ Ioc (x i₀) m} ∩ {i₀}ᶜ.pi fun j ↦ Ioc (x j) (y j)) = {z | z i₀ ≤ m} ∩ univ.pi fun j ↦ Ioc (x j) (y j)
Module: Mathlib.Topology.Algebra.Order.Field

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f : 𝕜 → α
h : Tendsto (fun x ↦ f x⁻¹) atTop l
⊢ Tendsto f (𝓝[>] 0) l

Tactic:
convert! h.comp tendsto_inv_nhdsGT_zero

Goal state after:
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f : 𝕜 → α
h : Tendsto (fun x ↦ f x⁻¹) atTop l
⊢ f = (fun x ↦ f x⁻¹) ∘ fun x ↦ x⁻¹
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case ht
α : Type u
ts : TopologicalSpace α
inst✝ : Preorder α
c : Set α
h : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
f g : Set α
hfc : f ⊆ c
hgc : g ⊆ c
hf_fin : f.Finite
hg_fin : g.Finite
⊢ IsOpen[ts] (⋂ a ∈ g, Iio a)

Tactic:
apply hg_fin.isOpen_biInter (fun i hi ↦ ?_)

Goal state after:
α : Type u
ts : TopologicalSpace α
inst✝ : Preorder α
c : Set α
h : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
f g : Set α
hfc : f ⊆ c
hgc : g ⊆ c
hf_fin : f.Finite
hg_fin : g.Finite
i : α
hi : i ∈ g
⊢ IsOpen[ts] (Iio i)
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case inr
𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
hx : a + p ∈ Icc a (a + p)
⊢ (fun x ↦ Quot.mk (EndpointIdent p a) (Set.inclusion ⋯ ((equivIco p a) x)))
      ((fun x ↦ x.liftOn (fun x ↦ ↑↑x) ⋯) (Quot.mk (EndpointIdent p a) ⟨a + p, hx⟩)) =
    Quot.mk (EndpointIdent p a) ⟨a + p, hx⟩

Tactic:
rw [← Quot.sound EndpointIdent.mk]

Goal state after:
case inr
𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
hx : a + p ∈ Icc a (a + p)
⊢ (fun x ↦ Quot.mk (EndpointIdent p a) (Set.inclusion ⋯ ((equivIco p a) x)))
      ((fun x ↦ x.liftOn (fun x ↦ ↑↑x) ⋯) (Quot.mk (EndpointIdent p a) ⟨a, ⋯⟩)) =
    Quot.mk (EndpointIdent p a) ⟨a, ⋯⟩
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 2
hS : S.IsComplex
h : S.Exact
⊢ (S.sc' hS 0 1 2 exact₂_iff._proof_2 exact₂_iff._proof_4 isComplex₂_iff._proof_5).Exact

Tactic:
exact h.exact 0 (by lia)

Goal state after:
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case mp.left
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ ((mk₂ (S.map' 0 1 isComplex₂_iff._proof_2 ⋯) (S.map' 1 2 isComplex₂_iff._proof_4 ⋯)).sc' ⋯ 0 1 2 exact₂_iff._proof_2
      exact₂_iff._proof_4 isComplex₂_iff._proof_5).Exact

Tactic:
exact h.exact 0 (by lia)

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X Y Z : Type u
z : Z
x : X
y : Y
⊢ freeMk (((x, y), z).1.1, ((x, y), z).1.2, ((x, y), z).2) =
    (Hom.hom (μIso R X (Y ⊗ Z)).hom)
      ((Hom.hom ((free R).obj X ◁ (μIso R Y Z).hom))
        ((Hom.hom (α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom)
          (freeMk ((x, y), z).1.1 ⊗ₜ[R] freeMk ((x, y), z).1.2 ⊗ₜ[R] freeMk ((x, y), z).2)))

Tactic:
MonoidalCategory.associator_hom_apply,

Goal state after:
R : Type u
inst✝ : CommRing R
X Y Z : Type u
z : Z
x : X
y : Y
⊢ freeMk (((x, y), z).1.1, ((x, y), z).1.2, ((x, y), z).2) =
    (Hom.hom (μIso R X (Y ⊗ Z)).hom)
      ((Hom.hom ((free R).obj X ◁ (μIso R Y Z).hom))
        (freeMk ((x, y), z).1.1 ⊗ₜ[R] (freeMk ((x, y), z).1.2 ⊗ₜ[R] freeMk ((x, y), z).2)))
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: case h_zero
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y : Free R C
f g : X ⟶ Y
⊢ ∀ (a : X ⟶ Y), 0 • F.map a = 0

Tactic:
simp [add_smul]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: case h_add
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y : Free R C
f g : X ⟶ Y
⊢ ∀ (a : X ⟶ Y) (b₁ b₂ : R), (b₁ + b₂) • F.map a = b₁ • F.map a + b₂ • F.map a

Tactic:
simp [add_smul]

Goal state after: