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

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
β : Type u_3
inst✝ : TopologicalSpace β
f : α → β
hf : IsCoinducing f
hf' : ∀ (y : β), IsConnected (f ⁻¹' {y})
y : ConnectedComponents α
x : α
h : ⋯.connectedComponentsMap (ConnectedComponents.mk x) = ⋯.connectedComponentsMap y
⊢ ConnectedComponents.mk x = y

Tactic:
obtain ⟨y, rfl⟩ := ConnectedComponents.surjective_coe y

Goal state after:
α : Type u
inst✝¹ : TopologicalSpace α
β : Type u_3
inst✝ : TopologicalSpace β
f : α → β
hf : IsCoinducing f
hf' : ∀ (y : β), IsConnected (f ⁻¹' {y})
x y : α
h : ⋯.connectedComponentsMap (ConnectedComponents.mk x) = ⋯.connectedComponentsMap (ConnectedComponents.mk y)
⊢ ConnectedComponents.mk x = ConnectedComponents.mk y
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_1
α : 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✝¹ x✝ : (i : ι) × ConnectedComponents ↑(U i)
i j : ι
y : ConnectedComponents ↑(U j)
x : ↑(U i)
hxy :
  (fun x ↦
        match x with
        | ⟨i, x⟩ => Quotient.lift (mk ∘ Subtype.val) ⋯ x)
      ⟨i, mk x⟩ =
    (fun x ↦
        match x with
        | ⟨i, x⟩ => Quotient.lift (mk ∘ Subtype.val) ⋯ x)
      ⟨j, y⟩
⊢ ⟨i, mk x⟩ = ⟨j, y⟩

Tactic:
obtain ⟨y, rfl⟩ := ConnectedComponents.surjective_coe y

Goal state after:
case refine_1
α : 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✝¹ x✝ : (i : ι) × ConnectedComponents ↑(U i)
i j : ι
x : ↑(U i)
y : ↑(U j)
hxy :
  (fun x ↦
        match x with
        | ⟨i, x⟩ => Quotient.lift (mk ∘ Subtype.val) ⋯ x)
      ⟨i, mk x⟩ =
    (fun x ↦
        match x with
        | ⟨i, x⟩ => Quotient.lift (mk ∘ Subtype.val) ⋯ x)
      ⟨j, mk y⟩
⊢ ⟨i, mk x⟩ = ⟨j, mk y⟩
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : Infinite (ConnectedComponents α)
h✝ : Nonempty α
⊢ (∀ (i : Fin (0 + 1)), IsClopen (![univ] i)) ∧
    (∀ (i : Fin (0 + 1)), (![univ] i).Nonempty) ∧ Pairwise (Disjoint on ![univ]) ∧ ⋃ i, ![univ] i = univ

Tactic:
by simp [isClopen_univ, Set.iUnion_fin_add_one_eq_iUnion_succ]

Goal state after:
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Nonempty X
s : Set X
hs : s ∈ residual X
t : Set X
ht_sub : t ⊆ s
htGδ : IsGδ t
ht_dense : Dense t
⊢ ¬IsMeagre s

Tactic:
intro hs_meagre

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Nonempty X
s : Set X
hs : s ∈ residual X
t : Set X
ht_sub : t ⊆ s
htGδ : IsGδ t
ht_dense : Dense t
hs_meagre : IsMeagre s
⊢ False
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : Preorder β
u : β → α
h : CauchySeq u
⊢ Tendsto (Prod.map u u) atTop (𝓤 α)

Tactic:
simpa only [Tendsto, prod_map_map_eq', prod_atTop_atTop_eq] using h.right

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

Goal state before:
pp: α : Type ua
u₁ u₂ : UniformSpace α
h : u₁ ≤ u₂
a : α
⊢ 𝓝 a ≤ 𝓝 a

Tactic:
rw [@nhds_eq_uniformity α u₁ a, @nhds_eq_uniformity α u₂ a]

Goal state after:
α : Type ua
u₁ u₂ : UniformSpace α
h : u₁ ≤ u₂
a : α
⊢ (𝓤 α).lift' (ball a) ≤ (𝓤 α).lift' (ball a)
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
⊢ Filter.comap (fun p ↦ (p.1.1, p.2.1)) (𝓤 α) ⊓ Filter.comap (fun p ↦ (p.1.2, p.2.2)) (𝓤 β) =
    Filter.comap (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (Filter.comap Prod.fst (𝓤 α) ⊓ Filter.comap Prod.snd (𝓤 β))

Tactic:
Filter.comap_inf,

Goal state after:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
⊢ Filter.comap (fun p ↦ (p.1.1, p.2.1)) (𝓤 α) ⊓ Filter.comap (fun p ↦ (p.1.2, p.2.2)) (𝓤 β) =
    Filter.comap (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (Filter.comap Prod.fst (𝓤 α)) ⊓
      Filter.comap (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (Filter.comap Prod.snd (𝓤 β))
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
ι : Type u_1
I : Set ι
hI : I.Finite
f : ι → Filter α
this : Finite ↑I
⊢ (∀ (i : Subtype (Membership.mem I)), (f ↑i).TotallyBounded) ↔ ∀ i ∈ I, (f i).TotallyBounded

Tactic:
Subtype.forall

Goal state after:
α : Type u
uniformSpace : UniformSpace α
ι : Type u_1
I : Set ι
hI : I.Finite
f : ι → Filter α
this : Finite ↑I
⊢ (∀ (a : ι) (b : a ∈ I), (f ↑⟨a, b⟩).TotallyBounded) ↔ ∀ i ∈ I, (f i).TotallyBounded
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
ι : Type u_1
I : Set ι
hI : I.Finite
s : ι → Set α
this : Finite ↑I
⊢ (∀ (i : ↑I), TotallyBounded (s ↑i)) ↔ ∀ i ∈ I, TotallyBounded (s i)

Tactic:
Subtype.forall

Goal state after:
α : Type u
uniformSpace : UniformSpace α
ι : Type u_1
I : Set ι
hI : I.Finite
s : ι → Set α
this : Finite ↑I
⊢ (∀ (a : ι) (b : a ∈ I), TotallyBounded (s ↑⟨a, b⟩)) ↔ ∀ i ∈ I, TotallyBounded (s i)
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α × α)
e : α → β
b : β
he₁ : IsUniformInducing e
he₂ : IsDenseInducing e
hs✝ : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen[instTopologicalSpaceProd] U
hsymm : SetRel.IsSymm U
a : α
ha : e a ∈ UniformSpace.ball b U
⊢ ∃ a, closure[inst✝.toTopologicalSpace] (e '' {a' | (a, a') ∈ s}) ∈ 𝓝 b

Tactic:
refine ⟨a, mem_of_superset ?_ (closure_mono <| image_mono <| UniformSpace.ball_mono hs a)⟩

Goal state after:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α × α)
e : α → β
b : β
he₁ : IsUniformInducing e
he₂ : IsDenseInducing e
hs✝ : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen[instTopologicalSpaceProd] U
hsymm : SetRel.IsSymm U
a : α
ha : e a ∈ UniformSpace.ball b U
⊢ closure[inst✝.toTopologicalSpace] (e '' UniformSpace.ball a (Prod.map e e ⁻¹' U)) ∈ 𝓝 b
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α × α)
e : α → β
b : β
he₁ : IsUniformInducing e
he₂ : IsDenseInducing e
hs✝ : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen[instTopologicalSpaceProd] U
hsymm : SetRel.IsSymm U
a : α
ha : e a ∈ UniformSpace.ball b U
ho : IsOpen[inst✝.toTopologicalSpace] (UniformSpace.ball (e a) U)
y : β
hy : y ∈ UniformSpace.ball (e a) U
V : Set β
hV : V ∈ 𝓝 y
⊢ (V ∩ e '' UniformSpace.ball a (Prod.map e e ⁻¹' U)).Nonempty

Tactic:
rcases he₂.dense.mem_nhds (inter_mem hV (ho.mem_nhds hy)) with ⟨x, hxV, hxU⟩

Goal state after:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α × α)
e : α → β
b : β
he₁ : IsUniformInducing e
he₂ : IsDenseInducing e
hs✝ : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen[instTopologicalSpaceProd] U
hsymm : SetRel.IsSymm U
a : α
ha : e a ∈ UniformSpace.ball b U
ho : IsOpen[inst✝.toTopologicalSpace] (UniformSpace.ball (e a) U)
y : β
hy : y ∈ UniformSpace.ball (e a) U
V : Set β
hV : V ∈ 𝓝 y
x : α
hxV : e x ∈ V
hxU : e x ∈ UniformSpace.ball (e a) U
⊢ (V ∩ e '' UniformSpace.ball a (Prod.map e e ⁻¹' U)).Nonempty
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : DiscreteUniformity β
f : α → β
hf : IsUniformEmbedding f
⊢ comap (fun x ↦ (f x.1, f x.2)) (𝓤 β) = 𝓟 SetRel.id

Tactic:
DiscreteUniformity.eq_principal_setRelId,

Goal state after:
α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : DiscreteUniformity β
f : α → β
hf : IsUniformEmbedding f
⊢ comap (fun x ↦ (f x.1, f x.2)) (𝓟 SetRel.id) = 𝓟 SetRel.id
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
p : Filter ι
h : TendstoLocallyUniformlyOn F f p s
h' : s' ⊆ s
⊢ TendstoLocallyUniformlyOn F f p s'

Tactic:
intro u hu x hx
  rcases h u hu x (h' hx) with ⟨t, ht, H⟩
  exact ⟨t, nhdsWithin_mono x h' ht, H.mono fun n => id⟩

Goal state after:
Module: Mathlib.Algebra.Order.Group.MinMax

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ |max a b - max c d| ≤ max |a - c| |b - d|

Tactic:
by
  refine abs_sub_le_iff.2 ⟨?_, ?_⟩
  · exact (max_sub_max_le_max _ _ _ _).trans (max_le_max (le_abs_self _) (le_abs_self _))
  · rw [abs_sub_comm a c, abs_sub_comm b d]
    exact (max_sub_max_le_max _ _ _ _).trans (max_le_max (le_abs_self _) (le_abs_self _))

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 : α → β
s : Set α
p : Filter ι
hf : TendstoLocallyUniformlyOn F f p s
a : α
ha : a ∈ s
⊢ Tendsto (fun i ↦ F i a) p (𝓝 (f a))

Tactic:
refine ((tendstoLocallyUniformlyOn_iff_filter.mp hf) a ha).tendsto_at ?_
  simpa only [Filter.principal_singleton] using pure_le_nhdsWithin ha

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

Goal state before:
pp: case mp
α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c x : α
⊢ x ∈ a • Icc b c → x ∈ Icc (a * b) (a * c)

Tactic:
rintro ⟨y, ⟨hby, hyc⟩, rfl⟩
    dsimp
    constructor <;> gcongr

Goal state after:
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✝ : DivisionMonoid α
f g s t : Filter α
h : s * t = 1
⊢ s⁻¹ = t

Tactic:
obtain ⟨a, b, rfl, rfl, hab⟩ := Filter.mul_eq_one_iff.1 h

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
f g : Filter α
a b : α
hab : a * b = 1
h : pure a * pure b = 1
⊢ (pure a)⁻¹ = pure b
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c d : α
h : [[c, d]] ⊆ [[a, b]]
⊢ max c d - min c d ≤ max a b - min a b

Tactic:
uIcc_subset_uIcc_iff_le

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c d : α
h : min a b ≤ min c d ∧ max c d ≤ max a b
⊢ max c d - min c d ≤ max a b - min a b
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: case inl
G₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
hab : a ≤ b
hc : 0 ≤ 0
⊢ (fun x ↦ x * 0) '' Icc a b = Icc (a * 0) (b * 0)

Tactic:
simp [(nonempty_Icc.2 hab).image_const]

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

Goal state before:
pp: M : Type u_1
X : Type u_2
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace X
inst✝³ : Group M
inst✝² : IsTopologicalGroup M
inst✝¹ : MulAction M X
inst✝ : DiscreteTopology X
h : ∀ (x : X), IsOpen[inst✝⁵] ↑(MulAction.stabilizer M x)
⊢ ∀ (b : X), Continuous[inst✝⁵, inst✝⁴] fun x ↦ (x, b).1 • (x, b).2

Tactic:
intro y

Goal state after:
M : Type u_1
X : Type u_2
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace X
inst✝³ : Group M
inst✝² : IsTopologicalGroup M
inst✝¹ : MulAction M X
inst✝ : DiscreteTopology X
h : ∀ (x : X), IsOpen[inst✝⁵] ↑(MulAction.stabilizer M x)
y : X
⊢ Continuous[inst✝⁵, inst✝⁴] fun x ↦ (x, y).1 • (x, y).2
Module: Mathlib.Topology.ContinuousMap.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 : C(X, Y)
hf : IsQuotientMap ⇑f
⊢ Continuous[inst✝¹, instTopologicalSpaceQuotient] (Setoid.quotientKerEquivOfSurjective ⇑f ⋯).invFun

Tactic:
rw [hf.continuous_iff]

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 : C(X, Y)
hf : IsQuotientMap ⇑f
⊢ Continuous[inst✝², instTopologicalSpaceQuotient] ((Setoid.quotientKerEquivOfSurjective ⇑f ⋯).invFun ∘ ⇑f)
Module: Mathlib.Topology.ContinuousMap.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 : C(X, Y)
hf : IsQuotientMap ⇑f
⊢ Continuous[inst✝¹, instTopologicalSpaceQuotient] (Setoid.quotientKerEquivOfSurjective ⇑f ⋯).invFun

Tactic:
rw [hf.continuous_iff]
    convert! continuous_quotient_mk'
    ext
    simp only [Equiv.invFun_as_coe, Function.comp_apply,
      (Setoid.quotientKerEquivOfSurjective f hf.surjective).symm_apply_eq]
    rfl

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

Goal state before:
pp: M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Mul M
inst✝ : ContinuousMul M
a b : M
⊢ 𝓝 a * 𝓝 b ≤ 𝓝 (a * b)

Tactic:
rw [← map₂_mul, ← map_uncurry_prod, ← nhds_prod_eq]

Goal state after:
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Mul M
inst✝ : ContinuousMul M
a b : M
⊢ map (Function.uncurry fun x1 x2 ↦ x1 * x2) (𝓝 (a, b)) ≤ 𝓝 (a * b)
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
f : X → Y
x✝ : Continuous[inst✝¹, inst✝] f
H : ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
ℱ : Filter X
y : Y
⊢ ∀ (x : Ultrafilter X), ↑x ≤ comap f (𝓝 y) ⊓ ℱ → ∃ x, f x = y ∧ ∃ u, ↑u ≤ 𝓝 x ⊓ ℱ

Tactic:
𝒰

Goal state after:
case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
x✝ : Continuous[inst✝¹, inst✝] f
H : ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
ℱ : Filter X
y : Y
𝒰 : Ultrafilter X
⊢ ↑𝒰 ≤ comap f (𝓝 y) ⊓ ℱ → ∃ x, f x = y ∧ ∃ u, ↑u ≤ 𝓝 x ⊓ ℱ
Module: Mathlib.Topology.Algebra.Monoid

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

Tactic:
simp_rw [mul_comm, hleft x₀]

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
hf : Continuous[inst✝², inst✝¹] f
hg : Continuous[inst✝¹, inst✝] g
hgf : IsProperMap (g ∘ f)
f_surj : Surjective f
⊢ IsProperMap g

Tactic:
refine ⟨hg, fun ℱ z h ↦ ?_⟩
  rw [← ℱ.map_comap_of_surjective f_surj, ← mapClusterPt_comp] at h
  rcases hgf.clusterPt_of_mapClusterPt h with ⟨x, rfl, hx⟩
  rw [← ℱ.map_comap_of_surjective f_surj]
  exact ⟨f x, rfl, hx.map hf.continuousAt tendsto_map⟩

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
s s' : Set G
hs₀ : s ∈ 𝓝 1
h_symm : ∀ x ∈ s, x⁻¹ ∈ s
⊢ closure[inst✝²] s' ⊆ s * s'

Tactic:
intro y

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
s s' : Set G
hs₀ : s ∈ 𝓝 1
h_symm : ∀ x ∈ s, x⁻¹ ∈ s
y : G
⊢ y ∈ closure[inst✝²] s' → y ∈ s * s'
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
s s' : Set G
hs₀ : s ∈ 𝓝 1
h_symm : ∀ x ∈ s, x⁻¹ ∈ s
y : G
hy : y ∈ closure[inst✝²] s'
b : G
hb : b ∈ s
hc : (fun x ↦ x * y) b ∈ s'
⊢ y ∈ s * s'

Tactic:
simpa using Set.mul_mem_mul (h_symm b hb) hc

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
s s' : Set G
hs'₀ : s' ∈ 𝓝 1
h_symm : ∀ x ∈ s', x⁻¹ ∈ s'
⊢ closure[inst✝²] s ⊆ s * s'

Tactic:
intro y

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
s s' : Set G
hs'₀ : s' ∈ 𝓝 1
h_symm : ∀ x ∈ s', x⁻¹ ∈ s'
y : G
⊢ y ∈ closure[inst✝²] s → y ∈ s * s'
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : InvolutiveInv G
inst✝ : ContinuousInv G
a : G
⊢ (𝓝[≠] a)⁻¹ = 𝓝[≠] a⁻¹

Tactic:
convert! (Homeomorph.inv G).isEmbedding.map_nhdsWithin_eq .. using 2

Goal state after:
case e'_3.e'_4
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : InvolutiveInv G
inst✝ : ContinuousInv G
a : G
⊢ {a⁻¹}ᶜ = ⇑(Homeomorph.inv G) '' {a}ᶜ
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : IsUniformGroup α
inst✝ : UniformSpace β
f : β → α
hf : UniformContinuous f
n : ℕ
⊢ UniformContinuous fun x ↦ f x ^ (n + 1)

Tactic:
simp_rw [pow_succ']

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : IsUniformGroup α
inst✝ : UniformSpace β
f : β → α
hf : UniformContinuous f
n : ℕ
⊢ UniformContinuous fun x ↦ f x * f x ^ n
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
φ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₂ * y₂⁻¹ * y₁ * x₁⁻¹
ψ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁⁻¹ * x₂ * (y₂⁻¹ * y₁)
g : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁
x✝ : (β × β) × β × β
⊢ φ x✝ = (g * ψ * g⁻¹) x✝

Tactic:
simp [φ, ψ, g, mul_assoc]

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
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : (𝓝 1).HasBasis (fun x ↦ True) u
u_anti : Antitone u
this : ∀ (ib : ℕ), ∃ a b, True ∧ ∀ (a_1 b_1 : G), a_1 ∈ u a → b_1 ∈ u b → a_1 * b_1 ∈ u ib
event_mul : ∀ (n : ℕ), ∀ᶠ (m : ℕ) in atTop, u m * u m ⊆ u n
⊢ ∃ u, (𝓝 1).HasAntitoneBasis u ∧ ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n

Tactic:
obtain ⟨φ, -, hφ, φ_anti_basis⟩ := HasAntitoneBasis.subbasis_with_rel ⟨hu, u_anti⟩ event_mul

Goal state after:
G : Type w
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : (𝓝 1).HasBasis (fun x ↦ True) u
u_anti : Antitone u
this : ∀ (ib : ℕ), ∃ a b, True ∧ ∀ (a_1 b_1 : G), a_1 ∈ u a → b_1 ∈ u b → a_1 * b_1 ∈ u ib
event_mul : ∀ (n : ℕ), ∀ᶠ (m : ℕ) in atTop, u m * u m ⊆ u n
φ : ℕ → ℕ
hφ : ∀ ⦃m n : ℕ⦄, m < n → u (φ n) * u (φ n) ⊆ u (φ m)
φ_anti_basis : (𝓝 1).HasAntitoneBasis (u ∘ φ)
⊢ ∃ u, (𝓝 1).HasAntitoneBasis u ∧ ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
Module: Mathlib.Order.Filter.AtTopBot.Field

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
c : α
n : ℕ
⊢ Tendsto (fun x ↦ c * x ^ n) atTop atBot ↔ n ≠ 0 ∧ c < 0

Tactic:
simp only [← tendsto_neg_atTop_iff, ← neg_mul, tendsto_const_mul_pow_atTop_iff, neg_pos]

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

Goal state before:
pp: K : Type u_1
inst✝⁷ : DivisionRing K
inst✝⁶ : TopologicalSpace K
R : Type u_2
inst✝⁵ : DivisionSemiring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : PosMulReflectLT R
inst✝¹ : TopologicalSpace R
inst✝ : ContinuousInv₀ R
⊢ Continuous (unitsEquivPos R).toFun

Tactic:
Topology.IsEmbedding.subtypeVal.continuous_iff

Goal state after:
K : Type u_1
inst✝⁷ : DivisionRing K
inst✝⁶ : TopologicalSpace K
R : Type u_2
inst✝⁵ : DivisionSemiring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : PosMulReflectLT R
inst✝¹ : TopologicalSpace R
inst✝ : ContinuousInv₀ R
⊢ Continuous (Subtype.val ∘ (unitsEquivPos R).toFun)
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝¹² : TopologicalSpace α
inst✝¹¹ : AddCommGroup α
inst✝¹⁰ : IsTopologicalAddGroup α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : AddCommGroup β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : AddCommGroup γ
inst✝⁵ : IsTopologicalAddGroup γ
inst✝⁴ : TopologicalSpace δ
inst✝³ : AddCommGroup δ
inst✝² : UniformSpace G
inst✝¹ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
f : δ →+ γ
df : IsDenseInducing ⇑f
φ : β →+ δ →+ G
hφ : Continuous[instTopologicalSpaceProd, inst✝².toTopologicalSpace] fun p ↦ (φ p.1) p.2
W' : Set G
W'_nhds : W' ∈ 𝓝 0
inst✝ : IsUniformAddGroup G
x₀ : α
y₀ : γ
ee : β × β → α × α := fun u ↦ (e u.1, e u.2)
ff : δ × δ → γ × γ := fun u ↦ (f u.1, f u.2)
lim_φ : Tendsto (fun p ↦ (φ p.1) p.2) (𝓝 (0, 0)) (𝓝 0)
lim_φ_sub_sub :
  Tendsto (fun p ↦ (fun p ↦ (φ p.1) p.2) (p.1.2 - p.1.1, p.2.2 - p.2.1))
    (comap ee (𝓝 (x₀, x₀)) ×ˢ comap ff (𝓝 (y₀, y₀))) (𝓝 0)
W : Set G
W_nhds : W ∈ 𝓝 0
W4 : ∀ {v w s t : G}, v ∈ W → w ∈ W → s ∈ W → t ∈ W → v + w + s + t ∈ W'
U₁ : Set β
U₁_nhds : U₁ ∈ comap (⇑e) (𝓝 x₀)
V₁ : Set δ
V₁_nhds : V₁ ∈ comap (⇑f) (𝓝 y₀)
H : ∀ x ∈ U₁, ∀ x' ∈ U₁, ∀ y ∈ V₁, ∀ y' ∈ V₁, (fun p ↦ (φ p.1) p.2) (x' - x, y' - y) ∈ W
x₁ : β
x₁_in : x₁ ∈ U₁
y₁ : δ
y₁_in : y₁ ∈ V₁
⊢ Continuous[instTopologicalSpaceProd, inst✝².toTopologicalSpace] fun p ↦ (φ.flip p.1) p.2

Tactic:
change Continuous ((fun p : β × δ => φ p.1 p.2) ∘ Prod.swap)

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝¹² : TopologicalSpace α
inst✝¹¹ : AddCommGroup α
inst✝¹⁰ : IsTopologicalAddGroup α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : AddCommGroup β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : AddCommGroup γ
inst✝⁵ : IsTopologicalAddGroup γ
inst✝⁴ : TopologicalSpace δ
inst✝³ : AddCommGroup δ
inst✝² : UniformSpace G
inst✝¹ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
f : δ →+ γ
df : IsDenseInducing ⇑f
φ : β →+ δ →+ G
hφ : Continuous[instTopologicalSpaceProd, inst✝².toTopologicalSpace] fun p ↦ (φ p.1) p.2
W' : Set G
W'_nhds : W' ∈ 𝓝 0
inst✝ : IsUniformAddGroup G
x₀ : α
y₀ : γ
ee : β × β → α × α := fun u ↦ (e u.1, e u.2)
ff : δ × δ → γ × γ := fun u ↦ (f u.1, f u.2)
lim_φ : Tendsto (fun p ↦ (φ p.1) p.2) (𝓝 (0, 0)) (𝓝 0)
lim_φ_sub_sub :
  Tendsto (fun p ↦ (fun p ↦ (φ p.1) p.2) (p.1.2 - p.1.1, p.2.2 - p.2.1))
    (comap ee (𝓝 (x₀, x₀)) ×ˢ comap ff (𝓝 (y₀, y₀))) (𝓝 0)
W : Set G
W_nhds : W ∈ 𝓝 0
W4 : ∀ {v w s t : G}, v ∈ W → w ∈ W → s ∈ W → t ∈ W → v + w + s + t ∈ W'
U₁ : Set β
U₁_nhds : U₁ ∈ comap (⇑e) (𝓝 x₀)
V₁ : Set δ
V₁_nhds : V₁ ∈ comap (⇑f) (𝓝 y₀)
H : ∀ x ∈ U₁, ∀ x' ∈ U₁, ∀ y ∈ V₁, ∀ y' ∈ V₁, (fun p ↦ (φ p.1) p.2) (x' - x, y' - y) ∈ W
x₁ : β
x₁_in : x₁ ∈ U₁
y₁ : δ
y₁_in : y₁ ∈ V₁
⊢ Continuous[instTopologicalSpaceProd, inst✝².toTopologicalSpace] ((fun p ↦ (φ p.1) p.2) ∘ Prod.swap)
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y x' y' : (i : ι) → α i
⊢ (Icc x y \ univ.pi fun i ↦ Ioo (x' i) (y' i)) ⊆ (⋃ i, Icc x (update y i (x' i))) ∪ ⋃ i, Icc (update x i (y' i)) y

Tactic:
rintro a ⟨⟨hxa, hay⟩, ha'⟩

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y x' y' a : (i : ι) → α i
ha' : a ∉ univ.pi fun i ↦ Ioo (x' i) (y' i)
hxa : x ≤ a
hay : a ≤ y
⊢ a ∈ (⋃ i, Icc x (update y i (x' i))) ∪ ⋃ i, Icc (update x i (y' i)) y