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

Goal state before:
pp: a b : ℕ
d : ℕ := a.gcd b
⊢ φ a * φ b ≤ φ (a * b)

Tactic:
rcases eq_zero_or_pos a with (rfl | ha0)

Goal state after:
case inl
b : ℕ
d : ℕ := gcd 0 b
⊢ φ 0 * φ b ≤ φ (0 * b)

case inr
a b : ℕ
d : ℕ := a.gcd b
ha0 : a > 0
⊢ φ a * φ b ≤ φ (a * b)
Module: Mathlib.Data.Nat.Totient

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

pp: case neg
a b : ℕ
h : a ∣ b
h' : φ a = φ b
ha : ¬a = 0
⊢ a = b ∨ 2 * a = b

Tactic:
· rw [ha, totient_zero, eq_comm, totient_eq_zero] at h'
    simp [ha, h']

Goal state after:
case neg
a b : ℕ
h : a ∣ b
h' : φ a = φ b
ha : ¬a = 0
⊢ a = b ∨ 2 * 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 c : α
⊢ toIocMod hp a b = c ↔ c ∈ Set.Ioc a (a + p) ∧ ∃ z, b = c + z • p

Tactic:
refine
    ⟨fun h =>
      ⟨h ▸ toIocMod_mem_Ioc hp a b, toIocDiv hp a b, h ▸ (toIocMod_add_toIocDiv_zsmul hp _ _).symm⟩,
      ?_⟩
  simp_rw [← @sub_eq_iff_eq_add]
  rintro ⟨hc, n, rfl⟩
  rw [← toIocDiv_eq_of_sub_zsmul_mem_Ioc hp hc, toIocMod]

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
p : Prop
⊢ IsOpen[inst✝] {_x | p}

Tactic:
by_cases p

Goal state after:
case pos
X : Type u
inst✝ : TopologicalSpace X
p : Prop
h✝ : p
⊢ IsOpen[inst✝] {_x | p}

case neg
X : Type u
inst✝ : TopologicalSpace X
p : Prop
h✝ : ¬p
⊢ IsOpen[inst✝] {_x | p}
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
ι : Sort v
inst✝¹ : TopologicalSpace X
inst✝ : Finite ι
s : ι → Set X
h : ∀ (i : ι), IsClosed[inst✝¹] (s i)
⊢ IsClosed[inst✝¹] (⋃ i, s i)

Tactic:
simp only [← isOpen_compl_iff, compl_iUnion] at *
  exact isOpen_iInter_of_finite h

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
h : Codisjoint (interior s) (interior t)
⊢ closure (s ∩ t) = closure s ∩ closure t

Tactic:
rw [← compl_inj_iff]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
h : Codisjoint (interior s) (interior t)
⊢ (closure (s ∩ t))ᶜ = (closure s ∩ closure t)ᶜ
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 ↔ b ∈ Set.Ioc a (a + p)

Tactic:
rw [toIocMod_eq_iff, and_iff_left]

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ ∃ z, b = b + z • 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 : α
h₁₂₃ : toIcoMod hp a b ≤ toIocMod hp a c
h₁₃₂ : toIcoMod hp a c ≤ toIocMod hp a b
h : ¬b ≡ a [PMOD p] ∧ ¬c ≡ b [PMOD p] ∧ ¬a ≡ c [PMOD p]
⊢ False

Tactic:
modEq_comm

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h₁₂₃ : toIcoMod hp a b ≤ toIocMod hp a c
h₁₃₂ : toIcoMod hp a c ≤ toIocMod hp a b
h : ¬a ≡ b [PMOD p] ∧ ¬c ≡ b [PMOD p] ∧ ¬a ≡ c [PMOD p]
⊢ False
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 : α
this : toIcoMod hp 0 (a - b) + toIocMod hp 0 (b - a) + (toIcoMod hp 0 (c - b) + toIocMod hp 0 (b - c)) = p + p
⊢ toIcoMod hp b a ≤ toIocMod hp b c ∨ toIcoMod hp b c ≤ toIocMod hp b a

Tactic:
simp only [add_add_add_comm] at this

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
this : toIcoMod hp 0 (a - b) + toIcoMod hp 0 (c - b) + (toIocMod hp 0 (b - a) + toIocMod hp 0 (b - c)) = p + p
⊢ toIcoMod hp b a ≤ toIocMod hp b c ∨ toIcoMod hp b c ≤ toIocMod hp b a
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: case inr
X : Type u
inst✝¹ : TopologicalSpace X
x : X
inst✝ : (𝓝[≠] x).NeBot
y : X
hne : y ≠ x
⊢ y ∈ closure[inst✝¹] {x}ᶜ

Tactic:
· exact subset_closure hne

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

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

Tactic:
simpa using toIocDiv_add_zsmul hp a b m

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
hf : IsOpenMap (⇑h ∘ f)
⊢ IsOpenMap f

Tactic:
← Function.id_comp f,

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 (id ∘ f)
Module: Mathlib.Topology.Constructions.SumProd

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

Tactic:
image_swap_eq_preimage_swap

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set (X × Y)
hs : IsClosed[instTopologicalSpaceProd] s
⊢ IsClosed[instTopologicalSpaceProd] (Prod.swap ⁻¹' s)
Module: Mathlib.Topology.Maps.Basic

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

Tactic:
hf.isClosed_iff_image_isClosed,

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsClosedEmbedding f
s : Set Y
hs : s ⊆ range f
⊢ IsClosed[inst✝] s ↔ IsClosed[inst✝] (f '' f ⁻¹' s)
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
x : α
⊢ (∀ᶠ (y : α) in 𝓝 x, y ∈ s → y ∈ t) ↔ ∀ᶠ (x : α) in 𝓝 x, x ∈ s ↔ x ∈ s ∩ t

Tactic:
mem_inter_iff,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
x : α
⊢ (∀ᶠ (y : α) in 𝓝 x, y ∈ s → y ∈ t) ↔ ∀ᶠ (x : α) in 𝓝 x, x ∈ s ↔ x ∈ s ∧ x ∈ t
Module: Mathlib.Topology.NhdsWithin

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

Tactic:
rw [nhdsWithin, principal_singleton, inf_eq_right.2 (pure_le_nhds a)]

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X × Y
⊢ map Prod.snd (𝓝[Prod.fst ⁻¹' {x.1}] x) = 𝓝 x.2

Tactic:
by
  refine le_antisymm (continuousAt_snd.mono_left inf_le_left) fun s hs => ?_
  rcases x with ⟨x, y⟩
  rw [mem_map, nhdsWithin, mem_inf_principal, mem_nhds_prod_iff] at hs
  rcases hs with ⟨u, hu, v, hv, H⟩
  simp only [prod_subset_iff, mem_singleton_iff, mem_ofPred_eq, mem_preimage] at H
  exact mem_of_superset hv fun z hz => H _ (mem_of_mem_nhds hu) _ hz rfl

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
f : β → α
a : α
s : Set α
l : Filter β
h : ∀ (i : Set α), a ∈ i ∧ IsOpen[inst✝] i → ∀ᶠ (a : β) in l, f a ∈ i ∩ s
⊢ ∀ᶠ (i : β) in l, f i ∈ s

Tactic:
mem_inter_iff,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
f : β → α
a : α
s : Set α
l : Filter β
h : ∀ (i : Set α), a ∈ i ∧ IsOpen[inst✝] i → ∀ᶠ (a : β) in l, f a ∈ i ∧ f a ∈ s
⊢ ∀ᶠ (i : β) in l, f i ∈ s
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 (𝓝 x) (𝓝 (f x))

Tactic:
← nhdsWithin_eq_nhds.2 hi

Goal state after:
α : 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))
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
u : Set α
hu : IsClosed[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s
⊢ IsClosed[inst✝¹] (u ∩ s)

Tactic:
apply IsClosed.inter hu.1 hs

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
x : ↑s
⊢ map Subtype.val (𝓝 x) = 𝓝[s] ↑x

Tactic:
by
  rw [IsInducing.subtypeVal.map_nhds_eq, Subtype.range_val]

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
x : α × β
⊢ ContinuousAt f x ↔ ContinuousAt (fun x_1 ↦ f (x_1, x.2)) x.1

Tactic:
by
  simp_rw [← continuousWithinAt_univ]; exact continuousWithinAt_prod_of_discrete_right

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

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
h : IsInducing (Sum.elim f g)
C : Set Z
C_closed : IsClosed[inst✝] C
hC : Sum.elim f g ⁻¹' C = range inl
A : closure[inst✝] (range f) ⊆ C
⊢ Disjoint (inr ⁻¹' Sum.elim f g ⁻¹' C) univ

Tactic:
hC,

Goal state after:
X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
h : IsInducing (Sum.elim f g)
C : Set Z
C_closed : IsClosed[inst✝] C
hC : Sum.elim f g ⁻¹' C = range inl
A : closure[inst✝] (range f) ⊆ C
⊢ Disjoint (inr ⁻¹' range inl) univ
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_5
s : ι → Set α
hf : ∀ (i : ι), ContinuousOn f (s i)
hs : ∀ (i : ι), IsOpen[inst✝¹] (s i)
x : α
i : ι
hxsi : x ∈ (fun i ↦ s i) i
⊢ ContinuousWithinAt f (⋃ i, s i) x

Tactic:
exact (hf i).continuousAt ((hs i).mem_nhds hxsi) |>.continuousWithinAt

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

Goal state before:
pp: α : Type u
f : Ultrafilter α
g : Filter α
⊢ Disjoint (↑f) g ↔ ↑f ⊓ g = ⊥

Tactic:
disjoint_iff

Goal state after:
α : Type u
f : Ultrafilter α
g : Filter α
⊢ ↑f ⊓ g = ⊥ ↔ ↑f ⊓ g = ⊥
Module: Mathlib.Topology.Compactness.LocallyCompact

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : WeaklyLocallyCompactSpace X
K : Set X
hK : IsCompact K
s : X → Set X
hc : ∀ (x : X), IsCompact (s x)
hmem : ∀ (x : X), s x ∈ 𝓝 x
⊢ ∃ K', IsCompact K' ∧ K ⊆ interior K'

Tactic:
rcases hK.elim_nhds_subcover _ fun x _ ↦ interior_mem_nhds.2 (hmem x) with ⟨I, -, hIK⟩

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : WeaklyLocallyCompactSpace X
K : Set X
hK : IsCompact K
s : X → Set X
hc : ∀ (x : X), IsCompact (s x)
hmem : ∀ (x : X), s x ∈ 𝓝 x
I : Finset X
hIK : K ⊆ ⋃ x ∈ I, interior (s x)
⊢ ∃ K', IsCompact K' ∧ K ⊆ interior K'
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: case inl
X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
hι : Countable ι
s : ι → Set X
hcomp : ∀ (i : ι), IsCompact (s i)
h✝ : IsEmpty ι
⊢ IsSigmaCompact (⋃ i, s i)

pp: case inr
X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
hι : Countable ι
s : ι → Set X
hcomp : ∀ (i : ι), IsCompact (s i)
h✝ : Nonempty ι
⊢ IsSigmaCompact (⋃ i, s i)

Tactic:
· simp only [iUnion_of_empty, isSigmaCompact_empty]

Goal state after:
case inr
X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
hι : Countable ι
s : ι → Set X
hcomp : ∀ (i : ι), IsCompact (s i)
h✝ : Nonempty ι
⊢ IsSigmaCompact (⋃ i, s i)
Module: Mathlib.Topology.Bases

Goal state before:
pp: case h_open
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
U : Set X
U_in_V : U ∈ V
⊢ IsOpen[inst✝] (π '' U)

Tactic:
apply h U (hV.isOpen U_in_V)

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed[inst✝] (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, s ∩ ⋂ i ∈ u, t i = ∅
ι✝ : Type u
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen[inst✝] (U i)
hsU : Disjoint s (⋂ i, (U i)ᶜ)
⊢ ∃ t, s ⊆ ⋃ i ∈ t, U i

Tactic:
disjoint_iff

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed[inst✝] (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, s ∩ ⋂ i ∈ u, t i = ∅
ι✝ : Type u
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen[inst✝] (U i)
hsU : s ⊓ ⋂ i, (U i)ᶜ = ⊥
⊢ ∃ t, s ⊆ ⋃ i ∈ t, U i
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed[inst✝] (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, s ∩ ⋂ i ∈ u, t i = ∅
ι✝ : Type u
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen[inst✝] (U i)
hsU : s ⊓ ⋂ i, (U i)ᶜ = ⊥
t : Finset ι✝
ht : s ∩ ⋂ i ∈ t, (U i)ᶜ = ∅
⊢ Disjoint s (⋂ i ∈ t, (U i)ᶜ)

Tactic:
disjoint_iff

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed[inst✝] (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, s ∩ ⋂ i ∈ u, t i = ∅
ι✝ : Type u
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen[inst✝] (U i)
hsU : s ⊓ ⋂ i, (U i)ᶜ = ⊥
t : Finset ι✝
ht : s ∩ ⋂ i ∈ t, (U i)ᶜ = ∅
⊢ s ⊓ ⋂ i ∈ t, (U i)ᶜ = ⊥
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsCompact t
b : Bool
⊢ IsCompact (bif b then s else t)

Tactic:
by cases b <;> assumption

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : PartialOrder α
s : Set α
x : α
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s
h : Minimal (fun x ↦ x ∈ { carrier := {x | ∃ a ∈ s, a ≤ x}, upper' := ⋯ }) x
⊢ x ∈ s

Tactic:
obtain ⟨a, has, hax⟩ := h.prop

Goal state after:
case refine_1
α : Type u_1
inst✝ : PartialOrder α
s : Set α
x : α
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s
h : Minimal (fun x ↦ x ∈ { carrier := {x | ∃ a ∈ s, a ≤ x}, upper' := ⋯ }) x
a : α
has : a ∈ s
hax : a ≤ x
⊢ x ∈ s
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: case neg
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (cocompact X) (𝓝 y)
hfc : Continuous[inst✝¹, inst✝] f
l : Filter Y
hne : l.NeBot
hle : l ≤ 𝓟 (insert y (range f))
s : Set Y
hsy : s ∈ 𝓝 y
t : Set Y
htl : t ∈ l
hd : Disjoint s t
K : Set X
hKc : IsCompact K
hKs : Kᶜ ⊆ f ⁻¹' s
this : f '' K ∈ l
⊢ ∃ x ∈ insert y (range f), ClusterPt x l

Tactic:
rcases hKc.image hfc (le_principal_iff.2 this) with ⟨y, hy, hyl⟩

Goal state after:
case neg
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
y✝ : Y
hf : Tendsto f (cocompact X) (𝓝 y✝)
hfc : Continuous[inst✝¹, inst✝] f
l : Filter Y
hne : l.NeBot
hle : l ≤ 𝓟 (insert y✝ (range f))
s : Set Y
hsy : s ∈ 𝓝 y✝
t : Set Y
htl : t ∈ l
hd : Disjoint s t
K : Set X
hKc : IsCompact K
hKs : Kᶜ ⊆ f ⁻¹' s
this : f '' K ∈ l
y : Y
hy : y ∈ f '' K
hyl : ClusterPt y l
⊢ ∃ x ∈ insert y✝ (range f), ClusterPt x l
Module: Mathlib.Topology.Inseparable

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

Tactic:
specializes_iff_forall_open

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R0Space X
x : X
ι✝ : Type u_1
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen[inst✝¹] (U i)
hxU : closure[inst✝¹] {x} ⊆ ⋃ i, U i
⊢ ∃ t, closure[inst✝¹] {x} ⊆ ⋃ i ∈ t, U i

Tactic:
obtain ⟨i, hi⟩ : ∃ i, x ∈ U i := mem_iUnion.1 <| hxU <| subset_closure rfl

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R0Space X
x : X
ι✝ : Type u_1
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen[inst✝¹] (U i)
hxU : closure[inst✝¹] {x} ⊆ ⋃ i, U i
i : ι✝
hi : x ∈ U i
⊢ ∃ t, closure[inst✝¹] {x} ⊆ ⋃ i ∈ t, U i
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case mp
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
x : X
H : (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S))
⊢ Disjoint (𝓝[≠] x) (𝓟 S)

pp: case mpr
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
x : X
H : Disjoint (𝓝[≠] x) (𝓟 S)
⊢ (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S))

Tactic:
· by_cases hx : x ∈ S
    exacts [H.2 hx, (H.1 hx).mono_left nhdsWithin_le_nhds]

Goal state after:
case mpr
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
x : X
H : Disjoint (𝓝[≠] x) (𝓟 S)
⊢ (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S))
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
t S U : Set X
hU' : IsOpen[inst✝] U
h₁ : U ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U
ht : IsIrreducible t
u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
x : X
hx : x ∈ S
hx' : x ∈ u
y : X
hy : y ∈ S
hy' : y ∈ v
⊢ ∀ u_1 ∈ {U, u, v}, IsOpen[inst✝] u_1

pp: case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
t S U : Set X
hU' : IsOpen[inst✝] U
h₁ : U ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U
ht : IsIrreducible t
u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
x : X
hx : x ∈ S
hx' : x ∈ u
y : X
hy : y ∈ S
hy' : y ∈ v
⊢ ∀ u_1 ∈ {U, u, v}, (t ∩ u_1).Nonempty

Tactic:
· simp [*]

Goal state after:
case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
t S U : Set X
hU' : IsOpen[inst✝] U
h₁ : U ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U
ht : IsIrreducible t
u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
x : X
hx : x ∈ S
hx' : x ∈ u
y : X
hy : y ∈ S
hy' : y ∈ v
⊢ ∀ u_1 ∈ {U, u, v}, (t ∩ u_1).Nonempty
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case h.left
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
U s : Set X
hs : Finite ↑s
t : Set X
ht : IsOpen[inst✝¹] t
h₁ts : x ∈ t
h₂ts : t ∩ {x}ᶜ ⊆ U
⊢ IsClosed[inst✝¹] (s \ {x} ∪ tᶜ)

Tactic:
exact s.toFinite.sdiff.isClosed.union (isClosed_compl_iff.2 ht)

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space X
x : X
s t : Set X
f : X → Y
y : X
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ ContinuousWithinAt f (insert x s) x ↔ ContinuousWithinAt f t x

Tactic:
← continuousWithinAt_insert_self (s := t)

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space X
x : X
s t : Set X
f : X → Y
y : X
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ ContinuousWithinAt f (insert x s) x ↔ ContinuousWithinAt f (insert x t) x
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
ι : Type u_3
I : Finset ι
s : ι → Set X
hs : ∀ i ∈ I, DiscreteTopology ↑(s i)
hs' : ∀ i ∈ I, IsClosed[inst✝] (s i)
⊢ DiscreteTopology ↑(⋃ i ∈ I, s i)

Tactic:
simp only [← isDiscrete_iff_discreteTopology] at *

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
ι : Type u_3
I : Finset ι
s : ι → Set X
hs' : ∀ i ∈ I, IsClosed[inst✝] (s i)
hs : ∀ i ∈ I, IsDiscrete (s i)
⊢ IsDiscrete (⋃ i ∈ I, s i)
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_3
inst✝ : Finite ι
s : ι → Set X
hs : ∀ (i : ι), DiscreteTopology ↑(s i)
hs' : ∀ (i : ι), IsClosed[inst✝¹] (s i)
⊢ DiscreteTopology ↑(⋃ i, s i)

Tactic:
simp only [← isDiscrete_iff_discreteTopology] at *

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_3
inst✝ : Finite ι
s : ι → Set X
hs' : ∀ (i : ι), IsClosed[inst✝¹] (s i)
hs : ∀ (i : ι), IsDiscrete (s i)
⊢ IsDiscrete (⋃ i, s i)
Module: Mathlib.Topology.Clopen

Goal state before:
pp: case refine_1
X : Type u
inst✝ : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
hab : s ∩ a ∩ b = ∅
⊢ s ⊆ s ∩ a ∪ s ∩ b

Tactic:
rw [← inter_union_distrib_left]
    exact subset_inter .rfl cover

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
s : Set X
hs : IsCompact s
ι : Type u_3
t : Finset ι
U : ι → Set X
hU : ∀ i ∈ t, IsOpen[inst✝¹] (U i)
hsC : s ⊆ ⋃ i ∈ t, U i
⊢ ∃ K, (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i

Tactic:
by
  classical
  induction t using Finset.induction generalizing U s with
  | empty =>
    refine ⟨fun _ => ∅, fun _ => isCompact_empty, fun i => empty_subset _, ?_⟩
    simpa only [subset_empty_iff, Finset.notMem_empty, iUnion_false, iUnion_empty] using hsC
  | insert x t hx ih =>
    simp only [Finset.set_biUnion_insert] at hsC
    simp only [Finset.forall_mem_insert] at hU
    have hU' : ∀ i ∈ t, IsOpen (U i) := fun i hi => hU.2 i hi
    rcases hs.binary_compact_cover hU.1 (isOpen_biUnion hU') hsC with
      ⟨K₁, K₂, h1K₁, h1K₂, h2K₁, h2K₂, hK⟩
    rcases ih h1K₂ U hU' h2K₂ with ⟨K, h1K, h2K, h3K⟩
    refine ⟨update K x K₁, ?_, ?_, ?_⟩
    · intro i
      rcases eq_or_ne i x with rfl | hi
      · simp only [update_self, h1K₁]
      · simp only [update_of_ne hi, h1K]
    · intro i
      rcases eq_or_ne i x with rfl | hi
      · simp only [update_self, h2K₁]
      · simp only [update_of_ne hi, h2K]
    · simp only [Finset.set_biUnion_insert_update _ hx, hK, h3K]

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

Goal state before:
pp: case refine_1.inl.refine_1
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : α
hx : inl x ∈ s
h : s ⊆ range inl
⊢ IsConnected (inl ⁻¹' s)

pp: case refine_1.inl.refine_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : α
hx : inl x ∈ s
h : s ⊆ range inl
⊢ s = inl '' inl ⁻¹' s

Tactic:
· exact hs.preimage_of_isOpenMap Sum.inl_injective isOpenMap_inl h

Goal state after:
case refine_1.inl.refine_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : α
hx : inl x ∈ s
h : s ⊆ range inl
⊢ s = inl '' inl ⁻¹' s
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_open : ∀ (i : ι), IsOpen[inst✝¹] (s i)
h_Union : ⋃ i, s i = univ
i : ι
⊢ IsOpen[inst✝¹] (⋃ i_1, s i_1 \ s i)

Tactic:
refine isOpen_iUnion (fun j ↦ ?_)

Goal state after:
α : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_open : ∀ (i : ι), IsOpen[inst✝¹] (s i)
h_Union : ⋃ i, s i = univ
i j : ι
⊢ IsOpen[inst✝¹] (s j \ s i)