mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
Φ : uliftYoneda.{max w v₂, v₁, u₁}.LeftExtension (F ⋙ uliftYoneda.{max w v₁, v₂, u₂})
f g : Functor.LeftExtension.mk F.op.lan (compULiftYonedaIsoULiftYonedaCompLan F).hom ⟶ Φ
P : Cᵒᵖ ⥤ Type (max (max w v₁) v₂)
⊢ (StructuredArrow.Hom.right f).app P = (StructuredArrow.Hom.right g).app P

Tactic:
apply (F.op.lan.obj P).hom_ext_of_isLeftKanExtension (F.op.lanUnit.app P)

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
Φ : uliftYoneda.{max w v₂, v₁, u₁}.LeftExtension (F ⋙ uliftYoneda.{max w v₁, v₂, u₂})
f g : Functor.LeftExtension.mk F.op.lan (compULiftYonedaIsoULiftYonedaCompLan F).hom ⟶ Φ
P : Cᵒᵖ ⥤ Type (max (max w v₁) v₂)
⊢ F.op.lanUnit.app P ≫ F.op.whiskerLeft ((StructuredArrow.Hom.right f).app P) =
    F.op.lanUnit.app P ≫ F.op.whiskerLeft ((StructuredArrow.Hom.right g).app P)
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
h : (yoneda.obj G).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
⊢ IsIso f

Tactic:
rw [← isIso_op_iff]
    suffices IsIso ((yoneda.obj G).map f.op) by
      exact @isIso_of_reflects_iso _ _ _ _ _ _ _ (yoneda.obj G) _ h
    rwa [isIso_iff_bijective, Function.bijective_iff_existsUnique]

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

Goal state before:
pp: A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
m : ℤ
g : ↥(ℤ ∙ m) →ₗ[ℤ] A
⊢ ∃ g', ∀ (x : ℤ) (mem : x ∈ ℤ ∙ m), g' x = g ⟨x, mem⟩

Tactic:
obtain rfl | h0 := eq_or_ne m 0

Goal state after:
case inl
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
g : ↥(ℤ ∙ 0) →ₗ[ℤ] A
⊢ ∃ g', ∀ (x : ℤ) (mem : x ∈ ℤ ∙ 0), g' x = g ⟨x, mem⟩

case inr
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
m : ℤ
g : ↥(ℤ ∙ m) →ₗ[ℤ] A
h0 : m ≠ 0
⊢ ∃ g', ∀ (x : ℤ) (mem : x ∈ ℤ ∙ m), g' x = g ⟨x, mem⟩
Module: Mathlib.GroupTheory.Divisible

Goal state before:
pp: A : Type u_1
inst✝ : AddCommGroup A
H : ∀ {n : ℤ}, n ≠ 0 → n • ⊤ = ⊤
n✝ : ℤ
a : A
hn : n✝ ≠ 0
h1 : ∃ a_1 ∈ ↑⊤, ((DistribMulAction.toAddMonoidEnd ℤ A) n✝) a_1 = a
⊢ n✝ • h1.choose = a

Tactic:
exact h1.choose_spec.2

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p n = #({x ∈ range n | p x})

Tactic:
count,

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ List.countP (fun b ↦ decide (p b)) (List.range n) = #({x ∈ range n | p x})
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case inr
d : ℕ
hd0 : d > 0
x : ℕ
⊢ φ x = #({k ∈ range (d * x) | (d * x).gcd k = d})

Tactic:
apply Finset.card_bij fun k _ => d * k

Goal state after:
case inr.hi
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ a ∈ {a ∈ range x | x.Coprime a}, d * a ∈ {k ∈ range (d * x) | (d * x).gcd k = d}

case inr.i_inj
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ a₁ ∈ {a ∈ range x | x.Coprime a}, ∀ a₂ ∈ {a ∈ range x | x.Coprime a}, d * a₁ = d * a₂ → a₁ = a₂

case inr.i_surj
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ b ∈ {k ∈ range (d * x) | (d * x).gcd k = d}, ∃ a, ∃ (_ : a ∈ {a ∈ range x | x.Coprime a}), d * a = b
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: case hf
ι : Type u_1
ι' : Type u_2
p : Finset ι × Finset ι'
⊢ ∀ ⦃b : Finset ι × Finset ι'⦄, p ≤ b → (fun p ↦ p.1 ×ˢ p.2) p ⊆ (fun p ↦ p.1 ×ˢ p.2) b

Tactic:
q

Goal state after:
case hf
ι : Type u_1
ι' : Type u_2
p q : Finset ι × Finset ι'
⊢ p ≤ q → (fun p ↦ p.1 ×ˢ p.2) p ⊆ (fun p ↦ p.1 ×ˢ p.2) q
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: p : ℕ
inst✝ : Fintype (ZMod p)ˣ
⊢ Prime p ↔ Fintype.card (ZMod p)ˣ = p - 1

Tactic:
rcases eq_zero_or_neZero p with rfl | hp

Goal state after:
case inl
inst✝ : Fintype (ZMod 0)ˣ
⊢ Prime 0 ↔ Fintype.card (ZMod 0)ˣ = 0 - 1

case inr
p : ℕ
inst✝ : Fintype (ZMod p)ˣ
hp : NeZero p
⊢ Prime p ↔ Fintype.card (ZMod p)ˣ = p - 1
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : atBot.IsCountablyGenerated
inst✝¹ : Preorder β
inst✝ : atBot.IsCountablyGenerated
⊢ atBot.IsCountablyGenerated

Tactic:
by
  rw [← prod_atBot_atBot_eq]
  infer_instance

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

Goal state before:
pp: case pos
a b : ℕ
h : a ∣ b
ha : Even a
h' : b = 0
ha' : a = 0
⊢ a = 0

Tactic:
ha'

Goal state after:
case pos
a b : ℕ
h : a ∣ b
ha : Even a
h' : b = 0
ha' : a = 0
⊢ 0 = 0
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ toIocMod hp a b = c ↔ c ∈ Set.Ioc a (a + p) ∧ ∃ z, b = c + z • p

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hf : Directed (fun x1 x2 ↦ x1 ≥ x2) f
hg : Monotone g
s : Set β
⊢ s ∈ (iInf f).lift g → s ∈ ⨅ i, (f i).lift g

Tactic:
by
    simp only [mem_lift_sets hg, exists_imp, and_imp, mem_iInf_of_directed hf]
    exact fun t i ht hs => mem_iInf_of_mem i <| mem_lift ht hs

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

Goal state before:
pp: α : Type u_1
β : Type u_2
h : Set α → Set β
a : α
hh : Monotone h
⊢ (pure a).lift' h = 𝓟 (h {a})

Tactic:
← principal_singleton,

Goal state after:
α : Type u_1
β : Type u_2
h : Set α → Set β
a : α
hh : Monotone h
⊢ (𝓟 {a}).lift' h = 𝓟 (h {a})
Module: Mathlib.Topology.Closure

Goal state before:
pp: case mp
X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ Dense {x}ᶜ → ¬IsOpen {x}

Tactic:
intro hd ho

Goal state after:
case mp
X : Type u
inst✝ : TopologicalSpace X
x : X
hd : Dense {x}ᶜ
ho : IsOpen {x}
⊢ 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 x✝ : α
⊢ toIcoMod hp a x✝ = toIocMod hp a x✝ ↔ ∃ i, x✝ - i • p ∈ Set.Ioo a (a + p)

Tactic:
←
    not_modEq_iff_toIcoMod_eq_toIocMod,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a x✝ : α
⊢ ¬a ≡ x✝ [PMOD p] ↔ ∃ i, x✝ - i • p ∈ Set.Ioo 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 : α
⊢ toIcoMod hp a b = toIcoMod hp (0 + a) b - a + a

Tactic:
zero_add,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp a b = toIcoMod hp a b - a + a
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp a b = toIocMod hp (0 + a) b - a + a

Tactic:
zero_add,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp a b = toIocMod hp a b - a + a
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp' : Fact (0 < p)
x₁ x₂ x₃ : α
⊢ toIcoMod ⋯ (0 + x₁) x₂ - x₁ ≤ toIocMod ⋯ (0 + x₁) x₃ - x₁ ↔ toIcoMod ⋯ x₁ x₂ ≤ toIocMod ⋯ x₁ x₃

Tactic:
zero_add,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp' : Fact (0 < p)
x₁ x₂ x₃ : α
⊢ toIcoMod ⋯ x₁ x₂ - x₁ ≤ toIocMod ⋯ x₁ x₃ - x₁ ↔ toIcoMod ⋯ x₁ x₂ ≤ toIocMod ⋯ x₁ x₃
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
a : α
f : Filter α
t : TopologicalSpace α
⊢ t ≤ nhdsAdjoint a f ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b

Tactic:
le_iff_nhds,

Goal state after:
α : Type u
a : α
f : Filter α
t : TopologicalSpace α
⊢ (∀ (x : α), 𝓝 x ≤ 𝓝 x) ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b
Module: Mathlib.Topology.Separation.SeparatedNhds

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hst' : IsOpen[inst✝] (s ∪ t)ᶜ
u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hsu : s ⊆ u
htv : t ⊆ v
huv : Disjoint u v
⊢ s ⊆ vᶜ

Tactic:
subset_compl_comm

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hst' : IsOpen[inst✝] (s ∪ t)ᶜ
u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hsu : s ⊆ u
htv : t ⊆ v
huv : Disjoint u v
⊢ v ⊆ sᶜ
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a : α
l : Filter α
x✝ : TopologicalSpace β
⊢ coinduced f (nhdsAdjoint a l) ≤ x✝ ↔ nhdsAdjoint (f a) (map f l) ≤ x✝

Tactic:
gc_nhds,

Goal state after:
α : Type u
β : Type v
f : α → β
a : α
l : Filter α
x✝ : TopologicalSpace β
⊢ coinduced f (nhdsAdjoint a l) ≤ x✝ ↔ map f l ≤ (fun t ↦ 𝓝 (f a)) x✝
Module: Mathlib.Topology.NhdsWithin

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

Tactic:
eventuallyEq_set,

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t u : Set α
hs : s ∈ 𝓝 a
h₂ : t ∩ s = u ∩ s
⊢ 𝓝[t ∩ s] a = 𝓝[u] a

Tactic:
nhdsWithin_restrict' u hs,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t u : Set α
hs : s ∈ 𝓝 a
h₂ : t ∩ s = u ∩ s
⊢ 𝓝[t ∩ s] a = 𝓝[u ∩ s] a
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
x : ↑s
⊢ 𝓝[s ↓∩ t] x = ⊥ ↔ 𝓝[t] ↑x ⊓ 𝓟 s = ⊥

Tactic:
by
  rw [inf_principal_eq_bot_iff_comap, nhdsWithin, nhdsWithin, comap_inf, comap_principal,
    nhds_induced]

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

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

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:
· simp [h, prod_eq_empty_iff.1 h]

Goal state after:
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 = ∅
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X✝ : Type u
Y : Type v
Z : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
X : Type u_5
⊢ ∀ (s : Set (Set X)), (∀ t ∈ s, t.Nonempty → tᶜ.Finite) → (⋃₀ s).Nonempty → (⋃₀ s)ᶜ.Finite

Tactic:
rintro s h ⟨x, t, hts, hzt⟩
    rw [compl_sUnion]
    exact Finite.sInter (mem_image_of_mem _ hts) (h t hts ⟨x, hzt⟩)

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
x : α
s : Set α
⊢ 𝓝ˢ[s] {x} = 𝓝[s] x

Tactic:
simp [nhdsSetWithin, nhdsWithin]

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : ∀ x ∈ s, ∃ t, IsOpen[inst✝¹] t ∧ x ∈ t ∧ ContinuousOn f (s ∩ t)
⊢ ContinuousOn f s

Tactic:
intro x xs

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : ∀ x ∈ s, ∃ t, IsOpen[inst✝¹] t ∧ x ∈ t ∧ ContinuousOn f (s ∩ t)
x : α
xs : x ∈ s
⊢ ContinuousWithinAt f s x
Module: Mathlib.Topology.ContinuousOn

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

Tactic:
simp +contextual [mem_nhdsWithin_iff_eventually, hf.nhds_eq_comap, forall_comm (α := _ ∈ _)]

Goal state after:
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
x : α
⊢ ⋃ y, ⋃ (_ : y ≤ x), accumulate s y = ⋃ y, ⋃ (_ : y ≤ x), s y

Tactic:
apply Subset.antisymm
  · exact iUnion₂_subset fun y hy => monotone_accumulate hy
  · exact iUnion₂_mono fun y _ => subset_accumulate

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: ι : 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
f : (i : ι) → X i
hf : f ∈ univ.pi s
o : Set ((i : ι) → X i)
ho : IsOpen[Pi.topologicalSpace] o
hfo : f ∈ o
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen[inst✝ a] (u a) ∧ f a ∈ u a
hI : (↑I).pi u ⊆ o
i : ι
hi : i ∈ I
⊢ (u i ∩ c i).Nonempty

Tactic:
exact mem_closure_iff.1 (hc i <| hf _ trivial) _ (huo i hi).1 (huo i hi).2

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

Goal state before:
pp: α : Type u
β : Type v
m : α → β
a : α
inj : Injective m
large : range m ∈ pure (m a)
⊢ 𝓟 (m ⁻¹' {m a}) = pure a

Tactic:
← principal_singleton,

Goal state after:
α : Type u
β : Type v
m : α → β
a : α
inj : Injective m
large : range m ∈ pure (m a)
⊢ 𝓟 (m ⁻¹' {m a}) = 𝓟 {a}
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
a : X
U : Set X
haU : U ∈ 𝓝 a
hfin : {i | (f i ∩ U).Nonempty}.Finite
⊢ 𝓝[⋃ i, f i] a = 𝓝[⋃ i, f i ∩ U] a

Tactic:
rw [← iUnion_inter, ← nhdsWithin_inter_of_mem' (nhdsWithin_le_nhds haU)]

Goal state after:
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
a : X
⊢ 𝓝[⋃ i, f i] a = ⨆ i, 𝓝[f i] a

Tactic:
by
  rcases hf a with ⟨U, haU, hfin⟩
  refine le_antisymm ?_ (Monotone.le_map_iSup fun _ _ ↦ nhdsWithin_mono _)
  calc
    𝓝[⋃ i, f i] a = 𝓝[⋃ i, f i ∩ U] a := by
      rw [← iUnion_inter, ← nhdsWithin_inter_of_mem' (nhdsWithin_le_nhds haU)]
    _ = 𝓝[⋃ i ∈ {j | (f j ∩ U).Nonempty}, (f i ∩ U)] a := by
      simp only [mem_ofPred_eq, iUnion_nonempty_self]
    _ = ⨆ i ∈ {j | (f j ∩ U).Nonempty}, 𝓝[f i ∩ U] a := nhdsWithin_biUnion hfin _ _
    _ ≤ ⨆ i, 𝓝[f i ∩ U] a := iSup₂_le_iSup _ _
    _ ≤ ⨆ i, 𝓝[f i] a := iSup_mono fun i ↦ nhdsWithin_mono _ inter_subset_left

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 : ContinuousOn f s
K : ℕ → Set X
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcov : ⋃ n, K n = s
⊢ ∀ (n : ℕ), IsCompact ((fun n ↦ f '' K n) n)

Tactic:
exact fun n ↦ (hcompact n).image_of_continuousOn (hf.mono (hcov.symm ▸ subset_iUnion K n))

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case h_nhds.inl
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
x : α
u : Set (α ⊕ β)
hxu : Sum.inl x ∈ u
u_open : IsOpen[instTopologicalSpaceSum] u
⊢ ∃ v ∈ (fun u ↦ Sum.inl '' u) '' s ∪ (fun u ↦ Sum.inr '' u) '' t, Sum.inl x ∈ v ∧ v ⊆ u

Tactic:
obtain ⟨v, vs, xv, vu⟩ : ∃ v ∈ s, x ∈ v ∧ v ⊆ Sum.inl ⁻¹' u :=
        hs.exists_subset_of_mem_open hxu (isOpen_sum_iff.1 u_open).1

Goal state after:
case h_nhds.inl
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
x : α
u : Set (α ⊕ β)
hxu : Sum.inl x ∈ u
u_open : IsOpen[instTopologicalSpaceSum] u
v : Set α
vs : v ∈ s
xv : x ∈ v
vu : v ⊆ Sum.inl ⁻¹' u
⊢ ∃ v ∈ (fun u ↦ Sum.inl '' u) '' s ∪ (fun u ↦ Sum.inr '' u) '' t, Sum.inl x ∈ v ∧ v ⊆ u
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: case inr
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 ι
⊢ SigmaCompactSpace ((i : ι) × X i)

Tactic:
rcases exists_surjective_nat ι with ⟨f, hf⟩

Goal state after:
case inr
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
⊢ SigmaCompactSpace ((i : ι) × X i)
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
W : Set X
hsubW : ⋂ i, V i ⊆ W
W_op : IsOpen[inst✝¹] W
hWU : W ⊆ U
H : ∀ (i : ι), (V i ∩ Wᶜ).Nonempty
i j : ι
⊢ ∃ z, (fun x1 x2 ↦ x1 ⊇ x2) (V i ∩ Wᶜ) (V z ∩ Wᶜ) ∧ (fun x1 x2 ↦ x1 ⊇ x2) (V j ∩ Wᶜ) (V z ∩ Wᶜ)

Tactic:
rcases hV i j with ⟨k, hki, hkj⟩

Goal state after:
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
W : Set X
hsubW : ⋂ i, V i ⊆ W
W_op : IsOpen[inst✝¹] W
hWU : W ⊆ U
H : ∀ (i : ι), (V i ∩ Wᶜ).Nonempty
i j k : ι
hki : V i ⊇ V k
hkj : V j ⊇ V k
⊢ ∃ z, (fun x1 x2 ↦ x1 ⊇ x2) (V i ∩ Wᶜ) (V z ∩ Wᶜ) ∧ (fun x1 x2 ↦ x1 ⊇ x2) (V j ∩ Wᶜ) (V z ∩ Wᶜ)
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
f : Filter X
⊢ Disjoint f (cocompact X) ↔ ∃ K ∈ f, IsCompact K

Tactic:
simp_rw [hasBasis_cocompact.disjoint_iff_right, compl_compl]
  tauto

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
U : Set X
⊢ U ∈ codiscreteWithin U

Tactic:
by simp [mem_codiscreteWithin]

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsDiscrete s
hs' : IsPreirreducible s
x : X
hxs : x ∈ s
y : X
hys : y ∈ s
U : Set X
hU : IsOpen[inst✝] U
hUx : U ∩ s = {x}
V : Set X
hV : IsOpen[inst✝] V
hVy : V ∩ s = {y}
⊢ x = y

Tactic:
obtain ⟨z, hz⟩ := hs' _ _ hU hV ⟨x, by grind⟩ ⟨y, by grind⟩

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsDiscrete s
hs' : IsPreirreducible s
x : X
hxs : x ∈ s
y : X
hys : y ∈ s
U : Set X
hU : IsOpen[inst✝] U
hUx : U ∩ s = {x}
V : Set X
hV : IsOpen[inst✝] V
hVy : V ∩ s = {y}
z : X
hz : z ∈ s ∩ (U ∩ V)
⊢ x = y
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
s t : Set X
f g : X → Y
h : EqOn f g s
hf : ContinuousOn f t
hg : ContinuousOn g t
hst : s ⊆ t
hts : t ⊆ closure[inst✝²] s
⊢ EqOn f g t

Tactic:
intro x hx
  have : (𝓝[s] x).NeBot := mem_closure_iff_clusterPt.mp (hts hx)
  exact
    tendsto_nhds_unique_of_eventuallyEq ((hf x hx).mono_left <| nhdsWithin_mono _ hst)
      ((hg x hx).mono_left <| nhdsWithin_mono _ hst) (h.eventuallyEq_of_mem self_mem_nhdsWithin)

Goal state after:
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
⊢ {x} ∈ 𝓝[s] x

Tactic:
rw [isDiscrete_iff_discreteTopology] at hs
  have : ({⟨x, hx⟩} : Set s) ∈ 𝓝 (⟨x, hx⟩ : s) := by simp [nhds_discrete]
  simpa only [nhdsWithin_eq_map_subtype_coe hx, image_singleton] using
    @image_mem_map _ _ _ ((↑) : s → X) _ this

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
x : α
s t : Set α
H1 : x ∈ s
H2 : x ∈ t
H3 : IsPreconnected s
H4 : IsPreconnected t
⊢ ∀ s_1 ∈ {s, t}, x ∈ s_1

Tactic:
by rintro r (rfl | rfl | h) <;> assumption

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
x : α
s t : Set α
H1 : x ∈ s
H2 : x ∈ t
H3 : IsPreconnected s
H4 : IsPreconnected t
⊢ ∀ s_1 ∈ {s, t}, IsPreconnected s_1

Tactic:
by rintro r (rfl | rfl | h) <;> assumption

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsClosedMap f
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ (s ∩ (f '' u ∩ f '' v)).Nonempty

Tactic:
refine isPreconnected_closed_iff.1 hs (f '' u) (f '' v) (hf u hu) (hf v hv) ?_ ?_ ?_

Goal state after:
case refine_1
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsClosedMap f
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ s ⊆ f '' u ∪ f '' v

case refine_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsClosedMap f
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ (s ∩ f '' u).Nonempty

case refine_3
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsClosedMap f
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ (s ∩ f '' v).Nonempty
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: case h.right.h
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
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → (∃ r, r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
S : Set (Set X)
hS : S.Countable
r : Set X → Set ι
hr : ∀ s ∈ S, (r s).Countable ∧ s ⊆ ⋃ i ∈ r s, U i
⊢ ∀ t' ∈ S, t' ⊆ ⋃ i ∈ ⋃ s ∈ S, r s, U i

Tactic:
simp only [mem_iUnion, exists_prop, iUnion_exists, biUnion_and']

Goal state after:
case h.right.h
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
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → (∃ r, r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
S : Set (Set X)
hS : S.Countable
r : Set X → Set ι
hr : ∀ s ∈ S, (r s).Countable ∧ s ⊆ ⋃ i ∈ r s, U i
⊢ ∀ t' ∈ S, t' ⊆ ⋃ y ∈ S, ⋃ x ∈ r y, U x