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

Goal state before:
pp: case mpr.refine_4
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective ⇑(ConcreteCategory.hom c.inl)
h₂ : Injective ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (Set.range ⇑(ConcreteCategory.hom c.inl)) (Set.range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : (fun X ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })),
    x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ Set.range ⇑(ConcreteCategory.hom c.inr)
⊢ ∀ {T : Type u} (f : X ⟶ T) (g : Y ⟶ T) (m : c.pt ⟶ T),
    c.inl ≫ m = f →
      c.inr ≫ m = g →
        m =
          ↾fun x ↦
            if h : x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) then
              (ConcreteCategory.hom f) ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inl)) h₁).symm ⟨x, h⟩)
            else (ConcreteCategory.hom g) ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inr)) h₂).symm ⟨x, ⋯⟩)

Tactic:
rintro T _ _ m rfl rfl

Goal state after:
case mpr.refine_4
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective ⇑(ConcreteCategory.hom c.inl)
h₂ : Injective ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (Set.range ⇑(ConcreteCategory.hom c.inl)) (Set.range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : (fun X ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })),
    x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ Set.range ⇑(ConcreteCategory.hom c.inr)
T : Type u
m : c.pt ⟶ T
⊢ m =
    ↾fun x ↦
      if h : x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) then
        (ConcreteCategory.hom (c.inl ≫ m)) ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inl)) h₁).symm ⟨x, h⟩)
      else (ConcreteCategory.hom (c.inr ≫ m)) ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inr)) h₂).symm ⟨x, ⋯⟩)
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: case mpr.refine_4
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective ⇑(ConcreteCategory.hom c.inl)
h₂ : Injective ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (Set.range ⇑(ConcreteCategory.hom c.inl)) (Set.range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : (fun X ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })),
    x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ Set.range ⇑(ConcreteCategory.hom c.inr)
T : Type u
m : c.pt ⟶ T
x : c.pt
⊢ (ConcreteCategory.hom m).toFun x =
    (ConcreteCategory.hom
          (↾fun x ↦
            if h : x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) then
              (ConcreteCategory.hom (c.inl ≫ m)) ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inl)) h₁).symm ⟨x, h⟩)
            else
              (ConcreteCategory.hom (c.inr ≫ m))
                ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inr)) h₂).symm ⟨x, ⋯⟩))).toFun
      x

Tactic:
simp only [TypeCat.Fun.toFun_apply, Functor.const_obj_obj, pair_obj_left, Set.mem_range,
          comp_apply, pair_obj_right, ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk]

Goal state after:
case mpr.refine_4
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective ⇑(ConcreteCategory.hom c.inl)
h₂ : Injective ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (Set.range ⇑(ConcreteCategory.hom c.inl)) (Set.range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : (fun X ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })),
    x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ Set.range ⇑(ConcreteCategory.hom c.inr)
T : Type u
m : c.pt ⟶ T
x : c.pt
⊢ (ConcreteCategory.hom m) x =
    if h : ∃ y, (ConcreteCategory.hom c.inl) y = x then
      (ConcreteCategory.hom m)
        ((ConcreteCategory.hom c.inl) ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inl)) h₁).symm ⟨x, ⋯⟩))
    else
      (ConcreteCategory.hom m)
        ((ConcreteCategory.hom c.inr) ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inr)) h₂).symm ⟨x, ⋯⟩))
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
c : α
inst✝¹ : Add α
inst✝ : MulOneClass β
hl : ∀ f ∈ [], Periodic f c
⊢ Periodic [].prod c

Tactic:
| nil =>

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
x : ↥(supExtensionOfMaxSingleton i f y)
r : R
a : N
ha : a ∈ (extensionOfMax i f).domain
eq1 : ↑x = ↑⟨a, ha⟩ + r • y
eq2 : ↑(fst i x) - a = (r - snd i x) • y
eq3 : (extendIdealTo i f h y) (r - snd i x) = ↑(extensionOfMax i f).toLinearPMap ⟨(r - snd i x) • y, ⋯⟩
⊢ extensionToFun i f h x = ↑(extensionOfMax i f).toLinearPMap ⟨a, ha⟩ + (extendIdealTo i f h y) r

Tactic:
simp only [map_sub, sub_smul, sub_eq_iff_eq_add] at eq3

Goal state after:
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
x : ↥(supExtensionOfMaxSingleton i f y)
r : R
a : N
ha : a ∈ (extensionOfMax i f).domain
eq1 : ↑x = ↑⟨a, ha⟩ + r • y
eq2 : ↑(fst i x) - a = (r - snd i x) • y
eq3 :
  (extendIdealTo i f h y) r =
    ↑(extensionOfMax i f).toLinearPMap ⟨r • y - snd i x • y, ⋯⟩ + (extendIdealTo i f h y) (snd i x)
⊢ extensionToFun i f h x = ↑(extensionOfMax i f).toLinearPMap ⟨a, ha⟩ + (extendIdealTo i f h y) r
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
x : ↥(supExtensionOfMaxSingleton i f y)
r : R
a : N
ha : a ∈ (extensionOfMax i f).domain
eq1 : ↑x = ↑⟨a, ha⟩ + r • y
eq2 : ↑(fst i x) - a = (r - snd i x) • y
eq3 :
  (extendIdealTo i f h y) r =
    ↑(extensionOfMax i f).toLinearPMap ⟨r • y - snd i x • y, ⋯⟩ + (extendIdealTo i f h y) (snd i x)
⊢ ↑(extensionOfMax i f).toLinearPMap (fst i x) + (extendIdealTo i f h y) (snd i x) =
    ↑(extensionOfMax i f).toLinearPMap (⟨a, ha⟩ + ⟨r • y - snd i x • y, ⋯⟩) + (extendIdealTo i f h y) (snd i x)

Tactic:
AddMemClass.mk_add_mk

Goal state after:
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
x : ↥(supExtensionOfMaxSingleton i f y)
r : R
a : N
ha : a ∈ (extensionOfMax i f).domain
eq1 : ↑x = ↑⟨a, ha⟩ + r • y
eq2 : ↑(fst i x) - a = (r - snd i x) • y
eq3 :
  (extendIdealTo i f h y) r =
    ↑(extensionOfMax i f).toLinearPMap ⟨r • y - snd i x • y, ⋯⟩ + (extendIdealTo i f h y) (snd i x)
⊢ ↑(extensionOfMax i f).toLinearPMap (fst i x) + (extendIdealTo i f h y) (snd i x) =
    ↑(extensionOfMax i f).toLinearPMap ⟨a + (r • y - snd i x • y), ⋯⟩ + (extendIdealTo i f h y) (snd i x)
Module: Mathlib.Data.Nat.Periodic

Goal state before:
pp: case e_a.e_f
n✝ a : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
pp : Periodic p a
n : ℕ
⊢ p n = ((fun x ↦ p x) ∘ fun x ↦ x % a) n

Tactic:
exact (pp.map_mod_nat n).symm

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

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
inst✝⁵ : Small.{v, u} R
S : Type u'
inst✝⁴ : Ring S
M : Type v
N : Type v'
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module S N
e₁ : R ≃+* S
e₂ : M ≃ₛₗ[↑e₁] N
inj : Injective R M
I : Ideal S
g : ↥I →ₗ[S] N
I' : Submodule R R := Submodule.map (↑e₁.symm.toSemilinearEquiv) I
e : ↥I' ≃ₛₗ[↑e₁] ↥I := (e₁.symm.toSemilinearEquiv.submoduleMap I).symm
⊢ ∃ g', ∀ (x : S) (mem : x ∈ I), g' x = g ⟨x, mem⟩

Tactic:
let f : I' →ₗ[R] M := e₂.symm.toLinearMap.comp (g.comp e.toLinearMap)

Goal state after:
R : Type u
inst✝⁶ : Ring R
inst✝⁵ : Small.{v, u} R
S : Type u'
inst✝⁴ : Ring S
M : Type v
N : Type v'
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module S N
e₁ : R ≃+* S
e₂ : M ≃ₛₗ[↑e₁] N
inj : Injective R M
I : Ideal S
g : ↥I →ₗ[S] N
I' : Submodule R R := Submodule.map (↑e₁.symm.toSemilinearEquiv) I
e : ↥I' ≃ₛₗ[↑e₁] ↥I := (e₁.symm.toSemilinearEquiv.submoduleMap I).symm
f : ↥I' →ₗ[R] M := ↑e₂.symm ∘ₛₗ g ∘ₛₗ ↑e
⊢ ∃ g', ∀ (x : S) (mem : x ∈ I), g' x = g ⟨x, mem⟩
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: p : ℕ
hp : Prime p
n : ℕ
hn : 0 < n
⊢ φ (p ^ n) = p ^ (n - 1) * (p - 1)

Tactic:
rcases exists_eq_succ_of_ne_zero (pos_iff_ne_zero.1 hn) with ⟨m, rfl⟩
  exact totient_prime_pow_succ hp _

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: β : Type u_4
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ l ≤ N, u l ≤ u k
ex : ∃ n ≥ N, u k < u n
⊢ ∃ n ≥ N, u k < u n ∧ ∀ m < n, N ≤ m → u m ≤ u k

Tactic:
by
    rcases Nat.findX ex with ⟨n, ⟨hnN, hnk⟩, hn_min⟩
    push Not at hn_min
    exact ⟨n, hnN, hnk, hn_min⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Set β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ∩ g t
s t : Set α
⊢ (𝓟 ∘ g) (s ∩ t) = (𝓟 ∘ g) s ⊓ (𝓟 ∘ g) t

Tactic:
by simp only [inf_principal, comp, hg]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
f : ι → Filter α
g : Set α → Set β
hg : ∀ {s t : Set α}, g (s ∩ t) = g s ∩ g t
hg' : g univ = univ
s t : Set α
⊢ (𝓟 ∘ g) (s ∩ t) = (𝓟 ∘ g) s ⊓ (𝓟 ∘ g) t

Tactic:
by simp only [inf_principal, comp, hg]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ Dense {x}ᶜ ↔ ¬IsOpen {x}

Tactic:
by
  constructor
  · intro hd ho
    exact (hd.inter_open_nonempty _ ho (singleton_nonempty _)).ne_empty (inter_compl_self _)
  · refine fun ho => dense_iff_inter_open.2 fun U hU hne => inter_compl_nonempty_iff.2 fun hUx => ?_
    obtain rfl : U = {x} := eq_singleton_iff_nonempty_unique_mem.2 ⟨hne, hUx⟩
    exact ho hU

Goal state after:
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
ι : Sort u_3
p : ι → Prop
s : ι → Set X
F : Filter X
hx : F.HasBasis p s
⊢ ClusterPt x F ↔ ∀ (i : ι), p i → ∃ᶠ (x : X) in 𝓝 x, x ∈ s i

Tactic:
simp only [(𝓝 x).basis_sets.clusterPt_iff hx, Filter.frequently_iff]
  exact ⟨fun h a b c d ↦ h d b, fun h a b c d ↦ h c d b⟩

Goal state after:
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
⊢ Disjoint (𝓝ˢ s) (𝓟 t) ↔ Disjoint s (closure[inst✝] t)

Tactic:
rw [disjoint_comm, disjoint_principal_nhdsSet, disjoint_comm]

Goal state after:
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: α : Type u_4
inst✝ : TopologicalSpace α
s : Set α
⊢ ¬(𝓝ˢ s).NeBot ↔ ¬s.Nonempty

Tactic:
simp [not_nonempty_iff_eq_empty]

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

Goal state before:
pp: α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
p : α
hp : 0 < p
a : α
⊢ ⋃ n, Icc (a + n • p) (a + (n + 1) • p) = univ

Tactic:
by
  simpa only [iUnion_Ioc_add_zsmul hp a, univ_subset_iff] using
    iUnion_mono fun n : ℤ => (Ioc_subset_Icc_self : Ioc (a + n • p) (a + (n + 1) • p) ⊆ Icc _ _)

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
h : ∀ (x : X), ∃ g, ContinuousAt g (f x) ∧ g (f x) = x ∧ RightInverse g f
x : X
g : Y → X
hgc : ContinuousAt g (f x)
hgx : g (f x) = x
hgf : RightInverse g f
⊢ 𝓝 (f x) = map f (map g (𝓝 (f x)))

Tactic:
rw [map_map, hgf.comp_eq_id, map_id]

Goal state after:
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 ∈ comap Subtype.val (𝓝 ↑a ⊓ 𝓟 (Subtype.val '' u)) ↔ 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 ∈ comap Subtype.val (𝓝[Subtype.val '' u] ↑a) ↔ t ∈ comap Subtype.val (𝓝[Subtype.val '' u] ↑a)
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
t : Set β
hf : ContinuousOn f s
hs : IsClosed[inst✝¹] s
ht : IsClosed[inst✝] t
⊢ IsClosed[inst✝¹] (s ∩ f ⁻¹' t)

Tactic:
rcases continuousOn_iff_isClosed.1 hf t ht with ⟨u, hu⟩
  rw [inter_comm, hu.2]
  apply IsClosed.inter hu.1 hs

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
x : α
⊢ ContinuousWithinAt f (s ∪ t) x ↔ ContinuousWithinAt f s x ∧ ContinuousWithinAt f t x

Tactic:
by
  simp only [ContinuousWithinAt, nhdsWithin_union, tendsto_sup]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
p : X → Prop
x : X
hx : p x
h : ∀ᶠ (x : X) in 𝓝 x, p x
⊢ range Subtype.val ∈ 𝓝 ↑⟨x, hx⟩

Tactic:
rw [Subtype.range_val]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
p : X → Prop
x : X
hx : p x
h : ∀ᶠ (x : X) in 𝓝 x, p x
⊢ p ∈ 𝓝 ↑⟨x, hx⟩
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
s : Set (Set α)
h_nhds : ∀ (a : α), (𝓝 a).HasBasis (fun t ↦ t ∈ s ∧ a ∈ t) id
x : α
⊢ 𝓝 x = 𝓝 x

Tactic:
simpa only [nhds_generateFrom, and_comm] using! (h_nhds x).eq_biInf

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case ne
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
⊢ {s | a ∈ s ∧ s ∈ b}.Nonempty

Tactic:
rcases eq_univ_iff_forall.1 hb.sUnion_eq a with ⟨i, h1, h2⟩
    exact ⟨i, h2, h1⟩

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : Dense s
u : Set ↑s
hud : Dense u
v : Set X
hv1 : IsOpen[inst✝] v
hv2 : Subtype.val ⁻¹' v = u
⊢ Dense v

Tactic:
dense_iff_inter_open

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : ∀ (U : Set X), IsOpen[inst✝] U → U.Nonempty → (U ∩ s).Nonempty
u : Set ↑s
hud : ∀ (U : Set ↑s), IsOpen[instTopologicalSpaceSubtype] U → U.Nonempty → (U ∩ u).Nonempty
v : Set X
hv1 : IsOpen[inst✝] v
hv2 : Subtype.val ⁻¹' v = u
⊢ ∀ (U : Set X), IsOpen[inst✝] U → U.Nonempty → (U ∩ v).Nonempty
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
I : Set ι
s : (i : ι) → Set (A i)
a : (i : ι) → A i
hs : I.pi s ∈ 𝓝 a
i : ι
hi : i ∈ I
⊢ s i ∈ 𝓝 (a i)

Tactic:
rw [nhds_pi] at hs; exact mem_of_pi_mem_pi hs hi

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case refine_2
ι : Type u_5
A : ι → Type u_9
g : (a : ι) → Set (Set (A a))
i : ι
s : Set (A i)
hs : s ∈ g i
⊢ IsOpen[coinduced (fun f ↦ f i) (generateFrom {t | ∃ s i, (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i).pi s})] s

Tactic:
refine GenerateOpen.basic _ ⟨update (fun i => univ) i s, {i}, ?_⟩

Goal state after:
case refine_2
ι : Type u_5
A : ι → Type u_9
g : (a : ι) → Set (Set (A a))
i : ι
s : Set (A i)
hs : s ∈ g i
⊢ (∀ a ∈ {i}, update (fun i ↦ univ) i s a ∈ g a) ∧ (fun f ↦ f i) ⁻¹' s = (↑{i}).pi (update (fun i ↦ univ) i s)
Module: Mathlib.Topology.Ultrafilter

Goal state before:
pp: X : Type u
x : X
inst✝ : TopologicalSpace X
f : Filter X
⊢ (𝓝 x ⊓ f).NeBot ↔ ∃ u, ↑u ≤ f ⊓ 𝓝 x

Tactic:
exists_ultrafilter_iff,

Goal state after:
X : Type u
x : X
inst✝ : TopologicalSpace X
f : Filter X
⊢ (𝓝 x ⊓ f).NeBot ↔ (f ⊓ 𝓝 x).NeBot
Module: Mathlib.Topology.Ultrafilter

Goal state before:
pp: X : Type u
α : Type u_1
x : X
inst✝ : TopologicalSpace X
F : Filter α
u : α → X
⊢ (comap u (𝓝 x) ⊓ F).NeBot ↔ ∃ U, ↑U ≤ F ⊓ comap u (𝓝 x)

Tactic:
exists_ultrafilter_iff,

Goal state after:
X : Type u
α : Type u_1
x : X
inst✝ : TopologicalSpace X
F : Filter α
u : α → X
⊢ (comap u (𝓝 x) ⊓ F).NeBot ↔ (F ⊓ comap u (𝓝 x)).NeBot
Module: Mathlib.Order.Filter.SmallSets

Goal state before:
pp: α : Type u_1
L : Filter (Set α)
l : Filter α
⊢ (fun L ↦ L.bind 𝓟) L ≤ l ↔ L ≤ l.smallSets

Tactic:
simp_rw [smallSets_eq_generate, le_generate_iff, image_subset_iff]

Goal state after:
α : Type u_1
L : Filter (Set α)
l : Filter α
⊢ L.bind 𝓟 ≤ l ↔ l.sets ⊆ powerset ⁻¹' L.sets
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
a : X
U : Set X
haU : U ∈ 𝓝 a
hfin : {i | (f i ∩ U).Nonempty}.Finite
⊢ 𝓝[⋃ i, f i] a ≤ ⨆ i, 𝓝[f i] a

Tactic:
calc
    𝓝[⋃ i, f i] a = 𝓝[⋃ i, f i ∩ U] a := by
      rw [← iUnion_inter, ← nhdsWithin_inter_of_mem' (nhdsWithin_le_nhds haU)]
    _ = 𝓝[⋃ i ∈ {j | (f j ∩ U).Nonempty}, (f i ∩ U)] a := by
      simp only [mem_ofPred_eq, iUnion_nonempty_self]
    _ = ⨆ i ∈ {j | (f j ∩ U).Nonempty}, 𝓝[f i ∩ U] a := nhdsWithin_biUnion hfin _ _
    _ ≤ ⨆ i, 𝓝[f i ∩ U] a := iSup₂_le_iSup _ _
    _ ≤ ⨆ i, 𝓝[f i] a := iSup_mono fun i ↦ nhdsWithin_mono _ inter_subset_left

Goal state after:
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ upperClosure s = ⊤ ↔ s = ∅

Tactic:
by
  rw [eq_top_iff, le_upperClosure]; simp

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case mp
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
h : ∀ t ⊆ S, ∃ u, IsOpen[inst✝] u ∧ u ∩ S = t
s : Set X
sS : s ⊆ S
⊢ ∃ U, IsClosed[inst✝] U ∧ U ∩ S = s

Tactic:
obtain ⟨U, Uo, Us⟩ := h (sᶜ ∩ S) inter_subset_right

Goal state after:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
h : ∀ t ⊆ S, ∃ u, IsOpen[inst✝] u ∧ u ∩ S = t
s : Set X
sS : s ⊆ S
U : Set X
Uo : IsOpen[inst✝] U
Us : U ∩ S = sᶜ ∩ S
⊢ ∃ U, IsClosed[inst✝] U ∧ U ∩ S = s
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case mpr
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
h : ∀ s ⊆ S, ∃ U, IsClosed[inst✝] U ∧ U ∩ S = s
s : Set X
sS : s ⊆ S
⊢ ∃ u, IsOpen[inst✝] u ∧ u ∩ S = s

Tactic:
obtain ⟨U, Uo, Us⟩ := h (sᶜ ∩ S) inter_subset_right

Goal state after:
case mpr
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
h : ∀ s ⊆ S, ∃ U, IsClosed[inst✝] U ∧ U ∩ S = s
s : Set X
sS : s ⊆ S
U : Set X
Uo : IsClosed[inst✝] U
Us : U ∩ S = sᶜ ∩ S
⊢ ∃ u, IsOpen[inst✝] u ∧ u ∩ S = s
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hs : IsDiscrete s
hf : ContinuousOn f (f ⁻¹' s)
hf' : Injective f
x : X
hx : x ∈ f ⁻¹' s
⊢ map f (𝓝[f ⁻¹' s] x) ≤ pure (f x)

Tactic:
← hs.nhdsWithin _ hx,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hs : IsDiscrete s
hf : ContinuousOn f (f ⁻¹' s)
hf' : Injective f
x : X
hx : x ∈ f ⁻¹' s
⊢ map f (𝓝[f ⁻¹' s] x) ≤ 𝓝[s] f x
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hs : IsDiscrete s
hf : ContinuousOn f (f ⁻¹' s)
H : ∀ (x : Y), IsDiscrete (f ⁻¹' {x})
x : X
hx : x ∈ f ⁻¹' s
h : 𝓝 x ⊓ comap f (pure (f x)) ≤ pure x
⊢ 𝓝[f ⁻¹' s] x ≤ pure x

Tactic:
← hs.nhdsWithin _ hx,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hs : IsDiscrete s
hf : ContinuousOn f (f ⁻¹' s)
H : ∀ (x : Y), IsDiscrete (f ⁻¹' {x})
x : X
hx : x ∈ f ⁻¹' s
h : 𝓝 x ⊓ comap f (𝓝[s] f x) ≤ pure x
⊢ 𝓝[f ⁻¹' s] x ≤ pure x
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
p : X → Prop
a : X
ha : a ∈ {x | ∀ᶠ (y : X) in 𝓝[≠] x, p y}
⊢ {x | ∀ᶠ (y : X) in 𝓝[≠] x, p y} ∈ 𝓝 a

Tactic:
filter_upwards [eventually_nhds_nhdsWithin.mpr ha] with b hb

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
p : X → Prop
a : X
ha : a ∈ {x | ∀ᶠ (y : X) in 𝓝[≠] x, p y}
b : X
hb : ∀ᶠ (x : X) in 𝓝[{a}ᶜ] b, p x
⊢ ∀ᶠ (y : X) in 𝓝[≠] b, p y
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
x : X
t : Set X
H1 : IsCompact t
H2 : x ∉ t
⊢ ∃ U V, IsOpen[inst✝¹] U ∧ IsOpen[inst✝¹] V ∧ t ⊆ U ∧ x ∈ V ∧ Disjoint U V

Tactic:
by
  simpa [SeparatedNhds] using SeparatedNhds.of_isCompact_isCompact_isClosed H1 isCompact_singleton
    isClosed_singleton <| disjoint_singleton_right.mpr H2

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

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : T1Space X
inst✝¹ : DecidableEq X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
x : X
y : Y
H : ContinuousOn f (s \ {x})
z : X
hzx : z ≠ x
hzs : z ∈ s
⊢ (fun a ↦ a ∈ {x} → False) ∈ 𝓝 z

Tactic:
exact isOpen_ne.mem_nhds hzx

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

Goal state before:
pp: case mpr
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
a : X
p : X → Prop
hs : IsOpen[inst✝] s
h : ∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝[s] y, p x
⊢ ∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝 y, p x

Tactic:
filter_upwards [h, eventually_nhdsWithin_of_forall fun _ a ↦ a] with _ _ _

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
a : X
p : X → Prop
hs : IsOpen[inst✝] s
h : ∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝[s] y, p x
a✝² : X
a✝¹ : ∀ᶠ (x : X) in 𝓝[s] a✝², p x
a✝ : a✝² ∈ s
⊢ ∀ᶠ (x : X) in 𝓝 a✝², p x
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case a
X : Type u_1
inst✝ : TopologicalSpace X
p : X
s : Set X
hs : Disjoint (𝓝[s] p) cofinite
⊢ 𝓝[s] p ≤ 𝓟 ({x | x ⤳ p} ∩ s)

Tactic:
simpa using ⟨hs.eventually_nhdsWithin_specializes, self_mem_nhdsWithin⟩

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

Goal state before:
pp: case refine_2.mk.mk
X : Type u_1
inst✝ : TopologicalSpace X
h : Std.Symm Specializes
x✝ : SeparationQuotient X
x : X
y✝ : SeparationQuotient X
y : X
sxspecsy : Quot.mk (⇑(inseparableSetoid X)) x ⤳ Quot.mk (⇑(inseparableSetoid X)) y
xspecy : x ⤳ y
yspecx : y ⤳ x
⊢ x ⤳ y ∧ y ⤳ x

Tactic:
exact ⟨xspecy, yspecx⟩

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen[inst✝¹] U
hV : IsOpen[inst✝¹] V
h2K : K ⊆ U ∪ V
⊢ ∃ K₁ K₂, IsCompact K₁ ∧ IsCompact K₂ ∧ K₁ ⊆ U ∧ K₂ ⊆ V ∧ K = K₁ ∪ K₂

Tactic:
have hK' : IsCompact (closure K) := hK.closure

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen[inst✝¹] U
hV : IsOpen[inst✝¹] V
h2K : K ⊆ U ∪ V
hK' : IsCompact (closure[inst✝¹] K)
⊢ ∃ K₁ K₂, IsCompact K₁ ∧ IsCompact K₂ ∧ K₁ ⊆ U ∧ K₂ ⊆ V ∧ K = K₁ ∪ K₂
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: case mp.sInter
α : Type u_2
g : Set (Set α)
s✝ : Set α
S : Set (Set α)
Sct : S.Countable
a✝ : ∀ s ∈ S, CountableGenerateSets g s
T : (s : Set α) → s ∈ S → Set (Set α)
Tg : ∀ (s : Set α) (a : s ∈ S), T s a ⊆ g
Tct : ∀ (s : Set α) (a : s ∈ S), (T s a).Countable
hT : ∀ (s : Set α) (a : s ∈ S), ⋂₀ T s a ⊆ s
s : Set α
H : s ∈ S
⊢ ⋂₀ ⋃ s, ⋃ (H : s ∈ S), T s H ⊆ s

Tactic:
exact subset_trans (sInter_subset_sInter (subset_iUnion₂ s H)) (hT s H)

Goal state after: