mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.Injective

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

Tactic:
have hf (x) (hx : x ∈ I') : f ⟨x, hx⟩ = e₂.symm (g ⟨e₁ x, by simp_all [I']⟩) := rfl

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

Goal state before:
pp: case mp
p : ℕ
hp : Prime p
n a : ℕ
ha : a < p ^ (n + 1)
hap : ¬p ∣ a
b : ℕ
h : b < p ^ n ∧ b * p = a
⊢ False

Tactic:
rcases h with ⟨_, rfl⟩

Goal state after:
case mp
p : ℕ
hp : Prime p
n b : ℕ
left✝ : b < p ^ n
ha : b * p < p ^ (n + 1)
hap : ¬p ∣ b * p
⊢ False
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: a : ℕ
han : 0 < a
ha : φ a ≤ 1
⊢ a ∣ 2

Tactic:
rcases totient_eq_one_iff.mp <| le_antisymm ha <| totient_pos.2 han with rfl | rfl <;> norm_num

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

Goal state before:
pp: a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * p * d)
hb : ¬a * (p * d) = 0
this : φ a < φ (p * a * d)
⊢ False

Tactic:
mul_comm a

Goal state after:
a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (p * a * d)
hb : ¬a * (p * d) = 0
this : φ a < φ (p * a * d)
⊢ 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 : α
⊢ toIcoDiv hp a (b - c) = toIcoDiv hp (a + c) b

Tactic:
apply toIcoDiv_eq_of_sub_zsmul_mem_Ico

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

Tactic:
apply toIocDiv_eq_of_sub_zsmul_mem_Ioc
  rw [← sub_right_comm, Set.sub_mem_Ioc_iff_left, add_right_comm]
  exact sub_toIocDiv_zsmul_mem_Ioc hp (a + c) b

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
α : Type u_1
inst✝ : TopologicalSpace X
hX : Nonempty X
f : Filter α
g : α → X
h : ¬∃ x, map g f ≤ 𝓝 x
⊢ ↑(if hp : ∃ x, map g f ≤ 𝓝 x then ⟨↑(Classical.indefiniteDescription (fun x ↦ map g f ≤ 𝓝 x) hp), ⋯⟩
      else ⟨Classical.choice hX, ⋯⟩) =
    Classical.choice hX

Tactic:
dif_neg h

Goal state after:
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 c : α
h : toIcoMod hp a b = toIcoMod hp a c
⊢ toIcoMod hp a c + toIcoDiv hp a c • p - (toIcoMod hp a c + toIcoDiv hp a b • p) =
    (toIcoDiv hp a c - toIcoDiv hp a b) • p

Tactic:
sub_smul

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

Tactic:
sub_smul

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
α : Type u_1
F : Filter α
u : α → X
x : X
v : α → X
h : u =ᶠ[F] v
⊢ MapClusterPt x F u ↔ MapClusterPt x F v

Tactic:
by
  simp only [mapClusterPt_def, map_congr h]

Goal state after:
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
s₁ s₂ : Set X
h : x ∈ closure[inst✝] (s₁ ∪ s₂)
h₁ : s₁ᶜ ∈ 𝓝 x
⊢ x ∈ closure[inst✝] s₂

Tactic:
rw [mem_closure_iff_nhds_ne_bot] at *
  rwa [← sup_principal, inf_sup_left, inf_principal_eq_bot.mpr h₁, bot_sup_eq] at h

Goal state after:
Module: Mathlib.Topology.NhdsSet

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

Tactic:
disjoint_principal_left,

Goal state after:
X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
⊢ sᶜ ∈ 𝓝ˢ t ↔ Disjoint (closure[inst✝] s) t
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s₁ s₂ t₁ t₂ : Set X
h₁ : s₁ ∈ 𝓝ˢ t₁
h₂ : s₂ ∈ 𝓝ˢ t₂
⊢ s₁ ∪ s₂ ∈ 𝓝ˢ t₁ ⊔ 𝓝ˢ t₂

Tactic:
exact union_mem_sup h₁ h₂

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
x✝ : ℕ
⊢ Disjoint (closure[inst✝] ((fun x ↦ univ) x✝)) ∅

Tactic:
apply disjoint_empty

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace X
inst✝ : IndiscreteTopology Y
f : X → Y
hf : IsInducing f
⊢ inst✝¹ = ⊤

Tactic:
cases IndiscreteTopology.eq_top Y

Goal state after:
case refl
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
f : X → Y
inst✝ : IndiscreteTopology Y
hf : IsInducing f
⊢ inst✝¹ = ⊤
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen[inst✝] s
⊢ IsOpen[inst✝] (id '' s)

Tactic:
image_id

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen[inst✝] s
⊢ IsOpen[inst✝] s
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsClosed[inst✝] s
⊢ IsClosed[inst✝] (id '' s)

Tactic:
image_id

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsClosed[inst✝] s
⊢ IsClosed[inst✝] s
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
ι : Sort u_5
inst✝ : Finite ι
s : ι → Set α
a : α
⊢ 𝓝[⋃₀ range s] a = ⨆ i, 𝓝[s i] a

Tactic:
nhdsWithin_sUnion (finite_range s),

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
ι : Sort u_5
inst✝ : Finite ι
s : ι → Set α
a : α
⊢ ⨆ s_1 ∈ range s, 𝓝[s_1] a = ⨆ i, 𝓝[s i] a
Module: Mathlib.Topology.NhdsWithin

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

Tactic:
by
  rw [← nhdsWithin_singleton, ← nhdsWithin_union, compl_union_self, nhdsWithin_univ]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
t u : Set ↑s
⊢ u ∈ 𝓝ˢ t ↔ Subtype.val '' u ∈ 𝓝ˢ[s] (Subtype.val '' t)

Tactic:
rw [← map_nhdsSet_subtype_val, image_mem_map_iff Subtype.val_injective]

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)
⊢ Disjoint (closure[inst✝] (range f)) (range g)

Tactic:
rcases h.isClosed_iff.mp isClosed_range_inl with ⟨C, C_closed, hC⟩
  have A : closure (range f) ⊆ C := by
    rw [C_closed.closure_subset_iff, ← elim_comp_inl f g, range_comp, image_subset_iff, hC]
  have B : Disjoint C (range g) := by
    rw [← image_univ, disjoint_image_right, ← elim_comp_inr f g, preimage_comp, hC,
        ← disjoint_image_right, ← image_univ]
    exact disjoint_image_inl_image_inr
  exact B.mono_left A

Goal state after:
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: α : Type u_1
f : ℕ → Set α
n : ℕ
x✝ : α
⊢ x✝ ∈ (partialSups f) n ↔ x✝ ∈ accumulate f n

Tactic:
simp [partialSups_eq_sup_range, accumulate, Nat.lt_succ_iff]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
i : ι
⊢ IsOpenMap (eval i)

Tactic:
refine (isTopologicalBasis_pi fun _ ↦ isTopologicalBasis_opens).isOpenMap_iff.2 ?_

Goal state after:
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
i : ι
⊢ ∀ s ∈ {S | ∃ U F, (∀ i ∈ F, U i ∈ {U | IsOpen[inst✝ i] U}) ∧ S = (↑F).pi U}, IsOpen[inst✝ i] (eval i '' s)
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
ι : Type u_1
s : ι → Set α
H : ∀ (i : ι), IsOpen[t] (s i)
B : Set (Set α) := {b | b ∈ countableBasis α ∧ ∃ i, b ⊆ s i}
f : ↑B → ι
hf : ∀ (b : ↑B), ↑b ⊆ s (f b)
⊢ ∃ T, T.Countable ∧ ⋃ i ∈ T, s i = ⋃ i, s i

Tactic:
have : Countable B := ((countable_countableBasis α).mono (sep_subset _ _)).to_subtype

Goal state after:
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
ι : Type u_1
s : ι → Set α
H : ∀ (i : ι), IsOpen[t] (s i)
B : Set (Set α) := {b | b ∈ countableBasis α ∧ ∃ i, b ⊆ s i}
f : ↑B → ι
hf : ∀ (b : ↑B), ↑b ⊆ s (f b)
this : Countable ↑B
⊢ ∃ T, T.Countable ∧ ⋃ i ∈ T, s i = ⋃ i, s i
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
⊢ ∃ K', IsCompact K' ∧ K ⊆ interior K'

Tactic:
choose s hc hmem using fun x : X ↦ exists_compact_mem_nhds x
  rcases hK.elim_nhds_subcover _ fun x _ ↦ interior_mem_nhds.2 (hmem x) with ⟨I, -, hIK⟩
  refine ⟨⋃ x ∈ I, s x, I.isCompact_biUnion fun _ _ ↦ hc _, hIK.trans ?_⟩
  exact iUnion₂_subset fun x hx ↦ interior_mono <| subset_iUnion₂ (s := fun x _ ↦ s x) x hx

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
e : ι' ≃ ι
h : LocallyFinite (f ∘ ⇑e)
⊢ LocallyFinite f

Tactic:
by simpa only [comp_def, e.apply_symm_apply] using h.comp_injective e.symm.injective

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
hs : IsSigmaCompact s
hf : ContinuousOn f s
⊢ IsSigmaCompact (f '' s)

Tactic:
by
  rcases hs with ⟨K, hcompact, hcov⟩
  refine ⟨fun n ↦ f '' K n, ?_, hcov.symm ▸ image_iUnion.symm⟩
  exact fun n ↦ (hcompact n).image_of_continuousOn (hf.mono (hcov.symm ▸ subset_iUnion K n))

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

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

Tactic:
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 inr.refine_1
X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y
s t : Set X✝
inst✝³ : SigmaCompactSpace X✝
inst✝² : Countable ι
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), SigmaCompactSpace (X i)
h✝ : Nonempty ι
f : ℕ → ι
hf : Function.Surjective f
n : ℕ
⊢ IsCompact ((fun n ↦ ⋃ k, ⋃ (_ : k ≤ n), Sigma.mk (f k) '' compactCovering (X (f k)) n) n)

pp: case inr.refine_2
X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y
s t : Set X✝
inst✝³ : SigmaCompactSpace X✝
inst✝² : Countable ι
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), SigmaCompactSpace (X i)
h✝ : Nonempty ι
f : ℕ → ι
hf : Function.Surjective f
⊢ ⋃ n, (fun n ↦ ⋃ k, ⋃ (_ : k ≤ n), Sigma.mk (f k) '' compactCovering (X (f k)) n) n = univ

Tactic:
· refine (finite_le_nat _).isCompact_biUnion fun k _ => ?_
      exact (isCompact_compactCovering _ _).image continuous_sigmaMk

Goal state after:
case inr.refine_2
X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y
s t : Set X✝
inst✝³ : SigmaCompactSpace X✝
inst✝² : Countable ι
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), SigmaCompactSpace (X i)
h✝ : Nonempty ι
f : ℕ → ι
hf : Function.Surjective f
⊢ ⋃ n, (fun n ↦ ⋃ k, ⋃ (_ : k ≤ n), Sigma.mk (f k) '' compactCovering (X (f k)) n) n = univ
Module: Mathlib.Order.UpperLower.CompleteLattice

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝ : LE α
s t : UpperSet α
h : s.carrier = t.carrier
⊢ s = t

Tactic:
cases s

Goal state after:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝ : LE α
t : UpperSet α
carrier✝ : Set α
upper'✝ : IsUpperSet carrier✝
h : { carrier := carrier✝, upper' := upper'✝ }.carrier = t.carrier
⊢ { carrier := carrier✝, upper' := upper'✝ } = t
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: case refine_1
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hst : tᶜ ⊆ s
htcl : IsClosed[inst✝] t
htco : IsCompact t
⊢ IsCompact (closure[inst✝] sᶜ)

Tactic:
exact htco.of_isClosed_subset isClosed_closure <|
      closure_minimal (compl_subset_comm.2 hst) htcl

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
tfae_1_to_2 : x ⤳ y → pure x ≤ 𝓝 y
tfae_2_to_3 : pure x ≤ 𝓝 y → ∀ (s : Set X), IsOpen[inst✝] s → y ∈ s → x ∈ s
tfae_3_to_4 : (∀ (s : Set X), IsOpen[inst✝] s → y ∈ s → x ∈ s) → ∀ (s : Set X), IsClosed[inst✝] s → x ∈ s → y ∈ s
tfae_4_to_5 : (∀ (s : Set X), IsClosed[inst✝] s → x ∈ s → y ∈ s) → y ∈ closure[inst✝] {x}
tfae_6_iff_5 : closure[inst✝] {y} ⊆ closure[inst✝] {x} ↔ y ∈ closure[inst✝] {x}
tfae_5_iff_7 : y ∈ closure[inst✝] {x} ↔ ClusterPt y (pure x)
⊢ [x ⤳ y, pure x ≤ 𝓝 y, ∀ (s : Set X), IsOpen[inst✝] s → y ∈ s → x ∈ s,
      ∀ (s : Set X), IsClosed[inst✝] s → x ∈ s → y ∈ s, y ∈ closure[inst✝] {x}, closure[inst✝] {y} ⊆ closure[inst✝] {x},
      ClusterPt y (pure x)].TFAE

Tactic:
tfae_have 5 → 1 := by
    refine fun h => (nhds_basis_opens _).ge_iff.2 ?_
    rintro s ⟨hy, ho⟩
    rcases mem_closure_iff.1 h s ho hy with ⟨z, hxs, rfl : z = x⟩
    exact ho.mem_nhds hxs

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
tfae_1_to_2 : x ⤳ y → pure x ≤ 𝓝 y
tfae_2_to_3 : pure x ≤ 𝓝 y → ∀ (s : Set X), IsOpen[inst✝] s → y ∈ s → x ∈ s
tfae_3_to_4 : (∀ (s : Set X), IsOpen[inst✝] s → y ∈ s → x ∈ s) → ∀ (s : Set X), IsClosed[inst✝] s → x ∈ s → y ∈ s
tfae_4_to_5 : (∀ (s : Set X), IsClosed[inst✝] s → x ∈ s → y ∈ s) → y ∈ closure[inst✝] {x}
tfae_6_iff_5 : closure[inst✝] {y} ⊆ closure[inst✝] {x} ↔ y ∈ closure[inst✝] {x}
tfae_5_iff_7 : y ∈ closure[inst✝] {x} ↔ ClusterPt y (pure x)
tfae_5_to_1 : y ∈ closure[inst✝] {x} → x ⤳ y
⊢ [x ⤳ y, pure x ≤ 𝓝 y, ∀ (s : Set X), IsOpen[inst✝] s → y ∈ s → x ∈ s,
      ∀ (s : Set X), IsClosed[inst✝] s → x ∈ s → y ∈ s, y ∈ closure[inst✝] {x}, closure[inst✝] {y} ⊆ closure[inst✝] {x},
      ClusterPt y (pure x)].TFAE
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
hs : IsCompact (f '' s)
F : Filter X
F_ne_bot : F.NeBot
F_le : F ≤ 𝓟 s
⊢ ∃ x ∈ s, ClusterPt x F

Tactic:
obtain ⟨_, ⟨x, x_in : x ∈ s, rfl⟩, hx : ClusterPt (f x) (map f F)⟩ :=
    hs ((map_mono F_le).trans_eq map_principal)

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
hs : IsCompact (f '' s)
F : Filter X
F_ne_bot : F.NeBot
F_le : F ≤ 𝓟 s
x : X
x_in : x ∈ s
hx : ClusterPt (f x) (map f F)
⊢ ∃ x ∈ s, ClusterPt x F
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ IsClosed (range mk)

Tactic:
range_mk

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ IsClosed univ
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ NoncompactSpace (X × Y) ↔ NoncompactSpace X ∧ Nonempty Y ∨ Nonempty X ∧ NoncompactSpace Y

Tactic:
by
  simp [← Filter.cocompact_neBot_iff, ← Filter.coprod_cocompact, Filter.coprod_neBot_iff]

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

Goal state before:
pp: case a
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, (↑t).Nonempty → IsOpen[inst✝¹] ↑t → ∃ x ∈ ↑t, IsOpen[inst✝¹] {x}
hne : (↑s).Nonempty
ho : IsOpen[inst✝¹] ↑s
⊢ ∃ x ∈ ↑s, IsOpen[inst✝¹] {x}

Tactic:
rcases em (∃ t, t ⊂ s ∧ t.Nonempty ∧ IsOpen (t : Set X)) with (⟨t, hts, htne, hto⟩ | ht)

Goal state after:
case a.inl
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, (↑t).Nonempty → IsOpen[inst✝¹] ↑t → ∃ x ∈ ↑t, IsOpen[inst✝¹] {x}
hne : (↑s).Nonempty
ho : IsOpen[inst✝¹] ↑s
t : Finset X
hts : t ⊂ s
htne : t.Nonempty
hto : IsOpen[inst✝¹] ↑t
⊢ ∃ x ∈ ↑s, IsOpen[inst✝¹] {x}

case a.inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, (↑t).Nonempty → IsOpen[inst✝¹] ↑t → ∃ x ∈ ↑t, IsOpen[inst✝¹] {x}
hne : (↑s).Nonempty
ho : IsOpen[inst✝¹] ↑s
ht : ¬∃ t ⊂ s, t.Nonempty ∧ IsOpen[inst✝¹] ↑t
⊢ ∃ x ∈ ↑s, IsOpen[inst✝¹] {x}
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: case h.refine_2
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}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty { U // U ∈ c }
U₀compl : Sᶜ ⊆ U₀
⊢ IsOpen[inst✝¹] (⋃₀ c)

Tactic:
exact isOpen_sUnion fun _ h => (hc h).2.1

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

Goal state before:
pp: case pos
α : Type u_1
s : Set α
t : Set Bool
h✝¹ : true ∈ t
h✝ : false ∈ t
⊢ s ∪ sᶜ = univ ∨ s ∪ sᶜ = s ∨ s ∪ sᶜ = sᶜ ∨ s ∪ sᶜ = ∅

Tactic:
simp [s.union_compl_self]

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

Goal state before:
pp: case neg
α : Type u_1
s : Set α
t : Set Bool
h✝¹ : true ∈ t
h✝ : ¬false ∈ t
⊢ s ∪ ∅ = univ ∨ s ∪ ∅ = s ∨ s ∪ ∅ = sᶜ ∨ s ∪ ∅ = ∅

Tactic:
simp [s.union_compl_self]

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

Goal state before:
pp: case pos
α : Type u_1
s : Set α
t : Set Bool
h✝¹ : ¬true ∈ t
h✝ : false ∈ t
⊢ ∅ ∪ sᶜ = univ ∨ ∅ ∪ sᶜ = s ∨ ∅ ∪ sᶜ = sᶜ ∨ ∅ ∪ sᶜ = ∅

Tactic:
simp [s.union_compl_self]

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

Goal state before:
pp: case neg
α : Type u_1
s : Set α
t : Set Bool
h✝¹ : ¬true ∈ t
h✝ : ¬false ∈ t
⊢ ∅ ∪ ∅ = univ ∨ ∅ ∪ ∅ = s ∨ ∅ ∪ ∅ = sᶜ ∨ ∅ ∪ ∅ = ∅

Tactic:
simp [s.union_compl_self]

Goal state after:
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : PartialOrder α
t : OrderClosedTopology α
⊢ IsClosed[instTopologicalSpaceProd] (diagonal α)

Tactic:
simpa only [diagonal, le_antisymm_iff] using!
      t.isClosed_le'.inter (isClosed_le continuous_snd continuous_fst)

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

Goal state before:
pp: case neg
X : Type u_3
T : Set (TopologicalSpace X)
hT : ∀ t ∈ T, R1Space X
x✝ : TopologicalSpace X := sInf T
x y : X
hTd : ∀ t ∈ T, ¬Disjoint (𝓝 x) (𝓝 y)
⊢ ⨅ t ∈ T, 𝓝 x ≤ ⨅ t ∈ T, 𝓝 y ∨ Disjoint (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y)

Tactic:
· exact .inl <| iInf₂_mono fun t ht ↦ ((hT t ht).1 x y).resolve_right (hTd t ht)

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

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝¹ : CountableInterFilter l✝
l : Filter β
inst✝ : CountableInterFilter l
f : α → β
⊢ CountableInterFilter (comap f l)

Tactic:
by
  refine ⟨fun S hSc hS => ?_⟩
  choose! t htl ht using hS
  have : (⋂ s ∈ S, t s) ∈ l := (countable_bInter_mem hSc).2 htl
  refine ⟨_, this, ?_⟩
  simpa [preimage_iInter] using iInter₂_mono ht

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
H : IsPreconnected s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst✝¹] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen[inst✝¹] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
huv : s ⊆ u' ∪ v'
⊢ (s ∩ (u' ∩ v')).Nonempty

Tactic:
refine H u' v' hu' hv' huv ⟨x, ?_⟩ ⟨y, ?_⟩ <;> rw [inter_comm]

Goal state after:
case refine_1
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
H : IsPreconnected s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst✝¹] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen[inst✝¹] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
huv : s ⊆ u' ∪ v'
⊢ x ∈ u' ∩ s

case refine_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
H : IsPreconnected s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst✝¹] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen[inst✝¹] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
huv : s ⊆ u' ∪ v'
⊢ y ∈ v' ∩ s
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case h
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
x✝ y : α
hx✝ : x✝ ∈ s
hy : y ∈ s
Q : ↑s → ↑s → Prop := fun a b ↦ P ↑a ↑b
this : PreconnectedSpace ↑s
x : α
hx : x ∈ s
Z : ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x
⊢ ∀ᶠ (y : { x // x ∈ s }) in 𝓝 ⟨x, hx⟩, Q ⟨x, hx⟩ y ∧ Q y ⟨x, hx⟩

Tactic:
rwa [nhdsWithin_eq_map_subtype_coe] at Z

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
⊢ (∀ {s : Set X} {a : X}, IsClosed[inst✝] s → a ∉ s → Disjoint (𝓝ˢ s) (𝓝 a)) ↔
    ∀ (x : X), (𝓝 x).lift' closure[inst✝] ≤ 𝓝 x

Tactic:
(@compl_surjective (Set X) _).forall,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
⊢ (∀ (x : Set X) {a : X}, IsClosed[inst✝] xᶜ → a ∉ xᶜ → Disjoint (𝓝ˢ xᶜ) (𝓝 a)) ↔
    ∀ (x : X), (𝓝 x).lift' closure[inst✝] ≤ 𝓝 x