mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: n : ℕ
m : ↑{m | m < n ∧ n.Coprime m}
⊢ ↑m ∈ {x ∈ range n | n.Coprime x}

Tactic:
by simpa only [Finset.mem_filter, Finset.mem_range] using! m.property

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

Goal state before:
pp: n : ℕ
m : ↥({x ∈ range n | n.Coprime x})
⊢ ↑m ∈ {m | m < n ∧ n.Coprime m}

Tactic:
by simpa only [Finset.mem_filter, Finset.mem_range] using! m.property

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 • p - b = -toIocMod hp a b

Tactic:
toIocMod,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocDiv hp a b • p - b = -(b - toIocDiv hp a b • 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 : α
⊢ toIocMod hp a b - b = -toIocDiv hp a b • p

Tactic:
toIocMod,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ b - toIocDiv hp a b • p - b = -toIocDiv hp a b • 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 : α
⊢ b - toIocMod hp a b = toIocDiv hp a b • p

Tactic:
toIocMod,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ b - (b - toIocDiv hp a b • p) = toIocDiv hp a b • 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 : α
⊢ toIocMod hp a b + toIocDiv hp a b • p = b

Tactic:
toIocMod,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ b - toIocDiv hp a b • p + toIocDiv hp a b • p = b
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 : α
⊢ toIocMod hp a b + toIocDiv hp a b • p = b

Tactic:
by
  rw [toIocMod, sub_add_cancel]

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

Tactic:
toIocMod,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ b + m • p - toIocDiv hp a (b + m • p) • p = toIocMod hp a b
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 : ℤ
⊢ b + m • p - (toIocDiv hp a b + m) • p = toIocMod hp a b

Tactic:
toIocMod,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ b + m • p - (toIocDiv hp a b + m) • p = b - toIocDiv hp a b • 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 : α
⊢ toIocMod hp a (b - c) = toIocMod hp (a + c) b - c

Tactic:
toIocMod,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ b - c - toIocDiv hp a (b - c) • p = b - toIocDiv hp (a + c) b • p - c
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 : α
⊢ toIocMod hp a (b + c) = toIocMod hp (a - c) b + c

Tactic:
toIocMod,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ b + c - toIocDiv hp a (b + c) • p = b - toIocDiv hp (a - c) b • p + c
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 : α
⊢ -b - toIcoDiv hp a (-b) • p = p - toIocMod hp (-a) b

Tactic:
toIocMod,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ -b - toIcoDiv hp a (-b) • p = p - (b - toIocDiv hp (-a) b • 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 : α
⊢ toIocMod hp a (-b) = p - toIcoMod hp (-a) b

Tactic:
toIocMod,

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

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

Tactic:
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.Algebra.Order.ToIntervalMod

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

Tactic:
toIocMod,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ b - toIcoDiv hp a b • p = b - toIocDiv hp a b • p ↔ toIcoDiv hp a b = toIocDiv hp a b
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 : α
⊢ b - toIcoDiv hp a b • p + p = toIocMod hp a b ↔ toIcoDiv hp a b = toIocDiv hp a b + 1

Tactic:
toIocMod,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ b - toIcoDiv hp a b • p + p = b - toIocDiv hp a b • p ↔ toIcoDiv hp a b = toIocDiv 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 : α
⊢ a ≡ b [PMOD p] ↔ toIcoDiv hp a b = toIocDiv hp a b + 1

Tactic:
rw [modEq_iff_toIcoMod_add_period_eq_toIocMod hp, toIcoMod, toIocMod, ← eq_sub_iff_add_eq,
    sub_sub, sub_right_inj, ← add_one_zsmul, zsmul_left_inj hp]

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 : α
⊢ b - toIcoDiv hp a b • p ≤ toIocMod hp a b

Tactic:
toIocMod,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ b - toIcoDiv hp a b • p ≤ b - toIocDiv hp a b • 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 : α
⊢ toIocMod hp a b ≤ b - toIcoDiv hp a b • p + p

Tactic:
toIocMod,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ b - toIocDiv hp a b • p ≤ b - toIcoDiv hp a b • p + p
Module: Mathlib.Topology.ClusterPt

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

Tactic:
by
  simp_rw [MapClusterPt, hx.clusterPt_iff_frequently, frequently_map]

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:
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
C : Set X
⊢ ClusterPt x (𝓟 C) ↔ x ∈ C ∨ AccPt x (𝓟 C)

Tactic:
by
  constructor
  · intro h
    by_contra! hc
    rw [accPt_principal_iff_clusterPt] at hc
    simp_all only [not_false_eq_true, sdiff_singleton_eq_self, not_true_eq_false, hc.1]
  · rintro (h | h)
    · exact clusterPt_principal_iff.mpr fun _ mem ↦ ⟨x, ⟨mem_of_mem_nhds mem, h⟩⟩
    · exact h.clusterPt

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

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp a b = a + p - Int.fract ((a + p - b) / p) * p

Tactic:
toIocMod,

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ b - toIocDiv hp a b • p = a + p - Int.fract ((a + p - b) / p) * p
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 b : α
⊢ ∃ i, b ∈ Ico (a + i • p) (a + (i + 1) • p)

Tactic:
rcases sub_toIcoDiv_zsmul_mem_Ico hp a b with ⟨hl, hr⟩

Goal state after:
α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a ≤ b - toIcoDiv hp a b • p
hr : b - toIcoDiv hp a b • p < a + p
⊢ ∃ i, b ∈ Ico (a + i • p) (a + (i + 1) • p)
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
p : X → Prop
⊢ (∀ᶠ (x : X) in 𝓝ˢ (s ∪ t), p x) ↔ (∀ᶠ (x : X) in 𝓝ˢ s, p x) ∧ ∀ᶠ (x : X) in 𝓝ˢ t, p x

Tactic:
by
  rw [nhdsSet_union, eventually_sup]

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
t₁ t₂ : TopologicalSpace α
h : ∀ (x : α), 𝓝 x ≤ 𝓝 x
s : Set α
⊢ IsOpen[t₂] s → IsOpen[t₁] s

Tactic:
rw [@isOpen_iff_mem_nhds _ t₁, @isOpen_iff_mem_nhds _ t₂]
  exact fun hs a ha => h _ (hs _ ha)

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
W : Type u_3
Z : Type u_4
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace W
inst✝² : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst✝¹ : TopologicalSpace X'
inst✝ : TopologicalSpace Y'
f : X ≃ₜ Y
g : Y → X
hg : Function.RightInverse g ⇑f
this : g = ⇑f.symm
⊢ Function.LeftInverse g ⇑f

Tactic:
by convert! f.left_inv

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

Tactic:
hgf.eq_coinduced,

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
hf : Continuous[inst✝², inst✝¹] f
hg : Continuous[inst✝¹, inst✝] g
hgf : IsCoinducing (g ∘ f)
⊢ coinduced (g ∘ f) inst✝² ≤ coinduced g inst✝¹
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: case inr.mp
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
⊢ IsOpen[instTopologicalSpaceProd] (s ×ˢ t) → IsOpen[inst✝¹] s ∧ IsOpen[inst✝] t ∨ s = ∅ ∨ t = ∅

Tactic:
intro (H : IsOpen (s ×ˢ t))
      refine Or.inl ⟨?_, ?_⟩
      · simpa only [fst_image_prod _ st.2] using isOpenMap_fst _ H
      · simpa only [snd_image_prod st.1 t] using isOpenMap_snd _ H

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
s : Set (CofiniteTopology X)
⊢ IsOpen s ↔ s.Nonempty → sᶜ.Finite

Tactic:
isOpen_coinduced,

Goal state after:
X : Type u
s : Set (CofiniteTopology X)
⊢ IsOpen[TopologicalSpace.cofinite] (WithTopology.toTopology TopologicalSpace.cofinite ⁻¹' s) ↔ s.Nonempty → sᶜ.Finite
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
s : Set (CofiniteTopology X)
⊢ IsOpen s ↔ s = ∅ ∨ sᶜ.Finite

Tactic:
simp only [isOpen_iff, nonempty_iff_ne_empty, or_iff_not_imp_left]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s u : Set α
⊢ u ∈ 𝓝ˢ s ↔ ∃ v ∈ 𝓝ˢ (f '' s), f ⁻¹' v ⊆ u

Tactic:
by
  let := t.induced f
  simp_rw [mem_nhdsSet_iff_exists, isOpen_induced_iff]
  refine ⟨fun ⟨v, ⟨v', hv'⟩, hv⟩ ↦ ?_, fun ⟨v, ⟨v', hv'⟩, hv⟩ ↦ ?_⟩
  · refine ⟨v', ⟨v', hv'.1, ?_, subset_rfl⟩, hv'.2.trans_subset hv.2⟩
    exact (image_mono hv.1).trans (by simp [hv'])
  · exact ⟨f ⁻¹' v', ⟨v', hv'.1, rfl⟩, image_subset_iff.1 hv'.2.1, (preimage_mono hv'.2.2).trans hv⟩

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → β
s : Set α
x : α
h : f =ᶠ[𝓝[s] x] g
hx : f x = g x
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt g s x

Tactic:
rw [ContinuousWithinAt, hx, tendsto_congr' h, ContinuousWithinAt]

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsInducing f
s : Set α
x : α
⊢ map f (𝓝[s] x) = 𝓝[f '' s] f x

Tactic:
ext; simp +contextual [mem_nhdsWithin_iff_eventually, hf.nhds_eq_comap, forall_comm (α := _ ∈ _)]

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : α → β
hfs : ContinuousOn f s
hft : ContinuousOn f t
hs : IsClosed[inst✝¹] s
ht : IsClosed[inst✝¹] t
x : α
hx : x ∈ s ∪ t
⊢ ContinuousWithinAt f s x

pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : α → β
hfs : ContinuousOn f s
hft : ContinuousOn f t
hs : IsClosed[inst✝¹] s
ht : IsClosed[inst✝¹] t
x : α
hx : x ∈ s ∪ t
⊢ ContinuousWithinAt f t x

Tactic:
· refine if hx : x ∈ s then hfs x hx else continuousWithinAt_of_notMem_closure ?_
    rwa [hs.closure_eq]

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : α → β
hfs : ContinuousOn f s
hft : ContinuousOn f t
hs : IsClosed[inst✝¹] s
ht : IsClosed[inst✝¹] t
x : α
hx : x ∈ s ∪ t
⊢ ContinuousWithinAt f t x
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : α → β
hfs : ContinuousOn f s
hft : ContinuousOn f t
hs : IsClosed[inst✝¹] s
ht : IsClosed[inst✝¹] t
x : α
hx : x ∈ s ∪ t
⊢ ContinuousWithinAt f t x

Tactic:
refine if hx : x ∈ t then hft x hx else continuousWithinAt_of_notMem_closure ?_

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : α → β
hfs : ContinuousOn f s
hft : ContinuousOn f t
hs : IsClosed[inst✝¹] s
ht : IsClosed[inst✝¹] t
x : α
hx✝ : x ∈ s ∪ t
hx : x ∉ t
⊢ x ∉ closure[inst✝¹] t
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
⊢ ∃ s ⊆ t, s.Countable ∧ IsTopologicalBasis s

Tactic:
have A : ∀ u ∈ countableBasis α, ∃ s ⊆ t, s.Countable ∧ u = ⋃ a ∈ s, a :=
    fun u hu ↦ ht.exists_countable_biUnion_of_isOpen ((isBasis_countableBasis α).isOpen hu)
  choose! s hst s_count hs using A
  refine ⟨⋃ u ∈ countableBasis α, s u, by simpa using hst,
    (countable_countableBasis α).biUnion s_count, ?_⟩
  apply isTopologicalBasis_of_isOpen_of_nhds
  · simp only [mem_iUnion, exists_prop, forall_exists_index, and_imp]
    have := @ht.isOpen
    grind
  · intro x v hx hv
    simp only [mem_iUnion, exists_prop]
    obtain ⟨u, u_mem, xu, uv⟩ : ∃ u ∈ countableBasis α, x ∈ u ∧ u ⊆ v :=
      (isBasis_countableBasis α).isOpen_iff.1 hv _ hx
    have : x ∈ ⋃ a ∈ s u, a := by
      convert! xu
      exact (hs u u_mem).symm
    obtain ⟨w, ws, xw⟩ : ∃ w ∈ s u, x ∈ w := by simpa using this
    refine ⟨w, ⟨u, u_mem, ws⟩, xw, ?_⟩
    apply Subset.trans (Subset.trans _ (hs u u_mem).symm.subset) uv
    exact subset_iUnion₂_of_subset w ws (Subset.refl _)

Goal state after:
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
g : ι' → ι
hf : LocallyFinite f
hg : InjOn g {i | (f (g i)).Nonempty}
x : X
⊢ ∃ t ∈ 𝓝 x, {i | ((f ∘ g) i ∩ t).Nonempty}.Finite

Tactic:
let ⟨t, htx, htf⟩ := hf x

Goal state after:
ι : Type u_1
ι' : Type u_2
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
g : ι' → ι
hf : LocallyFinite f
hg : InjOn g {i | (f (g i)).Nonempty}
x : X
t : Set X
htx : t ∈ 𝓝 x
htf : {i | (f i ∩ t).Nonempty}.Finite
⊢ ∃ t ∈ 𝓝 x, {i | ((f ∘ g) i ∩ t).Nonempty}.Finite
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
f : X → Set X
s : Set X
hs : IsClosed[inst✝¹] s
hf : ∀ x ∈ s, f x ∈ 𝓝[s] x
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x

Tactic:
simp only [nhdsWithin, mem_inf_principal] at hf

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
f : X → Set X
s : Set X
hs : IsClosed[inst✝¹] s
hf : ∀ x ∈ s, {x_1 | x_1 ∈ s → x_1 ∈ f x} ∈ 𝓝 x
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
l : Filter X
s' : Set X
hmem : s ∈ l
h : ∀ x ∈ s, ClusterPt x l → x ∈ s'
⊢ l ≤ 𝓝ˢ s'

Tactic:
refine le_iff_ultrafilter.2 fun f hf ↦ ?_
  rcases hs.ultrafilter_le_nhds' f (hf hmem) with ⟨x, hxs, hx⟩
  grw [hx]
  refine nhds_le_nhdsSet ?_
  exact h x hxs (.mono (.of_le_nhds hx) hf)

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s t : Set α
hs : IsLowerSet s
⊢ Disjoint s ↑(upperClosure t) ↔ Disjoint s t

Tactic:
simpa only [disjoint_comm] using hs.disjoint_upperClosure_left

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
s t : Set X✝
X : Type u_3
inst✝ : Infinite X
u v : Set (CofiniteTopology X)
⊢ IsOpen u → IsOpen v → (univ ∩ u).Nonempty → (univ ∩ v).Nonempty → (univ ∩ (u ∩ v)).Nonempty

Tactic:
by
    simp only [CofiniteTopology.isOpen_iff, univ_inter]
    intro hu hv hu' hv'
    simpa only [compl_union, compl_compl] using ((hu hu').union (hv hv')).infinite_compl.nonempty

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s : Set X
hs : s.Finite
⊢ IsClosed[inst✝¹] s

Tactic:
rw [← biUnion_of_singleton s]
  exact hs.isClosed_biUnion fun i _ => isClosed_singleton

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

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed[inst✝¹] S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen[inst✝¹] U ∧ Uᶜ.Nonempty}
U : Set X
h : Maximal (fun x ↦ x ∈ opens) U
⊢ ∃ V ⊆ S, V.Nonempty ∧ IsClosed[inst✝¹] V ∧ ∀ V' ⊆ V, V'.Nonempty → IsClosed[inst✝¹] V' → V' = V

Tactic:
obtain ⟨Uc, Uo, Ucne⟩ := h.prop

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed[inst✝¹] S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen[inst✝¹] U ∧ Uᶜ.Nonempty}
U : Set X
h : Maximal (fun x ↦ x ∈ opens) U
Uc : Sᶜ ⊆ U
Uo : IsOpen[inst✝¹] U
Ucne : Uᶜ.Nonempty
⊢ ∃ V ⊆ S, V.Nonempty ∧ IsClosed[inst✝¹] V ∧ ∀ V' ⊆ V, V'.Nonempty → IsClosed[inst✝¹] V' → V' = V
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case h₂.h
X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
h : (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
⊢ ¬Z ⊆ ⋃₀ (irreducibleComponents X \ {Z})

Tactic:
exact mt (mem_of_subset_sUnion_irreducibleComponents Z hZ _ hX.sdiff Set.sdiff_subset)
        (Set.notMem_sdiff_of_mem (Set.mem_singleton Z))

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 ι)

Goal state after:
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
x✝ : TopologicalSpace ι := ⊥
⊢ ∃ u v,
    IsOpen[instTopologicalSpaceSigma] u ∧ IsOpen[instTopologicalSpaceSigma] v ∧ ⟨i, x⟩ ∈ u ∧ ⟨j, y⟩ ∈ v ∧ Disjoint u v
Module: Mathlib.Order.SuccPred.Relation

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
r : α → α → Prop
n m : α
inst✝ : Std.Refl r
h1 : ∀ i ∈ Ico n m, r i (succ i)
h2 : ∀ i ∈ Ico m n, r (succ i) i
⊢ TransGen r n m

Tactic:
rcases eq_or_ne m n with (rfl | hmn); · exact TransGen.single (refl m)
  exact transGen_of_succ_of_ne r h1 h2 hmn.symm

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x y : X
s t : Set X
hu : t ⊆ insert y s
⊢ insert x s ∈ 𝓝[t] x

Tactic:
rcases eq_or_ne x y with (rfl | h)
  · exact mem_of_superset self_mem_nhdsWithin hu
  refine nhdsWithin_mono x hu ?_
  rw [nhdsWithin_insert_of_ne h]
  exact mem_of_superset self_mem_nhdsWithin (subset_insert x s)

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case insert
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t✝ : Set X
h : t✝.Finite
τ : X
t : Set X
hτ : τ ∉ t
⊢ t.Finite → tᶜ ∈ codiscreteWithin s → (insert τ t)ᶜ ∈ codiscreteWithin s

Tactic:
h₁t

Goal state after:
case insert
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t✝ : Set X
h : t✝.Finite
τ : X
t : Set X
hτ : τ ∉ t
h₁t : t.Finite
⊢ tᶜ ∈ codiscreteWithin s → (insert τ t)ᶜ ∈ codiscreteWithin s
Module: Mathlib.Topology.Connected.LocallyConnected

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
⊢ (∀ (x : α), (𝓝 x).HasBasis (fun s ↦ IsOpen[inst✝] s ∧ x ∈ s ∧ IsConnected s) id) ↔
    ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst✝] V ∧ x ∈ V ∧ IsConnected V

Tactic:
refine forall_congr' fun _ => ?_

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
x✝ : α
⊢ (𝓝 x✝).HasBasis (fun s ↦ IsOpen[inst✝] s ∧ x✝ ∈ s ∧ IsConnected s) id ↔
    ∀ U ∈ 𝓝 x✝, ∃ V ⊆ U, IsOpen[inst✝] V ∧ x✝ ∈ V ∧ IsConnected V