mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.Grp.AB

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
X Y : Discrete J ⥤ AddCommGrpCat
f : X ⟶ Y
hf : Epi f
iX : limit X ≅ AddCommGrpCat.of ((i : J) → ↑(X.obj { as := i })) :=
  (Pi.isoLimit X).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ X.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ X.obj { as := j }).isLimit
iY : limit Y ≅ AddCommGrpCat.of ((i : J) → ↑(Y.obj { as := i })) :=
  (Pi.isoLimit Y).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ Y.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ Y.obj { as := j }).isLimit
⊢ (Pi.map fun i ↦ ⇑(ConcreteCategory.hom (f.app { as := i }))) =
    ⇑(ConcreteCategory.hom
        (limit.lift (Discrete.functor fun j ↦ X.obj { as := j })
            { pt := AddCommGrpCat.of ((j : J) → ↑(X.obj { as := j })),
              π :=
                Discrete.natTrans fun j ↦
                  AddCommGrpCat.ofHom (Pi.evalAddMonoidHom (fun j ↦ ↑(X.obj { as := j })) j.as) } ≫
          limit.lift Y ((Cone.postcompose f).obj (Pi.cone X)) ≫
            (productIsProduct' Y).lift (getLimitCone Y).cone ≫
              AddCommGrpCat.ofHom
                {
                  toFun := fun x j ↦
                    (ConcreteCategory.hom
                        ((getLimitCone (Discrete.functor fun j ↦ Y.obj { as := j })).cone.π.app { as := j }))
                      x,
                  map_zero' := ⋯, map_add' := ⋯ }))

Tactic:
ext g j

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
X Y : Discrete J ⥤ AddCommGrpCat
f : X ⟶ Y
hf : Epi f
iX : limit X ≅ AddCommGrpCat.of ((i : J) → ↑(X.obj { as := i })) :=
  (Pi.isoLimit X).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ X.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ X.obj { as := j }).isLimit
iY : limit Y ≅ AddCommGrpCat.of ((i : J) → ↑(Y.obj { as := i })) :=
  (Pi.isoLimit Y).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ Y.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ Y.obj { as := j }).isLimit
g : (i : J) → ↑(X.obj { as := i })
j : J
⊢ Pi.map (fun i ↦ ⇑(ConcreteCategory.hom (f.app { as := i }))) g j =
    (ConcreteCategory.hom
        (limit.lift (Discrete.functor fun j ↦ X.obj { as := j })
            { pt := AddCommGrpCat.of ((j : J) → ↑(X.obj { as := j })),
              π :=
                Discrete.natTrans fun j ↦
                  AddCommGrpCat.ofHom (Pi.evalAddMonoidHom (fun j ↦ ↑(X.obj { as := j })) j.as) } ≫
          limit.lift Y ((Cone.postcompose f).obj (Pi.cone X)) ≫
            (productIsProduct' Y).lift (getLimitCone Y).cone ≫
              AddCommGrpCat.ofHom
                {
                  toFun := fun x j ↦
                    (ConcreteCategory.hom
                        ((getLimitCone (Discrete.functor fun j ↦ Y.obj { as := j })).cone.π.app { as := j }))
                      x,
                  map_zero' := ⋯, map_add' := ⋯ }))
      g j
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C : Type u
F : C → Type v
x✝² : C
x✝¹ x✝ : F x✝²
h : ((sigma F).inj x✝² x✝¹).fst = ((sigma F).inj x✝² x✝).fst ∧ ((sigma F).inj x✝² x✝¹).snd ≍ ((sigma F).inj x✝² x✝).snd
⊢ x✝¹ = x✝

Tactic:
simpa using h

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C : Type u
F : C → Type v
X Y : Type u
f : X ⟶ Y
inst✝ : Mono f
⊢ Nonempty (IsColimit (BinaryCofan.mk f (↾Subtype.val)))

Tactic:
rw [binaryCofan_isColimit_iff]

Goal state after:
C : Type u
F : C → Type v
X Y : Type u
f : X ⟶ Y
inst✝ : Mono f
⊢ Injective ⇑(ConcreteCategory.hom (BinaryCofan.mk f (↾Subtype.val)).inl) ∧
    Injective ⇑(ConcreteCategory.hom (BinaryCofan.mk f (↾Subtype.val)).inr) ∧
      IsCompl (Set.range ⇑(ConcreteCategory.hom (BinaryCofan.mk f (↾Subtype.val)).inl))
        (Set.range ⇑(ConcreteCategory.hom (BinaryCofan.mk f (↾Subtype.val)).inr))
Module: Mathlib.Algebra.Ring.NegOnePow

Goal state before:
pp: n : ℤ
hn : Even n
⊢ n.negOnePow = 1

Tactic:
by
  obtain ⟨k, rfl⟩ := hn
  rw [negOnePow_add, units_mul_self]

Goal state after:
Module: Mathlib.Algebra.Ring.NegOnePow

Goal state before:
pp: case pos
n₁ n₂ : ℤ
h₂ : Even n₂
⊢ n₁.negOnePow = n₂.negOnePow ↔ Even (n₁ - n₂)

Tactic:
rw [negOnePow_even _ h₂, Int.even_sub, negOnePow_eq_one_iff]
    tauto

Goal state after:
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: case ofNat
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddGroup α
h : Periodic f c
n : ℕ
⊢ Periodic f (Int.ofNat n • c)

pp: case negSucc
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddGroup α
h : Periodic f c
n : ℕ
⊢ Periodic f (Int.negSucc n • c)

Tactic:
· simpa only [Int.ofNat_eq_natCast, natCast_zsmul] using h.nsmul n

Goal state after:
case negSucc
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddGroup α
h : Periodic f c
n : ℕ
⊢ Periodic f (Int.negSucc n • c)
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
⊢ Pairwise (Disjoint on fun n ↦ Ioc (↑n) (↑n + 1))

Tactic:
by
  simpa only [zero_add] using pairwise_disjoint_Ioc_add_intCast (0 : α)

Goal state after:
Module: Mathlib.Data.Nat.Count

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
⊢ count p (a + b) = count (fun k ↦ p (k + b)) a + count p b

Tactic:
rw [add_comm, count_add, add_comm]
  simp_rw [add_comm b]

Goal state after:
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x ↦ x * p
a : ℕ
⊢ ∀ (x : ℕ), x < p ^ n ∧ x * p = a → a < p ^ (n + 1)

Tactic:
rintro b ⟨h, rfl⟩

Goal state after:
p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x ↦ x * p
b : ℕ
h : b < p ^ n
⊢ b * p < p ^ (n + 1)
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: α₁ : Type u_6
α₂ : Type u_7
β₁ : Type u_8
β₂ : Type u_9
inst✝¹ : Preorder β₁
inst✝ : Preorder β₂
u₁ : β₁ → α₁
u₂ : β₂ → α₂
⊢ map u₁ atTop ×ˢ map u₂ atTop = map (Prod.map u₁ u₂) atTop

Tactic:
by
  rw [prod_map_map_eq, prod_atTop_atTop_eq, Prod.map_def]

Goal state after:
Module: Mathlib.Order.Filter.Curry

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
m : Filter β
s : Set α
t : Set β
⊢ (∃ᶠ (x : α × β) in l.curry m, x ∈ s ×ˢ t) ↔ (∃ᶠ (x : α) in l, x ∈ s) ∧ ∃ᶠ (y : β) in m, y ∈ t

Tactic:
by
  simp [frequently_curry_iff]

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIcoMod hp (a + m • p) b = m • p + toIcoMod hp a b

Tactic:
toIcoMod_add_zsmul',

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIcoMod hp a b + m • p = m • p + toIcoMod hp a b
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
h : Set α → Set β
s : Set β
⊢ f.lift' h ⊓ 𝓟 s = f.lift' fun t ↦ h t ∩ s

Tactic:
by
  simp only [Filter.lift', Filter.lift, (· ∘ ·), ← inf_principal, iInf_subtype', ← iInf_inf]

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ b - c - toIcoDiv hp (a + c) b • p = b - toIcoDiv hp (a + c) b • p - c

Tactic:
sub_right_comm

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ b - c - toIocDiv hp (a + c) b • p = b - toIocDiv hp (a + c) b • p - c

Tactic:
sub_right_comm

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
ι : Sort v
inst✝ : Finite ι
f : ι → Set X
⊢ interior (⋂ i, f i) = ⋂ i, interior (f i)

Tactic:
rw [← sInter_range, (finite_range f).interior_sInter, biInter_range]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
S : Set (Set X)
hS : S.Finite
⊢ closure (⋃₀ S) = ⋃ s ∈ S, closure s

Tactic:
by
  rw [sUnion_eq_biUnion, hS.closure_biUnion]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ interior s = ∅ ↔ closure sᶜ = univ

Tactic:
closure_compl,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ interior s = ∅ ↔ (interior s)ᶜ = univ
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s U : Set X
h : U ∈ ⨆ x ∈ s, 𝓝 x
⊢ ∀ x ∈ s, U ∈ 𝓝 x

Tactic:
simpa using h

Goal state after:
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ 𝓝 x = pure x ↔ 𝓝[≠] x = ⊥

Tactic:
nhdsWithin,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ 𝓝 x = pure x ↔ 𝓝 x ⊓ 𝓟 {x}ᶜ = ⊥
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ (𝓝[s] x).NeBot ↔ ∀ ⦃t : Set X⦄, t ∈ 𝓝 x → (t ∩ s).Nonempty

Tactic:
nhdsWithin,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ (𝓝 x ⊓ 𝓟 s).NeBot ↔ ∀ ⦃t : Set X⦄, t ∈ 𝓝 x → (t ∩ s).Nonempty
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ frontier s = closure s ∩ closure sᶜ

Tactic:
closure_compl,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ frontier s = closure s ∩ (interior s)ᶜ
Module: Mathlib.Topology.Continuous

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
x : X
g : X → Y
h : f =ᶠ[𝓝 x] g
⊢ ContinuousAt f x ↔ ContinuousAt g x

Tactic:
simp only [ContinuousAt, tendsto_congr' h, h.eq_of_nhds]

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp a b = toIcoMod hp 0 (b - a) + a

Tactic:
by
  rw [toIcoMod_sub_eq_sub, zero_add, sub_add_cancel]

Goal state after:
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
⊢ (𝓝[≠] x ⊓ F).NeBot ↔ ClusterPt x (𝓟 {x}ᶜ ⊓ F)

Tactic:
nhdsWithin,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
⊢ (𝓝 x ⊓ 𝓟 {x}ᶜ ⊓ F).NeBot ↔ ClusterPt x (𝓟 {x}ᶜ ⊓ F)
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ x ∈ interior s ↔ x ∉ closure[inst✝] sᶜ

Tactic:
closure_compl,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ x ∈ interior s ↔ x ∉ (interior s)ᶜ
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
ι : Sort w
x : X
t : Set X
p : ι → Prop
s : ι → Set X
h : (𝓝 x).HasBasis p s
⊢ (∀ ⦃i : ι⦄, p i → ∀ ⦃j : Unit⦄, True → (s i ∩ t).Nonempty) ↔ ∀ (i : ι), p i → (s i ∩ t).Nonempty

Tactic:
by simp only [forall_const]

Goal state after:
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
⊢ ClusterPt x (F.lift' closure[inst✝]) ↔ ClusterPt x F

Tactic:
simp [clusterPt_iff_lift'_closure, lift'_lift'_assoc (monotone_closure X) (monotone_closure X)]

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case H.H.H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
hp' : Fact (0 < p)
z✝² z✝¹ z✝ : α
h₁₂₃ : toIcoMod ⋯ z✝² z✝¹ ≤ toIocMod ⋯ z✝² z✝
h₃₂₁ : toIcoMod ⋯ z✝² z✝ ≤ toIocMod ⋯ z✝² z✝¹
⊢ z✝² ≡ z✝¹ [PMOD p] ∨ z✝¹ ≡ z✝ [PMOD p] ∨ z✝ ≡ z✝² [PMOD p]

Tactic:
simpa only [modEq_comm] using toIxxMod_antisymm _ h₁₂₃ h₃₂₁

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
p : R
hp : 0 < p
a b : R
⊢ ↑(toIocDiv hp a b) * p - b = -toIocMod hp a b

Tactic:
by
  simpa using toIocDiv_zsmul_sub_self hp a b

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: β : Type u_2
α : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
f : α → β
h : ∀ (b : β), IsOpen[inst✝²] (f ⁻¹' {b})
s : Set β
x✝ : IsOpen[inst✝¹] s
⊢ IsOpen[inst✝²] (f ⁻¹' ⋃ x ∈ s, {x})

Tactic:
preimage_iUnion₂

Goal state after:
β : Type u_2
α : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
f : α → β
h : ∀ (b : β), IsOpen[inst✝²] (f ⁻¹' {b})
s : Set β
x✝ : IsOpen[inst✝¹] s
⊢ IsOpen[inst✝²] (⋃ i ∈ s, f ⁻¹' {i})
Module: Mathlib.Topology.Order

Goal state before:
pp: case mp
α : Type u
t : TopologicalSpace α
⊢ induced ofTopology t = ⊤ → t = ⊤

Tactic:
intro h
    simpa [induced_compose, comp_def, induced_fun_id] using congr(induced (toTopology t) $h)

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace X
hf : IsInducing f
s : Set X
x : X
⊢ x ∈ closure[inst✝] s ↔ x ∈ f ⁻¹' closure[inst✝¹] (f '' s)

Tactic:
Set.mem_preimage,

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace X
hf : IsInducing f
s : Set X
x : X
⊢ x ∈ closure[inst✝] s ↔ f x ∈ closure[inst✝¹] (f '' s)
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
s : Set X
⊢ ⇑h.symm ⁻¹' frontier s = frontier (⇑h.symm ⁻¹' s)

Tactic:
preimage_frontier

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
s : Set X
⊢ frontier (⇑h.symm ⁻¹' s) = frontier (⇑h.symm ⁻¹' s)
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
a : α
s : Set α
⊢ a ∈ closure[induced f t] s ↔ f a ∈ closure[t] (f '' s)

Tactic:
simp only [mem_closure_iff_frequently, nhds_induced, frequently_comap, mem_image, and_comm]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f_closed : IsClosedMap f
f_cont : Continuous[inst✝¹, inst✝] f
F : Filter X
⊢ F.lift' (closure[inst✝] ∘ image f) = map f (F.lift' closure[inst✝¹])

Tactic:
map_lift'_eq (monotone_closure X)

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f_closed : IsClosedMap f
f_cont : Continuous[inst✝¹, inst✝] f
F : Filter X
⊢ F.lift' (closure[inst✝] ∘ image f) = F.lift' (image f ∘ closure[inst✝¹])
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
h : Continuous[instTopologicalSpaceProd, tc1] fun p ↦ f p.1 p.2
⊢ Continuous[instTopologicalSpaceProd, tc1] fun p ↦ f p.1 p.2

Tactic:
have ha := @continuous_inf_dom_right _ _ id ta1 ta2 ta2 (@continuous_id _ (id _))
  have hb := @continuous_inf_dom_right _ _ id tb1 tb2 tb2 (@continuous_id _ (id _))
  have h_continuous_id := @Continuous.prodMap _ _ _ _ ta2 tb2 (ta1 ⊓ ta2) (tb1 ⊓ tb2) _ _ ha hb
  exact @Continuous.comp _ _ _ (id _) (id _) _ _ _ h h_continuous_id

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsClosedEmbedding f
s : Set X
h : IsClosed[inst✝] (f '' s)
⊢ IsClosed[inst✝¹] s

Tactic:
by
    rw [← preimage_image_eq s hf.injective]
    exact h.preimage hf.continuous

Goal state after:
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set (X × Y)
hs : IsClosed[instTopologicalSpaceProd] s
⊢ IsClosed[instTopologicalSpaceProd] (Prod.swap '' s)

Tactic:
rw [image_swap_eq_preimage_swap]
  exact hs.preimage continuous_swap

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
⊢ 𝓝[univ] a = 𝓝 a

Tactic:
nhdsWithin,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
⊢ 𝓝 a ⊓ 𝓟 univ = 𝓝 a
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
x : α
s t : Set α
hs : s ∈ 𝓝[t] x
t' : Set α
⊢ s \ t' ∈ 𝓝[t \ t'] x

Tactic:
nhdsWithin,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
x : α
s t : Set α
hs : s ∈ 𝓝[t] x
t' : Set α
⊢ s \ t' ∈ 𝓝 x ⊓ 𝓟 (t \ t')
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
x : α
⊢ s ∩ t =ᶠ[𝓝 x] s ∩ t ∩ s

Tactic:
simp [inter_comm s t, inter_assoc]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
⊢ 𝓝[∅] a = ⊥

Tactic:
nhdsWithin,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
⊢ 𝓝 a ⊓ 𝓟 ∅ = ⊥
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
⊢ 𝓝[{a}] a = pure a

Tactic:
nhdsWithin,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
⊢ 𝓝 a ⊓ 𝓟 {a} = pure a
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s u : Set α
t v : Set β
a : α
b : β
hu : u ∈ 𝓝[s] a
hv : v ∈ 𝓝[t] b
⊢ u ×ˢ v ∈ 𝓝[s] a ×ˢ 𝓝[t] b

Tactic:
exact prod_mem_prod hu hv

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
x : ↑s
⊢ 𝓝[s ↓∩ t] x = ⊥ ↔ comap Subtype.val (𝓝[t] ↑x) = ⊥

Tactic:
nhdsWithin,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
x : ↑s
⊢ 𝓝 x ⊓ 𝓟 (s ↓∩ t) = ⊥ ↔ comap Subtype.val (𝓝[t] ↑x) = ⊥
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
x : ↑s
⊢ 𝓝 x ⊓ 𝓟 (s ↓∩ t) = ⊥ ↔ comap Subtype.val (𝓝[t] ↑x) = ⊥

Tactic:
nhdsWithin,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
x : ↑s
⊢ 𝓝 x ⊓ 𝓟 (s ↓∩ t) = ⊥ ↔ comap Subtype.val (𝓝 ↑x ⊓ 𝓟 t) = ⊥
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
x : X
y : Y
hs : Prod.fst ⁻¹' s ∈ 𝓝[Prod.snd ⁻¹' {(x, y).2}] (x, y)
⊢ s ∈ 𝓝 (x, y).1

Tactic:
nhdsWithin,

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
x : X
y : Y
hs : Prod.fst ⁻¹' s ∈ 𝓝 (x, y) ⊓ 𝓟 (Prod.snd ⁻¹' {(x, y).2})
⊢ s ∈ 𝓝 (x, y).1
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
x : X
y : Y
hs : Prod.snd ⁻¹' s ∈ 𝓝[Prod.fst ⁻¹' {(x, y).1}] (x, y)
⊢ s ∈ 𝓝 (x, y).2

Tactic:
nhdsWithin,

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
x : X
y : Y
hs : Prod.snd ⁻¹' s ∈ 𝓝 (x, y) ⊓ 𝓟 (Prod.fst ⁻¹' {(x, y).1})
⊢ s ∈ 𝓝 (x, y).2
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
a : { x // x ∈ s }
t u : Set { x // x ∈ s }
⊢ t ∈ 𝓝[u] a ↔ t ∈ comap Subtype.val (𝓝[Subtype.val '' u] ↑a)

Tactic:
nhdsWithin,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
a : { x // x ∈ s }
t u : Set { x // x ∈ s }
⊢ t ∈ 𝓝 a ⊓ 𝓟 u ↔ t ∈ comap Subtype.val (𝓝[Subtype.val '' u] ↑a)
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case e'_3
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
p : X → Prop
f : Y → X
hf : IsOpenMap f
hp : ∀ (x : Y), p (f x)
u : Set Y
hu : IsOpen[inst✝] u
⊢ (fun x ↦ ⟨f x, ⋯⟩) '' u = Subtype.val ⁻¹' f '' u

Tactic:
exact Set.ext fun _ ↦ exists_congr fun _ ↦ and_congr_right' Subtype.ext_iff

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case e'_3
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
p : X → Prop
f : Y → X
hf : IsClosedMap f
hp : ∀ (x : Y), p (f x)
u : Set Y
hu : IsClosed[inst✝] u
⊢ (fun x ↦ ⟨f x, ⋯⟩) '' u = Subtype.val ⁻¹' f '' u

Tactic:
exact Set.ext fun _ ↦ exists_congr fun _ ↦ and_congr_right' Subtype.ext_iff

Goal state after:
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: case mp
X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X ⊕ Y → Z
⊢ IsClosedMap f → (IsClosedMap fun a ↦ f (inl a)) ∧ IsClosedMap fun b ↦ f (inr b)

Tactic:
intro h
    exact ⟨h.comp IsClosedEmbedding.inl.isClosedMap, h.comp IsClosedEmbedding.inr.isClosedMap⟩

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
s : Set (α × β)
x : α × β
⊢ Tendsto f (𝓝[s] (x.1, x.2)) (𝓝 (f (x.1, x.2))) ↔
    Tendsto (fun x_1 ↦ f (x.1, x_1)) (𝓝[{b | (x.1, b) ∈ s}] x.2) (𝓝 (f (x.1, x.2)))

Tactic:
nhdsWithin,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
s : Set (α × β)
x : α × β
⊢ Tendsto f (𝓝 (x.1, x.2) ⊓ 𝓟 s) (𝓝 (f (x.1, x.2))) ↔
    Tendsto (fun x_1 ↦ f (x.1, x_1)) (𝓝 x.2 ⊓ 𝓟 {b | (x.1, b) ∈ s}) (𝓝 (f (x.1, x.2)))
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
s : Set (α × β)
x : α × β
⊢ Tendsto f (𝓝[s] (x.1, x.2)) (𝓝 (f (x.1, x.2))) ↔
    Tendsto (fun x_1 ↦ f (x_1, x.2)) (𝓝[{a | (a, x.2) ∈ s}] x.1) (𝓝 (f (x.1, x.2)))

Tactic:
nhdsWithin,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
s : Set (α × β)
x : α × β
⊢ Tendsto f (𝓝 (x.1, x.2) ⊓ 𝓟 s) (𝓝 (f (x.1, x.2))) ↔
    Tendsto (fun x_1 ↦ f (x_1, x.2)) (𝓝 x.1 ⊓ 𝓟 {a | (a, x.2) ∈ s}) (𝓝 (f (x.1, x.2)))
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
g : β → α
x : β
s : Set β
h : LeftInvOn f g s
hx : f (g x) = x
hf : ContinuousWithinAt f (g '' s) (g x)
hg : ContinuousWithinAt g s x
A : g ∘ f =ᶠ[𝓝[g '' s] g x] id
⊢ Tendsto f (𝓝[g '' s] g x) (𝓝[s] x)

Tactic:
simpa only [hx] using hf.tendsto_nhdsWithin (h.mapsTo (surjOn_image _ _))

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
s : Set ι
⊢ IsOpen[instTopologicalSpaceSigma] (Sigma.fst ⁻¹' ⋃ x ∈ s, {x})

Tactic:
preimage_iUnion₂

Goal state after:
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
s : Set ι
⊢ IsOpen[instTopologicalSpaceSigma] (⋃ i ∈ s, Sigma.fst ⁻¹' {i})
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝[s] x
⊢ ∃ t, (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x

Tactic:
choose! V V_nhds hV using fun x hx => mem_nhdsWithin_iff_exists_mem_nhds_inter.1 (hU x hx)
  refine (hs.elim_nhds_subcover V V_nhds).imp fun t ⟨t_sub_s, ht⟩ =>
    ⟨t_sub_s, subset_trans ?_ (iUnion₂_mono fun x hx => hV x (t_sub_s x hx))⟩
  simpa [← iUnion_inter]

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set (SeparationQuotient X)
x : X
⊢ map mk (𝓝[mk ⁻¹' s] x) = 𝓝[s] mk x

Tactic:
nhdsWithin,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (SeparationQuotient X)
x : X
⊢ map mk (𝓝 x ⊓ 𝓟 (mk ⁻¹' s)) = 𝓝[s] mk x