mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
Φ : uliftYoneda.{max w v₂, v₁, u₁}.LeftExtension (F ⋙ uliftYoneda.{max w v₁, v₂, u₂})
f g : Functor.LeftExtension.mk F.op.lan (compULiftYonedaIsoULiftYonedaCompLan F).hom ⟶ Φ
P : Cᵒᵖ ⥤ Type (max (max w v₁) v₂)
x : P.Elementsᵒᵖ
eq :
  (𝟭 (Cᵒᵖ ⥤ Type (max (max w v₂) v₁))).map (uliftYonedaEquiv.symm (unop x).snd) ≫ F.op.lanUnit.app P =
    F.op.lanUnit.app (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop (unop x).1)) ≫
      (F.op.lan ⋙ (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max (max w v₂) v₁))).obj F.op).map
        (uliftYonedaEquiv.symm (unop x).snd)
⊢ (coconeOfRepresentable P).ι.app x ≫ F.op.lanUnit.app P ≫ F.op.whiskerLeft ((StructuredArrow.Hom.right f).app P) =
    (coconeOfRepresentable P).ι.app x ≫ F.op.lanUnit.app P ≫ F.op.whiskerLeft ((StructuredArrow.Hom.right g).app P)

Tactic:
have eq₁ := congr_hom (CC := fun X ↦ X) (congr_app (congr_app (StructuredArrow.w f) x.unop.1.unop)
    (F.op.obj x.unop.1)) (ULift.up (𝟙 _))

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
Φ : uliftYoneda.{max w v₂, v₁, u₁}.LeftExtension (F ⋙ uliftYoneda.{max w v₁, v₂, u₂})
f g : Functor.LeftExtension.mk F.op.lan (compULiftYonedaIsoULiftYonedaCompLan F).hom ⟶ Φ
P : Cᵒᵖ ⥤ Type (max (max w v₁) v₂)
x : P.Elementsᵒᵖ
eq :
  (𝟭 (Cᵒᵖ ⥤ Type (max (max w v₂) v₁))).map (uliftYonedaEquiv.symm (unop x).snd) ≫ F.op.lanUnit.app P =
    F.op.lanUnit.app (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop (unop x).1)) ≫
      (F.op.lan ⋙ (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max (max w v₂) v₁))).obj F.op).map
        (uliftYonedaEquiv.symm (unop x).snd)
eq₁ :
  (hom
        (((StructuredArrow.hom (Functor.LeftExtension.mk F.op.lan (compULiftYonedaIsoULiftYonedaCompLan F).hom) ≫
                  ((Functor.whiskeringLeft C (Cᵒᵖ ⥤ Type (max (max w v₁) v₂)) (Dᵒᵖ ⥤ Type (max (max w v₁) v₂))).obj
                        uliftYoneda.{max w v₂, v₁, u₁}).map
                    (StructuredArrow.Hom.right f)).app
              (unop (unop x).fst)).app
          (F.op.obj (unop x).fst)))
      { down := 𝟙 (unop (F.op.obj (unop x).fst)) } =
    (hom (((StructuredArrow.hom Φ).app (unop (unop x).fst)).app (F.op.obj (unop x).fst)))
      { down := 𝟙 (unop (F.op.obj (unop x).fst)) }
⊢ (coconeOfRepresentable P).ι.app x ≫ F.op.lanUnit.app P ≫ F.op.whiskerLeft ((StructuredArrow.Hom.right f).app P) =
    (coconeOfRepresentable P).ι.app x ≫ F.op.lanUnit.app P ≫ F.op.whiskerLeft ((StructuredArrow.Hom.right g).app P)
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
β : Type w
f : β → C
c : Cofan f
hc : IsColimit c
⊢ IsSeparator c.pt ↔ (ObjectProperty.ofObj f).IsSeparating

Tactic:
refine ⟨fun h X Y u v huv => ?_, fun h => isSeparator_of_isColimit_cofan h hc⟩

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
β : Type w
f : β → C
c : Cofan f
hc : IsColimit c
h : IsSeparator c.pt
X Y : C
u v : X ⟶ Y
huv : ∀ (G : C), ObjectProperty.ofObj f G → ∀ (h : G ⟶ X), h ≫ u = h ≫ v
⊢ u = v
Module: Mathlib.Data.Int.SuccPred

Goal state before:
pp: a b : ℕ
⊢ ↑a ⋖ ↑b ↔ a ⋖ b

Tactic:
rw [Order.covBy_iff_add_one_eq, Order.covBy_iff_add_one_eq]
  exact Int.natCast_inj

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
y : N
x : ↥(supExtensionOfMaxSingleton i f y)
a : N
a_mem : a ∈ ↑(extensionOfMax i f).domain
b : N
eq1 : (fun x1 x2 ↦ x1 + x2) a b = ↑x
z : R
eq2 : z • y = b
⊢ ↑x = ↑⟨a, a_mem⟩ + z • y

Tactic:
rw [← eq1, ← eq2]

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
r : R
hr : r • y ∈ (extensionOfMax i f).domain
⊢ (extendIdealTo i f h y) r = ↑(extensionOfMax i f).toLinearPMap ⟨r • y, hr⟩

Tactic:
simp only [ExtensionOfMaxAdjoin.extendIdealTo_is_extension i f h _ _ hr,
    ExtensionOfMaxAdjoin.idealTo, LinearMap.coe_mk, AddHom.coe_mk]

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

Goal state before:
pp: case inr
p : ℕ
inst✝ : Fintype (ZMod p)ˣ
hp : NeZero p
⊢ Prime p ↔ Fintype.card (ZMod p)ˣ = p - 1

Tactic:
ZMod.card_units_eq_totient,

Goal state after:
case inr
p : ℕ
inst✝ : Fintype (ZMod p)ˣ
hp : NeZero p
⊢ Prime p ↔ φ p = p - 1
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case pos
a b : ℕ
h : a ∣ b
h' : φ 0 = φ b
ha : a = 0
⊢ a = b ∨ 2 * a = b

Tactic:
totient_zero,

Goal state after:
case pos
a b : ℕ
h : a ∣ b
h' : 0 = φ b
ha : a = 0
⊢ a = b ∨ 2 * a = b
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case pos
a b : ℕ
h : a ∣ b
h' : φ a = φ 0
ha : ¬a = 0
hb : b = 0
⊢ a = b ∨ 2 * a = b

Tactic:
totient_zero,

Goal state after:
case pos
a b : ℕ
h : a ∣ b
h' : φ a = 0
ha : ¬a = 0
hb : b = 0
⊢ a = b ∨ 2 * a = b
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case pos
a b : ℕ
h : a ∣ b
ha : Even a
h' : φ 0 = φ b
ha' : a = 0
⊢ a = b

Tactic:
totient_zero,

Goal state after:
case pos
a b : ℕ
h : a ∣ b
ha : Even a
h' : 0 = φ b
ha' : a = 0
⊢ a = b
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : closure s ⊆ s
⊢ IsClosed s

Tactic:
subset_closure.antisymm h

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : closure s ⊆ s
⊢ IsClosed (closure s)
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 : α
tfae_3_to_2 : toIcoMod hp a b ≠ toIocMod hp a b → ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
tfae_4_to_3 : toIcoMod hp a b + p = toIocMod hp a b → toIcoMod hp a b ≠ toIocMod hp a b
x✝ : toIcoMod hp a b = a
h : toIcoMod hp a b = a := x✝
⊢ toIcoMod hp a b + p = toIocMod hp a b

Tactic:
rw [h, eq_comm, toIocMod_eq_iff, Set.right_mem_Ioc]
    refine ⟨lt_add_of_pos_right a hp, toIcoDiv hp a b - 1, ?_⟩
    rw [sub_one_zsmul, add_add_add_comm, add_neg_cancel, add_zero]
    conv_lhs => rw [← toIcoMod_add_toIcoDiv_zsmul hp a b, h]

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 : α
⊢ toIcoMod hp c a = toIcoMod hp c b ↔ a ≡ b [PMOD p]

Tactic:
toIcoMod_eq_toIcoMod,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ (∃ n, b - a = n • p) ↔ a ≡ b [PMOD p]
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 x✝ : α
⊢ x✝ ∈ {b | toIcoMod hp a b = toIocMod hp a b} ↔ x✝ ∈ ⋃ z, Set.Ioo (a + z • p) (a + p + z • p)

Tactic:
Set.mem_ofPred,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a x✝ : α
⊢ toIcoMod hp a x✝ = toIocMod hp a x✝ ↔ x✝ ∈ ⋃ z, Set.Ioo (a + z • p) (a + p + z • p)
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
α : Type u_1
x : X
f : α → X
l : Filter α
s : Set α
h : 𝓟 sᶜ ≤ comap f (𝓝 x)
h' : l ⊓ 𝓟 s ≤ comap f (𝓝 x)
this : (l ⊔ 𝓟 sᶜ) ⊓ ⊤ ≤ comap f (𝓝 x)
⊢ l ≤ comap f (𝓝 x)

Tactic:
inf_top_eq,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
α : Type u_1
x : X
f : α → X
l : Filter α
s : Set α
h : 𝓟 sᶜ ≤ comap f (𝓝 x)
h' : l ⊓ 𝓟 s ≤ comap f (𝓝 x)
this : l ⊔ 𝓟 sᶜ ≤ comap f (𝓝 x)
⊢ l ≤ comap f (𝓝 x)
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 : α
⊢ toIocDiv hp a b = toIcoDiv hp a b ∨ toIocDiv hp a b + 1 = toIcoDiv hp a b

Tactic:
rw [eq_comm, ← not_modEq_iff_toIcoDiv_eq_toIocDiv, eq_comm, ←
    modEq_iff_toIcoDiv_eq_toIocDiv_add_one]

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ ¬a ≡ b [PMOD p] ∨ a ≡ b [PMOD p]
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 : α
n : ℤ
hp' : Fact (0 < p)
x₁ x₂ x₃ : α ⧸ AddSubgroup.zmultiples p
⊢ btw x₁ x₂ x₃ ∨ btw x₃ x₂ x₁

Tactic:
induction x₁ using QuotientAddGroup.induction_on
      induction x₂ using QuotientAddGroup.induction_on
      induction x₃ using QuotientAddGroup.induction_on
      simp_rw [btw_coe_iff]
      apply toIxxMod_total

Goal state after:
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 '' frontier s = frontier (⇑h '' s)

Tactic:
rw [← preimage_symm, preimage_frontier]

Goal state after:
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
h : X ≃ₜ Y
f : Z → X
⊢ IsOpenMap (⇑h ∘ f) → IsOpenMap f

Tactic:
intro hf

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
h : X ≃ₜ Y
f : Z → X
hf : IsOpenMap (⇑h ∘ f)
⊢ IsOpenMap f
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
h : X ≃ₜ Y
f : Y → Z
⊢ IsOpenMap (f ∘ ⇑h) → IsOpenMap f

Tactic:
intro hf

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
h : X ≃ₜ Y
f : Y → Z
hf : IsOpenMap (f ∘ ⇑h)
⊢ IsOpenMap f
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hf : Continuous[inst✝², inst✝¹] f
hg : Continuous[inst✝¹, inst✝] g
hgf : IsCoinducing (g ∘ f)
⊢ inst✝ ≤ coinduced g inst✝¹

Tactic:
grw [hgf.eq_coinduced, ← coinduced_compose, hf.coinduced_le]

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Sort u_5
s : ι → Set α
hs : ∀ (x : α), ∃ i, s i ∈ 𝓝 x
hf : ∀ (i : ι), ContinuousOn f (s i)
x : α
i : ι
hi : s i ∈ 𝓝 x
⊢ Tendsto f (𝓝[s i] x) (𝓝 (f x))

Tactic:
exact hf _ _ (mem_of_mem_nhds hi)

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set ↑s
a : ↑s
⊢ ClusterPt a (𝓟 J) ↔ ∃ᶠ (x : α) in map Subtype.val (𝓝 ⟨↑a, ⋯⟩), ∃ (h : x ∈ s), ⟨x, h⟩ ∈ J

Tactic:
Filter.frequently_map,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set ↑s
a : ↑s
⊢ ClusterPt a (𝓟 J) ↔ ∃ᶠ (a : { x // x ∈ t }) in 𝓝 ⟨↑a, ⋯⟩, ∃ (h : ↑a ∈ s), ⟨↑a, h⟩ ∈ J
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: case refine_2
X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
inst✝¹ : Nonempty X
inst✝ : Nonempty Z
f : X → Y
g : Z → W
h : IsOpenMap (Prod.map f g)
⊢ IsOpenMap g

Tactic:
(isOpenQuotientMap_snd (X := X)).isOpenMap_iff

Goal state after:
case refine_2
X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
inst✝¹ : Nonempty X
inst✝ : Nonempty Z
f : X → Y
g : Z → W
h : IsOpenMap (Prod.map f g)
⊢ IsOpenMap (g ∘ Prod.snd)
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hs : ∀ (a : X), f a ∈ s
⊢ (∀ (s_1 : Set ↑s), IsOpen[instTopologicalSpaceSubtype] s_1 → IsOpen[inst✝¹] (codRestrict f s hs ⁻¹' s_1)) →
    ∀ (s : Set Y), IsOpen[inst✝] s → IsOpen[inst✝¹] (f ⁻¹' s)

Tactic:
intro hf

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hs : ∀ (a : X), f a ∈ s
hf : ∀ (s_1 : Set ↑s), IsOpen[instTopologicalSpaceSubtype] s_1 → IsOpen[inst✝¹] (codRestrict f s hs ⁻¹' s_1)
⊢ ∀ (s : Set Y), IsOpen[inst✝] s → IsOpen[inst✝¹] (f ⁻¹' s)
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Continuous[inst✝¹, inst✝] f
s u s' : Set β
h : u ∈ 𝓝ˢ[s'] s
⊢ f ⁻¹' u ∈ 𝓝ˢ[f ⁻¹' s'] (f ⁻¹' s)

Tactic:
by
  simpa using (hf.continuousOn (s := univ)).preimage_mem_nhdsSetWithin h

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
β : Type u_1
t✝ : TopologicalSpace α
B : Set (Set α)
s✝ : Set α
inst✝² : TopologicalSpace β
inst✝¹ : SeparableSpace α
inst✝ : SeparableSpace β
s : Set α
hsc : s.Countable
hsd : Dense s
t : Set β
htc : t.Countable
htd : Dense t
⊢ range Sum.inl ∪ range Sum.inr = univ

Tactic:
range_inl_union_range_inr

Goal state after:
Module: Mathlib.Order.Filter.Ultrafilter.Defs

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
f✝ g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter γ
m : α → β
n : β → γ
inj₀ : Injective n
large₀ : range n ∈ f
inj₁ : Injective m
large₁ : range m ∈ f.comap inj₀ large₀
inj₂ : optParam (Injective (n ∘ m)) ⋯
⊢ range (n ∘ m) ∈ f

Tactic:
by rw [range_comp]; exact image_mem_of_mem_comap large₀ large₁

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
S : Set β
⊢ (∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i) ↔
    ∃ U F, (∀ i ∈ F, U i ∈ preimage (f i) '' T i) ∧ S = ⋂ i ∈ F, U i

Tactic:
constructor <;> rintro ⟨U, F, hUT, hSU⟩

Goal state after:
case mp
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
S : Set β
U : (i : ι) → Set (X i)
F : Finset ι
hUT : ∀ i ∈ F, U i ∈ T i
hSU : S = ⋂ i ∈ F, f i ⁻¹' U i
⊢ ∃ U F, (∀ i ∈ F, U i ∈ preimage (f i) '' T i) ∧ S = ⋂ i ∈ F, U i

case mpr
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
S : Set β
U : ι → Set β
F : Finset ι
hUT : ∀ i ∈ F, U i ∈ preimage (f i) '' T i
hSU : S = ⋂ i ∈ F, U i
⊢ ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i
Module: Mathlib.Order.Filter.Ultrafilter.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
l₁ : Filter α
l₂ : Filter β
⊢ Tendsto f l₁ l₂ ↔ ∀ (g : Ultrafilter α), ↑g ≤ l₁ → Tendsto f (↑g) l₂

Tactic:
simpa only [tendsto_iff_comap] using le_iff_ultrafilter

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
s : Set α
hf : ∀ x ∈ s, f x ∈ 𝓝[s] x
this : ∀ (x : ↑s), Subtype.val ⁻¹' f ↑x ∈ 𝓝 x
t : Set ↑s
htc : t.Countable
htU : ⋃ x ∈ t, Subtype.val ⁻¹' f ↑x = univ
x : α
hx : x ∈ s
⊢ x ∈ ⋃ x ∈ Subtype.val '' t, f x

Tactic:
simp only [biUnion_image, eq_univ_iff_forall, ← preimage_iUnion, mem_preimage] at htU ⊢

Goal state after:
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
s : Set α
hf : ∀ x ∈ s, f x ∈ 𝓝[s] x
this : ∀ (x : ↑s), Subtype.val ⁻¹' f ↑x ∈ 𝓝 x
t : Set ↑s
htc : t.Countable
x : α
hx : x ∈ s
htU : ∀ (x : ↑s), ↑x ∈ ⋃ i ∈ t, f ↑i
⊢ x ∈ ⋃ y ∈ t, f ↑y
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen[inst✝] s
s' : Set X
hs' : IsOpen[inst✝] s'
ht : IsOpen[instTopologicalSpaceSubtype] (s ↓∩ s')
⊢ IsOpen[inst✝] (s ∩ s')

Tactic:
exact hs.inter hs'

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsClosed[inst✝] s
s' : Set X
hs' : IsClosed[inst✝] s'
ht : IsClosed[instTopologicalSpaceSubtype] (s ↓∩ s')
⊢ IsClosed[inst✝] (s ∩ s')

Tactic:
exact hs.inter hs'

Goal state after:
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: case neg
ι : Type u_1
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure[inst✝¹] (f i), ContinuousWithinAt g (f i) x
x : X
i : ι
hx : x ∉ closure[inst✝¹] (f i)
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))

Tactic:
· rw [mem_closure_iff_nhdsWithin_neBot, not_neBot] at hx
    rw [hx]
    exact tendsto_bot

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyCompactSpace X
s : Set X
hs : IsLocallyClosed s
⊢ IsLocallyClosed (range Subtype.val)

Tactic:
rwa [Subtype.range_val]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝² : TopologicalSpace β
inst✝¹ : SecondCountableTopology α
inst✝ : SecondCountableTopology β
b : Set (Set (α ⊕ β)) := (fun u ↦ Sum.inl '' u) '' countableBasis α ∪ (fun u ↦ Sum.inr '' u) '' countableBasis β
A : IsTopologicalBasis b
⊢ SecondCountableTopology (α ⊕ β)

Tactic:
have B : b.Countable :=
    (Countable.image (countable_countableBasis _) _).union
      (Countable.image (countable_countableBasis _) _)

Goal state after:
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝² : TopologicalSpace β
inst✝¹ : SecondCountableTopology α
inst✝ : SecondCountableTopology β
b : Set (Set (α ⊕ β)) := (fun u ↦ Sum.inl '' u) '' countableBasis α ∪ (fun u ↦ Sum.inr '' u) '' countableBasis β
A : IsTopologicalBasis b
B : b.Countable
⊢ SecondCountableTopology (α ⊕ β)
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
f : X → Set X
hf : ∀ (x : X), f x ∈ 𝓝[univ] x
s : Set X
hsc : s.Countable
hsU : univ ⊆ ⋃ x ∈ s, f x
⊢ ∃ s, s.Countable ∧ ⋃ x ∈ s, f x = univ

Tactic:
exact ⟨s, hsc, univ_subset_iff.1 hsU⟩

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

Goal state before:
pp: case refine_2
X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
s t : Set X✝
K✝ : CompactExhaustion X✝
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : SigmaCompactSpace X
K : ℕ → { s // IsCompact s } := fun n ↦ Nat.recOn n ⟨∅, ⋯⟩ fun n s ↦ ⟨⋯.choose ∪ compactCovering X n, ⋯⟩
⊢ ⋃ n, ↑(K n) = univ

Tactic:
refine univ_subset_iff.1 (iUnion_compactCovering X ▸ ?_)
    exact iUnion_mono' fun n => ⟨n + 1, subset_union_right⟩

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
l : Filter X
hs : IsCompact s
⊢ Disjoint (𝓝ˢ s) l ↔ ∀ x ∈ s, Disjoint (𝓝 x) l

Tactic:
refine ⟨fun h x hx => h.mono_left <| nhds_le_nhdsSet hx, fun H => ?_⟩
  choose! U hxU hUl using fun x hx => (nhds_basis_opens x).disjoint_iff_left.1 (H x hx)
  choose hxU hUo using hxU
  rcases hs.elim_nhds_subcover U fun x hx => (hUo x hx).mem_nhds (hxU x hx) with ⟨t, hts, hst⟩
  refine (hasBasis_nhdsSet _).disjoint_iff_left.2
    ⟨⋃ x ∈ t, U x, ⟨isOpen_biUnion fun x hx => hUo x (hts x hx), hst⟩, ?_⟩
  rw [compl_iUnion₂, biInter_finset_mem]
  exact fun x hx => hUl x (hts x hx)

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : f ≤ 𝓟 s
U : ↑s → Set X
hU : ∀ (x : ↑s), ↑x ∈ U x ∧ IsOpen[inst✝] (U x)
hUf : ∀ (x : ↑s), (U x)ᶜ ∈ f
t : Finset ↑s
ht : s ⊆ ⋃ i ∈ t, U i
⊢ sᶜ ∈ f

Tactic:
refine mem_of_superset ((biInter_finset_mem t).2 fun x _ => hUf x) ?_

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : f ≤ 𝓟 s
U : ↑s → Set X
hU : ∀ (x : ↑s), ↑x ∈ U x ∧ IsOpen[inst✝] (U x)
hUf : ∀ (x : ↑s), (U x)ᶜ ∈ f
t : Finset ↑s
ht : s ⊆ ⋃ i ∈ t, U i
⊢ ⋂ i ∈ t, (U i)ᶜ ⊆ sᶜ
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : NoMinOrder α
s : Set α
h₁ : upperClosure s = ⊥
h₂ : BddBelow s
⊢ False

Tactic:
simpa [h₁] using bddBelow_upperClosure.mpr h₂

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
inst✝ : (i : ι) → TopologicalSpace (A i)
f g : (i : ι) → A i
⊢ f ⤳ g ↔ ∀ (i : ι), f i ⤳ g i

Tactic:
simp only [Specializes, nhds_pi, pi_le_pi]

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₁ x₂ : X
y₁ y₂ : Y
⊢ ((x₁, y₁) ~ᵢ (x₂, y₂)) ↔ (x₁ ~ᵢ x₂) ∧ (y₁ ~ᵢ y₂)

Tactic:
by
  simp only [Inseparable, nhds_prod_eq, Filter.prod_inj]

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

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T0Space X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed[inst✝²] S
hne : S.Nonempty
⊢ ∃ x ∈ S, IsClosed[inst✝²] {x}

Tactic:
by
  obtain ⟨V, Vsub, Vne, Vcls, hV⟩ := hS.exists_minimal_nonempty_closed_subset hne
  rcases minimal_nonempty_closed_eq_singleton Vcls Vne hV with ⟨x, rfl⟩
  exact ⟨x, Vsub (mem_singleton x), Vcls⟩

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s z₁ z₂ : Set X
x✝¹ : IsClosed[inst✝] z₁
x✝ : IsClosed[inst✝] z₂
⊢ ¬s ⊆ z₁ ∧ ¬s ⊆ z₂ → ¬s ⊆ z₁ ∪ z₂ ↔ s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂

Tactic:
← not_or,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s z₁ z₂ : Set X
x✝¹ : IsClosed[inst✝] z₁
x✝ : IsClosed[inst✝] z₂
⊢ ¬(s ⊆ z₁ ∨ s ⊆ z₂) → ¬s ⊆ z₁ ∪ z₂ ↔ s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂