mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Generator.Basic

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

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

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
β : Type w
f : β → C
c : Fan f
hc : IsLimit c
h : IsCoseparator c.pt
X Y : C
u v : X ⟶ Y
huv : ∀ (G : C), ObjectProperty.ofObj f G → ∀ (h : Y ⟶ G), u ≫ h = v ≫ h
⊢ u = v
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
I : Type v₁
inst✝ : SmallCategory I
F : I ⥤ C
c : Cocone (F ⋙ yoneda)
hc : IsColimit c
⊢ (c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt).Final

Tactic:
apply Functor.final_of_isTerminal_colimit_comp_yoneda
  suffices IsTerminal (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙
      CostructuredArrow.toOver yoneda c.pt)) by
    apply IsTerminal.isTerminalOfObj (overEquivPresheafCostructuredArrow c.pt).inverse
    apply IsTerminal.ofIso this
    refine ?_ ≪≫ (preservesColimitIso (overEquivPresheafCostructuredArrow c.pt).inverse _).symm
    apply HasColimit.isoOfNatIso
    exact Functor.isoWhiskerLeft _
      (CostructuredArrow.toOverCompOverEquivPresheafCostructuredArrow c.pt).isoCompInverse
  apply IsTerminal.ofIso Over.mkIdTerminal
  let isc : IsColimit ((Over.forget _).mapCocone _) := isColimitOfPreserves _
    (colimit.isColimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙
      CostructuredArrow.toOver yoneda c.pt))
  exact Over.isoMk (hc.coconePointUniqueUpToIso isc) (hc.hom_ext fun i => by simp)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : AddZeroClass α
f : α → β
x : α
⊢ f (x + 0) = f x

Tactic:
by
  rw [add_zero]

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
a b : α
⊢ b - a ∈ Ico 0 b ↔ a ∈ Ioc 0 b

Tactic:
by
  simp only [sub_mem_Ico_iff_right, sub_self, sub_zero]

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

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

Tactic:
have : r ∈ ideal i f y := by
    change (r • y) ∈ (extensionOfMax i f).toLinearPMap.domain
    rw [eq1]
    apply Submodule.zero_mem _

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
r : R
eq1 : r • y = 0
this : r ∈ ideal i f y
⊢ (extendIdealTo i f h y) r = 0
Module: Mathlib.Data.Nat.Cast.Field

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionSemiring K
d m n : ℕ
inst✝ : CharZero K
hn : d ∣ n
hm : d ∣ m
⊢ ↑(m / d) / ↑(n / d) = ↑m / ↑n

Tactic:
rcases eq_or_ne d 0 with (rfl | hd)

Goal state after:
case inl
K : Type u_1
inst✝¹ : DivisionSemiring K
m n : ℕ
inst✝ : CharZero K
hn : 0 ∣ n
hm : 0 ∣ m
⊢ ↑(m / 0) / ↑(n / 0) = ↑m / ↑n

case inr
K : Type u_1
inst✝¹ : DivisionSemiring K
d m n : ℕ
inst✝ : CharZero K
hn : d ∣ n
hm : d ∣ m
hd : d ≠ 0
⊢ ↑(m / d) / ↑(n / d) = ↑m / ↑n
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: a b m n✝ p✝ : ℕ
motive : ℕ → Sort u_1
zero : motive 0
one : motive 1
prime_pow_mul : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)
n k : ℕ
hk : (m : ℕ) → m < k + 2 → motive m
p : ℕ := (k + 2).minFac
hp : Prime p
t : ℕ := (k + 2).factorization p
hpt : p ^ t ∣ k + 2
htp : 0 < t
⊢ k + 2 = p ^ t * ((k + 2) / p ^ t)

Tactic:
rw [Nat.mul_div_cancel' hpt]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
p : α × β → Prop
hp : ∀ᶠ (x : α × β) in atTop, p x
⊢ ∀ᶠ (k : α) in atTop, ∀ᶠ (l : β) in atTop, p (k, l)

Tactic:
rw [← prod_atTop_atTop_eq] at hp
  exact hp.curry

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

Goal state before:
pp: case neg
n : ℕ
hn : ¬n = 0
p : ℕ
hp : 0 < n.factorization p
⊢ p ^ (n.factorization p).pred.succ * (p - 1) = p ^ n.factorization p * (p - 1)

Tactic:
Nat.succ_pred_eq_of_pos hp

Goal state after:
case neg
n : ℕ
hn : ¬n = 0
p : ℕ
hp : 0 < n.factorization p
⊢ p ^ n.factorization p * (p - 1) = p ^ n.factorization p * (p - 1)
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ Dense (closure s) ↔ Dense s

Tactic:
Dense,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ (∀ (x : X), x ∈ closure (closure s)) ↔ Dense s
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ (∀ (x : X), x ∈ closure (closure s)) ↔ Dense s

Tactic:
Dense,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ (∀ (x : X), x ∈ closure (closure s)) ↔ ∀ (x : X), x ∈ closure s
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
hF : F.HasBasis p s
⊢ ClusterPt x F ↔ ∀ (i : ι), p i → x ∈ closure[inst✝] (s i)

Tactic:
simp only [(nhds_basis_opens _).clusterPt_iff hF, mem_closure_iff]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
ι : Sort u_3
p : ι → Prop
s : ι → Set X
F : Filter X
hF : F.HasBasis p s
⊢ (∀ ⦃i : Set X⦄, x ∈ i ∧ IsOpen[inst✝] i → ∀ ⦃j : ι⦄, p j → (i ∩ s j).Nonempty) ↔
    ∀ (i : ι), p i → ∀ (o : Set X), IsOpen[inst✝] o → x ∈ o → (o ∩ s i).Nonempty
Module: Mathlib.Topology.Order

Goal state before:
pp: case refl.refine_1.sUnion
α : Type u_1
U : Set α
inst✝ : IndiscreteTopology α
S✝ : Set (Set α)
a✝ : ∀ s ∈ S✝, TopologicalSpace.GenerateOpen (OrderDual.ofDual ⊤) s
ih : ∀ s ∈ S✝, s = ∅ ∨ s = univ
⊢ ⋃₀ S✝ = ∅ ∨ ⋃₀ S✝ = univ

Tactic:
exact sUnion_mem_empty_univ ih

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 Y
inst✝ : TopologicalSpace X
hf : IsInducing f
s : Set X
⊢ IsClosed[inst✝] s ↔ ∃ t, IsClosed[inst✝¹] t ∧ f ⁻¹' t = s

Tactic:
by rw [hf.eq_induced, isClosed_induced_iff]

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 ι
hI : I.Finite
s : (i : ι) → Set (X i)
x : (i : ι) → X i
⊢ 𝓝[I.pi s] x = (⨅ i ∈ I, comap (fun x ↦ x i) (𝓝[s i] x i)) ⊓ ⨅ i, ⨅ (_ : i ∉ I), comap (fun x ↦ x i) (𝓝 (x i))

Tactic:
simp only [nhdsWithin, nhds_pi, Filter.pi, pi_def, ← iInf_principal_finite hI, comap_inf,
    comap_principal]

Goal state after:
ι : Type u_5
X : ι → Type u_6
inst✝ : (i : ι) → TopologicalSpace (X i)
I : Set ι
hI : I.Finite
s : (i : ι) → Set (X i)
x : (i : ι) → X i
⊢ (⨅ i, comap (eval i) (𝓝 (x i))) ⊓ ⨅ i ∈ I, 𝓟 (eval i ⁻¹' s i) =
    (⨅ i ∈ I, comap (fun x ↦ x i) (𝓝 (x i)) ⊓ 𝓟 ((fun x ↦ x i) ⁻¹' s i)) ⊓
      ⨅ i, ⨅ (_ : i ∉ I), comap (fun x ↦ x i) (𝓝 (x i))
Module: Mathlib.Topology.Constructions

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

Tactic:
rw [nhds_subtype, ← comap_nhdsWithin_range, Subtype.range_val]

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
t : Set β
⊢ IsClosed[instTopologicalSpaceSubtype] (s.domRestrict f ⁻¹' t) ↔ ∃ u, IsClosed[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s

Tactic:
rw [isClosed_induced_iff, Set.domRestrict_eq, Set.preimage_comp]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
t : Set β
⊢ (∃ t_1, IsClosed[inst✝¹] t_1 ∧ Subtype.val ⁻¹' t_1 = Subtype.val ⁻¹' f ⁻¹' t) ↔
    ∃ u, IsClosed[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
s : Set (Set α)
hs : t = generateFrom s
⊢ IsTopologicalBasis ((fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s})

Tactic:
by
  subst t; let := generateFrom s
  refine ⟨?_, ?_, le_antisymm (le_generateFrom ?_) <| generateFrom_anti fun t ht => ?_⟩
  · rintro _ ⟨t₁, ⟨hft₁, ht₁b⟩, rfl⟩ _ ⟨t₂, ⟨hft₂, ht₂b⟩, rfl⟩ x h
    exact ⟨_, ⟨_, ⟨hft₁.union hft₂, union_subset ht₁b ht₂b⟩, sInter_union t₁ t₂⟩, h, Subset.rfl⟩
  · rw [sUnion_image, iUnion₂_eq_univ_iff]
    exact fun x => ⟨∅, ⟨finite_empty, empty_subset _⟩, sInter_empty.substr <| mem_univ x⟩
  · rintro _ ⟨t, ⟨hft, htb⟩, rfl⟩
    exact hft.isOpen_sInter fun s hs ↦ GenerateOpen.basic _ <| htb hs
  · rw [← sInter_singleton t]
    exact ⟨{t}, ⟨finite_singleton t, singleton_subset_iff.2 ht⟩, rfl⟩

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t✝ : TopologicalSpace α
B : Set (Set α)
s t : Set α
hB : IsTopologicalBasis B
hs : IsOpen[t✝] s
ht : IsOpen[t✝] t
h : ∀ U ∈ B, U ⊆ s ↔ U ⊆ t
⊢ s = t

Tactic:
rw [hB.open_eq_sUnion' hs, hB.open_eq_sUnion' ht]
  exact congr_arg _ (Set.ext fun U ↦ and_congr_right <| h _)

Goal state after:
Module: Mathlib.Topology.ContinuousOn

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

Tactic:
hf.isEmbedding.map_nhdsWithin_eq,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
s : Set β
x : α
⊢ 𝓝[f '' f ⁻¹' s] f x = 𝓝[s] f x
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
β : Type u_1
t✝ : TopologicalSpace α
B : Set (Set α)
s✝ : Set α
inst✝² : TopologicalSpace β
inst✝¹ : SeparableSpace α
inst✝ : SeparableSpace β
s : Set α
hsc : s.Countable
hsd : Dense s
t : Set β
htc : t.Countable
htd : Dense t
⊢ SeparableSpace (α × β)

Tactic:
exact ⟨⟨s ×ˢ t, hsc.prod htc, hsd.prod htd⟩⟩

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case h
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
x✝ : a ∈ s
I : Finset ι
t : (a : ι) → Set (A a)
h1 : ∀ a_1 ∈ I, IsOpen[T a_1] (t a_1) ∧ a a_1 ∈ t a_1
h2 : (↑I).pi t ⊆ s
i : ι
hi : i ∉ I
⊢ (univ ⊆ if i ∈ I then t i else univ) ∧ IsOpen[T i] univ ∧ a i ∈ univ

Tactic:
if_neg hi

Goal state after:
case h
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
x✝ : a ∈ s
I : Finset ι
t : (a : ι) → Set (A a)
h1 : ∀ a_1 ∈ I, IsOpen[T a_1] (t a_1) ∧ a a_1 ∈ t a_1
h2 : (↑I).pi t ⊆ s
i : ι
hi : i ∉ I
⊢ univ ⊆ univ ∧ IsOpen[T i] univ ∧ a i ∈ univ
Module: Mathlib.Topology.Bases

Goal state before:
pp: case inr
ι : Type u_2
inst✝¹ : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst✝ : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure[inst✝ i] (c i)
this : ∀ (i : ι), Countable ↑(c i)
⊢ IsSeparable (univ.pi s)

Tactic:
set g : (I : Finset ι) × ((i : I) → c i) → (i : ι) → X i := fun ⟨I, f⟩ i ↦
      if hi : i ∈ I then f ⟨i, hi⟩ else f₀ i

Goal state after:
case inr
ι : Type u_2
inst✝¹ : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst✝ : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure[inst✝ i] (c i)
this : ∀ (i : ι), Countable ↑(c i)
g : (I : Finset ι) × ((i : ↥I) → ↑(c ↑i)) → (i : ι) → X i :=
  fun x i ↦
    match x with
    | ⟨I, f⟩ => if hi : i ∈ I then ↑(f ⟨i, hi⟩) else f₀ i
⊢ IsSeparable (univ.pi s)
Module: Mathlib.Order.Filter.Ultrafilter.Basic

Goal state before:
pp: α : Type u
β : Type v
f : Ultrafilter α
inst✝ : Finite β
P : β → α → Prop
⊢ (∀ᶠ (i : α) in ↑f, ∃ a, P a i) ↔ ∃ a, ∀ᶠ (i : α) in ↑f, P a i

Tactic:
by
  simpa using eventually_exists_mem_iff (f := f) (P := P) Set.finite_univ

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

Goal state before:
pp: α : Type u
f : Ultrafilter α
s : Set α
h : s.Finite
h' : ⋃ x ∈ s, {x} ∈ f
a : α
has : a ∈ s
haf : {a} ∈ f
⊢ ∃ x ∈ s, f = pure x

Tactic:
exact ⟨a, has, eq_of_le (Filter.le_pure_iff.2 haf)⟩

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
ι : Type u_5
σ : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : TopologicalSpace X
f : Sigma σ → X
⊢ IsInducing f ↔
    (∀ (i : ι), IsInducing (f ∘ Sigma.mk i)) ∧ ∀ (i : ι), ∃ U, IsOpen[inst✝] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i

Tactic:
by
  refine ⟨fun h ↦ ⟨fun i ↦ h.comp IsEmbedding.sigmaMk.1, fun i ↦ ?_⟩, ?_⟩
  · rcases h.isOpen_iff.1 (isOpen_range_sigmaMk (i := i)) with ⟨U, hUo, hU⟩
    refine ⟨U, hUo, ?_⟩
    simpa [Set.ext_iff] using hU
  · refine fun ⟨h₁, h₂⟩ ↦ isInducing_iff_nhds.2 fun ⟨i, x⟩ ↦ ?_
    rw [Sigma.nhds_mk, (h₁ i).nhds_eq_comap, comp_apply, ← comap_comap, map_comap_of_mem]
    rcases h₂ i with ⟨U, hUo, hU⟩
    filter_upwards [preimage_mem_comap <| hUo.mem_nhds <| (hU _).2 rfl] with y hy
    simpa [hU] using hy

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
⊢ IsSigmaCompact s ↔ IsSigmaCompact (f '' s)

Tactic:
constructor
  · exact fun h ↦ h.image hf.continuous
  · rintro ⟨L, hcomp, hcov⟩
    -- Suppose f(s) is σ-compact; we want to show s is σ-compact.
    -- Write f(s) as a union of compact sets L n, so s = ⋃ K n with K n := f⁻¹(L n) ∩ s.
    -- Since f is inducing, each K n is compact iff L n is.
    refine ⟨fun n ↦ f ⁻¹' (L n) ∩ s, ?_, ?_⟩
    · intro n
      have : f '' (f ⁻¹' (L n) ∩ s) = L n := by
        rw [image_preimage_inter, inter_eq_left.mpr]
        exact (subset_iUnion _ n).trans hcov.le
      apply hf.isCompact_iff.mpr (this.symm ▸ (hcomp n))
    · calc ⋃ n, f ⁻¹' L n ∩ s
        _ = f ⁻¹' (⋃ n, L n) ∩ s := by rw [preimage_iUnion, iUnion_inter]
        _ = f ⁻¹' (f '' s) ∩ s := by rw [hcov]
        _ = s := inter_eq_right.mpr (subset_preimage_image _ _)

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

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

Tactic:
refine univ_subset_iff.1 (iUnion_compactCovering X ▸ ?_)

Goal state after:
case refine_2
X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
s t : Set X✝
K✝ : CompactExhaustion X✝
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : SigmaCompactSpace X
K : ℕ → { s // IsCompact s } := fun n ↦ Nat.recOn n ⟨∅, ⋯⟩ fun n s ↦ ⟨⋯.choose ∪ compactCovering X n, ⋯⟩
⊢ ⋃ n, compactCovering X n ⊆ ⋃ n, ↑(K n)
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:
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.Data.Set.Functor

Goal state before:
pp: α : Type u
β : Set α
γ : Set ↑β
a : α
ha :
  a ∈ do
    let a ← γ
    pure ↑a
⊢ ⟨a, ⋯⟩ ∈ γ

Tactic:
rcases ha with ⟨_, ⟨_, rfl⟩, _, ⟨ha, rfl⟩, _⟩; convert! ha

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
t : Set (Set X)
ht : ∀ a ∈ t, IsClosed[inst✝] a
h : ∀ a ⊆ t, a.Finite → (s ∩ ⋂₀ a).Nonempty
⊢ (s ∩ ⋂₀ t).Nonempty

Tactic:
rw [Set.sInter_eq_iInter]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
t : Set (Set X)
ht : ∀ a ∈ t, IsClosed[inst✝] a
h : ∀ a ⊆ t, a.Finite → (s ∩ ⋂₀ a).Nonempty
⊢ (s ∩ ⋂ i, ↑i).Nonempty
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Nonempty ι
V : ι → Set X
hV : Directed (fun x1 x2 ↦ x1 ⊇ x2) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed[inst✝¹] (V i)
U : Set X
hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x
⊢ ∃ i, V i ⊆ U

Tactic:
obtain ⟨W, hsubW, W_op, hWU⟩ := exists_open_set_nhds hU
  suffices ∃ i, V i ⊆ W from this.imp fun i hi => hi.trans hWU
  by_contra! H
  replace H : ∀ i, (V i ∩ Wᶜ).Nonempty := fun i => Set.inter_compl_nonempty_iff.mpr (H i)
  have : (⋂ i, V i ∩ Wᶜ).Nonempty := by
    refine
      IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed _ (fun i j => ?_) H
        (fun i => (hV_cpct i).inter_right W_op.isClosed_compl) fun i =>
        (hV_closed i).inter W_op.isClosed_compl
    rcases hV i j with ⟨k, hki, hkj⟩
    refine ⟨k, ⟨fun x => ?_, fun x => ?_⟩⟩ <;> simp only [and_imp, mem_inter_iff, mem_compl_iff] <;>
      tauto
  have : ¬⋂ i : ι, V i ⊆ W := by simpa [← iInter_inter, inter_compl_nonempty_iff]
  contradiction

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
hs : IsCompact s
t : Set Y
ht : IsCompact t
n : Set (X × Y)
hn✝ : IsOpen[instTopologicalSpaceProd] n
u : Set X
v : Set Y
hn : (u, v).1 ×ˢ (u, v).2 ⊆ n
huo : IsOpen[inst✝¹] (u, v).1
hsu : s ⊆ (u, v).1
hvo : IsOpen[inst✝] (u, v).2
htv : t ⊆ (u, v).2
⊢ ∃ u v, IsOpen[inst✝¹] u ∧ IsOpen[inst✝] v ∧ s ⊆ u ∧ t ⊆ v ∧ u ×ˢ v ⊆ n

Tactic:
exact ⟨u, v, huo, hvo, hsu, htv, hn⟩

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
⊢ comap f (cocompact Y) ≤ cocompact X

Tactic:
(Filter.hasBasis_cocompact.comap f).le_basis_iff Filter.hasBasis_cocompact

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
⊢ ∀ (i' : Set X), IsCompact i' → ∃ i, IsCompact i ∧ f ⁻¹' iᶜ ⊆ i'ᶜ
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: Y : Type u_2
inst✝ : TopologicalSpace Y
S : Set Y
⊢ DiscreteTopology ↑S ↔ ∀ x ∈ S, 𝓝[≠] x ⊓ 𝓟 S = ⊥

Tactic:
discreteTopology_iff_nhds_ne,

Goal state after:
Y : Type u_2
inst✝ : TopologicalSpace Y
S : Set Y
⊢ (∀ (x : ↑S), 𝓝[≠] x = ⊥) ↔ ∀ x ∈ S, 𝓝[≠] x ⊓ 𝓟 S = ⊥
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
⊢ T0Space X ↔ Pairwise fun a b ↦ a ∉ closure[inst✝] {b} ∨ b ∉ closure[inst✝] {a}

Tactic:
simp only [t0Space_iff_not_inseparable, inseparable_iff_mem_closure, not_and_or]

Goal state after:
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
i : ι✝
hi : x ∈ U i
y : X
hy : y ∈ closure[inst✝¹] {x}
⊢ y ∈ ⋃ i_1 ∈ {i}, U i_1

Tactic:
← specializes_iff_mem_closure,

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
y : X
hy : x ⤳ y
⊢ y ∈ ⋃ i_1 ∈ {i}, U i_1
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
i : ι✝
hi : x ∈ U i
y : X
hy : y ∈ closure[inst✝¹] {x}
⊢ y ∈ ⋃ i_1 ∈ {i}, U i_1

Tactic:
rw [← specializes_iff_mem_closure, specializes_comm] at hy

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
y : X
hy : y ⤳ x
⊢ y ∈ ⋃ i_1 ∈ {i}, U i_1
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
t : Finset (Set X)
⊢ (∀ u ∈ t, IsOpen[inst✝] u) → (∀ u ∈ t, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑t).Nonempty ↔
    (∀ u ∈ t, IsOpen[inst✝] u) → s ⊆ ⋃ a ∈ ↑t, aᶜ → ∃ z, (∃ a ∈ t, aᶜ = z) ∧ s ⊆ z

Tactic:
exists_exists_and_eq_and

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
t : Finset (Set X)
⊢ (∀ u ∈ t, IsOpen[inst✝] u) → (∀ u ∈ t, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑t).Nonempty ↔
    (∀ u ∈ t, IsOpen[inst✝] u) → s ⊆ ⋃ a ∈ ↑t, aᶜ → ∃ a ∈ t, s ⊆ aᶜ
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: case mp
ι : Type u_4
X : ι → Type u_5
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), T2Space (X i)
s : Set ((i : ι) → X i)
H : IsCompact s
⊢ IsClosed[topologicalSpace] s ∧ ∀ (i : ι), IsCompact (eval i '' s)

pp: case mpr
ι : Type u_4
X : ι → Type u_5
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), T2Space (X i)
s : Set ((i : ι) → X i)
H : IsClosed[topologicalSpace] s ∧ ∀ (i : ι), IsCompact (eval i '' s)
⊢ IsCompact s

Tactic:
· exact ⟨H.isClosed, fun i ↦ H.image <| continuous_apply i⟩

Goal state after:
case mpr
ι : Type u_4
X : ι → Type u_5
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), T2Space (X i)
s : Set ((i : ι) → X i)
H : IsClosed[topologicalSpace] s ∧ ∀ (i : ι), IsCompact (eval i '' s)
⊢ IsCompact s
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: ι : Type u_3
β : ι → Type u_4
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → TopologicalSpace (β i)
x : (i : ι) → β i
i : ι
inst✝ : ∀ (i : ι), T1Space (β i)
s : Set (β i)
hs : IsClosed[inst✝¹ i] s
⊢ IsClosed[Pi.topologicalSpace] (update x i '' s)

Tactic:
update_image

Goal state after:
ι : Type u_3
β : ι → Type u_4
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → TopologicalSpace (β i)
x : (i : ι) → β i
i : ι
inst✝ : ∀ (i : ι), T1Space (β i)
s : Set (β i)
hs : IsClosed[inst✝¹ i] s
⊢ IsClosed[Pi.topologicalSpace] (univ.pi (update (fun j ↦ {x j}) i s))
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
⊢ s.Nonempty ∧ IsPreconnected s ↔
    ∀ (U : Finset (Set α)),
      (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
        (∀ u ∈ U, IsOpen[inst✝] u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u

Tactic:
isPreconnected_iff_subset_of_disjoint

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
⊢ (s.Nonempty ∧ ∀ (u v : Set α), IsOpen[inst✝] u → IsOpen[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v) ↔
    ∀ (U : Finset (Set α)),
      (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
        (∀ u ∈ U, IsOpen[inst✝] u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst✝] (U i)
hsU : s ⊆ ⋃ i, U i
s✝ t✝ : Set X
⊢ s✝ ⊆ t✝ → (∃ r, r.Countable ∧ t✝ ⊆ ⋃ i ∈ r, U i) → ∃ r, r.Countable ∧ s✝ ⊆ ⋃ i ∈ r, U i

Tactic:
hst

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst✝] (U i)
hsU : s ⊆ ⋃ i, U i
s✝ t✝ : Set X
hst : s✝ ⊆ t✝
⊢ (∃ r, r.Countable ∧ t✝ ⊆ ⋃ i ∈ r, U i) → ∃ r, r.Countable ∧ s✝ ⊆ ⋃ i ∈ r, U i