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

Goal state before:
pp: case coprime
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
a b : ℕ
a✝¹ : 1 < a
a✝ : 1 < b
hab : a.Coprime b
ha : a ≠ 0 → f a = a.factorization.prod fun p k ↦ f (p ^ k)
hb : b ≠ 0 → f b = b.factorization.prod fun p k ↦ f (p ^ k)
hab_pos : a * b ≠ 0
⊢ f (a * b) = (a * b).factorization.prod fun p k ↦ f (p ^ k)

Tactic:
h_mult a b hab,

Goal state after:
case coprime
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
a b : ℕ
a✝¹ : 1 < a
a✝ : 1 < b
hab : a.Coprime b
ha : a ≠ 0 → f a = a.factorization.prod fun p k ↦ f (p ^ k)
hb : b ≠ 0 → f b = b.factorization.prod fun p k ↦ f (p ^ k)
hab_pos : a * b ≠ 0
⊢ f a * f b = (a * b).factorization.prod fun p k ↦ f (p ^ k)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype (ZMod n)ˣ
⊢ Fintype.card { x // x.val.Coprime n } = φ n

Tactic:
by
      obtain ⟨m, rfl⟩ : ∃ m, n = m + 1 := exists_eq_succ_of_ne_zero NeZero.out
      simp only [totient, Finset.card_eq_sum_ones, Fintype.card_subtype, Finset.sum_filter, ←
        Fin.sum_univ_eq_sum_range, @Nat.coprime_comm (m + 1)]
      rfl

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

Goal state before:
pp: case e'_3
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) ≤ 2 * (c ^ 2 + d + 1) + d'
c0 : c > 0
⊢ c ^ (2 * (c ^ 2 + d + 1) + d') * c ^ d' = (c ^ 2) ^ (c ^ 2 + d' + d + 1)

Tactic:
rw [← pow_mul, ← pow_add]

Goal state after:
case e'_3
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) ≤ 2 * (c ^ 2 + d + 1) + d'
c0 : c > 0
⊢ c ^ (2 * (c ^ 2 + d + 1) + d' + d') = c ^ (2 * (c ^ 2 + d' + d + 1))
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: n : ℕ
hn : 0 < n
this : ∏ x ∈ n.primeFactors, x ^ φ n ∣ n ^ φ n
p : ℕ
hp : p ∈ n.primeFactors
⊢ p ^ (φ n / (p - 1)) ∣ p ^ φ n

Tactic:
exact Nat.pow_dvd_pow p <| Nat.div_le_self _ _

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 by_cases p <;> simp [*]

Goal state after:
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
p : X → Prop
⊢ IsOpen[inst✝] {x | ∀ᶠ (y : X) in 𝓝 x, p y}

Tactic:
by
  simp only [← interior_setOfPred_eq, isOpen_interior]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen s
⊢ s ∩ (closure s \ s) = ∅

Tactic:
inter_sdiff_self

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen s
⊢ ∅ = ∅
Module: Mathlib.Topology.ClusterPt

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

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

Tactic:
· rwa [mem_closure_iff_nhdsWithin_neBot]

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsClosed[inst✝] s ↔ ∀ (x : X), (∀ U ∈ 𝓝 x, (U ∩ s).Nonempty) → x ∈ s

Tactic:
by
  simp_rw [isClosed_iff_clusterPt, ClusterPt, inf_principal_neBot_iff]

Goal state after:
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsClosed[inst✝] s ↔ ∀ (x : X) (F : Filter X), F.NeBot → F ≤ 𝓟 s → F ≤ 𝓝 x → x ∈ s

Tactic:
by
  simp_rw [isClosed_iff_clusterPt]
  exact ⟨fun hs x F F_ne FS Fx ↦ hs _ <| NeBot.mono F_ne (le_inf Fx FS),
         fun hs x hx ↦ hs x (𝓝 x ⊓ 𝓟 s) hx inf_le_right inf_le_left⟩

Goal state after:
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: α : Type u_4
inst✝ : TopologicalSpace α
s : Set α
⊢ 𝓝ˢ s = ⊥ → s = ∅

Tactic:
by simp [← empty_mem_iff_bot, mem_nhdsSet_iff_forall, eq_empty_iff_forall_notMem]

Goal state after:
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:
nhdsSet_union

Goal state after:
X : Type u_2
inst✝ : TopologicalSpace X
s₁ s₂ t₁ t₂ : Set X
h₁ : s₁ ∈ 𝓝ˢ t₁
h₂ : s₂ ∈ 𝓝ˢ t₂
⊢ s₁ ∪ s₂ ∈ 𝓝ˢ t₁ ⊔ 𝓝ˢ t₂
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
h : IsClosed[inst✝] t
⊢ 𝓝ˢ (s ∩ t ∪ s ∩ tᶜ) = 𝓝ˢ (s ∩ t) ⊔ 𝓝ˢ (s ∩ tᶜ)

Tactic:
nhdsSet_union

Goal state after:
X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
h : IsClosed[inst✝] t
⊢ 𝓝ˢ (s ∩ t) ⊔ 𝓝ˢ (s ∩ tᶜ) = 𝓝ˢ (s ∩ t) ⊔ 𝓝ˢ (s ∩ tᶜ)
Module: Mathlib.Topology.Order

Goal state before:
pp: case a
α : Type u
n : α → Filter α
ι : α → Sort u_1
p : (a : α) → ι a → Prop
s : (a : α) → ι a → Set α
hb : ∀ (a : α), (n a).HasBasis (p a) (s a)
hpure : ∀ (a : α) (i : ι a), p a i → a ∈ s a i
hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x
a : α
t : TopologicalSpace α := ⋯
⊢ 𝓝 a ≤ n a

Tactic:
intro U hU

Goal state after:
case a
α : Type u
n : α → Filter α
ι : α → Sort u_1
p : (a : α) → ι a → Prop
s : (a : α) → ι a → Set α
hb : ∀ (a : α), (n a).HasBasis (p a) (s a)
hpure : ∀ (a : α) (i : ι a), p a i → a ∈ s a i
hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x
a : α
t : TopologicalSpace α := TopologicalSpace.mkOfNhds n
U : Set α
hU : U ∈ n a
⊢ U ∈ 𝓝 a
Module: Mathlib.Topology.Separation.SeparatedNhds

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s₁ s₂ t₁ t₂ : Set X
s_sub : s₁ ⊆ s₂
t_sub : t₁ ⊆ t₂
u : ℕ → Set X
u_cov : s₂ ⊆ ⋃ n, u n
u_props : ∀ (n : ℕ), IsOpen[inst✝] (u n) ∧ Disjoint (closure[inst✝] (u n)) t₂
⊢ HasSeparatingCover s₁ t₁

Tactic:
exact
    ⟨u,
     s_sub.trans u_cov,
     fun n ↦
       ⟨(u_props n).1,
        disjoint_of_subset (fun ⦃_⦄ a ↦ a) t_sub (u_props n).2⟩⟩

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_4
β : Type u_5
e : α ≃ β
t : TopologicalSpace α
U : Set β
⊢ (∃ t_1, IsOpen[t] t_1 ∧ ⇑e.symm ⁻¹' t_1 = U) ↔ IsOpen[t] (⇑e ⁻¹' U)

Tactic:
simp only [e.symm.preimage_eq_iff_eq_image, exists_eq_right, Equiv.image_symm_eq_preimage]

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 X
⊢ IsClosed[inst✝] (⇑h.symm ⁻¹' s) ↔ IsClosed[inst✝¹] s

Tactic:
isClosed_preimage

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
s : Set X
⊢ IsClosed[inst✝¹] s ↔ IsClosed[inst✝¹] 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 : IsOpenMap f
⊢ IsOpen[inst✝] (range f)

Tactic:
rw [← image_univ]

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenMap f
⊢ IsOpen[inst✝] (f '' univ)
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
open_map : IsOpenMap f
cont : Continuous[inst✝¹, inst✝] f
surj : Surjective f
⊢ IsQuotientMap f

Tactic:
by
  rw [isQuotientMap_iff]
  refine ⟨.of_isOpen_preimage_iff_isOpen fun s ↦ ?_, surj⟩
  exact ⟨fun h => surj.image_preimage s ▸ open_map _ h, fun h => h.preimage cont⟩

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 X
inst✝ : TopologicalSpace Y
⊢ (∀ {s : Set X}, kernImage f (interior s) ⊆ interior (kernImage f s)) ↔
    ∀ {s : Set Y} (x : Set X), s ⊆ kernImage f (interior x) → s ⊆ interior (kernImage f x)

Tactic:
exact ⟨fun H s t hst ↦ hst.trans H, fun H s ↦ H _ subset_rfl⟩

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 X
inst✝ : TopologicalSpace Y
F : Filter X
f_closed : IsClosedMap f
f_cont : Continuous[inst✝¹, inst✝] f
y : Y
⊢ MapClusterPt y F f ↔ (F.lift' closure[inst✝¹] ⊓ 𝓟 (f ⁻¹' {y})).NeBot

Tactic:
by
  rw [MapClusterPt, clusterPt_iff_lift'_closure', f_closed.lift'_closure_map_eq f_cont,
      ← comap_principal, ← map_neBot_iff f, Filter.push_pull, principal_singleton]

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 : Y
⊢ comap Prod.fst (𝓝 (x, y).1) ⊓ 𝓝 (x, y) = comap Prod.fst (𝓝 x) ⊓ comap Prod.snd (𝓝 y)

Tactic:
nhds_induced

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
y : Y
⊢ comap Prod.fst (𝓝 (x, y).1) ⊓ comap Prod.snd (𝓝 (x, y).2) = comap Prod.fst (𝓝 x) ⊓ comap Prod.snd (𝓝 y)
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
x : ↑s
⊢ 𝓝 x ⊓ 𝓟 (s ↓∩ t) = ⊥ ↔ comap Subtype.val (𝓝 ↑x) ⊓ 𝓟 (Subtype.val ⁻¹' t) = ⊥

Tactic:
nhds_induced

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
x : ↑s
⊢ comap Subtype.val (𝓝 ↑x) ⊓ 𝓟 (s ↓∩ t) = ⊥ ↔ comap Subtype.val (𝓝 ↑x) ⊓ 𝓟 (Subtype.val ⁻¹' t) = ⊥
Module: Mathlib.Topology.Constructions.SumProd

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

Tactic:
have st : s.Nonempty ∧ t.Nonempty := prod_nonempty_iff.1 h
    constructor
    · intro (H : IsOpen (s ×ˢ t))
      refine Or.inl ⟨?_, ?_⟩
      · simpa only [fst_image_prod _ st.2] using isOpenMap_fst _ H
      · simpa only [snd_image_prod st.1 t] using isOpenMap_snd _ H
    · intro H
      simp only [st.1.ne_empty, st.2.ne_empty, or_false] at H
      exact H.1.prod H.2

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: case refine_1
α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s u : Set α
this : TopologicalSpace α := TopologicalSpace.induced f t
x✝ : ∃ U, (∃ t_1, IsOpen[t] t_1 ∧ f ⁻¹' t_1 = U) ∧ s ⊆ U ∧ U ⊆ u
v : Set α
v' : Set β
hv' : IsOpen[t] v' ∧ f ⁻¹' v' = v
hv : s ⊆ v ∧ v ⊆ u
⊢ ∃ v, (∃ U, IsOpen[t] U ∧ f '' s ⊆ U ∧ U ⊆ v) ∧ f ⁻¹' v ⊆ u

Tactic:
refine ⟨v', ⟨v', hv'.1, ?_, subset_rfl⟩, hv'.2.trans_subset hv.2⟩

Goal state after:
case refine_1
α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s u : Set α
this : TopologicalSpace α := TopologicalSpace.induced f t
x✝ : ∃ U, (∃ t_1, IsOpen[t] t_1 ∧ f ⁻¹' t_1 = U) ∧ s ⊆ U ∧ U ⊆ u
v : Set α
v' : Set β
hv' : IsOpen[t] v' ∧ f ⁻¹' v' = v
hv : s ⊆ v ∧ v ⊆ u
⊢ f '' s ⊆ v'
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsOpenMap f
finv : β → α
hleft : LeftInverse finv f
⊢ ContinuousOn finv (range f)

Tactic:
rw [← image_univ]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsOpenMap f
finv : β → α
hleft : LeftInverse finv f
⊢ ContinuousOn finv (f '' univ)
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
b : β
f : α → β
h : Continuous[inst✝¹, inst✝] f
h' : EqOn f (fun x ↦ b) s
⊢ Tendsto f (𝓝ˢ s) (𝓝 b)

Tactic:
← nhdsSet_singleton

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
b : β
f : α → β
h : Continuous[inst✝¹, inst✝] f
h' : EqOn f (fun x ↦ b) s
⊢ Tendsto f (𝓝ˢ s) (𝓝ˢ {b})
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
s : Set α
f : α → β
hf : Continuous[t, inst✝] f
c : Set α
c_count : c.Countable
hc : s ⊆ closure[t] c
⊢ IsSeparable (f '' s)

Tactic:
refine ⟨f '' c, c_count.image _, ?_⟩

Goal state after:
α : Type u
t : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
s : Set α
f : α → β
hf : Continuous[t, inst✝] f
c : Set α
c_count : c.Countable
hc : s ⊆ closure[t] c
⊢ f '' s ⊆ closure[inst✝] (f '' c)
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_1
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x✝ : TopologicalSpace β := ⨅ i, t i
⊢ ∀ u ∈ {S | ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, U i}, IsOpen[⨅ i, t i] u

Tactic:
rintro - ⟨U, F, hU, rfl⟩
    refine isOpen_biInter_finset fun i hi ↦
      (h_basis i).isOpen (t := t i) (hU i hi) |>.mono (iInf_le _ _)

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

Goal state before:
pp: α : Type u_1
⊢ ⊥.smallSets = pure ∅

Tactic:
rw [smallSets, lift'_bot, powerset_empty, principal_singleton]
  exact monotone_powerset

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✝ : LocallyCompactSpace Y
f : X → Y
hf : IsInducing f
U Z : Set Y
hU : IsOpen[inst✝¹] U
hZ : IsClosed[inst✝¹] Z
hUZ : range f = U ∩ Z
x : X
H : U ∈ 𝓝 (f x)
⊢ (comap f (𝓝[U ∩ Z] f x)).HasBasis (fun s ↦ (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U) fun s ↦ f ⁻¹' (s ∩ Z)

Tactic:
nhdsWithin_inter_of_mem (nhdsWithin_le_nhds H)

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LocallyCompactSpace Y
f : X → Y
hf : IsInducing f
U Z : Set Y
hU : IsOpen[inst✝¹] U
hZ : IsClosed[inst✝¹] Z
hUZ : range f = U ∩ Z
x : X
H : U ∈ 𝓝 (f x)
⊢ (comap f (𝓝[Z] f x)).HasBasis (fun s ↦ (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U) fun s ↦ f ⁻¹' (s ∩ Z)
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : Option ι → Set X
⊢ LocallyFinite (f ∘ ⇑(Equiv.optionEquivSumPUnit ι).symm) ↔ LocallyFinite (f ∘ some)

Tactic:
locallyFinite_sum

Goal state after:
ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : Option ι → Set X
⊢ LocallyFinite ((f ∘ ⇑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inl) ∧
      LocallyFinite ((f ∘ ⇑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inr) ↔
    LocallyFinite (f ∘ some)
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: case mpr.refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ n, L n = f '' s
⊢ ∀ (n : ℕ), IsCompact ((fun n ↦ f ⁻¹' L n ∩ s) n)

pp: case mpr.refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ n, L n = f '' s
⊢ ⋃ n, (fun n ↦ f ⁻¹' L n ∩ s) n = s

Tactic:
· 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))

Goal state after:
case mpr.refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ n, L n = f '' s
⊢ ⋃ n, (fun n ↦ f ⁻¹' L n ∩ s) n = s
Module: Mathlib.Topology.Compactness.Compact

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

Tactic:
← nhdsSet_singleton

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
l : Filter X
y : X
hmem : s ∈ l
h : ∀ x ∈ s, ClusterPt x l → x = y
⊢ l ≤ 𝓝ˢ {y}
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
Y : Type u_2
l : Filter Y
y : X
f : Y → X
hs : IsCompact s
hmem : ∀ᶠ (x : Y) in l, f x ∈ s
h : ∀ x ∈ s, MapClusterPt x l f → x = y
⊢ Tendsto f l (𝓝 y)

Tactic:
← nhdsSet_singleton

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
Y : Type u_2
l : Filter Y
y : X
f : Y → X
hs : IsCompact s
hmem : ∀ᶠ (x : Y) in l, f x ∈ s
h : ∀ x ∈ s, MapClusterPt x l f → x = y
⊢ Tendsto f l (𝓝ˢ {y})
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
T : TopologicalSpace X
S : Set (Set X)
hTS : T = generateFrom S
s : Set X
h : ∀ P ⊆ S, s ⊆ ⋃₀ P → ∃ Q ⊆ P, Q.Finite ∧ s ⊆ ⋃₀ Q
F : Ultrafilter X
hsF : s ∈ F
hF : ¬∃ x ∈ s, ↑F ≤ 𝓝 x
U : X → Set X
hxU : ∀ x ∈ s, x ∈ U x
hSU : ∀ x ∈ s, U x ∈ S
hUF : ∀ x ∈ s, U x ∉ F
Q : Set (Set X)
hQU : Q ⊆ U '' s
hQ : Q.Finite
hsQ : s ⊆ ⋃₀ Q
this : ∀ s ∈ Q, s ∉ F
hQF : ⋂₀ (compl '' Q) ∈ (↑F).sets
⊢ ⋃₀ Q ∉ F

Tactic:
simpa [-Set.sInter_image, ← Set.compl_sUnion, hsQ, F.compl_mem_iff_notMem] using hQF

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

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
⊢ cocompact X = cofinite

Tactic:
simp only [cocompact, hasBasis_cofinite.eq_biInf, isCompact_iff_finite]

Goal state after:
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✝ : LinearOrder α
⊢ LinearOrder (UpperSet α)

Tactic:
exact Lattice.toLinearOrder _

Goal state after:
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✝ : LinearOrder α
⊢ LinearOrder (LowerSet α)

Tactic:
exact Lattice.toLinearOrder _

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace X
f : X → Y
hf : Continuous[inst✝², inst✝¹] f
⊢ IsCompact (range f)

Tactic:
rw [← image_univ]

Goal state after:
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace X
f : X → Y
hf : Continuous[inst✝², inst✝¹] f
⊢ IsCompact (f '' univ)
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s : Set X
f g : X → Y
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : IsOpen[inst✝²] s
hf : Continuous[inst✝², inst✝¹] f
hg : Continuous[inst✝², inst✝¹] g
hspec : ∀ (x : X), f x ⤳ g x
this : ∀ (U : Set Y), IsOpen[inst✝¹] U → g ⁻¹' U ⊆ f ⁻¹' U
⊢ ∀ (s_1 : Set Y), IsOpen[inst✝¹] s_1 → IsOpen[inst✝²] (s.piecewise f g ⁻¹' s_1)

Tactic:
intro U hU

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s : Set X
f g : X → Y
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : IsOpen[inst✝²] s
hf : Continuous[inst✝², inst✝¹] f
hg : Continuous[inst✝², inst✝¹] g
hspec : ∀ (x : X), f x ⤳ g x
this : ∀ (U : Set Y), IsOpen[inst✝¹] U → g ⁻¹' U ⊆ f ⁻¹' U
U : Set Y
hU : IsOpen[inst✝¹] U
⊢ IsOpen[inst✝²] (s.piecewise f g ⁻¹' U)
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : CompactSpace Y
f : X → Y
hf : IsClosedEmbedding f
⊢ IsCompact (range f)

Tactic:
exact hf.isClosed_range.isCompact

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ SpecializingMap f ↔ ∀ (x : X), closure[inst✝] {f x} ⊆ f '' closure[inst✝¹] {x}

Tactic:
by
  simp only [SpecializingMap, Relation.Fibration, flip, specializes_iff_mem_closure]; rfl

Goal state after:
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: case hpg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
s : Set α
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hp : ∀ a ∈ s ∩ frontier {a | p a}, f a = g a
hf : ContinuousOn f (s ∩ closure[inst✝²] {a | p a})
hg : ContinuousOn g (s ∩ closure[inst✝²] {a | ¬p a})
⊢ ∀ a ∈ s ∩ frontier {a | p a}, Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))

Tactic:
rintro a ha
    simp only [hp a ha, ite_self]
    apply tendsto_nhdsWithin_mono_left (inter_subset_inter_right s subset_closure)
    rcases ha with ⟨has, ⟨_, ha⟩⟩
    rw [← mem_compl_iff, ← closure_compl] at ha
    apply hg a ⟨has, ha⟩

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case mp
X : Type u_3
inst✝ : TopologicalSpace X
s : Set X
H : s ∈ irreducibleComponents X
⊢ s ∈ {s | Maximal (fun x ↦ IsClosed[inst✝] x ∧ IsIrreducible x) s}

Tactic:
exact ⟨⟨isClosed_of_mem_irreducibleComponents _ H, H.1⟩, fun x h e => H.2 h.2 e⟩

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
⊢ IsDiscrete Set.univ

Tactic:
by
  rwa [isDiscrete_univ_iff]

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case neg
X : Type u_1
inst✝ : TopologicalSpace X
s U : Set X
hs : s ∈ codiscreteWithin U
hU : IsClosed[inst✝] U
x : X
hx : x ∈ (U \ s)ᶜ
h₁x : x ∉ U
⊢ ∀ᶠ (y : X) in 𝓝 x, y ∈ (U \ s)ᶜ

Tactic:
eventually_iff_exists_mem

Goal state after:
case neg
X : Type u_1
inst✝ : TopologicalSpace X
s U : Set X
hs : s ∈ codiscreteWithin U
hU : IsClosed[inst✝] U
x : X
hx : x ∈ (U \ s)ᶜ
h₁x : x ∉ U
⊢ ∃ v ∈ 𝓝 x, ∀ y ∈ v, y ∈ (U \ s)ᶜ
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : ClosedIicTopology α
a : α
⊢ IsOpen[inst✝²] (Ioi a)

Tactic:
rw [← compl_Iic]

Goal state after:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : ClosedIicTopology α
a : α
⊢ IsOpen[inst✝²] (Iic a)ᶜ
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LindelofSpace X
f : X → Y
hf : Continuous[inst✝², inst✝¹] f
⊢ IsLindelof (range f)

Tactic:
rw [← image_univ]

Goal state after:
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LindelofSpace X
f : X → Y
hf : Continuous[inst✝², inst✝¹] f
⊢ IsLindelof (f '' univ)
Module: Mathlib.Topology.Connected.TotallyDisconnected

Goal state before:
pp: case inr
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝² : TopologicalSpace α
s✝ t u v : Set α
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), TotallyDisconnectedSpace (X i)
s : Set ((i : ι) × X i)
x✝ : s ⊆ univ
hs : IsPreconnected s
h : s.Nonempty
⊢ s.Subsingleton

Tactic:
· obtain ⟨a, t, ht, rfl⟩ := Sigma.isConnected_iff.1 ⟨h, hs⟩
    exact ht.isPreconnected.subsingleton.image _

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
ι : Type u_3
ι' : Sort u_4
inst✝ : TopologicalSpace X
⊢ CountableInterFilter (residual X)

Tactic:
rw [residual]

Goal state after:
X : Type u_1
Y : Type u_2
ι : Type u_3
ι' : Sort u_4
inst✝ : TopologicalSpace X
⊢ CountableInterFilter (countableGenerate {t | IsOpen[inst✝] t ∧ Dense t})
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Nonempty X
s : Set X
hs : IsGδ s
hd : Dense s
h : IsMeagre s
⊢ False

Tactic:
rcases mem_residual.1 h with ⟨t, hts, htG, hd'⟩

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Nonempty X
s : Set X
hs : IsGδ s
hd : Dense s
h : IsMeagre s
t : Set X
hts : t ⊆ sᶜ
htG : IsGδ t
hd' : Dense t
⊢ False
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
⊢ TendstoUniformlyOn F f p s ↔ Tendsto (fun q ↦ (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 s) (𝓤 β)

Tactic:
by
  simp [tendstoUniformlyOn_iff_tendstoUniformlyOnFilter, tendstoUniformlyOnFilter_iff_tendsto]

Goal state after: