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

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
W : C
h : W ⟶ X
inst✝ : HasPullbacks C
⊢ ((equalizerSubobject (h ≫ f) (h ≫ g)).arrow ≫ h) ≫ f = ((equalizerSubobject (h ≫ f) (h ≫ g)).arrow ≫ h) ≫ g

Tactic:
rw [assoc, assoc, equalizerSubobject_arrow_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
B : C
⊢ initial.to B = 0

Tactic:
rw [← bot_arrow, bot_arrow_eq_zero]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : F.Faithful
S : ShortComplex C
hS : kernel.ι (F.map S.g) ≫ cokernel.π (F.map S.f) = 0
k : F.obj (Limits.kernel S.g) ⟶ Limits.kernel (F.map S.g)
hk : k ≫ kernel.ι (F.map S.g) = F.map (kernel.ι S.g)
l : cokernel (F.map S.f) ⟶ F.obj (cokernel S.f)
hl : cokernel.π (F.map S.f) ≫ l = F.map (cokernel.π S.f)
⊢ F.map (kernel.ι S.g) ≫ cokernel.π (F.map S.f) ≫ l = 0

Tactic:
← hk,

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : F.Faithful
S : ShortComplex C
hS : kernel.ι (F.map S.g) ≫ cokernel.π (F.map S.f) = 0
k : F.obj (Limits.kernel S.g) ⟶ Limits.kernel (F.map S.g)
hk : k ≫ kernel.ι (F.map S.g) = F.map (kernel.ι S.g)
l : cokernel (F.map S.f) ⟶ F.obj (cokernel S.f)
hl : cokernel.π (F.map S.f) ≫ l = F.map (cokernel.π S.f)
⊢ (k ≫ kernel.ι (F.map S.g)) ≫ cokernel.π (F.map S.f) ≫ l = 0
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : F.Faithful
S : ShortComplex C
hS : kernel.ι (F.map S.g) ≫ cokernel.π (F.map S.f) = 0
k : F.obj (Limits.kernel S.g) ⟶ Limits.kernel (F.map S.g)
hk : k ≫ kernel.ι (F.map S.g) = F.map (kernel.ι S.g)
l : cokernel (F.map S.f) ⟶ F.obj (cokernel S.f)
hl : cokernel.π (F.map S.f) ≫ l = F.map (cokernel.π S.f)
⊢ F.map (kernel.ι S.g ≫ cokernel.π S.f) = 0

Tactic:
rw [F.map_comp, ← hl, ← hk, Category.assoc, reassoc_of% hS, zero_comp, comp_zero]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: case e'_3
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
inst✝ : HasProduct Z
X : C
π : (a : α) → X ⟶ Z a
e_1✝ :
  ((∐ fun x ↦ op (Z x)) ⟶ op X) = ((Cofan.mk (∐ fun x ↦ op (Z x)) (Sigma.ι fun x ↦ op (Z x))).pt ⟶ op (Fan.mk X π).pt)
⊢ (Sigma.desc fun a ↦ (π a).op) = (coproductIsCoproduct fun x ↦ op (Z x)).desc (Fan.mk X π).op

Tactic:
simp [coproductIsCoproduct]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
L : C ⥤ D
H : Type u_3
inst✝⁴ : Category.{v_3, u_3} H
inst✝³ : L.Full
inst✝² : L.Faithful
F : C ⥤ H
inst✝¹ : L.HasPointwiseRightKanExtension F
inst✝ : ∀ (F : C ⥤ H), L.HasRightKanExtension F
⊢ IsIso ((L.ranAdjunction H).counit.app F)

Tactic:
rw [ranAdjunction_counit]
  infer_instance

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

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
S : ShortComplex (J ⥤ AddCommGrpCat)
hS :
  ∀ (j : J),
    (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).g).ker ≤
      (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).f).range
j : J
y : ToType (S.X₂.obj j)
hx : (ConcreteCategory.hom (colimit.ι S.X₂ j ≫ colim.map S.g)) y = 0
⊢ (ConcreteCategory.hom (colimit.ι S.X₂ j)) y ∈ (AddCommGrpCat.Hom.hom (S.map colim).f).range

Tactic:
colimit.ι_map,

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
S : ShortComplex (J ⥤ AddCommGrpCat)
hS :
  ∀ (j : J),
    (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).g).ker ≤
      (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).f).range
j : J
y : ToType (S.X₂.obj j)
hx : (ConcreteCategory.hom (S.g.app j ≫ colimit.ι S.X₃ j)) y = 0
⊢ (ConcreteCategory.hom (colimit.ι S.X₂ j)) y ∈ (AddCommGrpCat.Hom.hom (S.map colim).f).range
Module: Mathlib.Algebra.Category.Grp.AB

Goal state before:
pp: case h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
S : ShortComplex (J ⥤ AddCommGrpCat)
hS :
  ∀ (j : J),
    (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).g).ker ≤
      (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).f).range
j : J
y : ToType (S.X₂.obj j)
hx :
  (ConcreteCategory.hom (colimit.ι S.X₃ j)) ((ConcreteCategory.hom (S.g.app j)) y) =
    (AddCommGrpCat.Hom.hom (colimit.ι S.X₃ j)) 0
k : J
e₁ e₂ : j ⟶ k
hk : (ConcreteCategory.hom (S.g.app k)) ((ConcreteCategory.hom (S.X₂.map e₁)) y) = 0
t : ↑(S.map ((evaluation J AddCommGrpCat).obj k)).X₁
ht : (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj k)).f) t = (ConcreteCategory.hom (S.X₂.map e₁)) y
⊢ (ConcreteCategory.hom (colimit.ι S.X₁ k ≫ (S.map colim).f)) t = (ConcreteCategory.hom (colimit.ι S.X₂ j)) y

Tactic:
colimit.ι_map,

Goal state after:
case h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
S : ShortComplex (J ⥤ AddCommGrpCat)
hS :
  ∀ (j : J),
    (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).g).ker ≤
      (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).f).range
j : J
y : ToType (S.X₂.obj j)
hx :
  (ConcreteCategory.hom (colimit.ι S.X₃ j)) ((ConcreteCategory.hom (S.g.app j)) y) =
    (AddCommGrpCat.Hom.hom (colimit.ι S.X₃ j)) 0
k : J
e₁ e₂ : j ⟶ k
hk : (ConcreteCategory.hom (S.g.app k)) ((ConcreteCategory.hom (S.X₂.map e₁)) y) = 0
t : ↑(S.map ((evaluation J AddCommGrpCat).obj k)).X₁
ht : (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj k)).f) t = (ConcreteCategory.hom (S.X₂.map e₁)) y
⊢ (ConcreteCategory.hom (S.f.app k ≫ colimit.ι S.X₂ k)) t = (ConcreteCategory.hom (colimit.ι S.X₂ j)) y
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₂)
⊢ 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)

Tactic:
apply (colimitOfRepresentable.{max w v₂} P).hom_ext

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₂)
⊢ ∀ (j : P.Elementsᵒᵖ),
    (coconeOfRepresentable P).ι.app j ≫ F.op.lanUnit.app P ≫ F.op.whiskerLeft ((StructuredArrow.Hom.right f).app P) =
      (coconeOfRepresentable P).ι.app j ≫ 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_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
hG : IsCodetector G
A✝ B✝ : Cᵒᵖ
f : A✝ ⟶ B✝
hf : IsIso ((yoneda.obj G).map f)
⊢ IsIso f

Tactic:
refine (isIso_unop_iff _).1 (hG.def _ ?_)
    rwa [isIso_iff_bijective, Function.bijective_iff_existsUnique] at hf

Goal state after:
Module: Mathlib.Data.ZMod.IntUnitsPower

Goal state before:
pp: z₁ z₂ : ZMod 2
au : Additive ℤˣ
⊢ Additive.toMul au ^ ((z₁.val + z₂.val) % 2) = Additive.toMul au ^ (z₁.val + z₂.val)

Tactic:
← Int.units_pow_eq_pow_mod_two

Goal state after:
z₁ z₂ : ZMod 2
au : Additive ℤˣ
⊢ Additive.toMul au ^ (z₁.val + z₂.val) = Additive.toMul au ^ (z₁.val + z₂.val)
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddGroup α
h : Periodic f c
⊢ Periodic f (-c)

Tactic:
by
  simpa only [sub_eq_add_neg, Periodic] using h.sub_eq

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : NonAssocRing α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
hi : f 0 = 0
n : ℕ
⊢ f (↑↑n * c) = 0

Tactic:
by rw [Int.cast_natCast, h.nat_mul_eq_of_eq_zero hi n]

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
⊢ count p 0 = 0

Tactic:
by simp [count]

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

Goal state before:
pp: n : ℕ
⊢ ∑ m ∈ range n.succ with m ∣ n, φ m = n

Tactic:
by
  convert! sum_totient _ using 1
  simp only [Nat.divisors, sum_filter, range_eq_Ico]
  rw [sum_eq_sum_Ico_succ_bot] <;> simp

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

Goal state before:
pp: p n : ℕ
hp : Prime p
h : ¬p ∣ n
⊢ p.Coprime n

Tactic:
simpa [h] using coprime_or_dvd_of_prime hp n

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

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

Tactic:
· exact totient_pos.mpr <| pos_of_ne_zero ha

Goal state after:
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 ≠ toIocMod hp a b → ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)

Tactic:
← not_exists,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp a b ≠ toIocMod hp a b → ¬∃ x, b - x • p ∈ Set.Ioo a (a + p)
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsOpen s ↔ ∀ x ∈ s, ∃ t ⊆ s, IsOpen t ∧ x ∈ t

Tactic:
← subset_interior_iff_isOpen

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ s ⊆ interior s ↔ ∀ x ∈ s, ∃ t ⊆ s, IsOpen t ∧ x ∈ t
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ (⨅ s ∈ {s | x ∈ s ∧ IsOpen[inst✝] s}, 𝓟 s).HasBasis (fun s ↦ x ∈ s ∧ IsOpen[inst✝] s) fun s ↦ s

Tactic:
exact hasBasis_biInf_principal
    (fun s ⟨has, hs⟩ t ⟨hat, ht⟩ =>
      ⟨s ∩ t, ⟨⟨has, hat⟩, IsOpen.inter hs ht⟩, ⟨inter_subset_left, inter_subset_right⟩⟩)
    ⟨univ, ⟨mem_univ x, isOpen_univ⟩⟩

Goal state after:
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 : α
tfae_3_to_2 : toIcoMod hp a b ≠ toIocMod hp a b → ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
tfae_4_to_3 : toIcoMod hp a b + p = toIocMod hp a b → toIcoMod hp a b ≠ toIocMod hp a b
tfae_1_to_4 : toIcoMod hp a b = a → toIcoMod hp a b + p = toIocMod hp a b
⊢ (∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)) → toIcoMod hp a b = a

Tactic:
← not_exists,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
tfae_3_to_2 : toIcoMod hp a b ≠ toIocMod hp a b → ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
tfae_4_to_3 : toIcoMod hp a b + p = toIocMod hp a b → toIcoMod hp a b ≠ toIocMod hp a b
tfae_1_to_4 : toIcoMod hp a b = a → toIcoMod hp a b + p = toIocMod hp a b
⊢ (¬∃ x, b - x • p ∈ Set.Ioo a (a + p)) → toIcoMod hp a b = a
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
⊢ closure (s ∩ t) ∩ (closure sᶜ ∪ closure tᶜ) ⊆
    closure s ∩ closure sᶜ ∩ closure t ∪ closure s ∩ (closure t ∩ closure tᶜ)

Tactic:
refine (inter_subset_inter_left _ (closure_inter_subset_inter_closure s t)).trans_eq ?_

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
⊢ closure s ∩ closure t ∩ (closure sᶜ ∪ closure tᶜ) =
    closure s ∩ closure sᶜ ∩ closure t ∪ closure s ∩ (closure t ∩ closure tᶜ)
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
ι : Sort u_3
p : ι → Prop
s : ι → Set X
F : Filter X
hF : F.HasBasis p s
⊢ ClusterPt x F ↔ ∀ (i : ι), p i → x ∈ closure[inst✝] (s i)

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

Goal state after:
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
⊢ ↑(toIcoDiv hp a b) * p - b = -toIcoMod hp a b

Tactic:
simpa using toIcoDiv_zsmul_sub_self hp a b

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : Archimedean α
a : α
⊢ ⋃ n, Ioc (a + ↑n) (a + ↑n + 1) = univ

Tactic:
simpa only [zsmul_one, Int.cast_add, Int.cast_one, ← add_assoc] using
    iUnion_Ioc_add_zsmul zero_lt_one a

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
t₂ : TopologicalSpace α
inst✝ : IndiscreteTopology α
s : Set α
h : s.Nonempty
⊢ Dense s

Tactic:
by
  simp [dense_iff_inter_open, IndiscreteTopology.isOpen_iff, h]

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: β : Type u_2
α : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
f : α → β
h : ∀ (b : β), IsOpen[inst✝²] (f ⁻¹' {b})
s : Set β
x✝ : IsOpen[inst✝¹] s
⊢ IsOpen[inst✝²] (f ⁻¹' s)

Tactic:
rw [← biUnion_of_singleton s, preimage_iUnion₂]
    exact isOpen_biUnion fun _ _ => h _

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
hf : IsCoinducing f
hf' : Injective f
⊢ IsOpenMap f

Tactic:
by
  intro s hs
  rwa [← hf.isOpen_preimage, preimage_image_eq _ hf']

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
T : TopologicalSpace α
f : β → α
hf : Surjective f
a : β
⊢ map f (𝓝 a) = 𝓝 (f a)

Tactic:
by
  rw [nhds_induced, map_comap_of_surjective hf]

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
hf : IsOpenMap f
x : X
l : Filter Y
h : ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
⊢ comap f (𝓟 {f x}ᶜ) ⊓ comap f l ≤ 𝓟 {x}ᶜ ⊓ comap f l

Tactic:
comap_principal,

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenMap f
x : X
l : Filter Y
h : ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
⊢ 𝓟 (f ⁻¹' {f x}ᶜ) ⊓ comap f l ≤ 𝓟 {x}ᶜ ⊓ comap f l
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
⊢ 𝓝 a ⊓ ⊥ = ⊥

Tactic:
inf_bot_eq

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
⊢ ⊥ = ⊥
Module: Mathlib.Topology.NhdsWithin

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

Tactic:
by rw [← sup_comm, nhdsNE_sup_pure]

Goal state after:
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) ⊓ comap Subtype.val (𝓟 t) = ⊥

Tactic:
comap_principal,

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
f : β → α
a : α
s : Set α
l : Filter β
h : ∀ (i : Set α), a ∈ i ∧ IsOpen[inst✝] i → Tendsto f l (𝓟 (i ∩ s))
⊢ ∀ᶠ (i : β) in l, f i ∈ s

Tactic:
tendsto_principal,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
f : β → α
a : α
s : Set α
l : Filter β
h : ∀ (i : Set α), a ∈ i ∧ IsOpen[inst✝] i → ∀ᶠ (a : β) in l, f a ∈ i ∩ s
⊢ ∀ᶠ (i : β) in l, f i ∈ s
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
⊢ s ∈ 𝓝ˢ t ↔ ∃ u ⊆ s, IsOpen[inst✝] u ∧ t ⊆ u

Tactic:
simp [← nhdsSetWithin_univ, mem_nhdsSetWithin, and_comm, and_assoc]

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set (X ⊕ Y)
⊢ IsClosed[instTopologicalSpaceSum] s ↔ IsClosed[inst✝¹] (inl ⁻¹' s) ∧ IsClosed[inst✝] (inr ⁻¹' s)

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

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
i : Set ι
s : (a : ι) → Set (A a)
x : (a : ι) → A a
hi : i.Finite
hs : ∀ a ∈ i, s a ∈ 𝓝 (x a)
⊢ i.pi s ∈ 𝓝 x

Tactic:
pi_def,

Goal state after:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
i : Set ι
s : (a : ι) → Set (A a)
x : (a : ι) → A a
hi : i.Finite
hs : ∀ a ∈ i, s a ∈ 𝓝 (x a)
⊢ ⋂ a ∈ i, eval a ⁻¹' s a ∈ 𝓝 x
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst✝ : DecidableEq ι
s : Set ((a : ι) → A a)
x y : (a : ι) → A a
hs : ∃ I t, (∀ (i : ι), t i ∈ 𝓝 (x i)) ∧ (↑I).pi t ⊆ s
⊢ ∃ I, I.piecewise x y ∈ s

Tactic:
rcases hs with ⟨I, t, htx, hts⟩

Goal state after:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst✝ : DecidableEq ι
s : Set ((a : ι) → A a)
x y : (a : ι) → A a
I : Finset ι
t : (i : ι) → Set (A i)
htx : ∀ (i : ι), t i ∈ 𝓝 (x i)
hts : (↑I).pi t ⊆ s
⊢ ∃ I, I.piecewise x y ∈ s
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝¹ : TopologicalSpace β
inst✝ : FirstCountableTopology β
f : α → β
hf : IsInducing f
⊢ FirstCountableTopology α

Tactic:
by
  rw [hf.1]
  exact firstCountableTopology_induced α β f

Goal state after:
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)
this : Countable ↑B
⊢ ∀ t' ∈ range fun i ↦ s i, t' ⊆ ⋃ i ∈ range f, s i

Tactic:
rintro _ ⟨i, rfl⟩ x xs

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
i : ι
x : α
xs : x ∈ (fun i ↦ s i) i
⊢ x ∈ ⋃ i ∈ range f, s i
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
s : Set ι
S : ι → Set X
hc : s.Countable
hcomp : ∀ i ∈ s, IsSigmaCompact (S i)
this : Countable ↑s
⊢ IsSigmaCompact (⋃ i ∈ s, S i)

Tactic:
rw [biUnion_eq_iUnion]

Goal state after:
X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
s : Set ι
S : ι → Set X
hc : s.Countable
hcomp : ∀ i ∈ s, IsSigmaCompact (S i)
this : Countable ↑s
⊢ IsSigmaCompact (⋃ x, S ↑x)
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Finite
hf : ∀ i ∈ s, IsCompact (f i)
l : Ultrafilter X
hl : ⋃ i ∈ s, f i ∈ l
⊢ ∃ x ∈ ⋃ i ∈ s, f i, ↑l ≤ 𝓝 x

Tactic:
rw [Ultrafilter.finite_biUnion_mem_iff hs] at hl
    rcases hl with ⟨i, his, hi⟩
    rcases (hf i his).ultrafilter_le_nhds _ (le_principal_iff.2 hi) with ⟨x, hxi, hlx⟩
    exact ⟨x, mem_iUnion₂.2 ⟨i, his, hxi⟩, hlx⟩

Goal state after:
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
S : Set (Set α)
⊢ upperClosure (⋃₀ S) = ⨅ s ∈ S, upperClosure s

Tactic:
by
  simp_rw [sUnion_eq_biUnion, upperClosure_iUnion]

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:
classical 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:
classical exact Lattice.toLinearOrder _

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

Goal state before:
pp: X : Type u
Y : Type v
ι : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s t : Set X
f : X → Y
inst✝ : NoncompactSpace X
i✝ : Set X
hs : i✝ = univ
⊢ ¬IsCompact univ

Tactic:
exact noncompact_univ X

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
x : X
y : Y
⊢ map mk (𝓝 x) ×ˢ map mk (𝓝 y) = 𝓝 (mk x, mk y)

Tactic:
map_mk_nhds,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
y : Y
⊢ 𝓝 (mk x) ×ˢ map mk (𝓝 y) = 𝓝 (mk x, mk y)
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
y : Y
⊢ 𝓝 (mk x) ×ˢ map mk (𝓝 y) = 𝓝 (mk x, mk y)

Tactic:
map_mk_nhds,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
y : Y
⊢ 𝓝 (mk x) ×ˢ 𝓝 (mk y) = 𝓝 (mk x, mk y)
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
b : Set (Set X)
hb : IsTopologicalBasis b
x y : X
h : ∀ s ∈ b, x ∈ s ↔ y ∈ s
⊢ (𝓝 y).HasBasis (fun t ↦ t ∈ b ∧ x ∈ t) fun t ↦ t

Tactic:
by
      convert! hb.nhds_hasBasis using 2
      exact and_congr_right (h _)

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsDiscrete s ↔ ∀ t ⊆ s, ∃ u, IsOpen[inst✝] u ∧ u ∩ s = t

Tactic:
by
  simp_rw [isDiscrete_iff_discreteTopology, discreteTopology_iff_forall_isOpen,
    isOpen_induced_iff, ← image_eq_image (Subtype.val_injective), Subtype.image_preimage_coe,
    Subtype.forall_set_subtype (p := fun t ↦ ∃ u, IsOpen u ∧ s ∩ u = t), inter_comm]

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

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 : IsDiscrete s
hf : IsInducing f
⊢ IsDiscrete (f '' s)

Tactic:
by
  simp_all [isDiscrete_iff_nhdsWithin, ← hf.map_nhdsWithin_eq s]

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s U : Set X
⊢ s ∈ codiscreteWithin U ↔ ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅

Tactic:
simp only [mem_codiscreteWithin, disjoint_principal_right]
  refine ⟨fun h z hz ↦ ⟨(U \ s)ᶜ, h z hz, by simp⟩, fun h z hz ↦ ?_⟩
  rw [← exists_mem_subset_iff]
  obtain ⟨t, h₁t, h₂t⟩ := h z hz
  use t, h₁t, (disjoint_iff_inter_eq_empty.mpr h₂t).subset_compl_right

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
π : X → Y
h : IsOpenQuotientMap π
⊢ IsClosed[instTopologicalSpaceProd] (diagonal Y) ↔ IsClosed[instTopologicalSpaceProd] {q | π q.1 = π q.2}

Tactic:
replace h := IsOpenQuotientMap.prodMap h h

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
π : X → Y
h : IsOpenQuotientMap (Prod.map π π)
⊢ IsClosed[instTopologicalSpaceProd] (diagonal Y) ↔ IsClosed[instTopologicalSpaceProd] {q | π q.1 = π q.2}