mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inl.inl
α : Type u_1
inst✝ : PartialOrder α
a b c : α
hbc : b ≤ c
hca : c ≤ a
hcb : c ≤ b
hba : b ≤ a
⊢ a = b ∨ b = c ∨ c = a

pp: case inr.inl.inr.inl
α : Type u_1
inst✝ : PartialOrder α
a b c : α
hbc : b ≤ c
hca : c ≤ a
hba : b ≤ a
hac : a ≤ c
⊢ a = b ∨ b = c ∨ c = a

pp: case inr.inl.inr.inr
α : Type u_1
inst✝ : PartialOrder α
a b c : α
hbc : b ≤ c
hca : c ≤ a
hac : a ≤ c
hcb : c ≤ b
⊢ a = b ∨ b = c ∨ c = a

pp: case inr.inr.inl
α : Type u_1
inst✝ : PartialOrder α
a b c : α
hca : c ≤ a
hab : a ≤ b
hcb : c ≤ b
hba : b ≤ a
⊢ a = b ∨ b = c ∨ c = a

pp: case inr.inr.inr.inl
α : Type u_1
inst✝ : PartialOrder α
a b c : α
hca : c ≤ a
hab : a ≤ b
hba : b ≤ a
hac : a ≤ c
⊢ a = b ∨ b = c ∨ c = a

pp: case inr.inr.inr.inr
α : Type u_1
inst✝ : PartialOrder α
a b c : α
hca : c ≤ a
hab : a ≤ b
hac : a ≤ c
hcb : c ≤ b
⊢ a = b ∨ b = c ∨ c = a

Tactic:
· exact Or.inr (Or.inl <| hbc.antisymm hcb)

Goal state after:
case inr.inl.inr.inl
α : Type u_1
inst✝ : PartialOrder α
a b c : α
hbc : b ≤ c
hca : c ≤ a
hba : b ≤ a
hac : a ≤ c
⊢ a = b ∨ b = c ∨ c = a

case inr.inl.inr.inr
α : Type u_1
inst✝ : PartialOrder α
a b c : α
hbc : b ≤ c
hca : c ≤ a
hac : a ≤ c
hcb : c ≤ b
⊢ a = b ∨ b = c ∨ c = a

case inr.inr.inl
α : Type u_1
inst✝ : PartialOrder α
a b c : α
hca : c ≤ a
hab : a ≤ b
hcb : c ≤ b
hba : b ≤ a
⊢ a = b ∨ b = c ∨ c = a

case inr.inr.inr.inl
α : Type u_1
inst✝ : PartialOrder α
a b c : α
hca : c ≤ a
hab : a ≤ b
hba : b ≤ a
hac : a ≤ c
⊢ a = b ∨ b = c ∨ c = a

case inr.inr.inr.inr
α : Type u_1
inst✝ : PartialOrder α
a b c : α
hca : c ≤ a
hab : a ≤ b
hac : a ≤ c
hcb : c ≤ b
⊢ a = b ∨ b = c ∨ c = a
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inl.inr.inr
α : Type u_1
inst✝ : PartialOrder α
a b c : α
hbc : b ≤ c
hca : c ≤ a
hac : a ≤ c
hcb : c ≤ b
⊢ a = b ∨ b = c ∨ c = a

pp: case inr.inr.inl
α : Type u_1
inst✝ : PartialOrder α
a b c : α
hca : c ≤ a
hab : a ≤ b
hcb : c ≤ b
hba : b ≤ a
⊢ a = b ∨ b = c ∨ c = a

pp: case inr.inr.inr.inl
α : Type u_1
inst✝ : PartialOrder α
a b c : α
hca : c ≤ a
hab : a ≤ b
hba : b ≤ a
hac : a ≤ c
⊢ a = b ∨ b = c ∨ c = a

pp: case inr.inr.inr.inr
α : Type u_1
inst✝ : PartialOrder α
a b c : α
hca : c ≤ a
hab : a ≤ b
hac : a ≤ c
hcb : c ≤ b
⊢ a = b ∨ b = c ∨ c = a

Tactic:
· exact Or.inr (Or.inl <| hbc.antisymm hcb)

Goal state after:
case inr.inr.inl
α : Type u_1
inst✝ : PartialOrder α
a b c : α
hca : c ≤ a
hab : a ≤ b
hcb : c ≤ b
hba : b ≤ a
⊢ a = b ∨ b = c ∨ c = a

case inr.inr.inr.inl
α : Type u_1
inst✝ : PartialOrder α
a b c : α
hca : c ≤ a
hab : a ≤ b
hba : b ≤ a
hac : a ≤ c
⊢ a = b ∨ b = c ∨ c = a

case inr.inr.inr.inr
α : Type u_1
inst✝ : PartialOrder α
a b c : α
hca : c ≤ a
hab : a ≤ b
hac : a ≤ c
hcb : c ≤ b
⊢ a = b ∨ b = c ∨ c = a
Module: Mathlib.Order.Circular

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ btw a b c ∨ btw c b a

Tactic:
by
      rcases le_total a b with hab | hba <;> rcases le_total b c with hbc | hcb <;>
        rcases le_total c a with hca | hac
      · exact Or.inl (Or.inl ⟨hab, hbc⟩)
      · exact Or.inl (Or.inl ⟨hab, hbc⟩)
      · exact Or.inl (Or.inr <| Or.inr ⟨hca, hab⟩)
      · exact Or.inr (Or.inr <| Or.inr ⟨hac, hcb⟩)
      · exact Or.inl (Or.inr <| Or.inl ⟨hbc, hca⟩)
      · exact Or.inr (Or.inr <| Or.inl ⟨hba, hac⟩)
      · exact Or.inr (Or.inl ⟨hcb, hba⟩)
      · exact Or.inr (Or.inr <| Or.inl ⟨hba, hac⟩)

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.ModEq

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
a b p : G
⊢ a ≡ b [PMOD p] ↔ ↑a = ↑b

Tactic:
rw [modEq_comm]

Goal state after:
G : Type u_1
inst✝ : AddCommGroup G
a b p : G
⊢ b ≡ a [PMOD p] ↔ ↑a = ↑b
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
⊢ 0 < ∏ i ∈ n.primeFactors, i

Tactic:
prod_primeFactors_prod_factorization

Goal state after:
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
⊢ 0 < n.factorization.prod fun p x ↦ p
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 : ℤ
⊢ toIcoMod hp a (b + ↑m * p) = toIcoMod hp a b

Tactic:
by
  simpa using toIcoMod_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
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
s : Set Y
⊢ IsClosed[inst✝¹] (⇑h ⁻¹' s) ↔ IsClosed[inst✝] s

Tactic:
by
  simp only [← isOpen_compl_iff, ← preimage_compl, isOpen_preimage]

Goal state after:
Module: Mathlib.Topology.Bases

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

Tactic:
let := generateFrom s

Goal state after:
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
⊢ IsTopologicalBasis ((fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s})
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
s : Set X
t : Set Y
H : MapsTo f s t
hs : IsOpen[inst✝¹] s
⊢ IsOpen[instTopologicalSpaceSubtype] (range (MapsTo.restrict f s t H))

Tactic:
rw [MapsTo.range_restrict]
    exact continuous_subtype_val.1 _ (hf.isOpenMap _ hs)

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
hf : IsInducing f
hg : IsInducing g
hFg : Disjoint (𝓟 (range f)) (𝓝ˢ (range g))
hfG : Disjoint (𝓝ˢ (range f)) (𝓟 (range g))
x : X ⊕ Y
⊢ comap (Sum.elim f g) (𝓝 (Sum.elim f g x)) ≤ 𝓝 x

Tactic:
obtain x | x := x <;>
  simp only [comap_sumElim_eq, nhds_inl, nhds_inr, elim_inl, elim_inr, ← hf.nhds_eq_comap,
    ← hg.nhds_eq_comap, sup_le_iff, le_rfl, true_and, and_true] <;>
  convert! bot_le (α := Filter (X ⊕ Y))

Goal state after:
case e'_3
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
hf : IsInducing f
hg : IsInducing g
hFg : Disjoint (𝓟 (range f)) (𝓝ˢ (range g))
hfG : Disjoint (𝓝ˢ (range f)) (𝓟 (range g))
x : X
⊢ map inr (comap g (𝓝 (f x))) = ⊥

case e'_3
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
hf : IsInducing f
hg : IsInducing g
hFg : Disjoint (𝓟 (range f)) (𝓝ˢ (range g))
hfG : Disjoint (𝓝ˢ (range f)) (𝓟 (range g))
x : Y
⊢ map inl (comap f (𝓝 (g x))) = ⊥
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
B : ι → Type u_7
T : (i : ι) → TopologicalSpace (A i)
inst✝ : (i : ι) → TopologicalSpace (B i)
f : (i : ι) → A i → B i
hf : ∀ (i : ι), IsInducing (f i)
⊢ IsInducing (Pi.map f)

Tactic:
simp [isInducing_iff_nhds, nhds_pi, (hf _).nhds_eq_comap, Filter.pi_comap]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
β : Type u_1
t✝ : TopologicalSpace α
B : Set (Set α)
s : Set α
ι : Type u_2
X : ι → Type u_3
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), SeparableSpace (X i)
inst✝ : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), (t x).Countable
htd : ∀ (x : ι), Dense (t x)
this✝ : ∀ (i : ι), Countable ↑(t i)
a✝ : Nontrivial ((i : ι) → X i)
inhabited_h : Inhabited ((i : ι) → X i)
f : (I : Finset ι) × ((i : ↥I) → ↑(t ↑i)) → (i : ι) → X i :=
  fun x i ↦
    match x with
    | ⟨I, g⟩ => if hi : i ∈ I then ↑(g ⟨i, hi⟩) else default i
U : Set ((i : ι) → X i)
hU : IsOpen[Pi.topologicalSpace] U
x✝ : U.Nonempty
g : (i : ι) → X i
hg : g ∈ U
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen[inst✝² a] (u a) ∧ g a ∈ u a
huU : (↑I).pi u ⊆ U
this : ∀ (i : ↥I), ∃ y ∈ t ↑i, y ∈ u ↑i
⊢ (U ∩ range f).Nonempty

Tactic:
choose y hyt hyu using this

Goal state after:
α : Type u
β : Type u_1
t✝ : TopologicalSpace α
B : Set (Set α)
s : Set α
ι : Type u_2
X : ι → Type u_3
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), SeparableSpace (X i)
inst✝ : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), (t x).Countable
htd : ∀ (x : ι), Dense (t x)
this : ∀ (i : ι), Countable ↑(t i)
a✝ : Nontrivial ((i : ι) → X i)
inhabited_h : Inhabited ((i : ι) → X i)
f : (I : Finset ι) × ((i : ↥I) → ↑(t ↑i)) → (i : ι) → X i :=
  fun x i ↦
    match x with
    | ⟨I, g⟩ => if hi : i ∈ I then ↑(g ⟨i, hi⟩) else default i
U : Set ((i : ι) → X i)
hU : IsOpen[Pi.topologicalSpace] U
x✝ : U.Nonempty
g : (i : ι) → X i
hg : g ∈ U
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen[inst✝² a] (u a) ∧ g a ∈ u a
huU : (↑I).pi u ⊆ U
y : (i : ↥I) → X ↑i
hyt : ∀ (i : ↥I), y i ∈ t ↑i
hyu : ∀ (i : ↥I), y i ∈ u ↑i
⊢ (U ∩ range f).Nonempty
Module: Mathlib.Order.ZornAtoms

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : ∀ (c : Set α), IsChain (fun x1 x2 ↦ x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ x, x ≠ ⊤ ∧ x ∈ upperBounds c
⊢ IsCoatomic α

Tactic:
refine ⟨fun x => le_top.eq_or_lt.imp_right fun hx => ?_⟩
  have := zorn_le_nonempty₀ (Ico x ⊤) (fun c hxc hc y hy => ?_) x (left_mem_Ico.2 hx)
  · obtain ⟨y, hxy, hmax⟩ := this
    refine ⟨y, ⟨hmax.prop.2.ne, fun z hyz ↦ le_top.eq_or_lt.resolve_right fun hz => ?_⟩, hxy⟩
    exact hyz.ne <| hmax.eq_of_le ⟨hxy.trans hyz.le, hz⟩ hyz.le
  rcases h c hc ⟨y, hy⟩ fun h => (hxc h).2.ne rfl with ⟨z, hz, hcz⟩
  exact ⟨z, ⟨le_trans (hxc hy).1 (hcz hy), hz.lt_top⟩, hcz⟩

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u_1
β : Type u_2
t : TopologicalSpace β
inst✝ : SecondCountableTopology β
f : α → β
b : Set (Set β)
hb : b.Countable
eq : t = generateFrom b
this : TopologicalSpace α := induced f t
⊢ induced f t = generateFrom (preimage f '' b)

Tactic:
eq,

Goal state after:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
inst✝ : SecondCountableTopology β
f : α → β
b : Set (Set β)
hb : b.Countable
eq : t = generateFrom b
this : TopologicalSpace α := induced f t
⊢ induced f (generateFrom b) = generateFrom (preimage f '' b)
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
⊢ IsClosed[inst✝] (range ULift.down)

Tactic:
simp only [ULift.down_surjective.range_eq, isClosed_univ]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LocallyCompactPair X Y
f : X → Y
K : Set X
U : Set Y
hf : Continuous[inst✝², inst✝¹] f
hK : IsCompact K
hU : IsOpen[inst✝¹] U
hKU : MapsTo f K U
V : X → Set X
hxV : ∀ x ∈ K, V x ∈ 𝓝 x
hVc : ∀ x ∈ K, IsCompact (V x)
hVU : ∀ x ∈ K, MapsTo f (V x) U
s : Finset X
hsK : ∀ x ∈ s, x ∈ K
hKs : ⋃ x ∈ s, V x ∈ 𝓝ˢ K
⊢ ∃ L ∈ 𝓝ˢ K, IsCompact L ∧ MapsTo f L U

Tactic:
exact ⟨_, hKs, s.isCompact_biUnion fun x hx ↦ hVc x (hsK x hx), mapsTo_iUnion₂.2 fun x hx ↦
    hVU x (hsK x hx)⟩

Goal state after:
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure[inst✝¹] (f i), ContinuousWithinAt g (f i) x
x : X
⊢ Tendsto g (𝓝[⋃ i, f i] x) (𝓝 (g x))

Tactic:
hf.nhdsWithin_iUnion,

Goal state after:
ι : Type u_1
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure[inst✝¹] (f i), ContinuousWithinAt g (f i) x
x : X
⊢ Tendsto g (⨆ i, 𝓝[f i] x) (𝓝 (g x))
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: X : Type u_4
inst✝ : TopologicalSpace X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : X → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), {i | ((fun n ↦ {x | f (n + 1) x ≠ f n x}) i ∩ U x).Nonempty}.Finite
⊢ ∃ F, ∀ (x : X), ∀ᶠ (p : ℕ × X) in atTop ×ˢ 𝓝 x, f p.1 p.2 = F p.2

Tactic:
choose N hN using fun x => (hU x).bddAbove

Goal state after:
X : Type u_4
inst✝ : TopologicalSpace X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : X → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), {i | ((fun n ↦ {x | f (n + 1) x ≠ f n x}) i ∩ U x).Nonempty}.Finite
N : X → ℕ
hN : ∀ (x : X), N x ∈ upperBounds {i | ((fun n ↦ {x | f (n + 1) x ≠ f n x}) i ∩ U x).Nonempty}
⊢ ∃ F, ∀ (x : X), ∀ᶠ (p : ℕ × X) in atTop ×ˢ 𝓝 x, f p.1 p.2 = F p.2
Module: Mathlib.Topology.Compactness.LocallyFinite

Goal state before:
pp: X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
s : Set X
f : ι → Set X
hf : LocallyFinite f
hs : IsCompact s
⊢ {i | (f i ∩ s).Nonempty}.Finite

Tactic:
choose U hxU hUf using hf
  rcases hs.elim_nhds_subcover U fun x _ => hxU x with ⟨t, -, hsU⟩
  refine (t.finite_toSet.biUnion fun x _ => hUf x).subset ?_
  rintro i ⟨x, hx⟩
  rcases mem_iUnion₂.1 (hsU hx.2) with ⟨c, hct, hcx⟩
  exact mem_biUnion hct ⟨x, hx.1, hcx⟩

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun x1 x2 ↦ x1 ⊇ x2) t
htn : ∀ (i : ι), (t i).Nonempty
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed[inst✝] (t i)
i₀ : ι := hι.some
this : (t i₀ ∩ ⋂ i, t i).Nonempty
⊢ (⋂ i, t i).Nonempty

Tactic:
rwa [inter_eq_right.mpr (iInter_subset _ i₀)] at this

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace Y
f g : X → Y
l : Filter X
y : Y
h : ∀ (s : Set Y), IsOpen[inst✝] s → y ∈ s → g ⁻¹' s ∈ l
hl : ∀ (x : X) (s : Set Y), IsOpen[inst✝] s → g x ∈ s → f x ∈ s
⊢ ∀ (s : Set Y), IsOpen[inst✝] s → y ∈ s → f ⁻¹' s ∈ l

Tactic:
refine fun s ho hy => mem_of_superset (h s ho hy) fun x hx => ?_

Goal state after:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace Y
f g : X → Y
l : Filter X
y : Y
h : ∀ (s : Set Y), IsOpen[inst✝] s → y ∈ s → g ⁻¹' s ∈ l
hl : ∀ (x : X) (s : Set Y), IsOpen[inst✝] s → g x ∈ s → f x ∈ s
s : Set Y
ho : IsOpen[inst✝] s
hy : y ∈ s
x : X
hx : x ∈ g ⁻¹' s
⊢ x ∈ f ⁻¹' s
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:
rw [specializes_iff_forall_open]
  push Not
  rfl

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

Goal state before:
pp: case right
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
u : Set ((i : ι) × X i)
hu : IsCompact u
s : Finset ι
hs : u ⊆ ⋃ i ∈ s, Sigma.mk i '' Sigma.mk i ⁻¹' univ
⊢ ((↑s).sigma fun i ↦ Sigma.mk i ⁻¹' u) = u

Tactic:
· ext x
    simp only [Set.mem_sigma_iff, Finset.mem_coe, Set.mem_preimage, and_iff_right_iff_imp]
    intro hx
    obtain ⟨i, hi⟩ := Set.mem_iUnion.mp (hs hx)
    simp_all

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsDiscrete s ↔ ∀ x ∈ s, 𝓝[s] x = pure x

Tactic:
by
  simp [isDiscrete_iff_discreteTopology, discreteTopology_iff_isOpen_singleton,
    isOpen_singleton_iff_nhds_eq_pure, nhds_induced,
    ← (Filter.map_injective Subtype.val_injective).eq_iff,
    Filter.map_comap, nhdsWithin]

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace Y
f : X → Y
⊢ Tendsto f cofinite (cocompact Y) ↔ ∀ (K : Set Y), IsCompact K → (f ⁻¹' K).Finite

Tactic:
by
  rw [hasBasis_cocompact.tendsto_right_iff]
  refine forall₂_congr (fun K _ ↦ ?_)
  simp only [mem_compl_iff, eventually_cofinite, not_not, preimage]

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S T : Set X
⊢ (∀ i ∈ T, ∃ u, IsOpen[inst✝] u ∧ i ∈ u ∧ ∀ (x : X), x ∈ u ∧ x ∈ T ∧ x ∉ {i} → x ∈ S) ↔
    ∀ x ∈ T, ∃ u, IsOpen[inst✝] u ∧ x ∈ u ∧ ∀ (x_1 : X), x_1 ∈ u ∧ x_1 ∉ {x} → ¬(x_1 ∈ T ∧ x_1 ∉ S)

Tactic:
congr! 7 with x - u y

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
S T : Set X
x : X
u : Set X
y : X
⊢ y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S ↔ y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
h : IsPreirreducible S
x✝ : Set X
⊢ IsOpen[inst✝] x✝ → (S ∩ x✝).Nonempty → S ⊆ closure[inst✝] (S ∩ x✝)

Tactic:
exact subset_closure_inter_of_isPreirreducible_of_isOpen h

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
U s : Set X
hU : U ∈ 𝓝[≠] x
hs : Finite ↑s
⊢ U \ s ∈ 𝓝[≠] x

Tactic:
rw [mem_nhdsWithin] at hU ⊢
  obtain ⟨t, ht, h₁ts, h₂ts⟩ := hU
  use t \ (s \ {x})
  constructor
  · rw [← isClosed_compl_iff, compl_sdiff]
    exact s.toFinite.sdiff.isClosed.union (isClosed_compl_iff.2 ht)
  · tauto_set

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 Y
f : X → Y
s : Set X
x : X
c : Y
h : ContinuousWithinAt f s x
hx : x ∈ closure[inst✝²] s
ht : ∀ y ∈ s, f y = c
⊢ f x = c

Tactic:
← Set.mem_singleton_iff,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space Y
f : X → Y
s : Set X
x : X
c : Y
h : ContinuousWithinAt f s x
hx : x ∈ closure[inst✝²] s
ht : ∀ y ∈ s, f y = c
⊢ f x ∈ {c}
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsDiscrete s
x : X
hx : x ∈ s
U : Set X
hU_nhds : U ∈ 𝓝 x
hU_inter : U ∩ s = {x}
⊢ ∃ U, IsOpen[inst✝] U ∧ U ∩ s = {x}

Tactic:
obtain ⟨t, ht_sub, ht_open, ht_x⟩ := mem_nhds_iff.mp hU_nhds

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsDiscrete s
x : X
hx : x ∈ s
U : Set X
hU_nhds : U ∈ 𝓝 x
hU_inter : U ∩ s = {x}
t : Set X
ht_sub : t ⊆ U
ht_open : IsOpen[inst✝] t
ht_x : x ∈ t
⊢ ∃ U, IsOpen[inst✝] U ∧ U ∩ s = {x}
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
t : OrderClosedTopology α
inst✝ : Preorder β
⊢ IsClosed[Pi.topologicalSpace] {f | Monotone f}

Tactic:
simp_rw [← monotoneOn_univ]

Goal state after:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
t : OrderClosedTopology α
inst✝ : Preorder β
⊢ IsClosed[Pi.topologicalSpace] {f | MonotoneOn f univ}
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : R1Space Y
f : X → Y
x : X
K : Set X
s : Set Y
hf : Continuous[inst✝², inst✝¹] f
hs : s ∈ 𝓝 (f x)
hKc : IsCompact K
hKx : K ∈ 𝓝 x
hc : IsCompact (f '' K \ interior s)
y : Y
hys : y ∉ interior s
hxy : Inseparable (f x) y
⊢ False

Tactic:
refine hys <| (hxy.mem_open_iff isOpen_interior).1 ?_

Goal state after:
X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : R1Space Y
f : X → Y
x : X
K : Set X
s : Set Y
hf : Continuous[inst✝², inst✝¹] f
hs : s ∈ 𝓝 (f x)
hKc : IsCompact K
hKx : K ∈ 𝓝 x
hc : IsCompact (f '' K \ interior s)
y : Y
hys : y ∉ interior s
hxy : Inseparable (f x) y
⊢ f x ∈ interior s
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : R1Space Y
f : X → Y
x : X
K : Set X
s : Set Y
hf : Continuous[inst✝², inst✝¹] f
hs : s ∈ 𝓝 (f x)
hKc : IsCompact K
hKx : K ∈ 𝓝 x
hc : IsCompact (f '' K \ interior s)
⊢ ∃ L ∈ 𝓝 x, IsCompact L ∧ MapsTo f L s

Tactic:
obtain ⟨U, V, Uo, Vo, hxU, hV, hd⟩ : SeparatedNhds {f x} (f '' K \ interior s) := by
    simp_rw [separatedNhds_iff_disjoint, nhdsSet_singleton, hc.disjoint_nhdsSet_right,
      disjoint_nhds_nhds_iff_not_inseparable]
    rintro y ⟨-, hys⟩ hxy
    refine hys <| (hxy.mem_open_iff isOpen_interior).1 ?_
    rwa [mem_interior_iff_mem_nhds]

Goal state after:
X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : R1Space Y
f : X → Y
x : X
K : Set X
s : Set Y
hf : Continuous[inst✝², inst✝¹] f
hs : s ∈ 𝓝 (f x)
hKc : IsCompact K
hKx : K ∈ 𝓝 x
hc : IsCompact (f '' K \ interior s)
U V : Set Y
Uo : IsOpen[inst✝¹] U
Vo : IsOpen[inst✝¹] V
hxU : {f x} ⊆ U
hV : f '' K \ interior s ⊆ V
hd : Disjoint U V
⊢ ∃ L ∈ 𝓝 x, IsCompact L ∧ MapsTo f L s
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
f : β → α
l : Filter β
a : α
h : Tendsto f l (𝓝 a)
⊢ Tendsto (fun i ↦ max a (f i)) l (𝓝 a)

Tactic:
exact h.max_right

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

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : IsPreconnected s
u v : Set α
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hs : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
isPreconnected_closed_iff

Goal state after:
case mp
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h :
  ∀ (t t' : Set α),
    IsClosed[inst✝] t → IsClosed[inst✝] t' → s ⊆ t ∪ t' → (s ∩ t).Nonempty → (s ∩ t').Nonempty → (s ∩ (t ∩ t')).Nonempty
u v : Set α
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hs : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
⊢ s ⊆ u ∨ s ⊆ v
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case mpr
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
⊢ IsPreconnected s

Tactic:
isPreconnected_closed_iff

Goal state after:
case mpr
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
⊢ ∀ (t t' : Set α),
    IsClosed[inst✝] t → IsClosed[inst✝] t' → s ⊆ t ∪ t' → (s ∩ t).Nonempty → (s ∩ t').Nonempty → (s ∩ (t ∩ t')).Nonempty
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed[inst✝¹] s
ht : IsOpen[inst✝¹] t
hst : s ⊆ t
⊢ ∃ u, IsOpen[inst✝¹] u ∧ s ⊆ u ∧ closure[inst✝¹] u ⊆ t

Tactic:
by
  have : Disjoint s tᶜ := Set.disjoint_left.mpr fun x hxs hxt => hxt (hst hxs)
  rcases normal_separation hs (isClosed_compl_iff.2 ht) this with
    ⟨s', t', hs', ht', hss', htt', hs't'⟩
  refine ⟨s', hs', hss', Subset.trans (closure_minimal ?_ (isClosed_compl_iff.2 ht'))
    (compl_subset_comm.1 htt')⟩
  exact fun x hxs hxt => hs't'.le_bot ⟨hxs, hxt⟩

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

Goal state before:
pp: X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Countable
hf : ∀ i ∈ s, IsLindelof (f i)
⊢ IsLindelof (⋃ i ∈ s, f i)

Tactic:
apply isLindelof_of_countable_subcover
  intro i U hU hUcover
  have hiU : ∀ i ∈ s, f i ⊆ ⋃ i, U i :=
    fun _ is ↦ _root_.subset_trans (subset_biUnion_of_mem is) hUcover
  have iSets := fun i is ↦ (hf i is).elim_countable_subcover U hU (hiU i is)
  choose! r hr using iSets
  use ⋃ i ∈ s, r i
  constructor
  · refine (Countable.biUnion_iff hs).mpr ?h.left.a
    exact fun s hs ↦ (hr s hs).1
  · refine iUnion₂_subset ?h.right.h
    intro i is
    simp only [mem_iUnion, exists_prop, iUnion_exists, biUnion_and']
    intro x hx
    exact mem_biUnion is ((hr i is).2 hx)

Goal state after:
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
inst✝ : T2Space β
di : IsDenseInducing i
hd : Dense (range i)ᶜ
s : Set α
hs : IsCompact s
x : α
hx : s ∈ 𝓝 x
this : i '' s ∈ 𝓝 (i x)
y : β
hyi : y ∈ (range i)ᶜ
hys : y ∈ i '' s
⊢ False

Tactic:
exact hyi (image_subset_range _ _ hys)

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

Goal state before:
pp: case refine_2
α : Type u_3
inst✝ : TopologicalSpace α
x y : α
x✝¹ : x ≠ y
x✝ : (fun x1 x2 ↦ ∃ U, IsClopen U ∧ x1 ∈ U ∧ x2 ∈ Uᶜ) x y
U : Set α
hU : IsClopen U
Ux : x ∈ U
Ucy : y ∈ Uᶜ
⊢ ∃ u v, IsOpen[inst✝] u ∧ IsOpen[inst✝] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v

Tactic:
exact ⟨U, Uᶜ, hU.2, hU.compl.2, Ux, Ucy, (Set.union_compl_self U).ge, disjoint_compl_right⟩

Goal state after: