mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v, u'} D
inst✝³ : HasLimits D
inst✝² : WellPowered.{v, v, u'} D
P : ObjectProperty D
inst✝¹ : ObjectProperty.Small.{v, v, u'} P
hP : P.IsCoseparating
G : D ⥤ C
inst✝ : PreservesLimits G
⊢ G.IsRightAdjoint

Tactic:
have : ∀ A, HasInitial (StructuredArrow A G) := fun A ↦
    hasInitial_of_isCoseparating.{v} (StructuredArrow.isCoseparating_inverseImage_proj A G hP)
  exact isRightAdjointOfStructuredArrowInitials _

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
⊢ IsCoseparator (op G) ↔ IsSeparator G

Tactic:
by
  rw [IsSeparator, IsCoseparator, ← isCoseparating_op_iff, op_singleton]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
n : ℤ
x : α
⊢ f (x + (2 * n + 1) • c) = -f x

Tactic:
add_zsmul,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
n : ℤ
x : α
⊢ f (x + ((2 * n) • c + 1 • c)) = -f x
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: n : ℕ
⊢ φ n = Nat.card ↑{m | m < n ∧ n.Coprime m}

Tactic:
let e : { m | m < n ∧ n.Coprime m } ≃ {x ∈ range n | n.Coprime x} :=
    { toFun := fun m => ⟨m, by simpa only [Finset.mem_filter, Finset.mem_range] using! m.property⟩
      invFun := fun m => ⟨m, by simpa only [Finset.mem_filter, Finset.mem_range] using! m.property⟩
      left_inv := fun m => by simp only [Subtype.coe_eta]
      right_inv := fun m => by simp only }
  rw [totient_eq_card_coprime, card_congr e, card_eq_fintype_card, Fintype.card_coe]

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
⊢ ∃ n ≥ N, ∀ k < n, u k < u n

Tactic:
have ex : ∃ n ≥ N, u k < u n := exists_lt_of_tendsto_atTop hu _ _

Goal state after:
β : 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, ∀ k < n, u k < u n
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
T : Set (Set X)
empty_mem : ∅ ∈ T
sInter_mem : ∀ A ⊆ T, ⋂₀ A ∈ T
union_mem : ∀ A ∈ T, ∀ B ∈ T, A ∪ B ∈ T
s : Set (Set X)
hs : ∀ t ∈ s, tᶜ ∈ T
⊢ ⋂₀ (compl '' s) ∈ T

Tactic:
exact sInter_mem (compl '' s) fun z ⟨y, hy, hz⟩ => hz ▸ hs y hy

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 : α
⊢ toIocDiv hp a (-b) = -(toIcoDiv hp (-a) b + 1)

Tactic:
← neg_neg b,

Goal state after:
α : 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) + 1)
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 : ℤ
⊢ toIocMod hp a (b - m • p) = toIocMod hp a b

Tactic:
by
  rw [sub_eq_add_neg, ← neg_smul, toIocMod_add_zsmul]

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 : α
n : ℤ
⊢ toIcoMod hp a a = a

Tactic:
toIcoMod_apply_left

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
n : ℤ
⊢ a = a
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case refine_1
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ (∃ z, b = a + z • p) → toIocMod hp a b = a + p

Tactic:
rintro ⟨z, rfl⟩

Goal state after:
case refine_1
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
z : ℤ
⊢ toIocMod hp a (a + z • p) = a + p
Module: Mathlib.Algebra.Order.ToIntervalMod

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

Tactic:
add_one_zsmul,

Goal state after:
case refine_2
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
h : toIocMod hp a b = a + p
⊢ b = a + (toIocDiv hp a b • p + p)
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
f : Filter X
⊢ f ≤ 𝓝 x ↔ ∀ (s : Set X), x ∈ s → IsOpen[inst✝] s → s ∈ f

Tactic:
simp [nhds_def]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : IsClosed s
A : frontier s = s \ interior s
B : interior (frontier s) ⊆ interior s
C : interior (frontier s) ⊆ frontier s
this : interior (frontier s) ⊆ interior s ∩ (s \ interior s)
⊢ interior (frontier s) = ∅

Tactic:
rwa [inter_sdiff_self, subset_empty_iff] at this

Goal state after:
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
h : IsClosed[inst✝] t
⊢ 𝓝ˢ s ≤ 𝓝ˢ (t ∩ s) ⊔ 𝓟 tᶜ

Tactic:
rw [Set.inter_comm]

Goal state after:
X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
h : IsClosed[inst✝] t
⊢ 𝓝ˢ s ≤ 𝓝ˢ (s ∩ t) ⊔ 𝓟 tᶜ
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 Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Z
hg : IsInducing g
hf : IsInducing f
⊢ inst✝¹ = induced (g ∘ f) inst✝

Tactic:
rw [hf.eq_induced, hg.eq_induced, induced_compose]

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:
refine ⟨?_, fun hf => h.isOpenMap.comp 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
⊢ IsOpenMap (⇑h ∘ f) → IsOpenMap f
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
inst✝ : TopologicalSpace β
f : α → β
a : α
l : Filter α
⊢ Continuous[nhdsAdjoint a l, inst✝] f ↔ Tendsto f l (𝓝 (f a))

Tactic:
continuous_iff_le_induced,

Goal state after:
α : Type u
β : Type v
inst✝ : TopologicalSpace β
f : α → β
a : α
l : Filter α
⊢ nhdsAdjoint a l ≤ induced f inst✝ ↔ Tendsto f l (𝓝 (f a))
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 : IsOpenEmbedding f
x : X
l : Filter Y
⊢ AccPt x (comap f l) ↔ AccPt (f x) l

Tactic:
rw [accPt_iff_clusterPt, accPt_iff_clusterPt, ← hf.injective.preimage_image {x}, image_singleton,
    ← preimage_compl, ← comap_principal, ← comap_inf,
    hf.isOpenMap.clusterPt_comap_iff hf.continuous]

Goal state after:
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
hg : IsEmbedding g
hgf : IsClosedEmbedding (g ∘ f)
⊢ range f = g ⁻¹' g '' range f

Tactic:
hg.injective.preimage_image

Goal state after:
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
hg : IsEmbedding g
hgf : IsClosedEmbedding (g ∘ f)
⊢ range f = range f
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'ᶜ ∈ 𝓝 x ⊓ 𝓟 t ⊓ 𝓟 t'ᶜ

Tactic:
exact inter_mem_inf hs (mem_principal_self _)

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t u : Set α
h₀ : a ∈ s
h₁ : IsOpen[inst✝] s
h₂ : t ∩ s = u ∩ s
⊢ 𝓝[t] a = 𝓝[u] a

Tactic:
by
  rw [nhdsWithin_restrict t h₀ h₁, nhdsWithin_restrict u h₀ h₁, h₂]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: ι : Type u_5
X : ι → Type u_6
inst✝ : (i : ι) → TopologicalSpace (X i)
I : Set ι
s : (i : ι) → Set (X i)
x : (i : ι) → X i
⊢ (𝓝[I.pi s] x).NeBot ↔ ∀ i ∈ I, (𝓝[s i] x i).NeBot

Tactic:
simp [neBot_iff, nhdsWithin_pi_eq_bot]

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : ∀ x ∈ s, ∃ t, IsOpen[inst✝¹] t ∧ x ∈ t ∧ ContinuousOn f (s ∩ t)
⊢ ContinuousOn f s

Tactic:
by
  intro x xs
  rcases h x xs with ⟨t, open_t, xt, ct⟩
  have := ct x ⟨xs, xt⟩
  rwa [ContinuousWithinAt, ← nhdsWithin_restrict _ xt open_t] at this

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝¹ : SeparableSpace α
inst✝ : Nonempty α
⊢ ∃ u, DenseRange u

Tactic:
obtain ⟨s : Set α, hs, s_dense⟩ := exists_countable_dense α
  obtain ⟨u, hu⟩ := Set.countable_iff_exists_subset_range.mp hs
  exact ⟨u, s_dense.mono hu⟩

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 γ
f : α → β
g : β → γ
h : IsQuotientMap f
s : Set β
hs : IsOpen[inst✝¹] s
⊢ ContinuousOn g s ↔ ContinuousOn (g ∘ f) (f ⁻¹' s)

Tactic:
simp only [continuousOn_iff_continuous_domRestrict, (h.restrictPreimage_isOpen hs).continuous_iff]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : β → γ
h : IsQuotientMap f
s : Set β
hs : IsOpen[inst✝¹] s
⊢ Continuous[instTopologicalSpaceSubtype, inst✝] (s.domRestrict g ∘ s.restrictPreimage f) ↔
    Continuous[instTopologicalSpaceSubtype, inst✝] ((f ⁻¹' s).domRestrict (g ∘ f))
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst✝ : DecidableEq ι
s : Set ((a : ι) → A a)
x : (a : ι) → A a
hs : s ∈ 𝓝 x
y : (a : ι) → A a
⊢ ∃ I, I.piecewise x y ∈ s

Tactic:
by
  simp only [nhds_pi, Filter.mem_pi'] at hs
  rcases hs with ⟨I, t, htx, hts⟩
  refine ⟨I, hts fun i hi => ?_⟩
  simpa [Finset.mem_coe.1 hi] using mem_of_mem_nhds (htx i)

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case refine_2
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : TopologicalSpace X
f : Sigma σ → X
x✝¹ : (∀ (i : ι), IsInducing (f ∘ Sigma.mk i)) ∧ ∀ (i : ι), ∃ U, IsOpen[inst✝] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
h₁ : ∀ (i : ι), IsInducing (f ∘ Sigma.mk i)
h₂ : ∀ (i : ι), ∃ U, IsOpen[inst✝] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
x✝ : Sigma σ
i : ι
x : σ i
U : Set X
hUo : IsOpen[inst✝] U
hU : ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
⊢ range (Sigma.mk i) ∈ comap f (𝓝 (f ⟨i, x⟩))

Tactic:
filter_upwards [preimage_mem_comap <| hUo.mem_nhds <| (hU _).2 rfl] with y hy

Goal state after:
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : TopologicalSpace X
f : Sigma σ → X
x✝¹ : (∀ (i : ι), IsInducing (f ∘ Sigma.mk i)) ∧ ∀ (i : ι), ∃ U, IsOpen[inst✝] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
h₁ : ∀ (i : ι), IsInducing (f ∘ Sigma.mk i)
h₂ : ∀ (i : ι), ∃ U, IsOpen[inst✝] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
x✝ : Sigma σ
i : ι
x : σ i
U : Set X
hUo : IsOpen[inst✝] U
hU : ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
y : Sigma σ
hy : y ∈ f ⁻¹' U
⊢ y ∈ range (Sigma.mk i)
Module: Mathlib.Topology.Bases

Goal state before:
pp: case h_nhds
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
s : Set α → Set (Set α)
hst : ∀ u ∈ countableBasis α, s u ⊆ t
s_count : ∀ u ∈ countableBasis α, (s u).Countable
hs : ∀ u ∈ countableBasis α, u = ⋃ a ∈ s u, a
x : α
v : Set α
hx : x ∈ v
hv : IsOpen[t✝] v
u : Set α
u_mem : u ∈ countableBasis α
xu : x ∈ u
uv : u ⊆ v
this : x ∈ ⋃ a ∈ s u, a
w : Set α
ws : w ∈ s u
xw : x ∈ w
⊢ w ⊆ v

Tactic:
apply Subset.trans (Subset.trans _ (hs u u_mem).symm.subset) uv

Goal state after:
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
s : Set α → Set (Set α)
hst : ∀ u ∈ countableBasis α, s u ⊆ t
s_count : ∀ u ∈ countableBasis α, (s u).Countable
hs : ∀ u ∈ countableBasis α, u = ⋃ a ∈ s u, a
x : α
v : Set α
hx : x ∈ v
hv : IsOpen[t✝] v
u : Set α
u_mem : u ∈ countableBasis α
xu : x ∈ u
uv : u ⊆ v
this : x ∈ ⋃ a ∈ s u, a
w : Set α
ws : w ∈ s u
xw : x ∈ w
⊢ w ⊆ ⋃ a ∈ s u, a
Module: Mathlib.Order.Filter.SmallSets

Goal state before:
pp: α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
f : α → β
⊢ Tendsto (fun x ↦ f '' x) la.smallSets lb.smallSets ↔ Tendsto f la lb

Tactic:
rw [tendsto_smallSets_iff]
  refine forall₂_congr fun u hu ↦ ?_
  rw [eventually_smallSets' fun s t hst ht ↦ (image_mono hst).trans ht]
  simp only [image_subset_iff, exists_mem_subset_iff, mem_map]

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
⊢ ∃ t, ⋃ x ∈ t, U ↑x ⋯ ∈ 𝓝ˢ s

Tactic:
by
  rcases hs.elim_finite_subcover (fun x : s ↦ interior (U x x.2)) (fun _ ↦ isOpen_interior)
    fun x hx ↦ mem_iUnion.2 ⟨⟨x, hx⟩, mem_interior_iff_mem_nhds.2 <| hU _ _⟩ with ⟨t, hst⟩
  refine ⟨t, mem_nhdsSet_iff_forall.2 fun x hx ↦ ?_⟩
  rcases mem_iUnion₂.1 (hst hx) with ⟨y, hyt, hy⟩
  refine mem_of_superset ?_ (subset_biUnion_of_mem hyt)
  exact mem_interior_iff_mem_nhds.1 hy

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
S : Set (Set X)
hf : S.Finite
hc : ∀ s ∈ S, IsCompact s
⊢ IsCompact (⋃₀ S)

Tactic:
rw [sUnion_eq_biUnion]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
S : Set (Set X)
hf : S.Finite
hc : ∀ s ∈ S, IsCompact s
⊢ IsCompact (⋃ i ∈ S, i)
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α ≃o β
⊢ upperClosure (⇑f '' s) = (UpperSet.map f) (upperClosure s)

Tactic:
rw [← f.symm_symm, ← UpperSet.symm_map, f.symm_symm]
  ext
  simp only [SetLike.mem_coe]
  simp [f.le_symm_apply]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : LE α
f : ι → UpperSet α
⊢ ↑(⨆ i, f i).compl = ↑(⨆ i, (f i).compl)

Tactic:
by simp only [coe_compl, coe_iSup, compl_iInter, LowerSet.coe_iSup]

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ ¬x ⤳ y ↔ ∃ S, IsClosed[inst✝] S ∧ x ∈ S ∧ y ∉ S

Tactic:
rw [specializes_iff_forall_closed]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ (¬∀ (s : Set X), IsClosed[inst✝] s → x ∈ s → y ∈ s) ↔ ∃ S, IsClosed[inst✝] S ∧ x ∈ S ∧ y ∉ S
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
p : Prop
inst✝ : Decidable p
hf : p → Continuous[inst✝², inst✝¹] f
hg : ¬p → Continuous[inst✝², inst✝¹] g
⊢ Continuous[inst✝², inst✝¹] fun a ↦ if p then f a else g a

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
p : Prop
inst✝ : Decidable p
hf : p → Continuous[inst✝², inst✝¹] f
hg : ¬p → Continuous[inst✝², inst✝¹] g
h : p
⊢ Continuous[inst✝², inst✝¹] fun a ↦ f a

case neg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
p : Prop
inst✝ : Decidable p
hf : p → Continuous[inst✝², inst✝¹] f
hg : ¬p → Continuous[inst✝², inst✝¹] g
h : ¬p
⊢ Continuous[inst✝², inst✝¹] fun a ↦ g a
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_3
inst✝ : TopologicalSpace X
⊢ irreducibleComponents X = {s | Maximal (fun x ↦ IsClosed[inst✝] x ∧ IsIrreducible x) s}

Tactic:
by
  ext s
  constructor
  · intro H
    exact ⟨⟨isClosed_of_mem_irreducibleComponents _ H, H.1⟩, fun x h e => H.2 h.2 e⟩
  · intro H
    refine ⟨H.1.2, fun x h e => ?_⟩
    have : closure x ≤ s := H.2 ⟨isClosed_closure, h.closure⟩ (e.trans subset_closure)
    exact le_trans subset_closure this

Goal state after:
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
⊢ IsDiscrete (f ⁻¹' s)

Tactic:
by
  refine .of_nhdsWithin fun x hx ↦ ?_
  rw [← map_le_map_iff hf', map_pure, ← hs.nhdsWithin _ hx, ← Tendsto]
  exact (hf.continuousWithinAt hx).tendsto_nhdsWithin (Set.mapsTo_preimage _ _)

Goal state after:
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
inst✝¹ : T1Space X
inst✝ : WeaklyLocallyCompactSpace Y
hf' : Continuous[inst✝³, inst✝²] f
hf : Tendsto f cofinite (cocompact Y)
x : X
K : Set Y
hK : IsCompact K
hK' : K ∈ 𝓝 (f x)
U : Set Y
hU₁ : U ⊆ K
hU₂ : IsOpen[inst✝²] U
hU₃ : f x ∈ U
⊢ IsOpen[inst✝³] {x}

Tactic:
have hU₄ : Set.Finite (f ⁻¹' U) :=
    Finite.subset (tendsto_cofinite_cocompact_iff.mp hf K hK) (preimage_mono hU₁)

Goal state after:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : X → Y
inst✝¹ : T1Space X
inst✝ : WeaklyLocallyCompactSpace Y
hf' : Continuous[inst✝³, inst✝²] f
hf : Tendsto f cofinite (cocompact Y)
x : X
K : Set Y
hK : IsCompact K
hK' : K ∈ 𝓝 (f x)
U : Set Y
hU₁ : U ⊆ K
hU₂ : IsOpen[inst✝²] U
hU₃ : f x ∈ U
hU₄ : (f ⁻¹' U).Finite
⊢ IsOpen[inst✝³] {x}
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
x✝ : x ≠ y
⊢ (fun x y ↦ ∃ u v, IsOpen[inst✝] u ∧ IsOpen[inst✝] v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) x y ↔
    (fun x y ↦ Disjoint (𝓝 x) (𝓝 y)) x y

Tactic:
simp only [(nhds_basis_opens x).disjoint_iff (nhds_basis_opens y), ← exists_and_left,
    and_assoc, and_comm, and_left_comm]

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ T2Space X ↔ Pairwise fun x y ↦ Disjoint (𝓝 x) (𝓝 y)

Tactic:
refine (t2Space_iff X).trans (forall₃_congr fun x y _ => ?_)
  simp only [(nhds_basis_opens x).disjoint_iff (nhds_basis_opens y), ← exists_and_left,
    and_assoc, and_comm, and_left_comm]

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
⊢ ⋃₀ (irreducibleComponents X \ {Z}) ∪ Z = univ

Tactic:
← Set.sUnion_singleton Z,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
⊢ ⋃₀ (irreducibleComponents X \ {⋃₀ {Z}}) ∪ ⋃₀ {Z} = univ
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
t : Set X
ht : t ∈ irreducibleComponents X
f : Y → X
hf : IsOpenEmbedding f
h : (t ∩ range f).Nonempty
⊢ f ⁻¹' t ∈ irreducibleComponents Y

Tactic:
by
  refine preimage_mem_irreducibleComponents_of_isPreirreducible_fiber ht hf.continuous hf.isOpenMap
    (fun _ ↦ (subsingleton_singleton.preimage hf.injective).isPreirreducible) h

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

Goal state before:
pp: case inr
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
ι : Type u_4
X : ι → Type u_3
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (a : ι), T2Space (X a)
i : ι
x : X i
j : ι
y : X j
ne : ⟨i, x⟩ ≠ ⟨j, y⟩
h : i ≠ j
⊢ ∃ u v,
    IsOpen[instTopologicalSpaceSigma] u ∧ IsOpen[instTopologicalSpaceSigma] v ∧ ⟨i, x⟩ ∈ u ∧ ⟨j, y⟩ ∈ v ∧ Disjoint u v

Tactic:
· let _ := (⊥ : TopologicalSpace ι); have : DiscreteTopology ι := ⟨rfl⟩
    exact separated_by_continuous (continuous_def.2 fun u _ => isOpen_sigma_fst_preimage u) h

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
hs : s.Finite
ht : t.Finite
h : Disjoint s t
⊢ SeparatedNhds s t

Tactic:
by
  rw [← hs.coe_toFinset, ← ht.coe_toFinset]
  exact SeparatedNhds.of_finset_finset _ _ (Finite.disjoint_toFinset.2 h)

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

Goal state before:
pp: case mp
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
inst✝ : (𝓝[≠] x).NeBot
hfg : f =ᶠ[𝓝[≠] x] g
⊢ f =ᶠ[𝓝 x] g

Tactic:
apply eventuallyEq_nhds_of_eventuallyEq_nhdsNE hfg
    by_contra hCon
    obtain ⟨a, ha⟩ : {x | f x ≠ g x ∧ f x = g x}.Nonempty := by
      have h₁ := (eventually_nhdsWithin_of_eventually_nhds
        ((hf.ne_iff_eventually_ne hg).1 hCon)).and hfg
      have h₂ : ∅ ∉ 𝓝[≠] x := by exact empty_notMem (𝓝[≠] x)
      simp_all
    simp at ha

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
⊢ codiscreteWithin S = ⊥ ↔ IsDiscrete S

Tactic:
by
  simp [isDiscrete_iff_nhdsNE, codiscreteWithin, ← nhdsWithin_inter', Set.sdiff_eq, inter_comm]

Goal state after:
Module: Mathlib.Data.Set.BoolIndicator

Goal state before:
pp: α : Type u_1
s : Set α
x : α
⊢ x ∈ s ↔ (if x ∈ s then true else false) = true

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u_1
s : Set α
x : α
h : x ∈ s
⊢ x ∈ s ↔ true = true

case neg
α : Type u_1
s : Set α
x : α
h : ¬x ∈ s
⊢ x ∈ s ↔ False
Module: Mathlib.Data.Set.BoolIndicator

Goal state before:
pp: α : Type u_1
s : Set α
x : α
⊢ ¬x ∈ s ↔ (if x ∈ s then true else false) = false

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u_1
s : Set α
x : α
h : x ∈ s
⊢ ¬x ∈ s ↔ False

case neg
α : Type u_1
s : Set α
x : α
h : ¬x ∈ s
⊢ ¬x ∈ s ↔ false = false
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: α : Type u_2
g : Set (Set α)
⊢ IsGreatest {f | CountableInterFilter f ∧ g ⊆ f.sets} (countableGenerate g)

Tactic:
by
  refine ⟨⟨inferInstance, fun s => CountableGenerateSets.basic⟩, ?_⟩
  rintro f ⟨fct, hf⟩
  rwa [@le_countableGenerate_iff_of_countableInterFilter _ _ _ fct]

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hs : IsPreconnected s
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
specialize hs u v hu hv hsuv
  obtain hsu | hsu := (s ∩ u).eq_empty_or_nonempty
  · exact Or.inr ((Set.disjoint_iff_inter_eq_empty.2 hsu).subset_right_of_subset_union hsuv)
  · replace hs := mt (hs hsu)
    simp_rw [Set.not_nonempty_iff_eq_empty, ← Set.disjoint_iff_inter_eq_empty,
      disjoint_iff_inter_eq_empty.1 huv] at hs
    exact Or.inl ((hs s.disjoint_empty).subset_left_of_subset_union hsuv)

Goal state after: